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₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
e : S₁ ≅ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
rw : opcyclesMap' (e.hom ≫ e.inv) h₁ h₁ = 𝟙 h₁.Q
rw₁ : opcyclesMap' (𝟙 S₁) h₁ h₁ = 𝟙 h₁.Q
⊢ opcyclesMap' e.hom h₁ h₂ ≫ opcyclesMap' e.inv h₂ h₁ = 𝟙 h₁.Q
have rw₂ : Eq.{v_1 + 1} (α := h₁.Q ⟶ h₁.Q) (𝟙 h₁.Q) (𝟙 h₁.Q)
Tactic: rw [← opcyclesMap'_comp, e.hom_inv_id, opcyclesMap'_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₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
e : S₁ ≅ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
⊢ opcyclesMap' e.inv h₂ h₁ ≫ opcyclesMap' e.hom h₁ h₂ = 𝟙 h₂.Q
have rw : opcyclesMap' (e.inv ≫ e.hom) h₂ h₂ = 𝟙 h₂.Q
Tactic: rw [← opcyclesMap'_comp, e.inv_hom_id, opcyclesMap'_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₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
e : S₁ ≅ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
rw : opcyclesMap' (e.inv ≫ e.hom) h₂ h₂ = 𝟙 h₂.Q
⊢ opcyclesMap' e.inv h₂ h₁ ≫ opcyclesMap' e.hom h₁ h₂ = 𝟙 h₂.Q
have rw₁ : opcyclesMap' (𝟙 S₂) h₂ h₂ = 𝟙 h₂.Q
Tactic: rw [← opcyclesMap'_comp, e.inv_hom_id, opcyclesMap'_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₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
e : S₁ ≅ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
rw : opcyclesMap' (e.inv ≫ e.hom) h₂ h₂ = 𝟙 h₂.Q
rw₁ : opcyclesMap' (𝟙 S₂) h₂ h₂ = 𝟙 h₂.Q
⊢ opcyclesMap' e.inv h₂ h₁ ≫ opcyclesMap' e.hom h₁ h₂ = 𝟙 h₂.Q
have rw₂ : Eq.{v_1 + 1} (α := h₂.Q ⟶ h₂.Q) (𝟙 h₂.Q) (𝟙 h₂.Q)
Tactic: rw [← opcyclesMap'_comp, e.inv_hom_id, opcyclesMap'_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₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
e : S₁ ≅ S₂
inst_2 : S₁.HasRightHomology
inst_3 : S₂.HasRightHomology
⊢ CategoryStruct.comp (Y := S₂.rightHomology) (rightHomologyMap e.hom) (rightHomologyMap e.inv) = 𝟙 S₁.rightHomology
have rw : rightHomologyMap (e.hom ≫ e.inv) = 𝟙 S₁.rightHomology
Tactic: rw [← rightHomologyMap_comp, e.hom_inv_id, rightHomologyMap_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₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
e : S₁ ≅ S₂
inst_2 : S₁.HasRightHomology
inst_3 : S₂.HasRightHomology
rw : rightHomologyMap (e.hom ≫ e.inv) = 𝟙 S₁.rightHomology
⊢ CategoryStruct.comp (Y := S₂.rightHomology) (rightHomologyMap e.hom) (rightHomologyMap e.inv) = 𝟙 S₁.rightHomology
have rw₁ : rightHomologyMap (𝟙 S₁) = 𝟙 S₁.rightHomology
Tactic: rw [← rightHomologyMap_comp, e.hom_inv_id, rightHomologyMap_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₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
e : S₁ ≅ S₂
inst_2 : S₁.HasRightHomology
inst_3 : S₂.HasRightHomology
rw : rightHomologyMap (e.hom ≫ e.inv) = 𝟙 S₁.rightHomology
rw₁ : rightHomologyMap (𝟙 S₁) = 𝟙 S₁.rightHomology
⊢ CategoryStruct.comp (Y := S₂.rightHomology) (rightHomologyMap e.hom) (rightHomologyMap e.inv) = 𝟙 S₁.rightHomology
have rw₂ : Eq.{v_1 + 1} (α := S₁.rightHomology ⟶ S₁.rightHomology) (𝟙 S₁.rightHomology) (𝟙 S₁.rightHomology)
Tactic: rw [← rightHomologyMap_comp, e.hom_inv_id, rightHomologyMap_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₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
e : S₁ ≅ S₂
inst_2 : S₁.HasRightHomology
inst_3 : S₂.HasRightHomology
⊢ CategoryStruct.comp (Y := S₁.rightHomology) (rightHomologyMap e.inv) (rightHomologyMap e.hom) = 𝟙 S₂.rightHomology
have rw : rightHomologyMap (e.inv ≫ e.hom) = 𝟙 S₂.rightHomology
Tactic: rw [← rightHomologyMap_comp, e.inv_hom_id, rightHomologyMap_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₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
e : S₁ ≅ S₂
inst_2 : S₁.HasRightHomology
inst_3 : S₂.HasRightHomology
rw : rightHomologyMap (e.inv ≫ e.hom) = 𝟙 S₂.rightHomology
⊢ CategoryStruct.comp (Y := S₁.rightHomology) (rightHomologyMap e.inv) (rightHomologyMap e.hom) = 𝟙 S₂.rightHomology
have rw₁ : rightHomologyMap (𝟙 S₂) = 𝟙 S₂.rightHomology
Tactic: rw [← rightHomologyMap_comp, e.inv_hom_id, rightHomologyMap_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₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
e : S₁ ≅ S₂
inst_2 : S₁.HasRightHomology
inst_3 : S₂.HasRightHomology
rw : rightHomologyMap (e.inv ≫ e.hom) = 𝟙 S₂.rightHomology
rw₁ : rightHomologyMap (𝟙 S₂) = 𝟙 S₂.rightHomology
⊢ CategoryStruct.comp (Y := S₁.rightHomology) (rightHomologyMap e.inv) (rightHomologyMap e.hom) = 𝟙 S₂.rightHomology
have rw₂ : Eq.{v_1 + 1} (α := S₂.rightHomology ⟶ S₂.rightHomology) (𝟙 S₂.rightHomology) (𝟙 S₂.rightHomology)
Tactic: rw [← rightHomologyMap_comp, e.inv_hom_id, rightHomologyMap_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₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
e : S₁ ≅ S₂
inst_2 : S₁.HasRightHomology
inst_3 : S₂.HasRightHomology
⊢ CategoryStruct.comp (Y := S₂.opcycles) (opcyclesMap e.hom) (opcyclesMap e.inv) = 𝟙 S₁.opcycles
have rw : opcyclesMap (e.hom ≫ e.inv) = 𝟙 S₁.opcycles
Tactic: rw [← opcyclesMap_comp, e.hom_inv_id, opcyclesMap_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₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
e : S₁ ≅ S₂
inst_2 : S₁.HasRightHomology
inst_3 : S₂.HasRightHomology
rw : opcyclesMap (e.hom ≫ e.inv) = 𝟙 S₁.opcycles
⊢ CategoryStruct.comp (Y := S₂.opcycles) (opcyclesMap e.hom) (opcyclesMap e.inv) = 𝟙 S₁.opcycles
have rw₁ : opcyclesMap (𝟙 S₁) = 𝟙 S₁.opcycles
Tactic: rw [← opcyclesMap_comp, e.hom_inv_id, opcyclesMap_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₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
e : S₁ ≅ S₂
inst_2 : S₁.HasRightHomology
inst_3 : S₂.HasRightHomology
rw : opcyclesMap (e.hom ≫ e.inv) = 𝟙 S₁.opcycles
rw₁ : opcyclesMap (𝟙 S₁) = 𝟙 S₁.opcycles
⊢ CategoryStruct.comp (Y := S₂.opcycles) (opcyclesMap e.hom) (opcyclesMap e.inv) = 𝟙 S₁.opcycles
have rw₂ : Eq.{v_1 + 1} (α := S₁.opcycles ⟶ S₁.opcycles) (𝟙 S₁.opcycles) (𝟙 S₁.opcycles)
Tactic: rw [← opcyclesMap_comp, e.hom_inv_id, opcyclesMap_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₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
e : S₁ ≅ S₂
inst_2 : S₁.HasRightHomology
inst_3 : S₂.HasRightHomology
⊢ CategoryStruct.comp (Y := S₁.opcycles) (opcyclesMap e.inv) (opcyclesMap e.hom) = 𝟙 S₂.opcycles
have rw : opcyclesMap (e.inv ≫ e.hom) = 𝟙 S₂.opcycles
Tactic: rw [← opcyclesMap_comp, e.inv_hom_id, opcyclesMap_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₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
e : S₁ ≅ S₂
inst_2 : S₁.HasRightHomology
inst_3 : S₂.HasRightHomology
rw : opcyclesMap (e.inv ≫ e.hom) = 𝟙 S₂.opcycles
⊢ CategoryStruct.comp (Y := S₁.opcycles) (opcyclesMap e.inv) (opcyclesMap e.hom) = 𝟙 S₂.opcycles
have rw₁ : opcyclesMap (𝟙 S₂) = 𝟙 S₂.opcycles
Tactic: rw [← opcyclesMap_comp, e.inv_hom_id, opcyclesMap_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₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
e : S₁ ≅ S₂
inst_2 : S₁.HasRightHomology
inst_3 : S₂.HasRightHomology
rw : opcyclesMap (e.inv ≫ e.hom) = 𝟙 S₂.opcycles
rw₁ : opcyclesMap (𝟙 S₂) = 𝟙 S₂.opcycles
⊢ CategoryStruct.comp (Y := S₁.opcycles) (opcyclesMap e.inv) (opcyclesMap e.hom) = 𝟙 S₂.opcycles
have rw₂ : Eq.{v_1 + 1} (α := S₂.opcycles ⟶ S₂.opcycles) (𝟙 S₂.opcycles) (𝟙 S₂.opcycles)
Tactic: rw [← opcyclesMap_comp, e.inv_hom_id, opcyclesMap_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
h : S.RightHomologyData
inst_2 : S.HasRightHomology
⊢ Eq (α := S.X₂ ⟶ S.opcycles) (h.p ≫ Iso.inv h.opcyclesIso) S.pOpcycles
have dsimp : h.p ≫ opcyclesMap' (𝟙 S) h S.rightHomologyData = S.rightHomologyData.p
Tactic: dsimp [pOpcycles, RightHomologyData.opcyclesIso]
-- 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
h : S.RightHomologyData
inst_2 : S.HasRightHomology
⊢ Eq (α := h.H ⟶ S.opcycles) (Iso.inv h.rightHomologyIso ≫ S.rightHomologyι) (h.ι ≫ Iso.inv h.opcyclesIso)
have dsimp : rightHomologyMap' (𝟙 S) h S.rightHomologyData ≫ S.rightHomologyData.ι = h.ι ≫ opcyclesMap' (𝟙 S) h S.rightHomologyData
Tactic: dsimp only [rightHomologyι, rightHomologyIso, opcyclesIso, rightHomologyMapIso',
    opcyclesMapIso', Iso.refl]
-- 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
h : S.RightHomologyData
inst_2 : S.HasRightHomology
⊢ rightHomologyMap' (𝟙 S) h S.rightHomologyData ≫ S.rightHomologyData.ι = h.ι ≫ opcyclesMap' (𝟙 S) h S.rightHomologyData
have rw : Eq (α := h.H ⟶ S.opcycles) (h.ι ≫ opcyclesMap' (𝟙 S) h S.rightHomologyData)
  (h.ι ≫ opcyclesMap' (𝟙 S) h S.rightHomologyData)
Tactic: rw [rightHomologyι_naturality']
-- 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₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
γ : RightHomologyMapData φ h₁ h₂
inst_2 : S₁.HasRightHomology
inst_3 : S₂.HasRightHomology
⊢ Eq (α := S₁.rightHomology ⟶ S₂.rightHomology) (rightHomologyMap φ)
    (Iso.hom h₁.rightHomologyIso ≫ γ.φH ≫ Iso.inv h₂.rightHomologyIso)
have dsimp : Eq (α := S₁.rightHomology ⟶ S₂.rightHomology) (rightHomologyMap φ)
  (rightHomologyMap' (𝟙 S₁) S₁.rightHomologyData h₁ ≫ γ.φH ≫ rightHomologyMap' (𝟙 S₂) h₂ S₂.rightHomologyData)
Tactic: dsimp [RightHomologyData.rightHomologyIso, rightHomologyMapIso']
-- 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₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
γ : RightHomologyMapData φ h₁ h₂
inst_2 : S₁.HasRightHomology
inst_3 : S₂.HasRightHomology
⊢ Eq (α := S₁.rightHomology ⟶ S₂.rightHomology) (rightHomologyMap φ)
    (rightHomologyMap' (𝟙 S₁) S₁.rightHomologyData h₁ ≫ γ.φH ≫ rightHomologyMap' (𝟙 S₂) h₂ S₂.rightHomologyData)
have rw : Eq (α := S₁.rightHomology ⟶ S₂.rightHomology) (rightHomologyMap φ)
  (rightHomologyMap' φ S₁.rightHomologyData S₂.rightHomologyData)
Tactic: rw [← γ.rightHomologyMap'_eq, ← rightHomologyMap'_comp,
    ← rightHomologyMap'_comp, id_comp, 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₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
γ : RightHomologyMapData φ h₁ h₂
inst_2 : S₁.HasRightHomology
inst_3 : S₂.HasRightHomology
⊢ Eq (α := S₁.opcycles ⟶ S₂.opcycles) (opcyclesMap φ) (Iso.hom h₁.opcyclesIso ≫ γ.φQ ≫ Iso.inv h₂.opcyclesIso)
have dsimp : Eq (α := S₁.opcycles ⟶ S₂.opcycles) (opcyclesMap φ)
  (opcyclesMap' (𝟙 S₁) S₁.rightHomologyData h₁ ≫ γ.φQ ≫ opcyclesMap' (𝟙 S₂) h₂ S₂.rightHomologyData)
Tactic: dsimp [RightHomologyData.opcyclesIso, cyclesMapIso']
-- 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₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
γ : RightHomologyMapData φ h₁ h₂
inst_2 : S₁.HasRightHomology
inst_3 : S₂.HasRightHomology
⊢ Eq (α := S₁.opcycles ⟶ S₂.opcycles) (opcyclesMap φ)
    (opcyclesMap' (𝟙 S₁) S₁.rightHomologyData h₁ ≫ γ.φQ ≫ opcyclesMap' (𝟙 S₂) h₂ S₂.rightHomologyData)
have rw : Eq (α := S₁.opcycles ⟶ S₂.opcycles) (opcyclesMap φ) (opcyclesMap' φ S₁.rightHomologyData S₂.rightHomologyData)
Tactic: rw [← γ.opcyclesMap'_eq, ← opcyclesMap'_comp, ← opcyclesMap'_comp, id_comp, 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.HasLeftHomology
⊢ Eq (α := S.op.opcycles ⟶ Opposite.op S.X₁)
    (CategoryStruct.comp (Y := Opposite.op S.cycles) (Iso.hom S.opcyclesOpIso) (Quiver.Hom.op S.toCycles) :
      S.op.opcycles ⟶ Opposite.op S.X₁)
    (S.op.fromOpcycles : S.op.opcycles ⟶ S.op.X₃)
have dsimp : Eq (α := S.op.opcycles ⟶ Opposite.op S.X₁) (Iso.hom S.leftHomologyData.op.opcyclesIso ≫ S.leftHomologyData.f'.op)
  S.op.fromOpcycles
Tactic: dsimp [opcyclesOpIso, toCycles]
-- 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.opcycles ⟶ Opposite.op S.X₁) (Iso.hom S.leftHomologyData.op.opcyclesIso ≫ S.leftHomologyData.f'.op)
    S.op.fromOpcycles
have rw : CategoryStruct.comp (Y := S.op.opcycles) S.op.pOpcycles
    (Iso.hom S.leftHomologyData.op.opcyclesIso ≫ S.leftHomologyData.f'.op) =
  CategoryStruct.comp (Y := S.op.opcycles) S.op.pOpcycles S.op.fromOpcycles
Tactic: rw [← cancel_epi S.op.pOpcycles, p_fromOpcycles,
    RightHomologyData.pOpcycles_comp_opcyclesIso_hom_assoc,
    LeftHomologyData.op_p, ← op_comp, LeftHomologyData.f'_i, op_g]
-- 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
rw :
  CategoryStruct.comp (Y := S.op.opcycles) S.op.pOpcycles
      (Iso.hom S.leftHomologyData.op.opcyclesIso ≫ S.leftHomologyData.f'.op) =
    CategoryStruct.comp (Y := S.op.opcycles) S.op.pOpcycles S.op.fromOpcycles
⊢ Eq (α := S.op.opcycles ⟶ Opposite.op S.X₁) (Iso.hom S.leftHomologyData.op.opcyclesIso ≫ S.leftHomologyData.f'.op)
    S.op.fromOpcycles
have rw₁ : CategoryStruct.comp (Y := S.op.opcycles) S.op.pOpcycles
    (Iso.hom S.leftHomologyData.op.opcyclesIso ≫ S.leftHomologyData.f'.op) =
  S.op.g
Tactic: rw [← cancel_epi S.op.pOpcycles, p_fromOpcycles,
    RightHomologyData.pOpcycles_comp_opcyclesIso_hom_assoc,
    LeftHomologyData.op_p, ← op_comp, LeftHomologyData.f'_i, op_g]
-- 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
rw :
  CategoryStruct.comp (Y := S.op.opcycles) S.op.pOpcycles
      (Iso.hom S.leftHomologyData.op.opcyclesIso ≫ S.leftHomologyData.f'.op) =
    CategoryStruct.comp (Y := S.op.opcycles) S.op.pOpcycles S.op.fromOpcycles
rw₁ :
  CategoryStruct.comp (Y := S.op.opcycles) S.op.pOpcycles
      (Iso.hom S.leftHomologyData.op.opcyclesIso ≫ S.leftHomologyData.f'.op) =
    S.op.g
⊢ Eq (α := S.op.opcycles ⟶ Opposite.op S.X₁) (Iso.hom S.leftHomologyData.op.opcyclesIso ≫ S.leftHomologyData.f'.op)
    S.op.fromOpcycles
have rw₂ : S.leftHomologyData.op.p ≫ S.leftHomologyData.f'.op = S.op.g
Tactic: rw [← cancel_epi S.op.pOpcycles, p_fromOpcycles,
    RightHomologyData.pOpcycles_comp_opcyclesIso_hom_assoc,
    LeftHomologyData.op_p, ← op_comp, LeftHomologyData.f'_i, op_g]
-- 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
rw :
  CategoryStruct.comp (Y := S.op.opcycles) S.op.pOpcycles
      (Iso.hom S.leftHomologyData.op.opcyclesIso ≫ S.leftHomologyData.f'.op) =
    CategoryStruct.comp (Y := S.op.opcycles) S.op.pOpcycles S.op.fromOpcycles
rw₁ :
  CategoryStruct.comp (Y := S.op.opcycles) S.op.pOpcycles
      (Iso.hom S.leftHomologyData.op.opcyclesIso ≫ S.leftHomologyData.f'.op) =
    S.op.g
rw₂ : S.leftHomologyData.op.p ≫ S.leftHomologyData.f'.op = S.op.g
⊢ Eq (α := S.op.opcycles ⟶ Opposite.op S.X₁) (Iso.hom S.leftHomologyData.op.opcyclesIso ≫ S.leftHomologyData.f'.op)
    S.op.fromOpcycles
have rw₃ : S.leftHomologyData.i.op ≫ S.leftHomologyData.f'.op = S.op.g
Tactic: rw [← cancel_epi S.op.pOpcycles, p_fromOpcycles,
    RightHomologyData.pOpcycles_comp_opcyclesIso_hom_assoc,
    LeftHomologyData.op_p, ← op_comp, LeftHomologyData.f'_i, op_g]
-- 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
rw :
  CategoryStruct.comp (Y := S.op.opcycles) S.op.pOpcycles
      (Iso.hom S.leftHomologyData.op.opcyclesIso ≫ S.leftHomologyData.f'.op) =
    CategoryStruct.comp (Y := S.op.opcycles) S.op.pOpcycles S.op.fromOpcycles
rw₁ :
  CategoryStruct.comp (Y := S.op.opcycles) S.op.pOpcycles
      (Iso.hom S.leftHomologyData.op.opcyclesIso ≫ S.leftHomologyData.f'.op) =
    S.op.g
rw₂ : S.leftHomologyData.op.p ≫ S.leftHomologyData.f'.op = S.op.g
rw₃ : S.leftHomologyData.i.op ≫ S.leftHomologyData.f'.op = S.op.g
⊢ Eq (α := S.op.opcycles ⟶ Opposite.op S.X₁) (Iso.hom S.leftHomologyData.op.opcyclesIso ≫ S.leftHomologyData.f'.op)
    S.op.fromOpcycles
have rw₄ : (S.leftHomologyData.f' ≫ S.leftHomologyData.i).op = S.op.g
Tactic: rw [← cancel_epi S.op.pOpcycles, p_fromOpcycles,
    RightHomologyData.pOpcycles_comp_opcyclesIso_hom_assoc,
    LeftHomologyData.op_p, ← op_comp, LeftHomologyData.f'_i, op_g]
-- 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
rw :
  CategoryStruct.comp (Y := S.op.opcycles) S.op.pOpcycles
      (Iso.hom S.leftHomologyData.op.opcyclesIso ≫ S.leftHomologyData.f'.op) =
    CategoryStruct.comp (Y := S.op.opcycles) S.op.pOpcycles S.op.fromOpcycles
rw₁ :
  CategoryStruct.comp (Y := S.op.opcycles) S.op.pOpcycles
      (Iso.hom S.leftHomologyData.op.opcyclesIso ≫ S.leftHomologyData.f'.op) =
    S.op.g
rw₂ : S.leftHomologyData.op.p ≫ S.leftHomologyData.f'.op = S.op.g
rw₃ : S.leftHomologyData.i.op ≫ S.leftHomologyData.f'.op = S.op.g
rw₄ : (S.leftHomologyData.f' ≫ S.leftHomologyData.i).op = S.op.g
⊢ Eq (α := S.op.opcycles ⟶ Opposite.op S.X₁) (Iso.hom S.leftHomologyData.op.opcyclesIso ≫ S.leftHomologyData.f'.op)
    S.op.fromOpcycles
have rw₅ : S.f.op = S.op.g
Tactic: rw [← cancel_epi S.op.pOpcycles, p_fromOpcycles,
    RightHomologyData.pOpcycles_comp_opcyclesIso_hom_assoc,
    LeftHomologyData.op_p, ← op_comp, LeftHomologyData.f'_i, op_g]
-- 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
rw :
  CategoryStruct.comp (Y := S.op.opcycles) S.op.pOpcycles
      (Iso.hom S.leftHomologyData.op.opcyclesIso ≫ S.leftHomologyData.f'.op) =
    CategoryStruct.comp (Y := S.op.opcycles) S.op.pOpcycles S.op.fromOpcycles
rw₁ :
  CategoryStruct.comp (Y := S.op.opcycles) S.op.pOpcycles
      (Iso.hom S.leftHomologyData.op.opcyclesIso ≫ S.leftHomologyData.f'.op) =
    S.op.g
rw₂ : S.leftHomologyData.op.p ≫ S.leftHomologyData.f'.op = S.op.g
rw₃ : S.leftHomologyData.i.op ≫ S.leftHomologyData.f'.op = S.op.g
rw₄ : (S.leftHomologyData.f' ≫ S.leftHomologyData.i).op = S.op.g
rw₅ : S.f.op = S.op.g
⊢ Eq (α := S.op.opcycles ⟶ Opposite.op S.X₁) (Iso.hom S.leftHomologyData.op.opcyclesIso ≫ S.leftHomologyData.f'.op)
    S.op.fromOpcycles
have rw₆ : S.f.op = S.f.op
Tactic: rw [← cancel_epi S.op.pOpcycles, p_fromOpcycles,
    RightHomologyData.pOpcycles_comp_opcyclesIso_hom_assoc,
    LeftHomologyData.op_p, ← op_comp, LeftHomologyData.f'_i, op_g]
-- 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.X₃ ⟶ S.op.cycles)
    (CategoryStruct.comp (Y := Opposite.op S.opcycles) (Quiver.Hom.op S.fromOpcycles) (Iso.inv S.cyclesOpIso) :
      Opposite.op S.X₃ ⟶ S.op.cycles)
    (S.op.toCycles : S.op.X₁ ⟶ S.op.cycles)
have dsimp : Eq (α := Opposite.op S.X₃ ⟶ S.op.cycles) (S.rightHomologyData.g'.op ≫ Iso.inv S.rightHomologyData.op.cyclesIso)
  S.op.toCycles
Tactic: dsimp [cyclesOpIso, fromOpcycles]
-- 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.X₃ ⟶ S.op.cycles) (S.rightHomologyData.g'.op ≫ Iso.inv S.rightHomologyData.op.cyclesIso)
    S.op.toCycles
have 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
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
⊢ 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 =
  CategoryStruct.comp (Y := S.op.cycles) S.op.toCycles S.op.iCycles
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]