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
y : ℤ
inst_2 : K.HasTotal (up ℤ)
inst_3 : L.HasTotal (up ℤ)
n i₁ i₂ : ℤ
h : i₁ + i₂ = n
h₁ :
  (f.f i₁).f (i₂ + y) ≫
      ((i₁ * y).negOnePow •
        𝟙 ((L.X i₁).X (i₂ + y)) ≫ L.ιTotal (up ℤ) i₁ (i₂ + y) (n + y) ⋯ ≫ 𝟙 ((L.total (up ℤ)).X (n + y))) =
    ((i₁ * y).negOnePow •
        𝟙 ((K.X i₁).X (i₂ + y)) ≫ K.ιTotal (up ℤ) i₁ (i₂ + y) (n + y) ⋯ ≫ 𝟙 ((K.total (up ℤ)).X (n + y))) ≫
      HomologicalComplex.Hom.f (total.map f (up ℤ)) (n + y)
⊢ 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)

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 ℤ)
x y : ℤ
inst_2 : K.HasTotal (up ℤ)
w :
  ∀ (n n₁ n₂ : ℤ) (h : (up ℤ).π (up ℤ) (up ℤ) (n₁, n₂) = n),
    (Functor.obj (shiftFunctor₁ C x) (Functor.obj (shiftFunctor₂ C y) K)).ιTotal (up ℤ) n₁ n₂ n h ≫
        HomologicalComplex.Hom.f
          (Iso.hom
            ((Functor.obj (shiftFunctor₂ C y) K).totalShift₁Iso x ≪≫
              Functor.mapIso (shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) x) (K.totalShift₂Iso y)))
          n =
      (Functor.obj (shiftFunctor₁ C x) (Functor.obj (shiftFunctor₂ C y) K)).ιTotal (up ℤ) n₁ n₂ n h ≫
        (HSMul.hSMul (β :=
                (Functor.obj (shiftFunctor₂ C y ⋙ shiftFunctor₁ C x) K).total (up ℤ) ≅
                  Functor.obj
                    (shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) y ⋙
                      shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) x)
                    (K.total (up ℤ)))
                (x * y).negOnePow
                (total.mapIso (Iso.app (shiftFunctor₁₂CommIso C x y) K) (up ℤ) ≪≫
                  (Functor.obj (shiftFunctor₁ C x) K).totalShift₂Iso y ≪≫
                    Functor.mapIso (shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) y) (K.totalShift₁Iso x) ≪≫
                      Iso.app (shiftFunctorComm (CochainComplex.{v_1, u_1, 0} C ℤ) x y) (K.total (up ℤ)))).hom.f
          n
⊢ (Functor.obj (shiftFunctor₂ C y) K).totalShift₁Iso x ≪≫
      Functor.mapIso (shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) x) (K.totalShift₂Iso y) =
    HSMul.hSMul (β :=
      (Functor.obj (shiftFunctor₂ C y ⋙ shiftFunctor₁ C x) K).total (up ℤ) ≅
        Functor.obj
          (shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) y ⋙ shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) x)
          (K.total (up ℤ)))
      (x * y).negOnePow
      (total.mapIso (Iso.app (shiftFunctor₁₂CommIso C x y) K) (up ℤ) ≪≫
        (Functor.obj (shiftFunctor₁ C x) K).totalShift₂Iso y ≪≫
          Functor.mapIso (shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) y) (K.totalShift₁Iso x) ≪≫
            Iso.app (shiftFunctorComm (CochainComplex.{v_1, u_1, 0} C ℤ) x y) (K.total (up ℤ)))

