-- 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
x_1 : (face S).toSSet.obj (op j)
x : Δ[n].obj (op j)
hx : Membership.mem (γ := Set (Δ[n].obj (op j))) ((face S).obj (op j)) x
⊢ (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 }))
      ((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⦌))
        (Subtype.mk (p := fun (x : Δ[n].obj (op j)) ↦
          Membership.mem (γ := Set (Δ[n].obj (op j))) ((face S).obj (op j)) x) x hx)) =
    Subtype.mk (p := fun (x : Δ[n].obj (op j)) ↦ Membership.mem (γ := Set (Δ[n].obj (op j))) ((face S).obj (op j)) x) x
      hx
have mk : ∀ (j : ℕ) (x : (face S).toSSet _⦋j⦌) (x : Δ[n] _⦋j⦌)
  (hx : Membership.mem (γ := Set (Δ[n] _⦋j⦌)) ((face S).obj (op ⦋j⦌)) x),
  (fun (f : ⦋j⦌ ⟶ ⦋m⦌) ↦
        (Subtype.mk (p := fun (x : Δ[n] _⦋j⦌) ↦ Membership.mem (γ := Set (Δ[n] _⦋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] _⦋j⦌ // Membership.mem (γ := Set (Δ[n] _⦋j⦌)) ((face S).obj (op ⦋j⦌)) x }))
      ((fun (x : (face S).toSSet _⦋j⦌) ↦
          (match (motive := (face S).toSSet _⦋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] _⦋j⦌ ≃ (unop (op ⦋j⦌) ⟶ ⦋n⦌)) : (a : Δ[n] _⦋j⦌) → unop (op ⦋j⦌) ⟶ ⦋n⦌)
                                x) :
                            (a : Fin ((unop (op ⦋j⦌)).len + 1)) → Fin (⦋n⦌.len + 1))
                          i)
                        sorry),
                  monotone' := sorry } :
            ⦋j⦌ ⟶ ⦋m⦌))
        (Subtype.mk (p := fun (x : Δ[n] _⦋j⦌) ↦ Membership.mem (γ := Set (Δ[n] _⦋j⦌)) ((face S).obj (op ⦋j⦌)) x) x
          hx)) =
    Subtype.mk (p := fun (x : Δ[n] _⦋j⦌) ↦ Membership.mem (γ := Set (Δ[n] _⦋j⦌)) ((face S).obj (op ⦋j⦌)) x) x hx
Tactic: induction j using SimplexCategory.rec with | _ j
Cleared hypotheses: j, x_1, x, hx