awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Shift.CommShift
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
D₁ : Type u_4
D₂ : Type u_5
D₃ : Type u_6
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} C₃
inst_3 : Category.{v_4, u_4} D₁
inst_4 : Category.{v_5, u_5} D₂
inst_5 : Category.{v_6, u_6} D₃
F₁₂ : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
F₂₃ : Functor.{v_2, v_3, u_2, u_3} C₂ C₃
F₁₃ : Functor.{v_1, v_3, u_1, u_3} C₁ C₃
α : F₁₃ ⟶ F₁₂ ⋙ F₂₃
G₁₂ : Functor.{v_4, v_5, u_4, u_5} D₁ D₂
G₂₃ : Functor.{v_5, v_6, u_5, u_6} D₂ D₃
G₁₃ : Functor.{v_4, v_6, u_4, u_6} D₁ D₃
β : G₁₂ ⋙ G₂₃ ⟶ G₁₃
L₁ : Functor.{v_1, v_4, u_1, u_4} C₁ D₁
L₂ : Functor.{v_2, v_5, u_2, u_5} C₂ D₂
L₃ : Functor.{v_3, v_6, u_3, u_6} C₃ D₃
e₁₂ : F₁₂ ⋙ L₂ ⟶ L₁ ⋙ G₁₂
e₂₃ : F₂₃ ⋙ L₃ ⟶ L₂ ⋙ G₂₃
e₁₃ : F₁₃ ⋙ L₃ ⟶ L₁ ⋙ G₁₃
A : Type u_7
inst_6 : AddMonoid A
inst_7 : HasShift.{v_1, u_1, u_7} C₁ A
inst_8 : HasShift.{v_2, u_2, u_7} C₂ A
inst_9 : HasShift.{v_3, u_3, u_7} C₃ A
inst_10 : HasShift.{v_4, u_4, u_7} D₁ A
inst_11 : HasShift.{v_5, u_5, u_7} D₂ A
inst_12 : HasShift.{v_6, u_6, u_7} D₃ A
inst_13 : F₁₂.CommShift A
inst_14 : F₂₃.CommShift A
inst_15 : F₁₃.CommShift A
inst_16 : CommShift α A
inst_17 : G₁₂.CommShift A
inst_18 : G₂₃.CommShift A
inst_19 : G₁₃.CommShift A
inst_20 : CommShift β A
inst_21 : L₁.CommShift A
inst_22 : L₂.CommShift A
inst_23 : L₃.CommShift A
inst_24 : CommShift e₁₂ A
inst_25 : CommShift e₂₃ A
h₁₃ :
  e₁₃ =
    Functor.whiskerRight α L₃ ≫
      (F₁₂.associator F₂₃ L₃).hom ≫
        F₁₂.whiskerLeft e₂₃ ≫
          (F₁₂.associator L₂ G₂₃).inv ≫ Functor.whiskerRight e₁₂ G₂₃ ≫ (L₁.associator G₁₂ G₂₃).hom ≫ L₁.whiskerLeft β
subst :
  CommShift
    (Functor.whiskerRight α L₃ ≫
      (F₁₂.associator F₂₃ L₃).hom ≫
        F₁₂.whiskerLeft e₂₃ ≫
          (F₁₂.associator L₂ G₂₃).inv ≫ Functor.whiskerRight e₁₂ G₂₃ ≫ (L₁.associator G₁₂ G₂₃).hom ≫ L₁.whiskerLeft β)
    A
⊢ CommShift e₁₃ A

