awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Shift.Adjunction
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
G : Functor.{v_2, v_1, u_2, u_1} D C
adj : F ⊣ G
A : Type u_3
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_3} C A
inst_4 : HasShift.{v_2, u_2, u_3} D A
inst_5 : F.CommShift A
inst_6 : G.CommShift A
inst_7 : adj.CommShift A
a : A
X : C
⊢ Eq (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 C) X) ⟶
      (shiftFunctor C a ⋙ F ⋙ G).obj X)
    (Functor.map (shiftFunctor C a) (adj.unit.app X) ≫ NatTrans.app (Iso.inv (Functor.commShiftIso (F ⋙ G) a)) X)
    (adj.unit.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X))

Tactic:
simp [← cancel_mono (((F ⋙ G).commShiftIso _).hom.app _)]

Premises used: CategoryTheory.Functor.comp, CategoryTheory.cancel_mono, CategoryTheory.Functor.CommShift.commShiftIso, CategoryTheory.Iso.hom, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Shift.Adjunction
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
G : Functor.{v_2, v_1, u_2, u_1} D C
adj : F ⊣ G
A : Type u_3
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_3} C A
inst_4 : HasShift.{v_2, u_2, u_3} D A
inst_5 : F.CommShift A
inst_6 : G.CommShift A
inst_7 : adj.CommShift A
a : A
Y : D
⊢ Eq (α :=
    (shiftFunctor D a ⋙ G ⋙ F).obj Y ⟶
      Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (Functor.obj.{v_2, v_2, u_2, u_2} (𝟭 D) Y))
    (NatTrans.app (Iso.hom (Functor.commShiftIso (G ⋙ F) a)) Y ≫ Functor.map (shiftFunctor D a) (adj.counit.app Y))
    (adj.counit.app (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) Y))

Tactic:
simpa using (NatTrans.shift_app_comm adj.counit a Y)

Premises used: CategoryTheory.Adjunction.counit, CategoryTheory.NatTrans.shift_app_comm
-- Module: Mathlib.CategoryTheory.Shift.Adjunction
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
G : Functor.{v_2, v_1, u_2, u_1} D C
adj : F ⊣ G
A : Type u_3
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_3} C A
inst_4 : HasShift.{v_2, u_2, u_3} D A
inst_5 : F.CommShift A
inst_6 : G.CommShift A
inst_7 : adj.CommShift A
a : A
Y : D
⊢ Eq (α :=
    ((G ⋙ F) ⋙ shiftFunctor D a).obj Y ⟶
      Functor.obj.{v_2, v_2, u_2, u_2} (𝟭 D) (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) Y))
    (NatTrans.app (Iso.inv (Functor.commShiftIso (G ⋙ F) a)) Y ≫
      adj.counit.app (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) Y))
    (Functor.map (shiftFunctor D a) (adj.counit.app Y))

Tactic:
simp [← cancel_epi (((G ⋙ F).commShiftIso _).hom.app _)]

Premises used: CategoryTheory.Functor.comp, CategoryTheory.Functor.CommShift.commShiftIso, CategoryTheory.cancel_epi, CategoryTheory.Iso.hom, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Shift.Adjunction
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
G : Functor.{v_2, v_1, u_2, u_1} D C
adj : F ⊣ G
A : Type u_3
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_3} C A
inst_4 : HasShift.{v_2, u_2, u_3} D A
inst_5 : F.CommShift A
inst_6 : G.CommShift A
h : NatTrans.CommShift adj.unit A
a : A
w :
  ∀ (x : D),
    Eq (α := (shiftFunctor D a ⋙ G ⋙ F).obj x ⟶ Functor.obj.{v_2, v_2, u_2, u_2} (𝟭 D ⋙ shiftFunctor D a) x)
      (NatTrans.app (Iso.hom (Functor.commShiftIso (G ⋙ F) a) ≫ Functor.whiskerRight adj.counit (shiftFunctor D a)) x)
      (NatTrans.app (Functor.whiskerLeft (shiftFunctor D a) adj.counit ≫ Iso.hom (Functor.commShiftIso (𝟭 D) a)) x)
