-- 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⦌
trans :
  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)
trans₁ :
  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.map i.down
⊢ 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 i.down

Tactic:
trans F.map (SSet.toTopSimplex.inv.app ⦋n⦌ ≫ SSet.toTop.map (SSet.yonedaEquiv.symm i) ≫
      sSetTopAdj.counit.app X)

Premises used: SSet.yonedaEquiv, SSet.toTop, CategoryTheory.Functor.map, CategoryTheory.Adjunction.counit, SimplexCategory.mk, SSet.toTopSimplex, sSetTopAdj, CategoryTheory.CategoryStruct.comp, Equiv.symm, DFunLike.coe, CategoryTheory.Iso.inv, CategoryTheory.NatTrans.app