𝕜 : Type ?u.2329716
E : Type ?u.2329719
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x : F
h : ↑re (inner x x) = ‖x‖ * ‖x‖
⊢ inner x x = ‖x‖ * ‖x‖
𝕜 : Type ?u.2329716
E : Type ?u.2329719
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x : F
⊢ inner x x = ‖x‖ * ‖x‖
have h := @inner_self_eq_norm_mul_norm ℝ F _ _ _ x
no goals
𝕜 : Type ?u.2329716
E : Type ?u.2329719
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x : F
h : ↑re (inner x x) = ‖x‖ * ‖x‖
⊢ inner x x = ‖x‖ * ‖x‖
simpa using h