awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Euclidean.MongePoint
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
t : Triangle ℝ P
ho : t.orthocenter ∉ Set.range t.points
p : Fin 3 → P
hps : Set.range p ⊆ insert t.orthocenter (Set.range t.points)
hpi : Function.Injective p
hs : Set.range p = Set.range t.points
p₁ : P
hp₁ : p₁ ∈ Set.range t.points
right : ∀ (i : Fin (HAdd.hAdd (α := ℕ) 2 1)), dist (t.points i) (Simplex.circumcenter t) = Simplex.circumradius t
⊢ dist p₁ (Simplex.circumcenter t) = Simplex.circumradius t

Tactic:
rcases hp₁ with ⟨i, rfl⟩

Premises used: rfl
-- Module: Mathlib.Geometry.Euclidean.MongePoint
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
t : Triangle ℝ P
ho : t.orthocenter ∉ Set.range t.points
p : Fin 3 → P
hps : Set.range p ⊆ insert t.orthocenter (Set.range t.points)
hpi : Function.Injective p
hs : Set.range p = Set.range t.points
i : Fin (HAdd.hAdd (α := ℕ) 2 1)
⊢ dist (t.points i) (Simplex.circumcenter t) = Simplex.circumradius t

Tactic:
t.dist_circumcenter_eq_circumradius _

Premises used: Affine.Simplex.dist_circumcenter_eq_circumradius
-- Module: Mathlib.Geometry.Euclidean.MongePoint
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
t : Triangle ℝ P
ho : t.orthocenter ∉ Set.range t.points
p : Fin 3 → P
hps : Set.range p ⊆ insert t.orthocenter (Set.range t.points)
hpi : Function.Injective p
hs : Set.range p = Set.range t.points
i : Fin (HAdd.hAdd (α := ℕ) 2 1)
⊢ dist (t.points i) (Simplex.circumcenter t) = Simplex.circumradius t

Tactic:
exact t.dist_circumcenter_eq_circumradius _

Premises used: Affine.Simplex.dist_circumcenter_eq_circumradius
-- Module: Mathlib.Geometry.Euclidean.MongePoint
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
ho : OrthocentricSystem s
p : Fin 3 → P
hps : Set.range p ⊆ s
hpi : Function.Injective p
rcases :
  ∀ (t : Triangle ℝ P) (hto : t.orthocenter ∉ Set.range t.points) (hst : s = insert t.orthocenter (Set.range t.points)),
    AffineIndependent ℝ p
⊢ AffineIndependent ℝ p

Tactic:
rcases ho with ⟨t, hto, hst⟩
-- Module: Mathlib.Geometry.Euclidean.MongePoint
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
t : Triangle ℝ P
hto : t.orthocenter ∉ Set.range t.points
hst : s = insert t.orthocenter (Set.range t.points)
⊢ Set.range p ⊆ insert t.orthocenter (Set.range t.points)

Tactic:
rw [hst] at hps
-- Module: Mathlib.Geometry.Euclidean.MongePoint
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
t : Triangle ℝ P
hto : t.orthocenter ∉ Set.range t.points
hst : s = insert t.orthocenter (Set.range t.points)
hps₁ : Set.range p ⊆ insert t.orthocenter (Set.range t.points)
⊢ t.orthocenter ∉ Set.range t.points

Tactic:
rw [hst] at hps
-- Module: Mathlib.Geometry.Euclidean.MongePoint
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
t : Triangle ℝ P
hto : t.orthocenter ∉ Set.range t.points
hst : s = insert t.orthocenter (Set.range t.points)
hps₁ : Set.range p ⊆ insert t.orthocenter (Set.range t.points)
hto₁ : t.orthocenter ∉ Set.range t.points
⊢ s = insert t.orthocenter (Set.range t.points)

Tactic:
rw [hst] at hps
-- Module: Mathlib.Geometry.Euclidean.MongePoint
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
hpi : Function.Injective p
t : Triangle ℝ P
hps : Set.range p ⊆ insert t.orthocenter (Set.range t.points)
hto : t.orthocenter ∉ Set.range t.points
hst : s = insert t.orthocenter (Set.range t.points)
rcases :
  ∀ (c : P),
    Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range t.points)) c →
      ∀ (hc : ∀ p₁ ∈ Set.range p, dist p₁ c = Simplex.circumradius t), AffineIndependent ℝ p
