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

Tactic:
simp [h, lt_asymm] at h₃

Result:
no goals

Proof state:
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⟩

Tactic:
simp

Result:
no goals

Proof state:
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 (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), ⋯⟩).1, e.symm (↑⟨(e i, e j), ⋯⟩).2), ⋯⟩ = ⟨(i, j), h⟩

Tactic:
simp

Result:
no goals

Proof state:
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⟩

Tactic:
simp [h, lt_asymm] at h₃

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)
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)

Tactic:
convert (Injective.of_comp_iff' _ (Equiv.bijective f)).symm

Result:
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) =
    ((fun i => dist ((s.reindex e).points (↑i).1) ((s.reindex e).points (↑i).2)) ∘ ⇑f) x✝

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)
⊢ ∀ (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⟩

Tactic:
intro i j h

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)
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⟩

Proof state:
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))

Tactic:
simp

Result:
no goals

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)
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))

Tactic:
simp [dist_comm]

Result:
no goals