-- Lean 4 proof step from Mathlib.AlgebraicTopology.SingularHomology.Basic (goal)
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)
⊢ 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
have 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
Tactic: trans F.map (SSet.toTopSimplex.inv.app ⦋n⦌ ≫ SSet.toTop.map (SSet.yonedaEquiv.symm i) ≫
      sSetTopAdj.counit.app X)