⊢ AffineIndependent ℝ p

Tactic:
rcases exists_dist_eq_circumradius_of_subset_insert_orthocenter hto hps hpi with ⟨c, _, hc⟩

Premises used: EuclideanGeometry.exists_dist_eq_circumradius_of_subset_insert_orthocenter
-- Module: Mathlib.Geometry.Euclidean.MongePoint
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
hpi : Function.Injective p
t : Triangle ℝ P
hps : Set.range p ⊆ insert t.orthocenter (Set.range t.points)
hto : t.orthocenter ∉ Set.range t.points
hst : s = insert t.orthocenter (Set.range t.points)
c : P
left : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range t.points)) c
hc : ∀ p₁ ∈ Set.range p, dist p₁ c = Simplex.circumradius t
⊢ AffineIndependent ℝ p

Tactic:
Cospherical.affineIndependent ⟨c, t.circumradius, hc⟩ Set.Subset.rfl hpi

Premises used: EuclideanGeometry.Cospherical.affineIndependent, Set.Subset.rfl, Exists.intro, Affine.Simplex.circumradius
-- Module: Mathlib.Geometry.Euclidean.MongePoint
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
hpi : Function.Injective p
t : Triangle ℝ P
hps : Set.range p ⊆ insert t.orthocenter (Set.range t.points)
hto : t.orthocenter ∉ Set.range t.points
hst : s = insert t.orthocenter (Set.range t.points)
c : P
left : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range t.points)) c
hc : ∀ p₁ ∈ Set.range p, dist p₁ c = Simplex.circumradius t
⊢ AffineIndependent ℝ p

Tactic:
exact Cospherical.affineIndependent ⟨c, t.circumradius, hc⟩ Set.Subset.rfl hpi

Premises used: EuclideanGeometry.Cospherical.affineIndependent, Set.Subset.rfl, Exists.intro, Affine.Simplex.circumradius
-- Module: Mathlib.Geometry.Euclidean.MongePoint
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
ho : OrthocentricSystem s
p : Fin 3 → P
hps : Set.range p ⊆ s
hpi : Function.Injective p
⊢ AffineIndependent ℝ p

Tactic:
have ha := ho.affineIndependent hps hpi
-- Module: Mathlib.Geometry.Euclidean.MongePoint
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
ho : OrthocentricSystem s
p : Fin 3 → P
hps : Set.range p ⊆ s
hpi : Function.Injective p
ha : AffineIndependent ℝ p
rcases :
  ∀ (t : Triangle ℝ P),
    t.orthocenter ∉ Set.range t.points →
      ∀ (hts : s = insert t.orthocenter (Set.range t.points)),
        Eq (α := AffineSubspace ℝ P) (affineSpan ℝ (Set.range p)) (affineSpan ℝ s)
⊢ Eq (α := AffineSubspace ℝ P) (affineSpan ℝ (Set.range p)) (affineSpan ℝ s)

Tactic:
rcases ho with ⟨t, _, hts⟩
-- Module: Mathlib.Geometry.Euclidean.MongePoint
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
ha : AffineIndependent ℝ p
t : Triangle ℝ P
left : t.orthocenter ∉ Set.range t.points
hts : s = insert t.orthocenter (Set.range t.points)
rw :
  Eq (α := AffineSubspace ℝ P) (affineSpan ℝ (insert t.orthocenter (Set.range t.points)))
    (affineSpan ℝ (Set.range t.points))
rw₁ rw₂ : Eq (α := AffineSubspace ℝ P) (affineSpan ℝ (Set.range t.points)) (affineSpan ℝ (Set.range t.points))
⊢ Eq (α := AffineSubspace ℝ P) (affineSpan ℝ s) (affineSpan ℝ (Set.range t.points))

Tactic:
rw [hts, affineSpan_insert_eq_affineSpan ℝ t.orthocenter_mem_affineSpan]

