awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexInduction
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
d : ℤ
X : ℕ → Set (Cochain K L d)
φ : (n : ℕ) → (↑(X n) : Type v) → (↑(X (n + 1)) : Type v)
p₀ : ℤ
hφ : ∀ (n : ℕ) (x : (↑(X n) : Type v)), (↑(φ n x) : Cochain K L d).EqUpTo (↑x : Cochain K L d) (p₀ + (↑n : ℤ))
x₀ : (↑(X 0) : Type v)
k : ℕ
hk :
  ∀ (n₁ : ℕ),
    (↑(sequence (X := X) φ x₀ n₁) : Cochain K L d).EqUpTo (↑(sequence (X := X) φ x₀ (n₁ + k)) : Cochain K L d)
      (p₀ + (↑n₁ : ℤ))
n₁ : ℕ
p q : ℤ
hpq : p + d = q
hp : p ≤ p₀ + (↑n₁ : ℤ)
succ :
  (↑(φ (n₁ + k) (sequence (X := X) φ x₀ (n₁ + k))) : Cochain K L d).v p q hpq =
    (↑(sequence (X := X) φ x₀ (n₁ + (k + 1))) : Cochain K L d).v p q hpq
⊢ (↑(sequence (X := X) φ x₀ n₁) : Cochain K L d).v p q hpq =
    (↑(sequence (X := X) φ x₀ (n₁ + (k + 1))) : Cochain K L d).v p q hpq

Tactic:
rw [hk n₁ p q hpq hp, ← hφ (n₁ + k) (sequence φ x₀ (n₁ + k)) p q hpq (by lia)]

Premises used: HAdd.hAdd, CochainComplex.HomComplex.Cochain.InductionUp.sequence
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexInduction
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
d : ℤ
X : ℕ → Set (Cochain K L d)
φ : (n : ℕ) → (↑(X n) : Type v) → (↑(X (n + 1)) : Type v)
p₀ : ℤ
hφ : ∀ (n : ℕ) (x : (↑(X n) : Type v)), (↑(φ n x) : Cochain K L d).EqUpTo (↑x : Cochain K L d) (p₀ + (↑n : ℤ))
x₀ : (↑(X 0) : Type v)
k : ℕ
hk :
  ∀ (n₁ : ℕ),
    (↑(sequence (X := X) φ x₀ n₁) : Cochain K L d).EqUpTo (↑(sequence (X := X) φ x₀ (n₁ + k)) : Cochain K L d)
      (p₀ + (↑n₁ : ℤ))
n₁ : ℕ
p q : ℤ
hpq : p + d = q
hp : p ≤ p₀ + (↑n₁ : ℤ)
⊢ (↑(φ (n₁ + k) (sequence (X := X) φ x₀ (n₁ + k))) : Cochain K L d).v p q hpq =
    (↑(sequence (X := X) φ x₀ (n₁ + (k + 1))) : Cochain K L d).v p q hpq

Tactic:
dsimp [sequence]

Premises used: CochainComplex.HomComplex.Cochain.InductionUp.sequence
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexInduction
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
d : ℤ
X : ℕ → Set (Cochain K L d)
φ : (n : ℕ) → (↑(X n) : Type v) → (↑(X (n + 1)) : Type v)
p₀ : ℤ
hφ : ∀ (n : ℕ) (x : (↑(X n) : Type v)), (↑(φ n x) : Cochain K L d).EqUpTo (↑x : Cochain K L d) (p₀ + (↑n : ℤ))
x₀ : (↑(X 0) : Type v)
n₁ k : ℕ
zero :
  ∀ (n₁ : ℕ),
    (↑(sequence (X := X) φ x₀ n₁) : Cochain K L d).EqUpTo (↑(sequence (X := X) φ x₀ (n₁ + 0)) : Cochain K L d)
      (p₀ + (↑n₁ : ℤ))
succ :
  ∀ (k : ℕ)
    (hk :
      ∀ (n₁ : ℕ),
        (↑(sequence (X := X) φ x₀ n₁) : Cochain K L d).EqUpTo (↑(sequence (X := X) φ x₀ (n₁ + k)) : Cochain K L d)
          (p₀ + (↑n₁ : ℤ)))
    (n₁ : ℕ),
    (↑(sequence (X := X) φ x₀ n₁) : Cochain K L d).EqUpTo (↑(sequence (X := X) φ x₀ (n₁ + (k + 1))) : Cochain K L d)
      (p₀ + (↑n₁ : ℤ))
