awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
p₁ p₂ p : P
s : Sphere P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
o : P := s.center
t : ℝ
hpt : (AffineMap.lineMap p₁ p₂ : (a : ℝ) → P) t = p
ht₀ : 0 ≤ t
ht₁ : t ≤ 1
hne₁ : p ≠ p₁
hne₂ : p ≠ p₂
ht₀' : 0 < t
ht₁' : t < 1
u : V := p₁ -ᵥ o
v : V := p₂ -ᵥ o
hu : ‖u‖ = s.radius
hv : ‖v‖ = s.radius
huv : u ≠ v
hpo : p -ᵥ o = (1 - t) • u + t • v
⊢ Membership.mem (γ := Set V) (Metric.closedBall 0 s.radius) v

Tactic:
simp [Metric.mem_closedBall, hv]

Premises used: Metric.mem_closedBall
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
p₁ p₂ p : P
s : Sphere P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
o : P := s.center
t : ℝ
hpt : (AffineMap.lineMap p₁ p₂ : (a : ℝ) → P) t = p
ht₀ : 0 ≤ t
ht₁ : t ≤ 1
hne₁ : p ≠ p₁
hne₂ : p ≠ p₂
ht₀' : 0 < t
ht₁' : t < 1
u : V := p₁ -ᵥ o
v : V := p₂ -ᵥ o
hu : ‖u‖ = s.radius
hv : ‖v‖ = s.radius
huv : u ≠ v
hpo : p -ᵥ o = (1 - t) • u + t • v
⊢ Membership.mem (γ := Set V) (interior (Metric.closedBall 0 s.radius)) ((1 - t) • u + t • v)