Tactic:
ext n n₁ n₂ 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 : HomologicalComplex₂.{v_1, u_1, 0, 0} C (up ℤ) (up ℤ)
x y : ℤ
inst_2 : K.HasTotal (up ℤ)
n n₁ n₂ : ℤ
h : (up ℤ).π (up ℤ) (up ℤ) (n₁, n₂) = n
w :
  (Functor.obj (shiftFunctor₁ C x) (Functor.obj (shiftFunctor₂ C y) K)).ιTotal (up ℤ) n₁ n₂ n h ≫
      HomologicalComplex.Hom.f (Iso.hom ((Functor.obj (shiftFunctor₂ C y) K).totalShift₁Iso x)) n ≫
        HomologicalComplex.Hom.f (Iso.hom (K.totalShift₂Iso y)) (n + x) =
    (Functor.obj (shiftFunctor₁ C x) (Functor.obj (shiftFunctor₂ C y) K)).ιTotal (up ℤ) n₁ n₂ n h ≫
      HSMul.hSMul (β :=
        ((Functor.obj (shiftFunctor₁ C x) (Functor.obj (shiftFunctor₂ C y) K)).total (up ℤ)).X n ⟶
          (K.total (up ℤ)).X (n + x + y))
        (x * y).negOnePow
        (HomologicalComplex.Hom.f (total.map (NatTrans.app (Iso.hom (shiftFunctor₁₂CommIso C x y)) K) (up ℤ)) n ≫
          HomologicalComplex.Hom.f (Iso.hom ((Functor.obj (shiftFunctor₁ C x) K).totalShift₂Iso y)) n ≫
            HomologicalComplex.Hom.f (Iso.hom (K.totalShift₁Iso x)) (n + y) ≫
              HomologicalComplex.Hom.f
                (NatTrans.app (Iso.hom (shiftFunctorComm (CochainComplex.{v_1, u_1, 0} C ℤ) x y)) (K.total (up ℤ))) n)
⊢ (Functor.obj (shiftFunctor₁ C x) (Functor.obj (shiftFunctor₂ C y) K)).ιTotal (up ℤ) n₁ n₂ n h ≫
      HomologicalComplex.Hom.f
        (Iso.hom
          ((Functor.obj (shiftFunctor₂ C y) K).totalShift₁Iso x ≪≫
            Functor.mapIso (shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) x) (K.totalShift₂Iso y)))
        n =
    (Functor.obj (shiftFunctor₁ C x) (Functor.obj (shiftFunctor₂ C y) K)).ιTotal (up ℤ) n₁ n₂ n h ≫
      (HSMul.hSMul (β :=
              (Functor.obj (shiftFunctor₂ C y ⋙ shiftFunctor₁ C x) K).total (up ℤ) ≅
                Functor.obj
                  (shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) y ⋙
                    shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) x)
                  (K.total (up ℤ)))
              (x * y).negOnePow
              (total.mapIso (Iso.app (shiftFunctor₁₂CommIso C x y) K) (up ℤ) ≪≫
                (Functor.obj (shiftFunctor₁ C x) K).totalShift₂Iso y ≪≫
                  Functor.mapIso (shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) y) (K.totalShift₁Iso x) ≪≫
                    Iso.app (shiftFunctorComm (CochainComplex.{v_1, u_1, 0} C ℤ) x y) (K.total (up ℤ)))).hom.f
        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 : HomologicalComplex₂.{v_1, u_1, 0, 0} C (up ℤ) (up ℤ)
x y : ℤ
inst_2 : K.HasTotal (up ℤ)
n n₁ n₂ : ℤ
h : n₁ + n₂ = n
w :
  ((Functor.obj (shiftFunctor₂ C y) K).shiftFunctor₁XXIso n₁ x (n₁ + x) ⋯ n₂).hom ≫
      (Functor.obj (shiftFunctor₂ C y) K).ιTotal (up ℤ) (n₁ + x) n₂ (n + x) ⋯ ≫
        (CochainComplex.shiftFunctorObjXIso ((Functor.obj (shiftFunctor₂ C y) K).total (up ℤ)) x n (n + x) ⋯).inv ≫
          HomologicalComplex.Hom.f (Iso.hom (K.totalShift₂Iso y)) (n + x) =
    (x * y).negOnePow •
      (n₁ * y).negOnePow •
        ((NatTrans.app (Iso.hom (shiftFunctor₁₂CommIso C x y)) K).f n₁).f n₂ ≫
          (((Functor.obj (shiftFunctor₁ C x) K).shiftFunctor₂XXIso n₁ n₂ y (n₂ + y) ⋯).hom ≫
              (Functor.obj (shiftFunctor₁ C x) K).ιTotal (up ℤ) n₁ (n₂ + y) (n + y) ⋯ ≫
                (CochainComplex.shiftFunctorObjXIso ((Functor.obj (shiftFunctor₁ C x) K).total (up ℤ)) y n (n + y)
                    ⋯).inv) ≫
            HomologicalComplex.Hom.f (Iso.hom (K.totalShift₁Iso x)) (n + y) ≫
              HomologicalComplex.Hom.f
                (NatTrans.app (Iso.hom (shiftFunctorComm (CochainComplex.{v_1, u_1, 0} C ℤ) x y)) (K.total (up ℤ))) n
