-- 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⦌
⊢ 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)
have 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)
Tactic: dsimp [singularChainComplexFunctorAdjunction, Adjunction.ofNatIsoRight,
      Adjunction.equivHomsetRightOfNatIso, Adjunction.homEquiv,
      Adjunction.comp, singularChainComplexFunctor, SSet.chainComplexFunctor,
      SSet.chainComplexFunctorAdjunction]