awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
n : ℤ
γ : Cochain K L n
a n' n'' : ℤ
hn' : n' + a = n
hn'' : n + a = n''
rw : (a * n + a * (a - 1) / 2).negOnePow • γ.shift a = a.negOnePow • (γ.leftShift a n'' hn'').rightShift a n hn''
rw₁ : (a * n + a * (a - 1) / 2).negOnePow • γ.shift a = a.negOnePow • (a * n'' + a * (a - 1) / 2).negOnePow • γ.shift a
rw₂ :
  (a * n + a * (a - 1) / 2).negOnePow • γ.shift a = (a.negOnePow * (a * n'' + a * (a - 1) / 2).negOnePow) • γ.shift a
rw₃ :
  (a * n + a * (a - 1) / 2).negOnePow • γ.shift a =
    (a.negOnePow * (a * (n + a) + a * (a - 1) / 2).negOnePow) • γ.shift a
rw₄ :
  (a * n + a * (a - 1) / 2).negOnePow • γ.shift a =
    (a.negOnePow * (a * (a + n) + a * (a - 1) / 2).negOnePow) • γ.shift a
rw₅ :
  (a * n + a * (a - 1) / 2).negOnePow • γ.shift a =
    (a.negOnePow * (a * a + a * n + a * (a - 1) / 2).negOnePow) • γ.shift a
rw₆ :
  ((a * n).negOnePow * (a * (a - 1) / 2).negOnePow) • γ.shift a =
    (a.negOnePow * (a * a + a * n + a * (a - 1) / 2).negOnePow) • γ.shift a
rw₇ :
  ((a * n).negOnePow * (a * (a - 1) / 2).negOnePow) • γ.shift a =
    (a.negOnePow * ((a * a + a * n).negOnePow * (a * (a - 1) / 2).negOnePow)) • γ.shift a
rw₈ :
  ((a * n).negOnePow * (a * (a - 1) / 2).negOnePow) • γ.shift a =
    (a.negOnePow * ((a * a).negOnePow * (a * n).negOnePow * (a * (a - 1) / 2).negOnePow)) • γ.shift a
rw₉ :
  ((a * n).negOnePow * (a * (a - 1) / 2).negOnePow) • γ.shift a =
    (a.negOnePow * (a.negOnePow * (a * n).negOnePow * (a * (a - 1) / 2).negOnePow)) • γ.shift a
rw₁₀ :
  ((a * n).negOnePow * (a * (a - 1) / 2).negOnePow) • γ.shift a =
    (a.negOnePow * (a.negOnePow * (a * n).negOnePow) * (a * (a - 1) / 2).negOnePow) • γ.shift a
rw₁₁ :
  ((a * n).negOnePow * (a * (a - 1) / 2).negOnePow) • γ.shift a =
    (a.negOnePow * a.negOnePow * (a * n).negOnePow * (a * (a - 1) / 2).negOnePow) • γ.shift a
rw₁₂ :
  ((a * n).negOnePow * (a * (a - 1) / 2).negOnePow) • γ.shift a =
    (1 * (a * n).negOnePow * (a * (a - 1) / 2).negOnePow) • γ.shift a
rw₁₃ rw₁₄ :
  ((a * n).negOnePow * (a * (a - 1) / 2).negOnePow) • γ.shift a =
    ((a * n).negOnePow * (a * (a - 1) / 2).negOnePow) • γ.shift a
⊢ (γ.rightShift a n' hn').leftShift a n hn' = a.negOnePow • (γ.leftShift a n'' hn'').rightShift a n hn''

Tactic:
rw [leftShift_rightShift, rightShift_leftShift, smul_smul, ← hn'', add_comm n a, mul_add,
    Int.negOnePow_add, Int.negOnePow_add, Int.negOnePow_add, Int.negOnePow_mul_self,
    ← mul_assoc, ← mul_assoc, Int.units_mul_self, one_mul]