⊢ (↑(sequence (X := X) φ x₀ n₁) : Cochain K L d).EqUpTo (↑(sequence (X := X) φ x₀ (n₁ + k)) : Cochain K L d)
    (p₀ + (↑n₁ : ℤ))

Tactic:
induction k generalizing n₁ with
  | zero => intro _ _ _ _; simp
  | succ k hk =>
    intro p q hpq hp
    rw [hk n₁ p q hpq hp, ← hφ (n₁ + k) (sequence φ x₀ (n₁ + k)) p q hpq (by lia)]
    dsimp [sequence]

Premises used: CochainComplex.HomComplex.Cochain.InductionUp.sequence
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexInduction
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
d : ℤ
X : ℕ → Set (Cochain K L d)
φ : (n : ℕ) → (↑(X n) : Type v) → (↑(X (n + 1)) : Type v)
p₀ : ℤ
hφ : ∀ (n : ℕ) (x : (↑(X n) : Type v)), (↑(φ n x) : Cochain K L d).EqUpTo (↑x : Cochain K L d) (p₀ + (↑n : ℤ))
x₀ : (↑(X 0) : Type v)
n : ℕ
p q : ℤ
hpq : p + d = q
hp : p ≤ p₀ + (↑n : ℤ)
⊢ (p - p₀).toNat ≤ n

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexInduction
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
d : ℤ
X : ℕ → Set (Cochain K L d)
φ : (n : ℕ) → (↑(X n) : Type v) → (↑(X (n + 1)) : Type v)
p₀ : ℤ
hφ : ∀ (n : ℕ) (x : (↑(X n) : Type v)), (↑(φ n x) : Cochain K L d).EqUpTo (↑x : Cochain K L d) (p₀ + (↑n : ℤ))
x₀ : (↑(X 0) : Type v)
n : ℕ
p q : ℤ
hpq : p + d = q
hp : p ≤ p₀ + (↑n : ℤ)
⊢ p ≤ p₀ + (↑(p - p₀).toNat : ℤ)

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexInduction
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
d : ℤ
X : ℕ → Set (Cochain K L d)
φ : (n : ℕ) → (↑(X n) : Type v) → (↑(X (n + 1)) : Type v)
p₀ : ℤ
hφ : ∀ (n : ℕ) (x : (↑(X n) : Type v)), (↑(φ n x) : Cochain K L d).EqUpTo (↑x : Cochain K L d) (p₀ + (↑n : ℤ))
x₀ : (↑(X 0) : Type v)
n : ℕ
p q : ℤ
hpq : p + d = q
hp : p ≤ p₀ + (↑n : ℤ)
⊢ (limitSequence (X := X) φ hφ x₀).v p q hpq = (↑(sequence (X := X) φ x₀ n) : Cochain K L d).v p q hpq

Tactic:
exact sequence_eqUpTo φ hφ _ _ _ (by lia) _ _ _ (by lia)

