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 L : HomologicalComplex₂.{v_1, u_1, 0, 0} C (up ℤ) (up ℤ)
f : K ⟶ L
x y : ℤ
inst_2 : K.HasTotal (up ℤ)
n n' : ℤ
h : n + y = n'
i₁ i₂ : ℤ
hi : (up ℤ).π (up ℤ) (up ℤ) (i₁, i₂) = n'
⊢ CategoryStruct.comp (Y := (K.total (up ℤ)).X n') (K.ιTotal (up ℤ) i₁ i₂ n' hi)
      (CategoryStruct.comp (Y := ((Functor.obj (shiftFunctor₂ C y) K).total (up ℤ)).X n)
        (K.totalDesc fun (p q : ℤ) (hpq : p + q = n') ↦
          HSMul.hSMul (β := (K.X p).X q ⟶ ((Functor.obj (shiftFunctor₂ C y) K).total (up ℤ)).X n) (p * y).negOnePow
            (Iso.inv (XXIsoOfEq C (up ℤ) (up ℤ) K ⋯ ⋯) ≫
              (Functor.obj (shiftFunctor₂ C y) K).ιTotal (up ℤ) p (q - y) n ⋯))
        ((Functor.obj (shiftFunctor₂ C y) K).totalDesc fun (p q : ℤ) (hpq : p + q = n) ↦
          HSMul.hSMul (β := (K.X p).X (q + y) ⟶ (K.total (up ℤ)).X n') (p * y).negOnePow
            (K.ιTotal (up ℤ) p (q + y) n' ⋯))) =
    K.ιTotal (up ℤ) i₁ i₂ n' hi ≫ 𝟙 ((K.total (up ℤ)).X n')

Tactic:
simp only [ι_totalDesc_assoc, Linear.units_smul_comp, Category.assoc, ι_totalDesc,
      Linear.comp_units_smul, XXIsoOfEq_inv_ιTotal, smul_smul, Int.units_mul_self, one_smul,
      comp_id]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Linear.units_smul_comp, HomologicalComplex₂.ι_totalDesc_assoc, smul_smul, HomologicalComplex₂.ι_totalDesc, CategoryTheory.Linear.comp_units_smul, CategoryTheory.Category.comp_id, one_smul, HomologicalComplex₂.XXIsoOfEq_inv_ιTotal, 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 ℤ)
y : ℤ
inst_2 : K.HasTotal (up ℤ)
n₀ n₁ n₀' n₁' : ℤ
h₀ : n₀ + y = n₀'
h₁ : n₁ + y = n₁'
pos :
  ∀ (h : (up ℤ).Rel n₀ n₁),
    (Functor.obj (shiftFunctor₂ C y) K).D₁ (up ℤ) n₀ n₁ ≫ Iso.hom (K.totalShift₂XIso y n₁ n₁' h₁) =
      HSMul.hSMul (β :=
        ((Functor.obj (shiftFunctor₂ C y) K).total (up ℤ)).X n₀ ⟶
          GradedObject.mapObj.{0, 0, v_1, u_1} K.toGradedObject ((up ℤ).π (up ℤ) (up ℤ)) n₁')
        y.negOnePow (Iso.hom (K.totalShift₂XIso y n₀ n₀' h₀) ≫ K.D₁ (up ℤ) n₀' n₁')
neg :
  ∀ (h : ¬(up ℤ).Rel n₀ n₁),
    (Functor.obj (shiftFunctor₂ C y) K).D₁ (up ℤ) n₀ n₁ ≫ Iso.hom (K.totalShift₂XIso y n₁ n₁' h₁) =
      HSMul.hSMul (β :=
        ((Functor.obj (shiftFunctor₂ C y) K).total (up ℤ)).X n₀ ⟶
          GradedObject.mapObj.{0, 0, v_1, u_1} K.toGradedObject ((up ℤ).π (up ℤ) (up ℤ)) n₁')
        y.negOnePow (Iso.hom (K.totalShift₂XIso y n₀ n₀' h₀) ≫ K.D₁ (up ℤ) n₀' n₁')
⊢ (Functor.obj (shiftFunctor₂ C y) K).D₁ (up ℤ) n₀ n₁ ≫ Iso.hom (K.totalShift₂XIso y n₁ n₁' h₁) =
    HSMul.hSMul (β :=
      ((Functor.obj (shiftFunctor₂ C y) K).total (up ℤ)).X n₀ ⟶
        GradedObject.mapObj.{0, 0, v_1, u_1} K.toGradedObject ((up ℤ).π (up ℤ) (up ℤ)) n₁')
      y.negOnePow (Iso.hom (K.totalShift₂XIso y 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 ℤ)
y : ℤ
inst_2 : K.HasTotal (up ℤ)
n₀ n₁ n₀' n₁' : ℤ
h₀ : n₀ + y = n₀'
h₁ : n₁ + y = n₁'
h : (up ℤ).Rel n₀ n₁
pos :
  ∀ (i₁ i₂ : ℤ) (hi : (up ℤ).π (up ℤ) (up ℤ) (i₁, i₂) = n₀),
    CategoryStruct.comp (Y := ((Functor.obj (shiftFunctor₂ C y) K).total (up ℤ)).X n₀)
        ((Functor.obj (shiftFunctor₂ C y) K).ιTotal (up ℤ) i₁ i₂ n₀ hi)
        ((Functor.obj (shiftFunctor₂ C y) K).D₁ (up ℤ) n₀ n₁ ≫ Iso.hom (K.totalShift₂XIso y n₁ n₁' h₁)) =
      (Functor.obj (shiftFunctor₂ C y) K).ιTotal (up ℤ) i₁ i₂ n₀ hi ≫
        HSMul.hSMul (β :=
          ((Functor.obj (shiftFunctor₂ C y) K).total (up ℤ)).X n₀ ⟶
            GradedObject.mapObj.{0, 0, v_1, u_1} K.toGradedObject ((up ℤ).π (up ℤ) (up ℤ)) n₁')
          y.negOnePow (Iso.hom (K.totalShift₂XIso y n₀ n₀' h₀) ≫ K.D₁ (up ℤ) n₀' n₁')
⊢ (Functor.obj (shiftFunctor₂ C y) K).D₁ (up ℤ) n₀ n₁ ≫ Iso.hom (K.totalShift₂XIso y n₁ n₁' h₁) =
    HSMul.hSMul (β :=
      ((Functor.obj (shiftFunctor₂ C y) K).total (up ℤ)).X n₀ ⟶
        GradedObject.mapObj.{0, 0, v_1, u_1} K.toGradedObject ((up ℤ).π (up ℤ) (up ℤ)) n₁')
      y.negOnePow (Iso.hom (K.totalShift₂XIso y 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 ℤ)
y : ℤ
inst_2 : K.HasTotal (up ℤ)
n₀ n₁ n₀' n₁' : ℤ
h₀ : n₀ + y = n₀'
h₁ : n₁ + y = n₁'
h : n₀ + 1 = n₁
p q : ℤ
hpq : p + q = n₀
pos :
  CategoryStruct.comp (Y := ((Functor.obj (shiftFunctor₂ C y) K).total (up ℤ)).X n₀)
      ((Functor.obj (shiftFunctor₂ C y) K).ιTotal (up ℤ) p q n₀ hpq)
      ((Functor.obj (shiftFunctor₂ C y) K).D₁ (up ℤ) n₀ n₁ ≫
        (Functor.obj (shiftFunctor₂ C y) K).totalDesc fun (p q : ℤ) (hpq : p + q = n₁) ↦
          HSMul.hSMul (β := (K.X p).X (q + y) ⟶ (K.total (up ℤ)).X n₁') (p * y).negOnePow
            (K.ιTotal (up ℤ) p (q + y) n₁' ⋯)) =
    (Functor.obj (shiftFunctor₂ C y) K).ιTotal (up ℤ) p q n₀ hpq ≫
      HSMul.hSMul (β :=
        ((Functor.obj (shiftFunctor₂ C y) K).total (up ℤ)).X n₀ ⟶
          GradedObject.mapObj.{0, 0, v_1, u_1} K.toGradedObject ((up ℤ).π (up ℤ) (up ℤ)) n₁')
        y.negOnePow
        (((Functor.obj (shiftFunctor₂ C y) K).totalDesc fun (p q : ℤ) (hpq : p + q = n₀) ↦
            HSMul.hSMul (β := (K.X p).X (q + y) ⟶ (K.total (up ℤ)).X n₀') (p * y).negOnePow
              (K.ιTotal (up ℤ) p (q + y) n₀' ⋯)) ≫
          K.D₁ (up ℤ) n₀' n₁')
⊢ CategoryStruct.comp (Y := ((Functor.obj (shiftFunctor₂ C y) K).total (up ℤ)).X n₀)
      ((Functor.obj (shiftFunctor₂ C y) K).ιTotal (up ℤ) p q n₀ hpq)
      ((Functor.obj (shiftFunctor₂ C y) K).D₁ (up ℤ) n₀ n₁ ≫ Iso.hom (K.totalShift₂XIso y n₁ n₁' h₁)) =
    (Functor.obj (shiftFunctor₂ C y) K).ιTotal (up ℤ) p q n₀ hpq ≫
      HSMul.hSMul (β :=
        ((Functor.obj (shiftFunctor₂ C y) K).total (up ℤ)).X n₀ ⟶
          GradedObject.mapObj.{0, 0, v_1, u_1} K.toGradedObject ((up ℤ).π (up ℤ) (up ℤ)) n₁')
        y.negOnePow (Iso.hom (K.totalShift₂XIso y 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 ℤ)
y : ℤ
inst_2 : K.HasTotal (up ℤ)
n₀ n₁ n₀' n₁' : ℤ
h₀ : n₀ + y = n₀'
h₁ : n₁ + y = n₁'
h : n₀ + 1 = n₁
p q : ℤ
hpq : p + q = n₀
⊢ p + 1 + q = 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 ℤ)
y : ℤ
inst_2 : K.HasTotal (up ℤ)
n₀ n₁ n₀' n₁' : ℤ
h₀ : n₀ + y = n₀'
h₁ : n₁ + y = n₁'
h : n₀ + 1 = n₁
p q : ℤ
hpq : p + q = n₀
⊢ p + 1 + (q + y) = 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 ℤ)
y : ℤ
inst_2 : K.HasTotal (up ℤ)
n₀ n₁ n₀' n₁' : ℤ
h₀ : n₀ + y = n₀'
h₁ : n₁ + y = n₁'
h : n₀ + 1 = n₁
p q : ℤ
hpq : p + q = n₀
pos :
  (HSMul.hSMul (β :=
        ((Functor.obj (shiftFunctor₂ C y) K).X p).X q ⟶ ((Functor.obj (shiftFunctor₂ C y) K).total (up ℤ)).X n₁)
        ((up ℤ).ε₁ (up ℤ) (up ℤ) (p, q))
        (HomologicalComplex.Hom.f ((Functor.obj (shiftFunctor₂ C y) K).d p (p + 1)) q ≫
          (Functor.obj (shiftFunctor₂ C y) K).ιTotal (up ℤ) (p + 1) q n₁ ⋯) ≫
      (Functor.obj (shiftFunctor₂ C y) K).totalDesc fun (p q : ℤ) (hpq : p + q = n₁) ↦
        HSMul.hSMul (β := (K.X p).X (q + y) ⟶ (K.total (up ℤ)).X n₁') (p * y).negOnePow
          (K.ιTotal (up ℤ) p (q + y) n₁' ⋯)) =
    (y.negOnePow * (p * y).negOnePow) •
      HSMul.hSMul (β := (K.X p).X (q + y) ⟶ (K.total (up ℤ)).X n₁') ((up ℤ).ε₁ (up ℤ) (up ℤ) (p, q + y))
        (HomologicalComplex.Hom.f (K.d p (p + 1)) (q + y) ≫ K.ιTotal (up ℤ) (p + 1) (q + y) n₁' ⋯)
⊢ CategoryStruct.comp (Y := ((Functor.obj (shiftFunctor₂ C y) K).total (up ℤ)).X n₀)
      ((Functor.obj (shiftFunctor₂ C y) K).ιTotal (up ℤ) p q n₀ hpq)
      ((Functor.obj (shiftFunctor₂ C y) K).D₁ (up ℤ) n₀ n₁ ≫
        (Functor.obj (shiftFunctor₂ C y) K).totalDesc fun (p q : ℤ) (hpq : p + q = n₁) ↦
          HSMul.hSMul (β := (K.X p).X (q + y) ⟶ (K.total (up ℤ)).X n₁') (p * y).negOnePow
            (K.ιTotal (up ℤ) p (q + y) n₁' ⋯)) =
    (Functor.obj (shiftFunctor₂ C y) K).ιTotal (up ℤ) p q n₀ hpq ≫
      HSMul.hSMul (β :=
        ((Functor.obj (shiftFunctor₂ C y) K).total (up ℤ)).X n₀ ⟶
          GradedObject.mapObj.{0, 0, v_1, u_1} K.toGradedObject ((up ℤ).π (up ℤ) (up ℤ)) n₁')
        y.negOnePow
        (((Functor.obj (shiftFunctor₂ C y) K).totalDesc fun (p q : ℤ) (hpq : p + q = n₀) ↦
            HSMul.hSMul (β := (K.X p).X (q + y) ⟶ (K.total (up ℤ)).X n₀') (p * y).negOnePow
              (K.ιTotal (up ℤ) p (q + y) n₀' ⋯)) ≫
          K.D₁ (up ℤ) n₀' n₁')

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

Premises used: HomologicalComplex₂.ι_D₁_assoc, CategoryTheory.Linear.units_smul_comp, HomologicalComplex₂.ι_totalDesc_assoc, HomologicalComplex₂.d₁_eq, smul_smul, 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 ℤ)
y : ℤ
inst_2 : K.HasTotal (up ℤ)
n₀ n₁ n₀' n₁' : ℤ
h₀ : n₀ + y = n₀'
h₁ : n₁ + y = n₁'
h : n₀ + 1 = n₁
p q : ℤ
hpq : p + q = n₀
pos :
  (HSMul.hSMul (α := ℤˣ) (β := (K.X p).X (q + y) ⟶ ((Functor.obj (shiftFunctor₂ C y) K).total (up ℤ)).X n₁) 1
        (HomologicalComplex.Hom.f (K.d p (p + 1)) (q + y) ≫
          (Functor.obj (shiftFunctor₂ C y) K).ιTotal (up ℤ) (p + 1) q n₁ ⋯) ≫
      (Functor.obj (shiftFunctor₂ C y) K).totalDesc fun (p q : ℤ) (hpq : p + q = n₁) ↦
        HSMul.hSMul (β := (K.X p).X (q + y) ⟶ (K.total (up ℤ)).X n₁') (p * y).negOnePow
          (K.ιTotal (up ℤ) p (q + y) n₁' ⋯)) =
    (y.negOnePow * (p * y).negOnePow) •
      HSMul.hSMul (α := ℤˣ) (β := (K.X p).X (q + y) ⟶ (K.total (up ℤ)).X n₁') 1
        (HomologicalComplex.Hom.f (K.d p (p + 1)) (q + y) ≫ K.ιTotal (up ℤ) (p + 1) (q + y) n₁' ⋯)
⊢ (HSMul.hSMul (β :=
        ((Functor.obj (shiftFunctor₂ C y) K).X p).X q ⟶ ((Functor.obj (shiftFunctor₂ C y) K).total (up ℤ)).X n₁)
        ((up ℤ).ε₁ (up ℤ) (up ℤ) (p, q))
        (HomologicalComplex.Hom.f ((Functor.obj (shiftFunctor₂ C y) K).d p (p + 1)) q ≫
          (Functor.obj (shiftFunctor₂ C y) K).ιTotal (up ℤ) (p + 1) q n₁ ⋯) ≫
      (Functor.obj (shiftFunctor₂ C y) K).totalDesc fun (p q : ℤ) (hpq : p + q = n₁) ↦
        HSMul.hSMul (β := (K.X p).X (q + y) ⟶ (K.total (up ℤ)).X n₁') (p * y).negOnePow
          (K.ιTotal (up ℤ) p (q + y) n₁' ⋯)) =
    (y.negOnePow * (p * y).negOnePow) •
      HSMul.hSMul (β := (K.X p).X (q + y) ⟶ (K.total (up ℤ)).X n₁') ((up ℤ).ε₁ (up ℤ) (up ℤ) (p, q + y))
        (HomologicalComplex.Hom.f (K.d p (p + 1)) (q + y) ≫ K.ιTotal (up ℤ) (p + 1) (q + y) 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 ℤ)
y : ℤ
inst_2 : K.HasTotal (up ℤ)
n₀ n₁ n₀' n₁' : ℤ
h₀ : n₀ + y = n₀'
h₁ : n₁ + y = n₁'
h : n₀ + 1 = n₁
p q : ℤ
hpq : p + q = n₀
pos :
  HSMul.hSMul (β := (K.X p).X (q + y) ⟶ (K.total (up ℤ)).X n₁') ((p + 1) * y).negOnePow
      (HomologicalComplex.Hom.f (K.d p (p + 1)) (q + y) ≫ K.ιTotal (up ℤ) (p + 1) (q + y) n₁' ⋯) =
    HSMul.hSMul (β := (K.X p).X (q + y) ⟶ (K.total (up ℤ)).X n₁') (y + p * y).negOnePow
      (HomologicalComplex.Hom.f (K.d p (p + 1)) (q + y) ≫ K.ιTotal (up ℤ) (p + 1) (q + y) n₁' ⋯)
⊢ (HSMul.hSMul (α := ℤˣ) (β := (K.X p).X (q + y) ⟶ ((Functor.obj (shiftFunctor₂ C y) K).total (up ℤ)).X n₁) 1
        (HomologicalComplex.Hom.f (K.d p (p + 1)) (q + y) ≫
          (Functor.obj (shiftFunctor₂ C y) K).ιTotal (up ℤ) (p + 1) q n₁ ⋯) ≫
      (Functor.obj (shiftFunctor₂ C y) K).totalDesc fun (p q : ℤ) (hpq : p + q = n₁) ↦
        HSMul.hSMul (β := (K.X p).X (q + y) ⟶ (K.total (up ℤ)).X n₁') (p * y).negOnePow
          (K.ιTotal (up ℤ) p (q + y) n₁' ⋯)) =
    (y.negOnePow * (p * y).negOnePow) •
      HSMul.hSMul (α := ℤˣ) (β := (K.X p).X (q + y) ⟶ (K.total (up ℤ)).X n₁') 1
        (HomologicalComplex.Hom.f (K.d p (p + 1)) (q + y) ≫ K.ιTotal (up ℤ) (p + 1) (q + y) n₁' ⋯)

Tactic:
rw [one_smul, one_smul, Category.assoc, ι_totalDesc, Linear.comp_units_smul,
      ← Int.negOnePow_add]

Premises used: CategoryTheory.Category.assoc, Int.negOnePow_add, HomologicalComplex₂.ι_totalDesc, CategoryTheory.Linear.comp_units_smul, one_smul
-- 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 ℤ)
y : ℤ
inst_2 : K.HasTotal (up ℤ)
n₀ n₁ n₀' n₁' : ℤ
h₀ : n₀ + y = n₀'
h₁ : n₁ + y = n₁'
h : n₀ + 1 = n₁
p q : ℤ
hpq : p + q = n₀
pos : (p + 1) * y = y + p * y
⊢ HSMul.hSMul (β := (K.X p).X (q + y) ⟶ (K.total (up ℤ)).X n₁') ((p + 1) * y).negOnePow
      (HomologicalComplex.Hom.f (K.d p (p + 1)) (q + y) ≫ K.ιTotal (up ℤ) (p + 1) (q + y) n₁' ⋯) =
    HSMul.hSMul (β := (K.X p).X (q + y) ⟶ (K.total (up ℤ)).X n₁') (y + p * y).negOnePow
      (HomologicalComplex.Hom.f (K.d p (p + 1)) (q + y) ≫ K.ιTotal (up ℤ) (p + 1) (q + y) n₁' ⋯)

Tactic:
congr 2
-- 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 ℤ)
y : ℤ
inst_2 : K.HasTotal (up ℤ)
n₀ n₁ n₀' n₁' : ℤ
h₀ : n₀ + y = n₀'
h₁ : n₁ + y = n₁'
h : n₀ + 1 = n₁
p q : ℤ
hpq : p + q = n₀
linarith : (p + 1) * y < y + p * y → -1 + ((p + 1) * y + 1 - (y + p * y)) = 0
linarith₁ : y + p * y < (p + 1) * y → -1 + (y + p * y + 1 - (p + 1) * y) = 0
⊢ (p + 1) * y = y + p * y

Tactic:
linarith
-- 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 ℤ)
y : ℤ
inst_2 : K.HasTotal (up ℤ)
n₀ n₁ n₀' n₁' : ℤ
h₀ : n₀ + y = n₀'
h₁ : n₁ + y = n₁'
h : ¬(up ℤ).Rel n₀ n₁
neg : ¬(up ℤ).Rel n₀' n₁'
⊢ (Functor.obj (shiftFunctor₂ C y) K).D₁ (up ℤ) n₀ n₁ ≫ Iso.hom (K.totalShift₂XIso y n₁ n₁' h₁) =
    HSMul.hSMul (β :=
      ((Functor.obj (shiftFunctor₂ C y) K).total (up ℤ)).X n₀ ⟶
        GradedObject.mapObj.{0, 0, v_1, u_1} K.toGradedObject ((up ℤ).π (up ℤ) (up ℤ)) n₁')
      y.negOnePow (Iso.hom (K.totalShift₂XIso y 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 ℤ)
y : ℤ
inst_2 : K.HasTotal (up ℤ)
n₀ n₁ n₀' n₁' : ℤ
h₀ : n₀ + y = n₀'
h₁ : n₁ + y = 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 ℤ)
y : ℤ
inst_2 : K.HasTotal (up ℤ)
n₀ n₁ n₀' n₁' : ℤ
h₀ : n₀ + y = n₀'
h₁ : n₁ + y = n₁'
pos :
  ∀ (h : (up ℤ).Rel n₀ n₁),
    (Functor.obj (shiftFunctor₂ C y) K).D₂ (up ℤ) n₀ n₁ ≫ Iso.hom (K.totalShift₂XIso y n₁ n₁' h₁) =
      HSMul.hSMul (β :=
        ((Functor.obj (shiftFunctor₂ C y) K).total (up ℤ)).X n₀ ⟶
          GradedObject.mapObj.{0, 0, v_1, u_1} K.toGradedObject ((up ℤ).π (up ℤ) (up ℤ)) n₁')
        y.negOnePow (Iso.hom (K.totalShift₂XIso y n₀ n₀' h₀) ≫ K.D₂ (up ℤ) n₀' n₁')
neg :
  ∀ (h : ¬(up ℤ).Rel n₀ n₁),
    (Functor.obj (shiftFunctor₂ C y) K).D₂ (up ℤ) n₀ n₁ ≫ Iso.hom (K.totalShift₂XIso y n₁ n₁' h₁) =
      HSMul.hSMul (β :=
        ((Functor.obj (shiftFunctor₂ C y) K).total (up ℤ)).X n₀ ⟶
          GradedObject.mapObj.{0, 0, v_1, u_1} K.toGradedObject ((up ℤ).π (up ℤ) (up ℤ)) n₁')
        y.negOnePow (Iso.hom (K.totalShift₂XIso y n₀ n₀' h₀) ≫ K.D₂ (up ℤ) n₀' n₁')
⊢ (Functor.obj (shiftFunctor₂ C y) K).D₂ (up ℤ) n₀ n₁ ≫ Iso.hom (K.totalShift₂XIso y n₁ n₁' h₁) =
    HSMul.hSMul (β :=
      ((Functor.obj (shiftFunctor₂ C y) K).total (up ℤ)).X n₀ ⟶
        GradedObject.mapObj.{0, 0, v_1, u_1} K.toGradedObject ((up ℤ).π (up ℤ) (up ℤ)) n₁')
      y.negOnePow (Iso.hom (K.totalShift₂XIso y 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 ℤ)
y : ℤ
inst_2 : K.HasTotal (up ℤ)
n₀ n₁ n₀' n₁' : ℤ
h₀ : n₀ + y = n₀'
h₁ : n₁ + y = n₁'
h : (up ℤ).Rel n₀ n₁
pos :
  ∀ (i₁ i₂ : ℤ) (hi : (up ℤ).π (up ℤ) (up ℤ) (i₁, i₂) = n₀),
    CategoryStruct.comp (Y := ((Functor.obj (shiftFunctor₂ C y) K).total (up ℤ)).X n₀)
        ((Functor.obj (shiftFunctor₂ C y) K).ιTotal (up ℤ) i₁ i₂ n₀ hi)
        ((Functor.obj (shiftFunctor₂ C y) K).D₂ (up ℤ) n₀ n₁ ≫ Iso.hom (K.totalShift₂XIso y n₁ n₁' h₁)) =
      (Functor.obj (shiftFunctor₂ C y) K).ιTotal (up ℤ) i₁ i₂ n₀ hi ≫
        HSMul.hSMul (β :=
          ((Functor.obj (shiftFunctor₂ C y) K).total (up ℤ)).X n₀ ⟶
            GradedObject.mapObj.{0, 0, v_1, u_1} K.toGradedObject ((up ℤ).π (up ℤ) (up ℤ)) n₁')
          y.negOnePow (Iso.hom (K.totalShift₂XIso y n₀ n₀' h₀) ≫ K.D₂ (up ℤ) n₀' n₁')
⊢ (Functor.obj (shiftFunctor₂ C y) K).D₂ (up ℤ) n₀ n₁ ≫ Iso.hom (K.totalShift₂XIso y n₁ n₁' h₁) =
    HSMul.hSMul (β :=
      ((Functor.obj (shiftFunctor₂ C y) K).total (up ℤ)).X n₀ ⟶
        GradedObject.mapObj.{0, 0, v_1, u_1} K.toGradedObject ((up ℤ).π (up ℤ) (up ℤ)) n₁')
      y.negOnePow (Iso.hom (K.totalShift₂XIso y 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 ℤ)
y : ℤ
inst_2 : K.HasTotal (up ℤ)
n₀ n₁ n₀' n₁' : ℤ
h₀ : n₀ + y = n₀'
h₁ : n₁ + y = n₁'
h : n₀ + 1 = n₁
p q : ℤ
hpq : p + q = n₀
pos :
  CategoryStruct.comp (Y := ((Functor.obj (shiftFunctor₂ C y) K).total (up ℤ)).X n₀)
      ((Functor.obj (shiftFunctor₂ C y) K).ιTotal (up ℤ) p q n₀ hpq)
      ((Functor.obj (shiftFunctor₂ C y) K).D₂ (up ℤ) n₀ n₁ ≫
        (Functor.obj (shiftFunctor₂ C y) K).totalDesc fun (p q : ℤ) (hpq : p + q = n₁) ↦
          HSMul.hSMul (β := (K.X p).X (q + y) ⟶ (K.total (up ℤ)).X n₁') (p * y).negOnePow
            (K.ιTotal (up ℤ) p (q + y) n₁' ⋯)) =
    (Functor.obj (shiftFunctor₂ C y) K).ιTotal (up ℤ) p q n₀ hpq ≫
      HSMul.hSMul (β :=
        ((Functor.obj (shiftFunctor₂ C y) K).total (up ℤ)).X n₀ ⟶
          GradedObject.mapObj.{0, 0, v_1, u_1} K.toGradedObject ((up ℤ).π (up ℤ) (up ℤ)) n₁')
        y.negOnePow
        (((Functor.obj (shiftFunctor₂ C y) K).totalDesc fun (p q : ℤ) (hpq : p + q = n₀) ↦
            HSMul.hSMul (β := (K.X p).X (q + y) ⟶ (K.total (up ℤ)).X n₀') (p * y).negOnePow
              (K.ιTotal (up ℤ) p (q + y) n₀' ⋯)) ≫
          K.D₂ (up ℤ) n₀' n₁')
⊢ CategoryStruct.comp (Y := ((Functor.obj (shiftFunctor₂ C y) K).total (up ℤ)).X n₀)
      ((Functor.obj (shiftFunctor₂ C y) K).ιTotal (up ℤ) p q n₀ hpq)
      ((Functor.obj (shiftFunctor₂ C y) K).D₂ (up ℤ) n₀ n₁ ≫ Iso.hom (K.totalShift₂XIso y n₁ n₁' h₁)) =
    (Functor.obj (shiftFunctor₂ C y) K).ιTotal (up ℤ) p q n₀ hpq ≫
      HSMul.hSMul (β :=
        ((Functor.obj (shiftFunctor₂ C y) K).total (up ℤ)).X n₀ ⟶
          GradedObject.mapObj.{0, 0, v_1, u_1} K.toGradedObject ((up ℤ).π (up ℤ) (up ℤ)) n₁')
        y.negOnePow (Iso.hom (K.totalShift₂XIso y 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 ℤ)
y : ℤ
inst_2 : K.HasTotal (up ℤ)
n₀ n₁ n₀' n₁' : ℤ
h₀ : n₀ + y = n₀'
h₁ : n₁ + y = 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 ℤ)
y : ℤ
inst_2 : K.HasTotal (up ℤ)
n₀ n₁ n₀' n₁' : ℤ
h₀ : n₀ + y = n₀'
h₁ : n₁ + y = n₁'
h : n₀ + 1 = n₁
p q : ℤ
hpq : p + q = n₀
⊢ q + y + 1 = q + 1 + y

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 ℤ)
y : ℤ
inst_2 : K.HasTotal (up ℤ)
n₀ n₁ n₀' n₁' : ℤ
h₀ : n₀ + y = n₀'
h₁ : n₁ + y = n₁'
h : n₀ + 1 = n₁
p q : ℤ
hpq : p + q = n₀
⊢ p + (q + 1 + y) = 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 ℤ)
y : ℤ
inst_2 : K.HasTotal (up ℤ)
n₀ n₁ n₀' n₁' : ℤ
h₀ : n₀ + y = n₀'
h₁ : n₁ + y = n₁'
h : n₀ + 1 = n₁
p q : ℤ
hpq : p + q = n₀
pos :
  (up ℤ).ε₂ (up ℤ) (up ℤ) (p, q) •
      ((Functor.obj (shiftFunctor₂ C y) K).X p).d q (q + 1) ≫
        HSMul.hSMul (β := (K.X p).X (q + 1 + y) ⟶ (K.total (up ℤ)).X n₁') (p * y).negOnePow
          (K.ιTotal (up ℤ) p (q + 1 + y) n₁' ⋯) =
    HSMul.hSMul (β := (K.X p).X (q + y) ⟶ (K.total (up ℤ)).X n₁')
      (y.negOnePow * (p * y).negOnePow * (up ℤ).ε₂ (up ℤ) (up ℤ) (p, q + y))
      ((K.X p).d (q + y) (q + 1 + y) ≫ K.ιTotal (up ℤ) p (q + 1 + y) n₁' ⋯)
⊢ CategoryStruct.comp (Y := ((Functor.obj (shiftFunctor₂ C y) K).total (up ℤ)).X n₀)
      ((Functor.obj (shiftFunctor₂ C y) K).ιTotal (up ℤ) p q n₀ hpq)
      ((Functor.obj (shiftFunctor₂ C y) K).D₂ (up ℤ) n₀ n₁ ≫
        (Functor.obj (shiftFunctor₂ C y) K).totalDesc fun (p q : ℤ) (hpq : p + q = n₁) ↦
          HSMul.hSMul (β := (K.X p).X (q + y) ⟶ (K.total (up ℤ)).X n₁') (p * y).negOnePow
            (K.ιTotal (up ℤ) p (q + y) n₁' ⋯)) =
    (Functor.obj (shiftFunctor₂ C y) K).ιTotal (up ℤ) p q n₀ hpq ≫
      HSMul.hSMul (β :=
        ((Functor.obj (shiftFunctor₂ C y) K).total (up ℤ)).X n₀ ⟶
          GradedObject.mapObj.{0, 0, v_1, u_1} K.toGradedObject ((up ℤ).π (up ℤ) (up ℤ)) n₁')
        y.negOnePow
        (((Functor.obj (shiftFunctor₂ C y) K).totalDesc fun (p q : ℤ) (hpq : p + q = n₀) ↦
            HSMul.hSMul (β := (K.X p).X (q + y) ⟶ (K.total (up ℤ)).X n₀') (p * y).negOnePow
              (K.ιTotal (up ℤ) p (q + y) n₀' ⋯)) ≫
          K.D₂ (up ℤ) n₀' n₁')

Tactic:
rw [ι_D₂_assoc, Linear.comp_units_smul, ι_totalDesc_assoc, Linear.units_smul_comp,
      smul_smul, ι_D₂, ((shiftFunctor₂ C y).obj K).d₂_eq _ _ rfl _ (by dsimp; lia),
      K.d₂_eq _ _ (show q + y + 1 = q + 1 + y by lia) _ (by dsimp; lia),
      Linear.units_smul_comp, Category.assoc, smul_smul, ι_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₂.d₂_eq, HomologicalComplex₂.shiftFunctor₂, CategoryTheory.Functor.obj, rfl