Premises used: mul_assoc, CochainComplex.HomComplex.Cochain.leftShift_rightShift, smul_smul, Int.negOnePow_add, CochainComplex.HomComplex.Cochain.rightShift_leftShift, add_comm, mul_add, one_mul, Int.negOnePow_mul_self, Int.units_mul_self
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
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
K L M : CochainComplex.{v, u, 0} C ℤ
n : ℤ
γ : Cocycle K L n
a n' : ℤ
hn' : n' + a = n
⊢ n' + 1 + a = n + 1

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
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
K L M : CochainComplex.{v, u, 0} C ℤ
n : ℤ
γ : Cocycle K L n
a n' : ℤ
hn' : n' + a = n
⊢ Eq (α := Cochain K (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) a) L) (n' + 1))
    (δ n' (n' + 1) ((↑γ : Cochain K L n).rightShift a n' hn')) 0

Tactic:
simp only [Cochain.δ_rightShift _ a n' (n' + 1) hn' (n + 1) (by lia),
      δ_eq_zero, Cochain.rightShift_zero, smul_zero]

Premises used: smul_zero, CochainComplex.HomComplex.Cochain.rightShift_zero, CochainComplex.HomComplex.Cocycle.δ_eq_zero, HAdd.hAdd, CochainComplex.HomComplex.Cochain.δ_rightShift, OfNat.ofNat
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
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
K L M : CochainComplex.{v, u, 0} C ℤ
n_1 n' a : ℤ
γ : Cocycle K (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) a) L) n'
n : ℤ
hn : n' + a = n
⊢ n + 1 - a + a = n + 1

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
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
K L M : CochainComplex.{v, u, 0} C ℤ
n_1 n' a : ℤ
γ : Cocycle K (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) a) L) n'
n : ℤ
hn : n' + a = n
rw :
  a.negOnePow •
      Cochain.rightUnshift
        (δ n' (n + 1 - a) (↑γ : Cochain K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj L) n')) (n + 1) ⋯ =
    0
rw₁ : HSMul.hSMul (β := Cochain K L (n + 1)) a.negOnePow (Cochain.rightUnshift (n' := n + 1 - a) 0 (n + 1) ⋯) = 0
rw₂ : HSMul.hSMul (β := Cochain K L (n + 1)) a.negOnePow 0 = 0
rw₃ rw₄ : Eq.{v + 1} (α := Cochain K L (n + 1)) 0 0
⊢ Eq (α := Cochain K L (n + 1))
    (δ n (n + 1) ((↑γ : Cochain K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj L) n').rightUnshift n hn)) 0

Tactic:
rw [Cochain.δ_rightUnshift _ n hn (n + 1) (n + 1 - a) (by lia),
      δ_eq_zero, Cochain.rightUnshift_zero, smul_zero]

Premises used: HSub.hSub, smul_zero, CochainComplex.HomComplex.Cocycle.δ_eq_zero, HAdd.hAdd, CochainComplex.HomComplex.Cochain.δ_rightUnshift, OfNat.ofNat, CochainComplex.HomComplex.Cochain.rightUnshift_zero
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
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
K L M : CochainComplex.{v, u, 0} C ℤ
n : ℤ
γ : Cocycle K L n
a n' : ℤ
hn' : n + a = n'
⊢ n + 1 + a = n' + 1

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
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
K L M : CochainComplex.{v, u, 0} C ℤ
n : ℤ
γ : Cocycle K L n
a n' : ℤ
hn' : n + a = n'
⊢ Eq (α := Cochain (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) a) K) L (n' + 1))
    (δ n' (n' + 1) ((↑γ : Cochain K L n).leftShift a n' hn')) 0

Tactic:
simp only [Cochain.δ_leftShift _ a n' (n' + 1) hn' (n + 1) (by lia),
      δ_eq_zero, Cochain.leftShift_zero, smul_zero]

Premises used: smul_zero, CochainComplex.HomComplex.Cochain.leftShift_zero, CochainComplex.HomComplex.Cocycle.δ_eq_zero, HAdd.hAdd, OfNat.ofNat, CochainComplex.HomComplex.Cochain.δ_leftShift
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
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
K L M : CochainComplex.{v, u, 0} C ℤ
n_1 n' a : ℤ
γ : Cocycle (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) a) K) L n'
n : ℤ
hn : n + a = n'
rw :
  HSMul.hSMul (β := Cochain K L (n + 1)) a.negOnePow
      (Cochain.leftUnshift
        (δ n' (n + 1 + a) (↑γ : Cochain ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K) L n')) (n + 1) ⋯) =
    0
