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 a b : ℤ
h : (a, b) ∈ (up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n + x}
a₁ : a - x + x = 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) ⋯ :
                (↑((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

Tactic:
dsimp
-- Module: Mathlib.Algebra.Homology.TotalComplexShift
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K L : HomologicalComplex₂.{v_1, u_1, 0, 0} C (up ℤ) (up ℤ)
f : K ⟶ L
x y : ℤ
inst_2 : K.HasTotal (up ℤ)
n a b : ℤ
h : (a, b) ∈ (up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n + x}
⊢ a - x + x = a

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 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))) :
        ℤ × ℤ).2 =
    (↑(Subtype.mk (p := fun (x_1 : ℤ × ℤ) ↦ x_1 ∈ (up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n + x}) (a, b) h) : ℤ × ℤ).2

Tactic:
rfl
-- Module: Mathlib.Algebra.Homology.TotalComplexShift
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K L : HomologicalComplex₂.{v_1, u_1, 0, 0} C (up ℤ) (up ℤ)
f : K ⟶ L
x y : ℤ
inst_2 : K.HasTotal (up ℤ)
n : ℤ
x_1 : (↑((up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n}) : Type)
a b : ℤ
h : a + b = n
⊢ a + (b + y) = n + 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 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 = n + y

Tactic:
simp only [Set.mem_preimage, π_def, Set.mem_singleton_iff] at h ⊢

Premises used: Set.mem_singleton_iff, ComplexShape.π_def, Set.mem_preimage
-- 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 : ℤ
x_1 : (↑((up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n + y}) : Type)
a b : ℤ
h : a + b = n + y
⊢ a + (b - 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 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)
⊢ (fun (x : (↑((up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n + y}) : Type)) ↦
        (match (motive := (↑((up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n + y}) : Type) → (↑((up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n}) : Type))
            x with
          | ⟨(a, b), h⟩ => Subtype.mk (p := fun (x : ℤ × ℤ) ↦ x ∈ (up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n}) (a, b - y) ⋯ :
          (↑((up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n}) : Type)))
      ((fun (x : (↑((up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n}) : Type)) ↦
          (match (motive := (↑((up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n}) : Type) → (↑((up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n + y}) : Type))
              x with
            | ⟨(a, b), h⟩ => Subtype.mk (p := fun (x : ℤ × ℤ) ↦ x ∈ (up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n + y}) (a, b + y) ⋯ :
            (↑((up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n + y}) : Type)))
        x_1) =
    x_1

Tactic:
simp
-- 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 : ℤ
x_1 : (↑((up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n + y}) : Type)
⊢ (fun (x : (↑((up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n}) : Type)) ↦
        (match (motive := (↑((up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n}) : Type) → (↑((up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n + y}) : Type))
            x with
          | ⟨(a, b), h⟩ => Subtype.mk (p := fun (x : ℤ × ℤ) ↦ x ∈ (up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n + y}) (a, b + y) ⋯ :
          (↑((up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n + y}) : Type)))
      ((fun (x : (↑((up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n + y}) : Type)) ↦
          (match (motive := (↑((up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n + y}) : Type) → (↑((up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n}) : Type))
              x with
            | ⟨(a, b), h⟩ => Subtype.mk (p := fun (x : ℤ × ℤ) ↦ x ∈ (up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n}) (a, b - y) ⋯ :
            (↑((up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n}) : Type)))
        x_1) =
    x_1

Tactic:
simp
-- 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 ℤ)
dsimp : (Functor.obj (shiftFunctor₁ C x) (Functor.obj (shiftFunctor₂ C y) K)).HasTotal (up ℤ)
⊢ (Functor.obj (shiftFunctor₂ C y ⋙ shiftFunctor₁ C x) K).HasTotal (up ℤ)

Tactic:
dsimp
-- Module: Mathlib.Algebra.Homology.TotalComplexShift
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K L : HomologicalComplex₂.{v_1, u_1, 0, 0} C (up ℤ) (up ℤ)
f : K ⟶ L
x y : ℤ
inst_2 : K.HasTotal (up ℤ)
⊢ (Functor.obj (shiftFunctor₁ C x) (Functor.obj (shiftFunctor₂ C y) K)).HasTotal (up ℤ)

Tactic:
infer_instance
-- 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 ℤ)
dsimp : (Functor.obj (shiftFunctor₂ C y) (Functor.obj (shiftFunctor₁ C x) K)).HasTotal (up ℤ)
⊢ (Functor.obj (shiftFunctor₁ C x ⋙ shiftFunctor₂ C y) K).HasTotal (up ℤ)

