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