⊢ Eq (α := shiftFunctor D a ⋙ G ⋙ F ⟶ 𝟭 D ⋙ shiftFunctor D a)
    (Iso.hom (Functor.commShiftIso (G ⋙ F) a) ≫ Functor.whiskerRight adj.counit (shiftFunctor D a))
    (Functor.whiskerLeft (shiftFunctor D a) adj.counit ≫ Iso.hom (Functor.commShiftIso (𝟭 D) a))

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Shift.Adjunction
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
G : Functor.{v_2, v_1, u_2, u_1} D C
adj : F ⊣ G
A : Type u_3
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_3} C A
inst_4 : HasShift.{v_2, u_2, u_3} D A
inst_5 : F.CommShift A
inst_6 : G.CommShift A
h : NatTrans.CommShift adj.unit A
a : A
x : D
w :
  Eq (α :=
    F.obj (G.obj (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) x)) ⟶
      Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) x)
    (CategoryStruct.comp (Y := F.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (G.obj x)))
      (F.map (NatTrans.app (Iso.hom (Functor.commShiftIso G a)) x))
      (NatTrans.app (Iso.hom (Functor.commShiftIso F a)) (G.obj x) ≫ Functor.map (shiftFunctor D a) (adj.counit.app x)))
    (adj.counit.app (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) x))
⊢ Eq (α := (shiftFunctor D a ⋙ G ⋙ F).obj x ⟶ Functor.obj.{v_2, v_2, u_2, u_2} (𝟭 D ⋙ shiftFunctor D a) x)
    (NatTrans.app (Iso.hom (Functor.commShiftIso (G ⋙ F) a) ≫ Functor.whiskerRight adj.counit (shiftFunctor D a)) x)
    (NatTrans.app (Functor.whiskerLeft (shiftFunctor D a) adj.counit ≫ Iso.hom (Functor.commShiftIso (𝟭 D) a)) x)

Tactic:
simp only [Functor.comp_obj, Functor.id_obj, NatTrans.comp_app,
      Functor.commShiftIso_comp_hom_app, Functor.whiskerRight_app, assoc, Functor.whiskerLeft_app,
      Functor.commShiftIso_id_hom_app, comp_id]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Category.assoc, CategoryTheory.Functor.commShiftIso_comp_hom_app, CategoryTheory.Functor.whiskerLeft_app, CategoryTheory.Category.comp_id, CategoryTheory.Functor.commShiftIso_id_hom_app, CategoryTheory.Functor.id_obj, CategoryTheory.Functor.whiskerRight_app, CategoryTheory.NatTrans.comp_app
-- Module: Mathlib.CategoryTheory.Shift.Adjunction
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
G : Functor.{v_2, v_1, u_2, u_1} D C
adj : F ⊣ G
A : Type u_3
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_3} C A
inst_4 : HasShift.{v_2, u_2, u_3} D A
inst_5 : F.CommShift A
inst_6 : G.CommShift A
h : NatTrans.CommShift adj.unit A
a : A
x : D
⊢ Eq (α :=
    F.obj (G.obj (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) x)) ⟶
      Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) x)
    (CategoryStruct.comp (Y := F.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (G.obj x)))
      (F.map (NatTrans.app (Iso.hom (Functor.commShiftIso G a)) x))
      (NatTrans.app (Iso.hom (Functor.commShiftIso F a)) (G.obj x) ≫ Functor.map (shiftFunctor D a) (adj.counit.app x)))
    (adj.counit.app (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) x))

Tactic:
(compatibilityCounit_of_compatibilityUnit adj _ _ (fun X ↦ ?_) _).symm

Premises used: CategoryTheory.Adjunction.CommShift.compatibilityCounit_of_compatibilityUnit, Eq.symm
-- Module: Mathlib.CategoryTheory.Shift.Adjunction
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
G : Functor.{v_2, v_1, u_2, u_1} D C
adj : F ⊣ G
A : Type u_3
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_3} C A
inst_4 : HasShift.{v_2, u_2, u_3} D A
inst_5 : F.CommShift A
inst_6 : G.CommShift A
h : NatTrans.CommShift adj.unit A
a : A
x : D
w :
  ∀ (X : C),
    Eq (α :=
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 C) X) ⟶
        Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) ((F ⋙ G).obj X))
      (Functor.map (shiftFunctor C a) (adj.unit.app X))
      (adj.unit.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ≫
        CategoryStruct.comp (Y := G.obj ((F ⋙ shiftFunctor D a).obj X))
          (G.map (NatTrans.app (Iso.hom (Functor.commShiftIso F a)) X))
          (NatTrans.app (Iso.hom (Functor.commShiftIso G a)) (F.obj X)))
