awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
F G K : CochainComplex.{v, u, 0} C ℤ
f : F ⟶ G
g : G ⟶ K
⊢ ofHom (f ≫ g) = (ofHom f).comp (ofHom g) ⋯

Tactic:
simp only [ofHom, HomologicalComplex.comp_f, ofHoms_comp]

Premises used: CochainComplex.HomComplex.Cochain.ofHoms_comp, HomologicalComplex.comp_f, CochainComplex.HomComplex.Cochain.ofHom
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K : CochainComplex.{v, u, 0} C ℤ
p q : ℤ
hpq : p + 1 = q
⊢ (diff K).v p q hpq = K.d p q

Tactic:
rfl

Premises used: CochainComplex.HomComplex.Cochain.diff, CochainComplex.HomComplex.Cochain.mk, CochainComplex.HomComplex.Cochain.v, rfl
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
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
rw₁ rw₂ : q = q
⊢ p + m - n + n = q

Tactic:
rw [hpq, sub_add_cancel]

Premises used: sub_add_cancel
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
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
rw₄ rw₅ : p + n = p + n
⊢ p + n = q₁

Tactic:
rw [hq₁, ← hpq, ← hnm, ← add_assoc, add_sub_cancel_right]

Premises used: add_assoc, add_sub_cancel_right
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
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
rw₄ rw₅ : q = q
⊢ q₂ + n = q

Tactic:
rw [← hq₂, add_assoc, add_comm 1, hnm, hpq]