⊢ (Functor.obj (shiftFunctor₁ C x) (Functor.obj (shiftFunctor₂ C y) K)).ιTotal (up ℤ) n₁ n₂ n h ≫
      HomologicalComplex.Hom.f (Iso.hom ((Functor.obj (shiftFunctor₂ C y) K).totalShift₁Iso x)) n ≫
        HomologicalComplex.Hom.f (Iso.hom (K.totalShift₂Iso y)) (n + x) =
    (Functor.obj (shiftFunctor₁ C x) (Functor.obj (shiftFunctor₂ C y) K)).ιTotal (up ℤ) n₁ n₂ n h ≫
      HSMul.hSMul (β :=
        ((Functor.obj (shiftFunctor₁ C x) (Functor.obj (shiftFunctor₂ C y) K)).total (up ℤ)).X n ⟶
          (K.total (up ℤ)).X (n + x + y))
        (x * y).negOnePow
        (HomologicalComplex.Hom.f (total.map (NatTrans.app (Iso.hom (shiftFunctor₁₂CommIso C x y)) K) (up ℤ)) n ≫
          HomologicalComplex.Hom.f (Iso.hom ((Functor.obj (shiftFunctor₁ C x) K).totalShift₂Iso y)) n ≫
            HomologicalComplex.Hom.f (Iso.hom (K.totalShift₁Iso x)) (n + y) ≫
              HomologicalComplex.Hom.f
                (NatTrans.app (Iso.hom (shiftFunctorComm (CochainComplex.{v_1, u_1, 0} C ℤ) x y)) (K.total (up ℤ))) n)

Tactic:
rw [Linear.comp_units_smul, ι_totalShift₁Iso_hom_f_assoc _ x n₁ n₂ n h _ rfl _ rfl,
    ιTotal_map_assoc, ι_totalShift₂Iso_hom_f_assoc _ y n₁ n₂ n h _ rfl _ rfl,
    Linear.units_smul_comp, Linear.comp_units_smul]

Premises used: HomologicalComplex₂.ι_totalShift₁Iso_hom_f_assoc, CategoryTheory.Linear.units_smul_comp, CategoryTheory.Linear.comp_units_smul, HomologicalComplex₂.ι_totalShift₂Iso_hom_f_assoc, rfl, HomologicalComplex₂.ιTotal_map_assoc
-- 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 y : ℤ
inst_2 : K.HasTotal (up ℤ)
n n₁ n₂ : ℤ
h : n₁ + n₂ = n
w :
  𝟙 ((K.X (n₁ + x)).X (n₂ + y)) ≫
      (Functor.obj (shiftFunctor₂ C y) K).ιTotal (up ℤ) (n₁ + x) n₂ (n + x) ⋯ ≫
        𝟙 (((Functor.obj (shiftFunctor₂ C y) K).total (up ℤ)).X (n + x)) ≫
          HomologicalComplex.Hom.f (Iso.hom (K.totalShift₂Iso y)) (n + x) =
    (x * y).negOnePow •
      (n₁ * y).negOnePow •
        𝟙 ((K.X (n₁ + x)).X (n₂ + y)) ≫
          (𝟙 ((K.X (n₁ + x)).X (n₂ + y)) ≫
              (Functor.obj (shiftFunctor₁ C x) K).ιTotal (up ℤ) n₁ (n₂ + y) (n + y) ⋯ ≫
                𝟙 (((Functor.obj (shiftFunctor₁ C x) K).total (up ℤ)).X (n + y))) ≫
            HomologicalComplex.Hom.f (Iso.hom (K.totalShift₁Iso x)) (n + y) ≫
              HomologicalComplex.Hom.f
                (NatTrans.app (Iso.hom (shiftFunctorComm (CochainComplex.{v_1, u_1, 0} C ℤ) x y)) (K.total (up ℤ))) n
