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 a b : ℤ
h : (a, b) ∈ (up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n}
⊢ (↑((fun (x_1 : (↑((up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n + x}) : Type)) ↦
              (match (motive :=
                  (↑((up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n + x}) : Type) → (↑((up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n}) : Type)) x_1 with
                | ⟨(a, b), h⟩ => Subtype.mk (p := fun (x : ℤ × ℤ) ↦ x ∈ (up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n}) (a - x, b) ⋯ :
                (↑((up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n}) : Type)))
            ((fun (x_1 : (↑((up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n}) : Type)) ↦
                (match (motive :=
                    (↑((up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n}) : Type) → (↑((up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n + x}) : Type))
                    x_1 with
                  | ⟨(a, b), h⟩ =>
                    Subtype.mk (p := fun (x_2 : ℤ × ℤ) ↦ x_2 ∈ (up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n + x}) (a + x, b) ⋯ :
                  (↑((up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n + x}) : Type)))
              (Subtype.mk (p := fun (x : ℤ × ℤ) ↦ x ∈ (up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n}) (a, b) h))) :
        ℤ × ℤ).1 =
    (↑(Subtype.mk (p := fun (x : ℤ × ℤ) ↦ x ∈ (up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n}) (a, b) h) : ℤ × ℤ).1
have a₁ : a + x - x = a
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 L : HomologicalComplex₂.{v_1, u_1, 0, 0} C (up ℤ) (up ℤ)
f : K ⟶ L
x y : ℤ
inst_2 : K.HasTotal (up ℤ)
n a b : ℤ
h : (a, b) ∈ (up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n + x}
⊢ (fun (x_1 : (↑((up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n}) : Type)) ↦
        (match (motive := (↑((up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n}) : Type) → (↑((up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n + x}) : Type))
            x_1 with
          | ⟨(a, b), h⟩ => Subtype.mk (p := fun (x_2 : ℤ × ℤ) ↦ x_2 ∈ (up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n + x}) (a + x, b) ⋯ :
          (↑((up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n + x}) : Type)))
      ((fun (x_1 : (↑((up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n + x}) : Type)) ↦
          (match (motive := (↑((up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n + x}) : Type) → (↑((up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n}) : Type))
              x_1 with
            | ⟨(a, b), h⟩ => Subtype.mk (p := fun (x : ℤ × ℤ) ↦ x ∈ (up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n}) (a - x, b) ⋯ :
            (↑((up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n}) : Type)))
        (Subtype.mk (p := fun (x_1 : ℤ × ℤ) ↦ x_1 ∈ (up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n + x}) (a, b) h)) =
    Subtype.mk (p := fun (x_1 : ℤ × ℤ) ↦ x_1 ∈ (up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n + x}) (a, b) h
have a₁ : (↑((fun (x_1 : (↑((up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n}) : Type)) ↦
            (match (motive :=
                (↑((up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n}) : Type) → (↑((up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n + x}) : Type)) x_1 with
              | ⟨(a, b), h⟩ =>
                Subtype.mk (p := fun (x_2 : ℤ × ℤ) ↦ x_2 ∈ (up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n + x}) (a + x, b) sorry :
              (↑((up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n + x}) : Type)))
          ((fun (x_1 : (↑((up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n + x}) : Type)) ↦
              (match (motive :=
                  (↑((up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n + x}) : Type) → (↑((up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n}) : Type)) x_1 with
                | ⟨(a, b), h⟩ => Subtype.mk (p := fun (x : ℤ × ℤ) ↦ x ∈ (up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n}) (a - x, b) sorry :
                (↑((up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n}) : Type)))
            (Subtype.mk (p := fun (x_1 : ℤ × ℤ) ↦ x_1 ∈ (up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n + x}) (a, b) h))) :
      ℤ × ℤ).1 =
  (↑(Subtype.mk (p := fun (x_1 : ℤ × ℤ) ↦ x_1 ∈ (up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n + x}) (a, b) h) : ℤ × ℤ).1
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 a b : ℤ
h : (a, b) ∈ (up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n + x}
⊢ (↑((fun (x_1 : (↑((up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n}) : Type)) ↦
              (match (motive :=
                  (↑((up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n}) : Type) → (↑((up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n + x}) : Type)) x_1 with
                | ⟨(a, b), h⟩ =>
                  Subtype.mk (p := fun (x_2 : ℤ × ℤ) ↦ x_2 ∈ (up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n + x}) (a + x, b) ⋯ :
                (↑((up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n + x}) : Type)))
            ((fun (x_1 : (↑((up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n + x}) : Type)) ↦
                (match (motive :=
                    (↑((up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n + x}) : Type) → (↑((up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n}) : Type))
                    x_1 with
                  | ⟨(a, b), h⟩ => Subtype.mk (p := fun (x : ℤ × ℤ) ↦ x ∈ (up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n}) (a - x, b) ⋯ :
                  (↑((up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n}) : Type)))
              (Subtype.mk (p := fun (x_1 : ℤ × ℤ) ↦ x_1 ∈ (up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n + x}) (a, b) h))) :
        ℤ × ℤ).1 =
    (↑(Subtype.mk (p := fun (x_1 : ℤ × ℤ) ↦ x_1 ∈ (up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n + x}) (a, b) h) : ℤ × ℤ).1
