awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Shift.CommShift
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
A : Type u_4
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_4} C A
inst_4 : HasShift.{v_2, u_2, u_4} D A
inst_5 : F.CommShift A
X : C
a b : A
h : a + b = 0
eq :
  Eq (α :=
    (shiftFunctor.{v_1, u_1, u_4} C (A := A) 0 ⋙ F).obj X ⟶ (F ⋙ shiftFunctor.{v_2, u_2, u_4} D (A := A) 0).obj X)
    (NatTrans.app (Iso.hom (commShiftIso F 0)) X)
    (NatTrans.app (Iso.hom (CommShift.isoAdd' h (commShiftIso F a) (commShiftIso F b))) X)
⊢ Eq (α :=
    F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor.{v_1, u_1, u_4} C (A := A) 0) X) ⟶
      obj.{v_2, v_2, u_2, u_2} (shiftFunctor.{v_2, u_2, u_4} D (A := A) 0) (F.obj X))
    (F.map (NatTrans.app (Iso.hom (shiftFunctorZero C A)) X) ≫ NatTrans.app (Iso.inv (shiftFunctorZero D A)) (F.obj X))
    (F.map (NatTrans.app (Iso.hom (shiftFunctorAdd' C a b 0 h)) X) ≫
      CategoryStruct.comp (Y :=
        obj.{v_2, v_2, u_2, u_2} (shiftFunctor D b) (F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)))
        (NatTrans.app (Iso.hom (commShiftIso F b)) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X))
        (map (shiftFunctor D b) (NatTrans.app (Iso.hom (commShiftIso F a)) X) ≫
          NatTrans.app (Iso.inv (shiftFunctorAdd' D a b 0 h)) (F.obj X)))

Tactic:
simp only [commShiftIso_zero, comp_obj, CommShift.isoZero_hom_app,
    CommShift.isoAdd'_hom_app] at eq

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Functor.CommShift.isoZero_hom_app, CategoryTheory.Functor.CommShift.isoAdd'_hom_app, CategoryTheory.Functor.CommShift.commShiftIso_zero
-- Module: Mathlib.CategoryTheory.Shift.CommShift
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
A : Type u_4
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_4} C A
inst_4 : HasShift.{v_2, u_2, u_4} D A
inst_5 : F.CommShift A
X : C
a b : A
h : a + b = 0
eq :
  Eq (α :=
    F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor.{v_1, u_1, u_4} C (A := A) 0) X) ⟶
      obj.{v_2, v_2, u_2, u_2} (shiftFunctor.{v_2, u_2, u_4} D (A := A) 0) (F.obj X))
    (F.map (NatTrans.app (Iso.hom (shiftFunctorZero C A)) X) ≫ NatTrans.app (Iso.inv (shiftFunctorZero D A)) (F.obj X))
    (F.map (NatTrans.app (Iso.hom (shiftFunctorAdd' C a b 0 h)) X) ≫
      CategoryStruct.comp (Y :=
        obj.{v_2, v_2, u_2, u_2} (shiftFunctor D b) (F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)))
        (NatTrans.app (Iso.hom (commShiftIso F b)) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X))
        (map (shiftFunctor D b) (NatTrans.app (Iso.hom (commShiftIso F a)) X) ≫
          NatTrans.app (Iso.inv (shiftFunctorAdd' D a b 0 h)) (F.obj X)))
rw :
  Eq (α := F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor.{v_1, u_1, u_4} C (A := A) 0) X) ⟶ F.obj X)
    (F.map (NatTrans.app (Iso.hom (shiftFunctorAdd' C a b 0 h)) X) ≫
      F.map (NatTrans.app (Iso.inv (shiftFunctorAdd' C a b 0 h)) X) ≫
        F.map (NatTrans.app (Iso.hom (shiftFunctorZero C A)) X))
    (F.map (NatTrans.app (Iso.hom (shiftFunctorZero C A)) X) ≫
      CategoryStruct.comp (Y := obj.{v_2, v_2, u_2, u_2} (shiftFunctor.{v_2, u_2, u_4} D (A := A) 0) (F.obj X))
        (NatTrans.app (Iso.inv (shiftFunctorZero D A)) (F.obj X))
        (NatTrans.app (Iso.hom (shiftFunctorZero D A)) (F.obj X)))
⊢ Eq (α :=
    F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ⟶ F.obj X)
    (F.map (NatTrans.app (Iso.inv (shiftFunctorAdd' C a b 0 h)) X ≫ NatTrans.app (Iso.hom (shiftFunctorZero C A)) X))
    (CategoryStruct.comp (Y :=
      obj.{v_2, v_2, u_2, u_2} (shiftFunctor D b) (F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)))
      (NatTrans.app (Iso.hom (commShiftIso F b)) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X))
      (map (shiftFunctor D b) (NatTrans.app (Iso.hom (commShiftIso F a)) X) ≫
        NatTrans.app (Iso.inv (shiftFunctorAdd' D a b 0 h)) (F.obj X) ≫
          NatTrans.app (Iso.hom (shiftFunctorZero D A)) (F.obj X)))

Tactic:
rw [← cancel_epi (F.map ((shiftFunctorAdd' C a b 0 h).hom.app X)), ← reassoc_of% eq, F.map_comp]

Premises used: CategoryTheory.shiftFunctorAdd', CategoryTheory.Functor.map, CategoryTheory.Functor.map_comp, OfNat.ofNat, CategoryTheory.cancel_epi, CategoryTheory.Iso.hom, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Shift.CommShift
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
A : Type u_4
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_4} C A
inst_4 : HasShift.{v_2, u_2, u_4} D A
inst_5 : F.CommShift A
X : C
a b : A
h : a + b = 0
eq :
  Eq (α :=
    F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor.{v_1, u_1, u_4} C (A := A) 0) X) ⟶
      obj.{v_2, v_2, u_2, u_2} (shiftFunctor.{v_2, u_2, u_4} D (A := A) 0) (F.obj X))
    (F.map (NatTrans.app (Iso.hom (shiftFunctorZero C A)) X) ≫ NatTrans.app (Iso.inv (shiftFunctorZero D A)) (F.obj X))
    (F.map (NatTrans.app (Iso.hom (shiftFunctorAdd' C a b 0 h)) X) ≫
      CategoryStruct.comp (Y :=
        obj.{v_2, v_2, u_2, u_2} (shiftFunctor D b) (F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)))
        (NatTrans.app (Iso.hom (commShiftIso F b)) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X))
        (map (shiftFunctor D b) (NatTrans.app (Iso.hom (commShiftIso F a)) X) ≫
          NatTrans.app (Iso.inv (shiftFunctorAdd' D a b 0 h)) (F.obj X)))
⊢ Eq (α := F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor.{v_1, u_1, u_4} C (A := A) 0) X) ⟶ F.obj X)
    (F.map (NatTrans.app (Iso.hom (shiftFunctorAdd' C a b 0 h)) X) ≫
      F.map (NatTrans.app (Iso.inv (shiftFunctorAdd' C a b 0 h)) X) ≫
        F.map (NatTrans.app (Iso.hom (shiftFunctorZero C A)) X))
    (F.map (NatTrans.app (Iso.hom (shiftFunctorZero C A)) X) ≫
      CategoryStruct.comp (Y := obj.{v_2, v_2, u_2, u_2} (shiftFunctor.{v_2, u_2, u_4} D (A := A) 0) (F.obj X))
        (NatTrans.app (Iso.inv (shiftFunctorZero D A)) (F.obj X))
        (NatTrans.app (Iso.hom (shiftFunctorZero D A)) (F.obj X)))

Tactic:
simp only [Iso.inv_hom_id_app, id_obj, Category.comp_id, ← F.map_comp_assoc, Iso.hom_inv_id_app,
    F.map_id, Category.id_comp]

Premises used: CategoryTheory.Iso.hom_inv_id_app, CategoryTheory.Category.comp_id, CategoryTheory.Functor.map_comp_assoc, CategoryTheory.Functor.map_id, CategoryTheory.Functor.id_obj, CategoryTheory.Iso.inv_hom_id_app, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Shift.CommShift
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
A : Type u_4
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_4} C A
inst_4 : HasShift.{v_2, u_2, u_4} D A
inst_5 : F.CommShift A
X : C
a b : A
h : a + b = 0
rw :
  𝟙 (F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a ⋙ shiftFunctor C b) X)) =
    CategoryStruct.comp (Y := (F ⋙ shiftFunctor D b).obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X))
        (NatTrans.app (Iso.hom (commShiftIso F b)) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X))
        (map (shiftFunctor D b) (NatTrans.app (Iso.hom (commShiftIso F a)) X) ≫
          NatTrans.app (Iso.hom (shiftFunctorCompIsoId D a b h)) (F.obj X)) ≫
      CategoryStruct.comp (Y := obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a ⋙ shiftFunctor D b) (F.obj X))
        (NatTrans.app (Iso.inv (shiftFunctorCompIsoId D a b h)) (F.obj X))
        (map (shiftFunctor D b) (NatTrans.app (Iso.inv (commShiftIso F a)) X) ≫
          NatTrans.app (Iso.inv (commShiftIso F b)) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X))
⊢ Eq (α :=
    F.obj (obj.{v_1, v_1, u_1, u_1} (𝟭 C) X) ⟶ F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a ⋙ shiftFunctor C b) X))
    (F.map (NatTrans.app (Iso.inv (shiftFunctorCompIsoId C a b h)) X))
    (CategoryStruct.comp (Y := obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a ⋙ shiftFunctor D b) (F.obj X))
      (NatTrans.app (Iso.inv (shiftFunctorCompIsoId D a b h)) (F.obj X))
      (map (shiftFunctor D b) (NatTrans.app (Iso.inv (commShiftIso F a)) X) ≫
        NatTrans.app (Iso.inv (commShiftIso F b)) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)))

Tactic:
rw [← cancel_epi (F.map ((shiftFunctorCompIsoId C a b h).hom.app X)), ← F.map_comp,
    Iso.hom_inv_id_app, F.map_id, map_shiftFunctorCompIsoId_hom_app]

Premises used: CategoryTheory.Iso.hom_inv_id_app, CategoryTheory.Functor.map_shiftFunctorCompIsoId_hom_app, CategoryTheory.Functor.map, CategoryTheory.Functor.map_id, CategoryTheory.shiftFunctorCompIsoId, CategoryTheory.Functor.map_comp, CategoryTheory.cancel_epi, CategoryTheory.Iso.hom, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Shift.CommShift
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
A : Type u_4
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_4} C A
inst_4 : HasShift.{v_2, u_2, u_4} D A
inst_5 : F.CommShift A
X : C
a b : A
h : a + b = 0
⊢ 𝟙 (F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a ⋙ shiftFunctor C b) X)) =
    CategoryStruct.comp (Y := (F ⋙ shiftFunctor D b).obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X))
        (NatTrans.app (Iso.hom (commShiftIso F b)) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X))
        (map (shiftFunctor D b) (NatTrans.app (Iso.hom (commShiftIso F a)) X) ≫
          NatTrans.app (Iso.hom (shiftFunctorCompIsoId D a b h)) (F.obj X)) ≫
      CategoryStruct.comp (Y := obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a ⋙ shiftFunctor D b) (F.obj X))
        (NatTrans.app (Iso.inv (shiftFunctorCompIsoId D a b h)) (F.obj X))
        (map (shiftFunctor D b) (NatTrans.app (Iso.inv (commShiftIso F a)) X) ≫
          NatTrans.app (Iso.inv (commShiftIso F b)) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X))

Tactic:
simp only [comp_obj, id_obj, Category.assoc, Iso.hom_inv_id_app_assoc,
    ← Functor.map_comp_assoc, Iso.hom_inv_id_app, Functor.map_id, Category.id_comp]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Category.assoc, CategoryTheory.Iso.hom_inv_id_app, CategoryTheory.Functor.map_comp_assoc, CategoryTheory.Iso.hom_inv_id_app_assoc, CategoryTheory.Functor.map_id, CategoryTheory.Functor.id_obj, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Shift.CommShift
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F₁ F₂ : Functor.{v_1, v_2, u_1, u_2} C D
τ : F₁ ⟶ F₂
A : Type u_5
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_5} C A
inst_4 : HasShift.{v_2, u_2, u_5} D A
inst_5 : F₁.CommShift A
inst_6 : F₂.CommShift A
a : A
hτ : CommShiftCore τ a
X : C
⊢ Eq (α := (shiftFunctor C a ⋙ F₁).obj X ⟶ Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F₂.obj X))
    (app (Iso.hom (Functor.commShiftIso F₁ a)) X ≫ Functor.map (shiftFunctor D a) (τ.app X))
    (τ.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ≫ app (Iso.hom (Functor.commShiftIso F₂ a)) X)

Tactic:
congr_app hτ.shift_comm X

Premises used: CategoryTheory.NatTrans.congr_app, CategoryTheory.NatTrans.CommShiftCore.shift_comm
-- Module: Mathlib.CategoryTheory.Shift.CommShift
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F₁ F₂ : Functor.{v_1, v_2, u_1, u_2} C D
τ : F₁ ⟶ F₂
A : Type u_5
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_5} C A
inst_4 : HasShift.{v_2, u_2, u_5} D A
inst_5 : F₁.CommShift A
inst_6 : F₂.CommShift A
a : A
hτ : CommShiftCore τ a
X : C
rw :
  Eq (α :=
    Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F₁.obj X) ⟶
      Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F₂.obj X))
    (Functor.map (shiftFunctor D a) (τ.app X))
    (CategoryStruct.comp (Y := (shiftFunctor C a ⋙ F₁).obj X) (app (Iso.inv (Functor.commShiftIso F₁ a)) X)
      (app (Iso.hom (Functor.commShiftIso F₁ a)) X ≫ Functor.map (shiftFunctor D a) (τ.app X)))
rw₁ rw₂ :
  Eq (α :=
    Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F₁.obj X) ⟶
      Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F₂.obj X))
    (Functor.map (shiftFunctor D a) (τ.app X)) (Functor.map (shiftFunctor D a) (τ.app X))
⊢ Eq (α :=
    Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F₁.obj X) ⟶
      Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F₂.obj X))
    (Functor.map (shiftFunctor D a) (τ.app X))
    (CategoryStruct.comp (Y := (shiftFunctor C a ⋙ F₁).obj X) (app (Iso.inv (Functor.commShiftIso F₁ a)) X)
      (τ.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ≫ app (Iso.hom (Functor.commShiftIso F₂ a)) X))