Tactic:
have hmem := (strictConvex_closedBall ℝ (0 : V) s.radius)
    (by simp [Metric.mem_closedBall, hu]) (by simp [Metric.mem_closedBall, hv])
    huv (sub_pos.mpr ht₁') ht₀' (sub_add_cancel 1 t)
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
p₁ p₂ p : P
s : Sphere P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
o : P := s.center
t : ℝ
hpt : (AffineMap.lineMap p₁ p₂ : (a : ℝ) → P) t = p
ht₀ : 0 ≤ t
ht₁ : t ≤ 1
hne₁ : p ≠ p₁
hne₂ : p ≠ p₂
ht₀' : 0 < t
ht₁' : t < 1
u : V := p₁ -ᵥ o
v : V := p₂ -ᵥ o
hu : ‖u‖ = s.radius
hv : ‖v‖ = s.radius
huv : u ≠ v
hpo : p -ᵥ o = (1 - t) • u + t • v
hmem : Membership.mem (γ := Set V) (interior (Metric.closedBall 0 s.radius)) ((1 - t) • u + t • v)
rwa :
  ∀ (hmem : Membership.mem (γ := Set V) (Metric.ball 0 s.radius) ((1 - t) • u + t • v)),
    ‖(1 - t) • u + t • v‖ < s.radius
rwa₁ : ∀ (hmem : dist ((1 - t) • u + t • v) 0 < s.radius), ‖(1 - t) • u + t • v‖ < s.radius
rwa₂ rwa₃ rwa₄ rwa₅ : ∀ (hmem : ‖(1 - t) • u + t • v‖ < s.radius), ‖(1 - t) • u + t • v‖ < s.radius
⊢ ‖(1 - t) • u + t • v‖ < s.radius

Tactic:
rwa [interior_closedBall _ (fun h : s.radius = 0 => huv <|
      (norm_eq_zero.mp (hu.trans h)).trans (norm_eq_zero.mp (hv.trans h)).symm),
    Metric.mem_ball, dist_zero_right] at hmem

Premises used: norm_eq_zero, interior_closedBall, Metric.mem_ball, Iff.mp, Eq.symm, dist_zero_right, Eq.trans
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
p₁ p₂ : P
s : Sphere P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₁p₂ : p₁ ≠ p₂
⊢ dist s.center (midpoint ℝ p₁ p₂) < s.radius

Tactic:
s.dist_center_lt_radius_of_sbtw hp₁ hp₂ (sbtw_midpoint_of_ne ℝ hp₁p₂)

Premises used: Real, sbtw_midpoint_of_ne, EuclideanGeometry.Sphere.dist_center_lt_radius_of_sbtw
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst_4 : FiniteDimensional.{0, u_1} ℝ ↥s.direction
hd : finrank.{0, u_1} ℝ ↥s.direction = 2
s₁ s₂ : Sphere P
p₁ p₂ p : P
hs₁ : s₁.center ∈ s
hs₂ : s₂.center ∈ s
hp₁s : p₁ ∈ s
hp₂s : p₂ ∈ s
hps : p ∈ s
hs : s₁ ≠ s₂
hp : p₁ ≠ p₂
hp₁s₁ : p₁ ∈ s₁
hp₂s₁ : p₂ ∈ s₁
hps₁ : p ∈ s₁
hp₁s₂ : p₁ ∈ s₂
hp₂s₂ : p₂ ∈ s₂
hps₂ : p ∈ s₂
⊢ p = p₁ ∨ p = p₂

Tactic:
eq_of_dist_eq_of_dist_eq_of_mem_of_finrank_eq_two hd hs₁ hs₂ hp₁s hp₂s hps
    ((Sphere.center_ne_iff_ne_of_mem hps₁ hps₂).2 hs) hp hp₁s₁ hp₂s₁ hps₁ hp₁s₂ hp₂s₂ hps₂

Premises used: Iff.mpr, EuclideanGeometry.Sphere.center_ne_iff_ne_of_mem, EuclideanGeometry.eq_of_dist_eq_of_dist_eq_of_mem_of_finrank_eq_two
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
inst_4 : FiniteDimensional ℝ V
hd : finrank ℝ V = 2
s₁ s₂ : Sphere P
p₁ p₂ p : P
hs : s₁ ≠ s₂
hp : p₁ ≠ p₂
hp₁s₁ : p₁ ∈ s₁
hp₂s₁ : p₂ ∈ s₁
hps₁ : p ∈ s₁
hp₁s₂ : p₁ ∈ s₂
hp₂s₂ : p₂ ∈ s₂
hps₂ : p ∈ s₂
⊢ p = p₁ ∨ p = p₂

Tactic:
eq_of_dist_eq_of_dist_eq_of_finrank_eq_two hd ((Sphere.center_ne_iff_ne_of_mem hps₁ hps₂).2 hs) hp
    hp₁s₁ hp₂s₁ hps₁ hp₁s₂ hp₂s₂ hps₂

Premises used: Iff.mpr, EuclideanGeometry.Sphere.center_ne_iff_ne_of_mem, EuclideanGeometry.eq_of_dist_eq_of_dist_eq_of_finrank_eq_two
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s : Sphere P
p₁ p₂ : P
hp₁ : p₁ ∈ s
hp₂ : dist p₂ s.center ≤ s.radius
pos : ∀ (h : p₁ = p₂), 0 < ⟪p₁ -ᵥ p₂, p₁ -ᵥ s.center⟫ ∨ p₁ = p₂
neg : ∀ (h : ¬p₁ = p₂), 0 < ⟪p₁ -ᵥ p₂, p₁ -ᵥ s.center⟫ ∨ p₁ = p₂
⊢ 0 < ⟪p₁ -ᵥ p₂, p₁ -ᵥ s.center⟫ ∨ p₁ = p₂

Tactic:
by_cases h : p₁ = p₂
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s : Sphere P
p₁ p₂ : P
hp₁ : p₁ ∈ s
hp₂ : dist p₂ s.center ≤ s.radius
h : p₁ = p₂
⊢ 0 < ⟪p₁ -ᵥ p₂, p₁ -ᵥ s.center⟫ ∨ p₁ = p₂

Tactic:
Or.inr h

Premises used: Or.inr
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s : Sphere P
p₁ p₂ : P
hp₁ : p₁ ∈ s
hp₂ : dist p₂ s.center ≤ s.radius
h : p₁ = p₂
⊢ 0 < ⟪p₁ -ᵥ p₂, p₁ -ᵥ s.center⟫ ∨ p₁ = p₂

Tactic:
exact Or.inr h

Premises used: Or.inr
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s : Sphere P
p₁ p₂ : P
hp₁ : p₁ ∈ s
hp₂ : dist p₂ s.center ≤ s.radius
h : ¬p₁ = p₂
⊢ 0 < ⟪p₁ -ᵥ p₂, p₁ -ᵥ s.center⟫ ∨ p₁ = p₂

Tactic:
Or.inl ?_

Premises used: Or.inl
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s : Sphere P
p₁ p₂ : P
hp₁ : p₁ ∈ s
hp₂ : dist p₂ s.center ≤ s.radius
h : ¬p₁ = p₂
neg : 0 < ⟪p₁ -ᵥ p₂, p₁ -ᵥ s.center⟫
⊢ 0 < ⟪p₁ -ᵥ p₂, p₁ -ᵥ s.center⟫ ∨ p₁ = p₂

Tactic:
refine Or.inl ?_

Premises used: Or.inl
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s : Sphere P
p₁ p₂ : P
hp₁ : p₁ ∈ s
hp₂ : dist p₂ s.center ≤ s.radius
h : ¬p₁ = p₂
⊢ dist p₁ s.center = s.radius

Tactic:
rw [mem_sphere] at hp₁

Premises used: EuclideanGeometry.mem_sphere
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s : Sphere P
p₁ p₂ : P
hp₁ : p₁ ∈ s
hp₂ : dist p₂ s.center ≤ s.radius
h : ¬p₁ = p₂
hp₃ : dist p₁ s.center = s.radius
⊢ dist p₂ s.center ≤ s.radius

Tactic:
rw [mem_sphere] at hp₁

Premises used: EuclideanGeometry.mem_sphere
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s : Sphere P
p₁ p₂ : P
hp₁ : p₁ ∈ s
hp₂ : dist p₂ s.center ≤ s.radius
h : ¬p₁ = p₂
hp₃ : dist p₁ s.center = s.radius
hp₄ : dist p₂ s.center ≤ s.radius
⊢ ¬p₁ = p₂

Tactic:
rw [mem_sphere] at hp₁

Premises used: EuclideanGeometry.mem_sphere
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : 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₂
neg : ⟪p₂ -ᵥ s.center, p₁ -ᵥ s.center⟫ < ‖p₁ -ᵥ s.center‖ * ‖p₁ -ᵥ s.center‖
⊢ 0 < ⟪p₁ -ᵥ p₂, p₁ -ᵥ s.center⟫

Tactic:
rw [← vsub_sub_vsub_cancel_right p₁ p₂ s.center, inner_sub_left,
    real_inner_self_eq_norm_mul_norm, sub_pos]

Premises used: sub_pos, inner_sub_left, EuclideanGeometry.Sphere.center, vsub_sub_vsub_cancel_right, real_inner_self_eq_norm_mul_norm
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : 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⟫ < ‖p₁ -ᵥ s.center‖ * ‖p₁ -ᵥ s.center‖

Tactic:
lt_of_le_of_ne
    ((real_inner_le_norm _ _).trans (mul_le_mul_of_nonneg_right ?_ (norm_nonneg _))) ?_

Premises used: real_inner_le_norm, mul_le_mul_of_nonneg_right, LE.le.trans, norm_nonneg, lt_of_le_of_ne
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : 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₂
neg : ‖p₂ -ᵥ s.center‖ ≤ ‖p₁ -ᵥ s.center‖
neg₁ : ⟪p₂ -ᵥ s.center, p₁ -ᵥ s.center⟫ ≠ ‖p₁ -ᵥ s.center‖ * ‖p₁ -ᵥ s.center‖
⊢ ⟪p₂ -ᵥ s.center, p₁ -ᵥ s.center⟫ < ‖p₁ -ᵥ s.center‖ * ‖p₁ -ᵥ s.center‖

Tactic:
refine lt_of_le_of_ne
    ((real_inner_le_norm _ _).trans (mul_le_mul_of_nonneg_right ?_ (norm_nonneg _))) ?_

Premises used: real_inner_le_norm, mul_le_mul_of_nonneg_right, LE.le.trans, lt_of_le_of_ne
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : 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₂
neg : dist p₂ s.center ≤ ‖p₁ -ᵥ s.center‖
neg₁ : dist p₂ s.center ≤ dist p₁ s.center
neg₂ neg₃ neg₄ neg₅ : dist p₂ s.center ≤ s.radius
⊢ ‖p₂ -ᵥ s.center‖ ≤ ‖p₁ -ᵥ s.center‖

Tactic:
rwa [← dist_eq_norm_vsub, ← dist_eq_norm_vsub, hp₁]

Premises used: dist_eq_norm_vsub
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : 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₂
neg : ∀ (hp₂' : dist p₂ s.center < s.radius), ⟪p₂ -ᵥ s.center, p₁ -ᵥ s.center⟫ ≠ ‖p₁ -ᵥ s.center‖ * ‖p₁ -ᵥ s.center‖
neg₁ : ∀ (hp₂' : dist p₂ s.center = s.radius), ⟪p₂ -ᵥ s.center, p₁ -ᵥ s.center⟫ ≠ ‖p₁ -ᵥ s.center‖ * ‖p₁ -ᵥ s.center‖
⊢ ⟪p₂ -ᵥ s.center, p₁ -ᵥ s.center⟫ ≠ ‖p₁ -ᵥ s.center‖ * ‖p₁ -ᵥ s.center‖

Tactic:
rcases hp₂.lt_or_eq with (hp₂' | hp₂')

Premises used: LE.le.lt_or_eq
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : 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⟫ ≠ ‖p₁ -ᵥ s.center‖ * ‖p₁ -ᵥ s.center‖

Tactic:
((real_inner_le_norm _ _).trans_lt (mul_lt_mul_of_pos_right ?_ ?_)).ne

Premises used: mul_lt_mul_of_pos_right, real_inner_le_norm, LE.le.trans_lt, LT.lt.ne
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : 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
neg : ‖p₂ -ᵥ s.center‖ < ‖p₁ -ᵥ s.center‖
neg₁ : 0 < ‖p₁ -ᵥ s.center‖
⊢ ⟪p₂ -ᵥ s.center, p₁ -ᵥ s.center⟫ ≠ ‖p₁ -ᵥ s.center‖ * ‖p₁ -ᵥ s.center‖

Tactic:
refine ((real_inner_le_norm _ _).trans_lt (mul_lt_mul_of_pos_right ?_ ?_)).ne

Premises used: mul_lt_mul_of_pos_right, real_inner_le_norm, LE.le.trans_lt, LT.lt.ne
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : 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
neg : ∀ (hp₂' : dist p₂ s.center < dist p₁ s.center), ‖p₂ -ᵥ s.center‖ < ‖p₁ -ᵥ s.center‖
neg₁ : ∀ (hp₂' : ‖p₂ -ᵥ s.center‖ < dist p₁ s.center), ‖p₂ -ᵥ s.center‖ < ‖p₁ -ᵥ s.center‖
neg₂ neg₃ neg₄ neg₅ : ∀ (hp₂' : ‖p₂ -ᵥ s.center‖ < ‖p₁ -ᵥ s.center‖), ‖p₂ -ᵥ s.center‖ < ‖p₁ -ᵥ s.center‖
⊢ ‖p₂ -ᵥ s.center‖ < ‖p₁ -ᵥ s.center‖

Tactic:
rwa [← hp₁, @dist_eq_norm_vsub V, @dist_eq_norm_vsub V] at hp₂'

Premises used: dist_eq_norm_vsub
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : 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
neg : p₁ ≠ s.center
⊢ 0 < ‖p₁ -ᵥ s.center‖

Tactic:
rw [norm_pos_iff, vsub_ne_zero]

Premises used: norm_pos_iff, vsub_ne_zero
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : 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₂
⊢ dist p₂ s.center < dist s.center s.center

Tactic:
rw [← hp₁] at hp₂'
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : 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₂
hp₂'₁ : dist p₂ s.center < dist s.center s.center
⊢ dist s.center s.center = s.radius

Tactic:
rw [← hp₁] at hp₂'
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : 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₂
hp₂'₁ : dist p₂ s.center < dist s.center s.center
hp₃ : dist s.center s.center = s.radius
⊢ ¬s.center = p₂

Tactic:
rw [← hp₁] at hp₂'
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : 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

Tactic:
(dist_nonneg.not_gt : ¬dist p₂ s.center < 0) ?_

Premises used: dist_nonneg, LE.le.not_gt
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : 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₂
neg : dist p₂ s.center < 0
⊢ False

Tactic:
refine (dist_nonneg.not_gt : ¬dist p₂ s.center < 0) ?_

Premises used: dist_nonneg, LE.le.not_gt
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : 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

Tactic:
simpa using hp₂'
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : 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‖

Tactic:
rw [← hp₁, @dist_eq_norm_vsub V, @dist_eq_norm_vsub V] at hp₂'

Premises used: dist_eq_norm_vsub
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : 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‖
neg : ⟪p₂ -ᵥ s.center, p₁ -ᵥ s.center⟫ ≠ ‖p₂ -ᵥ s.center‖ * ‖p₁ -ᵥ s.center‖
⊢ ⟪p₂ -ᵥ s.center, p₁ -ᵥ s.center⟫ ≠ ‖p₁ -ᵥ s.center‖ * ‖p₁ -ᵥ s.center‖

Tactic:
nth_rw 1 [← hp₂']
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : 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‖
neg : p₁ ≠ s.center
⊢ ⟪p₂ -ᵥ s.center, p₁ -ᵥ s.center⟫ ≠ ‖p₂ -ᵥ s.center‖ * ‖p₁ -ᵥ s.center‖

Tactic:
rw [Ne, inner_eq_norm_mul_iff_real, hp₂', ← sub_eq_zero, ← smul_sub,
        vsub_sub_vsub_cancel_right, ← Ne, smul_ne_zero_iff, vsub_ne_zero,
        and_iff_left (Ne.symm h), norm_ne_zero_iff, vsub_ne_zero]

Premises used: sub_eq_zero, vsub_ne_zero, and_iff_left, Ne, Ne.symm, smul_sub, norm_ne_zero_iff, smul_ne_zero_iff, vsub_sub_vsub_cancel_right, inner_eq_norm_mul_iff_real
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : 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

Tactic:
h (Eq.symm ?_)

Premises used: Eq.symm
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : 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‖
neg : p₂ = s.center
⊢ False

Tactic:
refine h (Eq.symm ?_)

Premises used: Eq.symm
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : 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

Tactic:
simpa using hp₂'
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s : Sphere P
p₁ p₂ : P
hp₁ : p₁ ∈ s
hp₂ : dist p₂ s.center ≤ s.radius
inl : ∀ (h : 0 < ⟪p₁ -ᵥ p₂, p₁ -ᵥ s.center⟫), 0 ≤ ⟪p₁ -ᵥ p₂, p₁ -ᵥ s.center⟫
inr : ∀ (hp₂ : dist p₁ s.center ≤ s.radius), 0 ≤ ⟪p₁ -ᵥ p₁, p₁ -ᵥ s.center⟫
⊢ 0 ≤ ⟪p₁ -ᵥ p₂, p₁ -ᵥ s.center⟫

Tactic:
rcases inner_pos_or_eq_of_dist_le_radius hp₁ hp₂ with (h | rfl)

Premises used: EuclideanGeometry.inner_pos_or_eq_of_dist_le_radius, rfl
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s : Sphere P
p₁ p₂ : P
hp₁ : p₁ ∈ s
hp₂ : dist p₂ s.center ≤ s.radius
h : 0 < ⟪p₁ -ᵥ p₂, p₁ -ᵥ s.center⟫
⊢ 0 ≤ ⟪p₁ -ᵥ p₂, p₁ -ᵥ s.center⟫

Tactic:
h.le

Premises used: LT.lt.le
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s : Sphere P
p₁ p₂ : P
hp₁ : p₁ ∈ s
hp₂ : dist p₂ s.center ≤ s.radius
h : 0 < ⟪p₁ -ᵥ p₂, p₁ -ᵥ s.center⟫
⊢ 0 ≤ ⟪p₁ -ᵥ p₂, p₁ -ᵥ s.center⟫

Tactic:
exact h.le

Premises used: LT.lt.le
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s : Sphere P
p₁ : P
hp₁ : p₁ ∈ s
hp₂ : dist p₁ s.center ≤ s.radius
⊢ 0 ≤ ⟪p₁ -ᵥ p₁, p₁ -ᵥ s.center⟫

Tactic:
simp
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s : Sphere P
p₁ p₂ : P
hp₁ : p₁ ∈ s
hp₂ : dist p₂ s.center < s.radius
pos : ∀ (h : p₁ = p₂), 0 < ⟪p₁ -ᵥ p₂, p₁ -ᵥ s.center⟫
neg : ∀ (h : ¬p₁ = p₂), 0 < ⟪p₁ -ᵥ p₂, p₁ -ᵥ s.center⟫
⊢ 0 < ⟪p₁ -ᵥ p₂, p₁ -ᵥ s.center⟫

Tactic:
by_cases h : p₁ = p₂
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s : Sphere P
p₁ p₂ : P
hp₁ : p₁ ∈ s
hp₂ : dist p₂ s.center < s.radius
h : p₁ = p₂
⊢ dist p₂ s.center = s.radius

Tactic:
rw [h, mem_sphere] at hp₁

Premises used: EuclideanGeometry.mem_sphere
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s : Sphere P
p₁ p₂ : P
hp₁ : p₁ ∈ s
hp₂ : dist p₂ s.center < s.radius
h : p₁ = p₂
hp₃ : dist p₂ s.center = s.radius
⊢ dist p₂ s.center < s.radius

Tactic:
rw [h, mem_sphere] at hp₁

Premises used: EuclideanGeometry.mem_sphere
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s : Sphere P
p₁ p₂ : P
hp₁ : p₁ ∈ s
hp₂ : dist p₂ s.center < s.radius
h : p₁ = p₂
hp₃ : dist p₂ s.center = s.radius
hp₄ : dist p₂ s.center < s.radius
⊢ p₁ = p₂

Tactic:
rw [h, mem_sphere] at hp₁

Premises used: EuclideanGeometry.mem_sphere
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : 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 < ⟪p₁ -ᵥ p₂, p₁ -ᵥ s.center⟫

Tactic:
False.elim (hp₂.ne hp₁)

Premises used: False.elim, LT.lt.ne
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : 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 < ⟪p₁ -ᵥ p₂, p₁ -ᵥ s.center⟫

Tactic:
exact False.elim (hp₂.ne hp₁)

Premises used: False.elim, LT.lt.ne
-- Module: Mathlib.Geometry.Euclidean.Sphere.Basic
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s : Sphere P
p₁ p₂ : P
hp₁ : p₁ ∈ s
hp₂ : dist p₂ s.center < s.radius
h : ¬p₁ = p₂
⊢ 0 < ⟪p₁ -ᵥ p₂, p₁ -ᵥ s.center⟫

Tactic:
(inner_pos_or_eq_of_dist_le_radius hp₁ hp₂.le).resolve_right h

Premises used: EuclideanGeometry.inner_pos_or_eq_of_dist_le_radius, LT.lt.le, Or.resolve_right