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
n : ℕ
s : Simplex R P n
hr : s.Regular
i j : Fin (n + 1)
hij : i ≠ j
hn : n ≠ 0
hi : ¬i = 1
⊢ dist (s.points i) (s.points j) = dist (s.points 0) (s.points 1)
have neg : ∀ (x : P ≃ᵢ P)
  (hx :
    s.points ∘ (⇑(Equiv.trans (Equiv.swap 0 i) (Equiv.swap 1 j)) : (a : Fin (n + 1)) → Fin (n + 1)) =
      (⇑x : (a : P) → P) ∘ s.points),
  dist (s.points i) (s.points j) = dist (s.points 0) (s.points 1)
Tactic: rcases hr ((Equiv.swap 0 i).trans (Equiv.swap 1 j)) with ⟨x, 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
n : ℕ
s : Simplex R P n
hr : s.Regular
i j : Fin (n + 1)
hij : i ≠ j
hn : n ≠ 0
hi : ¬i = 1
x : P ≃ᵢ P
hx :
  s.points ∘ (⇑(Equiv.trans (Equiv.swap 0 i) (Equiv.swap 1 j)) : (a : Fin (n + 1)) → Fin (n + 1)) =
    (⇑x : (a : P) → P) ∘ s.points
⊢ dist (s.points i) (s.points j) = dist (s.points 0) (s.points 1)
have neg : dist (s.points i) (s.points j) = dist (α := P) ((x : (a : P) → P) (s.points 0) : P) ((x : (a : P) → P) (s.points 1) : P)
Tactic: nth_rw 2 [← x.dist_eq]
-- 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
n : ℕ
s : Simplex R P n
hr : s.Regular
i j : Fin (n + 1)
hij : i ≠ j
hn : n ≠ 0
hi : ¬i = 1
x : P ≃ᵢ P
hx :
  s.points ∘ (⇑(Equiv.trans (Equiv.swap 0 i) (Equiv.swap 1 j)) : (a : Fin (n + 1)) → Fin (n + 1)) =
    (⇑x : (a : P) → P) ∘ s.points
⊢ dist (s.points i) (s.points j) =
    dist (α := P) ((x : (a : P) → P) (s.points 0) : P) ((x : (a : P) → P) (s.points 1) : P)
have neg : dist (s.points i) (s.points j) =
  dist
    (comp (α := Fin (n + 1)) s.points
      (⇑(Equiv.trans (Equiv.swap 0 i) (Equiv.swap 1 j)) : (a : Fin (n + 1)) → Fin (n + 1)) 0)
    (comp (α := Fin (n + 1)) s.points
      (⇑(Equiv.trans (Equiv.swap 0 i) (Equiv.swap 1 j)) : (a : Fin (n + 1)) → Fin (n + 1)) 1)
