-- Lean 4 proof step from Mathlib.AlgebraicTopology.ExtraDegeneracy (goal)
Goal:
Δ : SimplexCategory
x : SSet.stdSimplex.obj Δ _⦋0⦌
⊢ Eq (α := unop (op ⦋0⦌) ⟶ Δ)
    (((objEquiv : SSet.stdSimplex.obj Δ _⦋0⦌ ≃ (unop (op ⦋0⦌) ⟶ Δ)) :
          (a : SSet.stdSimplex.obj Δ _⦋0⦌) → unop (op ⦋0⦌) ⟶ Δ)
        (TypeCat.Fun.toFun
          (ConcreteCategory.hom (FC := TypeCat.Fun)
            ((↾fun (f : SSet.stdSimplex.obj Δ _⦋0⦌) ↦
                (Equiv.symm objEquiv : (a : ⦋1⦌ ⟶ Δ) → SSet.stdSimplex.obj Δ _⦋1⦌)
                  (SimplexCategory.Hom.mk
                    {
                      toFun :=
                        shiftFun
                          (⇑(SimplexCategory.Hom.toOrderHom
                                (((objEquiv : SSet.stdSimplex.obj Δ _⦋0⦌ ≃ (unop (op ⦋0⦌) ⟶ Δ)) :
                                    (a : SSet.stdSimplex.obj Δ _⦋0⦌) → ⦋0⦌ ⟶ Δ)
                                  f)) :
                            (a : Fin 1) → Fin (Δ.len + 1)),
                      monotone' := ⋯ : Fin 2 →o Fin (Δ.len + 1) })) ≫
              SimplicialObject.δ (SSet.stdSimplex.obj Δ) 1))
          x) :
      unop (op ⦋0⦌) ⟶ Δ)
    (((objEquiv : SSet.stdSimplex.obj Δ _⦋0⦌ ≃ (unop (op ⦋0⦌) ⟶ Δ)) :
          (a : SSet.stdSimplex.obj Δ _⦋0⦌) → unop (op ⦋0⦌) ⟶ Δ)
        (TypeCat.Fun.toFun
          (ConcreteCategory.hom (FC := TypeCat.Fun)
            (CategoryStruct.comp (Y := ⊤_ Type u_1) (Limits.terminal.from (SSet.stdSimplex.obj Δ _⦋0⦌))
              (↾fun (x : ⊤_ Type u_1) ↦
                objMk ((OrderHom.const (Fin 1) : (a : Fin (Δ.len + 1)) → Fin 1 →o Fin (Δ.len + 1)) 0))))
          x) :
      unop (op ⦋0⦌) ⟶ Δ)
have h : ∀ (j : Fin ((unop (op ⦋0⦌)).len + 1)),
  (↑((SimplexCategory.Hom.toOrderHom
              (((objEquiv : SSet.stdSimplex.obj Δ _⦋0⦌ ≃ (unop (op ⦋0⦌) ⟶ Δ)) :
                  (a : SSet.stdSimplex.obj Δ _⦋0⦌) → unop (op ⦋0⦌) ⟶ Δ)
                (TypeCat.Fun.toFun
                  (ConcreteCategory.hom (FC := TypeCat.Fun)
                    ((↾fun (f : SSet.stdSimplex.obj Δ _⦋0⦌) ↦
                        (Equiv.symm objEquiv : (a : ⦋1⦌ ⟶ Δ) → SSet.stdSimplex.obj Δ _⦋1⦌)
                          (SimplexCategory.Hom.mk
                            {
                              toFun :=
                                shiftFun
                                  (⇑(SimplexCategory.Hom.toOrderHom
                                        (((objEquiv : SSet.stdSimplex.obj Δ _⦋0⦌ ≃ (unop (op ⦋0⦌) ⟶ Δ)) :
                                            (a : SSet.stdSimplex.obj Δ _⦋0⦌) → ⦋0⦌ ⟶ Δ)
                                          f)) :
                                    (a : Fin 1) → Fin (Δ.len + 1)),
                              monotone' := sorry : Fin 2 →o Fin (Δ.len + 1) })) ≫
                      SimplicialObject.δ (SSet.stdSimplex.obj Δ) 1))
                  x)) :
            (a : Fin ((unop (op ⦋0⦌)).len + 1)) → Fin (Δ.len + 1))
          j) :
      ℕ) =
    (↑((SimplexCategory.Hom.toOrderHom
              (((objEquiv : SSet.stdSimplex.obj Δ _⦋0⦌ ≃ (unop (op ⦋0⦌) ⟶ Δ)) :
                  (a : SSet.stdSimplex.obj Δ _⦋0⦌) → unop (op ⦋0⦌) ⟶ Δ)
                (TypeCat.Fun.toFun
                  (ConcreteCategory.hom (FC := TypeCat.Fun)
                    (CategoryStruct.comp (Y := ⊤_ Type u_1) (Limits.terminal.from (SSet.stdSimplex.obj Δ _⦋0⦌))
                      (↾fun (x : ⊤_ Type u_1) ↦
                        objMk ((OrderHom.const (Fin 1) : (a : Fin (Δ.len + 1)) → Fin 1 →o Fin (Δ.len + 1)) 0))))
                  x)) :
            (a : Fin ((unop (op ⦋0⦌)).len + 1)) → Fin (Δ.len + 1))
          j) :
      ℕ)
Tactic: ext j