awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ShortComplex.{v_1, u_1} C
inst_2 : S.HasRightHomology
rw :
  CategoryStruct.comp (Y := S.op.cycles) (S.rightHomologyData.g'.op ≫ Iso.inv S.rightHomologyData.op.cyclesIso)
      S.op.iCycles =
    CategoryStruct.comp (Y := S.op.cycles) S.op.toCycles S.op.iCycles
rw₁ :
  S.rightHomologyData.g'.op ≫
      CategoryStruct.comp (Y := S.op.cycles) (Iso.inv S.rightHomologyData.op.cyclesIso) S.op.iCycles =
    CategoryStruct.comp (Y := S.op.cycles) S.op.toCycles S.op.iCycles
⊢ Eq (α := Opposite.op S.X₃ ⟶ S.op.cycles) (S.rightHomologyData.g'.op ≫ Iso.inv S.rightHomologyData.op.cyclesIso)
    S.op.toCycles
have rw₂ : S.rightHomologyData.g'.op ≫
    CategoryStruct.comp (Y := S.op.cycles) (Iso.inv S.rightHomologyData.op.cyclesIso) S.op.iCycles =
  S.op.f
Tactic: rw [← cancel_mono S.op.iCycles, assoc, toCycles_i,
    LeftHomologyData.cyclesIso_inv_comp_iCycles, RightHomologyData.op_i,
    ← op_comp, RightHomologyData.p_g', op_f]
-- 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 : ShortComplex.{v_1, u_1} C
inst_2 : S.HasRightHomology
rw :
  CategoryStruct.comp (Y := S.op.cycles) (S.rightHomologyData.g'.op ≫ Iso.inv S.rightHomologyData.op.cyclesIso)
      S.op.iCycles =
    CategoryStruct.comp (Y := S.op.cycles) S.op.toCycles S.op.iCycles
rw₁ :
  S.rightHomologyData.g'.op ≫
      CategoryStruct.comp (Y := S.op.cycles) (Iso.inv S.rightHomologyData.op.cyclesIso) S.op.iCycles =
    CategoryStruct.comp (Y := S.op.cycles) S.op.toCycles S.op.iCycles
rw₂ :
  S.rightHomologyData.g'.op ≫
      CategoryStruct.comp (Y := S.op.cycles) (Iso.inv S.rightHomologyData.op.cyclesIso) S.op.iCycles =
    S.op.f
⊢ Eq (α := Opposite.op S.X₃ ⟶ S.op.cycles) (S.rightHomologyData.g'.op ≫ Iso.inv S.rightHomologyData.op.cyclesIso)
    S.op.toCycles
have rw₃ : S.rightHomologyData.g'.op ≫ S.rightHomologyData.op.i = S.op.f
Tactic: rw [← cancel_mono S.op.iCycles, assoc, toCycles_i,
    LeftHomologyData.cyclesIso_inv_comp_iCycles, RightHomologyData.op_i,
    ← op_comp, RightHomologyData.p_g', op_f]
-- 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 : ShortComplex.{v_1, u_1} C
inst_2 : S.HasRightHomology
rw :
  CategoryStruct.comp (Y := S.op.cycles) (S.rightHomologyData.g'.op ≫ Iso.inv S.rightHomologyData.op.cyclesIso)
      S.op.iCycles =
    CategoryStruct.comp (Y := S.op.cycles) S.op.toCycles S.op.iCycles
rw₁ :
  S.rightHomologyData.g'.op ≫
      CategoryStruct.comp (Y := S.op.cycles) (Iso.inv S.rightHomologyData.op.cyclesIso) S.op.iCycles =
    CategoryStruct.comp (Y := S.op.cycles) S.op.toCycles S.op.iCycles
rw₂ :
  S.rightHomologyData.g'.op ≫
      CategoryStruct.comp (Y := S.op.cycles) (Iso.inv S.rightHomologyData.op.cyclesIso) S.op.iCycles =
    S.op.f
rw₃ : S.rightHomologyData.g'.op ≫ S.rightHomologyData.op.i = S.op.f
⊢ Eq (α := Opposite.op S.X₃ ⟶ S.op.cycles) (S.rightHomologyData.g'.op ≫ Iso.inv S.rightHomologyData.op.cyclesIso)
    S.op.toCycles
have rw₄ : S.rightHomologyData.g'.op ≫ S.rightHomologyData.p.op = S.op.f
Tactic: rw [← cancel_mono S.op.iCycles, assoc, toCycles_i,
    LeftHomologyData.cyclesIso_inv_comp_iCycles, RightHomologyData.op_i,
    ← op_comp, RightHomologyData.p_g', op_f]
-- 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 : ShortComplex.{v_1, u_1} C
inst_2 : S.HasRightHomology
rw :
  CategoryStruct.comp (Y := S.op.cycles) (S.rightHomologyData.g'.op ≫ Iso.inv S.rightHomologyData.op.cyclesIso)
      S.op.iCycles =
    CategoryStruct.comp (Y := S.op.cycles) S.op.toCycles S.op.iCycles
rw₁ :
  S.rightHomologyData.g'.op ≫
      CategoryStruct.comp (Y := S.op.cycles) (Iso.inv S.rightHomologyData.op.cyclesIso) S.op.iCycles =
    CategoryStruct.comp (Y := S.op.cycles) S.op.toCycles S.op.iCycles
rw₂ :
  S.rightHomologyData.g'.op ≫
      CategoryStruct.comp (Y := S.op.cycles) (Iso.inv S.rightHomologyData.op.cyclesIso) S.op.iCycles =
    S.op.f
rw₃ : S.rightHomologyData.g'.op ≫ S.rightHomologyData.op.i = S.op.f
rw₄ : S.rightHomologyData.g'.op ≫ S.rightHomologyData.p.op = S.op.f
⊢ Eq (α := Opposite.op S.X₃ ⟶ S.op.cycles) (S.rightHomologyData.g'.op ≫ Iso.inv S.rightHomologyData.op.cyclesIso)
    S.op.toCycles
have rw₅ : (S.rightHomologyData.p ≫ S.rightHomologyData.g').op = S.op.f
Tactic: rw [← cancel_mono S.op.iCycles, assoc, toCycles_i,
    LeftHomologyData.cyclesIso_inv_comp_iCycles, RightHomologyData.op_i,
    ← op_comp, RightHomologyData.p_g', op_f]
-- 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 : ShortComplex.{v_1, u_1} C
inst_2 : S.HasRightHomology
rw :
  CategoryStruct.comp (Y := S.op.cycles) (S.rightHomologyData.g'.op ≫ Iso.inv S.rightHomologyData.op.cyclesIso)
      S.op.iCycles =
    CategoryStruct.comp (Y := S.op.cycles) S.op.toCycles S.op.iCycles
rw₁ :
  S.rightHomologyData.g'.op ≫
      CategoryStruct.comp (Y := S.op.cycles) (Iso.inv S.rightHomologyData.op.cyclesIso) S.op.iCycles =
    CategoryStruct.comp (Y := S.op.cycles) S.op.toCycles S.op.iCycles
rw₂ :
  S.rightHomologyData.g'.op ≫
      CategoryStruct.comp (Y := S.op.cycles) (Iso.inv S.rightHomologyData.op.cyclesIso) S.op.iCycles =
    S.op.f
rw₃ : S.rightHomologyData.g'.op ≫ S.rightHomologyData.op.i = S.op.f
rw₄ : S.rightHomologyData.g'.op ≫ S.rightHomologyData.p.op = S.op.f
rw₅ : (S.rightHomologyData.p ≫ S.rightHomologyData.g').op = S.op.f
⊢ Eq (α := Opposite.op S.X₃ ⟶ S.op.cycles) (S.rightHomologyData.g'.op ≫ Iso.inv S.rightHomologyData.op.cyclesIso)
    S.op.toCycles
have rw₆ : S.g.op = S.op.f
Tactic: rw [← cancel_mono S.op.iCycles, assoc, toCycles_i,
    LeftHomologyData.cyclesIso_inv_comp_iCycles, RightHomologyData.op_i,
    ← op_comp, RightHomologyData.p_g', op_f]
-- 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 : ShortComplex.{v_1, u_1} C
inst_2 : S.HasRightHomology
rw :
  CategoryStruct.comp (Y := S.op.cycles) (S.rightHomologyData.g'.op ≫ Iso.inv S.rightHomologyData.op.cyclesIso)
      S.op.iCycles =
    CategoryStruct.comp (Y := S.op.cycles) S.op.toCycles S.op.iCycles
rw₁ :
  S.rightHomologyData.g'.op ≫
      CategoryStruct.comp (Y := S.op.cycles) (Iso.inv S.rightHomologyData.op.cyclesIso) S.op.iCycles =
    CategoryStruct.comp (Y := S.op.cycles) S.op.toCycles S.op.iCycles
rw₂ :
  S.rightHomologyData.g'.op ≫
      CategoryStruct.comp (Y := S.op.cycles) (Iso.inv S.rightHomologyData.op.cyclesIso) S.op.iCycles =
    S.op.f
rw₃ : S.rightHomologyData.g'.op ≫ S.rightHomologyData.op.i = S.op.f
rw₄ : S.rightHomologyData.g'.op ≫ S.rightHomologyData.p.op = S.op.f
rw₅ : (S.rightHomologyData.p ≫ S.rightHomologyData.g').op = S.op.f
rw₆ : S.g.op = S.op.f
⊢ Eq (α := Opposite.op S.X₃ ⟶ S.op.cycles) (S.rightHomologyData.g'.op ≫ Iso.inv S.rightHomologyData.op.cyclesIso)
    S.op.toCycles
have rw₇ : S.g.op = S.g.op
Tactic: rw [← cancel_mono S.op.iCycles, assoc, toCycles_i,
    LeftHomologyData.cyclesIso_inv_comp_iCycles, RightHomologyData.op_i,
    ← op_comp, RightHomologyData.p_g', op_f]
-- 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 : ShortComplex.{v_1, u_1} C
inst_2 : S.HasLeftHomology
⊢ Eq (α := S.op.X₂ ⟶ Opposite.op S.cycles) (S.op.pOpcycles ≫ Iso.hom S.opcyclesOpIso) (Quiver.Hom.op S.iCycles)
have dsimp : CategoryStruct.comp (Y := S.op.opcycles) S.op.pOpcycles (Iso.hom S.leftHomologyData.op.opcyclesIso) =
  Quiver.Hom.op S.iCycles
Tactic: dsimp [opcyclesOpIso]
-- 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 : ShortComplex.{v_1, u_1} C
inst_2 : S.HasLeftHomology
⊢ CategoryStruct.comp (Y := S.op.opcycles) S.op.pOpcycles (Iso.hom S.leftHomologyData.op.opcyclesIso) =
    Quiver.Hom.op S.iCycles
have rw : S.leftHomologyData.op.p = Quiver.Hom.op S.iCycles
Tactic: rw [← S.leftHomologyData.op.p_comp_opcyclesIso_inv, assoc,
    Iso.inv_hom_id, comp_id]
-- 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 : ShortComplex.{v_1, u_1} C
inst_2 : S.HasRightHomology
⊢ Eq (α := Opposite.op S.opcycles ⟶ S.op.X₂) (Iso.inv S.cyclesOpIso ≫ S.op.iCycles) (Quiver.Hom.op S.pOpcycles)
have dsimp : CategoryStruct.comp (Y := S.op.cycles) (Iso.inv S.rightHomologyData.op.cyclesIso) S.op.iCycles =
  Quiver.Hom.op S.pOpcycles
Tactic: dsimp [cyclesOpIso]
-- 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 : ShortComplex.{v_1, u_1} C
inst_2 : S.HasRightHomology
⊢ CategoryStruct.comp (Y := S.op.cycles) (Iso.inv S.rightHomologyData.op.cyclesIso) S.op.iCycles =
    Quiver.Hom.op S.pOpcycles
have rw : S.rightHomologyData.op.i = Quiver.Hom.op S.pOpcycles
Tactic: rw [← S.rightHomologyData.op.cyclesIso_hom_comp_i, Iso.inv_hom_id_assoc]
-- 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₁.HasLeftHomology
inst_3 : S₂.HasLeftHomology
⊢ 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)
have 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))
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]
-- 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₁.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))
⊢ 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)
have 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))
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]
-- 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₁.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))
⊢ 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)
have 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))
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]
-- 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₁.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))
⊢ 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)
have 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))
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]
-- 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₁.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))
⊢ 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)
have 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 φ)))
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]
-- 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₁.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 φ)))
⊢ 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)
have 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 φ)))
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]