-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Homotopy (goal)
Goal:
X Y : SSet
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
i j : Fin (n + 1)
hij : j ≤ i
x : X _⦋n⦌
⊢ Eq (α := Y _⦋n + 1 + 1⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (H.h.app (op ⦋n + 1 + 1⦌)) :
          (a : X _⦋n + 1 + 1⦌ ⊗ Δ[1] _⦋n + 1 + 1⦌) → Y _⦋n + 1 + 1⦌)
        (((ConcreteCategory.hom (FC := TypeCat.Fun)
                  (NatTrans.app ((Equiv.symm yonedaEquiv : (a : X _⦋n⦌) → Δ[n] ⟶ X) x) (op ⦋n + 1 + 1⦌)) :
                (a : Δ[n] _⦋n + 1 + 1⦌) → X _⦋n + 1 + 1⦌)
              ((ConcreteCategory.hom (FC := TypeCat.Fun) (σ Δ[n] i.succ) : (a : Δ[n] _⦋n + 1⦌) → Δ[n] _⦋n + 1 + 1⦌)
                  ((Equiv.symm stdSimplex.objEquiv : (a : ⦋n + 1⦌ ⟶ ⦋n⦌) → Δ[n] _⦋n + 1⦌) (SimplexCategory.σ j) :
                    Δ[n] _⦋n + 1⦌) :
                Δ[n] _⦋n + 1 + 1⦌),
            (ConcreteCategory.hom (FC := TypeCat.Fun) (σ Δ[1] i.succ) : (a : Δ[1] _⦋n + 1⦌) → Δ[1] _⦋n + 1 + 1⦌)
              (stdSimplex.objMk₁ j.castSucc.succ)) :
          X _⦋n + 1 + 1⦌ × Δ[1] _⦋n + 1 + 1⦌) :
      Y _⦋n + 1 + 1⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (H.h.app (op ⦋n + 1 + 1⦌)) :
          (a : X _⦋n + 1 + 1⦌ ⊗ Δ[1] _⦋n + 1 + 1⦌) → Y _⦋n + 1 + 1⦌)
        (((ConcreteCategory.hom (FC := TypeCat.Fun)
                  (NatTrans.app
                    ((Equiv.symm yonedaEquiv : (a : X _⦋n + 1⦌) → Δ[n + 1] ⟶ X)
                      ((ConcreteCategory.hom (FC := TypeCat.Fun) (σ X i) : (a : X _⦋n⦌) → X _⦋n + 1⦌) x : X _⦋n + 1⦌))
                    (op ⦋n + 1 + 1⦌)) :
                (a : Δ[n + 1] _⦋n + 1 + 1⦌) → X _⦋n + 1 + 1⦌)
              ((Equiv.symm stdSimplex.objEquiv : (a : ⦋n + 1 + 1⦌ ⟶ ⦋n + 1⦌) → Δ[n + 1] _⦋n + 1 + 1⦌)
                  (SimplexCategory.σ j.castSucc) :
                Δ[n + 1] _⦋n + 1 + 1⦌),
            stdSimplex.objMk₁ j.castSucc.castSucc.succ) :
          X _⦋n + 1 + 1⦌ × Δ[1] _⦋n + 1 + 1⦌) :
      Y _⦋n + 1 + 1⦌)
have h : Eq (α := X _⦋n + 1 + 1⦌ × Δ[1] _⦋n + 1 + 1⦌)
  (((ConcreteCategory.hom (FC := TypeCat.Fun)
            (NatTrans.app ((Equiv.symm yonedaEquiv : (a : X _⦋n⦌) → Δ[n] ⟶ X) x) (op ⦋n + 1 + 1⦌)) :
          (a : Δ[n] _⦋n + 1 + 1⦌) → X _⦋n + 1 + 1⦌)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (σ Δ[n] i.succ) : (a : Δ[n] _⦋n + 1⦌) → Δ[n] _⦋n + 1 + 1⦌)
            ((Equiv.symm stdSimplex.objEquiv : (a : ⦋n + 1⦌ ⟶ ⦋n⦌) → Δ[n] _⦋n + 1⦌) (SimplexCategory.σ j) :
              Δ[n] _⦋n + 1⦌) :
          Δ[n] _⦋n + 1 + 1⦌),
      (ConcreteCategory.hom (FC := TypeCat.Fun) (σ Δ[1] i.succ) : (a : Δ[1] _⦋n + 1⦌) → Δ[1] _⦋n + 1 + 1⦌)
        (stdSimplex.objMk₁ j.castSucc.succ)) :
    X _⦋n + 1 + 1⦌ × Δ[1] _⦋n + 1 + 1⦌)
  (((ConcreteCategory.hom (FC := TypeCat.Fun)
            (NatTrans.app
              ((Equiv.symm yonedaEquiv : (a : X _⦋n + 1⦌) → Δ[n + 1] ⟶ X)
                ((ConcreteCategory.hom (FC := TypeCat.Fun) (σ X i) : (a : X _⦋n⦌) → X _⦋n + 1⦌) x : X _⦋n + 1⦌))
              (op ⦋n + 1 + 1⦌)) :
          (a : Δ[n + 1] _⦋n + 1 + 1⦌) → X _⦋n + 1 + 1⦌)
        ((Equiv.symm stdSimplex.objEquiv : (a : ⦋n + 1 + 1⦌ ⟶ ⦋n + 1⦌) → Δ[n + 1] _⦋n + 1 + 1⦌)
            (SimplexCategory.σ j.castSucc) :
          Δ[n + 1] _⦋n + 1 + 1⦌),
      stdSimplex.objMk₁ j.castSucc.castSucc.succ) :
    X _⦋n + 1 + 1⦌ × Δ[1] _⦋n + 1 + 1⦌)
Tactic: apply congr_arg