-- Lean 4 proof step from Mathlib.Algebra.Homology.SingleHomology (goal)
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))
⊢ 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))
have 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))
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]