awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologySequenceLemmas (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex.{v_1, u_1, u_2} C c)
hS : S.ShortExact
j : ι
h₁ : Mono (X := S.X₂.homology j) (Y := S.X₃.homology j) (HomologicalComplex.homologyMap S.g j)
h₂ : ∀ (i : ι), c.Rel i j → Epi (X := S.X₂.homology i) (Y := S.X₃.homology i) (HomologicalComplex.homologyMap S.g i)
i : ι
hij : c.Rel i j
this : Epi (X := S.X₂.homology i) (Y := S.X₃.homology i) (HomologicalComplex.homologyMap S.g i)
⊢ IsZero.{v_1, u_1} (S.X₁.homology j)
have pos : { X₁ := S.X₃.homology i, X₂ := S.X₁.homology j, X₃ := S.X₂.homology j, f := hS.δ i j hij,
      g := HomologicalComplex.homologyMap S.f j, zero := sorry : ShortComplex.{v_1, u_1} C }.f =
  0
Tactic: apply (hS.homology_exact₁ i j hij).isZero_X₂
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologySequenceLemmas (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex.{v_1, u_1, u_2} C c)
hS : S.ShortExact
j : ι
h₁ : Mono (X := S.X₂.homology j) (Y := S.X₃.homology j) (HomologicalComplex.homologyMap S.g j)
h₂ : ∀ (i : ι), c.Rel i j → Epi (X := S.X₂.homology i) (Y := S.X₃.homology i) (HomologicalComplex.homologyMap S.g i)
i : ι
hij : c.Rel i j
this : Epi (X := S.X₂.homology i) (Y := S.X₃.homology i) (HomologicalComplex.homologyMap S.g i)
pos :
  { X₁ := S.X₃.homology i, X₂ := S.X₁.homology j, X₃ := S.X₂.homology j, f := hS.δ i j hij,
        g := HomologicalComplex.homologyMap S.f j, zero := ⋯ : ShortComplex.{v_1, u_1} C }.f =
    0
⊢ IsZero.{v_1, u_1} (S.X₁.homology j)
have pos₁ : { X₁ := S.X₃.homology i, X₂ := S.X₁.homology j, X₃ := S.X₂.homology j, f := hS.δ i j hij,
      g := HomologicalComplex.homologyMap S.f j, zero := sorry : ShortComplex.{v_1, u_1} C }.g =
  0
Tactic: apply (hS.homology_exact₁ i j hij).isZero_X₂
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologySequenceLemmas (hypothesis)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex.{v_1, u_1, u_2} C c)
hS : S.ShortExact
j : ι
h₁ : Mono (X := S.X₂.homology j) (Y := S.X₃.homology j) (HomologicalComplex.homologyMap S.g j)
h₂ : ∀ (i : ι), c.Rel i j → Epi (X := S.X₂.homology i) (Y := S.X₃.homology i) (HomologicalComplex.homologyMap S.g i)
hj : ∀ (i : ι), ¬c.Rel i j
⊢ IsZero.{v_1, u_1} (S.X₁.homology j)
have this : Mono S.f
Tactic: have := hS.mono_f
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologySequenceLemmas (hypothesis)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex.{v_1, u_1, u_2} C c)
hS : S.ShortExact
j : ι
h₁ : Mono (X := S.X₂.homology j) (Y := S.X₃.homology j) (HomologicalComplex.homologyMap S.g j)
h₂ : ∀ (i : ι), c.Rel i j → Epi (X := S.X₂.homology i) (Y := S.X₃.homology i) (HomologicalComplex.homologyMap S.g i)
hj : ∀ (i : ι), ¬c.Rel i j
this : Mono S.f
⊢ IsZero.{v_1, u_1} (S.X₁.homology j)
have this₁ : Mono (X := S.X₁.homology j) (Y := S.X₂.homology j) (HomologicalComplex.homologyMap S.f j)
Tactic: have := HomologicalComplex.mono_homologyMap_of_mono_of_not_rel S.f j hj
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologySequenceLemmas (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex.{v_1, u_1, u_2} C c)
hS : S.ShortExact
j : ι
h₁ : Mono (X := S.X₂.homology j) (Y := S.X₃.homology j) (HomologicalComplex.homologyMap S.g j)
h₂ : ∀ (i : ι), c.Rel i j → Epi (X := S.X₂.homology i) (Y := S.X₃.homology i) (HomologicalComplex.homologyMap S.g i)
hj : ∀ (i : ι), ¬c.Rel i j
this_1 : Mono S.f
this : Mono (X := S.X₁.homology j) (Y := S.X₂.homology j) (HomologicalComplex.homologyMap S.f j)
⊢ IsZero.{v_1, u_1} (S.X₁.homology j)
have neg : Eq (α := S.X₁.homology j ⟶ S.X₃.homology j)
  (CategoryStruct.comp (Y := S.X₂.homology j) (𝟙 (S.X₁.homology j) ≫ HomologicalComplex.homologyMap S.f j)
    (HomologicalComplex.homologyMap S.g j))
  (CategoryStruct.comp (Y := S.X₂.homology j)
    (CategoryStruct.comp (Y := S.X₁.homology j) 0 (HomologicalComplex.homologyMap S.f j))
    (HomologicalComplex.homologyMap S.g j))
