-- 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₁.HasRightHomology
inst_3 : S₂.HasRightHomology
rw :
  Eq (α := Opposite.op S₂.opcycles ⟶ S₁.op.X₂)
    (CategoryStruct.comp (Y := S₁.op.cycles)
      (CategoryStruct.comp (Y := Opposite.op S₁.opcycles) (Quiver.Hom.op (opcyclesMap φ)) (Iso.inv S₁.cyclesOpIso) :
        Opposite.op S₂.opcycles ⟶ S₁.op.cycles)
      (S₁.op.iCycles : S₁.op.cycles ⟶ S₁.op.X₂))
    (CategoryStruct.comp (Y := S₁.op.cycles) (Iso.inv S₂.cyclesOpIso ≫ cyclesMap (opMap φ)) S₁.op.iCycles)
rw₁ :
  Eq (α := Opposite.op S₂.opcycles ⟶ S₁.op.X₂)
    (CategoryStruct.comp (Y := Opposite.op S₁.opcycles) (Quiver.Hom.op (opcyclesMap φ))
      (Iso.inv S₁.cyclesOpIso ≫ S₁.op.iCycles))
    (CategoryStruct.comp (Y := S₁.op.cycles) (Iso.inv S₂.cyclesOpIso ≫ cyclesMap (opMap φ)) S₁.op.iCycles)
rw₂ :
  Eq (α := Opposite.op S₂.opcycles ⟶ S₁.op.X₂)
    (CategoryStruct.comp (Y := Opposite.op S₁.opcycles) (Quiver.Hom.op (opcyclesMap φ))
      (Iso.inv S₁.cyclesOpIso ≫ S₁.op.iCycles))
    (Iso.inv S₂.cyclesOpIso ≫ CategoryStruct.comp (Y := S₁.op.cycles) (cyclesMap (opMap φ)) S₁.op.iCycles)
rw₃ :
  Eq (α := Opposite.op S₂.opcycles ⟶ S₁.op.X₂)
    (CategoryStruct.comp (Y := Opposite.op S₁.opcycles) (Quiver.Hom.op (opcyclesMap φ)) (Quiver.Hom.op S₁.pOpcycles))
    (Iso.inv S₂.cyclesOpIso ≫ CategoryStruct.comp (Y := S₁.op.cycles) (cyclesMap (opMap φ)) S₁.op.iCycles)
rw₄ :
  Eq (α := Opposite.op S₂.opcycles ⟶ S₁.op.X₂)
    (CategoryStruct.comp (Y := Opposite.op S₁.opcycles) (Quiver.Hom.op (opcyclesMap φ)) (Quiver.Hom.op S₁.pOpcycles))
    (Iso.inv S₂.cyclesOpIso ≫ S₂.op.iCycles ≫ (opMap φ).τ₂)
rw₅ :
  Eq (α := Opposite.op S₂.opcycles ⟶ S₁.op.X₂)
    (CategoryStruct.comp (Y := Opposite.op S₁.opcycles) (Quiver.Hom.op (opcyclesMap φ)) (Quiver.Hom.op S₁.pOpcycles))
    (Quiver.Hom.op S₂.pOpcycles ≫ (opMap φ).τ₂)
rw₆ :
  Eq (α := Opposite.op S₂.opcycles ⟶ S₁.op.X₂)
    (Quiver.Hom.op (CategoryStruct.comp (Y := S₁.opcycles) S₁.pOpcycles (opcyclesMap φ)))
    (Quiver.Hom.op S₂.pOpcycles ≫ (opMap φ).τ₂)
rw₇ :
  Eq (α := Opposite.op S₂.opcycles ⟶ S₁.op.X₂) (Quiver.Hom.op (φ.τ₂ ≫ S₂.pOpcycles))
    (Quiver.Hom.op S₂.pOpcycles ≫ (opMap φ).τ₂)
rw₈ :
  Eq (α := Opposite.op S₂.opcycles ⟶ S₁.op.X₂) (Quiver.Hom.op S₂.pOpcycles ≫ φ.τ₂.op)
    (Quiver.Hom.op S₂.pOpcycles ≫ (opMap φ).τ₂)
rw₉ rw₁₀ :
  Eq.{v_1 + 1} (α := Opposite.op S₂.opcycles ⟶ S₁.op.X₂) (Quiver.Hom.op S₂.pOpcycles ≫ φ.τ₂.op)
    (Quiver.Hom.op S₂.pOpcycles ≫ φ.τ₂.op)
⊢ Eq (α := Opposite.op S₂.opcycles ⟶ S₁.op.cycles)
    (CategoryStruct.comp (Y := Opposite.op S₁.opcycles) (Quiver.Hom.op (opcyclesMap φ)) (Iso.inv S₁.cyclesOpIso) :
      Opposite.op S₂.opcycles ⟶ S₁.op.cycles)
    (Iso.inv S₂.cyclesOpIso ≫ cyclesMap (opMap φ) : Opposite.op S₂.opcycles ⟶ S₁.op.cycles)

Tactic:
rw [← cancel_mono S₁.op.iCycles, assoc, assoc, cyclesOpIso_inv_op_iCycles, cyclesMap_i,
    cyclesOpIso_inv_op_iCycles_assoc, ← op_comp, p_opcyclesMap, op_comp, opMap_τ₂]

Premises used: CategoryTheory.ShortComplex.cyclesOpIso_inv_op_iCycles_assoc, CategoryTheory.Category.assoc, CategoryTheory.op_comp, CategoryTheory.cancel_mono, CategoryTheory.ShortComplex.opMap_τ₂, CategoryTheory.ShortComplex.op, CategoryTheory.ShortComplex.iCycles, CategoryTheory.ShortComplex.cyclesMap_i, CategoryTheory.ShortComplex.cyclesOpIso_inv_op_iCycles, CategoryTheory.ShortComplex.p_opcyclesMap