awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
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 : ι
inst_2 : K.HasHomology i
hij : c.Rel i (c.next i)
⊢ Eq (α := K.cycles i ⟶ K.X (c.next i)) (K.iCycles i ≫ K.d i (c.next i)) 0

Tactic:
(K.sc i).iCycles_g

Premises used: CategoryTheory.ShortComplex.iCycles_g, HomologicalComplex.iCycles, HomologicalComplex.sc, HomologicalComplex.cycles
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
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 : ι
inst_2 : K.HasHomology i
hij : c.Rel i (c.next i)
⊢ Eq (α := K.cycles i ⟶ K.X (c.next i)) (K.iCycles i ≫ K.d i (c.next i)) 0

Tactic:
exact (K.sc i).iCycles_g

Premises used: CategoryTheory.ShortComplex.iCycles_g, HomologicalComplex.sc
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
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 : ι
inst_2 : K.HasHomology i
hij : ¬c.Rel i j
neg : Eq (α := K.cycles i ⟶ K.X j) (K.iCycles i ≫ 0) 0
neg₁ neg₂ : Eq.{v_1 + 1} (α := K.cycles i ⟶ K.X j) 0 0
⊢ Eq (α := K.cycles i ⟶ K.X j) (K.iCycles i ≫ K.d i j) 0

Tactic:
rw [K.shape _ _ hij, comp_zero]

Premises used: CategoryTheory.Limits.comp_zero, HomologicalComplex.shape
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
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 L M : HomologicalComplex.{v_1, u_1, u_2} C c
φ : K ⟶ L
iso : K ≅ L
ψ : L ⟶ M
i j k : ι
inst_2 : K.HasHomology i
hj : c.next i = j
obtain :
  IsLimit (F := parallelPair (Y := K.X (c.next i)) (K.d i (c.next i)) 0)
    (KernelFork.ofι (Z := K.cycles i) (K.iCycles i) ⋯)
⊢ IsLimit (KernelFork.ofι (Z := K.cycles i) (K.iCycles i) ⋯)

Tactic:
obtain rfl := hj

Premises used: rfl
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
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 L M : HomologicalComplex.{v_1, u_1, u_2} C c
φ : K ⟶ L
iso : K ≅ L
ψ : L ⟶ M
i k : ι
inst_2 : K.HasHomology i
⊢ IsLimit (F := parallelPair (Y := K.X (c.next i)) (K.d i (c.next i)) 0)
    (KernelFork.ofι (Z := K.cycles i) (K.iCycles i) ⋯)

Tactic:
exact (K.sc i).cyclesIsKernel

Premises used: CategoryTheory.ShortComplex.cyclesIsKernel, HomologicalComplex.sc
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
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 : ι
inst_2 : K.HasHomology j
⊢ CategoryStruct.comp (Y := K.cycles j) (K.toCycles i j) (K.iCycles j) = K.d i j

Tactic:
liftCycles_i _ _ _ _ _

Premises used: HomologicalComplex.liftCycles_i, HomologicalComplex.toCycles
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
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 L M : HomologicalComplex.{v_1, u_1, u_2} C c
φ : K ⟶ L
iso : K ≅ L
ψ : L ⟶ M
i j k : ι
inst_2 : K.HasHomology i
⊢ Mono (X := K.cycles i) (K.sc i).iCycles

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
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 L M : HomologicalComplex.{v_1, u_1, u_2} C c
φ : K ⟶ L
iso : K ≅ L
ψ : L ⟶ M
i j k : ι
inst_2 : K.HasHomology i
⊢ Epi (X := K.cycles i) (Y := K.homology i) (K.sc i).homologyπ

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
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 : ι
inst_2 : K.HasHomology k
⊢ Eq (α := K.X i ⟶ K.cycles k) (K.d i j ≫ K.toCycles j k) 0

Tactic:
simp only [← cancel_mono (K.iCycles k), assoc, toCycles_i, d_comp_d, zero_comp]

Premises used: CategoryTheory.Category.assoc, HomologicalComplex.toCycles_i, HomologicalComplex.iCycles, CategoryTheory.cancel_mono, HomologicalComplex.d_comp_d, CategoryTheory.Limits.zero_comp
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
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 : ι
inst_2 : K.HasHomology j
hij : ¬c.Rel i j
rw :
  CategoryStruct.comp (Y := K.cycles j) (K.toCycles i j) (K.iCycles j) =
    CategoryStruct.comp (Y := K.cycles j) 0 (K.iCycles j)
