V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x✝ y✝ x y : V
⊢ inner x y / (‖x‖ * ‖y‖) ≤ 1
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x✝ y✝ x y : V
⊢ angle x y = 0 ↔ x ≠ 0 ∧ ∃ r, 0 < r ∧ y = r • x
rw [angle, ← real_inner_div_norm_mul_norm_eq_one_iff, Real.arccos_eq_zero, LE.le.le_iff_eq,
  eq_comm]
no goals
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x✝ y✝ x y : V
⊢ inner x y / (‖x‖ * ‖y‖) ≤ 1
exact (abs_le.mp (abs_real_inner_div_norm_mul_norm_le_one x y)).2