awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Affine.Simplex
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.swap 0 j) : (a : Fin (n + 1)) → Fin (n + 1)) = (⇑x : (a : P) → P) ∘ s.points
h : Eq (α := Fin (n + 1)) ((Equiv.swap 0 j : (a : Fin (n + 1)) → Fin (n + 1)) 1) 1
⊢ dist (s.points j) (s.points 1) = dist (s.points j) (s.points ((Equiv.swap 0 j : (a : Fin (n + 1)) → Fin (n + 1)) 1))

Tactic:
convert! rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Affine.Simplex
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.swap 0 j) : (a : Fin (n + 1)) → Fin (n + 1)) = (⇑x : (a : P) → P) ∘ s.points
⊢ Ne (α := Fin (n + 1)) 1 0

Tactic:
simp [hn]
-- Module: Mathlib.Analysis.Normed.Affine.Simplex
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.swap 0 j) : (a : Fin (n + 1)) → Fin (n + 1)) = (⇑x : (a : P) → P) ∘ s.points
⊢ 1 ≠ j

Tactic:
lia
-- Module: Mathlib.Analysis.Normed.Affine.Simplex
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.swap 0 j) : (a : Fin (n + 1)) → Fin (n + 1)) = (⇑x : (a : P) → P) ∘ s.points
h h₁ : Eq (α := Fin (n + 1)) 1 1
⊢ Eq (α := Fin (n + 1)) ((Equiv.swap 0 j : (a : Fin (n + 1)) → Fin (n + 1)) 1) 1

Tactic:
rw [Equiv.swap_apply_of_ne_of_ne (by simp [hn]) (by lia)]

Premises used: Equiv.swap_apply_of_ne_of_ne
-- Module: Mathlib.Analysis.Normed.Affine.Simplex
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
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)
⊢ 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⟩

Premises used: Equiv.trans, Equiv.swap, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Affine.Simplex
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
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)
⊢ dist (s.points i) (s.points j) = dist (s.points 0) (s.points 1)

Tactic:
nth_rw 2 [← x.dist_eq]

Premises used: IsometryEquiv.dist_eq
-- Module: Mathlib.Analysis.Normed.Affine.Simplex
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
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)
⊢ 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:
simp_rw [← Function.comp_apply (f := x), ← hx]

Premises used: Function.comp_apply
-- Module: Mathlib.Analysis.Normed.Affine.Simplex
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
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)))
⊢ 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 only [Equiv.coe_trans, comp_apply, Equiv.swap_apply_left]

Premises used: Function.comp_apply, Equiv.coe_trans, Equiv.swap_apply_left
-- Module: Mathlib.Analysis.Normed.Affine.Simplex
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 i) (s.points j)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Affine.Simplex
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
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
⊢ 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:
convert! rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Affine.Simplex
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)) i = i

Tactic:
Equiv.swap_apply_of_ne_of_ne hi hij

Premises used: Equiv.swap_apply_of_ne_of_ne
-- Module: Mathlib.Analysis.Normed.Affine.Simplex
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)) i = i

Tactic:
exact Equiv.swap_apply_of_ne_of_ne hi hij

Premises used: Equiv.swap_apply_of_ne_of_ne
-- Module: Mathlib.Analysis.Normed.Affine.Simplex
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
⊢ Ne (α := Fin (n + 1)) 1 0

Tactic:
simp [hn]
-- Module: Mathlib.Analysis.Normed.Affine.Simplex
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)) 1 = j
⊢ (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:
rw [Equiv.swap_apply_of_ne_of_ne (by simp [hn]) (Ne.symm hi)]

Premises used: Ne.symm, Equiv.swap_apply_of_ne_of_ne
-- Module: Mathlib.Analysis.Normed.Affine.Simplex
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)) 1 = j

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Affine.Simplex
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 : Simplex.Scalene t
⊢ Ne (α := Fin 3) 0 1

Tactic:
decide
-- Module: Mathlib.Analysis.Normed.Affine.Simplex
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 : Simplex.Scalene t
⊢ Ne (α := Fin 3) 0 2

Tactic:
decide
-- Module: Mathlib.Analysis.Normed.Affine.Simplex
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 : Simplex.Scalene t
⊢ ¬(Eq (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) 0 0 ∧ Eq (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) 1 2)

Tactic:
decide
-- Module: Mathlib.Analysis.Normed.Affine.Simplex
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 : Simplex.Scalene t
⊢ ¬(Eq (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) 0 2 ∧ Eq (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) 1 0)

Tactic:
decide
-- Module: Mathlib.Analysis.Normed.Affine.Simplex
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 : Simplex.Scalene t
⊢ Ne (α := Fin 3) 1 2

Tactic:
decide
-- Module: Mathlib.Analysis.Normed.Affine.Simplex
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 : Simplex.Scalene t
⊢ ¬(Eq (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) 0 1 ∧ Eq (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) 1 2)

Tactic:
decide
-- Module: Mathlib.Analysis.Normed.Affine.Simplex
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 : Simplex.Scalene t
⊢ ¬(Eq (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) 0 2 ∧ Eq (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) 1 1)

Tactic:
decide
-- Module: Mathlib.Analysis.Normed.Affine.Simplex
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 : Simplex.Scalene t
⊢ ¬(Eq (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) 0 1 ∧ Eq (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) 2 2)

Tactic:
decide
-- Module: Mathlib.Analysis.Normed.Affine.Simplex
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 : Simplex.Scalene t
⊢ ¬(Eq (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) 0 2 ∧ Eq (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) 2 1)

Tactic:
decide
-- Module: Mathlib.Analysis.Normed.Affine.Simplex
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
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
⊢ 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)

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₃⟩ ↦ ?_⟩
-- Module: Mathlib.Analysis.Normed.Affine.Simplex
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
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)
⊢ ∀ ⦃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₂

Tactic:
⟨⟨y₁, y₂⟩, hy⟩
-- Module: Mathlib.Analysis.Normed.Affine.Simplex
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₂)
simp : x₁ = y₁ ∧ x₂ = 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)

Tactic:
simp only [Subtype.mk.injEq, Prod.mk.injEq]

Premises used: Prod.mk.injEq, Subtype.mk.injEq
-- Module: Mathlib.Analysis.Normed.Affine.Simplex
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₂
2 :
  ∀ (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₂
⊢ x₁ = y₁ ∧ x₂ = y₂

Tactic:
fin_cases x₁
-- Module: Mathlib.Analysis.Normed.Affine.Simplex
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₂
h_2 :
  ∀
    (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₂
⊢ (fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨0, ⋯⟩ = y₁ ∧ x₂ = y₂

Tactic:
fin_cases x₂