-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex (goal)
Goal:
n m : ℕ
left :
  Function.Injective (β :=
    { 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)
        ⋯
⊢ Function.Bijective (β :=
    { 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)
        ⋯
have right : Function.Surjective (β :=
  { x : Finset (Fin (n + 1)) //
    Membership.mem (γ := Set (Finset (Fin (n + 1)))) {S : Finset (Fin (n + 1)) | #S = m + 1} x })
  fun
    (x :
      { x : @Functor.obj SimplexCategory smallCategory SSet Functor.category stdSimplex ⦋n⦌ _⦋m⦌ //
        Membership.mem (γ := Set (@Functor.obj SimplexCategory smallCategory SSet Functor.category stdSimplex ⦋n⦌ _⦋m⦌))
          (nonDegenerate (@Functor.obj SimplexCategory smallCategory SSet Functor.category stdSimplex ⦋n⦌) m) x }) ↦
  match (motive :=
    { x : @Functor.obj SimplexCategory smallCategory SSet Functor.category stdSimplex ⦋n⦌ _⦋m⦌ //
        Membership.mem (γ := Set (@Functor.obj SimplexCategory smallCategory SSet Functor.category stdSimplex ⦋n⦌ _⦋m⦌))
          (nonDegenerate (@Functor.obj SimplexCategory smallCategory SSet Functor.category stdSimplex ⦋n⦌) 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
Tactic: constructor