Premises used: Real, Affine.Triangle.orthocenter_mem_affineSpan, affineSpan_insert_eq_affineSpan
-- Module: Mathlib.Geometry.Euclidean.MongePoint
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
ha : AffineIndependent ℝ p
t : Triangle ℝ P
left : t.orthocenter ∉ Set.range t.points
hts : s = insert t.orthocenter (Set.range t.points)
⊢ Eq (α := AffineSubspace ℝ P) (affineSpan ℝ s) (affineSpan ℝ (Set.range t.points))

Tactic:
have hs : affineSpan ℝ s = affineSpan ℝ (Set.range t.points) := by
    rw [hts, affineSpan_insert_eq_affineSpan ℝ t.orthocenter_mem_affineSpan]
-- Module: Mathlib.Geometry.Euclidean.MongePoint
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
ha : AffineIndependent ℝ p
t : Triangle ℝ P
left : t.orthocenter ∉ Set.range t.points
hts : s = insert t.orthocenter (Set.range t.points)
hs : Eq (α := AffineSubspace ℝ P) (affineSpan ℝ s) (affineSpan ℝ (Set.range t.points))
⊢ Eq (α := AffineSubspace ℝ P) (affineSpan ℝ (Set.range p)) (affineSpan ℝ s)

Tactic:
ext_of_direction_eq ?_
    ⟨p 0, mem_affineSpan ℝ (Set.mem_range_self _), mem_affineSpan ℝ (hps (Set.mem_range_self _))⟩

Premises used: Set.mem_range_self, Real, mem_affineSpan, And.intro, Exists.intro, AffineSubspace.ext_of_direction_eq, OfNat.ofNat
-- Module: Mathlib.Geometry.Euclidean.MongePoint
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
ha : AffineIndependent ℝ p
t : Triangle ℝ P
left : t.orthocenter ∉ Set.range t.points
hts : s = insert t.orthocenter (Set.range t.points)
hs : Eq (α := AffineSubspace ℝ P) (affineSpan ℝ s) (affineSpan ℝ (Set.range t.points))
refine : Eq (α := Submodule ℝ V) (direction (affineSpan ℝ (Set.range p))) (direction (affineSpan ℝ s))
⊢ Eq (α := AffineSubspace ℝ P) (affineSpan ℝ (Set.range p)) (affineSpan ℝ s)

Tactic:
refine ext_of_direction_eq ?_
    ⟨p 0, mem_affineSpan ℝ (Set.mem_range_self _), mem_affineSpan ℝ (hps (Set.mem_range_self _))⟩

Premises used: Set.mem_range_self, Real, mem_affineSpan, And.intro, Exists.intro, AffineSubspace.ext_of_direction_eq, OfNat.ofNat
-- Module: Mathlib.Geometry.Euclidean.MongePoint
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
ha : AffineIndependent ℝ p
t : Triangle ℝ P
left : t.orthocenter ∉ Set.range t.points
hts : s = insert t.orthocenter (Set.range t.points)
hs : Eq (α := AffineSubspace ℝ P) (affineSpan ℝ s) (affineSpan ℝ (Set.range t.points))
rw : FiniteDimensional.{0, u_1} ℝ ↥(direction (affineSpan ℝ (Set.range t.points)))
⊢ FiniteDimensional.{0, u_1} ℝ ↥(direction (affineSpan ℝ s))

Tactic:
rw [hs]
-- Module: Mathlib.Geometry.Euclidean.MongePoint
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
ha : AffineIndependent ℝ p
t : Triangle ℝ P
left : t.orthocenter ∉ Set.range t.points
hts : s = insert t.orthocenter (Set.range t.points)
hs : Eq (α := AffineSubspace ℝ P) (affineSpan ℝ s) (affineSpan ℝ (Set.range t.points))
⊢ FiniteDimensional.{0, u_1} ℝ ↥(direction (affineSpan ℝ (Set.range t.points)))

Tactic:
infer_instance
-- Module: Mathlib.Geometry.Euclidean.MongePoint
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
ha : AffineIndependent ℝ p
t : Triangle ℝ P
left : t.orthocenter ∉ Set.range t.points
hts : s = insert t.orthocenter (Set.range t.points)
hs : Eq (α := AffineSubspace ℝ P) (affineSpan ℝ s) (affineSpan ℝ (Set.range t.points))
⊢ FiniteDimensional.{0, u_1} ℝ ↥(direction (affineSpan ℝ s))

