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 : ℤ
⊢ (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

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 = γ₁.rightUnshift n hn + γ₂.rightUnshift n hn

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

Premises used: HAdd.hAdd, CochainComplex.HomComplex.Cochain.rightShiftAddEquiv, 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 : ℤ
γ₁ γ₂ : 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 + γ₂.rightUnshift n hn

Tactic:
apply map_add

Premises used: map_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 : ℤ
γ₁ γ₂ : 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 = γ₁.leftUnshift n hn + γ₂.leftUnshift n hn

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

Premises used: HAdd.hAdd, CochainComplex.HomComplex.Cochain.leftShiftAddEquiv, 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 : ℤ
γ₁ γ₂ : 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 + γ₂.leftUnshift n hn

Tactic:
apply map_add

Premises used: map_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 : CochainComplex.{v, u, 0} C ℤ
n : ℤ
γ : Cochain K L n
a n' : ℤ
hn' : n' + a = n
x : R
h : ∀ (p q : ℤ) (hpq : p + n' = q), ((x • γ).rightShift a n' hn').v p q hpq = (x • γ.rightShift a n' hn').v p q hpq
⊢ (x • γ).rightShift a n' hn' = x • γ.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
R : Type u_1
inst_2 : Ring R
inst_3 : Linear.{u_1, v, u} R C
K L : CochainComplex.{v, u, 0} C ℤ
n : ℤ
γ : Cochain K L n
a n' : ℤ
hn' : n' + a = n
x : R
p q : ℤ
hpq : p + n' = q
h : ((x • γ).rightShift a n' hn').v p q hpq = x • (γ.rightShift a n' hn').v p q hpq
⊢ ((x • γ).rightShift a n' hn').v p q hpq = (x • γ.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
R : Type u_1
inst_2 : Ring R
inst_3 : Linear.{u_1, v, u} R C
K L : CochainComplex.{v, u, 0} C ℤ
n : ℤ
γ : Cochain K L n
a n' : ℤ
hn' : n' + a = n
x : R
p q : ℤ
hpq : p + n' = q
⊢ ((x • γ).rightShift a n' hn').v p q hpq = x • (γ.rightShift a n' hn').v p q hpq

Tactic:
simp only [rightShift_v _ a n' hn' p q hpq _ rfl, smul_v, Linear.smul_comp]

Premises used: CochainComplex.HomComplex.Cochain.smul_v, CochainComplex.HomComplex.Cochain.rightShift_v, rfl, CategoryTheory.Linear.smul_comp
-- 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 : CochainComplex.{v, u, 0} C ℤ
n : ℤ
γ : Cochain K L n
a n' : ℤ
hn' : n + a = n'
x : R
h : ∀ (p q : ℤ) (hpq : p + n' = q), ((x • γ).leftShift a n' hn').v p q hpq = (x • γ.leftShift a n' hn').v p q hpq
⊢ (x • γ).leftShift a n' hn' = x • γ.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
R : Type u_1
inst_2 : Ring R
inst_3 : Linear.{u_1, v, u} R C
K L : CochainComplex.{v, u, 0} C ℤ
n : ℤ
γ : Cochain K L n
a n' : ℤ
hn' : n + a = n'
x : R
p q : ℤ
hpq : p + n' = q
h : ((x • γ).leftShift a n' hn').v p q hpq = x • (γ.leftShift a n' hn').v p q hpq
⊢ ((x • γ).leftShift a n' hn').v p q hpq = (x • γ.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
R : Type u_1
inst_2 : Ring R
inst_3 : Linear.{u_1, v, u} R C
K L : CochainComplex.{v, u, 0} C ℤ
n : ℤ
γ : Cochain K L n
a n' : ℤ
hn' : n + a = n'
x : R
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
R : Type u_1
inst_2 : Ring R
inst_3 : Linear.{u_1, v, u} R C
K L : CochainComplex.{v, u, 0} C ℤ
n : ℤ
γ : Cochain K L n
a n' : ℤ
hn' : n + a = n'
x : R
p q : ℤ
hpq : p + n' = q
⊢ ((x • γ).leftShift a n' hn').v p q hpq = x • (γ.leftShift a n' hn').v p q hpq

Tactic:
simp only [leftShift_v _ a n' hn' p q hpq (p + a) (by lia), smul_v, Linear.comp_smul,
    smul_comm x]

Premises used: CategoryTheory.Linear.comp_smul, HAdd.hAdd, CochainComplex.HomComplex.Cochain.smul_v, CochainComplex.HomComplex.Cochain.leftShift_v, SMulCommClass.smul_comm
-- 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 : CochainComplex.{v, u, 0} C ℤ
n : ℤ
γ : Cochain K L n
a : ℤ
x : R
h : ∀ (p q : ℤ) (hpq : p + n = q), ((x • γ).shift a).v p q hpq = (x • γ.shift a).v p q hpq
⊢ (x • γ).shift a = x • γ.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
R : Type u_1
inst_2 : Ring R
inst_3 : Linear.{u_1, v, u} R C
K L : CochainComplex.{v, u, 0} C ℤ
n : ℤ
γ : Cochain K L n
a : ℤ
x : R
p q : ℤ
hpq : p + n = q
h : ((x • γ).shift a).v p q hpq = x • (γ.shift a).v p q hpq
⊢ ((x • γ).shift a).v p q hpq = (x • γ.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
R : Type u_1
inst_2 : Ring R
inst_3 : Linear.{u_1, v, u} R C
K L : CochainComplex.{v, u, 0} C ℤ
n : ℤ
γ : Cochain K L n
a : ℤ
x : R
p q : ℤ
hpq : p + n = q
⊢ ((x • γ).shift a).v p q hpq = x • (γ.shift a).v p q hpq

Tactic:
simp only [shift_v', smul_v]

Premises used: CochainComplex.HomComplex.Cochain.smul_v, CochainComplex.HomComplex.Cochain.shift_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
x : R
γ : Cochain K L n
dsimp : (x • γ).rightShift a n' hn' = x • γ.rightShift a n' hn'
⊢ (rightShiftAddEquiv K L n a n' hn' :
        (a_1 : Cochain K L n) → Cochain K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj L) n')
      (x • γ) =
    HSMul.hSMul (β := Cochain K (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) a) L) n') x
      ((rightShiftAddEquiv K L n a n' hn' :
            (a_1 : Cochain K L n) → Cochain K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj L) n')
          γ :
        Cochain K (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) a) L) n')

Tactic:
dsimp
-- 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
x : R
γ : Cochain K L n
⊢ (x • γ).rightShift a n' hn' = x • γ.rightShift a n' hn'

Tactic:
simp only [rightShift_smul]

Premises used: CochainComplex.HomComplex.Cochain.rightShift_smul
-- 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'
x : R
γ : Cochain K L n
dsimp : (x • γ).leftShift a n' hn = x • γ.leftShift a n' hn
⊢ (leftShiftAddEquiv K L n a n' hn :
        (a_1 : Cochain K L n) → Cochain ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K) L n')
      (x • γ) =
    HSMul.hSMul (β := Cochain (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) a) K) L n') x
      ((leftShiftAddEquiv K L n a n' hn :
            (a_1 : Cochain K L n) → Cochain ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K) L n')
          γ :
        Cochain (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) a) K) L n')

Tactic:
dsimp
-- 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'
x : R
γ : Cochain K L n
⊢ (x • γ).leftShift a n' hn = x • γ.leftShift a n' hn

Tactic:
simp only [leftShift_smul]

Premises used: CochainComplex.HomComplex.Cochain.leftShift_smul
-- 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 : ℤ
x : R
x_1 : Cochain K L n
dsimp : (x • x_1).shift a = x • x_1.shift a
⊢ AddHom.toFun
      (↑(shiftAddHom K L n a) :
        Cochain K L n →ₙ+
          Cochain ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K)
            ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj L) n)
      (x • x_1) =
    HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) x : R)
      (AddHom.toFun
        (↑(shiftAddHom K L n a) :
          Cochain K L n →ₙ+
            Cochain ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K)
              ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj L) n)
        x_1)

