-- Lean 4 proof step from Mathlib.AlgebraicTopology.ExtraDegeneracy (goal)
Goal:
Δ : SimplexCategory
n : ℕ
i : Fin (n + 1)
φ : (stdSimplex.obj Δ).left _⦋n⦌
⊢ 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))))
          φ)))
have 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))
Tactic: ext j : 2