Premises used: add_assoc, add_comm, OfNat.ofNat
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
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₂
⊢ q₁ = p + n

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
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₂
obtain :
  ∀ (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 ⋯
⊢ (δ 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 ⋯

Tactic:
obtain rfl : q₁ = p + n := by lia

Premises used: rfl
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
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
⊢ q₂ = p + m - n

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
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
obtain :
  ∀ (hq₂ : p + 1 = p + m - n),
    (δ n m z).v p q hpq = z.v p (p + n) ⋯ ≫ G.d (p + n) q + m.negOnePow • F.d p (p + m - n) ≫ z.v (p + m - n) q ⋯
⊢ (δ 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 ⋯

Tactic:
obtain rfl : q₂ = p + m - n := by lia

Premises used: rfl
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
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
hq₁ : p + n = q - 1
hq₂ : p + 1 = p + m - n
⊢ (δ n m z).v p q hpq = z.v p (p + n) ⋯ ≫ G.d (p + n) q + m.negOnePow • F.d p (p + m - n) ≫ z.v (p + m - n) q ⋯

Tactic:
rfl
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
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
h : ∀ (p q : ℤ) (hpq : p + m = q), (δ n m z).v p q hpq = Cochain.v 0 p q hpq
⊢ δ n m z = 0

Tactic:
ext p q hpq
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
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
h₁ : ¬(ComplexShape.up ℤ).Rel p (p + m - n)
⊢ 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)

Tactic:
rw [Cochain.mk_v, Cochain.zero_v, F.shape, G.shape, comp_zero, zero_add, zero_comp, smul_zero]

Premises used: CategoryTheory.Limits.comp_zero, CochainComplex.HomComplex.Cochain.zero_v, smul_zero, zero_add, CategoryTheory.Limits.zero_comp, CochainComplex.HomComplex.Cochain.mk_v, HomologicalComplex.shape
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
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 : p + n + 1 = q
⊢ n + 1 = m

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
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
⊢ ¬p + n + 1 = q

Tactic:
exact fun _ => hnm (by lia)
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
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 : p + 1 = p + m - n
⊢ n + 1 = m

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
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
⊢ ¬p + 1 = p + m - n

Tactic:
exact fun _ => hnm (by lia)
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
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 β
neg : ∀ (h : ¬n + 1 = m), δ n m (α + β) = δ n m α + δ n m β
⊢ δ n m (α + β) = δ n m α + δ n m β

Tactic:
by_cases h : n + 1 = m
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
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
pos : ∀ (p q : ℤ) (hpq : p + m = q), (δ n m (α + β)).v p q hpq = (δ n m α + δ n m β).v p q hpq
⊢ δ n m (α + β) = δ n m α + δ n m β

Tactic:
ext p q hpq
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
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
pos : (δ n m (α + β)).v p q hpq = (δ n m α).v p q hpq + (δ n m β).v p q hpq
⊢ (δ n m (α + β)).v p q hpq = (δ n m α + δ n m β).v p q hpq

Tactic:
dsimp
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
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
pos :
  α.v p (q - 1) ⋯ ≫ G.d (q - 1) q + β.v p (q - 1) ⋯ ≫ G.d (q - 1) q +
      (m.negOnePow • F.d p (p + 1) ≫ α.v (p + 1) q ⋯ + m.negOnePow • F.d p (p + 1) ≫ β.v (p + 1) q ⋯) =
    α.v p (q - 1) ⋯ ≫ G.d (q - 1) q + m.negOnePow • F.d p (p + 1) ≫ α.v (p + 1) q ⋯ +
      (β.v p (q - 1) ⋯ ≫ G.d (q - 1) q + m.negOnePow • F.d p (p + 1) ≫ β.v (p + 1) q ⋯)
⊢ (δ n m (α + β)).v p q hpq = (δ n m α).v p q hpq + (δ n m β).v p q hpq

Tactic:
simp only [δ_v n m h _ p q hpq _ _ rfl rfl, Cochain.add_v, add_comp, comp_add, smul_add]

Premises used: CochainComplex.HomComplex.δ_v, CategoryTheory.Preadditive.add_comp, CategoryTheory.Preadditive.comp_add, CochainComplex.HomComplex.Cochain.add_v, smul_add, rfl
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
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
⊢ α.v p (q - 1) ⋯ ≫ G.d (q - 1) q + β.v p (q - 1) ⋯ ≫ G.d (q - 1) q +
      (m.negOnePow • F.d p (p + 1) ≫ α.v (p + 1) q ⋯ + m.negOnePow • F.d p (p + 1) ≫ β.v (p + 1) q ⋯) =
    α.v p (q - 1) ⋯ ≫ G.d (q - 1) q + m.negOnePow • F.d p (p + 1) ≫ α.v (p + 1) q ⋯ +
      (β.v p (q - 1) ⋯ ≫ G.d (q - 1) q + m.negOnePow • F.d p (p + 1) ≫ β.v (p + 1) q ⋯)

Tactic:
abel
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
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 β

Tactic:
simp only [δ_shape _ _ h, add_zero]

Premises used: CochainComplex.HomComplex.δ_shape, add_zero
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
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)
neg : ∀ (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)

Tactic:
by_cases h : n + 1 = m
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
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
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
⊢ δ n m (r • a) = HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) r : R) (δ n m a)

Tactic:
ext p q hpq
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
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
pos : (δ n m (r • a)).v p q hpq = r • (δ n m a).v p q hpq
⊢ (δ 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:
dsimp
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
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 = r • (δ n m a).v p q hpq

Tactic:
simp only [δ_v n m h _ p q hpq _ _ rfl rfl, Cochain.smul_v, Linear.comp_smul,
        Linear.smul_comp, smul_add, smul_comm m.negOnePow r]

Premises used: CochainComplex.HomComplex.δ_v, CategoryTheory.Linear.comp_smul, CochainComplex.HomComplex.Cochain.smul_v, SMulCommClass.smul_comm, smul_add, Int.negOnePow, rfl, CategoryTheory.Linear.smul_comp
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
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)

Tactic:
simp only [δ_shape _ _ h, smul_zero]

Premises used: smul_zero, CochainComplex.HomComplex.δ_shape
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
F G : CochainComplex.{v, u, 0} C ℤ
n m : ℤ
z₁ z₂ : Cochain F G n
⊢ δ n m (z₁ + z₂) = δ n m z₁ + δ n m z₂