rw₁ : HSMul.hSMul (β := Cochain K L (n + 1)) a.negOnePow (Cochain.leftUnshift (n' := n + 1 + a) 0 (n + 1) ⋯) = 0
rw₂ : HSMul.hSMul (β := Cochain K L (n + 1)) a.negOnePow 0 = 0
rw₃ rw₄ : Eq.{v + 1} (α := Cochain K L (n + 1)) 0 0
⊢ Eq (α := Cochain K L (n + 1))
    (δ n (n + 1) ((↑γ : Cochain ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K) L n').leftUnshift n hn)) 0

Tactic:
rw [Cochain.δ_leftUnshift _ n hn (n + 1) (n + 1 + a) rfl,
      δ_eq_zero, Cochain.leftUnshift_zero, smul_zero]

Premises used: smul_zero, CochainComplex.HomComplex.Cocycle.δ_eq_zero, HAdd.hAdd, CochainComplex.HomComplex.Cochain.δ_leftUnshift, OfNat.ofNat, rfl, CochainComplex.HomComplex.Cochain.leftUnshift_zero
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
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
K L M : CochainComplex.{v, u, 0} C ℤ
n : ℤ
γ : Cocycle K L n
a : ℤ
⊢ Eq (α :=
    Cochain (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) a) K)
      (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) a) L) (n + 1))
    (δ n (n + 1) ((↑γ : Cochain K L n).shift a)) 0

Tactic:
simp only [Cochain.δ_shift, δ_eq_zero, Cochain.shift_zero, smul_zero]

