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 : AffineSubspace ℝ P
inst_4 : Nonempty.{u_2 + 1} ↥S
inst_5 : S.direction.HasOrthogonalProjection
ps : Set ↥S
h : Cospherical (Subtype.val (p := fun (x : P) ↦ x ∈ S) '' ps)
inl :
  ∀ (h : Cospherical.{u_2} (P := P) (Set.image (α := ↥S) (Subtype.val (p := fun (x : P) ↦ x ∈ S)) ∅)),
    Cospherical.{u_2} (P := ↥S) ∅
inr : ∀ (p₀ : ↥S) (hp₀ : p₀ ∈ ps), Cospherical ps
⊢ Cospherical ps

Tactic:
rcases ps.eq_empty_or_nonempty with rfl | ⟨p₀, hp₀⟩

Premises used: Set.eq_empty_or_nonempty, 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 : AffineSubspace ℝ P
inst_4 : Nonempty.{u_2 + 1} ↥S
inst_5 : S.direction.HasOrthogonalProjection
h : Cospherical.{u_2} (P := P) (Set.image (α := ↥S) (Subtype.val (p := fun (x : P) ↦ x ∈ S)) ∅)
⊢ Cospherical.{u_2} (P := ↥S) ∅

Tactic:
cospherical_empty

Premises used: EuclideanGeometry.cospherical_empty
-- 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 : Nonempty.{u_2 + 1} ↥S
inst_5 : S.direction.HasOrthogonalProjection
h : Cospherical.{u_2} (P := P) (Set.image (α := ↥S) (Subtype.val (p := fun (x : P) ↦ x ∈ S)) ∅)
⊢ Cospherical.{u_2} (P := ↥S) ∅

Tactic:
exact cospherical_empty

Premises used: EuclideanGeometry.cospherical_empty
-- 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 : Nonempty.{u_2 + 1} ↥S
inst_5 : S.direction.HasOrthogonalProjection
ps : Set ↥S
h : Cospherical (Subtype.val (p := fun (x : P) ↦ x ∈ S) '' ps)
p₀ : ↥S
hp₀ : p₀ ∈ ps
inr : ∀ (c : P) (r : ℝ) (hr : ∀ p ∈ Subtype.val (p := fun (x : P) ↦ x ∈ S) '' ps, dist p c = r), Cospherical ps
⊢ Cospherical ps

Tactic:
rcases h with ⟨c, r, hr⟩
-- 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 : Nonempty.{u_2 + 1} ↥S
inst_5 : S.direction.HasOrthogonalProjection
ps : Set ↥S
p₀ : ↥S
hp₀ : p₀ ∈ ps
c : P
r : ℝ
hr : ∀ p ∈ Subtype.val (p := fun (x : P) ↦ x ∈ S) '' ps, dist p c = r
c' : ↥S := (orthogonalProjection S : (a : P) → ↥S) c
⊢ Cospherical ps

Tactic:
⟨c', dist p₀ c', fun p hp => ?_⟩

Premises used: EuclideanGeometry.Cospherical, Exists.intro, Dist.dist
-- 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 : Nonempty.{u_2 + 1} ↥S
inst_5 : S.direction.HasOrthogonalProjection
ps : Set ↥S
p₀ : ↥S
hp₀ : p₀ ∈ ps
c : P
r : ℝ
hr : ∀ p ∈ Subtype.val (p := fun (x : P) ↦ x ∈ S) '' ps, dist p c = r
c' : ↥S := (orthogonalProjection S : (a : P) → ↥S) c
inr : ∀ (p : ↥S) (hp : p ∈ ps), dist p c' = dist p₀ c'
⊢ Cospherical ps

Tactic:
refine ⟨c', dist p₀ c', fun p 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 : AffineSubspace ℝ P
inst_4 : Nonempty.{u_2 + 1} ↥S
inst_5 : S.direction.HasOrthogonalProjection
ps : Set ↥S
p₀ : ↥S
hp₀ : p₀ ∈ ps
c : P
r : ℝ
hr : ∀ p ∈ Subtype.val (p := fun (x : P) ↦ x ∈ S) '' ps, dist p c = r
c' : ↥S := (orthogonalProjection S : (a : P) → ↥S) c
p : ↥S
hp : p ∈ ps
⊢ dist (↑p : P) c = r