Tactic:
have hfd : FiniteDimensional ℝ (affineSpan ℝ s).direction := by rw [hs]; infer_instance
-- Module: Mathlib.Geometry.Euclidean.MongePoint
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
ha : AffineIndependent ℝ p
t : Triangle ℝ P
left : t.orthocenter ∉ Set.range t.points
hts : s = insert t.orthocenter (Set.range t.points)
hs : Eq (α := AffineSubspace ℝ P) (affineSpan ℝ s) (affineSpan ℝ (Set.range t.points))
hfd : FiniteDimensional.{0, u_1} ℝ ↥(direction (affineSpan ℝ s))
⊢ Eq (α := Submodule ℝ V) (direction (affineSpan ℝ (Set.range p))) (direction (affineSpan ℝ s))

Tactic:
Submodule.eq_of_le_of_finrank_eq (direction_le (affineSpan_mono ℝ hps)) ?_

Premises used: AffineSubspace.direction_le, Real, Submodule.eq_of_le_of_finrank_eq, affineSpan_mono
-- Module: Mathlib.Geometry.Euclidean.MongePoint
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
ha : AffineIndependent ℝ p
t : Triangle ℝ P
left : t.orthocenter ∉ Set.range t.points
hts : s = insert t.orthocenter (Set.range t.points)
hs : Eq (α := AffineSubspace ℝ P) (affineSpan ℝ s) (affineSpan ℝ (Set.range t.points))
hfd : FiniteDimensional.{0, u_1} ℝ ↥(direction (affineSpan ℝ s))
rw :
  finrank.{0, u_1} ℝ ↥(direction (affineSpan ℝ (Set.range p))) =
    finrank.{0, u_1} ℝ ↥(direction (affineSpan ℝ (Set.range t.points)))
rw₁ :
  finrank.{0, u_1} ℝ ↥(vectorSpan ℝ (Set.range p)) = finrank.{0, u_1} ℝ ↥(direction (affineSpan ℝ (Set.range t.points)))
rw₂ : finrank.{0, u_1} ℝ ↥(vectorSpan ℝ (Set.range p)) = finrank.{0, u_1} ℝ ↥(vectorSpan ℝ (Set.range t.points))
rw₃ : 2 = finrank.{0, u_1} ℝ ↥(vectorSpan ℝ (Set.range t.points))
rw₄ rw₅ : Eq (α := ℕ) 2 2
⊢ finrank.{0, u_1} ℝ ↥(direction (affineSpan ℝ (Set.range p))) = finrank.{0, u_1} ℝ ↥(direction (affineSpan ℝ s))

Tactic:
rw [hs, direction_affineSpan, direction_affineSpan, ha.finrank_vectorSpan (Fintype.card_fin _),
    t.independent.finrank_vectorSpan (Fintype.card_fin _)]

Premises used: direction_affineSpan, Fintype.card_fin, AffineIndependent.finrank_vectorSpan, Affine.Simplex.independent
-- Module: Mathlib.Geometry.Euclidean.MongePoint
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
ho : OrthocentricSystem s
rcases :
  ∀ (t : Triangle ℝ P) (hto : t.orthocenter ∉ Set.range t.points) (hts : s = insert t.orthocenter (Set.range t.points)),
    ∃ (r : ℝ), ∀ (t : Triangle ℝ P), Set.range t.points ⊆ s → Simplex.circumradius t = r
⊢ ∃ (r : ℝ), ∀ (t : Triangle ℝ P), Set.range t.points ⊆ s → Simplex.circumradius t = r

Tactic:
rcases ho with ⟨t, hto, hts⟩
-- Module: Mathlib.Geometry.Euclidean.MongePoint
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
t : Triangle ℝ P
hto : t.orthocenter ∉ Set.range t.points
hts : s = insert t.orthocenter (Set.range t.points)
h : ∀ (t_1 : Triangle ℝ P), Set.range t_1.points ⊆ s → Simplex.circumradius t_1 = Simplex.circumradius t
⊢ ∃ (r : ℝ), ∀ (t : Triangle ℝ P), Set.range t.points ⊆ s → Simplex.circumradius t = r

