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 : HomologicalComplex₂.{v_1, u_1, 0, 0} C (up ℤ) (up ℤ)
x : ℤ
inst_2 : K.HasTotal (up ℤ)
b n a' : ℤ
ha' : a' + b = n + x
h : a' - x + b = n
dsimp :
  Eq (α := (K.X a').X b ⟶ ((Functor.obj (shiftFunctor₁ C x) K).total (up ℤ)).X n)
    (K.ιTotal (up ℤ) a' b (n + x) ha' ≫
      𝟙 ((K.total (up ℤ)).X (n + x)) ≫
        K.totalDesc fun (p q : ℤ) (hpq : p + q = n + x) ↦
          eqToHom ⋯ ≫ (Functor.obj (shiftFunctor₁ C x) K).ιTotal (up ℤ) (p - x) q n ⋯)
    (eqToHom ⋯ ≫ (Functor.obj (shiftFunctor₁ C x) K).ιTotal (up ℤ) (a' - x) b n h)
⊢ K.ιTotal (up ℤ) a' b (n + x) ha' ≫
      (CochainComplex.shiftFunctorObjXIso (K.total (up ℤ)) x n (n + x) ⋯).inv ≫
        HomologicalComplex.Hom.f (Iso.inv (K.totalShift₁Iso x)) n =
    (K.shiftFunctor₁XXIso (a' - x) x a' ⋯ b).inv ≫ (Functor.obj (shiftFunctor₁ C x) K).ιTotal (up ℤ) (a' - x) b n h

Tactic:
dsimp [totalShift₁Iso, totalShift₁XIso, shiftFunctor₁XXIso, XXIsoOfEq]

Premises used: HomologicalComplex₂.totalShift₁XIso, HomologicalComplex₂.XXIsoOfEq, HomologicalComplex₂.shiftFunctor₁XXIso, HomologicalComplex₂.totalShift₁Iso
-- 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 ℤ)
b n a' : ℤ
ha' : a' + b = n + x
h : a' - x + b = n
⊢ Eq (α := (K.X a').X b ⟶ ((Functor.obj (shiftFunctor₁ C x) K).total (up ℤ)).X n)
    (K.ιTotal (up ℤ) a' b (n + x) ha' ≫
      𝟙 ((K.total (up ℤ)).X (n + x)) ≫
        K.totalDesc fun (p q : ℤ) (hpq : p + q = n + x) ↦
          eqToHom ⋯ ≫ (Functor.obj (shiftFunctor₁ C x) K).ιTotal (up ℤ) (p - x) q n ⋯)
    (eqToHom ⋯ ≫ (Functor.obj (shiftFunctor₁ C x) K).ιTotal (up ℤ) (a' - x) b n h)

Tactic:
simp only [id_comp, ι_totalDesc]

Premises used: HomologicalComplex₂.ι_totalDesc, CategoryTheory.Category.id_comp
-- Module: Mathlib.Algebra.Homology.TotalComplexShift
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K L : HomologicalComplex₂.{v_1, u_1, 0, 0} C (up ℤ) (up ℤ)
f : K ⟶ L
x : ℤ
inst_2 : K.HasTotal (up ℤ)
inst_3 : L.HasTotal (up ℤ)
h :
  ∀ (n i₁ i₂ : ℤ) (h : (up ℤ).π (up ℤ) (up ℤ) (i₁, i₂) = n),
    Eq (α :=
      ((Functor.obj (shiftFunctor₁ C x) K).X i₁).X i₂ ⟶
        (Functor.obj (shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) x) (L.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 ℤ) i₁ i₂ n h)
        (HomologicalComplex.Hom.f
          (total.map (CategoryTheory.Functor.map (shiftFunctor₁ C x) f) (up ℤ) ≫ Iso.hom (L.totalShift₁Iso x)) 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 h :
          ((Functor.obj (shiftFunctor₁ C x) K).X i₁).X i₂ ⟶ ((Functor.obj (shiftFunctor₁ C x) K).total (up ℤ)).X n)
        (HomologicalComplex.Hom.f
            (CategoryStruct.comp (Y :=
              Functor.obj (shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) x) (K.total (up ℤ)))
              (Iso.hom (K.totalShift₁Iso x))
              (CategoryTheory.Functor.map (shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) x)
                (total.map f (up ℤ))))
            n :
          ((Functor.obj (shiftFunctor₁ C x) K).total (up ℤ)).X n ⟶
            (Functor.obj (shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) x) (L.total (up ℤ))).X n))
⊢ Eq (α :=
    (Functor.obj (shiftFunctor₁ C x) K).total (up ℤ) ⟶
      Functor.obj (shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) x) (L.total (up ℤ)))
    (total.map (CategoryTheory.Functor.map (shiftFunctor₁ C x) f) (up ℤ) ≫ Iso.hom (L.totalShift₁Iso x) :
      (Functor.obj (shiftFunctor₁ C x) K).total (up ℤ) ⟶
        Functor.obj (shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) x) (L.total (up ℤ)))
    (CategoryStruct.comp (Y :=
        Functor.obj (shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) x) (K.total (up ℤ)))
        (Iso.hom (K.totalShift₁Iso x))
        (CategoryTheory.Functor.map (shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) x) (total.map f (up ℤ))) :
      (Functor.obj (shiftFunctor₁ C x) K).total (up ℤ) ⟶
        Functor.obj (shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) x) (L.total (up ℤ)))