Premises used: CochainComplex.HomComplex.Cochain.InductionUp.sequence_eqUpTo
-- 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
p q : ℤ
hpq : p + n' = q
⊢ p + n = q + a

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 : ℤ
γ γ₁ γ₂ : Cochain K L n
a n' : ℤ
hn' : n' + a = n
p q : ℤ
hpq : p + n' = q
p' : ℤ
hp' : p + n = p'
rw : p + n = q + a
rw₁ : p + n = p + n' + a
rw₂ : p + (n' + a) = p + n' + a
rw₃ rw₄ : p + (n' + a) = p + (n' + a)
⊢ p' = q + a

Tactic:
rw [← hp', ← hpq, ← hn', add_assoc]

Premises used: add_assoc
-- 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' : ℤ
hp' : p + n = p'
subst : (γ.rightShift a n' hn').v p q hpq = γ.v p (p + n) ⋯ ≫ (L.shiftFunctorObjXIso a q (p + n) ⋯).inv
⊢ (γ.rightShift a n' hn').v p q hpq = γ.v p p' hp' ≫ (L.shiftFunctorObjXIso a q p' ⋯).inv

Tactic:
subst hp'
-- 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
⊢ v (mk fun (p q : ℤ) (hpq : p + n' = q) ↦ γ.v p (p + n) ⋯ ≫ (L.shiftFunctorObjXIso a q (p + n) ⋯).inv) p q hpq =
    γ.v p (p + n) ⋯ ≫ (L.shiftFunctorObjXIso a q (p + n) ⋯).inv

Tactic:
simp only [mk_v]

Premises used: CochainComplex.HomComplex.Cochain.mk_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 : ℤ
γ γ₁ γ₂ : 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
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'
p q : ℤ
hpq : p + n' = q
p' : ℤ
hp' : p' + n = q
rw : p' + n = p + a + n
rw₁ : q = p + a + n
rw₂ : q = p + (a + n)
rw₃ : q = p + (n + a)
rw₄ : q = p + n'
rw₅ rw₆ : q = q
⊢ p' = p + a

Tactic:
rw [← add_left_inj n, hp', add_assoc, add_comm a, hn', hpq]

Premises used: add_assoc, add_left_inj, add_comm
-- 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' : ℤ
hp' : p' + n = q
⊢ p' = p + a

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
p' : ℤ
hp' : p' + n = q
obtain :
  ∀ (hp' : p + a + n = q),
    (γ.leftShift a n' hn').v p q hpq =
      (a * n' + a * (a - 1) / 2).negOnePow • (K.shiftFunctorObjXIso a p (p + a) ⋯).hom ≫ γ.v (p + a) q hp'
⊢ (γ.leftShift a n' hn').v p q hpq =
    (a * n' + a * (a - 1) / 2).negOnePow • (K.shiftFunctorObjXIso a p p' ⋯).hom ≫ γ.v p' q hp'

Tactic:
obtain rfl : p' = p + a := by lia

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 : ℤ
γ : Cochain K L n
a n' : ℤ
hn' : n + a = n'
p q : ℤ
hpq : p + n' = q
hp' : p + a + n = q
⊢ v
      (mk fun (p q : ℤ) (hpq : p + n' = q) ↦
        (a * n' + a * (a - 1) / 2).negOnePow • (K.shiftFunctorObjXIso a p (p + a) ⋯).hom ≫ γ.v (p + a) q ⋯)
      p q hpq =
    (a * n' + a * (a - 1) / 2).negOnePow • (K.shiftFunctorObjXIso a p (p + a) ⋯).hom ≫ γ.v (p + a) q hp'

Tactic:
simp only [mk_v]

Premises used: CochainComplex.HomComplex.Cochain.mk_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 : ℤ
γ : Cochain K (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) a) L) n'
n : ℤ
hn : n' + a = n
p q : ℤ
hpq : p + n = q
rw : p + n = p + n' + a
rw₁ : p + n = p + (n' + a)
rw₂ rw₃ : p + n = p + n
⊢ q = p + n' + a

Tactic:
rw [← hpq, add_assoc, hn]

Premises used: add_assoc
-- 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 : ℤ
γ : Cochain K (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) a) L) n'
n : ℤ
hn : n' + a = n
p q : ℤ
hpq : p + n = q
p' : ℤ
hp' : p + n' = p'
rw : p + n = p' + a
rw₁ : p + (n' + a) = p' + a
rw₂ : p + n' + a = p' + a
rw₃ rw₄ : p' + a = p' + a
⊢ q = p' + a

Tactic:
rw [← hpq, ← hn, ← add_assoc, hp']

Premises used: add_assoc
-- 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
p q : ℤ
hpq : p + n = q
p' : ℤ
hp' : p + n' = p'
subst : (γ.rightUnshift n hn).v p q hpq = γ.v p (p + n') ⋯ ≫ (L.shiftFunctorObjXIso a (p + n') q ⋯).hom
⊢ (γ.rightUnshift n hn).v p q hpq = γ.v p p' hp' ≫ (L.shiftFunctorObjXIso a p' q ⋯).hom

Tactic:
subst hp'
-- 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
p q : ℤ
hpq : p + n = q
⊢ v (mk fun (p q : ℤ) (hpq : p + n = q) ↦ γ.v p (p + n') ⋯ ≫ (L.shiftFunctorObjXIso a (p + n') q ⋯).hom) p q hpq =
    γ.v p (p + n') ⋯ ≫ (L.shiftFunctorObjXIso a (p + n') q ⋯).hom

Tactic:
simp only [mk_v]

Premises used: CochainComplex.HomComplex.Cochain.mk_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 : ℤ
γ : 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
⊢ p = p - a + a

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 : ℤ
γ_1 γ₁ γ₂ : Cochain K L n_1
n' a : ℤ
γ : 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
⊢ 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 M : CochainComplex.{v, u, 0} C ℤ
n_1 : ℤ
γ_1 γ₁ γ₂ : Cochain K L n_1
n' a : ℤ
γ : 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
p' : ℤ
hp' : p' + n' = q
⊢ p = p' + a

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 : ℤ
γ_1 γ₁ γ₂ : Cochain K L n_1
n' a : ℤ
γ : 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
p' : ℤ
hp' : p' + n' = q
⊢ p' + 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' a : ℤ
γ : 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
p' : ℤ
hp' : p' + n' = q
⊢ p' = p - a

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' a : ℤ
γ : 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
p' : ℤ
hp' : p' + n' = q
obtain :
  ∀ (hp' : p - a + n' = q),
    (γ.leftUnshift n hn).v p q hpq =
      (a * n' + a * (a - 1) / 2).negOnePow • (K.shiftFunctorObjXIso a (p - a) p ⋯).inv ≫ γ.v (p - a) q ⋯
⊢ (γ.leftUnshift n hn).v p q hpq =
    (a * n' + a * (a - 1) / 2).negOnePow • (K.shiftFunctorObjXIso a p' p ⋯).inv ≫ γ.v p' q ⋯

Tactic:
obtain rfl : p' = p - a := by lia

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' a : ℤ
γ : 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
hp' : p - a + n' = q
⊢ (γ.leftUnshift n hn).v p q hpq =
    (a * n' + a * (a - 1) / 2).negOnePow • (K.shiftFunctorObjXIso a (p - a) p ⋯).inv ≫ γ.v (p - a) q ⋯

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

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 : ℤ
γ γ₁ γ₂ : Cochain K L n
a p q : ℤ
hpq : p + n = q
p' q' : ℤ
hp' : p' = p + a
hq' : q' = q + a
rw : p + a + n = q'
rw₁ : p + a + n = q + a
rw₂ : p + a + n = p + n + a
rw₃ : p + (a + n) = p + n + a
rw₄ : p + (n + a) = p + n + a
rw₅ rw₆ : p + (n + a) = p + (n + a)
⊢ p' + n = q'

Tactic:
rw [hp', hq', ← hpq, add_assoc, add_comm a, add_assoc]

Premises used: add_assoc, add_comm
-- 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
p' q' : ℤ
hp' : p' = p + a
hq' : q' = q + a
subst :
  (γ.shift a).v p q hpq =
    (K.shiftFunctorObjXIso a p (p + a) ⋯).hom ≫ γ.v (p + a) (q + a) ⋯ ≫ (L.shiftFunctorObjXIso a q (q + a) ⋯).inv
⊢ (γ.shift a).v p q hpq = (K.shiftFunctorObjXIso a p p' hp').hom ≫ γ.v p' q' ⋯ ≫ (L.shiftFunctorObjXIso a q q' hq').inv

Tactic:
subst hp' hq'
-- 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 =
    (K.shiftFunctorObjXIso a p (p + a) ⋯).hom ≫ γ.v (p + a) (q + a) ⋯ ≫ (L.shiftFunctorObjXIso a q (q + a) ⋯).inv

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

Tactic:
simp only [shift_v γ a p q hpq _ _ rfl rfl, shiftFunctor_obj_X, shiftFunctorObjXIso,
    HomologicalComplex.XIsoOfEq_rfl, Iso.refl_hom, Iso.refl_inv, comp_id, id_comp]

Premises used: HomologicalComplex.XIsoOfEq_rfl, CochainComplex.shiftFunctor_obj_X, CochainComplex.shiftFunctorObjXIso, CategoryTheory.Category.comp_id, CategoryTheory.Iso.refl_inv, CochainComplex.HomComplex.Cochain.shift_v, CategoryTheory.Iso.refl_hom, rfl, CategoryTheory.Category.id_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 : ℤ
γ : Cochain K L n
a n' : ℤ
hn' : n' + a = n
h : ∀ (p q : ℤ) (hpq : p + n = q), ((γ.rightShift a n' hn').rightUnshift n hn').v p q hpq = γ.v p q hpq
⊢ (γ.rightShift a n' hn').rightUnshift 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
⊢ ((γ.rightShift a n' hn').rightUnshift n hn').v p q hpq = γ.v p q hpq

Tactic:
simp only [rightUnshift_v _ n hn' p q hpq (p + n') rfl,
    γ.rightShift_v _ _ hn' p (p + n') rfl q hpq,
    shiftFunctorObjXIso, assoc, Iso.inv_hom_id, comp_id]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.inv_hom_id, CochainComplex.HomComplex.Cochain.rightUnshift_v, CochainComplex.shiftFunctorObjXIso, CategoryTheory.Category.comp_id, HAdd.hAdd, CochainComplex.HomComplex.Cochain.rightShift_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 ℤ
a n' : ℤ
γ : Cochain K (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) a) L) n'
n : ℤ
hn' : n' + a = n
h : ∀ (p q : ℤ) (hpq : p + n' = q), ((γ.rightUnshift n hn').rightShift a n' hn').v p q hpq = γ.v p q hpq
⊢ (γ.rightUnshift 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 ℤ
a n' : ℤ
γ : Cochain K (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) a) L) n'
n : ℤ
hn' : n' + a = n
p q : ℤ
hpq : p + n' = q
⊢ ((γ.rightUnshift n hn').rightShift a n' hn').v p q hpq = γ.v p q hpq

Tactic:
simp only [(γ.rightUnshift n hn').rightShift_v a n' hn' p q hpq (p + n) rfl,
    γ.rightUnshift_v n hn' p (p + n) rfl q hpq,
    shiftFunctorObjXIso, assoc, Iso.hom_inv_id, comp_id]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.hom_inv_id, CochainComplex.HomComplex.Cochain.rightUnshift_v, CochainComplex.shiftFunctorObjXIso, CategoryTheory.Category.comp_id, HAdd.hAdd, CochainComplex.HomComplex.Cochain.rightUnshift, CochainComplex.HomComplex.Cochain.rightShift_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').leftUnshift n hn').v p q hpq = γ.v p q hpq
⊢ (γ.leftShift a n' hn').leftUnshift 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
⊢ q - n' + 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
h :
  (a * n' + a * (a - 1) / 2).negOnePow •
      (K.shiftFunctorObjXIso a (q - n') p ⋯).inv ≫ (γ.leftShift a n' hn').v (q - n') q ⋯ =
    γ.v p q hpq
h₁ :
  (a * n' + a * (a - 1) / 2).negOnePow •
      (K.shiftFunctorObjXIso a (q - n') p ⋯).inv ≫
        ((a * n' + a * (a - 1) / 2).negOnePow • (K.shiftFunctorObjXIso a (q - n') p ⋯).hom ≫ γ.v p q hpq) =
    γ.v p q hpq
h₂ :
  (a * n' + a * (a - 1) / 2).negOnePow •
      (a * n' + a * (a - 1) / 2).negOnePow •
        (K.shiftFunctorObjXIso a (q - n') p ⋯).inv ≫ (K.shiftFunctorObjXIso a (q - n') p ⋯).hom ≫ γ.v p q hpq =
    γ.v p q hpq
h₃ : (a * n' + a * (a - 1) / 2).negOnePow • (a * n' + a * (a - 1) / 2).negOnePow • γ.v p q hpq = γ.v p q hpq
h₄ : ((a * n' + a * (a - 1) / 2).negOnePow * (a * n' + a * (a - 1) / 2).negOnePow) • γ.v p q hpq = γ.v p q hpq
h₅ : HSMul.hSMul (α := ℤˣ) 1 (γ.v p q hpq) = γ.v p q hpq
h₆ h₇ : γ.v p q hpq = γ.v p q hpq
⊢ ((γ.leftShift a n' hn').leftUnshift n hn').v p q hpq = γ.v p q hpq

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

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

Tactic:
lia