-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.RightHomology (goal)
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 (α := S₂.op.cycles ⟶ S₁.op.cycles)
    (CategoryStruct.comp (Y := Opposite.op S₁.opcycles) (cyclesMap (opMap φ) ≫ Iso.hom S₁.cyclesOpIso)
        (Iso.inv S₁.cyclesOpIso) :
      S₂.op.cycles ⟶ S₁.op.cycles)
    (CategoryStruct.comp (Y := Opposite.op S₁.opcycles)
        (CategoryStruct.comp (Y := Opposite.op S₂.opcycles) (Iso.hom S₂.cyclesOpIso) (Quiver.Hom.op (opcyclesMap φ)))
        (Iso.inv S₁.cyclesOpIso) :
      S₂.op.cycles ⟶ S₁.op.cycles)
rw₁ :
  Eq (α := S₂.op.cycles ⟶ S₁.op.cycles)
    (CategoryStruct.comp (Y := S₁.op.cycles) (cyclesMap (opMap φ) : S₂.op.cycles ⟶ S₁.op.cycles)
        (CategoryStruct.comp (Y := Opposite.op S₁.opcycles) (Iso.hom S₁.cyclesOpIso) (Iso.inv S₁.cyclesOpIso) :
          S₁.op.cycles ⟶ S₁.op.cycles) :
      S₂.op.cycles ⟶ S₁.op.cycles)
    (CategoryStruct.comp (Y := Opposite.op S₁.opcycles)
        (CategoryStruct.comp (Y := Opposite.op S₂.opcycles) (Iso.hom S₂.cyclesOpIso) (Quiver.Hom.op (opcyclesMap φ)))
        (Iso.inv S₁.cyclesOpIso) :
      S₂.op.cycles ⟶ S₁.op.cycles)
rw₂ :
  Eq (α := S₂.op.cycles ⟶ S₁.op.cycles)
    (CategoryStruct.comp (Y := S₁.op.cycles) (cyclesMap (opMap φ) : S₂.op.cycles ⟶ S₁.op.cycles)
        (CategoryStruct.comp (Y := Opposite.op S₁.opcycles) (Iso.hom S₁.cyclesOpIso) (Iso.inv S₁.cyclesOpIso) :
          S₁.op.cycles ⟶ S₁.op.cycles) :
      S₂.op.cycles ⟶ S₁.op.cycles)
    (CategoryStruct.comp (Y := Opposite.op S₂.opcycles) (Iso.hom S₂.cyclesOpIso)
        (CategoryStruct.comp (Y := Opposite.op S₁.opcycles) (Quiver.Hom.op (opcyclesMap φ)) (Iso.inv S₁.cyclesOpIso)) :
      S₂.op.cycles ⟶ S₁.op.cycles)
rw₃ :
  Eq (α := S₂.op.cycles ⟶ S₁.op.cycles) (cyclesMap (opMap φ) ≫ 𝟙 S₁.op.cycles : S₂.op.cycles ⟶ S₁.op.cycles)
    (CategoryStruct.comp (Y := Opposite.op S₂.opcycles) (Iso.hom S₂.cyclesOpIso)
        (CategoryStruct.comp (Y := Opposite.op S₁.opcycles) (Quiver.Hom.op (opcyclesMap φ)) (Iso.inv S₁.cyclesOpIso)) :
      S₂.op.cycles ⟶ S₁.op.cycles)
rw₄ :
  Eq (α := S₂.op.cycles ⟶ S₁.op.cycles) (cyclesMap (opMap φ) : S₂.op.cycles ⟶ S₁.op.cycles)
    (CategoryStruct.comp (Y := Opposite.op S₂.opcycles) (Iso.hom S₂.cyclesOpIso)
        (CategoryStruct.comp (Y := Opposite.op S₁.opcycles) (Quiver.Hom.op (opcyclesMap φ)) (Iso.inv S₁.cyclesOpIso)) :
      S₂.op.cycles ⟶ S₁.op.cycles)
⊢ Eq (α := S₂.op.cycles ⟶ Opposite.op S₁.opcycles)
    (cyclesMap (opMap φ) ≫ Iso.hom S₁.cyclesOpIso : S₂.op.cycles ⟶ Opposite.op S₁.opcycles)
    (CategoryStruct.comp (Y := Opposite.op S₂.opcycles) (Iso.hom S₂.cyclesOpIso) (Quiver.Hom.op (opcyclesMap φ)) :
      S₂.op.cycles ⟶ Opposite.op S₁.opcycles)
have rw₅ : Eq (α := S₂.op.cycles ⟶ S₁.op.cycles) (cyclesMap (opMap φ) : S₂.op.cycles ⟶ S₁.op.cycles)
  (CategoryStruct.comp (Y := Opposite.op S₂.opcycles) (Iso.hom S₂.cyclesOpIso)
      (Iso.inv S₂.cyclesOpIso ≫ cyclesMap (opMap φ)) :
    S₂.op.cycles ⟶ S₁.op.cycles)
Tactic: rw [← cancel_mono (S₁.cyclesOpIso).inv, assoc, assoc, Iso.hom_inv_id, comp_id,
    cyclesOpIso_inv_naturality, Iso.hom_inv_id_assoc]