Tactic:
ext n i₁ i₂ 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 : ℤ
inst_2 : K.HasTotal (up ℤ)
inst_3 : L.HasTotal (up ℤ)
n i₁ i₂ : ℤ
h : (up ℤ).π (up ℤ) (up ℤ) (i₁, i₂) = n
h₁ :
  Eq (α := (K.X (i₁ + x)).X i₂ ⟶ (L.total (up ℤ)).X (n + x))
    (CategoryStruct.comp (Y := ((Functor.obj (shiftFunctor₁ C x) K).total (up ℤ)).X n)
      ((Functor.obj (shiftFunctor₁ C x) K).ιTotal (up ℤ) i₁ i₂ n h)
      (HomologicalComplex.Hom.f (total.map (CategoryTheory.Functor.map (shiftFunctor₁ C x) f) (up ℤ)) n ≫
        HomologicalComplex.Hom.f (Iso.hom (L.totalShift₁Iso x)) 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 h :
        ((Functor.obj (shiftFunctor₁ C x) K).X i₁).X i₂ ⟶ ((Functor.obj (shiftFunctor₁ C x) K).total (up ℤ)).X n)
      (CategoryStruct.comp (Y := (K.total (up ℤ)).X (n + x)) (HomologicalComplex.Hom.f (Iso.hom (K.totalShift₁Iso x)) n)
          (HomologicalComplex.Hom.f (total.map f (up ℤ)) (n + x)) :
        ((Functor.obj (shiftFunctor₁ C x) K).total (up ℤ)).X n ⟶ (L.total (up ℤ)).X (n + x)))
⊢ Eq (α :=
    ((Functor.obj (shiftFunctor₁ C x) K).X i₁).X i₂ ⟶
      (Functor.obj (shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) x) (L.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 ℤ) i₁ i₂ n h)
      (HomologicalComplex.Hom.f
        (total.map (CategoryTheory.Functor.map (shiftFunctor₁ C x) f) (up ℤ) ≫ Iso.hom (L.totalShift₁Iso x)) 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 h :
        ((Functor.obj (shiftFunctor₁ C x) K).X i₁).X i₂ ⟶ ((Functor.obj (shiftFunctor₁ C x) K).total (up ℤ)).X n)
      (HomologicalComplex.Hom.f
          (CategoryStruct.comp (Y :=
            Functor.obj (shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) x) (K.total (up ℤ)))
            (Iso.hom (K.totalShift₁Iso x))
            (CategoryTheory.Functor.map (shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) x)
              (total.map f (up ℤ))))
          n :
        ((Functor.obj (shiftFunctor₁ C x) K).total (up ℤ)).X n ⟶
          (Functor.obj (shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) x) (L.total (up ℤ))).X n))

