-- 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 (α :=
    opcycles.{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)
    ((opcyclesMap (CategoryTheory.Functor.map (single C c j) f) j ≫ Iso.inv (singleObjOpcyclesSelfIso c j B)) ≫
      Iso.hom (singleObjOpcyclesSelfIso c j B))
    ((Iso.inv (singleObjOpcyclesSelfIso c j A) ≫ f) ≫ Iso.hom (singleObjOpcyclesSelfIso c j B))
rw₁ :
  Eq (α :=
    opcycles.{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)
    (opcyclesMap (CategoryTheory.Functor.map (single C c j) f) j ≫
      Iso.inv (singleObjOpcyclesSelfIso c j B) ≫ Iso.hom (singleObjOpcyclesSelfIso c j B))
    ((Iso.inv (singleObjOpcyclesSelfIso c j A) ≫ f) ≫ Iso.hom (singleObjOpcyclesSelfIso c j B))
rw₂ :
  Eq (α :=
    opcycles.{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)
    (opcyclesMap (CategoryTheory.Functor.map (single C c j) f) j ≫
      Iso.inv (singleObjOpcyclesSelfIso c j B) ≫ Iso.hom (singleObjOpcyclesSelfIso c j B))
    (Iso.inv (singleObjOpcyclesSelfIso c j A) ≫ f ≫ Iso.hom (singleObjOpcyclesSelfIso c j B))
rw₃ :
  opcyclesMap (CategoryTheory.Functor.map (single C c j) f) j ≫
      𝟙 (opcycles.{v, u, u_1} (Functor.obj (single C c j) B) j) =
    Iso.inv (singleObjOpcyclesSelfIso c j A) ≫ f ≫ Iso.hom (singleObjOpcyclesSelfIso c j B)
rw₄ :
  Eq (α :=
    opcycles.{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)
    (opcyclesMap (CategoryTheory.Functor.map (single C c j) f) j)
    (Iso.inv (singleObjOpcyclesSelfIso c j A) ≫ f ≫ Iso.hom (singleObjOpcyclesSelfIso c j B))
rw₅ :
  Eq (α :=
    opcycles.{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)
    (opcyclesMap (CategoryTheory.Functor.map (single C c j) f) j)
    (Iso.inv (singleObjOpcyclesSelfIso c j A) ≫
      Iso.hom (singleObjOpcyclesSelfIso c j A) ≫ opcyclesMap (CategoryTheory.Functor.map (single C c j) f) j)
rw₆ rw₇ :
  Eq (α :=
    opcycles.{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)
    (opcyclesMap (CategoryTheory.Functor.map (single C c j) f) j)
    (opcyclesMap (CategoryTheory.Functor.map (single C c j) f) j)
⊢ Eq (α := opcycles.{v, u, u_1} (Functor.obj (single C c j) A) j ⟶ B)
    (opcyclesMap (CategoryTheory.Functor.map (single C c j) f) j ≫ Iso.inv (singleObjOpcyclesSelfIso c j B))
    (Iso.inv (singleObjOpcyclesSelfIso c j A) ≫ f)

Tactic:
rw [← cancel_mono (singleObjOpcyclesSelfIso c j B).hom, assoc, assoc, Iso.inv_hom_id,
    comp_id, ← singleObjOpcyclesSelfIso_hom_naturality, Iso.inv_hom_id_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.inv_hom_id, CategoryTheory.cancel_mono, CategoryTheory.Category.comp_id, CategoryTheory.Iso.inv_hom_id_assoc, HomologicalComplex.singleObjOpcyclesSelfIso, CategoryTheory.Iso.hom, HomologicalComplex.singleObjOpcyclesSelfIso_hom_naturality