-- Module: Mathlib.AlgebraicTopology.SingularHomology.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasCoproducts.{w, v, u} C
inst_2 : Preadditive.{v, u} C
n : ℕ
F : CategoryTheory.Functor.{w, v, w + 1, u} TopCat C
X : TopCat
i : TopCat.toSSet.obj X _⦋n⦌
dsimp :
  Eq (α := F.obj (TopCat.uliftFunctor.obj (TopCat.of (↑(_root_.stdSimplex ℝ (Fin (n + 1))) : Type))) ⟶ F.obj X)
    (CategoryStruct.comp (Y :=
        sigmaObj.{w, v, u} fun (x : TopCat.toSSet.obj X _⦋n⦌) ↦
          F.obj (TopCat.uliftFunctor.obj (TopCat.of (↑(_root_.stdSimplex ℝ (Fin (n + 1))) : Type))))
        (Sigma.ι.{w, v, u} (C := C)
          (fun (x : TopCat.toSSet.obj X _⦋n⦌) ↦
            F.obj (TopCat.uliftFunctor.obj (TopCat.of (↑(_root_.stdSimplex ℝ (Fin (n + 1))) : Type))))
          i)
        (CategoryStruct.comp (Y := sigmaObj.{w, v, u} fun (x : TopCat.toSSet.obj X _⦋n⦌) ↦ F.obj (toTop.obj Δ[n]))
          (Limits.Sigma.map fun (x : TopCat.toSSet.obj X _⦋n⦌) ↦ F.map (toTopSimplex.inv.app ⦋n⦌))
          (𝟙 (sigmaObj.{w, v, u} fun (x : TopCat.toSSet.obj X _⦋n⦌) ↦ F.obj (toTop.obj Δ[n])) ≫
            (𝟙 (sigmaObj.{w, v, u} fun (x : TopCat.toSSet.obj X _⦋n⦌) ↦ F.obj (toTop.obj Δ[n])) ≫
                (Sigma.desc fun (α : TopCat.toSSet.obj X _⦋n⦌) ↦
                    F.map
                      (toTop.map
                        ((Equiv.symm SSet.yonedaEquiv : (a : TopCat.toSSet.obj X _⦋n⦌) → Δ[n] ⟶ TopCat.toSSet.obj X)
                          α))) ≫
                  𝟙 (F.obj (toTop.obj (TopCat.toSSet.obj X)))) ≫
              (NatTrans.app (Adjunction.counit (Adjunction.whiskerLeft C sSetTopAdj)) F).app X)) :
      F.obj (TopCat.uliftFunctor.obj (TopCat.of (↑(_root_.stdSimplex ℝ (Fin (n + 1))) : Type))) ⟶ F.obj X)
    (F.map
        (toTopSimplex.inv.app ⦋n⦌ ≫
          toTop.map ((Equiv.symm SSet.yonedaEquiv : (a : TopCat.toSSet.obj X _⦋n⦌) → Δ[n] ⟶ TopCat.toSSet.obj X) i) ≫
            sSetTopAdj.counit.app X) :
      F.obj (TopCat.uliftFunctor.obj (TopCat.of (↑(_root_.stdSimplex ℝ (Fin (n + 1))) : Type))) ⟶ F.obj X)
⊢ CategoryStruct.comp (Y :=
      sigmaObj.{w, v, u} fun (x : TopCat.toSSet.obj X _⦋n⦌) ↦
        Functor.obj (Functor.obj (evaluation TopCat C) (SimplexCategory.toTop.{w} ^⦋n⦌)) F)
      (Sigma.ι.{w, v, u} (C := C)
          (fun (x : TopCat.toSSet.obj X _⦋n⦌) ↦
            Functor.obj (Functor.obj (evaluation TopCat C) (SimplexCategory.toTop.{w} ^⦋n⦌)) F)
          i :
        Functor.obj (Functor.obj (evaluation TopCat C) (SimplexCategory.toTop.{w} ^⦋n⦌)) F ⟶
          sigmaObj.{w, v, u} fun (x : TopCat.toSSet.obj X _⦋n⦌) ↦
            Functor.obj (Functor.obj (evaluation TopCat C) (SimplexCategory.toTop.{w} ^⦋n⦌)) F)
      (NatTrans.app (NatTrans.app (Adjunction.counit (singularChainComplexFunctorAdjunction C n)) F) X :
        (Functor.obj
                (Functor.obj (evaluation TopCat C) (SimplexCategory.toTop.{w} ^⦋n⦌) ⋙
                  Functor.obj (C := C ⥤ TopCat ⥤ HomologicalComplex.{v, u, 0} C (ComplexShape.down ℕ))
                    (Functor.obj Functor.postcompose₂ (eval C (ComplexShape.down ℕ) n)) (singularChainComplexFunctor C))
                F).obj
            X ⟶
          (Functor.obj (𝟭 (CategoryTheory.Functor.{w, v, w + 1, u} TopCat C)) F).obj X) =
    F.map
      (toTopSimplex.inv.app ⦋n⦌ ≫
        toTop.map ((Equiv.symm SSet.yonedaEquiv : (a : TopCat.toSSet.obj X _⦋n⦌) → Δ[n] ⟶ TopCat.toSSet.obj X) i) ≫
          sSetTopAdj.counit.app X)

Tactic:
dsimp [singularChainComplexFunctorAdjunction, Adjunction.ofNatIsoRight,
      Adjunction.equivHomsetRightOfNatIso, Adjunction.homEquiv,
      Adjunction.comp, singularChainComplexFunctor, SSet.chainComplexFunctor,
      SSet.chainComplexFunctorAdjunction]

Premises used: SSet.chainComplexFunctorAdjunction, SSet.chainComplexFunctor, AlgebraicTopology.singularChainComplexFunctorAdjunction, CategoryTheory.Adjunction.equivHomsetRightOfNatIso, CategoryTheory.Adjunction.homEquiv, CategoryTheory.Adjunction.comp, CategoryTheory.Adjunction.ofNatIsoRight, AlgebraicTopology.singularChainComplexFunctor