awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift (goal)
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
⊢ ((γ.leftUnshift n hn').leftShift a n' hn').v p q hpq = γ.v p q hpq
have h₆ : γ.v p q sorry = γ.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]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift (goal)
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
⊢ (γ₁ + γ₂).rightShift a n' hn' = γ₁.rightShift a n' hn' + γ₂.rightShift a n' hn'
have 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
Tactic: ext p q hpq
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift (goal)
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' + γ₂.rightShift a n' hn').v p q hpq
have 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
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift (goal)
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'
⊢ (γ₁ + γ₂).leftShift a n' hn' = γ₁.leftShift a n' hn' + γ₂.leftShift a n' hn'
have 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
Tactic: ext p q hpq
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift (goal)
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' + γ₂.leftShift a n' hn').v p q hpq
have 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
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift (goal)
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 : ℤ
⊢ (γ₁ + γ₂).shift a = γ₁.shift a + γ₂.shift a
have h : ∀ (p q : ℤ) (hpq : p + n = q), ((γ₁ + γ₂).shift a).v p q hpq = (γ₁.shift a + γ₂.shift a).v p q hpq
Tactic: ext p q hpq
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift (goal)
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 + γ₂.shift a).v p q hpq
have h : ((γ₁ + γ₂).shift a).v p q hpq = (γ₁.shift a).v p q hpq + (γ₂.shift a).v p q hpq
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift (goal)
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.{v + 1} (α := Cochain K (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) a) L) n')
    (rightShift 0 a n' hn') 0
have 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')
Tactic: change rightShiftAddEquiv K L n a n' hn' 0 = 0
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift (goal)
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.{v + 1} (α := Cochain K L n) (rightUnshift 0 n hn') 0
have 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)
Tactic: change (rightShiftAddEquiv K L n a n' hn').symm 0 = 0
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift (goal)
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.{v + 1} (α := Cochain (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) a) K) L n')
    (leftShift 0 a n' hn') 0
have 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')
Tactic: change leftShiftAddEquiv K L n a n' hn' 0 = 0
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift (goal)
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.{v + 1} (α := Cochain K L n) (leftUnshift 0 n hn') 0
have 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)
Tactic: change (leftShiftAddEquiv K L n a n' hn').symm 0 = 0
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift (goal)
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.{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
have 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)
Tactic: change shiftAddHom K L n a 0 = 0
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift (goal)
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
⊢ (-γ).rightShift a n' hn' = -γ.rightShift a n' hn'
have 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'
Tactic: change rightShiftAddEquiv K L n a n' hn' (-γ) = _
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift (goal)
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
⊢ (-γ).rightUnshift n hn = -γ.rightUnshift n hn
have 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
Tactic: change (rightShiftAddEquiv K L n a n' hn).symm (-γ) = _
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift (goal)
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'
⊢ (-γ).leftShift a n' hn' = -γ.leftShift a n' hn'
have 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'
Tactic: change leftShiftAddEquiv K L n a n' hn' (-γ) = _
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift (goal)
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'
⊢ (-γ).leftUnshift n hn = -γ.leftUnshift n hn
have 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
Tactic: change (leftShiftAddEquiv K L n a n' hn).symm (-γ) = _
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift (goal)
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 : ℤ
⊢ (-γ).shift a = -γ.shift a
have 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
Tactic: change shiftAddHom K L n a (-γ) = _
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift (goal)
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
⊢ (γ₁ + γ₂).rightUnshift n hn = γ₁.rightUnshift n hn + γ₂.rightUnshift n hn
have 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
Tactic: change (rightShiftAddEquiv K L n a n' hn).symm (γ₁ + γ₂) = _
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift (goal)
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'
⊢ (γ₁ + γ₂).leftUnshift n hn = γ₁.leftUnshift n hn + γ₂.leftUnshift n hn
have 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
Tactic: change (leftShiftAddEquiv K L n a n' hn).symm (γ₁ + γ₂) = _
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift (goal)
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'
have 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
Tactic: ext p q hpq
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift (goal)
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
have h : ((x • γ).rightShift a n' hn').v p q hpq = x • (γ.rightShift a n' hn').v p q hpq
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift (goal)
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'
have 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
Tactic: ext p q hpq
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift (goal)
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
have h : ((x • γ).leftShift a n' hn').v p q hpq = x • (γ.leftShift a n' hn').v p q hpq
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift (goal)
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
⊢ (x • γ).shift a = x • γ.shift a
have h : ∀ (p q : ℤ) (hpq : p + n = q), ((x • γ).shift a).v p q hpq = (x • γ.shift a).v p q hpq
Tactic: ext p q hpq
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift (goal)
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
have h : ((x • γ).shift a).v p q hpq = x • (γ.shift a).v p q hpq
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift (goal)
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
⊢ (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')
have dsimp : (x • γ).rightShift a n' hn' = x • γ.rightShift a n' hn'
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift (goal)
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
⊢ (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')
have dsimp : (x • γ).leftShift a n' hn = x • γ.leftShift a n' hn
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift (goal)
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
⊢ 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)
have dsimp : (x • x_1).shift a = x • x_1.shift a
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift (goal)
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ˣ
⊢ (x • γ).shift a = x • γ.shift a
have h : ∀ (p q : ℤ) (hpq : p + n = q), ((x • γ).shift a).v p q hpq = (x • γ.shift a).v p q hpq
Tactic: ext p q hpq
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift (goal)
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
have h : ((x • γ).shift a).v p q hpq = x • (γ.shift a).v p q hpq
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift (goal)
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
have 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
Tactic: change (rightShiftLinearEquiv R K L n a n' hn).symm (x • γ) = _
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift (goal)
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
have 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
Tactic: change (leftShiftLinearEquiv R K L n a n' hn).symm (x • γ) = _
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift (goal)
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'
⊢ (γ.comp γ' hnm).rightUnshift nm' hnm' = γ.comp (γ'.rightUnshift m' hm') ⋯
have h : ∀ (p q : ℤ) (hpq : p + nm' = q),
  ((γ.comp γ' hnm).rightUnshift nm' hnm').v p q hpq = (γ.comp (γ'.rightUnshift m' hm') sorry).v p q hpq
Tactic: ext p q hpq
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift (goal)
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
⊢ ((γ.comp γ' hnm).rightUnshift nm' hnm').v p q hpq = (γ.comp (γ'.rightUnshift m' hm') ⋯).v p q hpq
have h : (γ.comp γ' hnm).v p (p + n + m) sorry ≫ (M.shiftFunctorObjXIso a (p + n + m) q sorry).hom =
  (γ.comp (γ'.rightUnshift m' hm') sorry).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]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift (goal)
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
⊢ ((γ.comp γ' hnm).rightUnshift nm' hnm').v p q hpq = (γ.comp (γ'.rightUnshift m' hm') ⋯).v p q hpq
have h₁ : (γ.v p (p + n) sorry ≫ γ'.v (p + n) (p + n + m) sorry) ≫ (M.shiftFunctorObjXIso a (p + n + m) q sorry).hom =
  (γ.comp (γ'.rightUnshift m' hm') sorry).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]