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 ℤ
a n' : ℤ
γ : Cochain (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) a) K) L n'
n : ℤ
hn' : n + a = n'
p q : ℤ
hpq : p + n' = q
h :
  (a * n' + a * (a - 1) / 2).negOnePow •
      (K.shiftFunctorObjXIso a p (q - n) ⋯).hom ≫ (γ.leftUnshift n hn').v (q - n) q ⋯ =
    γ.v p q hpq
h₁ :
  (a * n' + a * (a - 1) / 2).negOnePow •
      (K.shiftFunctorObjXIso a p (q - n) ⋯).hom ≫
        ((a * n' + a * (a - 1) / 2).negOnePow • (K.shiftFunctorObjXIso a p (q - n) ⋯).inv ≫ γ.v p q ⋯) =
    γ.v p q hpq
h₂ :
  (a * n' + a * (a - 1) / 2).negOnePow •
      (a * n' + a * (a - 1) / 2).negOnePow •
        (K.shiftFunctorObjXIso a p (q - n) ⋯).hom ≫ (K.shiftFunctorObjXIso a p (q - n) ⋯).inv ≫ γ.v p q ⋯ =
    γ.v p q hpq
h₃ :
  ((a * n' + a * (a - 1) / 2).negOnePow * (a * n' + a * (a - 1) / 2).negOnePow) •
      (K.shiftFunctorObjXIso a p (q - n) ⋯).hom ≫ (K.shiftFunctorObjXIso a p (q - n) ⋯).inv ≫ γ.v p q ⋯ =
    γ.v p q hpq
h₄ : ((a * n' + a * (a - 1) / 2).negOnePow * (a * n' + a * (a - 1) / 2).negOnePow) • γ.v p q ⋯ = γ.v p q hpq
h₅ : HSMul.hSMul (α := ℤˣ) 1 (γ.v p q ⋯) = γ.v p q hpq
h₆ h₇ : γ.v p q ⋯ = γ.v p q hpq
⊢ ((γ.leftUnshift n hn').leftShift a n' hn').v p q hpq = γ.v p q hpq

Tactic:
rw [(γ.leftUnshift n hn').leftShift_v a n' hn' p q hpq (q - n) (by lia),
    γ.leftUnshift_v n hn' (q - n) q (by lia) p hpq, Linear.comp_units_smul, smul_smul,
    Iso.hom_inv_id_assoc, Int.units_mul_self, one_smul]

Premises used: HSub.hSub, smul_smul, CochainComplex.HomComplex.Cochain.leftUnshift, CochainComplex.HomComplex.Cochain.leftUnshift_v, CategoryTheory.Linear.comp_units_smul, one_smul, CochainComplex.HomComplex.Cochain.leftShift_v, CategoryTheory.Iso.hom_inv_id_assoc, 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
K L : CochainComplex.{v, u, 0} C ℤ
n : ℤ
γ₁ γ₂ : Cochain K L n
a n' : ℤ
hn' : n' + a = n
h :
  ∀ (p q : ℤ) (hpq : p + n' = q),
    ((γ₁ + γ₂).rightShift a n' hn').v p q hpq = (γ₁.rightShift a n' hn' + γ₂.rightShift a n' hn').v p q hpq
⊢ (γ₁ + γ₂).rightShift a n' hn' = γ₁.rightShift a n' hn' + γ₂.rightShift a n' hn'

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 : ℤ
γ₁ γ₂ : Cochain K L n
a n' : ℤ
hn' : n' + a = n
p q : ℤ
hpq : p + n' = q
h : ((γ₁ + γ₂).rightShift a n' hn').v p q hpq = (γ₁.rightShift a n' hn').v p q hpq + (γ₂.rightShift a n' hn').v p q hpq
⊢ ((γ₁ + γ₂).rightShift a n' hn').v p q hpq = (γ₁.rightShift a n' hn' + γ₂.rightShift a n' hn').v p q hpq

Tactic:
dsimp
-- 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' : ℤ
hn' : n' + a = n
p q : ℤ
hpq : p + n' = q
⊢ ((γ₁ + γ₂).rightShift a n' hn').v p q hpq = (γ₁.rightShift a n' hn').v p q hpq + (γ₂.rightShift a n' hn').v p q hpq

Tactic:
simp only [rightShift_v _ a n' hn' p q hpq _ rfl, add_v, add_comp]

Premises used: CategoryTheory.Preadditive.add_comp, CochainComplex.HomComplex.Cochain.rightShift_v, CochainComplex.HomComplex.Cochain.add_v, 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 : ℤ
γ₁ γ₂ : Cochain K L n
a n' : ℤ
hn' : n + a = n'
h :
  ∀ (p q : ℤ) (hpq : p + n' = q),
    ((γ₁ + γ₂).leftShift a n' hn').v p q hpq = (γ₁.leftShift a n' hn' + γ₂.leftShift a n' hn').v p q hpq
⊢ (γ₁ + γ₂).leftShift a n' hn' = γ₁.leftShift a n' hn' + γ₂.leftShift a n' hn'

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 : ℤ
γ₁ γ₂ : Cochain K L n
a n' : ℤ
hn' : n + a = n'
p q : ℤ
hpq : p + n' = q
h : ((γ₁ + γ₂).leftShift a n' hn').v p q hpq = (γ₁.leftShift a n' hn').v p q hpq + (γ₂.leftShift a n' hn').v p q hpq
⊢ ((γ₁ + γ₂).leftShift a n' hn').v p q hpq = (γ₁.leftShift a n' hn' + γ₂.leftShift a n' hn').v p q hpq

Tactic:
dsimp
-- 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' : ℤ
hn' : n + a = n'
p q : ℤ
hpq : p + n' = q
⊢ p + a + n = q

Tactic:
lia
-- 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' : ℤ
hn' : n + a = n'
p q : ℤ
hpq : p + n' = q
⊢ ((γ₁ + γ₂).leftShift a n' hn').v p q hpq = (γ₁.leftShift a n' hn').v p q hpq + (γ₂.leftShift a n' hn').v p q hpq

Tactic:
simp only [leftShift_v _ a n' hn' p q hpq (p + a) (by lia), add_v, comp_add, smul_add]

Premises used: HAdd.hAdd, CochainComplex.HomComplex.Cochain.leftShift_v, CategoryTheory.Preadditive.comp_add, CochainComplex.HomComplex.Cochain.add_v, smul_add
-- 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 : ℤ
h : ∀ (p q : ℤ) (hpq : p + n = q), ((γ₁ + γ₂).shift a).v p q hpq = (γ₁.shift a + γ₂.shift a).v p q hpq
⊢ (γ₁ + γ₂).shift a = γ₁.shift a + γ₂.shift a

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 : ℤ
γ₁ γ₂ : Cochain K L n
a p q : ℤ
hpq : p + n = q
h : ((γ₁ + γ₂).shift a).v p q hpq = (γ₁.shift a).v p q hpq + (γ₂.shift a).v p q hpq
⊢ ((γ₁ + γ₂).shift a).v p q hpq = (γ₁.shift a + γ₂.shift a).v p q hpq

Tactic:
dsimp
-- 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 p q : ℤ
hpq : p + n = q
⊢ ((γ₁ + γ₂).shift a).v p q hpq = (γ₁.shift a).v p q hpq + (γ₂.shift a).v p q hpq

Tactic:
simp only [shift_v', add_v]

Premises used: CochainComplex.HomComplex.Cochain.shift_v', CochainComplex.HomComplex.Cochain.add_v
-- 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 : ℤ
γ_1 γ₁ γ₂ : Cochain K L n_1
n a n' : ℤ
hn' : n' + a = n
γ : Cochain K L n
⊢ (fun (γ : Cochain K (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) a) L) n') ↦
        γ.rightUnshift n hn')
      ((fun (γ : Cochain K L n) ↦ γ.rightShift a n' hn') γ) =
    γ

Tactic:
simp only [rightUnshift_rightShift]

Premises used: CochainComplex.HomComplex.Cochain.rightUnshift_rightShift
-- 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 : ℤ
γ_1 γ₁ γ₂ : Cochain K L n_1
n a n' : ℤ
hn' : n' + a = n
γ : Cochain K (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) a) L) n'
⊢ (fun (γ : Cochain K L n) ↦ γ.rightShift a n' hn')
      ((fun (γ : Cochain K (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) a) L) n') ↦
          γ.rightUnshift n hn')
        γ) =
    γ

Tactic:
simp only [rightShift_rightUnshift]

Premises used: CochainComplex.HomComplex.Cochain.rightShift_rightUnshift
-- 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 : ℤ
γ_1 γ₁ γ₂ : Cochain K L n_1
n a n' : ℤ
hn' : n' + a = n
γ γ' : Cochain K L n
⊢ (γ + γ').rightShift a n' hn' = γ.rightShift a n' hn' + γ'.rightShift a n' hn'

Tactic:
simp only [rightShift_add]

Premises used: CochainComplex.HomComplex.Cochain.rightShift_add
-- 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 : ℤ
γ_1 γ₁ γ₂ : Cochain K L n_1
n a n' : ℤ
hn' : n + a = n'
γ : Cochain K L n
⊢ (fun (γ : Cochain (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) a) K) L n') ↦
        γ.leftUnshift n hn')
      ((fun (γ : Cochain K L n) ↦ γ.leftShift a n' hn') γ) =
    γ

Tactic:
simp only [leftUnshift_leftShift]

Premises used: CochainComplex.HomComplex.Cochain.leftUnshift_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 : ℤ
γ_1 γ₁ γ₂ : Cochain K L n_1
n a n' : ℤ
hn' : n + a = n'
γ : Cochain (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) a) K) L n'
⊢ (fun (γ : Cochain K L n) ↦ γ.leftShift a n' hn')
      ((fun (γ : Cochain (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) a) K) L n') ↦
          γ.leftUnshift n hn')
        γ) =
    γ

Tactic:
simp only [leftShift_leftUnshift]

Premises used: CochainComplex.HomComplex.Cochain.leftShift_leftUnshift
-- 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 : ℤ
γ_1 γ₁ γ₂ : Cochain K L n_1
n a n' : ℤ
hn' : n + a = n'
γ γ' : Cochain K L n
⊢ (γ + γ').leftShift a n' hn' = γ.leftShift a n' hn' + γ'.leftShift a n' hn'

Tactic:
simp only [leftShift_add]

Premises used: CochainComplex.HomComplex.Cochain.leftShift_add
-- 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 : ℤ
γ γ₁ γ₂ : Cochain K L n_1
n a : ℤ
a_1 b : Cochain K L n
⊢ (a_1 + b).shift a = a_1.shift a + b.shift a

Tactic:
simp only [shift_add]

Premises used: CochainComplex.HomComplex.Cochain.shift_add
-- 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 a n' : ℤ
hn' : n' + a = n
change :
  Eq (α := Cochain K (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) a) L) n')
    ((rightShiftAddEquiv K L n a n' hn' :
          (a_1 : Cochain K L n) → Cochain K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj L) n')
        0 :
      Cochain K (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) a) L) n')
    (0 : Cochain K (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) a) L) n')
⊢ Eq.{v + 1} (α := Cochain K (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) a) L) n')
    (rightShift 0 a n' hn') 0

Tactic:
change rightShiftAddEquiv K L n a n' hn' 0 = 0

Premises used: CochainComplex.HomComplex.Cochain.rightShiftAddEquiv, OfNat.ofNat, DFunLike.coe
-- 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 a n' : ℤ
hn' : n' + a = n
⊢ Eq (α := Cochain K (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) a) L) n')
    ((rightShiftAddEquiv K L n a n' hn' :
          (a_1 : Cochain K L n) → Cochain K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj L) n')
        0 :
      Cochain K (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) a) L) n')
    (0 : Cochain K (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) a) L) n')

Tactic:
apply map_zero

Premises used: map_zero
-- 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 a n' : ℤ
hn' : n' + a = n
change :
  Eq (α := Cochain K L n)
    (((rightShiftAddEquiv K L n a n' hn').symm :
          (a : Cochain K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj L) n') → Cochain K L n)
        0 :
      Cochain K L n)
    (0 : Cochain K L n)
⊢ Eq.{v + 1} (α := Cochain K L n) (rightUnshift 0 n hn') 0

Tactic:
change (rightShiftAddEquiv K L n a n' hn').symm 0 = 0

Premises used: CochainComplex.HomComplex.Cochain.rightShiftAddEquiv, OfNat.ofNat, DFunLike.coe, AddEquiv.symm
-- 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 a n' : ℤ
hn' : n' + a = n
⊢ Eq (α := Cochain K L n)
    (((rightShiftAddEquiv K L n a n' hn').symm :
          (a : Cochain K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj L) n') → Cochain K L n)
        0 :
      Cochain K L n)
    (0 : Cochain K L n)

Tactic:
apply map_zero

Premises used: map_zero
-- 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 a n' : ℤ
hn' : n + a = n'
change :
  Eq (α := Cochain (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) a) K) L n')
    ((leftShiftAddEquiv K L n a n' hn' :
          (a_1 : Cochain K L n) → Cochain ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K) L n')
        0 :
      Cochain (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) a) K) L n')
    (0 : Cochain (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) a) K) L n')
⊢ Eq.{v + 1} (α := Cochain (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) a) K) L n')
    (leftShift 0 a n' hn') 0

Tactic:
change leftShiftAddEquiv K L n a n' hn' 0 = 0

Premises used: CochainComplex.HomComplex.Cochain.leftShiftAddEquiv, OfNat.ofNat, DFunLike.coe
-- 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 a n' : ℤ
hn' : n + a = n'
⊢ Eq (α := Cochain (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) a) K) L n')
    ((leftShiftAddEquiv K L n a n' hn' :
          (a_1 : Cochain K L n) → Cochain ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K) L n')
        0 :
      Cochain (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) a) K) L n')
    (0 : Cochain (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) a) K) L n')

