-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n : ℕ
S : Finset (Fin (n + 1))
m : ℕ
e : Fin (m + 1) ≃o ↥S
X X' : SimplexCategory
f : X ⟶ X'
g : X' ⟶ ⦋m⦌
⊢ Eq.{u + 1} (α := (face S).toSSet.obj (op X))
    (({
            toFun := fun (f : X ⟶ ⦋m⦌) ↦
              Subtype.mk (p := fun (x : Δ[n].obj (op X)) ↦
                Membership.mem (γ := Set (Δ[n].obj (op X))) ((face S).obj (op X)) x)
                (objMk
                  (OrderHom.comp (OrderHom.Subtype.val fun (x : Fin (n + 1)) ↦ x ∈ S)
                    (e.toOrderEmbedding.toOrderHom.comp (Hom.toOrderHom f))))
                ⋯,
            invFun := fun (x : (face S).toSSet.obj (op X)) ↦
              match (motive := (face S).toSSet.obj (op X) → (X ⟶ ⦋m⦌)) x with
              | ⟨x, hx⟩ =>
                Hom.mk
                  {
                    toFun := fun (i : Fin (X.len + 1)) ↦
                      (e.symm : (a : ↥S) → Fin (m + 1))
                        (Subtype.mk (p := fun (x : Fin (n + 1)) ↦ x ∈ S)
                          ((Hom.toOrderHom
                                (((objEquiv : Δ[n].obj (op X) ≃ (unop (op X) ⟶ ⦋n⦌)) :
                                    (a : Δ[n].obj (op X)) → unop (op X) ⟶ ⦋n⦌)
                                  x) :
                              (a : Fin ((unop (op X)).len + 1)) → Fin (⦋n⦌.len + 1))
                            i)
                          ⋯),
                    monotone' := ⋯ },
            left_inv := ⋯, right_inv := ⋯ } :
          (a : X ⟶ ⦋m⦌) → (face S).toSSet.obj (op X))
        (f ≫ g) :
      (face S).toSSet.obj (op X))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((face S).toSSet.map f.op) :
          (a : (fun (X : Type u) ↦ X) ((face S).toSSet.obj (op X'))) →
            (fun (X : Type u) ↦ X) ((face S).toSSet.obj (op X)))
        (({
              toFun := fun (f : X' ⟶ ⦋m⦌) ↦
                Subtype.mk (p := fun (x : Δ[n].obj (op X')) ↦
                  Membership.mem (γ := Set (Δ[n].obj (op X'))) ((face S).obj (op X')) x)
                  (objMk
                    (OrderHom.comp (OrderHom.Subtype.val fun (x : Fin (n + 1)) ↦ x ∈ S)
                      (e.toOrderEmbedding.toOrderHom.comp (Hom.toOrderHom f))))
                  ⋯,
              invFun := fun (x : (face S).toSSet.obj (op X')) ↦
                match (motive := (face S).toSSet.obj (op X') → (X' ⟶ ⦋m⦌)) x with
                | ⟨x, hx⟩ =>
                  Hom.mk
                    {
                      toFun := fun (i : Fin (X'.len + 1)) ↦
                        (e.symm : (a : ↥S) → Fin (m + 1))
                          (Subtype.mk (p := fun (x : Fin (n + 1)) ↦ x ∈ S)
                            ((Hom.toOrderHom
                                  (((objEquiv : Δ[n].obj (op X') ≃ (unop (op X') ⟶ ⦋n⦌)) :
                                      (a : Δ[n].obj (op X')) → unop (op X') ⟶ ⦋n⦌)
                                    x) :
                                (a : Fin ((unop (op X')).len + 1)) → Fin (⦋n⦌.len + 1))
                              i)
                            ⋯),
                      monotone' := ⋯ },
              left_inv := ⋯, right_inv := ⋯ } :
            (a : X' ⟶ ⦋m⦌) → (face S).toSSet.obj (op X'))
          g) :
      (fun (X : Type u) ↦ X) ((face S).toSSet.obj (op X)))

Tactic:
aesop