⊢ Eq (α :=
    F.obj (G.obj (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) x)) ⟶
      Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) x)
    (CategoryStruct.comp (Y := F.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (G.obj x)))
      (F.map (NatTrans.app (Iso.hom (Functor.commShiftIso G a)) x))
      (NatTrans.app (Iso.hom (Functor.commShiftIso F a)) (G.obj x) ≫ Functor.map (shiftFunctor D a) (adj.counit.app x)))
    (adj.counit.app (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) x))

Tactic:
refine (compatibilityCounit_of_compatibilityUnit adj _ _ (fun X ↦ ?_) _).symm

Premises used: CategoryTheory.Adjunction.CommShift.compatibilityCounit_of_compatibilityUnit, Eq.symm
-- Module: Mathlib.CategoryTheory.Shift.Adjunction
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
G : Functor.{v_2, v_1, u_2, u_1} D C
adj : F ⊣ G
A : Type u_3
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_3} C A
inst_4 : HasShift.{v_2, u_2, u_3} D A
inst_5 : F.CommShift A
inst_6 : G.CommShift A
h : NatTrans.CommShift adj.unit A
a : A
x : D
X : C
⊢ Eq (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 C) X) ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) ((F ⋙ G).obj X))
    (Functor.map (shiftFunctor C a) (adj.unit.app X))
    (adj.unit.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ≫
      CategoryStruct.comp (Y := G.obj ((F ⋙ shiftFunctor D a).obj X))
        (G.map (NatTrans.app (Iso.hom (Functor.commShiftIso F a)) X))
        (NatTrans.app (Iso.hom (Functor.commShiftIso G a)) (F.obj X)))

Tactic:
simpa [Functor.commShiftIso_comp_hom_app] using NatTrans.shift_app_comm adj.unit a X

