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 : 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₀
⊢ (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₁' ⋯)
have pos : CategoryStruct.comp (Y :=
    GradedObject.mapObj.{0, 0, v_1, u_1} (Functor.obj (shiftFunctor₁ C x) K).toGradedObject ((up ℤ).π (up ℤ) (up ℤ)) n₁)
    (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₁ sorry :
      (K.X (p + x)).X q ⟶ ((Functor.obj (shiftFunctor₁ C x) K).total (up ℤ)).X n₁)
    ((Functor.obj (shiftFunctor₁ C x) K).totalDesc fun (p q : ℤ) (hpq : p + q = n₁) ↦ K.ιTotal (up ℤ) (p + x) q n₁' sorry) =
  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₁' sorry)
Tactic: rw [one_smul, Category.assoc, ι_totalDesc, one_smul, Linear.units_smul_comp]
-- 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 ℤ)
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 :=
      GradedObject.mapObj.{0, 0, v_1, u_1} (Functor.obj (shiftFunctor₁ C x) K).toGradedObject ((up ℤ).π (up ℤ) (up ℤ))
        n₁)
      (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₁ ⋯ :
        (K.X (p + x)).X q ⟶ ((Functor.obj (shiftFunctor₁ C x) K).total (up ℤ)).X 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 (α := ℤˣ) (β := (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₁' ⋯)
have pos₁ : 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) ≫
    CategoryStruct.comp (Y :=
      GradedObject.mapObj.{0, 0, v_1, u_1} (Functor.obj (shiftFunctor₁ C x) K).toGradedObject ((up ℤ).π (up ℤ) (up ℤ))
        n₁)
      ((Functor.obj (shiftFunctor₁ C x) K).ιTotal (up ℤ) (p + 1) q n₁ sorry :
        ((Functor.obj (shiftFunctor₁ C x) K).X (p + 1)).X q ⟶ ((Functor.obj (shiftFunctor₁ C x) K).total (up ℤ)).X n₁)
      ((Functor.obj (shiftFunctor₁ C x) K).totalDesc fun (p q : ℤ) (hpq : p + q = n₁) ↦
        K.ιTotal (up ℤ) (p + x) q n₁' sorry) =
  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₁' sorry)
Tactic: rw [one_smul, Category.assoc, ι_totalDesc, one_smul, Linear.units_smul_comp]
-- 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 ℤ)
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 :=
      GradedObject.mapObj.{0, 0, v_1, u_1} (Functor.obj (shiftFunctor₁ C x) K).toGradedObject ((up ℤ).π (up ℤ) (up ℤ))
        n₁)
      (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₁ ⋯ :
        (K.X (p + x)).X q ⟶ ((Functor.obj (shiftFunctor₁ C x) K).total (up ℤ)).X 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₁' ⋯)
pos₁ :
  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) ≫
      CategoryStruct.comp (Y :=
        GradedObject.mapObj.{0, 0, v_1, u_1} (Functor.obj (shiftFunctor₁ C x) K).toGradedObject ((up ℤ).π (up ℤ) (up ℤ))
          n₁)
        ((Functor.obj (shiftFunctor₁ C x) K).ιTotal (up ℤ) (p + 1) q n₁ ⋯ :
          ((Functor.obj (shiftFunctor₁ C x) K).X (p + 1)).X q ⟶ ((Functor.obj (shiftFunctor₁ C x) K).total (up ℤ)).X 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 (α := ℤˣ) (β := (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₁' ⋯)
have pos₂ : 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) ≫
    K.ιTotal (up ℤ) (p + 1 + x) q n₁' sorry =
  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₁' sorry)
Tactic: rw [one_smul, Category.assoc, ι_totalDesc, one_smul, Linear.units_smul_comp]
-- 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 ℤ)
x : ℤ
inst_2 : K.HasTotal (up ℤ)
n₀ n₁ n₀' n₁' : ℤ
h₀ : n₀ + x = n₀'
h₁ : n₁ + x = n₁'
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₁')
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 ℤ)
x : ℤ
inst_2 : K.HasTotal (up ℤ)
n₀ n₁ n₀' n₁' : ℤ
h₀ : n₀ + x = n₀'
h₁ : n₁ + x = 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₁')
have 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₁')
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 ℤ)
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₁')
⊢ (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₁')
have 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₁')
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 ℤ)
x : ℤ
inst_2 : K.HasTotal (up ℤ)
n₀ n₁ n₀' n₁' : ℤ
h₀ : n₀ + x = n₀'
h₁ : n₁ + x = n₁'
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₁')
have 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₁')
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 ℤ)
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₀
⊢ 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₁')
have 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₁' sorry) =
  (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₀' 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 ℤ)
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₀
⊢ 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₁')
have 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₁' sorry) =
  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₁' sorry)
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]
-- 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 ℤ)
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₀
⊢ 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₁' ⋯)
have 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₁' sorry) =
  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₁' 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 ℤ)
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₀
⊢ 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₁' ⋯)
have pos : p.negOnePow = x.negOnePow * (p + x).negOnePow
Tactic: congr 1
-- 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 ℤ)
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.negOnePow = x.negOnePow * (p + x).negOnePow
have pos : p.negOnePow = x.negOnePow * (x + p).negOnePow
Tactic: rw [add_comm p, Int.negOnePow_add, ← mul_assoc, Int.units_mul_self, one_mul]
-- 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 ℤ)
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
⊢ p.negOnePow = x.negOnePow * (p + x).negOnePow
have pos₁ : p.negOnePow = x.negOnePow * (x.negOnePow * p.negOnePow)
Tactic: rw [add_comm p, Int.negOnePow_add, ← mul_assoc, Int.units_mul_self, one_mul]
-- 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 ℤ)
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)
⊢ p.negOnePow = x.negOnePow * (p + x).negOnePow
have pos₂ : p.negOnePow = x.negOnePow * x.negOnePow * p.negOnePow
Tactic: rw [add_comm p, Int.negOnePow_add, ← mul_assoc, Int.units_mul_self, one_mul]
-- 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 ℤ)
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
⊢ p.negOnePow = x.negOnePow * (p + x).negOnePow
have pos₃ : p.negOnePow = 1 * p.negOnePow
Tactic: rw [add_comm p, Int.negOnePow_add, ← mul_assoc, Int.units_mul_self, one_mul]
-- 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 ℤ)
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
⊢ p.negOnePow = x.negOnePow * (p + x).negOnePow
have pos₄ : p.negOnePow = p.negOnePow
Tactic: rw [add_comm p, Int.negOnePow_add, ← mul_assoc, Int.units_mul_self, one_mul]
-- 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 ℤ)
x : ℤ
inst_2 : K.HasTotal (up ℤ)
n₀ n₁ n₀' n₁' : ℤ
h₀ : n₀ + x = n₀'
h₁ : n₁ + x = n₁'
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₁')
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 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
        ((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')
have dsimp : Iso.hom (K.totalShift₁XIso x n (n + x) sorry) ≫
    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) 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 ℤ)
x : ℤ
inst_2 : K.HasTotal (up ℤ)
a b n : ℤ
h : a + b = n
a' : ℤ
ha' : a' = a + x
n' : ℤ
hn' : n' = 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' ha' b).hom ≫
      K.ιTotal (up ℤ) a' b n' ⋯ ≫ (CochainComplex.shiftFunctorObjXIso (K.total (up ℤ)) x n n' hn').inv
have 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) sorry b).hom ≫
    K.ιTotal (up ℤ) (a + x) b (n + x) sorry ≫ (CochainComplex.shiftFunctorObjXIso (K.total (up ℤ)) x n (n + x) sorry).inv
Tactic: subst ha' hn'
Cleared hypotheses: a', ha', n', hn'