Tactic:
dsimp at 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 : ℤ
inst_2 : K.HasTotal (up ℤ)
inst_3 : L.HasTotal (up ℤ)
n i₁ i₂ : ℤ
h : i₁ + i₂ = n
h₁ :
  HomologicalComplex.Hom.f (HomologicalComplex.Hom.f (CategoryTheory.Functor.map (shiftFunctor₁ C x) f) i₁) i₂ ≫
      (L.shiftFunctor₁XXIso i₁ x (i₁ + x) ⋯ i₂).hom ≫
        L.ιTotal (up ℤ) (i₁ + x) i₂ (n + x) ⋯ ≫
          (CochainComplex.shiftFunctorObjXIso (L.total (up ℤ)) x n (n + x) ⋯).inv =
    (K.shiftFunctor₁XXIso i₁ x (i₁ + x) ⋯ i₂).hom ≫
      K.ιTotal (up ℤ) (i₁ + x) i₂ (n + x) ⋯ ≫
        (CochainComplex.shiftFunctorObjXIso (K.total (up ℤ)) x n (n + x) ⋯).inv ≫
          HomologicalComplex.Hom.f (total.map f (up ℤ)) (n + x)
⊢ Eq (α := (K.X (i₁ + x)).X i₂ ⟶ (L.total (up ℤ)).X (n + x))
    (CategoryStruct.comp (Y := ((Functor.obj (shiftFunctor₁ C x) K).total (up ℤ)).X n)
      ((Functor.obj (shiftFunctor₁ C x) K).ιTotal (up ℤ) i₁ i₂ n h)
      (HomologicalComplex.Hom.f (total.map (CategoryTheory.Functor.map (shiftFunctor₁ C x) f) (up ℤ)) n ≫
        HomologicalComplex.Hom.f (Iso.hom (L.totalShift₁Iso x)) 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 h :
        ((Functor.obj (shiftFunctor₁ C x) K).X i₁).X i₂ ⟶ ((Functor.obj (shiftFunctor₁ C x) K).total (up ℤ)).X n)
      (CategoryStruct.comp (Y := (K.total (up ℤ)).X (n + x)) (HomologicalComplex.Hom.f (Iso.hom (K.totalShift₁Iso x)) n)
          (HomologicalComplex.Hom.f (total.map f (up ℤ)) (n + x)) :
        ((Functor.obj (shiftFunctor₁ C x) K).total (up ℤ)).X n ⟶ (L.total (up ℤ)).X (n + x)))

Tactic:
rw [ιTotal_map_assoc, L.ι_totalShift₁Iso_hom_f x i₁ i₂ n h _ rfl _ rfl,
    K.ι_totalShift₁Iso_hom_f_assoc x i₁ i₂ n h _ rfl _ rfl]

Premises used: HomologicalComplex₂.ι_totalShift₁Iso_hom_f_assoc, rfl, HomologicalComplex₂.ιTotal_map_assoc, HomologicalComplex₂.ι_totalShift₁Iso_hom_f
-- 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 : ℤ
inst_2 : K.HasTotal (up ℤ)
inst_3 : L.HasTotal (up ℤ)
n i₁ i₂ : ℤ
h : i₁ + i₂ = n
h₁ :
  HomologicalComplex.Hom.f (f.f (i₁ + x)) i₂ ≫
      𝟙 ((L.X (i₁ + x)).X i₂) ≫ L.ιTotal (up ℤ) (i₁ + x) i₂ (n + x) ⋯ ≫ 𝟙 ((L.total (up ℤ)).X (n + x)) =
    𝟙 ((K.X (i₁ + x)).X i₂) ≫
      K.ιTotal (up ℤ) (i₁ + x) i₂ (n + x) ⋯ ≫
        𝟙 ((K.total (up ℤ)).X (n + x)) ≫ HomologicalComplex.Hom.f (total.map f (up ℤ)) (n + x)
