-- 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 (α :=
    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)
⊢ Eq (α := HomologicalComplex.homology (obj (homogeneousCochains.{u_1, u_2, u_3} R G) X) 0 ⟶ obj (invariants R G) Y)
    (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
          (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 ≫
        Iso.hom
          (TopModuleCat.ofIso
            (kerHomogeneousCochainsZeroEquiv R G X ((ComplexShape.up ℕ).next 0)
              continuousCohomologyZeroIso._proof_2))) ≫
      CategoryTheory.Functor.map (invariants R G) f)

Tactic:
rw [Category.assoc, ← Iso.inv_comp_eq]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.inv_comp_eq