-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex (goal)
Goal:
n m : ℕ
S : Finset (Fin (n + 1))
hS : #S = m + 1
e : Fin (m + 1) ≃o ↥S := monoEquivOfFin ↥S ⋯
right :
  Membership.mem (γ := Set (Δ[n] _⦋m⦌)) (Δ[n].nonDegenerate m)
    (objMk (OrderHom.comp (OrderHom.Subtype.val fun (x : Fin (n + 1)) ↦ x ∈ S) e.toOrderEmbedding.toOrderHom))
⊢ ∃ (a : { x : Δ[n] _⦋m⦌ // Membership.mem (γ := Set (Δ[n] _⦋m⦌)) (Δ[n].nonDegenerate m) x }),
    Eq (α :=
      { x : Finset (Fin (n + 1)) //
        Membership.mem (γ := Set (Finset (Fin (n + 1)))) {S : Finset (Fin (n + 1)) | #S = m + 1} x })
      ((fun (x : { x : Δ[n] _⦋m⦌ // Membership.mem (γ := Set (Δ[n] _⦋m⦌)) (Δ[n].nonDegenerate m) x }) ↦
          (match (motive :=
              { x : Δ[n] _⦋m⦌ // Membership.mem (γ := Set (Δ[n] _⦋m⦌)) (Δ[n].nonDegenerate m) x } →
                { x : Finset (Fin (n + 1)) //
                  Membership.mem (γ := Set (Finset (Fin (n + 1)))) {S : Finset (Fin (n + 1)) | #S = m + 1} x })
              x with
            | ⟨x, hx⟩ =>
              Subtype.mk (p := fun (x : Finset (Fin (n + 1))) ↦
                Membership.mem (γ := Set (Finset (Fin (n + 1)))) {S : Finset (Fin (n + 1)) | #S = m + 1} x)
                (Finset.image (α := Fin ((unop (op ⦋m⦌)).len + 1))
                  (⇑(Hom.toOrderHom
                        (((objEquiv : Δ[n] _⦋m⦌ ≃ (unop (op ⦋m⦌) ⟶ ⦋n⦌)) : (a : Δ[n] _⦋m⦌) → unop (op ⦋m⦌) ⟶ ⦋n⦌) x)) :
                    (a : Fin ((unop (op ⦋m⦌)).len + 1)) → Fin (⦋n⦌.len + 1))
                  univ)
                ⋯ :
            { x : Finset (Fin (n + 1)) //
              Membership.mem (γ := Set (Finset (Fin (n + 1)))) {S : Finset (Fin (n + 1)) | #S = m + 1} x }))
        a)
      (Subtype.mk (p := fun (x : Finset (Fin (n + 1))) ↦
        Membership.mem (γ := Set (Finset (Fin (n + 1)))) {S : Finset (Fin (n + 1)) | #S = m + 1} x) S hS)
have right₁ : Eq (α :=
  { x : Finset (Fin (n + 1)) //
    Membership.mem (γ := Set (Finset (Fin (n + 1)))) {S : Finset (Fin (n + 1)) | #S = m + 1} x })
  ((fun (x : { x : Δ[n] _⦋m⦌ // Membership.mem (γ := Set (Δ[n] _⦋m⦌)) (Δ[n].nonDegenerate m) x }) ↦
      (match (motive :=
          { x : Δ[n] _⦋m⦌ // Membership.mem (γ := Set (Δ[n] _⦋m⦌)) (Δ[n].nonDegenerate m) x } →
            { x : Finset (Fin (n + 1)) //
              Membership.mem (γ := Set (Finset (Fin (n + 1)))) {S : Finset (Fin (n + 1)) | #S = m + 1} x })
          x with
        | ⟨x, hx⟩ =>
          Subtype.mk (p := fun (x : Finset (Fin (n + 1))) ↦
            Membership.mem (γ := Set (Finset (Fin (n + 1)))) {S : Finset (Fin (n + 1)) | #S = m + 1} x)
            (Finset.image (α := Fin ((unop (op ⦋m⦌)).len + 1))
              (⇑(Hom.toOrderHom
                    (((objEquiv : Δ[n] _⦋m⦌ ≃ (unop (op ⦋m⦌) ⟶ ⦋n⦌)) : (a : Δ[n] _⦋m⦌) → unop (op ⦋m⦌) ⟶ ⦋n⦌) x)) :
                (a : Fin ((unop (op ⦋m⦌)).len + 1)) → Fin (⦋n⦌.len + 1))
              univ)
            sorry :
        { x : Finset (Fin (n + 1)) //
          Membership.mem (γ := Set (Finset (Fin (n + 1)))) {S : Finset (Fin (n + 1)) | #S = m + 1} x }))
    (Subtype.mk (p := fun (x : Δ[n] _⦋m⦌) ↦ Membership.mem (γ := Set (Δ[n] _⦋m⦌)) (Δ[n].nonDegenerate m) x)
      (objMk (OrderHom.comp (OrderHom.Subtype.val fun (x : Fin (n + 1)) ↦ x ∈ S) e.toOrderEmbedding.toOrderHom)) sorry))
  (Subtype.mk (p := fun (x : Finset (Fin (n + 1))) ↦
    Membership.mem (γ := Set (Finset (Fin (n + 1)))) {S : Finset (Fin (n + 1)) | #S = m + 1} x) S hS)
Tactic: refine ⟨⟨objMk ((OrderHom.Subtype.val _).comp e.toOrderEmbedding.toOrderHom), ?_⟩, ?_⟩