⊢ ((Functor.obj (shiftFunctor₂ C y) K).shiftFunctor₁XXIso n₁ x (n₁ + x) ⋯ n₂).hom ≫
      (Functor.obj (shiftFunctor₂ C y) K).ιTotal (up ℤ) (n₁ + x) n₂ (n + x) ⋯ ≫
        (CochainComplex.shiftFunctorObjXIso ((Functor.obj (shiftFunctor₂ C y) K).total (up ℤ)) x n (n + x) ⋯).inv ≫
          HomologicalComplex.Hom.f (Iso.hom (K.totalShift₂Iso y)) (n + x) =
    (x * y).negOnePow •
      (n₁ * y).negOnePow •
        ((NatTrans.app (Iso.hom (shiftFunctor₁₂CommIso C x y)) K).f n₁).f n₂ ≫
          (((Functor.obj (shiftFunctor₁ C x) K).shiftFunctor₂XXIso n₁ n₂ y (n₂ + y) ⋯).hom ≫
              (Functor.obj (shiftFunctor₁ C x) K).ιTotal (up ℤ) n₁ (n₂ + y) (n + y) ⋯ ≫
                (CochainComplex.shiftFunctorObjXIso ((Functor.obj (shiftFunctor₁ C x) K).total (up ℤ)) y n (n + y)
                    ⋯).inv) ≫
            HomologicalComplex.Hom.f (Iso.hom (K.totalShift₁Iso x)) (n + y) ≫
              HomologicalComplex.Hom.f
                (NatTrans.app (Iso.hom (shiftFunctorComm (CochainComplex.{v_1, u_1, 0} C ℤ) x y)) (K.total (up ℤ))) n

Tactic:
dsimp [shiftFunctor₁₂CommIso]

Premises used: HomologicalComplex₂.shiftFunctor₁₂CommIso
-- 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 y : ℤ
inst_2 : K.HasTotal (up ℤ)
n n₁ n₂ : ℤ
h : n₁ + n₂ = n
⊢ n₁ + x + n₂ = n + 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 y : ℤ
inst_2 : K.HasTotal (up ℤ)
n n₁ n₂ : ℤ
h : n₁ + n₂ = n
w :
  (n₁ * y + x * y).negOnePow •
      Iso.hom (K.shiftFunctor₂XXIso (n₁ + x) n₂ y (n₂ + y) ⋯) ≫
        K.ιTotal (up ℤ) (n₁ + x) (n₂ + y) (n + x + y) ⋯ ≫
          Iso.inv (CochainComplex.shiftFunctorObjXIso (K.total (up ℤ)) y (n + x) (n + x + y) ⋯) =
    (n₁ * y + x * y).negOnePow •
      (Functor.obj (shiftFunctor₁ C x) K).ιTotal (up ℤ) n₁ (n₂ + y) (n + y) ⋯ ≫
        HomologicalComplex.Hom.f (Iso.hom (K.totalShift₁Iso x)) (n + y) ≫
          HomologicalComplex.Hom.f
            (NatTrans.app (Iso.hom (shiftFunctorComm (CochainComplex.{v_1, u_1, 0} C ℤ) x y)) (K.total (up ℤ))) n
⊢ 𝟙 ((K.X (n₁ + x)).X (n₂ + y)) ≫
      (Functor.obj (shiftFunctor₂ C y) K).ιTotal (up ℤ) (n₁ + x) n₂ (n + x) ⋯ ≫
        𝟙 (((Functor.obj (shiftFunctor₂ C y) K).total (up ℤ)).X (n + x)) ≫
          HomologicalComplex.Hom.f (Iso.hom (K.totalShift₂Iso y)) (n + x) =
    (x * y).negOnePow •
      (n₁ * y).negOnePow •
        𝟙 ((K.X (n₁ + x)).X (n₂ + y)) ≫
          (𝟙 ((K.X (n₁ + x)).X (n₂ + y)) ≫
              (Functor.obj (shiftFunctor₁ C x) K).ιTotal (up ℤ) n₁ (n₂ + y) (n + y) ⋯ ≫
                𝟙 (((Functor.obj (shiftFunctor₁ C x) K).total (up ℤ)).X (n + y))) ≫
            HomologicalComplex.Hom.f (Iso.hom (K.totalShift₁Iso x)) (n + y) ≫
              HomologicalComplex.Hom.f
                (NatTrans.app (Iso.hom (shiftFunctorComm (CochainComplex.{v_1, u_1, 0} C ℤ) x y)) (K.total (up ℤ))) n