Premises used: CochainComplex.HomComplex.Cochain.shift_zero, smul_zero, CochainComplex.HomComplex.Cocycle.δ_eq_zero, CochainComplex.HomComplex.Cochain.δ_shift
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
n : ℤ
K' : CochainComplex.{v, u, 0} C ℤ
g : K' ⟶ K
f : K ⟶ Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) n) L
h :
  ∀ (p q : ℤ) (hpq : p + n = q),
    Eq (α := K'.X p ⟶ L.X q)
      (Cochain.v
        (↑((equivHomShift : (a : K' ⟶ (CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L) → Cocycle K' L n)
              (g ≫ f)) :
          Cochain K' L n)
        p q hpq)
      (Cochain.v
        (↑(precomp
              ((equivHomShift : (a : K ⟶ (CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L) → Cocycle K L n) f)
              g) :
          Cochain K' L n)
        p q hpq)
⊢ Eq (α := Cocycle K' L n)
    ((equivHomShift : (a : K' ⟶ (CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L) → Cocycle K' L n) (g ≫ f) :
      Cocycle K' L n)
    (precomp ((equivHomShift : (a : K ⟶ (CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L) → Cocycle K L n) f)
        g :
      Cocycle K' L n)

Tactic:
ext p q hpq
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
n : ℤ
K' : CochainComplex.{v, u, 0} C ℤ
g : K' ⟶ K
f : K ⟶ Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) n) L
p q : ℤ
hpq : p + n = q
⊢ Eq (α := K'.X p ⟶ L.X q)
    (Cochain.v
      (↑((equivHomShift : (a : K' ⟶ (CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L) → Cocycle K' L n)
            (g ≫ f)) :
        Cochain K' L n)
      p q hpq)
    (Cochain.v
      (↑(precomp
            ((equivHomShift : (a : K ⟶ (CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L) → Cocycle K L n) f)
            g) :
        Cochain K' L n)
      p q hpq)

Tactic:
simp [equivHomShift_apply, Cochain.rightUnshift_v _ _ _ _ _ _ _ (add_zero p)]

Premises used: CochainComplex.HomComplex.Cochain.rightUnshift_v, add_zero, CochainComplex.HomComplex.Cocycle.equivHomShift_apply
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
n : ℤ
z : Cocycle K L n
K' : CochainComplex.{v, u, 0} C ℤ
g : K' ⟶ K
⊢ Eq (α := Cocycle K' L n)
    ((equivHomShift : (a : K' ⟶ (CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L) → Cocycle K' L n)
        ((AddEquiv.symm equivHomShift :
            (a : Cocycle K' L n) → K' ⟶ (CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L)
          (z.precomp g)) :
      Cocycle K' L n)
    ((equivHomShift : (a : K' ⟶ (CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L) → Cocycle K' L n)
        (g ≫
          (AddEquiv.symm equivHomShift :
              (a : Cocycle K L n) → K ⟶ (CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L)
            z) :
      Cocycle K' L n)

Tactic:
simp [equivHomShift_comp]

Premises used: CochainComplex.HomComplex.Cocycle.equivHomShift_comp
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
n : ℤ
f : K ⟶ Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) n) L
L' : CochainComplex.{v, u, 0} C ℤ
g : L ⟶ L'
h :
  ∀ (p : ℤ),
    Eq (α := K.X p ⟶ L'.X (p + n))
      (Cochain.v
        (↑((equivHomShift : (a : K ⟶ (CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L') → Cocycle K L' n)
              (f ≫ CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) n) g)) :
          Cochain K L' n)
        p (p + n) ⋯)
      (Cochain.v
        (↑(postcomp
              ((equivHomShift : (a : K ⟶ (CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L) → Cocycle K L n) f)
              g) :
          Cochain K L' n)
        p (p + n) ⋯)
⊢ Eq (α := Cocycle K L' n)
    ((equivHomShift : (a : K ⟶ (CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L') → Cocycle K L' n)
        (f ≫ CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) n) g) :
      Cocycle K L' n)
    (postcomp ((equivHomShift : (a : K ⟶ (CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L) → Cocycle K L n) f)
        g :
      Cocycle K L' n)

Tactic:
ext p q rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
n : ℤ
f : K ⟶ Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) n) L
L' : CochainComplex.{v, u, 0} C ℤ
g : L ⟶ L'
p : ℤ
⊢ Eq (α := K.X p ⟶ L'.X (p + n))
    (Cochain.v
      (↑((equivHomShift : (a : K ⟶ (CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L') → Cocycle K L' n)
            (f ≫ CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) n) g)) :
        Cochain K L' n)
      p (p + n) ⋯)
    (Cochain.v
      (↑(postcomp
            ((equivHomShift : (a : K ⟶ (CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L) → Cocycle K L n) f)
            g) :
        Cochain K L' n)
      p (p + n) ⋯)

Tactic:
simp [equivHomShift_apply, Cochain.rightUnshift_v _ _ _ _ _ _ _ (add_zero p)]

Premises used: CochainComplex.HomComplex.Cochain.rightUnshift_v, add_zero, CochainComplex.HomComplex.Cocycle.equivHomShift_apply
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
n : ℤ
z : Cocycle K L n
L' : CochainComplex.{v, u, 0} C ℤ
g : L ⟶ L'
⊢ Eq (α := Cocycle K L' n)
    ((equivHomShift : (a : K ⟶ (CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L') → Cocycle K L' n)
        ((AddEquiv.symm equivHomShift :
            (a : Cocycle K L' n) → K ⟶ (CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L')
          (z.postcomp g)) :
      Cocycle K L' n)
    ((equivHomShift : (a : K ⟶ (CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L') → Cocycle K L' n)
        ((AddEquiv.symm equivHomShift :
              (a : Cocycle K L n) → K ⟶ (CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L)
            z ≫
          CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) n) g) :
      Cocycle K L' n)

Tactic:
simp [equivHomShift_comp_shift]

Premises used: CochainComplex.HomComplex.Cocycle.equivHomShift_comp_shift
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
X : C
K : CochainComplex.{v, u, 0} C ℤ
p q n : ℤ
h : p + n = q
⊢ Eq.{v + 1} (α := Cochain (Functor.obj (singleFunctor C p) X) K n) (fromSingleMk 0 h) 0

Tactic:
simp [fromSingleMk]

Premises used: CochainComplex.HomComplex.Cochain.fromSingleMk
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
X : C
K : CochainComplex.{v, u, 0} C ℤ
p q : ℤ
f : X ⟶ K.X q
n : ℤ
h : p + n = q
⊢ Eq (α := HomologicalComplex.X.{v, u, 0} (Functor.obj (singleFunctor C p) X) p ⟶ K.X q) (v (fromSingleMk f h) p q h)
    (Iso.hom (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) p X) ≫ f)

Tactic:
simp [fromSingleMk]

Premises used: CochainComplex.HomComplex.Cochain.fromSingleMk
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
X : C
K : CochainComplex.{v, u, 0} C ℤ
p q : ℤ
f : X ⟶ K.X q
n : ℤ
h : p + n = q
p' q' : ℤ
hpq' : p' + n = q'
hp' : p' ≠ p
⊢ Eq (α := HomologicalComplex.X.{v, u, 0} (Functor.obj (singleFunctor C p) X) p' ⟶ K.X q')
    (v (fromSingleMk f h) p' q' hpq') 0

Tactic:
single_v_eq_zero _ _ _ _ _ hp'

Premises used: CochainComplex.HomComplex.Cochain.fromSingleMk, CochainComplex.HomComplex.Cochain.single_v_eq_zero
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
X : C
K : CochainComplex.{v, u, 0} C ℤ
p q : ℤ
f : X ⟶ K.X q
n : ℤ
h : p + n = q
n' q' : ℤ
h' : p + n' = q'
pos :
  ∀ (hq : q + 1 = q'),
    Eq (α := Cochain (Functor.obj (singleFunctor C p) X) K n') (δ n n' (fromSingleMk f h))
      (fromSingleMk (f ≫ K.d q q') h')
neg :
  ∀ (hq : ¬q + 1 = q'),
    Eq (α := Cochain (Functor.obj (singleFunctor C p) X) K n') (δ n n' (fromSingleMk f h))
      (fromSingleMk (f ≫ K.d q q') h')
⊢ Eq (α := Cochain (Functor.obj (singleFunctor C p) X) K n') (δ n n' (fromSingleMk f h))
    (fromSingleMk (f ≫ K.d q q') h')

Tactic:
by_cases hq : q + 1 = q'
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
X : C
K : CochainComplex.{v, u, 0} C ℤ
p q : ℤ
f : X ⟶ K.X q
n : ℤ
h : p + n = q
n' q' : ℤ
h' : p + n' = q'
hq : q + 1 = q'
⊢ n + 1 = n'

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
X : C
K : CochainComplex.{v, u, 0} C ℤ
p q : ℤ
f : X ⟶ K.X q
n : ℤ
h : p + n = q
n' q' : ℤ
h' : p + n' = q'
hq : q + 1 = q'
⊢ p - 1 + 1 = p

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
X : C
K : CochainComplex.{v, u, 0} C ℤ
p q : ℤ
f : X ⟶ K.X q
n : ℤ
h : p + n = q
n' q' : ℤ
h' : p + n' = q'
hq : q + 1 = q'
pos :
  single ((Iso.hom (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) p X) ≫ f) ≫ K.d q q') n' +
      HSMul.hSMul (β := Cochain (Functor.obj (singleFunctor C p) X) K n') n'.negOnePow
        (single (p := p - 1)
          (HomologicalComplex.d (Functor.obj (singleFunctor C p) X) (p - 1) p ≫
            Iso.hom (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) p X) ≫ f)
          n') =
    single (Iso.hom (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) p X) ≫ f ≫ K.d q q') n'
⊢ Eq (α := Cochain (Functor.obj (singleFunctor C p) X) K n')
    (δ n n' (single (Iso.hom (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) p X) ≫ f) n))
    (single (Iso.hom (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) p X) ≫ f ≫ K.d q q') n')

Tactic:
rw [δ_single _ n n' (by lia) (p - 1) q' (by lia) hq]

Premises used: CochainComplex.HomComplex.Cochain.δ_single, HSub.hSub, OfNat.ofNat
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
X : C
K : CochainComplex.{v, u, 0} C ℤ
p q : ℤ
f : X ⟶ K.X q
n : ℤ
h : p + n = q
n' q' : ℤ
h' : p + n' = q'
hq : q + 1 = q'
⊢ single ((Iso.hom (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) p X) ≫ f) ≫ K.d q q') n' +
      HSMul.hSMul (β := Cochain (Functor.obj (singleFunctor C p) X) K n') n'.negOnePow
        (single (p := p - 1)
          (HomologicalComplex.d (Functor.obj (singleFunctor C p) X) (p - 1) p ≫
            Iso.hom (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) p X) ≫ f)
          n') =
    single (Iso.hom (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) p X) ≫ f ≫ K.d q q') n'

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
X : C
K : CochainComplex.{v, u, 0} C ℤ
p q : ℤ
f : X ⟶ K.X q
n : ℤ
h : p + n = q
n' q' : ℤ
h' : p + n' = q'
hq : ¬q + 1 = q'
⊢ ¬n + 1 = n'

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
X : C
K : CochainComplex.{v, u, 0} C ℤ
p q : ℤ
f : X ⟶ K.X q
n : ℤ
h : p + n = q
n' q' : ℤ
h' : p + n' = q'
hq : ¬q + 1 = q'
⊢ ¬q + 1 = q'

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
X : C
K : CochainComplex.{v, u, 0} C ℤ
p q : ℤ
f : X ⟶ K.X q
n : ℤ
h : p + n = q
n' q' : ℤ
h' : p + n' = q'
hq : ¬q + 1 = q'
⊢ Eq (α := Cochain (Functor.obj (singleFunctor C p) X) K n') (δ n n' (fromSingleMk f h))
    (fromSingleMk (f ≫ K.d q q') h')

Tactic:
simp [δ_shape n n' (by lia), HomologicalComplex.shape K q q' (by simp; lia),
      fromSingleMk]

Premises used: CochainComplex.HomComplex.δ_shape, CochainComplex.HomComplex.Cochain.fromSingleMk, HomologicalComplex.shape
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
X : C
K : CochainComplex.{v, u, 0} C ℤ
p q n : ℤ
h : p + n = q
α : Cochain (Functor.obj (singleFunctor C p) X) K n
h₁ :
  ∀ (p' q' : ℤ) (hpq' : p' + n = q'),
    v
        ((fun (f : X ⟶ K.X q) ↦ (fromSingleMk f h : Cochain (Functor.obj (singleFunctor C p) X) K n))
          ((fun (α : Cochain (Functor.obj (singleFunctor C p) X) K n) ↦
              Iso.inv (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) p X) ≫ α.v p q h)
            α))
        p' q' hpq' =
      α.v p' q' hpq'
⊢ (fun (f : X ⟶ K.X q) ↦ (fromSingleMk f h : Cochain (Functor.obj (singleFunctor C p) X) K n))
      ((fun (α : Cochain (Functor.obj (singleFunctor C p) X) K n) ↦
          Iso.inv (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) p X) ≫ α.v p q h)
        α) =
    α

Tactic:
ext p' q' hpq'
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
X : C
K : CochainComplex.{v, u, 0} C ℤ
p q n : ℤ
h : p + n = q
α : Cochain (Functor.obj (singleFunctor C p) X) K n
p' q' : ℤ
hpq' : p' + n = q'
pos :
  ∀ (hp : p' = p),
    v
        ((fun (f : X ⟶ K.X q) ↦ (fromSingleMk f h : Cochain (Functor.obj (singleFunctor C p) X) K n))
          ((fun (α : Cochain (Functor.obj (singleFunctor C p) X) K n) ↦
              Iso.inv (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) p X) ≫ α.v p q h)
            α))
        p' q' hpq' =
      α.v p' q' hpq'
neg :
  ∀ (hp : ¬p' = p),
    v
        ((fun (f : X ⟶ K.X q) ↦ (fromSingleMk f h : Cochain (Functor.obj (singleFunctor C p) X) K n))
          ((fun (α : Cochain (Functor.obj (singleFunctor C p) X) K n) ↦
              Iso.inv (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) p X) ≫ α.v p q h)
            α))
        p' q' hpq' =
      α.v p' q' hpq'
⊢ v
      ((fun (f : X ⟶ K.X q) ↦ (fromSingleMk f h : Cochain (Functor.obj (singleFunctor C p) X) K n))
        ((fun (α : Cochain (Functor.obj (singleFunctor C p) X) K n) ↦
            Iso.inv (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) p X) ≫ α.v p q h)
          α))
      p' q' hpq' =
    α.v p' q' hpq'

Tactic:
by_cases hp : p' = p