Tactic:
(δ_hom ℤ F G n m).map_add z₁ z₂

Premises used: LinearMap.map_add, CochainComplex.HomComplex.Cochain.mk, Int, CochainComplex.HomComplex.δ, CochainComplex.HomComplex.δ_hom
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
F G : CochainComplex.{v, u, 0} C ℤ
n m : ℤ
z₁ z₂ : Cochain F G n
⊢ δ n m (z₁ - z₂) = δ n m z₁ - δ n m z₂

Tactic:
(δ_hom ℤ F G n m).map_sub z₁ z₂

Premises used: CochainComplex.HomComplex.Cochain.mk, Int, CochainComplex.HomComplex.δ, LinearMap.map_sub, CochainComplex.HomComplex.δ_hom
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
F G : CochainComplex.{v, u, 0} C ℤ
n m : ℤ
⊢ Eq.{v + 1} (α := Cochain F G m) (δ n m 0) 0

Tactic:
(δ_hom ℤ F G n m).map_zero

Premises used: CochainComplex.HomComplex.Cochain.mk, LinearMap.map_zero, Int, CochainComplex.HomComplex.δ, CochainComplex.HomComplex.δ_hom
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
F G : CochainComplex.{v, u, 0} C ℤ
n m : ℤ
z : Cochain F G n
⊢ δ n m (-z) = -δ n m z

Tactic:
(δ_hom ℤ F G n m).map_neg z

Premises used: LinearMap.map_neg, CochainComplex.HomComplex.Cochain.mk, Int, CochainComplex.HomComplex.δ, CochainComplex.HomComplex.δ_hom
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
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 : CochainComplex.{v, u, 0} C ℤ
n m : ℤ
k : R
z : Cochain F G n
⊢ δ n m (k • z) = k • δ n m z

Tactic:
(δ_hom R F G n m).map_smul k z

Premises used: CochainComplex.HomComplex.Cochain.mk, CochainComplex.HomComplex.δ, LinearMap.map_smul, CochainComplex.HomComplex.δ_hom
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
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 : CochainComplex.{v, u, 0} C ℤ
n m : ℤ
k : Rˣ
z : Cochain F G n
⊢ δ n m (k • z) = k • δ n m z

Tactic:
δ_smul ..

Premises used: CochainComplex.HomComplex.δ_smul
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
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
neg : ∀ (h₁₂ : ¬n₁ + 1 = n₂), δ n₁ n₂ (δ n₀ n₁ z) = 0
⊢ δ n₁ n₂ (δ n₀ n₁ z) = 0

Tactic:
by_cases h₁₂ : n₁ + 1 = n₂
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
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₂
neg neg₁ : Eq.{v + 1} (α := Cochain F G n₂) 0 0
⊢ δ n₁ n₂ (δ n₀ n₁ z) = 0

Tactic:
rw [δ_shape _ _ h₁₂]

Premises used: CochainComplex.HomComplex.δ_shape
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
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
neg : ∀ (h₀₁ : ¬n₀ + 1 = n₁), δ n₁ n₂ (δ n₀ n₁ z) = 0
⊢ δ n₁ n₂ (δ n₀ n₁ z) = 0

Tactic:
by_cases h₀₁ : n₀ + 1 = n₁
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
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
neg₁ neg₂ : Eq.{v + 1} (α := Cochain F G n₂) 0 0
⊢ δ n₁ n₂ (δ n₀ n₁ z) = 0

Tactic:
rw [δ_shape _ _ h₀₁, δ_zero]

Premises used: CochainComplex.HomComplex.δ_zero, CochainComplex.HomComplex.δ_shape
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
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₁
pos : ∀ (p q : ℤ) (hpq : p + n₂ = q), (δ n₁ n₂ (δ n₀ n₁ z)).v p q hpq = Cochain.v 0 p q hpq
⊢ δ n₁ n₂ (δ n₀ n₁ z) = 0

