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

Tactic:
ext k