Premises used: CategoryTheory.Functor.commShiftIso_comp_hom_app, CategoryTheory.Adjunction.unit, CategoryTheory.NatTrans.shift_app_comm
-- Module: Mathlib.CategoryTheory.Shift.Adjunction
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
G : Functor.{v_2, v_1, u_2, u_1} D C
adj : F ⊣ G
A : Type u_3
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_3} C A
inst_4 : HasShift.{v_2, u_2, u_3} D A
inst_5 : F.CommShift A
inst_6 : G.CommShift A
E : Type u_4
inst_7 : Category.{v_3, u_4} E
F' : Functor.{v_2, v_3, u_2, u_4} D E
G' : Functor.{v_3, v_2, u_4, u_2} E D
adj' : F' ⊣ G'
inst_8 : HasShift.{v_3, u_4, u_3} E A
inst_9 : F'.CommShift A
inst_10 : G'.CommShift A
inst_11 : adj.CommShift A
inst_12 : adj'.CommShift A
rw :
  NatTrans.CommShift
    (adj.unit ≫
      Functor.whiskerRight F.rightUnitor.inv G ≫
        Functor.whiskerRight (F.whiskerLeft adj'.unit) G ≫
          Functor.whiskerRight (F.associator F' G').inv G ≫ ((F ⋙ F').associator G' G).hom)
    A
⊢ NatTrans.CommShift (adj.comp adj').unit A

Tactic:
rw [comp_unit]

Premises used: CategoryTheory.Adjunction.comp_unit
-- Module: Mathlib.CategoryTheory.Shift.Adjunction
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
G : Functor.{v_2, v_1, u_2, u_1} D C
adj : F ⊣ G
A : Type u_3
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_3} C A
inst_4 : HasShift.{v_2, u_2, u_3} D A
inst_5 : F.CommShift A
inst_6 : G.CommShift A
E : Type u_4
inst_7 : Category.{v_3, u_4} E
F' : Functor.{v_2, v_3, u_2, u_4} D E
G' : Functor.{v_3, v_2, u_4, u_2} E D
adj' : F' ⊣ G'
inst_8 : HasShift.{v_3, u_4, u_3} E A
inst_9 : F'.CommShift A
inst_10 : G'.CommShift A
inst_11 : adj.CommShift A
inst_12 : adj'.CommShift A
⊢ NatTrans.CommShift
    (adj.unit ≫
      Functor.whiskerRight F.rightUnitor.inv G ≫
        Functor.whiskerRight (F.whiskerLeft adj'.unit) G ≫
          Functor.whiskerRight (F.associator F' G').inv G ≫ ((F ⋙ F').associator G' G).hom)
    A

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Shift.Adjunction
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
G : Functor.{v_2, v_1, u_2, u_1} D C
adj : F ⊣ G
A : Type u_3
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_3} C A
inst_4 : HasShift.{v_2, u_2, u_3} D A
inst_5 : F.CommShift A
inst_6 : G.CommShift A
E : Type u_4
inst_7 : Category.{v_3, u_4} E
F' : Functor.{v_2, v_3, u_2, u_4} D E
G' : Functor.{v_3, v_2, u_4, u_2} E D
adj' : F' ⊣ G'
inst_8 : HasShift.{v_3, u_4, u_3} E A
inst_9 : F'.CommShift A
inst_10 : G'.CommShift A
inst_11 : adj.CommShift A
inst_12 : adj'.CommShift A
rw :
  NatTrans.CommShift
    (((G' ⋙ G).associator F F').inv ≫
      Functor.whiskerRight (G'.associator G F).hom F' ≫
        Functor.whiskerRight (G'.whiskerLeft adj.counit) F' ≫ Functor.whiskerRight G'.rightUnitor.hom F' ≫ adj'.counit)
    A
⊢ NatTrans.CommShift (adj.comp adj').counit A

Tactic:
rw [comp_counit]

Premises used: CategoryTheory.Adjunction.comp_counit
-- Module: Mathlib.CategoryTheory.Shift.Adjunction
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
G : Functor.{v_2, v_1, u_2, u_1} D C
adj : F ⊣ G
A : Type u_3
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_3} C A
inst_4 : HasShift.{v_2, u_2, u_3} D A
inst_5 : F.CommShift A
inst_6 : G.CommShift A
E : Type u_4
inst_7 : Category.{v_3, u_4} E
F' : Functor.{v_2, v_3, u_2, u_4} D E
G' : Functor.{v_3, v_2, u_4, u_2} E D
adj' : F' ⊣ G'
inst_8 : HasShift.{v_3, u_4, u_3} E A
inst_9 : F'.CommShift A
inst_10 : G'.CommShift A
inst_11 : adj.CommShift A
inst_12 : adj'.CommShift A
⊢ NatTrans.CommShift
    (((G' ⋙ G).associator F F').inv ≫
      Functor.whiskerRight (G'.associator G F).hom F' ≫
        Functor.whiskerRight (G'.whiskerLeft adj.counit) F' ≫ Functor.whiskerRight G'.rightUnitor.hom F' ≫ adj'.counit)
    A

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Shift.Adjunction
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
G : Functor.{v_2, v_1, u_2, u_1} D C
adj : F ⊣ G
A : Type u_3
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_3} C A
inst_4 : HasShift.{v_2, u_2, u_3} D A
inst_5 : F.CommShift A
inst_6 : G.CommShift A
inst_7 : adj.CommShift A
a : A
X : C
⊢ Eq (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 C) X) ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) ((F ⋙ G).obj X))
    (Functor.map (shiftFunctor C a) (adj.unit.app X))
    (adj.unit.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ≫
      CategoryStruct.comp (Y := G.obj ((F ⋙ shiftFunctor D a).obj X))
        (G.map (NatTrans.app (Iso.hom (Functor.commShiftIso F a)) X))
        (NatTrans.app (Iso.hom (Functor.commShiftIso G a)) (F.obj X)))

Tactic:
simpa [Functor.commShiftIso_comp_hom_app] using NatTrans.shift_app_comm adj.unit a X

Premises used: CategoryTheory.Functor.commShiftIso_comp_hom_app, CategoryTheory.Adjunction.unit, CategoryTheory.NatTrans.shift_app_comm
-- Module: Mathlib.CategoryTheory.Shift.Adjunction
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
G : Functor.{v_2, v_1, u_2, u_1} D C
adj : F ⊣ G
A : Type u_3
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_3} C A
inst_4 : HasShift.{v_2, u_2, u_3} D A
inst_5 : F.CommShift A
inst_6 : G.CommShift A
inst_7 : adj.CommShift A
a : A
Y : D
⊢ Eq (α :=
    (shiftFunctor D a ⋙ G ⋙ F).obj Y ⟶
      Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (Functor.obj.{v_2, v_2, u_2, u_2} (𝟭 D) Y))
    (NatTrans.app (Iso.hom (Functor.commShiftIso (G ⋙ F) a)) Y ≫ Functor.map (shiftFunctor D a) (adj.counit.app Y))
    (adj.counit.app (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) Y) ≫
      NatTrans.app (Iso.hom (Functor.commShiftIso (𝟭 D) a)) Y)

Tactic:
have eq := NatTrans.shift_app_comm adj.counit a Y
-- Module: Mathlib.CategoryTheory.Shift.Adjunction
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
G : Functor.{v_2, v_1, u_2, u_1} D C
adj : F ⊣ G
A : Type u_3
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_3} C A
inst_4 : HasShift.{v_2, u_2, u_3} D A
inst_5 : F.CommShift A
inst_6 : G.CommShift A
inst_7 : adj.CommShift A
a : A
Y : D
eq :
  Eq (α :=
    (shiftFunctor D a ⋙ G ⋙ F).obj Y ⟶
      Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (Functor.obj.{v_2, v_2, u_2, u_2} (𝟭 D) Y))
    (NatTrans.app (Iso.hom (Functor.commShiftIso (G ⋙ F) a)) Y ≫ Functor.map (shiftFunctor D a) (adj.counit.app Y))
    (adj.counit.app (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) Y) ≫
      NatTrans.app (Iso.hom (Functor.commShiftIso (𝟭 D) a)) Y)
⊢ Eq (α :=
    F.obj (G.obj (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) Y)) ⟶
      Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) Y)
    (CategoryStruct.comp (Y := F.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (G.obj Y)))
      (F.map (NatTrans.app (Iso.hom (Functor.commShiftIso G a)) Y))
      (NatTrans.app (Iso.hom (Functor.commShiftIso F a)) (G.obj Y) ≫ Functor.map (shiftFunctor D a) (adj.counit.app Y)))
    (adj.counit.app (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) Y))

