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
s : Set P
p : Fin 3 → P
hps : Set.range p ⊆ s
hpi : Function.Injective p
v : V
hv0 : v ≠ 0
c : P
r : ℝ
hs : ∀ p ∈ s, dist p c = r
hs' : ∀ (i : Fin 3), dist (p i) c = r
f : (i : Fin 3) → ℝ
hf : ∀ (i : Fin 3), p i = f i • v +ᵥ p 0
hf0 : f 0 = 0
hfi : Function.Injective f
hsd : ∀ (i : Fin 3), f i = 0 ∨ f i = -2 * ⟪v, p 0 -ᵥ c⟫ / ⟪v, v⟫
⊢ ∀ (i : Fin 3), i ≠ 0 → f i ≠ 0

Tactic:
have hfn0 : ∀ i, i ≠ 0 → f i ≠ 0 := fun i => (hfi.ne_iff' hf0).2
-- 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 : Set P
p : Fin 3 → P
hps : Set.range p ⊆ s
hpi : Function.Injective p
v : V
hv0 : v ≠ 0
c : P
r : ℝ
hs : ∀ p ∈ s, dist p c = r
hs' : ∀ (i : Fin 3), dist (p i) c = r
f : (i : Fin 3) → ℝ
hf : ∀ (i : Fin 3), p i = f i • v +ᵥ p 0
hf0 : f 0 = 0
hfi : Function.Injective f
hsd : ∀ (i : Fin 3), f i = 0 ∨ f i = -2 * ⟪v, p 0 -ᵥ c⟫ / ⟪v, v⟫
hfn0 : ∀ (i : Fin 3), i ≠ 0 → f i ≠ 0
i : Fin 3
hi : i ≠ 0
⊢ f i = 0 ∨ f i = -2 * ⟪v, p 0 -ᵥ c⟫ / ⟪v, v⟫

Tactic:
have hsdi := hsd i
-- 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 : Set P
p : Fin 3 → P
hps : Set.range p ⊆ s
hpi : Function.Injective p
v : V
hv0 : v ≠ 0
c : P
r : ℝ
hs : ∀ p ∈ s, dist p c = r
hs' : ∀ (i : Fin 3), dist (p i) c = r
f : (i : Fin 3) → ℝ
hf : ∀ (i : Fin 3), p i = f i • v +ᵥ p 0
hf0 : f 0 = 0
hfi : Function.Injective f
hsd : ∀ (i : Fin 3), f i = 0 ∨ f i = -2 * ⟪v, p 0 -ᵥ c⟫ / ⟪v, v⟫
hfn0 : ∀ (i : Fin 3), i ≠ 0 → f i ≠ 0
i : Fin 3
hi : i ≠ 0
hsdi : f i = 0 ∨ f i = -2 * ⟪v, p 0 -ᵥ c⟫ / ⟪v, v⟫
⊢ f i = -2 * ⟪v, p 0 -ᵥ c⟫ / ⟪v, v⟫

Tactic:
simpa [hfn0, hi] using hsdi
-- 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 : Set P
p : Fin 3 → P
hps : Set.range p ⊆ s
hpi : Function.Injective p
v : V
hv0 : v ≠ 0
c : P
r : ℝ
hs : ∀ p ∈ s, dist p c = r
hs' : ∀ (i : Fin 3), dist (p i) c = r
f : (i : Fin 3) → ℝ
hf : ∀ (i : Fin 3), p i = f i • v +ᵥ p 0
hf0 : f 0 = 0
hfi : Function.Injective f
hsd : ∀ (i : Fin 3), f i = 0 ∨ f i = -2 * ⟪v, p 0 -ᵥ c⟫ / ⟪v, v⟫
hfn0 : ∀ (i : Fin 3), i ≠ 0 → f i ≠ 0
⊢ ∀ (i : Fin 3), i ≠ 0 → f i = -2 * ⟪v, p 0 -ᵥ c⟫ / ⟪v, v⟫

Tactic:
have hfn0' : ∀ i, i ≠ 0 → f i = -2 * ⟪v, p 0 -ᵥ c⟫ / ⟪v, v⟫ := by
    intro i hi
    have hsdi := hsd i
    simpa [hfn0, hi] using hsdi
-- 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 : Set P
p : Fin 3 → P
hps : Set.range p ⊆ s
hpi : Function.Injective p
v : V
hv0 : v ≠ 0
c : P
r : ℝ
hs : ∀ p ∈ s, dist p c = r
hs' : ∀ (i : Fin 3), dist (p i) c = r
f : (i : Fin 3) → ℝ
hf : ∀ (i : Fin 3), p i = f i • v +ᵥ p 0
hf0 : f 0 = 0
hfi : Function.Injective f
hsd : ∀ (i : Fin 3), f i = 0 ∨ f i = -2 * ⟪v, p 0 -ᵥ c⟫ / ⟪v, v⟫
hfn0 : ∀ (i : Fin 3), i ≠ 0 → f i ≠ 0
hfn0' : ∀ (i : Fin 3), i ≠ 0 → f i = -2 * ⟪v, p 0 -ᵥ c⟫ / ⟪v, v⟫
⊢ Ne (α := Fin 3) 1 0

Tactic:
decide
-- 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 : Set P
p : Fin 3 → P
hps : Set.range p ⊆ s
hpi : Function.Injective p
v : V
hv0 : v ≠ 0
c : P
r : ℝ
hs : ∀ p ∈ s, dist p c = r
hs' : ∀ (i : Fin 3), dist (p i) c = r
f : (i : Fin 3) → ℝ
hf : ∀ (i : Fin 3), p i = f i • v +ᵥ p 0
hf0 : f 0 = 0
hfi : Function.Injective f
hsd : ∀ (i : Fin 3), f i = 0 ∨ f i = -2 * ⟪v, p 0 -ᵥ c⟫ / ⟪v, v⟫
hfn0 : ∀ (i : Fin 3), i ≠ 0 → f i ≠ 0
hfn0' : ∀ (i : Fin 3), i ≠ 0 → f i = -2 * ⟪v, p 0 -ᵥ c⟫ / ⟪v, v⟫
rw : -2 * ⟪v, p 0 -ᵥ c⟫ / ⟪v, v⟫ = f 2
rw₁ rw₂ : -2 * ⟪v, p 0 -ᵥ c⟫ / ⟪v, v⟫ = -2 * ⟪v, p 0 -ᵥ c⟫ / ⟪v, v⟫
⊢ f 1 = f 2

Tactic:
rw [hfn0' 1 (by decide), hfn0' 2 (by decide)]

Premises used: OfNat.ofNat
-- 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 : Set P
p : Fin 3 → P
hps : Set.range p ⊆ s
hpi : Function.Injective p
v : V
hv0 : v ≠ 0
c : P
r : ℝ
hs : ∀ p ∈ s, dist p c = r
hs' : ∀ (i : Fin 3), dist (p i) c = r
f : (i : Fin 3) → ℝ
hf : ∀ (i : Fin 3), p i = f i • v +ᵥ p 0
hf0 : f 0 = 0
hfi : Function.Injective f
hsd : ∀ (i : Fin 3), f i = 0 ∨ f i = -2 * ⟪v, p 0 -ᵥ c⟫ / ⟪v, v⟫
hfn0 : ∀ (i : Fin 3), i ≠ 0 → f i ≠ 0
hfn0' : ∀ (i : Fin 3), i ≠ 0 → f i = -2 * ⟪v, p 0 -ᵥ c⟫ / ⟪v, v⟫
⊢ f 1 = f 2

Tactic:
have hf12 : f 1 = f 2 := by rw [hfn0' 1 (by decide), hfn0' 2 (by decide)]
-- 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 : Set P
p : Fin 3 → P
hps : Set.range p ⊆ s
hpi : Function.Injective p
v : V
hv0 : v ≠ 0
c : P
r : ℝ
hs : ∀ p ∈ s, dist p c = r
hs' : ∀ (i : Fin 3), dist (p i) c = r
f : (i : Fin 3) → ℝ
hf : ∀ (i : Fin 3), p i = f i • v +ᵥ p 0
hf0 : f 0 = 0
hfi : Function.Injective f
hsd : ∀ (i : Fin 3), f i = 0 ∨ f i = -2 * ⟪v, p 0 -ᵥ c⟫ / ⟪v, v⟫
hfn0 : ∀ (i : Fin 3), i ≠ 0 → f i ≠ 0
hfn0' : ∀ (i : Fin 3), i ≠ 0 → f i = -2 * ⟪v, p 0 -ᵥ c⟫ / ⟪v, v⟫
hf12 : f 1 = f 2
⊢ Ne (α := Fin 3) 1 2

Tactic:
decide
-- 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 : Set P
p : Fin 3 → P
hps : Set.range p ⊆ s
hpi : Function.Injective p
v : V
hv0 : v ≠ 0
c : P
r : ℝ
hs : ∀ p ∈ s, dist p c = r
hs' : ∀ (i : Fin 3), dist (p i) c = r
f : (i : Fin 3) → ℝ
hf : ∀ (i : Fin 3), p i = f i • v +ᵥ p 0
hf0 : f 0 = 0
hfi : Function.Injective f
hsd : ∀ (i : Fin 3), f i = 0 ∨ f i = -2 * ⟪v, p 0 -ᵥ c⟫ / ⟪v, v⟫
hfn0 : ∀ (i : Fin 3), i ≠ 0 → f i ≠ 0
hfn0' : ∀ (i : Fin 3), i ≠ 0 → f i = -2 * ⟪v, p 0 -ᵥ c⟫ / ⟪v, v⟫
hf12 : f 1 = f 2
⊢ False

Tactic:
exact (by decide : (1 : Fin 3) ≠ 2) (hfi hf12)
-- 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 : Set P
hs : Cospherical s
p₁ p₂ p₃ : P
h₁ : p₁ ∈ s
h₂ : p₂ ∈ s
h₃ : p₃ ∈ s
h₁₂ : p₁ ≠ p₂
h₁₃ : p₁ ≠ p₃
h₂₃ : p₂ ≠ p₃
⊢ AffineIndependent ℝ ![p₁, p₂, p₃]

Tactic:
hs.affineIndependent ?_ ?_

Premises used: EuclideanGeometry.Cospherical.affineIndependent
-- 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 : Set P
hs : Cospherical s
p₁ p₂ p₃ : P
h₁ : p₁ ∈ s
h₂ : p₂ ∈ s
h₃ : p₃ ∈ s
h₁₂ : p₁ ≠ p₂
h₁₃ : p₁ ≠ p₃
h₂₃ : p₂ ≠ p₃
refine_1 : Set.range ![p₁, p₂, p₃] ⊆ s
refine_2 : Function.Injective ![p₁, p₂, p₃]
⊢ AffineIndependent ℝ ![p₁, p₂, p₃]

Tactic:
refine hs.affineIndependent ?_ ?_

Premises used: EuclideanGeometry.Cospherical.affineIndependent
-- 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 : Set P
hs : Cospherical s
p₁ p₂ p₃ : P
h₁ : p₁ ∈ s
h₂ : p₂ ∈ s
h₃ : p₃ ∈ s
h₁₂ : p₁ ≠ p₂
h₁₃ : p₁ ≠ p₃
h₂₃ : p₂ ≠ p₃
⊢ Set.range ![p₁, p₂, p₃] ⊆ s

Tactic:
simp [h₁, h₂, h₃, Set.insert_subset_iff]

Premises used: Set.insert_subset_iff
-- 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 : Set P
hs : Cospherical s
p₁ p₂ p₃ : P
h₁ : p₁ ∈ s
h₂ : p₂ ∈ s
h₃ : p₃ ∈ s
h₁₂ : p₁ ≠ p₂
h₁₃ : p₁ ≠ p₃
h₂₃ : p₂ ≠ p₃
refine_2 :
  p₁ ∉
      Set.range (ι := Fin (Nat.succ 0).succ)
        (Fin.cons (α := fun (a : Fin (Nat.succ 0).succ) ↦ P) p₂
          (Fin.cons (α := fun (a : Fin (Nat.succ 0)) ↦ P) p₃ ![])) ∧
    p₂ ∉ Set.range (ι := Fin (Nat.succ 0)) (Fin.cons (α := fun (a : Fin (Nat.succ 0)) ↦ P) p₃ ![]) ∧
      p₃ ∉ Set.range ![] ∧ Function.Injective.{1, u_2 + 1} (β := P) ![]
⊢ Function.Injective ![p₁, p₂, p₃]

Tactic:
simp only [Matrix.vecCons, Fin.cons_injective_iff]

Premises used: Fin.cons_injective_iff, Matrix.vecCons
-- 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 : Set P
hs : Cospherical s
p₁ p₂ p₃ : P
h₁ : p₁ ∈ s
h₂ : p₂ ∈ s
h₃ : p₃ ∈ s
h₁₂ : p₁ ≠ p₂
h₁₃ : p₁ ≠ p₃
h₂₃ : p₂ ≠ p₃
⊢ p₁ ∉
      Set.range (ι := Fin (Nat.succ 0).succ)
        (Fin.cons (α := fun (a : Fin (Nat.succ 0).succ) ↦ P) p₂
          (Fin.cons (α := fun (a : Fin (Nat.succ 0)) ↦ P) p₃ ![])) ∧
    p₂ ∉ Set.range (ι := Fin (Nat.succ 0)) (Fin.cons (α := fun (a : Fin (Nat.succ 0)) ↦ P) p₃ ![]) ∧
      p₃ ∉ Set.range ![] ∧ Function.Injective.{1, u_2 + 1} (β := P) ![]

Tactic:
simp [h₁₂, h₁₃, h₂₃, Function.Injective, eq_iff_true_of_subsingleton]

Premises used: Function.Injective, eq_iff_true_of_subsingleton
-- 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
hs : Cospherical (P := P) {p₁, p₂, p₃}
h₁₂ : p₁ ≠ p₂
h₁₃ : p₁ ≠ p₃
h₂₃ : p₂ ≠ p₃
⊢ AffineIndependent ℝ ![p₁, p₂, p₃]

Tactic:
hs.affineIndependent_of_mem_of_ne (Set.mem_insert _ _)
    (Set.mem_insert_of_mem _ (Set.mem_insert _ _))
    (Set.mem_insert_of_mem _ (Set.mem_insert_of_mem _ (Set.mem_singleton _))) h₁₂ h₁₃ h₂₃

Premises used: Set.mem_singleton, EuclideanGeometry.Cospherical.affineIndependent_of_mem_of_ne, Set.mem_insert_of_mem, Set.mem_insert
-- 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₁ s₂ : Sphere P
hp₁s₁ : p₁ ∈ s₁
hp₂s₁ : p₂ ∈ s₁
hp₁s₂ : p₁ ∈ s₂
hp₂s₂ : p₂ ∈ s₂
⊢ ⟪s₂.center -ᵥ s₁.center, p₂ -ᵥ p₁⟫ = 0

Tactic:
inner_vsub_vsub_of_dist_eq_of_dist_eq (dist_center_eq_dist_center_of_mem_sphere hp₁s₁ hp₂s₁)
    (dist_center_eq_dist_center_of_mem_sphere hp₁s₂ hp₂s₂)

Premises used: EuclideanGeometry.inner_vsub_vsub_of_dist_eq_of_dist_eq, EuclideanGeometry.dist_center_eq_dist_center_of_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
p₁ p₂ : P
s : Sphere P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
⊢ ⟪s.center -ᵥ midpoint ℝ p₁ p₂, p₂ -ᵥ p₁⟫ = 0

Tactic:
inner_vsub_vsub_of_dist_eq_of_dist_eq
    (dist_left_midpoint_eq_dist_right_midpoint p₁ p₂)
    (dist_center_eq_dist_center_of_mem_sphere hp₁ hp₂)

Premises used: dist_left_midpoint_eq_dist_right_midpoint, EuclideanGeometry.inner_vsub_vsub_of_dist_eq_of_dist_eq, EuclideanGeometry.dist_center_eq_dist_center_of_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
p₁ p₂ p : P
s : Sphere P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp : Sbtw ℝ p₁ p p₂
set :
  let o := s.center;
  dist o p < s.radius
⊢ dist s.center p < s.radius

Tactic:
set o := s.center

Premises used: EuclideanGeometry.Sphere.center
-- 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
hp : Sbtw ℝ p₁ p p₂
o : P := s.center
obtain :
  ∀ (t : ℝ) (hpt : (AffineMap.lineMap p₁ p₂ : (a : ℝ) → P) t = p) (ht₀ : 0 ≤ t) (ht₁ : t ≤ 1) (hne₁ : p ≠ p₁)
    (hne₂ : p ≠ p₂), dist o p < s.radius
⊢ dist o p < s.radius

Tactic:
obtain ⟨⟨t, ⟨ht₀, ht₁⟩, hpt⟩, hne₁, hne₂⟩ := 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
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₂
h : 0 = t
rw : (AffineMap.lineMap p₁ p₂ : (a : ℝ) → P) t = p₁
rw₁ : (AffineMap.lineMap p₁ p₂ : (a : ℝ) → P) 0 = p₁
rw₂ rw₃ : p₁ = p₁
⊢ p = p₁

Tactic:
rw [← hpt, ← h, AffineMap.lineMap_apply_zero]

Premises used: AffineMap.lineMap_apply_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
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₂
⊢ 0 < t

Tactic:
have ht₀' : 0 < t := lt_of_le_of_ne ht₀ fun h => hne₁ <| by
    rw [← hpt, ← h, AffineMap.lineMap_apply_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
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
h : t = 1
rw : (AffineMap.lineMap p₁ p₂ : (a : ℝ) → P) t = p₂
rw₁ : (AffineMap.lineMap p₁ p₂ : (a : ℝ) → P) 1 = p₂
rw₂ rw₃ : p₂ = p₂
⊢ p = p₂

Tactic:
rw [← hpt, h, AffineMap.lineMap_apply_one]

Premises used: AffineMap.lineMap_apply_one
-- 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
⊢ t < 1

Tactic:
have ht₁' : t < 1 := lt_of_le_of_ne ht₁ fun h => hne₂ <| by
    rw [← hpt, h, AffineMap.lineMap_apply_one]
-- 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
rw : dist p₁ o = s.radius
⊢ ‖u‖ = s.radius

Tactic:
rw [← dist_eq_norm_vsub]

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
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
⊢ dist p₁ o = s.radius

Tactic:
mem_sphere.mp hp₁

Premises used: EuclideanGeometry.mem_sphere, Iff.mp
-- 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
⊢ dist p₁ o = s.radius

Tactic:
exact mem_sphere.mp hp₁

Premises used: EuclideanGeometry.mem_sphere, Iff.mp
-- 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
⊢ ‖u‖ = s.radius

Tactic:
have hu : ‖u‖ = s.radius := by rw [← dist_eq_norm_vsub]; exact mem_sphere.mp 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
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
rw : dist p₂ o = s.radius
⊢ ‖v‖ = s.radius

Tactic:
rw [← dist_eq_norm_vsub]

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
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
⊢ dist p₂ o = s.radius

Tactic:
mem_sphere.mp hp₂

Premises used: EuclideanGeometry.mem_sphere, Iff.mp
-- 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
⊢ dist p₂ o = s.radius

Tactic:
exact mem_sphere.mp hp₂

Premises used: EuclideanGeometry.mem_sphere, Iff.mp
-- 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
⊢ ‖v‖ = s.radius

Tactic:
have hv : ‖v‖ = s.radius := by rw [← dist_eq_norm_vsub]; exact mem_sphere.mp 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
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
h : u = v
rw : (AffineMap.lineMap p₁ p₂ : (a : ℝ) → P) t = p₁
rw₁ : (AffineMap.lineMap p₂ p₂ : (a : ℝ) → P) t = p₂
rw₂ : (AffineMap.const ℝ ℝ p₂ : (a : ℝ) → P) t = p₂
rw₃ rw₄ : p₂ = p₂
⊢ p = p₁

Tactic:
rw [← hpt, vsub_left_cancel h, AffineMap.lineMap_same, AffineMap.const_apply]

Premises used: AffineMap.const_apply, AffineMap.lineMap_same, vsub_left_cancel
-- 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
⊢ u ≠ v

Tactic:
have huv : u ≠ v := fun h => hne₁ <| by
    rw [← hpt, vsub_left_cancel h, AffineMap.lineMap_same, AffineMap.const_apply]
-- 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
rw : t • (v - u) + (p₁ -ᵥ o) = (1 - t) • u + t • v
⊢ p -ᵥ o = (1 - t) • u + t • v

Tactic:
rw [show p = (AffineMap.lineMap p₁ p₂) t from hpt.symm, AffineMap.lineMap_apply,
      vadd_vsub_assoc, show (p₂ -ᵥ p₁ : V) = v - u from
      (vsub_sub_vsub_cancel_right p₂ p₁ o).symm]

Premises used: vadd_vsub_assoc, AffineMap.lineMap_apply, vsub_sub_vsub_cancel_right, 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
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
⊢ t • (v - u) + (p₁ -ᵥ o) = (1 - t) • u + t • v

Tactic:
module
-- 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
⊢ p -ᵥ o = (1 - t) • u + t • v

Tactic:
have hpo : p -ᵥ o = (1 - t) • u + t • v := by
    rw [show p = (AffineMap.lineMap p₁ p₂) t from hpt.symm, AffineMap.lineMap_apply,
      vadd_vsub_assoc, show (p₂ -ᵥ p₁ : V) = v - u from
      (vsub_sub_vsub_cancel_right p₂ p₁ o).symm]
    module
-- 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
rw : ‖(1 - t) • u + t • v‖ < s.radius
⊢ dist o p < s.radius

Tactic:
rw [dist_comm, dist_eq_norm_vsub, hpo]

Premises used: dist_comm, 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
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) u

Tactic:
simp [Metric.mem_closedBall, hu]

Premises used: Metric.mem_closedBall