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₁ 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 (P := P) (affineSpan ℝ {t₁.orthocenter, t₁.points i₃}))ᗮ
    (t₁.points i₁ -ᵥ t₁.points i₂)
have hle : (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 _ _))
-- 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₃}
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₂)
have right : Membership.mem (γ := Submodule ℝ V) (vectorSpan ℝ (t₁.points '' {i₃}ᶜ)) (t₁.points i₁ -ᵥ t₁.points i₂)
Tactic: refine hle ((t₁.vectorSpan_isOrtho_altitude_direction i₃) ?_)
-- 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))
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) (vectorSpan ℝ (t₁.points '' {i₃}ᶜ)) (t₁.points i₁ -ᵥ t₁.points i₂)
have hui : Eq (α := Set (Fin 3)) {i₃}ᶜ {i₁, i₂}
Tactic: have hui : ({i₃}ᶜ : Set _) = {i₁, i₂} := 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₃}
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 ℝ (t₁.points '' {i₃}ᶜ)) (t₁.points i₁ -ᵥ t₁.points i₂)
have right : Membership.mem (γ := Submodule ℝ V) (vectorSpan ℝ (P := P) {t₁.points i₁, t₁.points i₂}) (t₁.points i₁ -ᵥ t₁.points i₂)
Tactic: rw [hui, Set.image_insert_eq, Set.image_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₁ 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₂.orthocenter = t₁.points i₁
have refine_1 : t₁.points i₁ ∈ altitude t₂ j₂
Tactic: refine (Triangle.eq_orthocenter_of_forall_mem_altitude hj₂₃ ?_ ?_).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₃
refine_1 : t₁.points i₁ ∈ altitude t₂ j₂
⊢ t₂.orthocenter = t₁.points i₁
have refine_2 : t₁.points i₁ ∈ altitude t₂ j₃
Tactic: refine (Triangle.eq_orthocenter_of_forall_mem_altitude hj₂₃ ?_ ?_).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₃
⊢ t₁.points i₁ ∈ altitude t₂ j₂
have refine_1 : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {t₁.points i₁, t₁.points i₂}) (t₁.points i₁)
Tactic: rw [altitude_replace_orthocenter_eq_affineSpan hi₁₂ hi₁₃ hi₂₃ hj₁₂ hj₁₃ hj₂₃ h₁ h₂ 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₁ ∈ altitude t₂ j₃
have refine_2 : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {t₁.points i₁, t₁.points i₃}) (t₁.points i₁)
Tactic: rw [altitude_replace_orthocenter_eq_affineSpan hi₁₃ hi₁₂ hi₂₃.symm hj₁₃ hj₁₂ hj₂₃.symm h₁ h₃ 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
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
⊢ (∃ (i₁ : Fin 3) (i₂ : Fin 3) (i₃ : Fin 3) (j₂ : Fin 3) (j₃ : Fin 3),
      i₁ ≠ i₂ ∧
        i₁ ≠ i₃ ∧
          i₂ ≠ i₃ ∧
            (∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃) ∧
              p i₁ = t.orthocenter ∧ j₂ ≠ j₃ ∧ t.points j₂ = p i₂ ∧ t.points j₃ = p i₃) ∨
    Set.range p = Set.range t.points
have pos : ∀ (h : t.orthocenter ∈ Set.range p),
  (∃ (i₁ : Fin 3) (i₂ : Fin 3) (i₃ : Fin 3) (j₂ : Fin 3) (j₃ : Fin 3),
      i₁ ≠ i₂ ∧
        i₁ ≠ i₃ ∧
          i₂ ≠ i₃ ∧
            (∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃) ∧
              p i₁ = t.orthocenter ∧ j₂ ≠ j₃ ∧ t.points j₂ = p i₂ ∧ t.points j₃ = p i₃) ∨
    Set.range p = Set.range t.points
Tactic: by_cases h : t.orthocenter ∈ Set.range p
-- 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
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
pos :
  ∀ (h : t.orthocenter ∈ Set.range p),
    (∃ (i₁ : Fin 3) (i₂ : Fin 3) (i₃ : Fin 3) (j₂ : Fin 3) (j₃ : Fin 3),
        i₁ ≠ i₂ ∧
          i₁ ≠ i₃ ∧
            i₂ ≠ i₃ ∧
              (∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃) ∧
                p i₁ = t.orthocenter ∧ j₂ ≠ j₃ ∧ t.points j₂ = p i₂ ∧ t.points j₃ = p i₃) ∨
      Set.range p = Set.range t.points
⊢ (∃ (i₁ : Fin 3) (i₂ : Fin 3) (i₃ : Fin 3) (j₂ : Fin 3) (j₃ : Fin 3),
      i₁ ≠ i₂ ∧
        i₁ ≠ i₃ ∧
          i₂ ≠ i₃ ∧
            (∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃) ∧
              p i₁ = t.orthocenter ∧ j₂ ≠ j₃ ∧ t.points j₂ = p i₂ ∧ t.points j₃ = p i₃) ∨
    Set.range p = Set.range t.points
have neg : ∀ (h : t.orthocenter ∉ Set.range p),
  (∃ (i₁ : Fin 3) (i₂ : Fin 3) (i₃ : Fin 3) (j₂ : Fin 3) (j₃ : Fin 3),
      i₁ ≠ i₂ ∧
        i₁ ≠ i₃ ∧
          i₂ ≠ i₃ ∧
            (∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃) ∧
              p i₁ = t.orthocenter ∧ j₂ ≠ j₃ ∧ t.points j₂ = p i₂ ∧ t.points j₃ = p i₃) ∨
    Set.range p = Set.range t.points
Tactic: by_cases h : t.orthocenter ∈ Set.range p
-- 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
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
h : t.orthocenter ∈ Set.range p
⊢ (∃ (i₁ : Fin 3) (i₂ : Fin 3) (i₃ : Fin 3) (j₂ : Fin 3) (j₃ : Fin 3),
      i₁ ≠ i₂ ∧
        i₁ ≠ i₃ ∧
          i₂ ≠ i₃ ∧
            (∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃) ∧
              p i₁ = t.orthocenter ∧ j₂ ≠ j₃ ∧ t.points j₂ = p i₂ ∧ t.points j₃ = p i₃) ∨
    Set.range p = Set.range t.points
have pos : ∃ (i₁ : Fin 3) (i₂ : Fin 3) (i₃ : Fin 3) (j₂ : Fin 3) (j₃ : Fin 3),
  i₁ ≠ i₂ ∧
    i₁ ≠ i₃ ∧
      i₂ ≠ i₃ ∧
        (∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃) ∧
          p i₁ = t.orthocenter ∧ j₂ ≠ j₃ ∧ t.points j₂ = p i₂ ∧ t.points j₃ = p i₃
Tactic: left
-- 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
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
h : t.orthocenter ∈ Set.range p
⊢ ∃ (i₁ : Fin 3) (i₂ : Fin 3) (i₃ : Fin 3) (j₂ : Fin 3) (j₃ : Fin 3),
    i₁ ≠ i₂ ∧
      i₁ ≠ i₃ ∧
        i₂ ≠ i₃ ∧
          (∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃) ∧
            p i₁ = t.orthocenter ∧ j₂ ≠ j₃ ∧ t.points j₂ = p i₂ ∧ t.points j₃ = p i₃
have pos : ∀ (i₁ : Fin 3) (h₁ : p i₁ = t.orthocenter),
  ∃ (i₁ : Fin 3) (i₂ : Fin 3) (i₃ : Fin 3) (j₂ : Fin 3) (j₃ : Fin 3),
    i₁ ≠ i₂ ∧
      i₁ ≠ i₃ ∧
        i₂ ≠ i₃ ∧
          (∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃) ∧
            p i₁ = t.orthocenter ∧ j₂ ≠ j₃ ∧ t.points j₂ = p i₂ ∧ t.points j₃ = p i₃
Tactic: rcases h with ⟨i₁, 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
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
i₁ : Fin 3
h₁ : p i₁ = t.orthocenter
⊢ ∃ (i₁ : Fin 3) (i₂ : Fin 3) (i₃ : Fin 3) (j₂ : Fin 3) (j₃ : Fin 3),
    i₁ ≠ i₂ ∧
      i₁ ≠ i₃ ∧
        i₂ ≠ i₃ ∧
          (∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃) ∧
            p i₁ = t.orthocenter ∧ j₂ ≠ j₃ ∧ t.points j₂ = p i₂ ∧ t.points j₃ = p i₃
have pos : ∀ (i₂ i₃ : Fin 3) (h₁₂ : i₁ ≠ i₂) (h₁₃ : i₁ ≠ i₃) (h₂₃ : i₂ ≠ i₃) (h₁₂₃ : ∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃),
  ∃ (i₁ : Fin 3) (i₂ : Fin 3) (i₃ : Fin 3) (j₂ : Fin 3) (j₃ : Fin 3),
    i₁ ≠ i₂ ∧
      i₁ ≠ i₃ ∧
        i₂ ≠ i₃ ∧
          (∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃) ∧
            p i₁ = t.orthocenter ∧ j₂ ≠ j₃ ∧ t.points j₂ = p i₂ ∧ t.points j₃ = p i₃
Tactic: obtain ⟨i₂, i₃, h₁₂, h₁₃, h₂₃, h₁₂₃⟩ :
        ∃ i₂ i₃ : Fin 3, i₁ ≠ i₂ ∧ i₁ ≠ i₃ ∧ i₂ ≠ i₃ ∧ ∀ i : Fin 3, i = i₁ ∨ i = i₂ ∨ i = i₃ := by
      clear h₁
      decide +revert
-- 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
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
i₁ : Fin 3
h₁ : p i₁ = t.orthocenter
i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
h₁₂₃ : ∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃
i : Fin 3
hi : i₁ ≠ i
⊢ ∃ (j : Fin 3), t.points j = p i
have hps₁ : p i ∈ Set.range t.points
Tactic: replace hps := Set.mem_of_mem_insert_of_ne
        (Set.mem_of_mem_of_subset (Set.mem_range_self i) hps) (h₁ ▸ hpi.ne hi.symm)
Cleared hypotheses: hps
-- 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
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
i₁ : Fin 3
h₁ : p i₁ = t.orthocenter
i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
h₁₂₃ : ∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃
⊢ ∃ (i₁ : Fin 3) (i₂ : Fin 3) (i₃ : Fin 3) (j₂ : Fin 3) (j₃ : Fin 3),
    i₁ ≠ i₂ ∧
      i₁ ≠ i₃ ∧
        i₂ ≠ i₃ ∧
          (∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃) ∧
            p i₁ = t.orthocenter ∧ j₂ ≠ j₃ ∧ t.points j₂ = p i₂ ∧ t.points j₃ = p i₃
have h : ∀ (i : Fin 3), i₁ ≠ i → ∃ (j : Fin 3), t.points j = p i
Tactic: have h : ∀ i, i₁ ≠ i → ∃ j : Fin 3, t.points j = p i := by
      intro i hi
      replace hps := Set.mem_of_mem_insert_of_ne
        (Set.mem_of_mem_of_subset (Set.mem_range_self i) hps) (h₁ ▸ hpi.ne hi.symm)
      exact hps
-- 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
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
i₁ : Fin 3
h₁ : p i₁ = t.orthocenter
i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
h₁₂₃ : ∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃
h : ∀ (i : Fin 3), i₁ ≠ i → ∃ (j : Fin 3), t.points j = p i
⊢ ∃ (i₁ : Fin 3) (i₂ : Fin 3) (i₃ : Fin 3) (j₂ : Fin 3) (j₃ : Fin 3),
    i₁ ≠ i₂ ∧
      i₁ ≠ i₃ ∧
        i₂ ≠ i₃ ∧
          (∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃) ∧
            p i₁ = t.orthocenter ∧ j₂ ≠ j₃ ∧ t.points j₂ = p i₂ ∧ t.points j₃ = p i₃
have pos : ∀ (j₂ : Fin 3) (h₂ : t.points j₂ = p i₂),
  ∃ (i₁ : Fin 3) (i₂ : Fin 3) (i₃ : Fin 3) (j₂ : Fin 3) (j₃ : Fin 3),
    i₁ ≠ i₂ ∧
      i₁ ≠ i₃ ∧
        i₂ ≠ i₃ ∧
          (∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃) ∧
            p i₁ = t.orthocenter ∧ j₂ ≠ j₃ ∧ t.points j₂ = p i₂ ∧ t.points j₃ = p i₃
Tactic: rcases h i₂ h₁₂ with ⟨j₂, 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
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
i₁ : Fin 3
h₁ : p i₁ = t.orthocenter
i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
h₁₂₃ : ∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃
h : ∀ (i : Fin 3), i₁ ≠ i → ∃ (j : Fin 3), t.points j = p i
j₂ : Fin 3
h₂ : t.points j₂ = p i₂
⊢ ∃ (i₁ : Fin 3) (i₂ : Fin 3) (i₃ : Fin 3) (j₂ : Fin 3) (j₃ : Fin 3),
    i₁ ≠ i₂ ∧
      i₁ ≠ i₃ ∧
        i₂ ≠ i₃ ∧
          (∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃) ∧
            p i₁ = t.orthocenter ∧ j₂ ≠ j₃ ∧ t.points j₂ = p i₂ ∧ t.points j₃ = p i₃
have pos : ∀ (j₃ : Fin 3) (h₃ : t.points j₃ = p i₃),
  ∃ (i₁ : Fin 3) (i₂ : Fin 3) (i₃ : Fin 3) (j₂ : Fin 3) (j₃ : Fin 3),
    i₁ ≠ i₂ ∧
      i₁ ≠ i₃ ∧
        i₂ ≠ i₃ ∧
          (∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃) ∧
            p i₁ = t.orthocenter ∧ j₂ ≠ j₃ ∧ t.points j₂ = p i₂ ∧ t.points j₃ = p i₃
Tactic: rcases h i₃ h₁₃ with ⟨j₃, 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
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
i₁ : Fin 3
h₁ : p i₁ = t.orthocenter
i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
h₁₂₃ : ∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃
h : ∀ (i : Fin 3), i₁ ≠ i → ∃ (j : Fin 3), t.points j = p i
j₂ : Fin 3
h₂ : t.points j₂ = p i₂
j₃ : Fin 3
h₃ : t.points j₃ = p i₃
he : j₂ = j₃
⊢ False
have h₄ : p i₃ = p i₂
Tactic: rw [he, h₃] at h₂
Cleared hypotheses: h₂, h₃, he
-- 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
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
i₁ : Fin 3
h₁ : p i₁ = t.orthocenter
i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
h₁₂₃ : ∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃
h : ∀ (i : Fin 3), i₁ ≠ i → ∃ (j : Fin 3), t.points j = p i
j₂ : Fin 3
h₂ : t.points j₂ = p i₂
j₃ : Fin 3
h₃ : t.points j₃ = p i₃
⊢ ∃ (i₁ : Fin 3) (i₂ : Fin 3) (i₃ : Fin 3) (j₂ : Fin 3) (j₃ : Fin 3),
    i₁ ≠ i₂ ∧
      i₁ ≠ i₃ ∧
        i₂ ≠ i₃ ∧
          (∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃) ∧
            p i₁ = t.orthocenter ∧ j₂ ≠ j₃ ∧ t.points j₂ = p i₂ ∧ t.points j₃ = p i₃
have hj₂₃ : j₂ ≠ j₃
Tactic: have hj₂₃ : j₂ ≠ j₃ := by
      intro he
      rw [he, h₃] at h₂
      exact h₂₃.symm (hpi 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
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
h : t.orthocenter ∉ Set.range p
⊢ (∃ (i₁ : Fin 3) (i₂ : Fin 3) (i₃ : Fin 3) (j₂ : Fin 3) (j₃ : Fin 3),
      i₁ ≠ i₂ ∧
        i₁ ≠ i₃ ∧
          i₂ ≠ i₃ ∧
            (∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃) ∧
              p i₁ = t.orthocenter ∧ j₂ ≠ j₃ ∧ t.points j₂ = p i₂ ∧ t.points j₃ = p i₃) ∨
    Set.range p = Set.range t.points
have neg : Set.range p = Set.range t.points
Tactic: right
-- 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
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
h : t.orthocenter ∉ Set.range p
⊢ Set.range p = Set.range t.points
have hs : Set.range p ⊆ insert t.orthocenter (Set.range t.points) \ {t.orthocenter}
Tactic: have hs := Set.subset_diff_singleton hps 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
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
h : t.orthocenter ∉ Set.range p
hs : Set.range p ⊆ insert t.orthocenter (Set.range t.points) \ {t.orthocenter}
⊢ Set.range p = Set.range t.points
have hs₁ : Set.range p ⊆ Set.range t.points
Tactic: rw [Set.insert_diff_self_of_notMem ho] at hs
Cleared hypotheses: 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
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
h : t.orthocenter ∉ Set.range p
hs : Set.range p ⊆ Set.range t.points
⊢ Set.range p = Set.range t.points
have neg : Fintype.card.{u_2} (↑(Set.range t.points) : Type u_2) ≤ Fintype.card.{u_2} (↑(Set.range p) : Type u_2)
Tactic: refine Set.eq_of_subset_of_card_le 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
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
h : t.orthocenter ∉ Set.range p
hs : Set.range p ⊆ Set.range t.points
⊢ Fintype.card.{u_2} (↑(Set.range t.points) : Type u_2) ≤ Fintype.card.{u_2} (↑(Set.range p) : Type u_2)
have neg : Fintype.card.{u_2} (↑(Set.range t.points) : Type u_2) ≤ Fintype.card (Fin 3)
Tactic: rw [Set.card_range_of_injective hpi, Set.card_range_of_injective t.independent.injective]
-- 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
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
h : t.orthocenter ∉ Set.range p
hs : Set.range p ⊆ Set.range t.points
neg : Fintype.card.{u_2} (↑(Set.range t.points) : Type u_2) ≤ Fintype.card (Fin 3)
⊢ Fintype.card.{u_2} (↑(Set.range t.points) : Type u_2) ≤ Fintype.card.{u_2} (↑(Set.range p) : Type u_2)
have neg₁ : Fintype.card (Fin (HAdd.hAdd (α := ℕ) 2 1)) ≤ Fintype.card (Fin (HAdd.hAdd (α := ℕ) 2 1))
Tactic: rw [Set.card_range_of_injective hpi, Set.card_range_of_injective t.independent.injective]
-- 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
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
h : t.orthocenter ∉ Set.range p
hs : Set.range p ⊆ Set.range t.points
⊢ Set.range p = Set.range t.points
have neg : Fintype.card.{u_2} (↑(Set.range t.points) : Type u_2) ≤ Fintype.card.{u_2} (↑(Set.range p) : Type u_2)
Tactic: classical
    refine Set.eq_of_subset_of_card_le hs ?_
    rw [Set.card_range_of_injective hpi, Set.card_range_of_injective t.independent.injective]