awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.Simplex (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_3
inst : Ring R
inst_1 : SeminormedAddCommGroup V
inst_2 : PseudoMetricSpace P
inst_3 : Module R V
inst_4 : NormedAddTorsor V P
t : Triangle R P
h :
  dist (t.points 0) (t.points 1) ≠ dist (t.points 0) (t.points 2) ∧
    dist (t.points 0) (t.points 1) ≠ dist (t.points 1) (t.points 2) ∧
      dist (t.points 0) (t.points 2) ≠ dist (t.points 1) (t.points 2)
h₁ : dist (t.points 0) (t.points 1) ≠ dist (t.points 0) (t.points 2)
h₂ : dist (t.points 0) (t.points 1) ≠ dist (t.points 1) (t.points 2)
h₃ : dist (t.points 0) (t.points 2) ≠ dist (t.points 1) (t.points 2)
x₂ y₁ y₂ : Fin (HAdd.hAdd (α := ℕ) 2 1)
hy : y₁ < y₂
hx : (fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨1, ⋯⟩ < x₂
hxy :
  dist (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))) (t.points x₂) =
    dist (t.points y₁) (t.points y₂)
⊢ (fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨1, ⋯⟩ = y₁ ∧ x₂ = y₂
have 1 : ∀
  (hx :
    LT.lt (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨1, sorry⟩)
      ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨0, sorry⟩))
  (hxy :
    dist (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨1, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))))
        (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨0, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))) =
      dist (t.points y₁) (t.points y₂)),
  (fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨1, sorry⟩ = y₁ ∧ (fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨0, sorry⟩ = y₂
Tactic: fin_cases x₂
Cleared hypotheses: x₂, hx, hxy
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.Simplex (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_3
inst : Ring R
inst_1 : SeminormedAddCommGroup V
inst_2 : PseudoMetricSpace P
inst_3 : Module R V
inst_4 : NormedAddTorsor V P
t : Triangle R P
h :
  dist (t.points 0) (t.points 1) ≠ dist (t.points 0) (t.points 2) ∧
    dist (t.points 0) (t.points 1) ≠ dist (t.points 1) (t.points 2) ∧
      dist (t.points 0) (t.points 2) ≠ dist (t.points 1) (t.points 2)
h₁ : dist (t.points 0) (t.points 1) ≠ dist (t.points 0) (t.points 2)
h₂ : dist (t.points 0) (t.points 1) ≠ dist (t.points 1) (t.points 2)
h₃ : dist (t.points 0) (t.points 2) ≠ dist (t.points 1) (t.points 2)
x₂ y₁ y₂ : Fin (HAdd.hAdd (α := ℕ) 2 1)
hy : y₁ < y₂
hx : (fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨1, ⋯⟩ < x₂
hxy :
  dist (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))) (t.points x₂) =
    dist (t.points y₁) (t.points y₂)
1 :
  ∀
    (hx :
      LT.lt (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨1, ⋯⟩)
        ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨0, ⋯⟩))
    (hxy :
      dist (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))))
          (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))) =
        dist (t.points y₁) (t.points y₂)),
    (fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨1, ⋯⟩ = y₁ ∧ (fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨0, ⋯⟩ = y₂
⊢ (fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨1, ⋯⟩ = y₁ ∧ x₂ = y₂
have 1₁ : ∀
  (hx :
    LT.lt (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨1, sorry⟩)
      ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨1, sorry⟩))
  (hxy :
    dist (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨1, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))))
        (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨1, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))) =
      dist (t.points y₁) (t.points y₂)),
  (fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨1, sorry⟩ = y₁ ∧ (fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨1, sorry⟩ = y₂
Tactic: fin_cases x₂
Cleared hypotheses: x₂, hx, hxy
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.Simplex (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_3
inst : Ring R
inst_1 : SeminormedAddCommGroup V
inst_2 : PseudoMetricSpace P
inst_3 : Module R V
inst_4 : NormedAddTorsor V P
t : Triangle R P
h :
  dist (t.points 0) (t.points 1) ≠ dist (t.points 0) (t.points 2) ∧
    dist (t.points 0) (t.points 1) ≠ dist (t.points 1) (t.points 2) ∧
      dist (t.points 0) (t.points 2) ≠ dist (t.points 1) (t.points 2)
h₁ : dist (t.points 0) (t.points 1) ≠ dist (t.points 0) (t.points 2)
h₂ : dist (t.points 0) (t.points 1) ≠ dist (t.points 1) (t.points 2)
h₃ : dist (t.points 0) (t.points 2) ≠ dist (t.points 1) (t.points 2)
x₂ y₁ y₂ : Fin (HAdd.hAdd (α := ℕ) 2 1)
hy : y₁ < y₂
hx : (fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨1, ⋯⟩ < x₂
hxy :
  dist (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))) (t.points x₂) =
    dist (t.points y₁) (t.points y₂)
1 :
  ∀
    (hx :
      LT.lt (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨1, ⋯⟩)
        ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨0, ⋯⟩))
    (hxy :
      dist (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))))
          (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))) =
        dist (t.points y₁) (t.points y₂)),
    (fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨1, ⋯⟩ = y₁ ∧ (fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨0, ⋯⟩ = y₂
h_1 :
  ∀
    (hx :
      LT.lt (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨1, ⋯⟩)
        ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨1, ⋯⟩))
    (hxy :
      dist (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))))
          (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))) =
        dist (t.points y₁) (t.points y₂)),
    (fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨1, ⋯⟩ = y₁ ∧ (fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨1, ⋯⟩ = y₂
⊢ (fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨1, ⋯⟩ = y₁ ∧ x₂ = y₂
have 1₁ : ∀
  (hx :
    LT.lt (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨1, sorry⟩)
      ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨2, sorry⟩))
  (hxy :
    dist (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨1, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))))
        (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨2, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))) =
      dist (t.points y₁) (t.points y₂)),
  (fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨1, sorry⟩ = y₁ ∧ (fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨2, sorry⟩ = y₂
Tactic: fin_cases x₂
Cleared hypotheses: x₂, hx, hxy
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.Simplex (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_3
inst : Ring R
inst_1 : SeminormedAddCommGroup V
inst_2 : PseudoMetricSpace P
inst_3 : Module R V
inst_4 : NormedAddTorsor V P
t : Triangle R P
h :
  dist (t.points 0) (t.points 1) ≠ dist (t.points 0) (t.points 2) ∧
    dist (t.points 0) (t.points 1) ≠ dist (t.points 1) (t.points 2) ∧
      dist (t.points 0) (t.points 2) ≠ dist (t.points 1) (t.points 2)
h₁ : dist (t.points 0) (t.points 1) ≠ dist (t.points 0) (t.points 2)
h₂ : dist (t.points 0) (t.points 1) ≠ dist (t.points 1) (t.points 2)
h₃ : dist (t.points 0) (t.points 2) ≠ dist (t.points 1) (t.points 2)
x₂ y₁ y₂ : Fin (HAdd.hAdd (α := ℕ) 2 1)
hy : y₁ < y₂
hx : (fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨2, ⋯⟩ < x₂
hxy :
  dist (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))) (t.points x₂) =
    dist (t.points y₁) (t.points y₂)
⊢ (fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨2, ⋯⟩ = y₁ ∧ x₂ = y₂
have 2 : ∀
  (hx :
    LT.lt (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨2, sorry⟩)
      ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨0, sorry⟩))
  (hxy :
    dist (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨2, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))))
        (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨0, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))) =
      dist (t.points y₁) (t.points y₂)),
  (fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨2, sorry⟩ = y₁ ∧ (fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨0, sorry⟩ = y₂
Tactic: fin_cases x₂
Cleared hypotheses: x₂, hx, hxy
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.Simplex (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_3
inst : Ring R
inst_1 : SeminormedAddCommGroup V
inst_2 : PseudoMetricSpace P
inst_3 : Module R V
inst_4 : NormedAddTorsor V P
t : Triangle R P
h :
  dist (t.points 0) (t.points 1) ≠ dist (t.points 0) (t.points 2) ∧
    dist (t.points 0) (t.points 1) ≠ dist (t.points 1) (t.points 2) ∧
      dist (t.points 0) (t.points 2) ≠ dist (t.points 1) (t.points 2)
h₁ : dist (t.points 0) (t.points 1) ≠ dist (t.points 0) (t.points 2)
h₂ : dist (t.points 0) (t.points 1) ≠ dist (t.points 1) (t.points 2)
h₃ : dist (t.points 0) (t.points 2) ≠ dist (t.points 1) (t.points 2)
x₂ y₁ y₂ : Fin (HAdd.hAdd (α := ℕ) 2 1)
hy : y₁ < y₂
hx : (fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨2, ⋯⟩ < x₂
hxy :
  dist (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))) (t.points x₂) =
    dist (t.points y₁) (t.points y₂)
2 :
  ∀
    (hx :
      LT.lt (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨2, ⋯⟩)
        ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨0, ⋯⟩))
    (hxy :
      dist (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))))
          (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))) =
        dist (t.points y₁) (t.points y₂)),
    (fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨2, ⋯⟩ = y₁ ∧ (fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨0, ⋯⟩ = y₂
⊢ (fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨2, ⋯⟩ = y₁ ∧ x₂ = y₂
have 2₁ : ∀
  (hx :
    LT.lt (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨2, sorry⟩)
      ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨1, sorry⟩))
  (hxy :
    dist (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨2, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))))
        (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨1, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))) =
      dist (t.points y₁) (t.points y₂)),
  (fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨2, sorry⟩ = y₁ ∧ (fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨1, sorry⟩ = y₂
Tactic: fin_cases x₂
Cleared hypotheses: x₂, hx, hxy
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.Simplex (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_3
inst : Ring R
inst_1 : SeminormedAddCommGroup V
inst_2 : PseudoMetricSpace P
inst_3 : Module R V
inst_4 : NormedAddTorsor V P
t : Triangle R P
h :
  dist (t.points 0) (t.points 1) ≠ dist (t.points 0) (t.points 2) ∧
    dist (t.points 0) (t.points 1) ≠ dist (t.points 1) (t.points 2) ∧
      dist (t.points 0) (t.points 2) ≠ dist (t.points 1) (t.points 2)
h₁ : dist (t.points 0) (t.points 1) ≠ dist (t.points 0) (t.points 2)
h₂ : dist (t.points 0) (t.points 1) ≠ dist (t.points 1) (t.points 2)
h₃ : dist (t.points 0) (t.points 2) ≠ dist (t.points 1) (t.points 2)
x₂ y₁ y₂ : Fin (HAdd.hAdd (α := ℕ) 2 1)
hy : y₁ < y₂
hx : (fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨2, ⋯⟩ < x₂
hxy :
  dist (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))) (t.points x₂) =
    dist (t.points y₁) (t.points y₂)
2 :
  ∀
    (hx :
      LT.lt (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨2, ⋯⟩)
        ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨0, ⋯⟩))
    (hxy :
      dist (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))))
          (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))) =
        dist (t.points y₁) (t.points y₂)),
    (fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨2, ⋯⟩ = y₁ ∧ (fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨0, ⋯⟩ = y₂
h_1 :
  ∀
    (hx :
      LT.lt (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨2, ⋯⟩)
        ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨1, ⋯⟩))
    (hxy :
      dist (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))))
          (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))) =
        dist (t.points y₁) (t.points y₂)),
    (fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨2, ⋯⟩ = y₁ ∧ (fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨1, ⋯⟩ = y₂
⊢ (fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨2, ⋯⟩ = y₁ ∧ x₂ = y₂
have 2₁ : ∀
  (hx :
    LT.lt (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨2, sorry⟩)
      ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨2, sorry⟩))
  (hxy :
    dist (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨2, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))))
        (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨2, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))) =
      dist (t.points y₁) (t.points y₂)),
  (fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨2, sorry⟩ = y₁ ∧ (fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨2, sorry⟩ = y₂
Tactic: fin_cases x₂
Cleared hypotheses: x₂, hx, hxy
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.Simplex (hypothesis)
Goal:
R : Type u_1
V : Type u_2
P : Type u_3
inst : Ring R
inst_1 : SeminormedAddCommGroup V
inst_2 : PseudoMetricSpace P
inst_3 : Module R V
inst_4 : NormedAddTorsor V P
t : Triangle R P
h :
  dist (t.points 0) (t.points 1) ≠ dist (t.points 0) (t.points 2) ∧
    dist (t.points 0) (t.points 1) ≠ dist (t.points 1) (t.points 2) ∧
      dist (t.points 0) (t.points 2) ≠ dist (t.points 1) (t.points 2)
h₁ : dist (t.points 0) (t.points 1) ≠ dist (t.points 0) (t.points 2)
h₂ : dist (t.points 0) (t.points 1) ≠ dist (t.points 1) (t.points 2)
h₃ : dist (t.points 0) (t.points 2) ≠ dist (t.points 1) (t.points 2)
y₁ y₂ : Fin (HAdd.hAdd (α := ℕ) 2 1)
hy : y₁ < y₂
hx :
  LT.lt (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨0, ⋯⟩)
    ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨1, ⋯⟩)
hxy :
  dist (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))))
      (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))) =
    dist (t.points y₁) (t.points y₂)