⊢ HomologicalComplex.Hom.f (HomologicalComplex.Hom.f (CategoryTheory.Functor.map (shiftFunctor₁ C x) f) i₁) i₂ ≫
      (L.shiftFunctor₁XXIso i₁ x (i₁ + x) ⋯ i₂).hom ≫
        L.ιTotal (up ℤ) (i₁ + x) i₂ (n + x) ⋯ ≫
          (CochainComplex.shiftFunctorObjXIso (L.total (up ℤ)) x n (n + x) ⋯).inv =
    (K.shiftFunctor₁XXIso i₁ x (i₁ + x) ⋯ i₂).hom ≫
      K.ιTotal (up ℤ) (i₁ + x) i₂ (n + x) ⋯ ≫
        (CochainComplex.shiftFunctorObjXIso (K.total (up ℤ)) x n (n + x) ⋯).inv ≫
          HomologicalComplex.Hom.f (total.map f (up ℤ)) (n + x)

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 : ℤ
inst_2 : K.HasTotal (up ℤ)
inst_3 : L.HasTotal (up ℤ)
n i₁ i₂ : ℤ
h : i₁ + i₂ = n
h₁ :
  HomologicalComplex.Hom.f (f.f (i₁ + x)) i₂ ≫ L.ιTotal (up ℤ) (i₁ + x) i₂ (n + x) ⋯ ≫ 𝟙 ((L.total (up ℤ)).X (n + x)) =
    𝟙 ((K.X (i₁ + x)).X i₂) ≫
      K.ιTotal (up ℤ) (i₁ + x) i₂ (n + x) ⋯ ≫
        𝟙 ((K.total (up ℤ)).X (n + x)) ≫ HomologicalComplex.Hom.f (total.map f (up ℤ)) (n + x)
h₂ :
  HomologicalComplex.Hom.f (f.f (i₁ + x)) i₂ ≫ L.ιTotal (up ℤ) (i₁ + x) i₂ (n + x) ⋯ ≫ 𝟙 ((L.total (up ℤ)).X (n + x)) =
    K.ιTotal (up ℤ) (i₁ + x) i₂ (n + x) ⋯ ≫
      𝟙 ((K.total (up ℤ)).X (n + x)) ≫ HomologicalComplex.Hom.f (total.map f (up ℤ)) (n + x)
h₃ :
  HomologicalComplex.Hom.f (f.f (i₁ + x)) i₂ ≫ L.ιTotal (up ℤ) (i₁ + x) i₂ (n + x) ⋯ ≫ 𝟙 ((L.total (up ℤ)).X (n + x)) =
    CategoryStruct.comp (Y := (K.total (up ℤ)).X (n + x)) (K.ιTotal (up ℤ) (i₁ + x) i₂ (n + x) ⋯)
      (HomologicalComplex.Hom.f (total.map f (up ℤ)) (n + x))
h₄ :
  Eq (α := (K.X (i₁ + x)).X i₂ ⟶ (L.total (up ℤ)).X (n + x))
    (HomologicalComplex.Hom.f (f.f (i₁ + x)) i₂ ≫ L.ιTotal (up ℤ) (i₁ + x) i₂ (n + x) ⋯)
    (CategoryStruct.comp (Y := (K.total (up ℤ)).X (n + x)) (K.ιTotal (up ℤ) (i₁ + x) i₂ (n + x) ⋯)
      (HomologicalComplex.Hom.f (total.map f (up ℤ)) (n + x)))
h₅ h₆ :
  Eq (α := (K.X (i₁ + x)).X i₂ ⟶ (L.total (up ℤ)).X (n + x))
    (HomologicalComplex.Hom.f (f.f (i₁ + x)) i₂ ≫ L.ιTotal (up ℤ) (i₁ + x) i₂ (n + x) ⋯)
    (HomologicalComplex.Hom.f (f.f (i₁ + x)) i₂ ≫ L.ιTotal (up ℤ) (i₁ + x) i₂ (n + x) ⋯)
