awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.ExactFunctor (hypothesis)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Abelian.{v_1, u_1} C
inst_3 : Abelian.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.Additive
tfae_1_to_3 : ∀ (a : ∀ (S : ShortComplex.{v_1, u_1} C), S.ShortExact → ShortExact (S.map F)), F.PreservesHomology
hF : ∀ (S : ShortComplex.{v_1, u_1} C), S.Exact → Exact (S.map F)
S : ShortComplex.{v_1, u_1} C
hS : S.ShortExact
⊢ ShortExact (S.map F)
have this : Mono (X := X₁ (S.map F)) (f (S.map F))
Tactic: have : Mono (S.map F).f := exact_iff_mono _ (by simp) |>.1 <|
      hF (.mk (0 : 0 ⟶ S.X₁) S.f <| by simp) (exact_iff_mono _ (by simp) |>.2 hS.mono_f)
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.ExactFunctor (hypothesis)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Abelian.{v_1, u_1} C
inst_3 : Abelian.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.Additive
tfae_1_to_3 : ∀ (a : ∀ (S : ShortComplex.{v_1, u_1} C), S.ShortExact → ShortExact (S.map F)), F.PreservesHomology
hF : ∀ (S : ShortComplex.{v_1, u_1} C), S.Exact → Exact (S.map F)
S : ShortComplex.{v_1, u_1} C
hS : S.ShortExact
this : Mono (X := X₁ (S.map F)) (f (S.map F))
⊢ ShortExact (S.map F)
have this₁ : Epi (X := X₂ (S.map F)) (g (S.map F))
Tactic: have : Epi (S.map F).g := exact_iff_epi _ (by simp) |>.1 <|
      hF (.mk S.g (0 : S.X₃ ⟶ 0) <| by simp) (exact_iff_epi _ (by simp) |>.2 hS.epi_g)
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.ExactFunctor (hypothesis)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Abelian.{v_1, u_1} C
inst_3 : Abelian.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.Additive
tfae_1_to_3 : ∀ (a : ∀ (S : ShortComplex.{v_1, u_1} C), S.ShortExact → ShortExact (S.map F)), F.PreservesHomology
⊢ [∀ (S : ShortComplex.{v_1, u_1} C), S.ShortExact → ShortExact (S.map F),
      ∀ (S : ShortComplex.{v_1, u_1} C), S.Exact → Exact (S.map F), F.PreservesHomology,
      PreservesFiniteLimits F ∧ PreservesFiniteColimits F].TFAE
have tfae_2_to_1 : ∀ (a : ∀ (S : ShortComplex.{v_1, u_1} C), S.Exact → Exact (S.map F)) (S : ShortComplex.{v_1, u_1} C),
  S.ShortExact → ShortExact (S.map F)
Tactic: tfae_have 2 → 1
  | hF, S, hS => by
    have : Mono (S.map F).f := exact_iff_mono _ (by simp) |>.1 <|
      hF (.mk (0 : 0 ⟶ S.X₁) S.f <| by simp) (exact_iff_mono _ (by simp) |>.2 hS.mono_f)
    have : Epi (S.map F).g := exact_iff_epi _ (by simp) |>.1 <|
      hF (.mk S.g (0 : S.X₃ ⟶ 0) <| by simp) (exact_iff_epi _ (by simp) |>.2 hS.epi_g)
    exact ⟨hF S hS.exact⟩
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.ExactFunctor (hypothesis)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Abelian.{v_1, u_1} C
inst_3 : Abelian.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.Additive
tfae_1_to_3 : ∀ (a : ∀ (S : ShortComplex.{v_1, u_1} C), S.ShortExact → ShortExact (S.map F)), F.PreservesHomology
tfae_2_to_1 :
  ∀ (a : ∀ (S : ShortComplex.{v_1, u_1} C), S.Exact → Exact (S.map F)) (S : ShortComplex.{v_1, u_1} C),
    S.ShortExact → ShortExact (S.map F)
⊢ [∀ (S : ShortComplex.{v_1, u_1} C), S.ShortExact → ShortExact (S.map F),
      ∀ (S : ShortComplex.{v_1, u_1} C), S.Exact → Exact (S.map F), F.PreservesHomology,
      PreservesFiniteLimits F ∧ PreservesFiniteColimits F].TFAE
have tfae_3_to_4 : ∀ (a : F.PreservesHomology), PreservesFiniteLimits F ∧ PreservesFiniteColimits F
Tactic: tfae_have 3 → 4
  | h => ⟨preservesFiniteLimits_of_preservesHomology F,
      preservesFiniteColimits_of_preservesHomology F⟩
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.ExactFunctor (hypothesis)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Abelian.{v_1, u_1} C
inst_3 : Abelian.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.Additive
tfae_1_to_3 : ∀ (a : ∀ (S : ShortComplex.{v_1, u_1} C), S.ShortExact → ShortExact (S.map F)), F.PreservesHomology
tfae_2_to_1 :
  ∀ (a : ∀ (S : ShortComplex.{v_1, u_1} C), S.Exact → Exact (S.map F)) (S : ShortComplex.{v_1, u_1} C),
    S.ShortExact → ShortExact (S.map F)