⊢ (fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨0, ⋯⟩ = y₁ ∧ (fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨1, ⋯⟩ = y₂
have hx₁ : True
Tactic: simp +decide only at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.Simplex (hypothesis)
Goal:
R : Type u_1
V : Type u_2
P : Type u_3
inst : Ring R
inst_1 : SeminormedAddCommGroup V
inst_2 : PseudoMetricSpace P
inst_3 : Module R V
inst_4 : NormedAddTorsor V P
t : Triangle R P
h :
  dist (t.points 0) (t.points 1) ≠ dist (t.points 0) (t.points 2) ∧
    dist (t.points 0) (t.points 1) ≠ dist (t.points 1) (t.points 2) ∧
      dist (t.points 0) (t.points 2) ≠ dist (t.points 1) (t.points 2)
h₁ : dist (t.points 0) (t.points 1) ≠ dist (t.points 0) (t.points 2)
h₂ : dist (t.points 0) (t.points 1) ≠ dist (t.points 1) (t.points 2)
h₃ : dist (t.points 0) (t.points 2) ≠ dist (t.points 1) (t.points 2)
y₁ y₂ : Fin (HAdd.hAdd (α := ℕ) 2 1)
hy : y₁ < y₂
hx :
  LT.lt (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨0, ⋯⟩)
    ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨2, ⋯⟩)
hxy :
  dist (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))))
      (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))) =
    dist (t.points y₁) (t.points y₂)