Tactic:
dsimp
-- 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 : ℤ
x : R
x_1 : Cochain K L n
⊢ (x • x_1).shift a = x • x_1.shift a

Tactic:
simp only [shift_smul]

Premises used: CochainComplex.HomComplex.Cochain.shift_smul
-- 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 : CochainComplex.{v, u, 0} C ℤ
n : ℤ
γ : Cochain K L n
a n' : ℤ
hn' : n' + a = n
x : Rˣ
⊢ (x • γ).rightShift a n' hn' = x • γ.rightShift a n' hn'

Tactic:
apply rightShift_smul

Premises used: CochainComplex.HomComplex.Cochain.rightShift_smul
-- 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 : CochainComplex.{v, u, 0} C ℤ
n : ℤ
γ : Cochain K L n
a n' : ℤ
hn' : n + a = n'
x : Rˣ
⊢ (x • γ).leftShift a n' hn' = x • γ.leftShift a n' hn'

Tactic:
apply leftShift_smul

Premises used: CochainComplex.HomComplex.Cochain.leftShift_smul
-- 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 : CochainComplex.{v, u, 0} C ℤ
n : ℤ
γ : Cochain K L n
a : ℤ
x : Rˣ
h : ∀ (p q : ℤ) (hpq : p + n = q), ((x • γ).shift a).v p q hpq = (x • γ.shift a).v p q hpq
⊢ (x • γ).shift a = x • γ.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
R : Type u_1
inst_2 : Ring R
inst_3 : Linear.{u_1, v, u} R C
K L : CochainComplex.{v, u, 0} C ℤ
n : ℤ
γ : Cochain K L n
a : ℤ
x : Rˣ
p q : ℤ
hpq : p + n = q
h : ((x • γ).shift a).v p q hpq = x • (γ.shift a).v p q hpq
⊢ ((x • γ).shift a).v p q hpq = (x • γ.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
R : Type u_1
inst_2 : Ring R
inst_3 : Linear.{u_1, v, u} R C
K L : CochainComplex.{v, u, 0} C ℤ
n : ℤ
γ : Cochain K L n
a : ℤ
x : Rˣ
p q : ℤ
hpq : p + n = q
⊢ ((x • γ).shift a).v p q hpq = x • (γ.shift a).v p q hpq

Tactic:
simp only [shift_v', units_smul_v]

Premises used: CochainComplex.HomComplex.Cochain.units_smul_v, CochainComplex.HomComplex.Cochain.shift_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 : 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
x : R
change :
  (LinearEquiv.symm (rightShiftLinearEquiv R K L n a n' hn) :
        (a : Cochain K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj L) n') → Cochain K L n)
      (x • γ) =
    x • γ.rightUnshift n hn
⊢ (x • γ).rightUnshift n hn = x • γ.rightUnshift n hn

Tactic:
change (rightShiftLinearEquiv R K L n a n' hn).symm (x • γ) = _

Premises used: LinearEquiv.symm, CochainComplex.HomComplex.Cochain.rightShiftLinearEquiv, HSMul.hSMul, DFunLike.coe
-- 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 : 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
x : R
⊢ (LinearEquiv.symm (rightShiftLinearEquiv R K L n a n' hn) :
        (a : Cochain K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj L) n') → Cochain K L n)
      (x • γ) =
    x • γ.rightUnshift n hn

Tactic:
apply map_smul

Premises used: map_smul
-- 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 : 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
x : Rˣ
⊢ (x • γ).rightUnshift n hn = x • γ.rightUnshift n hn

Tactic:
apply rightUnshift_smul

Premises used: CochainComplex.HomComplex.Cochain.rightUnshift_smul
-- 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 : 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'
x : R
change :
  (LinearEquiv.symm (leftShiftLinearEquiv R K L n a n' hn) :
        (a : Cochain ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K) L n') → Cochain K L n)
      (x • γ) =
    x • γ.leftUnshift n hn
⊢ (x • γ).leftUnshift n hn = x • γ.leftUnshift n hn

Tactic:
change (leftShiftLinearEquiv R K L n a n' hn).symm (x • γ) = _

Premises used: LinearEquiv.symm, HSMul.hSMul, CochainComplex.HomComplex.Cochain.leftShiftLinearEquiv, DFunLike.coe
-- 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 : 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'
x : R
⊢ (LinearEquiv.symm (leftShiftLinearEquiv R K L n a n' hn) :
        (a : Cochain ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K) L n') → Cochain K L n)
      (x • γ) =
    x • γ.leftUnshift n hn

Tactic:
apply map_smul

Premises used: map_smul
-- 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 : 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'
x : Rˣ
⊢ (x • γ).leftUnshift n hn = x • γ.leftUnshift n hn

Tactic:
apply leftUnshift_smul

Premises used: CochainComplex.HomComplex.Cochain.leftUnshift_smul
-- 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 : ℤ
γ γ₁ γ₂ : Cochain K L n
m a : ℤ
γ' : Cochain L (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) a) M) m
nm : ℤ
hnm : n + m = nm
nm' : ℤ
hnm' : nm + a = nm'
m' : ℤ
hm' : m + a = m'
⊢ n + m' = nm'

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 M : CochainComplex.{v, u, 0} C ℤ
n : ℤ
γ : Cochain K L n
m a : ℤ
γ' : Cochain L (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) a) M) m
nm : ℤ
hnm : n + m = nm
nm' : ℤ
hnm' : nm + a = nm'
m' : ℤ
hm' : m + a = m'
h :
  ∀ (p q : ℤ) (hpq : p + nm' = q),
    ((γ.comp γ' hnm).rightUnshift nm' hnm').v p q hpq = (γ.comp (γ'.rightUnshift m' hm') ⋯).v p q hpq
⊢ (γ.comp γ' hnm).rightUnshift nm' hnm' = γ.comp (γ'.rightUnshift m' hm') ⋯

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 M : CochainComplex.{v, u, 0} C ℤ
n : ℤ
γ : Cochain K L n
m a : ℤ
γ' : Cochain L (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) a) M) m
nm : ℤ
hnm : n + m = nm
nm' : ℤ
hnm' : nm + a = nm'
m' : ℤ
hm' : m + a = m'
p q : ℤ
hpq : p + nm' = q
⊢ p + nm = p + n + m

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 M : CochainComplex.{v, u, 0} C ℤ
n : ℤ
γ : Cochain K L n
m a : ℤ
γ' : Cochain L (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) a) M) m
nm : ℤ
hnm : n + m = nm
nm' : ℤ
hnm' : nm + a = nm'
m' : ℤ
hm' : m + a = m'
p q : ℤ
hpq : p + nm' = q
⊢ n + m' = nm'

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 M : CochainComplex.{v, u, 0} C ℤ
n : ℤ
γ : Cochain K L n
m a : ℤ
γ' : Cochain L (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) a) M) m
nm : ℤ
hnm : n + m = nm
nm' : ℤ
hnm' : nm + a = nm'
m' : ℤ
hm' : m + a = m'
p q : ℤ
hpq : p + nm' = q
⊢ p + n = p + n

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 M : CochainComplex.{v, u, 0} C ℤ
n : ℤ
γ : Cochain K L n
m a : ℤ
γ' : Cochain L (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) a) M) m
nm : ℤ
hnm : n + m = nm
nm' : ℤ
hnm' : nm + a = nm'
m' : ℤ
hm' : m + a = m'
p q : ℤ
hpq : p + nm' = q
⊢ p + n + m' = 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 M : CochainComplex.{v, u, 0} C ℤ
n : ℤ
γ : Cochain K L n
m a : ℤ
γ' : Cochain L (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) a) M) m
nm : ℤ
hnm : n + m = nm
nm' : ℤ
hnm' : nm + a = nm'
m' : ℤ
hm' : m + a = m'
p q : ℤ
hpq : p + nm' = q
h :
  (γ.comp γ' hnm).v p (p + n + m) ⋯ ≫ (M.shiftFunctorObjXIso a (p + n + m) q ⋯).hom =
    (γ.comp (γ'.rightUnshift m' hm') ⋯).v p q hpq
h₁ :
  (γ.v p (p + n) ⋯ ≫ γ'.v (p + n) (p + n + m) ⋯) ≫ (M.shiftFunctorObjXIso a (p + n + m) q ⋯).hom =
    (γ.comp (γ'.rightUnshift m' hm') ⋯).v p q hpq
h₂ :
  (γ.v p (p + n) ⋯ ≫ γ'.v (p + n) (p + n + m) ⋯) ≫ (M.shiftFunctorObjXIso a (p + n + m) q ⋯).hom =
    γ.v p (p + n) ⋯ ≫ (γ'.rightUnshift m' hm').v (p + n) q ⋯
h₃ :
  (γ.v p (p + n) ⋯ ≫ γ'.v (p + n) (p + n + m) ⋯) ≫ (M.shiftFunctorObjXIso a (p + n + m) q ⋯).hom =
    γ.v p (p + n) ⋯ ≫ γ'.v (p + n) (p + n + m) ⋯ ≫ (M.shiftFunctorObjXIso a (p + n + m) q ⋯).hom
h₄ h₅ :
  γ.v p (p + n) ⋯ ≫ γ'.v (p + n) (p + n + m) ⋯ ≫ (M.shiftFunctorObjXIso a (p + n + m) q ⋯).hom =
    γ.v p (p + n) ⋯ ≫ γ'.v (p + n) (p + n + m) ⋯ ≫ (M.shiftFunctorObjXIso a (p + n + m) q ⋯).hom
⊢ ((γ.comp γ' hnm).rightUnshift nm' hnm').v p q hpq = (γ.comp (γ'.rightUnshift m' hm') ⋯).v p q hpq

Tactic:
rw [(γ.comp γ' hnm).rightUnshift_v nm' hnm' p q hpq (p + n + m) (by lia),
    γ.comp_v γ' hnm p (p + n) (p + n + m) rfl rfl,
    comp_v _ _ (show n + m' = nm' by lia) p (p + n) q (by lia) (by lia),
    γ'.rightUnshift_v m' hm' (p + n) q (by lia) (p + n + m) rfl, assoc]

Premises used: CategoryTheory.Category.assoc, CochainComplex.HomComplex.Cochain.comp, CochainComplex.HomComplex.Cochain.comp_v, CochainComplex.HomComplex.Cochain.rightUnshift_v, HAdd.hAdd, rfl
-- 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 : ℤ
γ γ₁ γ₂ : Cochain K L n
a n' : ℤ
hn' : n + a = n'
m t t' : ℤ
γ' : Cochain L M m
h : n + m = t
ht' : t + a = t'
rw : n' + m = t + a
rw₁ : n' + m = n + m + a
rw₂ : n + a + m = n + m + a
rw₃ : n + (a + m) = n + m + a
rw₄ : n + (m + a) = n + m + a
rw₅ rw₆ : n + (m + a) = n + (m + a)
⊢ n' + m = t'

Tactic:
rw [← ht', ← h, ← hn', add_assoc, add_comm a, add_assoc]

Premises used: add_assoc, add_comm