Tactic:
rw [id_comp, id_comp, id_comp, id_comp, comp_id,
    ι_totalShift₂Iso_hom_f _ y (n₁ + x) n₂ (n + x) (by lia) _ rfl _ rfl, smul_smul,
    ← Int.negOnePow_add, add_mul, add_comm (x * y)]

Premises used: add_mul, HMul.hMul, smul_smul, Int.negOnePow_add, CategoryTheory.Category.comp_id, add_comm, HAdd.hAdd, HomologicalComplex₂.ι_totalShift₂Iso_hom_f, rfl, 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 : HomologicalComplex₂.{v_1, u_1, 0, 0} C (up ℤ) (up ℤ)
x y : ℤ
inst_2 : K.HasTotal (up ℤ)
n n₁ n₂ : ℤ
h : n₁ + n₂ = n
w :
  (n₁ * y + x * y).negOnePow •
      𝟙 ((K.X (n₁ + x)).X (n₂ + y)) ≫
        K.ιTotal (up ℤ) (n₁ + x) (n₂ + y) (n + x + y) ⋯ ≫ 𝟙 ((K.total (up ℤ)).X (n + x + y)) =
    (n₁ * y + x * y).negOnePow •
      (Functor.obj (shiftFunctor₁ C x) K).ιTotal (up ℤ) n₁ (n₂ + y) (n + y) ⋯ ≫
        HomologicalComplex.Hom.f (Iso.hom (K.totalShift₁Iso x)) (n + y) ≫
          HomologicalComplex.Hom.f
            (NatTrans.app (Iso.hom (shiftFunctorComm (CochainComplex.{v_1, u_1, 0} C ℤ) x y)) (K.total (up ℤ))) n
⊢ (n₁ * y + x * y).negOnePow •
      Iso.hom (K.shiftFunctor₂XXIso (n₁ + x) n₂ y (n₂ + y) ⋯) ≫
        K.ιTotal (up ℤ) (n₁ + x) (n₂ + y) (n + x + y) ⋯ ≫
          Iso.inv (CochainComplex.shiftFunctorObjXIso (K.total (up ℤ)) y (n + x) (n + x + y) ⋯) =
    (n₁ * y + x * y).negOnePow •
      (Functor.obj (shiftFunctor₁ C x) K).ιTotal (up ℤ) n₁ (n₂ + y) (n + y) ⋯ ≫
        HomologicalComplex.Hom.f (Iso.hom (K.totalShift₁Iso x)) (n + y) ≫
          HomologicalComplex.Hom.f
            (NatTrans.app (Iso.hom (shiftFunctorComm (CochainComplex.{v_1, u_1, 0} C ℤ) x y)) (K.total (up ℤ))) 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 ℤ)