Tactic:
grind
-- 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 : Nonempty.{u_2 + 1} ↥S
inst_5 : S.direction.HasOrthogonalProjection
ps : Set ↥S
p₀ : ↥S
hp₀ : p₀ ∈ ps
c : P
r : ℝ
hr : ∀ p ∈ Subtype.val (p := fun (x : P) ↦ x ∈ S) '' ps, dist p c = r
c' : ↥S := (orthogonalProjection S : (a : P) → ↥S) c
p : ↥S
hp : p ∈ ps
⊢ dist (↑p : P) c = r

Tactic:
have hp_dist : dist (p : P) c = r := by grind
-- 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 : Nonempty.{u_2 + 1} ↥S
inst_5 : S.direction.HasOrthogonalProjection
ps : Set ↥S
p₀ : ↥S
hp₀ : p₀ ∈ ps
c : P
r : ℝ
hr : ∀ p ∈ Subtype.val (p := fun (x : P) ↦ x ∈ S) '' ps, dist p c = r
c' : ↥S := (orthogonalProjection S : (a : P) → ↥S) c
p : ↥S
hp : p ∈ ps
hp_dist : dist (↑p : P) c = r
⊢ dist (↑p₀ : P) c = r

Tactic:
grind
-- 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 : Nonempty.{u_2 + 1} ↥S
inst_5 : S.direction.HasOrthogonalProjection
ps : Set ↥S
p₀ : ↥S
hp₀ : p₀ ∈ ps
c : P
r : ℝ
hr : ∀ p ∈ Subtype.val (p := fun (x : P) ↦ x ∈ S) '' ps, dist p c = r
c' : ↥S := (orthogonalProjection S : (a : P) → ↥S) c
p : ↥S
hp : p ∈ ps
hp_dist : dist (↑p : P) c = r
⊢ dist (↑p₀ : P) c = r

Tactic:
have hp₀_dist : dist (p₀ : P) c = r := by grind
-- 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 : Nonempty.{u_2 + 1} ↥S
inst_5 : S.direction.HasOrthogonalProjection
ps : Set ↥S
p₀ : ↥S
hp₀ : p₀ ∈ ps
c : P
r : ℝ
hr : ∀ p ∈ Subtype.val (p := fun (x : P) ↦ x ∈ S) '' ps, dist p c = r
c' : ↥S := (orthogonalProjection S : (a : P) → ↥S) c
p : ↥S
hp : p ∈ ps
hp_dist : dist (↑p : P) c = r
hp₀_dist : dist (↑p₀ : P) c = r
⊢ dist (↑p : P) c = dist (↑p₀ : P) c

Tactic:
have hpp₀ : dist (p : P) (c : P) = dist (p₀ : P) (c : P) := hp_dist.trans hp₀_dist.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 : AffineSubspace ℝ P
inst_4 : Nonempty.{u_2 + 1} ↥S
inst_5 : S.direction.HasOrthogonalProjection
ps : Set ↥S
p₀ : ↥S
hp₀ : p₀ ∈ ps
c : P
r : ℝ
hr : ∀ p ∈ Subtype.val (p := fun (x : P) ↦ x ∈ S) '' ps, dist p c = r
c' : ↥S := (orthogonalProjection S : (a : P) → ↥S) c
p : ↥S
hp : p ∈ ps
hp_dist : dist (↑p : P) c = r
hp₀_dist : dist (↑p₀ : P) c = r
hpp₀ : dist (↑p : P) c = dist (↑p₀ : P) c
⊢ dist p c' = dist p₀ c'

Tactic:
(dist_eq_iff_dist_orthogonalProjection_eq (s := S) (p₃ := c) p.2 p₀.2).1 hpp₀

Premises used: EuclideanGeometry.dist_eq_iff_dist_orthogonalProjection_eq, Iff.mp, Subtype.property
-- 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 : Nonempty.{u_2 + 1} ↥S
inst_5 : S.direction.HasOrthogonalProjection
ps : Set ↥S
p₀ : ↥S
hp₀ : p₀ ∈ ps
c : P
r : ℝ
hr : ∀ p ∈ Subtype.val (p := fun (x : P) ↦ x ∈ S) '' ps, dist p c = r
c' : ↥S := (orthogonalProjection S : (a : P) → ↥S) c
p : ↥S
hp : p ∈ ps
hp_dist : dist (↑p : P) c = r
hp₀_dist : dist (↑p₀ : P) c = r
hpp₀ : dist (↑p : P) c = dist (↑p₀ : P) c
⊢ dist p c' = dist p₀ c'