Tactic: rw [IsZero.iff_id_eq_zero,
      ← cancel_mono (HomologicalComplex.homologyMap S.f j),
      ← cancel_mono (HomologicalComplex.homologyMap S.g j)]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologySequenceLemmas (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex.{v_1, u_1, u_2} C c)
hS : S.ShortExact
i : ι
h₁ : S.X₁.ExactAt i
h₃ : S.X₃.ExactAt i
⊢ S.X₂.ExactAt i
have rw : ∀ (h₁ : IsZero.{v_1, u_1} (S.X₁.homology i)) (h₃ : IsZero.{v_1, u_1} (S.X₃.homology i)),
  IsZero.{v_1, u_1} (S.X₂.homology i)
Tactic: rw [exactAt_iff_isZero_homology] at h₁ h₃ ⊢
Cleared hypotheses: h₁, h₃
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologySequenceLemmas (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex.{v_1, u_1, u_2} C c)
hS : S.ShortExact
i : ι
h₁ : Epi (X := S.X₁.homology i) (Y := S.X₂.homology i) (HomologicalComplex.homologyMap S.f i)
h₂ : ∀ (j : ι), c.Rel i j → Mono (X := S.X₁.homology j) (Y := S.X₂.homology j) (HomologicalComplex.homologyMap S.f j)
⊢ S.X₃.ExactAt i
have rw : IsZero.{v_1, u_1} (S.X₃.homology i)
Tactic: rw [exactAt_iff_isZero_homology]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologySequenceLemmas (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex.{v_1, u_1, u_2} C c)
hS : S.ShortExact
i : ι
h₁ : Epi (X := S.X₁.homology i) (Y := S.X₂.homology i) (HomologicalComplex.homologyMap S.f i)
h₂ : ∀ (j : ι), c.Rel i j → Mono (X := S.X₁.homology j) (Y := S.X₂.homology j) (HomologicalComplex.homologyMap S.f j)
⊢ IsZero.{v_1, u_1} (S.X₃.homology i)
have pos : ∀ (hi : ∃ (j : ι), c.Rel i j), IsZero.{v_1, u_1} (S.X₃.homology i)
Tactic: by_cases! hi : ∃ j, c.Rel i j
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologySequenceLemmas (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex.{v_1, u_1, u_2} C c)
hS : S.ShortExact
i : ι
h₁ : Epi (X := S.X₁.homology i) (Y := S.X₂.homology i) (HomologicalComplex.homologyMap S.f i)
h₂ : ∀ (j : ι), c.Rel i j → Mono (X := S.X₁.homology j) (Y := S.X₂.homology j) (HomologicalComplex.homologyMap S.f j)
pos : ∀ (hi : ∃ (j : ι), c.Rel i j), IsZero.{v_1, u_1} (S.X₃.homology i)
⊢ IsZero.{v_1, u_1} (S.X₃.homology i)
have neg : ∀ (hi : ∀ (j : ι), ¬c.Rel i j), IsZero.{v_1, u_1} (S.X₃.homology i)
Tactic: by_cases! hi : ∃ j, c.Rel i j
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologySequenceLemmas (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex.{v_1, u_1, u_2} C c)
hS : S.ShortExact
i : ι
h₁ : Epi (X := S.X₁.homology i) (Y := S.X₂.homology i) (HomologicalComplex.homologyMap S.f i)
h₂ : ∀ (j : ι), c.Rel i j → Mono (X := S.X₁.homology j) (Y := S.X₂.homology j) (HomologicalComplex.homologyMap S.f j)
hi : ∃ (j : ι), c.Rel i j
⊢ IsZero.{v_1, u_1} (S.X₃.homology i)
have pos : ∀ (j : ι) (hij : c.Rel i j), IsZero.{v_1, u_1} (S.X₃.homology i)
Tactic: obtain ⟨j, hij⟩ := hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologySequenceLemmas (hypothesis)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex.{v_1, u_1, u_2} C c)
hS : S.ShortExact
i : ι
h₁ : Epi (X := S.X₁.homology i) (Y := S.X₂.homology i) (HomologicalComplex.homologyMap S.f i)
h₂ : ∀ (j : ι), c.Rel i j → Mono (X := S.X₁.homology j) (Y := S.X₂.homology j) (HomologicalComplex.homologyMap S.f j)
j : ι
hij : c.Rel i j
⊢ IsZero.{v_1, u_1} (S.X₃.homology i)
have this : Mono (X := S.X₁.homology j) (Y := S.X₂.homology j) (HomologicalComplex.homologyMap S.f j)
Tactic: have := h₂ j hij
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologySequenceLemmas (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex.{v_1, u_1, u_2} C c)
hS : S.ShortExact
i : ι
h₁ : Epi (X := S.X₁.homology i) (Y := S.X₂.homology i) (HomologicalComplex.homologyMap S.f i)
h₂ : ∀ (j : ι), c.Rel i j → Mono (X := S.X₁.homology j) (Y := S.X₂.homology j) (HomologicalComplex.homologyMap S.f j)
j : ι
hij : c.Rel i j
this : Mono (X := S.X₁.homology j) (Y := S.X₂.homology j) (HomologicalComplex.homologyMap S.f j)
⊢ IsZero.{v_1, u_1} (S.X₃.homology i)
have pos : { X₁ := S.X₂.homology i, X₂ := S.X₃.homology i, X₃ := S.X₁.homology j, f := HomologicalComplex.homologyMap S.g i,
      g := hS.δ i j hij, zero := sorry : ShortComplex.{v_1, u_1} C }.f =
  0
