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 ℤ)
y : ℤ
inst_2 : K.HasTotal (up ℤ)
n₀ n₁ n₀' n₁' : ℤ
h₀ : n₀ + y = n₀'
h₁ : n₁ + y = n₁'
h : n₀ + 1 = n₁
p q : ℤ
hpq : p + q = n₀
pos :
  p.negOnePow •
      HSMul.hSMul (β := (K.X p).X (q + y) ⟶ (K.X p).X (q + 1 + y)) y.negOnePow ((K.X p).d (q + y) (q + 1 + y)) ≫
        HSMul.hSMul (β := (K.X p).X (q + 1 + y) ⟶ (K.total (up ℤ)).X n₁') (p * y).negOnePow
          (K.ιTotal (up ℤ) p (q + 1 + y) n₁' ⋯) =
    HSMul.hSMul (β := (K.X p).X (q + y) ⟶ (K.total (up ℤ)).X n₁') (y.negOnePow * (p * y).negOnePow * p.negOnePow)
      ((K.X p).d (q + y) (q + 1 + y) ≫ K.ιTotal (up ℤ) p (q + 1 + y) n₁' ⋯)
⊢ (up ℤ).ε₂ (up ℤ) (up ℤ) (p, q) •
      ((Functor.obj (shiftFunctor₂ C y) K).X p).d q (q + 1) ≫
        HSMul.hSMul (β := (K.X p).X (q + 1 + y) ⟶ (K.total (up ℤ)).X n₁') (p * y).negOnePow
          (K.ιTotal (up ℤ) p (q + 1 + y) n₁' ⋯) =
    HSMul.hSMul (β := (K.X p).X (q + y) ⟶ (K.total (up ℤ)).X n₁')
      (y.negOnePow * (p * y).negOnePow * (up ℤ).ε₂ (up ℤ) (up ℤ) (p, q + y))
      ((K.X p).d (q + y) (q + 1 + y) ≫ K.ιTotal (up ℤ) p (q + 1 + y) 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 : HomologicalComplex₂.{v_1, u_1, 0, 0} C (up ℤ) (up ℤ)
y : ℤ
inst_2 : K.HasTotal (up ℤ)
n₀ n₁ n₀' n₁' : ℤ
h₀ : n₀ + y = n₀'
h₁ : n₁ + y = n₁'
h : n₀ + 1 = n₁
p q : ℤ
hpq : p + q = n₀
pos :
  HSMul.hSMul (β := (K.X p).X (q + y) ⟶ (K.total (up ℤ)).X n₁') (p + y + p * y).negOnePow
      ((K.X p).d (q + y) (q + 1 + y) ≫ K.ιTotal (up ℤ) p (q + 1 + y) n₁' ⋯) =
    HSMul.hSMul (β := (K.X p).X (q + y) ⟶ (K.total (up ℤ)).X n₁') (y + p * y + p).negOnePow
      ((K.X p).d (q + y) (q + 1 + y) ≫ K.ιTotal (up ℤ) p (q + 1 + y) n₁' ⋯)
⊢ p.negOnePow •
      HSMul.hSMul (β := (K.X p).X (q + y) ⟶ (K.X p).X (q + 1 + y)) y.negOnePow ((K.X p).d (q + y) (q + 1 + y)) ≫
        HSMul.hSMul (β := (K.X p).X (q + 1 + y) ⟶ (K.total (up ℤ)).X n₁') (p * y).negOnePow
          (K.ιTotal (up ℤ) p (q + 1 + y) n₁' ⋯) =
    HSMul.hSMul (β := (K.X p).X (q + y) ⟶ (K.total (up ℤ)).X n₁') (y.negOnePow * (p * y).negOnePow * p.negOnePow)
      ((K.X p).d (q + y) (q + 1 + y) ≫ K.ιTotal (up ℤ) p (q + 1 + y) n₁' ⋯)

Tactic:
rw [Linear.units_smul_comp, Linear.comp_units_smul, smul_smul, smul_smul,
      ← Int.negOnePow_add, ← Int.negOnePow_add, ← Int.negOnePow_add,
      ← Int.negOnePow_add]

Premises used: CategoryTheory.Linear.units_smul_comp, smul_smul, Int.negOnePow_add, CategoryTheory.Linear.comp_units_smul
-- 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 ℤ)
y : ℤ
inst_2 : K.HasTotal (up ℤ)
n₀ n₁ n₀' n₁' : ℤ
h₀ : n₀ + y = n₀'
h₁ : n₁ + y = n₁'
h : n₀ + 1 = n₁
p q : ℤ
hpq : p + q = n₀
pos : p + y + p * y = y + p * y + p
⊢ HSMul.hSMul (β := (K.X p).X (q + y) ⟶ (K.total (up ℤ)).X n₁') (p + y + p * y).negOnePow
      ((K.X p).d (q + y) (q + 1 + y) ≫ K.ιTotal (up ℤ) p (q + 1 + y) n₁' ⋯) =
    HSMul.hSMul (β := (K.X p).X (q + y) ⟶ (K.total (up ℤ)).X n₁') (y + p * y + p).negOnePow
      ((K.X p).d (q + y) (q + 1 + y) ≫ K.ιTotal (up ℤ) p (q + 1 + y) n₁' ⋯)

Tactic:
congr 2
-- 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 ℤ)
y : ℤ
inst_2 : K.HasTotal (up ℤ)
n₀ n₁ n₀' n₁' : ℤ
h₀ : n₀ + y = n₀'
h₁ : n₁ + y = n₁'
h : n₀ + 1 = n₁
p q : ℤ
hpq : p + q = n₀
⊢ p + y + p * y = y + p * y + 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 : HomologicalComplex₂.{v_1, u_1, 0, 0} C (up ℤ) (up ℤ)
y : ℤ
inst_2 : K.HasTotal (up ℤ)
n₀ n₁ n₀' n₁' : ℤ
h₀ : n₀ + y = n₀'
h₁ : n₁ + y = n₁'
h : ¬(up ℤ).Rel n₀ n₁
neg : ¬(up ℤ).Rel n₀' n₁'
⊢ (Functor.obj (shiftFunctor₂ C y) K).D₂ (up ℤ) n₀ n₁ ≫ Iso.hom (K.totalShift₂XIso y n₁ n₁' h₁) =
    HSMul.hSMul (β :=
      ((Functor.obj (shiftFunctor₂ C y) K).total (up ℤ)).X n₀ ⟶
        GradedObject.mapObj.{0, 0, v_1, u_1} K.toGradedObject ((up ℤ).π (up ℤ) (up ℤ)) n₁')
      y.negOnePow (Iso.hom (K.totalShift₂XIso y n₀ n₀' h₀) ≫ K.D₂ (up ℤ) n₀' n₁')

Tactic:
rw [D₂_shape _ _ _ _ h, zero_comp, D₂_shape, comp_zero, smul_zero]

Premises used: CategoryTheory.Limits.comp_zero, smul_zero, HomologicalComplex₂.D₂_shape, CategoryTheory.Limits.zero_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 : HomologicalComplex₂.{v_1, u_1, 0, 0} C (up ℤ) (up ℤ)
y : ℤ
inst_2 : K.HasTotal (up ℤ)
n₀ n₁ n₀' n₁' : ℤ
h₀ : n₀ + y = n₀'
h₁ : n₁ + y = n₁'
h : ¬(up ℤ).Rel n₀ n₁
⊢ ¬n₀ + 1 = n₁

Tactic:
simp_all only [up_Rel]

Premises used: ComplexShape.up_Rel
-- 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 ℤ)
y : ℤ
inst_2 : K.HasTotal (up ℤ)
n₀ n₁ n₀' n₁' : ℤ
h₀ : n₀ + y = n₀'
h₁ : n₁ + y = n₁'
h : ¬n₀ + 1 = n₁
⊢ ¬n₀' + 1 = n₁'

Tactic:
grind
-- 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 : (up ℤ).Rel n n'
dsimp :
  Iso.hom (K.totalShift₂XIso y n (n + y) ⋯) ≫
      HSMul.hSMul (β := (K.total (up ℤ)).X (n + y) ⟶ (K.total (up ℤ)).X (n' + y)) y.negOnePow
        ((K.total (up ℤ)).d (n + y) (n' + y)) =
    ((Functor.obj (shiftFunctor₂ C y) K).total (up ℤ)).d n n' ≫ Iso.hom (K.totalShift₂XIso y n' (n' + y) ⋯)
⊢ Iso.hom
        ((fun (n : ℤ) ↦
            (K.totalShift₂XIso y n (n + y) ⋯ :
              ((Functor.obj (shiftFunctor₂ C y) K).total (up ℤ)).X n ≅ (K.total (up ℤ)).X (n + y)))
          n) ≫
      (Functor.obj (shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) y) (K.total (up ℤ))).d n n' =
    ((Functor.obj (shiftFunctor₂ C y) K).total (up ℤ)).d n n' ≫
      Iso.hom
        ((fun (n : ℤ) ↦
            (K.totalShift₂XIso y n (n + y) ⋯ :
              ((Functor.obj (shiftFunctor₂ C y) K).total (up ℤ)).X n ≅ (K.total (up ℤ)).X (n + y)))
          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 : (up ℤ).Rel n n'
⊢ Iso.hom (K.totalShift₂XIso y n (n + y) ⋯) ≫
      HSMul.hSMul (β := (K.total (up ℤ)).X (n + y) ⟶ (K.total (up ℤ)).X (n' + y)) y.negOnePow
        ((K.total (up ℤ)).d (n + y) (n' + y)) =
    ((Functor.obj (shiftFunctor₂ C y) K).total (up ℤ)).d n n' ≫ Iso.hom (K.totalShift₂XIso y n' (n' + y) ⋯)

Tactic:
simp only [total_d, Preadditive.add_comp, Preadditive.comp_add, smul_add,
        Linear.comp_units_smul, K.D₁_totalShift₂XIso_hom y n n' _ _ rfl rfl,
        K.D₂_totalShift₂XIso_hom y n n' _ _ rfl rfl]

Premises used: CategoryTheory.Linear.comp_units_smul, CategoryTheory.Preadditive.add_comp, CategoryTheory.Preadditive.comp_add, HomologicalComplex₂.total_d, HomologicalComplex₂.D₁_totalShift₂XIso_hom, HomologicalComplex₂.D₂_totalShift₂XIso_hom, smul_add, 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 ℤ)
a b n : ℤ
h : a + b = n
b' : ℤ
hb' : b' = b + y
n' : ℤ
hn' : n' = n + y
⊢ a + b' = 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 ℤ)
y : ℤ
inst_2 : K.HasTotal (up ℤ)
a b n : ℤ
h : a + b = n
b' : ℤ
hb' : b' = b + y
n' : ℤ
hn' : n' = n + y
subst :
  (Functor.obj (shiftFunctor₂ C y) K).ιTotal (up ℤ) a b n h ≫
      HomologicalComplex.Hom.f (Iso.hom (K.totalShift₂Iso y)) n =
    (a * y).negOnePow •
      (K.shiftFunctor₂XXIso a b y (b + y) ⋯).hom ≫
        K.ιTotal (up ℤ) a (b + y) (n + y) ⋯ ≫ (CochainComplex.shiftFunctorObjXIso (K.total (up ℤ)) y n (n + y) ⋯).inv
⊢ (Functor.obj (shiftFunctor₂ C y) K).ιTotal (up ℤ) a b n h ≫
      HomologicalComplex.Hom.f (Iso.hom (K.totalShift₂Iso y)) n =
    (a * y).negOnePow •
      (K.shiftFunctor₂XXIso a b y b' hb').hom ≫
        K.ιTotal (up ℤ) a b' n' ⋯ ≫ (CochainComplex.shiftFunctorObjXIso (K.total (up ℤ)) y n n' hn').inv

Tactic:
subst hb' hn'
-- 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 ℤ)
y : ℤ
inst_2 : K.HasTotal (up ℤ)
a b n : ℤ
h : a + b = n
dsimp :
  CategoryStruct.comp (Y := ((Functor.obj (shiftFunctor₂ C y) K).total (up ℤ)).X n)
      ((Functor.obj (shiftFunctor₂ C y) K).ιTotal (up ℤ) a b n h)
      ((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 + y)) (p * y).negOnePow
          (K.ιTotal (up ℤ) p (q + y) (n + y) ⋯)) =
    (a * y).negOnePow • 𝟙 ((K.X a).X (b + y)) ≫ K.ιTotal (up ℤ) a (b + y) (n + y) ⋯ ≫ 𝟙 ((K.total (up ℤ)).X (n + y))
⊢ (Functor.obj (shiftFunctor₂ C y) K).ιTotal (up ℤ) a b n h ≫
      HomologicalComplex.Hom.f (Iso.hom (K.totalShift₂Iso y)) n =
    (a * y).negOnePow •
      (K.shiftFunctor₂XXIso a b y (b + y) ⋯).hom ≫
        K.ιTotal (up ℤ) a (b + y) (n + y) ⋯ ≫ (CochainComplex.shiftFunctorObjXIso (K.total (up ℤ)) y n (n + y) ⋯).inv

Tactic:
dsimp [totalShift₂Iso, totalShift₂XIso]

Premises used: HomologicalComplex₂.totalShift₂Iso, 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 ℤ)
y : ℤ
inst_2 : K.HasTotal (up ℤ)
a b n : ℤ
h : a + b = n
⊢ CategoryStruct.comp (Y := ((Functor.obj (shiftFunctor₂ C y) K).total (up ℤ)).X n)
      ((Functor.obj (shiftFunctor₂ C y) K).ιTotal (up ℤ) a b n h)
      ((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 + y)) (p * y).negOnePow
          (K.ιTotal (up ℤ) p (q + y) (n + y) ⋯)) =
    (a * y).negOnePow • 𝟙 ((K.X a).X (b + y)) ≫ K.ιTotal (up ℤ) a (b + y) (n + y) ⋯ ≫ 𝟙 ((K.total (up ℤ)).X (n + y))

Tactic:
simp only [ι_totalDesc, comp_id, id_comp]

Premises used: HomologicalComplex₂.ι_totalDesc, 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 ℤ)
a b n : ℤ
h : a + b = n
b' n' : ℤ
hb' : a + b' = n'
hn' : n' = n + y
⊢ b' = b + 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 : HomologicalComplex₂.{v_1, u_1, 0, 0} C (up ℤ) (up ℤ)
y : ℤ
inst_2 : K.HasTotal (up ℤ)
a b n : ℤ
h : a + b = n
b' n' : ℤ
hb' : a + b' = n'
hn' : n' = n + y
subst :
  ∀ (hb' : a + b' = n + y),
    K.ιTotal (up ℤ) a b' (n + y) hb' ≫
        (CochainComplex.shiftFunctorObjXIso (K.total (up ℤ)) y n (n + y) ⋯).inv ≫
          HomologicalComplex.Hom.f (Iso.inv (K.totalShift₂Iso y)) n =
      HSMul.hSMul (β := (K.X a).X b' ⟶ ((Functor.obj (shiftFunctor₂ C y) K).total (up ℤ)).X n) (a * y).negOnePow
        ((K.shiftFunctor₂XXIso a b y b' ⋯).inv ≫ (Functor.obj (shiftFunctor₂ C y) K).ιTotal (up ℤ) a b n h)
⊢ K.ιTotal (up ℤ) a b' n' hb' ≫
      (CochainComplex.shiftFunctorObjXIso (K.total (up ℤ)) y n n' hn').inv ≫
        HomologicalComplex.Hom.f (Iso.inv (K.totalShift₂Iso y)) n =
    HSMul.hSMul (β := (K.X a).X b' ⟶ ((Functor.obj (shiftFunctor₂ C y) K).total (up ℤ)).X n) (a * y).negOnePow
      ((K.shiftFunctor₂XXIso a b y b' ⋯).inv ≫ (Functor.obj (shiftFunctor₂ C y) K).ιTotal (up ℤ) a b n h)

Tactic:
subst hn'
-- 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 ℤ)
y : ℤ
inst_2 : K.HasTotal (up ℤ)
a b n : ℤ
h : a + b = n
b' : ℤ
hb' : a + b' = n + y
⊢ b = b' - 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 : HomologicalComplex₂.{v_1, u_1, 0, 0} C (up ℤ) (up ℤ)
y : ℤ
inst_2 : K.HasTotal (up ℤ)
a b n : ℤ
h : a + b = n
b' : ℤ
hb' : a + b' = n + y
obtain :
  ∀ (h : a + (b' - y) = n),
    K.ιTotal (up ℤ) a b' (n + y) hb' ≫
        (CochainComplex.shiftFunctorObjXIso (K.total (up ℤ)) y n (n + y) ⋯).inv ≫
          HomologicalComplex.Hom.f (Iso.inv (K.totalShift₂Iso y)) n =
      HSMul.hSMul (β := (K.X a).X b' ⟶ ((Functor.obj (shiftFunctor₂ C y) K).total (up ℤ)).X n) (a * y).negOnePow
        ((K.shiftFunctor₂XXIso a (b' - y) y b' ⋯).inv ≫
          (Functor.obj (shiftFunctor₂ C y) K).ιTotal (up ℤ) a (b' - y) n h)
⊢ K.ιTotal (up ℤ) a b' (n + y) hb' ≫
      (CochainComplex.shiftFunctorObjXIso (K.total (up ℤ)) y n (n + y) ⋯).inv ≫
        HomologicalComplex.Hom.f (Iso.inv (K.totalShift₂Iso y)) n =
    HSMul.hSMul (β := (K.X a).X b' ⟶ ((Functor.obj (shiftFunctor₂ C y) K).total (up ℤ)).X n) (a * y).negOnePow
      ((K.shiftFunctor₂XXIso a b y b' ⋯).inv ≫ (Functor.obj (shiftFunctor₂ C y) K).ιTotal (up ℤ) a b n h)

Tactic:
obtain rfl : b = b' - y := by lia

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

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

Premises used: HomologicalComplex₂.totalShift₂Iso, HomologicalComplex₂.XXIsoOfEq, HomologicalComplex₂.totalShift₂XIso, HomologicalComplex₂.shiftFunctor₂XXIso
-- 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 ℤ)
y : ℤ
inst_2 : K.HasTotal (up ℤ)
a n b' : ℤ
hb' : a + b' = n + y
h : a + (b' - y) = n
⊢ (K.ιTotal (up ℤ) a b' (n + y) hb' ≫
      𝟙 ((K.total (up ℤ)).X (n + y)) ≫
        K.totalDesc fun (p q : ℤ) (hpq : p + q = n + y) ↦
          HSMul.hSMul (β := (K.X p).X q ⟶ ((Functor.obj (shiftFunctor₂ C y) K).total (up ℤ)).X n) (p * y).negOnePow
            (eqToHom ⋯ ≫ (Functor.obj (shiftFunctor₂ C y) K).ιTotal (up ℤ) p (q - y) n ⋯)) =
    HSMul.hSMul (β := (K.X a).X b' ⟶ ((Functor.obj (shiftFunctor₂ C y) K).total (up ℤ)).X n) (a * y).negOnePow
      (eqToHom ⋯ ≫ (Functor.obj (shiftFunctor₂ C y) K).ιTotal (up ℤ) a (b' - y) 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
y : ℤ
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 y) K).X i₁).X i₂ ⟶
        (Functor.obj (shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) y) (L.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 ℤ) i₁ i₂ n h)
        (HomologicalComplex.Hom.f
          (total.map (CategoryTheory.Functor.map (shiftFunctor₂ C y) f) (up ℤ) ≫ Iso.hom (L.totalShift₂Iso y)) n))
      (CategoryStruct.comp (Y := ((Functor.obj (shiftFunctor₂ C y) K).total (up ℤ)).X n)
        ((Functor.obj (shiftFunctor₂ C y) K).ιTotal (up ℤ) i₁ i₂ n h :
          ((Functor.obj (shiftFunctor₂ C y) K).X i₁).X i₂ ⟶ ((Functor.obj (shiftFunctor₂ C y) K).total (up ℤ)).X n)
        (HomologicalComplex.Hom.f
            (CategoryStruct.comp (Y :=
              Functor.obj (shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) y) (K.total (up ℤ)))
              (Iso.hom (K.totalShift₂Iso y))
              (CategoryTheory.Functor.map (shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) y)
                (total.map f (up ℤ))))
            n :
          ((Functor.obj (shiftFunctor₂ C y) K).total (up ℤ)).X n ⟶
            (Functor.obj (shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) y) (L.total (up ℤ))).X n))
⊢ Eq (α :=
    (Functor.obj (shiftFunctor₂ C y) K).total (up ℤ) ⟶
      Functor.obj (shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) y) (L.total (up ℤ)))
    (total.map (CategoryTheory.Functor.map (shiftFunctor₂ C y) f) (up ℤ) ≫ Iso.hom (L.totalShift₂Iso y) :
      (Functor.obj (shiftFunctor₂ C y) K).total (up ℤ) ⟶
        Functor.obj (shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) y) (L.total (up ℤ)))
    (CategoryStruct.comp (Y :=
        Functor.obj (shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) y) (K.total (up ℤ)))
        (Iso.hom (K.totalShift₂Iso y))
        (CategoryTheory.Functor.map (shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) y) (total.map f (up ℤ))) :
      (Functor.obj (shiftFunctor₂ C y) K).total (up ℤ) ⟶
        Functor.obj (shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) y) (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
y : ℤ
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 (i₂ + y) ⟶ (L.total (up ℤ)).X (n + y))
    (CategoryStruct.comp (Y := ((Functor.obj (shiftFunctor₂ C y) K).total (up ℤ)).X n)
      ((Functor.obj (shiftFunctor₂ C y) K).ιTotal (up ℤ) i₁ i₂ n h)
      (HomologicalComplex.Hom.f (total.map (CategoryTheory.Functor.map (shiftFunctor₂ C y) f) (up ℤ)) n ≫
        HomologicalComplex.Hom.f (Iso.hom (L.totalShift₂Iso y)) n))
    (CategoryStruct.comp (Y := ((Functor.obj (shiftFunctor₂ C y) K).total (up ℤ)).X n)
      ((Functor.obj (shiftFunctor₂ C y) K).ιTotal (up ℤ) i₁ i₂ n h :
        ((Functor.obj (shiftFunctor₂ C y) K).X i₁).X i₂ ⟶ ((Functor.obj (shiftFunctor₂ C y) K).total (up ℤ)).X n)
      (CategoryStruct.comp (Y := (K.total (up ℤ)).X (n + y)) (HomologicalComplex.Hom.f (Iso.hom (K.totalShift₂Iso y)) n)
          (HomologicalComplex.Hom.f (total.map f (up ℤ)) (n + y)) :
        ((Functor.obj (shiftFunctor₂ C y) K).total (up ℤ)).X n ⟶ (L.total (up ℤ)).X (n + y)))
⊢ Eq (α :=
    ((Functor.obj (shiftFunctor₂ C y) K).X i₁).X i₂ ⟶
      (Functor.obj (shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) y) (L.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 ℤ) i₁ i₂ n h)
      (HomologicalComplex.Hom.f
        (total.map (CategoryTheory.Functor.map (shiftFunctor₂ C y) f) (up ℤ) ≫ Iso.hom (L.totalShift₂Iso y)) n))
    (CategoryStruct.comp (Y := ((Functor.obj (shiftFunctor₂ C y) K).total (up ℤ)).X n)
      ((Functor.obj (shiftFunctor₂ C y) K).ιTotal (up ℤ) i₁ i₂ n h :
        ((Functor.obj (shiftFunctor₂ C y) K).X i₁).X i₂ ⟶ ((Functor.obj (shiftFunctor₂ C y) K).total (up ℤ)).X n)
      (HomologicalComplex.Hom.f
          (CategoryStruct.comp (Y :=
            Functor.obj (shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) y) (K.total (up ℤ)))
            (Iso.hom (K.totalShift₂Iso y))
            (CategoryTheory.Functor.map (shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) y)
              (total.map f (up ℤ))))
          n :
        ((Functor.obj (shiftFunctor₂ C y) K).total (up ℤ)).X n ⟶
          (Functor.obj (shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) y) (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
y : ℤ
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 y) f) i₁) i₂ ≫
      ((i₁ * y).negOnePow •
        (L.shiftFunctor₂XXIso i₁ i₂ y (i₂ + y) ⋯).hom ≫
          L.ιTotal (up ℤ) i₁ (i₂ + y) (n + y) ⋯ ≫
            (CochainComplex.shiftFunctorObjXIso (L.total (up ℤ)) y n (n + y) ⋯).inv) =
    ((i₁ * y).negOnePow •
        (K.shiftFunctor₂XXIso i₁ i₂ y (i₂ + y) ⋯).hom ≫
          K.ιTotal (up ℤ) i₁ (i₂ + y) (n + y) ⋯ ≫
            (CochainComplex.shiftFunctorObjXIso (K.total (up ℤ)) y n (n + y) ⋯).inv) ≫
      HomologicalComplex.Hom.f (total.map f (up ℤ)) (n + y)
⊢ Eq (α := (K.X i₁).X (i₂ + y) ⟶ (L.total (up ℤ)).X (n + y))
    (CategoryStruct.comp (Y := ((Functor.obj (shiftFunctor₂ C y) K).total (up ℤ)).X n)
      ((Functor.obj (shiftFunctor₂ C y) K).ιTotal (up ℤ) i₁ i₂ n h)
      (HomologicalComplex.Hom.f (total.map (CategoryTheory.Functor.map (shiftFunctor₂ C y) f) (up ℤ)) n ≫
        HomologicalComplex.Hom.f (Iso.hom (L.totalShift₂Iso y)) n))
    (CategoryStruct.comp (Y := ((Functor.obj (shiftFunctor₂ C y) K).total (up ℤ)).X n)
      ((Functor.obj (shiftFunctor₂ C y) K).ιTotal (up ℤ) i₁ i₂ n h :
        ((Functor.obj (shiftFunctor₂ C y) K).X i₁).X i₂ ⟶ ((Functor.obj (shiftFunctor₂ C y) K).total (up ℤ)).X n)
      (CategoryStruct.comp (Y := (K.total (up ℤ)).X (n + y)) (HomologicalComplex.Hom.f (Iso.hom (K.totalShift₂Iso y)) n)
          (HomologicalComplex.Hom.f (total.map f (up ℤ)) (n + y)) :
        ((Functor.obj (shiftFunctor₂ C y) K).total (up ℤ)).X n ⟶ (L.total (up ℤ)).X (n + y)))

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

Premises used: HomologicalComplex₂.ι_totalShift₂Iso_hom_f_assoc, HomologicalComplex₂.ι_totalShift₂Iso_hom_f, rfl, HomologicalComplex₂.ιTotal_map_assoc