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₁ 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 φ)))
⊢ 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 ≫ φ.τ₂))
  (Quiver.Hom.op (CategoryStruct.comp (Y := S₂.cycles) (cyclesMap φ) S₂.iCycles))
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 φ)))
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))
⊢ 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 ≫ φ.τ₂)) (Quiver.Hom.op (S₁.iCycles ≫ φ.τ₂))
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
⊢ Eq (α := Opposite.op S₂.cycles ⟶ S₁.op.opcycles)
    (CategoryStruct.comp (Y := Opposite.op S₁.cycles) (Quiver.Hom.op (cyclesMap φ)) (Iso.inv S₁.opcyclesOpIso) :
      Opposite.op S₂.cycles ⟶ S₁.op.opcycles)
    (Iso.inv S₂.opcyclesOpIso ≫ opcyclesMap (opMap φ) : Opposite.op S₂.cycles ⟶ S₁.op.opcycles)
have rw : Eq (α := S₂.op.opcycles ⟶ S₁.op.opcycles)
  (CategoryStruct.comp (Y := Opposite.op S₂.cycles) (Iso.hom S₂.opcyclesOpIso)
      (CategoryStruct.comp (Y := Opposite.op S₁.cycles) (Quiver.Hom.op (cyclesMap φ)) (Iso.inv S₁.opcyclesOpIso)) :
    S₂.op.opcycles ⟶ S₁.op.opcycles)
  (CategoryStruct.comp (Y := Opposite.op S₂.cycles) (Iso.hom S₂.opcyclesOpIso)
      (Iso.inv S₂.opcyclesOpIso ≫ opcyclesMap (opMap φ)) :
    S₂.op.opcycles ⟶ S₁.op.opcycles)
