-- Module: Mathlib.Algebra.Category.ContinuousCohomology.Basic
Goal:
R : Type u_1
G : Type u_2
inst : CommRing R
inst_1 : Group G
inst_2 : TopologicalSpace R
inst_3 : TopologicalSpace G
inst_4 : IsTopologicalGroup G
X Y : Action (TopModuleCat R) G
f : X ⟶ Y
rw :
  Eq (α :=
    (LeftHomologyData.ofIsLimitKernelFork (HomologicalComplex.sc (obj (homogeneousCochains.{u_1, u_2, u_3} R G) X) 0) ⋯
          (Limits.KernelFork.ofι
            (TopModuleCat.kerι ((obj (homogeneousCochains.{u_1, u_2, u_3} R G) X).d 0 ((ComplexShape.up ℕ).next 0))) ⋯)
          (TopModuleCat.isLimitKer
            ((obj (homogeneousCochains.{u_1, u_2, u_3} R G) X).d 0 ((ComplexShape.up ℕ).next 0)))).K ⟶
      obj (invariants R G) Y)
    (cyclesMap'
        (CategoryTheory.Functor.map (HomologicalComplex.shortComplexFunctor (TopModuleCat R) (ComplexShape.up ℕ) 0)
          (CategoryTheory.Functor.map (homogeneousCochains.{u_1, u_2, u_3} R G) f))
        (LeftHomologyData.ofIsLimitKernelFork
          (HomologicalComplex.sc (obj (homogeneousCochains.{u_1, u_2, u_3} R G) X) 0) ⋯
          (Limits.KernelFork.ofι
            (TopModuleCat.kerι ((obj (homogeneousCochains.{u_1, u_2, u_3} R G) X).d 0 ((ComplexShape.up ℕ).next 0))) ⋯)
          (TopModuleCat.isLimitKer
            ((obj (homogeneousCochains.{u_1, u_2, u_3} R G) X).d 0 ((ComplexShape.up ℕ).next 0))))
        (LeftHomologyData.ofIsLimitKernelFork
          (HomologicalComplex.sc (obj (homogeneousCochains.{u_1, u_2, u_3} R G) Y) 0) ⋯
          (Limits.KernelFork.ofι
            (TopModuleCat.kerι ((obj (homogeneousCochains.{u_1, u_2, u_3} R G) Y).d 0 ((ComplexShape.up ℕ).next 0))) ⋯)
          (TopModuleCat.isLimitKer
            ((obj (homogeneousCochains.{u_1, u_2, u_3} R G) Y).d 0 ((ComplexShape.up ℕ).next 0)))) ≫
      (LeftHomologyData.ofIsLimitKernelFork (HomologicalComplex.sc (obj (homogeneousCochains.{u_1, u_2, u_3} R G) Y) 0)
            ⋯
            (Limits.KernelFork.ofι
              (TopModuleCat.kerι ((obj (homogeneousCochains.{u_1, u_2, u_3} R G) Y).d 0 ((ComplexShape.up ℕ).next 0)))
              ⋯)
            (TopModuleCat.isLimitKer
              ((obj (homogeneousCochains.{u_1, u_2, u_3} R G) Y).d 0 ((ComplexShape.up ℕ).next 0)))).π ≫
        Iso.hom
          (TopModuleCat.ofIso
            (kerHomogeneousCochainsZeroEquiv R G Y ((ComplexShape.up ℕ).next 0) continuousCohomologyZeroIso._proof_2)))
    ((LeftHomologyData.ofIsLimitKernelFork (HomologicalComplex.sc (obj (homogeneousCochains.{u_1, u_2, u_3} R G) X) 0) ⋯
          (Limits.KernelFork.ofι
            (TopModuleCat.kerι ((obj (homogeneousCochains.{u_1, u_2, u_3} R G) X).d 0 ((ComplexShape.up ℕ).next 0))) ⋯)
          (TopModuleCat.isLimitKer
            ((obj (homogeneousCochains.{u_1, u_2, u_3} R G) X).d 0 ((ComplexShape.up ℕ).next 0)))).π ≫
      Iso.hom
          (TopModuleCat.ofIso
            (kerHomogeneousCochainsZeroEquiv R G X ((ComplexShape.up ℕ).next 0) continuousCohomologyZeroIso._proof_2)) ≫
        CategoryTheory.Functor.map (invariants R G) f)
