euler_four_square_identity.lean

import algebra.ring
import tactic

def sqr {α} [ring α] (a : α) := a * a

theorem euler_four_square_identity {α} [comm_ring α]
: ∀ a₁ a₂ a₃ a₄ b₁ b₂ b₃ b₄ : α, ∃ c₁ c₂ c₃ c₄ : α,
    (sqr a₁ + sqr a₂ + sqr a₃ + sqr a₄) * (sqr b₁ + sqr b₂ + sqr b₃ + sqr b₄)
    = (sqr c₁ + sqr c₂ + sqr c₃ + sqr c₄)
:= by {
  intros,
  use a₁ * b₁ - a₂ * b₂ - a₃ * b₃ - a₄ * b₄,
  use a₁ * b₂ + a₂ * b₁ + a₃ * b₄ - a₄ * b₃,
  use a₁ * b₃ - a₂ * b₄ + a₃ * b₁ + a₄ * b₂,
  use a₁ * b₄ + a₂ * b₃ - a₃ * b₂ + a₄ * b₁,
  dsimp [sqr],
  ring  -- Quite Easily Done, as an algebra teacher of mine used to say
}