Tactic:
exact (dist_eq_iff_dist_orthogonalProjection_eq (s := S) (p₃ := c) p.2 p₀.2).1 hpp₀

Premises used: EuclideanGeometry.dist_eq_iff_dist_orthogonalProjection_eq, Iff.mp, Subtype.property
-- 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₁ S₂ : AffineSubspace ℝ P
inst_4 : Nonempty.{u_2 + 1} ↥S₁
ps : Set ↥S₁
inst_5 : S₁.direction.HasOrthogonalProjection
inst_6 : S₂.direction.HasOrthogonalProjection
hS : S₁ ≤ S₂
obtain : ∀ (p : ↥S₁), Nonempty.{u_2 + 1} ↥S₂
⊢ Nonempty.{u_2 + 1} ↥S₂

Tactic:
obtain ⟨p⟩ := ‹Nonempty S₁›

Premises used: Membership.mem, Subtype, Nonempty
-- 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₁ S₂ : AffineSubspace ℝ P
inst_4 : Nonempty.{u_2 + 1} ↥S₁
ps : Set ↥S₁
inst_5 : S₁.direction.HasOrthogonalProjection
inst_6 : S₂.direction.HasOrthogonalProjection
hS : S₁ ≤ S₂
p : ↥S₁
⊢ Nonempty.{u_2 + 1} ↥S₂

Tactic:
⟨⟨p, hS p.property⟩⟩

Premises used: Nonempty.intro, Subtype.mk, Subtype.val, Subtype.property
-- 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₁ S₂ : AffineSubspace ℝ P
inst_4 : Nonempty.{u_2 + 1} ↥S₁
ps : Set ↥S₁
inst_5 : S₁.direction.HasOrthogonalProjection
inst_6 : S₂.direction.HasOrthogonalProjection
hS : S₁ ≤ S₂
p : ↥S₁
⊢ Nonempty.{u_2 + 1} ↥S₂

Tactic:
exact ⟨⟨p, hS p.property⟩⟩
-- 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₁ S₂ : AffineSubspace ℝ P
inst_4 : Nonempty.{u_2 + 1} ↥S₁
ps : Set ↥S₁
inst_5 : S₁.direction.HasOrthogonalProjection
inst_6 : S₂.direction.HasOrthogonalProjection
hS : S₁ ≤ S₂
⊢ Nonempty.{u_2 + 1} ↥S₂

Tactic:
haveI : Nonempty S₂ := by obtain ⟨p⟩ := ‹Nonempty S₁›; exact ⟨⟨p, hS p.property⟩⟩
-- 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₁ S₂ : AffineSubspace ℝ P
inst_4 : Nonempty.{u_2 + 1} ↥S₁
ps : Set ↥S₁
inst_5 : S₁.direction.HasOrthogonalProjection
inst_6 : S₂.direction.HasOrthogonalProjection
hS : S₁ ≤ S₂
this : Nonempty.{u_2 + 1} ↥S₂
⊢ Cospherical (P := ↥S₂) ((⇑(AffineSubspace.inclusion hS) : (a : ↥S₁) → ↥S₂) '' ps) ↔ Cospherical ps

Tactic:
simp [(Cospherical.subtype_val_iff (S := S₂) (ps := AffineSubspace.inclusion hS '' ps)).symm,
    Set.image_image]

Premises used: EuclideanGeometry.Cospherical.subtype_val_iff, Set.image_image, Iff.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 : Set P
hs : Cospherical s
p : Fin 3 → P
hps : Set.range p ⊆ s
hpi : Function.Injective p
rw : ¬Collinear ℝ (Set.range p)
⊢ AffineIndependent ℝ p

Tactic:
rw [affineIndependent_iff_not_collinear]

Premises used: affineIndependent_iff_not_collinear
-- 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 : Fin 3 → P
hps : Set.range p ⊆ s
hpi : Function.Injective p
hc : Collinear ℝ (Set.range p)
⊢ ∃ (v : V), ∀ p_1 ∈ Set.range p, ∃ (r : ℝ), p_1 = r • v +ᵥ p 0

