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₁ 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₃
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₂)
⊢ affineSpan ℝ {t₁.points i₁, t₁.points i₂} = altitude t₂ j₂

Tactic:
rw [← h₂, t₂.affineSpan_pair_eq_altitude_iff]

Premises used: Affine.Simplex.affineSpan_pair_eq_altitude_iff
-- 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₁ 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₃
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₂)
⊢ 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₂]
-- 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₁ 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₃
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₂)
⊢ 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:
use t₁.independent.injective.ne hi₁₂

Premises used: Function.Injective.ne, AffineIndependent.injective, 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
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))

Tactic:
ext_of_direction_eq ?_
      ⟨t₁.points i₃, mem_affineSpan ℝ ⟨j₃, h₃⟩, mem_affineSpan ℝ (Set.mem_range_self _)⟩

Premises used: Set.mem_range_self, Affine.Simplex.points, Real, mem_affineSpan, And.intro, Exists.intro, AffineSubspace.ext_of_direction_eq
-- 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₁ 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 :
  Eq (α := Submodule ℝ V) (direction (affineSpan ℝ (Set.range t₂.points)))
    (direction (affineSpan ℝ (Set.range t₁.points)))
⊢ Eq (α := AffineSubspace ℝ P) (affineSpan ℝ (Set.range t₂.points)) (affineSpan ℝ (Set.range t₁.points))

Tactic:
refine ext_of_direction_eq ?_
      ⟨t₁.points i₃, mem_affineSpan ℝ ⟨j₃, h₃⟩, mem_affineSpan ℝ (Set.mem_range_self _)⟩
-- 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₁ 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)))

Tactic:
Submodule.eq_of_le_of_finrank_eq (direction_le (affineSpan_le_of_subset_coe ?_))
      ?_

Premises used: AffineSubspace.direction_le, affineSpan_le_of_subset_coe, Submodule.eq_of_le_of_finrank_eq
-- 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₁ 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)
refine_2 :
  finrank.{0, u_1} ℝ ↥(direction (affineSpan ℝ (Set.range t₂.points))) =
    finrank.{0, u_1} ℝ ↥(direction (affineSpan ℝ (Set.range t₁.points)))
⊢ Eq (α := Submodule ℝ V) (direction (affineSpan ℝ (Set.range t₂.points)))
    (direction (affineSpan ℝ (Set.range t₁.points)))

Tactic:
refine Submodule.eq_of_le_of_finrank_eq (direction_le (affineSpan_le_of_subset_coe ?_))
      ?_

Premises used: AffineSubspace.direction_le, affineSpan_le_of_subset_coe, Submodule.eq_of_le_of_finrank_eq
-- 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₁ 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 (α := Set (Fin 3)) Set.univ {j₁, j₂, j₃}

Tactic:
grind
-- 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₁ 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 (α := Set (Fin 3)) Set.univ {j₁, j₂, j₃}

Tactic:
have hu : (Set.univ : Set (Fin 3)) = {j₁, j₂, j₃} := by grind
-- 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₁ 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₃}
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)
⊢ Set.range t₂.points ⊆ (↑(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]

Premises used: Set.singleton_subset_iff, Set.image_univ, Set.image_singleton, Set.insert_subset_iff, Set.image_insert_eq
-- 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₁ 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₃}
⊢ 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:
⟨t₁.orthocenter_mem_affineSpan, mem_affineSpan ℝ (Set.mem_range_self _),
          mem_affineSpan ℝ (Set.mem_range_self _)⟩

Premises used: Set.mem_range_self, Real, mem_affineSpan, And.intro, Affine.Triangle.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
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₃}
⊢ 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:
exact
        ⟨t₁.orthocenter_mem_affineSpan, mem_affineSpan ℝ (Set.mem_range_self _),
          mem_affineSpan ℝ (Set.mem_range_self _)⟩
-- 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₁ 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
refine_2₃ refine_2₄ : Eq (α := ℕ) 2 2
⊢ finrank.{0, u_1} ℝ ↥(direction (affineSpan ℝ (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 _)]

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
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))

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 _)]
-- 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₁ 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))
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₂)
⊢ 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]
-- 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₁ 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))
right :
  Membership.mem (γ := Submodule ℝ V) (direction (affineSpan ℝ (t₂.points '' {j₂}ᶜ)))ᗮ (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:
use mem_affineSpan ℝ (Set.mem_range_self _)

Premises used: Set.mem_range_self, Real, 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
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))
⊢ Eq (α := Set (Fin 3)) {j₂}ᶜ {j₁, j₃}

Tactic:
grind
-- 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₁ 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))
⊢ Eq (α := Set (Fin 3)) {j₂}ᶜ {j₁, j₃}

Tactic:
have hu : ({j₂}ᶜ : Set _) = {j₁, j₃} := by grind
-- 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₁ 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₃}
right :
  Membership.mem (γ := Submodule ℝ V) (direction (P := P) (affineSpan ℝ {t₁.orthocenter, t₁.points i₃}))ᗮ
    (t₁.points i₁ -ᵥ t₁.points i₂)
