awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.Embedding.TruncLEHomology
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 : ι
j' : ι'
hj' : c'.Rel (e.f i) j'
pos :
  { X₁ := (K.shortComplexTruncLE e).X₂.homology (e.f i), X₂ := (K.shortComplexTruncLE e).X₃.homology (e.f i),
        X₃ := (K.shortComplexTruncLE e).X₁.homology j', f := homologyMap (K.shortComplexTruncLE e).g (e.f i),
        g := ShortComplex.ShortExact.δ ⋯ (e.f i) j' hj', zero := ⋯ : ShortComplex.{v_1, u_3} C }.f =
    0
pos₁ :
  { X₁ := (K.shortComplexTruncLE e).X₂.homology (e.f i), X₂ := (K.shortComplexTruncLE e).X₃.homology (e.f i),
        X₃ := (K.shortComplexTruncLE e).X₁.homology j', f := homologyMap (K.shortComplexTruncLE e).g (e.f i),
        g := ShortComplex.ShortExact.δ ⋯ (e.f i) j' hj', zero := ⋯ : ShortComplex.{v_1, u_3} C }.g =
    0
⊢ IsZero.{v_1, u_3} ((K.shortComplexTruncLE e).X₃.homology (e.f i))

Tactic:
apply ((K.shortComplexTruncLE_shortExact e).homology_exact₃ (e.f i) j' hj').isZero_X₂

Premises used: CategoryTheory.ShortComplex.ShortExact.homology_exact₃, HomologicalComplex.shortComplexTruncLE_shortExact, ComplexShape.Embedding.f, CategoryTheory.ShortComplex.Exact.isZero_X₂
-- Module: Mathlib.Algebra.Homology.Embedding.TruncLEHomology
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 : ι
j' : ι'
hj' : c'.Rel (e.f i) j'
pos :
  Eq (α :=
    (K.truncLE e).homology (e.f i) ⟶
      { X₁ := (K.shortComplexTruncLE e).X₂.homology (e.f i), X₂ := (K.shortComplexTruncLE e).X₃.homology (e.f i),
          X₃ := (K.shortComplexTruncLE e).X₁.homology j', f := homologyMap (K.shortComplexTruncLE e).g (e.f i),
          g := ShortComplex.ShortExact.δ ⋯ (e.f i) j' hj', zero := ⋯ : ShortComplex.{v_1, u_3} C }.X₂)
    (homologyMap (K.ιTruncLE e) (e.f i) ≫
      { X₁ := (K.shortComplexTruncLE e).X₂.homology (e.f i), X₂ := (K.shortComplexTruncLE e).X₃.homology (e.f i),
          X₃ := (K.shortComplexTruncLE e).X₁.homology j', f := homologyMap (K.shortComplexTruncLE e).g (e.f i),
          g := ShortComplex.ShortExact.δ ⋯ (e.f i) j' hj', zero := ⋯ : ShortComplex.{v_1, u_3} C }.f)
    0
⊢ { X₁ := (K.shortComplexTruncLE e).X₂.homology (e.f i), X₂ := (K.shortComplexTruncLE e).X₃.homology (e.f i),
        X₃ := (K.shortComplexTruncLE e).X₁.homology j', f := homologyMap (K.shortComplexTruncLE e).g (e.f i),
        g := ShortComplex.ShortExact.δ ⋯ (e.f i) j' hj', zero := ⋯ : ShortComplex.{v_1, u_3} C }.f =
    0

Tactic:
rw [← cancel_epi (homologyMap (K.ιTruncLE e) (e.f i)), comp_zero]

Premises used: HomologicalComplex.ιTruncLE, CategoryTheory.Limits.comp_zero, ComplexShape.Embedding.f, HomologicalComplex.homologyMap, CategoryTheory.cancel_epi
-- Module: Mathlib.Algebra.Homology.Embedding.TruncLEHomology
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 : ι
j' : ι'
hj' : c'.Rel (e.f i) j'
pos :
  Eq (α := (K.truncLE e).homology (e.f i) ⟶ (cokernel (X := K.truncLE e) (K.ιTruncLE e)).homology (e.f i))
    (CategoryStruct.comp (Y := K.homology (e.f i)) (homologyMap (K.ιTruncLE e) (e.f i))
      (homologyMap (cokernel.π (K.ιTruncLE e)) (e.f i)))
    0