x y : ℤ
inst_2 : K.HasTotal (up ℤ)
n n₁ n₂ : ℤ
h : n₁ + n₂ = n
⊢ n₁ + (n₂ + 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 : HomologicalComplex₂.{v_1, u_1, 0, 0} C (up ℤ) (up ℤ)
x y : ℤ
inst_2 : K.HasTotal (up ℤ)
n n₁ n₂ : ℤ
h : n₁ + n₂ = n
⊢ n + x + y = n + y + 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 y : ℤ
inst_2 : K.HasTotal (up ℤ)
n n₁ n₂ : ℤ
h : n₁ + n₂ = n
w :
  HSMul.hSMul (β := (K.X (n₁ + x)).X (n₂ + y) ⟶ (K.total (up ℤ)).X (n + x + y)) (n₁ * y + x * y).negOnePow
      (K.ιTotal (up ℤ) (n₁ + x) (n₂ + y) (n + x + y) ⋯) =
    HSMul.hSMul (β := (K.X (n₁ + x)).X (n₂ + y) ⟶ (K.total (up ℤ)).X (n + x + y)) (n₁ * y + x * y).negOnePow
      (Iso.hom (K.shiftFunctor₁XXIso n₁ x (n₁ + x) ⋯ (n₂ + y)) ≫
        K.ιTotal (up ℤ) (n₁ + x) (n₂ + y) (n + x + y) ⋯ ≫
          (CochainComplex.shiftFunctorObjXIso (K.total (up ℤ)) x (n + y) (n + x + y) ⋯).inv ≫
            Iso.hom ((K.total (up ℤ)).XIsoOfEq ⋯))
⊢ (n₁ * y + x * y).negOnePow •
      𝟙 ((K.X (n₁ + x)).X (n₂ + y)) ≫
        K.ιTotal (up ℤ) (n₁ + x) (n₂ + y) (n + x + y) ⋯ ≫ 𝟙 ((K.total (up ℤ)).X (n + x + y)) =
    (n₁ * y + x * y).negOnePow •
      (Functor.obj (shiftFunctor₁ C x) K).ιTotal (up ℤ) n₁ (n₂ + y) (n + y) ⋯ ≫
        HomologicalComplex.Hom.f (Iso.hom (K.totalShift₁Iso x)) (n + y) ≫
          HomologicalComplex.Hom.f
            (NatTrans.app (Iso.hom (shiftFunctorComm (CochainComplex.{v_1, u_1, 0} C ℤ) x y)) (K.total (up ℤ))) n

Tactic:
rw [id_comp, comp_id,
    ι_totalShift₁Iso_hom_f_assoc _ x n₁ (n₂ + y) (n + y) (by lia) _ rfl (n + x + y) (by lia),
    CochainComplex.shiftFunctorComm_hom_app_f]

Premises used: HomologicalComplex₂.ι_totalShift₁Iso_hom_f_assoc, CategoryTheory.Category.comp_id, HAdd.hAdd, CochainComplex.shiftFunctorComm_hom_app_f, rfl, 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 : HomologicalComplex₂.{v_1, u_1, 0, 0} C (up ℤ) (up ℤ)
x y : ℤ
inst_2 : K.HasTotal (up ℤ)
n n₁ n₂ : ℤ
h : n₁ + n₂ = n
w :
  HSMul.hSMul (β := (K.X (n₁ + x)).X (n₂ + y) ⟶ (K.total (up ℤ)).X (n + x + y)) (n₁ * y + x * y).negOnePow
      (K.ιTotal (up ℤ) (n₁ + x) (n₂ + y) (n + x + y) ⋯) =
    HSMul.hSMul (β := (K.X (n₁ + x)).X (n₂ + y) ⟶ (K.total (up ℤ)).X (n + x + y)) (n₁ * y + x * y).negOnePow
      (𝟙 ((K.X (n₁ + x)).X (n₂ + y)) ≫
        K.ιTotal (up ℤ) (n₁ + x) (n₂ + y) (n + x + y) ⋯ ≫
          ((K.total (up ℤ)).XIsoOfEq ⋯).inv ≫ Iso.hom ((K.total (up ℤ)).XIsoOfEq ⋯))
⊢ HSMul.hSMul (β := (K.X (n₁ + x)).X (n₂ + y) ⟶ (K.total (up ℤ)).X (n + x + y)) (n₁ * y + x * y).negOnePow
      (K.ιTotal (up ℤ) (n₁ + x) (n₂ + y) (n + x + y) ⋯) =
    HSMul.hSMul (β := (K.X (n₁ + x)).X (n₂ + y) ⟶ (K.total (up ℤ)).X (n + x + y)) (n₁ * y + x * y).negOnePow
      (Iso.hom (K.shiftFunctor₁XXIso n₁ x (n₁ + x) ⋯ (n₂ + y)) ≫
        K.ιTotal (up ℤ) (n₁ + x) (n₂ + y) (n + x + y) ⋯ ≫
          (CochainComplex.shiftFunctorObjXIso (K.total (up ℤ)) x (n + y) (n + x + y) ⋯).inv ≫
            Iso.hom ((K.total (up ℤ)).XIsoOfEq ⋯))

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 ℤ)
x y : ℤ
inst_2 : K.HasTotal (up ℤ)
n n₁ n₂ : ℤ
h : n₁ + n₂ = n
w :
  HSMul.hSMul (β := (K.X (n₁ + x)).X (n₂ + y) ⟶ (K.total (up ℤ)).X (n + x + y)) (n₁ * y + x * y).negOnePow
      (K.ιTotal (up ℤ) (n₁ + x) (n₂ + y) (n + x + y) ⋯) =
    (n₁ * y + x * y).negOnePow •
      𝟙 ((K.X (n₁ + x)).X (n₂ + y)) ≫
        K.ιTotal (up ℤ) (n₁ + x) (n₂ + y) (n + x + y) ⋯ ≫ 𝟙 ((K.total (up ℤ)).X (n + x + y))
