-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Homotopy
Goal:
X Y : SSet
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
hij : j.castSucc < i
x : X _⦋n + 1⦌
h :
  Eq (α := X _⦋n + 1⦌)
    (((ConcreteCategory.hom (FC := TypeCat.Fun)
                (X.map
                  (Quiver.Hom.op
                    (((stdSimplex.objEquiv : Δ[n + 1] _⦋n + 1⦌ ≃ (unop (op ⦋n + 1⦌) ⟶ ⦋n + 1⦌)) :
                        (a : Δ[n + 1] _⦋n + 1⦌) → ⦋n + 1⦌ ⟶ ⦋n + 1⦌)
                      ((ConcreteCategory.hom (FC := TypeCat.Fun) (δ Δ[n + 1] i.succ) :
                          (a : Δ[n + 1] _⦋n + 1 + 1⦌) → Δ[n + 1] _⦋n + 1⦌)
                        ((Equiv.symm stdSimplex.objEquiv : (a : ⦋n + 1 + 1⦌ ⟶ ⦋n + 1⦌) → Δ[n + 1] _⦋n + 1 + 1⦌)
                            (SimplexCategory.σ j.castSucc) :
                          Δ[n + 1] _⦋n + 1 + 1⦌))))) :
              (a : X _⦋n + 1⦌) → X _⦋n + 1⦌)
            x,
          (ConcreteCategory.hom (FC := TypeCat.Fun) (δ Δ[1] i.succ) : (a : Δ[1] _⦋n + 1 + 1⦌) → Δ[1] _⦋n + 1⦌)
            (stdSimplex.objMk₁ j.castSucc.castSucc.succ)).1 :
      X _⦋n + 1⦌)
    (((ConcreteCategory.hom (FC := TypeCat.Fun)
                (NatTrans.app
                  ((Equiv.symm yonedaEquiv : (a : X _⦋n⦌) → Δ[n] ⟶ X)
                    ((ConcreteCategory.hom (FC := TypeCat.Fun) (δ X i) : (a : X _⦋n + 1⦌) → X _⦋n⦌) x : X _⦋n⦌))
                  (op ⦋n + 1⦌)) :
              (a : Δ[n] _⦋n + 1⦌) → X _⦋n + 1⦌)
            ((Equiv.symm stdSimplex.objEquiv : (a : ⦋n + 1⦌ ⟶ ⦋n⦌) → Δ[n] _⦋n + 1⦌) (SimplexCategory.σ j) :
              Δ[n] _⦋n + 1⦌),
          stdSimplex.objMk₁ j.castSucc.succ).1 :
      X _⦋n + 1⦌)
h₁ :
  ∀ (k : Fin (n + 1 + 1)),
    Eq (α := Fin (HAdd.hAdd (α := ℕ) 1 1))
      (((((ConcreteCategory.hom (FC := TypeCat.Fun)
                        (X.map
                          (Quiver.Hom.op
                            (((stdSimplex.objEquiv : Δ[n + 1] _⦋n + 1⦌ ≃ (unop (op ⦋n + 1⦌) ⟶ ⦋n + 1⦌)) :
                                (a : Δ[n + 1] _⦋n + 1⦌) → ⦋n + 1⦌ ⟶ ⦋n + 1⦌)
                              ((ConcreteCategory.hom (FC := TypeCat.Fun) (δ Δ[n + 1] i.succ) :
                                  (a : Δ[n + 1] _⦋n + 1 + 1⦌) → Δ[n + 1] _⦋n + 1⦌)
                                ((Equiv.symm stdSimplex.objEquiv : (a : ⦋n + 1 + 1⦌ ⟶ ⦋n + 1⦌) → Δ[n + 1] _⦋n + 1 + 1⦌)
                                    (SimplexCategory.σ j.castSucc) :
                                  Δ[n + 1] _⦋n + 1 + 1⦌))))) :
                      (a : X _⦋n + 1⦌) → X _⦋n + 1⦌)
                    x,
                  (ConcreteCategory.hom (FC := TypeCat.Fun) (δ Δ[1] i.succ) : (a : Δ[1] _⦋n + 1 + 1⦌) → Δ[1] _⦋n + 1⦌)
                    (stdSimplex.objMk₁ j.castSucc.castSucc.succ)).2 :
              Δ[1] _⦋n + 1⦌) :
            (a : Fin (n + 1 + 1)) → Fin (1 + 1))
          k :
        Fin (HAdd.hAdd (α := ℕ) 1 1))
      (((((ConcreteCategory.hom (FC := TypeCat.Fun)
                        (NatTrans.app
                          ((Equiv.symm yonedaEquiv : (a : X _⦋n⦌) → Δ[n] ⟶ X)
                            ((ConcreteCategory.hom (FC := TypeCat.Fun) (δ X i) : (a : X _⦋n + 1⦌) → X _⦋n⦌) x : X _⦋n⦌))
                          (op ⦋n + 1⦌)) :
                      (a : Δ[n] _⦋n + 1⦌) → X _⦋n + 1⦌)
                    ((Equiv.symm stdSimplex.objEquiv : (a : ⦋n + 1⦌ ⟶ ⦋n⦌) → Δ[n] _⦋n + 1⦌) (SimplexCategory.σ j) :
                      Δ[n] _⦋n + 1⦌),
                  stdSimplex.objMk₁ j.castSucc.succ) :
                X _⦋n + 1⦌ × Δ[1] _⦋n + 1⦌).2 :
            (a : Fin (n + 1 + 1)) → Fin (1 + 1))
          k :
        Fin (HAdd.hAdd (α := ℕ) 1 1))
