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 ℤ
n₁ n₂ : ℤ
z₁ : Cochain F G n₁
z₂ : Cochain G K n₂
p q : ℤ
hpq : p + (n₁ + n₂ + 1) = q
⊢ p + n₁ + 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 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₂ = 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 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 + 1 + n₁ = p + 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₁ = p + n₁ + 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 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 :
  (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 ⋯
⊢ 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

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]

Premises used: CochainComplex.HomComplex.Cochain.comp, CochainComplex.HomComplex.δ_v, CochainComplex.HomComplex.Cochain.comp_v, add_assoc, HAdd.hAdd, OfNat.ofNat, Eq.symm, rfl
-- 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 :
  z₁.v p (p + n₁) ⋯ ≫ z₂.v (p + n₁) (p + n₁ + n₂) ⋯ ≫ K.d (p + n₁ + n₂) q +
      -((n₂.negOnePow * n₁.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 +
        -(n₂.negOnePow • z₁.v p (p + n₁) ⋯ ≫ 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) ≫ z₂.v (p + n₁ + 1) q ⋯ +
        -((n₂.negOnePow * n₁.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 +
      (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 ⋯

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]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Linear.units_smul_comp, CategoryTheory.Preadditive.comp_neg, smul_smul, Int.negOnePow_add, smul_neg, CategoryTheory.Linear.comp_units_smul, CategoryTheory.Preadditive.add_comp, Units.neg_smul, CategoryTheory.Preadditive.comp_add, CategoryTheory.Preadditive.neg_comp, mul_comm, Int.negOnePow_succ, smul_add, Int.negOnePow
-- 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
⊢ z₁.v p (p + n₁) ⋯ ≫ z₂.v (p + n₁) (p + n₁ + n₂) ⋯ ≫ K.d (p + n₁ + n₂) q +
      -((n₂.negOnePow * n₁.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 +
        -(n₂.negOnePow • z₁.v p (p + n₁) ⋯ ≫ 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) ≫ z₂.v (p + n₁ + 1) q ⋯ +
        -((n₂.negOnePow * n₁.negOnePow) • F.d p (p + 1) ≫ z₁.v (p + 1) (p + n₁ + 1) ⋯ ≫ z₂.v (p + n₁ + 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 n₂ : ℤ
z₁ : Cochain F G 0
z₂ : Cochain G K n₂
m₂ : ℤ
h₂ : n₂ + 1 = m₂
rw : n₂ + 1 = m₂
rw₁ rw₂ : m₂ = m₂
⊢ 1 + n₂ = m₂

Tactic:
rw [add_comm, h₂]

Premises used: add_comm
-- 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₂ : ℤ
z₁ : Cochain F G 0
z₂ : Cochain G K n₂
m₂ : ℤ
h₂ : n₂ + 1 = m₂
⊢ δ n₂ m₂ (z₁.comp z₂ ⋯) = z₁.comp (δ n₂ m₂ z₂) ⋯ + n₂.negOnePow • Cochain.comp (δ 0 1 z₁) z₂ ⋯

Tactic:
δ_comp z₁ z₂ (zero_add n₂) 1 m₂ m₂ h₂ (zero_add 1) h₂

Premises used: CochainComplex.HomComplex.δ_comp, zero_add, 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₁ : ℤ
z₁ : Cochain F G n₁
z₂ : Cochain G K 0
m₁ : ℤ
h₁ : n₁ + 1 = m₁
⊢ δ n₁ m₁ (z₁.comp z₂ ⋯) = z₁.comp (δ 0 1 z₂) h₁ + (δ n₁ m₁ z₁).comp z₂ ⋯

Tactic:
simp only [δ_comp z₁ z₂ (add_zero n₁) m₁ 1 m₁ h₁ h₁ (zero_add 1), one_smul,
    Int.negOnePow_zero]

Premises used: CochainComplex.HomComplex.δ_comp, zero_add, one_smul, Int.negOnePow_zero, add_zero, 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 ℤ
z : Cochain F G 0
p q : ℤ
hpq : p + 1 = q
⊢ p = 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 ℤ
z : Cochain F G 0
p q : ℤ
hpq : p + 1 = q
⊢ Cochain.v (δ 0 1 z) p q hpq = z.v p p ⋯ ≫ G.d p q - F.d p q ≫ z.v q q ⋯

Tactic:
simp only [δ_v 0 1 (zero_add 1) z p q hpq p q (by lia) hpq, Int.negOnePow_one, Units.neg_smul,
    one_smul, sub_eq_add_neg]

Premises used: CochainComplex.HomComplex.δ_v, sub_eq_add_neg, Int.negOnePow_one, zero_add, one_smul, Units.neg_smul, 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 ℤ
p : ℤ
φ : F ⟶ G
pos : ∀ (h : p = 1), δ 0 p (Cochain.ofHom φ) = 0
neg : ∀ (h : ¬p = 1), δ 0 p (Cochain.ofHom φ) = 0
⊢ δ 0 p (Cochain.ofHom φ) = 0

Tactic:
by_cases h : p = 1
-- 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 ℤ
p : ℤ
φ : F ⟶ G
h : p = 1
pos : Eq (α := Cochain F G 1) (δ 0 1 (Cochain.ofHom φ)) 0
⊢ δ 0 p (Cochain.ofHom φ) = 0

Tactic:
subst h
-- 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 ℤ
φ : F ⟶ G
pos : ∀ (p q : ℤ) (hpq : p + 1 = q), Cochain.v (δ 0 1 (Cochain.ofHom φ)) p q hpq = Cochain.v 0 p q hpq
⊢ Eq (α := Cochain F G 1) (δ 0 1 (Cochain.ofHom φ)) 0

Tactic:
ext
-- 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 ℤ
φ : F ⟶ G
p q : ℤ
hpq : p + 1 = q
⊢ Cochain.v (δ 0 1 (Cochain.ofHom φ)) p q hpq = Cochain.v 0 p q hpq

Tactic:
simp
-- 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 ℤ
p : ℤ
φ : F ⟶ G
h : ¬p = 1
neg : ¬HAdd.hAdd (α := ℤ) 0 1 = p
⊢ δ 0 p (Cochain.ofHom φ) = 0

Tactic:
rw [δ_shape]

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 ℤ
p : ℤ
φ : F ⟶ G
h : ¬p = 1
⊢ ¬HAdd.hAdd (α := ℤ) 0 1 = p

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 ℤ
φ₁ φ₂ : F ⟶ G
h : Homotopy φ₁ φ₂
h₁ : ∀ (p : ℤ), Cochain.v (δ (-1) 0 (Cochain.ofHomotopy h)) p p ⋯ = (Cochain.ofHom φ₁ - Cochain.ofHom φ₂).v p p ⋯
⊢ δ (-1) 0 (Cochain.ofHomotopy h) = Cochain.ofHom φ₁ - Cochain.ofHom φ₂

Tactic:
ext p
-- 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 ℤ
φ₁ φ₂ : F ⟶ G
h : Homotopy φ₁ φ₂
p : ℤ
⊢ φ₁.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
-- 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 ℤ
φ₁ φ₂ : 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
⊢ (ComplexShape.up ℤ).Rel p (p + 1)

Tactic:
simp
-- 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 ℤ
φ₁ φ₂ : F ⟶ G
h : Homotopy φ₁ φ₂
p : ℤ
eq :
  φ₁.f p =
    HAdd.hAdd (β := F.X p ⟶ G.X p) (CategoryStruct.comp (Y := F.X (p + 1)) (F.d p (p + 1)) (h.hom (p + 1) 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
⊢ (ComplexShape.up ℤ).Rel (p - 1) p

Tactic:
simp
-- 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 ℤ
φ₁ φ₂ : 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
⊢ φ₁.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

Premises used: Homotopy.hom, prevD_eq, dNext_eq
-- 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 ℤ
φ₁ φ₂ : 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
h₁ :
  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 ⋯
⊢ Cochain.v (δ (-1) 0 (Cochain.ofHomotopy h)) p p ⋯ = (Cochain.ofHom φ₁ - Cochain.ofHom φ₂).v p p ⋯

Tactic:
rw [Cochain.ofHomotopy, δ_v (-1) 0 (neg_add_cancel 1) _ p p (add_zero p) (p - 1) (p + 1) rfl rfl]

Premises used: CochainComplex.HomComplex.δ_v, HSub.hSub, neg_add_cancel, HAdd.hAdd, add_zero, OfNat.ofNat, Neg.neg, rfl, CochainComplex.HomComplex.Cochain.ofHomotopy
-- 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 ℤ
φ₁ φ₂ : 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
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
⊢ 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 ⋯

Tactic:
simp only [Cochain.mk_v, one_smul, Int.negOnePow_zero, Cochain.sub_v, Cochain.ofHom_v, eq]

Premises used: CochainComplex.HomComplex.Cochain.sub_v, CochainComplex.HomComplex.Cochain.ofHom_v, one_smul, Int.negOnePow_zero, CochainComplex.HomComplex.Cochain.mk_v
-- 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 ℤ
φ₁ φ₂ : 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
⊢ 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:
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 : ℤ
z : Cochain F G (-1)
i j : ℤ
hij : j + 1 = i
rw : j + 1 + -1 = j
rw₁ rw₂ : j = j
⊢ i + -1 = j

Tactic:
rw [← hij, add_neg_cancel_right]

Premises used: add_neg_cancel_right
-- 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 ℤ
z : Cochain F G (-1)
h :
  ∀ (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 ⋯
⊢ δ (-1) 0 z = Cochain.ofHom (Homotopy.nullHomotopicMap' fun (i j : ℤ) (hij : (ComplexShape.up ℤ).Rel j i) ↦ z.v i j ⋯)

Tactic:
ext p
-- 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 ℤ
z : Cochain F G (-1)
p : ℤ
h :
  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 ⋯
⊢ 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 ⋯

Tactic:
rw [δ_v (-1) 0 (neg_add_cancel 1) _ p p (add_zero p) (p - 1) (p + 1) rfl rfl]

Premises used: CochainComplex.HomComplex.δ_v, HSub.hSub, neg_add_cancel, HAdd.hAdd, add_zero, OfNat.ofNat, Neg.neg, 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 ℤ
z : Cochain F G (-1)
p : ℤ
h :
  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
⊢ 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 ⋯

Tactic:
simp only [one_smul, Cochain.ofHom_v, Int.negOnePow_zero]

Premises used: CochainComplex.HomComplex.Cochain.ofHom_v, one_smul, Int.negOnePow_zero
-- 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 ℤ
z : Cochain F G (-1)
p : ℤ
⊢ (ComplexShape.up ℤ).Rel (p - 1) p

Tactic:
simp
-- 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 ℤ
z : Cochain F G (-1)
p : ℤ
⊢ (ComplexShape.up ℤ).Rel p (p + 1)

Tactic:
simp
-- 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 ℤ
z : Cochain F G (-1)
p : ℤ
h :
  z.v p (p - 1) ⋯ ≫ G.d (p - 1) p + F.d p (p + 1) ≫ z.v (p + 1) p ⋯ =
    CategoryStruct.comp (Y := F.X (p + 1)) (F.d p (p + 1)) (z.v (p + 1) p ⋯) +
      CategoryStruct.comp (Y := G.X (p - 1)) (z.v p (p - 1) ⋯) (G.d (p - 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

Tactic:
rw [Homotopy.nullHomotopicMap'_f (show (ComplexShape.up ℤ).Rel (p - 1) p by simp)
    (show (ComplexShape.up ℤ).Rel p (p + 1) by simp)]

Premises used: Homotopy.nullHomotopicMap'_f
-- 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 ℤ
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 ⋯ =
    CategoryStruct.comp (Y := F.X (p + 1)) (F.d p (p + 1)) (z.v (p + 1) p ⋯) +
      CategoryStruct.comp (Y := G.X (p - 1)) (z.v p (p - 1) ⋯) (G.d (p - 1) p)

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 x x_1 : ℤ
hij : ¬(ComplexShape.up ℤ).Rel x x_1
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)
⊢ 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

Tactic:
ext
-- 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 x x_1 : ℤ
hij : ¬(ComplexShape.up ℤ).Rel x x_1
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:
simp [δ_shape _ _ hij]

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
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 x_2 : ℤ
h : (ComplexShape.up ℤ).Rel x x_1
h_1 : (ComplexShape.up ℤ).Rel x_1 x_2
hf :
  ∀ (x_3 : (↑(AddCommGrpCat.of (Cochain F G x)) : Type v)) (p q : ℤ) (hpq : p + x_2 = q),
    Eq.{v + 1} (α := F.X p ⟶ G.X q)
      (Cochain.v
        ((AddCommGrpCat.Hom.hom
              (CategoryStruct.comp (Y := AddCommGrpCat.of (Cochain F G x_1))
                (AddCommGrpCat.ofHom (↑(δ_hom ℤ F G x x_1) : Cochain F G x →+ Cochain F G x_1))
                (AddCommGrpCat.ofHom (↑(δ_hom ℤ F G x_1 x_2) : Cochain F G x_1 →+ Cochain F G x_2))) :
            (a : (↑(AddCommGrpCat.of (Cochain F G x)) : Type v)) → (↑(AddCommGrpCat.of (Cochain F G x_2)) : Type v))
          x_3)
        p q hpq)
      (Cochain.v
        ((AddCommGrpCat.Hom.hom 0 :
            (a : (↑(AddCommGrpCat.of (Cochain F G x)) : Type v)) → (↑(AddCommGrpCat.of (Cochain F G x_2)) : Type v))
          x_3)
        p q hpq)
⊢ Eq (α := AddCommGrpCat.of (Cochain F G x) ⟶ AddCommGrpCat.of (Cochain F G x_2))
    (CategoryStruct.comp (Y := AddCommGrpCat.of (Cochain F G x_1))
      (AddCommGrpCat.ofHom (↑(δ_hom ℤ F G x x_1) : Cochain F G x →+ Cochain F G x_1))
      (AddCommGrpCat.ofHom (↑(δ_hom ℤ F G x_1 x_2) : Cochain F G x_1 →+ Cochain F G x_2)))
    0

Tactic:
ext