Tactic:
rw [← hτ.shift_app_comm, Iso.inv_hom_id_app_assoc]

Premises used: CategoryTheory.NatTrans.CommShiftCore.shift_app_comm, CategoryTheory.Iso.inv_hom_id_app_assoc
-- Module: Mathlib.CategoryTheory.Shift.CommShift
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F₁ F₂ : Functor.{v_1, v_2, u_1, u_2} C D
τ : F₁ ⟶ F₂
A : Type u_5
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_5} C A
inst_4 : HasShift.{v_2, u_2, u_5} D A
inst_5 : F₁.CommShift A
inst_6 : F₂.CommShift A
a : A
hτ : CommShiftCore τ a
X : C
⊢ Eq (α :=
    F₁.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ⟶
      F₂.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X))
    (τ.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X))
    (CategoryStruct.comp (Y := (F₁ ⋙ shiftFunctor D a).obj X) (app (Iso.hom (Functor.commShiftIso F₁ a)) X)
      (Functor.map (shiftFunctor D a) (τ.app X) ≫ app (Iso.inv (Functor.commShiftIso F₂ a)) X))

Tactic:
simp [hτ.shift_app_comm_assoc τ X]

Premises used: CategoryTheory.NatTrans.CommShiftCore.shift_app_comm_assoc
-- Module: Mathlib.CategoryTheory.Shift.CommShift
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F₁ F₂ : Functor.{v_1, v_2, u_1, u_2} C D
τ : F₁ ⟶ F₂
A : Type u_5
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_5} C A
inst_4 : HasShift.{v_2, u_2, u_5} D A
inst_5 : F₁.CommShift A
inst_6 : F₂.CommShift A
w :
  ∀ (X : C),
    Eq (α :=
      (shiftFunctor.{v_1, u_1, u_5} C (A := A) 0 ⋙ F₁).obj X ⟶ (F₂ ⋙ shiftFunctor.{v_2, u_2, u_5} D (A := A) 0).obj X)
      (app (Iso.hom (Functor.commShiftIso F₁ 0) ≫ Functor.whiskerRight τ (shiftFunctor.{v_2, u_2, u_5} D (A := A) 0)) X)
      (app (Functor.whiskerLeft (shiftFunctor.{v_1, u_1, u_5} C (A := A) 0) τ ≫ Iso.hom (Functor.commShiftIso F₂ 0)) X)