Tactic: rw [← cancel_epi (S₂.opcyclesOpIso.hom), Iso.hom_inv_id_assoc,
    ← opcyclesOpIso_hom_naturality_assoc, Iso.hom_inv_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₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
inst_2 : S₁.HasLeftHomology
inst_3 : S₂.HasLeftHomology
rw :
  Eq (α := S₂.op.opcycles ⟶ S₁.op.opcycles)
    (CategoryStruct.comp (Y := Opposite.op S₂.cycles) (Iso.hom S₂.opcyclesOpIso)
        (CategoryStruct.comp (Y := Opposite.op S₁.cycles) (Quiver.Hom.op (cyclesMap φ)) (Iso.inv S₁.opcyclesOpIso)) :
      S₂.op.opcycles ⟶ S₁.op.opcycles)
    (CategoryStruct.comp (Y := Opposite.op S₂.cycles) (Iso.hom S₂.opcyclesOpIso)
        (Iso.inv S₂.opcyclesOpIso ≫ opcyclesMap (opMap φ)) :
      S₂.op.opcycles ⟶ S₁.op.opcycles)
⊢ Eq (α := Opposite.op S₂.cycles ⟶ S₁.op.opcycles)
    (CategoryStruct.comp (Y := Opposite.op S₁.cycles) (Quiver.Hom.op (cyclesMap φ)) (Iso.inv S₁.opcyclesOpIso) :
      Opposite.op S₂.cycles ⟶ S₁.op.opcycles)
    (Iso.inv S₂.opcyclesOpIso ≫ opcyclesMap (opMap φ) : Opposite.op S₂.cycles ⟶ S₁.op.opcycles)
have rw₁ : Eq (α := S₂.op.opcycles ⟶ S₁.op.opcycles)
  (CategoryStruct.comp (Y := Opposite.op S₂.cycles) (Iso.hom S₂.opcyclesOpIso)
      (CategoryStruct.comp (Y := Opposite.op S₁.cycles) (Quiver.Hom.op (cyclesMap φ)) (Iso.inv S₁.opcyclesOpIso)) :
    S₂.op.opcycles ⟶ S₁.op.opcycles)
  (opcyclesMap (opMap φ) : S₂.op.opcycles ⟶ S₁.op.opcycles)
Tactic: rw [← cancel_epi (S₂.opcyclesOpIso.hom), Iso.hom_inv_id_assoc,
    ← opcyclesOpIso_hom_naturality_assoc, Iso.hom_inv_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₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
inst_2 : S₁.HasLeftHomology
inst_3 : S₂.HasLeftHomology
rw :
  Eq (α := S₂.op.opcycles ⟶ S₁.op.opcycles)
    (CategoryStruct.comp (Y := Opposite.op S₂.cycles) (Iso.hom S₂.opcyclesOpIso)
        (CategoryStruct.comp (Y := Opposite.op S₁.cycles) (Quiver.Hom.op (cyclesMap φ)) (Iso.inv S₁.opcyclesOpIso)) :
      S₂.op.opcycles ⟶ S₁.op.opcycles)
    (CategoryStruct.comp (Y := Opposite.op S₂.cycles) (Iso.hom S₂.opcyclesOpIso)
        (Iso.inv S₂.opcyclesOpIso ≫ opcyclesMap (opMap φ)) :
      S₂.op.opcycles ⟶ S₁.op.opcycles)
rw₁ :
  Eq (α := S₂.op.opcycles ⟶ S₁.op.opcycles)
    (CategoryStruct.comp (Y := Opposite.op S₂.cycles) (Iso.hom S₂.opcyclesOpIso)
        (CategoryStruct.comp (Y := Opposite.op S₁.cycles) (Quiver.Hom.op (cyclesMap φ)) (Iso.inv S₁.opcyclesOpIso)) :
      S₂.op.opcycles ⟶ S₁.op.opcycles)
    (opcyclesMap (opMap φ) : S₂.op.opcycles ⟶ S₁.op.opcycles)
⊢ Eq (α := Opposite.op S₂.cycles ⟶ S₁.op.opcycles)
    (CategoryStruct.comp (Y := Opposite.op S₁.cycles) (Quiver.Hom.op (cyclesMap φ)) (Iso.inv S₁.opcyclesOpIso) :
      Opposite.op S₂.cycles ⟶ S₁.op.opcycles)
    (Iso.inv S₂.opcyclesOpIso ≫ opcyclesMap (opMap φ) : Opposite.op S₂.cycles ⟶ S₁.op.opcycles)
have rw₂ : Eq (α := S₂.op.opcycles ⟶ S₁.op.opcycles)
  (CategoryStruct.comp (Y := S₁.op.opcycles) (opcyclesMap (opMap φ) : S₂.op.opcycles ⟶ S₁.op.opcycles)
      (CategoryStruct.comp (Y := Opposite.op S₁.cycles) (Iso.hom S₁.opcyclesOpIso) (Iso.inv S₁.opcyclesOpIso) :
        S₁.op.opcycles ⟶ S₁.op.opcycles) :
    S₂.op.opcycles ⟶ S₁.op.opcycles)
  (opcyclesMap (opMap φ) : S₂.op.opcycles ⟶ S₁.op.opcycles)
Tactic: rw [← cancel_epi (S₂.opcyclesOpIso.hom), Iso.hom_inv_id_assoc,
    ← opcyclesOpIso_hom_naturality_assoc, Iso.hom_inv_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₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
inst_2 : S₁.HasLeftHomology
inst_3 : S₂.HasLeftHomology
rw :
  Eq (α := S₂.op.opcycles ⟶ S₁.op.opcycles)
    (CategoryStruct.comp (Y := Opposite.op S₂.cycles) (Iso.hom S₂.opcyclesOpIso)
        (CategoryStruct.comp (Y := Opposite.op S₁.cycles) (Quiver.Hom.op (cyclesMap φ)) (Iso.inv S₁.opcyclesOpIso)) :
      S₂.op.opcycles ⟶ S₁.op.opcycles)
    (CategoryStruct.comp (Y := Opposite.op S₂.cycles) (Iso.hom S₂.opcyclesOpIso)
        (Iso.inv S₂.opcyclesOpIso ≫ opcyclesMap (opMap φ)) :
      S₂.op.opcycles ⟶ S₁.op.opcycles)
rw₁ :
  Eq (α := S₂.op.opcycles ⟶ S₁.op.opcycles)
    (CategoryStruct.comp (Y := Opposite.op S₂.cycles) (Iso.hom S₂.opcyclesOpIso)
        (CategoryStruct.comp (Y := Opposite.op S₁.cycles) (Quiver.Hom.op (cyclesMap φ)) (Iso.inv S₁.opcyclesOpIso)) :
      S₂.op.opcycles ⟶ S₁.op.opcycles)
    (opcyclesMap (opMap φ) : S₂.op.opcycles ⟶ S₁.op.opcycles)
rw₂ :
  Eq (α := S₂.op.opcycles ⟶ S₁.op.opcycles)
    (CategoryStruct.comp (Y := S₁.op.opcycles) (opcyclesMap (opMap φ) : S₂.op.opcycles ⟶ S₁.op.opcycles)
        (CategoryStruct.comp (Y := Opposite.op S₁.cycles) (Iso.hom S₁.opcyclesOpIso) (Iso.inv S₁.opcyclesOpIso) :
          S₁.op.opcycles ⟶ S₁.op.opcycles) :
      S₂.op.opcycles ⟶ S₁.op.opcycles)
    (opcyclesMap (opMap φ) : S₂.op.opcycles ⟶ S₁.op.opcycles)
⊢ Eq (α := Opposite.op S₂.cycles ⟶ S₁.op.opcycles)
    (CategoryStruct.comp (Y := Opposite.op S₁.cycles) (Quiver.Hom.op (cyclesMap φ)) (Iso.inv S₁.opcyclesOpIso) :
      Opposite.op S₂.cycles ⟶ S₁.op.opcycles)
    (Iso.inv S₂.opcyclesOpIso ≫ opcyclesMap (opMap φ) : Opposite.op S₂.cycles ⟶ S₁.op.opcycles)
have rw₃ : Eq (α := S₂.op.opcycles ⟶ S₁.op.opcycles) (opcyclesMap (opMap φ) ≫ 𝟙 S₁.op.opcycles) (opcyclesMap (opMap φ))
Tactic: rw [← cancel_epi (S₂.opcyclesOpIso.hom), Iso.hom_inv_id_assoc,
    ← opcyclesOpIso_hom_naturality_assoc, Iso.hom_inv_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₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
inst_2 : S₁.HasLeftHomology
inst_3 : S₂.HasLeftHomology
rw :
  Eq (α := S₂.op.opcycles ⟶ S₁.op.opcycles)
    (CategoryStruct.comp (Y := Opposite.op S₂.cycles) (Iso.hom S₂.opcyclesOpIso)
        (CategoryStruct.comp (Y := Opposite.op S₁.cycles) (Quiver.Hom.op (cyclesMap φ)) (Iso.inv S₁.opcyclesOpIso)) :
      S₂.op.opcycles ⟶ S₁.op.opcycles)
    (CategoryStruct.comp (Y := Opposite.op S₂.cycles) (Iso.hom S₂.opcyclesOpIso)
        (Iso.inv S₂.opcyclesOpIso ≫ opcyclesMap (opMap φ)) :
      S₂.op.opcycles ⟶ S₁.op.opcycles)
rw₁ :
  Eq (α := S₂.op.opcycles ⟶ S₁.op.opcycles)
    (CategoryStruct.comp (Y := Opposite.op S₂.cycles) (Iso.hom S₂.opcyclesOpIso)
        (CategoryStruct.comp (Y := Opposite.op S₁.cycles) (Quiver.Hom.op (cyclesMap φ)) (Iso.inv S₁.opcyclesOpIso)) :
      S₂.op.opcycles ⟶ S₁.op.opcycles)
    (opcyclesMap (opMap φ) : S₂.op.opcycles ⟶ S₁.op.opcycles)
rw₂ :
  Eq (α := S₂.op.opcycles ⟶ S₁.op.opcycles)
    (CategoryStruct.comp (Y := S₁.op.opcycles) (opcyclesMap (opMap φ) : S₂.op.opcycles ⟶ S₁.op.opcycles)
        (CategoryStruct.comp (Y := Opposite.op S₁.cycles) (Iso.hom S₁.opcyclesOpIso) (Iso.inv S₁.opcyclesOpIso) :
          S₁.op.opcycles ⟶ S₁.op.opcycles) :
      S₂.op.opcycles ⟶ S₁.op.opcycles)
    (opcyclesMap (opMap φ) : S₂.op.opcycles ⟶ S₁.op.opcycles)
rw₃ : Eq (α := S₂.op.opcycles ⟶ S₁.op.opcycles) (opcyclesMap (opMap φ) ≫ 𝟙 S₁.op.opcycles) (opcyclesMap (opMap φ))
⊢ Eq (α := Opposite.op S₂.cycles ⟶ S₁.op.opcycles)
    (CategoryStruct.comp (Y := Opposite.op S₁.cycles) (Quiver.Hom.op (cyclesMap φ)) (Iso.inv S₁.opcyclesOpIso) :
      Opposite.op S₂.cycles ⟶ S₁.op.opcycles)
    (Iso.inv S₂.opcyclesOpIso ≫ opcyclesMap (opMap φ) : Opposite.op S₂.cycles ⟶ S₁.op.opcycles)
have rw₄ : Eq (α := S₂.op.opcycles ⟶ S₁.op.opcycles) (opcyclesMap (opMap φ)) (opcyclesMap (opMap φ))
Tactic: rw [← cancel_epi (S₂.opcyclesOpIso.hom), Iso.hom_inv_id_assoc,
    ← opcyclesOpIso_hom_naturality_assoc, Iso.hom_inv_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₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
inst_2 : S₁.HasRightHomology
inst_3 : S₂.HasRightHomology
⊢ 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)
have 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)
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_τ₂]
-- 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 (α := 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)
⊢ 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)
have 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)
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_τ₂]
-- 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 (α := 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)
⊢ 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)
have 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)
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_τ₂]
-- 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 (α := 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)
⊢ 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)
have 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)
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_τ₂]
-- 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 (α := 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)
⊢ 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)
have 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 φ).τ₂)
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_τ₂]