Theorem: Imo1998P2.add_sq_add_sq_sub (Compfiles/Imo1998P2.lean)

State before:
C : Type u_1
J : Type u_2
r : C → J → Prop
α : Type u_3
inst✝ : Ring α
x y : α
⊢ (x + y) * (x + y) + (x - y) * (x - y) = 2 * x * x + 2 * y * y
Tactic:
noncomm_ring
State after:
no goals