awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.Additive (goal)
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
W : Type u_2
inst_2 : Category.{v_1, u_2} W
inst_3 : Preadditive.{v_1, u_2} W
W₁ : Type u_3
W₂ : Type u_4
inst_4 : Category.{v_2, u_3} W₁
inst_5 : Category.{v_3, u_4} W₂
inst_6 : HasZeroMorphisms.{v_2, u_3} W₁
inst_7 : HasZeroMorphisms.{v_3, u_4} W₂
c_1 : ComplexShape ι
C D : HomologicalComplex.{v, u, u_1} V c_1
f_1 : C ⟶ D
i_1 : ι
inst_8 : HasZeroObject.{v_2, u_3} W₁
inst_9 : HasZeroObject.{v_3, u_4} W₂
F : CategoryTheory.Functor.{v_2, v_3, u_3, u_4} W₁ W₂
inst_10 : F.PreservesZeroMorphisms
c : ComplexShape ι
inst_11 : DecidableEq ι
j : ι
X Y : W₁
f : X ⟶ Y
i : ι
h : i = j
⊢ Eq (α :=
    F.obj (HomologicalComplex.X.{v_2, u_3, u_1} (Functor.obj (single W₁ c j) X) i) ⟶
      HomologicalComplex.X.{v_3, u_4, u_1} (Functor.obj (single W₂ c j) (F.obj Y)) i)
    (F.map (Hom.f (CategoryTheory.Functor.map (single W₁ c j) f) i) ≫ eqToHom ⋯)
    (CategoryStruct.comp (Y := HomologicalComplex.X.{v_3, u_4, u_1} (Functor.obj (single W₂ c j) (F.obj X)) i)
      (eqToHom ⋯) (Hom.f (CategoryTheory.Functor.map (single W₂ c j) (F.map f)) i))
have pos : Eq (α :=
  F.obj (HomologicalComplex.X.{v_2, u_3, u_1} (Functor.obj (single W₁ c i) X) i) ⟶
    HomologicalComplex.X.{v_3, u_4, u_1} (Functor.obj (single W₂ c i) (F.obj Y)) i)
  (F.map (Hom.f (CategoryTheory.Functor.map (single W₁ c i) f) i) ≫ eqToHom sorry)
  (CategoryStruct.comp (Y := HomologicalComplex.X.{v_3, u_4, u_1} (Functor.obj (single W₂ c i) (F.obj X)) i) (eqToHom sorry)
    (Hom.f (CategoryTheory.Functor.map (single W₂ c i) (F.map f)) i))
