-- Mathlib/Analysis/Normed/Affine/Simplex.lean
@[simp] lemma scalene_reindex_iff {s : Simplex R P m} (e : Fin (m + 1) ≃ Fin (n + 1)) :
    (s.reindex e).Scalene ↔ s.Scalene

Proof state:
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring R
inst✝³ : SeminormedAddCommGroup V
inst✝² : PseudoMetricSpace P
inst✝¹ : Module R V
inst✝ : NormedAddTorsor V P
m n : ℕ
s : Simplex R P m
e : Fin (m + 1) ≃ Fin (n + 1)
f : { x // x.1 < x.2 } ≃ { y // y.1 < y.2 } :=
  { toFun := fun x => if h : e (↑x).1 < e (↑x).2 then ⟨(e (↑x).1, e (↑x).2), h⟩ else ⟨(e (↑x).2, e (↑x).1), ⋯⟩,
    invFun := fun y =>
      if h : e.symm (↑y).1 < e.symm (↑y).2 then ⟨(e.symm (↑y).1, e.symm (↑y).2), h⟩
      else ⟨(e.symm (↑y).2, e.symm (↑y).1), ⋯⟩,
    left_inv := ⋯, right_inv := ⋯ }
⊢ (s.reindex e).Scalene ↔ s.Scalene

Tactic:
simp_rw [Scalene]

Result:
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring R
inst✝³ : SeminormedAddCommGroup V
inst✝² : PseudoMetricSpace P
inst✝¹ : Module R V
inst✝ : NormedAddTorsor V P
m n : ℕ
s : Simplex R P m
e : Fin (m + 1) ≃ Fin (n + 1)
f : { x // x.1 < x.2 } ≃ { y // y.1 < y.2 } :=
  { toFun := fun x => if h : e (↑x).1 < e (↑x).2 then ⟨(e (↑x).1, e (↑x).2), h⟩ else ⟨(e (↑x).2, e (↑x).1), ⋯⟩,
    invFun := fun y =>
      if h : e.symm (↑y).1 < e.symm (↑y).2 then ⟨(e.symm (↑y).1, e.symm (↑y).2), h⟩
      else ⟨(e.symm (↑y).2, e.symm (↑y).1), ⋯⟩,
    left_inv := ⋯, right_inv := ⋯ }
⊢ (Injective fun i => dist ((s.reindex e).points (↑i).1) ((s.reindex e).points (↑i).2)) ↔
    Injective fun i => dist (s.points (↑i).1) (s.points (↑i).2)

Proof state:
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring R
inst✝³ : SeminormedAddCommGroup V
inst✝² : PseudoMetricSpace P
inst✝¹ : Module R V
inst✝ : NormedAddTorsor V P
m n : ℕ
s : Simplex R P m
e : Fin (m + 1) ≃ Fin (n + 1)
⊢ RightInverse
    (fun y =>
      if h : e.symm (↑y).1 < e.symm (↑y).2 then ⟨(e.symm (↑y).1, e.symm (↑y).2), h⟩
      else ⟨(e.symm (↑y).2, e.symm (↑y).1), ⋯⟩)
    fun x => if h : e (↑x).1 < e (↑x).2 then ⟨(e (↑x).1, e (↑x).2), h⟩ else ⟨(e (↑x).2, e (↑x).1), ⋯⟩

Tactic:
simp only [RightInverse, LeftInverse, Subtype.forall, Prod.forall]

Result:
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring R
inst✝³ : SeminormedAddCommGroup V
inst✝² : PseudoMetricSpace P
inst✝¹ : Module R V
inst✝ : NormedAddTorsor V P
m n : ℕ
s : Simplex R P m
e : Fin (m + 1) ≃ Fin (n + 1)
⊢ ∀ (a b : Fin (n + 1)) (b_1 : a < b),
    (if h :
          e (↑(if h : e.symm a < e.symm b then ⟨(e.symm a, e.symm b), ⋯⟩ else ⟨(e.symm b, e.symm a), ⋯⟩)).1 <
            e (↑(if h : e.symm a < e.symm b then ⟨(e.symm a, e.symm b), ⋯⟩ else ⟨(e.symm b, e.symm a), ⋯⟩)).2 then
        ⟨(e (↑(if h : e.symm a < e.symm b then ⟨(e.symm a, e.symm b), ⋯⟩ else ⟨(e.symm b, e.symm a), ⋯⟩)).1,
            e (↑(if h : e.symm a < e.symm b then ⟨(e.symm a, e.symm b), ⋯⟩ else ⟨(e.symm b, e.symm a), ⋯⟩)).2),
          ⋯⟩
      else
        ⟨(e (↑(if h : e.symm a < e.symm b then ⟨(e.symm a, e.symm b), ⋯⟩ else ⟨(e.symm b, e.symm a), ⋯⟩)).2,
            e (↑(if h : e.symm a < e.symm b then ⟨(e.symm a, e.symm b), ⋯⟩ else ⟨(e.symm b, e.symm a), ⋯⟩)).1),
          ⋯⟩) =
      ⟨(a, b), b_1⟩

Proof state:
case neg
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring R
inst✝³ : SeminormedAddCommGroup V
inst✝² : PseudoMetricSpace P
inst✝¹ : Module R V
inst✝ : NormedAddTorsor V P
m n : ℕ
s : Simplex R P m
e : Fin (m + 1) ≃ Fin (n + 1)
i j : Fin (m + 1)
h : i < j
h₁ : e i < e j
h₂ : ¬e.symm (↑⟨(e i, e j), ⋯⟩).1 < e.symm (↑⟨(e i, e j), ⋯⟩).2
⊢ ⟨(e.symm (↑⟨(e i, e j), ⋯⟩).2, e.symm (↑⟨(e i, e j), ⋯⟩).1), ⋯⟩ = ⟨(i, j), h⟩

Tactic:
simp [h] at h₂

Result:
no goals