-- Module: Mathlib.AlgebraicTopology.ExtraDegeneracy
Goal:
Δ : SimplexCategory
x : SSet.stdSimplex.obj Δ _⦋0⦌
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' := ⋯ : 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) :
        ℕ)
⊢ 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⦌) ⟶ Δ)

Tactic:
ext j