⊢ Eq (α := shiftFunctor.{v_1, u_1, u_5} C (A := A) 0 ⋙ F₁ ⟶ F₂ ⋙ shiftFunctor.{v_2, u_2, u_5} D (A := A) 0)
    (Iso.hom (Functor.commShiftIso F₁ 0) ≫ Functor.whiskerRight τ (shiftFunctor.{v_2, u_2, u_5} D (A := A) 0))
    (Functor.whiskerLeft (shiftFunctor.{v_1, u_1, u_5} C (A := A) 0) τ ≫ Iso.hom (Functor.commShiftIso F₂ 0))

Tactic:
ext X
-- Module: Mathlib.CategoryTheory.Shift.CommShift
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F₁ F₂ : Functor.{v_1, v_2, u_1, u_2} C D
τ : F₁ ⟶ F₂
A : Type u_5
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_5} C A
inst_4 : HasShift.{v_2, u_2, u_5} D A
inst_5 : F₁.CommShift A
inst_6 : F₂.CommShift A
X : C
⊢ Eq (α :=
    (shiftFunctor.{v_1, u_1, u_5} C (A := A) 0 ⋙ F₁).obj X ⟶ (F₂ ⋙ shiftFunctor.{v_2, u_2, u_5} D (A := A) 0).obj X)
    (app (Iso.hom (Functor.commShiftIso F₁ 0) ≫ Functor.whiskerRight τ (shiftFunctor.{v_2, u_2, u_5} D (A := A) 0)) X)
    (app (Functor.whiskerLeft (shiftFunctor.{v_1, u_1, u_5} C (A := A) 0) τ ≫ Iso.hom (Functor.commShiftIso F₂ 0)) X)

