V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x✝ y✝ x y : V
r : ℝ
hr : 0 < r
⊢ arccos (inner x (r • y) / (‖x‖ * ‖r • y‖)) = arccos (inner x y / (‖x‖ * ‖y‖))
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x✝ y✝ x y : V
r : ℝ
hr : 0 < r
⊢ angle x (r • y) = angle x y
unfold angle
no goals
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x✝ y✝ x y : V
r : ℝ
hr : 0 < r
⊢ arccos (inner x (r • y) / (‖x‖ * ‖r • y‖)) = arccos (inner x y / (‖x‖ * ‖y‖))
rw [inner_smul_right, norm_smul, Real.norm_eq_abs, abs_of_nonneg (le_of_lt hr), ← mul_assoc,
  mul_comm _ r, mul_assoc, mul_div_mul_left _ _ (ne_of_gt hr)]