tfae_3_to_4 : ∀ (a : F.PreservesHomology), PreservesFiniteLimits F ∧ PreservesFiniteColimits F
⊢ [∀ (S : ShortComplex.{v_1, u_1} C), S.ShortExact → ShortExact (S.map F),
      ∀ (S : ShortComplex.{v_1, u_1} C), S.Exact → Exact (S.map F), F.PreservesHomology,
      PreservesFiniteLimits F ∧ PreservesFiniteColimits F].TFAE
have tfae_4_to_2 : ∀ (a : PreservesFiniteLimits F ∧ PreservesFiniteColimits F) (S : ShortComplex.{v_1, u_1} C), S.Exact → Exact (S.map F)
Tactic: tfae_have 4 → 2
  | ⟨h1, h2⟩, _, h => h.map F
-- 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 : A ⟶ K.X i
j : ι
hj : c.next i = j
hk : k ≫ K.d i j = 0
⊢ k ≫ (K.sc i).g = 0
have hk₁ : Eq (α := A ⟶ K.X (c.next i)) (k ≫ K.d i (c.next i)) 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 : A ⟶ K.X i
j : ι
hj : c.next i = j
hk : k ≫ K.d i j = 0
⊢ CategoryStruct.comp (Y := K.cycles i) (K.liftCycles k j hj hk) (K.iCycles i) = k
have dsimp : CategoryStruct.comp (Y := K.cycles i) ((K.sc i).liftCycles k sorry) (K.sc i).iCycles = k
Tactic: dsimp [liftCycles, iCycles]
-- 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
⊢ Eq (α := K.cycles i ⟶ K.X j) (K.iCycles i ≫ K.d i j) 0
have pos : ∀ (hij : c.Rel i j), Eq (α := K.cycles i ⟶ K.X j) (K.iCycles i ≫ K.d i 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 i
pos : ∀ (hij : c.Rel i j), Eq (α := K.cycles i ⟶ K.X j) (K.iCycles i ≫ K.d i j) 0
⊢ Eq (α := K.cycles i ⟶ K.X j) (K.iCycles i ≫ K.d i j) 0
have neg : ∀ (hij : ¬c.Rel i j), Eq (α := K.cycles i ⟶ K.X j) (K.iCycles i ≫ K.d i 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 i
hij : c.Rel i j
⊢ Eq (α := K.cycles i ⟶ K.X j) (K.iCycles i ≫ K.d i j) 0
have pos : ∀ (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: obtain rfl := c.next_eq' hij
Cleared hypotheses: j, 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
⊢ Eq (α := K.cycles i ⟶ K.X j) (K.iCycles i ≫ K.d i j) 0
have neg : Eq (α := K.cycles i ⟶ K.X j) (K.iCycles i ≫ 0) 0
Tactic: rw [K.shape _ _ hij, 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 j : ι
inst_2 : K.HasHomology i
hij : ¬c.Rel i j
neg : Eq (α := K.cycles i ⟶ K.X j) (K.iCycles i ≫ 0) 0
⊢ Eq (α := K.cycles i ⟶ K.X j) (K.iCycles i ≫ K.d i j) 0
have neg₁ : Eq.{v_1 + 1} (α := K.cycles i ⟶ K.X j) 0 0
Tactic: rw [K.shape _ _ hij, 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
hj : c.next i = j
⊢ IsLimit (KernelFork.ofι (Z := K.cycles i) (K.iCycles i) ⋯)
have 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) sorry)
Tactic: obtain rfl := hj
Cleared hypotheses: j, hj
-- 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.cycles j) (K.toCycles i j) 0
have rw : CategoryStruct.comp (Y := K.cycles j) (K.toCycles i j) (K.iCycles j) =
  CategoryStruct.comp (Y := K.cycles j) 0 (K.iCycles j)
Tactic: rw [← cancel_mono (K.iCycles j), toCycles_i, zero_comp, 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 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)
⊢ Eq (α := K.X i ⟶ K.cycles j) (K.toCycles i j) 0
have rw₁ : K.d i j = CategoryStruct.comp (Y := K.cycles j) 0 (K.iCycles j)
Tactic: rw [← cancel_mono (K.iCycles j), toCycles_i, zero_comp, 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 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)
⊢ Eq (α := K.X i ⟶ K.cycles j) (K.toCycles i j) 0
have rw₂ : K.d i j = 0
Tactic: rw [← cancel_mono (K.iCycles j), toCycles_i, zero_comp, 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 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
⊢ Eq (α := K.X i ⟶ K.cycles j) (K.toCycles i j) 0
have rw₃ : Eq.{v_1 + 1} (α := K.X i ⟶ K.X j) 0 0
Tactic: rw [← cancel_mono (K.iCycles j), toCycles_i, zero_comp, 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 : A ⟶ K.X i
j : ι
hj : c.next i = j
hk : k ≫ K.d i j = 0
α : A' ⟶ A
⊢ (α ≫ k) ≫ K.d i j = 0
have rw : α ≫ k ≫ K.d i j = 0
Tactic: rw [assoc, hk, 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_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
⊢ (α ≫ k) ≫ K.d i j = 0
have rw₁ : Eq (α := A' ⟶ K.X j) (α ≫ 0) 0
Tactic: rw [assoc, hk, 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_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
⊢ (α ≫ k) ≫ K.d i j = 0
have rw₂ : Eq.{v_1 + 1} (α := A' ⟶ K.X j) 0 0
Tactic: rw [assoc, hk, 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_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
⊢ k ≫ K.d i j = 0
have rw : (x ≫ K.d i' i) ≫ K.d i j = 0
Tactic: rw [hx, assoc, K.d_comp_d, 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_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
⊢ k ≫ K.d i j = 0
have rw₁ : x ≫ K.d i' i ≫ K.d i j = 0
Tactic: rw [hx, assoc, K.d_comp_d, 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_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
⊢ k ≫ K.d i j = 0
have rw₂ : Eq (α := A ⟶ K.X j) (x ≫ 0) 0
Tactic: rw [hx, assoc, K.d_comp_d, 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_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
⊢ k ≫ K.d i j = 0
have rw₃ : Eq.{v_1 + 1} (α := A ⟶ K.X j) 0 0
Tactic: rw [hx, assoc, K.d_comp_d, 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 : A ⟶ K.X i
j : ι
hj : c.next i = j
i' : ι
x : A ⟶ K.X i'
hx : k = x ≫ K.d i' i
⊢ Eq (α := A ⟶ K.homology i) (K.liftCycles k j hj ⋯ ≫ K.homologyπ i) 0
have pos : ∀ (h : c.Rel i' i), Eq (α := A ⟶ K.homology i) (K.liftCycles k j hj sorry ≫ K.homologyπ i) 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 : 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
⊢ Eq (α := A ⟶ K.homology i) (K.liftCycles k j hj ⋯ ≫ K.homologyπ i) 0
have neg : ∀ (h : ¬c.Rel i' i), Eq (α := A ⟶ K.homology i) (K.liftCycles k j hj sorry ≫ K.homologyπ i) 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 : 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.homology i) (K.liftCycles k j hj ⋯ ≫ K.homologyπ i) 0
have 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 sorry ≫ K.homologyπ i) 0
Tactic: obtain rfl := c.prev_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 : 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 ≫ K.d i j = 0
have rw : (x ≫ K.d i' i) ≫ K.d i j = 0
Tactic: rw [hx, assoc, K.d_comp_d, 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 : 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
⊢ k ≫ K.d i j = 0
have rw₁ : x ≫ K.d i' i ≫ K.d i j = 0
Tactic: rw [hx, assoc, K.d_comp_d, 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 : 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
⊢ k ≫ K.d i j = 0
have rw₂ : Eq (α := A ⟶ K.X j) (x ≫ 0) 0
Tactic: rw [hx, assoc, K.d_comp_d, 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 : 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
⊢ k ≫ K.d i j = 0
have rw₃ : Eq.{v_1 + 1} (α := A ⟶ K.X j) 0 0
Tactic: rw [hx, assoc, K.d_comp_d, comp_zero]
-- 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 : 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
have hx₁ : k = 0
Tactic: rw [K.shape _ _ h, comp_zero] 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 : 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
⊢ Eq (α := A ⟶ K.cycles i) (K.liftCycles k j hj ⋯) 0
have rw : CategoryStruct.comp (Y := K.cycles i) (K.liftCycles k j hj sorry) (K.iCycles i) =
  CategoryStruct.comp (Y := K.cycles i) 0 (K.iCycles i)
Tactic: rw [← cancel_mono (K.iCycles i), zero_comp, liftCycles_i, 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 : 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)
⊢ Eq (α := A ⟶ K.cycles i) (K.liftCycles k j hj ⋯) 0
have rw₁ : CategoryStruct.comp (Y := K.cycles i) (K.liftCycles k j hj sorry) (K.iCycles i) = 0
Tactic: rw [← cancel_mono (K.iCycles i), zero_comp, liftCycles_i, 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 : 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
⊢ Eq (α := A ⟶ K.cycles i) (K.liftCycles k j hj ⋯) 0
have rw₃ : Eq.{v_1 + 1} (α := A ⟶ K.X i) 0 0
Tactic: rw [← cancel_mono (K.iCycles i), zero_comp, liftCycles_i, 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 : 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.homology i) (K.liftCycles k j hj ⋯ ≫ K.homologyπ i) 0
have this : Eq (α := A ⟶ K.cycles i) (K.liftCycles k j hj sorry) 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]
-- 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 : 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
⊢ Eq (α := A ⟶ K.homology i) (K.liftCycles k j hj ⋯ ≫ K.homologyπ i) 0
have neg : Eq (α := A ⟶ K.homology i) (0 ≫ K.homologyπ i) 0
Tactic: rw [this, 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 : 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
⊢ Eq (α := A ⟶ K.homology i) (K.liftCycles k j hj ⋯ ≫ K.homologyπ i) 0
have neg₁ : Eq.{v_1 + 1} (α := A ⟶ K.homology i) 0 0
Tactic: rw [this, zero_comp]