𝕜 : Type u_2
E : Type u_1
F : Type ?u.2331497
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x y : E
⊢ ↑re (inner (x + y) (x + y)) = ↑re (inner x x) + 2 * ↑re (inner x y) + ↑re (inner y y)
𝕜 : Type u_2
E : Type u_1
F : Type ?u.2331497
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x y : E
⊢ ‖x + y‖ ^ 2 = ‖x‖ ^ 2 + 2 * ↑re (inner x y) + ‖y‖ ^ 2
repeat' rw [sq (M := ℝ), ← @inner_self_eq_norm_mul_norm 𝕜]
𝕜 : Type u_2
E : Type u_1
F : Type ?u.2331497
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x y : E
⊢ ↑re (inner x x + inner x y + inner y x + inner y y) =
    ↑re (inner x x) + (↑re (inner x y) + ↑re (inner x y)) + ↑re (inner y y)
𝕜 : Type u_2
E : Type u_1
F : Type ?u.2331497
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x y : E
⊢ ↑re (inner (x + y) (x + y)) = ↑re (inner x x) + 2 * ↑re (inner x y) + ↑re (inner y y)
rw [inner_add_add_self, two_mul]
𝕜 : Type u_2
E : Type u_1
F : Type ?u.2331497
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x y : E
⊢ ↑re (inner y x) = ↑re (inner x y)
𝕜 : Type u_2
E : Type u_1
F : Type ?u.2331497
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x y : E
⊢ ↑re (inner x x + inner x y + inner y x + inner y y) =
    ↑re (inner x x) + (↑re (inner x y) + ↑re (inner x y)) + ↑re (inner y y)
simp only [add_assoc, add_left_inj, add_right_inj, AddMonoidHom.map_add]
no goals
𝕜 : Type u_2
E : Type u_1
F : Type ?u.2331497
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x y : E
⊢ ↑re (inner y x) = ↑re (inner x y)
rw [← inner_conj_symm, conj_re]
𝕜 : Type u_2
E : Type u_1
F : Type ?u.2331497
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x y : E
⊢ ↑re (inner (x + y) (x + y)) = ↑re (inner x x) + 2 * ↑re (inner x y) + ↑re (inner y y)
𝕜 : Type u_2
E : Type u_1
F : Type ?u.2331497
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x y : E
⊢ ↑re (inner (x + y) (x + y)) = ↑re (inner x x) + 2 * ↑re (inner x y) + ↑re (inner y y)
rw [sq (M := ℝ), ← @inner_self_eq_norm_mul_norm 𝕜]