awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.MongePoint (hypothesis)
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 ℝ (Set.range p)) (affineSpan ℝ s)
have hs : 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]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.MongePoint (goal)
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)
have refine : Eq (α := Submodule ℝ V) (direction (affineSpan ℝ (Set.range p))) (direction (affineSpan ℝ s))
Tactic: refine ext_of_direction_eq ?_
    ⟨p 0, mem_affineSpan ℝ (Set.mem_range_self _), mem_affineSpan ℝ (hps (Set.mem_range_self _))⟩
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.MongePoint (goal)
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))
have rw : FiniteDimensional.{0, u_1} ℝ ↥(direction (affineSpan ℝ (Set.range t.points)))
Tactic: rw [hs]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.MongePoint (hypothesis)
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 (α := Submodule ℝ V) (direction (affineSpan ℝ (Set.range p))) (direction (affineSpan ℝ s))
have hfd : FiniteDimensional.{0, u_1} ℝ ↥(direction (affineSpan ℝ s))
Tactic: have hfd : FiniteDimensional ℝ (affineSpan ℝ s).direction := by rw [hs]; infer_instance
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.MongePoint (goal)
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))
⊢ finrank.{0, u_1} ℝ ↥(direction (affineSpan ℝ (Set.range p))) = finrank.{0, u_1} ℝ ↥(direction (affineSpan ℝ s))
have rw : finrank.{0, u_1} ℝ ↥(direction (affineSpan ℝ (Set.range p))) =
  finrank.{0, u_1} ℝ ↥(direction (affineSpan ℝ (Set.range t.points)))
Tactic: rw [hs, direction_affineSpan, direction_affineSpan, ha.finrank_vectorSpan (Fintype.card_fin _),
    t.independent.finrank_vectorSpan (Fintype.card_fin _)]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.MongePoint (goal)
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)))
⊢ finrank.{0, u_1} ℝ ↥(direction (affineSpan ℝ (Set.range p))) = finrank.{0, u_1} ℝ ↥(direction (affineSpan ℝ s))
have rw₁ : finrank.{0, u_1} ℝ ↥(vectorSpan ℝ (Set.range p)) = finrank.{0, u_1} ℝ ↥(direction (affineSpan ℝ (Set.range t.points)))
Tactic: rw [hs, direction_affineSpan, direction_affineSpan, ha.finrank_vectorSpan (Fintype.card_fin _),
    t.independent.finrank_vectorSpan (Fintype.card_fin _)]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.MongePoint (goal)
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)))
⊢ finrank.{0, u_1} ℝ ↥(direction (affineSpan ℝ (Set.range p))) = finrank.{0, u_1} ℝ ↥(direction (affineSpan ℝ s))
have rw₂ : finrank.{0, u_1} ℝ ↥(vectorSpan ℝ (Set.range p)) = finrank.{0, u_1} ℝ ↥(vectorSpan ℝ (Set.range t.points))
Tactic: rw [hs, direction_affineSpan, direction_affineSpan, ha.finrank_vectorSpan (Fintype.card_fin _),
    t.independent.finrank_vectorSpan (Fintype.card_fin _)]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.MongePoint (goal)
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))
⊢ finrank.{0, u_1} ℝ ↥(direction (affineSpan ℝ (Set.range p))) = finrank.{0, u_1} ℝ ↥(direction (affineSpan ℝ s))
have rw₃ : 2 = finrank.{0, u_1} ℝ ↥(vectorSpan ℝ (Set.range t.points))
Tactic: rw [hs, direction_affineSpan, direction_affineSpan, ha.finrank_vectorSpan (Fintype.card_fin _),
    t.independent.finrank_vectorSpan (Fintype.card_fin _)]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.MongePoint (goal)
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))
⊢ finrank.{0, u_1} ℝ ↥(direction (affineSpan ℝ (Set.range p))) = finrank.{0, u_1} ℝ ↥(direction (affineSpan ℝ s))
have rw₄ : Eq (α := ℕ) 2 2
Tactic: rw [hs, direction_affineSpan, direction_affineSpan, ha.finrank_vectorSpan (Fintype.card_fin _),
    t.independent.finrank_vectorSpan (Fintype.card_fin _)]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.MongePoint (goal)
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
⊢ ∃ (r : ℝ), ∀ (t : Triangle ℝ P), Set.range t.points ⊆ s → Simplex.circumradius t = r
have 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
Tactic: rcases ho with ⟨t, hto, hts⟩
Cleared hypotheses: ho
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.MongePoint (goal)
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)
⊢ ∃ (r : ℝ), ∀ (t : Triangle ℝ P), Set.range t.points ⊆ s → Simplex.circumradius t = r
have h : ∀ (t_1 : Triangle ℝ P), Set.range t_1.points ⊆ s → Simplex.circumradius t_1 = Simplex.circumradius t
Tactic: use t.circumradius
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.MongePoint (hypothesis)
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
⊢ Simplex.circumradius t₂ = Simplex.circumradius t
have ht₃ : Set.range t₂.points ⊆ insert t.orthocenter (Set.range t.points)
Tactic: rw [hts] at ht₂
Cleared hypotheses: ht₂, ht₂s
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.MongePoint (goal)
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
⊢ Simplex.circumradius t₂ = Simplex.circumradius t
have 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
Tactic: rcases exists_dist_eq_circumradius_of_subset_insert_orthocenter hto ht₂
      t₂.independent.injective with
    ⟨c, hc, h⟩
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.MongePoint (hypothesis)
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
⊢ Simplex.circumradius t₂ = Simplex.circumradius t
have h₁ : ∀ (i : Fin 3), dist (t₂.points i) c = Simplex.circumradius t
Tactic: rw [Set.forall_mem_range] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.MongePoint (goal)
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
have rw : Set.range t.points ⊆ insert t.orthocenter (Set.range t.points)
Tactic: rw [hts]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.MongePoint (hypothesis)
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
⊢ Simplex.circumradius t₂ = Simplex.circumradius t
have hs : Set.range t.points ⊆ s
Tactic: have hs : Set.range t.points ⊆ s := by
    rw [hts]
    exact Set.subset_insert _ _
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.MongePoint (hypothesis)
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
⊢ Simplex.circumradius t₂ = Simplex.circumradius t
have hc₁ : 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
Cleared hypotheses: hc, h, hs
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.MongePoint (goal)
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
t : Triangle ℝ P
ht : Set.range t.points ⊆ s
⊢ s = insert t.orthocenter (Set.range t.points)
have rcases : ∀ (t₀ : Triangle ℝ P) (ht₀o : t₀.orthocenter ∉ Set.range t₀.points)
  (ht₀s : s = insert t₀.orthocenter (Set.range t₀.points)), s = insert t.orthocenter (Set.range t.points)
