𝕜 : Type u_1
E : Type u_2
F : Type ?u.2478434
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x y : E
⊢ ‖inner x y‖ ≤ sqrt (↑re (inner x x)) * sqrt (↑re (inner y y))
𝕜 : Type u_1
E : Type u_2
F : Type ?u.2478434
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x y : E
⊢ ‖inner x y‖ ≤ ‖x‖ * ‖y‖
rw [norm_eq_sqrt_inner (𝕜 := 𝕜) x, norm_eq_sqrt_inner (𝕜 := 𝕜) y]
𝕜 : Type u_1
E : Type u_2
F : Type ?u.2478434
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x y : E
this : InnerProductSpace.Core 𝕜 E := InnerProductSpace.toCore
⊢ ‖inner x y‖ ≤ sqrt (↑re (inner x x)) * sqrt (↑re (inner y y))
𝕜 : Type u_1
E : Type u_2
F : Type ?u.2478434
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x y : E
⊢ ‖inner x y‖ ≤ sqrt (↑re (inner x x)) * sqrt (↑re (inner y y))
letI : InnerProductSpace.Core 𝕜 E := InnerProductSpace.toCore
no goals
𝕜 : Type u_1
E : Type u_2
F : Type ?u.2478434
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x y : E
this : InnerProductSpace.Core 𝕜 E := InnerProductSpace.toCore
⊢ ‖inner x y‖ ≤ sqrt (↑re (inner x x)) * sqrt (↑re (inner y y))
exact InnerProductSpace.Core.norm_inner_le_norm x y