awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.TruncLEHomology (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : Abelian.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_2 : e.IsTruncLE
i : ι
hi : ¬∃ (j' : ι'), c'.Rel (e.f i) j'
this :
  IsIso (X := (K.shortComplexTruncLE e).X₁.homology (e.f i)) (Y := (K.shortComplexTruncLE e).X₂.homology (e.f i))
    (homologyMap (K.shortComplexTruncLE e).f (e.f i))
neg :
  Eq.{v_1 + 1} (α := (K.shortComplexTruncLE e).X₃.homology (e.f i) ⟶ (K.shortComplexTruncLE e).X₃.homology (e.f i))
    (𝟙 ((K.shortComplexTruncLE e).X₃.homology (e.f i))) 0
neg₁ :
  Eq (α := (K.shortComplexTruncLE e).X₂.homology (e.f i) ⟶ (K.shortComplexTruncLE e).X₃.homology (e.f i))
    (homologyMap (K.shortComplexTruncLE e).g (e.f i) ≫ 𝟙 ((K.shortComplexTruncLE e).X₃.homology (e.f i)))
    (CategoryStruct.comp (Y := (K.shortComplexTruncLE e).X₃.homology (e.f i))
      (homologyMap (K.shortComplexTruncLE e).g (e.f i)) 0)
neg₂ :
  Eq (α := (K.shortComplexTruncLE e).X₂.homology (e.f i) ⟶ (K.shortComplexTruncLE e).X₃.homology (e.f i))
    (homologyMap (K.shortComplexTruncLE e).g (e.f i))
    (CategoryStruct.comp (Y := (K.shortComplexTruncLE e).X₃.homology (e.f i))
      (homologyMap (K.shortComplexTruncLE e).g (e.f i)) 0)
neg₃ :
  Eq (α := (K.shortComplexTruncLE e).X₂.homology (e.f i) ⟶ (K.shortComplexTruncLE e).X₃.homology (e.f i))
    (homologyMap (K.shortComplexTruncLE e).g (e.f i)) 0
neg₄ :
  Eq (α := (K.shortComplexTruncLE e).X₁.homology (e.f i) ⟶ (K.shortComplexTruncLE e).X₃.homology (e.f i))
    (CategoryStruct.comp (Y := (K.shortComplexTruncLE e).X₂.homology (e.f i))
      (homologyMap (K.shortComplexTruncLE e).f (e.f i)) (homologyMap (K.shortComplexTruncLE e).g (e.f i)))
    (CategoryStruct.comp (Y := (K.shortComplexTruncLE e).X₂.homology (e.f i))
      (homologyMap (K.shortComplexTruncLE e).f (e.f i)) 0)
⊢ IsZero.{v_1, u_3} ((K.shortComplexTruncLE e).X₃.homology (e.f i))
have neg₅ : Eq (α := (K.shortComplexTruncLE e).X₁.homology (e.f i) ⟶ (K.shortComplexTruncLE e).X₃.homology (e.f i))
  (CategoryStruct.comp (Y := (K.shortComplexTruncLE e).X₂.homology (e.f i))
    (homologyMap (K.shortComplexTruncLE e).f (e.f i)) (homologyMap (K.shortComplexTruncLE e).g (e.f i)))
  0
Tactic: rw [IsZero.iff_id_eq_zero, ← cancel_epi (homologyMap (K.shortComplexTruncLE e).g (e.f i)),
        comp_id, comp_zero, ← cancel_epi (homologyMap (K.shortComplexTruncLE e).f (e.f i)),
        comp_zero, ← homologyMap_comp, ShortComplex.zero, homologyMap_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.TruncLEHomology (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : Abelian.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_2 : e.IsTruncLE
i : ι
hi : ¬∃ (j' : ι'), c'.Rel (e.f i) j'
this :
  IsIso (X := (K.shortComplexTruncLE e).X₁.homology (e.f i)) (Y := (K.shortComplexTruncLE e).X₂.homology (e.f i))
    (homologyMap (K.shortComplexTruncLE e).f (e.f i))
neg :
  Eq.{v_1 + 1} (α := (K.shortComplexTruncLE e).X₃.homology (e.f i) ⟶ (K.shortComplexTruncLE e).X₃.homology (e.f i))
    (𝟙 ((K.shortComplexTruncLE e).X₃.homology (e.f i))) 0
neg₁ :
  Eq (α := (K.shortComplexTruncLE e).X₂.homology (e.f i) ⟶ (K.shortComplexTruncLE e).X₃.homology (e.f i))
    (homologyMap (K.shortComplexTruncLE e).g (e.f i) ≫ 𝟙 ((K.shortComplexTruncLE e).X₃.homology (e.f i)))
    (CategoryStruct.comp (Y := (K.shortComplexTruncLE e).X₃.homology (e.f i))
      (homologyMap (K.shortComplexTruncLE e).g (e.f i)) 0)
neg₂ :
  Eq (α := (K.shortComplexTruncLE e).X₂.homology (e.f i) ⟶ (K.shortComplexTruncLE e).X₃.homology (e.f i))
    (homologyMap (K.shortComplexTruncLE e).g (e.f i))
    (CategoryStruct.comp (Y := (K.shortComplexTruncLE e).X₃.homology (e.f i))
      (homologyMap (K.shortComplexTruncLE e).g (e.f i)) 0)
neg₃ :
  Eq (α := (K.shortComplexTruncLE e).X₂.homology (e.f i) ⟶ (K.shortComplexTruncLE e).X₃.homology (e.f i))
    (homologyMap (K.shortComplexTruncLE e).g (e.f i)) 0
neg₄ :
  Eq (α := (K.shortComplexTruncLE e).X₁.homology (e.f i) ⟶ (K.shortComplexTruncLE e).X₃.homology (e.f i))
    (CategoryStruct.comp (Y := (K.shortComplexTruncLE e).X₂.homology (e.f i))
      (homologyMap (K.shortComplexTruncLE e).f (e.f i)) (homologyMap (K.shortComplexTruncLE e).g (e.f i)))
    (CategoryStruct.comp (Y := (K.shortComplexTruncLE e).X₂.homology (e.f i))
      (homologyMap (K.shortComplexTruncLE e).f (e.f i)) 0)
neg₅ :
  Eq (α := (K.shortComplexTruncLE e).X₁.homology (e.f i) ⟶ (K.shortComplexTruncLE e).X₃.homology (e.f i))
    (CategoryStruct.comp (Y := (K.shortComplexTruncLE e).X₂.homology (e.f i))
      (homologyMap (K.shortComplexTruncLE e).f (e.f i)) (homologyMap (K.shortComplexTruncLE e).g (e.f i)))
    0
⊢ IsZero.{v_1, u_3} ((K.shortComplexTruncLE e).X₃.homology (e.f i))
have neg₆ : Eq (α := (K.shortComplexTruncLE e).X₁.homology (e.f i) ⟶ (K.shortComplexTruncLE e).X₃.homology (e.f i))
  (homologyMap ((K.shortComplexTruncLE e).f ≫ (K.shortComplexTruncLE e).g) (e.f i)) 0
Tactic: rw [IsZero.iff_id_eq_zero, ← cancel_epi (homologyMap (K.shortComplexTruncLE e).g (e.f i)),
        comp_id, comp_zero, ← cancel_epi (homologyMap (K.shortComplexTruncLE e).f (e.f i)),
        comp_zero, ← homologyMap_comp, ShortComplex.zero, homologyMap_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.TruncLEHomology (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : Abelian.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_2 : e.IsTruncLE
i : ι
hi : ¬∃ (j' : ι'), c'.Rel (e.f i) j'
this :
  IsIso (X := (K.shortComplexTruncLE e).X₁.homology (e.f i)) (Y := (K.shortComplexTruncLE e).X₂.homology (e.f i))
    (homologyMap (K.shortComplexTruncLE e).f (e.f i))
neg :
  Eq.{v_1 + 1} (α := (K.shortComplexTruncLE e).X₃.homology (e.f i) ⟶ (K.shortComplexTruncLE e).X₃.homology (e.f i))
    (𝟙 ((K.shortComplexTruncLE e).X₃.homology (e.f i))) 0
neg₁ :
  Eq (α := (K.shortComplexTruncLE e).X₂.homology (e.f i) ⟶ (K.shortComplexTruncLE e).X₃.homology (e.f i))
    (homologyMap (K.shortComplexTruncLE e).g (e.f i) ≫ 𝟙 ((K.shortComplexTruncLE e).X₃.homology (e.f i)))
    (CategoryStruct.comp (Y := (K.shortComplexTruncLE e).X₃.homology (e.f i))
      (homologyMap (K.shortComplexTruncLE e).g (e.f i)) 0)
neg₂ :
  Eq (α := (K.shortComplexTruncLE e).X₂.homology (e.f i) ⟶ (K.shortComplexTruncLE e).X₃.homology (e.f i))
    (homologyMap (K.shortComplexTruncLE e).g (e.f i))
    (CategoryStruct.comp (Y := (K.shortComplexTruncLE e).X₃.homology (e.f i))
      (homologyMap (K.shortComplexTruncLE e).g (e.f i)) 0)
neg₃ :
  Eq (α := (K.shortComplexTruncLE e).X₂.homology (e.f i) ⟶ (K.shortComplexTruncLE e).X₃.homology (e.f i))
    (homologyMap (K.shortComplexTruncLE e).g (e.f i)) 0
neg₄ :
  Eq (α := (K.shortComplexTruncLE e).X₁.homology (e.f i) ⟶ (K.shortComplexTruncLE e).X₃.homology (e.f i))
    (CategoryStruct.comp (Y := (K.shortComplexTruncLE e).X₂.homology (e.f i))
      (homologyMap (K.shortComplexTruncLE e).f (e.f i)) (homologyMap (K.shortComplexTruncLE e).g (e.f i)))
    (CategoryStruct.comp (Y := (K.shortComplexTruncLE e).X₂.homology (e.f i))
      (homologyMap (K.shortComplexTruncLE e).f (e.f i)) 0)
neg₅ :
  Eq (α := (K.shortComplexTruncLE e).X₁.homology (e.f i) ⟶ (K.shortComplexTruncLE e).X₃.homology (e.f i))
    (CategoryStruct.comp (Y := (K.shortComplexTruncLE e).X₂.homology (e.f i))
      (homologyMap (K.shortComplexTruncLE e).f (e.f i)) (homologyMap (K.shortComplexTruncLE e).g (e.f i)))
    0
neg₆ :
  Eq (α := (K.shortComplexTruncLE e).X₁.homology (e.f i) ⟶ (K.shortComplexTruncLE e).X₃.homology (e.f i))
    (homologyMap ((K.shortComplexTruncLE e).f ≫ (K.shortComplexTruncLE e).g) (e.f i)) 0
⊢ IsZero.{v_1, u_3} ((K.shortComplexTruncLE e).X₃.homology (e.f i))
have neg₇ : Eq.{v_1 + 1} (α := (K.shortComplexTruncLE e).X₁.homology (e.f i) ⟶ (K.shortComplexTruncLE e).X₃.homology (e.f i))
  (homologyMap 0 (e.f i)) 0
Tactic: rw [IsZero.iff_id_eq_zero, ← cancel_epi (homologyMap (K.shortComplexTruncLE e).g (e.f i)),
        comp_id, comp_zero, ← cancel_epi (homologyMap (K.shortComplexTruncLE e).f (e.f i)),
        comp_zero, ← homologyMap_comp, ShortComplex.zero, homologyMap_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.TruncLEHomology (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : Abelian.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_2 : e.IsTruncLE
i : ι
hi : ¬∃ (j' : ι'), c'.Rel (e.f i) j'
this :
  IsIso (X := (K.shortComplexTruncLE e).X₁.homology (e.f i)) (Y := (K.shortComplexTruncLE e).X₂.homology (e.f i))
    (homologyMap (K.shortComplexTruncLE e).f (e.f i))
neg :
  Eq.{v_1 + 1} (α := (K.shortComplexTruncLE e).X₃.homology (e.f i) ⟶ (K.shortComplexTruncLE e).X₃.homology (e.f i))
    (𝟙 ((K.shortComplexTruncLE e).X₃.homology (e.f i))) 0
neg₁ :
  Eq (α := (K.shortComplexTruncLE e).X₂.homology (e.f i) ⟶ (K.shortComplexTruncLE e).X₃.homology (e.f i))
    (homologyMap (K.shortComplexTruncLE e).g (e.f i) ≫ 𝟙 ((K.shortComplexTruncLE e).X₃.homology (e.f i)))
    (CategoryStruct.comp (Y := (K.shortComplexTruncLE e).X₃.homology (e.f i))
      (homologyMap (K.shortComplexTruncLE e).g (e.f i)) 0)
neg₂ :
  Eq (α := (K.shortComplexTruncLE e).X₂.homology (e.f i) ⟶ (K.shortComplexTruncLE e).X₃.homology (e.f i))
    (homologyMap (K.shortComplexTruncLE e).g (e.f i))
    (CategoryStruct.comp (Y := (K.shortComplexTruncLE e).X₃.homology (e.f i))
      (homologyMap (K.shortComplexTruncLE e).g (e.f i)) 0)
neg₃ :
  Eq (α := (K.shortComplexTruncLE e).X₂.homology (e.f i) ⟶ (K.shortComplexTruncLE e).X₃.homology (e.f i))
    (homologyMap (K.shortComplexTruncLE e).g (e.f i)) 0
neg₄ :
  Eq (α := (K.shortComplexTruncLE e).X₁.homology (e.f i) ⟶ (K.shortComplexTruncLE e).X₃.homology (e.f i))
    (CategoryStruct.comp (Y := (K.shortComplexTruncLE e).X₂.homology (e.f i))
      (homologyMap (K.shortComplexTruncLE e).f (e.f i)) (homologyMap (K.shortComplexTruncLE e).g (e.f i)))
    (CategoryStruct.comp (Y := (K.shortComplexTruncLE e).X₂.homology (e.f i))
      (homologyMap (K.shortComplexTruncLE e).f (e.f i)) 0)
neg₅ :
  Eq (α := (K.shortComplexTruncLE e).X₁.homology (e.f i) ⟶ (K.shortComplexTruncLE e).X₃.homology (e.f i))
    (CategoryStruct.comp (Y := (K.shortComplexTruncLE e).X₂.homology (e.f i))
      (homologyMap (K.shortComplexTruncLE e).f (e.f i)) (homologyMap (K.shortComplexTruncLE e).g (e.f i)))
    0
neg₆ :
  Eq (α := (K.shortComplexTruncLE e).X₁.homology (e.f i) ⟶ (K.shortComplexTruncLE e).X₃.homology (e.f i))
    (homologyMap ((K.shortComplexTruncLE e).f ≫ (K.shortComplexTruncLE e).g) (e.f i)) 0
neg₇ :
  Eq.{v_1 + 1} (α := (K.shortComplexTruncLE e).X₁.homology (e.f i) ⟶ (K.shortComplexTruncLE e).X₃.homology (e.f i))
    (homologyMap 0 (e.f i)) 0
⊢ IsZero.{v_1, u_3} ((K.shortComplexTruncLE e).X₃.homology (e.f i))
have neg₈ : Eq.{v_1 + 1} (α := (K.shortComplexTruncLE e).X₁.homology (e.f i) ⟶ (K.shortComplexTruncLE e).X₃.homology (e.f i)) 0 0
Tactic: rw [IsZero.iff_id_eq_zero, ← cancel_epi (homologyMap (K.shortComplexTruncLE e).g (e.f i)),
        comp_id, comp_zero, ← cancel_epi (homologyMap (K.shortComplexTruncLE e).f (e.f i)),
        comp_zero, ← homologyMap_comp, ShortComplex.zero, homologyMap_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.EulerCharacteristic (goal)
Goal:
ι : Type u_1
c : ComplexShape ι
inst : c.EulerCharSigns
i : ℤ
⊢ (i + 1).negOnePow = -i.negOnePow
have rw : -i.negOnePow = -i.negOnePow
Tactic: rw [Int.negOnePow_succ]
-- Lean 4 proof step from Mathlib.Algebra.Homology.EulerCharacteristic (goal)
Goal:
R : Type u_1
inst : Ring R
ι : Type u_2
c : ComplexShape ι
inst_1 : c.EulerCharSigns
X : GradedObject ι (ModuleCat.{u_3, u_1} R)
⊢ (Function.support (M := ℤ) fun (i : ι) ↦ (↑(c.χ i) : ℤ) * (↑(Module.finrank.{u_1, u_3} R (↑(X i) : Type u_3)) : ℤ)) =
    finrankSupport X
have simp : Eq.{u_2 + 1} (α := Set ι)
  (Function.support (M := ℤ) fun (x : ι) ↦ (↑(Module.finrank.{u_1, u_3} R (↑(X x) : Type u_3)) : ℤ))
  (Function.support (M := ℕ) fun (i : ι) ↦ Module.finrank.{u_1, u_3} R (↑(X i) : Type u_3))
Tactic: simp only [finrankSupport, Function.support_mul_of_ne_zero_left (fun i => Units.ne_zero (c.χ i))]
-- Lean 4 proof step from Mathlib.Algebra.Homology.EulerCharacteristic (goal)
Goal:
R : Type u_1
inst : Ring R
ι : Type u_2
c : ComplexShape ι
inst_1 : c.EulerCharSigns
X : GradedObject ι (ModuleCat.{u_3, u_1} R)
⊢ Eq.{u_2 + 1} (α := Set ι)
    (Function.support (M := ℤ) fun (x : ι) ↦ (↑(Module.finrank.{u_1, u_3} R (↑(X x) : Type u_3)) : ℤ))
    (Function.support (M := ℕ) fun (i : ι) ↦ Module.finrank.{u_1, u_3} R (↑(X i) : Type u_3))
have h : ∀ (i : ι),
  Membership.mem (γ := Set ι)
      (Function.support (M := ℤ) fun (x : ι) ↦ (↑(Module.finrank.{u_1, u_3} R (↑(X x) : Type u_3)) : ℤ)) i ↔
    Membership.mem (γ := Set ι)
      (Function.support (M := ℕ) fun (i : ι) ↦ Module.finrank.{u_1, u_3} R (↑(X i) : Type u_3)) i
Tactic: ext i
-- Lean 4 proof step from Mathlib.Algebra.Homology.EulerCharacteristic (goal)
Goal:
R : Type u_1
inst : Ring R
ι : Type u_2
c : ComplexShape ι
inst_1 : c.EulerCharSigns
X : GradedObject ι (ModuleCat.{u_3, u_1} R)
indices : Finset ι
h_support : finrankSupport X ⊆ (↑indices : Set ι)
⊢ Eq (α := ℤ) (∑ᶠ (i : ι), (↑(c.χ i) : ℤ) * (↑(Module.finrank.{u_1, u_3} R (↑(X i) : Type u_3)) : ℤ))
    (∑ i ∈ indices, (↑(c.χ i) : ℤ) * (↑(Module.finrank.{u_1, u_3} R (↑(X i) : Type u_3)) : ℤ))
have h : (Function.support (M := ℤ) fun (i : ι) ↦ (↑(c.χ i) : ℤ) * (↑(Module.finrank.{u_1, u_3} R (↑(X i) : Type u_3)) : ℤ)) ⊆
  (↑indices : Set ι)
Tactic: rw [finsum_eq_sum_of_support_subset]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ExactSequenceFour (hypothesis)
Goal:
C : Type u_1
inst : Category.{u_2, u_1} C
inst_1 : Preadditive.{u_2, u_1} C
n : ℕ
S : ComposableArrows.{u_2, u_1} C (n + 3)
hS : S.IsComplex
k : ℕ
hk : k ≤ n
cc :
  CokernelCofork (X := S.obj ⟨k, ⋯⟩) (Y := S.obj ⟨k + 1, ⋯⟩)
    (S.map' k (k + 1) ⋯ ⋯ : S.obj (⟨k, ⋯⟩ : Fin (n + 3 + 1)) ⟶ S.obj ⟨k + 1, ⋯⟩)
kf :
  KernelFork (X := S.obj ⟨k + 2, ⋯⟩) (Y := S.obj ⟨k + 3, ⋯⟩)
    (S.map' (k + 2) (k + 3) ⋯ ⋯ : S.obj (⟨k + 2, ⋯⟩ : Fin (n + 3 + 1)) ⟶ S.obj ⟨k + 3, ⋯⟩)
hcc : IsColimit cc
hkf : IsLimit kf
hS' : (S.sc hS (k + 1) ⋯).Exact
⊢ Epi (hS.cokerToKer' k hk cc kf hcc hkf)
have this : HasZeroObject.{u_2, u_1} C
Tactic: have := hS'.hasZeroObject
-- Lean 4 proof step from Mathlib.Algebra.Homology.ExactSequenceFour (hypothesis)
Goal:
C : Type u_1
inst : Category.{u_2, u_1} C
inst_1 : Preadditive.{u_2, u_1} C
n : ℕ
S : ComposableArrows.{u_2, u_1} C (n + 3)
hS : S.IsComplex
k : ℕ
hk : k ≤ n
cc :
  CokernelCofork (X := S.obj ⟨k, ⋯⟩) (Y := S.obj ⟨k + 1, ⋯⟩)
    (S.map' k (k + 1) ⋯ ⋯ : S.obj (⟨k, ⋯⟩ : Fin (n + 3 + 1)) ⟶ S.obj ⟨k + 1, ⋯⟩)
kf :
  KernelFork (X := S.obj ⟨k + 2, ⋯⟩) (Y := S.obj ⟨k + 3, ⋯⟩)
    (S.map' (k + 2) (k + 3) ⋯ ⋯ : S.obj (⟨k + 2, ⋯⟩ : Fin (n + 3 + 1)) ⟶ S.obj ⟨k + 3, ⋯⟩)
hcc : IsColimit cc
hkf : IsLimit kf
hS' : (S.sc hS (k + 1) ⋯).Exact
this : HasZeroObject.{u_2, u_1} C
⊢ Epi (hS.cokerToKer' k hk cc kf hcc hkf)
have this₁ : (S.sc hS (k + 1) sorry).HasHomology
Tactic: have := hS'.hasHomology
-- Lean 4 proof step from Mathlib.Algebra.Homology.ExactSequenceFour (hypothesis)
Goal:
C : Type u_1
inst : Category.{u_2, u_1} C
inst_1 : Preadditive.{u_2, u_1} C
n : ℕ
S : ComposableArrows.{u_2, u_1} C (n + 3)
hS : S.IsComplex
k : ℕ
hk : k ≤ n
cc :
  CokernelCofork (X := S.obj ⟨k, ⋯⟩) (Y := S.obj ⟨k + 1, ⋯⟩)
    (S.map' k (k + 1) ⋯ ⋯ : S.obj (⟨k, ⋯⟩ : Fin (n + 3 + 1)) ⟶ S.obj ⟨k + 1, ⋯⟩)
kf :
  KernelFork (X := S.obj ⟨k + 2, ⋯⟩) (Y := S.obj ⟨k + 3, ⋯⟩)
    (S.map' (k + 2) (k + 3) ⋯ ⋯ : S.obj (⟨k + 2, ⋯⟩ : Fin (n + 3 + 1)) ⟶ S.obj ⟨k + 3, ⋯⟩)
hcc : IsColimit cc
hkf : IsLimit kf
hS' : (S.sc hS (k + 1) ⋯).Exact
this_1 : HasZeroObject.{u_2, u_1} C
this : (S.sc hS (k + 1) ⋯).HasHomology
h : (S.sc hS (k + 1) ⋯).LeftHomologyData := hS'.leftHomologyDataOfIsLimitKernelFork kf hkf
⊢ Epi (hS.cokerToKer' k hk cc kf hcc hkf)
have this₁ : Epi h.f'
Tactic: have := h.exact_iff_epi_f'.1 hS'
-- Lean 4 proof step from Mathlib.Algebra.Homology.ExactSequenceFour (goal)
Goal:
C : Type u_1
inst : Category.{u_2, u_1} C
inst_1 : Preadditive.{u_2, u_1} C
n : ℕ
S : ComposableArrows.{u_2, u_1} C (n + 3)
hS : S.IsComplex
k : ℕ
hk : k ≤ n
cc :
  CokernelCofork (X := S.obj ⟨k, ⋯⟩) (Y := S.obj ⟨k + 1, ⋯⟩)
    (S.map' k (k + 1) ⋯ ⋯ : S.obj (⟨k, ⋯⟩ : Fin (n + 3 + 1)) ⟶ S.obj ⟨k + 1, ⋯⟩)
kf :
  KernelFork (X := S.obj ⟨k + 2, ⋯⟩) (Y := S.obj ⟨k + 3, ⋯⟩)
    (S.map' (k + 2) (k + 3) ⋯ ⋯ : S.obj (⟨k + 2, ⋯⟩ : Fin (n + 3 + 1)) ⟶ S.obj ⟨k + 3, ⋯⟩)
hcc : IsColimit cc
hkf : IsLimit kf
hS' : (S.sc hS (k + 1) ⋯).Exact
this_1 : HasZeroObject.{u_2, u_1} C
this_2 : (S.sc hS (k + 1) ⋯).HasHomology
h : (S.sc hS (k + 1) ⋯).LeftHomologyData := hS'.leftHomologyDataOfIsLimitKernelFork kf hkf
this : Epi h.f'
⊢ Cofork.π cc ≫ hS.cokerToKer' k hk cc kf hcc hkf = h.f'
have rw : (Cofork.π cc ≫ hS.cokerToKer' k hk cc kf hcc hkf) ≫ h.i = h.f' ≫ h.i
Tactic: rw [← cancel_mono h.i, h.f'_i, ShortComplex.Exact.leftHomologyDataOfIsLimitKernelFork_i,
      assoc, IsComplex.cokerToKer'_fac]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ExactSequenceFour (goal)
Goal:
C : Type u_1
inst : Category.{u_2, u_1} C
inst_1 : Preadditive.{u_2, u_1} C
n : ℕ
S : ComposableArrows.{u_2, u_1} C (n + 3)
hS : S.IsComplex
k : ℕ
hk : k ≤ n
cc :
  CokernelCofork (X := S.obj ⟨k, ⋯⟩) (Y := S.obj ⟨k + 1, ⋯⟩)
    (S.map' k (k + 1) ⋯ ⋯ : S.obj (⟨k, ⋯⟩ : Fin (n + 3 + 1)) ⟶ S.obj ⟨k + 1, ⋯⟩)
kf :
  KernelFork (X := S.obj ⟨k + 2, ⋯⟩) (Y := S.obj ⟨k + 3, ⋯⟩)
    (S.map' (k + 2) (k + 3) ⋯ ⋯ : S.obj (⟨k + 2, ⋯⟩ : Fin (n + 3 + 1)) ⟶ S.obj ⟨k + 3, ⋯⟩)
hcc : IsColimit cc
hkf : IsLimit kf
hS' : (S.sc hS (k + 1) ⋯).Exact
this_1 : HasZeroObject.{u_2, u_1} C
this_2 : (S.sc hS (k + 1) ⋯).HasHomology
h : (S.sc hS (k + 1) ⋯).LeftHomologyData := hS'.leftHomologyDataOfIsLimitKernelFork kf hkf
this : Epi h.f'
rw : (Cofork.π cc ≫ hS.cokerToKer' k hk cc kf hcc hkf) ≫ h.i = h.f' ≫ h.i
⊢ Cofork.π cc ≫ hS.cokerToKer' k hk cc kf hcc hkf = h.f'
have rw₁ : (Cofork.π cc ≫ hS.cokerToKer' k hk cc kf hcc hkf) ≫ h.i = (S.sc hS (k + 1) sorry).f
Tactic: rw [← cancel_mono h.i, h.f'_i, ShortComplex.Exact.leftHomologyDataOfIsLimitKernelFork_i,
      assoc, IsComplex.cokerToKer'_fac]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ExactSequenceFour (goal)
Goal:
C : Type u_1
inst : Category.{u_2, u_1} C
inst_1 : Preadditive.{u_2, u_1} C
n : ℕ
S : ComposableArrows.{u_2, u_1} C (n + 3)
hS : S.IsComplex
k : ℕ
hk : k ≤ n
cc :
  CokernelCofork (X := S.obj ⟨k, ⋯⟩) (Y := S.obj ⟨k + 1, ⋯⟩)
    (S.map' k (k + 1) ⋯ ⋯ : S.obj (⟨k, ⋯⟩ : Fin (n + 3 + 1)) ⟶ S.obj ⟨k + 1, ⋯⟩)
kf :
  KernelFork (X := S.obj ⟨k + 2, ⋯⟩) (Y := S.obj ⟨k + 3, ⋯⟩)
    (S.map' (k + 2) (k + 3) ⋯ ⋯ : S.obj (⟨k + 2, ⋯⟩ : Fin (n + 3 + 1)) ⟶ S.obj ⟨k + 3, ⋯⟩)
hcc : IsColimit cc
hkf : IsLimit kf
hS' : (S.sc hS (k + 1) ⋯).Exact
this_1 : HasZeroObject.{u_2, u_1} C
this_2 : (S.sc hS (k + 1) ⋯).HasHomology
h : (S.sc hS (k + 1) ⋯).LeftHomologyData := hS'.leftHomologyDataOfIsLimitKernelFork kf hkf
this : Epi h.f'
rw : (Cofork.π cc ≫ hS.cokerToKer' k hk cc kf hcc hkf) ≫ h.i = h.f' ≫ h.i
rw₁ : (Cofork.π cc ≫ hS.cokerToKer' k hk cc kf hcc hkf) ≫ h.i = (S.sc hS (k + 1) ⋯).f
⊢ Cofork.π cc ≫ hS.cokerToKer' k hk cc kf hcc hkf = h.f'
have rw₂ : (Cofork.π cc ≫ hS.cokerToKer' k hk cc kf hcc hkf) ≫ Fork.ι kf = (S.sc hS (k + 1) sorry).f
Tactic: rw [← cancel_mono h.i, h.f'_i, ShortComplex.Exact.leftHomologyDataOfIsLimitKernelFork_i,
      assoc, IsComplex.cokerToKer'_fac]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ExactSequenceFour (goal)
Goal:
C : Type u_1
inst : Category.{u_2, u_1} C
inst_1 : Preadditive.{u_2, u_1} C
n : ℕ
S : ComposableArrows.{u_2, u_1} C (n + 3)
hS : S.IsComplex
k : ℕ
hk : k ≤ n
cc :
  CokernelCofork (X := S.obj ⟨k, ⋯⟩) (Y := S.obj ⟨k + 1, ⋯⟩)
    (S.map' k (k + 1) ⋯ ⋯ : S.obj (⟨k, ⋯⟩ : Fin (n + 3 + 1)) ⟶ S.obj ⟨k + 1, ⋯⟩)
kf :
  KernelFork (X := S.obj ⟨k + 2, ⋯⟩) (Y := S.obj ⟨k + 3, ⋯⟩)
    (S.map' (k + 2) (k + 3) ⋯ ⋯ : S.obj (⟨k + 2, ⋯⟩ : Fin (n + 3 + 1)) ⟶ S.obj ⟨k + 3, ⋯⟩)
hcc : IsColimit cc
hkf : IsLimit kf
hS' : (S.sc hS (k + 1) ⋯).Exact
this_1 : HasZeroObject.{u_2, u_1} C
this_2 : (S.sc hS (k + 1) ⋯).HasHomology
h : (S.sc hS (k + 1) ⋯).LeftHomologyData := hS'.leftHomologyDataOfIsLimitKernelFork kf hkf
this : Epi h.f'
rw : (Cofork.π cc ≫ hS.cokerToKer' k hk cc kf hcc hkf) ≫ h.i = h.f' ≫ h.i
rw₁ : (Cofork.π cc ≫ hS.cokerToKer' k hk cc kf hcc hkf) ≫ h.i = (S.sc hS (k + 1) ⋯).f
rw₂ : (Cofork.π cc ≫ hS.cokerToKer' k hk cc kf hcc hkf) ≫ Fork.ι kf = (S.sc hS (k + 1) ⋯).f
⊢ Cofork.π cc ≫ hS.cokerToKer' k hk cc kf hcc hkf = h.f'
have rw₃ : Cofork.π cc ≫ hS.cokerToKer' k hk cc kf hcc hkf ≫ Fork.ι kf = (S.sc hS (k + 1) sorry).f
Tactic: rw [← cancel_mono h.i, h.f'_i, ShortComplex.Exact.leftHomologyDataOfIsLimitKernelFork_i,
      assoc, IsComplex.cokerToKer'_fac]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ExactSequenceFour (goal)
Goal:
C : Type u_1
inst : Category.{u_2, u_1} C
inst_1 : Preadditive.{u_2, u_1} C
n : ℕ
S : ComposableArrows.{u_2, u_1} C (n + 3)
hS : S.IsComplex
k : ℕ
hk : k ≤ n
cc :
  CokernelCofork (X := S.obj ⟨k, ⋯⟩) (Y := S.obj ⟨k + 1, ⋯⟩)
    (S.map' k (k + 1) ⋯ ⋯ : S.obj (⟨k, ⋯⟩ : Fin (n + 3 + 1)) ⟶ S.obj ⟨k + 1, ⋯⟩)
kf :
  KernelFork (X := S.obj ⟨k + 2, ⋯⟩) (Y := S.obj ⟨k + 3, ⋯⟩)
    (S.map' (k + 2) (k + 3) ⋯ ⋯ : S.obj (⟨k + 2, ⋯⟩ : Fin (n + 3 + 1)) ⟶ S.obj ⟨k + 3, ⋯⟩)
hcc : IsColimit cc
hkf : IsLimit kf
hS' : (S.sc hS (k + 1) ⋯).Exact
this_1 : HasZeroObject.{u_2, u_1} C
this_2 : (S.sc hS (k + 1) ⋯).HasHomology
h : (S.sc hS (k + 1) ⋯).LeftHomologyData := hS'.leftHomologyDataOfIsLimitKernelFork kf hkf
this : Epi h.f'
rw : (Cofork.π cc ≫ hS.cokerToKer' k hk cc kf hcc hkf) ≫ h.i = h.f' ≫ h.i
rw₁ : (Cofork.π cc ≫ hS.cokerToKer' k hk cc kf hcc hkf) ≫ h.i = (S.sc hS (k + 1) ⋯).f
rw₂ : (Cofork.π cc ≫ hS.cokerToKer' k hk cc kf hcc hkf) ≫ Fork.ι kf = (S.sc hS (k + 1) ⋯).f
rw₃ : Cofork.π cc ≫ hS.cokerToKer' k hk cc kf hcc hkf ≫ Fork.ι kf = (S.sc hS (k + 1) ⋯).f
⊢ Cofork.π cc ≫ hS.cokerToKer' k hk cc kf hcc hkf = h.f'
have rw₄ : S.map' (k + 1) (k + 2) sorry sorry = (S.sc hS (k + 1) sorry).f
Tactic: rw [← cancel_mono h.i, h.f'_i, ShortComplex.Exact.leftHomologyDataOfIsLimitKernelFork_i,
      assoc, IsComplex.cokerToKer'_fac]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ExactSequenceFour (hypothesis)
Goal:
C : Type u_1
inst : Category.{u_2, u_1} C
inst_1 : Preadditive.{u_2, u_1} C
n : ℕ
S : ComposableArrows.{u_2, u_1} C (n + 3)
hS : S.IsComplex
k : ℕ
hk : k ≤ n
cc :
  CokernelCofork (X := S.obj ⟨k, ⋯⟩) (Y := S.obj ⟨k + 1, ⋯⟩)
    (S.map' k (k + 1) ⋯ ⋯ : S.obj (⟨k, ⋯⟩ : Fin (n + 3 + 1)) ⟶ S.obj ⟨k + 1, ⋯⟩)
kf :
  KernelFork (X := S.obj ⟨k + 2, ⋯⟩) (Y := S.obj ⟨k + 3, ⋯⟩)
    (S.map' (k + 2) (k + 3) ⋯ ⋯ : S.obj (⟨k + 2, ⋯⟩ : Fin (n + 3 + 1)) ⟶ S.obj ⟨k + 3, ⋯⟩)
hcc : IsColimit cc
hkf : IsLimit kf
hS' : (S.sc hS (k + 1) ⋯).Exact
this_1 : HasZeroObject.{u_2, u_1} C
this_2 : (S.sc hS (k + 1) ⋯).HasHomology
h : (S.sc hS (k + 1) ⋯).LeftHomologyData := hS'.leftHomologyDataOfIsLimitKernelFork kf hkf
this : Epi h.f'
⊢ Epi (hS.cokerToKer' k hk cc kf hcc hkf)
have fac : Cofork.π cc ≫ hS.cokerToKer' k hk cc kf hcc hkf = h.f'
Tactic: have fac : cc.π ≫ hS.cokerToKer' k hk cc kf hcc hkf = h.f' := by
    rw [← cancel_mono h.i, h.f'_i, ShortComplex.Exact.leftHomologyDataOfIsLimitKernelFork_i,
      assoc, IsComplex.cokerToKer'_fac]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ExactSequenceFour (hypothesis)
Goal:
C : Type u_1
inst : Category.{u_2, u_1} C
inst_1 : Preadditive.{u_2, u_1} C
n : ℕ
S : ComposableArrows.{u_2, u_1} C (n + 3)
hS : S.IsComplex
k : ℕ
hk : k ≤ n
cc :
  CokernelCofork (X := S.obj ⟨k, ⋯⟩) (Y := S.obj ⟨k + 1, ⋯⟩)
    (S.map' k (k + 1) ⋯ ⋯ : S.obj (⟨k, ⋯⟩ : Fin (n + 3 + 1)) ⟶ S.obj ⟨k + 1, ⋯⟩)
kf :
  KernelFork (X := S.obj ⟨k + 2, ⋯⟩) (Y := S.obj ⟨k + 3, ⋯⟩)
    (S.map' (k + 2) (k + 3) ⋯ ⋯ : S.obj (⟨k + 2, ⋯⟩ : Fin (n + 3 + 1)) ⟶ S.obj ⟨k + 3, ⋯⟩)
hcc : IsColimit cc
hkf : IsLimit kf
hS' : (S.sc hS k ⋯).Exact
⊢ Mono (hS.cokerToKer' k hk cc kf hcc hkf)
have this : HasZeroObject.{u_2, u_1} C
Tactic: have := hS'.hasZeroObject