-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Homotopy
Goal:
X Y : SSet
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
i : Fin (n + 1)
x : X _⦋n + 1⦌
h :
  Eq (α := Y _⦋n + 1⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (H.h.app (op ⦋n + 1⦌)) : (a : X _⦋n + 1⦌ ⊗ Δ[1] _⦋n + 1⦌) → Y _⦋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.castSucc.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.σ i.succ) :
                            Δ[n + 1] _⦋n + 1 + 1⦌))))) :
                (a : X _⦋n + 1⦌) → X _⦋n + 1⦌)
              x,
            (ConcreteCategory.hom (FC := TypeCat.Fun) (δ Δ[1] i.castSucc.succ) :
                (a : Δ[1] _⦋n + 1 + 1⦌) → Δ[1] _⦋n + 1⦌)
              (stdSimplex.objMk₁ i.castSucc.succ.succ)) :
          X _⦋n + 1⦌ × Δ[1] _⦋n + 1⦌) :
      Y _⦋n + 1⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (H.h.app (op ⦋n + 1⦌)) : (a : X _⦋n + 1⦌ ⊗ Δ[1] _⦋n + 1⦌) → Y _⦋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.castSucc.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.σ i.castSucc) :
                            Δ[n + 1] _⦋n + 1 + 1⦌))))) :
                (a : X _⦋n + 1⦌) → X _⦋n + 1⦌)
              x,
            (ConcreteCategory.hom (FC := TypeCat.Fun) (δ Δ[1] i.castSucc.succ) :
                (a : Δ[1] _⦋n + 1 + 1⦌) → Δ[1] _⦋n + 1⦌)
              (stdSimplex.objMk₁ i.castSucc.castSucc.succ)) :
          X _⦋n + 1⦌ × Δ[1] _⦋n + 1⦌) :
      Y _⦋n + 1⦌)
⊢ Eq (α := Y _⦋n + 1⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (NatTrans.app ((Equiv.symm yonedaEquiv : (a : X _⦋n + 1⦌) → Δ[n + 1] ⟶ X) x ▷ Δ[1] ≫ H.h) (op ⦋n + 1⦌)) :
          (a : (Δ[n + 1] ⊗ Δ[1]) _⦋n + 1⦌) → Y _⦋n + 1⦌)
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
                (δ (tensorObj (𝒞 := Functor.category) Δ[n + 1] Δ[1]) i.castSucc.succ) :
              (a : (Δ[n + 1] ⊗ Δ[1]) _⦋n + 1 + 1⦌) → (Δ[n + 1] ⊗ Δ[1]) _⦋n + 1⦌)
            (↑((prodStdSimplex.nonDegenerateEquiv₁ :
                    (a : Fin (n + 1 + 1)) → (↑((Δ[n + 1] ⊗ Δ[1]).nonDegenerate (n + 1 + 1)) : Type u))
                  i.succ) :
              (Δ[n + 1] ⊗ Δ[1]) _⦋n + 1 + 1⦌) :
          tensorObj (𝒞 := Functor.category) Δ[n + 1] Δ[1] _⦋n + 1⦌) :
      Y _⦋n + 1⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (NatTrans.app ((Equiv.symm yonedaEquiv : (a : X _⦋n + 1⦌) → Δ[n + 1] ⟶ X) x ▷ Δ[1] ≫ H.h) (op ⦋n + 1⦌)) :
          (a : (Δ[n + 1] ⊗ Δ[1]) _⦋n + 1⦌) → Y _⦋n + 1⦌)
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
                (δ (tensorObj (𝒞 := Functor.category) Δ[n + 1] Δ[1]) i.castSucc.succ) :
              (a : (Δ[n + 1] ⊗ Δ[1]) _⦋n + 1 + 1⦌) → (Δ[n + 1] ⊗ Δ[1]) _⦋n + 1⦌)
            (↑((prodStdSimplex.nonDegenerateEquiv₁ :
                    (a : Fin (n + 1 + 1)) → (↑((Δ[n + 1] ⊗ Δ[1]).nonDegenerate (n + 1 + 1)) : Type u))
                  i.castSucc) :
              (Δ[n + 1] ⊗ Δ[1]) _⦋n + 1 + 1⦌) :
          tensorObj (𝒞 := Functor.category) Δ[n + 1] Δ[1] _⦋n + 1⦌) :
      Y _⦋n + 1⦌)

Tactic:
dsimp