𝕜 : Type ?u.1881062
E : Type ?u.1881065
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x y : F
⊢ inner y x * inner y x ≤ ‖inner y x * inner y x‖
𝕜 : Type ?u.1881062
E : Type ?u.1881065
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x y : F
⊢ inner x y * inner x y ≤ ‖inner x y‖ * ‖inner y x‖
rw [real_inner_comm y, ← norm_mul]
no goals
𝕜 : Type ?u.1881062
E : Type ?u.1881065
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x y : F
⊢ inner y x * inner y x ≤ ‖inner y x * inner y x‖
exact le_abs_self _