-- 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 : ℕ
R : C
dsimp :
  Eq.{v + 1} (α :=
    R ⟶
      sigmaObj.{w, v, u}
        fun
          (x :
            TopCat.toSSet.obj
                (TopCat.uliftFunctor.obj (TopCat.of (↑(_root_.stdSimplex ℝ (Fin (n + 1))) : Type))) _⦋n⦌) ↦
        R)
    (CategoryStruct.comp (Y := sigmaObj.{w, v, u} fun (x : TopCat.toSSet.obj (toTop.obj Δ[n]) _⦋n⦌) ↦ R)
        (CategoryStruct.comp (Y := sigmaObj.{w, v, u} fun (x : Δ[n] _⦋n⦌) ↦ R)
          (Sigma.ι.{w, v, u} (β := Δ[n] _⦋n⦌) (C := C) (fun (x : Δ[n] _⦋n⦌) ↦ R)
            ((Equiv.symm stdSimplex.objEquiv : (a : ⦋n⦌ ⟶ ⦋n⦌) → Δ[n] _⦋n⦌) (𝟙 ⦋n⦌) : Δ[n] _⦋n⦌))
          ((𝟙 (sigmaObj.{w, v, u} fun (x : Δ[n] _⦋n⦌) ↦ R) ≫
              NatTrans.app
                  (NatTrans.app (Adjunction.unit (Adjunction.whiskerLeft C sSetTopAdj))
                    (Functor.obj
                      (Functor.obj (C := C ⥤ SSet ⥤ HomologicalComplex.{v, u, 0} C (ComplexShape.down ℕ))
                        (Functor.obj Functor.postcompose₂ (eval C (ComplexShape.down ℕ) n))
                        (Functor.obj (Functor.obj Functor.postcompose₂ (alternatingFaceMapComplex C))
                          (sigmaConst ⋙ SimplicialObject.whiskering (Type w) C)))
                      R))
                  Δ[n] ≫
                𝟙 (sigmaObj.{w, v, u} fun (x : TopCat.toSSet.obj (toTop.obj Δ[n]) _⦋n⦌) ↦ R)) ≫
            𝟙 (sigmaObj.{w, v, u} fun (x : TopCat.toSSet.obj (toTop.obj Δ[n]) _⦋n⦌) ↦ R)))
        (Sigma.map'
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
                (NatTrans.app (TopCat.toSSet.map (toTopSimplex.hom.app ⦋n⦌)) (Opposite.op ⦋n⦌))) :
            (a : TopCat.toSSet.obj (toTop.obj Δ[n]) _⦋n⦌) →
              TopCat.toSSet.obj
                  (TopCat.uliftFunctor.obj (TopCat.of (↑(_root_.stdSimplex ℝ (Fin (n + 1))) : Type))) _⦋n⦌)
          fun (x : TopCat.toSSet.obj (toTop.obj Δ[n]) _⦋n⦌) ↦ 𝟙 R) :
      R ⟶
        sigmaObj.{w, v, u}
          fun
            (x :
              TopCat.toSSet.obj
                  (TopCat.uliftFunctor.obj (TopCat.of (↑(_root_.stdSimplex ℝ (Fin (n + 1))) : Type))) _⦋n⦌) ↦
          R)
    (Sigma.ι.{w, v, u} (β :=
        TopCat.toSSet.obj (TopCat.uliftFunctor.obj (TopCat.of (↑(_root_.stdSimplex ℝ (Fin (n + 1))) : Type))) _⦋n⦌)
        (C := C)
        (fun
            (x :
              TopCat.toSSet.obj
                  (TopCat.uliftFunctor.obj (TopCat.of (↑(_root_.stdSimplex ℝ (Fin (n + 1))) : Type))) _⦋n⦌) ↦
          R)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (stdSimplexToTop.app ⦋n⦌) (Opposite.op ⦋n⦌)) :
              (a : Δ[n] _⦋n⦌) →
                TopCat.toSSet.obj
                    (TopCat.uliftFunctor.obj (TopCat.of (↑(_root_.stdSimplex ℝ (Fin (n + 1))) : Type))) _⦋n⦌)
            ((Equiv.symm stdSimplex.objEquiv : (a : ⦋n⦌ ⟶ ⦋n⦌) → Δ[n] _⦋n⦌) (𝟙 ⦋n⦌) : Δ[n] _⦋n⦌) :
          TopCat.toSSet.obj (TopCat.uliftFunctor.obj (TopCat.of (↑(_root_.stdSimplex ℝ (Fin (n + 1))) : Type))) _⦋n⦌) :
      R ⟶
        sigmaObj.{w, v, u}
          fun
            (x :
              TopCat.toSSet.obj
                  (TopCat.uliftFunctor.obj (TopCat.of (↑(_root_.stdSimplex ℝ (Fin (n + 1))) : Type))) _⦋n⦌) ↦
          R)
⊢ Eq.{v + 1} (α :=
    Functor.obj.{v, v, u, u} (𝟭 C) R ⟶
      Functor.obj.{v, v, u, u}
        (Functor.obj (C := C ⥤ TopCat ⥤ HomologicalComplex.{v, u, 0} C (ComplexShape.down ℕ))
            (Functor.obj Functor.postcompose₂ (eval C (ComplexShape.down ℕ) n)) (singularChainComplexFunctor C) ⋙
          Functor.obj (evaluation TopCat C) (SimplexCategory.toTop.{w} ^⦋n⦌))
        R)
    (NatTrans.app (Adjunction.unit (singularChainComplexFunctorAdjunction C n)) R)
    (Sigma.ι.{w, v, u} (β := (fun (X : Type w) ↦ X) ((SimplexCategory.toTop.{w} ⋙ TopCat.toSSet) ^⦋n⦌ _⦋n⦌)) (C := C)
      (fun (x : (fun (X : Type w) ↦ X) ((SimplexCategory.toTop.{w} ⋙ TopCat.toSSet) ^⦋n⦌ _⦋n⦌)) ↦ R)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (stdSimplexToTop.app ⦋n⦌) (Opposite.op ⦋n⦌)) :
            (a : (fun (X : Type w) ↦ X) (Δ[n] _⦋n⦌)) →
              (fun (X : Type w) ↦ X) ((SimplexCategory.toTop.{w} ⋙ TopCat.toSSet) ^⦋n⦌ _⦋n⦌))
          ((Equiv.symm stdSimplex.objEquiv : (a : Opposite.unop (Opposite.op ⦋n⦌) ⟶ ⦋n⦌) → Δ[n] _⦋n⦌) (𝟙 ⦋n⦌) :
            Δ[n] _⦋n⦌) :
        (fun (X : Type w) ↦ X) ((SimplexCategory.toTop.{w} ⋙ TopCat.toSSet) ^⦋n⦌ _⦋n⦌)))

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

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