Tactic: simp_rw [← Function.comp_apply (f := x), ← 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
n : ℕ
s : Simplex R P n
hr : s.Regular
i j : Fin (n + 1)
hij : i ≠ j
hn : n ≠ 0
hi : ¬i = 1
x : P ≃ᵢ P
hx :
  s.points ∘ (⇑(Equiv.trans (Equiv.swap 0 i) (Equiv.swap 1 j)) : (a : Fin (n + 1)) → Fin (n + 1)) =
    (⇑x : (a : P) → P) ∘ s.points
⊢ dist (s.points i) (s.points j) =
    dist
      (comp (α := Fin (n + 1)) s.points
        (⇑(Equiv.trans (Equiv.swap 0 i) (Equiv.swap 1 j)) : (a : Fin (n + 1)) → Fin (n + 1)) 0)
      (comp (α := Fin (n + 1)) s.points
        (⇑(Equiv.trans (Equiv.swap 0 i) (Equiv.swap 1 j)) : (a : Fin (n + 1)) → Fin (n + 1)) 1)
have neg : dist (s.points i) (s.points j) =
  dist (s.points ((Equiv.swap 1 j : (a : Fin (n + 1)) → Fin (n + 1)) i))
    (s.points
      ((Equiv.swap 1 j : (a : Fin (n + 1)) → Fin (n + 1)) ((Equiv.swap 0 i : (a : Fin (n + 1)) → Fin (n + 1)) 1)))
Tactic: simp only [Equiv.coe_trans, comp_apply, Equiv.swap_apply_left]
-- 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
n : ℕ
s : Simplex R P n
hr : s.Regular
i j : Fin (n + 1)
hij : i ≠ j
hn : n ≠ 0
hi : ¬i = 1
x : P ≃ᵢ P
hx :
  s.points ∘ (⇑(Equiv.trans (Equiv.swap 0 i) (Equiv.swap 1 j)) : (a : Fin (n + 1)) → Fin (n + 1)) =
    (⇑x : (a : P) → P) ∘ s.points
⊢ dist (s.points i) (s.points j) =
    dist (s.points ((Equiv.swap 1 j : (a : Fin (n + 1)) → Fin (n + 1)) i))
      (s.points
        ((Equiv.swap 1 j : (a : Fin (n + 1)) → Fin (n + 1)) ((Equiv.swap 0 i : (a : Fin (n + 1)) → Fin (n + 1)) 1)))
have h : (Equiv.swap 1 j : (a : Fin (n + 1)) → Fin (n + 1)) i = i
Tactic: convert! rfl
-- 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
n : ℕ
s : Simplex R P n
hr : s.Regular
i j : Fin (n + 1)
hij : i ≠ j
hn : n ≠ 0
hi : ¬i = 1
x : P ≃ᵢ P
hx :
  s.points ∘ (⇑(Equiv.trans (Equiv.swap 0 i) (Equiv.swap 1 j)) : (a : Fin (n + 1)) → Fin (n + 1)) =
    (⇑x : (a : P) → P) ∘ s.points
h : (Equiv.swap 1 j : (a : Fin (n + 1)) → Fin (n + 1)) i = i
⊢ dist (s.points i) (s.points j) =
    dist (s.points ((Equiv.swap 1 j : (a : Fin (n + 1)) → Fin (n + 1)) i))
      (s.points
        ((Equiv.swap 1 j : (a : Fin (n + 1)) → Fin (n + 1)) ((Equiv.swap 0 i : (a : Fin (n + 1)) → Fin (n + 1)) 1)))
have h₁ : (Equiv.swap 1 j : (a : Fin (n + 1)) → Fin (n + 1)) ((Equiv.swap 0 i : (a : Fin (n + 1)) → Fin (n + 1)) 1) = j
Tactic: convert! rfl
-- 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
n : ℕ
s : Simplex R P n
hr : s.Regular
i j : Fin (n + 1)
hij : i ≠ j
hn : n ≠ 0
hi : ¬i = 1
x : P ≃ᵢ P
hx :
  s.points ∘ (⇑(Equiv.trans (Equiv.swap 0 i) (Equiv.swap 1 j)) : (a : Fin (n + 1)) → Fin (n + 1)) =
    (⇑x : (a : P) → P) ∘ s.points
⊢ (Equiv.swap 1 j : (a : Fin (n + 1)) → Fin (n + 1)) ((Equiv.swap 0 i : (a : Fin (n + 1)) → Fin (n + 1)) 1) = j
have h : (Equiv.swap 1 j : (a : Fin (n + 1)) → Fin (n + 1)) 1 = j
Tactic: rw [Equiv.swap_apply_of_ne_of_ne (by simp [hn]) (Ne.symm hi)]
-- 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
⊢ Simplex.Scalene t ↔
    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)
