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
t : Triangle ℝ P
i₁ i₂ : Fin 3
h : i₁ ≠ i₂
⊢ -(∑ x : Fin (0 + 2 + 1),
            (∑ x_1 : Fin (0 + 2 + 1),
                HSub.hSub (α := ℝ) (↑(HAdd.hAdd (α := ℕ) 0 1) : ℝ)⁻¹ (if x = i₁ ∨ x = i₂ then 1 else 0) *
                    HSub.hSub (α := ℝ) (↑(HAdd.hAdd (α := ℕ) 0 1) : ℝ)⁻¹ (if x_1 = i₁ ∨ x_1 = i₂ then 1 else 0) *
                  (dist (pointsWithCircumcenter t (PointsWithCircumcenterIndex.pointIndex x))
                      (pointsWithCircumcenter t (PointsWithCircumcenterIndex.pointIndex x_1)) *
                    dist (pointsWithCircumcenter t (PointsWithCircumcenterIndex.pointIndex x))
                      (pointsWithCircumcenter t (PointsWithCircumcenterIndex.pointIndex x_1))) +
              HSub.hSub (α := ℝ) (↑(HAdd.hAdd (α := ℕ) 0 1) : ℝ)⁻¹ (if x = i₁ ∨ x = i₂ then 1 else 0) *
                  (HDiv.hDiv (α := ℝ) (-2) (↑(HAdd.hAdd (α := ℕ) 0 1) : ℝ) - -1) *
                (dist (pointsWithCircumcenter t (PointsWithCircumcenterIndex.pointIndex x))
                    (pointsWithCircumcenter t PointsWithCircumcenterIndex.circumcenterIndex) *
                  dist (pointsWithCircumcenter t (PointsWithCircumcenterIndex.pointIndex x))
                    (pointsWithCircumcenter t PointsWithCircumcenterIndex.circumcenterIndex))) +
          (∑ x : Fin (0 + 2 + 1),
              (HDiv.hDiv (α := ℝ) (-2) (↑(HAdd.hAdd (α := ℕ) 0 1) : ℝ) - -1) *
                  HSub.hSub (α := ℝ) (↑(HAdd.hAdd (α := ℕ) 0 1) : ℝ)⁻¹ (if x = i₁ ∨ x = i₂ then 1 else 0) *
                (dist (pointsWithCircumcenter t PointsWithCircumcenterIndex.circumcenterIndex)
                    (pointsWithCircumcenter t (PointsWithCircumcenterIndex.pointIndex x)) *
                  dist (pointsWithCircumcenter t PointsWithCircumcenterIndex.circumcenterIndex)
                    (pointsWithCircumcenter t (PointsWithCircumcenterIndex.pointIndex x))) +
            (HDiv.hDiv (α := ℝ) (-2) (↑(HAdd.hAdd (α := ℕ) 0 1) : ℝ) - -1) *
                (HDiv.hDiv (α := ℝ) (-2) (↑(HAdd.hAdd (α := ℕ) 0 1) : ℝ) - -1) *
              (dist (pointsWithCircumcenter t PointsWithCircumcenterIndex.circumcenterIndex)
                  (pointsWithCircumcenter t PointsWithCircumcenterIndex.circumcenterIndex) *
                dist (pointsWithCircumcenter t PointsWithCircumcenterIndex.circumcenterIndex)
                  (pointsWithCircumcenter t PointsWithCircumcenterIndex.circumcenterIndex)))) /
      2 =
    circumradius t * circumradius t
have hu : Subset (α := Finset (Fin 3)) {i₁, i₂} univ
Tactic: have hu : ({i₁, i₂} : Finset (Fin 3)) ⊆ univ := subset_univ _
-- 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
t : Triangle ℝ P
i₁ i₂ : Fin 3
h : i₁ ≠ i₂
⊢ dist t.orthocenter
      ((reflection (affineSpan ℝ (t.points '' (↑{i₁, i₂} : Set (Fin (2 + 1))))) : (a : P) → P) (circumcenter t)) =
    circumradius t