Tactic:
use t.circumradius

Premises used: Affine.Simplex.circumradius
-- Module: Mathlib.Geometry.Euclidean.MongePoint
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
t : Triangle ℝ P
hto : t.orthocenter ∉ Set.range t.points
hts : s = insert t.orthocenter (Set.range t.points)
t₂ : Triangle ℝ P
ht₂ : Set.range t₂.points ⊆ s
⊢ Set.range t₂.points ⊆ s

Tactic:
have ht₂s := ht₂
-- Module: Mathlib.Geometry.Euclidean.MongePoint
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
t : Triangle ℝ P
hto : t.orthocenter ∉ Set.range t.points
hts : s = insert t.orthocenter (Set.range t.points)
t₂ : Triangle ℝ P
ht₂ ht₂s : Set.range t₂.points ⊆ s
⊢ Set.range t₂.points ⊆ insert t.orthocenter (Set.range t.points)

Tactic:
rw [hts] at ht₂
-- Module: Mathlib.Geometry.Euclidean.MongePoint
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
t : Triangle ℝ P
hto : t.orthocenter ∉ Set.range t.points
hts : s = insert t.orthocenter (Set.range t.points)
t₂ : Triangle ℝ P
ht₂ ht₂s : Set.range t₂.points ⊆ s
ht₃ : Set.range t₂.points ⊆ insert t.orthocenter (Set.range t.points)
⊢ Set.range t₂.points ⊆ s

Tactic:
rw [hts] at ht₂
-- Module: Mathlib.Geometry.Euclidean.MongePoint
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
t : Triangle ℝ P
hto : t.orthocenter ∉ Set.range t.points
hts : s = insert t.orthocenter (Set.range t.points)
t₂ : Triangle ℝ P
ht₂ : Set.range t₂.points ⊆ insert t.orthocenter (Set.range t.points)
ht₂s : Set.range t₂.points ⊆ s
h :
  ∀ (c : P) (hc : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range t.points)) c)
    (h : ∀ p₁ ∈ Set.range t₂.points, dist p₁ c = Simplex.circumradius t),
    Simplex.circumradius t₂ = Simplex.circumradius t
⊢ Simplex.circumradius t₂ = Simplex.circumradius t

Tactic:
rcases exists_dist_eq_circumradius_of_subset_insert_orthocenter hto ht₂
      t₂.independent.injective with
    ⟨c, hc, h⟩

Premises used: AffineIndependent.injective, EuclideanGeometry.exists_dist_eq_circumradius_of_subset_insert_orthocenter, Affine.Simplex.independent
-- Module: Mathlib.Geometry.Euclidean.MongePoint
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
t : Triangle ℝ P
hto : t.orthocenter ∉ Set.range t.points
hts : s = insert t.orthocenter (Set.range t.points)
t₂ : Triangle ℝ P
ht₂ : Set.range t₂.points ⊆ insert t.orthocenter (Set.range t.points)
ht₂s : Set.range t₂.points ⊆ s
c : P
hc : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range t.points)) c
h : ∀ p₁ ∈ Set.range t₂.points, dist p₁ c = Simplex.circumradius t
⊢ ∀ (i : Fin 3), dist (t₂.points i) c = Simplex.circumradius t

Tactic:
rw [Set.forall_mem_range] at h

Premises used: Set.forall_mem_range
-- Module: Mathlib.Geometry.Euclidean.MongePoint
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
t : Triangle ℝ P
hto : t.orthocenter ∉ Set.range t.points
hts : s = insert t.orthocenter (Set.range t.points)
t₂ : Triangle ℝ P
ht₂ : Set.range t₂.points ⊆ insert t.orthocenter (Set.range t.points)
ht₂s : Set.range t₂.points ⊆ s
c : P
hc : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range t.points)) c
h : ∀ (i : Fin 3), dist (t₂.points i) c = Simplex.circumradius t
rw : Set.range t.points ⊆ insert t.orthocenter (Set.range t.points)
⊢ Set.range t.points ⊆ s