⊢ Eq (α :=
    (K.truncLE e).homology (e.f i) ⟶
      { X₁ := (K.shortComplexTruncLE e).X₂.homology (e.f i), X₂ := (K.shortComplexTruncLE e).X₃.homology (e.f i),
          X₃ := (K.shortComplexTruncLE e).X₁.homology j', f := homologyMap (K.shortComplexTruncLE e).g (e.f i),
          g := ShortComplex.ShortExact.δ ⋯ (e.f i) j' hj', zero := ⋯ : ShortComplex.{v_1, u_3} C }.X₂)
    (homologyMap (K.ιTruncLE e) (e.f i) ≫
      { X₁ := (K.shortComplexTruncLE e).X₂.homology (e.f i), X₂ := (K.shortComplexTruncLE e).X₃.homology (e.f i),
          X₃ := (K.shortComplexTruncLE e).X₁.homology j', f := homologyMap (K.shortComplexTruncLE e).g (e.f i),
          g := ShortComplex.ShortExact.δ ⋯ (e.f i) j' hj', zero := ⋯ : ShortComplex.{v_1, u_3} C }.f)
    0

Tactic:
dsimp [shortComplexTruncLE]

Premises used: HomologicalComplex.shortComplexTruncLE
-- Module: Mathlib.Algebra.Homology.Embedding.TruncLEHomology
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 : ι
j' : ι'
hj' : c'.Rel (e.f i) j'
pos :
  Eq (α := (K.truncLE e).homology (e.f i) ⟶ (cokernel (X := K.truncLE e) (K.ιTruncLE e)).homology (e.f i))
    (homologyMap (K.ιTruncLE e ≫ cokernel.π (K.ιTruncLE e)) (e.f i)) 0
pos₁ :
  Eq.{v_1 + 1} (α := (K.truncLE e).homology (e.f i) ⟶ (cokernel (X := K.truncLE e) (K.ιTruncLE e)).homology (e.f i))
    (homologyMap 0 (e.f i)) 0
pos₂ pos₃ :
  Eq.{v_1 + 1} (α := (K.truncLE e).homology (e.f i) ⟶ (cokernel (X := K.truncLE e) (K.ιTruncLE e)).homology (e.f i)) 0 0
⊢ Eq (α := (K.truncLE e).homology (e.f i) ⟶ (cokernel (X := K.truncLE e) (K.ιTruncLE e)).homology (e.f i))
    (CategoryStruct.comp (Y := K.homology (e.f i)) (homologyMap (K.ιTruncLE e) (e.f i))
      (homologyMap (cokernel.π (K.ιTruncLE e)) (e.f i)))
    0

Tactic:
rw [← homologyMap_comp, cokernel.condition, homologyMap_zero]

Premises used: CategoryTheory.Limits.cokernel.condition, HomologicalComplex.homologyMap_comp, HomologicalComplex.homologyMap_zero
-- Module: Mathlib.Algebra.Homology.Embedding.TruncLEHomology
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 : ι
j' : ι'
hj' : c'.Rel (e.f i) j'
⊢ { X₁ := (K.shortComplexTruncLE e).X₂.homology (e.f i), X₂ := (K.shortComplexTruncLE e).X₃.homology (e.f i),
        X₃ := (K.shortComplexTruncLE e).X₁.homology j', f := homologyMap (K.shortComplexTruncLE e).g (e.f i),
        g := ShortComplex.ShortExact.δ ⋯ (e.f i) j' hj', zero := ⋯ : ShortComplex.{v_1, u_3} C }.g =
    0

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.Embedding.TruncLEHomology
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'
dsimp : IsIso (X := (K.truncLE e).homology (e.f i)) (Y := K.homology (e.f i)) (homologyMap (K.ιTruncLE e) (e.f i))
⊢ 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))

