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
F G K L : CochainComplex.{v, u, 0} C ℤ
n₁ n₂ n₃ : ℤ
z₁ : Cochain F G n₁
z₂ : Cochain G K n₂
z₃ : Cochain K L n₃
p q : ℤ
hpq : p + (n₁ + n₂ + n₃) = q
h : (z₁.comp z₂ ⋯).v p (p + n₁ + n₂) ⋯ ≫ z₃.v (p + n₁ + n₂) q ⋯ = (z₁.comp (z₂.comp z₃ ⋯) ⋯).v p q hpq
h₁ : (z₁.v p (p + n₁) ⋯ ≫ z₂.v (p + n₁) (p + n₁ + n₂) ⋯) ≫ z₃.v (p + n₁ + n₂) q ⋯ = (z₁.comp (z₂.comp z₃ ⋯) ⋯).v p q hpq
h₂ :
  (z₁.v p (p + n₁) ⋯ ≫ z₂.v (p + n₁) (p + n₁ + n₂) ⋯) ≫ z₃.v (p + n₁ + n₂) q ⋯ =
    z₁.v p (p + n₁) ⋯ ≫ (z₂.comp z₃ ⋯).v (p + n₁) q ⋯
⊢ v ((z₁.comp z₂ ⋯).comp z₃ ⋯) p q hpq = (z₁.comp (z₂.comp z₃ ⋯) ⋯).v p q hpq
have h₃ : (z₁.v p (p + n₁) sorry ≫ z₂.v (p + n₁) (p + n₁ + n₂) sorry) ≫ z₃.v (p + n₁ + n₂) q sorry =
  z₁.v p (p + n₁) sorry ≫ z₂.v (p + n₁) (p + n₁ + n₂) sorry ≫ z₃.v (p + n₁ + n₂) q sorry
Tactic: rw [comp_v _ _ rfl p (p + n₁ + n₂) q (add_assoc _ _ _).symm (by lia),
    comp_v z₁ z₂ rfl p (p + n₁) (p + n₁ + n₂) (by lia) (by lia),
    comp_v z₁ (z₂.comp z₃ rfl) (add_assoc n₁ n₂ n₃).symm p (p + n₁) q (by lia) (by lia),
    comp_v z₂ z₃ rfl (p + n₁) (p + n₁ + n₂) q (by lia) (by lia), assoc]
-- 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 K L : CochainComplex.{v, u, 0} C ℤ
n₁ n₂ n₃ : ℤ
z₁ : Cochain F G n₁
z₂ : Cochain G K n₂
z₃ : Cochain K L n₃
p q : ℤ
hpq : p + (n₁ + n₂ + n₃) = q
h : (z₁.comp z₂ ⋯).v p (p + n₁ + n₂) ⋯ ≫ z₃.v (p + n₁ + n₂) q ⋯ = (z₁.comp (z₂.comp z₃ ⋯) ⋯).v p q hpq
h₁ : (z₁.v p (p + n₁) ⋯ ≫ z₂.v (p + n₁) (p + n₁ + n₂) ⋯) ≫ z₃.v (p + n₁ + n₂) q ⋯ = (z₁.comp (z₂.comp z₃ ⋯) ⋯).v p q hpq
h₂ :
  (z₁.v p (p + n₁) ⋯ ≫ z₂.v (p + n₁) (p + n₁ + n₂) ⋯) ≫ z₃.v (p + n₁ + n₂) q ⋯ =
    z₁.v p (p + n₁) ⋯ ≫ (z₂.comp z₃ ⋯).v (p + n₁) q ⋯
h₃ :
  (z₁.v p (p + n₁) ⋯ ≫ z₂.v (p + n₁) (p + n₁ + n₂) ⋯) ≫ z₃.v (p + n₁ + n₂) q ⋯ =
    z₁.v p (p + n₁) ⋯ ≫ z₂.v (p + n₁) (p + n₁ + n₂) ⋯ ≫ z₃.v (p + n₁ + n₂) q ⋯
⊢ v ((z₁.comp z₂ ⋯).comp z₃ ⋯) p q hpq = (z₁.comp (z₂.comp z₃ ⋯) ⋯).v p q hpq
have h₄ : z₁.v p (p + n₁) sorry ≫ z₂.v (p + n₁) (p + n₁ + n₂) sorry ≫ z₃.v (p + n₁ + n₂) q sorry =
  z₁.v p (p + n₁) sorry ≫ z₂.v (p + n₁) (p + n₁ + n₂) sorry ≫ z₃.v (p + n₁ + n₂) q sorry