have refine : 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)), Simplex.Scalene t
Tactic: refine ⟨fun h ↦
    ⟨h.dist_ne (by decide : (0 : Fin 3) ≠ 1) (by decide : (0 : Fin 3) ≠ 2) (by decide) (by decide),
     h.dist_ne (by decide : (0 : Fin 3) ≠ 1) (by decide : (1 : Fin 3) ≠ 2) (by decide) (by decide),
     h.dist_ne (by decide : (0 : Fin 3) ≠ 2) (by decide : (1 : Fin 3) ≠ 2) (by decide) (by decide)⟩,
    fun ⟨h₁, 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
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₁ x₂ : Fin (HAdd.hAdd (α := ℕ) 2 1)
hx : (x₁, x₂).1 < (x₁, x₂).2
⊢ ∀ ⦃a₂ : { x : Fin (HAdd.hAdd (α := ℕ) 2 1) × Fin (HAdd.hAdd (α := ℕ) 2 1) // x.1 < x.2 }⦄,
    Eq (α := ℝ)
        ((fun (i : { x : Fin (HAdd.hAdd (α := ℕ) 2 1) × Fin (HAdd.hAdd (α := ℕ) 2 1) // x.1 < x.2 }) ↦
            dist (t.points (↑i : Fin (2 + 1) × Fin (2 + 1)).1) (t.points (↑i : Fin (2 + 1) × Fin (2 + 1)).2))
          (Subtype.mk (p := fun (x : Fin (HAdd.hAdd (α := ℕ) 2 1) × Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ x.1 < x.2) (x₁, x₂)
            hx))
        ((fun (i : { x : Fin (HAdd.hAdd (α := ℕ) 2 1) × Fin (HAdd.hAdd (α := ℕ) 2 1) // x.1 < x.2 }) ↦
            dist (t.points (↑i : Fin (2 + 1) × Fin (2 + 1)).1) (t.points (↑i : Fin (2 + 1) × Fin (2 + 1)).2))
          a₂) →
      Subtype.mk (p := fun (x : Fin (HAdd.hAdd (α := ℕ) 2 1) × Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ x.1 < x.2) (x₁, x₂) hx =
        a₂
have this : ∀ (y₁ y₂ : Fin (HAdd.hAdd (α := ℕ) 2 1)) (hy : (y₁, y₂).1 < (y₁, y₂).2),
  Eq (α := ℝ)
      ((fun (i : { x : Fin (HAdd.hAdd (α := ℕ) 2 1) × Fin (HAdd.hAdd (α := ℕ) 2 1) // x.1 < x.2 }) ↦
          dist (t.points (↑i : Fin (2 + 1) × Fin (2 + 1)).1) (t.points (↑i : Fin (2 + 1) × Fin (2 + 1)).2))
        (Subtype.mk (p := fun (x : Fin (HAdd.hAdd (α := ℕ) 2 1) × Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ x.1 < x.2) (x₁, x₂)
          hx))
      ((fun (i : { x : Fin (HAdd.hAdd (α := ℕ) 2 1) × Fin (HAdd.hAdd (α := ℕ) 2 1) // x.1 < x.2 }) ↦
          dist (t.points (↑i : Fin (2 + 1) × Fin (2 + 1)).1) (t.points (↑i : Fin (2 + 1) × Fin (2 + 1)).2))
        (Subtype.mk (p := fun (x : Fin (HAdd.hAdd (α := ℕ) 2 1) × Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ x.1 < x.2) (y₁, y₂)
          hy)) →
    Eq (α := { x : Fin (HAdd.hAdd (α := ℕ) 2 1) × Fin (HAdd.hAdd (α := ℕ) 2 1) // x.1 < x.2 })
      (Subtype.mk (p := fun (x : Fin (HAdd.hAdd (α := ℕ) 2 1) × Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ x.1 < x.2) (x₁, x₂) hx)
      (Subtype.mk (p := fun (x : Fin (HAdd.hAdd (α := ℕ) 2 1) × Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ x.1 < x.2) (y₁, y₂) hy)
Tactic: ⟨⟨y₁, y₂⟩, hy⟩
-- 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₁ x₂ : Fin (HAdd.hAdd (α := ℕ) 2 1)
hx : x₁ < x₂
y₁ y₂ : Fin (HAdd.hAdd (α := ℕ) 2 1)
hy : y₁ < y₂
hxy : dist (t.points x₁) (t.points x₂) = dist (t.points y₁) (t.points y₂)
⊢ Eq (α := { x : Fin (HAdd.hAdd (α := ℕ) 2 1) × Fin (HAdd.hAdd (α := ℕ) 2 1) // x.1 < x.2 })
    (Subtype.mk (p := fun (x : Fin (HAdd.hAdd (α := ℕ) 2 1) × Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ x.1 < x.2) (x₁, x₂) hx)
    (Subtype.mk (p := fun (x : Fin (HAdd.hAdd (α := ℕ) 2 1) × Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ x.1 < x.2) (y₁, y₂) hy)
have simp : x₁ = y₁ ∧ x₂ = y₂
Tactic: simp only [Subtype.mk.injEq, Prod.mk.injEq]
-- 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₁ x₂ : Fin (HAdd.hAdd (α := ℕ) 2 1)
hx : x₁ < x₂
y₁ y₂ : Fin (HAdd.hAdd (α := ℕ) 2 1)
hy : y₁ < y₂
hxy : dist (t.points x₁) (t.points x₂) = dist (t.points y₁) (t.points y₂)
⊢ x₁ = y₁ ∧ x₂ = y₂
have 0 : ∀ (hx : (fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨0, sorry⟩ < x₂)
  (hxy :
    dist (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨0, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))))
        (t.points x₂) =
      dist (t.points y₁) (t.points y₂)),
  (fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨0, sorry⟩ = y₁ ∧ x₂ = 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₁ x₂ : Fin (HAdd.hAdd (α := ℕ) 2 1)
hx : x₁ < x₂
y₁ y₂ : Fin (HAdd.hAdd (α := ℕ) 2 1)
hy : y₁ < y₂
hxy : dist (t.points x₁) (t.points x₂) = dist (t.points y₁) (t.points y₂)
0 :
  ∀ (hx : (fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨0, ⋯⟩ < x₂)
    (hxy :
      dist (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))))
          (t.points x₂) =
        dist (t.points y₁) (t.points y₂)),
    (fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨0, ⋯⟩ = y₁ ∧ x₂ = y₂
⊢ x₁ = y₁ ∧ x₂ = y₂
have 1 : ∀ (hx : (fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨1, sorry⟩ < x₂)
  (hxy :
    dist (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨1, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))))
        (t.points x₂) =
      dist (t.points y₁) (t.points y₂)),
  (fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨1, sorry⟩ = y₁ ∧ x₂ = 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₁ x₂ : Fin (HAdd.hAdd (α := ℕ) 2 1)
hx : x₁ < x₂
y₁ y₂ : Fin (HAdd.hAdd (α := ℕ) 2 1)
hy : y₁ < y₂
hxy : dist (t.points x₁) (t.points x₂) = dist (t.points y₁) (t.points y₂)
0 :
  ∀ (hx : (fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨0, ⋯⟩ < x₂)
    (hxy :
      dist (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))))
          (t.points x₂) =
        dist (t.points y₁) (t.points y₂)),
    (fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨0, ⋯⟩ = y₁ ∧ x₂ = y₂
1 :
  ∀ (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₂
⊢ x₁ = y₁ ∧ x₂ = y₂
have 2 : ∀ (hx : (fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨2, sorry⟩ < x₂)
  (hxy :
    dist (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨2, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))))
        (t.points x₂) =
      dist (t.points y₁) (t.points y₂)),
  (fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨2, sorry⟩ = y₁ ∧ x₂ = 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) ⟨0, ⋯⟩ < x₂
hxy :
  dist (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))) (t.points x₂) =
    dist (t.points y₁) (t.points y₂)
⊢ (fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨0, ⋯⟩ = y₁ ∧ x₂ = y₂
have 0 : ∀
  (hx :
    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) (⟨0, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))) =
      dist (t.points y₁) (t.points y₂)),
  (fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨0, 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) ⟨0, ⋯⟩ < x₂
hxy :
  dist (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))) (t.points x₂) =
    dist (t.points y₁) (t.points y₂)
0 :
  ∀
    (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) ⟨0, ⋯⟩))
    (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) (⟨0, ⋯⟩ : 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) ⟨0, ⋯⟩ = y₂
⊢ (fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨0, ⋯⟩ = y₁ ∧ x₂ = y₂
have 0₁ : ∀
  (hx :
    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) ⟨1, 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 y₁) (t.points y₂)),
  (fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨0, 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) ⟨0, ⋯⟩ < x₂
hxy :
  dist (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))) (t.points x₂) =
    dist (t.points y₁) (t.points y₂)
0 :
  ∀
    (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) ⟨0, ⋯⟩))
    (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) (⟨0, ⋯⟩ : 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) ⟨0, ⋯⟩ = y₂
h_1 :
  ∀
    (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₂
⊢ (fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨0, ⋯⟩ = y₁ ∧ x₂ = y₂
have 0₁ : ∀
  (hx :
    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) ⟨2, 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 y₁) (t.points y₂)),
  (fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨0, sorry⟩ = y₁ ∧ (fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨2, sorry⟩ = y₂
Tactic: fin_cases x₂
Cleared hypotheses: x₂, hx, hxy