Tactic: rcases ho with ⟨t₀, ht₀o, ht₀s⟩
Cleared hypotheses: ho
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.MongePoint (hypothesis)
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
ht : Set.range t.points ⊆ s
t₀ : Triangle ℝ P
ht₀o : t₀.orthocenter ∉ Set.range t₀.points
ht₀s : s = insert t₀.orthocenter (Set.range t₀.points)
⊢ s = insert t.orthocenter (Set.range t.points)
have ht₁ : Set.range t.points ⊆ insert t₀.orthocenter (Set.range t₀.points)
Tactic: rw [ht₀s] at ht
Cleared hypotheses: ht, ht₀o, ht₀s
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.MongePoint (goal)
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 t₀ : Triangle ℝ P
ht : Set.range t.points ⊆ insert t₀.orthocenter (Set.range t₀.points)
ht₀o : t₀.orthocenter ∉ Set.range t₀.points
ht₀s : s = insert t₀.orthocenter (Set.range t₀.points)
⊢ s = insert t.orthocenter (Set.range t.points)
have inl : ∀ (i₁ i₂ i₃ j₂ j₃ : Fin 3) (h₁₂ : i₁ ≠ i₂) (h₁₃ : i₁ ≠ i₃) (h₂₃ : i₂ ≠ i₃)
  (h₁₂₃ : ∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃) (h₁ : t.points i₁ = t₀.orthocenter) (hj₂₃ : j₂ ≠ j₃)
  (h₂ : t₀.points j₂ = t.points i₂) (h₃ : t₀.points j₃ = t.points i₃), s = insert t.orthocenter (Set.range t.points)
Tactic: rcases exists_of_range_subset_orthocentricSystem ht₀o ht t.independent.injective with
    (⟨i₁, i₂, i₃, j₂, j₃, h₁₂, h₁₃, h₂₃, h₁₂₃, h₁, hj₂₃, h₂, h₃⟩ | hs)
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.MongePoint (goal)
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 t₀ : Triangle ℝ P
ht : Set.range t.points ⊆ insert t₀.orthocenter (Set.range t₀.points)
ht₀o : t₀.orthocenter ∉ Set.range t₀.points
ht₀s : s = insert t₀.orthocenter (Set.range t₀.points)
inl :
  ∀ (i₁ i₂ i₃ j₂ j₃ : Fin 3) (h₁₂ : i₁ ≠ i₂) (h₁₃ : i₁ ≠ i₃) (h₂₃ : i₂ ≠ i₃)
    (h₁₂₃ : ∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃) (h₁ : t.points i₁ = t₀.orthocenter) (hj₂₃ : j₂ ≠ j₃)
    (h₂ : t₀.points j₂ = t.points i₂) (h₃ : t₀.points j₃ = t.points i₃), s = insert t.orthocenter (Set.range t.points)
