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)
y₂ : Fin (HAdd.hAdd (α := ℕ) 2 1)
hx : True
hy : (fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨2, ⋯⟩ < 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) (⟨2, ⋯⟩ : 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) ⟨2, ⋯⟩) ∧
    (fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨1, ⋯⟩ = y₂
have 0 : ∀
  (hy :
    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) (⟨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) (⟨2, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))))
        (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨0, sorry⟩))),
  Eq (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨0, sorry⟩)
      ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨2, sorry⟩) ∧
    Eq (α := 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⟩)
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₂ : Fin (HAdd.hAdd (α := ℕ) 2 1)
hx : True
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) (⟨2, ⋯⟩ : 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) ⟨2, ⋯⟩ = y₂
have 0 : ∀
  (hy :
    LT.lt (α := 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⟩))
  (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) (⟨2, 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 ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨0, sorry⟩))),
  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⟩) ∧
    Eq (α := 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⟩)
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₂ : Fin (HAdd.hAdd (α := ℕ) 2 1)
hx : True
hy : (fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨1, ⋯⟩ < 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) (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))) =
    dist (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨1, ⋯⟩ : 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) ⟨1, ⋯⟩) ∧
    (fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨2, ⋯⟩ = y₂
have 0 : ∀
  (hy :
    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) (⟨0, 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 ((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⟩))),
  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⟩) ∧
    Eq (α := 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⟩)
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₂ : Fin (HAdd.hAdd (α := ℕ) 2 1)
hx : True
hy : (fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨2, ⋯⟩ < 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) (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))) =
    dist (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨2, ⋯⟩ : 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) ⟨2, ⋯⟩) ∧
    (fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨2, ⋯⟩ = y₂
have 0 : ∀
  (hy :
    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) (⟨0, 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 ((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⟩))),
  Eq (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨0, sorry⟩)
      ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨2, sorry⟩) ∧
    Eq (α := 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⟩)
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₂ : Fin (HAdd.hAdd (α := ℕ) 2 1)
hx : True
hy : (fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨0, ⋯⟩ < y₂
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 ((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) ⟨1, ⋯⟩)
      ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨0, ⋯⟩) ∧
    (fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨2, ⋯⟩ = y₂
have 1 : ∀
  (hy :
    LT.lt (α := 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⟩))
  (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 ((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) ⟨0, sorry⟩))),
  Eq (α := 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⟩) ∧
    Eq (α := 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⟩)
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₂ : Fin (HAdd.hAdd (α := ℕ) 2 1)
hx : True
hy : (fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨1, ⋯⟩ < y₂
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 ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))) (t.points y₂)
⊢ Eq (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨1, ⋯⟩)
      ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨1, ⋯⟩) ∧
    (fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨2, ⋯⟩ = y₂
have 1 : ∀
  (hy :
    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) (⟨2, 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 ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨0, sorry⟩))),
  Eq (α := 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⟩) ∧
    Eq (α := 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⟩)
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₂ : Fin (HAdd.hAdd (α := ℕ) 2 1)
hx : True
hy : (fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨2, ⋯⟩ < y₂
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 ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))) (t.points y₂)
⊢ Eq (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨1, ⋯⟩)
      ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨2, ⋯⟩) ∧
    (fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨2, ⋯⟩ = y₂
have 1 : ∀
  (hy :
    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) (⟨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 ((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⟩))),
  Eq (α := 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⟩) ∧
    Eq (α := 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⟩)
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
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
⊢ Simplex.Equilateral t ↔
    dist (t.points i₁) (t.points i₂) = dist (t.points i₁) (t.points i₃) ∧
      dist (t.points i₁) (t.points i₂) = dist (t.points i₂) (t.points i₃)
have refine_1 : Simplex.Equilateral t →
  ∀ (r : ℝ) (hr : ∀ (i j : Fin (HAdd.hAdd (α := ℕ) 2 1)), i ≠ j → dist (t.points i) (t.points j) = r),
    dist (t.points i₁) (t.points i₂) = dist (t.points i₁) (t.points i₃) ∧
      dist (t.points i₁) (t.points i₂) = dist (t.points i₂) (t.points i₃)
Tactic: refine ⟨fun ⟨r, hr⟩ ↦ ?_, fun h ↦ ?_⟩
-- 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
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
refine_1 :
  Simplex.Equilateral t →
    ∀ (r : ℝ) (hr : ∀ (i j : Fin (HAdd.hAdd (α := ℕ) 2 1)), i ≠ j → dist (t.points i) (t.points j) = r),
      dist (t.points i₁) (t.points i₂) = dist (t.points i₁) (t.points i₃) ∧
        dist (t.points i₁) (t.points i₂) = dist (t.points i₂) (t.points i₃)
⊢ Simplex.Equilateral t ↔
    dist (t.points i₁) (t.points i₂) = dist (t.points i₁) (t.points i₃) ∧
      dist (t.points i₁) (t.points i₂) = dist (t.points i₂) (t.points i₃)
have refine_2 : ∀
  (h :
    dist (t.points i₁) (t.points i₂) = dist (t.points i₁) (t.points i₃) ∧
      dist (t.points i₁) (t.points i₂) = dist (t.points i₂) (t.points i₃)),
  Simplex.Equilateral t
Tactic: refine ⟨fun ⟨r, hr⟩ ↦ ?_, fun h ↦ ?_⟩
-- 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
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
h :
  dist (t.points i₁) (t.points i₂) = dist (t.points i₁) (t.points i₃) ∧
    dist (t.points i₁) (t.points i₂) = dist (t.points i₂) (t.points i₃)
⊢ Simplex.Equilateral t
have refine_2 : ∀ (i j : Fin (HAdd.hAdd (α := ℕ) 2 1)), i ≠ j → dist (t.points i) (t.points j) = dist (t.points i₁) (t.points i₂)
Tactic: refine ⟨dist (t.points i₁) (t.points i₂), ?_⟩
-- 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
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
h :
  dist (t.points i₁) (t.points i₂) = dist (t.points i₁) (t.points i₃) ∧
    dist (t.points i₁) (t.points i₂) = dist (t.points i₂) (t.points i₃)
i j : Fin (HAdd.hAdd (α := ℕ) 2 1)
hij : i ≠ j
⊢ dist (t.points i) (t.points j) = dist (t.points i₁) (t.points i₂)
have hi : i = i₁ ∧ j = i₂ ∨ i = i₂ ∧ j = i₁ ∨ i = i₁ ∧ j = i₃ ∨ i = i₃ ∧ j = i₁ ∨ i = i₂ ∧ j = i₃ ∨ i = i₃ ∧ j = i₂
Tactic: have hi : (i = i₁ ∧ j = i₂) ∨ (i = i₂ ∧ j = i₁) ∨ (i = i₁ ∧ j = i₃) ∨
      (i = i₃ ∧ j = i₁) ∨ (i = i₂ ∧ j = i₃) ∨ (i = i₃ ∧ j = i₂) := by
      clear h
      decide +revert
-- 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
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
h :
  dist (t.points i₁) (t.points i₂) = dist (t.points i₁) (t.points i₃) ∧
    dist (t.points i₁) (t.points i₂) = dist (t.points i₂) (t.points i₃)
i j : Fin (HAdd.hAdd (α := ℕ) 2 1)
hij : i ≠ j
hi : i = i₁ ∧ j = i₂ ∨ i = i₂ ∧ j = i₁ ∨ i = i₁ ∧ j = i₃ ∨ i = i₃ ∧ j = i₁ ∨ i = i₂ ∧ j = i₃ ∨ i = i₃ ∧ j = i₂
⊢ dist (t.points i) (t.points j) = dist (t.points i₁) (t.points i₂)
have h₁ : dist (t.points i₁) (t.points i₂) = dist (t.points i₁) (t.points i₃)
Tactic: rcases h with ⟨h₁, h₂⟩
Cleared hypotheses: h
-- 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
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
h :
  dist (t.points i₁) (t.points i₂) = dist (t.points i₁) (t.points i₃) ∧
    dist (t.points i₁) (t.points i₂) = dist (t.points i₂) (t.points i₃)
i j : Fin (HAdd.hAdd (α := ℕ) 2 1)
hij : i ≠ j
hi : i = i₁ ∧ j = i₂ ∨ i = i₂ ∧ j = i₁ ∨ i = i₁ ∧ j = i₃ ∨ i = i₃ ∧ j = i₁ ∨ i = i₂ ∧ j = i₃ ∨ i = i₃ ∧ j = i₂
h₁ : dist (t.points i₁) (t.points i₂) = dist (t.points i₁) (t.points i₃)
⊢ dist (t.points i) (t.points j) = dist (t.points i₁) (t.points i₂)
have h₂ : dist (t.points i₁) (t.points i₂) = dist (t.points i₂) (t.points i₃)
Tactic: rcases h with ⟨h₁, h₂⟩
Cleared hypotheses: h
-- 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
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
i j : Fin (HAdd.hAdd (α := ℕ) 2 1)
hij : i ≠ j
hi : i = i₁ ∧ j = i₂ ∨ i = i₂ ∧ j = i₁ ∨ i = i₁ ∧ j = i₃ ∨ i = i₃ ∧ j = i₁ ∨ i = i₂ ∧ j = i₃ ∨ i = i₃ ∧ j = i₂
h₁ : dist (t.points i₁) (t.points i₂) = dist (t.points i₁) (t.points i₃)
h₂ : dist (t.points i₁) (t.points i₂) = dist (t.points i₂) (t.points i₃)
⊢ dist (t.points i) (t.points j) = dist (t.points i₁) (t.points i₂)
have refine_2 : ∀ (h₁₃ : i ≠ i₃) (h₂₃ : j ≠ i₃) (h₁₂ : i ≠ j) (h₁ : dist (t.points i) (t.points j) = dist (t.points i) (t.points i₃))
  (h₂ : dist (t.points i) (t.points j) = dist (t.points j) (t.points i₃)),
  dist (t.points i) (t.points j) = dist (t.points i) (t.points j)
Tactic: rcases hi with ⟨rfl, rfl⟩ | ⟨rfl, rfl⟩ | ⟨rfl, rfl⟩ | ⟨rfl, rfl⟩ | ⟨rfl, rfl⟩ | ⟨rfl, rfl⟩
Cleared hypotheses: i₁, i₂, h₁₂, h₁₃, h₂₃, hi, h₁, h₂
-- 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
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
i j : Fin (HAdd.hAdd (α := ℕ) 2 1)
hij : i ≠ j
hi : i = i₁ ∧ j = i₂ ∨ i = i₂ ∧ j = i₁ ∨ i = i₁ ∧ j = i₃ ∨ i = i₃ ∧ j = i₁ ∨ i = i₂ ∧ j = i₃ ∨ i = i₃ ∧ j = i₂
h₁ : dist (t.points i₁) (t.points i₂) = dist (t.points i₁) (t.points i₃)
h₂ : dist (t.points i₁) (t.points i₂) = dist (t.points i₂) (t.points i₃)
refine_2 :
  ∀ (h₁₃ : i ≠ i₃) (h₂₃ : j ≠ i₃) (h₁₂ : i ≠ j) (h₁ : dist (t.points i) (t.points j) = dist (t.points i) (t.points i₃))
    (h₂ : dist (t.points i) (t.points j) = dist (t.points j) (t.points i₃)),
    dist (t.points i) (t.points j) = dist (t.points i) (t.points j)
⊢ dist (t.points i) (t.points j) = dist (t.points i₁) (t.points i₂)
have refine_2₁ : ∀ (h₂₃ : i ≠ i₃) (h₁₃ : j ≠ i₃) (h₁₂ : j ≠ i) (h₁ : dist (t.points j) (t.points i) = dist (t.points j) (t.points i₃))
  (h₂ : dist (t.points j) (t.points i) = dist (t.points i) (t.points i₃)),
  dist (t.points i) (t.points j) = dist (t.points j) (t.points i)
Tactic: rcases hi with ⟨rfl, rfl⟩ | ⟨rfl, rfl⟩ | ⟨rfl, rfl⟩ | ⟨rfl, rfl⟩ | ⟨rfl, rfl⟩ | ⟨rfl, rfl⟩
Cleared hypotheses: i₁, i₂, h₁₂, h₁₃, h₂₃, hi, h₁, h₂