have simp : dist t.orthocenter ((reflection (affineSpan ℝ (t.points '' {i₁, i₂})) : (a : P) → P) (circumcenter t)) = circumradius t
Tactic: simp only [coe_insert, coe_singleton]
-- 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
t : Triangle ℝ P
i₁ i₂ : Fin 3
h : i₁ ≠ i₂
⊢ dist (circumcenter t) ((reflection (affineSpan ℝ (t.points '' {i₁, i₂})) : (a : P) → P) t.orthocenter) =
    circumradius t
have rw : dist ((reflection (affineSpan ℝ (t.points '' {i₁, i₂})) : (a : P) → P) (circumcenter t)) t.orthocenter = circumradius t
Tactic: rw [EuclideanGeometry.dist_reflection, dist_comm, dist_orthocenter_reflection_circumcenter t 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
t : Triangle ℝ P
i₁ i₂ : Fin 3
h : i₁ ≠ i₂
rw :
  dist ((reflection (affineSpan ℝ (t.points '' {i₁, i₂})) : (a : P) → P) (circumcenter t)) t.orthocenter =
    circumradius t
⊢ dist (circumcenter t) ((reflection (affineSpan ℝ (t.points '' {i₁, i₂})) : (a : P) → P) t.orthocenter) =
    circumradius t
have rw₁ : dist t.orthocenter ((reflection (affineSpan ℝ (t.points '' {i₁, i₂})) : (a : P) → P) (circumcenter t)) = circumradius t
Tactic: rw [EuclideanGeometry.dist_reflection, dist_comm, dist_orthocenter_reflection_circumcenter t 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
t : Triangle ℝ P
i₁ i₂ : Fin 3
h : i₁ ≠ i₂
rw :
  dist ((reflection (affineSpan ℝ (t.points '' {i₁, i₂})) : (a : P) → P) (circumcenter t)) t.orthocenter =
    circumradius t
rw₁ :
  dist t.orthocenter ((reflection (affineSpan ℝ (t.points '' {i₁, i₂})) : (a : P) → P) (circumcenter t)) =
    circumradius t
⊢ dist (circumcenter t) ((reflection (affineSpan ℝ (t.points '' {i₁, i₂})) : (a : P) → P) t.orthocenter) =
    circumradius t
have rw₂ : circumradius t = circumradius t
Tactic: rw [EuclideanGeometry.dist_reflection, dist_comm, dist_orthocenter_reflection_circumcenter t 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
t : Triangle ℝ P
i₁ i₂ : Fin 3
h : i₁ ≠ i₂
⊢ dist (circumcenter t)
      ((reflection (affineSpan ℝ (t.points '' (↑{i₁, i₂} : Set (Fin (2 + 1))))) : (a : P) → P) t.orthocenter) =
    circumradius t
have simp : dist (circumcenter t) ((reflection (affineSpan ℝ (t.points '' {i₁, i₂})) : (a : P) → P) t.orthocenter) = circumradius t
Tactic: simp only [coe_insert, coe_singleton]
-- 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
t : Triangle ℝ P
i : Fin 3
⊢ affineSpan ℝ {t.orthocenter, t.points i} ≤ altitude t i
have refine : {t.orthocenter, t.points i} ⊆ (↑(altitude t i) : Set P)
Tactic: refine affineSpan_le_of_subset_coe ?_
-- 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
t : Triangle ℝ P
i : Fin 3
⊢ {t.orthocenter, t.points i} ⊆ (↑(altitude t i) : Set P)
have rw : t.orthocenter ∈ (↑(altitude t i) : Set P) ∧ t.points i ∈ (↑(altitude t i) : Set P)
Tactic: rw [Set.insert_subset_iff, Set.singleton_subset_iff]
-- 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
t₁ t₂ : Triangle ℝ P
i₁ i₂ i₃ j₁ j₂ j₃ : Fin 3
hi₁₂ : i₁ ≠ i₂
hi₁₃ : i₁ ≠ i₃
hi₂₃ : i₂ ≠ i₃
hj₁₂ : j₁ ≠ j₂
hj₁₃ : j₁ ≠ j₃
hj₂₃ : j₂ ≠ j₃
h₁ : t₂.points j₁ = t₁.orthocenter
h₂ : t₂.points j₂ = t₁.points i₂
h₃ : t₂.points j₃ = t₁.points i₃
⊢ altitude t₂ j₂ = affineSpan ℝ {t₁.points i₁, t₁.points i₂}
have symm : affineSpan ℝ {t₁.points i₁, t₁.points i₂} = altitude t₂ j₂
Tactic: symm
-- 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
t₁ t₂ : Triangle ℝ P
i₁ i₂ i₃ j₁ j₂ j₃ : Fin 3
hi₁₂ : i₁ ≠ i₂
hi₁₃ : i₁ ≠ i₃
hi₂₃ : i₂ ≠ i₃
hj₁₂ : j₁ ≠ j₂
hj₁₃ : j₁ ≠ j₃
hj₂₃ : j₂ ≠ j₃
h₁ : t₂.points j₁ = t₁.orthocenter
h₂ : t₂.points j₂ = t₁.points i₂
h₃ : t₂.points j₃ = t₁.points i₃
⊢ affineSpan ℝ {t₁.points i₁, t₁.points i₂} = altitude t₂ j₂
have rw : t₁.points i₁ ≠ t₂.points j₂ ∧
  Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range t₂.points)) (t₁.points i₁) ∧
    Membership.mem (γ := Submodule ℝ V) (direction (affineSpan ℝ (t₂.points '' {j₂}ᶜ)))ᗮ (t₁.points i₁ -ᵥ t₂.points j₂)
Tactic: rw [← h₂, t₂.affineSpan_pair_eq_altitude_iff]
-- 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
t₁ t₂ : Triangle ℝ P
i₁ i₂ i₃ j₁ j₂ j₃ : Fin 3
hi₁₂ : i₁ ≠ i₂
hi₁₃ : i₁ ≠ i₃
hi₂₃ : i₂ ≠ i₃
hj₁₂ : j₁ ≠ j₂
hj₁₃ : j₁ ≠ j₃
hj₂₃ : j₂ ≠ j₃
h₁ : t₂.points j₁ = t₁.orthocenter
h₂ : t₂.points j₂ = t₁.points i₂
h₃ : t₂.points j₃ = t₁.points i₃
⊢ t₁.points i₁ ≠ t₂.points j₂ ∧
    Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range t₂.points)) (t₁.points i₁) ∧
      Membership.mem (γ := Submodule ℝ V) (direction (affineSpan ℝ (t₂.points '' {j₂}ᶜ)))ᗮ
        (t₁.points i₁ -ᵥ t₂.points j₂)