⊢ Membership.mem (γ := Submodule ℝ V) (direction (affineSpan ℝ (t₂.points '' {j₂}ᶜ)))ᗮ (t₁.points i₁ -ᵥ t₁.points i₂)

Tactic:
rw [hu, Set.image_insert_eq, Set.image_singleton, h₁, h₃]

Premises used: Set.image_singleton, Set.image_insert_eq
-- 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₁ 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₃}
⊢ (altitude t₁ i₃).directionᗮ ≤ (direction (P := P) (affineSpan ℝ {t₁.orthocenter, t₁.points i₃}))ᗮ

Tactic:
have hle : (t₁.altitude i₃).directionᗮ ≤ line[ℝ, t₁.orthocenter, t₁.points i₃].directionᗮ :=
    Submodule.orthogonal_le (direction_le (affineSpan_orthocenter_point_le_altitude _ _))
-- 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₁ 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₃}
hle : (altitude t₁ i₃).directionᗮ ≤ (direction (P := P) (affineSpan ℝ {t₁.orthocenter, t₁.points i₃}))ᗮ
⊢ Membership.mem (γ := Submodule ℝ V) (direction (P := P) (affineSpan ℝ {t₁.orthocenter, t₁.points i₃}))ᗮ
    (t₁.points i₁ -ᵥ t₁.points i₂)

Tactic:
hle ((t₁.vectorSpan_isOrtho_altitude_direction i₃) ?_)

Premises used: Affine.Simplex.vectorSpan_isOrtho_altitude_direction
-- 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₁ 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₃}
hle : (altitude t₁ i₃).directionᗮ ≤ (direction (P := P) (affineSpan ℝ {t₁.orthocenter, t₁.points i₃}))ᗮ
right : Membership.mem (γ := Submodule ℝ V) (vectorSpan ℝ (t₁.points '' {i₃}ᶜ)) (t₁.points i₁ -ᵥ t₁.points i₂)
⊢ Membership.mem (γ := Submodule ℝ V) (direction (P := P) (affineSpan ℝ {t₁.orthocenter, t₁.points i₃}))ᗮ
    (t₁.points i₁ -ᵥ t₁.points i₂)

Tactic:
refine hle ((t₁.vectorSpan_isOrtho_altitude_direction i₃) ?_)

Premises used: Affine.Simplex.vectorSpan_isOrtho_altitude_direction
-- 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₁ 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₃}
hle : (altitude t₁ i₃).directionᗮ ≤ (direction (P := P) (affineSpan ℝ {t₁.orthocenter, t₁.points i₃}))ᗮ
⊢ Eq (α := Set (Fin 3)) {i₃}ᶜ {i₁, i₂}

Tactic:
grind
-- 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₁ 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₃}
hle : (altitude t₁ i₃).directionᗮ ≤ (direction (P := P) (affineSpan ℝ {t₁.orthocenter, t₁.points i₃}))ᗮ
⊢ Eq (α := Set (Fin 3)) {i₃}ᶜ {i₁, i₂}

Tactic:
have hui : ({i₃}ᶜ : Set _) = {i₁, i₂} := by grind
-- 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₁ 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₃}
hle : (altitude t₁ i₃).directionᗮ ≤ (direction (P := P) (affineSpan ℝ {t₁.orthocenter, t₁.points i₃}))ᗮ
hui : Eq (α := Set (Fin 3)) {i₃}ᶜ {i₁, i₂}
right :
  Membership.mem (γ := Submodule ℝ V) (vectorSpan ℝ (P := P) {t₁.points i₁, t₁.points i₂})
    (t₁.points i₁ -ᵥ t₁.points i₂)
⊢ Membership.mem (γ := Submodule ℝ V) (vectorSpan ℝ (t₁.points '' {i₃}ᶜ)) (t₁.points i₁ -ᵥ t₁.points i₂)

Tactic:
rw [hui, Set.image_insert_eq, Set.image_singleton]

Premises used: Set.image_singleton, Set.image_insert_eq
-- 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₁ 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₃}
hle : (altitude t₁ i₃).directionᗮ ≤ (direction (P := P) (affineSpan ℝ {t₁.orthocenter, t₁.points i₃}))ᗮ
hui : Eq (α := Set (Fin 3)) {i₃}ᶜ {i₁, i₂}
⊢ Membership.mem (γ := Submodule ℝ V) (vectorSpan ℝ (P := P) {t₁.points i₁, t₁.points i₂})
    (t₁.points i₁ -ᵥ t₁.points i₂)

Tactic:
vsub_mem_vectorSpan ℝ (Set.mem_insert _ _) (Set.mem_insert_of_mem _ (Set.mem_singleton _))

Premises used: Set.mem_singleton, vsub_mem_vectorSpan, Real, Set.Mem, Set.mem_insert_of_mem, Set.mem_insert