⊢ s = insert t.orthocenter (Set.range t.points)
have inr : ∀ (hs : Set.range t.points = Set.range t₀.points), s = insert t.orthocenter (Set.range t.points)
Tactic: rcases exists_of_range_subset_orthocentricSystem ht₀o ht t.independent.injective with
    (⟨i₁, i₂, i₃, j₂, j₃, h₁₂, h₁₃, h₂₃, h₁₂₃, h₁, hj₂₃, h₂, h₃⟩ | hs)
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.MongePoint (goal)
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 t₀ : Triangle ℝ P
ht : Set.range t.points ⊆ insert t₀.orthocenter (Set.range t₀.points)
ht₀o : t₀.orthocenter ∉ Set.range t₀.points
ht₀s : s = insert t₀.orthocenter (Set.range t₀.points)
i₁ i₂ i₃ j₂ j₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
h₁₂₃ : ∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃
h₁ : t.points i₁ = t₀.orthocenter
hj₂₃ : j₂ ≠ j₃
h₂ : t₀.points j₂ = t.points i₂
h₃ : t₀.points j₃ = t.points i₃
⊢ s = insert t.orthocenter (Set.range t.points)
have inl : ∀ (j₁ : Fin 3) (hj₁₂ : j₁ ≠ j₂) (hj₁₃ : j₁ ≠ j₃) (hj₁₂₃ : ∀ (j : Fin 3), j = j₁ ∨ j = j₂ ∨ j = j₃),
  s = insert t.orthocenter (Set.range t.points)