Tactic: apply (hS.homology_exact₃ i j hij).isZero_X₂
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologySequenceLemmas (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex.{v_1, u_1, u_2} C c)
hS : S.ShortExact
i : ι
h₁ : Epi (X := S.X₁.homology i) (Y := S.X₂.homology i) (HomologicalComplex.homologyMap S.f i)
h₂ : ∀ (j : ι), c.Rel i j → Mono (X := S.X₁.homology j) (Y := S.X₂.homology j) (HomologicalComplex.homologyMap S.f j)
j : ι
hij : c.Rel i j
this : Mono (X := S.X₁.homology j) (Y := S.X₂.homology j) (HomologicalComplex.homologyMap S.f j)
pos :
  { X₁ := S.X₂.homology i, X₂ := S.X₃.homology i, X₃ := S.X₁.homology j, f := HomologicalComplex.homologyMap S.g i,
        g := hS.δ i j hij, zero := ⋯ : ShortComplex.{v_1, u_1} C }.f =
    0
⊢ IsZero.{v_1, u_1} (S.X₃.homology i)
have pos₁ : { X₁ := S.X₂.homology i, X₂ := S.X₃.homology i, X₃ := S.X₁.homology j, f := HomologicalComplex.homologyMap S.g i,
      g := hS.δ i j hij, zero := sorry : ShortComplex.{v_1, u_1} C }.g =
  0