⊢ (fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨0, ⋯⟩ = y₁ ∧ (fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨2, ⋯⟩ = y₂
have hx₁ : True
Tactic: simp +decide only at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.Simplex (hypothesis)
Goal:
R : Type u_1
V : Type u_2
P : Type u_3
inst : Ring R
inst_1 : SeminormedAddCommGroup V
inst_2 : PseudoMetricSpace P
inst_3 : Module R V
inst_4 : NormedAddTorsor V P
t : Triangle R P
h :
  dist (t.points 0) (t.points 1) ≠ dist (t.points 0) (t.points 2) ∧
    dist (t.points 0) (t.points 1) ≠ dist (t.points 1) (t.points 2) ∧
      dist (t.points 0) (t.points 2) ≠ dist (t.points 1) (t.points 2)
h₁ : dist (t.points 0) (t.points 1) ≠ dist (t.points 0) (t.points 2)
h₂ : dist (t.points 0) (t.points 1) ≠ dist (t.points 1) (t.points 2)
h₃ : dist (t.points 0) (t.points 2) ≠ dist (t.points 1) (t.points 2)
y₁ y₂ : Fin (HAdd.hAdd (α := ℕ) 2 1)
hy : y₁ < y₂
hx :
  LT.lt (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨1, ⋯⟩)
    ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨2, ⋯⟩)
hxy :
  dist (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))))
      (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))) =
    dist (t.points y₁) (t.points y₂)