⊢ Eq (α :=
    TopModuleCat.ker (M := (obj (homogeneousCochains.{u_1, u_2, u_3} R G) X).X 0) (N :=
        (obj (homogeneousCochains.{u_1, u_2, u_3} R G) X).X ((ComplexShape.up ℕ).next 0))
        ((obj (homogeneousCochains.{u_1, u_2, u_3} R G) X).d 0 ((ComplexShape.up ℕ).next 0)) ⟶
      obj (invariants R G) Y)
    (CategoryStruct.comp (Y := HomologicalComplex.homology (obj (homogeneousCochains.{u_1, u_2, u_3} R G) X) 0)
      (Iso.inv
        (LeftHomologyData.ofIsLimitKernelFork
            (HomologicalComplex.sc (obj (homogeneousCochains.{u_1, u_2, u_3} R G) X) 0) ⋯
            (Limits.KernelFork.ofι
              (TopModuleCat.kerι ((obj (homogeneousCochains.{u_1, u_2, u_3} R G) X).d 0 ((ComplexShape.up ℕ).next 0)))
              ⋯)
            (TopModuleCat.isLimitKer
              ((obj (homogeneousCochains.{u_1, u_2, u_3} R G) X).d 0 ((ComplexShape.up ℕ).next 0)))).homologyIso)
      (CategoryStruct.comp (Y := HomologicalComplex.homology (obj (homogeneousCochains.{u_1, u_2, u_3} R G) Y) 0)
        (homologyMap
          (CategoryTheory.Functor.map (HomologicalComplex.shortComplexFunctor (TopModuleCat R) (ComplexShape.up ℕ) 0)
            (CategoryTheory.Functor.map (homogeneousCochains.{u_1, u_2, u_3} R G) f)))
        (Iso.hom
            (LeftHomologyData.ofIsLimitKernelFork
                (HomologicalComplex.sc (obj (homogeneousCochains.{u_1, u_2, u_3} R G) Y) 0) ⋯
                (Limits.KernelFork.ofι
                  (TopModuleCat.kerι
                    ((obj (homogeneousCochains.{u_1, u_2, u_3} R G) Y).d 0 ((ComplexShape.up ℕ).next 0)))
                  ⋯)
                (TopModuleCat.isLimitKer
                  ((obj (homogeneousCochains.{u_1, u_2, u_3} R G) Y).d 0 ((ComplexShape.up ℕ).next 0)))).homologyIso ≫
          Iso.hom
            (TopModuleCat.ofIso
              (kerHomogeneousCochainsZeroEquiv R G Y ((ComplexShape.up ℕ).next 0)
                continuousCohomologyZeroIso._proof_2)))))
    (Iso.hom
        (TopModuleCat.ofIso
          (kerHomogeneousCochainsZeroEquiv R G X ((ComplexShape.up ℕ).next 0) continuousCohomologyZeroIso._proof_2)) ≫
      CategoryTheory.Functor.map (invariants R G) f)

Tactic:
rw [LeftHomologyData.leftHomologyIso_inv_naturality_assoc, Iso.inv_hom_id_assoc,
    ← cancel_epi (LeftHomologyData.π _), leftHomologyπ_naturality'_assoc]

Premises used: CategoryTheory.Iso.inv_hom_id_assoc, CategoryTheory.ShortComplex.leftHomologyπ_naturality'_assoc, CategoryTheory.ShortComplex.LeftHomologyData.leftHomologyIso_inv_naturality_assoc, CategoryTheory.ShortComplex.LeftHomologyData.π, CategoryTheory.cancel_epi