w₁ :
  HSMul.hSMul (β := (K.X (n₁ + x)).X (n₂ + y) ⟶ (K.total (up ℤ)).X (n + x + y)) (n₁ * y + x * y).negOnePow
      (K.ιTotal (up ℤ) (n₁ + x) (n₂ + y) (n + x + y) ⋯) =
    HSMul.hSMul (β := (K.X (n₁ + x)).X (n₂ + y) ⟶ (K.total (up ℤ)).X (n + x + y)) (n₁ * y + x * y).negOnePow
      (𝟙 ((K.X (n₁ + x)).X (n₂ + y)) ≫ K.ιTotal (up ℤ) (n₁ + x) (n₂ + y) (n + x + y) ⋯)
w₂ w₃ :
  HSMul.hSMul (β := (K.X (n₁ + x)).X (n₂ + y) ⟶ (K.total (up ℤ)).X (n + x + y)) (n₁ * y + x * y).negOnePow
      (K.ιTotal (up ℤ) (n₁ + x) (n₂ + y) (n + x + y) ⋯) =
    HSMul.hSMul (β := (K.X (n₁ + x)).X (n₂ + y) ⟶ (K.total (up ℤ)).X (n + x + y)) (n₁ * y + x * y).negOnePow
      (K.ιTotal (up ℤ) (n₁ + x) (n₂ + y) (n + x + y) ⋯)
⊢ HSMul.hSMul (β := (K.X (n₁ + x)).X (n₂ + y) ⟶ (K.total (up ℤ)).X (n + x + y)) (n₁ * y + x * y).negOnePow
      (K.ιTotal (up ℤ) (n₁ + x) (n₂ + y) (n + x + y) ⋯) =
    HSMul.hSMul (β := (K.X (n₁ + x)).X (n₂ + y) ⟶ (K.total (up ℤ)).X (n + x + y)) (n₁ * y + x * y).negOnePow
      (𝟙 ((K.X (n₁ + x)).X (n₂ + y)) ≫
        K.ιTotal (up ℤ) (n₁ + x) (n₂ + y) (n + x + y) ⋯ ≫
          ((K.total (up ℤ)).XIsoOfEq ⋯).inv ≫ Iso.hom ((K.total (up ℤ)).XIsoOfEq ⋯))

Tactic:
rw [Iso.inv_hom_id, comp_id, id_comp]

Premises used: CategoryTheory.Iso.inv_hom_id, 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 : HomologicalComplex₂.{v_1, u_1, 0, 0} C (up ℤ) (up ℤ)
x y : ℤ
inst_2 : K.HasTotal (up ℤ)
⊢ Iso.hom ((Functor.obj (shiftFunctor₂ C y) K).totalShift₁Iso x) ≫
      CategoryTheory.Functor.map (shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) x)
        (Iso.hom (K.totalShift₂Iso y)) =
    HSMul.hSMul (β :=
      (Functor.obj (shiftFunctor₂ C y ⋙ shiftFunctor₁ C x) K).total (up ℤ) ⟶
        Functor.obj
          (shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) y ⋙ shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) x)
          (K.total (up ℤ)))
      (x * y).negOnePow
      (total.map (NatTrans.app (Iso.hom (shiftFunctor₁₂CommIso C x y)) K) (up ℤ) ≫
        Iso.hom ((Functor.obj (shiftFunctor₁ C x) K).totalShift₂Iso y) ≫
          CategoryTheory.Functor.map (shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) y)
              (Iso.hom (K.totalShift₁Iso x)) ≫
            NatTrans.app (Iso.hom (shiftFunctorComm (CochainComplex.{v_1, u_1, 0} C ℤ) x y)) (K.total (up ℤ)))

