-- 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)
f : { x : Fin (m + 1) × Fin (m + 1) // x.1 < x.2 } ≃ { y : Fin (n + 1) × Fin (n + 1) // y.1 < y.2 } :=
  {
    toFun := 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)
          ⋯,
    invFun := 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)
          ⋯,
    left_inv := ⋯, right_inv := ⋯ }
x : { x : Fin (m + 1) × Fin (m + 1) // x.1 < x.2 }
h :
  ∀
    (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))),
    dist (s.points (↑x : Fin (m + 1) × Fin (m + 1)).1) (s.points (↑x : Fin (m + 1) × Fin (m + 1)).2) =
      dist
        (s.points
          ((e.symm : (a : Fin (n + 1)) → Fin (m + 1))
            (↑(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) :
                Fin (n + 1) × Fin (n + 1)).1))
        (s.points
          ((e.symm : (a : Fin (n + 1)) → Fin (m + 1))
            (↑(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) :
                Fin (n + 1) × Fin (n + 1)).2))
h₁ :
  ∀
    (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))),
    dist (s.points (↑x : Fin (m + 1) × Fin (m + 1)).1) (s.points (↑x : Fin (m + 1) × Fin (m + 1)).2) =
      dist
        (s.points
          ((e.symm : (a : Fin (n + 1)) → Fin (m + 1))
            (↑(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)
                    ⋯) :
                Fin (n + 1) × Fin (n + 1)).1))
        (s.points
          ((e.symm : (a : Fin (n + 1)) → Fin (m + 1))
            (↑(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)
                    ⋯) :
                Fin (n + 1) × Fin (n + 1)).2))
⊢ dist (s.points (↑x : Fin (m + 1) × Fin (m + 1)).1) (s.points (↑x : Fin (m + 1) × Fin (m + 1)).2) =
    dist
      (s.points
        ((e.symm : (a : Fin (n + 1)) → Fin (m + 1))
          (↑(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)
                    ⋯) :
              Fin (n + 1) × Fin (n + 1)).1))
      (s.points
        ((e.symm : (a : Fin (n + 1)) → Fin (m + 1))
          (↑(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)
                    ⋯) :
              Fin (n + 1) × Fin (n + 1)).2))

Tactic:
split