awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K 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
⊢ IsColimit (F := parallelPair (Y := K.cycles j) (K.toCycles i j) 0) (CokernelCofork.ofπ (K.homologyπ j) ⋯)
have 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) sorry)
Tactic: subst hi
Cleared hypotheses: i, hi
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex (hypothesis)
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
⊢ (K.sc i).f ≫ k = 0
have hk₁ : Eq (α := K.X (c.prev i) ⟶ A) (K.d (c.prev i) i ≫ k) 0
Tactic: subst hj
Cleared hypotheses: j, hj, hk
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
i : ι
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.pOpcycles i) (K.descOpcycles k j hj hk) = k
have dsimp : CategoryStruct.comp (Y := K.opcycles i) (K.sc i).pOpcycles ((K.sc i).descOpcycles k sorry) = k
Tactic: dsimp [descOpcycles, pOpcycles]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
i j : ι
inst_2 : K.HasHomology j
⊢ Eq (α := K.X i ⟶ K.opcycles j) (K.d i j ≫ K.pOpcycles j) 0
have pos : ∀ (hij : c.Rel i j), Eq (α := K.X i ⟶ K.opcycles j) (K.d i j ≫ K.pOpcycles j) 0
Tactic: by_cases hij : c.Rel i j
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
i j : ι
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
⊢ Eq (α := K.X i ⟶ K.opcycles j) (K.d i j ≫ K.pOpcycles j) 0
have neg : ∀ (hij : ¬c.Rel i j), Eq (α := K.X i ⟶ K.opcycles j) (K.d i j ≫ K.pOpcycles j) 0
Tactic: by_cases hij : c.Rel i j
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
i j : ι
inst_2 : K.HasHomology j
hij : c.Rel i j
⊢ Eq (α := K.X i ⟶ K.opcycles j) (K.d i j ≫ K.pOpcycles j) 0
have 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
Tactic: obtain rfl := c.prev_eq' hij
Cleared hypotheses: i, hij
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
i j : ι
inst_2 : K.HasHomology j
hij : ¬c.Rel i j
⊢ Eq (α := K.X i ⟶ K.opcycles j) (K.d i j ≫ K.pOpcycles j) 0
have neg : Eq (α := K.X i ⟶ K.opcycles j) (0 ≫ K.pOpcycles j) 0
Tactic: rw [K.shape _ _ hij, zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
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
⊢ Eq (α := K.X i ⟶ K.opcycles j) (K.d i j ≫ K.pOpcycles j) 0
have neg₁ : Eq.{v_1 + 1} (α := K.X i ⟶ K.opcycles j) 0 0
Tactic: rw [K.shape _ _ hij, zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K 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
⊢ IsColimit (CokernelCofork.ofπ (Z := K.opcycles j) (K.pOpcycles j) ⋯)
have 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) sorry)
Tactic: obtain rfl := hi
Cleared hypotheses: i, inst_2, hi
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
i j : ι
inst_2 : K.HasHomology i
hij : ¬c.Rel i j
⊢ Eq (α := K.opcycles i ⟶ K.X j) (K.fromOpcycles i j) 0
have rw : CategoryStruct.comp (Y := K.opcycles i) (K.pOpcycles i) (K.fromOpcycles i j) =
  CategoryStruct.comp (Y := K.opcycles i) (K.pOpcycles i) 0