Tactic: rw [comp_v _ _ rfl p (p + n₁ + n₂) q (add_assoc _ _ _).symm (by lia),
    comp_v z₁ z₂ rfl p (p + n₁) (p + n₁ + n₂) (by lia) (by lia),
    comp_v z₁ (z₂.comp z₃ rfl) (add_assoc n₁ n₂ n₃).symm p (p + n₁) q (by lia) (by lia),
    comp_v z₂ z₃ rfl (p + n₁) (p + n₁ + n₂) q (by lia) (by lia), assoc]
-- 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 n₁ n₂ n₁₂ : ℤ
z₁ : Cochain F G n₁
z₂ : Cochain G K (-n₂)
z₃ : Cochain K L n₂
h₁₂ : n₁ + -n₂ = n₁₂
⊢ n₁₂ + n₂ = n₁
have rw : n₁ + -n₂ + n₂ = n₁
Tactic: rw [← h₁₂, add_assoc, neg_add_cancel, add_zero]
-- 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 n₁ n₂ n₁₂ : ℤ
z₁ : Cochain F G n₁
z₂ : Cochain G K (-n₂)
z₃ : Cochain K L n₂
h₁₂ : n₁ + -n₂ = n₁₂
rw : n₁ + -n₂ + n₂ = n₁
⊢ n₁₂ + n₂ = n₁
have rw₁ : n₁ + (-n₂ + n₂) = n₁
Tactic: rw [← h₁₂, add_assoc, neg_add_cancel, add_zero]
-- 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 n₁ n₂ n₁₂ : ℤ
z₁ : Cochain F G n₁
z₂ : Cochain G K (-n₂)
z₃ : Cochain K L n₂
h₁₂ : n₁ + -n₂ = n₁₂
rw : n₁ + -n₂ + n₂ = n₁
rw₁ : n₁ + (-n₂ + n₂) = n₁
⊢ n₁₂ + n₂ = n₁
have rw₂ : n₁ + 0 = n₁
Tactic: rw [← h₁₂, add_assoc, neg_add_cancel, add_zero]
-- 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 n₁ n₂ n₁₂ : ℤ
z₁ : Cochain F G n₁
z₂ : Cochain G K (-n₂)
z₃ : Cochain K L n₂
h₁₂ : n₁ + -n₂ = n₁₂
rw : n₁ + -n₂ + n₂ = n₁
rw₁ : n₁ + (-n₂ + n₂) = n₁
rw₂ : n₁ + 0 = n₁
⊢ n₁₂ + n₂ = n₁
have rw₃ : n₁ = n₁
Tactic: rw [← h₁₂, add_assoc, neg_add_cancel, add_zero]
-- 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 K : CochainComplex.{v, u, 0} C ℤ
n₁ n₂ n₁₂ : ℤ
z₂ : Cochain G K n₂
h : n₁ + n₂ = n₁₂
⊢ Eq (α := Cochain F K n₁₂) (comp 0 z₂ h) 0
have h₁ : ∀ (p q : ℤ) (hpq : p + n₁₂ = q), Eq (α := F.X p ⟶ K.X q) (v (comp 0 z₂ h) 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
F G K : CochainComplex.{v, u, 0} C ℤ
n₁ n₂ n₁₂ : ℤ
z₁ z₁' : Cochain F G n₁
z₂ : Cochain G K n₂
h : n₁ + n₂ = n₁₂
⊢ (z₁ + z₁').comp z₂ h = z₁.comp z₂ h + z₁'.comp z₂ h
have h₁ : ∀ (p q : ℤ) (hpq : p + n₁₂ = q), ((z₁ + z₁').comp z₂ h).v p q hpq = (z₁.comp z₂ h + z₁'.comp z₂ h).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
F G K : CochainComplex.{v, u, 0} C ℤ
n₁ n₂ n₁₂ : ℤ
z₁ z₁' : Cochain F G n₁
z₂ : Cochain G K n₂
h : n₁ + n₂ = n₁₂
⊢ (z₁ - z₁').comp z₂ h = z₁.comp z₂ h - z₁'.comp z₂ h
have h₁ : ∀ (p q : ℤ) (hpq : p + n₁₂ = q), ((z₁ - z₁').comp z₂ h).v p q hpq = (z₁.comp z₂ h - z₁'.comp z₂ h).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
F G K : CochainComplex.{v, u, 0} C ℤ
n₁ n₂ n₁₂ : ℤ
z₁ : Cochain F G n₁
z₂ : Cochain G K n₂
h : n₁ + n₂ = n₁₂
⊢ (-z₁).comp z₂ h = -z₁.comp z₂ h
have h₁ : ∀ (p q : ℤ) (hpq : p + n₁₂ = q), ((-z₁).comp z₂ h).v p q hpq = (-z₁.comp z₂ h).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 : CochainComplex.{v, u, 0} C ℤ
n₁ n₂ n₁₂ : ℤ
k : R
z₁ : Cochain F G n₁
z₂ : Cochain G K n₂
h : n₁ + n₂ = n₁₂
⊢ (k • z₁).comp z₂ h = k • z₁.comp z₂ h
have h₁ : ∀ (p q : ℤ) (hpq : p + n₁₂ = q), ((k • z₁).comp z₂ h).v p q hpq = (k • z₁.comp z₂ h).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
F G : CochainComplex.{v, u, 0} C ℤ
n : ℤ
z₂ : Cochain F G n
⊢ (ofHom (𝟙 F)).comp z₂ ⋯ = z₂
have h : ∀ (p q : ℤ) (hpq : p + n = q), ((ofHom (𝟙 F)).comp z₂ sorry).v p q hpq = z₂.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
F G K : CochainComplex.{v, u, 0} C ℤ
n₁ n₂ n₁₂ : ℤ
z₁ : Cochain F G n₁
h : n₁ + n₂ = n₁₂
⊢ Eq (α := Cochain F K n₁₂) (z₁.comp 0 h) 0
have h₁ : ∀ (p q : ℤ) (hpq : p + n₁₂ = q), Eq (α := F.X p ⟶ K.X q) (v (z₁.comp 0 h) 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
F G K : CochainComplex.{v, u, 0} C ℤ
n₁ n₂ n₁₂ : ℤ
z₁ : Cochain F G n₁
z₂ z₂' : Cochain G K n₂
h : n₁ + n₂ = n₁₂
⊢ z₁.comp (z₂ + z₂') h = z₁.comp z₂ h + z₁.comp z₂' h
have h₁ : ∀ (p q : ℤ) (hpq : p + n₁₂ = q), (z₁.comp (z₂ + z₂') h).v p q hpq = (z₁.comp z₂ h + z₁.comp z₂' h).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
F G K : CochainComplex.{v, u, 0} C ℤ
n₁ n₂ n₁₂ : ℤ
z₁ : Cochain F G n₁
z₂ z₂' : Cochain G K n₂
h : n₁ + n₂ = n₁₂
⊢ z₁.comp (z₂ - z₂') h = z₁.comp z₂ h - z₁.comp z₂' h
have h₁ : ∀ (p q : ℤ) (hpq : p + n₁₂ = q), (z₁.comp (z₂ - z₂') h).v p q hpq = (z₁.comp z₂ h - z₁.comp z₂' h).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
F G K : CochainComplex.{v, u, 0} C ℤ
n₁ n₂ n₁₂ : ℤ
z₁ : Cochain F G n₁
z₂ : Cochain G K n₂
h : n₁ + n₂ = n₁₂
⊢ z₁.comp (-z₂) h = -z₁.comp z₂ h
have h₁ : ∀ (p q : ℤ) (hpq : p + n₁₂ = q), (z₁.comp (-z₂) h).v p q hpq = (-z₁.comp z₂ h).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 : CochainComplex.{v, u, 0} C ℤ
n₁ n₂ n₁₂ : ℤ
z₁ : Cochain F G n₁
k : R
z₂ : Cochain G K n₂
h : n₁ + n₂ = n₁₂
⊢ z₁.comp (k • z₂) h = k • z₁.comp z₂ h
have h₁ : ∀ (p q : ℤ) (hpq : p + n₁₂ = q), (z₁.comp (k • z₂) h).v p q hpq = (k • z₁.comp z₂ h).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
F G : CochainComplex.{v, u, 0} C ℤ
n : ℤ
z₁ : Cochain F G n
⊢ z₁.comp (ofHom (𝟙 G)) ⋯ = z₁
have h : ∀ (p q : ℤ) (hpq : p + n = q), (z₁.comp (ofHom (𝟙 G)) sorry).v p q hpq = z₁.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 : ℤ
z : Cochain F G n
p q : ℤ
hpq : p + m = q
⊢ p + m - n + n = q
have rw : q - n + n = q
Tactic: rw [hpq, sub_add_cancel]
-- 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 : ℤ
z : Cochain F G n
p q : ℤ
hpq : p + m = q
rw : q - n + n = q
⊢ p + m - n + n = q
have rw₁ : q = q
Tactic: rw [hpq, sub_add_cancel]
-- 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 : ℤ
hnm : n + 1 = m
z : Cochain F G n
p q : ℤ
hpq : p + m = q
q₁ q₂ : ℤ
hq₁ : q₁ = q - 1
hq₂ : p + 1 = q₂
⊢ p + n = q₁
have rw : p + n = q - 1
Tactic: rw [hq₁, ← hpq, ← hnm, ← add_assoc, add_sub_cancel_right]
-- 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 : ℤ
hnm : n + 1 = m
z : Cochain F G n
p q : ℤ
hpq : p + m = q
q₁ q₂ : ℤ
hq₁ : q₁ = q - 1
hq₂ : p + 1 = q₂
rw : p + n = q - 1
⊢ p + n = q₁
have rw₁ : p + n = p + m - 1
Tactic: rw [hq₁, ← hpq, ← hnm, ← add_assoc, add_sub_cancel_right]
-- 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 : ℤ
hnm : n + 1 = m
z : Cochain F G n
p q : ℤ
hpq : p + m = q
q₁ q₂ : ℤ
hq₁ : q₁ = q - 1
hq₂ : p + 1 = q₂
rw : p + n = q - 1
rw₁ : p + n = p + m - 1
⊢ p + n = q₁
have rw₂ : p + n = p + (n + 1) - 1
Tactic: rw [hq₁, ← hpq, ← hnm, ← add_assoc, add_sub_cancel_right]
-- 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 : ℤ
hnm : n + 1 = m
z : Cochain F G n
p q : ℤ
hpq : p + m = q
q₁ q₂ : ℤ
hq₁ : q₁ = q - 1
hq₂ : p + 1 = q₂
rw : p + n = q - 1
rw₁ : p + n = p + m - 1
rw₂ : p + n = p + (n + 1) - 1
⊢ p + n = q₁
have rw₃ : p + n = p + n + 1 - 1
Tactic: rw [hq₁, ← hpq, ← hnm, ← add_assoc, add_sub_cancel_right]
-- 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 : ℤ
hnm : n + 1 = m
z : Cochain F G n
p q : ℤ
hpq : p + m = q
q₁ q₂ : ℤ
hq₁ : q₁ = q - 1
hq₂ : p + 1 = q₂
rw : p + n = q - 1
rw₁ : p + n = p + m - 1
rw₂ : p + n = p + (n + 1) - 1
rw₃ : p + n = p + n + 1 - 1
⊢ p + n = q₁
have rw₄ : p + n = p + n
Tactic: rw [hq₁, ← hpq, ← hnm, ← add_assoc, add_sub_cancel_right]
-- 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 : ℤ
hnm : n + 1 = m
z : Cochain F G n
p q : ℤ
hpq : p + m = q
q₁ q₂ : ℤ
hq₁ : q₁ = q - 1
hq₂ : p + 1 = q₂
⊢ q₂ + n = q
have rw : p + 1 + n = q
Tactic: rw [← hq₂, add_assoc, add_comm 1, hnm, 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 : ℤ
hnm : n + 1 = m
z : Cochain F G n
p q : ℤ
hpq : p + m = q
q₁ q₂ : ℤ
hq₁ : q₁ = q - 1
hq₂ : p + 1 = q₂
rw : p + 1 + n = q
⊢ q₂ + n = q
have rw₁ : p + (1 + n) = q
Tactic: rw [← hq₂, add_assoc, add_comm 1, hnm, 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 : ℤ
hnm : n + 1 = m
z : Cochain F G n
p q : ℤ
hpq : p + m = q
q₁ q₂ : ℤ
hq₁ : q₁ = q - 1
hq₂ : p + 1 = q₂
rw : p + 1 + n = q
rw₁ : p + (1 + n) = q
⊢ q₂ + n = q
have rw₂ : p + (n + 1) = q
Tactic: rw [← hq₂, add_assoc, add_comm 1, hnm, 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 : ℤ
hnm : n + 1 = m
z : Cochain F G n
p q : ℤ
hpq : p + m = q
q₁ q₂ : ℤ
hq₁ : q₁ = q - 1
hq₂ : p + 1 = q₂
rw : p + 1 + n = q
rw₁ : p + (1 + n) = q
rw₂ : p + (n + 1) = q
rw₃ : p + m = q
⊢ q₂ + n = q
have rw₄ : q = q
Tactic: rw [← hq₂, add_assoc, add_comm 1, hnm, 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 ℤ
n m : ℤ
hnm : n + 1 = m
z : Cochain F G n
p q : ℤ
hpq : p + m = q
q₁ q₂ : ℤ
hq₁ : q₁ = q - 1
hq₂ : p + 1 = q₂
⊢ (δ n m z).v p q hpq = z.v p q₁ ⋯ ≫ G.d q₁ q + m.negOnePow • F.d p q₂ ≫ z.v q₂ q ⋯
have obtain : ∀ (hq₁ : p + n = q - 1), (δ n m z).v p q hpq = z.v p (p + n) sorry ≫ G.d (p + n) q + m.negOnePow • F.d p q₂ ≫ z.v q₂ q sorry
Tactic: obtain rfl : q₁ = p + n := by lia
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
F G : CochainComplex.{v, u, 0} C ℤ
n m : ℤ
hnm : n + 1 = m
z : Cochain F G n
p q : ℤ
hpq : p + m = q
q₂ : ℤ
hq₂ : p + 1 = q₂
hq₁ : p + n = q - 1
⊢ (δ n m z).v p q hpq = z.v p (p + n) ⋯ ≫ G.d (p + n) q + m.negOnePow • F.d p q₂ ≫ z.v q₂ q ⋯
have obtain : ∀ (hq₂ : p + 1 = p + m - n),
  (δ n m z).v p q hpq = z.v p (p + n) sorry ≫ G.d (p + n) q + m.negOnePow • F.d p (p + m - n) ≫ z.v (p + m - n) q sorry
Tactic: obtain rfl : q₂ = p + m - n := by lia
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
F G : CochainComplex.{v, u, 0} C ℤ
n m : ℤ
hnm : ¬n + 1 = m
z : Cochain F G n
⊢ δ n m z = 0
have h : ∀ (p q : ℤ) (hpq : p + m = q), (δ n m z).v p q hpq = Cochain.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
F G : CochainComplex.{v, u, 0} C ℤ
n m : ℤ
hnm : ¬n + 1 = m
z : Cochain F G n
p q : ℤ
hpq : p + m = q
⊢ Eq.{v + 1} (α := F.X p ⟶ G.X q)
    (Cochain.v
      (Cochain.mk fun (p q : ℤ) (hpq : p + m = q) ↦
        z.v p (p + n) ⋯ ≫ G.d (p + n) q + m.negOnePow • F.d p (p + m - n) ≫ z.v (p + m - n) q ⋯)
      p q hpq)
    (Cochain.v 0 p q hpq)
have h : ¬(ComplexShape.up ℤ).Rel (p + n) q
Tactic: rw [Cochain.mk_v, Cochain.zero_v, F.shape, G.shape, comp_zero, zero_add, zero_comp, smul_zero]
-- 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 ℤ
n m : ℤ
hnm : ¬n + 1 = m
z : Cochain F G n
p q : ℤ
hpq : p + m = q
h : ¬(ComplexShape.up ℤ).Rel (p + n) q
⊢ Eq.{v + 1} (α := F.X p ⟶ G.X q)
    (Cochain.v
      (Cochain.mk fun (p q : ℤ) (hpq : p + m = q) ↦
        z.v p (p + n) ⋯ ≫ G.d (p + n) q + m.negOnePow • F.d p (p + m - n) ≫ z.v (p + m - n) q ⋯)
      p q hpq)
    (Cochain.v 0 p q hpq)
have h₁ : ¬(ComplexShape.up ℤ).Rel p (p + m - n)
Tactic: rw [Cochain.mk_v, Cochain.zero_v, F.shape, G.shape, comp_zero, zero_add, zero_comp, smul_zero]
-- 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 : ℤ
α β : Cochain F G n
⊢ δ n m (α + β) = δ n m α + δ n m β
have pos : ∀ (h : n + 1 = m), δ n m (α + β) = δ n m α + δ n m β
Tactic: by_cases h : n + 1 = m
-- 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 : ℤ
α β : Cochain F G n
pos : ∀ (h : n + 1 = m), δ n m (α + β) = δ n m α + δ n m β
⊢ δ n m (α + β) = δ n m α + δ n m β
have neg : ∀ (h : ¬n + 1 = m), δ n m (α + β) = δ n m α + δ n m β
Tactic: by_cases h : n + 1 = m
-- 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 : ℤ
α β : Cochain F G n
h : n + 1 = m
⊢ δ n m (α + β) = δ n m α + δ n m β
have pos : ∀ (p q : ℤ) (hpq : p + m = q), (δ n m (α + β)).v p q hpq = (δ n m α + δ n 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
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 : ℤ
α β : Cochain F G n
h : n + 1 = m
p q : ℤ
hpq : p + m = q
⊢ (δ n m (α + β)).v p q hpq = (δ n m α + δ n m β).v p q hpq
have pos : (δ n m (α + β)).v p q hpq = (δ n m α).v p q hpq + (δ n m β).v p q hpq
Tactic: dsimp
-- 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 : ℤ
α β : Cochain F G n
h : n + 1 = m
p q : ℤ
hpq : p + m = q
⊢ (δ n m (α + β)).v p q hpq = (δ n m α).v p q hpq + (δ n m β).v p q hpq
have pos : α.v p (q - 1) sorry ≫ G.d (q - 1) q + β.v p (q - 1) sorry ≫ G.d (q - 1) q +
    (m.negOnePow • F.d p (p + 1) ≫ α.v (p + 1) q sorry + m.negOnePow • F.d p (p + 1) ≫ β.v (p + 1) q sorry) =
  α.v p (q - 1) sorry ≫ G.d (q - 1) q + m.negOnePow • F.d p (p + 1) ≫ α.v (p + 1) q sorry +
    (β.v p (q - 1) sorry ≫ G.d (q - 1) q + m.negOnePow • F.d p (p + 1) ≫ β.v (p + 1) q sorry)
Tactic: simp only [δ_v n m h _ p q hpq _ _ rfl rfl, Cochain.add_v, add_comp, comp_add, smul_add]
-- 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 : ℤ
r : R
a : Cochain F G n
⊢ δ n m (r • a) = HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) r : R) (δ n m a)
have pos : ∀ (h : n + 1 = m), δ n m (r • a) = HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) r : R) (δ n m a)
Tactic: by_cases h : n + 1 = m
-- 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 : ℤ
r : R
a : Cochain F G n
pos : ∀ (h : n + 1 = m), δ n m (r • a) = HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) r : R) (δ n m a)
⊢ δ n m (r • a) = HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) r : R) (δ n m a)
have neg : ∀ (h : ¬n + 1 = m), δ n m (r • a) = HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) r : R) (δ n m a)
Tactic: by_cases h : n + 1 = m
-- 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 : ℤ
r : R
a : Cochain F G n
h : n + 1 = m
⊢ δ n m (r • a) = HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) r : R) (δ n m a)
have pos : ∀ (p q : ℤ) (hpq : p + m = q),
  (δ n m (r • a)).v p q hpq = (HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) r : R) (δ n m a)).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 : ℤ
r : R
a : Cochain F G n
h : n + 1 = m
p q : ℤ
hpq : p + m = q
⊢ (δ n m (r • a)).v p q hpq = (HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) r : R) (δ n m a)).v p q hpq
have pos : (δ n m (r • a)).v p q hpq = r • (δ n m a).v p q hpq
Tactic: dsimp
-- 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 ℤ
n₀ n₁ n₂ : ℤ
z : Cochain F G n₀
⊢ δ n₁ n₂ (δ n₀ n₁ z) = 0
have pos : ∀ (h₁₂ : n₁ + 1 = n₂), δ n₁ n₂ (δ n₀ n₁ z) = 0
Tactic: by_cases h₁₂ : n₁ + 1 = n₂
-- 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 ℤ
n₀ n₁ n₂ : ℤ
z : Cochain F G n₀
pos : ∀ (h₁₂ : n₁ + 1 = n₂), δ n₁ n₂ (δ n₀ n₁ z) = 0
⊢ δ n₁ n₂ (δ n₀ n₁ z) = 0
have neg : ∀ (h₁₂ : ¬n₁ + 1 = n₂), δ n₁ n₂ (δ n₀ n₁ z) = 0
Tactic: by_cases h₁₂ : n₁ + 1 = n₂
-- 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 ℤ
n₀ n₁ n₂ : ℤ
z : Cochain F G n₀
h₁₂ : ¬n₁ + 1 = n₂
⊢ δ n₁ n₂ (δ n₀ n₁ z) = 0
have neg : Eq.{v + 1} (α := Cochain F G n₂) 0 0
Tactic: rw [δ_shape _ _ h₁₂]