⊢ (fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨1, ⋯⟩ = y₁ ∧ (fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨2, ⋯⟩ = y₂
have hx₁ : True
Tactic: simp +decide only at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.Simplex (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_3
inst : Ring R
inst_1 : SeminormedAddCommGroup V
inst_2 : PseudoMetricSpace P
inst_3 : Module R V
inst_4 : NormedAddTorsor V P
t : Triangle R P
h :
  dist (t.points 0) (t.points 1) ≠ dist (t.points 0) (t.points 2) ∧
    dist (t.points 0) (t.points 1) ≠ dist (t.points 1) (t.points 2) ∧
      dist (t.points 0) (t.points 2) ≠ dist (t.points 1) (t.points 2)
h₁ : dist (t.points 0) (t.points 1) ≠ dist (t.points 0) (t.points 2)
h₂ : dist (t.points 0) (t.points 1) ≠ dist (t.points 1) (t.points 2)
h₃ : dist (t.points 0) (t.points 2) ≠ dist (t.points 1) (t.points 2)
y₁ y₂ : Fin (HAdd.hAdd (α := ℕ) 2 1)
hy : y₁ < y₂
hxy :
  dist (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))))
      (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))) =
    dist (t.points y₁) (t.points y₂)
hx : True
⊢ (fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨0, ⋯⟩ = y₁ ∧ (fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨1, ⋯⟩ = y₂
have 0 : ∀ (hy : (fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨0, sorry⟩ < y₂)
  (hxy :
    dist (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨0, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))))
        (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨1, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))) =
      dist (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨0, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))))
        (t.points y₂)),
  Eq (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨0, sorry⟩)
      ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨0, sorry⟩) ∧
    (fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨1, sorry⟩ = y₂
Tactic: fin_cases y₁
Cleared hypotheses: y₁, hy, hxy
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.Simplex (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_3
inst : Ring R
inst_1 : SeminormedAddCommGroup V
inst_2 : PseudoMetricSpace P
inst_3 : Module R V
inst_4 : NormedAddTorsor V P
t : Triangle R P
h :
  dist (t.points 0) (t.points 1) ≠ dist (t.points 0) (t.points 2) ∧
    dist (t.points 0) (t.points 1) ≠ dist (t.points 1) (t.points 2) ∧
      dist (t.points 0) (t.points 2) ≠ dist (t.points 1) (t.points 2)
h₁ : dist (t.points 0) (t.points 1) ≠ dist (t.points 0) (t.points 2)
h₂ : dist (t.points 0) (t.points 1) ≠ dist (t.points 1) (t.points 2)
h₃ : dist (t.points 0) (t.points 2) ≠ dist (t.points 1) (t.points 2)
y₁ y₂ : Fin (HAdd.hAdd (α := ℕ) 2 1)
hy : y₁ < y₂
hxy :
  dist (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))))
      (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))) =
    dist (t.points y₁) (t.points y₂)
hx : True
0 :
  ∀ (hy : (fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨0, ⋯⟩ < y₂)
    (hxy :
      dist (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))))
          (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))) =
        dist (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))))
          (t.points y₂)),
    Eq (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨0, ⋯⟩)
        ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨0, ⋯⟩) ∧
      (fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨1, ⋯⟩ = y₂
⊢ (fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨0, ⋯⟩ = y₁ ∧ (fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨1, ⋯⟩ = y₂
have 0₁ : ∀ (hy : (fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨1, sorry⟩ < y₂)
  (hxy :
    dist (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨0, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))))
        (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨1, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))) =
      dist (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨1, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))))
        (t.points y₂)),
  Eq (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨0, sorry⟩)
      ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨1, sorry⟩) ∧
    (fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨1, sorry⟩ = y₂
Tactic: fin_cases y₁
Cleared hypotheses: y₁, hy, hxy