𝕜 : Type u_1
E : Type u_2
F : Type ?u.1684989
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x : E
⊢ ↑(↑re (inner x x)) = inner x x
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1684989
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x : E
⊢ ↑‖inner x x‖ = inner x x
rw [← inner_self_re_eq_norm]
no goals
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1684989
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x : E
⊢ ↑(↑re (inner x x)) = inner x x
exact inner_self_ofReal_re _