awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplex (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
R : Type u_1
inst_2 : Ring R
inst_3 : Linear.{u_1, v, u} R C
F G K L : CochainComplex.{v, u, 0} C ℤ
n m : ℤ
φ₁ φ₂ : F ⟶ G
z : { z : Cochain F G (-1) // ofHom φ₁ = δ (-1) 0 z + ofHom φ₂ }
⊢ (fun (ho : Homotopy φ₁ φ₂) ↦
        (Subtype.mk (p := fun (z : Cochain F G (-1)) ↦ ofHom φ₁ = δ (-1) 0 z + ofHom φ₂) (ofHomotopy ho) ⋯ :
          { z : Cochain F G (-1) // ofHom φ₁ = δ (-1) 0 z + ofHom φ₂ }))
      ((fun (z : { z : Cochain F G (-1) // ofHom φ₁ = δ (-1) 0 z + ofHom φ₂ }) ↦
          ({ hom := fun (i j : ℤ) ↦ if hij : i + -1 = j then (↑z : Cochain F G (-1)).v i j hij else 0, zero := ⋯,
              comm := ⋯ } :
            Homotopy φ₁ φ₂))
        z) =
    z
have a : ∀ (p q : ℤ) (hpq : p + -1 = q),
  v
      (↑((fun (ho : Homotopy φ₁ φ₂) ↦
              (Subtype.mk (p := fun (z : Cochain F G (-1)) ↦ ofHom φ₁ = δ (-1) 0 z + ofHom φ₂) (ofHomotopy ho) sorry :
                { z : Cochain F G (-1) // ofHom φ₁ = δ (-1) 0 z + ofHom φ₂ }))
            ((fun (z : { z : Cochain F G (-1) // ofHom φ₁ = δ (-1) 0 z + ofHom φ₂ }) ↦
                ({ hom := fun (i j : ℤ) ↦ if hij : i + -1 = j then (↑z : Cochain F G (-1)).v i j hij else 0, zero := sorry,
                    comm := sorry } :
                  Homotopy φ₁ φ₂))
              z)) :
        Cochain F G (-1))
      p q hpq =
    (↑z : Cochain F G (-1)).v p q hpq
Tactic: ext p q hpq
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplex (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
R : Type u_1
inst_2 : Ring R
inst_3 : Linear.{u_1, v, u} R C
F G K L : CochainComplex.{v, u, 0} C ℤ
n m : ℤ
φ₁ φ₂ : F ⟶ G
z : { z : Cochain F G (-1) // ofHom φ₁ = δ (-1) 0 z + ofHom φ₂ }
p q : ℤ
hpq : p + -1 = q
⊢ v
      (↑((fun (ho : Homotopy φ₁ φ₂) ↦
              (Subtype.mk (p := fun (z : Cochain F G (-1)) ↦ ofHom φ₁ = δ (-1) 0 z + ofHom φ₂) (ofHomotopy ho) ⋯ :
                { z : Cochain F G (-1) // ofHom φ₁ = δ (-1) 0 z + ofHom φ₂ }))
            ((fun (z : { z : Cochain F G (-1) // ofHom φ₁ = δ (-1) 0 z + ofHom φ₂ }) ↦
                ({ hom := fun (i j : ℤ) ↦ if hij : i + -1 = j then (↑z : Cochain F G (-1)).v i j hij else 0, zero := ⋯,
                    comm := ⋯ } :
                  Homotopy φ₁ φ₂))
              z)) :
        Cochain F G (-1))
      p q hpq =
    (↑z : Cochain F G (-1)).v p q hpq
have a : (if hij : p + -1 = q then (↑z : Cochain F G (-1)).v p q hij else 0) = (↑z : Cochain F G (-1)).v p q hpq
Tactic: dsimp [Cochain.ofHomotopy]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplex (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
R : Type u_1
inst_2 : Ring R
inst_3 : Linear.{u_1, v, u} R C
F G K L : CochainComplex.{v, u, 0} C ℤ
n m : ℤ
φ₁ φ₂ : F ⟶ G
z : { z : Cochain F G (-1) // ofHom φ₁ = δ (-1) 0 z + ofHom φ₂ }
p q : ℤ
hpq : p + -1 = q
⊢ (if hij : p + -1 = q then (↑z : Cochain F G (-1)).v p q hij else 0) = (↑z : Cochain F G (-1)).v p q hpq
have a : (↑z : Cochain F G (-1)).v p q hpq = (↑z : Cochain F G (-1)).v p q hpq
Tactic: rw [dif_pos hpq]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplex (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
F G : CochainComplex.{v, u, 0} C ℤ
f₁ f₂ : F ⟶ G
h : ofHom f₁ = ofHom f₂
⊢ Eq (α := Cocycle F G 0) ((Cocycle.equivHom F G : (a : F ⟶ G) → Cocycle F G 0) f₁ : Cocycle F G 0)
    ((Cocycle.equivHom F G : (a : F ⟶ G) → Cocycle F G 0) f₂ : Cocycle F G 0)
have h₁ : Eq.{v + 1} (α := Cochain F G 0) (↑((Cocycle.equivHom F G : (a : F ⟶ G) → Cocycle F G 0) f₁) : Cochain F G 0)
  (↑((Cocycle.equivHom F G : (a : F ⟶ G) → Cocycle F G 0) f₂) : Cochain F G 0)
Tactic: ext1
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplex (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
p q : ℤ
f : K.X p ⟶ L.X q
n : ℤ
hpq : p + n = q
⊢ (single f n).v p q hpq = f
have dsimp : (if p = p ∧ q = q then 𝟙 (K.X p) ≫ f ≫ 𝟙 (L.X q) else 0) = f
Tactic: dsimp [single]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplex (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
p q : ℤ
f : K.X p ⟶ L.X q
n : ℤ
hpq : p + n = q
⊢ (if p = p ∧ q = q then 𝟙 (K.X p) ≫ f ≫ 𝟙 (L.X q) else 0) = f
have hc : p = p ∧ q = q
Tactic: rw [if_pos, id_comp, comp_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplex (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
p q : ℤ
f : K.X p ⟶ L.X q
n : ℤ
hpq : p + n = q
⊢ p = p ∧ q = q
have hc : p = p
Tactic: tauto
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplex (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
p q : ℤ
f : K.X p ⟶ L.X q
n : ℤ
hpq : p + n = q
hc : p = p
⊢ p = p ∧ q = q
have hc₁ : q = q
Tactic: tauto
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplex (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
p q : ℤ
f : K.X p ⟶ L.X q
n p' q' : ℤ
hpq' : p' + n = q'
hp' : p' ≠ p
⊢ Eq.{v + 1} (α := K.X p' ⟶ L.X q')
    (if h : p = p' ∧ q = q' then (HomologicalComplex.XIsoOfEq K ⋯).inv ≫ f ≫ (HomologicalComplex.XIsoOfEq L ⋯).hom
    else 0)
    0
have hnc : ¬(p = p' ∧ q = q')
Tactic: rw [dif_neg]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplex (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
p q n : ℤ
⊢ Eq.{v + 1} (α := Cochain K L n) (single (p := p) (q := q) 0 n) 0
have h : ∀ (p' q' : ℤ) (hpq' : p' + n = q'),
  Eq.{v + 1} (α := K.X p' ⟶ L.X q') (v (single (p := p) (q := q) 0 n) p' q' hpq') (v 0 p' q' hpq')
Tactic: ext p' q' hpq'
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplex (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
p q n p' q' : ℤ
hpq' : p' + n = q'
⊢ Eq.{v + 1} (α := K.X p' ⟶ L.X q') (v (single (p := p) (q := q) 0 n) p' q' hpq') (v 0 p' q' hpq')
have pos : ∀ (hp : p' = p), Eq.{v + 1} (α := K.X p' ⟶ L.X q') (v (single (p := p) (q := q) 0 n) p' q' hpq') (v 0 p' q' hpq')
Tactic: by_cases hp : p' = p
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplex (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
p q n p' q' : ℤ
hpq' : p' + n = q'
pos : ∀ (hp : p' = p), Eq.{v + 1} (α := K.X p' ⟶ L.X q') (v (single (p := p) (q := q) 0 n) p' q' hpq') (v 0 p' q' hpq')
⊢ Eq.{v + 1} (α := K.X p' ⟶ L.X q') (v (single (p := p) (q := q) 0 n) p' q' hpq') (v 0 p' q' hpq')
have neg : ∀ (hp : ¬p' = p), Eq.{v + 1} (α := K.X p' ⟶ L.X q') (v (single (p := p) (q := q) 0 n) p' q' hpq') (v 0 p' q' hpq')
Tactic: by_cases hp : p' = p
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplex (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
p q n p' q' : ℤ
hpq' : p' + n = q'
hp : p' = p
⊢ Eq.{v + 1} (α := K.X p' ⟶ L.X q') (v (single (p := p) (q := q) 0 n) p' q' hpq') (v 0 p' q' hpq')
have pos : Eq.{v + 1} (α := K.X p' ⟶ L.X q') (v (single (p := p') (q := q) 0 n) p' q' hpq') (v 0 p' q' hpq')
Tactic: subst hp
Cleared hypotheses: p, hp
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplex (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
q n p' q' : ℤ
hpq' : p' + n = q'
⊢ Eq.{v + 1} (α := K.X p' ⟶ L.X q') (v (single (p := p') (q := q) 0 n) p' q' hpq') (v 0 p' q' hpq')
have pos : ∀ (hq : q' = q), Eq.{v + 1} (α := K.X p' ⟶ L.X q') (v (single (p := p') (q := q) 0 n) p' q' hpq') (v 0 p' q' hpq')
Tactic: by_cases hq : q' = q
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplex (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
q n p' q' : ℤ
hpq' : p' + n = q'
pos : ∀ (hq : q' = q), Eq.{v + 1} (α := K.X p' ⟶ L.X q') (v (single (p := p') (q := q) 0 n) p' q' hpq') (v 0 p' q' hpq')
⊢ Eq.{v + 1} (α := K.X p' ⟶ L.X q') (v (single (p := p') (q := q) 0 n) p' q' hpq') (v 0 p' q' hpq')
have neg : ∀ (hq : ¬q' = q), Eq.{v + 1} (α := K.X p' ⟶ L.X q') (v (single (p := p') (q := q) 0 n) p' q' hpq') (v 0 p' q' hpq')
Tactic: by_cases hq : q' = q
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplex (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
q n p' q' : ℤ
hpq' : p' + n = q'
hq : q' = q
⊢ Eq.{v + 1} (α := K.X p' ⟶ L.X q') (v (single (p := p') (q := q) 0 n) p' q' hpq') (v 0 p' q' hpq')
have pos : Eq.{v + 1} (α := K.X p' ⟶ L.X q') (v (single (p := p') (q := q') 0 n) p' q' hpq') (v 0 p' q' hpq')
Tactic: subst hq
Cleared hypotheses: q, hq
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplex (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
p q : ℤ
f : K.X p ⟶ L.X q
n m : ℤ
hm : n + 1 = m
p' q' : ℤ
hp' : p' + 1 = p
hq' : q + 1 = q'
⊢ δ n m (single f n) = single (f ≫ L.d q q') m + m.negOnePow • single (K.d p' p ≫ f) m
have h : ∀ (p'' q'' : ℤ) (hpq'' : p'' + m = q''),
  (δ n m (single f n)).v p'' q'' hpq'' =
    (single (f ≫ L.d q q') m + m.negOnePow • single (K.d p' p ≫ f) m).v p'' q'' hpq''
Tactic: ext p'' q'' hpq''
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplex (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
p q : ℤ
f : K.X p ⟶ L.X q
n m : ℤ
hm : n + 1 = m
p' q' : ℤ
hp' : p' + 1 = p
hq' : q + 1 = q'
p'' q'' : ℤ
hpq'' : p'' + m = q''
⊢ (δ n m (single f n)).v p'' q'' hpq'' =
    (single (f ≫ L.d q q') m + m.negOnePow • single (K.d p' p ≫ f) m).v p'' q'' hpq''
have h : (single f n).v p'' (q'' - 1) sorry ≫ L.d (q'' - 1) q'' + m.negOnePow • K.d p'' (p'' + 1) ≫ (single f n).v (p'' + 1) q'' sorry =
  (single (f ≫ L.d q q') m).v p'' q'' hpq'' + m.negOnePow • (single (K.d p' p ≫ f) m).v p'' q'' hpq''
Tactic: rw [δ_v n m hm (single f n) p'' q'' (by lia) (q'' - 1) (p'' + 1) rfl (by lia),
    add_v, units_smul_v]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplex (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
p q : ℤ
f : K.X p ⟶ L.X q
n m : ℤ
hm : n + 1 = m
p' q' : ℤ
hp' : p' + 1 = p
hq' : q + 1 = q'
p'' q'' : ℤ
hpq'' : p'' + m = q''
⊢ (single f n).v p'' (q'' - 1) ⋯ ≫ L.d (q'' - 1) q'' +
      m.negOnePow • K.d p'' (p'' + 1) ≫ (single f n).v (p'' + 1) q'' ⋯ =
    (single (f ≫ L.d q q') m).v p'' q'' hpq'' + m.negOnePow • (single (K.d p' p ≫ f) m).v p'' q'' hpq''
have h : (single f n).v p'' (q'' - 1) sorry ≫ L.d (q'' - 1) q'' = (single (f ≫ L.d q q') m).v p'' q'' hpq''
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplex (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
p q : ℤ
f : K.X p ⟶ L.X q
n m : ℤ
hm : n + 1 = m
p' q' : ℤ
hp' : p' + 1 = p
hq' : q + 1 = q'
p'' q'' : ℤ
hpq'' : p'' + m = q''
h : (single f n).v p'' (q'' - 1) ⋯ ≫ L.d (q'' - 1) q'' = (single (f ≫ L.d q q') m).v p'' q'' hpq''
⊢ (single f n).v p'' (q'' - 1) ⋯ ≫ L.d (q'' - 1) q'' +
      m.negOnePow • K.d p'' (p'' + 1) ≫ (single f n).v (p'' + 1) q'' ⋯ =
    (single (f ≫ L.d q q') m).v p'' q'' hpq'' + m.negOnePow • (single (K.d p' p ≫ f) m).v p'' q'' hpq''
have h₁ : m.negOnePow • K.d p'' (p'' + 1) ≫ (single f n).v (p'' + 1) q'' sorry =
  m.negOnePow • (single (K.d p' p ≫ f) m).v p'' q'' hpq''
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplex (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
p q : ℤ
f : K.X p ⟶ L.X q
n m : ℤ
hm : n + 1 = m
p' q' : ℤ
hp' : p' + 1 = p
hq' : q + 1 = q'
p'' q'' : ℤ
hpq'' : p'' + m = q''
⊢ (single f n).v p'' (q'' - 1) ⋯ ≫ L.d (q'' - 1) q'' = (single (f ≫ L.d q q') m).v p'' q'' hpq''
have pos : ∀ (h : p'' = p), (single f n).v p'' (q'' - 1) sorry ≫ L.d (q'' - 1) q'' = (single (f ≫ L.d q q') m).v p'' q'' hpq''
Tactic: by_cases h : p'' = p
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplex (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
p q : ℤ
f : K.X p ⟶ L.X q
n m : ℤ
hm : n + 1 = m
p' q' : ℤ
hp' : p' + 1 = p
hq' : q + 1 = q'
p'' q'' : ℤ
hpq'' : p'' + m = q''
pos : ∀ (h : p'' = p), (single f n).v p'' (q'' - 1) ⋯ ≫ L.d (q'' - 1) q'' = (single (f ≫ L.d q q') m).v p'' q'' hpq''
⊢ (single f n).v p'' (q'' - 1) ⋯ ≫ L.d (q'' - 1) q'' = (single (f ≫ L.d q q') m).v p'' q'' hpq''
have neg : ∀ (h : ¬p'' = p), (single f n).v p'' (q'' - 1) sorry ≫ L.d (q'' - 1) q'' = (single (f ≫ L.d q q') m).v p'' q'' hpq''
Tactic: by_cases h : p'' = p
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplex (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
p q : ℤ
f : K.X p ⟶ L.X q
n m : ℤ
hm : n + 1 = m
p' q' : ℤ
hp' : p' + 1 = p
hq' : q + 1 = q'
p'' q'' : ℤ
hpq'' : p'' + m = q''
h : p'' = p
⊢ (single f n).v p'' (q'' - 1) ⋯ ≫ L.d (q'' - 1) q'' = (single (f ≫ L.d q q') m).v p'' q'' hpq''
have pos : ∀ (f : K.X p'' ⟶ L.X q) (hp' : p' + 1 = p''),
  (single f n).v p'' (q'' - 1) sorry ≫ L.d (q'' - 1) q'' = (single (f ≫ L.d q q') m).v p'' q'' hpq''
Tactic: subst h
Cleared hypotheses: p, f, hp', h
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplex (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
q n m : ℤ
hm : n + 1 = m
p' q' : ℤ
hq' : q + 1 = q'
p'' q'' : ℤ
hpq'' : p'' + m = q''
f : K.X p'' ⟶ L.X q
hp' : p' + 1 = p''
⊢ (single f n).v p'' (q'' - 1) ⋯ ≫ L.d (q'' - 1) q'' = (single (f ≫ L.d q q') m).v p'' q'' hpq''
have pos : ∀ (h : q = q'' - 1), (single f n).v p'' (q'' - 1) sorry ≫ L.d (q'' - 1) q'' = (single (f ≫ L.d q q') m).v p'' q'' hpq''
Tactic: by_cases h : q = q'' - 1
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplex (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
q n m : ℤ
hm : n + 1 = m
p' q' : ℤ
hq' : q + 1 = q'
p'' q'' : ℤ
hpq'' : p'' + m = q''
f : K.X p'' ⟶ L.X q
hp' : p' + 1 = p''
pos :
  ∀ (h : q = q'' - 1), (single f n).v p'' (q'' - 1) ⋯ ≫ L.d (q'' - 1) q'' = (single (f ≫ L.d q q') m).v p'' q'' hpq''
⊢ (single f n).v p'' (q'' - 1) ⋯ ≫ L.d (q'' - 1) q'' = (single (f ≫ L.d q q') m).v p'' q'' hpq''
have neg : ∀ (h : ¬q = q'' - 1), (single f n).v p'' (q'' - 1) sorry ≫ L.d (q'' - 1) q'' = (single (f ≫ L.d q q') m).v p'' q'' hpq''
Tactic: by_cases h : q = q'' - 1
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplex (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
q n m : ℤ
hm : n + 1 = m
p' q' : ℤ
hq' : q + 1 = q'
p'' q'' : ℤ
hpq'' : p'' + m = q''
f : K.X p'' ⟶ L.X q
hp' : p' + 1 = p''
h : q = q'' - 1
⊢ (single f n).v p'' (q'' - 1) ⋯ ≫ L.d (q'' - 1) q'' = (single (f ≫ L.d q q') m).v p'' q'' hpq''
have pos : ∀ (hq' : q'' - 1 + 1 = q') (f : K.X p'' ⟶ L.X (q'' - 1)),
  (single f n).v p'' (q'' - 1) sorry ≫ L.d (q'' - 1) q'' = (single (f ≫ L.d (q'' - 1) q') m).v p'' q'' hpq''
Tactic: subst h
Cleared hypotheses: q, hq', f, h
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplex (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
n m : ℤ
hm : n + 1 = m
p' q' p'' q'' : ℤ
hpq'' : p'' + m = q''
hp' : p' + 1 = p''
hq' : q'' - 1 + 1 = q'
f : K.X p'' ⟶ L.X (q'' - 1)
⊢ (single f n).v p'' (q'' - 1) ⋯ ≫ L.d (q'' - 1) q'' = (single (f ≫ L.d (q'' - 1) q') m).v p'' q'' hpq''
have pos : ∀ (hpq'' : p'' + m = q') (hq' : q' - 1 + 1 = q') (f : K.X p'' ⟶ L.X (q' - 1)),
  (single f n).v p'' (q' - 1) sorry ≫ L.d (q' - 1) q' = (single (f ≫ L.d (q' - 1) q') m).v p'' q' hpq''
Tactic: obtain rfl : q' = q'' := by lia
Cleared hypotheses: q'', hpq'', hq', f
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplex (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
q n m : ℤ
hm : n + 1 = m
p' q' : ℤ
hq' : q + 1 = q'
p'' q'' : ℤ
hpq'' : p'' + m = q''
f : K.X p'' ⟶ L.X q
hp' : p' + 1 = p''
h : ¬q = q'' - 1
⊢ (single f n).v p'' (q'' - 1) ⋯ ≫ L.d (q'' - 1) q'' = (single (f ≫ L.d q q') m).v p'' q'' hpq''
have neg : q'' ≠ q'
Tactic: rw [single_v_eq_zero', single_v_eq_zero', zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplex (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
q n m : ℤ
hm : n + 1 = m
p' q' : ℤ
hq' : q + 1 = q'
p'' q'' : ℤ
hpq'' : p'' + m = q''
f : K.X p'' ⟶ L.X q
hp' : p' + 1 = p''
h : ¬q = q'' - 1
neg : q'' ≠ q'
⊢ (single f n).v p'' (q'' - 1) ⋯ ≫ L.d (q'' - 1) q'' = (single (f ≫ L.d q q') m).v p'' q'' hpq''
have neg₁ : q'' - 1 ≠ q
Tactic: rw [single_v_eq_zero', single_v_eq_zero', zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplex (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
p q : ℤ
f : K.X p ⟶ L.X q
n m : ℤ
hm : n + 1 = m
p' q' : ℤ
hp' : p' + 1 = p
hq' : q + 1 = q'
p'' q'' : ℤ
hpq'' : p'' + m = q''
h : ¬p'' = p
⊢ (single f n).v p'' (q'' - 1) ⋯ ≫ L.d (q'' - 1) q'' = (single (f ≫ L.d q q') m).v p'' q'' hpq''
have neg : CategoryStruct.comp (Y := L.X (q'' - 1)) 0 (L.d (q'' - 1) q'') = (single (f ≫ L.d q q') m).v p'' q'' hpq''
Tactic: rw [single_v_eq_zero _ _ _ _ _ h, single_v_eq_zero _ _ _ _ _ h, zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplex (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
p q : ℤ
f : K.X p ⟶ L.X q
n m : ℤ
hm : n + 1 = m
p' q' : ℤ
hp' : p' + 1 = p
hq' : q + 1 = q'
p'' q'' : ℤ
hpq'' : p'' + m = q''
h : ¬p'' = p
neg : CategoryStruct.comp (Y := L.X (q'' - 1)) 0 (L.d (q'' - 1) q'') = (single (f ≫ L.d q q') m).v p'' q'' hpq''
⊢ (single f n).v p'' (q'' - 1) ⋯ ≫ L.d (q'' - 1) q'' = (single (f ≫ L.d q q') m).v p'' q'' hpq''
have neg₁ : Eq (α := K.X p'' ⟶ L.X q'') (CategoryStruct.comp (Y := L.X (q'' - 1)) 0 (L.d (q'' - 1) q'')) 0
Tactic: rw [single_v_eq_zero _ _ _ _ _ h, single_v_eq_zero _ _ _ _ _ h, zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplex (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
p q : ℤ
f : K.X p ⟶ L.X q
n m : ℤ
hm : n + 1 = m
p' q' : ℤ
hp' : p' + 1 = p
hq' : q + 1 = q'
p'' q'' : ℤ
hpq'' : p'' + m = q''
h : ¬p'' = p
neg : CategoryStruct.comp (Y := L.X (q'' - 1)) 0 (L.d (q'' - 1) q'') = (single (f ≫ L.d q q') m).v p'' q'' hpq''
neg₁ : Eq (α := K.X p'' ⟶ L.X q'') (CategoryStruct.comp (Y := L.X (q'' - 1)) 0 (L.d (q'' - 1) q'')) 0
⊢ (single f n).v p'' (q'' - 1) ⋯ ≫ L.d (q'' - 1) q'' = (single (f ≫ L.d q q') m).v p'' q'' hpq''
have neg₂ : Eq.{v + 1} (α := K.X p'' ⟶ L.X q'') 0 0
Tactic: rw [single_v_eq_zero _ _ _ _ _ h, single_v_eq_zero _ _ _ _ _ h, zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplex (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
p q : ℤ
f : K.X p ⟶ L.X q
n m : ℤ
hm : n + 1 = m
p' q' : ℤ
hp' : p' + 1 = p
hq' : q + 1 = q'
p'' q'' : ℤ
hpq'' : p'' + m = q''
⊢ m.negOnePow • K.d p'' (p'' + 1) ≫ (single f n).v (p'' + 1) q'' ⋯ =
    m.negOnePow • (single (K.d p' p ≫ f) m).v p'' q'' hpq''
have h : ∀ (hpq'' : p'' + (n + 1) = q''),
  (n + 1).negOnePow • K.d p'' (p'' + 1) ≫ (single f n).v (p'' + 1) q'' sorry =
    (n + 1).negOnePow • v (single (K.d p' p ≫ f) (n + 1)) p'' q'' hpq''
Tactic: subst hm
Cleared hypotheses: m, hm, hpq''
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplex (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
p q : ℤ
f : K.X p ⟶ L.X q
n p' q' : ℤ
hp' : p' + 1 = p
hq' : q + 1 = q'
p'' q'' : ℤ
hpq'' : p'' + (n + 1) = q''
⊢ (n + 1).negOnePow • K.d p'' (p'' + 1) ≫ (single f n).v (p'' + 1) q'' ⋯ =
    (n + 1).negOnePow • v (single (K.d p' p ≫ f) (n + 1)) p'' q'' hpq''
have pos : ∀ (h : q'' = q),
  (n + 1).negOnePow • K.d p'' (p'' + 1) ≫ (single f n).v (p'' + 1) q'' sorry =
    (n + 1).negOnePow • v (single (K.d p' p ≫ f) (n + 1)) p'' q'' hpq''
Tactic: by_cases h : q'' = q
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplex (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
p q : ℤ
f : K.X p ⟶ L.X q
n p' q' : ℤ
hp' : p' + 1 = p
hq' : q + 1 = q'
p'' q'' : ℤ
hpq'' : p'' + (n + 1) = q''
pos :
  ∀ (h : q'' = q),
    (n + 1).negOnePow • K.d p'' (p'' + 1) ≫ (single f n).v (p'' + 1) q'' ⋯ =
      (n + 1).negOnePow • v (single (K.d p' p ≫ f) (n + 1)) p'' q'' hpq''
⊢ (n + 1).negOnePow • K.d p'' (p'' + 1) ≫ (single f n).v (p'' + 1) q'' ⋯ =
    (n + 1).negOnePow • v (single (K.d p' p ≫ f) (n + 1)) p'' q'' hpq''
have neg : ∀ (h : ¬q'' = q),
  (n + 1).negOnePow • K.d p'' (p'' + 1) ≫ (single f n).v (p'' + 1) q'' sorry =
    (n + 1).negOnePow • v (single (K.d p' p ≫ f) (n + 1)) p'' q'' hpq''
Tactic: by_cases h : q'' = q
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplex (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
p q : ℤ
f : K.X p ⟶ L.X q
n p' q' : ℤ
hp' : p' + 1 = p
hq' : q + 1 = q'
p'' q'' : ℤ
hpq'' : p'' + (n + 1) = q''
h : q'' = q
⊢ (n + 1).negOnePow • K.d p'' (p'' + 1) ≫ (single f n).v (p'' + 1) q'' ⋯ =
    (n + 1).negOnePow • v (single (K.d p' p ≫ f) (n + 1)) p'' q'' hpq''
have pos : ∀ (f : K.X p ⟶ L.X q'') (hq' : q'' + 1 = q'),
  (n + 1).negOnePow • K.d p'' (p'' + 1) ≫ (single f n).v (p'' + 1) q'' sorry =
    (n + 1).negOnePow • v (single (K.d p' p ≫ f) (n + 1)) p'' q'' hpq''
Tactic: subst h
Cleared hypotheses: q, f, hq', h
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplex (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
p n p' q' : ℤ
hp' : p' + 1 = p
p'' q'' : ℤ
hpq'' : p'' + (n + 1) = q''
f : K.X p ⟶ L.X q''
hq' : q'' + 1 = q'
⊢ (n + 1).negOnePow • K.d p'' (p'' + 1) ≫ (single f n).v (p'' + 1) q'' ⋯ =
    (n + 1).negOnePow • v (single (K.d p' p ≫ f) (n + 1)) p'' q'' hpq''
have pos : ∀ (h : p'' = p'),
  (n + 1).negOnePow • K.d p'' (p'' + 1) ≫ (single f n).v (p'' + 1) q'' sorry =
    (n + 1).negOnePow • v (single (K.d p' p ≫ f) (n + 1)) p'' q'' hpq''
Tactic: by_cases h : p'' = p'
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplex (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
p n p' q' : ℤ
hp' : p' + 1 = p
p'' q'' : ℤ
hpq'' : p'' + (n + 1) = q''
f : K.X p ⟶ L.X q''
hq' : q'' + 1 = q'
pos :
  ∀ (h : p'' = p'),
    (n + 1).negOnePow • K.d p'' (p'' + 1) ≫ (single f n).v (p'' + 1) q'' ⋯ =
      (n + 1).negOnePow • v (single (K.d p' p ≫ f) (n + 1)) p'' q'' hpq''
⊢ (n + 1).negOnePow • K.d p'' (p'' + 1) ≫ (single f n).v (p'' + 1) q'' ⋯ =
    (n + 1).negOnePow • v (single (K.d p' p ≫ f) (n + 1)) p'' q'' hpq''
have neg : ∀ (h : ¬p'' = p'),
  (n + 1).negOnePow • K.d p'' (p'' + 1) ≫ (single f n).v (p'' + 1) q'' sorry =
    (n + 1).negOnePow • v (single (K.d p' p ≫ f) (n + 1)) p'' q'' hpq''
Tactic: by_cases h : p'' = p'