Tactic: apply (hS.homology_exact₃ i j hij).isZero_X₂
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologySequenceLemmas (hypothesis)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex.{v_1, u_1, u_2} C c)
hS : S.ShortExact
i : ι
h₁ : Epi (X := S.X₁.homology i) (Y := S.X₂.homology i) (HomologicalComplex.homologyMap S.f i)
h₂ : ∀ (j : ι), c.Rel i j → Mono (X := S.X₁.homology j) (Y := S.X₂.homology j) (HomologicalComplex.homologyMap S.f j)
hi : ∀ (j : ι), ¬c.Rel i j
⊢ IsZero.{v_1, u_1} (S.X₃.homology i)
have this : Epi S.g
Tactic: have := hS.epi_g
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologySequenceLemmas (hypothesis)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex.{v_1, u_1, u_2} C c)
hS : S.ShortExact
i : ι
h₁ : Epi (X := S.X₁.homology i) (Y := S.X₂.homology i) (HomologicalComplex.homologyMap S.f i)
h₂ : ∀ (j : ι), c.Rel i j → Mono (X := S.X₁.homology j) (Y := S.X₂.homology j) (HomologicalComplex.homologyMap S.f j)
hi : ∀ (j : ι), ¬c.Rel i j
this : Epi S.g
⊢ IsZero.{v_1, u_1} (S.X₃.homology i)
have this₁ : Epi (X := S.X₂.homology i) (Y := S.X₃.homology i) (HomologicalComplex.homologyMap S.g i)
Tactic: have := HomologicalComplex.epi_homologyMap_of_epi_of_not_rel S.g i hi
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologySequenceLemmas (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex.{v_1, u_1, u_2} C c)
hS : S.ShortExact
i : ι
h₁ : Epi (X := S.X₁.homology i) (Y := S.X₂.homology i) (HomologicalComplex.homologyMap S.f i)
h₂ : ∀ (j : ι), c.Rel i j → Mono (X := S.X₁.homology j) (Y := S.X₂.homology j) (HomologicalComplex.homologyMap S.f j)
hi : ∀ (j : ι), ¬c.Rel i j
this_1 : Epi S.g
this : Epi (X := S.X₂.homology i) (Y := S.X₃.homology i) (HomologicalComplex.homologyMap S.g i)
⊢ IsZero.{v_1, u_1} (S.X₃.homology i)
have neg : Eq (α := S.X₁.homology i ⟶ S.X₃.homology i)
  (CategoryStruct.comp (Y := S.X₂.homology i) (HomologicalComplex.homologyMap S.f i)
    (HomologicalComplex.homologyMap S.g i ≫ 𝟙 (S.X₃.homology i)))
  (CategoryStruct.comp (Y := S.X₂.homology i) (HomologicalComplex.homologyMap S.f i)
    (CategoryStruct.comp (Y := S.X₃.homology i) (HomologicalComplex.homologyMap S.g i) 0))