Tactic:
simp only [Functor.comp_obj, Functor.id_obj, Functor.commShiftIso_comp_hom_app, assoc,
    Functor.commShiftIso_id_hom_app, comp_id] at eq

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Category.assoc, CategoryTheory.Functor.commShiftIso_comp_hom_app, CategoryTheory.Category.comp_id, CategoryTheory.Functor.commShiftIso_id_hom_app, CategoryTheory.Functor.id_obj
-- Module: Mathlib.CategoryTheory.Shift.Adjunction
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
G : Functor.{v_2, v_1, u_2, u_1} D C
adj : F ⊣ G
A : Type u_3
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_3} C A
inst_4 : HasShift.{v_2, u_2, u_3} D A
inst_5 : F.CommShift A
inst_6 : G.CommShift A
inst_7 : adj.CommShift A
a : A
Y : D
eq :
  Eq (α :=
    F.obj (G.obj (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) Y)) ⟶
      Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) Y)
    (CategoryStruct.comp (Y := F.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (G.obj Y)))
      (F.map (NatTrans.app (Iso.hom (Functor.commShiftIso G a)) Y))
      (NatTrans.app (Iso.hom (Functor.commShiftIso F a)) (G.obj Y) ≫ Functor.map (shiftFunctor D a) (adj.counit.app Y)))
    (adj.counit.app (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) Y))
⊢ Eq (α :=
    Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) ((G ⋙ F).obj Y) ⟶
      Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (Functor.obj.{v_2, v_2, u_2, u_2} (𝟭 D) Y))
    (Functor.map (shiftFunctor D a) (adj.counit.app Y))
    (CategoryStruct.comp (Y := (shiftFunctor C a ⋙ F).obj (G.obj Y))
      (NatTrans.app (Iso.inv (Functor.commShiftIso F a)) (G.obj Y))
      (F.map (NatTrans.app (Iso.inv (Functor.commShiftIso G a)) Y) ≫
        adj.counit.app (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) Y)))

Tactic:
simp only [← eq, Functor.comp_obj, Functor.id_obj, ← F.map_comp_assoc, Iso.inv_hom_id_app,
    F.map_id, id_comp, Iso.inv_hom_id_app_assoc]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Functor.map_comp_assoc, CategoryTheory.Functor.map_id, CategoryTheory.Functor.id_obj, CategoryTheory.Iso.inv_hom_id_app, CategoryTheory.Iso.inv_hom_id_app_assoc, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Shift.Adjunction
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
G : Functor.{v_2, v_1, u_2, u_1} D C
adj : F ⊣ G
A : Type u_3
inst_2 : AddGroup A
inst_3 : HasShift.{v_1, u_1, u_3} C A
inst_4 : HasShift.{v_2, u_2, u_3} D A
a b : A
h : b + a = 0
inst_5 : F.CommShift A
X : D
rw : a + b + a = 0 + a
rw₁ : a + (b + a) = 0 + a
rw₂ : a + 0 = 0 + a
rw₃ : a + 0 = a
rw₄ rw₅ : a = a
⊢ a + b = 0