Tactic:
congr_arg Iso.hom (totalShift₁Iso_trans_totalShift₂Iso K x y)

Premises used: congr_arg, HomologicalComplex₂.totalShift₁Iso_trans_totalShift₂Iso, CategoryTheory.Iso.hom
-- Module: Mathlib.Algebra.Homology.TotalComplexSymmetry
Goal:
C : Type u_1
I₁ : Type u_2
I₂ : Type u_3
J : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂.{v_1, u_1, u_2, u_3} C c₁ c₂
c : ComplexShape J
inst_2 : TotalComplexShape c₁ c₂ c
inst_3 : TotalComplexShape c₂ c₁ c
inst_4 : TotalComplexShapeSymmetry c₁ c₂ c
inst_5 : K.HasTotal c
⊢ K.flip.HasTotal c

Tactic:
fun j =>
  hasCoproduct_of_equiv_of_iso (K.toGradedObject.mapObjFun (ComplexShape.π c₁ c₂ c) j) _
    (ComplexShape.symmetryEquiv c₁ c₂ c j) (fun _ => Iso.refl _)

Premises used: CategoryTheory.Limits.hasCoproduct_of_equiv_of_iso, HomologicalComplex₂.toGradedObject, ComplexShape.symmetryEquiv, CategoryTheory.GradedObject.mapObjFun, CategoryTheory.Iso.refl, HomologicalComplex₂.flip, ComplexShape.π
-- Module: Mathlib.Algebra.Homology.TotalComplexSymmetry
Goal:
C : Type u_1
I₁ : Type u_2
I₂ : Type u_3
J : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂.{v_1, u_1, u_2, u_3} C c₁ c₂
c : ComplexShape J
inst_2 : TotalComplexShape c₁ c₂ c
inst_3 : TotalComplexShape c₂ c₁ c
inst_4 : TotalComplexShapeSymmetry c₁ c₂ c
mp : K.flip.HasTotal c → K.HasTotal c
mpr : K.HasTotal c → K.flip.HasTotal c
⊢ K.flip.HasTotal c ↔ K.HasTotal c

Tactic:
constructor
-- Module: Mathlib.Algebra.Homology.TotalComplexSymmetry
Goal:
C : Type u_1
I₁ : Type u_2
I₂ : Type u_3
J : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂.{v_1, u_1, u_2, u_3} C c₁ c₂
c : ComplexShape J
inst_2 : TotalComplexShape c₁ c₂ c
inst_3 : TotalComplexShape c₂ c₁ c
inst_4 : TotalComplexShapeSymmetry c₁ c₂ c
h : K.flip.HasTotal c
mp : K.flip.flip.HasTotal c
⊢ K.HasTotal c

Tactic:
change K.flip.flip.HasTotal c

Premises used: HomologicalComplex₂.HasTotal, HomologicalComplex₂.flip
-- Module: Mathlib.Algebra.Homology.TotalComplexSymmetry
Goal:
C : Type u_1
I₁ : Type u_2
I₂ : Type u_3
J : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂.{v_1, u_1, u_2, u_3} C c₁ c₂
c : ComplexShape J
inst_2 : TotalComplexShape c₁ c₂ c
inst_3 : TotalComplexShape c₂ c₁ c
inst_4 : TotalComplexShapeSymmetry c₁ c₂ c
h : K.flip.HasTotal c
mp : ∀ (this : TotalComplexShapeSymmetry c₂ c₁ c), K.flip.flip.HasTotal c
⊢ K.flip.flip.HasTotal c

Tactic:
have := TotalComplexShapeSymmetry.symmetry c₁ c₂ c