Tactic: rw [IsZero.iff_id_eq_zero,
      ← cancel_epi (HomologicalComplex.homologyMap S.g i),
      ← cancel_epi (HomologicalComplex.homologyMap S.f i)]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Homotopy (goal)
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
c : ComplexShape ι
C D : HomologicalComplex.{v, u, u_1} V c
f : (i j : ι) → C.X i ⟶ D.X j
i i' : ι
w : c.Rel i i'
⊢ (dNext i : (a : (i j : ι) → C.X i ⟶ D.X j) → C.X i ⟶ D.X i) f = C.d i i' ≫ f i' i
have obtain : ∀ (w : c.Rel i (c.next i)),
  (dNext i : (a : (i j : ι) → C.X i ⟶ D.X j) → C.X i ⟶ D.X i) f =
    CategoryStruct.comp (Y := C.X (c.next i)) (C.d i (c.next i)) (f (c.next i) i)
Tactic: obtain rfl := c.next_eq' w
Cleared hypotheses: i', w
-- Lean 4 proof step from Mathlib.Algebra.Homology.Homotopy (goal)
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
c : ComplexShape ι
C D : HomologicalComplex.{v, u, u_1} V c
f : (i j : ι) → C.X i ⟶ D.X j
i : ι
hi : ¬c.Rel i (c.next i)
⊢ Eq.{v + 1} (α := C.X i ⟶ D.X i) ((dNext i : (a : (i j : ι) → C.X i ⟶ D.X j) → C.X i ⟶ D.X i) f : C.X i ⟶ D.X i)
    (0 : C.X i ⟶ D.X i)