have a₁ : a - x + x = a
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.TotalComplexShift (hypothesis)
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 : ℤ
x_1 : (↑((up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n}) : Type)
a b : ℤ
h : (a, b) ∈ (up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n}
⊢ (a, b + y) ∈ (up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n + y}
have h₁ : a + b = n
Tactic: simp only [Set.mem_preimage, π_def, Set.mem_singleton_iff] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Homology.TotalComplexShift (hypothesis)
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 : ℤ
x_1 : (↑((up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n + y}) : Type)
a b : ℤ
h : (a, b) ∈ (up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n + y}
⊢ (a, b - y) ∈ (up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n}
have h₁ : a + b = n + y
Tactic: simp only [Set.mem_preimage, π_def, Set.mem_singleton_iff] at h ⊢
Cleared hypotheses: h
-- 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 ℤ)
⊢ (Functor.obj (shiftFunctor₂ C y ⋙ shiftFunctor₁ C x) K).HasTotal (up ℤ)
have dsimp : (Functor.obj (shiftFunctor₁ C x) (Functor.obj (shiftFunctor₂ C y) K)).HasTotal (up ℤ)
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 L : HomologicalComplex₂.{v_1, u_1, 0, 0} C (up ℤ) (up ℤ)
f : K ⟶ L
x y : ℤ
inst_2 : K.HasTotal (up ℤ)
⊢ (Functor.obj (shiftFunctor₁ C x ⋙ shiftFunctor₂ C y) K).HasTotal (up ℤ)
have dsimp : (Functor.obj (shiftFunctor₂ C y) (Functor.obj (shiftFunctor₁ C x) K)).HasTotal (up ℤ)
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 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 + x = n'
⊢ CategoryStruct.comp (Y := (K.total (up ℤ)).X n')
      ((Functor.obj (shiftFunctor₁ C x) K).totalDesc fun (p q : ℤ) (hpq : (up ℤ).π (up ℤ) (up ℤ) (p, q) = n) ↦
        K.ιTotal (up ℤ) (p + x) q n' ⋯)
      (K.totalDesc fun (p q : ℤ) (hpq : (up ℤ).π (up ℤ) (up ℤ) (p, q) = n') ↦
        Iso.inv (XXIsoOfEq C (up ℤ) (up ℤ) K ⋯ ⋯) ≫ (Functor.obj (shiftFunctor₁ C x) K).ιTotal (up ℤ) (p - x) q n ⋯) =
    𝟙 (((Functor.obj (shiftFunctor₁ C x) K).total (up ℤ)).X n)
have h₁ : ∀ (p q : ℤ) (h_1 : (up ℤ).π (up ℤ) (up ℤ) (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 h_1)
      (CategoryStruct.comp (Y := (K.total (up ℤ)).X n')
        ((Functor.obj (shiftFunctor₁ C x) K).totalDesc fun (p q : ℤ) (hpq : (up ℤ).π (up ℤ) (up ℤ) (p, q) = n) ↦
          K.ιTotal (up ℤ) (p + x) q n' sorry)
        (K.totalDesc fun (p q : ℤ) (hpq : (up ℤ).π (up ℤ) (up ℤ) (p, q) = n') ↦
          Iso.inv (XXIsoOfEq C (up ℤ) (up ℤ) K sorry sorry) ≫
            (Functor.obj (shiftFunctor₁ C x) K).ιTotal (up ℤ) (p - x) q n sorry)) =
    (Functor.obj (shiftFunctor₁ C x) K).ιTotal (up ℤ) p q n h_1 ≫
      𝟙 (((Functor.obj (shiftFunctor₁ C x) K).total (up ℤ)).X n)
Tactic: ext p q h
-- 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 + x = n'
p q : ℤ
h : (up ℤ).π (up ℤ) (up ℤ) (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 h)
      (CategoryStruct.comp (Y := (K.total (up ℤ)).X n')
        ((Functor.obj (shiftFunctor₁ C x) K).totalDesc fun (p q : ℤ) (hpq : (up ℤ).π (up ℤ) (up ℤ) (p, q) = n) ↦
          K.ιTotal (up ℤ) (p + x) q n' ⋯)
        (K.totalDesc fun (p q : ℤ) (hpq : (up ℤ).π (up ℤ) (up ℤ) (p, q) = n') ↦
          Iso.inv (XXIsoOfEq C (up ℤ) (up ℤ) K ⋯ ⋯) ≫
            (Functor.obj (shiftFunctor₁ C x) K).ιTotal (up ℤ) (p - x) q n ⋯)) =
    (Functor.obj (shiftFunctor₁ C x) K).ιTotal (up ℤ) p q n h ≫
      𝟙 (((Functor.obj (shiftFunctor₁ C x) K).total (up ℤ)).X n)
have h₁ : CategoryStruct.comp (Y := ((Functor.obj (shiftFunctor₁ C x) K).total (up ℤ)).X n)
    ((Functor.obj (shiftFunctor₁ C x) K).ιTotal (up ℤ) p q n h)
    (CategoryStruct.comp (Y := (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)
      (K.totalDesc fun (p q : ℤ) (hpq : p + q = n') ↦
        Iso.inv (XXIsoOfEq C (up ℤ) (up ℤ) K sorry sorry) ≫ (Functor.obj (shiftFunctor₁ C x) K).ιTotal (up ℤ) (p - x) q n sorry)) =
  (Functor.obj (shiftFunctor₁ C x) K).ιTotal (up ℤ) p q n h ≫ 𝟙 (((Functor.obj (shiftFunctor₁ C x) 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 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 + x = n'
p q : ℤ
h : (up ℤ).π (up ℤ) (up ℤ) (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 h)
      (CategoryStruct.comp (Y := (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' ⋯)
        (K.totalDesc fun (p q : ℤ) (hpq : p + q = n') ↦
          Iso.inv (XXIsoOfEq C (up ℤ) (up ℤ) K ⋯ ⋯) ≫
            (Functor.obj (shiftFunctor₁ C x) K).ιTotal (up ℤ) (p - x) q n ⋯)) =
    (Functor.obj (shiftFunctor₁ C x) K).ιTotal (up ℤ) p q n h ≫
      𝟙 (((Functor.obj (shiftFunctor₁ C x) K).total (up ℤ)).X n)
have h₁ : Eq (α := (K.X (p + x)).X q ⟶ ((Functor.obj (shiftFunctor₁ C x) K).total (up ℤ)).X n)
  (Iso.inv (XXIsoOfEq C (up ℤ) (up ℤ) K sorry sorry) ≫ (Functor.obj (shiftFunctor₁ C x) K).ιTotal (up ℤ) (p + x - x) q n sorry)
  ((Functor.obj (shiftFunctor₁ C x) K).ιTotal (up ℤ) p q n h)
Tactic: simp only [ι_totalDesc_assoc, CochainComplex.shiftFunctor_obj_X', ι_totalDesc, 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 + x = n'
⊢ CategoryStruct.comp (Y := ((Functor.obj (shiftFunctor₁ C x) K).total (up ℤ)).X n)
      (K.totalDesc fun (p q : ℤ) (hpq : (up ℤ).π (up ℤ) (up ℤ) (p, q) = n') ↦
        Iso.inv (XXIsoOfEq C (up ℤ) (up ℤ) K ⋯ ⋯) ≫ (Functor.obj (shiftFunctor₁ C x) K).ιTotal (up ℤ) (p - x) q n ⋯)
      ((Functor.obj (shiftFunctor₁ C x) K).totalDesc fun (p q : ℤ) (hpq : (up ℤ).π (up ℤ) (up ℤ) (p, q) = n) ↦
        K.ιTotal (up ℤ) (p + x) q 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 x) K).total (up ℤ)).X n)
        (K.totalDesc fun (p q : ℤ) (hpq : (up ℤ).π (up ℤ) (up ℤ) (p, q) = n') ↦
          Iso.inv (XXIsoOfEq C (up ℤ) (up ℤ) K sorry sorry) ≫ (Functor.obj (shiftFunctor₁ C x) K).ιTotal (up ℤ) (p - x) q n sorry)
        ((Functor.obj (shiftFunctor₁ C x) K).totalDesc fun (p q : ℤ) (hpq : (up ℤ).π (up ℤ) (up ℤ) (p, q) = n) ↦
          K.ιTotal (up ℤ) (p + x) q 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 + x = 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 x) K).total (up ℤ)).X n)
        (K.totalDesc fun (p q : ℤ) (hpq : (up ℤ).π (up ℤ) (up ℤ) (p, q) = n') ↦
          Iso.inv (XXIsoOfEq C (up ℤ) (up ℤ) K ⋯ ⋯) ≫ (Functor.obj (shiftFunctor₁ C x) K).ιTotal (up ℤ) (p - x) q n ⋯)
        ((Functor.obj (shiftFunctor₁ C x) K).totalDesc fun (p q : ℤ) (hpq : (up ℤ).π (up ℤ) (up ℤ) (p, q) = n) ↦
          K.ιTotal (up ℤ) (p + x) q 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 x) K).total (up ℤ)).X n)
      (K.totalDesc fun (p q : ℤ) (hpq : p + q = n') ↦
        Iso.inv (XXIsoOfEq C (up ℤ) (up ℤ) K sorry sorry) ≫ (Functor.obj (shiftFunctor₁ C x) K).ιTotal (up ℤ) (p - x) q n sorry)
      ((Functor.obj (shiftFunctor₁ C x) K).totalDesc fun (p q : ℤ) (hpq : p + q = n) ↦
        K.ιTotal (up ℤ) (p + x) q 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 ℤ)
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 ⟶ ((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₁ sorry) ≫
    (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₁') ((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₁' 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 _ (show p + x + 1 = p + 1 + x by lia) _ _ (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 ℤ)
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 ⟶ ((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₁' ⋯)
have 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₁ sorry) ≫
    (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: dsimp