-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
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
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))))
              ⋯ :
            { 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)
                          ⋯),
                    monotone' := ⋯ } :
              ⦋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
⊢ (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

Tactic:
induction j using SimplexCategory.rec with | _ j