∀ {n : ℕ} (S : Finset (Fin (n + 1))) (m : ℕ) (e : Fin (m + 1) ≃o ↥S) {j : SimplexCategory}
  (x : (SSet.stdSimplex.face S).toSSet.obj (Opposite.op j))
  (x : (SSet.stdSimplex.obj (SimplexCategory.mk n)).obj (Opposite.op j))
  (hx : x ∈ (SSet.stdSimplex.face S).obj (Opposite.op j)),
  (fun f =>
        ⟨SSet.stdSimplex.objMk
            ((OrderHom.Subtype.val ↑S).comp (e.toOrderEmbedding.toOrderHom.comp (SimplexCategory.Hom.toOrderHom f))),
          ⋯⟩)
      ((fun x =>
          match x with
          | ⟨x, hx⟩ =>
            SimplexCategory.Hom.mk
              { toFun := fun i => e.symm ⟨(SimplexCategory.Hom.toOrderHom (SSet.stdSimplex.objEquiv x)) i, ⋯⟩,
                monotone' := ⋯ })
        ⟨x, hx⟩) =
    ⟨x, hx⟩