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
⊢ secondInter s p v ∈ s ↔ p ∈ s
simp_rw [mem_sphere, Sphere.secondInter_dist]