Tactic:
simp [Functor.commShiftIso_zero, ← NatTrans.naturality]

Premises used: CategoryTheory.NatTrans.naturality, CategoryTheory.Functor.CommShift.commShiftIso_zero
-- Module: Mathlib.CategoryTheory.Shift.CommShift
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F₁ F₂ : Functor.{v_1, v_2, u_1, u_2} C D
τ : F₁ ⟶ F₂
A : Type u_5
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_5} C A
inst_4 : HasShift.{v_2, u_2, u_5} D A
inst_5 : F₁.CommShift A
inst_6 : F₂.CommShift A
a b : A
ha : CommShiftCore τ a
hb : CommShiftCore τ b
w :
  ∀ (X : C),
    Eq (α := (shiftFunctor C (a + b) ⋙ F₁).obj X ⟶ (F₂ ⋙ shiftFunctor D (a + b)).obj X)
      (app (Iso.hom (Functor.commShiftIso F₁ (a + b)) ≫ Functor.whiskerRight τ (shiftFunctor D (a + b))) X)
      (app (Functor.whiskerLeft (shiftFunctor C (a + b)) τ ≫ Iso.hom (Functor.commShiftIso F₂ (a + b))) X)
⊢ Eq (α := shiftFunctor C (a + b) ⋙ F₁ ⟶ F₂ ⋙ shiftFunctor D (a + b))
    (Iso.hom (Functor.commShiftIso F₁ (a + b)) ≫ Functor.whiskerRight τ (shiftFunctor D (a + b)))
    (Functor.whiskerLeft (shiftFunctor C (a + b)) τ ≫ Iso.hom (Functor.commShiftIso F₂ (a + b)))

