Lagrange four-square theorem

import Mathlib

theorem lagrange_four_squares (n : ℕ) : ∃ a b c d : ℕ, n = a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 := by 
  obtain ⟨a, b, c, d, h⟩  := Nat.sum_four_squares n
  use a, b, c, d
  rw [h]