V : Type u_2
P : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p : P
v : V
r : ℝ
hr : r ≠ 0
⊢ (-2 * (r * inner v (p -ᵥ s.center)) / r / r / inner v v * r) • v +ᵥ p =
    (-2 * inner v (p -ᵥ s.center) / inner v v) • v +ᵥ p
V : Type u_2
P : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p : P
v : V
r : ℝ
hr : r ≠ 0
⊢ secondInter s p (r • v) = secondInter s p v
simp_rw [Sphere.secondInter, real_inner_smul_left, inner_smul_right, smul_smul,
  div_mul_eq_div_div]
no goals
V : Type u_2
P : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p : P
v : V
r : ℝ
hr : r ≠ 0
⊢ (-2 * (r * inner v (p -ᵥ s.center)) / r / r / inner v v * r) • v +ᵥ p =
    (-2 * inner v (p -ᵥ s.center) / inner v v) • v +ᵥ p
rw [mul_comm, ← mul_div_assoc, ← mul_div_assoc, mul_div_cancel_left _ hr, mul_comm, mul_assoc,
  mul_div_cancel_left _ hr, mul_comm]