𝕜 : Type ?u.3160254
E : Type ?u.3160257
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x : F
r : ℝ
hx : x ≠ 0
hr : r < 0
⊢ r * (‖x‖ * ‖x‖) ≠ 0
𝕜 : Type ?u.3160254
E : Type ?u.3160257
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x : F
r : ℝ
hx : x ≠ 0
hr : r < 0
⊢ inner x (r • x) / (‖x‖ * ‖r • x‖) = -1
rw [real_inner_smul_self_right, norm_smul, Real.norm_eq_abs, ← mul_assoc ‖x‖, mul_comm _ (|r|),
  mul_assoc, abs_of_neg hr, neg_mul, div_neg_eq_neg_div, div_self]
no goals
𝕜 : Type ?u.3160254
E : Type ?u.3160257
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x : F
r : ℝ
hx : x ≠ 0
hr : r < 0
⊢ r * (‖x‖ * ‖x‖) ≠ 0
exact mul_ne_zero hr.ne (mul_self_ne_zero.2 (norm_ne_zero_iff.2 hx))