no goals
n : ℕ
⊢ ∃ a b c d, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = n
induction n using Nat.recOnMul with
| h0 => exact ⟨0, 0, 0, 0, rfl⟩
| h1 => exact ⟨1, 0, 0, 0, rfl⟩
| hp p hp => exact hp.sum_four_squares
| h m n hm hn =>
  rcases hm with ⟨a, b, c, d, rfl⟩
  rcases hn with ⟨w, x, y, z, rfl⟩
  exact ⟨_, _, _, _, euler_four_squares _ _ _ _ _ _ _ _⟩
no goals
case h0

⊢ ∃ a b c d, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = 0
exact ⟨0, 0, 0, 0, rfl⟩
no goals
case h1

⊢ ∃ a b c d, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = 1
exact ⟨1, 0, 0, 0, rfl⟩
no goals
case hp
p : ℕ
hp : Prime p
⊢ ∃ a b c d, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = p
exact hp.sum_four_squares
case h.intro.intro.intro.intro
n : ℕ
hn : ∃ a b c d, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = n
a b c d : ℕ
⊢ ∃ a_1 b_1 c_1 d_1, a_1 ^ 2 + b_1 ^ 2 + c_1 ^ 2 + d_1 ^ 2 = (a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2) * n
case h
m n : ℕ
hm : ∃ a b c d, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = m
hn : ∃ a b c d, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = n
⊢ ∃ a b c d, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = m * n
rcases hm with ⟨a, b, c, d, rfl⟩
case h.intro.intro.intro.intro.intro.intro.intro.intro
a b c d w x y z : ℕ
⊢ ∃ a_1 b_1 c_1 d_1,
    a_1 ^ 2 + b_1 ^ 2 + c_1 ^ 2 + d_1 ^ 2 = (a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2) * (w ^ 2 + x ^ 2 + y ^ 2 + z ^ 2)
case h.intro.intro.intro.intro
n : ℕ
hn : ∃ a b c d, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = n
a b c d : ℕ
⊢ ∃ a_1 b_1 c_1 d_1, a_1 ^ 2 + b_1 ^ 2 + c_1 ^ 2 + d_1 ^ 2 = (a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2) * n
rcases hn with ⟨w, x, y, z, rfl⟩
no goals
case h.intro.intro.intro.intro.intro.intro.intro.intro
a b c d w x y z : ℕ
⊢ ∃ a_1 b_1 c_1 d_1,
    a_1 ^ 2 + b_1 ^ 2 + c_1 ^ 2 + d_1 ^ 2 = (a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2) * (w ^ 2 + x ^ 2 + y ^ 2 + z ^ 2)
exact ⟨_, _, _, _, euler_four_squares _ _ _ _ _ _ _ _⟩