Tactic: subst h
Cleared hypotheses: j, h
-- Lean 4 proof step from Mathlib.Algebra.Homology.AlternatingConst (goal)
Goal:
i j : ℕ
h : (up ℕ).Rel i j
⊢ Odd (i + j)
have subst : Odd (i + (i + 1))
Tactic: subst h
Cleared hypotheses: j, h
-- Lean 4 proof step from Mathlib.Algebra.Homology.AlternatingConst (goal)
Goal:
i j : ℕ
h : (down ℕ).Rel i j
⊢ Odd (i + j)
have subst : Odd (j + 1 + j)
Tactic: subst h
Cleared hypotheses: i, h
-- Lean 4 proof step from Mathlib.Algebra.Homology.AlternatingConst (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
A : C
φ ψ : A ⟶ A
hOdd : φ ≫ ψ = 0
hEven : ψ ≫ φ = 0
c : ComplexShape ℕ
inst_2 : DecidableRel c.Rel
hc : ∀ (i j : ℕ), c.Rel i j → Odd (i + j)
i j k : ℕ
hij : c.Rel i j
hjk : c.Rel j k
⊢ Eq.{v_1 + 1} (α := A ⟶ A)
    (CategoryStruct.comp (Y := A) (if hij : c.Rel i j then if hi : Even i then φ else ψ else 0)
      (if hij : c.Rel j k then if hi : Even j then φ else ψ else 0))
    0
have this : Odd (i + j)
Tactic: have := hc i j hij
-- Lean 4 proof step from Mathlib.Algebra.Homology.AlternatingConst (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
A : C
φ ψ : A ⟶ A
hOdd : φ ≫ ψ = 0
hEven : ψ ≫ φ = 0
c : ComplexShape ℕ
inst_2 : DecidableRel c.Rel
hc : ∀ (i j : ℕ), c.Rel i j → Odd (i + j)
i j k : ℕ
hij : c.Rel i j
hjk : c.Rel j k
this : Odd (i + j)
⊢ Eq.{v_1 + 1} (α := A ⟶ A)
    (CategoryStruct.comp (Y := A) (if hij : c.Rel i j then if hi : Even i then φ else ψ else 0)
      (if hij : c.Rel j k then if hi : Even j then φ else ψ else 0))
    0
have pos : ∀ (hi : Even i) (hj : Even j), φ ≫ φ = 0
Tactic: split_ifs with hi hj hj
-- Lean 4 proof step from Mathlib.Algebra.Homology.AlternatingConst (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
A : C
φ ψ : A ⟶ A
hOdd : φ ≫ ψ = 0
hEven : ψ ≫ φ = 0
c : ComplexShape ℕ
inst_2 : DecidableRel c.Rel
hc : ∀ (i j : ℕ), c.Rel i j → Odd (i + j)
i j k : ℕ
hij : c.Rel i j
hjk : c.Rel j k
this : Odd (i + j)
pos : ∀ (hi : Even i) (hj : Even j), φ ≫ φ = 0
⊢ Eq.{v_1 + 1} (α := A ⟶ A)
    (CategoryStruct.comp (Y := A) (if hij : c.Rel i j then if hi : Even i then φ else ψ else 0)
      (if hij : c.Rel j k then if hi : Even j then φ else ψ else 0))
    0
have neg : ∀ (hi : Even i) (hj : ¬Even j), φ ≫ ψ = 0
Tactic: split_ifs with hi hj hj
-- Lean 4 proof step from Mathlib.Algebra.Homology.AlternatingConst (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
A : C
φ ψ : A ⟶ A
hOdd : φ ≫ ψ = 0
hEven : ψ ≫ φ = 0
c : ComplexShape ℕ
inst_2 : DecidableRel c.Rel
hc : ∀ (i j : ℕ), c.Rel i j → Odd (i + j)
i j k : ℕ
hij : c.Rel i j
hjk : c.Rel j k
this : Odd (i + j)
pos : ∀ (hi : Even i) (hj : Even j), φ ≫ φ = 0
neg : ∀ (hi : Even i) (hj : ¬Even j), φ ≫ ψ = 0
⊢ Eq.{v_1 + 1} (α := A ⟶ A)
    (CategoryStruct.comp (Y := A) (if hij : c.Rel i j then if hi : Even i then φ else ψ else 0)
      (if hij : c.Rel j k then if hi : Even j then φ else ψ else 0))
    0
have pos₁ : ∀ (hi : ¬Even i) (hj : Even j), ψ ≫ φ = 0
Tactic: split_ifs with hi hj hj
-- Lean 4 proof step from Mathlib.Algebra.Homology.AlternatingConst (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
A : C
φ ψ : A ⟶ A
hOdd : φ ≫ ψ = 0
hEven : ψ ≫ φ = 0
c : ComplexShape ℕ
inst_2 : DecidableRel c.Rel
hc : ∀ (i j : ℕ), c.Rel i j → Odd (i + j)
i j k : ℕ
hij : c.Rel i j
hjk : c.Rel j k
this : Odd (i + j)
pos : ∀ (hi : Even i) (hj : Even j), φ ≫ φ = 0
neg : ∀ (hi : Even i) (hj : ¬Even j), φ ≫ ψ = 0
pos₁ : ∀ (hi : ¬Even i) (hj : Even j), ψ ≫ φ = 0
⊢ Eq.{v_1 + 1} (α := A ⟶ A)
    (CategoryStruct.comp (Y := A) (if hij : c.Rel i j then if hi : Even i then φ else ψ else 0)
      (if hij : c.Rel j k then if hi : Even j then φ else ψ else 0))
    0
have neg₁ : ∀ (hi : ¬Even i) (hj : ¬Even j), ψ ≫ ψ = 0
Tactic: split_ifs with hi hj hj
-- Lean 4 proof step from Mathlib.Algebra.Homology.AlternatingConst (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
A : C
φ ψ : A ⟶ A
hOdd : φ ≫ ψ = 0
hEven : ψ ≫ φ = 0
c : ComplexShape ℕ
inst_2 : DecidableRel c.Rel
hc : ∀ (i j : ℕ), c.Rel i j → Odd (i + j)
i j k : ℕ
hij : c.Rel i j
hjk : c.Rel j k
h : Even j
⊢ Iso.hom (Iso.refl ((alternatingConst A hOdd hEven hc).sc' i j k).X₁) ≫
      { X₁ := A, X₂ := A, X₃ := A, f := ψ, g := φ, zero := hEven : ShortComplex.{v_1, u_1} C }.f =
    ((alternatingConst A hOdd hEven hc).sc' i j k).f ≫
      Iso.hom (Iso.refl ((alternatingConst A hOdd hEven hc).sc' i j k).X₂)
have simp_all : Even i → ψ = φ
Tactic: simp_all only [alternatingConst, dite_eq_ite, Iso.refl_hom, Category.id_comp,
        shortComplexFunctor'_obj_f, ↓reduceIte, Category.comp_id, right_eq_ite_iff]
-- Lean 4 proof step from Mathlib.Algebra.Homology.AlternatingConst (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
A : C
φ ψ : A ⟶ A
hOdd : φ ≫ ψ = 0
hEven : ψ ≫ φ = 0
c : ComplexShape ℕ
inst_2 : DecidableRel c.Rel
hc : ∀ (i j : ℕ), c.Rel i j → Odd (i + j)
i j k : ℕ
hij : c.Rel i j
hjk : c.Rel j k
h : Even j
hi : Even i
⊢ ψ = φ
have this : Odd (i + j)
Tactic: have := hc i j hij
-- Lean 4 proof step from Mathlib.Algebra.Homology.AlternatingConst (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
A : C
φ ψ : A ⟶ A
hOdd : φ ≫ ψ = 0
hEven : ψ ≫ φ = 0
c : ComplexShape ℕ
inst_2 : DecidableRel c.Rel
hc : ∀ (i j : ℕ), c.Rel i j → Odd (i + j)
i j k : ℕ
hij : c.Rel i j
hjk : c.Rel j k
h : Odd j
⊢ Iso.hom (Iso.refl ((alternatingConst A hOdd hEven hc).sc' i j k).X₁) ≫
      { X₁ := A, X₂ := A, X₃ := A, f := φ, g := ψ, zero := hOdd : ShortComplex.{v_1, u_1} C }.f =
    ((alternatingConst A hOdd hEven hc).sc' i j k).f ≫
      Iso.hom (Iso.refl ((alternatingConst A hOdd hEven hc).sc' i j k).X₂)
have simp_all : ¬Even i → φ = ψ
Tactic: simp_all only [alternatingConst, dite_eq_ite, Iso.refl_hom, Category.id_comp,
        shortComplexFunctor'_obj_f, ↓reduceIte, Category.comp_id, left_eq_ite_iff]
-- Lean 4 proof step from Mathlib.Algebra.Homology.AlternatingConst (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
A : C
φ ψ : A ⟶ A
hOdd : φ ≫ ψ = 0
hEven : ψ ≫ φ = 0
c : ComplexShape ℕ
inst_2 : DecidableRel c.Rel
hc : ∀ (i j : ℕ), c.Rel i j → Odd (i + j)
i j k : ℕ
hij : c.Rel i j
hjk : c.Rel j k
h : Odd j
hi : ¬Even i
⊢ φ = ψ
have this : Odd (i + j)
Tactic: have := hc i j hij
-- Lean 4 proof step from Mathlib.Algebra.Homology.AlternatingConst (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
A : C
φ ψ : A ⟶ A
hOdd : φ ≫ ψ = 0
hEven : ψ ≫ φ = 0
c : ComplexShape ℕ
inst_2 : DecidableRel c.Rel
hc : ∀ (i j : ℕ), c.Rel i j → Odd (i + j)
inst_3 : CategoryWithHomology.{v_1, u_1} C
j : ℕ
hpj : c.Rel (c.prev j) j
hnj : c.Rel j (c.next j)
h : Even j
⊢ Eq (α := (alternatingConst A hOdd hEven hc).cycles j ⟶ A) ((alternatingConst A hOdd hEven hc).iCycles j ≫ φ) 0
have rw : Eq (α := { X₁ := A, X₂ := A, X₃ := A, f := ψ, g := φ, zero := hEven : ShortComplex.{v_1, u_1} C }.cycles ⟶ A)
  (CategoryStruct.comp (Y := ((alternatingConst A hOdd hEven hc).sc' (c.prev j) j (c.next j)).cycles)
    (Iso.inv (ShortComplex.cyclesMapIso (alternatingConstScIsoEven A hOdd hEven hc hpj hnj h)) :
      { X₁ := A, X₂ := A, X₃ := A, f := ψ, g := φ, zero := hEven : ShortComplex.{v_1, u_1} C }.cycles ⟶
        ((alternatingConst A hOdd hEven hc).sc' (c.prev j) j (c.next j)).cycles)
    ((alternatingConst A hOdd hEven hc).iCycles j ≫ φ : (alternatingConst A hOdd hEven hc).cycles j ⟶ A))
  (CategoryStruct.comp (Y := ((alternatingConst A hOdd hEven hc).sc' (c.prev j) j (c.next j)).cycles)
    (Iso.inv (ShortComplex.cyclesMapIso (alternatingConstScIsoEven A hOdd hEven hc hpj hnj h))) 0)
Tactic: rw [← cancel_epi (ShortComplex.cyclesMapIso
    (alternatingConstScIsoEven A hOdd hEven hc hpj hnj h)).inv]
-- Lean 4 proof step from Mathlib.Algebra.Homology.AlternatingConst (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
A : C
φ ψ : A ⟶ A
hOdd : φ ≫ ψ = 0
hEven : ψ ≫ φ = 0
c : ComplexShape ℕ
inst_2 : DecidableRel c.Rel
hc : ∀ (i j : ℕ), c.Rel i j → Odd (i + j)
inst_3 : CategoryWithHomology.{v_1, u_1} C
j : ℕ
hpj : c.Rel (c.prev j) j
hnj : c.Rel j (c.next j)
h : Odd j
⊢ Eq (α := (alternatingConst A hOdd hEven hc).cycles j ⟶ A) ((alternatingConst A hOdd hEven hc).iCycles j ≫ ψ) 0
have rw : Eq (α := { X₁ := A, X₂ := A, X₃ := A, f := φ, g := ψ, zero := hOdd : ShortComplex.{v_1, u_1} C }.cycles ⟶ A)
  (CategoryStruct.comp (Y := ((alternatingConst A hOdd hEven hc).sc' (c.prev j) j (c.next j)).cycles)
    (Iso.inv (ShortComplex.cyclesMapIso (alternatingConstScIsoOdd A hOdd hEven hc hpj hnj h)) :
      { X₁ := A, X₂ := A, X₃ := A, f := φ, g := ψ, zero := hOdd : ShortComplex.{v_1, u_1} C }.cycles ⟶
        ((alternatingConst A hOdd hEven hc).sc' (c.prev j) j (c.next j)).cycles)
    ((alternatingConst A hOdd hEven hc).iCycles j ≫ ψ : (alternatingConst A hOdd hEven hc).cycles j ⟶ A))
  (CategoryStruct.comp (Y := ((alternatingConst A hOdd hEven hc).sc' (c.prev j) j (c.next j)).cycles)
    (Iso.inv (ShortComplex.cyclesMapIso (alternatingConstScIsoOdd A hOdd hEven hc hpj hnj h))) 0)
Tactic: rw [← cancel_epi (ShortComplex.cyclesMapIso
    (alternatingConstScIsoOdd A hOdd hEven hc hpj hnj h)).inv]
-- Lean 4 proof step from Mathlib.Algebra.Homology.AlternatingConst (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
X Y : C
f : X ⟶ Y
i j : ℕ
hij : (ComplexShape.down ℕ).Rel i j
⊢ Eq (α :=
    HomologicalComplex.X.{v_1, u_1, 0} (c := ComplexShape.down ℕ) (HomologicalComplex.alternatingConst X ⋯ ⋯ ⋯) i ⟶
      HomologicalComplex.X.{v_1, u_1, 0} (c := ComplexShape.down ℕ) (HomologicalComplex.alternatingConst Y ⋯ ⋯ ⋯) j)
    (f ≫ HomologicalComplex.d (HomologicalComplex.alternatingConst Y ⋯ ⋯ ⋯) i j)
    (HomologicalComplex.d (HomologicalComplex.alternatingConst X ⋯ ⋯ ⋯) i j ≫ f)
have pos : Even i →
  Eq (α :=
    HomologicalComplex.X.{v_1, u_1, 0} (c := ComplexShape.down ℕ) (HomologicalComplex.alternatingConst X sorry sorry sorry) i ⟶
      HomologicalComplex.X.{v_1, u_1, 0} (c := ComplexShape.down ℕ) (HomologicalComplex.alternatingConst Y sorry sorry sorry) j)
    (f ≫ HomologicalComplex.d (HomologicalComplex.alternatingConst Y sorry sorry sorry) i j)
    (HomologicalComplex.d (HomologicalComplex.alternatingConst X sorry sorry sorry) i j ≫ f)
Tactic: by_cases Even i
-- Lean 4 proof step from Mathlib.Algebra.Homology.AlternatingConst (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
X Y : C
f : X ⟶ Y
i j : ℕ
hij : (ComplexShape.down ℕ).Rel i j
pos :
  Even i →
    Eq (α :=
      HomologicalComplex.X.{v_1, u_1, 0} (c := ComplexShape.down ℕ) (HomologicalComplex.alternatingConst X ⋯ ⋯ ⋯) i ⟶
        HomologicalComplex.X.{v_1, u_1, 0} (c := ComplexShape.down ℕ) (HomologicalComplex.alternatingConst Y ⋯ ⋯ ⋯) j)
      (f ≫ HomologicalComplex.d (HomologicalComplex.alternatingConst Y ⋯ ⋯ ⋯) i j)
      (HomologicalComplex.d (HomologicalComplex.alternatingConst X ⋯ ⋯ ⋯) i j ≫ f)
⊢ Eq (α :=
    HomologicalComplex.X.{v_1, u_1, 0} (c := ComplexShape.down ℕ) (HomologicalComplex.alternatingConst X ⋯ ⋯ ⋯) i ⟶
      HomologicalComplex.X.{v_1, u_1, 0} (c := ComplexShape.down ℕ) (HomologicalComplex.alternatingConst Y ⋯ ⋯ ⋯) j)
    (f ≫ HomologicalComplex.d (HomologicalComplex.alternatingConst Y ⋯ ⋯ ⋯) i j)
    (HomologicalComplex.d (HomologicalComplex.alternatingConst X ⋯ ⋯ ⋯) i j ≫ f)
have neg : ¬Even i →
  Eq (α :=
    HomologicalComplex.X.{v_1, u_1, 0} (c := ComplexShape.down ℕ) (HomologicalComplex.alternatingConst X sorry sorry sorry) i ⟶
      HomologicalComplex.X.{v_1, u_1, 0} (c := ComplexShape.down ℕ) (HomologicalComplex.alternatingConst Y sorry sorry sorry) j)
    (f ≫ HomologicalComplex.d (HomologicalComplex.alternatingConst Y sorry sorry sorry) i j)
    (HomologicalComplex.d (HomologicalComplex.alternatingConst X sorry sorry sorry) i j ≫ f)
Tactic: by_cases Even i
-- Lean 4 proof step from Mathlib.Algebra.Homology.AlternatingConst (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
X : C
n : ℕ
hn : Even n
h₀ : n ≠ 0
⊢ ∀ (Z : C) (g : Z ⟶ ShortComplex.X₂.{v_1, u_1} (HomologicalComplex.sc (Functor.obj alternatingConst X) n)),
    g ≫ ShortComplex.g (HomologicalComplex.sc (Functor.obj alternatingConst X) n) = 0 → g = 0
have zero : ∀ (hn : Even (α := ℕ) 0) (h₀ : Ne (α := ℕ) 0 0) (Z : C)
  (g : Z ⟶ ShortComplex.X₂.{v_1, u_1} (HomologicalComplex.sc (Functor.obj alternatingConst X) 0)),
  g ≫ ShortComplex.g (HomologicalComplex.sc (Functor.obj alternatingConst X) 0) = 0 → g = 0
Tactic: cases n
Cleared hypotheses: n, hn, h₀
-- Lean 4 proof step from Mathlib.Algebra.Homology.AlternatingConst (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
X : C
n : ℕ
hn : Even n
h₀ : n ≠ 0
zero :
  ∀ (hn : Even (α := ℕ) 0) (h₀ : Ne (α := ℕ) 0 0) (Z : C)
    (g : Z ⟶ ShortComplex.X₂.{v_1, u_1} (HomologicalComplex.sc (Functor.obj alternatingConst X) 0)),
    g ≫ ShortComplex.g (HomologicalComplex.sc (Functor.obj alternatingConst X) 0) = 0 → g = 0
⊢ ∀ (Z : C) (g : Z ⟶ ShortComplex.X₂.{v_1, u_1} (HomologicalComplex.sc (Functor.obj alternatingConst X) n)),
    g ≫ ShortComplex.g (HomologicalComplex.sc (Functor.obj alternatingConst X) n) = 0 → g = 0
have succ : ∀ (n : ℕ) (hn : Even (n + 1)) (h₀ : n + 1 ≠ 0) (Z : C)
  (g : Z ⟶ ShortComplex.X₂.{v_1, u_1} (HomologicalComplex.sc (Functor.obj alternatingConst X) (n + 1))),
  g ≫ ShortComplex.g (HomologicalComplex.sc (Functor.obj alternatingConst X) (n + 1)) = 0 → g = 0
Tactic: cases n
Cleared hypotheses: n, hn, h₀
-- Lean 4 proof step from Mathlib.Algebra.Homology.AlternatingConst (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
X : C
n : ℕ
⊢ HomologicalComplex.HasHomology.{v_1, u_1, 0} (Functor.obj alternatingConst X) n
have inl : ∀ (h : Even n), HomologicalComplex.HasHomology.{v_1, u_1, 0} (Functor.obj alternatingConst X) n
Tactic: rcases n.even_or_odd with h | h
-- Lean 4 proof step from Mathlib.Algebra.Homology.AlternatingConst (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
X : C
n : ℕ
inl : ∀ (h : Even n), HomologicalComplex.HasHomology.{v_1, u_1, 0} (Functor.obj alternatingConst X) n
⊢ HomologicalComplex.HasHomology.{v_1, u_1, 0} (Functor.obj alternatingConst X) n
have inr : ∀ (h : Odd n), HomologicalComplex.HasHomology.{v_1, u_1, 0} (Functor.obj alternatingConst X) n
Tactic: rcases n.even_or_odd with h | h
-- Lean 4 proof step from Mathlib.Algebra.Homology.AlternatingConst (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
X : C
n : ℕ
h : Even n
⊢ HomologicalComplex.HasHomology.{v_1, u_1, 0} (Functor.obj alternatingConst X) n
have inl : ∀ (h : Even (α := ℕ) 0), HomologicalComplex.HasHomology.{v_1, u_1, 0} (Functor.obj alternatingConst X) 0
Tactic: rcases n with - | n
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.Algebra.Homology.AlternatingConst (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
X : C
n : ℕ
h : Even n
inl : ∀ (h : Even (α := ℕ) 0), HomologicalComplex.HasHomology.{v_1, u_1, 0} (Functor.obj alternatingConst X) 0
⊢ HomologicalComplex.HasHomology.{v_1, u_1, 0} (Functor.obj alternatingConst X) n
have inl₁ : ∀ (n : ℕ) (h : Even (n + 1)), HomologicalComplex.HasHomology.{v_1, u_1, 0} (Functor.obj alternatingConst X) (n + 1)
Tactic: rcases n with - | n
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.Algebra.Homology.AlternatingConst (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
X : C
n : ℕ
hn : n ≠ 0
⊢ HomologicalComplex.ExactAt.{v_1, u_1, 0} (Functor.obj alternatingConst X) n
have inl : ∀ (h : Even n), HomologicalComplex.ExactAt.{v_1, u_1, 0} (Functor.obj alternatingConst X) n
Tactic: rcases n.even_or_odd with h | h
-- Lean 4 proof step from Mathlib.Algebra.Homology.AlternatingConst (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
X : C
n : ℕ
hn : n ≠ 0
inl : ∀ (h : Even n), HomologicalComplex.ExactAt.{v_1, u_1, 0} (Functor.obj alternatingConst X) n
⊢ HomologicalComplex.ExactAt.{v_1, u_1, 0} (Functor.obj alternatingConst X) n
have inr : ∀ (h : Odd n), HomologicalComplex.ExactAt.{v_1, u_1, 0} (Functor.obj alternatingConst X) n
Tactic: rcases n.even_or_odd with h | h
-- Lean 4 proof step from Mathlib.Algebra.Homology.Augment (goal)
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
C : ChainComplex.{v, u, 0} V ℕ
X : V
f : C.X 0 ⟶ X
w : Eq (α := C.X 1 ⟶ X) (C.d 1 0 ≫ f) 0
i j : ℕ
h : ¬(ComplexShape.down ℕ).Rel (i + 1) (j + 1)
⊢ Eq.{v + 1} (α :=
    Quiver.Hom.{v, u} (V := V)
      (match (motive := ℕ → V) i + 1 with
        | 0 => X
        | i.succ => C.X i :
        V)
      (match (motive := ℕ → V) j + 1 with
        | 0 => X
        | i.succ => C.X i :
        V))
    (match (motive :=
        (x x_1 : ℕ) →
          Quiver.Hom.{v, u} (V := V)
            (match (motive := ℕ → V) x with
              | 0 => X
              | i.succ => C.X i :
              V)
            (match (motive := ℕ → V) x_1 with
              | 0 => X
              | i.succ => C.X i :
              V))
        i + 1, j + 1 with
      | 1, 0 => f
      | i.succ, j.succ => C.d i j
      | x, x_1 => 0 :
      Quiver.Hom.{v, u} (V := V)
        (match (motive := ℕ → V) i + 1 with
          | 0 => X
          | i.succ => C.X i :
          V)
        (match (motive := ℕ → V) j + 1 with
          | 0 => X
          | i.succ => C.X i :
          V))
    (0 :
      Quiver.Hom.{v, u} (V := V)
        (match (motive := ℕ → V) i + 1 with
          | 0 => X
          | i.succ => C.X i :
          V)
        (match (motive := ℕ → V) j + 1 with
          | 0 => X
          | i.succ => C.X i :
          V))
have simp : C.d i j = 0
Tactic: simp only
-- Lean 4 proof step from Mathlib.Algebra.Homology.Augment (goal)
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
C : ChainComplex.{v, u, 0} V ℕ
X : V
f : C.X 0 ⟶ X
w : Eq (α := C.X 1 ⟶ X) (C.d 1 0 ≫ f) 0
i j : ℕ
⊢ (C.augment f w).d (i + 1) (j + 1) = C.d i j
have zero : Eq (α := (C.augment f w).X (HAdd.hAdd (α := ℕ) 0 1) ⟶ (C.augment f w).X (j + 1))
  ((C.augment f w).d (HAdd.hAdd (α := ℕ) 0 1) (j + 1)) (C.d 0 j)
Tactic: cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Algebra.Homology.Augment (goal)
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
C : ChainComplex.{v, u, 0} V ℕ
X : V
f : C.X 0 ⟶ X
w : Eq (α := C.X 1 ⟶ X) (C.d 1 0 ≫ f) 0
i j : ℕ
zero :
  Eq (α := (C.augment f w).X (HAdd.hAdd (α := ℕ) 0 1) ⟶ (C.augment f w).X (j + 1))
    ((C.augment f w).d (HAdd.hAdd (α := ℕ) 0 1) (j + 1)) (C.d 0 j)
⊢ (C.augment f w).d (i + 1) (j + 1) = C.d i j
have succ : ∀ (n : ℕ),
  Eq (α := (C.augment f w).X (n + 1 + 1) ⟶ (C.augment f w).X (j + 1)) ((C.augment f w).d (n + 1 + 1) (j + 1))
    (C.d (n + 1) j)
Tactic: cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Algebra.Homology.Augment (goal)
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
C : ChainComplex.{v, u, 0} V ℕ
i : ℕ
⊢ Eq (α := C.X (i + 2) ⟶ C.X 0) (C.d (i + 2) 0) 0
have a : ¬(ComplexShape.down ℕ).Rel (i + 2) 0
Tactic: rw [C.shape]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Augment (goal)
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
C : ChainComplex.{v, u, 0} V ℕ
i j : ℕ
⊢ (ComplexShape.down ℕ).Rel 0 j →
    Eq.{v + 1} (α := ((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) ⋯).X 0 ⟶ C.X j)
      (CategoryStruct.comp (Y := C.X 0)
          (match (motive := (x : ℕ) → ((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) ⋯).X x ⟶ C.X x) 0 with
          | 0 => 𝟙 (((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) ⋯).X 0)
          | n.succ => 𝟙 (((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) ⋯).X (n + 1)))
          (C.d 0 j) :
        ((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) ⋯).X 0 ⟶ C.X j)
      (((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) ⋯).d 0 j ≫
          match (motive := (x : ℕ) → ((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) ⋯).X x ⟶ C.X x) j with
          | 0 => 𝟙 (((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) ⋯).X 0)
          | n.succ => 𝟙 (((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) ⋯).X (n + 1)) :
        ((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) ⋯).X 0 ⟶ C.X j)
have zero : (ComplexShape.down ℕ).Rel 0 0 →
  Eq.{v + 1} (α := ((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) sorry).X 0 ⟶ C.X 0)
    (CategoryStruct.comp (Y := C.X 0)
        (match (motive := (x : ℕ) → ((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) sorry).X x ⟶ C.X x) 0 with
        | 0 => 𝟙 (((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) sorry).X 0)
        | n.succ => 𝟙 (((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) sorry).X (n + 1)))
        (C.d 0 0) :
      ((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) sorry).X 0 ⟶ C.X 0)
    (CategoryStruct.comp (Y := ((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) sorry).X 0)
        (((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) sorry).d 0 0)
        (match (motive := (x : ℕ) → ((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) sorry).X x ⟶ C.X x) 0 with
        | 0 => 𝟙 (((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) sorry).X 0)
        | n.succ => 𝟙 (((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) sorry).X (n + 1))) :
      ((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) sorry).X 0 ⟶ C.X 0)
Tactic: rcases j with - | j
Cleared hypotheses: j