Tactic:
ext X
-- Module: Mathlib.CategoryTheory.Shift.CommShift
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F₁ F₂ : Functor.{v_1, v_2, u_1, u_2} C D
τ : F₁ ⟶ F₂
A : Type u_5
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_5} C A
inst_4 : HasShift.{v_2, u_2, u_5} D A
inst_5 : F₁.CommShift A
inst_6 : F₂.CommShift A
a b : A
ha : CommShiftCore τ a
hb : CommShiftCore τ b
X : C
⊢ Eq (α :=
    Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a ⋙ shiftFunctor D b) (F₁.obj X) ⟶
      Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (a + b)) (F₂.obj X))
    (Functor.map (shiftFunctor D a ⋙ shiftFunctor D b) (τ.app X) ≫ app (Iso.inv (shiftFunctorAdd D a b)) (F₂.obj X))
    (app (Iso.inv (shiftFunctorAdd D a b)) (F₁.obj X) ≫ Functor.map (shiftFunctor D (a + b)) (τ.app X))

Tactic:
have := (shiftFunctorAdd D a b).inv.naturality (τ.app X)
-- Module: Mathlib.CategoryTheory.Shift.CommShift
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F₁ F₂ : Functor.{v_1, v_2, u_1, u_2} C D
τ : F₁ ⟶ F₂
A : Type u_5
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_5} C A
inst_4 : HasShift.{v_2, u_2, u_5} D A
inst_5 : F₁.CommShift A
inst_6 : F₂.CommShift A
a b : A
ha : CommShiftCore τ a
hb : CommShiftCore τ b
X : C
this :
  Eq (α :=
    Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a ⋙ shiftFunctor D b) (F₁.obj X) ⟶
      Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (a + b)) (F₂.obj X))
    (Functor.map (shiftFunctor D a ⋙ shiftFunctor D b) (τ.app X) ≫ app (Iso.inv (shiftFunctorAdd D a b)) (F₂.obj X))
    (app (Iso.inv (shiftFunctorAdd D a b)) (F₁.obj X) ≫ Functor.map (shiftFunctor D (a + b)) (τ.app X))
