awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.TotalComplexShift
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K : HomologicalComplex₂.{v_1, u_1, 0, 0} C (up ℤ) (up ℤ)
x : ℤ
inst_2 : K.HasTotal (up ℤ)
n₀ n₁ n₀' n₁' : ℤ
h₀ : n₀ + x = n₀'
h₁ : n₁ + x = n₁'
h : n₀ + 1 = n₁
p q : ℤ
hpq : p + q = n₀
pos :
  (HSMul.hSMul (β :=
        ((Functor.obj (shiftFunctor₁ C x) K).X p).X q ⟶ ((Functor.obj (shiftFunctor₁ C x) K).total (up ℤ)).X n₁)
        ((up ℤ).ε₁ (up ℤ) (up ℤ) (p, q))
        (HomologicalComplex.Hom.f ((Functor.obj (shiftFunctor₁ C x) K).d p (p + 1)) q ≫
          (Functor.obj (shiftFunctor₁ C x) K).ιTotal (up ℤ) (p + 1) q n₁ ⋯) ≫
      (Functor.obj (shiftFunctor₁ C x) K).totalDesc fun (p q : ℤ) (hpq : p + q = n₁) ↦
        K.ιTotal (up ℤ) (p + x) q n₁' ⋯) =
    x.negOnePow •
      HSMul.hSMul (β := (K.X (p + x)).X q ⟶ (K.total (up ℤ)).X n₁') ((up ℤ).ε₁ (up ℤ) (up ℤ) (p + x, q))
        (HomologicalComplex.Hom.f (K.d (p + x) (p + 1 + x)) q ≫ K.ιTotal (up ℤ) (p + 1 + x) q n₁' ⋯)
⊢ CategoryStruct.comp (Y := ((Functor.obj (shiftFunctor₁ C x) K).total (up ℤ)).X n₀)
      ((Functor.obj (shiftFunctor₁ C x) K).ιTotal (up ℤ) p q n₀ hpq)
      ((Functor.obj (shiftFunctor₁ C x) K).D₁ (up ℤ) n₀ n₁ ≫
        (Functor.obj (shiftFunctor₁ C x) K).totalDesc fun (p q : ℤ) (hpq : p + q = n₁) ↦
          K.ιTotal (up ℤ) (p + x) q n₁' ⋯) =
    (Functor.obj (shiftFunctor₁ C x) K).ιTotal (up ℤ) p q n₀ hpq ≫
      HSMul.hSMul (β :=
        ((Functor.obj (shiftFunctor₁ C x) K).total (up ℤ)).X n₀ ⟶
          GradedObject.mapObj.{0, 0, v_1, u_1} K.toGradedObject ((up ℤ).π (up ℤ) (up ℤ)) n₁')
        x.negOnePow
        (((Functor.obj (shiftFunctor₁ C x) K).totalDesc fun (p q : ℤ) (hpq : p + q = n₀) ↦
            K.ιTotal (up ℤ) (p + x) q n₀' ⋯) ≫
          K.D₁ (up ℤ) n₀' n₁')

Tactic:
rw [ι_D₁_assoc, Linear.comp_units_smul, ι_totalDesc_assoc, ι_D₁,
      ((shiftFunctor₁ C x).obj K).d₁_eq _ rfl _ _ (by dsimp; lia),
      K.d₁_eq _ (show p + x + 1 = p + 1 + x by lia) _ _ (by dsimp; lia)]

Premises used: HomologicalComplex₂.ι_D₁_assoc, HomologicalComplex₂.ι_totalDesc_assoc, HomologicalComplex₂.d₁_eq, CategoryTheory.Linear.comp_units_smul, HomologicalComplex₂.shiftFunctor₁, HomologicalComplex₂.ι_D₁, CategoryTheory.Functor.obj, rfl
-- Module: Mathlib.Algebra.Homology.TotalComplexShift
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K : HomologicalComplex₂.{v_1, u_1, 0, 0} C (up ℤ) (up ℤ)
x : ℤ
inst_2 : K.HasTotal (up ℤ)
n₀ n₁ n₀' n₁' : ℤ
h₀ : n₀ + x = n₀'
h₁ : n₁ + x = n₁'
h : n₀ + 1 = n₁
p q : ℤ
hpq : p + q = n₀
pos :
  (HSMul.hSMul (α := ℤˣ) (β := (K.X (p + x)).X q ⟶ ((Functor.obj (shiftFunctor₁ C x) K).total (up ℤ)).X n₁) 1
        (HSMul.hSMul (β := (K.X (p + x)).X q ⟶ (K.X (p + 1 + x)).X q) x.negOnePow
            (HomologicalComplex.Hom.f (K.d (p + x) (p + 1 + x)) q) ≫
          (Functor.obj (shiftFunctor₁ C x) K).ιTotal (up ℤ) (p + 1) q n₁ ⋯) ≫
      (Functor.obj (shiftFunctor₁ C x) K).totalDesc fun (p q : ℤ) (hpq : p + q = n₁) ↦
        K.ιTotal (up ℤ) (p + x) q n₁' ⋯) =
    x.negOnePow •
      HSMul.hSMul (α := ℤˣ) (β := (K.X (p + x)).X q ⟶ (K.total (up ℤ)).X n₁') 1
        (HomologicalComplex.Hom.f (K.d (p + x) (p + 1 + x)) q ≫ K.ιTotal (up ℤ) (p + 1 + x) q n₁' ⋯)
⊢ (HSMul.hSMul (β :=
        ((Functor.obj (shiftFunctor₁ C x) K).X p).X q ⟶ ((Functor.obj (shiftFunctor₁ C x) K).total (up ℤ)).X n₁)
        ((up ℤ).ε₁ (up ℤ) (up ℤ) (p, q))
        (HomologicalComplex.Hom.f ((Functor.obj (shiftFunctor₁ C x) K).d p (p + 1)) q ≫
          (Functor.obj (shiftFunctor₁ C x) K).ιTotal (up ℤ) (p + 1) q n₁ ⋯) ≫
      (Functor.obj (shiftFunctor₁ C x) K).totalDesc fun (p q : ℤ) (hpq : p + q = n₁) ↦
        K.ιTotal (up ℤ) (p + x) q n₁' ⋯) =
    x.negOnePow •
      HSMul.hSMul (β := (K.X (p + x)).X q ⟶ (K.total (up ℤ)).X n₁') ((up ℤ).ε₁ (up ℤ) (up ℤ) (p + x, q))
        (HomologicalComplex.Hom.f (K.d (p + x) (p + 1 + x)) q ≫ K.ιTotal (up ℤ) (p + 1 + x) q n₁' ⋯)

Tactic:
dsimp
-- Module: Mathlib.Algebra.Homology.TotalComplexShift
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K : HomologicalComplex₂.{v_1, u_1, 0, 0} C (up ℤ) (up ℤ)
x : ℤ
inst_2 : K.HasTotal (up ℤ)
n₀ n₁ n₀' n₁' : ℤ
h₀ : n₀ + x = n₀'
h₁ : n₁ + x = n₁'
h : ¬(up ℤ).Rel n₀ n₁
neg : ¬(up ℤ).Rel n₀' n₁'
⊢ (Functor.obj (shiftFunctor₁ C x) K).D₁ (up ℤ) n₀ n₁ ≫ Iso.hom (K.totalShift₁XIso x n₁ n₁' h₁) =
    HSMul.hSMul (β :=
      ((Functor.obj (shiftFunctor₁ C x) K).total (up ℤ)).X n₀ ⟶
        GradedObject.mapObj.{0, 0, v_1, u_1} K.toGradedObject ((up ℤ).π (up ℤ) (up ℤ)) n₁')
      x.negOnePow (Iso.hom (K.totalShift₁XIso x n₀ n₀' h₀) ≫ K.D₁ (up ℤ) n₀' n₁')

Tactic:
rw [D₁_shape _ _ _ _ h, zero_comp, D₁_shape, comp_zero, smul_zero]

Premises used: CategoryTheory.Limits.comp_zero, smul_zero, HomologicalComplex₂.D₁_shape, CategoryTheory.Limits.zero_comp
-- Module: Mathlib.Algebra.Homology.TotalComplexShift
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K : HomologicalComplex₂.{v_1, u_1, 0, 0} C (up ℤ) (up ℤ)
x : ℤ
inst_2 : K.HasTotal (up ℤ)
n₀ n₁ n₀' n₁' : ℤ
h₀ : n₀ + x = n₀'
h₁ : n₁ + x = n₁'
h : ¬(up ℤ).Rel n₀ n₁
⊢ ¬(up ℤ).Rel n₀' n₁'

Tactic:
grind [up_Rel]

Premises used: ComplexShape.up_Rel
-- Module: Mathlib.Algebra.Homology.TotalComplexShift
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K : HomologicalComplex₂.{v_1, u_1, 0, 0} C (up ℤ) (up ℤ)
x : ℤ
inst_2 : K.HasTotal (up ℤ)
n₀ n₁ n₀' n₁' : ℤ
h₀ : n₀ + x = n₀'
h₁ : n₁ + x = n₁'
pos :
  ∀ (h : (up ℤ).Rel n₀ n₁),
    (Functor.obj (shiftFunctor₁ C x) K).D₂ (up ℤ) n₀ n₁ ≫ Iso.hom (K.totalShift₁XIso x n₁ n₁' h₁) =
      HSMul.hSMul (β :=
        ((Functor.obj (shiftFunctor₁ C x) K).total (up ℤ)).X n₀ ⟶
          GradedObject.mapObj.{0, 0, v_1, u_1} K.toGradedObject ((up ℤ).π (up ℤ) (up ℤ)) n₁')
        x.negOnePow (Iso.hom (K.totalShift₁XIso x n₀ n₀' h₀) ≫ K.D₂ (up ℤ) n₀' n₁')
neg :
  ∀ (h : ¬(up ℤ).Rel n₀ n₁),
    (Functor.obj (shiftFunctor₁ C x) K).D₂ (up ℤ) n₀ n₁ ≫ Iso.hom (K.totalShift₁XIso x n₁ n₁' h₁) =
      HSMul.hSMul (β :=
        ((Functor.obj (shiftFunctor₁ C x) K).total (up ℤ)).X n₀ ⟶
          GradedObject.mapObj.{0, 0, v_1, u_1} K.toGradedObject ((up ℤ).π (up ℤ) (up ℤ)) n₁')
        x.negOnePow (Iso.hom (K.totalShift₁XIso x n₀ n₀' h₀) ≫ K.D₂ (up ℤ) n₀' n₁')
⊢ (Functor.obj (shiftFunctor₁ C x) K).D₂ (up ℤ) n₀ n₁ ≫ Iso.hom (K.totalShift₁XIso x n₁ n₁' h₁) =
    HSMul.hSMul (β :=
      ((Functor.obj (shiftFunctor₁ C x) K).total (up ℤ)).X n₀ ⟶
        GradedObject.mapObj.{0, 0, v_1, u_1} K.toGradedObject ((up ℤ).π (up ℤ) (up ℤ)) n₁')
      x.negOnePow (Iso.hom (K.totalShift₁XIso x n₀ n₀' h₀) ≫ K.D₂ (up ℤ) n₀' n₁')

Tactic:
by_cases h : (up ℤ).Rel n₀ n₁

Premises used: Int, ComplexShape.Rel, ComplexShape.up
-- Module: Mathlib.Algebra.Homology.TotalComplexShift
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K : HomologicalComplex₂.{v_1, u_1, 0, 0} C (up ℤ) (up ℤ)
x : ℤ
inst_2 : K.HasTotal (up ℤ)
n₀ n₁ n₀' n₁' : ℤ
h₀ : n₀ + x = n₀'
h₁ : n₁ + x = n₁'
h : (up ℤ).Rel n₀ n₁
pos :
  ∀ (i₁ i₂ : ℤ) (hi : (up ℤ).π (up ℤ) (up ℤ) (i₁, i₂) = n₀),
    CategoryStruct.comp (Y := ((Functor.obj (shiftFunctor₁ C x) K).total (up ℤ)).X n₀)
        ((Functor.obj (shiftFunctor₁ C x) K).ιTotal (up ℤ) i₁ i₂ n₀ hi)
        ((Functor.obj (shiftFunctor₁ C x) K).D₂ (up ℤ) n₀ n₁ ≫ Iso.hom (K.totalShift₁XIso x n₁ n₁' h₁)) =
      (Functor.obj (shiftFunctor₁ C x) K).ιTotal (up ℤ) i₁ i₂ n₀ hi ≫
        HSMul.hSMul (β :=
          ((Functor.obj (shiftFunctor₁ C x) K).total (up ℤ)).X n₀ ⟶
            GradedObject.mapObj.{0, 0, v_1, u_1} K.toGradedObject ((up ℤ).π (up ℤ) (up ℤ)) n₁')
          x.negOnePow (Iso.hom (K.totalShift₁XIso x n₀ n₀' h₀) ≫ K.D₂ (up ℤ) n₀' n₁')
⊢ (Functor.obj (shiftFunctor₁ C x) K).D₂ (up ℤ) n₀ n₁ ≫ Iso.hom (K.totalShift₁XIso x n₁ n₁' h₁) =
    HSMul.hSMul (β :=
      ((Functor.obj (shiftFunctor₁ C x) K).total (up ℤ)).X n₀ ⟶
        GradedObject.mapObj.{0, 0, v_1, u_1} K.toGradedObject ((up ℤ).π (up ℤ) (up ℤ)) n₁')
      x.negOnePow (Iso.hom (K.totalShift₁XIso x n₀ n₀' h₀) ≫ K.D₂ (up ℤ) n₀' n₁')

Tactic:
apply total.hom_ext

Premises used: HomologicalComplex₂.total.hom_ext
-- Module: Mathlib.Algebra.Homology.TotalComplexShift
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K : HomologicalComplex₂.{v_1, u_1, 0, 0} C (up ℤ) (up ℤ)
x : ℤ
inst_2 : K.HasTotal (up ℤ)
n₀ n₁ n₀' n₁' : ℤ
h₀ : n₀ + x = n₀'
h₁ : n₁ + x = n₁'
h : n₀ + 1 = n₁
p q : ℤ
hpq : p + q = n₀
pos :
  CategoryStruct.comp (Y := ((Functor.obj (shiftFunctor₁ C x) K).total (up ℤ)).X n₀)
      ((Functor.obj (shiftFunctor₁ C x) K).ιTotal (up ℤ) p q n₀ hpq)
      ((Functor.obj (shiftFunctor₁ C x) K).D₂ (up ℤ) n₀ n₁ ≫
        (Functor.obj (shiftFunctor₁ C x) K).totalDesc fun (p q : ℤ) (hpq : p + q = n₁) ↦
          K.ιTotal (up ℤ) (p + x) q n₁' ⋯) =
    (Functor.obj (shiftFunctor₁ C x) K).ιTotal (up ℤ) p q n₀ hpq ≫
      HSMul.hSMul (β :=
        ((Functor.obj (shiftFunctor₁ C x) K).total (up ℤ)).X n₀ ⟶
          GradedObject.mapObj.{0, 0, v_1, u_1} K.toGradedObject ((up ℤ).π (up ℤ) (up ℤ)) n₁')
        x.negOnePow
        (((Functor.obj (shiftFunctor₁ C x) K).totalDesc fun (p q : ℤ) (hpq : p + q = n₀) ↦
            K.ιTotal (up ℤ) (p + x) q n₀' ⋯) ≫
          K.D₂ (up ℤ) n₀' n₁')
⊢ CategoryStruct.comp (Y := ((Functor.obj (shiftFunctor₁ C x) K).total (up ℤ)).X n₀)
      ((Functor.obj (shiftFunctor₁ C x) K).ιTotal (up ℤ) p q n₀ hpq)
      ((Functor.obj (shiftFunctor₁ C x) K).D₂ (up ℤ) n₀ n₁ ≫ Iso.hom (K.totalShift₁XIso x n₁ n₁' h₁)) =
    (Functor.obj (shiftFunctor₁ C x) K).ιTotal (up ℤ) p q n₀ hpq ≫
      HSMul.hSMul (β :=
        ((Functor.obj (shiftFunctor₁ C x) K).total (up ℤ)).X n₀ ⟶
          GradedObject.mapObj.{0, 0, v_1, u_1} K.toGradedObject ((up ℤ).π (up ℤ) (up ℤ)) n₁')
        x.negOnePow (Iso.hom (K.totalShift₁XIso x n₀ n₀' h₀) ≫ K.D₂ (up ℤ) n₀' n₁')

Tactic:
dsimp [totalShift₁XIso]

Premises used: HomologicalComplex₂.totalShift₁XIso
-- Module: Mathlib.Algebra.Homology.TotalComplexShift
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K : HomologicalComplex₂.{v_1, u_1, 0, 0} C (up ℤ) (up ℤ)
x : ℤ
inst_2 : K.HasTotal (up ℤ)
n₀ n₁ n₀' n₁' : ℤ
h₀ : n₀ + x = n₀'
h₁ : n₁ + x = n₁'
h : n₀ + 1 = n₁
p q : ℤ
hpq : p + q = n₀
⊢ p + (q + 1) = n₁

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.TotalComplexShift
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K : HomologicalComplex₂.{v_1, u_1, 0, 0} C (up ℤ) (up ℤ)
x : ℤ
inst_2 : K.HasTotal (up ℤ)
n₀ n₁ n₀' n₁' : ℤ
h₀ : n₀ + x = n₀'
h₁ : n₁ + x = n₁'
h : n₀ + 1 = n₁
p q : ℤ
hpq : p + q = n₀
⊢ p + x + (q + 1) = n₁'

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.TotalComplexShift
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K : HomologicalComplex₂.{v_1, u_1, 0, 0} C (up ℤ) (up ℤ)
x : ℤ
inst_2 : K.HasTotal (up ℤ)
n₀ n₁ n₀' n₁' : ℤ
h₀ : n₀ + x = n₀'
h₁ : n₁ + x = n₁'
h : n₀ + 1 = n₁
p q : ℤ
hpq : p + q = n₀
pos :
  HSMul.hSMul (β := ((Functor.obj (shiftFunctor₁ C x) K).X p).X q ⟶ (K.total (up ℤ)).X n₁')
      ((up ℤ).ε₂ (up ℤ) (up ℤ) (p, q))
      (((Functor.obj (shiftFunctor₁ C x) K).X p).d q (q + 1) ≫ K.ιTotal (up ℤ) (p + x) (q + 1) n₁' ⋯) =
    HSMul.hSMul (β := (K.X (p + x)).X q ⟶ (K.total (up ℤ)).X n₁') (x.negOnePow * (up ℤ).ε₂ (up ℤ) (up ℤ) (p + x, q))
      ((K.X (p + x)).d q (q + 1) ≫ K.ιTotal (up ℤ) (p + x) (q + 1) n₁' ⋯)
⊢ CategoryStruct.comp (Y := ((Functor.obj (shiftFunctor₁ C x) K).total (up ℤ)).X n₀)
      ((Functor.obj (shiftFunctor₁ C x) K).ιTotal (up ℤ) p q n₀ hpq)
      ((Functor.obj (shiftFunctor₁ C x) K).D₂ (up ℤ) n₀ n₁ ≫
        (Functor.obj (shiftFunctor₁ C x) K).totalDesc fun (p q : ℤ) (hpq : p + q = n₁) ↦
          K.ιTotal (up ℤ) (p + x) q n₁' ⋯) =
    (Functor.obj (shiftFunctor₁ C x) K).ιTotal (up ℤ) p q n₀ hpq ≫
      HSMul.hSMul (β :=
        ((Functor.obj (shiftFunctor₁ C x) K).total (up ℤ)).X n₀ ⟶
          GradedObject.mapObj.{0, 0, v_1, u_1} K.toGradedObject ((up ℤ).π (up ℤ) (up ℤ)) n₁')
        x.negOnePow
        (((Functor.obj (shiftFunctor₁ C x) K).totalDesc fun (p q : ℤ) (hpq : p + q = n₀) ↦
            K.ιTotal (up ℤ) (p + x) q n₀' ⋯) ≫
          K.D₂ (up ℤ) n₀' n₁')

Tactic:
rw [ι_D₂_assoc, Linear.comp_units_smul, ι_totalDesc_assoc, ι_D₂,
      ((shiftFunctor₁ C x).obj K).d₂_eq _ _ rfl _ (by dsimp; lia),
      K.d₂_eq _ _ rfl _ (by dsimp; lia), smul_smul,
      Linear.units_smul_comp, Category.assoc, ι_totalDesc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Linear.units_smul_comp, HomologicalComplex₂.ι_totalDesc_assoc, HomologicalComplex₂.ι_D₂, smul_smul, HomologicalComplex₂.ι_D₂_assoc, HomologicalComplex₂.ι_totalDesc, CategoryTheory.Linear.comp_units_smul, HomologicalComplex₂.shiftFunctor₁, HomologicalComplex₂.d₂_eq, CategoryTheory.Functor.obj, rfl
-- Module: Mathlib.Algebra.Homology.TotalComplexShift
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K : HomologicalComplex₂.{v_1, u_1, 0, 0} C (up ℤ) (up ℤ)
x : ℤ
inst_2 : K.HasTotal (up ℤ)
n₀ n₁ n₀' n₁' : ℤ
h₀ : n₀ + x = n₀'
h₁ : n₁ + x = n₁'
h : n₀ + 1 = n₁
p q : ℤ
hpq : p + q = n₀
pos :
  HSMul.hSMul (β := (K.X (p + x)).X q ⟶ (K.total (up ℤ)).X n₁') p.negOnePow
      ((K.X (p + x)).d q (q + 1) ≫ K.ιTotal (up ℤ) (p + x) (q + 1) n₁' ⋯) =
    HSMul.hSMul (β := (K.X (p + x)).X q ⟶ (K.total (up ℤ)).X n₁') (x.negOnePow * (p + x).negOnePow)
      ((K.X (p + x)).d q (q + 1) ≫ K.ιTotal (up ℤ) (p + x) (q + 1) n₁' ⋯)
⊢ HSMul.hSMul (β := ((Functor.obj (shiftFunctor₁ C x) K).X p).X q ⟶ (K.total (up ℤ)).X n₁')
      ((up ℤ).ε₂ (up ℤ) (up ℤ) (p, q))
      (((Functor.obj (shiftFunctor₁ C x) K).X p).d q (q + 1) ≫ K.ιTotal (up ℤ) (p + x) (q + 1) n₁' ⋯) =
    HSMul.hSMul (β := (K.X (p + x)).X q ⟶ (K.total (up ℤ)).X n₁') (x.negOnePow * (up ℤ).ε₂ (up ℤ) (up ℤ) (p + x, q))
      ((K.X (p + x)).d q (q + 1) ≫ K.ιTotal (up ℤ) (p + x) (q + 1) n₁' ⋯)

Tactic:
dsimp
-- Module: Mathlib.Algebra.Homology.TotalComplexShift
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K : HomologicalComplex₂.{v_1, u_1, 0, 0} C (up ℤ) (up ℤ)
x : ℤ
inst_2 : K.HasTotal (up ℤ)
n₀ n₁ n₀' n₁' : ℤ
h₀ : n₀ + x = n₀'
h₁ : n₁ + x = n₁'
h : n₀ + 1 = n₁
p q : ℤ
hpq : p + q = n₀
pos : p.negOnePow = x.negOnePow * (p + x).negOnePow
⊢ HSMul.hSMul (β := (K.X (p + x)).X q ⟶ (K.total (up ℤ)).X n₁') p.negOnePow
      ((K.X (p + x)).d q (q + 1) ≫ K.ιTotal (up ℤ) (p + x) (q + 1) n₁' ⋯) =
    HSMul.hSMul (β := (K.X (p + x)).X q ⟶ (K.total (up ℤ)).X n₁') (x.negOnePow * (p + x).negOnePow)
      ((K.X (p + x)).d q (q + 1) ≫ K.ιTotal (up ℤ) (p + x) (q + 1) n₁' ⋯)

Tactic:
congr 1
-- Module: Mathlib.Algebra.Homology.TotalComplexShift
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K : HomologicalComplex₂.{v_1, u_1, 0, 0} C (up ℤ) (up ℤ)
x : ℤ
inst_2 : K.HasTotal (up ℤ)
n₀ n₁ n₀' n₁' : ℤ
h₀ : n₀ + x = n₀'
h₁ : n₁ + x = n₁'
h : n₀ + 1 = n₁
p q : ℤ
hpq : p + q = n₀
pos : p.negOnePow = x.negOnePow * (x + p).negOnePow
pos₁ : p.negOnePow = x.negOnePow * (x.negOnePow * p.negOnePow)
pos₂ : p.negOnePow = x.negOnePow * x.negOnePow * p.negOnePow
pos₃ : p.negOnePow = 1 * p.negOnePow
pos₄ pos₅ : p.negOnePow = p.negOnePow
⊢ p.negOnePow = x.negOnePow * (p + x).negOnePow

Tactic:
rw [add_comm p, Int.negOnePow_add, ← mul_assoc, Int.units_mul_self, one_mul]

Premises used: mul_assoc, Int.negOnePow_add, add_comm, one_mul, Int.units_mul_self
-- Module: Mathlib.Algebra.Homology.TotalComplexShift
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K : HomologicalComplex₂.{v_1, u_1, 0, 0} C (up ℤ) (up ℤ)
x : ℤ
inst_2 : K.HasTotal (up ℤ)
n₀ n₁ n₀' n₁' : ℤ
h₀ : n₀ + x = n₀'
h₁ : n₁ + x = n₁'
h : ¬(up ℤ).Rel n₀ n₁
neg : ¬(up ℤ).Rel n₀' n₁'
⊢ (Functor.obj (shiftFunctor₁ C x) K).D₂ (up ℤ) n₀ n₁ ≫ Iso.hom (K.totalShift₁XIso x n₁ n₁' h₁) =
    HSMul.hSMul (β :=
      ((Functor.obj (shiftFunctor₁ C x) K).total (up ℤ)).X n₀ ⟶
        GradedObject.mapObj.{0, 0, v_1, u_1} K.toGradedObject ((up ℤ).π (up ℤ) (up ℤ)) n₁')
      x.negOnePow (Iso.hom (K.totalShift₁XIso x n₀ n₀' h₀) ≫ K.D₂ (up ℤ) n₀' n₁')

Tactic:
rw [D₂_shape _ _ _ _ h, zero_comp, D₂_shape, comp_zero, smul_zero]

Premises used: CategoryTheory.Limits.comp_zero, smul_zero, HomologicalComplex₂.D₂_shape, CategoryTheory.Limits.zero_comp
-- Module: Mathlib.Algebra.Homology.TotalComplexShift
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K L : HomologicalComplex₂.{v_1, u_1, 0, 0} C (up ℤ) (up ℤ)
f : K ⟶ L
x y : ℤ
inst_2 : K.HasTotal (up ℤ)
n n' : ℤ
h : (up ℤ).Rel n n'
dsimp :
  Iso.hom (K.totalShift₁XIso x n (n + x) ⋯) ≫
      HSMul.hSMul (β := (K.total (up ℤ)).X (n + x) ⟶ (K.total (up ℤ)).X (n' + x)) x.negOnePow
        ((K.total (up ℤ)).d (n + x) (n' + x)) =
    ((Functor.obj (shiftFunctor₁ C x) K).total (up ℤ)).d n n' ≫ Iso.hom (K.totalShift₁XIso x n' (n' + x) ⋯)
⊢ Iso.hom
        ((fun (n : ℤ) ↦
            (K.totalShift₁XIso x n (n + x) ⋯ :
              ((Functor.obj (shiftFunctor₁ C x) K).total (up ℤ)).X n ≅ (K.total (up ℤ)).X (n + x)))
          n) ≫
      (Functor.obj (shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) x) (K.total (up ℤ))).d n n' =
    ((Functor.obj (shiftFunctor₁ C x) K).total (up ℤ)).d n n' ≫
      Iso.hom
        ((fun (n : ℤ) ↦
            (K.totalShift₁XIso x n (n + x) ⋯ :
              ((Functor.obj (shiftFunctor₁ C x) K).total (up ℤ)).X n ≅ (K.total (up ℤ)).X (n + x)))
          n')

Tactic:
dsimp
-- Module: Mathlib.Algebra.Homology.TotalComplexShift
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K L : HomologicalComplex₂.{v_1, u_1, 0, 0} C (up ℤ) (up ℤ)
f : K ⟶ L
x y : ℤ
inst_2 : K.HasTotal (up ℤ)
n n' : ℤ
h : (up ℤ).Rel n n'
⊢ Iso.hom (K.totalShift₁XIso x n (n + x) ⋯) ≫
      HSMul.hSMul (β := (K.total (up ℤ)).X (n + x) ⟶ (K.total (up ℤ)).X (n' + x)) x.negOnePow
        ((K.total (up ℤ)).d (n + x) (n' + x)) =
    ((Functor.obj (shiftFunctor₁ C x) K).total (up ℤ)).d n n' ≫ Iso.hom (K.totalShift₁XIso x n' (n' + x) ⋯)

Tactic:
simp only [total_d, Preadditive.add_comp, Preadditive.comp_add, smul_add,
        Linear.comp_units_smul, K.D₁_totalShift₁XIso_hom x n n' _ _ rfl rfl,
        K.D₂_totalShift₁XIso_hom x n n' _ _ rfl rfl]

Premises used: CategoryTheory.Linear.comp_units_smul, HomologicalComplex₂.D₁_totalShift₁XIso_hom, HomologicalComplex₂.D₂_totalShift₁XIso_hom, CategoryTheory.Preadditive.add_comp, CategoryTheory.Preadditive.comp_add, HomologicalComplex₂.total_d, smul_add, rfl
-- Module: Mathlib.Algebra.Homology.TotalComplexShift
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K L : HomologicalComplex₂.{v_1, u_1, 0, 0} C (up ℤ) (up ℤ)
f : K ⟶ L
x y : ℤ
inst_2 : K.HasTotal (up ℤ)
a b n : ℤ
h : a + b = n
a' : ℤ
ha' : a' = a + x
n' : ℤ
hn' : n' = n + x
⊢ a' + b = n'

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.TotalComplexShift
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K : HomologicalComplex₂.{v_1, u_1, 0, 0} C (up ℤ) (up ℤ)
x : ℤ
inst_2 : K.HasTotal (up ℤ)
a b n : ℤ
h : a + b = n
a' : ℤ
ha' : a' = a + x
n' : ℤ
hn' : n' = n + x
subst :
  (Functor.obj (shiftFunctor₁ C x) K).ιTotal (up ℤ) a b n h ≫
      HomologicalComplex.Hom.f (Iso.hom (K.totalShift₁Iso x)) n =
    (K.shiftFunctor₁XXIso a x (a + x) ⋯ b).hom ≫
      K.ιTotal (up ℤ) (a + x) b (n + x) ⋯ ≫ (CochainComplex.shiftFunctorObjXIso (K.total (up ℤ)) x n (n + x) ⋯).inv
⊢ (Functor.obj (shiftFunctor₁ C x) K).ιTotal (up ℤ) a b n h ≫
      HomologicalComplex.Hom.f (Iso.hom (K.totalShift₁Iso x)) n =
    (K.shiftFunctor₁XXIso a x a' ha' b).hom ≫
      K.ιTotal (up ℤ) a' b n' ⋯ ≫ (CochainComplex.shiftFunctorObjXIso (K.total (up ℤ)) x n n' hn').inv

Tactic:
subst ha' hn'
-- Module: Mathlib.Algebra.Homology.TotalComplexShift
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K : HomologicalComplex₂.{v_1, u_1, 0, 0} C (up ℤ) (up ℤ)
x : ℤ
inst_2 : K.HasTotal (up ℤ)
a b n : ℤ
h : a + b = n
dsimp :
  CategoryStruct.comp (Y := ((Functor.obj (shiftFunctor₁ C x) K).total (up ℤ)).X n)
      ((Functor.obj (shiftFunctor₁ C x) K).ιTotal (up ℤ) a b n h)
      ((Functor.obj (shiftFunctor₁ C x) K).totalDesc fun (p q : ℤ) (hpq : p + q = n) ↦
        K.ιTotal (up ℤ) (p + x) q (n + x) ⋯) =
    𝟙 ((K.X (a + x)).X b) ≫ K.ιTotal (up ℤ) (a + x) b (n + x) ⋯ ≫ 𝟙 ((K.total (up ℤ)).X (n + x))
⊢ (Functor.obj (shiftFunctor₁ C x) K).ιTotal (up ℤ) a b n h ≫
      HomologicalComplex.Hom.f (Iso.hom (K.totalShift₁Iso x)) n =
    (K.shiftFunctor₁XXIso a x (a + x) ⋯ b).hom ≫
      K.ιTotal (up ℤ) (a + x) b (n + x) ⋯ ≫ (CochainComplex.shiftFunctorObjXIso (K.total (up ℤ)) x n (n + x) ⋯).inv

Tactic:
dsimp [totalShift₁Iso, totalShift₁XIso]

Premises used: HomologicalComplex₂.totalShift₁XIso, HomologicalComplex₂.totalShift₁Iso
-- Module: Mathlib.Algebra.Homology.TotalComplexShift
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K : HomologicalComplex₂.{v_1, u_1, 0, 0} C (up ℤ) (up ℤ)
x : ℤ
inst_2 : K.HasTotal (up ℤ)
a b n : ℤ
h : a + b = n
⊢ CategoryStruct.comp (Y := ((Functor.obj (shiftFunctor₁ C x) K).total (up ℤ)).X n)
      ((Functor.obj (shiftFunctor₁ C x) K).ιTotal (up ℤ) a b n h)
      ((Functor.obj (shiftFunctor₁ C x) K).totalDesc fun (p q : ℤ) (hpq : p + q = n) ↦
        K.ιTotal (up ℤ) (p + x) q (n + x) ⋯) =
    𝟙 ((K.X (a + x)).X b) ≫ K.ιTotal (up ℤ) (a + x) b (n + x) ⋯ ≫ 𝟙 ((K.total (up ℤ)).X (n + x))

Tactic:
simp only [ι_totalDesc, comp_id, id_comp]

Premises used: HomologicalComplex₂.ι_totalDesc, CategoryTheory.Category.comp_id, CategoryTheory.Category.id_comp
-- Module: Mathlib.Algebra.Homology.TotalComplexShift
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K L : HomologicalComplex₂.{v_1, u_1, 0, 0} C (up ℤ) (up ℤ)
f : K ⟶ L
x y : ℤ
inst_2 : K.HasTotal (up ℤ)
a b n : ℤ
h : a + b = n
a' n' : ℤ
ha' : a' + b = n'
hn' : n' = n + x
⊢ a' = a + x

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.TotalComplexShift
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K : HomologicalComplex₂.{v_1, u_1, 0, 0} C (up ℤ) (up ℤ)
x : ℤ
inst_2 : K.HasTotal (up ℤ)
a b n : ℤ
h : a + b = n
a' n' : ℤ
ha' : a' + b = n'
hn' : n' = n + x
subst :
  ∀ (ha' : a' + b = n + x),
    K.ιTotal (up ℤ) a' b (n + x) ha' ≫
        (CochainComplex.shiftFunctorObjXIso (K.total (up ℤ)) x n (n + x) ⋯).inv ≫
          HomologicalComplex.Hom.f (Iso.inv (K.totalShift₁Iso x)) n =
      (K.shiftFunctor₁XXIso a x a' ⋯ b).inv ≫ (Functor.obj (shiftFunctor₁ C x) K).ιTotal (up ℤ) a b n h
⊢ K.ιTotal (up ℤ) a' b n' ha' ≫
      (CochainComplex.shiftFunctorObjXIso (K.total (up ℤ)) x n n' hn').inv ≫
        HomologicalComplex.Hom.f (Iso.inv (K.totalShift₁Iso x)) n =
    (K.shiftFunctor₁XXIso a x a' ⋯ b).inv ≫ (Functor.obj (shiftFunctor₁ C x) K).ιTotal (up ℤ) a b n h

Tactic:
subst hn'
-- Module: Mathlib.Algebra.Homology.TotalComplexShift
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K : HomologicalComplex₂.{v_1, u_1, 0, 0} C (up ℤ) (up ℤ)
x : ℤ
inst_2 : K.HasTotal (up ℤ)
a b n : ℤ
h : a + b = n
a' : ℤ
ha' : a' + b = n + x
⊢ a = a' - x

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.TotalComplexShift
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K : HomologicalComplex₂.{v_1, u_1, 0, 0} C (up ℤ) (up ℤ)
x : ℤ
inst_2 : K.HasTotal (up ℤ)
a b n : ℤ
h : a + b = n
a' : ℤ
ha' : a' + b = n + x
obtain :
  ∀ (h : a' - x + b = n),
    K.ιTotal (up ℤ) a' b (n + x) ha' ≫
        (CochainComplex.shiftFunctorObjXIso (K.total (up ℤ)) x n (n + x) ⋯).inv ≫
          HomologicalComplex.Hom.f (Iso.inv (K.totalShift₁Iso x)) n =
      (K.shiftFunctor₁XXIso (a' - x) x a' ⋯ b).inv ≫ (Functor.obj (shiftFunctor₁ C x) K).ιTotal (up ℤ) (a' - x) b n h
⊢ K.ιTotal (up ℤ) a' b (n + x) ha' ≫
      (CochainComplex.shiftFunctorObjXIso (K.total (up ℤ)) x n (n + x) ⋯).inv ≫
        HomologicalComplex.Hom.f (Iso.inv (K.totalShift₁Iso x)) n =
    (K.shiftFunctor₁XXIso a x a' ⋯ b).inv ≫ (Functor.obj (shiftFunctor₁ C x) K).ιTotal (up ℤ) a b n h

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

Premises used: rfl