𝕜 : Type u_1
E : Type u_2
F : Type ?u.1814317
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x y : E
⊢ inner x x + inner x y + inner y x + inner y y + (inner x x - inner x y - inner y x + inner y y) =
    2 * (inner x x + inner y y)
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1814317
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x y : E
⊢ inner (x + y) (x + y) + inner (x - y) (x - y) = 2 * (inner x x + inner y y)
simp only [inner_add_add_self, inner_sub_sub_self]
no goals
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1814317
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x y : E
⊢ inner x x + inner x y + inner y x + inner y y + (inner x x - inner x y - inner y x + inner y y) =
    2 * (inner x x + inner y y)
ring