have rw : t₁.points i₁ ≠ t₁.points i₂ ∧
  Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range t₂.points)) (t₁.points i₁) ∧
    Membership.mem (γ := Submodule ℝ V) (direction (affineSpan ℝ (t₂.points '' {j₂}ᶜ)))ᗮ (t₁.points i₁ -ᵥ t₁.points i₂)
Tactic: rw [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
t₁ t₂ : Triangle ℝ P
i₁ i₂ i₃ j₁ j₂ j₃ : Fin 3
hi₁₂ : i₁ ≠ i₂
hi₁₃ : i₁ ≠ i₃
hi₂₃ : i₂ ≠ i₃
hj₁₂ : j₁ ≠ j₂
hj₁₃ : j₁ ≠ j₃
hj₂₃ : j₂ ≠ j₃
h₁ : t₂.points j₁ = t₁.orthocenter
h₂ : t₂.points j₂ = t₁.points i₂
h₃ : t₂.points j₃ = t₁.points i₃
⊢ t₁.points i₁ ≠ t₁.points i₂ ∧
    Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range t₂.points)) (t₁.points i₁) ∧
      Membership.mem (γ := Submodule ℝ V) (direction (affineSpan ℝ (t₂.points '' {j₂}ᶜ)))ᗮ
        (t₁.points i₁ -ᵥ t₁.points i₂)