Tactic: rw [← cancel_epi (K.pOpcycles i), p_fromOpcycles, comp_zero, K.shape _ _ hij]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
i j : ι
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
⊢ Eq (α := K.opcycles i ⟶ K.X j) (K.fromOpcycles i j) 0
have rw₁ : K.d i j = CategoryStruct.comp (Y := K.opcycles i) (K.pOpcycles i) 0
Tactic: rw [← cancel_epi (K.pOpcycles i), p_fromOpcycles, comp_zero, K.shape _ _ hij]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
i j : ι
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
⊢ Eq (α := K.opcycles i ⟶ K.X j) (K.fromOpcycles i j) 0
have rw₂ : K.d i j = 0
Tactic: rw [← cancel_epi (K.pOpcycles i), p_fromOpcycles, comp_zero, K.shape _ _ hij]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
i j : ι
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
⊢ Eq (α := K.opcycles i ⟶ K.X j) (K.fromOpcycles i j) 0
have rw₃ : Eq.{v_1 + 1} (α := K.X i ⟶ K.X j) 0 0
Tactic: rw [← cancel_epi (K.pOpcycles i), p_fromOpcycles, comp_zero, K.shape _ _ hij]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K 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 : K.X i ⟶ A
j : ι
hj : c.prev i = j
hk : K.d j i ≫ k = 0
α : A ⟶ A'
⊢ K.d j i ≫ k ≫ α = 0
have rw : Eq (α := K.X j ⟶ A') (0 ≫ α) 0
Tactic: rw [reassoc_of% hk, zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K 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 : K.X i ⟶ A
j : ι
hj : c.prev i = j
hk : K.d j i ≫ k = 0
α : A ⟶ A'
rw : Eq (α := K.X j ⟶ A') (0 ≫ α) 0
⊢ K.d j i ≫ k ≫ α = 0
have rw₁ : Eq.{v_1 + 1} (α := K.X j ⟶ A') 0 0
Tactic: rw [reassoc_of% hk, zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K 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
i' : ι
x : K.X i' ⟶ A
hx : k = K.d i i' ≫ x
⊢ K.d j i ≫ k = 0
have rw : K.d j i ≫ K.d i i' ≫ x = 0
Tactic: rw [hx, K.d_comp_d_assoc, zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K 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
i' : ι
x : K.X i' ⟶ A
hx : k = K.d i i' ≫ x
rw : K.d j i ≫ K.d i i' ≫ x = 0
⊢ K.d j i ≫ k = 0
have rw₁ : Eq (α := K.X j ⟶ A) (0 ≫ x) 0
Tactic: rw [hx, K.d_comp_d_assoc, zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K 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
i' : ι
x : K.X i' ⟶ A
hx : k = K.d i i' ≫ x
rw : K.d j i ≫ K.d i i' ≫ x = 0
rw₁ : Eq (α := K.X j ⟶ A) (0 ≫ x) 0
⊢ K.d j i ≫ k = 0
have rw₂ : Eq.{v_1 + 1} (α := K.X j ⟶ A) 0 0
Tactic: rw [hx, K.d_comp_d_assoc, zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
i : ι
inst_2 : K.HasHomology i
A : C
k : K.X i ⟶ A
j : ι
hj : c.prev i = j
i' : ι
x : K.X i' ⟶ A
hx : k = K.d i i' ≫ x
⊢ Eq (α := K.homology i ⟶ A) (K.homologyι i ≫ K.descOpcycles k j hj ⋯) 0
have pos : ∀ (h : c.Rel i i'), Eq (α := K.homology i ⟶ A) (K.homologyι i ≫ K.descOpcycles k j hj sorry) 0
Tactic: by_cases h : c.Rel i i'
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
i : ι
inst_2 : K.HasHomology i
A : C
k : K.X i ⟶ A
j : ι
hj : c.prev i = j
i' : ι
x : K.X i' ⟶ A
hx : k = K.d i i' ≫ x
pos : ∀ (h : c.Rel i i'), Eq (α := K.homology i ⟶ A) (K.homologyι i ≫ K.descOpcycles k j hj ⋯) 0
⊢ Eq (α := K.homology i ⟶ A) (K.homologyι i ≫ K.descOpcycles k j hj ⋯) 0
have neg : ∀ (h : ¬c.Rel i i'), Eq (α := K.homology i ⟶ A) (K.homologyι i ≫ K.descOpcycles k j hj sorry) 0
Tactic: by_cases h : c.Rel i i'
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
i : ι
inst_2 : K.HasHomology i
A : C
k : K.X i ⟶ A
j : ι
hj : c.prev i = j
i' : ι
x : K.X i' ⟶ A
hx : k = K.d i i' ≫ x
h : c.Rel i i'
⊢ Eq (α := K.homology i ⟶ A) (K.homologyι i ≫ K.descOpcycles k j hj ⋯) 0
have pos : ∀ (x : K.X (c.next i) ⟶ A) (hx : k = K.d i (c.next i) ≫ x) (h : c.Rel i (c.next i)),
  Eq (α := K.homology i ⟶ A) (K.homologyι i ≫ K.descOpcycles k j hj sorry) 0
Tactic: obtain rfl := c.next_eq' h
Cleared hypotheses: i', x, hx, h
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
i : ι
inst_2 : K.HasHomology i
A : C
k : K.X i ⟶ A
j : ι
hj : c.prev i = j
i' : ι
x : K.X i' ⟶ A
hx : k = K.d i i' ≫ x
h : ¬c.Rel i i'
⊢ K.d j i ≫ k = 0
have rw : K.d j i ≫ K.d i i' ≫ x = 0
Tactic: rw [hx, K.d_comp_d_assoc, zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
i : ι
inst_2 : K.HasHomology i
A : C
k : K.X i ⟶ A
j : ι
hj : c.prev i = j
i' : ι
x : K.X i' ⟶ A
hx : k = K.d i i' ≫ x
h : ¬c.Rel i i'
rw : K.d j i ≫ K.d i i' ≫ x = 0
⊢ K.d j i ≫ k = 0
have rw₁ : Eq (α := K.X j ⟶ A) (0 ≫ x) 0
Tactic: rw [hx, K.d_comp_d_assoc, zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
i : ι
inst_2 : K.HasHomology i
A : C
k : K.X i ⟶ A
j : ι
hj : c.prev i = j
i' : ι
x : K.X i' ⟶ A
hx : k = K.d i i' ≫ x
h : ¬c.Rel i i'
rw : K.d j i ≫ K.d i i' ≫ x = 0
rw₁ : Eq (α := K.X j ⟶ A) (0 ≫ x) 0
⊢ K.d j i ≫ k = 0
have rw₂ : Eq.{v_1 + 1} (α := K.X j ⟶ A) 0 0
Tactic: rw [hx, K.d_comp_d_assoc, zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex (hypothesis)
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
i' : ι
x : K.X i' ⟶ A
hx : k = K.d i i' ≫ x
h : ¬c.Rel i i'
⊢ Eq (α := K.opcycles i ⟶ A) (K.descOpcycles k j hj ⋯) 0
have hx₁ : k = 0
Tactic: rw [K.shape _ _ h, zero_comp] at hx
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
i : ι
inst_2 : K.HasHomology i
A : C
k : K.X i ⟶ A
j : ι
hj : c.prev i = j
i' : ι
x : K.X i' ⟶ A
hx_1 : k = K.d i i' ≫ x
hx : k = 0
h : ¬c.Rel i i'
⊢ Eq (α := K.opcycles i ⟶ A) (K.descOpcycles k j hj ⋯) 0
have rw : CategoryStruct.comp (Y := K.opcycles i) (K.pOpcycles i) (K.descOpcycles k j hj sorry) =
  CategoryStruct.comp (Y := K.opcycles i) (K.pOpcycles i) 0
Tactic: rw [← cancel_epi (K.pOpcycles i), comp_zero, p_descOpcycles, hx]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
i : ι
inst_2 : K.HasHomology i
A : C
k : K.X i ⟶ A
j : ι
hj : c.prev i = j
i' : ι
x : K.X i' ⟶ A
hx_1 : k = K.d i i' ≫ x
hx : k = 0
h : ¬c.Rel i i'
rw :
  CategoryStruct.comp (Y := K.opcycles i) (K.pOpcycles i) (K.descOpcycles k j hj ⋯) =
    CategoryStruct.comp (Y := K.opcycles i) (K.pOpcycles i) 0
⊢ Eq (α := K.opcycles i ⟶ A) (K.descOpcycles k j hj ⋯) 0
have rw₁ : CategoryStruct.comp (Y := K.opcycles i) (K.pOpcycles i) (K.descOpcycles k j hj sorry) = 0
Tactic: rw [← cancel_epi (K.pOpcycles i), comp_zero, p_descOpcycles, hx]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
i : ι
inst_2 : K.HasHomology i
A : C
k : K.X i ⟶ A
j : ι
hj : c.prev i = j
i' : ι
x : K.X i' ⟶ A
hx_1 : k = K.d i i' ≫ x
hx : k = 0
h : ¬c.Rel i i'
rw :
  CategoryStruct.comp (Y := K.opcycles i) (K.pOpcycles i) (K.descOpcycles k j hj ⋯) =
    CategoryStruct.comp (Y := K.opcycles i) (K.pOpcycles i) 0
rw₁ : CategoryStruct.comp (Y := K.opcycles i) (K.pOpcycles i) (K.descOpcycles k j hj ⋯) = 0
rw₂ : k = 0
⊢ Eq (α := K.opcycles i ⟶ A) (K.descOpcycles k j hj ⋯) 0
have rw₃ : Eq.{v_1 + 1} (α := K.X i ⟶ A) 0 0
Tactic: rw [← cancel_epi (K.pOpcycles i), comp_zero, p_descOpcycles, hx]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex (hypothesis)
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
i' : ι
x : K.X i' ⟶ A
hx : k = K.d i i' ≫ x
h : ¬c.Rel i i'
⊢ Eq (α := K.homology i ⟶ A) (K.homologyι i ≫ K.descOpcycles k j hj ⋯) 0
have this : Eq (α := K.opcycles i ⟶ A) (K.descOpcycles k j hj sorry) 0
Tactic: have : K.descOpcycles k j hj (by rw [hx, K.d_comp_d_assoc, zero_comp]) = 0 := by
      rw [K.shape _ _ h, zero_comp] at hx
      rw [← cancel_epi (K.pOpcycles i), comp_zero, p_descOpcycles, hx]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
i : ι
inst_2 : K.HasHomology i
A : C
k : K.X i ⟶ A
j : ι
hj : c.prev i = j
i' : ι
x : K.X i' ⟶ A
hx : k = K.d i i' ≫ x
h : ¬c.Rel i i'
this : Eq (α := K.opcycles i ⟶ A) (K.descOpcycles k j hj ⋯) 0
⊢ Eq (α := K.homology i ⟶ A) (K.homologyι i ≫ K.descOpcycles k j hj ⋯) 0
have neg : Eq (α := K.homology i ⟶ A) (K.homologyι i ≫ 0) 0
Tactic: rw [this, comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
i : ι
inst_2 : K.HasHomology i
A : C
k : K.X i ⟶ A
j : ι
hj : c.prev i = j
i' : ι
x : K.X i' ⟶ A
hx : k = K.d i i' ≫ x
h : ¬c.Rel i i'
this : Eq (α := K.opcycles i ⟶ A) (K.descOpcycles k j hj ⋯) 0
neg : Eq (α := K.homology i ⟶ A) (K.homologyι i ≫ 0) 0
⊢ Eq (α := K.homology i ⟶ A) (K.homologyι i ≫ K.descOpcycles k j hj ⋯) 0
have neg₁ : Eq.{v_1 + 1} (α := K.homology i ⟶ A) 0 0
Tactic: rw [this, comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K 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.next i = j
⊢ IsLimit (F := parallelPair (X := K.opcycles i) (K.fromOpcycles i j) 0) (KernelFork.ofι (K.homologyι i) ⋯)
have subst : IsLimit (F := parallelPair (X := K.opcycles i) (Y := K.X (c.next i)) (K.fromOpcycles i (c.next i)) 0)
  (KernelFork.ofι (K.homologyι i) sorry)
Tactic: subst hi
Cleared hypotheses: j, hi
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K L M : HomologicalComplex.{v_1, u_1, u_2} C c
φ : K ⟶ L
ψ : L ⟶ M
i : ι
inst_2 : K.HasHomology i
inst_3 : L.HasHomology i
inst_4 : M.HasHomology i
⊢ Eq (α := K.homology i ⟶ M.homology i) (homologyMap (φ ≫ ψ) i)
    (CategoryStruct.comp (Y := L.homology i) (homologyMap φ i) (homologyMap ψ i))
have dsimp : Eq (α := K.homology i ⟶ M.homology i)
  (ShortComplex.homologyMap (CategoryTheory.Functor.map (shortComplexFunctor C c i) (φ ≫ ψ)))
  (CategoryStruct.comp (Y := L.homology i)
    (ShortComplex.homologyMap (CategoryTheory.Functor.map (shortComplexFunctor C c i) φ))
    (ShortComplex.homologyMap (CategoryTheory.Functor.map (shortComplexFunctor C c i) ψ)))
Tactic: dsimp [homologyMap]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K L M : HomologicalComplex.{v_1, u_1, u_2} C c
φ : K ⟶ L
ψ : L ⟶ M
i : ι
inst_2 : K.HasHomology i
inst_3 : L.HasHomology i
inst_4 : M.HasHomology i
⊢ Eq (α := K.homology i ⟶ M.homology i)
    (ShortComplex.homologyMap (CategoryTheory.Functor.map (shortComplexFunctor C c i) (φ ≫ ψ)))
    (CategoryStruct.comp (Y := L.homology i)
      (ShortComplex.homologyMap (CategoryTheory.Functor.map (shortComplexFunctor C c i) φ))
      (ShortComplex.homologyMap (CategoryTheory.Functor.map (shortComplexFunctor C c i) ψ)))
have rw : Eq (α := K.homology i ⟶ M.homology i)
  (ShortComplex.homologyMap
    (CategoryTheory.Functor.map (shortComplexFunctor C c i) φ ≫
      CategoryTheory.Functor.map (shortComplexFunctor C c i) ψ))
  (CategoryStruct.comp (Y := L.homology i)
    (ShortComplex.homologyMap (CategoryTheory.Functor.map (shortComplexFunctor C c i) φ))
    (ShortComplex.homologyMap (CategoryTheory.Functor.map (shortComplexFunctor C c i) ψ)))
Tactic: rw [Functor.map_comp, ShortComplex.homologyMap_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K L M : HomologicalComplex.{v_1, u_1, u_2} C c
φ : K ⟶ L
ψ : L ⟶ M
i : ι
inst_2 : K.HasHomology i
inst_3 : L.HasHomology i
inst_4 : M.HasHomology i
rw :
  Eq (α := K.homology i ⟶ M.homology i)
    (ShortComplex.homologyMap
      (CategoryTheory.Functor.map (shortComplexFunctor C c i) φ ≫
        CategoryTheory.Functor.map (shortComplexFunctor C c i) ψ))
    (CategoryStruct.comp (Y := L.homology i)
      (ShortComplex.homologyMap (CategoryTheory.Functor.map (shortComplexFunctor C c i) φ))
      (ShortComplex.homologyMap (CategoryTheory.Functor.map (shortComplexFunctor C c i) ψ)))
⊢ Eq (α := K.homology i ⟶ M.homology i)
    (ShortComplex.homologyMap (CategoryTheory.Functor.map (shortComplexFunctor C c i) (φ ≫ ψ)))
    (CategoryStruct.comp (Y := L.homology i)
      (ShortComplex.homologyMap (CategoryTheory.Functor.map (shortComplexFunctor C c i) φ))
      (ShortComplex.homologyMap (CategoryTheory.Functor.map (shortComplexFunctor C c i) ψ)))
have rw₁ : Eq (α := K.homology i ⟶ M.homology i)
  (CategoryStruct.comp (Y := (Functor.obj (shortComplexFunctor C c i) L).homology)
    (ShortComplex.homologyMap (CategoryTheory.Functor.map (shortComplexFunctor C c i) φ))
    (ShortComplex.homologyMap (CategoryTheory.Functor.map (shortComplexFunctor C c i) ψ)))
  (CategoryStruct.comp (Y := L.homology i)
    (ShortComplex.homologyMap (CategoryTheory.Functor.map (shortComplexFunctor C c i) φ))
    (ShortComplex.homologyMap (CategoryTheory.Functor.map (shortComplexFunctor C c i) ψ)))
Tactic: rw [Functor.map_comp, ShortComplex.homologyMap_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K L M : HomologicalComplex.{v_1, u_1, u_2} C c
φ : K ⟶ L
ψ : L ⟶ M
i : ι
inst_2 : K.HasHomology i
inst_3 : L.HasHomology i
inst_4 : M.HasHomology i
⊢ Eq (α := K.cycles i ⟶ M.cycles i) (cyclesMap (φ ≫ ψ) i)
    (CategoryStruct.comp (Y := L.cycles i) (cyclesMap φ i) (cyclesMap ψ i))
have dsimp : Eq (α := K.cycles i ⟶ M.cycles i)
  (ShortComplex.cyclesMap (CategoryTheory.Functor.map (shortComplexFunctor C c i) (φ ≫ ψ)))
  (CategoryStruct.comp (Y := L.cycles i)
    (ShortComplex.cyclesMap (CategoryTheory.Functor.map (shortComplexFunctor C c i) φ))
    (ShortComplex.cyclesMap (CategoryTheory.Functor.map (shortComplexFunctor C c i) ψ)))
Tactic: dsimp [cyclesMap]