awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.TotalComplexShift (goal)
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_1 : n + y = n'
p q : ℤ
h : (up ℤ).π (up ℤ) (up ℤ) (p, q) = 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 h)
      (CategoryStruct.comp (Y := (K.total (up ℤ)).X 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.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).ιTotal (up ℤ) p q n h ≫
      𝟙 (((Functor.obj (shiftFunctor₂ C y) K).total (up ℤ)).X n)
have h₁ : Eq (α := (K.X p).X (q + y) ⟶ ((Functor.obj (shiftFunctor₂ C y) K).total (up ℤ)).X n)
  (Iso.inv (XXIsoOfEq C (up ℤ) (up ℤ) K sorry sorry) ≫ (Functor.obj (shiftFunctor₂ C y) K).ιTotal (up ℤ) p (q + y - y) n sorry)
  ((Functor.obj (shiftFunctor₂ C y) K).ιTotal (up ℤ) p q n h)
Tactic: simp only [ι_totalDesc_assoc, Linear.units_smul_comp, ι_totalDesc, smul_smul,
      Int.units_mul_self, one_smul, comp_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.TotalComplexShift (goal)
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'
⊢ CategoryStruct.comp (Y := ((Functor.obj (shiftFunctor₂ C y) K).total (up ℤ)).X n)
      (K.totalDesc fun (p q : ℤ) (hpq : (up ℤ).π (up ℤ) (up ℤ) (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 : (up ℤ).π (up ℤ) (up ℤ) (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 ℤ)).X n')
have h₁ : ∀ (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 : (up ℤ).π (up ℤ) (up ℤ) (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 sorry sorry) ≫
              (Functor.obj (shiftFunctor₂ C y) K).ιTotal (up ℤ) p (q - y) n sorry))
        ((Functor.obj (shiftFunctor₂ C y) K).totalDesc fun (p q : ℤ) (hpq : (up ℤ).π (up ℤ) (up ℤ) (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' sorry))) =
    K.ιTotal (up ℤ) i₁ i₂ n' hi ≫ 𝟙 ((K.total (up ℤ)).X n')
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Homology.TotalComplexShift (goal)
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 : (up ℤ).π (up ℤ) (up ℤ) (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 : (up ℤ).π (up ℤ) (up ℤ) (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')
have h₁ : 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 sorry sorry) ≫ (Functor.obj (shiftFunctor₂ C y) K).ιTotal (up ℤ) p (q - y) n sorry))
      ((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' sorry))) =
  K.ιTotal (up ℤ) i₁ i₂ n' hi ≫ 𝟙 ((K.total (up ℤ)).X n')
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.TotalComplexShift (goal)
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₁'
⊢ (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₁')
have 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₁')
Tactic: by_cases h : (up ℤ).Rel n₀ n₁
-- Lean 4 proof step from Mathlib.Algebra.Homology.TotalComplexShift (goal)
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₁')
⊢ (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₁')
have 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₁')
Tactic: by_cases h : (up ℤ).Rel n₀ n₁
-- Lean 4 proof step from Mathlib.Algebra.Homology.TotalComplexShift (goal)
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₁
⊢ (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₁')
have 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₁')
Tactic: apply total.hom_ext
-- Lean 4 proof step from Mathlib.Algebra.Homology.TotalComplexShift (goal)
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₀
⊢ 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₁')
have 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₁' sorry)) =
  (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₀' sorry)) ≫
        K.D₁ (up ℤ) n₀' n₁')
Tactic: dsimp [totalShift₂XIso]
-- Lean 4 proof step from Mathlib.Algebra.Homology.TotalComplexShift (goal)
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₀
⊢ 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₁')
have 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₁ sorry) ≫
    (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₁' sorry)) =
  (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₁' sorry)
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)]
-- Lean 4 proof step from Mathlib.Algebra.Homology.TotalComplexShift (goal)
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₀
⊢ (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₁' ⋯)
have 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₁ sorry) ≫
    (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₁' sorry)) =
  (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₁' sorry)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.TotalComplexShift (goal)
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₀
⊢ (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₁' ⋯)
have 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₁' sorry) =
  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₁' sorry)
Tactic: rw [one_smul, one_smul, Category.assoc, ι_totalDesc, Linear.comp_units_smul,
      ← Int.negOnePow_add]
-- Lean 4 proof step from Mathlib.Algebra.Homology.TotalComplexShift (goal)
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₀
⊢ 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₁' ⋯)
have pos : (p + 1) * y = y + p * y
Tactic: congr 2
-- Lean 4 proof step from Mathlib.Algebra.Homology.TotalComplexShift (goal)
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) * y = y + p * y
have linarith : (p + 1) * y < y + p * y → -1 + ((p + 1) * y + 1 - (y + p * y)) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Algebra.Homology.TotalComplexShift (goal)
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
⊢ (p + 1) * y = y + p * y
have linarith₁ : y + p * y < (p + 1) * y → -1 + (y + p * y + 1 - (p + 1) * y) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Algebra.Homology.TotalComplexShift (goal)
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₁
⊢ (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₁')
have neg : ¬(up ℤ).Rel n₀' n₁'
Tactic: rw [D₁_shape _ _ _ _ h, zero_comp, D₁_shape, comp_zero, smul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.TotalComplexShift (goal)
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₁'
⊢ (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₁')
have 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₁')
Tactic: by_cases h : (up ℤ).Rel n₀ n₁
-- Lean 4 proof step from Mathlib.Algebra.Homology.TotalComplexShift (goal)
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₁')
⊢ (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₁')
have 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₁')
Tactic: by_cases h : (up ℤ).Rel n₀ n₁
-- Lean 4 proof step from Mathlib.Algebra.Homology.TotalComplexShift (goal)
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₁
⊢ (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₁')
have 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₁')
Tactic: apply total.hom_ext