-- Module: Mathlib.AlgebraicTopology.ExtraDegeneracy
Goal:
Δ : SimplexCategory
x : SSet.stdSimplex.obj Δ _⦋0⦌
j : Fin ((unop (op ⦋0⦌)).len + 1)
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' := ⋯ : 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, ⋯⟩ : 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, ⋯⟩)) :
      ℕ)
⊢ (↑((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) :
      ℕ)

Tactic:
fin_cases j