have right : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range t₂.points)) (t₁.points i₁) ∧
  Membership.mem (γ := Submodule ℝ V) (direction (affineSpan ℝ (t₂.points '' {j₂}ᶜ)))ᗮ (t₁.points i₁ -ᵥ t₁.points i₂)
Tactic: use t₁.independent.injective.ne hi₁₂
-- 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
t₁ t₂ : Triangle ℝ P
i₁ i₂ i₃ j₁ j₂ j₃ : Fin 3
hi₁₂ : i₁ ≠ i₂
hi₁₃ : i₁ ≠ i₃
hi₂₃ : i₂ ≠ i₃
hj₁₂ : j₁ ≠ j₂
hj₁₃ : j₁ ≠ j₃
hj₂₃ : j₂ ≠ j₃
h₁ : t₂.points j₁ = t₁.orthocenter
h₂ : t₂.points j₂ = t₁.points i₂
h₃ : t₂.points j₃ = t₁.points i₃
⊢ Eq (α := AffineSubspace ℝ P) (affineSpan ℝ (Set.range t₂.points)) (affineSpan ℝ (Set.range t₁.points))
have refine : Eq (α := Submodule ℝ V) (direction (affineSpan ℝ (Set.range t₂.points)))
  (direction (affineSpan ℝ (Set.range t₁.points)))