⊢ Eq (α := X _⦋n + 1⦌ × Δ[1] _⦋n + 1⦌)
    (((ConcreteCategory.hom (FC := TypeCat.Fun)
              (X.map
                (Quiver.Hom.op
                  (((stdSimplex.objEquiv : Δ[n + 1] _⦋n + 1⦌ ≃ (unop (op ⦋n + 1⦌) ⟶ ⦋n + 1⦌)) :
                      (a : Δ[n + 1] _⦋n + 1⦌) → ⦋n + 1⦌ ⟶ ⦋n + 1⦌)
                    ((ConcreteCategory.hom (FC := TypeCat.Fun) (δ Δ[n + 1] i.succ) :
                        (a : Δ[n + 1] _⦋n + 1 + 1⦌) → Δ[n + 1] _⦋n + 1⦌)
                      ((Equiv.symm stdSimplex.objEquiv : (a : ⦋n + 1 + 1⦌ ⟶ ⦋n + 1⦌) → Δ[n + 1] _⦋n + 1 + 1⦌)
                          (SimplexCategory.σ j.castSucc) :
                        Δ[n + 1] _⦋n + 1 + 1⦌))))) :
            (a : X _⦋n + 1⦌) → X _⦋n + 1⦌)
          x,
        (ConcreteCategory.hom (FC := TypeCat.Fun) (δ Δ[1] i.succ) : (a : Δ[1] _⦋n + 1 + 1⦌) → Δ[1] _⦋n + 1⦌)
          (stdSimplex.objMk₁ j.castSucc.castSucc.succ)) :
      X _⦋n + 1⦌ × Δ[1] _⦋n + 1⦌)
    (((ConcreteCategory.hom (FC := TypeCat.Fun)
              (NatTrans.app
                ((Equiv.symm yonedaEquiv : (a : X _⦋n⦌) → Δ[n] ⟶ X)
                  ((ConcreteCategory.hom (FC := TypeCat.Fun) (δ X i) : (a : X _⦋n + 1⦌) → X _⦋n⦌) x : X _⦋n⦌))
                (op ⦋n + 1⦌)) :
            (a : Δ[n] _⦋n + 1⦌) → X _⦋n + 1⦌)
          ((Equiv.symm stdSimplex.objEquiv : (a : ⦋n + 1⦌ ⟶ ⦋n⦌) → Δ[n] _⦋n + 1⦌) (SimplexCategory.σ j) :
            Δ[n] _⦋n + 1⦌),
        stdSimplex.objMk₁ j.castSucc.succ) :
      X _⦋n + 1⦌ × Δ[1] _⦋n + 1⦌)

Tactic:
ext k : 2