Tactic:
apply map_zero

Premises used: map_zero
-- 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 a n' : ℤ
hn' : n + a = n'
change :
  Eq (α := Cochain K L n)
    (((leftShiftAddEquiv K L n a n' hn').symm :
          (a : Cochain ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K) L n') → Cochain K L n)
        0 :
      Cochain K L n)
    (0 : Cochain K L n)
⊢ Eq.{v + 1} (α := Cochain K L n) (leftUnshift 0 n hn') 0

Tactic:
change (leftShiftAddEquiv K L n a n' hn').symm 0 = 0

Premises used: CochainComplex.HomComplex.Cochain.leftShiftAddEquiv, OfNat.ofNat, DFunLike.coe, AddEquiv.symm
-- 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 a n' : ℤ
hn' : n + a = n'
⊢ Eq (α := Cochain K L n)
    (((leftShiftAddEquiv K L n a n' hn').symm :
          (a : Cochain ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K) L n') → Cochain K L n)
        0 :
      Cochain K L n)
    (0 : Cochain K L n)

Tactic:
apply map_zero

Premises used: map_zero
-- 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 a : ℤ
change :
  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)
    ((shiftAddHom K L n a :
          (a_1 : Cochain K L n) →
            Cochain ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K)
              ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj L) n)
        0 :
      Cochain (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) a) K)
        (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) a) L) n)
    (0 :
      Cochain (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) a) K)
        (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) a) L) n)