Tactic:
rw [← add_left_inj a, add_assoc, h, zero_add, add_zero]

Premises used: add_assoc, add_left_inj, zero_add, add_zero
-- Module: Mathlib.CategoryTheory.Shift.Adjunction
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
G : Functor.{v_2, v_1, u_2, u_1} D C
adj : F ⊣ G
A : Type u_3
inst_2 : AddGroup A
inst_3 : HasShift.{v_1, u_1, u_3} C A
inst_4 : HasShift.{v_2, u_2, u_3} D A
a b : A
h : b + a = 0
inst_5 : F.CommShift A
X : D
rw : b + a = -a + a
rw₁ : 0 = -a + a
rw₂ rw₃ : Eq.{u_3 + 1} (α := A) 0 0
⊢ b = -a

Tactic:
rw [← add_left_inj a, h, neg_add_cancel]

Premises used: add_left_inj, neg_add_cancel
-- Module: Mathlib.CategoryTheory.Shift.Adjunction
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
G : Functor.{v_2, v_1, u_2, u_1} D C
adj : F ⊣ G
A : Type u_3
inst_2 : AddGroup A
inst_3 : HasShift.{v_1, u_1, u_3} C A
inst_4 : HasShift.{v_2, u_2, u_3} D A
a : A
inst_5 : F.CommShift A
X : D
h : -a + a = 0
⊢ Eq (α := (shiftFunctor D a ⋙ G).obj X ⟶ (G ⋙ shiftFunctor C a).obj X) (NatTrans.app (Iso.hom (iso adj a)) X)
    (CategoryStruct.comp (Y :=
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (-a) ⋙ shiftFunctor C a)
        (G.obj (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) X)))
      (NatTrans.app (Iso.inv (shiftFunctorCompIsoId C (-a) a h))
        (G.obj (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) X)))
      (Functor.map (shiftFunctor C a)
          (adj.unit.app
            (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (-a))
              (G.obj (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) X)))) ≫
        CategoryStruct.comp (Y :=
          Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a)
            (G.obj ((F ⋙ shiftFunctor D (-a)).obj (G.obj (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) X)))))
          (Functor.map (shiftFunctor C a)
            (G.map
              (NatTrans.app (Iso.hom (Functor.commShiftIso F (-a)))
                (G.obj (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) X)))))
          (Functor.map (shiftFunctor C a)
              (G.map
                (Functor.map (shiftFunctor D (-a))
                  (adj.counit.app (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) X)))) ≫
            Functor.map (shiftFunctor C a) (G.map (NatTrans.app (Iso.hom (shiftFunctorCompIsoId D a (-a) ⋯)) X)))))

Tactic:
simp [iso, iso', shiftEquiv']

Premises used: CategoryTheory.shiftEquiv', CategoryTheory.Adjunction.RightAdjointCommShift.iso', CategoryTheory.Adjunction.RightAdjointCommShift.iso
-- Module: Mathlib.CategoryTheory.Shift.Adjunction
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
G : Functor.{v_2, v_1, u_2, u_1} D C
adj : F ⊣ G
A : Type u_3
inst_2 : AddGroup A
inst_3 : HasShift.{v_1, u_1, u_3} C A
inst_4 : HasShift.{v_2, u_2, u_3} D A
a b : A
h : b + a = 0
inst_5 : F.CommShift A
Y : D
rw : a + -a = 0
rw₁ rw₂ : Eq.{u_3 + 1} (α := A) 0 0
⊢ a + b = 0

Tactic:
rw [eq_neg_of_add_eq_zero_left h, add_neg_cancel]

Premises used: add_neg_cancel, eq_neg_of_add_eq_zero_left
-- Module: Mathlib.CategoryTheory.Shift.Adjunction
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
G : Functor.{v_2, v_1, u_2, u_1} D C
adj : F ⊣ G
A : Type u_3
inst_2 : AddGroup A
inst_3 : HasShift.{v_1, u_1, u_3} C A
inst_4 : HasShift.{v_2, u_2, u_3} D A
a b : A
h : b + a = 0
inst_5 : F.CommShift A
Y : D
rw : b + a = -a + a
rw₁ : 0 = -a + a
rw₂ rw₃ : Eq.{u_3 + 1} (α := A) 0 0
⊢ b = -a

Tactic:
rw [← add_left_inj a, h, neg_add_cancel]

Premises used: add_left_inj, neg_add_cancel