-- 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 :
  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))
⊢ dist (s.points (↑x : Fin (m + 1) × Fin (m + 1)).1) (s.points (↑x : Fin (m + 1) × Fin (m + 1)).2) =
    ((fun (i : { x : Fin (n + 1) × Fin (n + 1) // x.1 < x.2 }) ↦
          dist ((s.reindex e).points (↑i : Fin (n + 1) × Fin (n + 1)).1)
            ((s.reindex e).points (↑i : Fin (n + 1) × Fin (n + 1)).2)) ∘
        (⇑f : (a : { x : Fin (m + 1) × Fin (m + 1) // x.1 < x.2 }) → { y : Fin (n + 1) × Fin (n + 1) // y.1 < y.2 }))
      x

Tactic:
simp only [reindex_points, comp_apply, Equiv.coe_fn_mk, f]

Premises used: Affine.Simplex.reindex_points, Equiv.coe_fn_mk, Function.comp_apply