awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Preadditive (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
H₁ : S₁.RightHomologyData
H₂ : S₂.RightHomologyData
h₀ : S₁.X₁ ⟶ S₂.X₁
h₀_f : h₀ ≫ S₂.f = 0
h₁ : S₁.X₂ ⟶ S₂.X₁
h₂ : S₁.X₃ ⟶ S₂.X₂
h₃ : S₁.X₃ ⟶ S₂.X₃
g_h₃ : S₁.g ≫ h₃ = 0
rw : H₁.p ≫ H₁.descQ (S₁.g ≫ h₂ ≫ H₂.p) ⋯ ≫ H₂.g' = H₁.p ≫ H₁.g' ≫ (S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).τ₃
rw₁ : (S₁.g ≫ h₂ ≫ H₂.p) ≫ H₂.g' = H₁.p ≫ H₁.g' ≫ (S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).τ₃
rw₂ : (S₁.g ≫ h₂ ≫ H₂.p) ≫ H₂.g' = S₁.g ≫ (S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).τ₃
rw₃ : (S₁.g ≫ h₂ ≫ H₂.p) ≫ H₂.g' = S₁.g ≫ (h₂ ≫ S₂.g + h₃)
rw₄ : (S₁.g ≫ h₂ ≫ H₂.p) ≫ H₂.g' = S₁.g ≫ h₂ ≫ S₂.g + S₁.g ≫ h₃
rw₅ : S₁.g ≫ (h₂ ≫ H₂.p) ≫ H₂.g' = S₁.g ≫ h₂ ≫ S₂.g + S₁.g ≫ h₃
rw₆ : S₁.g ≫ h₂ ≫ H₂.p ≫ H₂.g' = S₁.g ≫ h₂ ≫ S₂.g + S₁.g ≫ h₃
rw₇ : S₁.g ≫ h₂ ≫ S₂.g = S₁.g ≫ h₂ ≫ S₂.g + S₁.g ≫ h₃
rw₈ : S₁.g ≫ h₂ ≫ S₂.g = S₁.g ≫ h₂ ≫ S₂.g + 0
⊢ H₁.descQ (S₁.g ≫ h₂ ≫ H₂.p) ⋯ ≫ H₂.g' = H₁.g' ≫ (S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).τ₃
have rw₉ : S₁.g ≫ h₂ ≫ S₂.g = S₁.g ≫ h₂ ≫ S₂.g
Tactic: rw [← cancel_epi H₁.p, RightHomologyData.p_descQ_assoc, RightHomologyData.p_g'_assoc,
      nullHomotopic_τ₃, comp_add, assoc, assoc, RightHomologyData.p_g', g_h₃, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Preadditive (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
H₁ : S₁.RightHomologyData
H₂ : S₂.RightHomologyData
h₀ : S₁.X₁ ⟶ S₂.X₁
h₀_f : h₀ ≫ S₂.f = 0
h₁ : S₁.X₂ ⟶ S₂.X₁
h₂ : S₁.X₃ ⟶ S₂.X₂
h₃ : S₁.X₃ ⟶ S₂.X₃
g_h₃ : S₁.g ≫ h₃ = 0
⊢ 0 ≫ H₂.ι = H₁.ι ≫ H₁.descQ (S₁.g ≫ h₂ ≫ H₂.p) ⋯
have rw : Eq (α := H₁.H ⟶ H₂.Q) (0 ≫ H₂.ι) 0
Tactic: rw [H₁.ι_descQ_eq_zero_of_boundary (S₁.g ≫ h₂ ≫ H₂.p) (h₂ ≫ H₂.p) rfl, zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Preadditive (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
H₁ : S₁.RightHomologyData
H₂ : S₂.RightHomologyData
h₀ : S₁.X₁ ⟶ S₂.X₁
h₀_f : h₀ ≫ S₂.f = 0
h₁ : S₁.X₂ ⟶ S₂.X₁
h₂ : S₁.X₃ ⟶ S₂.X₂
h₃ : S₁.X₃ ⟶ S₂.X₃
g_h₃ : S₁.g ≫ h₃ = 0
rw : Eq (α := H₁.H ⟶ H₂.Q) (0 ≫ H₂.ι) 0
⊢ 0 ≫ H₂.ι = H₁.ι ≫ H₁.descQ (S₁.g ≫ h₂ ≫ H₂.p) ⋯
have rw₁ : Eq.{v_1 + 1} (α := H₁.H ⟶ H₂.Q) 0 0
Tactic: rw [H₁.ι_descQ_eq_zero_of_boundary (S₁.g ≫ h₂ ≫ H₂.p) (h₂ ≫ H₂.p) rfl, zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Preadditive (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ₁ φ₂ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
⊢ leftHomologyMap' φ₁ h₁ h₂ = leftHomologyMap' φ₂ h₁ h₂
have rw : leftHomologyMap' (φ₂ + S₁.nullHomotopic S₂ h.h₀ sorry h.h₁ h.h₂ h.h₃ sorry) h₁ h₂ = leftHomologyMap' φ₂ h₁ h₂
Tactic: rw [h.eq_add_nullHomotopic, leftHomologyMap'_add, leftHomologyMap'_nullHomotopic, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Preadditive (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ₁ φ₂ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
rw : leftHomologyMap' (φ₂ + S₁.nullHomotopic S₂ h.h₀ ⋯ h.h₁ h.h₂ h.h₃ ⋯) h₁ h₂ = leftHomologyMap' φ₂ h₁ h₂
⊢ leftHomologyMap' φ₁ h₁ h₂ = leftHomologyMap' φ₂ h₁ h₂
have rw₁ : leftHomologyMap' φ₂ h₁ h₂ + leftHomologyMap' (S₁.nullHomotopic S₂ h.h₀ sorry h.h₁ h.h₂ h.h₃ sorry) h₁ h₂ =
  leftHomologyMap' φ₂ h₁ h₂
Tactic: rw [h.eq_add_nullHomotopic, leftHomologyMap'_add, leftHomologyMap'_nullHomotopic, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Preadditive (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ₁ φ₂ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
rw : leftHomologyMap' (φ₂ + S₁.nullHomotopic S₂ h.h₀ ⋯ h.h₁ h.h₂ h.h₃ ⋯) h₁ h₂ = leftHomologyMap' φ₂ h₁ h₂
rw₁ :
  leftHomologyMap' φ₂ h₁ h₂ + leftHomologyMap' (S₁.nullHomotopic S₂ h.h₀ ⋯ h.h₁ h.h₂ h.h₃ ⋯) h₁ h₂ =
    leftHomologyMap' φ₂ h₁ h₂
⊢ leftHomologyMap' φ₁ h₁ h₂ = leftHomologyMap' φ₂ h₁ h₂
have rw₂ : leftHomologyMap' φ₂ h₁ h₂ + 0 = leftHomologyMap' φ₂ h₁ h₂
Tactic: rw [h.eq_add_nullHomotopic, leftHomologyMap'_add, leftHomologyMap'_nullHomotopic, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Preadditive (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ₁ φ₂ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
rw : leftHomologyMap' (φ₂ + S₁.nullHomotopic S₂ h.h₀ ⋯ h.h₁ h.h₂ h.h₃ ⋯) h₁ h₂ = leftHomologyMap' φ₂ h₁ h₂
rw₁ :
  leftHomologyMap' φ₂ h₁ h₂ + leftHomologyMap' (S₁.nullHomotopic S₂ h.h₀ ⋯ h.h₁ h.h₂ h.h₃ ⋯) h₁ h₂ =
    leftHomologyMap' φ₂ h₁ h₂
rw₂ : leftHomologyMap' φ₂ h₁ h₂ + 0 = leftHomologyMap' φ₂ h₁ h₂
⊢ leftHomologyMap' φ₁ h₁ h₂ = leftHomologyMap' φ₂ h₁ h₂
have rw₃ : leftHomologyMap' φ₂ h₁ h₂ = leftHomologyMap' φ₂ h₁ h₂
Tactic: rw [h.eq_add_nullHomotopic, leftHomologyMap'_add, leftHomologyMap'_nullHomotopic, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Preadditive (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ₁ φ₂ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
⊢ rightHomologyMap' φ₁ h₁ h₂ = rightHomologyMap' φ₂ h₁ h₂
have rw : rightHomologyMap' (φ₂ + S₁.nullHomotopic S₂ h.h₀ sorry h.h₁ h.h₂ h.h₃ sorry) h₁ h₂ = rightHomologyMap' φ₂ h₁ h₂
Tactic: rw [h.eq_add_nullHomotopic, rightHomologyMap'_add, rightHomologyMap'_nullHomotopic, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Preadditive (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ₁ φ₂ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
rw : rightHomologyMap' (φ₂ + S₁.nullHomotopic S₂ h.h₀ ⋯ h.h₁ h.h₂ h.h₃ ⋯) h₁ h₂ = rightHomologyMap' φ₂ h₁ h₂
⊢ rightHomologyMap' φ₁ h₁ h₂ = rightHomologyMap' φ₂ h₁ h₂
have rw₁ : rightHomologyMap' φ₂ h₁ h₂ + rightHomologyMap' (S₁.nullHomotopic S₂ h.h₀ sorry h.h₁ h.h₂ h.h₃ sorry) h₁ h₂ =
  rightHomologyMap' φ₂ h₁ h₂
Tactic: rw [h.eq_add_nullHomotopic, rightHomologyMap'_add, rightHomologyMap'_nullHomotopic, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Preadditive (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ₁ φ₂ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
rw : rightHomologyMap' (φ₂ + S₁.nullHomotopic S₂ h.h₀ ⋯ h.h₁ h.h₂ h.h₃ ⋯) h₁ h₂ = rightHomologyMap' φ₂ h₁ h₂
rw₁ :
  rightHomologyMap' φ₂ h₁ h₂ + rightHomologyMap' (S₁.nullHomotopic S₂ h.h₀ ⋯ h.h₁ h.h₂ h.h₃ ⋯) h₁ h₂ =
    rightHomologyMap' φ₂ h₁ h₂
⊢ rightHomologyMap' φ₁ h₁ h₂ = rightHomologyMap' φ₂ h₁ h₂
have rw₂ : rightHomologyMap' φ₂ h₁ h₂ + 0 = rightHomologyMap' φ₂ h₁ h₂
Tactic: rw [h.eq_add_nullHomotopic, rightHomologyMap'_add, rightHomologyMap'_nullHomotopic, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Preadditive (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ₁ φ₂ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
rw : rightHomologyMap' (φ₂ + S₁.nullHomotopic S₂ h.h₀ ⋯ h.h₁ h.h₂ h.h₃ ⋯) h₁ h₂ = rightHomologyMap' φ₂ h₁ h₂
rw₁ :
  rightHomologyMap' φ₂ h₁ h₂ + rightHomologyMap' (S₁.nullHomotopic S₂ h.h₀ ⋯ h.h₁ h.h₂ h.h₃ ⋯) h₁ h₂ =
    rightHomologyMap' φ₂ h₁ h₂
rw₂ : rightHomologyMap' φ₂ h₁ h₂ + 0 = rightHomologyMap' φ₂ h₁ h₂
⊢ rightHomologyMap' φ₁ h₁ h₂ = rightHomologyMap' φ₂ h₁ h₂
have rw₃ : rightHomologyMap' φ₂ h₁ h₂ = rightHomologyMap' φ₂ h₁ h₂
Tactic: rw [h.eq_add_nullHomotopic, rightHomologyMap'_add, rightHomologyMap'_nullHomotopic, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Preadditive (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ₁ φ₂ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
h₁ : S₁.HomologyData
h₂ : S₂.HomologyData
⊢ homologyMap' φ₁ h₁ h₂ = homologyMap' φ₂ h₁ h₂
have rw : homologyMap' (φ₂ + S₁.nullHomotopic S₂ h.h₀ sorry h.h₁ h.h₂ h.h₃ sorry) h₁ h₂ = homologyMap' φ₂ h₁ h₂
Tactic: rw [h.eq_add_nullHomotopic, homologyMap'_add, homologyMap'_nullHomotopic, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Preadditive (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ₁ φ₂ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
h₁ : S₁.HomologyData
h₂ : S₂.HomologyData
rw : homologyMap' (φ₂ + S₁.nullHomotopic S₂ h.h₀ ⋯ h.h₁ h.h₂ h.h₃ ⋯) h₁ h₂ = homologyMap' φ₂ h₁ h₂
⊢ homologyMap' φ₁ h₁ h₂ = homologyMap' φ₂ h₁ h₂
have rw₁ : homologyMap' φ₂ h₁ h₂ + homologyMap' (S₁.nullHomotopic S₂ h.h₀ sorry h.h₁ h.h₂ h.h₃ sorry) h₁ h₂ = homologyMap' φ₂ h₁ h₂
Tactic: rw [h.eq_add_nullHomotopic, homologyMap'_add, homologyMap'_nullHomotopic, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Preadditive (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ₁ φ₂ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
h₁ : S₁.HomologyData
h₂ : S₂.HomologyData
rw : homologyMap' (φ₂ + S₁.nullHomotopic S₂ h.h₀ ⋯ h.h₁ h.h₂ h.h₃ ⋯) h₁ h₂ = homologyMap' φ₂ h₁ h₂
rw₁ : homologyMap' φ₂ h₁ h₂ + homologyMap' (S₁.nullHomotopic S₂ h.h₀ ⋯ h.h₁ h.h₂ h.h₃ ⋯) h₁ h₂ = homologyMap' φ₂ h₁ h₂
⊢ homologyMap' φ₁ h₁ h₂ = homologyMap' φ₂ h₁ h₂
have rw₂ : homologyMap' φ₂ h₁ h₂ + 0 = homologyMap' φ₂ h₁ h₂
Tactic: rw [h.eq_add_nullHomotopic, homologyMap'_add, homologyMap'_nullHomotopic, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Preadditive (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ₁ φ₂ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
h₁ : S₁.HomologyData
h₂ : S₂.HomologyData
rw : homologyMap' (φ₂ + S₁.nullHomotopic S₂ h.h₀ ⋯ h.h₁ h.h₂ h.h₃ ⋯) h₁ h₂ = homologyMap' φ₂ h₁ h₂
rw₁ : homologyMap' φ₂ h₁ h₂ + homologyMap' (S₁.nullHomotopic S₂ h.h₀ ⋯ h.h₁ h.h₂ h.h₃ ⋯) h₁ h₂ = homologyMap' φ₂ h₁ h₂
rw₂ : homologyMap' φ₂ h₁ h₂ + 0 = homologyMap' φ₂ h₁ h₂
⊢ homologyMap' φ₁ h₁ h₂ = homologyMap' φ₂ h₁ h₂
have rw₃ : homologyMap' φ₂ h₁ h₂ = homologyMap' φ₂ h₁ h₂
Tactic: rw [h.eq_add_nullHomotopic, homologyMap'_add, homologyMap'_nullHomotopic, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Preadditive (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S₁ S₂ S₃ S : ShortComplex.{v_1, u_1} C
inst_2 : S.HasLeftHomology
A : C
k k' : A ⟶ S.X₂
hk : k ≫ S.g = 0
hk' : k' ≫ S.g = 0
⊢ (k + k') ≫ S.g = 0
have rw : k ≫ S.g + k' ≫ S.g = 0
Tactic: rw [add_comp, hk, hk', add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Preadditive (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S₁ S₂ S₃ S : ShortComplex.{v_1, u_1} C
inst_2 : S.HasLeftHomology
A : C
k k' : A ⟶ S.X₂
hk : k ≫ S.g = 0
hk' : k' ≫ S.g = 0
rw : k ≫ S.g + k' ≫ S.g = 0
⊢ (k + k') ≫ S.g = 0
have rw₁ : 0 + k' ≫ S.g = 0
Tactic: rw [add_comp, hk, hk', add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Preadditive (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S₁ S₂ S₃ S : ShortComplex.{v_1, u_1} C
inst_2 : S.HasLeftHomology
A : C
k k' : A ⟶ S.X₂
hk : k ≫ S.g = 0
hk' : k' ≫ S.g = 0
rw : k ≫ S.g + k' ≫ S.g = 0
rw₁ : 0 + k' ≫ S.g = 0
⊢ (k + k') ≫ S.g = 0
have rw₂ : HAdd.hAdd (α := A ⟶ S.X₃) 0 0 = 0
Tactic: rw [add_comp, hk, hk', add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Preadditive (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S₁ S₂ S₃ S : ShortComplex.{v_1, u_1} C
inst_2 : S.HasLeftHomology
A : C
k k' : A ⟶ S.X₂
hk : k ≫ S.g = 0
hk' : k' ≫ S.g = 0
rw : k ≫ S.g + k' ≫ S.g = 0
rw₁ : 0 + k' ≫ S.g = 0
rw₂ : HAdd.hAdd (α := A ⟶ S.X₃) 0 0 = 0
⊢ (k + k') ≫ S.g = 0
have rw₃ : Eq.{v_1 + 1} (α := A ⟶ S.X₃) 0 0
Tactic: rw [add_comp, hk, hk', add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Preadditive (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S₁ S₂ S₃ S : ShortComplex.{v_1, u_1} C
inst_2 : S.HasLeftHomology
A : C
k k' : A ⟶ S.X₂
hk : k ≫ S.g = 0
hk' : k' ≫ S.g = 0
⊢ (k - k') ≫ S.g = 0
have rw : k ≫ S.g - k' ≫ S.g = 0
Tactic: rw [sub_comp, hk, hk', sub_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Preadditive (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S₁ S₂ S₃ S : ShortComplex.{v_1, u_1} C
inst_2 : S.HasLeftHomology
A : C
k k' : A ⟶ S.X₂
hk : k ≫ S.g = 0
hk' : k' ≫ S.g = 0
rw : k ≫ S.g - k' ≫ S.g = 0
⊢ (k - k') ≫ S.g = 0
have rw₁ : 0 - k' ≫ S.g = 0
Tactic: rw [sub_comp, hk, hk', sub_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Preadditive (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S₁ S₂ S₃ S : ShortComplex.{v_1, u_1} C
inst_2 : S.HasLeftHomology
A : C
k k' : A ⟶ S.X₂
hk : k ≫ S.g = 0
hk' : k' ≫ S.g = 0
rw : k ≫ S.g - k' ≫ S.g = 0
rw₁ : 0 - k' ≫ S.g = 0
⊢ (k - k') ≫ S.g = 0
have rw₂ : HSub.hSub (α := A ⟶ S.X₃) 0 0 = 0
Tactic: rw [sub_comp, hk, hk', sub_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Preadditive (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S₁ S₂ S₃ S : ShortComplex.{v_1, u_1} C
inst_2 : S.HasLeftHomology
A : C
k k' : A ⟶ S.X₂
hk : k ≫ S.g = 0
hk' : k' ≫ S.g = 0
rw : k ≫ S.g - k' ≫ S.g = 0
rw₁ : 0 - k' ≫ S.g = 0
rw₂ : HSub.hSub (α := A ⟶ S.X₃) 0 0 = 0
⊢ (k - k') ≫ S.g = 0
have rw₃ : Eq.{v_1 + 1} (α := A ⟶ S.X₃) 0 0
Tactic: rw [sub_comp, hk, hk', sub_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.PreservesHomology (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : HasZeroMorphisms.{v_1, u_1} C
inst_3 : HasZeroMorphisms.{v_2, u_2} D
S : ShortComplex.{v_1, u_1} C
h : S.LeftHomologyData
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : h.IsPreservedBy F
⊢ f' (h.map F) = F.map h.f'
have rw : Eq (α := X₁ (S.map F) ⟶ X₂ (S.map F))
  (CategoryStruct.comp (Y := K (S := S.map F) (h.map F)) (f' (h.map F)) (i (h.map F))) (F.map h.f' ≫ i (h.map F))
Tactic: rw [← cancel_mono (h.map F).i, f'_i, map_f, map_i, ← F.map_comp, f'_i]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.PreservesHomology (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : HasZeroMorphisms.{v_1, u_1} C
inst_3 : HasZeroMorphisms.{v_2, u_2} D
S : ShortComplex.{v_1, u_1} C
h : S.LeftHomologyData
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : h.IsPreservedBy F
rw :
  Eq (α := X₁ (S.map F) ⟶ X₂ (S.map F))
    (CategoryStruct.comp (Y := K (S := S.map F) (h.map F)) (f' (h.map F)) (i (h.map F))) (F.map h.f' ≫ i (h.map F))
⊢ f' (h.map F) = F.map h.f'
have rw₁ : Eq (α := X₁ (S.map F) ⟶ X₂ (S.map F)) (f (S.map F)) (F.map h.f' ≫ i (h.map F))
Tactic: rw [← cancel_mono (h.map F).i, f'_i, map_f, map_i, ← F.map_comp, f'_i]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.PreservesHomology (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : HasZeroMorphisms.{v_1, u_1} C
inst_3 : HasZeroMorphisms.{v_2, u_2} D
S : ShortComplex.{v_1, u_1} C
h : S.LeftHomologyData
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : h.IsPreservedBy F
rw :
  Eq (α := X₁ (S.map F) ⟶ X₂ (S.map F))
    (CategoryStruct.comp (Y := K (S := S.map F) (h.map F)) (f' (h.map F)) (i (h.map F))) (F.map h.f' ≫ i (h.map F))
rw₁ : Eq (α := X₁ (S.map F) ⟶ X₂ (S.map F)) (f (S.map F)) (F.map h.f' ≫ i (h.map F))
⊢ f' (h.map F) = F.map h.f'
have rw₂ : F.map S.f = F.map h.f' ≫ i (h.map F)
Tactic: rw [← cancel_mono (h.map F).i, f'_i, map_f, map_i, ← F.map_comp, f'_i]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.PreservesHomology (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : HasZeroMorphisms.{v_1, u_1} C
inst_3 : HasZeroMorphisms.{v_2, u_2} D
S : ShortComplex.{v_1, u_1} C
h : S.LeftHomologyData
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : h.IsPreservedBy F
rw :
  Eq (α := X₁ (S.map F) ⟶ X₂ (S.map F))
    (CategoryStruct.comp (Y := K (S := S.map F) (h.map F)) (f' (h.map F)) (i (h.map F))) (F.map h.f' ≫ i (h.map F))
rw₁ : Eq (α := X₁ (S.map F) ⟶ X₂ (S.map F)) (f (S.map F)) (F.map h.f' ≫ i (h.map F))
rw₂ : F.map S.f = F.map h.f' ≫ i (h.map F)
⊢ f' (h.map F) = F.map h.f'
have rw₃ : F.map S.f = F.map h.f' ≫ F.map h.i
Tactic: rw [← cancel_mono (h.map F).i, f'_i, map_f, map_i, ← F.map_comp, f'_i]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.PreservesHomology (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : HasZeroMorphisms.{v_1, u_1} C
inst_3 : HasZeroMorphisms.{v_2, u_2} D
S : ShortComplex.{v_1, u_1} C
h : S.LeftHomologyData
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : h.IsPreservedBy F
rw :
  Eq (α := X₁ (S.map F) ⟶ X₂ (S.map F))
    (CategoryStruct.comp (Y := K (S := S.map F) (h.map F)) (f' (h.map F)) (i (h.map F))) (F.map h.f' ≫ i (h.map F))
rw₁ : Eq (α := X₁ (S.map F) ⟶ X₂ (S.map F)) (f (S.map F)) (F.map h.f' ≫ i (h.map F))
rw₂ : F.map S.f = F.map h.f' ≫ i (h.map F)
rw₃ : F.map S.f = F.map h.f' ≫ F.map h.i
⊢ f' (h.map F) = F.map h.f'
have rw₄ : F.map S.f = F.map (h.f' ≫ h.i)
Tactic: rw [← cancel_mono (h.map F).i, f'_i, map_f, map_i, ← F.map_comp, f'_i]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.PreservesHomology (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : HasZeroMorphisms.{v_1, u_1} C
inst_3 : HasZeroMorphisms.{v_2, u_2} D
S : ShortComplex.{v_1, u_1} C
h : S.LeftHomologyData
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : h.IsPreservedBy F
rw :
  Eq (α := X₁ (S.map F) ⟶ X₂ (S.map F))
    (CategoryStruct.comp (Y := K (S := S.map F) (h.map F)) (f' (h.map F)) (i (h.map F))) (F.map h.f' ≫ i (h.map F))
rw₁ : Eq (α := X₁ (S.map F) ⟶ X₂ (S.map F)) (f (S.map F)) (F.map h.f' ≫ i (h.map F))
rw₂ : F.map S.f = F.map h.f' ≫ i (h.map F)
rw₃ : F.map S.f = F.map h.f' ≫ F.map h.i
rw₄ : F.map S.f = F.map (h.f' ≫ h.i)
⊢ f' (h.map F) = F.map h.f'
have rw₅ : F.map S.f = F.map S.f
Tactic: rw [← cancel_mono (h.map F).i, f'_i, map_f, map_i, ← F.map_comp, f'_i]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.PreservesHomology (hypothesis)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : HasZeroMorphisms.{v_1, u_1} C
inst_3 : HasZeroMorphisms.{v_2, u_2} D
S S₁ S₂ : ShortComplex.{v_1, u_1} C
h : S.RightHomologyData
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : h.IsPreservedBy F
⊢ RightHomologyData (S.map F)
have this : PreservesColimit (parallelPair S.f 0) F
Tactic: have := IsPreservedBy.hf h F
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.PreservesHomology (hypothesis)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : HasZeroMorphisms.{v_1, u_1} C
inst_3 : HasZeroMorphisms.{v_2, u_2} D
S S₁ S₂ : ShortComplex.{v_1, u_1} C
h : S.RightHomologyData
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : h.IsPreservedBy F
this : PreservesColimit (parallelPair S.f 0) F
⊢ RightHomologyData (S.map F)
have this₁ : PreservesLimit (parallelPair h.g' 0) F
Tactic: have := IsPreservedBy.hg' h F
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.PreservesHomology (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : HasZeroMorphisms.{v_1, u_1} C
inst_3 : HasZeroMorphisms.{v_2, u_2} D
S S₁ S₂ : ShortComplex.{v_1, u_1} C
h : S.RightHomologyData
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : h.IsPreservedBy F
this_1 : PreservesColimit (parallelPair S.f 0) F
this : PreservesLimit (parallelPair h.g' 0) F
⊢ F.map S.f ≫ F.map h.p = 0
have rw : F.map (S.f ≫ h.p) = 0
Tactic: rw [← F.map_comp, h.wp, F.map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.PreservesHomology (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : HasZeroMorphisms.{v_1, u_1} C
inst_3 : HasZeroMorphisms.{v_2, u_2} D
S S₁ S₂ : ShortComplex.{v_1, u_1} C
h : S.RightHomologyData
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : h.IsPreservedBy F
this_1 : PreservesColimit (parallelPair S.f 0) F
this : PreservesLimit (parallelPair h.g' 0) F
rw : F.map (S.f ≫ h.p) = 0
⊢ F.map S.f ≫ F.map h.p = 0
have rw₁ : Eq (α := F.obj S.X₁ ⟶ F.obj h.Q) (F.map 0) 0
Tactic: rw [← F.map_comp, h.wp, F.map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.PreservesHomology (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : HasZeroMorphisms.{v_1, u_1} C
inst_3 : HasZeroMorphisms.{v_2, u_2} D
S S₁ S₂ : ShortComplex.{v_1, u_1} C
h : S.RightHomologyData
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : h.IsPreservedBy F
this_1 : PreservesColimit (parallelPair S.f 0) F
this : PreservesLimit (parallelPair h.g' 0) F
rw : F.map (S.f ≫ h.p) = 0
rw₁ : Eq (α := F.obj S.X₁ ⟶ F.obj h.Q) (F.map 0) 0
⊢ F.map S.f ≫ F.map h.p = 0
have rw₂ : Eq.{v_2 + 1} (α := F.obj S.X₁ ⟶ F.obj h.Q) 0 0
Tactic: rw [← F.map_comp, h.wp, F.map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.PreservesHomology (hypothesis)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : HasZeroMorphisms.{v_1, u_1} C
inst_3 : HasZeroMorphisms.{v_2, u_2} D
S S₁ S₂ : ShortComplex.{v_1, u_1} C
h : S.RightHomologyData
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : h.IsPreservedBy F
this_1 : PreservesColimit (parallelPair S.f 0) F
this : PreservesLimit (parallelPair h.g' 0) F
⊢ RightHomologyData (S.map F)
have wp : F.map S.f ≫ F.map h.p = 0
Tactic: have wp : F.map S.f ≫ F.map h.p = 0 := by rw [← F.map_comp, h.wp, F.map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.PreservesHomology (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : HasZeroMorphisms.{v_1, u_1} C
inst_3 : HasZeroMorphisms.{v_2, u_2} D
S S₁ S₂ : ShortComplex.{v_1, u_1} C
h : S.RightHomologyData
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : h.IsPreservedBy F
this_1 : PreservesColimit (parallelPair S.f 0) F
this : PreservesLimit (parallelPair h.g' 0) F
wp : F.map S.f ≫ F.map h.p = 0
⊢ RightHomologyData (S.map F)
have have : (hp : IsColimit (F := parallelPair (F.map S.f) 0) ((CokernelCofork.ofπ h.p sorry).map F)) → RightHomologyData (S.map F)
Tactic: have hp := CokernelCofork.mapIsColimit _ h.hp F