-- Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
inst_2 : S₁.HasLeftHomology
inst_3 : S₂.HasLeftHomology
rw :
  Eq (α := S₂.op.X₂ ⟶ Opposite.op S₁.cycles)
    (CategoryStruct.comp (Y := S₂.op.opcycles) S₂.op.pOpcycles (opcyclesMap (opMap φ) ≫ Iso.hom S₁.opcyclesOpIso))
    (CategoryStruct.comp (Y := S₂.op.opcycles) (S₂.op.pOpcycles : S₂.op.X₂ ⟶ S₂.op.opcycles)
      (CategoryStruct.comp (Y := Opposite.op S₂.cycles) (Iso.hom S₂.opcyclesOpIso) (Quiver.Hom.op (cyclesMap φ)) :
        S₂.op.opcycles ⟶ Opposite.op S₁.cycles))
rw₁ :
  Eq (α := S₂.op.X₂ ⟶ Opposite.op S₁.cycles) ((opMap φ).τ₂ ≫ S₁.op.pOpcycles ≫ Iso.hom S₁.opcyclesOpIso)
    (CategoryStruct.comp (Y := S₂.op.opcycles) (S₂.op.pOpcycles : S₂.op.X₂ ⟶ S₂.op.opcycles)
      (CategoryStruct.comp (Y := Opposite.op S₂.cycles) (Iso.hom S₂.opcyclesOpIso) (Quiver.Hom.op (cyclesMap φ)) :
        S₂.op.opcycles ⟶ Opposite.op S₁.cycles))
rw₂ :
  Eq (α := S₂.op.X₂ ⟶ Opposite.op S₁.cycles) (φ.τ₂.op ≫ S₁.op.pOpcycles ≫ Iso.hom S₁.opcyclesOpIso)
    (CategoryStruct.comp (Y := S₂.op.opcycles) (S₂.op.pOpcycles : S₂.op.X₂ ⟶ S₂.op.opcycles)
      (CategoryStruct.comp (Y := Opposite.op S₂.cycles) (Iso.hom S₂.opcyclesOpIso) (Quiver.Hom.op (cyclesMap φ)) :
        S₂.op.opcycles ⟶ Opposite.op S₁.cycles))
rw₃ :
  Eq (α := S₂.op.X₂ ⟶ Opposite.op S₁.cycles) (φ.τ₂.op ≫ Quiver.Hom.op S₁.iCycles)
    (CategoryStruct.comp (Y := S₂.op.opcycles) (S₂.op.pOpcycles : S₂.op.X₂ ⟶ S₂.op.opcycles)
      (CategoryStruct.comp (Y := Opposite.op S₂.cycles) (Iso.hom S₂.opcyclesOpIso) (Quiver.Hom.op (cyclesMap φ)) :
        S₂.op.opcycles ⟶ Opposite.op S₁.cycles))
rw₄ :
  Eq.{v_1 + 1} (α := S₂.op.X₂ ⟶ Opposite.op S₁.cycles) (φ.τ₂.op ≫ Quiver.Hom.op S₁.iCycles)
    (CategoryStruct.comp (Y := Opposite.op S₂.cycles) (Quiver.Hom.op S₂.iCycles) (Quiver.Hom.op (cyclesMap φ)))
rw₅ :
  Eq (α := S₂.op.X₂ ⟶ Opposite.op S₁.cycles) (Quiver.Hom.op (S₁.iCycles ≫ φ.τ₂))
    (CategoryStruct.comp (Y := Opposite.op S₂.cycles) (Quiver.Hom.op S₂.iCycles) (Quiver.Hom.op (cyclesMap φ)))
rw₆ :
  Eq (α := S₂.op.X₂ ⟶ Opposite.op S₁.cycles) (Quiver.Hom.op (S₁.iCycles ≫ φ.τ₂))
    (Quiver.Hom.op (CategoryStruct.comp (Y := S₂.cycles) (cyclesMap φ) S₂.iCycles))
rw₇ rw₈ :
  Eq (α := S₂.op.X₂ ⟶ Opposite.op S₁.cycles) (Quiver.Hom.op (S₁.iCycles ≫ φ.τ₂)) (Quiver.Hom.op (S₁.iCycles ≫ φ.τ₂))
⊢ Eq (α := S₂.op.opcycles ⟶ Opposite.op S₁.cycles)
    (opcyclesMap (opMap φ) ≫ Iso.hom S₁.opcyclesOpIso : S₂.op.opcycles ⟶ Opposite.op S₁.cycles)
    (CategoryStruct.comp (Y := Opposite.op S₂.cycles) (Iso.hom S₂.opcyclesOpIso) (Quiver.Hom.op (cyclesMap φ)) :
      S₂.op.opcycles ⟶ Opposite.op S₁.cycles)

Tactic:
rw [← cancel_epi S₂.op.pOpcycles, p_opcyclesMap_assoc, opMap_τ₂,
    op_pOpcycles_opcyclesOpIso_hom, op_pOpcycles_opcyclesOpIso_hom_assoc, ← op_comp,
    ← op_comp, cyclesMap_i]

Premises used: CategoryTheory.op_comp, CategoryTheory.ShortComplex.op_pOpcycles_opcyclesOpIso_hom, CategoryTheory.ShortComplex.op_pOpcycles_opcyclesOpIso_hom_assoc, CategoryTheory.ShortComplex.pOpcycles, CategoryTheory.ShortComplex.opMap_τ₂, CategoryTheory.ShortComplex.op, CategoryTheory.ShortComplex.p_opcyclesMap_assoc, CategoryTheory.ShortComplex.cyclesMap_i, CategoryTheory.cancel_epi