have dsimp : CategoryStruct.comp (Y := C.X (c.next i)) (C.d i (c.next i)) (f (c.next i) i) = 0
Tactic: dsimp [dNext]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Homotopy (goal)
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
c : ComplexShape ι
C D : HomologicalComplex.{v, u, u_1} V c
f : (i j : ι) → C.X i ⟶ D.X j
i : ι
hi : ¬c.Rel i (c.next i)
⊢ CategoryStruct.comp (Y := C.X (c.next i)) (C.d i (c.next i)) (f (c.next i) i) = 0
have rw : Eq.{v + 1} (α := C.X i ⟶ D.X i) (CategoryStruct.comp (Y := C.X (c.next i)) 0 (f (c.next i) i)) 0
Tactic: rw [shape _ _ _ hi, zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Homotopy (goal)
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
c : ComplexShape ι
C D : HomologicalComplex.{v, u, u_1} V c
f : (i j : ι) → C.X i ⟶ D.X j
i : ι
hi : ¬c.Rel i (c.next i)
rw : Eq.{v + 1} (α := C.X i ⟶ D.X i) (CategoryStruct.comp (Y := C.X (c.next i)) 0 (f (c.next i) i)) 0
⊢ CategoryStruct.comp (Y := C.X (c.next i)) (C.d i (c.next i)) (f (c.next i) i) = 0
have rw₁ : Eq.{v + 1} (α := C.X i ⟶ D.X i) 0 0
Tactic: rw [shape _ _ _ hi, zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Homotopy (goal)
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
c : ComplexShape ι
C D : HomologicalComplex.{v, u, u_1} V c
f : (i j : ι) → C.X i ⟶ D.X j
i : ι
hi : ¬c.Rel (c.prev i) i
⊢ Eq.{v + 1} (α := C.X i ⟶ D.X i) ((prevD i : (a : (i j : ι) → C.X i ⟶ D.X j) → C.X i ⟶ D.X i) f : C.X i ⟶ D.X i)
    (0 : C.X i ⟶ D.X i)
have dsimp : CategoryStruct.comp (Y := D.X (c.prev i)) (f i (c.prev i)) (D.d (c.prev i) i) = 0
Tactic: dsimp [prevD]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Homotopy (goal)
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
c : ComplexShape ι
C D : HomologicalComplex.{v, u, u_1} V c
f : (i j : ι) → C.X i ⟶ D.X j
i : ι
hi : ¬c.Rel (c.prev i) i
⊢ CategoryStruct.comp (Y := D.X (c.prev i)) (f i (c.prev i)) (D.d (c.prev i) i) = 0
have rw : Eq.{v + 1} (α := C.X i ⟶ D.X i) (CategoryStruct.comp (Y := D.X (c.prev i)) (f i (c.prev i)) 0) 0
Tactic: rw [shape _ _ _ hi, comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Homotopy (goal)
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
c : ComplexShape ι
C D : HomologicalComplex.{v, u, u_1} V c
f : (i j : ι) → C.X i ⟶ D.X j
i : ι
hi : ¬c.Rel (c.prev i) i
rw : Eq.{v + 1} (α := C.X i ⟶ D.X i) (CategoryStruct.comp (Y := D.X (c.prev i)) (f i (c.prev i)) 0) 0
⊢ CategoryStruct.comp (Y := D.X (c.prev i)) (f i (c.prev i)) (D.d (c.prev i) i) = 0
have rw₁ : Eq.{v + 1} (α := C.X i ⟶ D.X i) 0 0
Tactic: rw [shape _ _ _ hi, comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Homotopy (goal)
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
c : ComplexShape ι
C D : HomologicalComplex.{v, u, u_1} V c
f : (i j : ι) → C.X i ⟶ D.X j
j j' : ι
w : c.Rel j' j
⊢ (prevD j : (a : (i j : ι) → C.X i ⟶ D.X j) → C.X j ⟶ D.X j) f = f j j' ≫ D.d j' j
have obtain : ∀ (w : c.Rel (c.prev j) j),
  (prevD j : (a : (i j : ι) → C.X i ⟶ D.X j) → C.X j ⟶ D.X j) f =
    CategoryStruct.comp (Y := D.X (c.prev j)) (f j (c.prev j)) (D.d (c.prev j) j)
Tactic: obtain rfl := c.prev_eq' w
Cleared hypotheses: j', w
-- Lean 4 proof step from Mathlib.Algebra.Homology.Homotopy (goal)
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
c : ComplexShape ι
C D E : HomologicalComplex.{v, u, u_1} V c
f : (i j : ι) → C.X i ⟶ D.X j
g : D ⟶ E
j : ι
⊢ Eq.{v + 1} (α := C.X j ⟶ E.X j)
    ((prevD j : (a : (i j : ι) → C.X i ⟶ E.X j) → C.X j ⟶ E.X j) fun (i j : ι) ↦ f i j ≫ g.f j : C.X j ⟶ E.X j)
    ((prevD j : (a : (i j : ι) → C.X i ⟶ D.X j) → C.X j ⟶ D.X j) f ≫ g.f j : C.X j ⟶ E.X j)
have dsimp : CategoryStruct.comp (Y := E.X (c.prev j)) (f j (c.prev j) ≫ g.f (c.prev j)) (E.d (c.prev j) j) =
  CategoryStruct.comp (Y := D.X (c.prev j)) (f j (c.prev j)) (D.d (c.prev j) j) ≫ g.f j
Tactic: dsimp [prevD]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Homotopy (goal)
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
C D : ChainComplex.{v, u, 0} V ℕ
i : ℕ
f : (i j : ℕ) → C.X i ⟶ D.X j
⊢ (dNext i : (a : (i j : ℕ) → C.X i ⟶ D.X j) → C.X i ⟶ D.X i) f =
    CategoryStruct.comp (Y := C.X (i - 1)) (C.d i (i - 1)) (f (i - 1) i)
have dsimp : CategoryStruct.comp (Y := C.X ((ComplexShape.down ℕ).next i)) (C.d i ((ComplexShape.down ℕ).next i))
    (f ((ComplexShape.down ℕ).next i) i) =
  CategoryStruct.comp (Y := C.X (i - 1)) (C.d i (i - 1)) (f (i - 1) i)
Tactic: dsimp [dNext]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Homotopy (goal)
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
C D : ChainComplex.{v, u, 0} V ℕ
i : ℕ
f : (i j : ℕ) → C.X i ⟶ D.X j
⊢ CategoryStruct.comp (Y := C.X ((ComplexShape.down ℕ).next i)) (C.d i ((ComplexShape.down ℕ).next i))
      (f ((ComplexShape.down ℕ).next i) i) =
    CategoryStruct.comp (Y := C.X (i - 1)) (C.d i (i - 1)) (f (i - 1) i)
have zero : Eq (α := C.X 0 ⟶ D.X 0)
  (CategoryStruct.comp (Y := C.X ((ComplexShape.down ℕ).next 0)) (C.d 0 ((ComplexShape.down ℕ).next 0))
    (f ((ComplexShape.down ℕ).next 0) 0))
  (CategoryStruct.comp (Y := C.X (HSub.hSub (α := ℕ) 0 1)) (C.d 0 (HSub.hSub (α := ℕ) 0 1))
    (f (HSub.hSub (α := ℕ) 0 1) 0))
Tactic: cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Algebra.Homology.Homotopy (goal)
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
C D : ChainComplex.{v, u, 0} V ℕ
i : ℕ
f : (i j : ℕ) → C.X i ⟶ D.X j
zero :
  Eq (α := C.X 0 ⟶ D.X 0)
    (CategoryStruct.comp (Y := C.X ((ComplexShape.down ℕ).next 0)) (C.d 0 ((ComplexShape.down ℕ).next 0))
      (f ((ComplexShape.down ℕ).next 0) 0))
    (CategoryStruct.comp (Y := C.X (HSub.hSub (α := ℕ) 0 1)) (C.d 0 (HSub.hSub (α := ℕ) 0 1))
      (f (HSub.hSub (α := ℕ) 0 1) 0))
⊢ CategoryStruct.comp (Y := C.X ((ComplexShape.down ℕ).next i)) (C.d i ((ComplexShape.down ℕ).next i))
      (f ((ComplexShape.down ℕ).next i) i) =
    CategoryStruct.comp (Y := C.X (i - 1)) (C.d i (i - 1)) (f (i - 1) i)
have succ : ∀ (n : ℕ),
  Eq (α := C.X (n + 1) ⟶ D.X (n + 1))
    (CategoryStruct.comp (Y := C.X ((ComplexShape.down ℕ).next (n + 1)))
      (C.d (n + 1) ((ComplexShape.down ℕ).next (n + 1))) (f ((ComplexShape.down ℕ).next (n + 1)) (n + 1)))
    (CategoryStruct.comp (Y := C.X (n + 1 - 1)) (C.d (n + 1) (n + 1 - 1)) (f (n + 1 - 1) (n + 1)))
Tactic: cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Algebra.Homology.Homotopy (goal)
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
C D : ChainComplex.{v, u, 0} V ℕ
f : (i j : ℕ) → C.X i ⟶ D.X j
n : ℕ
⊢ Eq (α := C.X (n + 1) ⟶ D.X (n + 1))
    (CategoryStruct.comp (Y := C.X ((ComplexShape.down ℕ).next (n + 1)))
      (C.d (n + 1) ((ComplexShape.down ℕ).next (n + 1))) (f ((ComplexShape.down ℕ).next (n + 1)) (n + 1)))
    (CategoryStruct.comp (Y := C.X (n + 1 - 1)) (C.d (n + 1) (n + 1 - 1)) (f (n + 1 - 1) (n + 1)))
have succ : (ComplexShape.down ℕ).next (n + 1) = n + 1 - 1
Tactic: congr
-- Lean 4 proof step from Mathlib.Algebra.Homology.Homotopy (goal)
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
C D : CochainComplex.{v, u, 0} V ℕ
i : ℕ
f : (i j : ℕ) → C.X i ⟶ D.X j
⊢ (prevD i : (a : (i j : ℕ) → C.X i ⟶ D.X j) → C.X i ⟶ D.X i) f =
    CategoryStruct.comp (Y := D.X (i - 1)) (f i (i - 1)) (D.d (i - 1) i)
have dsimp : CategoryStruct.comp (Y := D.X ((ComplexShape.up ℕ).prev i)) (f i ((ComplexShape.up ℕ).prev i))
    (D.d ((ComplexShape.up ℕ).prev i) i) =
  CategoryStruct.comp (Y := D.X (i - 1)) (f i (i - 1)) (D.d (i - 1) i)
Tactic: dsimp [prevD]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Homotopy (goal)
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
C D : CochainComplex.{v, u, 0} V ℕ
i : ℕ
f : (i j : ℕ) → C.X i ⟶ D.X j
⊢ CategoryStruct.comp (Y := D.X ((ComplexShape.up ℕ).prev i)) (f i ((ComplexShape.up ℕ).prev i))
      (D.d ((ComplexShape.up ℕ).prev i) i) =
    CategoryStruct.comp (Y := D.X (i - 1)) (f i (i - 1)) (D.d (i - 1) i)
have zero : Eq (α := C.X 0 ⟶ D.X 0)
  (CategoryStruct.comp (Y := D.X ((ComplexShape.up ℕ).prev 0)) (f 0 ((ComplexShape.up ℕ).prev 0))
    (D.d ((ComplexShape.up ℕ).prev 0) 0))
  (CategoryStruct.comp (Y := D.X (HSub.hSub (α := ℕ) 0 1)) (f 0 (HSub.hSub (α := ℕ) 0 1))
    (D.d (HSub.hSub (α := ℕ) 0 1) 0))
Tactic: cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Algebra.Homology.Homotopy (goal)
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
C D : CochainComplex.{v, u, 0} V ℕ
i : ℕ
f : (i j : ℕ) → C.X i ⟶ D.X j
zero :
  Eq (α := C.X 0 ⟶ D.X 0)
    (CategoryStruct.comp (Y := D.X ((ComplexShape.up ℕ).prev 0)) (f 0 ((ComplexShape.up ℕ).prev 0))
      (D.d ((ComplexShape.up ℕ).prev 0) 0))
    (CategoryStruct.comp (Y := D.X (HSub.hSub (α := ℕ) 0 1)) (f 0 (HSub.hSub (α := ℕ) 0 1))
      (D.d (HSub.hSub (α := ℕ) 0 1) 0))
⊢ CategoryStruct.comp (Y := D.X ((ComplexShape.up ℕ).prev i)) (f i ((ComplexShape.up ℕ).prev i))
      (D.d ((ComplexShape.up ℕ).prev i) i) =
    CategoryStruct.comp (Y := D.X (i - 1)) (f i (i - 1)) (D.d (i - 1) i)
have succ : ∀ (n : ℕ),
  Eq (α := C.X (n + 1) ⟶ D.X (n + 1))
    (CategoryStruct.comp (Y := D.X ((ComplexShape.up ℕ).prev (n + 1))) (f (n + 1) ((ComplexShape.up ℕ).prev (n + 1)))
      (D.d ((ComplexShape.up ℕ).prev (n + 1)) (n + 1)))
    (CategoryStruct.comp (Y := D.X (n + 1 - 1)) (f (n + 1) (n + 1 - 1)) (D.d (n + 1 - 1) (n + 1)))
Tactic: cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Algebra.Homology.Homotopy (goal)
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
C D : CochainComplex.{v, u, 0} V ℕ
f : (i j : ℕ) → C.X i ⟶ D.X j
n : ℕ
⊢ Eq (α := C.X (n + 1) ⟶ D.X (n + 1))
    (CategoryStruct.comp (Y := D.X ((ComplexShape.up ℕ).prev (n + 1))) (f (n + 1) ((ComplexShape.up ℕ).prev (n + 1)))
      (D.d ((ComplexShape.up ℕ).prev (n + 1)) (n + 1)))
    (CategoryStruct.comp (Y := D.X (n + 1 - 1)) (f (n + 1) (n + 1 - 1)) (D.d (n + 1 - 1) (n + 1)))
have succ : (ComplexShape.up ℕ).prev (n + 1) = n + 1 - 1
Tactic: congr