Tactic:
dsimp
-- Module: Mathlib.Algebra.Homology.Embedding.TruncLEHomology
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'
⊢ IsIso (X := (K.truncLE e).homology (e.f i)) (Y := K.homology (e.f i)) (homologyMap (K.ιTruncLE e) (e.f i))

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Homology.Embedding.TruncLEHomology
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'
⊢ 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))

Tactic:
have : IsIso (homologyMap (K.shortComplexTruncLE e).f (e.f i)) := by dsimp; infer_instance
-- Module: Mathlib.Algebra.Homology.EulerCharacteristic
Goal:
ι : Type u_1
c : ComplexShape ι
inst : c.EulerCharSigns
i j : ι
h : c.Rel i j
⊢ c.χ j = -c.χ i

Tactic:
EulerCharSigns.χ_next h

Premises used: ComplexShape.EulerCharSigns.χ_next
-- Module: Mathlib.Algebra.Homology.EulerCharacteristic
Goal:
ι : Type u_1
c : ComplexShape ι
inst : c.EulerCharSigns
i j : ι
h : c.Rel i j
⊢ c.χ i = -c.χ j

Tactic:
simp [c.χ_next h]

Premises used: ComplexShape.χ_next
-- Module: Mathlib.Algebra.Homology.EulerCharacteristic
Goal:
ι : Type u_1
c : ComplexShape ι
inst : c.EulerCharSigns
i : ℤ
rw rw₁ : -i.negOnePow = -i.negOnePow
⊢ (i + 1).negOnePow = -i.negOnePow

Tactic:
rw [Int.negOnePow_succ]

Premises used: Int.negOnePow_succ
-- Module: Mathlib.Algebra.Homology.EulerCharacteristic
Goal:
ι : Type u_1
c : ComplexShape ι
inst : c.EulerCharSigns
j : ℤ
⊢ j.negOnePow = -(j + 1).negOnePow

Tactic:
simp [Int.negOnePow_succ]

Premises used: Int.negOnePow_succ
-- Module: Mathlib.Algebra.Homology.EulerCharacteristic
Goal:
ι : Type u_1
c : ComplexShape ι
inst : c.EulerCharSigns
i : ℕ
⊢ HPow.hPow (α := ℤˣ) (-1) (i + 1) = -HPow.hPow (α := ℤˣ) (-1) i

Tactic:
simp [pow_add]

Premises used: pow_add
-- Module: Mathlib.Algebra.Homology.EulerCharacteristic
Goal:
ι : Type u_1
c : ComplexShape ι
inst : c.EulerCharSigns
j : ℕ
⊢ HPow.hPow (α := ℤˣ) (-1) j = -HPow.hPow (α := ℤˣ) (-1) (j + 1)

Tactic:
simp [pow_add]

Premises used: pow_add
-- Module: Mathlib.Algebra.Homology.EulerCharacteristic
Goal:
R : Type u_1
inst : Ring R
ι : Type u_2
X : GradedObject ι (ModuleCat.{u_3, u_1} R)
s : Set ι
⊢ finrankSupport X ⊆ s ↔ ∀ i ∉ s, Module.finrank.{u_1, u_3} R (↑(X i) : Type u_3) = 0

Tactic:
Function.support_subset_iff'

Premises used: GradedObject.finrankSupport, Function.support_subset_iff'
-- Module: Mathlib.Algebra.Homology.EulerCharacteristic
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)
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))
⊢ (Function.support (M := ℤ) fun (i : ι) ↦ (↑(c.χ i) : ℤ) * (↑(Module.finrank.{u_1, u_3} R (↑(X i) : Type u_3)) : ℤ)) =
    finrankSupport X

Tactic:
simp only [finrankSupport, Function.support_mul_of_ne_zero_left (fun i => Units.ne_zero (c.χ i))]