Tactic:
ext p q hpq
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
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
pos : (δ n₁ n₂ (δ n₀ n₁ z)).v p q hpq = 0
⊢ (δ n₁ n₂ (δ n₀ n₁ z)).v p q hpq = Cochain.v 0 p q hpq

Tactic:
dsimp
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
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
⊢ p + n₁ = q - 1

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
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
⊢ q - 2 = q - 1 - 1

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
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
⊢ p + 1 + n₁ = q

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
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
⊢ p + 1 + 1 = p + 2

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
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 = 0

Tactic:
simp only [δ_v n₁ n₂ h₁₂ _ p q hpq _ _ rfl rfl,
    δ_v n₀ n₁ h₀₁ z p (q - 1) (by lia) (q - 2) _ (by lia) rfl,
    δ_v n₀ n₁ h₀₁ z (p + 1) q (by lia) _ (p + 2) rfl (by lia),
    ← h₁₂, Int.negOnePow_succ, add_comp, assoc,
    HomologicalComplex.d_comp_d, comp_zero, zero_add, comp_add,
    HomologicalComplex.d_comp_d_assoc, zero_comp, smul_zero,
    add_zero, add_neg_cancel, Units.neg_smul,
    Linear.units_smul_comp, Linear.comp_units_smul]

Premises used: CategoryTheory.Category.assoc, add_neg_cancel, CochainComplex.HomComplex.δ_v, HomologicalComplex.d_comp_d_assoc, CategoryTheory.Linear.units_smul_comp, HSub.hSub, CategoryTheory.Limits.comp_zero, smul_zero, CategoryTheory.Linear.comp_units_smul, zero_add, CategoryTheory.Preadditive.add_comp, Units.neg_smul, HAdd.hAdd, CategoryTheory.Preadditive.comp_add, HomologicalComplex.d_comp_d, CategoryTheory.Limits.zero_comp, add_zero, OfNat.ofNat, Int.negOnePow_succ, rfl
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
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
rw₃ rw₄ : n₁ + (n₂ + 1) = n₁ + (n₂ + 1)
⊢ n₁ + m₂ = m₁₂

Tactic:
rw [← h₁₂, ← h₂, ← h, add_assoc]

Premises used: add_assoc
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
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
rw₅ rw₆ : n₁ + (n₂ + 1) = n₁ + (n₂ + 1)
⊢ m₁ + n₂ = m₁₂

Tactic:
rw [← h₁₂, ← h₁, ← h, add_assoc, add_comm 1, add_assoc]

Premises used: add_assoc, add_comm, OfNat.ofNat
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
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₂
subst :
  δ (n₁ + n₂) (n₁ + n₂ + 1) (z₁.comp z₂ ⋯) =
    z₁.comp (δ n₂ (n₂ + 1) z₂) ⋯ + n₂.negOnePow • Cochain.comp (δ n₁ (n₁ + 1) z₁) z₂ ⋯
⊢ δ n₁₂ m₁₂ (z₁.comp z₂ h) = z₁.comp (δ n₂ m₂ z₂) ⋯ + n₂.negOnePow • (δ n₁ m₁ z₁).comp z₂ ⋯

Tactic:
subst h₁₂ h₁ h₂ h
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
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₂
h :
  ∀ (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
⊢ δ (n₁ + n₂) (n₁ + n₂ + 1) (z₁.comp z₂ ⋯) =
    z₁.comp (δ n₂ (n₂ + 1) z₂) ⋯ + n₂.negOnePow • Cochain.comp (δ n₁ (n₁ + 1) z₁) z₂ ⋯

Tactic:
ext p q hpq
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
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
h :
  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
⊢ 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

Tactic:
dsimp
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
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
⊢ p + n₁ + (n₂ + 1) = q

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
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
⊢ n₁ + 1 + n₂ = n₁ + n₂ + 1

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
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
⊢ p + (n₁ + 1) = p + n₁ + 1

Tactic:
lia