Tactic: refine ext_of_direction_eq ?_
      ⟨t₁.points i₃, mem_affineSpan ℝ ⟨j₃, h₃⟩, mem_affineSpan ℝ (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
t₁ t₂ : Triangle ℝ P
i₁ i₂ i₃ j₁ j₂ j₃ : Fin 3
hi₁₂ : i₁ ≠ i₂
hi₁₃ : i₁ ≠ i₃
hi₂₃ : i₂ ≠ i₃
hj₁₂ : j₁ ≠ j₂
hj₁₃ : j₁ ≠ j₃
hj₂₃ : j₂ ≠ j₃
h₁ : t₂.points j₁ = t₁.orthocenter
h₂ : t₂.points j₂ = t₁.points i₂
h₃ : t₂.points j₃ = t₁.points i₃
⊢ Eq (α := Submodule ℝ V) (direction (affineSpan ℝ (Set.range t₂.points)))
    (direction (affineSpan ℝ (Set.range t₁.points)))
have refine_1 : Set.range t₂.points ⊆ (↑(affineSpan ℝ (Set.range t₁.points)) : Set P)
Tactic: refine Submodule.eq_of_le_of_finrank_eq (direction_le (affineSpan_le_of_subset_coe ?_))
      ?_
-- 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
t₁ t₂ : Triangle ℝ P
i₁ i₂ i₃ j₁ j₂ j₃ : Fin 3
hi₁₂ : i₁ ≠ i₂
hi₁₃ : i₁ ≠ i₃
hi₂₃ : i₂ ≠ i₃
hj₁₂ : j₁ ≠ j₂
hj₁₃ : j₁ ≠ j₃
hj₂₃ : j₂ ≠ j₃
h₁ : t₂.points j₁ = t₁.orthocenter
h₂ : t₂.points j₂ = t₁.points i₂
h₃ : t₂.points j₃ = t₁.points i₃
refine_1 : Set.range t₂.points ⊆ (↑(affineSpan ℝ (Set.range t₁.points)) : Set P)
⊢ Eq (α := Submodule ℝ V) (direction (affineSpan ℝ (Set.range t₂.points)))
    (direction (affineSpan ℝ (Set.range t₁.points)))
have refine_2 : finrank.{0, u_1} ℝ ↥(direction (affineSpan ℝ (Set.range t₂.points))) =
  finrank.{0, u_1} ℝ ↥(direction (affineSpan ℝ (Set.range t₁.points)))
Tactic: refine Submodule.eq_of_le_of_finrank_eq (direction_le (affineSpan_le_of_subset_coe ?_))
      ?_
-- 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
t₁ t₂ : Triangle ℝ P
i₁ i₂ i₃ j₁ j₂ j₃ : Fin 3
hi₁₂ : i₁ ≠ i₂
hi₁₃ : i₁ ≠ i₃
hi₂₃ : i₂ ≠ i₃
hj₁₂ : j₁ ≠ j₂
hj₁₃ : j₁ ≠ j₃
hj₂₃ : j₂ ≠ j₃
h₁ : t₂.points j₁ = t₁.orthocenter
h₂ : t₂.points j₂ = t₁.points i₂
h₃ : t₂.points j₃ = t₁.points i₃
⊢ Set.range t₂.points ⊆ (↑(affineSpan ℝ (Set.range t₁.points)) : Set P)
have hu : Eq (α := Set (Fin 3)) Set.univ {j₁, j₂, j₃}
Tactic: have hu : (Set.univ : Set (Fin 3)) = {j₁, j₂, j₃} := by grind
-- 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
t₁ t₂ : Triangle ℝ P
i₁ i₂ i₃ j₁ j₂ j₃ : Fin 3
hi₁₂ : i₁ ≠ i₂
hi₁₃ : i₁ ≠ i₃
hi₂₃ : i₂ ≠ i₃
hj₁₂ : j₁ ≠ j₂
hj₁₃ : j₁ ≠ j₃
hj₂₃ : j₂ ≠ j₃
h₁ : t₂.points j₁ = t₁.orthocenter
h₂ : t₂.points j₂ = t₁.points i₂
h₃ : t₂.points j₃ = t₁.points i₃
hu : Eq (α := Set (Fin 3)) Set.univ {j₁, j₂, j₃}
⊢ Set.range t₂.points ⊆ (↑(affineSpan ℝ (Set.range t₁.points)) : Set P)
have refine_1 : t₁.orthocenter ∈ (↑(affineSpan ℝ (Set.range t₁.points)) : Set P) ∧
  t₁.points i₂ ∈ (↑(affineSpan ℝ (Set.range t₁.points)) : Set P) ∧
    t₁.points i₃ ∈ (↑(affineSpan ℝ (Set.range t₁.points)) : Set P)
Tactic: rw [← Set.image_univ, hu, Set.image_insert_eq, Set.image_insert_eq, Set.image_singleton, h₁,
        h₂, h₃, Set.insert_subset_iff, Set.insert_subset_iff, Set.singleton_subset_iff]
-- 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
t₁ t₂ : Triangle ℝ P
i₁ i₂ i₃ j₁ j₂ j₃ : Fin 3
hi₁₂ : i₁ ≠ i₂
hi₁₃ : i₁ ≠ i₃
hi₂₃ : i₂ ≠ i₃
hj₁₂ : j₁ ≠ j₂
hj₁₃ : j₁ ≠ j₃
hj₂₃ : j₂ ≠ j₃
h₁ : t₂.points j₁ = t₁.orthocenter
h₂ : t₂.points j₂ = t₁.points i₂
h₃ : t₂.points j₃ = t₁.points i₃
⊢ finrank.{0, u_1} ℝ ↥(direction (affineSpan ℝ (Set.range t₂.points))) =
    finrank.{0, u_1} ℝ ↥(direction (affineSpan ℝ (Set.range t₁.points)))
have refine_2 : finrank.{0, u_1} ℝ ↥(vectorSpan ℝ (Set.range t₂.points)) =
  finrank.{0, u_1} ℝ ↥(direction (affineSpan ℝ (Set.range t₁.points)))
Tactic: rw [direction_affineSpan, direction_affineSpan,
        t₁.independent.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
t₁ t₂ : Triangle ℝ P
i₁ i₂ i₃ j₁ j₂ j₃ : Fin 3
hi₁₂ : i₁ ≠ i₂
hi₁₃ : i₁ ≠ i₃
hi₂₃ : i₂ ≠ i₃
hj₁₂ : j₁ ≠ j₂
hj₁₃ : j₁ ≠ j₃
hj₂₃ : j₂ ≠ j₃
h₁ : t₂.points j₁ = t₁.orthocenter
h₂ : t₂.points j₂ = t₁.points i₂
h₃ : t₂.points j₃ = t₁.points i₃
refine_2 :
  finrank.{0, u_1} ℝ ↥(vectorSpan ℝ (Set.range t₂.points)) =
    finrank.{0, u_1} ℝ ↥(direction (affineSpan ℝ (Set.range t₁.points)))
⊢ finrank.{0, u_1} ℝ ↥(direction (affineSpan ℝ (Set.range t₂.points))) =
    finrank.{0, u_1} ℝ ↥(direction (affineSpan ℝ (Set.range t₁.points)))
have refine_2₁ : finrank.{0, u_1} ℝ ↥(vectorSpan ℝ (Set.range t₂.points)) = finrank.{0, u_1} ℝ ↥(vectorSpan ℝ (Set.range t₁.points))
Tactic: rw [direction_affineSpan, direction_affineSpan,
        t₁.independent.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
t₁ t₂ : Triangle ℝ P
i₁ i₂ i₃ j₁ j₂ j₃ : Fin 3
hi₁₂ : i₁ ≠ i₂
hi₁₃ : i₁ ≠ i₃
hi₂₃ : i₂ ≠ i₃
hj₁₂ : j₁ ≠ j₂
hj₁₃ : j₁ ≠ j₃
hj₂₃ : j₂ ≠ j₃
h₁ : t₂.points j₁ = t₁.orthocenter
h₂ : t₂.points j₂ = t₁.points i₂
h₃ : t₂.points j₃ = t₁.points i₃
refine_2 :
  finrank.{0, u_1} ℝ ↥(vectorSpan ℝ (Set.range t₂.points)) =
    finrank.{0, u_1} ℝ ↥(direction (affineSpan ℝ (Set.range t₁.points)))
refine_2₁ :
  finrank.{0, u_1} ℝ ↥(vectorSpan ℝ (Set.range t₂.points)) = finrank.{0, u_1} ℝ ↥(vectorSpan ℝ (Set.range t₁.points))
⊢ finrank.{0, u_1} ℝ ↥(direction (affineSpan ℝ (Set.range t₂.points))) =
    finrank.{0, u_1} ℝ ↥(direction (affineSpan ℝ (Set.range t₁.points)))
have refine_2₂ : finrank.{0, u_1} ℝ ↥(vectorSpan ℝ (Set.range t₂.points)) = 2
Tactic: rw [direction_affineSpan, direction_affineSpan,
        t₁.independent.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
t₁ t₂ : Triangle ℝ P
i₁ i₂ i₃ j₁ j₂ j₃ : Fin 3
hi₁₂ : i₁ ≠ i₂
hi₁₃ : i₁ ≠ i₃
hi₂₃ : i₂ ≠ i₃
hj₁₂ : j₁ ≠ j₂
hj₁₃ : j₁ ≠ j₃
hj₂₃ : j₂ ≠ j₃
h₁ : t₂.points j₁ = t₁.orthocenter
h₂ : t₂.points j₂ = t₁.points i₂
h₃ : t₂.points j₃ = t₁.points i₃
refine_2 :
  finrank.{0, u_1} ℝ ↥(vectorSpan ℝ (Set.range t₂.points)) =
    finrank.{0, u_1} ℝ ↥(direction (affineSpan ℝ (Set.range t₁.points)))
refine_2₁ :
  finrank.{0, u_1} ℝ ↥(vectorSpan ℝ (Set.range t₂.points)) = finrank.{0, u_1} ℝ ↥(vectorSpan ℝ (Set.range t₁.points))
refine_2₂ : finrank.{0, u_1} ℝ ↥(vectorSpan ℝ (Set.range t₂.points)) = 2
⊢ finrank.{0, u_1} ℝ ↥(direction (affineSpan ℝ (Set.range t₂.points))) =
    finrank.{0, u_1} ℝ ↥(direction (affineSpan ℝ (Set.range t₁.points)))
have refine_2₃ : Eq (α := ℕ) 2 2
Tactic: rw [direction_affineSpan, direction_affineSpan,
        t₁.independent.finrank_vectorSpan (Fintype.card_fin _),
        t₂.independent.finrank_vectorSpan (Fintype.card_fin _)]
-- 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
t₁ t₂ : Triangle ℝ P
i₁ i₂ i₃ j₁ j₂ j₃ : Fin 3
hi₁₂ : i₁ ≠ i₂
hi₁₃ : i₁ ≠ i₃
hi₂₃ : i₂ ≠ i₃
hj₁₂ : j₁ ≠ j₂
hj₁₃ : j₁ ≠ j₃
hj₂₃ : j₂ ≠ j₃
h₁ : t₂.points j₁ = t₁.orthocenter
h₂ : t₂.points j₂ = t₁.points i₂
h₃ : t₂.points j₃ = t₁.points i₃
⊢ Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range t₂.points)) (t₁.points i₁) ∧
    Membership.mem (γ := Submodule ℝ V) (direction (affineSpan ℝ (t₂.points '' {j₂}ᶜ)))ᗮ (t₁.points i₁ -ᵥ t₁.points i₂)
have he : Eq (α := AffineSubspace ℝ P) (affineSpan ℝ (Set.range t₂.points)) (affineSpan ℝ (Set.range t₁.points))
Tactic: have he : affineSpan ℝ (Set.range t₂.points) = affineSpan ℝ (Set.range t₁.points) := by
    refine ext_of_direction_eq ?_
      ⟨t₁.points i₃, mem_affineSpan ℝ ⟨j₃, h₃⟩, mem_affineSpan ℝ (Set.mem_range_self _)⟩
    refine Submodule.eq_of_le_of_finrank_eq (direction_le (affineSpan_le_of_subset_coe ?_))
      ?_
    · have hu : (Set.univ : Set (Fin 3)) = {j₁, j₂, j₃} := by grind
      rw [← Set.image_univ, hu, Set.image_insert_eq, Set.image_insert_eq, Set.image_singleton, h₁,
        h₂, h₃, Set.insert_subset_iff, Set.insert_subset_iff, Set.singleton_subset_iff]
      exact
        ⟨t₁.orthocenter_mem_affineSpan, mem_affineSpan ℝ (Set.mem_range_self _),
          mem_affineSpan ℝ (Set.mem_range_self _)⟩
    · rw [direction_affineSpan, direction_affineSpan,
        t₁.independent.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
t₁ t₂ : Triangle ℝ P
i₁ i₂ i₃ j₁ j₂ j₃ : Fin 3
hi₁₂ : i₁ ≠ i₂
hi₁₃ : i₁ ≠ i₃
hi₂₃ : i₂ ≠ i₃
hj₁₂ : j₁ ≠ j₂
hj₁₃ : j₁ ≠ j₃
hj₂₃ : j₂ ≠ j₃
h₁ : t₂.points j₁ = t₁.orthocenter
h₂ : t₂.points j₂ = t₁.points i₂
h₃ : t₂.points j₃ = t₁.points i₃
he : Eq (α := AffineSubspace ℝ P) (affineSpan ℝ (Set.range t₂.points)) (affineSpan ℝ (Set.range t₁.points))
⊢ Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range t₂.points)) (t₁.points i₁) ∧
    Membership.mem (γ := Submodule ℝ V) (direction (affineSpan ℝ (t₂.points '' {j₂}ᶜ)))ᗮ (t₁.points i₁ -ᵥ t₁.points i₂)
have right : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range t₁.points)) (t₁.points i₁) ∧
  Membership.mem (γ := Submodule ℝ V) (direction (affineSpan ℝ (t₂.points '' {j₂}ᶜ)))ᗮ (t₁.points i₁ -ᵥ t₁.points i₂)
