-- Lean 4 proof step from Mathlib.AlgebraicTopology.ExtraDegeneracy (goal)
Goal:
Δ : SimplexCategory
x : SSet.stdSimplex.obj Δ _⦋0⦌
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' := ⋯ : 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) :
      ℕ)
have h : (↑((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))
        ((fun (i : Fin ((unop (op ⦋0⦌)).len + 1)) ↦ i) (⟨0, sorry⟩ : 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)
                  (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))
        ((fun (i : Fin ((unop (op ⦋0⦌)).len + 1)) ↦ i) ⟨0, sorry⟩)) :
    ℕ)
Tactic: fin_cases j
Cleared hypotheses: j