⊢ Eq.{v + 1} (α :=
    Cochain (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) a) K)
      (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) a) L) n)
    (shift 0 a) 0

Tactic:
change shiftAddHom K L n a 0 = 0

Premises used: OfNat.ofNat, DFunLike.coe, CochainComplex.HomComplex.Cochain.shiftAddHom
-- 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 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)
    ((shiftAddHom K L n a :
          (a_1 : Cochain K L n) →
            Cochain ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K)
              ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj L) n)
        0 :
      Cochain (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) a) K)
        (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) a) L) n)
    (0 :
      Cochain (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) a) K)
        (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) a) L) n)

Tactic:
apply map_zero

Premises used: map_zero
-- 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' : ℤ
hn' : n' + a = n
change :
  (rightShiftAddEquiv K L n a n' hn' :
        (a_1 : Cochain K L n) → Cochain K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj L) n')
      (-γ) =
    -γ.rightShift a n' hn'
⊢ (-γ).rightShift a n' hn' = -γ.rightShift a n' hn'

Tactic:
change rightShiftAddEquiv K L n a n' hn' (-γ) = _

Premises used: CochainComplex.HomComplex.Cochain.rightShiftAddEquiv, DFunLike.coe, Neg.neg
-- 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' : ℤ
hn' : n' + a = n
⊢ (rightShiftAddEquiv K L n a n' hn' :
        (a_1 : Cochain K L n) → Cochain K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj L) n')
      (-γ) =
    -γ.rightShift a n' hn'

