𝕜 : Type ?u.3138511
E : Type ?u.3138514
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
⊢ abs (inner x y) / (‖x‖ * ‖y‖) ≤ 1
𝕜 : Type ?u.3138511
E : Type ?u.3138514
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
⊢ abs (inner x y / (‖x‖ * ‖y‖)) ≤ 1
rw [abs_div, abs_mul, abs_norm, abs_norm]
no goals
𝕜 : Type ?u.3138511
E : Type ?u.3138514
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
⊢ abs (inner x y) / (‖x‖ * ‖y‖) ≤ 1
exact div_le_one_of_le (abs_real_inner_le_norm x y) (mul_nonneg (norm_nonneg _) (norm_nonneg _))