-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n m : ℕ
x₂ : Δ[n] _⦋m⦌
h₂ : Membership.mem (γ := Set (Δ[n] _⦋m⦌)) (Δ[n].nonDegenerate m) x₂
f₁ : unop (op ⦋m⦌) ⟶ ⦋n⦌
h₁ :
  Membership.mem.{u, u} (α := Δ[n] _⦋m⦌) (γ := Set (Δ[n] _⦋m⦌)) (Δ[n].nonDegenerate m)
    ((Equiv.symm objEquiv : (a : unop (op ⦋m⦌) ⟶ ⦋n⦌) → Δ[n] _⦋m⦌) f₁ : Δ[n] _⦋m⦌)
h₃ :
  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 }))
      (Subtype.mk (p := fun (x : Δ[n] _⦋m⦌) ↦ Membership.mem (γ := Set (Δ[n] _⦋m⦌)) (Δ[n].nonDegenerate m) x)
        ((Equiv.symm objEquiv : (a : unop (op ⦋m⦌) ⟶ ⦋n⦌) → Δ[n] _⦋m⦌) f₁) h₁))
    ((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 }))
      (Subtype.mk (p := fun (x : Δ[n] _⦋m⦌) ↦ Membership.mem (γ := Set (Δ[n] _⦋m⦌)) (Δ[n].nonDegenerate m) x) x₂ h₂))
left :
  ∀ (f₂ : unop (op ⦋m⦌) ⟶ ⦋n⦌)
    (h₂ :
      Membership.mem.{u, u} (α := Δ[n] _⦋m⦌) (γ := Set (Δ[n] _⦋m⦌)) (Δ[n].nonDegenerate m)
        ((Equiv.symm objEquiv : (a : unop (op ⦋m⦌) ⟶ ⦋n⦌) → Δ[n] _⦋m⦌) f₂ : Δ[n] _⦋m⦌))
    (h₃ :
      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 }))
          (Subtype.mk (p := fun (x : Δ[n] _⦋m⦌) ↦ Membership.mem (γ := Set (Δ[n] _⦋m⦌)) (Δ[n].nonDegenerate m) x)
            ((Equiv.symm objEquiv : (a : unop (op ⦋m⦌) ⟶ ⦋n⦌) → Δ[n] _⦋m⦌) f₁) h₁))
        ((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 }))
          (Subtype.mk (p := fun (x : Δ[n] _⦋m⦌) ↦ Membership.mem (γ := Set (Δ[n] _⦋m⦌)) (Δ[n].nonDegenerate m) x)
            ((Equiv.symm objEquiv : (a : unop (op ⦋m⦌) ⟶ ⦋n⦌) → Δ[n] _⦋m⦌) f₂) h₂))),
    Eq.{u + 1} (α := { x : Δ[n] _⦋m⦌ // Membership.mem (γ := Set (Δ[n] _⦋m⦌)) (Δ[n].nonDegenerate m) x })
      (Subtype.mk (p := fun (x : Δ[n] _⦋m⦌) ↦ Membership.mem (γ := Set (Δ[n] _⦋m⦌)) (Δ[n].nonDegenerate m) x)
          ((Equiv.symm objEquiv : (a : unop (op ⦋m⦌) ⟶ ⦋n⦌) → Δ[n] _⦋m⦌) f₁) h₁ :
        { x : Δ[n] _⦋m⦌ // Membership.mem (γ := Set (Δ[n] _⦋m⦌)) (Δ[n].nonDegenerate m) x })
      (Subtype.mk (p := fun (x : Δ[n] _⦋m⦌) ↦ Membership.mem (γ := Set (Δ[n] _⦋m⦌)) (Δ[n].nonDegenerate m) x)
          ((Equiv.symm objEquiv : (a : unop (op ⦋m⦌) ⟶ ⦋n⦌) → Δ[n] _⦋m⦌) f₂) h₂ :
        { x : Δ[n] _⦋m⦌ // Membership.mem (γ := Set (Δ[n] _⦋m⦌)) (Δ[n].nonDegenerate m) x })
⊢ Subtype.mk (p := fun (x : Δ[n] _⦋m⦌) ↦ Membership.mem (γ := Set (Δ[n] _⦋m⦌)) (Δ[n].nonDegenerate m) x)
      ((Equiv.symm objEquiv : (a : unop (op ⦋m⦌) ⟶ ⦋n⦌) → Δ[n] _⦋m⦌) f₁) h₁ =
    Subtype.mk (p := fun (x : Δ[n] _⦋m⦌) ↦ Membership.mem (γ := Set (Δ[n] _⦋m⦌)) (Δ[n].nonDegenerate m) x) x₂ h₂

Tactic:
obtain ⟨f₂, rfl⟩ := objEquiv.symm.surjective x₂

Premises used: Equiv.surjective, Equiv.symm, SSet.stdSimplex.objEquiv, rfl