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 : CochainComplex.{v, u, 0} C ℤ
n₀ n₁ n₂ : ℤ
z : Cochain F G n₀
h₁₂ : n₁ + 1 = 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₀
h₁₂ : n₁ + 1 = 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₂
h₀₁ : ¬n₀ + 1 = n₁
⊢ δ n₁ n₂ (δ n₀ n₁ z) = 0
have neg : Eq.{v + 1} (α := Cochain F G n₂) (δ n₁ n₂ 0) 0
Tactic: rw [δ_shape _ _ h₀₁, δ_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₀ n₁ n₂ : ℤ
z : Cochain F G n₀
h₁₂ : n₁ + 1 = n₂
h₀₁ : ¬n₀ + 1 = n₁
neg : Eq.{v + 1} (α := Cochain F G n₂) (δ n₁ n₂ 0) 0
⊢ δ n₁ n₂ (δ n₀ n₁ z) = 0
have neg₁ : Eq.{v + 1} (α := Cochain F G n₂) 0 0
Tactic: rw [δ_shape _ _ h₀₁, δ_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₀ n₁ n₂ : ℤ
z : Cochain F G n₀
h₁₂ : n₁ + 1 = n₂
h₀₁ : n₀ + 1 = n₁
⊢ δ n₁ n₂ (δ n₀ n₁ z) = 0
have pos : ∀ (p q : ℤ) (hpq : p + n₂ = q), (δ n₁ n₂ (δ n₀ n₁ 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₀ n₁ n₂ : ℤ
z : Cochain F G n₀
h₁₂ : n₁ + 1 = n₂
h₀₁ : n₀ + 1 = n₁
p q : ℤ
hpq : p + n₂ = q
⊢ (δ n₁ n₂ (δ n₀ n₁ z)).v p q hpq = Cochain.v 0 p q hpq
have pos : (δ n₁ n₂ (δ n₀ n₁ z)).v p q hpq = 0
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 n₁ n₂ n₁₂ : ℤ
z₁ : Cochain F G n₁
z₂ : Cochain G K n₂
h : n₁ + n₂ = n₁₂
m₁ m₂ m₁₂ : ℤ
h₁₂ : n₁₂ + 1 = m₁₂
h₁ : n₁ + 1 = m₁
h₂ : n₂ + 1 = m₂
⊢ n₁ + m₂ = m₁₂
have rw : n₁ + m₂ = n₁₂ + 1
Tactic: rw [← h₁₂, ← h₂, ← h, add_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₂
h : n₁ + n₂ = n₁₂
m₁ m₂ m₁₂ : ℤ
h₁₂ : n₁₂ + 1 = m₁₂
h₁ : n₁ + 1 = m₁
h₂ : n₂ + 1 = m₂
rw : n₁ + m₂ = n₁₂ + 1
⊢ n₁ + m₂ = m₁₂
have rw₁ : n₁ + (n₂ + 1) = n₁₂ + 1
Tactic: rw [← h₁₂, ← h₂, ← h, add_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₂
h : n₁ + n₂ = n₁₂
m₁ m₂ m₁₂ : ℤ
h₁₂ : n₁₂ + 1 = m₁₂
h₁ : n₁ + 1 = m₁
h₂ : n₂ + 1 = m₂
rw : n₁ + m₂ = n₁₂ + 1
rw₁ : n₁ + (n₂ + 1) = n₁₂ + 1
⊢ n₁ + m₂ = m₁₂
have rw₂ : n₁ + (n₂ + 1) = n₁ + n₂ + 1
Tactic: rw [← h₁₂, ← h₂, ← h, add_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₂
h : n₁ + n₂ = n₁₂
m₁ m₂ m₁₂ : ℤ
h₁₂ : n₁₂ + 1 = m₁₂
h₁ : n₁ + 1 = m₁
h₂ : n₂ + 1 = m₂
rw : n₁ + m₂ = n₁₂ + 1
rw₁ : n₁ + (n₂ + 1) = n₁₂ + 1
rw₂ : n₁ + (n₂ + 1) = n₁ + n₂ + 1
⊢ n₁ + m₂ = m₁₂
have rw₃ : n₁ + (n₂ + 1) = n₁ + (n₂ + 1)
Tactic: rw [← h₁₂, ← h₂, ← h, add_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₂
h : n₁ + n₂ = n₁₂
m₁ m₂ m₁₂ : ℤ
h₁₂ : n₁₂ + 1 = m₁₂
h₁ : n₁ + 1 = m₁
h₂ : n₂ + 1 = m₂
⊢ m₁ + n₂ = m₁₂
have rw : m₁ + n₂ = n₁₂ + 1
Tactic: rw [← h₁₂, ← h₁, ← h, add_assoc, add_comm 1, add_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₂
h : n₁ + n₂ = n₁₂
m₁ m₂ m₁₂ : ℤ
h₁₂ : n₁₂ + 1 = m₁₂
h₁ : n₁ + 1 = m₁
h₂ : n₂ + 1 = m₂
rw : m₁ + n₂ = n₁₂ + 1
⊢ m₁ + n₂ = m₁₂
have rw₁ : n₁ + 1 + n₂ = n₁₂ + 1
Tactic: rw [← h₁₂, ← h₁, ← h, add_assoc, add_comm 1, add_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₂
h : n₁ + n₂ = n₁₂
m₁ m₂ m₁₂ : ℤ
h₁₂ : n₁₂ + 1 = m₁₂
h₁ : n₁ + 1 = m₁
h₂ : n₂ + 1 = m₂
rw : m₁ + n₂ = n₁₂ + 1
rw₁ : n₁ + 1 + n₂ = n₁₂ + 1
⊢ m₁ + n₂ = m₁₂
have rw₂ : n₁ + 1 + n₂ = n₁ + n₂ + 1
Tactic: rw [← h₁₂, ← h₁, ← h, add_assoc, add_comm 1, add_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₂
h : n₁ + n₂ = n₁₂
m₁ m₂ m₁₂ : ℤ
h₁₂ : n₁₂ + 1 = m₁₂
h₁ : n₁ + 1 = m₁
h₂ : n₂ + 1 = m₂
rw : m₁ + n₂ = n₁₂ + 1
rw₁ : n₁ + 1 + n₂ = n₁₂ + 1
rw₂ : n₁ + 1 + n₂ = n₁ + n₂ + 1
⊢ m₁ + n₂ = m₁₂
have rw₃ : n₁ + (1 + n₂) = n₁ + n₂ + 1
Tactic: rw [← h₁₂, ← h₁, ← h, add_assoc, add_comm 1, add_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₂
h : n₁ + n₂ = n₁₂
m₁ m₂ m₁₂ : ℤ
h₁₂ : n₁₂ + 1 = m₁₂
h₁ : n₁ + 1 = m₁
h₂ : n₂ + 1 = m₂
rw : m₁ + n₂ = n₁₂ + 1
rw₁ : n₁ + 1 + n₂ = n₁₂ + 1
rw₂ : n₁ + 1 + n₂ = n₁ + n₂ + 1
rw₃ : n₁ + (1 + n₂) = n₁ + n₂ + 1
⊢ m₁ + n₂ = m₁₂
have rw₄ : n₁ + (n₂ + 1) = n₁ + n₂ + 1
Tactic: rw [← h₁₂, ← h₁, ← h, add_assoc, add_comm 1, add_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₂
h : n₁ + n₂ = n₁₂
m₁ m₂ m₁₂ : ℤ
h₁₂ : n₁₂ + 1 = m₁₂
h₁ : n₁ + 1 = m₁
h₂ : n₂ + 1 = m₂
rw : m₁ + n₂ = n₁₂ + 1
rw₁ : n₁ + 1 + n₂ = n₁₂ + 1
rw₂ : n₁ + 1 + n₂ = n₁ + n₂ + 1
rw₃ : n₁ + (1 + n₂) = n₁ + n₂ + 1
rw₄ : n₁ + (n₂ + 1) = n₁ + n₂ + 1
⊢ m₁ + n₂ = m₁₂
have rw₅ : n₁ + (n₂ + 1) = n₁ + (n₂ + 1)
Tactic: rw [← h₁₂, ← h₁, ← h, add_assoc, add_comm 1, add_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 : CochainComplex.{v, u, 0} C ℤ
n₁ n₂ n₁₂ : ℤ
z₁ : Cochain F G n₁
z₂ : Cochain G K n₂
h : n₁ + n₂ = n₁₂
m₁ m₂ m₁₂ : ℤ
h₁₂ : n₁₂ + 1 = m₁₂
h₁ : n₁ + 1 = m₁
h₂ : n₂ + 1 = m₂
⊢ δ n₁₂ m₁₂ (z₁.comp z₂ h) = z₁.comp (δ n₂ m₂ z₂) ⋯ + n₂.negOnePow • (δ n₁ m₁ z₁).comp z₂ ⋯
have subst : δ (n₁ + n₂) (n₁ + n₂ + 1) (z₁.comp z₂ sorry) =
  z₁.comp (δ n₂ (n₂ + 1) z₂) sorry + n₂.negOnePow • Cochain.comp (δ n₁ (n₁ + 1) z₁) z₂ sorry
Tactic: subst h₁₂ h₁ h₂ h
Cleared hypotheses: n₁₂, h, m₁, m₂, m₁₂, h₁₂, h₁, 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
F G K : CochainComplex.{v, u, 0} C ℤ
n₁ n₂ : ℤ
z₁ : Cochain F G n₁
z₂ : Cochain G K n₂
⊢ δ (n₁ + n₂) (n₁ + n₂ + 1) (z₁.comp z₂ ⋯) =
    z₁.comp (δ n₂ (n₂ + 1) z₂) ⋯ + n₂.negOnePow • Cochain.comp (δ n₁ (n₁ + 1) z₁) z₂ ⋯
have h : ∀ (p q : ℤ) (hpq : p + (n₁ + n₂ + 1) = q),
  Cochain.v (δ (n₁ + n₂) (n₁ + n₂ + 1) (z₁.comp z₂ sorry)) p q hpq =
    (z₁.comp (δ n₂ (n₂ + 1) z₂) sorry + n₂.negOnePow • Cochain.comp (δ n₁ (n₁ + 1) z₁) z₂ sorry).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₂ : ℤ
z₁ : Cochain F G n₁
z₂ : Cochain G K n₂
p q : ℤ
hpq : p + (n₁ + n₂ + 1) = q
⊢ Cochain.v (δ (n₁ + n₂) (n₁ + n₂ + 1) (z₁.comp z₂ ⋯)) p q hpq =
    (z₁.comp (δ n₂ (n₂ + 1) z₂) ⋯ + n₂.negOnePow • Cochain.comp (δ n₁ (n₁ + 1) z₁) z₂ ⋯).v p q hpq
have h : Cochain.v (δ (n₁ + n₂) (n₁ + n₂ + 1) (z₁.comp z₂ sorry)) p q hpq =
  (z₁.comp (δ n₂ (n₂ + 1) z₂) sorry).v p q hpq + n₂.negOnePow • (Cochain.comp (δ n₁ (n₁ + 1) z₁) z₂ sorry).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 K : CochainComplex.{v, u, 0} C ℤ
n₁ n₂ : ℤ
z₁ : Cochain F G n₁
z₂ : Cochain G K n₂
p q : ℤ
hpq : p + (n₁ + n₂ + 1) = q
⊢ Cochain.v (δ (n₁ + n₂) (n₁ + n₂ + 1) (z₁.comp z₂ ⋯)) p q hpq =
    (z₁.comp (δ n₂ (n₂ + 1) z₂) ⋯).v p q hpq + n₂.negOnePow • (Cochain.comp (δ n₁ (n₁ + 1) z₁) z₂ ⋯).v p q hpq
have h : (z₁.v p (p + n₁) sorry ≫ z₂.v (p + n₁) (p + n₁ + n₂) sorry) ≫ K.d (p + n₁ + n₂) q +
    (n₁ + n₂ + 1).negOnePow • F.d p (p + 1) ≫ z₁.v (p + 1) (p + n₁ + 1) sorry ≫ z₂.v (p + n₁ + 1) q sorry =
  z₁.v p (p + n₁) sorry ≫
      (z₂.v (p + n₁) (p + n₁ + n₂) sorry ≫ K.d (p + n₁ + n₂) q +
        HSMul.hSMul (β := G.X (p + n₁) ⟶ K.X q) (n₂ + 1).negOnePow
          (G.d (p + n₁) (p + n₁ + 1) ≫ z₂.v (p + n₁ + 1) q sorry)) +
    n₂.negOnePow •
      (z₁.v p (p + n₁) sorry ≫ G.d (p + n₁) (p + n₁ + 1) +
          (n₁ + 1).negOnePow • F.d p (p + 1) ≫ z₁.v (p + 1) (p + n₁ + 1) sorry) ≫
        z₂.v (p + n₁ + 1) q sorry
Tactic: rw [z₁.comp_v _ (add_assoc n₁ n₂ 1).symm p _ q rfl (by lia),
    Cochain.comp_v _ _ (show n₁ + 1 + n₂ = n₁ + n₂ + 1 by lia) p (p + n₁ + 1) q
      (by lia) (by lia),
    δ_v (n₁ + n₂) _ rfl (z₁.comp z₂ rfl) p q hpq (p + n₁ + n₂) _ (by lia) rfl,
    z₁.comp_v z₂ rfl p _ _ rfl rfl,
    z₁.comp_v z₂ rfl (p + 1) (p + n₁ + 1) q (by lia) (by lia),
    δ_v n₂ (n₂ + 1) rfl z₂ (p + n₁) q (by lia) (p + n₁ + n₂) _ (by lia) rfl,
    δ_v n₁ (n₁ + 1) rfl z₁ p (p + n₁ + 1) (by lia) (p + n₁) _ (by lia) rfl]
-- 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₂ : ℤ
z₁ : Cochain F G n₁
z₂ : Cochain G K n₂
p q : ℤ
hpq : p + (n₁ + n₂ + 1) = q
⊢ (z₁.v p (p + n₁) ⋯ ≫ z₂.v (p + n₁) (p + n₁ + n₂) ⋯) ≫ K.d (p + n₁ + n₂) q +
      (n₁ + n₂ + 1).negOnePow • F.d p (p + 1) ≫ z₁.v (p + 1) (p + n₁ + 1) ⋯ ≫ z₂.v (p + n₁ + 1) q ⋯ =
    z₁.v p (p + n₁) ⋯ ≫
        (z₂.v (p + n₁) (p + n₁ + n₂) ⋯ ≫ K.d (p + n₁ + n₂) q +
          HSMul.hSMul (β := G.X (p + n₁) ⟶ K.X q) (n₂ + 1).negOnePow
            (G.d (p + n₁) (p + n₁ + 1) ≫ z₂.v (p + n₁ + 1) q ⋯)) +
      n₂.negOnePow •
        (z₁.v p (p + n₁) ⋯ ≫ G.d (p + n₁) (p + n₁ + 1) +
            (n₁ + 1).negOnePow • F.d p (p + 1) ≫ z₁.v (p + 1) (p + n₁ + 1) ⋯) ≫
          z₂.v (p + n₁ + 1) q ⋯
have h : z₁.v p (p + n₁) sorry ≫ z₂.v (p + n₁) (p + n₁ + n₂) sorry ≫ K.d (p + n₁ + n₂) q +
    -((n₂.negOnePow * n₁.negOnePow) • F.d p (p + 1) ≫ z₁.v (p + 1) (p + n₁ + 1) sorry ≫ z₂.v (p + n₁ + 1) q sorry) =
  z₁.v p (p + n₁) sorry ≫ z₂.v (p + n₁) (p + n₁ + n₂) sorry ≫ K.d (p + n₁ + n₂) q +
      -(n₂.negOnePow • z₁.v p (p + n₁) sorry ≫ G.d (p + n₁) (p + n₁ + 1) ≫ z₂.v (p + n₁ + 1) q sorry) +
    (n₂.negOnePow • z₁.v p (p + n₁) sorry ≫ G.d (p + n₁) (p + n₁ + 1) ≫ z₂.v (p + n₁ + 1) q sorry +
      -((n₂.negOnePow * n₁.negOnePow) • F.d p (p + 1) ≫ z₁.v (p + 1) (p + n₁ + 1) sorry ≫ z₂.v (p + n₁ + 1) q sorry))
Tactic: simp only [assoc, comp_add, add_comp, Int.negOnePow_succ, Int.negOnePow_add n₁ n₂,
    Units.neg_smul, comp_neg, neg_comp, smul_neg, smul_smul, Linear.units_smul_comp,
    mul_comm n₁.negOnePow n₂.negOnePow, Linear.comp_units_smul, 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 n₂ : ℤ
z₁ : Cochain F G 0
z₂ : Cochain G K n₂
m₂ : ℤ
h₂ : n₂ + 1 = m₂
rw : n₂ + 1 = m₂
⊢ 1 + n₂ = m₂
have rw₁ : m₂ = m₂
Tactic: rw [add_comm, 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
F G : CochainComplex.{v, u, 0} C ℤ
p : ℤ
φ : F ⟶ G
⊢ δ 0 p (Cochain.ofHom φ) = 0
have pos : ∀ (h : p = 1), δ 0 p (Cochain.ofHom φ) = 0
Tactic: by_cases h : p = 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
F G : CochainComplex.{v, u, 0} C ℤ
p : ℤ
φ : F ⟶ G
pos : ∀ (h : p = 1), δ 0 p (Cochain.ofHom φ) = 0
⊢ δ 0 p (Cochain.ofHom φ) = 0
have neg : ∀ (h : ¬p = 1), δ 0 p (Cochain.ofHom φ) = 0
Tactic: by_cases h : p = 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
F G : CochainComplex.{v, u, 0} C ℤ
p : ℤ
φ : F ⟶ G
h : p = 1
⊢ δ 0 p (Cochain.ofHom φ) = 0
have pos : Eq (α := Cochain F G 1) (δ 0 1 (Cochain.ofHom φ)) 0
Tactic: subst h
Cleared hypotheses: p, 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
F G : CochainComplex.{v, u, 0} C ℤ
φ : F ⟶ G
⊢ Eq (α := Cochain F G 1) (δ 0 1 (Cochain.ofHom φ)) 0
have pos : ∀ (p q : ℤ) (hpq : p + 1 = q), Cochain.v (δ 0 1 (Cochain.ofHom φ)) p q hpq = Cochain.v 0 p q hpq
Tactic: ext
-- 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 ℤ
p : ℤ
φ : F ⟶ G
h : ¬p = 1
⊢ δ 0 p (Cochain.ofHom φ) = 0
have neg : ¬HAdd.hAdd (α := ℤ) 0 1 = p
Tactic: rw [δ_shape]
-- 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 ⟶ G
h : Homotopy φ₁ φ₂
⊢ δ (-1) 0 (Cochain.ofHomotopy h) = Cochain.ofHom φ₁ - Cochain.ofHom φ₂
have h₁ : ∀ (p : ℤ), Cochain.v (δ (-1) 0 (Cochain.ofHomotopy h)) p p sorry = (Cochain.ofHom φ₁ - Cochain.ofHom φ₂).v p p sorry
Tactic: ext p
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplex (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
F G : CochainComplex.{v, u, 0} C ℤ
φ₁ φ₂ : F ⟶ G
h : Homotopy φ₁ φ₂
p : ℤ
⊢ Cochain.v (δ (-1) 0 (Cochain.ofHomotopy h)) p p ⋯ = (Cochain.ofHom φ₁ - Cochain.ofHom φ₂).v p p ⋯
have eq : φ₁.f p =
  HAdd.hAdd (α := F.X p ⟶ G.X p) (β := F.X p ⟶ G.X p)
      ((dNext p : (a : (i j : ℤ) → F.X i ⟶ G.X j) → F.X p ⟶ G.X p) h.hom : F.X p ⟶ G.X p)
      ((prevD p : (a : (i j : ℤ) → F.X i ⟶ G.X j) → F.X p ⟶ G.X p) h.hom : F.X p ⟶ G.X p) +
    φ₂.f p
Tactic: have eq := h.comm p
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplex (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
F G : CochainComplex.{v, u, 0} C ℤ
φ₁ φ₂ : F ⟶ G
h : Homotopy φ₁ φ₂
p : ℤ
eq :
  φ₁.f p =
    HAdd.hAdd (α := F.X p ⟶ G.X p) (β := F.X p ⟶ G.X p)
        ((dNext p : (a : (i j : ℤ) → F.X i ⟶ G.X j) → F.X p ⟶ G.X p) h.hom : F.X p ⟶ G.X p)
        ((prevD p : (a : (i j : ℤ) → F.X i ⟶ G.X j) → F.X p ⟶ G.X p) h.hom : F.X p ⟶ G.X p) +
      φ₂.f p
⊢ Cochain.v (δ (-1) 0 (Cochain.ofHomotopy h)) p p ⋯ = (Cochain.ofHom φ₁ - Cochain.ofHom φ₂).v p p ⋯
have eq₁ : φ₁.f p =
  CategoryStruct.comp (Y := F.X (p + 1)) (F.d p (p + 1)) (h.hom (p + 1) p) +
      CategoryStruct.comp (Y := G.X (p - 1)) (h.hom p (p - 1)) (G.d (p - 1) p) +
    φ₂.f p
Tactic: rw [dNext_eq h.hom (show (ComplexShape.up ℤ).Rel p (p + 1) by simp),
    prevD_eq h.hom (show (ComplexShape.up ℤ).Rel (p - 1) p by simp)] at eq
Cleared hypotheses: eq
-- 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 ⟶ G
h : Homotopy φ₁ φ₂
p : ℤ
eq :
  φ₁.f p =
    CategoryStruct.comp (Y := F.X (p + 1)) (F.d p (p + 1)) (h.hom (p + 1) p) +
        CategoryStruct.comp (Y := G.X (p - 1)) (h.hom p (p - 1)) (G.d (p - 1) p) +
      φ₂.f p
⊢ Cochain.v (δ (-1) 0 (Cochain.ofHomotopy h)) p p ⋯ = (Cochain.ofHom φ₁ - Cochain.ofHom φ₂).v p p ⋯
have h₁ : Cochain.v (Cochain.mk fun (p q : ℤ) (x : p + -1 = q) ↦ h.hom p q) p (p - 1) sorry ≫ G.d (p - 1) p +
    HSMul.hSMul (β := F.X p ⟶ G.X p) (Int.negOnePow 0)
      (F.d p (p + 1) ≫ Cochain.v (Cochain.mk fun (p q : ℤ) (x : p + -1 = q) ↦ h.hom p q) (p + 1) p sorry) =
  (Cochain.ofHom φ₁ - Cochain.ofHom φ₂).v p p sorry
Tactic: rw [Cochain.ofHomotopy, δ_v (-1) 0 (neg_add_cancel 1) _ p p (add_zero p) (p - 1) (p + 1) rfl rfl]
-- 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 ⟶ G
h : Homotopy φ₁ φ₂
p : ℤ
eq :
  φ₁.f p =
    CategoryStruct.comp (Y := F.X (p + 1)) (F.d p (p + 1)) (h.hom (p + 1) p) +
        CategoryStruct.comp (Y := G.X (p - 1)) (h.hom p (p - 1)) (G.d (p - 1) p) +
      φ₂.f p
⊢ Cochain.v (Cochain.mk fun (p q : ℤ) (x : p + -1 = q) ↦ h.hom p q) p (p - 1) ⋯ ≫ G.d (p - 1) p +
      HSMul.hSMul (β := F.X p ⟶ G.X p) (Int.negOnePow 0)
        (F.d p (p + 1) ≫ Cochain.v (Cochain.mk fun (p q : ℤ) (x : p + -1 = q) ↦ h.hom p q) (p + 1) p ⋯) =
    (Cochain.ofHom φ₁ - Cochain.ofHom φ₂).v p p ⋯
have h₁ : CategoryStruct.comp (Y := G.X (p - 1)) (h.hom p (p - 1)) (G.d (p - 1) p) +
    CategoryStruct.comp (Y := F.X (p + 1)) (F.d p (p + 1)) (h.hom (p + 1) p) =
  CategoryStruct.comp (Y := F.X (p + 1)) (F.d p (p + 1)) (h.hom (p + 1) p) +
        CategoryStruct.comp (Y := G.X (p - 1)) (h.hom p (p - 1)) (G.d (p - 1) p) +
      φ₂.f p -
    φ₂.f p
Tactic: simp only [Cochain.mk_v, one_smul, Int.negOnePow_zero, Cochain.sub_v, Cochain.ofHom_v, eq]
-- 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 (-1)
i j : ℤ
hij : j + 1 = i
⊢ i + -1 = j
have rw : j + 1 + -1 = j
Tactic: rw [← hij, add_neg_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 : ℤ
z : Cochain F G (-1)
i j : ℤ
hij : j + 1 = i
rw : j + 1 + -1 = j
⊢ i + -1 = j
have rw₁ : j = j
Tactic: rw [← hij, add_neg_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
F G : CochainComplex.{v, u, 0} C ℤ
z : Cochain F G (-1)
⊢ δ (-1) 0 z = Cochain.ofHom (Homotopy.nullHomotopicMap' fun (i j : ℤ) (hij : (ComplexShape.up ℤ).Rel j i) ↦ z.v i j ⋯)
have h : ∀ (p : ℤ),
  Cochain.v (δ (-1) 0 z) p p sorry =
    Cochain.v (Cochain.ofHom (Homotopy.nullHomotopicMap' fun (i j : ℤ) (hij : (ComplexShape.up ℤ).Rel j i) ↦ z.v i j sorry))
      p p sorry
Tactic: ext 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
F G : CochainComplex.{v, u, 0} C ℤ
z : Cochain F G (-1)
p : ℤ
⊢ Cochain.v (δ (-1) 0 z) p p ⋯ =
    Cochain.v (Cochain.ofHom (Homotopy.nullHomotopicMap' fun (i j : ℤ) (hij : (ComplexShape.up ℤ).Rel j i) ↦ z.v i j ⋯))
      p p ⋯
have h : z.v p (p - 1) sorry ≫ G.d (p - 1) p + Int.negOnePow 0 • F.d p (p + 1) ≫ z.v (p + 1) p sorry =
  Cochain.v (Cochain.ofHom (Homotopy.nullHomotopicMap' fun (i j : ℤ) (hij : (ComplexShape.up ℤ).Rel j i) ↦ z.v i j sorry)) p
    p sorry
Tactic: rw [δ_v (-1) 0 (neg_add_cancel 1) _ p p (add_zero p) (p - 1) (p + 1) rfl rfl]
-- 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 ℤ
z : Cochain F G (-1)
p : ℤ
⊢ z.v p (p - 1) ⋯ ≫ G.d (p - 1) p + Int.negOnePow 0 • F.d p (p + 1) ≫ z.v (p + 1) p ⋯ =
    Cochain.v (Cochain.ofHom (Homotopy.nullHomotopicMap' fun (i j : ℤ) (hij : (ComplexShape.up ℤ).Rel j i) ↦ z.v i j ⋯))
      p p ⋯
have h : z.v p (p - 1) sorry ≫ G.d (p - 1) p + F.d p (p + 1) ≫ z.v (p + 1) p sorry =
  HomologicalComplex.Hom.f (Homotopy.nullHomotopicMap' fun (i j : ℤ) (hij : (ComplexShape.up ℤ).Rel j i) ↦ z.v i j sorry) p
Tactic: simp only [one_smul, Cochain.ofHom_v, Int.negOnePow_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 ℤ
z : Cochain F G (-1)
p : ℤ
⊢ z.v p (p - 1) ⋯ ≫ G.d (p - 1) p + F.d p (p + 1) ≫ z.v (p + 1) p ⋯ =
    HomologicalComplex.Hom.f (Homotopy.nullHomotopicMap' fun (i j : ℤ) (hij : (ComplexShape.up ℤ).Rel j i) ↦ z.v i j ⋯)
      p
have h : z.v p (p - 1) sorry ≫ G.d (p - 1) p + F.d p (p + 1) ≫ z.v (p + 1) p sorry =
  CategoryStruct.comp (Y := F.X (p + 1)) (F.d p (p + 1)) (z.v (p + 1) p sorry) +
    CategoryStruct.comp (Y := G.X (p - 1)) (z.v p (p - 1) sorry) (G.d (p - 1) p)
Tactic: rw [Homotopy.nullHomotopicMap'_f (show (ComplexShape.up ℤ).Rel (p - 1) p by simp)
    (show (ComplexShape.up ℤ).Rel p (p + 1) by simp)]
-- 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 x x_1 : ℤ
hij : ¬(ComplexShape.up ℤ).Rel x x_1
⊢ Eq (α := AddCommGrpCat.of (Cochain F G x) ⟶ AddCommGrpCat.of (Cochain F G x_1))
    (AddCommGrpCat.ofHom (↑(δ_hom ℤ F G x x_1) : Cochain F G x →+ Cochain F G x_1)) 0
have hf : ∀ (x_2 : (↑(AddCommGrpCat.of (Cochain F G x)) : Type v)) (p q : ℤ) (hpq : p + x_1 = q),
  Eq.{v + 1} (α := F.X p ⟶ G.X q)
    (Cochain.v
      ((AddCommGrpCat.Hom.hom (AddCommGrpCat.ofHom (↑(δ_hom ℤ F G x x_1) : Cochain F G x →+ Cochain F G x_1)) :
          (a : (↑(AddCommGrpCat.of (Cochain F G x)) : Type v)) → (↑(AddCommGrpCat.of (Cochain F G x_1)) : Type v))
        x_2)
      p q hpq)
    (Cochain.v
      ((AddCommGrpCat.Hom.hom 0 :
          (a : (↑(AddCommGrpCat.of (Cochain F G x)) : Type v)) → (↑(AddCommGrpCat.of (Cochain F G x_1)) : Type v))
        x_2)
      p q hpq)
Tactic: ext