-- 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} (α :=
    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)
have simp : 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)
  (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 (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⦌)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (sSetTopAdj.unit.app Δ[n]) (Opposite.op ⦋n⦌)) :
                (a : Δ[n] _⦋n⦌) → TopCat.toSSet.obj (toTop.obj Δ[n]) _⦋n⦌)
              ((Equiv.symm stdSimplex.objEquiv : (a : ⦋n⦌ ⟶ ⦋n⦌) → Δ[n] _⦋n⦌) (𝟙 ⦋n⦌) : Δ[n] _⦋n⦌) :
            TopCat.toSSet.obj (toTop.obj Δ[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)
  (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 (sSetTopAdj.unit.app Δ[n]) (Opposite.op ⦋n⦌) ≫
                NatTrans.app (TopCat.toSSet.map (toTopSimplex.hom.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: simp [stdSimplexToTop]