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
⊢ dist ((-2 * inner v (p -ᵥ s.center) / inner v v) • v +ᵥ p) s.center = dist p s.center
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
⊢ dist (secondInter s p v) s.center = dist p s.center
rw [Sphere.secondInter]
case pos
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
hv : v = 0
⊢ dist ((-2 * inner v (p -ᵥ s.center) / inner v v) • v +ᵥ p) s.center = dist p s.center

case neg
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
hv : ¬v = 0
⊢ dist ((-2 * inner v (p -ᵥ s.center) / inner v v) • v +ᵥ p) s.center = dist p s.center
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
⊢ dist ((-2 * inner v (p -ᵥ s.center) / inner v v) • v +ᵥ p) s.center = dist p s.center
by_cases hv : v = 0
case neg
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
hv : ¬v = 0
⊢ -2 * inner v (p -ᵥ s.center) / inner v v = 0 ∨
    -2 * inner v (p -ᵥ s.center) / inner v v = -2 * inner v (p -ᵥ s.center) / inner v v
case neg
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
hv : ¬v = 0
⊢ dist ((-2 * inner v (p -ᵥ s.center) / inner v v) • v +ᵥ p) s.center = dist p s.center
rw [dist_smul_vadd_eq_dist _ _ hv]
no goals
case neg
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
hv : ¬v = 0
⊢ -2 * inner v (p -ᵥ s.center) / inner v v = 0 ∨
    -2 * inner v (p -ᵥ s.center) / inner v v = -2 * inner v (p -ᵥ s.center) / inner v v
exact Or.inr rfl
no goals
case pos
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
hv : v = 0
⊢ dist ((-2 * inner v (p -ᵥ s.center) / inner v v) • v +ᵥ p) s.center = dist p s.center
simp [hv]