Tactic:
dsimp
-- Module: Mathlib.Algebra.Homology.TotalComplexShift
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K L : HomologicalComplex₂.{v_1, u_1, 0, 0} C (up ℤ) (up ℤ)
f : K ⟶ L
x y : ℤ
inst_2 : K.HasTotal (up ℤ)
⊢ (Functor.obj (shiftFunctor₂ C y) (Functor.obj (shiftFunctor₁ C x) K)).HasTotal (up ℤ)

Tactic:
infer_instance
-- 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 + x = n'
p q : ℤ
hpq : p + q = n
⊢ p + x + 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 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'
p q : ℤ
hpq : p + q = n'
⊢ p - x + 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 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'
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' ⋯)
          (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_1 ≫
        𝟙 (((Functor.obj (shiftFunctor₁ C x) K).total (up ℤ)).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)

Tactic:
ext p q h
-- 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_1 : n + x = n'
p q : ℤ
h : (up ℤ).π (up ℤ) (up ℤ) (p, q) = n
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' ⋯)
        (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)
⊢ 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)

Tactic:
dsimp
-- Module: Mathlib.Algebra.Homology.TotalComplexShift
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K L : HomologicalComplex₂.{v_1, u_1, 0, 0} C (up ℤ) (up ℤ)
f : K ⟶ L
x y : ℤ
inst_2 : K.HasTotal (up ℤ)
n n' : ℤ
h_1 : n + x = n'
p q : ℤ
h : (up ℤ).π (up ℤ) (up ℤ) (p, q) = n
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 ⋯ ⋯) ≫ (Functor.obj (shiftFunctor₁ C x) K).ιTotal (up ℤ) (p + x - x) q n ⋯)
    ((Functor.obj (shiftFunctor₁ C x) K).ιTotal (up ℤ) p q n 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' ⋯)
        (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)

Tactic:
simp only [ι_totalDesc_assoc, CochainComplex.shiftFunctor_obj_X', ι_totalDesc, comp_id]

Premises used: HomologicalComplex₂.ι_totalDesc_assoc, HomologicalComplex₂.ι_totalDesc, CategoryTheory.Category.comp_id, CochainComplex.shiftFunctor_obj_X'
-- 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_1 : n + x = n'
p q : ℤ
h : (up ℤ).π (up ℤ) (up ℤ) (p, q) = n
⊢ p + x - x = p

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 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
⊢ Eq (α := (K.X (p + x)).X q ⟶ ((Functor.obj (shiftFunctor₁ C x) K).total (up ℤ)).X n)
    (Iso.inv (XXIsoOfEq C (up ℤ) (up ℤ) K ⋯ ⋯) ≫ (Functor.obj (shiftFunctor₁ C x) K).ιTotal (up ℤ) (p + x - x) q n ⋯)
    ((Functor.obj (shiftFunctor₁ C x) K).ιTotal (up ℤ) p q n h)

Tactic:
exact ((shiftFunctor₁ C x).obj K).XXIsoOfEq_inv_ιTotal _ (by lia) rfl _ _

Premises used: HomologicalComplex₂.shiftFunctor₁, HomologicalComplex₂.XXIsoOfEq_inv_ιTotal, 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 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'
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 ⋯ ⋯) ≫ (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')
⊢ 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')

Tactic:
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 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'
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 ⋯ ⋯) ≫ (Functor.obj (shiftFunctor₁ C x) K).ιTotal (up ℤ) (p - x) q n ⋯)
        ((Functor.obj (shiftFunctor₁ C x) K).totalDesc fun (p q : ℤ) (hpq : p + q = n) ↦
          K.ιTotal (up ℤ) (p + x) q n' ⋯)) =
    K.ιTotal (up ℤ) i₁ i₂ n' hi ≫ 𝟙 ((K.total (up ℤ)).X 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')

Tactic:
dsimp
-- Module: Mathlib.Algebra.Homology.TotalComplexShift
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K L : HomologicalComplex₂.{v_1, u_1, 0, 0} C (up ℤ) (up ℤ)
f : K ⟶ L
x y : ℤ
inst_2 : K.HasTotal (up ℤ)
n n' : ℤ
h : 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 : 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 : p + q = n) ↦
          K.ιTotal (up ℤ) (p + x) q n' ⋯)) =
    K.ιTotal (up ℤ) i₁ i₂ n' hi ≫ 𝟙 ((K.total (up ℤ)).X n')

Tactic:
simp only [ι_totalDesc_assoc, Category.assoc, ι_totalDesc, XXIsoOfEq_inv_ιTotal, comp_id]

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

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

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

Tactic:
apply total.hom_ext

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

Tactic:
dsimp [totalShift₁XIso]

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

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

Tactic:
lia