𝕜 : Type u_2
E : Type u_1
F : Type ?u.2369823
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
𝕜 : Type u_2
E : Type u_1
F : Type ?u.2369823
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x y : E
⊢ ‖x + y‖ * ‖x + y‖ = ‖x‖ * ‖x‖ + 2 * ↑re (inner x y) + ‖y‖ * ‖y‖
repeat' rw [← sq (M := ℝ)]
no goals
𝕜 : Type u_2
E : Type u_1
F : Type ?u.2369823
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
exact norm_add_sq _ _
𝕜 : Type u_2
E : Type u_1
F : Type ?u.2369823
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
𝕜 : Type u_2
E : Type u_1
F : Type ?u.2369823
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
rw [← sq (M := ℝ)]