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
hs : s.Scalene
i₁ i₂ i₃ i₄ : Fin (n + 1)
h₁₂ : i₁ ≠ i₂
h₃₄ : i₃ ≠ i₄
h₁₂₃₄ : ¬i₁ = i₃ ∨ ¬i₂ = i₄
h₁₂₄₃ : ¬i₁ = i₄ ∨ ¬i₂ = i₃
inl : ∀ (h₁₂lt : i₁ < i₂), dist (s.points i₁) (s.points i₂) ≠ dist (s.points i₃) (s.points i₄)
inr : ∀ (h₂₁lt : i₂ < i₁), dist (s.points i₁) (s.points i₂) ≠ dist (s.points i₃) (s.points i₄)
⊢ dist (s.points i₁) (s.points i₂) ≠ dist (s.points i₃) (s.points i₄)

Tactic:
rcases h₁₂.lt_or_gt with h₁₂lt | h₂₁lt

Premises used: Ne.lt_or_gt
-- 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
hs : s.Scalene
i₁ i₂ i₃ i₄ : Fin (n + 1)
h₁₂ : i₁ ≠ i₂
h₃₄ : i₃ ≠ i₄
h₁₂₃₄ : ¬i₁ = i₃ ∨ ¬i₂ = i₄
h₁₂₄₃ : ¬i₁ = i₄ ∨ ¬i₂ = i₃
h₁₂lt : i₁ < i₂
inl : ∀ (h₃₄lt : i₃ < i₄), dist (s.points i₁) (s.points i₂) ≠ dist (s.points i₃) (s.points i₄)
inl₁ : ∀ (h₄₃lt : i₄ < i₃), dist (s.points i₁) (s.points i₂) ≠ dist (s.points i₃) (s.points i₄)
⊢ dist (s.points i₁) (s.points i₂) ≠ dist (s.points i₃) (s.points i₄)

Tactic:
rcases h₃₄.lt_or_gt with h₃₄lt | h₄₃lt

Premises used: Ne.lt_or_gt
-- 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
hs : s.Scalene
i₁ i₂ i₃ i₄ : Fin (n + 1)
h₁₂ : i₁ ≠ i₂
h₃₄ : i₃ ≠ i₄
h₁₂₃₄ : ¬i₁ = i₃ ∨ ¬i₂ = i₄
h₁₂₄₃ : ¬i₁ = i₄ ∨ ¬i₂ = i₃
h₂₁lt : i₂ < i₁
inr : ∀ (h₃₄lt : i₃ < i₄), dist (s.points i₁) (s.points i₂) ≠ dist (s.points i₃) (s.points i₄)
inr₁ : ∀ (h₄₃lt : i₄ < i₃), dist (s.points i₁) (s.points i₂) ≠ dist (s.points i₃) (s.points i₄)
⊢ dist (s.points i₁) (s.points i₂) ≠ dist (s.points i₃) (s.points i₄)

Tactic:
rcases h₃₄.lt_or_gt with h₃₄lt | h₄₃lt

