-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex (hypothesis)
Goal:
n d : ℕ
x : (↑(Δ[n].nonDegenerate d) : Type u)
this :
  Mono (C := SimplexCategory) (X := unop (op ⦋d⦌)) (Y := ⦋n⦌)
    (((objEquiv : Δ[n] _⦋d⦌ ≃ (unop (op ⦋d⦌) ⟶ ⦋n⦌)) : (a : Δ[n] _⦋d⦌) → unop (op ⦋d⦌) ⟶ ⦋n⦌) (↑x : Δ[n] _⦋d⦌))
⊢ ∀ {a b : Fin (d + 1)},
    LE.le (α :=
        ↥(↑(((nonDegenerateEquiv' :
                    (↑(Δ[n].nonDegenerate d) : Type u) ≃ (↑{S : Finset (Fin (n + 1)) | #S = d + 1} : Type)) :
                  (a : (↑(Δ[n].nonDegenerate d) : Type u)) → (↑{S : Finset (Fin (n + 1)) | #S = d + 1} : Type))
                x) :
            Finset (Fin (n + 1))))
        ((Equiv.ofBijective
                (fun (i : Fin (d + 1)) ↦
                  Subtype.mk (p := fun (x_1 : Fin (n + 1)) ↦
                    Membership.mem (γ := Finset (Fin (n + 1)))
                      (↑(((nonDegenerateEquiv' :
                                (↑(Δ[n].nonDegenerate d) : Type u) ≃
                                  (↑{S : Finset (Fin (n + 1)) | #S = d + 1} : Type)) :
                              (a : (↑(Δ[n].nonDegenerate d) : Type u)) →
                                (↑{S : Finset (Fin (n + 1)) | #S = d + 1} : Type))
                            x) :
                        Finset (Fin (n + 1)))
                      x_1)
                    (((↑x : Δ[n] _⦋d⦌) : (a : Fin (d + 1)) → Fin (n + 1)) i) ⋯)
                ⋯ :
              (a : Fin (d + 1)) →
                ↥(↑((nonDegenerateEquiv' :
                          (a : (↑(Δ[n].nonDegenerate d) : Type u)) → (↑{S : Finset (Fin (n + 1)) | #S = d + 1} : Type))
                        x) :
                    Finset (Fin (n + 1))))
            a :
          ↥(↑(((nonDegenerateEquiv' :
                      (↑(Δ[n].nonDegenerate d) : Type u) ≃ (↑{S : Finset (Fin (n + 1)) | #S = d + 1} : Type)) :
                    (a : (↑(Δ[n].nonDegenerate d) : Type u)) → (↑{S : Finset (Fin (n + 1)) | #S = d + 1} : Type))
                  x) :
              Finset (Fin (n + 1))))
        ((Equiv.ofBijective
                (fun (i : Fin (d + 1)) ↦
                  Subtype.mk (p := fun (x_1 : Fin (n + 1)) ↦
                    Membership.mem (γ := Finset (Fin (n + 1)))
                      (↑(((nonDegenerateEquiv' :
                                (↑(Δ[n].nonDegenerate d) : Type u) ≃
                                  (↑{S : Finset (Fin (n + 1)) | #S = d + 1} : Type)) :
                              (a : (↑(Δ[n].nonDegenerate d) : Type u)) →
                                (↑{S : Finset (Fin (n + 1)) | #S = d + 1} : Type))
                            x) :
                        Finset (Fin (n + 1)))
                      x_1)
                    (((↑x : Δ[n] _⦋d⦌) : (a : Fin (d + 1)) → Fin (n + 1)) i) ⋯)
                ⋯ :
              (a : Fin (d + 1)) →
                ↥(↑((nonDegenerateEquiv' :
                          (a : (↑(Δ[n].nonDegenerate d) : Type u)) → (↑{S : Finset (Fin (n + 1)) | #S = d + 1} : Type))
                        x) :
                    Finset (Fin (n + 1))))
            b :
          ↥(↑(((nonDegenerateEquiv' :
                      (↑(Δ[n].nonDegenerate d) : Type u) ≃ (↑{S : Finset (Fin (n + 1)) | #S = d + 1} : Type)) :
                    (a : (↑(Δ[n].nonDegenerate d) : Type u)) → (↑{S : Finset (Fin (n + 1)) | #S = d + 1} : Type))
                  x) :
              Finset (Fin (n + 1)))) ↔
      a ≤ b
have this₁ : Function.Injective (α := Fin ((unop (op ⦋d⦌)).len + 1)) (β := Fin (⦋n⦌.len + 1))
  (⇑(Hom.toOrderHom
        (((objEquiv : Δ[n] _⦋d⦌ ≃ (unop (op ⦋d⦌) ⟶ ⦋n⦌)) : (a : Δ[n] _⦋d⦌) → unop (op ⦋d⦌) ⟶ ⦋n⦌) (↑x : Δ[n] _⦋d⦌))) :
    (a : Fin ((unop (op ⦋d⦌)).len + 1)) → Fin (⦋n⦌.len + 1))
Tactic: rw [SimplexCategory.mono_iff_injective] at this
Cleared hypotheses: this