-- 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)
⊢ LeftInverse
    (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 [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 (m + 1)) (b_1 : a < b),
    (if h :
          e.symm (↑(if h : e a < e b then ⟨(e a, e b), ⋯⟩ else ⟨(e b, e a), ⋯⟩)).1 <
            e.symm (↑(if h : e a < e b then ⟨(e a, e b), ⋯⟩ else ⟨(e b, e a), ⋯⟩)).2 then
        ⟨(e.symm (↑(if h : e a < e b then ⟨(e a, e b), ⋯⟩ else ⟨(e b, e a), ⋯⟩)).1,
            e.symm (↑(if h : e a < e b then ⟨(e a, e b), ⋯⟩ else ⟨(e b, e a), ⋯⟩)).2),
          ⋯⟩
      else
        ⟨(e.symm (↑(if h : e a < e b then ⟨(e a, e b), ⋯⟩ else ⟨(e b, e a), ⋯⟩)).2,
            e.symm (↑(if h : e a < e b then ⟨(e a, e b), ⋯⟩ else ⟨(e b, e 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 j, e i), ⋯⟩).1 < e.symm (↑⟨(e j, e i), ⋯⟩).2
⊢ ⟨(e.symm (↑⟨(e j, e i), ⋯⟩).2, e.symm (↑⟨(e j, e i), ⋯⟩).1), ⋯⟩ = ⟨(i, j), h⟩

Tactic:
simp

Result:
no goals

Proof state:
case h.e'_2.h.e'_3.h
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 := ⋯ }
x✝ : { x // x.1 < x.2 }
⊢ dist (s.points (↑x✝).1) (s.points (↑x✝).2) =
    dist
      (s.points
        (e.symm (↑(if h : e (↑x✝).1 < e (↑x✝).2 then ⟨(e (↑x✝).1, e (↑x✝).2), h⟩ else ⟨(e (↑x✝).2, e (↑x✝).1), ⋯⟩)).1))
      (s.points
        (e.symm (↑(if h : e (↑x✝).1 < e (↑x✝).2 then ⟨(e (↑x✝).1, e (↑x✝).2), h⟩ else ⟨(e (↑x✝).2, e (↑x✝).1), ⋯⟩)).2))

Tactic:
split_ifs with h

Result:
case pos
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 := ⋯ }
x✝ : { x // x.1 < x.2 }
h : e (↑x✝).1 < e (↑x✝).2
⊢ dist (s.points (↑x✝).1) (s.points (↑x✝).2) =
    dist (s.points (e.symm (↑⟨(e (↑x✝).1, e (↑x✝).2), h⟩).1)) (s.points (e.symm (↑⟨(e (↑x✝).1, e (↑x✝).2), h⟩).2))

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)
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 := ⋯ }
x✝ : { x // x.1 < x.2 }
h : ¬e (↑x✝).1 < e (↑x✝).2
⊢ dist (s.points (↑x✝).1) (s.points (↑x✝).2) =
    dist (s.points (e.symm (↑⟨(e (↑x✝).2, e (↑x✝).1), ⋯⟩).1)) (s.points (e.symm (↑⟨(e (↑x✝).2, e (↑x✝).1), ⋯⟩).2))

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 (n + 1)
h : i < j
h₁ : ¬e.symm i < e.symm j
h₃ : ¬e (↑⟨(e.symm j, e.symm i), ⋯⟩).1 < e (↑⟨(e.symm j, e.symm i), ⋯⟩).2
⊢ ⟨(e (↑⟨(e.symm j, e.symm i), ⋯⟩).2, e (↑⟨(e.symm j, e.symm i), ⋯⟩).1), ⋯⟩ = ⟨(i, j), h⟩

Tactic:
simp

Result:
no goals

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)
i j : Fin (n + 1)
h : i < j
⊢ (if h_1 :
        e (↑(if h : e.symm i < e.symm j then ⟨(e.symm i, e.symm j), ⋯⟩ else ⟨(e.symm j, e.symm i), ⋯⟩)).1 <
          e (↑(if h : e.symm i < e.symm j then ⟨(e.symm i, e.symm j), ⋯⟩ else ⟨(e.symm j, e.symm i), ⋯⟩)).2 then
      ⟨(e (↑(if h_2 : e.symm i < e.symm j then ⟨(e.symm i, e.symm j), ⋯⟩ else ⟨(e.symm j, e.symm i), ⋯⟩)).1,
          e (↑(if h_2 : e.symm i < e.symm j then ⟨(e.symm i, e.symm j), ⋯⟩ else ⟨(e.symm j, e.symm i), ⋯⟩)).2),
        ⋯⟩
    else
      ⟨(e (↑(if h_2 : e.symm i < e.symm j then ⟨(e.symm i, e.symm j), ⋯⟩ else ⟨(e.symm j, e.symm i), ⋯⟩)).2,
          e (↑(if h_2 : e.symm i < e.symm j then ⟨(e.symm i, e.symm j), ⋯⟩ else ⟨(e.symm j, e.symm i), ⋯⟩)).1),
        ⋯⟩) =
    ⟨(i, j), h⟩

Tactic:
split_ifs with h₁ h₂ h₃

Result:
case pos
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 (n + 1)
h : i < j
h₁ : e.symm i < e.symm j
h₂ : e (↑⟨(e.symm i, e.symm j), ⋯⟩).1 < e (↑⟨(e.symm i, e.symm j), ⋯⟩).2
⊢ ⟨(e (↑⟨(e.symm i, e.symm j), ⋯⟩).1, e (↑⟨(e.symm i, e.symm j), ⋯⟩).2), ⋯⟩ = ⟨(i, j), h⟩

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 (n + 1)
h : i < j
h₁ : e.symm i < e.symm j
h₂ : ¬e (↑⟨(e.symm i, e.symm j), ⋯⟩).1 < e (↑⟨(e.symm i, e.symm j), ⋯⟩).2
⊢ ⟨(e (↑⟨(e.symm i, e.symm j), ⋯⟩).2, e (↑⟨(e.symm i, e.symm j), ⋯⟩).1), ⋯⟩ = ⟨(i, j), h⟩

case pos
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 (n + 1)
h : i < j
h₁ : ¬e.symm i < e.symm j
h₃ : e (↑⟨(e.symm j, e.symm i), ⋯⟩).1 < e (↑⟨(e.symm j, e.symm i), ⋯⟩).2
⊢ ⟨(e (↑⟨(e.symm j, e.symm i), ⋯⟩).1, e (↑⟨(e.symm j, e.symm i), ⋯⟩).2), ⋯⟩ = ⟨(i, j), h⟩

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 (n + 1)
h : i < j
h₁ : ¬e.symm i < e.symm j
h₃ : ¬e (↑⟨(e.symm j, e.symm i), ⋯⟩).1 < e (↑⟨(e.symm j, e.symm i), ⋯⟩).2
⊢ ⟨(e (↑⟨(e.symm j, e.symm i), ⋯⟩).2, e (↑⟨(e.symm j, e.symm i), ⋯⟩).1), ⋯⟩ = ⟨(i, j), h⟩