Premises used: Ne.lt_or_gt
-- 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
hs : s.Scalene
i₁ i₂ i₃ i₄ : Fin (n + 1)
h₁₂ : i₁ ≠ i₂
h₃₄ : i₃ ≠ i₄
h₁₂₃₄ : ¬i₁ = i₃ ∨ ¬i₂ = i₄
h₁₂₄₃ : ¬i₁ = i₄ ∨ ¬i₂ = i₃
h₁₂lt : i₁ < i₂
h₃₄lt : i₃ < i₄
inl :
  Ne (α := { x : Fin (n + 1) × Fin (n + 1) // x.1 < x.2 })
    (Subtype.mk (p := fun (x : Fin (n + 1) × Fin (n + 1)) ↦ x.1 < x.2) (i₁, i₂) h₁₂lt)
    (Subtype.mk (p := fun (x : Fin (n + 1) × Fin (n + 1)) ↦ x.1 < x.2) (i₃, i₄) h₃₄lt)
⊢ dist (s.points i₁) (s.points i₂) ≠ dist (s.points i₃) (s.points i₄)

Tactic:
apply hs.ne (a₁ := ⟨(i₁, i₂), h₁₂lt⟩) (a₂ := ⟨(i₃, i₄), h₃₄lt⟩)

Premises used: Function.Injective.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
hs : s.Scalene
i₁ i₂ i₃ i₄ : Fin (n + 1)
h₁₂ : i₁ ≠ i₂
h₃₄ : i₃ ≠ i₄
h₁₂₃₄ : ¬i₁ = i₃ ∨ ¬i₂ = i₄
h₁₂₄₃ : ¬i₁ = i₄ ∨ ¬i₂ = i₃
h₁₂lt : i₁ < i₂
h₃₄lt : i₃ < i₄
inl :
  ¬i₁ = i₃ →
    Ne (α := { x : Fin (n + 1) × Fin (n + 1) // x.1 < x.2 })
      (Subtype.mk (p := fun (x : Fin (n + 1) × Fin (n + 1)) ↦ x.1 < x.2) (i₁, i₂) h₁₂lt)
      (Subtype.mk (p := fun (x : Fin (n + 1) × Fin (n + 1)) ↦ x.1 < x.2) (i₃, i₄) h₃₄lt)
inl₁ :
  ¬i₂ = i₄ →
    Ne (α := { x : Fin (n + 1) × Fin (n + 1) // x.1 < x.2 })
      (Subtype.mk (p := fun (x : Fin (n + 1) × Fin (n + 1)) ↦ x.1 < x.2) (i₁, i₂) h₁₂lt)
      (Subtype.mk (p := fun (x : Fin (n + 1) × Fin (n + 1)) ↦ x.1 < x.2) (i₃, i₄) h₃₄lt)
⊢ Ne (α := { x : Fin (n + 1) × Fin (n + 1) // x.1 < x.2 })
    (Subtype.mk (p := fun (x : Fin (n + 1) × Fin (n + 1)) ↦ x.1 < x.2) (i₁, i₂) h₁₂lt)
    (Subtype.mk (p := fun (x : Fin (n + 1) × Fin (n + 1)) ↦ x.1 < x.2) (i₃, i₄) h₃₄lt)

Tactic:
cases 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
n : ℕ
s : Simplex R P n
hs : s.Scalene
i₁ i₂ i₃ i₄ : Fin (n + 1)
h₁₂ : i₁ ≠ i₂
h₃₄ : i₃ ≠ i₄
h₁₂₄₃ : ¬i₁ = i₄ ∨ ¬i₂ = i₃
h₁₂lt : i₁ < i₂
h₃₄lt : i₃ < i₄
h : ¬i₁ = i₃
⊢ Ne (α := { x : Fin (n + 1) × Fin (n + 1) // x.1 < x.2 })
    (Subtype.mk (p := fun (x : Fin (n + 1) × Fin (n + 1)) ↦ x.1 < x.2) (i₁, i₂) h₁₂lt)
    (Subtype.mk (p := fun (x : Fin (n + 1) × Fin (n + 1)) ↦ x.1 < x.2) (i₃, i₄) h₃₄lt)

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
n : ℕ
s : Simplex R P n
hs : s.Scalene
i₁ i₂ i₃ i₄ : Fin (n + 1)
h₁₂ : i₁ ≠ i₂
h₃₄ : i₃ ≠ i₄
h₁₂₄₃ : ¬i₁ = i₄ ∨ ¬i₂ = i₃
h₁₂lt : i₁ < i₂
h₃₄lt : i₃ < i₄
h : ¬i₂ = i₄
⊢ Ne (α := { x : Fin (n + 1) × Fin (n + 1) // x.1 < x.2 })
    (Subtype.mk (p := fun (x : Fin (n + 1) × Fin (n + 1)) ↦ x.1 < x.2) (i₁, i₂) h₁₂lt)
    (Subtype.mk (p := fun (x : Fin (n + 1) × Fin (n + 1)) ↦ x.1 < x.2) (i₃, i₄) h₃₄lt)

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
n : ℕ
s : Simplex R P n
hs : s.Scalene
i₁ i₂ i₃ i₄ : Fin (n + 1)
h₁₂ : i₁ ≠ i₂
h₃₄ : i₃ ≠ i₄
h₁₂₃₄ : ¬i₁ = i₃ ∨ ¬i₂ = i₄
h₁₂₄₃ : ¬i₁ = i₄ ∨ ¬i₂ = i₃
h₁₂lt : i₁ < i₂
h₄₃lt : i₄ < i₃
inl : dist (s.points i₁) (s.points i₂) ≠ dist (s.points i₄) (s.points i₃)
⊢ dist (s.points i₁) (s.points i₂) ≠ dist (s.points i₃) (s.points i₄)

Tactic:
nth_rw 2 [dist_comm]

Premises used: dist_comm
-- 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
hs : s.Scalene
i₁ i₂ i₃ i₄ : Fin (n + 1)
h₁₂ : i₁ ≠ i₂
h₃₄ : i₃ ≠ i₄
h₁₂₃₄ : ¬i₁ = i₃ ∨ ¬i₂ = i₄
h₁₂₄₃ : ¬i₁ = i₄ ∨ ¬i₂ = i₃
h₁₂lt : i₁ < i₂
h₄₃lt : i₄ < i₃
inl :
  Ne (α := { x : Fin (n + 1) × Fin (n + 1) // x.1 < x.2 })
    (Subtype.mk (p := fun (x : Fin (n + 1) × Fin (n + 1)) ↦ x.1 < x.2) (i₁, i₂) h₁₂lt)
    (Subtype.mk (p := fun (x : Fin (n + 1) × Fin (n + 1)) ↦ x.1 < x.2) (i₄, i₃) h₄₃lt)
⊢ dist (s.points i₁) (s.points i₂) ≠ dist (s.points i₄) (s.points i₃)

Tactic:
apply hs.ne (a₁ := ⟨(i₁, i₂), h₁₂lt⟩) (a₂ := ⟨(i₄, i₃), h₄₃lt⟩)

Premises used: Function.Injective.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
hs : s.Scalene
i₁ i₂ i₃ i₄ : Fin (n + 1)
h₁₂ : i₁ ≠ i₂
h₃₄ : i₃ ≠ i₄
h₁₂₃₄ : ¬i₁ = i₃ ∨ ¬i₂ = i₄
h₁₂₄₃ : ¬i₁ = i₄ ∨ ¬i₂ = i₃
h₁₂lt : i₁ < i₂
h₄₃lt : i₄ < i₃
inl :
  ¬i₁ = i₄ →
    Ne (α := { x : Fin (n + 1) × Fin (n + 1) // x.1 < x.2 })
      (Subtype.mk (p := fun (x : Fin (n + 1) × Fin (n + 1)) ↦ x.1 < x.2) (i₁, i₂) h₁₂lt)
      (Subtype.mk (p := fun (x : Fin (n + 1) × Fin (n + 1)) ↦ x.1 < x.2) (i₄, i₃) h₄₃lt)
inl₁ :
  ¬i₂ = i₃ →
    Ne (α := { x : Fin (n + 1) × Fin (n + 1) // x.1 < x.2 })
      (Subtype.mk (p := fun (x : Fin (n + 1) × Fin (n + 1)) ↦ x.1 < x.2) (i₁, i₂) h₁₂lt)
      (Subtype.mk (p := fun (x : Fin (n + 1) × Fin (n + 1)) ↦ x.1 < x.2) (i₄, i₃) h₄₃lt)
⊢ Ne (α := { x : Fin (n + 1) × Fin (n + 1) // x.1 < x.2 })
    (Subtype.mk (p := fun (x : Fin (n + 1) × Fin (n + 1)) ↦ x.1 < x.2) (i₁, i₂) h₁₂lt)
    (Subtype.mk (p := fun (x : Fin (n + 1) × Fin (n + 1)) ↦ x.1 < x.2) (i₄, i₃) h₄₃lt)

Tactic:
cases 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
n : ℕ
s : Simplex R P n
hs : s.Scalene
i₁ i₂ i₃ i₄ : Fin (n + 1)
h₁₂ : i₁ ≠ i₂
h₃₄ : i₃ ≠ i₄
h₁₂₃₄ : ¬i₁ = i₃ ∨ ¬i₂ = i₄
h₁₂lt : i₁ < i₂
h₄₃lt : i₄ < i₃
h : ¬i₁ = i₄
⊢ Ne (α := { x : Fin (n + 1) × Fin (n + 1) // x.1 < x.2 })
    (Subtype.mk (p := fun (x : Fin (n + 1) × Fin (n + 1)) ↦ x.1 < x.2) (i₁, i₂) h₁₂lt)
    (Subtype.mk (p := fun (x : Fin (n + 1) × Fin (n + 1)) ↦ x.1 < x.2) (i₄, i₃) h₄₃lt)

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
n : ℕ
s : Simplex R P n
hs : s.Scalene
i₁ i₂ i₃ i₄ : Fin (n + 1)
h₁₂ : i₁ ≠ i₂
h₃₄ : i₃ ≠ i₄
h₁₂₃₄ : ¬i₁ = i₃ ∨ ¬i₂ = i₄
h₁₂lt : i₁ < i₂
h₄₃lt : i₄ < i₃
h : ¬i₂ = i₃
⊢ Ne (α := { x : Fin (n + 1) × Fin (n + 1) // x.1 < x.2 })
    (Subtype.mk (p := fun (x : Fin (n + 1) × Fin (n + 1)) ↦ x.1 < x.2) (i₁, i₂) h₁₂lt)
    (Subtype.mk (p := fun (x : Fin (n + 1) × Fin (n + 1)) ↦ x.1 < x.2) (i₄, i₃) h₄₃lt)

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
n : ℕ
s : Simplex R P n
hs : s.Scalene
i₁ i₂ i₃ i₄ : Fin (n + 1)
h₁₂ : i₁ ≠ i₂
h₃₄ : i₃ ≠ i₄
h₁₂₃₄ : ¬i₁ = i₃ ∨ ¬i₂ = i₄
h₁₂₄₃ : ¬i₁ = i₄ ∨ ¬i₂ = i₃
h₂₁lt : i₂ < i₁
h₃₄lt : i₃ < i₄
inr : dist (s.points i₂) (s.points i₁) ≠ dist (s.points i₃) (s.points i₄)
⊢ dist (s.points i₁) (s.points i₂) ≠ dist (s.points i₃) (s.points i₄)

Tactic:
rw [dist_comm]

Premises used: dist_comm
-- 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
hs : s.Scalene
i₁ i₂ i₃ i₄ : Fin (n + 1)
h₁₂ : i₁ ≠ i₂
h₃₄ : i₃ ≠ i₄
h₁₂₃₄ : ¬i₁ = i₃ ∨ ¬i₂ = i₄
h₁₂₄₃ : ¬i₁ = i₄ ∨ ¬i₂ = i₃
h₂₁lt : i₂ < i₁
h₃₄lt : i₃ < i₄
inr :
  Ne (α := { x : Fin (n + 1) × Fin (n + 1) // x.1 < x.2 })
    (Subtype.mk (p := fun (x : Fin (n + 1) × Fin (n + 1)) ↦ x.1 < x.2) (i₂, i₁) h₂₁lt)
    (Subtype.mk (p := fun (x : Fin (n + 1) × Fin (n + 1)) ↦ x.1 < x.2) (i₃, i₄) h₃₄lt)
⊢ dist (s.points i₂) (s.points i₁) ≠ dist (s.points i₃) (s.points i₄)

Tactic:
apply hs.ne (a₁ := ⟨(i₂, i₁), h₂₁lt⟩) (a₂ := ⟨(i₃, i₄), h₃₄lt⟩)

Premises used: Function.Injective.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
hs : s.Scalene
i₁ i₂ i₃ i₄ : Fin (n + 1)
h₁₂ : i₁ ≠ i₂
h₃₄ : i₃ ≠ i₄
h₁₂₃₄ : ¬i₁ = i₃ ∨ ¬i₂ = i₄
h₁₂₄₃ : ¬i₁ = i₄ ∨ ¬i₂ = i₃
h₂₁lt : i₂ < i₁
h₃₄lt : i₃ < i₄
inr :
  ¬i₁ = i₄ →
    Ne (α := { x : Fin (n + 1) × Fin (n + 1) // x.1 < x.2 })
      (Subtype.mk (p := fun (x : Fin (n + 1) × Fin (n + 1)) ↦ x.1 < x.2) (i₂, i₁) h₂₁lt)
      (Subtype.mk (p := fun (x : Fin (n + 1) × Fin (n + 1)) ↦ x.1 < x.2) (i₃, i₄) h₃₄lt)
inr₁ :
  ¬i₂ = i₃ →
    Ne (α := { x : Fin (n + 1) × Fin (n + 1) // x.1 < x.2 })
      (Subtype.mk (p := fun (x : Fin (n + 1) × Fin (n + 1)) ↦ x.1 < x.2) (i₂, i₁) h₂₁lt)
      (Subtype.mk (p := fun (x : Fin (n + 1) × Fin (n + 1)) ↦ x.1 < x.2) (i₃, i₄) h₃₄lt)
⊢ Ne (α := { x : Fin (n + 1) × Fin (n + 1) // x.1 < x.2 })
    (Subtype.mk (p := fun (x : Fin (n + 1) × Fin (n + 1)) ↦ x.1 < x.2) (i₂, i₁) h₂₁lt)
    (Subtype.mk (p := fun (x : Fin (n + 1) × Fin (n + 1)) ↦ x.1 < x.2) (i₃, i₄) h₃₄lt)

Tactic:
cases 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
n : ℕ
s : Simplex R P n
hs : s.Scalene
i₁ i₂ i₃ i₄ : Fin (n + 1)
h₁₂ : i₁ ≠ i₂
h₃₄ : i₃ ≠ i₄
h₁₂₃₄ : ¬i₁ = i₃ ∨ ¬i₂ = i₄
h₂₁lt : i₂ < i₁
h₃₄lt : i₃ < i₄
h : ¬i₁ = i₄
⊢ Ne (α := { x : Fin (n + 1) × Fin (n + 1) // x.1 < x.2 })
    (Subtype.mk (p := fun (x : Fin (n + 1) × Fin (n + 1)) ↦ x.1 < x.2) (i₂, i₁) h₂₁lt)
    (Subtype.mk (p := fun (x : Fin (n + 1) × Fin (n + 1)) ↦ x.1 < x.2) (i₃, i₄) h₃₄lt)

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
n : ℕ
s : Simplex R P n
hs : s.Scalene
i₁ i₂ i₃ i₄ : Fin (n + 1)
h₁₂ : i₁ ≠ i₂
h₃₄ : i₃ ≠ i₄
h₁₂₃₄ : ¬i₁ = i₃ ∨ ¬i₂ = i₄
h₂₁lt : i₂ < i₁
h₃₄lt : i₃ < i₄
h : ¬i₂ = i₃
⊢ Ne (α := { x : Fin (n + 1) × Fin (n + 1) // x.1 < x.2 })
    (Subtype.mk (p := fun (x : Fin (n + 1) × Fin (n + 1)) ↦ x.1 < x.2) (i₂, i₁) h₂₁lt)
    (Subtype.mk (p := fun (x : Fin (n + 1) × Fin (n + 1)) ↦ x.1 < x.2) (i₃, i₄) h₃₄lt)

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
n : ℕ
s : Simplex R P n
hs : s.Scalene
i₁ i₂ i₃ i₄ : Fin (n + 1)
h₁₂ : i₁ ≠ i₂
h₃₄ : i₃ ≠ i₄
h₁₂₃₄ : ¬i₁ = i₃ ∨ ¬i₂ = i₄
h₁₂₄₃ : ¬i₁ = i₄ ∨ ¬i₂ = i₃
h₂₁lt : i₂ < i₁
h₄₃lt : i₄ < i₃
inr : dist (s.points i₂) (s.points i₁) ≠ dist (s.points i₃) (s.points i₄)
⊢ dist (s.points i₁) (s.points i₂) ≠ dist (s.points i₃) (s.points i₄)

Tactic:
rw [dist_comm]

Premises used: dist_comm
-- 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
hs : s.Scalene
i₁ i₂ i₃ i₄ : Fin (n + 1)
h₁₂ : i₁ ≠ i₂
h₃₄ : i₃ ≠ i₄
h₁₂₃₄ : ¬i₁ = i₃ ∨ ¬i₂ = i₄
h₁₂₄₃ : ¬i₁ = i₄ ∨ ¬i₂ = i₃
h₂₁lt : i₂ < i₁
h₄₃lt : i₄ < i₃
inr : dist (s.points i₂) (s.points i₁) ≠ dist (s.points i₄) (s.points i₃)
⊢ dist (s.points i₂) (s.points i₁) ≠ dist (s.points i₃) (s.points i₄)

Tactic:
nth_rw 2 [dist_comm]

Premises used: dist_comm
-- 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
hs : s.Scalene
i₁ i₂ i₃ i₄ : Fin (n + 1)
h₁₂ : i₁ ≠ i₂
h₃₄ : i₃ ≠ i₄
h₁₂₃₄ : ¬i₁ = i₃ ∨ ¬i₂ = i₄
h₁₂₄₃ : ¬i₁ = i₄ ∨ ¬i₂ = i₃
h₂₁lt : i₂ < i₁
h₄₃lt : i₄ < i₃
inr :
  Ne (α := { x : Fin (n + 1) × Fin (n + 1) // x.1 < x.2 })
    (Subtype.mk (p := fun (x : Fin (n + 1) × Fin (n + 1)) ↦ x.1 < x.2) (i₂, i₁) h₂₁lt)
    (Subtype.mk (p := fun (x : Fin (n + 1) × Fin (n + 1)) ↦ x.1 < x.2) (i₄, i₃) h₄₃lt)
⊢ dist (s.points i₂) (s.points i₁) ≠ dist (s.points i₄) (s.points i₃)

Tactic:
apply hs.ne (a₁ := ⟨(i₂, i₁), h₂₁lt⟩) (a₂ := ⟨(i₄, i₃), h₄₃lt⟩)

Premises used: Function.Injective.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
hs : s.Scalene
i₁ i₂ i₃ i₄ : Fin (n + 1)
h₁₂ : i₁ ≠ i₂
h₃₄ : i₃ ≠ i₄
h₁₂₃₄ : ¬i₁ = i₃ ∨ ¬i₂ = i₄
h₁₂₄₃ : ¬i₁ = i₄ ∨ ¬i₂ = i₃
h₂₁lt : i₂ < i₁
h₄₃lt : i₄ < i₃
inr :
  ¬i₁ = i₃ →
    Ne (α := { x : Fin (n + 1) × Fin (n + 1) // x.1 < x.2 })
      (Subtype.mk (p := fun (x : Fin (n + 1) × Fin (n + 1)) ↦ x.1 < x.2) (i₂, i₁) h₂₁lt)
      (Subtype.mk (p := fun (x : Fin (n + 1) × Fin (n + 1)) ↦ x.1 < x.2) (i₄, i₃) h₄₃lt)
inr₁ :
  ¬i₂ = i₄ →
    Ne (α := { x : Fin (n + 1) × Fin (n + 1) // x.1 < x.2 })
      (Subtype.mk (p := fun (x : Fin (n + 1) × Fin (n + 1)) ↦ x.1 < x.2) (i₂, i₁) h₂₁lt)
      (Subtype.mk (p := fun (x : Fin (n + 1) × Fin (n + 1)) ↦ x.1 < x.2) (i₄, i₃) h₄₃lt)
⊢ Ne (α := { x : Fin (n + 1) × Fin (n + 1) // x.1 < x.2 })
    (Subtype.mk (p := fun (x : Fin (n + 1) × Fin (n + 1)) ↦ x.1 < x.2) (i₂, i₁) h₂₁lt)
    (Subtype.mk (p := fun (x : Fin (n + 1) × Fin (n + 1)) ↦ x.1 < x.2) (i₄, i₃) h₄₃lt)

Tactic:
cases 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
n : ℕ
s : Simplex R P n
hs : s.Scalene
i₁ i₂ i₃ i₄ : Fin (n + 1)
h₁₂ : i₁ ≠ i₂
h₃₄ : i₃ ≠ i₄
h₁₂₄₃ : ¬i₁ = i₄ ∨ ¬i₂ = i₃
h₂₁lt : i₂ < i₁
h₄₃lt : i₄ < i₃
h : ¬i₁ = i₃
⊢ Ne (α := { x : Fin (n + 1) × Fin (n + 1) // x.1 < x.2 })
    (Subtype.mk (p := fun (x : Fin (n + 1) × Fin (n + 1)) ↦ x.1 < x.2) (i₂, i₁) h₂₁lt)
    (Subtype.mk (p := fun (x : Fin (n + 1) × Fin (n + 1)) ↦ x.1 < x.2) (i₄, i₃) h₄₃lt)

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
n : ℕ
s : Simplex R P n
hs : s.Scalene
i₁ i₂ i₃ i₄ : Fin (n + 1)
h₁₂ : i₁ ≠ i₂
h₃₄ : i₃ ≠ i₄
h₁₂₄₃ : ¬i₁ = i₄ ∨ ¬i₂ = i₃
h₂₁lt : i₂ < i₁
h₄₃lt : i₄ < i₃
h : ¬i₂ = i₄
⊢ Ne (α := { x : Fin (n + 1) × Fin (n + 1) // x.1 < x.2 })
    (Subtype.mk (p := fun (x : Fin (n + 1) × Fin (n + 1)) ↦ x.1 < x.2) (i₂, i₁) h₂₁lt)
    (Subtype.mk (p := fun (x : Fin (n + 1) × Fin (n + 1)) ↦ x.1 < x.2) (i₄, i₃) h₄₃lt)

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
m n : ℕ
s : Simplex R P m
e : Fin (m + 1) ≃ Fin (n + 1)
⊢ LeftInverse
    (fun (y : { y : Fin (n + 1) × Fin (n + 1) // y.1 < y.2 }) ↦
      if h :
          LT.lt (α := Fin (m + 1))
            ((e.symm : (a : Fin (n + 1)) → Fin (m + 1)) (↑y : Fin (n + 1) × Fin (n + 1)).1 : Fin (m + 1))
            ((e.symm : (a : Fin (n + 1)) → Fin (m + 1)) (↑y : Fin (n + 1) × Fin (n + 1)).2 : Fin (m + 1)) then
        Subtype.mk (p := fun (x : Fin (m + 1) × Fin (m + 1)) ↦ x.1 < x.2)
          ((e.symm : (a : Fin (n + 1)) → Fin (m + 1)) (↑y : Fin (n + 1) × Fin (n + 1)).1,
            (e.symm : (a : Fin (n + 1)) → Fin (m + 1)) (↑y : Fin (n + 1) × Fin (n + 1)).2)
          h
      else
        Subtype.mk (p := fun (x : Fin (m + 1) × Fin (m + 1)) ↦ x.1 < x.2)
          ((e.symm : (a : Fin (n + 1)) → Fin (m + 1)) (↑y : Fin (n + 1) × Fin (n + 1)).2,
            (e.symm : (a : Fin (n + 1)) → Fin (m + 1)) (↑y : Fin (n + 1) × Fin (n + 1)).1)
          ⋯)
    fun (x : { x : Fin (m + 1) × Fin (m + 1) // x.1 < x.2 }) ↦
    if h :
        LT.lt (α := Fin (n + 1))
          ((e : (a : Fin (m + 1)) → Fin (n + 1)) (↑x : Fin (m + 1) × Fin (m + 1)).1 : Fin (n + 1))
          ((e : (a : Fin (m + 1)) → Fin (n + 1)) (↑x : Fin (m + 1) × Fin (m + 1)).2 : Fin (n + 1)) then
      Subtype.mk (p := fun (y : Fin (n + 1) × Fin (n + 1)) ↦ y.1 < y.2)
        ((e : (a : Fin (m + 1)) → Fin (n + 1)) (↑x : Fin (m + 1) × Fin (m + 1)).1,
          (e : (a : Fin (m + 1)) → Fin (n + 1)) (↑x : Fin (m + 1) × Fin (m + 1)).2)
        h
    else
      Subtype.mk (p := fun (y : Fin (n + 1) × Fin (n + 1)) ↦ y.1 < y.2)
        ((e : (a : Fin (m + 1)) → Fin (n + 1)) (↑x : Fin (m + 1) × Fin (m + 1)).2,
          (e : (a : Fin (m + 1)) → Fin (n + 1)) (↑x : Fin (m + 1) × Fin (m + 1)).1)
        ⋯

Tactic:
grind
-- 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
m n : ℕ
s : Simplex R P m
e : Fin (m + 1) ≃ Fin (n + 1)
⊢ RightInverse
    (fun (y : { y : Fin (n + 1) × Fin (n + 1) // y.1 < y.2 }) ↦
      if h :
          LT.lt (α := Fin (m + 1))
            ((e.symm : (a : Fin (n + 1)) → Fin (m + 1)) (↑y : Fin (n + 1) × Fin (n + 1)).1 : Fin (m + 1))
            ((e.symm : (a : Fin (n + 1)) → Fin (m + 1)) (↑y : Fin (n + 1) × Fin (n + 1)).2 : Fin (m + 1)) then
        Subtype.mk (p := fun (x : Fin (m + 1) × Fin (m + 1)) ↦ x.1 < x.2)
          ((e.symm : (a : Fin (n + 1)) → Fin (m + 1)) (↑y : Fin (n + 1) × Fin (n + 1)).1,
            (e.symm : (a : Fin (n + 1)) → Fin (m + 1)) (↑y : Fin (n + 1) × Fin (n + 1)).2)
          h
      else
        Subtype.mk (p := fun (x : Fin (m + 1) × Fin (m + 1)) ↦ x.1 < x.2)
          ((e.symm : (a : Fin (n + 1)) → Fin (m + 1)) (↑y : Fin (n + 1) × Fin (n + 1)).2,
            (e.symm : (a : Fin (n + 1)) → Fin (m + 1)) (↑y : Fin (n + 1) × Fin (n + 1)).1)
          ⋯)
    fun (x : { x : Fin (m + 1) × Fin (m + 1) // x.1 < x.2 }) ↦
    if h :
        LT.lt (α := Fin (n + 1))
          ((e : (a : Fin (m + 1)) → Fin (n + 1)) (↑x : Fin (m + 1) × Fin (m + 1)).1 : Fin (n + 1))
          ((e : (a : Fin (m + 1)) → Fin (n + 1)) (↑x : Fin (m + 1) × Fin (m + 1)).2 : Fin (n + 1)) then
      Subtype.mk (p := fun (y : Fin (n + 1) × Fin (n + 1)) ↦ y.1 < y.2)
        ((e : (a : Fin (m + 1)) → Fin (n + 1)) (↑x : Fin (m + 1) × Fin (m + 1)).1,
          (e : (a : Fin (m + 1)) → Fin (n + 1)) (↑x : Fin (m + 1) × Fin (m + 1)).2)
        h
    else
      Subtype.mk (p := fun (y : Fin (n + 1) × Fin (n + 1)) ↦ y.1 < y.2)
        ((e : (a : Fin (m + 1)) → Fin (n + 1)) (↑x : Fin (m + 1) × Fin (m + 1)).2,
          (e : (a : Fin (m + 1)) → Fin (n + 1)) (↑x : Fin (m + 1) × Fin (m + 1)).1)
        ⋯

Tactic:
grind