w :
  Eq (α :=
    F₁.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (a + b)) X) ⟶
      Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (a + b)) (F₂.obj X))
    (app (Iso.hom (Functor.commShiftIso F₁ (a + b))) X ≫ Functor.map (shiftFunctor D (a + b)) (τ.app X))
    (τ.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (a + b)) X) ≫
      app (Iso.hom (Functor.commShiftIso F₂ (a + b))) X)
⊢ Eq (α := (shiftFunctor C (a + b) ⋙ F₁).obj X ⟶ (F₂ ⋙ shiftFunctor D (a + b)).obj X)
    (app (Iso.hom (Functor.commShiftIso F₁ (a + b)) ≫ Functor.whiskerRight τ (shiftFunctor D (a + b))) X)
    (app (Functor.whiskerLeft (shiftFunctor C (a + b)) τ ≫ Iso.hom (Functor.commShiftIso F₂ (a + b))) X)

Tactic:
dsimp at this ⊢
-- Module: Mathlib.CategoryTheory.Shift.CommShift
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F₁ F₂ : Functor.{v_1, v_2, u_1, u_2} C D
τ : F₁ ⟶ F₂
A : Type u_5
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_5} C A
inst_4 : HasShift.{v_2, u_2, u_5} D A
inst_5 : F₁.CommShift A
inst_6 : F₂.CommShift A
inst_7 : CommShift τ A
a : A
⊢ Eq (α := shiftFunctor C a ⋙ F₁ ⟶ F₂ ⋙ shiftFunctor D a)
    (Iso.hom (Functor.commShiftIso F₁ a) ≫ Functor.whiskerRight τ (shiftFunctor D a))
    (Functor.whiskerLeft (shiftFunctor C a) τ ≫ Iso.hom (Functor.commShiftIso F₂ a))

