awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
i j k : ι
hi : c.prev j = i
hk : c.next j = k
inst_2 : K.HasHomology j
inst_3 : (K.sc' i j k).HasHomology
⊢ Eq (α := K.X j ⟶ K.opcycles j)
    (CategoryStruct.comp (Y := (K.sc' i j k).opcycles) (K.sc' i j k).pOpcycles
        (ShortComplex.opcyclesMap (NatTrans.app (Iso.inv (natIsoSc' C c i j k hi hk)) K)) :
      K.X j ⟶ K.opcycles j)
    (K.pOpcycles j : K.X j ⟶ K.opcycles j)
have simp : Eq (α := K.X j ⟶ K.opcycles j) ((K.sc j).pOpcycles : (K.sc j).X₂ ⟶ (K.sc j).opcycles)
  (K.pOpcycles j : K.X j ⟶ K.opcycles j)
Tactic: simp only [ShortComplex.p_opcyclesMap, shortComplexFunctor'_obj_X₂, shortComplexFunctor_obj_X₂,
    natIsoSc'_inv_app_τ₂, id_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
j : ι
inst_2 : K.HasHomology j
inst_3 : (K.sc' (c.prev j) j (c.next j)).HasHomology
⊢ K.homologyIsoSc' (c.prev j) j (c.next j) ⋯ ⋯ = Iso.refl (K.homology j)
have w : Iso.hom (K.homologyIsoSc' (c.prev j) j (c.next j) sorry sorry) = Iso.hom (Iso.refl (K.homology j))
Tactic: ext : 1
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Homology (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S₁ S₂ : ShortComplex.{v, u} C
φ : S₁ ⟶ S₂
h₁ : S₁.HomologyData
h₂ : S₂.HomologyData
γ₁ γ₂ : HomologyMapData φ h₁ h₂
eq : γ₁ = γ₂
⊢ γ₁.left.φH = γ₂.left.φH
have rw : γ₂.left.φH = γ₂.left.φH
Tactic: rw [eq]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Homology (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S : ShortComplex.{v, u} C
inst_2 : S.HasHomology
⊢ Eq (α := S.homology ≅ S.leftHomologyData.H) S.leftHomologyData.homologyIso (Iso.symm S.leftHomologyIso)
have w : Eq (α := S.homology ⟶ S.leftHomologyData.H) (Iso.hom S.leftHomologyData.homologyIso)
  (Iso.hom (Iso.symm S.leftHomologyIso))
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Homology (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S : ShortComplex.{v, u} C
inst_2 : S.HasHomology
⊢ Eq (α := S.homology ⟶ S.leftHomologyData.H) (Iso.hom S.leftHomologyData.homologyIso)
    (Iso.hom (Iso.symm S.leftHomologyIso))
have w : Eq (α := S.homology ⟶ S.leftHomology)
  (CategoryStruct.comp (Y := S.leftHomology) (leftHomologyMap' (𝟙 S) S.homologyData.left S.leftHomologyData)
    (leftHomologyMap' (𝟙 S) S.leftHomologyData S.leftHomologyData))
  (leftHomologyMap' (𝟙 S) S.homologyData.left S.leftHomologyData)
Tactic: dsimp [homologyIso, leftHomologyIso, ShortComplex.leftHomologyIso]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Homology (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S : ShortComplex.{v, u} C
inst_2 : S.HasHomology
⊢ Eq (α := S.homology ⟶ S.leftHomology)
    (CategoryStruct.comp (Y := S.leftHomology) (leftHomologyMap' (𝟙 S) S.homologyData.left S.leftHomologyData)
      (leftHomologyMap' (𝟙 S) S.leftHomologyData S.leftHomologyData))
    (leftHomologyMap' (𝟙 S) S.homologyData.left S.leftHomologyData)
have w : Eq (α := S.homology ⟶ S.leftHomology) (leftHomologyMap' (𝟙 S ≫ 𝟙 S) S.homologyData.left S.leftHomologyData)
  (leftHomologyMap' (𝟙 S) S.homologyData.left S.leftHomologyData)
Tactic: rw [← leftHomologyMap'_comp, comp_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Homology (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S : ShortComplex.{v, u} C
inst_2 : S.HasHomology
w :
  Eq (α := S.homology ⟶ S.leftHomology) (leftHomologyMap' (𝟙 S ≫ 𝟙 S) S.homologyData.left S.leftHomologyData)
    (leftHomologyMap' (𝟙 S) S.homologyData.left S.leftHomologyData)
⊢ Eq (α := S.homology ⟶ S.leftHomology)
    (CategoryStruct.comp (Y := S.leftHomology) (leftHomologyMap' (𝟙 S) S.homologyData.left S.leftHomologyData)
      (leftHomologyMap' (𝟙 S) S.leftHomologyData S.leftHomologyData))
    (leftHomologyMap' (𝟙 S) S.homologyData.left S.leftHomologyData)
have w₁ : Eq (α := S.homology ⟶ S.leftHomology) (leftHomologyMap' (𝟙 S) S.homologyData.left S.leftHomologyData)
  (leftHomologyMap' (𝟙 S) S.homologyData.left S.leftHomologyData)
Tactic: rw [← leftHomologyMap'_comp, comp_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Homology (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S : ShortComplex.{v, u} C
inst_2 : S.HasHomology
⊢ Eq (α := S.homology ≅ S.rightHomologyData.H) S.rightHomologyData.homologyIso (Iso.symm S.rightHomologyIso)
have w : Eq (α := S.homology ⟶ S.rightHomologyData.H) (Iso.hom S.rightHomologyData.homologyIso)
  (Iso.hom (Iso.symm S.rightHomologyIso))
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Homology (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S₁ S₂ : ShortComplex.{v, u} C
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
γ : LeftHomologyMapData φ h₁ h₂
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
⊢ Eq (α := S₁.homology ⟶ S₂.homology) (homologyMap φ) (Iso.hom h₁.homologyIso ≫ γ.φH ≫ Iso.inv h₂.homologyIso)
have dsimp : Eq (α := S₁.homology ⟶ S₂.homology) (leftHomologyMap' φ S₁.homologyData.left S₂.homologyData.left)
  (CategoryStruct.comp (Y := S₁.leftHomology) (leftHomologyMap' (𝟙 S₁) S₁.homologyData.left S₁.leftHomologyData)
      (leftHomologyMap' (𝟙 S₁) S₁.leftHomologyData h₁) ≫
    γ.φH ≫
      CategoryStruct.comp (Y := S₂.leftHomology) (leftHomologyMap' (𝟙 S₂) h₂ S₂.leftHomologyData)
        (leftHomologyMap' (𝟙 S₂) S₂.leftHomologyData S₂.homologyData.left))
Tactic: dsimp [homologyMap, LeftHomologyData.homologyIso, leftHomologyIso,
    LeftHomologyData.leftHomologyIso, homologyMap']
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Homology (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S₁ S₂ : ShortComplex.{v, u} C
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
γ : RightHomologyMapData φ h₁ h₂
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
⊢ Eq (α := S₁.homology ⟶ S₂.homology) (homologyMap φ) (Iso.hom h₁.homologyIso ≫ γ.φH ≫ Iso.inv h₂.homologyIso)
have dsimp : leftHomologyMap' φ S₁.homologyData.left S₂.homologyData.left =
  CategoryStruct.comp (Y := S₁.rightHomology)
      (S₁.homologyData.iso.hom ≫ rightHomologyMap' (𝟙 S₁) S₁.homologyData.right S₁.rightHomologyData)
      (rightHomologyMap' (𝟙 S₁) S₁.rightHomologyData h₁) ≫
    γ.φH ≫
      CategoryStruct.comp (Y := S₂.rightHomology) (rightHomologyMap' (𝟙 S₂) h₂ S₂.rightHomologyData)
        (rightHomologyMap' (𝟙 S₂) S₂.rightHomologyData S₂.homologyData.right ≫ S₂.homologyData.iso.inv)
Tactic: dsimp [homologyMap, homologyMap', RightHomologyData.homologyIso,
    rightHomologyIso, RightHomologyData.rightHomologyIso]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Homology (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S₁ S₂ : ShortComplex.{v, u} C
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
γ : RightHomologyMapData φ h₁ h₂
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
⊢ leftHomologyMap' φ S₁.homologyData.left S₂.homologyData.left =
    CategoryStruct.comp (Y := S₁.rightHomology)
        (S₁.homologyData.iso.hom ≫ rightHomologyMap' (𝟙 S₁) S₁.homologyData.right S₁.rightHomologyData)
        (rightHomologyMap' (𝟙 S₁) S₁.rightHomologyData h₁) ≫
      γ.φH ≫
        CategoryStruct.comp (Y := S₂.rightHomology) (rightHomologyMap' (𝟙 S₂) h₂ S₂.rightHomologyData)
          (rightHomologyMap' (𝟙 S₂) S₂.rightHomologyData S₂.homologyData.right ≫ S₂.homologyData.iso.inv)
have have : ∀ (γ' : HomologyMapData φ S₁.homologyData S₂.homologyData),
  leftHomologyMap' φ S₁.homologyData.left S₂.homologyData.left =
    CategoryStruct.comp (Y := S₁.rightHomology)
        (S₁.homologyData.iso.hom ≫ rightHomologyMap' (𝟙 S₁) S₁.homologyData.right S₁.rightHomologyData)
        (rightHomologyMap' (𝟙 S₁) S₁.rightHomologyData h₁) ≫
      γ.φH ≫
        CategoryStruct.comp (Y := S₂.rightHomology) (rightHomologyMap' (𝟙 S₂) h₂ S₂.rightHomologyData)
          (rightHomologyMap' (𝟙 S₂) S₂.rightHomologyData S₂.homologyData.right ≫ S₂.homologyData.iso.inv)
Tactic: have γ' : HomologyMapData φ S₁.homologyData S₂.homologyData := default
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Homology (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S S₁ S₂ S₃ S₄ : ShortComplex.{v, u} C
φ : S₁ ⟶ S₂
h₁_1 : S₁.HomologyData
h₂_1 : S₂.HomologyData
e : S₁ ≅ S₂
h₁ : S₁.HomologyData
h₂ : S₂.HomologyData
⊢ homologyMap' e.hom h₁ h₂ ≫ homologyMap' e.inv h₂ h₁ = 𝟙 h₁.left.H
have rw : homologyMap' (e.hom ≫ e.inv) h₁ h₁ = 𝟙 h₁.left.H
Tactic: rw [← homologyMap'_comp, e.hom_inv_id, homologyMap'_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Homology (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S S₁ S₂ S₃ S₄ : ShortComplex.{v, u} C
φ : S₁ ⟶ S₂
h₁_1 : S₁.HomologyData
h₂_1 : S₂.HomologyData
e : S₁ ≅ S₂
h₁ : S₁.HomologyData
h₂ : S₂.HomologyData
rw : homologyMap' (e.hom ≫ e.inv) h₁ h₁ = 𝟙 h₁.left.H
⊢ homologyMap' e.hom h₁ h₂ ≫ homologyMap' e.inv h₂ h₁ = 𝟙 h₁.left.H
have rw₁ : homologyMap' (𝟙 S₁) h₁ h₁ = 𝟙 h₁.left.H
Tactic: rw [← homologyMap'_comp, e.hom_inv_id, homologyMap'_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Homology (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S S₁ S₂ S₃ S₄ : ShortComplex.{v, u} C
φ : S₁ ⟶ S₂
h₁_1 : S₁.HomologyData
h₂_1 : S₂.HomologyData
e : S₁ ≅ S₂
h₁ : S₁.HomologyData
h₂ : S₂.HomologyData
rw : homologyMap' (e.hom ≫ e.inv) h₁ h₁ = 𝟙 h₁.left.H
rw₁ : homologyMap' (𝟙 S₁) h₁ h₁ = 𝟙 h₁.left.H
⊢ homologyMap' e.hom h₁ h₂ ≫ homologyMap' e.inv h₂ h₁ = 𝟙 h₁.left.H
have rw₂ : Eq.{v + 1} (α := h₁.left.H ⟶ h₁.left.H) (𝟙 h₁.left.H) (𝟙 h₁.left.H)
Tactic: rw [← homologyMap'_comp, e.hom_inv_id, homologyMap'_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Homology (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S S₁ S₂ S₃ S₄ : ShortComplex.{v, u} C
φ : S₁ ⟶ S₂
h₁_1 : S₁.HomologyData
h₂_1 : S₂.HomologyData
e : S₁ ≅ S₂
h₁ : S₁.HomologyData
h₂ : S₂.HomologyData
⊢ homologyMap' e.inv h₂ h₁ ≫ homologyMap' e.hom h₁ h₂ = 𝟙 h₂.left.H
have rw : homologyMap' (e.inv ≫ e.hom) h₂ h₂ = 𝟙 h₂.left.H
Tactic: rw [← homologyMap'_comp, e.inv_hom_id, homologyMap'_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Homology (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S S₁ S₂ S₃ S₄ : ShortComplex.{v, u} C
φ : S₁ ⟶ S₂
h₁_1 : S₁.HomologyData
h₂_1 : S₂.HomologyData
e : S₁ ≅ S₂
h₁ : S₁.HomologyData
h₂ : S₂.HomologyData
rw : homologyMap' (e.inv ≫ e.hom) h₂ h₂ = 𝟙 h₂.left.H
⊢ homologyMap' e.inv h₂ h₁ ≫ homologyMap' e.hom h₁ h₂ = 𝟙 h₂.left.H
have rw₁ : homologyMap' (𝟙 S₂) h₂ h₂ = 𝟙 h₂.left.H
Tactic: rw [← homologyMap'_comp, e.inv_hom_id, homologyMap'_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Homology (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S S₁ S₂ S₃ S₄ : ShortComplex.{v, u} C
φ : S₁ ⟶ S₂
h₁_1 : S₁.HomologyData
h₂_1 : S₂.HomologyData
e : S₁ ≅ S₂
h₁ : S₁.HomologyData
h₂ : S₂.HomologyData
rw : homologyMap' (e.inv ≫ e.hom) h₂ h₂ = 𝟙 h₂.left.H
rw₁ : homologyMap' (𝟙 S₂) h₂ h₂ = 𝟙 h₂.left.H
⊢ homologyMap' e.inv h₂ h₁ ≫ homologyMap' e.hom h₁ h₂ = 𝟙 h₂.left.H
have rw₂ : Eq.{v + 1} (α := h₂.left.H ⟶ h₂.left.H) (𝟙 h₂.left.H) (𝟙 h₂.left.H)
Tactic: rw [← homologyMap'_comp, e.inv_hom_id, homologyMap'_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Homology (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S S₁ S₂ S₃ S₄ : ShortComplex.{v, u} C
φ : S₁ ⟶ S₂
h₁ : S₁.HomologyData
h₂ : S₂.HomologyData
e : S₁ ≅ S₂
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
⊢ CategoryStruct.comp (Y := S₂.homology) (homologyMap e.hom) (homologyMap e.inv) = 𝟙 S₁.homology
have rw : homologyMap (e.hom ≫ e.inv) = 𝟙 S₁.homology
Tactic: rw [← homologyMap_comp, e.hom_inv_id, homologyMap_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Homology (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S S₁ S₂ S₃ S₄ : ShortComplex.{v, u} C
φ : S₁ ⟶ S₂
h₁ : S₁.HomologyData
h₂ : S₂.HomologyData
e : S₁ ≅ S₂
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
rw : homologyMap (e.hom ≫ e.inv) = 𝟙 S₁.homology
⊢ CategoryStruct.comp (Y := S₂.homology) (homologyMap e.hom) (homologyMap e.inv) = 𝟙 S₁.homology
have rw₁ : homologyMap (𝟙 S₁) = 𝟙 S₁.homology
Tactic: rw [← homologyMap_comp, e.hom_inv_id, homologyMap_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Homology (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S S₁ S₂ S₃ S₄ : ShortComplex.{v, u} C
φ : S₁ ⟶ S₂
h₁ : S₁.HomologyData
h₂ : S₂.HomologyData
e : S₁ ≅ S₂
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
rw : homologyMap (e.hom ≫ e.inv) = 𝟙 S₁.homology
rw₁ : homologyMap (𝟙 S₁) = 𝟙 S₁.homology
⊢ CategoryStruct.comp (Y := S₂.homology) (homologyMap e.hom) (homologyMap e.inv) = 𝟙 S₁.homology
have rw₂ : Eq.{v + 1} (α := S₁.homology ⟶ S₁.homology) (𝟙 S₁.homology) (𝟙 S₁.homology)
Tactic: rw [← homologyMap_comp, e.hom_inv_id, homologyMap_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Homology (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S S₁ S₂ S₃ S₄ : ShortComplex.{v, u} C
φ : S₁ ⟶ S₂
h₁ : S₁.HomologyData
h₂ : S₂.HomologyData
e : S₁ ≅ S₂
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
⊢ CategoryStruct.comp (Y := S₁.homology) (homologyMap e.inv) (homologyMap e.hom) = 𝟙 S₂.homology
have rw : homologyMap (e.inv ≫ e.hom) = 𝟙 S₂.homology
Tactic: rw [← homologyMap_comp, e.inv_hom_id, homologyMap_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Homology (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S S₁ S₂ S₃ S₄ : ShortComplex.{v, u} C
φ : S₁ ⟶ S₂
h₁ : S₁.HomologyData
h₂ : S₂.HomologyData
e : S₁ ≅ S₂
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
rw : homologyMap (e.inv ≫ e.hom) = 𝟙 S₂.homology
⊢ CategoryStruct.comp (Y := S₁.homology) (homologyMap e.inv) (homologyMap e.hom) = 𝟙 S₂.homology
have rw₁ : homologyMap (𝟙 S₂) = 𝟙 S₂.homology
Tactic: rw [← homologyMap_comp, e.inv_hom_id, homologyMap_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Homology (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S S₁ S₂ S₃ S₄ : ShortComplex.{v, u} C
φ : S₁ ⟶ S₂
h₁ : S₁.HomologyData
h₂ : S₂.HomologyData
e : S₁ ≅ S₂
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
rw : homologyMap (e.inv ≫ e.hom) = 𝟙 S₂.homology
rw₁ : homologyMap (𝟙 S₂) = 𝟙 S₂.homology
⊢ CategoryStruct.comp (Y := S₁.homology) (homologyMap e.inv) (homologyMap e.hom) = 𝟙 S₂.homology
have rw₂ : Eq.{v + 1} (α := S₂.homology ⟶ S₂.homology) (𝟙 S₂.homology) (𝟙 S₂.homology)
Tactic: rw [← homologyMap_comp, e.inv_hom_id, homologyMap_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Homology (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S S₁ S₂ S₃ S₄ : ShortComplex.{v, u} C
φ : S₁ ⟶ S₂
h₁_1 : S₁.HomologyData
h₂_1 : S₂.HomologyData
h₁ : S.LeftHomologyData
h₂ : S.RightHomologyData
⊢ h₁.descH (h₁.i ≫ h₂.p) ⋯ ≫ h₂.g' = 0
have rw : h₁.π ≫ h₁.descH (h₁.i ≫ h₂.p) sorry ≫ h₂.g' = h₁.π ≫ 0
Tactic: rw [← cancel_epi h₁.π, LeftHomologyData.π_descH_assoc, assoc,
      RightHomologyData.p_g', LeftHomologyData.wi, comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Homology (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S S₁ S₂ S₃ S₄ : ShortComplex.{v, u} C
φ : S₁ ⟶ S₂
h₁_1 : S₁.HomologyData
h₂_1 : S₂.HomologyData
h₁ : S.LeftHomologyData
h₂ : S.RightHomologyData
rw : h₁.π ≫ h₁.descH (h₁.i ≫ h₂.p) ⋯ ≫ h₂.g' = h₁.π ≫ 0
⊢ h₁.descH (h₁.i ≫ h₂.p) ⋯ ≫ h₂.g' = 0
have rw₁ : (h₁.i ≫ h₂.p) ≫ h₂.g' = h₁.π ≫ 0
Tactic: rw [← cancel_epi h₁.π, LeftHomologyData.π_descH_assoc, assoc,
      RightHomologyData.p_g', LeftHomologyData.wi, comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Homology (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S S₁ S₂ S₃ S₄ : ShortComplex.{v, u} C
φ : S₁ ⟶ S₂
h₁_1 : S₁.HomologyData
h₂_1 : S₂.HomologyData
h₁ : S.LeftHomologyData
h₂ : S.RightHomologyData
rw : h₁.π ≫ h₁.descH (h₁.i ≫ h₂.p) ⋯ ≫ h₂.g' = h₁.π ≫ 0
rw₁ : (h₁.i ≫ h₂.p) ≫ h₂.g' = h₁.π ≫ 0
⊢ h₁.descH (h₁.i ≫ h₂.p) ⋯ ≫ h₂.g' = 0
have rw₂ : h₁.i ≫ h₂.p ≫ h₂.g' = h₁.π ≫ 0
Tactic: rw [← cancel_epi h₁.π, LeftHomologyData.π_descH_assoc, assoc,
      RightHomologyData.p_g', LeftHomologyData.wi, comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Homology (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S S₁ S₂ S₃ S₄ : ShortComplex.{v, u} C
φ : S₁ ⟶ S₂
h₁_1 : S₁.HomologyData
h₂_1 : S₂.HomologyData
h₁ : S.LeftHomologyData
h₂ : S.RightHomologyData
rw : h₁.π ≫ h₁.descH (h₁.i ≫ h₂.p) ⋯ ≫ h₂.g' = h₁.π ≫ 0
rw₁ : (h₁.i ≫ h₂.p) ≫ h₂.g' = h₁.π ≫ 0
rw₂ : h₁.i ≫ h₂.p ≫ h₂.g' = h₁.π ≫ 0
⊢ h₁.descH (h₁.i ≫ h₂.p) ⋯ ≫ h₂.g' = 0
have rw₃ : h₁.i ≫ S.g = h₁.π ≫ 0
Tactic: rw [← cancel_epi h₁.π, LeftHomologyData.π_descH_assoc, assoc,
      RightHomologyData.p_g', LeftHomologyData.wi, comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Homology (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S S₁ S₂ S₃ S₄ : ShortComplex.{v, u} C
φ : S₁ ⟶ S₂
h₁_1 : S₁.HomologyData
h₂_1 : S₂.HomologyData
h₁ : S.LeftHomologyData
h₂ : S.RightHomologyData
rw : h₁.π ≫ h₁.descH (h₁.i ≫ h₂.p) ⋯ ≫ h₂.g' = h₁.π ≫ 0
rw₁ : (h₁.i ≫ h₂.p) ≫ h₂.g' = h₁.π ≫ 0
rw₂ : h₁.i ≫ h₂.p ≫ h₂.g' = h₁.π ≫ 0
rw₃ : h₁.i ≫ S.g = h₁.π ≫ 0
⊢ h₁.descH (h₁.i ≫ h₂.p) ⋯ ≫ h₂.g' = 0
have rw₄ : Eq (α := h₁.K ⟶ S.X₃) 0 (h₁.π ≫ 0)
Tactic: rw [← cancel_epi h₁.π, LeftHomologyData.π_descH_assoc, assoc,
      RightHomologyData.p_g', LeftHomologyData.wi, comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Homology (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S S₁ S₂ S₃ S₄ : ShortComplex.{v, u} C
φ : S₁ ⟶ S₂
h₁_1 : S₁.HomologyData
h₂_1 : S₂.HomologyData
h₁ : S.LeftHomologyData
h₂ : S.RightHomologyData
rw : h₁.π ≫ h₁.descH (h₁.i ≫ h₂.p) ⋯ ≫ h₂.g' = h₁.π ≫ 0
rw₁ : (h₁.i ≫ h₂.p) ≫ h₂.g' = h₁.π ≫ 0
rw₂ : h₁.i ≫ h₂.p ≫ h₂.g' = h₁.π ≫ 0
rw₃ : h₁.i ≫ S.g = h₁.π ≫ 0
rw₄ : Eq (α := h₁.K ⟶ S.X₃) 0 (h₁.π ≫ 0)
⊢ h₁.descH (h₁.i ≫ h₂.p) ⋯ ≫ h₂.g' = 0
have rw₅ : Eq.{v + 1} (α := h₁.K ⟶ S.X₃) 0 0
Tactic: rw [← cancel_epi h₁.π, LeftHomologyData.π_descH_assoc, assoc,
      RightHomologyData.p_g', LeftHomologyData.wi, comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Homology (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S S₁ S₂ S₃ S₄ : ShortComplex.{v, u} C
φ : S₁ ⟶ S₂
h₁_1 : S₁.HomologyData
h₂_1 : S₂.HomologyData
h₁ : S.LeftHomologyData
h₂ : S.RightHomologyData
⊢ h₁.descH (h₁.i ≫ h₂.p) ⋯ ≫ h₂.g' = 0
have rw : h₁.π ≫ h₁.descH (h₁.i ≫ h₂.p) sorry ≫ h₂.g' = h₁.π ≫ 0
Tactic: rw [← cancel_epi h₁.π, LeftHomologyData.π_descH_assoc, assoc,
          RightHomologyData.p_g', LeftHomologyData.wi, comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Homology (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S S₁ S₂ S₃ S₄ : ShortComplex.{v, u} C
φ : S₁ ⟶ S₂
h₁_1 : S₁.HomologyData
h₂_1 : S₂.HomologyData
h₁ : S.LeftHomologyData
h₂ : S.RightHomologyData
rw : h₁.π ≫ h₁.descH (h₁.i ≫ h₂.p) ⋯ ≫ h₂.g' = h₁.π ≫ 0
⊢ h₁.descH (h₁.i ≫ h₂.p) ⋯ ≫ h₂.g' = 0
have rw₁ : (h₁.i ≫ h₂.p) ≫ h₂.g' = h₁.π ≫ 0
Tactic: rw [← cancel_epi h₁.π, LeftHomologyData.π_descH_assoc, assoc,
          RightHomologyData.p_g', LeftHomologyData.wi, comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Homology (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S S₁ S₂ S₃ S₄ : ShortComplex.{v, u} C
φ : S₁ ⟶ S₂
h₁_1 : S₁.HomologyData
h₂_1 : S₂.HomologyData
h₁ : S.LeftHomologyData
h₂ : S.RightHomologyData
rw : h₁.π ≫ h₁.descH (h₁.i ≫ h₂.p) ⋯ ≫ h₂.g' = h₁.π ≫ 0
rw₁ : (h₁.i ≫ h₂.p) ≫ h₂.g' = h₁.π ≫ 0
⊢ h₁.descH (h₁.i ≫ h₂.p) ⋯ ≫ h₂.g' = 0
have rw₂ : h₁.i ≫ h₂.p ≫ h₂.g' = h₁.π ≫ 0
Tactic: rw [← cancel_epi h₁.π, LeftHomologyData.π_descH_assoc, assoc,
          RightHomologyData.p_g', LeftHomologyData.wi, comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Homology (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S S₁ S₂ S₃ S₄ : ShortComplex.{v, u} C
φ : S₁ ⟶ S₂
h₁_1 : S₁.HomologyData
h₂_1 : S₂.HomologyData
h₁ : S.LeftHomologyData
h₂ : S.RightHomologyData
rw : h₁.π ≫ h₁.descH (h₁.i ≫ h₂.p) ⋯ ≫ h₂.g' = h₁.π ≫ 0
rw₁ : (h₁.i ≫ h₂.p) ≫ h₂.g' = h₁.π ≫ 0
rw₂ : h₁.i ≫ h₂.p ≫ h₂.g' = h₁.π ≫ 0
⊢ h₁.descH (h₁.i ≫ h₂.p) ⋯ ≫ h₂.g' = 0
have rw₃ : h₁.i ≫ S.g = h₁.π ≫ 0
Tactic: rw [← cancel_epi h₁.π, LeftHomologyData.π_descH_assoc, assoc,
          RightHomologyData.p_g', LeftHomologyData.wi, comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Homology (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S S₁ S₂ S₃ S₄ : ShortComplex.{v, u} C
φ : S₁ ⟶ S₂
h₁_1 : S₁.HomologyData
h₂_1 : S₂.HomologyData
h₁ : S.LeftHomologyData
h₂ : S.RightHomologyData
rw : h₁.π ≫ h₁.descH (h₁.i ≫ h₂.p) ⋯ ≫ h₂.g' = h₁.π ≫ 0
rw₁ : (h₁.i ≫ h₂.p) ≫ h₂.g' = h₁.π ≫ 0
rw₂ : h₁.i ≫ h₂.p ≫ h₂.g' = h₁.π ≫ 0
rw₃ : h₁.i ≫ S.g = h₁.π ≫ 0
⊢ h₁.descH (h₁.i ≫ h₂.p) ⋯ ≫ h₂.g' = 0
have rw₄ : Eq (α := h₁.K ⟶ S.X₃) 0 (h₁.π ≫ 0)
Tactic: rw [← cancel_epi h₁.π, LeftHomologyData.π_descH_assoc, assoc,
          RightHomologyData.p_g', LeftHomologyData.wi, comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Homology (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S S₁ S₂ S₃ S₄ : ShortComplex.{v, u} C
φ : S₁ ⟶ S₂
h₁_1 : S₁.HomologyData
h₂_1 : S₂.HomologyData
h₁ : S.LeftHomologyData
h₂ : S.RightHomologyData
rw : h₁.π ≫ h₁.descH (h₁.i ≫ h₂.p) ⋯ ≫ h₂.g' = h₁.π ≫ 0
rw₁ : (h₁.i ≫ h₂.p) ≫ h₂.g' = h₁.π ≫ 0
rw₂ : h₁.i ≫ h₂.p ≫ h₂.g' = h₁.π ≫ 0
rw₃ : h₁.i ≫ S.g = h₁.π ≫ 0
rw₄ : Eq (α := h₁.K ⟶ S.X₃) 0 (h₁.π ≫ 0)
⊢ h₁.descH (h₁.i ≫ h₂.p) ⋯ ≫ h₂.g' = 0
have rw₅ : Eq.{v + 1} (α := h₁.K ⟶ S.X₃) 0 0
Tactic: rw [← cancel_epi h₁.π, LeftHomologyData.π_descH_assoc, assoc,
          RightHomologyData.p_g', LeftHomologyData.wi, comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Homology (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S S₁ S₂ S₃ S₄ : ShortComplex.{v, u} C
φ : S₁ ⟶ S₂
h₁_1 : S₁.HomologyData
h₂_1 : S₂.HomologyData
h₁ : S.LeftHomologyData
h₂ : S.RightHomologyData
⊢ h₁.f' ≫ h₂.liftH (h₁.i ≫ h₂.p) ⋯ = 0
have rw : (h₁.f' ≫ h₂.liftH (h₁.i ≫ h₂.p) sorry) ≫ h₂.ι = 0 ≫ h₂.ι
Tactic: rw [← cancel_mono h₂.ι, assoc, RightHomologyData.liftH_ι,
          LeftHomologyData.f'_i_assoc, RightHomologyData.wp, zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Homology (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S S₁ S₂ S₃ S₄ : ShortComplex.{v, u} C
φ : S₁ ⟶ S₂
h₁_1 : S₁.HomologyData
h₂_1 : S₂.HomologyData
h₁ : S.LeftHomologyData
h₂ : S.RightHomologyData
rw : (h₁.f' ≫ h₂.liftH (h₁.i ≫ h₂.p) ⋯) ≫ h₂.ι = 0 ≫ h₂.ι
⊢ h₁.f' ≫ h₂.liftH (h₁.i ≫ h₂.p) ⋯ = 0
have rw₁ : h₁.f' ≫ h₂.liftH (h₁.i ≫ h₂.p) sorry ≫ h₂.ι = 0 ≫ h₂.ι
Tactic: rw [← cancel_mono h₂.ι, assoc, RightHomologyData.liftH_ι,
          LeftHomologyData.f'_i_assoc, RightHomologyData.wp, zero_comp]