rw₁ : K.d i j = CategoryStruct.comp (Y := K.cycles j) 0 (K.iCycles j)
rw₂ : K.d i j = 0
rw₃ rw₄ : Eq.{v_1 + 1} (α := K.X i ⟶ K.X j) 0 0
⊢ Eq (α := K.X i ⟶ K.cycles j) (K.toCycles i j) 0

Tactic:
rw [← cancel_mono (K.iCycles j), toCycles_i, zero_comp, K.shape _ _ hij]

Premises used: HomologicalComplex.toCycles_i, HomologicalComplex.iCycles, CategoryTheory.cancel_mono, CategoryTheory.Limits.zero_comp, HomologicalComplex.shape
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
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 L M : HomologicalComplex.{v_1, u_1, u_2} C c
φ : K ⟶ L
iso : K ≅ L
ψ : L ⟶ M
i j_1 k_1 : ι
inst_2 : K.HasHomology i
A' A : C
k : A ⟶ K.X i
j : ι
hj : c.next i = j
hk : k ≫ K.d i j = 0
α : A' ⟶ A
rw : α ≫ k ≫ K.d i j = 0
rw₁ : Eq (α := A' ⟶ K.X j) (α ≫ 0) 0
rw₂ rw₃ : Eq.{v_1 + 1} (α := A' ⟶ K.X j) 0 0
⊢ (α ≫ k) ≫ K.d i j = 0

Tactic:
rw [assoc, hk, comp_zero]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.comp_zero
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
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 : ι
inst_2 : K.HasHomology i
A' A : C
k : A ⟶ K.X i
j : ι
hj : c.next i = j
hk : k ≫ K.d i j = 0
α : A' ⟶ A
⊢ Eq (α := A' ⟶ K.cycles i) (α ≫ K.liftCycles k j hj hk) (K.liftCycles (α ≫ k) j hj ⋯)

Tactic:
simp only [← cancel_mono (K.iCycles i), assoc, liftCycles_i]

Premises used: CategoryTheory.Category.assoc, HomologicalComplex.iCycles, CategoryTheory.cancel_mono, HomologicalComplex.liftCycles_i
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
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 L M : HomologicalComplex.{v_1, u_1, u_2} C c
φ : K ⟶ L
iso : K ≅ L
ψ : L ⟶ M
i j_1 k_1 : ι
inst_2 : K.HasHomology i
A : C
k : A ⟶ K.X i
j : ι
hj : c.next i = j
i' : ι
x : A ⟶ K.X i'
hx : k = x ≫ K.d i' i
rw : (x ≫ K.d i' i) ≫ K.d i j = 0
rw₁ : x ≫ K.d i' i ≫ K.d i j = 0
rw₂ : Eq (α := A ⟶ K.X j) (x ≫ 0) 0
rw₃ rw₄ : Eq.{v_1 + 1} (α := A ⟶ K.X j) 0 0
⊢ k ≫ K.d i j = 0

Tactic:
rw [hx, assoc, K.d_comp_d, comp_zero]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.comp_zero, HomologicalComplex.d_comp_d
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
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 : ι
inst_2 : K.HasHomology i
A : C
k : A ⟶ K.X i
j : ι
hj : c.next i = j
i' : ι
x : A ⟶ K.X i'
hx : k = x ≫ K.d i' i
pos : ∀ (h : c.Rel i' i), Eq (α := A ⟶ K.homology i) (K.liftCycles k j hj ⋯ ≫ K.homologyπ i) 0
neg : ∀ (h : ¬c.Rel i' i), Eq (α := A ⟶ K.homology i) (K.liftCycles k j hj ⋯ ≫ K.homologyπ i) 0
⊢ Eq (α := A ⟶ K.homology i) (K.liftCycles k j hj ⋯ ≫ K.homologyπ i) 0

Tactic:
by_cases h : c.Rel i' i

Premises used: ComplexShape.Rel
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
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 : ι
inst_2 : K.HasHomology i
A : C
k : A ⟶ K.X i
j : ι
hj : c.next i = j
i' : ι
x : A ⟶ K.X i'
hx : k = x ≫ K.d i' i
h : c.Rel i' i
pos :
  ∀ (x : A ⟶ K.X (c.prev i)) (hx : k = x ≫ K.d (c.prev i) i) (h : c.Rel (c.prev i) i),
    Eq (α := A ⟶ K.homology i) (K.liftCycles k j hj ⋯ ≫ K.homologyπ i) 0
⊢ Eq (α := A ⟶ K.homology i) (K.liftCycles k j hj ⋯ ≫ K.homologyπ i) 0

Tactic:
obtain rfl := c.prev_eq' h

Premises used: ComplexShape.prev_eq', rfl
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
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 : ι
inst_2 : K.HasHomology i
A : C
k : A ⟶ K.X i
j : ι
hj : c.next i = j
x : A ⟶ K.X (c.prev i)
hx : k = x ≫ K.d (c.prev i) i
h : c.Rel (c.prev i) i
⊢ Eq (α := A ⟶ K.homology i) (K.liftCycles k j hj ⋯ ≫ K.homologyπ i) 0

Tactic:
(K.sc i).liftCycles_homologyπ_eq_zero_of_boundary _ x hx

Premises used: HomologicalComplex.homologyπ, HomologicalComplex.sc, HomologicalComplex.liftCycles, CategoryTheory.ShortComplex.liftCycles_homologyπ_eq_zero_of_boundary, HomologicalComplex.homology, HomologicalComplex.cycles
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
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 : ι
inst_2 : K.HasHomology i
A : C
k : A ⟶ K.X i
j : ι
hj : c.next i = j
x : A ⟶ K.X (c.prev i)
hx : k = x ≫ K.d (c.prev i) i
h : c.Rel (c.prev i) i
⊢ Eq (α := A ⟶ K.homology i) (K.liftCycles k j hj ⋯ ≫ K.homologyπ i) 0

Tactic:
exact (K.sc i).liftCycles_homologyπ_eq_zero_of_boundary _ x hx

Premises used: HomologicalComplex.sc, CategoryTheory.ShortComplex.liftCycles_homologyπ_eq_zero_of_boundary
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
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 : ι
inst_2 : K.HasHomology i
A : C
k : A ⟶ K.X i
j : ι
hj : c.next i = j
i' : ι
x : A ⟶ K.X i'
hx : k = x ≫ K.d i' i
h : ¬c.Rel i' i
rw : (x ≫ K.d i' i) ≫ K.d i j = 0
rw₁ : x ≫ K.d i' i ≫ K.d i j = 0
rw₂ : Eq (α := A ⟶ K.X j) (x ≫ 0) 0
rw₃ rw₄ : Eq.{v_1 + 1} (α := A ⟶ K.X j) 0 0
⊢ k ≫ K.d i j = 0

Tactic:
rw [hx, assoc, K.d_comp_d, comp_zero]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.comp_zero, HomologicalComplex.d_comp_d
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
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 : ι
inst_2 : K.HasHomology i
A : C
k : A ⟶ K.X i
j : ι
hj : c.next i = j
i' : ι
x : A ⟶ K.X i'
hx : k = x ≫ K.d i' i
h : ¬c.Rel i' i
⊢ k = 0

Tactic:
rw [K.shape _ _ h, comp_zero] at hx

Premises used: CategoryTheory.Limits.comp_zero, HomologicalComplex.shape
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
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 : ι
inst_2 : K.HasHomology i
A : C
k : A ⟶ K.X i
j : ι
hj : c.next i = j
i' : ι
x : A ⟶ K.X i'
hx : k = x ≫ K.d i' i
h : ¬c.Rel i' i
hx₁ : k = 0
⊢ ¬c.Rel i' i

Tactic:
rw [K.shape _ _ h, comp_zero] at hx

Premises used: CategoryTheory.Limits.comp_zero, HomologicalComplex.shape
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
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 : ι
inst_2 : K.HasHomology i
A : C
k : A ⟶ K.X i
j : ι
hj : c.next i = j
i' : ι
x : A ⟶ K.X i'
hx_1 : k = x ≫ K.d i' i
hx : k = 0
h : ¬c.Rel i' i
rw :
  CategoryStruct.comp (Y := K.cycles i) (K.liftCycles k j hj ⋯) (K.iCycles i) =
    CategoryStruct.comp (Y := K.cycles i) 0 (K.iCycles i)
rw₁ : CategoryStruct.comp (Y := K.cycles i) (K.liftCycles k j hj ⋯) (K.iCycles i) = 0
rw₂ : k = 0
rw₃ rw₄ : Eq.{v_1 + 1} (α := A ⟶ K.X i) 0 0
⊢ Eq (α := A ⟶ K.cycles i) (K.liftCycles k j hj ⋯) 0

Tactic:
rw [← cancel_mono (K.iCycles i), zero_comp, liftCycles_i, hx]

Premises used: HomologicalComplex.iCycles, CategoryTheory.cancel_mono, HomologicalComplex.liftCycles_i, CategoryTheory.Limits.zero_comp
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
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 : ι
inst_2 : K.HasHomology i
A : C
k : A ⟶ K.X i
j : ι
hj : c.next i = j
i' : ι
x : A ⟶ K.X i'
hx : k = x ≫ K.d i' i
h : ¬c.Rel i' i
⊢ Eq (α := A ⟶ K.cycles i) (K.liftCycles k j hj ⋯) 0

Tactic:
have : liftCycles K k j hj (by rw [hx, assoc, K.d_comp_d, comp_zero]) = 0 := by
      rw [K.shape _ _ h, comp_zero] at hx
      rw [← cancel_mono (K.iCycles i), zero_comp, liftCycles_i, hx]
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
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 : ι
inst_2 : K.HasHomology i
A : C
k : A ⟶ K.X i
j : ι
hj : c.next i = j
i' : ι
x : A ⟶ K.X i'
hx : k = x ≫ K.d i' i
h : ¬c.Rel i' i
this : Eq (α := A ⟶ K.cycles i) (K.liftCycles k j hj ⋯) 0
neg : Eq (α := A ⟶ K.homology i) (0 ≫ K.homologyπ i) 0
neg₁ neg₂ : Eq.{v_1 + 1} (α := A ⟶ K.homology i) 0 0
⊢ Eq (α := A ⟶ K.homology i) (K.liftCycles k j hj ⋯ ≫ K.homologyπ i) 0

Tactic:
rw [this, zero_comp]

Premises used: CategoryTheory.Limits.zero_comp
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
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 : ι
inst_2 : K.HasHomology j
⊢ K.d i j = 𝟙 (K.X i) ≫ K.d i j

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
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 L M : HomologicalComplex.{v_1, u_1, u_2} C c
φ : K ⟶ L
iso : K ≅ L
ψ : L ⟶ M
i j k : ι
hi : c.prev j = i
inst_2 : K.HasHomology j
subst :
  IsColimit (F := parallelPair (X := K.X (c.prev j)) (Y := K.cycles j) (K.toCycles (c.prev j) j) 0)
    (CokernelCofork.ofπ (K.homologyπ j) ⋯)
⊢ IsColimit (F := parallelPair (Y := K.cycles j) (K.toCycles i j) 0) (CokernelCofork.ofπ (K.homologyπ j) ⋯)

Tactic:
subst hi
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
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 L M : HomologicalComplex.{v_1, u_1, u_2} C c
φ : K ⟶ L
iso : K ≅ L
ψ : L ⟶ M
j k : ι
inst_2 : K.HasHomology j
⊢ IsColimit (F := parallelPair (X := K.X (c.prev j)) (Y := K.cycles j) (K.toCycles (c.prev j) j) 0)
    (CokernelCofork.ofπ (K.homologyπ j) ⋯)

Tactic:
exact (K.sc j).homologyIsCokernel

Premises used: HomologicalComplex.sc, CategoryTheory.ShortComplex.homologyIsCokernel
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
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 L M : HomologicalComplex.{v_1, u_1, u_2} C c
φ : K ⟶ L
iso : K ≅ L
ψ : L ⟶ M
i j_1 k_1 : ι
inst_2 : K.HasHomology i
A : C
k : K.X i ⟶ A
j : ι
hj : c.prev i = j
hk : K.d j i ≫ k = 0
⊢ Eq (α := K.X (c.prev i) ⟶ A) (K.d (c.prev i) i ≫ k) 0

Tactic:
subst hj
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
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 L M : HomologicalComplex.{v_1, u_1, u_2} C c
φ : K ⟶ L
iso : K ≅ L
ψ : L ⟶ M
i j k_1 : ι
inst_2 : K.HasHomology i
A : C
k : K.X i ⟶ A
hk : Eq (α := K.X (c.prev i) ⟶ A) (K.d (c.prev i) i ≫ k) 0
⊢ (K.sc i).f ≫ k = 0

Tactic:
hk
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
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 L M : HomologicalComplex.{v_1, u_1, u_2} C c
φ : K ⟶ L
iso : K ≅ L
ψ : L ⟶ M
i j k_1 : ι
inst_2 : K.HasHomology i
A : C
k : K.X i ⟶ A
hk : Eq (α := K.X (c.prev i) ⟶ A) (K.d (c.prev i) i ≫ k) 0
⊢ (K.sc i).f ≫ k = 0

Tactic:
exact hk
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
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 : ι
inst_2 : K.HasHomology i
A : C
k : K.X i ⟶ A
j : ι
hj : c.prev i = j
hk : K.d j i ≫ k = 0
dsimp : CategoryStruct.comp (Y := K.opcycles i) (K.sc i).pOpcycles ((K.sc i).descOpcycles k ⋯) = k
⊢ CategoryStruct.comp (Y := K.opcycles i) (K.pOpcycles i) (K.descOpcycles k j hj hk) = k

Tactic:
dsimp [descOpcycles, pOpcycles]

Premises used: HomologicalComplex.pOpcycles, HomologicalComplex.descOpcycles
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
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 : ι
inst_2 : K.HasHomology i
A : C
k : K.X i ⟶ A
j : ι
hj : c.prev i = j
hk : K.d j i ≫ k = 0
⊢ CategoryStruct.comp (Y := K.opcycles i) (K.sc i).pOpcycles ((K.sc i).descOpcycles k ⋯) = k

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
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 : ι
inst_2 : K.HasHomology j
pos : ∀ (hij : c.Rel i j), Eq (α := K.X i ⟶ K.opcycles j) (K.d i j ≫ K.pOpcycles j) 0
neg : ∀ (hij : ¬c.Rel i j), Eq (α := K.X i ⟶ K.opcycles j) (K.d i j ≫ K.pOpcycles j) 0
⊢ Eq (α := K.X i ⟶ K.opcycles j) (K.d i j ≫ K.pOpcycles j) 0

Tactic:
by_cases hij : c.Rel i j

Premises used: ComplexShape.Rel
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
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 : ι
inst_2 : K.HasHomology j
hij : c.Rel i j
pos : ∀ (hij : c.Rel (c.prev j) j), Eq (α := K.X (c.prev j) ⟶ K.opcycles j) (K.d (c.prev j) j ≫ K.pOpcycles j) 0
⊢ Eq (α := K.X i ⟶ K.opcycles j) (K.d i j ≫ K.pOpcycles j) 0

Tactic:
obtain rfl := c.prev_eq' hij

Premises used: ComplexShape.prev_eq', rfl
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
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
hij : c.Rel (c.prev j) j
⊢ Eq (α := K.X (c.prev j) ⟶ K.opcycles j) (K.d (c.prev j) j ≫ K.pOpcycles j) 0

Tactic:
(K.sc j).f_pOpcycles

Premises used: HomologicalComplex.opcycles, HomologicalComplex.sc, HomologicalComplex.pOpcycles, CategoryTheory.ShortComplex.f_pOpcycles
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
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
hij : c.Rel (c.prev j) j
⊢ Eq (α := K.X (c.prev j) ⟶ K.opcycles j) (K.d (c.prev j) j ≫ K.pOpcycles j) 0

Tactic:
exact (K.sc j).f_pOpcycles

Premises used: HomologicalComplex.sc, CategoryTheory.ShortComplex.f_pOpcycles
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
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 : ι
inst_2 : K.HasHomology j
hij : ¬c.Rel i j
neg : Eq (α := K.X i ⟶ K.opcycles j) (0 ≫ K.pOpcycles j) 0
neg₁ neg₂ : Eq.{v_1 + 1} (α := K.X i ⟶ K.opcycles j) 0 0
⊢ Eq (α := K.X i ⟶ K.opcycles j) (K.d i j ≫ K.pOpcycles j) 0

Tactic:
rw [K.shape _ _ hij, zero_comp]

Premises used: CategoryTheory.Limits.zero_comp, HomologicalComplex.shape
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
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 L M : HomologicalComplex.{v_1, u_1, u_2} C c
φ : K ⟶ L
iso : K ≅ L
ψ : L ⟶ M
i j k : ι
inst_2 : K.HasHomology i
hi : c.prev j = i
inst_3 : K.HasHomology j
obtain :
  [K.HasHomology (c.prev j)] →
    IsColimit (F := parallelPair (X := K.X (c.prev j)) (K.d (c.prev j) j) 0)
      (CokernelCofork.ofπ (Z := K.opcycles j) (K.pOpcycles j) ⋯)
⊢ IsColimit (CokernelCofork.ofπ (Z := K.opcycles j) (K.pOpcycles j) ⋯)

Tactic:
obtain rfl := hi

Premises used: rfl
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
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 L M : HomologicalComplex.{v_1, u_1, u_2} C c
φ : K ⟶ L
iso : K ≅ L
ψ : L ⟶ M
j k : ι
inst_2 : K.HasHomology j
inst_3 : K.HasHomology (c.prev j)
⊢ IsColimit (F := parallelPair (X := K.X (c.prev j)) (K.d (c.prev j) j) 0)
    (CokernelCofork.ofπ (Z := K.opcycles j) (K.pOpcycles j) ⋯)

Tactic:
exact (K.sc j).opcyclesIsCokernel

Premises used: HomologicalComplex.sc, CategoryTheory.ShortComplex.opcyclesIsCokernel
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
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 : ι
inst_2 : K.HasHomology i
⊢ CategoryStruct.comp (Y := K.opcycles i) (K.pOpcycles i) (K.fromOpcycles i j) = K.d i j

Tactic:
p_descOpcycles _ _ _ _ _

Premises used: HomologicalComplex.fromOpcycles, HomologicalComplex.p_descOpcycles
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
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 L M : HomologicalComplex.{v_1, u_1, u_2} C c
φ : K ⟶ L
iso : K ≅ L
ψ : L ⟶ M
i j k : ι
inst_2 : K.HasHomology i
⊢ Epi (Y := K.opcycles i) (K.sc i).pOpcycles

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
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 L M : HomologicalComplex.{v_1, u_1, u_2} C c
φ : K ⟶ L
iso : K ≅ L
ψ : L ⟶ M
i j k : ι
inst_2 : K.HasHomology i
⊢ Mono (X := K.homology i) (K.sc i).homologyι

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
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 : ι
inst_2 : K.HasHomology i
⊢ Eq (α := K.opcycles i ⟶ K.X k) (K.fromOpcycles i j ≫ K.d j k) 0

Tactic:
simp only [← cancel_epi (K.pOpcycles i), p_fromOpcycles_assoc, d_comp_d, comp_zero]

Premises used: CategoryTheory.Limits.comp_zero, HomologicalComplex.d_comp_d, HomologicalComplex.pOpcycles, HomologicalComplex.p_fromOpcycles_assoc, CategoryTheory.cancel_epi
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
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 : ι
inst_2 : K.HasHomology i
hij : ¬c.Rel i j
rw :
  CategoryStruct.comp (Y := K.opcycles i) (K.pOpcycles i) (K.fromOpcycles i j) =
    CategoryStruct.comp (Y := K.opcycles i) (K.pOpcycles i) 0
rw₁ : K.d i j = CategoryStruct.comp (Y := K.opcycles i) (K.pOpcycles i) 0
rw₂ : K.d i j = 0
rw₃ rw₄ : Eq.{v_1 + 1} (α := K.X i ⟶ K.X j) 0 0
⊢ Eq (α := K.opcycles i ⟶ K.X j) (K.fromOpcycles i j) 0

Tactic:
rw [← cancel_epi (K.pOpcycles i), p_fromOpcycles, comp_zero, K.shape _ _ hij]

Premises used: HomologicalComplex.p_fromOpcycles, CategoryTheory.Limits.comp_zero, HomologicalComplex.pOpcycles, CategoryTheory.cancel_epi, HomologicalComplex.shape