Tactic:
apply CommShift.shift_comm

Premises used: CategoryTheory.NatTrans.CommShift.shift_comm
-- Module: Mathlib.CategoryTheory.Shift.CommShift
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F₁ F₂ : Functor.{v_1, v_2, u_1, u_2} C D
τ : F₁ ⟶ F₂
A : Type u_5
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_5} C A
inst_4 : HasShift.{v_2, u_2, u_5} D A
inst_5 : F₁.CommShift A
inst_6 : F₂.CommShift A
inst_7 : CommShift τ A
a : A
X : C
⊢ Eq (α := (shiftFunctor C a ⋙ F₁).obj X ⟶ Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F₂.obj X))
    (app (Iso.hom (Functor.commShiftIso F₁ a)) X ≫ Functor.map (shiftFunctor D a) (τ.app X))
    (τ.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ≫ app (Iso.hom (Functor.commShiftIso F₂ a)) X)

Tactic:
congr_app (shift_comm τ a) X

Premises used: CategoryTheory.NatTrans.shift_comm, CategoryTheory.NatTrans.congr_app
-- Module: Mathlib.CategoryTheory.Shift.CommShift
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F₁ F₂ : Functor.{v_1, v_2, u_1, u_2} C D
τ : F₁ ⟶ F₂
A : Type u_5
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_5} C A
inst_4 : HasShift.{v_2, u_2, u_5} D A
inst_5 : F₁.CommShift A
inst_6 : F₂.CommShift A
inst_7 : CommShift τ A
a : A
X : C
rw :
  Eq (α :=
    Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F₁.obj X) ⟶
      Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F₂.obj X))
    (Functor.map (shiftFunctor D a) (τ.app X))
    (CategoryStruct.comp (Y := (shiftFunctor C a ⋙ F₁).obj X) (app (Iso.inv (Functor.commShiftIso F₁ a)) X)
      (app (Iso.hom (Functor.commShiftIso F₁ a)) X ≫ Functor.map (shiftFunctor D a) (τ.app X)))
rw₁ rw₂ :
  Eq (α :=
    Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F₁.obj X) ⟶
      Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F₂.obj X))
    (Functor.map (shiftFunctor D a) (τ.app X)) (Functor.map (shiftFunctor D a) (τ.app X))
⊢ Eq (α :=
    Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F₁.obj X) ⟶
      Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F₂.obj X))
    (Functor.map (shiftFunctor D a) (τ.app X))
    (CategoryStruct.comp (Y := (shiftFunctor C a ⋙ F₁).obj X) (app (Iso.inv (Functor.commShiftIso F₁ a)) X)
      (τ.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ≫ app (Iso.hom (Functor.commShiftIso F₂ a)) X))

Tactic:
rw [← shift_app_comm, Iso.inv_hom_id_app_assoc]

Premises used: CategoryTheory.NatTrans.shift_app_comm, CategoryTheory.Iso.inv_hom_id_app_assoc
-- Module: Mathlib.CategoryTheory.Shift.CommShift
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F₁ F₂ : Functor.{v_1, v_2, u_1, u_2} C D
τ : F₁ ⟶ F₂
A : Type u_5
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_5} C A
inst_4 : HasShift.{v_2, u_2, u_5} D A
inst_5 : F₁.CommShift A
inst_6 : F₂.CommShift A
inst_7 : CommShift τ A
a : A
X : C
⊢ Eq (α :=
    F₁.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ⟶
      F₂.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X))
    (τ.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X))
    (CategoryStruct.comp (Y := (F₁ ⋙ shiftFunctor D a).obj X) (app (Iso.hom (Functor.commShiftIso F₁ a)) X)
      (Functor.map (shiftFunctor D a) (τ.app X) ≫ app (Iso.inv (Functor.commShiftIso F₂ a)) X))

Tactic:
simp [shift_app_comm_assoc τ a X]

Premises used: CategoryTheory.NatTrans.shift_app_comm_assoc