-- 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 := ⋯ }
h :
  ∀ (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
⊢ (Injective (β := ℝ) 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)) ↔
    Injective (β := ℝ) fun (i : { x : Fin (m + 1) × Fin (m + 1) // x.1 < x.2 }) ↦
      dist (s.points (↑i : Fin (m + 1) × Fin (m + 1)).1) (s.points (↑i : Fin (m + 1) × Fin (m + 1)).2)

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

Premises used: Equiv.bijective, Function.Injective.of_comp_iff', Iff.symm