Tactic:
subst h₁₃
-- Module: Mathlib.CategoryTheory.Shift.CommShift
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
D₁ : Type u_4
D₂ : Type u_5
D₃ : Type u_6
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} C₃
inst_3 : Category.{v_4, u_4} D₁
inst_4 : Category.{v_5, u_5} D₂
inst_5 : Category.{v_6, u_6} D₃
F₁₂ : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
F₂₃ : Functor.{v_2, v_3, u_2, u_3} C₂ C₃
F₁₃ : Functor.{v_1, v_3, u_1, u_3} C₁ C₃
α : F₁₃ ⟶ F₁₂ ⋙ F₂₃
G₁₂ : Functor.{v_4, v_5, u_4, u_5} D₁ D₂
G₂₃ : Functor.{v_5, v_6, u_5, u_6} D₂ D₃
G₁₃ : Functor.{v_4, v_6, u_4, u_6} D₁ D₃
β : G₁₂ ⋙ G₂₃ ⟶ G₁₃
L₁ : Functor.{v_1, v_4, u_1, u_4} C₁ D₁
L₂ : Functor.{v_2, v_5, u_2, u_5} C₂ D₂
L₃ : Functor.{v_3, v_6, u_3, u_6} C₃ D₃
e₁₂ : F₁₂ ⋙ L₂ ⟶ L₁ ⋙ G₁₂
e₂₃ : F₂₃ ⋙ L₃ ⟶ L₂ ⋙ G₂₃
A : Type u_7
inst_6 : AddMonoid A
inst_7 : HasShift.{v_1, u_1, u_7} C₁ A
inst_8 : HasShift.{v_2, u_2, u_7} C₂ A
inst_9 : HasShift.{v_3, u_3, u_7} C₃ A
inst_10 : HasShift.{v_4, u_4, u_7} D₁ A
inst_11 : HasShift.{v_5, u_5, u_7} D₂ A
inst_12 : HasShift.{v_6, u_6, u_7} D₃ A
inst_13 : F₁₂.CommShift A
inst_14 : F₂₃.CommShift A
inst_15 : F₁₃.CommShift A
inst_16 : CommShift α A
inst_17 : G₁₂.CommShift A
inst_18 : G₂₃.CommShift A
inst_19 : G₁₃.CommShift A
inst_20 : CommShift β A
inst_21 : L₁.CommShift A
inst_22 : L₂.CommShift A
inst_23 : L₃.CommShift A
inst_24 : CommShift e₁₂ A
inst_25 : CommShift e₂₃ A
⊢ CommShift
    (Functor.whiskerRight α L₃ ≫
      (F₁₂.associator F₂₃ L₃).hom ≫
        F₁₂.whiskerLeft e₂₃ ≫
          (F₁₂.associator L₂ G₂₃).inv ≫ Functor.whiskerRight e₁₂ G₂₃ ≫ (L₁.associator G₁₂ G₂₃).hom ≫ L₁.whiskerLeft β)
    A

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Shift.CommShiftTwo
Goal:
C₁ : Type u_1
C₁' : Type u_2
C₂ : Type u_3
C₂' : Type u_4
D : Type u_5
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₁'
inst_2 : Category.{v_3, u_3} C₂
inst_3 : Category.{v_4, u_4} C₂'
inst_4 : Category.{v_5, u_5} D
inst_5 : Preadditive.{v_5, u_5} D
inst_6 : HasShift.{v_5, u_5, 0} D ℤ
inst_7 : ∀ (n : ℤ), Functor.Additive.{v_5, u_5, v_5, u_5} (shiftFunctor D n)
x x_1 x_2 : ℤ × ℤ
dsimp :
  HPow.hPow (α :=
        (CatCenter.{v_5, u_5} (PullbackShift.{v_5, u_5, 0, 0} D (AddMonoidHom.fst ℤ ℤ + AddMonoidHom.snd ℤ ℤ)))ˣ) (-1)
        ((x.1 + x_1.1) * x_2.2) *
      HPow.hPow (α :=
        (CatCenter.{v_5, u_5} (PullbackShift.{v_5, u_5, 0, 0} D (AddMonoidHom.fst ℤ ℤ + AddMonoidHom.snd ℤ ℤ)))ˣ) (-1)
        (x.1 * x_1.2) =
    HPow.hPow (α :=
        (CatCenter.{v_5, u_5} (PullbackShift.{v_5, u_5, 0, 0} D (AddMonoidHom.fst ℤ ℤ + AddMonoidHom.snd ℤ ℤ)))ˣ) (-1)
        (x.1 * (x_1.2 + x_2.2)) *
      HPow.hPow (α :=
        (CatCenter.{v_5, u_5} (PullbackShift.{v_5, u_5, 0, 0} D (AddMonoidHom.fst ℤ ℤ + AddMonoidHom.snd ℤ ℤ)))ˣ) (-1)
        (x_1.1 * x_2.2)
⊢ HPow.hPow (α :=
        (CatCenter.{v_5, u_5} (PullbackShift.{v_5, u_5, 0, 0} D (AddMonoidHom.fst ℤ ℤ + AddMonoidHom.snd ℤ ℤ)))ˣ) (-1)
        ((x + x_1).1 * x_2.2) *
      HPow.hPow (α :=
        (CatCenter.{v_5, u_5} (PullbackShift.{v_5, u_5, 0, 0} D (AddMonoidHom.fst ℤ ℤ + AddMonoidHom.snd ℤ ℤ)))ˣ) (-1)
        (x.1 * x_1.2) =
    HPow.hPow (α :=
        (CatCenter.{v_5, u_5} (PullbackShift.{v_5, u_5, 0, 0} D (AddMonoidHom.fst ℤ ℤ + AddMonoidHom.snd ℤ ℤ)))ˣ) (-1)
        (x.1 * (x_1 + x_2).2) *
      HPow.hPow (α :=
        (CatCenter.{v_5, u_5} (PullbackShift.{v_5, u_5, 0, 0} D (AddMonoidHom.fst ℤ ℤ + AddMonoidHom.snd ℤ ℤ)))ˣ) (-1)
        (x_1.1 * x_2.2)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Shift.CommShiftTwo