Tactic:
rw [collinear_iff_of_mem (Set.mem_range_self (0 : Fin 3))] at hc

Premises used: Set.mem_range_self, collinear_iff_of_mem, 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
hs : Cospherical s
p : Fin 3 → P
hps : Set.range p ⊆ s
hpi : Function.Injective p
hc : ∃ (v : V), ∀ p_1 ∈ Set.range p, ∃ (r : ℝ), p_1 = r • v +ᵥ p 0
rcases : ∀ (v : V) (hv : ∀ p_1 ∈ Set.range p, ∃ (r : ℝ), p_1 = r • v +ᵥ p 0), False
⊢ False

Tactic:
rcases hc with ⟨v, hv⟩
-- 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 : Fin 3 → P
hps : Set.range p ⊆ s
hpi : Function.Injective p
v : V
hv : ∀ p_1 ∈ Set.range p, ∃ (r : ℝ), p_1 = r • v +ᵥ p 0
⊢ ∀ (i : Fin 3), ∃ (r : ℝ), p i = r • v +ᵥ p 0

Tactic:
rw [Set.forall_mem_range] at hv

Premises used: Set.forall_mem_range
-- 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 : Fin 3 → P
hps : Set.range p ⊆ s
hpi : Function.Injective p
v : V
hv : ∀ (i : Fin 3), ∃ (r : ℝ), p i = r • v +ᵥ p 0
h : v = 0
⊢ p 1 = p 0

Tactic:
simpa [h] using hv 1

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
hs : Cospherical s
p : Fin 3 → P
hps : Set.range p ⊆ s
hpi : Function.Injective p
v : V
hv : ∀ (i : Fin 3), ∃ (r : ℝ), p i = r • v +ᵥ p 0
h : v = 0
⊢ p 1 = p 0

Tactic:
have he : p 1 = p 0 := by simpa [h] using hv 1
-- 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 : Fin 3 → P
hps : Set.range p ⊆ s
hpi : Function.Injective p
v : V
hv : ∀ (i : Fin 3), ∃ (r : ℝ), p i = r • v +ᵥ p 0
h : v = 0
he : p 1 = p 0
⊢ 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
hs : Cospherical s
p : Fin 3 → P
hps : Set.range p ⊆ s
hpi : Function.Injective p
v : V
hv : ∀ (i : Fin 3), ∃ (r : ℝ), p i = r • v +ᵥ p 0
h : v = 0
he : p 1 = p 0
⊢ False

Tactic:
exact (by decide : (1 : Fin 3) ≠ 0) (hpi he)
-- 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 : Fin 3 → P
hps : Set.range p ⊆ s
hpi : Function.Injective p
v : V
hv : ∀ (i : Fin 3), ∃ (r : ℝ), p i = r • v +ᵥ p 0
⊢ v ≠ 0

Tactic:
have hv0 : v ≠ 0 := by
    intro h
    have he : p 1 = p 0 := by simpa [h] using hv 1
    exact (by decide : (1 : Fin 3) ≠ 0) (hpi he)
-- 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 : Fin 3 → P
hps : Set.range p ⊆ s
hpi : Function.Injective p
v : V
hv : ∀ (i : Fin 3), ∃ (r : ℝ), p i = r • v +ᵥ p 0
hv0 : v ≠ 0
rcases : ∀ (c : P) (r : ℝ) (hs : ∀ p ∈ s, dist p c = r), False
⊢ False

Tactic:
rcases hs with ⟨c, r, hs⟩
-- 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
hv : ∀ (i : Fin 3), ∃ (r : ℝ), p i = r • v +ᵥ p 0
hv0 : v ≠ 0
c : P
r : ℝ
hs : ∀ p ∈ s, dist p c = r
⊢ ∀ (i : Fin 3), dist (p i) c = r

Tactic:
have hs' := fun i => hs (p i) (Set.mem_of_mem_of_subset (Set.mem_range_self _) hps)
-- 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
hv : ∀ (i : Fin 3), ∃ (r : ℝ), p i = r • v +ᵥ p 0
hv0 : v ≠ 0
c : P
r : ℝ
hs : ∀ p ∈ s, dist p c = r
hs' : ∀ (i : Fin 3), dist (p i) c = r
choose : ∀ (f : (i : Fin 3) → ℝ) (hf : ∀ (i : Fin 3), p i = f i • v +ᵥ p 0), False
⊢ False

