𝕜 : Type u_1
E : Type u_2
F : Type ?u.1652408
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x : E
⊢ ↑re (inner x x) = ‖↑(↑re (inner x x))‖
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1652408
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‖
conv_rhs => rw [← inner_self_ofReal_re]
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1652408
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x : E
⊢ ‖↑(↑re (inner x x))‖ = ↑re (inner x x)
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1652408
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x : E
⊢ ↑re (inner x x) = ‖↑(↑re (inner x x))‖
symm
no goals
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1652408
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x : E
⊢ ‖↑(↑re (inner x x))‖ = ↑re (inner x x)
exact norm_of_nonneg inner_self_nonneg