Premises used: GradedObject.finrankSupport, Units.ne_zero, Function.support_mul_of_ne_zero_left, ComplexShape.χ
-- Module: Mathlib.Algebra.Homology.EulerCharacteristic
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)
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
⊢ 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:
ext i
-- Module: Mathlib.Algebra.Homology.EulerCharacteristic
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)
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:
simp [Function.mem_support]

Premises used: Function.mem_support
-- Module: Mathlib.Algebra.Homology.EulerCharacteristic
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 ι)
h :
  (Function.support (M := ℤ) fun (i : ι) ↦ (↑(c.χ i) : ℤ) * (↑(Module.finrank.{u_1, u_3} R (↑(X i) : Type u_3)) : ℤ)) ⊆
    (↑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)) : ℤ))

Tactic:
rw [finsum_eq_sum_of_support_subset]

Premises used: finsum_eq_sum_of_support_subset
-- Module: Mathlib.Algebra.Homology.EulerCharacteristic
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 ι)
⊢ (Function.support (M := ℤ) fun (i : ι) ↦ (↑(c.χ i) : ℤ) * (↑(Module.finrank.{u_1, u_3} R (↑(X i) : Type u_3)) : ℤ)) ⊆
    (↑indices : Set ι)

Tactic:
(support_eulerChar_summand c X).symm ▸ h_support

Premises used: Eq.rec, _private.0.GradedObject.support_eulerChar_summand, Eq.symm
-- Module: Mathlib.Algebra.Homology.EulerCharacteristic
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 ι)
⊢ (Function.support (M := ℤ) fun (i : ι) ↦ (↑(c.χ i) : ℤ) * (↑(Module.finrank.{u_1, u_3} R (↑(X i) : Type u_3)) : ℤ)) ⊆
    (↑indices : Set ι)

Tactic:
exact (support_eulerChar_summand c X).symm ▸ h_support
-- Module: Mathlib.Algebra.Homology.EulerCharacteristic
Goal:
R : Type u_1
inst : Ring R
ι : Type u_2
c : ComplexShape ι
inst_1 : c.EulerCharSigns
C : HomologicalComplex (ModuleCat.{u_3, u_1} R) c
indices : Finset ι
h_support : GradedObject.finrankSupport C.X ⊆ (↑indices : Set ι)
⊢ C.eulerChar = ∑ i ∈ indices, (↑(c.χ i) : ℤ) * (↑(Module.finrank.{u_1, u_3} R (↑(C.X i) : Type u_3)) : ℤ)

Tactic:
GradedObject.eulerChar_eq_sum_finSet_of_finrankSupport_subset c C.X indices h_support

Premises used: HomologicalComplex.X, GradedObject.eulerChar_eq_sum_finSet_of_finrankSupport_subset
-- Module: Mathlib.Algebra.Homology.EulerCharacteristic
Goal:
R : Type u_1
inst : Ring R
ι : Type u_2
c : ComplexShape ι
inst_1 : c.EulerCharSigns
C : HomologicalComplex (ModuleCat.{u_3, u_1} R) c
inst_2 : ∀ (i : ι), C.HasHomology i
indices : Finset ι
h_support : (GradedObject.finrankSupport.{u_1, u_2, u_3} (R := R) fun (i : ι) ↦ C.homology i) ⊆ (↑indices : Set ι)
⊢ C.homologyEulerChar =
    ∑ i ∈ indices, (↑(c.χ i) : ℤ) * (↑(Module.finrank.{u_1, u_3} R (↑(C.homology i) : Type u_3)) : ℤ)

Tactic:
GradedObject.eulerChar_eq_sum_finSet_of_finrankSupport_subset c
    (fun i => C.homology i) indices h_support

