-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.Simplex (goal)
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 }
⊢ 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
have 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)
                  sorry) :
            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)
                  sorry) :
            Fin (n + 1) × Fin (n + 1)).2))
Tactic: simp only [reindex_points, comp_apply, Equiv.coe_fn_mk, f]