-- Module: Mathlib.Algebra.Homology.SingleHomology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasZeroObject.{v, u} C
ι : Type u_1
inst_3 : DecidableEq ι
c : ComplexShape ι
j : ι
A B : C
f : A ⟶ B
rw :
  Eq (α := cycles.{v, u, u_1} (Functor.obj (single C c j) A) j ⟶ opcycles.{v, u, u_1} (Functor.obj (single C c j) B) j)
    (Iso.hom (singleObjCyclesSelfIso c j A) ≫
      Iso.hom (singleObjOpcyclesSelfIso c j A) ≫ opcyclesMap (CategoryTheory.Functor.map (single C c j) f) j)
    (Iso.hom (singleObjCyclesSelfIso c j A) ≫ f ≫ Iso.hom (singleObjOpcyclesSelfIso c j B))
rw₁ :
  Eq (α := cycles.{v, u, u_1} (Functor.obj (single C c j) A) j ⟶ opcycles.{v, u, u_1} (Functor.obj (single C c j) B) j)
    (iCycles (Functor.obj (single C c j) A) j ≫
      CategoryStruct.comp (Y := opcycles.{v, u, u_1} (Functor.obj (single C c j) A) j)
        (pOpcycles (Functor.obj (single C c j) A) j) (opcyclesMap (CategoryTheory.Functor.map (single C c j) f) j))
    (Iso.hom (singleObjCyclesSelfIso c j A) ≫ f ≫ Iso.hom (singleObjOpcyclesSelfIso c j B))
rw₂ :
  Eq (α := cycles.{v, u, u_1} (Functor.obj (single C c j) A) j ⟶ opcycles.{v, u, u_1} (Functor.obj (single C c j) B) j)
    (iCycles (Functor.obj (single C c j) A) j ≫
      Hom.f (CategoryTheory.Functor.map (single C c j) f) j ≫ pOpcycles (Functor.obj (single C c j) B) j)
    (Iso.hom (singleObjCyclesSelfIso c j A) ≫ f ≫ Iso.hom (singleObjOpcyclesSelfIso c j B))
rw₃ :
  Eq (α := cycles.{v, u, u_1} (Functor.obj (single C c j) A) j ⟶ opcycles.{v, u, u_1} (Functor.obj (single C c j) B) j)
    (iCycles (Functor.obj (single C c j) A) j ≫
      (Iso.hom (singleObjXSelf c j A) ≫ f ≫ Iso.inv (singleObjXSelf c j B)) ≫
        pOpcycles (Functor.obj (single C c j) B) j)
    (Iso.hom (singleObjCyclesSelfIso c j A) ≫ f ≫ Iso.hom (singleObjOpcyclesSelfIso c j B))
rw₄ :
  Eq (α := cycles.{v, u, u_1} (Functor.obj (single C c j) A) j ⟶ opcycles.{v, u, u_1} (Functor.obj (single C c j) B) j)
    (iCycles (Functor.obj (single C c j) A) j ≫
      Iso.hom (singleObjXSelf c j A) ≫
        (f ≫ Iso.inv (singleObjXSelf c j B)) ≫ pOpcycles (Functor.obj (single C c j) B) j)
    (Iso.hom (singleObjCyclesSelfIso c j A) ≫ f ≫ Iso.hom (singleObjOpcyclesSelfIso c j B))
rw₅ :
  Eq (α := cycles.{v, u, u_1} (Functor.obj (single C c j) A) j ⟶ opcycles.{v, u, u_1} (Functor.obj (single C c j) B) j)
    (iCycles (Functor.obj (single C c j) A) j ≫
      Iso.hom (singleObjXSelf c j A) ≫ f ≫ Iso.inv (singleObjXSelf c j B) ≫ pOpcycles (Functor.obj (single C c j) B) j)
    (Iso.hom (singleObjCyclesSelfIso c j A) ≫ f ≫ Iso.hom (singleObjOpcyclesSelfIso c j B))
rw₆ :
  Eq (α := cycles.{v, u, u_1} (Functor.obj (single C c j) A) j ⟶ opcycles.{v, u, u_1} (Functor.obj (single C c j) B) j)
    (iCycles (Functor.obj (single C c j) A) j ≫
      Iso.hom (singleObjXSelf c j A) ≫ f ≫ Iso.inv (singleObjXSelf c j B) ≫ pOpcycles (Functor.obj (single C c j) B) j)
    ((iCycles (Functor.obj (single C c j) A) j ≫ Iso.hom (singleObjXSelf c j A)) ≫
      f ≫ Iso.hom (singleObjOpcyclesSelfIso c j B))
rw₇ :
  Eq (α := cycles.{v, u, u_1} (Functor.obj (single C c j) A) j ⟶ opcycles.{v, u, u_1} (Functor.obj (single C c j) B) j)
    (iCycles (Functor.obj (single C c j) A) j ≫
      Iso.hom (singleObjXSelf c j A) ≫ f ≫ Iso.inv (singleObjXSelf c j B) ≫ pOpcycles (Functor.obj (single C c j) B) j)
    ((iCycles (Functor.obj (single C c j) A) j ≫ Iso.hom (singleObjXSelf c j A)) ≫
      f ≫ Iso.inv (singleObjXSelf c j B) ≫ pOpcycles (Functor.obj (single C c j) B) j)
rw₈ rw₉ :
  Eq (α := cycles.{v, u, u_1} (Functor.obj (single C c j) A) j ⟶ opcycles.{v, u, u_1} (Functor.obj (single C c j) B) j)
    (iCycles (Functor.obj (single C c j) A) j ≫
      Iso.hom (singleObjXSelf c j A) ≫ f ≫ Iso.inv (singleObjXSelf c j B) ≫ pOpcycles (Functor.obj (single C c j) B) j)
    (iCycles (Functor.obj (single C c j) A) j ≫
      Iso.hom (singleObjXSelf c j A) ≫ f ≫ Iso.inv (singleObjXSelf c j B) ≫ pOpcycles (Functor.obj (single C c j) B) j)
⊢ Eq (α := A ⟶ opcycles.{v, u, u_1} (Functor.obj (single C c j) B) j)
    (Iso.hom (singleObjOpcyclesSelfIso c j A) ≫ opcyclesMap (CategoryTheory.Functor.map (single C c j) f) j)
    (f ≫ Iso.hom (singleObjOpcyclesSelfIso c j B))

Tactic:
rw [← cancel_epi (singleObjCyclesSelfIso c j A).hom,
    singleObjCyclesSelfIso_hom_singleObjOpcyclesSelfIso_hom_assoc, p_opcyclesMap,
    single_map_f_self, assoc, assoc, singleObjCyclesSelfIso_hom,
    singleObjOpcyclesSelfIso_hom, assoc]

Premises used: HomologicalComplex.singleObjCyclesSelfIso_hom_singleObjOpcyclesSelfIso_hom_assoc, CategoryTheory.Category.assoc, HomologicalComplex.singleObjOpcyclesSelfIso_hom, HomologicalComplex.singleObjCyclesSelfIso, HomologicalComplex.p_opcyclesMap, HomologicalComplex.single_map_f_self, CategoryTheory.cancel_epi, CategoryTheory.Iso.hom, HomologicalComplex.singleObjCyclesSelfIso_hom