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₂ : P
hp₁ : p₁ ∈ s
hp₂ : dist p₂ s.center ≤ s.radius
h : p₁ = p₂
⊢ 0 < inner (p₁ -ᵥ p₂) (p₁ -ᵥ s.center) ∨ p₁ = p₂

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₂ : P
hp₁ : p₁ ∈ s
hp₂ : dist p₂ s.center ≤ s.radius
h : ¬p₁ = p₂
⊢ 0 < inner (p₁ -ᵥ p₂) (p₁ -ᵥ s.center) ∨ p₁ = 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₂ : P
hp₁ : p₁ ∈ s
hp₂ : dist p₂ s.center ≤ s.radius
⊢ 0 < inner (p₁ -ᵥ p₂) (p₁ -ᵥ s.center) ∨ p₁ = p₂
by_cases h : p₁ = p₂
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₂ : P
hp₁ : p₁ ∈ s
hp₂ : dist p₂ s.center ≤ s.radius
h : ¬p₁ = p₂
⊢ 0 < inner (p₁ -ᵥ p₂) (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₂ : P
hp₁ : p₁ ∈ s
hp₂ : dist p₂ s.center ≤ s.radius
h : ¬p₁ = p₂
⊢ 0 < inner (p₁ -ᵥ p₂) (p₁ -ᵥ s.center) ∨ p₁ = p₂
refine' Or.inl _
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₂ : P
hp₁ : dist p₁ s.center = s.radius
hp₂ : dist p₂ s.center ≤ s.radius
h : ¬p₁ = p₂
⊢ 0 < inner (p₁ -ᵥ p₂) (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₂ : P
hp₁ : p₁ ∈ s
hp₂ : dist p₂ s.center ≤ s.radius
h : ¬p₁ = p₂
⊢ 0 < inner (p₁ -ᵥ p₂) (p₁ -ᵥ s.center)
rw [mem_sphere] at hp₁
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₂ : P
hp₁ : dist p₁ s.center = s.radius
hp₂ : dist p₂ s.center ≤ s.radius
h : ¬p₁ = p₂
⊢ inner (p₂ -ᵥ s.center) (p₁ -ᵥ s.center) < ‖p₁ -ᵥ s.center‖ * ‖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₂ : P
hp₁ : dist p₁ s.center = s.radius
hp₂ : dist p₂ s.center ≤ s.radius
h : ¬p₁ = p₂
⊢ 0 < inner (p₁ -ᵥ p₂) (p₁ -ᵥ s.center)
rw [← vsub_sub_vsub_cancel_right p₁ p₂ s.center, inner_sub_left,
  real_inner_self_eq_norm_mul_norm, sub_pos]
case neg.refine'_1
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₂ : P
hp₁ : dist p₁ s.center = s.radius
hp₂ : dist p₂ s.center ≤ s.radius
h : ¬p₁ = p₂
⊢ ‖p₂ -ᵥ s.center‖ ≤ ‖p₁ -ᵥ s.center‖

case neg.refine'_2
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₂ : P
hp₁ : dist p₁ s.center = s.radius
hp₂ : dist p₂ s.center ≤ s.radius
h : ¬p₁ = p₂
⊢ inner (p₂ -ᵥ s.center) (p₁ -ᵥ s.center) ≠ ‖p₁ -ᵥ s.center‖ * ‖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₂ : P
hp₁ : dist p₁ s.center = s.radius
hp₂ : dist p₂ s.center ≤ s.radius
h : ¬p₁ = p₂
⊢ inner (p₂ -ᵥ s.center) (p₁ -ᵥ s.center) < ‖p₁ -ᵥ s.center‖ * ‖p₁ -ᵥ s.center‖
refine'
  lt_of_le_of_ne ((real_inner_le_norm _ _).trans (mul_le_mul_of_nonneg_right _ (norm_nonneg _))) _
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₂ : P
hp₁ : p₁ ∈ s
hp₂ : dist p₂ s.center ≤ s.radius
h : p₁ = p₂
⊢ 0 < inner (p₁ -ᵥ p₂) (p₁ -ᵥ s.center) ∨ p₁ = p₂
exact Or.inr h
no goals
case neg.refine'_1
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₂ : P
hp₁ : dist p₁ s.center = s.radius
hp₂ : dist p₂ s.center ≤ s.radius
h : ¬p₁ = p₂
⊢ ‖p₂ -ᵥ s.center‖ ≤ ‖p₁ -ᵥ s.center‖
rwa [← dist_eq_norm_vsub, ← dist_eq_norm_vsub, hp₁]
case neg.refine'_2.inl
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₂ : P
hp₁ : dist p₁ s.center = s.radius
hp₂ : dist p₂ s.center ≤ s.radius
h : ¬p₁ = p₂
hp₂' : dist p₂ s.center < s.radius
⊢ inner (p₂ -ᵥ s.center) (p₁ -ᵥ s.center) ≠ ‖p₁ -ᵥ s.center‖ * ‖p₁ -ᵥ s.center‖

case neg.refine'_2.inr
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₂ : P
hp₁ : dist p₁ s.center = s.radius
hp₂ : dist p₂ s.center ≤ s.radius
h : ¬p₁ = p₂
hp₂' : dist p₂ s.center = s.radius
⊢ inner (p₂ -ᵥ s.center) (p₁ -ᵥ s.center) ≠ ‖p₁ -ᵥ s.center‖ * ‖p₁ -ᵥ s.center‖
case neg.refine'_2
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₂ : P
hp₁ : dist p₁ s.center = s.radius
hp₂ : dist p₂ s.center ≤ s.radius
h : ¬p₁ = p₂
⊢ inner (p₂ -ᵥ s.center) (p₁ -ᵥ s.center) ≠ ‖p₁ -ᵥ s.center‖ * ‖p₁ -ᵥ s.center‖
rcases hp₂.lt_or_eq with (hp₂' | hp₂')
case neg.refine'_2.inl.refine'_1
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₂ : P
hp₁ : dist p₁ s.center = s.radius
hp₂ : dist p₂ s.center ≤ s.radius
h : ¬p₁ = p₂
hp₂' : dist p₂ s.center < s.radius
⊢ ‖p₂ -ᵥ s.center‖ < ‖p₁ -ᵥ s.center‖

case neg.refine'_2.inl.refine'_2
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₂ : P
hp₁ : dist p₁ s.center = s.radius
hp₂ : dist p₂ s.center ≤ s.radius
h : ¬p₁ = p₂
hp₂' : dist p₂ s.center < s.radius
⊢ 0 < ‖p₁ -ᵥ s.center‖
case neg.refine'_2.inl
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₂ : P
hp₁ : dist p₁ s.center = s.radius
hp₂ : dist p₂ s.center ≤ s.radius
h : ¬p₁ = p₂
hp₂' : dist p₂ s.center < s.radius
⊢ inner (p₂ -ᵥ s.center) (p₁ -ᵥ s.center) ≠ ‖p₁ -ᵥ s.center‖ * ‖p₁ -ᵥ s.center‖
refine' ((real_inner_le_norm _ _).trans_lt (mul_lt_mul_of_pos_right _ _)).ne
no goals
case neg.refine'_2.inl.refine'_1
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₂ : P
hp₁ : dist p₁ s.center = s.radius
hp₂ : dist p₂ s.center ≤ s.radius
h : ¬p₁ = p₂
hp₂' : dist p₂ s.center < s.radius
⊢ ‖p₂ -ᵥ s.center‖ < ‖p₁ -ᵥ s.center‖
rwa [← hp₁, @dist_eq_norm_vsub V, @dist_eq_norm_vsub V] at hp₂'
case neg.refine'_2.inl.refine'_2
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₂ : P
hp₁ : dist p₁ s.center = s.radius
hp₂ : dist p₂ s.center ≤ s.radius
h : ¬p₁ = p₂
hp₂' : dist p₂ s.center < s.radius
⊢ p₁ ≠ s.center
case neg.refine'_2.inl.refine'_2
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₂ : P
hp₁ : dist p₁ s.center = s.radius
hp₂ : dist p₂ s.center ≤ s.radius
h : ¬p₁ = p₂
hp₂' : dist p₂ s.center < s.radius
⊢ 0 < ‖p₁ -ᵥ s.center‖
rw [norm_pos_iff, vsub_ne_zero]
case neg.refine'_2.inl.refine'_2
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
hp₂ : dist p₂ s.center ≤ s.radius
hp₂' : dist p₂ s.center < s.radius
hp₁ : dist s.center s.center = s.radius
h : ¬s.center = p₂
⊢ False
case neg.refine'_2.inl.refine'_2
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₂ : P
hp₁ : dist p₁ s.center = s.radius
hp₂ : dist p₂ s.center ≤ s.radius
h : ¬p₁ = p₂
hp₂' : dist p₂ s.center < s.radius
⊢ p₁ ≠ s.center
rintro rfl
case neg.refine'_2.inl.refine'_2
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
hp₂ : dist p₂ s.center ≤ s.radius
hp₂' : dist p₂ s.center < dist s.center s.center
hp₁ : dist s.center s.center = s.radius
h : ¬s.center = p₂
⊢ False
case neg.refine'_2.inl.refine'_2
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
hp₂ : dist p₂ s.center ≤ s.radius
hp₂' : dist p₂ s.center < s.radius
hp₁ : dist s.center s.center = s.radius
h : ¬s.center = p₂
⊢ False
rw [← hp₁] at hp₂'
case neg.refine'_2.inl.refine'_2
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
hp₂ : dist p₂ s.center ≤ s.radius
hp₂' : dist p₂ s.center < dist s.center s.center
hp₁ : dist s.center s.center = s.radius
h : ¬s.center = p₂
⊢ dist p₂ s.center < 0
case neg.refine'_2.inl.refine'_2
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
hp₂ : dist p₂ s.center ≤ s.radius
hp₂' : dist p₂ s.center < dist s.center s.center
hp₁ : dist s.center s.center = s.radius
h : ¬s.center = p₂
⊢ False
refine' (dist_nonneg.not_lt : ¬dist p₂ s.center < 0) _
no goals
case neg.refine'_2.inl.refine'_2
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
hp₂ : dist p₂ s.center ≤ s.radius
hp₂' : dist p₂ s.center < dist s.center s.center
hp₁ : dist s.center s.center = s.radius
h : ¬s.center = p₂
⊢ dist p₂ s.center < 0
simpa using hp₂'
case neg.refine'_2.inr
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₂ : P
hp₁ : dist p₁ s.center = s.radius
hp₂ : dist p₂ s.center ≤ s.radius
h : ¬p₁ = p₂
hp₂' : ‖p₂ -ᵥ s.center‖ = ‖p₁ -ᵥ s.center‖
⊢ inner (p₂ -ᵥ s.center) (p₁ -ᵥ s.center) ≠ ‖p₁ -ᵥ s.center‖ * ‖p₁ -ᵥ s.center‖
case neg.refine'_2.inr
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₂ : P
hp₁ : dist p₁ s.center = s.radius
hp₂ : dist p₂ s.center ≤ s.radius
h : ¬p₁ = p₂
hp₂' : dist p₂ s.center = s.radius
⊢ inner (p₂ -ᵥ s.center) (p₁ -ᵥ s.center) ≠ ‖p₁ -ᵥ s.center‖ * ‖p₁ -ᵥ s.center‖
rw [← hp₁, @dist_eq_norm_vsub V, @dist_eq_norm_vsub V] at hp₂'
case neg.refine'_2.inr
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₂ : P
hp₁ : dist p₁ s.center = s.radius
hp₂ : dist p₂ s.center ≤ s.radius
h : ¬p₁ = p₂
hp₂' : ‖p₂ -ᵥ s.center‖ = ‖p₁ -ᵥ s.center‖
⊢ inner (p₂ -ᵥ s.center) (p₁ -ᵥ s.center) ≠ ‖p₂ -ᵥ s.center‖ * ‖p₁ -ᵥ s.center‖
case neg.refine'_2.inr
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₂ : P
hp₁ : dist p₁ s.center = s.radius
hp₂ : dist p₂ s.center ≤ s.radius
h : ¬p₁ = p₂
hp₂' : ‖p₂ -ᵥ s.center‖ = ‖p₁ -ᵥ s.center‖
⊢ inner (p₂ -ᵥ s.center) (p₁ -ᵥ s.center) ≠ ‖p₁ -ᵥ s.center‖ * ‖p₁ -ᵥ s.center‖
nth_rw 1 [← hp₂']
case neg.refine'_2.inr
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₂ : P
hp₁ : dist p₁ s.center = s.radius
hp₂ : dist p₂ s.center ≤ s.radius
h : ¬p₁ = p₂
hp₂' : ‖p₂ -ᵥ s.center‖ = ‖p₁ -ᵥ s.center‖
⊢ p₁ ≠ s.center
case neg.refine'_2.inr
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₂ : P
hp₁ : dist p₁ s.center = s.radius
hp₂ : dist p₂ s.center ≤ s.radius
h : ¬p₁ = p₂
hp₂' : ‖p₂ -ᵥ s.center‖ = ‖p₁ -ᵥ s.center‖
⊢ inner (p₂ -ᵥ s.center) (p₁ -ᵥ s.center) ≠ ‖p₂ -ᵥ s.center‖ * ‖p₁ -ᵥ s.center‖
rw [Ne.def, inner_eq_norm_mul_iff_real, hp₂', ← sub_eq_zero, ← smul_sub,
  vsub_sub_vsub_cancel_right, ← Ne.def, smul_ne_zero_iff, vsub_ne_zero,
  and_iff_left (Ne.symm h), norm_ne_zero_iff, vsub_ne_zero]
case neg.refine'_2.inr
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
hp₂ : dist p₂ s.center ≤ s.radius
hp₁ : dist s.center s.center = s.radius
h : ¬s.center = p₂
hp₂' : ‖p₂ -ᵥ s.center‖ = ‖s.center -ᵥ s.center‖
⊢ False
case neg.refine'_2.inr
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₂ : P
hp₁ : dist p₁ s.center = s.radius
hp₂ : dist p₂ s.center ≤ s.radius
h : ¬p₁ = p₂
hp₂' : ‖p₂ -ᵥ s.center‖ = ‖p₁ -ᵥ s.center‖
⊢ p₁ ≠ s.center
rintro rfl
case neg.refine'_2.inr
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
hp₂ : dist p₂ s.center ≤ s.radius
hp₁ : dist s.center s.center = s.radius
h : ¬s.center = p₂
hp₂' : ‖p₂ -ᵥ s.center‖ = ‖s.center -ᵥ s.center‖
⊢ p₂ = s.center
case neg.refine'_2.inr
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
hp₂ : dist p₂ s.center ≤ s.radius
hp₁ : dist s.center s.center = s.radius
h : ¬s.center = p₂
hp₂' : ‖p₂ -ᵥ s.center‖ = ‖s.center -ᵥ s.center‖
⊢ False
refine' h (Eq.symm _)
no goals
case neg.refine'_2.inr
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
hp₂ : dist p₂ s.center ≤ s.radius
hp₁ : dist s.center s.center = s.radius
h : ¬s.center = p₂
hp₂' : ‖p₂ -ᵥ s.center‖ = ‖s.center -ᵥ s.center‖
⊢ p₂ = s.center
simpa using hp₂'