Tactic:
rw [hts]
-- Module: Mathlib.Geometry.Euclidean.MongePoint
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
t : Triangle ℝ P
hto : t.orthocenter ∉ Set.range t.points
hts : s = insert t.orthocenter (Set.range t.points)
t₂ : Triangle ℝ P
ht₂ : Set.range t₂.points ⊆ insert t.orthocenter (Set.range t.points)
ht₂s : Set.range t₂.points ⊆ s
c : P
hc : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range t.points)) c
h : ∀ (i : Fin 3), dist (t₂.points i) c = Simplex.circumradius t
⊢ Set.range t.points ⊆ insert t.orthocenter (Set.range t.points)

Tactic:
Set.subset_insert _ _

Premises used: Set.subset_insert
-- Module: Mathlib.Geometry.Euclidean.MongePoint
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
t : Triangle ℝ P
hto : t.orthocenter ∉ Set.range t.points
hts : s = insert t.orthocenter (Set.range t.points)
t₂ : Triangle ℝ P
ht₂ : Set.range t₂.points ⊆ insert t.orthocenter (Set.range t.points)
ht₂s : Set.range t₂.points ⊆ s
c : P
hc : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range t.points)) c
h : ∀ (i : Fin 3), dist (t₂.points i) c = Simplex.circumradius t
⊢ Set.range t.points ⊆ insert t.orthocenter (Set.range t.points)

Tactic:
exact Set.subset_insert _ _

Premises used: Set.subset_insert
-- Module: Mathlib.Geometry.Euclidean.MongePoint
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
t : Triangle ℝ P
hto : t.orthocenter ∉ Set.range t.points
hts : s = insert t.orthocenter (Set.range t.points)
t₂ : Triangle ℝ P
ht₂ : Set.range t₂.points ⊆ insert t.orthocenter (Set.range t.points)
ht₂s : Set.range t₂.points ⊆ s
c : P
hc : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range t.points)) c
h : ∀ (i : Fin 3), dist (t₂.points i) c = Simplex.circumradius t
⊢ Set.range t.points ⊆ s

Tactic:
have hs : Set.range t.points ⊆ s := by
    rw [hts]
    exact Set.subset_insert _ _
-- Module: Mathlib.Geometry.Euclidean.MongePoint
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
t : Triangle ℝ P
hto : t.orthocenter ∉ Set.range t.points
hts : s = insert t.orthocenter (Set.range t.points)
t₂ : Triangle ℝ P
ht₂ : Set.range t₂.points ⊆ insert t.orthocenter (Set.range t.points)
ht₂s : Set.range t₂.points ⊆ s
c : P
hc : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range t.points)) c
h : ∀ (i : Fin 3), dist (t₂.points i) c = Simplex.circumradius t
hs : Set.range t.points ⊆ s
⊢ Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range t₂.points)) c

Tactic:
rw [affineSpan_of_orthocentricSystem ⟨t, hto, hts⟩ hs t.independent.injective,
    ← affineSpan_of_orthocentricSystem ⟨t, hto, hts⟩ ht₂s t₂.independent.injective] at hc

Premises used: EuclideanGeometry.affineSpan_of_orthocentricSystem, AffineIndependent.injective, And.intro, Exists.intro, Affine.Simplex.independent
-- Module: Mathlib.Geometry.Euclidean.MongePoint
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
t : Triangle ℝ P
hto : t.orthocenter ∉ Set.range t.points
hts : s = insert t.orthocenter (Set.range t.points)
t₂ : Triangle ℝ P
ht₂ : Set.range t₂.points ⊆ insert t.orthocenter (Set.range t.points)
ht₂s : Set.range t₂.points ⊆ s
c : P
hc : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range t.points)) c
h : ∀ (i : Fin 3), dist (t₂.points i) c = Simplex.circumradius t
hs : Set.range t.points ⊆ s
hc₁ : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range t₂.points)) c
⊢ ∀ (i : Fin 3), dist (t₂.points i) c = Simplex.circumradius t

Tactic:
rw [affineSpan_of_orthocentricSystem ⟨t, hto, hts⟩ hs t.independent.injective,
    ← affineSpan_of_orthocentricSystem ⟨t, hto, hts⟩ ht₂s t₂.independent.injective] at hc

Premises used: EuclideanGeometry.affineSpan_of_orthocentricSystem, AffineIndependent.injective, And.intro, Exists.intro, Affine.Simplex.independent