-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex (goal)
Goal:
n : ℕ
S : Finset (Fin (n + 1))
m : ℕ
e : Fin (m + 1) ≃o ↥S
j : SimplexCategory
f : j ⟶ ⦋m⦌
⊢ (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
have 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)
                              sorry),
                        monotone' := sorry } :
                  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))))
                      sorry :
                    { 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))
Tactic: ext i : 3