Tactic:
apply map_neg

Premises used: map_neg
-- 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' a : ℤ
γ : Cochain K (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) a) L) n'
n : ℤ
hn : n' + a = n
change :
  ((rightShiftAddEquiv K L n a n' hn).symm :
        (a : Cochain K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj L) n') → Cochain K L n)
      (-γ) =
    -γ.rightUnshift n hn
⊢ (-γ).rightUnshift n hn = -γ.rightUnshift n hn

Tactic:
change (rightShiftAddEquiv K L n a n' hn).symm (-γ) = _

Premises used: CochainComplex.HomComplex.Cochain.rightShiftAddEquiv, DFunLike.coe, Neg.neg, AddEquiv.symm
-- 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' a : ℤ
γ : Cochain K (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) a) L) n'
n : ℤ
hn : n' + a = n
⊢ ((rightShiftAddEquiv K L n a n' hn).symm :
        (a : Cochain K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj L) n') → Cochain K L n)
      (-γ) =
    -γ.rightUnshift n hn

Tactic:
apply map_neg

Premises used: map_neg
-- 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' : ℤ
hn' : n + a = n'
change :
  (leftShiftAddEquiv K L n a n' hn' :
        (a_1 : Cochain K L n) → Cochain ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K) L n')
      (-γ) =
    -γ.leftShift a n' hn'
⊢ (-γ).leftShift a n' hn' = -γ.leftShift a n' hn'

Tactic:
change leftShiftAddEquiv K L n a n' hn' (-γ) = _

Premises used: CochainComplex.HomComplex.Cochain.leftShiftAddEquiv, DFunLike.coe, Neg.neg
-- 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' : ℤ
hn' : n + a = n'
⊢ (leftShiftAddEquiv K L n a n' hn' :
        (a_1 : Cochain K L n) → Cochain ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K) L n')
      (-γ) =
    -γ.leftShift a n' hn'

Tactic:
apply map_neg

Premises used: map_neg
-- 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' a : ℤ
γ : Cochain (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) a) K) L n'
n : ℤ
hn : n + a = n'
change :
  ((leftShiftAddEquiv K L n a n' hn).symm :
        (a : Cochain ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K) L n') → Cochain K L n)
      (-γ) =
    -γ.leftUnshift n hn
⊢ (-γ).leftUnshift n hn = -γ.leftUnshift n hn

Tactic:
change (leftShiftAddEquiv K L n a n' hn).symm (-γ) = _

Premises used: CochainComplex.HomComplex.Cochain.leftShiftAddEquiv, DFunLike.coe, Neg.neg, AddEquiv.symm
-- 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' a : ℤ
γ : Cochain (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) a) K) L n'
n : ℤ
hn : n + a = n'
⊢ ((leftShiftAddEquiv K L n a n' hn).symm :
        (a : Cochain ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K) L n') → Cochain K L n)
      (-γ) =
    -γ.leftUnshift n hn

Tactic:
apply map_neg

Premises used: map_neg
-- 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 : ℤ
change :
  (shiftAddHom K L n a :
        (a_1 : Cochain K L n) →
          Cochain ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K)
            ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj L) n)
      (-γ) =
    -γ.shift a
⊢ (-γ).shift a = -γ.shift a

Tactic:
change shiftAddHom K L n a (-γ) = _

Premises used: DFunLike.coe, Neg.neg, CochainComplex.HomComplex.Cochain.shiftAddHom