Premises used: GradedObject.eulerChar_eq_sum_finSet_of_finrankSupport_subset, HomologicalComplex.homology
-- Module: Mathlib.Algebra.Homology.ExactSequenceFour
Goal:
C : Type u_1
inst : Category.{u_2, u_1} C
inst_1 : HasZeroMorphisms.{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
⊢ Eq (α := S.obj (⟨k, ⋯⟩ : Fin (n + 3 + 1)) ⟶ S.obj ⟨k + 2, ⋯⟩)
    (CategoryStruct.comp (Y := S.obj ⟨k + 1, ⋯⟩)
          (S.map' k (k + 1) ⋯ ⋯ : S.obj (⟨k, ⋯⟩ : Fin (n + 3 + 1)) ⟶ S.obj ⟨k + 1, ⋯⟩)
          (hkf.lift (KernelFork.ofι (S.map' (k + 1) (k + 1 + 1) ⋯ ⋯) ⋯) :
            (KernelFork.ofι (S.map' (k + 1) (k + 1 + 1) ⋯ ⋯) ⋯).pt ⟶ kf.pt) ≫
        Fork.ι kf :
      S.obj (⟨k, ⋯⟩ : Fin (n + 3 + 1)) ⟶ S.obj ⟨k + 2, ⋯⟩)
    (0 ≫ Fork.ι kf : S.obj (⟨k, ⋯⟩ : Fin (n + 3 + 1)) ⟶ S.obj ⟨k + 2, ⋯⟩)

Tactic:
simpa using hS.zero k

Premises used: CategoryTheory.ComposableArrows.IsComplex.zero
-- Module: Mathlib.Algebra.Homology.ExactSequenceFour
Goal:
C : Type u_1
inst : Category.{u_2, u_1} C
inst_1 : HasZeroMorphisms.{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
⊢ Cofork.π cc ≫ hS.cokerToKer' k hk cc kf hcc hkf ≫ Fork.ι kf = S.map' (k + 1) (k + 2) ⋯ ⋯

Tactic:
simp [cokerToKer']

Premises used: CategoryTheory.ComposableArrows.IsComplex.cokerToKer'
-- Module: Mathlib.Algebra.Homology.ExactSequenceFour
Goal:
C : Type u_1
inst : Category.{u_2, u_1} C
inst_1 : HasZeroMorphisms.{u_2, u_1} C
n : ℕ
S : ComposableArrows.{u_2, u_1} C (n + 3)
hS : S.IsComplex
k : ℕ
hk : k ≤ n
inst_2 :
  HasCokernel (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, ⋯⟩)
inst_3 :
  HasKernel (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, ⋯⟩)
⊢ Eq (α := S.obj (⟨k + 1, ⋯⟩ : Fin (n + 3 + 1)) ⟶ S.obj ⟨k + 2, ⋯⟩)
    (CategoryStruct.comp (Y :=
        cokernel (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, ⋯⟩))
        (cokernel.π (S.map' k (k + 1) ⋯ ⋯) :
          S.obj (⟨k + 1, ⋯⟩ : Fin (n + 3 + 1)) ⟶
            cokernel (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, ⋯⟩))
        (CategoryStruct.comp (Y :=
            kernel (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, ⋯⟩))
            (hS.cokerToKer k hk) (kernel.ι (S.map' (k + 2) (k + 3) ⋯ ⋯)) :
          cokernel (X := S.obj (⟨k, ⋯⟩ : Fin (n + 3 + 1))) (Y := S.obj (⟨k + 1, ⋯⟩ : Fin (n + 3 + 1)))
              (S.map' k (k + 1) ⋯ ⋯ : S.obj (⟨k, ⋯⟩ : Fin (n + 3 + 1)) ⟶ S.obj (⟨k + 1, ⋯⟩ : Fin (n + 3 + 1))) ⟶
            S.obj ⟨k + 2, ⋯⟩) :
      S.obj (⟨k + 1, ⋯⟩ : Fin (n + 3 + 1)) ⟶ S.obj ⟨k + 2, ⋯⟩)
    (S.map' (k + 1) (k + 2) ⋯ ⋯ : S.obj (⟨k + 1, ⋯⟩ : Fin (n + 3 + 1)) ⟶ S.obj ⟨k + 2, ⋯⟩)

Tactic:
hS.cokerToKer'_fac k hk _ _ (cokernelIsCokernel _) (kernelIsKernel _)

Premises used: CategoryTheory.Limits.limit.π, CategoryTheory.Limits.colimit, CategoryTheory.Limits.limit, CategoryTheory.Limits.cokernelIsCokernel, CategoryTheory.ComposableArrows.IsComplex.cokerToKer, CategoryTheory.Limits.kernelIsKernel, CategoryTheory.ComposableArrows.IsComplex.cokerToKer'_fac, CategoryTheory.Limits.colimit.ι
-- Module: Mathlib.Algebra.Homology.ExactSequenceFour
Goal:
C : Type u_1
inst : Category.{u_2, u_1} C
inst_1 : HasZeroMorphisms.{u_2, u_1} C
n : ℕ
S : ComposableArrows.{u_2, u_1} C (n + 3)
hS : S.IsComplex
k : ℕ
hk : k ≤ n
inst_2 : (S.sc hS k ⋯).HasRightHomology
inst_3 : (S.sc hS (k + 1) ⋯).HasLeftHomology
⊢ CategoryStruct.comp (Y := (S.sc hS k ⋯).opcycles) (S.sc hS k ⋯).pOpcycles
      (CategoryStruct.comp (Y := (S.sc hS (k + 1) ⋯).cycles)
        (hS.opcyclesToCycles k ⋯ : (S.sc hS k ⋯).opcycles ⟶ (S.sc hS (k + 1) ⋯).cycles)
        ((S.sc hS (k + 1) ⋯).iCycles : (S.sc hS (k + 1) ⋯).cycles ⟶ (S.sc hS (k + 1) ⋯).X₂)) =
    S.map' (k + 1) (k + 2) ⋯ ⋯

Tactic:
hS.cokerToKer'_fac k hk _ _ (S.sc hS k _).opcyclesIsCokernel
    (S.sc hS (k + 1) _).cyclesIsKernel

Premises used: CategoryTheory.ShortComplex.opcycles, CategoryTheory.ShortComplex.cyclesIsKernel, CategoryTheory.ShortComplex.pOpcycles, CategoryTheory.ComposableArrows.sc, HAdd.hAdd, CategoryTheory.Limits.Fork.ι, CategoryTheory.ComposableArrows.IsComplex.opcyclesToCycles, CategoryTheory.ShortComplex.iCycles, OfNat.ofNat, CategoryTheory.ShortComplex.cycles, CategoryTheory.ComposableArrows.IsComplex.cokerToKer'_fac, CategoryTheory.ShortComplex.opcyclesIsCokernel, CategoryTheory.Limits.Cofork.π
-- Module: Mathlib.Algebra.Homology.ExactSequenceFour
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
⊢ HasZeroObject.{u_2, u_1} C

Tactic:
have := hS'.hasZeroObject
-- Module: Mathlib.Algebra.Homology.ExactSequenceFour
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
⊢ (S.sc hS (k + 1) ⋯).HasHomology

Tactic:
have := hS'.hasHomology
-- Module: Mathlib.Algebra.Homology.ExactSequenceFour
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 h.f'

Tactic:
have := h.exact_iff_epi_f'.1 hS'
-- Module: Mathlib.Algebra.Homology.ExactSequenceFour
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
rw₄ rw₅ : S.map' (k + 1) (k + 2) ⋯ ⋯ = (S.sc hS (k + 1) ⋯).f
⊢ Cofork.π cc ≫ hS.cokerToKer' k hk cc kf hcc hkf = h.f'

Tactic:
rw [← cancel_mono h.i, h.f'_i, ShortComplex.Exact.leftHomologyDataOfIsLimitKernelFork_i,
      assoc, IsComplex.cokerToKer'_fac]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.ShortComplex.LeftHomologyData.f'_i, CategoryTheory.cancel_mono, CategoryTheory.ShortComplex.Exact.leftHomologyDataOfIsLimitKernelFork_i, CategoryTheory.ComposableArrows.IsComplex.cokerToKer'_fac, CategoryTheory.ShortComplex.LeftHomologyData.i