Tactic: rw [he]
-- 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
t₁ t₂ : Triangle ℝ P
i₁ i₂ i₃ j₁ j₂ j₃ : Fin 3
hi₁₂ : i₁ ≠ i₂
hi₁₃ : i₁ ≠ i₃
hi₂₃ : i₂ ≠ i₃
hj₁₂ : j₁ ≠ j₂
hj₁₃ : j₁ ≠ j₃
hj₂₃ : j₂ ≠ j₃
h₁ : t₂.points j₁ = t₁.orthocenter
h₂ : t₂.points j₂ = t₁.points i₂
h₃ : t₂.points j₃ = t₁.points i₃
he : Eq (α := AffineSubspace ℝ P) (affineSpan ℝ (Set.range t₂.points)) (affineSpan ℝ (Set.range t₁.points))
⊢ Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range t₁.points)) (t₁.points i₁) ∧
    Membership.mem (γ := Submodule ℝ V) (direction (affineSpan ℝ (t₂.points '' {j₂}ᶜ)))ᗮ (t₁.points i₁ -ᵥ t₁.points i₂)
have right : Membership.mem (γ := Submodule ℝ V) (direction (affineSpan ℝ (t₂.points '' {j₂}ᶜ)))ᗮ (t₁.points i₁ -ᵥ t₁.points i₂)
Tactic: use mem_affineSpan ℝ (Set.mem_range_self _)
-- 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
t₁ t₂ : Triangle ℝ P
i₁ i₂ i₃ j₁ j₂ j₃ : Fin 3
hi₁₂ : i₁ ≠ i₂
hi₁₃ : i₁ ≠ i₃
hi₂₃ : i₂ ≠ i₃
hj₁₂ : j₁ ≠ j₂
hj₁₃ : j₁ ≠ j₃
hj₂₃ : j₂ ≠ j₃
h₁ : t₂.points j₁ = t₁.orthocenter
h₂ : t₂.points j₂ = t₁.points i₂
h₃ : t₂.points j₃ = t₁.points i₃
he : Eq (α := AffineSubspace ℝ P) (affineSpan ℝ (Set.range t₂.points)) (affineSpan ℝ (Set.range t₁.points))
⊢ Membership.mem (γ := Submodule ℝ V) (direction (affineSpan ℝ (t₂.points '' {j₂}ᶜ)))ᗮ (t₁.points i₁ -ᵥ t₁.points i₂)
have hu : Eq (α := Set (Fin 3)) {j₂}ᶜ {j₁, j₃}
Tactic: have hu : ({j₂}ᶜ : Set _) = {j₁, j₃} := by grind
-- 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
t₁ t₂ : Triangle ℝ P
i₁ i₂ i₃ j₁ j₂ j₃ : Fin 3
hi₁₂ : i₁ ≠ i₂
hi₁₃ : i₁ ≠ i₃
hi₂₃ : i₂ ≠ i₃
hj₁₂ : j₁ ≠ j₂
hj₁₃ : j₁ ≠ j₃
hj₂₃ : j₂ ≠ j₃
h₁ : t₂.points j₁ = t₁.orthocenter
h₂ : t₂.points j₂ = t₁.points i₂
h₃ : t₂.points j₃ = t₁.points i₃
he : Eq (α := AffineSubspace ℝ P) (affineSpan ℝ (Set.range t₂.points)) (affineSpan ℝ (Set.range t₁.points))
hu : Eq (α := Set (Fin 3)) {j₂}ᶜ {j₁, j₃}
⊢ Membership.mem (γ := Submodule ℝ V) (direction (affineSpan ℝ (t₂.points '' {j₂}ᶜ)))ᗮ (t₁.points i₁ -ᵥ t₁.points i₂)
have right : Membership.mem (γ := Submodule ℝ V) (direction (P := P) (affineSpan ℝ {t₁.orthocenter, t₁.points i₃}))ᗮ
  (t₁.points i₁ -ᵥ t₁.points i₂)
Tactic: rw [hu, Set.image_insert_eq, Set.image_singleton, h₁, h₃]