Tactic: obtain ⟨j₁, hj₁₂, hj₁₃, hj₁₂₃⟩ :
        ∃ j₁ : Fin 3, j₁ ≠ j₂ ∧ j₁ ≠ j₃ ∧ ∀ j : Fin 3, j = j₁ ∨ j = j₂ ∨ j = j₃ := by
      clear h₂ h₃
      decide +revert
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.MongePoint (goal)
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 t₀ : Triangle ℝ P
ht : Set.range t.points ⊆ insert t₀.orthocenter (Set.range t₀.points)
ht₀o : t₀.orthocenter ∉ Set.range t₀.points
ht₀s : s = insert t₀.orthocenter (Set.range t₀.points)
i₁ i₂ i₃ j₂ j₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
h₁₂₃ : ∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃
h₁ : t.points i₁ = t₀.orthocenter
hj₂₃ : j₂ ≠ j₃
h₂ : t₀.points j₂ = t.points i₂
h₃ : t₀.points j₃ = t.points i₃
j₁ : Fin 3
hj₁₂ : j₁ ≠ j₂
hj₁₃ : j₁ ≠ j₃
hj₁₂₃ : ∀ (j : Fin 3), j = j₁ ∨ j = j₂ ∨ j = j₃
h : t₀.points j₁ = t.orthocenter
⊢ Eq (α := Set (Fin 3)) Set.univ {i₁, i₂, i₃}
have h₄ : ∀ (x : Fin 3), Membership.mem (γ := Set (Fin 3)) Set.univ x ↔ Membership.mem (γ := Set (Fin 3)) {i₁, i₂, i₃} x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.MongePoint (hypothesis)
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 t₀ : Triangle ℝ P
ht : Set.range t.points ⊆ insert t₀.orthocenter (Set.range t₀.points)
ht₀o : t₀.orthocenter ∉ Set.range t₀.points
ht₀s : s = insert t₀.orthocenter (Set.range t₀.points)
i₁ i₂ i₃ j₂ j₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
h₁₂₃ : ∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃
h₁ : t.points i₁ = t₀.orthocenter
hj₂₃ : j₂ ≠ j₃
h₂ : t₀.points j₂ = t.points i₂
h₃ : t₀.points j₃ = t.points i₃
j₁ : Fin 3
hj₁₂ : j₁ ≠ j₂
hj₁₃ : j₁ ≠ j₃
hj₁₂₃ : ∀ (j : Fin 3), j = j₁ ∨ j = j₂ ∨ j = j₃
h : t₀.points j₁ = t.orthocenter
⊢ s = insert t.orthocenter (Set.range t.points)
have hui : Eq (α := Set (Fin 3)) Set.univ {i₁, i₂, i₃}
Tactic: have hui : (Set.univ : Set (Fin 3)) = {i₁, i₂, i₃} := by ext x; simpa using h₁₂₃ x
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.MongePoint (goal)
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 t₀ : Triangle ℝ P
ht : Set.range t.points ⊆ insert t₀.orthocenter (Set.range t₀.points)
ht₀o : t₀.orthocenter ∉ Set.range t₀.points
ht₀s : s = insert t₀.orthocenter (Set.range t₀.points)
i₁ i₂ i₃ j₂ j₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
h₁₂₃ : ∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃
h₁ : t.points i₁ = t₀.orthocenter
hj₂₃ : j₂ ≠ j₃
h₂ : t₀.points j₂ = t.points i₂
h₃ : t₀.points j₃ = t.points i₃
j₁ : Fin 3
hj₁₂ : j₁ ≠ j₂
hj₁₃ : j₁ ≠ j₃
hj₁₂₃ : ∀ (j : Fin 3), j = j₁ ∨ j = j₂ ∨ j = j₃
h : t₀.points j₁ = t.orthocenter
hui : Eq (α := Set (Fin 3)) Set.univ {i₁, i₂, i₃}
⊢ Eq (α := Set (Fin 3)) Set.univ {j₁, j₂, j₃}
have h₄ : ∀ (x : Fin 3), Membership.mem (γ := Set (Fin 3)) Set.univ x ↔ Membership.mem (γ := Set (Fin 3)) {j₁, j₂, j₃} x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.MongePoint (hypothesis)
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 t₀ : Triangle ℝ P
ht : Set.range t.points ⊆ insert t₀.orthocenter (Set.range t₀.points)
ht₀o : t₀.orthocenter ∉ Set.range t₀.points
ht₀s : s = insert t₀.orthocenter (Set.range t₀.points)
i₁ i₂ i₃ j₂ j₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
h₁₂₃ : ∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃
h₁ : t.points i₁ = t₀.orthocenter
hj₂₃ : j₂ ≠ j₃
h₂ : t₀.points j₂ = t.points i₂
h₃ : t₀.points j₃ = t.points i₃
j₁ : Fin 3
hj₁₂ : j₁ ≠ j₂
hj₁₃ : j₁ ≠ j₃
hj₁₂₃ : ∀ (j : Fin 3), j = j₁ ∨ j = j₂ ∨ j = j₃
h : t₀.points j₁ = t.orthocenter
hui : Eq (α := Set (Fin 3)) Set.univ {i₁, i₂, i₃}
⊢ s = insert t.orthocenter (Set.range t.points)
have huj : Eq (α := Set (Fin 3)) Set.univ {j₁, j₂, j₃}
Tactic: have huj : (Set.univ : Set (Fin 3)) = {j₁, j₂, j₃} := by ext x; simpa using hj₁₂₃ x
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.MongePoint (goal)
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 t₀ : Triangle ℝ P
ht : Set.range t.points ⊆ insert t₀.orthocenter (Set.range t₀.points)
ht₀o : t₀.orthocenter ∉ Set.range t₀.points
ht₀s : s = insert t₀.orthocenter (Set.range t₀.points)
i₁ i₂ i₃ j₂ j₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
h₁₂₃ : ∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃
h₁ : t.points i₁ = t₀.orthocenter
hj₂₃ : j₂ ≠ j₃
h₂ : t₀.points j₂ = t.points i₂
h₃ : t₀.points j₃ = t.points i₃
j₁ : Fin 3
hj₁₂ : j₁ ≠ j₂
hj₁₃ : j₁ ≠ j₃
hj₁₂₃ : ∀ (j : Fin 3), j = j₁ ∨ j = j₂ ∨ j = j₃
h : t₀.points j₁ = t.orthocenter
hui : Eq (α := Set (Fin 3)) Set.univ {i₁, i₂, i₃}
huj : Eq (α := Set (Fin 3)) Set.univ {j₁, j₂, j₃}
⊢ s = insert t.orthocenter (Set.range t.points)
have rw : insert t₀.orthocenter (t₀.points '' {j₁, j₂, j₃}) = insert (t₀.points j₁) (t.points '' {i₁, i₂, i₃})
Tactic: rw [← h, ht₀s, ← Set.image_univ, huj, ← Set.image_univ, hui]