Goal:
C₁ : Type u_1
C₁' : Type u_2
C₂ : Type u_3
C₂' : Type u_4
D : Type u_5
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₁'
inst_2 : Category.{v_3, u_3} C₂
inst_3 : Category.{v_4, u_4} C₂'
inst_4 : Category.{v_5, u_5} D
inst_5 : Preadditive.{v_5, u_5} D
inst_6 : HasShift.{v_5, u_5, 0} D ℤ
inst_7 : ∀ (n : ℤ), Functor.Additive.{v_5, u_5, v_5, u_5} (shiftFunctor D n)
x x_1 x_2 : ℤ × ℤ
rw :
  HPow.hPow (α :=
      (CatCenter.{v_5, u_5} (PullbackShift.{v_5, u_5, 0, 0} D (AddMonoidHom.fst ℤ ℤ + AddMonoidHom.snd ℤ ℤ)))ˣ) (-1)
      ((x.1 + x_1.1) * x_2.2 + x.1 * x_1.2) =
    HPow.hPow (α :=
      (CatCenter.{v_5, u_5} (PullbackShift.{v_5, u_5, 0, 0} D (AddMonoidHom.fst ℤ ℤ + AddMonoidHom.snd ℤ ℤ)))ˣ) (-1)
      (x.1 * (x_1.2 + x_2.2) + x_1.1 * x_2.2)
⊢ HPow.hPow (α :=
        (CatCenter.{v_5, u_5} (PullbackShift.{v_5, u_5, 0, 0} D (AddMonoidHom.fst ℤ ℤ + AddMonoidHom.snd ℤ ℤ)))ˣ) (-1)
        ((x.1 + x_1.1) * x_2.2) *
      HPow.hPow (α :=
        (CatCenter.{v_5, u_5} (PullbackShift.{v_5, u_5, 0, 0} D (AddMonoidHom.fst ℤ ℤ + AddMonoidHom.snd ℤ ℤ)))ˣ) (-1)
        (x.1 * x_1.2) =
    HPow.hPow (α :=
        (CatCenter.{v_5, u_5} (PullbackShift.{v_5, u_5, 0, 0} D (AddMonoidHom.fst ℤ ℤ + AddMonoidHom.snd ℤ ℤ)))ˣ) (-1)
        (x.1 * (x_1.2 + x_2.2)) *
      HPow.hPow (α :=
        (CatCenter.{v_5, u_5} (PullbackShift.{v_5, u_5, 0, 0} D (AddMonoidHom.fst ℤ ℤ + AddMonoidHom.snd ℤ ℤ)))ˣ) (-1)
        (x_1.1 * x_2.2)

Tactic:
rw [← zpow_add, ← zpow_add]

Premises used: zpow_add
-- Module: Mathlib.CategoryTheory.Shift.CommShiftTwo
Goal:
C₁ : Type u_1
C₁' : Type u_2
C₂ : Type u_3
C₂' : Type u_4
D : Type u_5
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₁'
inst_2 : Category.{v_3, u_3} C₂
inst_3 : Category.{v_4, u_4} C₂'
inst_4 : Category.{v_5, u_5} D
inst_5 : Preadditive.{v_5, u_5} D
inst_6 : HasShift.{v_5, u_5, 0} D ℤ
inst_7 : ∀ (n : ℤ), Functor.Additive.{v_5, u_5, v_5, u_5} (shiftFunctor D n)
x x_1 x_2 : ℤ × ℤ
⊢ HPow.hPow (α :=
      (CatCenter.{v_5, u_5} (PullbackShift.{v_5, u_5, 0, 0} D (AddMonoidHom.fst ℤ ℤ + AddMonoidHom.snd ℤ ℤ)))ˣ) (-1)
      ((x.1 + x_1.1) * x_2.2 + x.1 * x_1.2) =
    HPow.hPow (α :=
      (CatCenter.{v_5, u_5} (PullbackShift.{v_5, u_5, 0, 0} D (AddMonoidHom.fst ℤ ℤ + AddMonoidHom.snd ℤ ℤ)))ˣ) (-1)
      (x.1 * (x_1.2 + x_2.2) + x_1.1 * x_2.2)

