-- Module: Mathlib.AlgebraicTopology.ExtraDegeneracy
Goal:
Δ : SimplexCategory
n : ℕ
i : Fin (n + 1)
φ : (stdSimplex.obj Δ).left _⦋n⦌
h :
  ∀ (j : Fin ((unop (op ⦋n + 1 + 1⦌)).len + 1)),
    Eq (α := Fin (Δ.len + 1))
      ((SimplexCategory.Hom.toOrderHom
              (((objEquiv : SSet.stdSimplex.obj Δ _⦋n + 1 + 1⦌ ≃ (unop (op ⦋n + 1 + 1⦌) ⟶ Δ)) :
                  (a : SSet.stdSimplex.obj Δ _⦋n + 1 + 1⦌) → unop (op ⦋n + 1 + 1⦌) ⟶ Δ)
                (TypeCat.Fun.toFun
                  (ConcreteCategory.hom (FC := TypeCat.Fun)
                    ((↾fun (f : (stdSimplex.obj Δ).left _⦋n⦌) ↦
                        (Equiv.symm objEquiv : (a : unop (op ⦋n + 1⦌) ⟶ Δ) → SSet.stdSimplex.obj Δ _⦋n + 1⦌)
                          (shift
                            (((objEquiv : SSet.stdSimplex.obj Δ _⦋n⦌ ≃ (unop (op ⦋n⦌) ⟶ Δ)) :
                                (a : SSet.stdSimplex.obj Δ _⦋n⦌) → unop (op ⦋n⦌) ⟶ Δ)
                              f))) ≫
                      (stdSimplex.obj Δ).left.σ i.succ))
                  φ)) :
            (a : Fin ((unop (op ⦋n + 1 + 1⦌)).len + 1)) → Fin (Δ.len + 1))
          j :
        Fin (Δ.len + 1))
      ((SimplexCategory.Hom.toOrderHom
              (((objEquiv : SSet.stdSimplex.obj Δ _⦋n + 1 + 1⦌ ≃ (unop (op ⦋n + 1 + 1⦌) ⟶ Δ)) :
                  (a : SSet.stdSimplex.obj Δ _⦋n + 1 + 1⦌) → unop (op ⦋n + 1 + 1⦌) ⟶ Δ)
                (TypeCat.Fun.toFun
                  (ConcreteCategory.hom (FC := TypeCat.Fun)
                    ((stdSimplex.obj Δ).left.σ i ≫
                      ↾fun (f : (stdSimplex.obj Δ).left _⦋n + 1⦌) ↦
                        (Equiv.symm objEquiv : (a : unop (op ⦋n + 1 + 1⦌) ⟶ Δ) → SSet.stdSimplex.obj Δ _⦋n + 1 + 1⦌)
                          (shift
                            (((objEquiv : SSet.stdSimplex.obj Δ _⦋n + 1⦌ ≃ (unop (op ⦋n + 1⦌) ⟶ Δ)) :
                                (a : SSet.stdSimplex.obj Δ _⦋n + 1⦌) → unop (op ⦋n + 1⦌) ⟶ Δ)
                              f))))
                  φ)) :
            (a : Fin ((unop (op ⦋n + 1 + 1⦌)).len + 1)) → Fin (Δ.len + 1))
          j :
        Fin (Δ.len + 1))
⊢ Eq (α := Fin ((unop (op ⦋n + 1 + 1⦌)).len + 1) →o Fin (Δ.len + 1))
    (SimplexCategory.Hom.toOrderHom
      (((objEquiv : SSet.stdSimplex.obj Δ _⦋n + 1 + 1⦌ ≃ (unop (op ⦋n + 1 + 1⦌) ⟶ Δ)) :
          (a : SSet.stdSimplex.obj Δ _⦋n + 1 + 1⦌) → unop (op ⦋n + 1 + 1⦌) ⟶ Δ)
        (TypeCat.Fun.toFun
          (ConcreteCategory.hom (FC := TypeCat.Fun)
            ((↾fun (f : (stdSimplex.obj Δ).left _⦋n⦌) ↦
                (Equiv.symm objEquiv : (a : unop (op ⦋n + 1⦌) ⟶ Δ) → SSet.stdSimplex.obj Δ _⦋n + 1⦌)
                  (shift
                    (((objEquiv : SSet.stdSimplex.obj Δ _⦋n⦌ ≃ (unop (op ⦋n⦌) ⟶ Δ)) :
                        (a : SSet.stdSimplex.obj Δ _⦋n⦌) → unop (op ⦋n⦌) ⟶ Δ)
                      f))) ≫
              (stdSimplex.obj Δ).left.σ i.succ))
          φ)))
    (SimplexCategory.Hom.toOrderHom
      (((objEquiv : SSet.stdSimplex.obj Δ _⦋n + 1 + 1⦌ ≃ (unop (op ⦋n + 1 + 1⦌) ⟶ Δ)) :
          (a : SSet.stdSimplex.obj Δ _⦋n + 1 + 1⦌) → unop (op ⦋n + 1 + 1⦌) ⟶ Δ)
        (TypeCat.Fun.toFun
          (ConcreteCategory.hom (FC := TypeCat.Fun)
            ((stdSimplex.obj Δ).left.σ i ≫
              ↾fun (f : (stdSimplex.obj Δ).left _⦋n + 1⦌) ↦
                (Equiv.symm objEquiv : (a : unop (op ⦋n + 1 + 1⦌) ⟶ Δ) → SSet.stdSimplex.obj Δ _⦋n + 1 + 1⦌)
                  (shift
                    (((objEquiv : SSet.stdSimplex.obj Δ _⦋n + 1⦌ ≃ (unop (op ⦋n + 1⦌) ⟶ Δ)) :
                        (a : SSet.stdSimplex.obj Δ _⦋n + 1⦌) → unop (op ⦋n + 1⦌) ⟶ Δ)
                      f))))
          φ)))

Tactic:
ext j : 2