Tactic:
choose f hf using hv
-- 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
i : Fin 3
rw : dist (p i) c = r
⊢ dist (f i • v +ᵥ p 0) c = r

Tactic:
rw [← hf]
-- 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
i : Fin 3
⊢ dist (p i) c = r

Tactic:
hs' 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
i : Fin 3
⊢ dist (p i) c = r

Tactic:
exact hs' 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
⊢ ∀ (i : Fin 3), dist (f i • v +ᵥ p 0) c = r

Tactic:
have hsd : ∀ i, dist (f i • v +ᵥ p 0) c = r := by
    intro i
    rw [← hf]
    exact hs' 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
hsd : ∀ (i : Fin 3), dist (f i • v +ᵥ p 0) c = r
⊢ p 0 = f 0 • v +ᵥ p 0

Tactic:
have hf0' := hf 0
-- 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
hsd : ∀ (i : Fin 3), dist (f i • v +ᵥ p 0) c = r
hf0' : p 0 = f 0 • v +ᵥ p 0
⊢ f 0 = 0 ∨ v = 0

Tactic:
rw [eq_comm, ← @vsub_eq_zero_iff_eq V, vadd_vsub, smul_eq_zero] at hf0'

Premises used: vsub_eq_zero_iff_eq, eq_comm, vadd_vsub, smul_eq_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 : 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
hsd : ∀ (i : Fin 3), dist (f i • v +ᵥ p 0) c = r
hf0' : f 0 = 0 ∨ v = 0
⊢ f 0 = 0

Tactic:
simpa [hv0] using hf0'
-- 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
hsd : ∀ (i : Fin 3), dist (f i • v +ᵥ p 0) c = r
⊢ f 0 = 0

Tactic:
have hf0 : f 0 = 0 := by
    have hf0' := hf 0
    rw [eq_comm, ← @vsub_eq_zero_iff_eq V, vadd_vsub, smul_eq_zero] at hf0'
    simpa [hv0] using hf0'
-- 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
hsd : ∀ (i : Fin 3), dist (f i • v +ᵥ p 0) c = r
hf0 : f 0 = 0
i j : Fin 3
h : f i = f j
⊢ p i = f i • v +ᵥ p 0

Tactic:
have hi := hf 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
hsd : ∀ (i : Fin 3), dist (f i • v +ᵥ p 0) c = r
hf0 : f 0 = 0
i j : Fin 3
h : f i = f j
hi : p i = f i • v +ᵥ p 0
⊢ p i = p j

Tactic:
rw [h, ← hf j] at hi
-- 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
hsd : ∀ (i : Fin 3), dist (f i • v +ᵥ p 0) c = r
hf0 : f 0 = 0
i j : Fin 3
h : f i = f j
hi : p i = p j
⊢ i = j

Tactic:
hpi hi
-- 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
hsd : ∀ (i : Fin 3), dist (f i • v +ᵥ p 0) c = r
hf0 : f 0 = 0
i j : Fin 3
h : f i = f j
hi : p i = p j
⊢ i = j

Tactic:
exact hpi hi
-- 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
hsd : ∀ (i : Fin 3), dist (f i • v +ᵥ p 0) c = r
hf0 : f 0 = 0
⊢ Function.Injective f

Tactic:
have hfi : Function.Injective f := by
    intro i j h
    have hi := hf i
    rw [h, ← hf j] at hi
    exact hpi hi
-- 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
hsd : ∀ (i : Fin 3), dist (f i • v +ᵥ p 0) c = r
hf0 : f 0 = 0
hfi : Function.Injective f
⊢ ∀ (i : Fin 3), f i = 0 ∨ f i = -2 * ⟪v, p 0 -ᵥ c⟫ / ⟪v, v⟫

Tactic:
simp_rw [← hsd 0, hf0, zero_smul, zero_vadd, dist_smul_vadd_eq_dist (p 0) c hv0] at hsd

Premises used: zero_vadd, zero_smul, EuclideanGeometry.dist_smul_vadd_eq_dist, OfNat.ofNat