⊢ HomologicalComplex.Hom.f (f.f (i₁ + x)) i₂ ≫
      𝟙 ((L.X (i₁ + x)).X i₂) ≫ L.ιTotal (up ℤ) (i₁ + x) i₂ (n + x) ⋯ ≫ 𝟙 ((L.total (up ℤ)).X (n + x)) =
    𝟙 ((K.X (i₁ + x)).X i₂) ≫
      K.ιTotal (up ℤ) (i₁ + x) i₂ (n + x) ⋯ ≫
        𝟙 ((K.total (up ℤ)).X (n + x)) ≫ HomologicalComplex.Hom.f (total.map f (up ℤ)) (n + x)

Tactic:
rw [id_comp, id_comp, id_comp, comp_id, ιTotal_map]

Premises used: HomologicalComplex₂.ιTotal_map, CategoryTheory.Category.comp_id, CategoryTheory.Category.id_comp
-- Module: Mathlib.Algebra.Homology.TotalComplexShift
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K 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'
p q : ℤ
hpq : p + q = n
⊢ p + (q + y) = n'

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.TotalComplexShift
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K 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'
p q : ℤ
hpq : p + q = n'
⊢ p + (q - y) = n

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.TotalComplexShift
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K 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'
h₁ :
  ∀ (p q : ℤ) (h_1 : (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_1)
        (CategoryStruct.comp (Y := (K.total (up ℤ)).X 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.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).ιTotal (up ℤ) p q n h_1 ≫
        𝟙 (((Functor.obj (shiftFunctor₂ C y) K).total (up ℤ)).X n)
⊢ CategoryStruct.comp (Y := (K.total (up ℤ)).X 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.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).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 + y = n'
p q : ℤ
h : (up ℤ).π (up ℤ) (up ℤ) (p, q) = n
h₁ :
  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)
⊢ 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 : (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.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).ιTotal (up ℤ) p q n h ≫
      𝟙 (((Functor.obj (shiftFunctor₂ C y) 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 + y = n'
p q : ℤ
h : (up ℤ).π (up ℤ) (up ℤ) (p, q) = n
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 ⋯ ⋯) ≫ (Functor.obj (shiftFunctor₂ C y) K).ιTotal (up ℤ) p (q + y - y) n ⋯)
    ((Functor.obj (shiftFunctor₂ C y) K).ιTotal (up ℤ) p q n h)
⊢ 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)

Tactic:
simp only [ι_totalDesc_assoc, Linear.units_smul_comp, ι_totalDesc, smul_smul,
      Int.units_mul_self, one_smul, comp_id]

Premises used: CategoryTheory.Linear.units_smul_comp, HomologicalComplex₂.ι_totalDesc_assoc, smul_smul, HomologicalComplex₂.ι_totalDesc, CategoryTheory.Category.comp_id, one_smul, Int.units_mul_self
-- Module: Mathlib.Algebra.Homology.TotalComplexShift
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K 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
⊢ q + y - y = q

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

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

Premises used: HomologicalComplex₂.XXIsoOfEq_inv_ιTotal, HomologicalComplex₂.shiftFunctor₂, 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 + y = 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 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')
⊢ 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')

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 + y = 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 y) K).total (up ℤ)).X n)
        (K.totalDesc fun (p q : ℤ) (hpq : p + q = n') ↦
          HSMul.hSMul (β := (K.X p).X q ⟶ ((Functor.obj (shiftFunctor₂ C y) K).total (up ℤ)).X n) (p * y).negOnePow
            (Iso.inv (XXIsoOfEq C (up ℤ) (up ℤ) K ⋯ ⋯) ≫
              (Functor.obj (shiftFunctor₂ C y) K).ιTotal (up ℤ) p (q - y) n ⋯))
        ((Functor.obj (shiftFunctor₂ C y) K).totalDesc fun (p q : ℤ) (hpq : p + q = n) ↦
          HSMul.hSMul (β := (K.X p).X (q + y) ⟶ (K.total (up ℤ)).X n') (p * y).negOnePow
            (K.ιTotal (up ℤ) p (q + y) n' ⋯))) =
    K.ιTotal (up ℤ) i₁ i₂ n' hi ≫ 𝟙 ((K.total (up ℤ)).X n')
⊢ 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')

Tactic:
dsimp