Tactic:
lia
-- Module: Mathlib.CategoryTheory.Shift.CommShiftTwo
Goal:
C₁ : Type u_1
C₁' : Type u_2
C₂ : Type u_3
C₂' : Type u_4
D : Type u_5
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₁'
inst_2 : Category.{v_3, u_3} C₂
inst_3 : Category.{v_4, u_4} C₂'
inst_4 : Category.{v_5, u_5} D
M : Type u_6
inst_5 : AddCommMonoid M
inst_6 : HasShift.{v_1, u_1, u_6} C₁ M
inst_7 : HasShift.{v_2, u_2, u_6} C₁' M
inst_8 : HasShift.{v_3, u_3, u_6} C₂ M
inst_9 : HasShift.{v_5, u_5, u_6} D M
F : Functor.{v_2, v_1, u_2, u_1} C₁' C₁
inst_10 : F.CommShift M
G : C₁ ⥤ Functor.{v_3, v_5, u_3, u_5} C₂ D
h : CommShift₂Setup.{v_5, u_5, u_6} D M
inst_11 : G.CommShift₂ h
X₁' Y₁' : C₁'
f : X₁' ⟶ Y₁'
dsimp : NatTrans.CommShift (G.map (F.map f)) M
⊢ NatTrans.CommShift ((F ⋙ G).map f) M

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Shift.CommShiftTwo
Goal:
C₁ : Type u_1
C₁' : Type u_2
C₂ : Type u_3
C₂' : Type u_4
D : Type u_5
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₁'
inst_2 : Category.{v_3, u_3} C₂
inst_3 : Category.{v_4, u_4} C₂'
inst_4 : Category.{v_5, u_5} D
M : Type u_6
inst_5 : AddCommMonoid M
inst_6 : HasShift.{v_1, u_1, u_6} C₁ M
inst_7 : HasShift.{v_2, u_2, u_6} C₁' M
inst_8 : HasShift.{v_3, u_3, u_6} C₂ M
inst_9 : HasShift.{v_5, u_5, u_6} D M
F : Functor.{v_2, v_1, u_2, u_1} C₁' C₁
inst_10 : F.CommShift M
G : C₁ ⥤ Functor.{v_3, v_5, u_3, u_5} C₂ D
h : CommShift₂Setup.{v_5, u_5, u_6} D M
inst_11 : G.CommShift₂ h
X₁' Y₁' : C₁'
f : X₁' ⟶ Y₁'
⊢ NatTrans.CommShift (G.map (F.map f)) M

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Shift.CommShiftTwo
Goal:
C₁ : Type u_1
C₁' : Type u_2
C₂ : Type u_3
C₂' : Type u_4
D : Type u_5
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₁'
inst_2 : Category.{v_3, u_3} C₂
inst_3 : Category.{v_4, u_4} C₂'
inst_4 : Category.{v_5, u_5} D
M : Type u_6
inst_5 : AddCommMonoid M
inst_6 : HasShift.{v_1, u_1, u_6} C₁ M
inst_7 : HasShift.{v_2, u_2, u_6} C₁' M
inst_8 : HasShift.{v_3, u_3, u_6} C₂ M
inst_9 : HasShift.{v_5, u_5, u_6} D M
F : Functor.{v_2, v_1, u_2, u_1} C₁' C₁
inst_10 : F.CommShift M
G : C₁ ⥤ Functor.{v_3, v_5, u_3, u_5} C₂ D
h : CommShift₂Setup.{v_5, u_5, u_6} D M
inst_11 : G.CommShift₂ h
X₁' : C₁'
X₂ : C₂
m n : M
⊢ Eq (α :=
    (shiftFunctor C₂ n ⋙ G.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C₁ m) (F.obj X₁'))).obj X₂ ⟶
      obj.{v_5, v_5, u_5, u_5} (shiftFunctor D n) ((G.flip.obj X₂ ⋙ shiftFunctor D m).obj (F.obj X₁')))
    (NatTrans.app (Iso.hom (commShiftIso (G.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C₁ m) (F.obj X₁'))) n)) X₂ ≫
      map (shiftFunctor D n) (NatTrans.app (Iso.hom (commShiftIso (G.flip.obj X₂) m)) (F.obj X₁')))
    (NatTrans.app (Iso.hom (commShiftIso (G.flip.obj (obj.{v_3, v_3, u_3, u_3} (shiftFunctor C₂ n) X₂)) m))
        (F.obj X₁') ≫
      map (shiftFunctor D m) (NatTrans.app (Iso.hom (commShiftIso (G.obj (F.obj X₁')) n)) X₂) ≫
        Iso.inv (shiftComm ((G.obj (F.obj X₁')).obj X₂) m n) ≫
          (↑(h.ε m n) : CatCenter D).app
            (obj.{v_5, v_5, u_5, u_5} (shiftFunctor D n)
              (obj.{v_5, v_5, u_5, u_5} (shiftFunctor D m) ((G.obj (F.obj X₁')).obj X₂))))

Tactic:
have := G.commShift₂_comm h (F.obj X₁') X₂ m n
-- Module: Mathlib.CategoryTheory.Shift.CommShiftTwo
Goal:
C₁ : Type u_1
C₁' : Type u_2
C₂ : Type u_3
C₂' : Type u_4
D : Type u_5
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₁'
inst_2 : Category.{v_3, u_3} C₂
inst_3 : Category.{v_4, u_4} C₂'
inst_4 : Category.{v_5, u_5} D
M : Type u_6
inst_5 : AddCommMonoid M
inst_6 : HasShift.{v_1, u_1, u_6} C₁ M
inst_7 : HasShift.{v_4, u_4, u_6} C₂' M
inst_8 : HasShift.{v_3, u_3, u_6} C₂ M
inst_9 : HasShift.{v_5, u_5, u_6} D M
F : Functor.{v_4, v_3, u_4, u_3} C₂' C₂
inst_10 : F.CommShift M
G : C₁ ⥤ Functor.{v_3, v_5, u_3, u_5} C₂ D
h : CommShift₂Setup.{v_5, u_5, u_6} D M
inst_11 : G.CommShift₂ h
X₁ Y₁ : C₁
f : X₁ ⟶ Y₁
⊢ NatTrans.CommShift (F.whiskerLeft (G.map f)) M

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Shift.CommShiftTwo
Goal:
C₁ : Type u_1
C₁' : Type u_2
C₂ : Type u_3
C₂' : Type u_4
D : Type u_5
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₁'
inst_2 : Category.{v_3, u_3} C₂
inst_3 : Category.{v_4, u_4} C₂'
inst_4 : Category.{v_5, u_5} D
M : Type u_6
inst_5 : AddCommMonoid M
inst_6 : HasShift.{v_1, u_1, u_6} C₁ M
inst_7 : HasShift.{v_4, u_4, u_6} C₂' M
inst_8 : HasShift.{v_3, u_3, u_6} C₂ M
inst_9 : HasShift.{v_5, u_5, u_6} D M
F : Functor.{v_4, v_3, u_4, u_3} C₂' C₂
inst_10 : F.CommShift M
G : C₁ ⥤ Functor.{v_3, v_5, u_3, u_5} C₂ D
h : CommShift₂Setup.{v_5, u_5, u_6} D M
inst_11 : G.CommShift₂ h
X₁ : C₁
X₂' : C₂'
m n : M
⊢ Eq (α :=
    (shiftFunctor C₂ n ⋙ G.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C₁ m) X₁)).obj (F.obj X₂') ⟶
      obj.{v_5, v_5, u_5, u_5} (shiftFunctor D n) ((G.flip.obj (F.obj X₂') ⋙ shiftFunctor D m).obj X₁))
    (NatTrans.app (Iso.hom (commShiftIso (G.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C₁ m) X₁)) n)) (F.obj X₂') ≫
      map (shiftFunctor D n) (NatTrans.app (Iso.hom (commShiftIso (G.flip.obj (F.obj X₂')) m)) X₁))
    (NatTrans.app (Iso.hom (commShiftIso (G.flip.obj (obj.{v_3, v_3, u_3, u_3} (shiftFunctor C₂ n) (F.obj X₂'))) m))
        X₁ ≫
      map (shiftFunctor D m) (NatTrans.app (Iso.hom (commShiftIso (G.obj X₁) n)) (F.obj X₂')) ≫
        Iso.inv (shiftComm ((G.obj X₁).obj (F.obj X₂')) m n) ≫
          (↑(h.ε m n) : CatCenter D).app
            (obj.{v_5, v_5, u_5, u_5} (shiftFunctor D n)
              (obj.{v_5, v_5, u_5, u_5} (shiftFunctor D m) ((G.obj X₁).obj (F.obj X₂')))))

Tactic:
have := G.commShift₂_comm h X₁ (F.obj X₂') m n
-- Module: Mathlib.CategoryTheory.Shift.CommShiftTwo
Goal:
C₁ : Type u_1
C₁' : Type u_2
C₂ : Type u_3
C₂' : Type u_4
D : Type u_5
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₁'
inst_2 : Category.{v_3, u_3} C₂
inst_3 : Category.{v_4, u_4} C₂'
inst_4 : Category.{v_5, u_5} D
M : Type u_6
inst_5 : AddCommMonoid M
inst_6 : HasShift.{v_1, u_1, u_6} C₁ M
inst_7 : HasShift.{v_4, u_4, u_6} C₂' M
inst_8 : HasShift.{v_3, u_3, u_6} C₂ M
inst_9 : HasShift.{v_5, u_5, u_6} D M
F : Functor.{v_4, v_3, u_4, u_3} C₂' C₂
inst_10 : F.CommShift M
G : C₁ ⥤ Functor.{v_3, v_5, u_3, u_5} C₂ D
h : CommShift₂Setup.{v_5, u_5, u_6} D M
inst_11 : G.CommShift₂ h
X₁ : C₁
X₂' : C₂'
m n : M
this :
  Eq (α :=
    (G.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C₁ m) X₁)).obj
        (obj.{v_3, v_3, u_3, u_3} (shiftFunctor C₂ n) (F.obj X₂')) ⟶
      obj.{v_5, v_5, u_5, u_5} (shiftFunctor D n)
        (obj.{v_5, v_5, u_5, u_5} (shiftFunctor D m) ((G.obj X₁).obj (F.obj X₂'))))
    (NatTrans.app (Iso.hom (commShiftIso (G.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C₁ m) X₁)) n)) (F.obj X₂') ≫
      map (shiftFunctor D n) (NatTrans.app (Iso.hom (commShiftIso (G.flip.obj (F.obj X₂')) m)) X₁))
    (CategoryStruct.comp (Y :=
      obj.{v_5, v_5, u_5, u_5} (shiftFunctor D m)
        ((G.obj X₁).obj (obj.{v_3, v_3, u_3, u_3} (shiftFunctor C₂ n) (F.obj X₂'))))
      (NatTrans.app (Iso.hom (commShiftIso (G.flip.obj (obj.{v_3, v_3, u_3, u_3} (shiftFunctor C₂ n) (F.obj X₂'))) m))
        X₁)
      (map (shiftFunctor D m) (NatTrans.app (Iso.hom (commShiftIso (G.obj X₁) n)) (F.obj X₂')) ≫
        NatTrans.app (Iso.inv (shiftFunctorComm D m n)) ((G.obj X₁).obj (F.obj X₂')) ≫
          (↑(h.ε m n) : CatCenter D).app
            (obj.{v_5, v_5, u_5, u_5} (shiftFunctor D n)
              (obj.{v_5, v_5, u_5, u_5} (shiftFunctor D m) ((G.obj X₁).obj (F.obj X₂'))))))
⊢ Eq (α :=
    (G.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C₁ m) X₁)).obj
        (F.obj (obj.{v_4, v_4, u_4, u_4} (shiftFunctor C₂' n) X₂')) ⟶
      obj.{v_5, v_5, u_5, u_5} (shiftFunctor D m)
        ((G.obj X₁).obj (obj.{v_3, v_3, u_3, u_3} (shiftFunctor C₂ n) (F.obj X₂'))))
    ((G.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C₁ m) X₁)).map (NatTrans.app (Iso.hom (commShiftIso F n)) X₂') ≫
      NatTrans.app (Iso.hom (commShiftIso (G.flip.obj (obj.{v_3, v_3, u_3, u_3} (shiftFunctor C₂ n) (F.obj X₂'))) m))
        X₁)
    (NatTrans.app
        (Iso.hom
          (commShiftIso
            ((G ⋙ obj (whiskeringLeft C₂' C₂ D) F).flip.obj (obj.{v_4, v_4, u_4, u_4} (shiftFunctor C₂' n) X₂')) m))
        X₁ ≫
      map (shiftFunctor D m) ((G.obj X₁).map (NatTrans.app (Iso.hom (commShiftIso F n)) X₂')))

Tactic:
(NatTrans.shift_app_comm (G.flip.map ((F.commShiftIso n).hom.app X₂')) m X₁).symm

Premises used: CategoryTheory.Functor.flip, CategoryTheory.Functor.map, Eq.symm, CategoryTheory.NatTrans.shift_app_comm, CategoryTheory.Functor.CommShift.commShiftIso, CategoryTheory.Iso.hom, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Shift.CommShiftTwo
Goal:
C₁ : Type u_1
C₁' : Type u_2
C₂ : Type u_3
C₂' : Type u_4
D : Type u_5
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₁'
inst_2 : Category.{v_3, u_3} C₂
inst_3 : Category.{v_4, u_4} C₂'
inst_4 : Category.{v_5, u_5} D
M : Type u_6
inst_5 : AddCommMonoid M
inst_6 : HasShift.{v_1, u_1, u_6} C₁ M
inst_7 : HasShift.{v_4, u_4, u_6} C₂' M
inst_8 : HasShift.{v_3, u_3, u_6} C₂ M
inst_9 : HasShift.{v_5, u_5, u_6} D M
F : Functor.{v_4, v_3, u_4, u_3} C₂' C₂
inst_10 : F.CommShift M
G : C₁ ⥤ Functor.{v_3, v_5, u_3, u_5} C₂ D
h : CommShift₂Setup.{v_5, u_5, u_6} D M
inst_11 : G.CommShift₂ h
X₁ : C₁
X₂' : C₂'
m n : M
this :
  Eq (α :=
    (G.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C₁ m) X₁)).obj
        (obj.{v_3, v_3, u_3, u_3} (shiftFunctor C₂ n) (F.obj X₂')) ⟶
      obj.{v_5, v_5, u_5, u_5} (shiftFunctor D n)
        (obj.{v_5, v_5, u_5, u_5} (shiftFunctor D m) ((G.obj X₁).obj (F.obj X₂'))))
    (NatTrans.app (Iso.hom (commShiftIso (G.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C₁ m) X₁)) n)) (F.obj X₂') ≫
      map (shiftFunctor D n) (NatTrans.app (Iso.hom (commShiftIso (G.flip.obj (F.obj X₂')) m)) X₁))
    (CategoryStruct.comp (Y :=
      obj.{v_5, v_5, u_5, u_5} (shiftFunctor D m)
        ((G.obj X₁).obj (obj.{v_3, v_3, u_3, u_3} (shiftFunctor C₂ n) (F.obj X₂'))))
      (NatTrans.app (Iso.hom (commShiftIso (G.flip.obj (obj.{v_3, v_3, u_3, u_3} (shiftFunctor C₂ n) (F.obj X₂'))) m))
        X₁)
      (map (shiftFunctor D m) (NatTrans.app (Iso.hom (commShiftIso (G.obj X₁) n)) (F.obj X₂')) ≫
        NatTrans.app (Iso.inv (shiftFunctorComm D m n)) ((G.obj X₁).obj (F.obj X₂')) ≫
          (↑(h.ε m n) : CatCenter D).app
            (obj.{v_5, v_5, u_5, u_5} (shiftFunctor D n)
              (obj.{v_5, v_5, u_5, u_5} (shiftFunctor D m) ((G.obj X₁).obj (F.obj X₂'))))))
⊢ Eq (α :=
    (G.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C₁ m) X₁)).obj
        (F.obj (obj.{v_4, v_4, u_4, u_4} (shiftFunctor C₂' n) X₂')) ⟶
      obj.{v_5, v_5, u_5, u_5} (shiftFunctor D m)
        ((G.obj X₁).obj (obj.{v_3, v_3, u_3, u_3} (shiftFunctor C₂ n) (F.obj X₂'))))
    ((G.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C₁ m) X₁)).map (NatTrans.app (Iso.hom (commShiftIso F n)) X₂') ≫
      NatTrans.app (Iso.hom (commShiftIso (G.flip.obj (obj.{v_3, v_3, u_3, u_3} (shiftFunctor C₂ n) (F.obj X₂'))) m))
        X₁)
    (NatTrans.app
        (Iso.hom
          (commShiftIso
            ((G ⋙ obj (whiskeringLeft C₂' C₂ D) F).flip.obj (obj.{v_4, v_4, u_4, u_4} (shiftFunctor C₂' n) X₂')) m))
        X₁ ≫
      map (shiftFunctor D m) ((G.obj X₁).map (NatTrans.app (Iso.hom (commShiftIso F n)) X₂')))

Tactic:
exact (NatTrans.shift_app_comm (G.flip.map ((F.commShiftIso n).hom.app X₂')) m X₁).symm

Premises used: CategoryTheory.Functor.flip, CategoryTheory.Functor.map, Eq.symm, CategoryTheory.NatTrans.shift_app_comm, CategoryTheory.Functor.CommShift.commShiftIso, CategoryTheory.Iso.hom, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Shift.CommShiftTwo
Goal:
C₁ : Type u_1
C₁' : Type u_2
C₂ : Type u_3
C₂' : Type u_4
D : Type u_5
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₁'
inst_2 : Category.{v_3, u_3} C₂
inst_3 : Category.{v_4, u_4} C₂'
inst_4 : Category.{v_5, u_5} D
M : Type u_6
inst_5 : AddCommMonoid M
inst_6 : HasShift.{v_1, u_1, u_6} C₁ M
inst_7 : HasShift.{v_3, u_3, u_6} C₂ M
inst_8 : HasShift.{v_5, u_5, u_6} D M
G₁ G₂ G₃ : C₁ ⥤ Functor.{v_3, v_5, u_3, u_5} C₂ D
τ : G₁ ⟶ G₂
τ' : G₂ ⟶ G₃
h : CommShift₂Setup.{v_5, u_5, u_6} D M
inst_9 : G₁.CommShift₂ h
inst_10 : G₂.CommShift₂ h
inst_11 : G₃.CommShift₂ h
x : C₁
⊢ CommShift (𝟙 (G₁.obj x)) M

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Shift.CommShiftTwo
Goal:
C₁ : Type u_1
C₁' : Type u_2
C₂ : Type u_3
C₂' : Type u_4
D : Type u_5
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₁'
inst_2 : Category.{v_3, u_3} C₂
inst_3 : Category.{v_4, u_4} C₂'
inst_4 : Category.{v_5, u_5} D
M : Type u_6
inst_5 : AddCommMonoid M
inst_6 : HasShift.{v_1, u_1, u_6} C₁ M
inst_7 : HasShift.{v_3, u_3, u_6} C₂ M
inst_8 : HasShift.{v_5, u_5, u_6} D M
G₁ G₂ G₃ : C₁ ⥤ Functor.{v_3, v_5, u_3, u_5} C₂ D
τ : G₁ ⟶ G₂
τ' : G₂ ⟶ G₃
h : CommShift₂Setup.{v_5, u_5, u_6} D M
inst_9 : G₁.CommShift₂ h
inst_10 : G₂.CommShift₂ h
inst_11 : G₃.CommShift₂ h
x : C₂
simp : CommShift (𝟙 (G₁.flip.obj x)) M
⊢ CommShift (flipApp (𝟙 G₁) x) M

Tactic:
simp only [flipApp, flipFunctor_obj, Functor.map_id, id_app]

Premises used: CategoryTheory.flipFunctor_obj, CategoryTheory.NatTrans.flipApp, CategoryTheory.Functor.map_id, CategoryTheory.NatTrans.id_app
-- Module: Mathlib.CategoryTheory.Shift.CommShiftTwo
Goal:
C₁ : Type u_1
C₁' : Type u_2
C₂ : Type u_3
C₂' : Type u_4
D : Type u_5
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₁'
inst_2 : Category.{v_3, u_3} C₂
inst_3 : Category.{v_4, u_4} C₂'
inst_4 : Category.{v_5, u_5} D
M : Type u_6
inst_5 : AddCommMonoid M
inst_6 : HasShift.{v_1, u_1, u_6} C₁ M
inst_7 : HasShift.{v_3, u_3, u_6} C₂ M
inst_8 : HasShift.{v_5, u_5, u_6} D M
G₁ G₂ G₃ : C₁ ⥤ Functor.{v_3, v_5, u_3, u_5} C₂ D
τ : G₁ ⟶ G₂
τ' : G₂ ⟶ G₃
h : CommShift₂Setup.{v_5, u_5, u_6} D M
inst_9 : G₁.CommShift₂ h
inst_10 : G₂.CommShift₂ h
inst_11 : G₃.CommShift₂ h
x : C₂
⊢ CommShift (𝟙 (G₁.flip.obj x)) M

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Shift.CommShiftTwo
Goal:
C₁ : Type u_1
C₁' : Type u_2
C₂ : Type u_3
C₂' : Type u_4
D : Type u_5
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₁'
inst_2 : Category.{v_3, u_3} C₂
inst_3 : Category.{v_4, u_4} C₂'
inst_4 : Category.{v_5, u_5} D
M : Type u_6
inst_5 : AddCommMonoid M
inst_6 : HasShift.{v_1, u_1, u_6} C₁ M
inst_7 : HasShift.{v_3, u_3, u_6} C₂ M
inst_8 : HasShift.{v_5, u_5, u_6} D M
G₁ G₂ G₃ : C₁ ⥤ Functor.{v_3, v_5, u_3, u_5} C₂ D
τ : G₁ ⟶ G₂
τ' : G₂ ⟶ G₃
h : CommShift₂Setup.{v_5, u_5, u_6} D M
inst_9 : G₁.CommShift₂ h
inst_10 : G₂.CommShift₂ h
inst_11 : G₃.CommShift₂ h
inst_12 : CommShift₂ τ h
inst_13 : CommShift₂ τ' h
x : C₁
⊢ CommShift (τ.app x ≫ τ'.app x) M

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Shift.CommShiftTwo
Goal:
C₁ : Type u_1
C₁' : Type u_2
C₂ : Type u_3
C₂' : Type u_4
D : Type u_5
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₁'
inst_2 : Category.{v_3, u_3} C₂
inst_3 : Category.{v_4, u_4} C₂'
inst_4 : Category.{v_5, u_5} D
M : Type u_6
inst_5 : AddCommMonoid M
inst_6 : HasShift.{v_1, u_1, u_6} C₁ M
inst_7 : HasShift.{v_3, u_3, u_6} C₂ M
inst_8 : HasShift.{v_5, u_5, u_6} D M
G₁ G₂ G₃ : C₁ ⥤ Functor.{v_3, v_5, u_3, u_5} C₂ D
τ : G₁ ⟶ G₂
τ' : G₂ ⟶ G₃
h : CommShift₂Setup.{v_5, u_5, u_6} D M
inst_9 : G₁.CommShift₂ h
inst_10 : G₂.CommShift₂ h
inst_11 : G₃.CommShift₂ h
inst_12 : CommShift₂ τ h
inst_13 : CommShift₂ τ' h
x : C₂
simp :
  CommShift (F₁ := G₁.flip.obj x) (F₂ := G₃.flip.obj x)
    (CategoryStruct.comp (Y := G₂.flip.obj x) (app (Functor.map (flipFunctor C₁ C₂ D) τ) x)
        (app (Functor.map (flipFunctor C₁ C₂ D) τ') x) :
      G₁.flip.obj x ⟶ G₃.flip.obj x)
    M
⊢ CommShift (flipApp (τ ≫ τ') x) M

Tactic:
simp only [flipApp, flipFunctor_obj, Functor.map_comp, comp_app]

Premises used: CategoryTheory.flipFunctor_obj, CategoryTheory.NatTrans.flipApp, CategoryTheory.Functor.map_comp, CategoryTheory.NatTrans.comp_app