-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n : ℕ
S : Finset (Fin (n + 1))
m : ℕ
e : Fin (m + 1) ≃o ↥S
j : SimplexCategory
f : j ⟶ ⦋m⦌
a :
  ∀ (i : Fin (j.len + 1)),
    Eq (α := Fin (⦋m⦌.len + 1))
      ((Hom.toOrderHom
              ((fun (x : (face S).toSSet.obj (op j)) ↦
                  (match (motive := (face S).toSSet.obj (op j) → (j ⟶ ⦋m⦌)) x with
                    | ⟨x, hx⟩ =>
                      Hom.mk
                        {
                          toFun := fun (i : Fin (j.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 j) ≃ (unop (op j) ⟶ ⦋n⦌)) :
                                          (a : Δ[n].obj (op j)) → unop (op j) ⟶ ⦋n⦌)
                                        x) :
                                    (a : Fin ((unop (op j)).len + 1)) → Fin (⦋n⦌.len + 1))
                                  i)
                                ⋯),
                          monotone' := ⋯ } :
                    j ⟶ ⦋m⦌))
                ((fun (f : j ⟶ ⦋m⦌) ↦
                    (Subtype.mk (p := fun (x : Δ[n].obj (op j)) ↦
                        Membership.mem (γ := Set (Δ[n].obj (op j))) ((face S).obj (op j)) x)
                        (objMk
                          (OrderHom.comp (OrderHom.Subtype.val fun (x : Fin (n + 1)) ↦ x ∈ S)
                            (e.toOrderEmbedding.toOrderHom.comp (Hom.toOrderHom f))))
                        ⋯ :
                      { x : Δ[n].obj (op j) // Membership.mem (γ := Set (Δ[n].obj (op j))) ((face S).obj (op j)) x }))
                  f)) :
            (a : Fin (j.len + 1)) → Fin (⦋m⦌.len + 1))
          i :
        Fin (⦋m⦌.len + 1))
      ((Hom.toOrderHom f : (a : Fin (j.len + 1)) → Fin (⦋m⦌.len + 1)) i : Fin (⦋m⦌.len + 1))
⊢ (fun (x : (face S).toSSet.obj (op j)) ↦
        (match (motive := (face S).toSSet.obj (op j) → (j ⟶ ⦋m⦌)) x with
          | ⟨x, hx⟩ =>
            Hom.mk
              {
                toFun := fun (i : Fin (j.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 j) ≃ (unop (op j) ⟶ ⦋n⦌)) :
                                (a : Δ[n].obj (op j)) → unop (op j) ⟶ ⦋n⦌)
                              x) :
                          (a : Fin ((unop (op j)).len + 1)) → Fin (⦋n⦌.len + 1))
                        i)
                      ⋯),
                monotone' := ⋯ } :
          j ⟶ ⦋m⦌))
      ((fun (f : j ⟶ ⦋m⦌) ↦
          (Subtype.mk (p := fun (x : Δ[n].obj (op j)) ↦
              Membership.mem (γ := Set (Δ[n].obj (op j))) ((face S).obj (op j)) x)
              (objMk
                (OrderHom.comp (OrderHom.Subtype.val fun (x : Fin (n + 1)) ↦ x ∈ S)
                  (e.toOrderEmbedding.toOrderHom.comp (Hom.toOrderHom f))))
              ⋯ :
            { x : Δ[n].obj (op j) // Membership.mem (γ := Set (Δ[n].obj (op j))) ((face S).obj (op j)) x }))
        f) =
    f

Tactic:
ext i : 3