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 : 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
obtain :
  ∀ (h : -a + a = 0),
    Eq (α := (G ⋙ shiftFunctor C a).obj Y ⟶ (shiftFunctor D a ⋙ G).obj Y) (NatTrans.app (Iso.inv (iso adj a)) Y)
      (adj.unit.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (G.obj Y)) ≫
        G.map
            (NatTrans.app (Iso.inv (shiftFunctorCompIsoId D (-a) a h))
              (F.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (G.obj Y)))) ≫
          G.map
              (Functor.map (shiftFunctor D a)
                (Functor.map (shiftFunctor D (-a)) (NatTrans.app (Iso.hom (Functor.commShiftIso F a)) (G.obj Y)))) ≫
            G.map
                (Functor.map (shiftFunctor D a)
                  (NatTrans.app (Iso.hom (shiftFunctorCompIsoId D a (-a) ⋯)) (F.obj (G.obj Y)))) ≫
              G.map (Functor.map (shiftFunctor D a) (adj.counit.app Y)))
⊢ Eq (α := (G ⋙ shiftFunctor C a).obj Y ⟶ (shiftFunctor D a ⋙ G).obj Y) (NatTrans.app (Iso.inv (iso adj a)) Y)
    (adj.unit.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (G.obj Y)) ≫
      G.map
          (NatTrans.app (Iso.inv (shiftFunctorCompIsoId D b a h))
            (F.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (G.obj Y)))) ≫
        G.map
            (Functor.map (shiftFunctor D a)
              (Functor.map (shiftFunctor D b) (NatTrans.app (Iso.hom (Functor.commShiftIso F a)) (G.obj Y)))) ≫
          G.map
              (Functor.map (shiftFunctor D a)
                (NatTrans.app (Iso.hom (shiftFunctorCompIsoId D a b ⋯)) (F.obj (G.obj Y)))) ≫
            G.map (Functor.map (shiftFunctor D a) (adj.counit.app Y)))

Tactic:
obtain rfl : b = -a := by rw [← add_left_inj a, h, neg_add_cancel]

Premises used: rfl
-- 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
Y : D
h : -a + a = 0
a₁ :
  G.map
    (Functor.map (shiftFunctor D a)
      (𝟙 ((F ⋙ shiftFunctor D (-a)).obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (G.obj Y)))))
| CategoryStruct.comp (Y :=
    G.obj
      (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a)
        (F.obj
          (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (-a))
            (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (G.obj Y))))))
    (G.map
      (Functor.map (shiftFunctor D a)
        (NatTrans.app (Iso.inv (Functor.commShiftIso F (-a)))
          (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (G.obj Y)))))
    (G.map
      (Functor.map (shiftFunctor D a)
        (NatTrans.app (Iso.hom (Functor.commShiftIso F (-a)))
          (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (G.obj Y)))))

Tactic:
rw [← Functor.map_comp, ← Functor.map_comp, Iso.inv_hom_id_app]

Premises used: CategoryTheory.Functor.map_comp, CategoryTheory.Iso.inv_hom_id_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 : 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
Y : D
h : -a + a = 0
⊢ Eq (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (G.obj Y) ⟶
      G.obj (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) Y))
    (adj.unit.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (G.obj Y)) ≫
      G.map
          (NatTrans.app (Iso.inv (shiftFunctorCompIsoId D (-a) a ⋯))
            (F.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (G.obj Y)))) ≫
        ((G.map
                (Functor.map (shiftFunctor D a)
                  (𝟙 ((F ⋙ shiftFunctor D (-a)).obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (G.obj Y))))) ≫
              G.map
                (Functor.map (shiftFunctor D a)
                  (Functor.map (shiftFunctor D (-a)) (NatTrans.app (Iso.hom (Functor.commShiftIso F a)) (G.obj Y))))) ≫
            G.map
              (Functor.map (shiftFunctor D a)
                (NatTrans.app (Iso.hom (shiftFunctorCompIsoId D a (-a) ⋯)) (F.obj (G.obj Y))))) ≫
          G.map (Functor.map (shiftFunctor D a) (adj.counit.app Y)))
    (adj.unit.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (G.obj Y)) ≫
      G.map
          (NatTrans.app (Iso.inv (shiftFunctorCompIsoId D (-a) a h))
            (F.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (G.obj Y)))) ≫
        G.map
            (Functor.map (shiftFunctor D a)
              (Functor.map (shiftFunctor D (-a)) (NatTrans.app (Iso.hom (Functor.commShiftIso F a)) (G.obj Y)))) ≫
          G.map
              (Functor.map (shiftFunctor D a)
                (NatTrans.app (Iso.hom (shiftFunctorCompIsoId D a (-a) ⋯)) (F.obj (G.obj Y)))) ≫
            G.map (Functor.map (shiftFunctor D a) (adj.counit.app Y)))

Tactic:
simp only [Functor.comp_obj, Functor.map_id, id_comp, assoc]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Category.assoc, CategoryTheory.Functor.map_id, 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
inst_5 : F.CommShift A
a : A
X : C
rw :
  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 D a ⋙ G).obj (F.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) (G.obj (F.obj X))) ≫
          G.map
              (NatTrans.app (Iso.inv (shiftFunctorCompIsoId D (-a) a ⋯))
                (F.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (G.obj (F.obj X))))) ≫
            G.map
                (Functor.map (shiftFunctor D a)
                  (Functor.map (shiftFunctor D (-a))
                    (NatTrans.app (Iso.hom (Functor.commShiftIso F a)) (G.obj (F.obj X))))) ≫
              G.map
                  (Functor.map (shiftFunctor D a)
                    (NatTrans.app (Iso.hom (shiftFunctorCompIsoId D a (-a) ⋯)) (F.obj (G.obj (F.obj X))))) ≫
                G.map (Functor.map (shiftFunctor D a) (adj.counit.app (F.obj X))) :
      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 D a ⋙ G).obj (F.obj X))
    (adj.unit.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ≫
        G.map (NatTrans.app (Iso.hom (Functor.commShiftIso F a)) X) ≫ 𝟙 ((shiftFunctor D a ⋙ G).obj (F.obj X)) :
      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 D a ⋙ G).obj (F.obj X))
⊢ 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 (iso adj a)) (F.obj X)))

Tactic:
rw [← cancel_mono ((RightAdjointCommShift.iso adj a).inv.app _), assoc, assoc,
    Iso.hom_inv_id_app, RightAdjointCommShift.iso_inv_app adj _ _ (neg_add_cancel a)]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.hom_inv_id_app, CategoryTheory.cancel_mono, neg_add_cancel, CategoryTheory.Adjunction.RightAdjointCommShift.iso_inv_app, CategoryTheory.Adjunction.RightAdjointCommShift.iso, CategoryTheory.Iso.inv, 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 : AddGroup 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
a : A
X : C
a₁ :
  Eq (α :=
    F.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ⟶
      Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F.obj X))
    (F.map (Functor.map (shiftFunctor C a) (adj.unit.app X)) ≫
      CategoryStruct.comp (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) (F.obj (G.obj (F.obj X)))))
        (Functor.map (𝟭 D) (NatTrans.app (Iso.hom (Functor.commShiftIso F a)) (G.obj (F.obj X))))
        (NatTrans.app (Iso.inv (shiftFunctorCompIsoId D (-a) a ⋯))
            (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F.obj (G.obj (F.obj X)))) ≫
          Functor.map (shiftFunctor D a)
              (NatTrans.app (Iso.hom (shiftFunctorCompIsoId D a (-a) ⋯)) (F.obj (G.obj (F.obj X)))) ≫
            Functor.map (shiftFunctor D a) (adj.counit.app (F.obj X))))
    (NatTrans.app (Iso.hom (Functor.commShiftIso F a)) X)
⊢ Eq (α :=
    F.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ⟶
      Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F.obj X))
    (F.map (Functor.map (shiftFunctor C a) (adj.unit.app X)) ≫
      NatTrans.app (Iso.inv (shiftFunctorCompIsoId D (-a) a ⋯))
          (F.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (G.obj (F.obj X)))) ≫
        Functor.map (shiftFunctor D a)
            (Functor.map (shiftFunctor D (-a)) (NatTrans.app (Iso.hom (Functor.commShiftIso F a)) (G.obj (F.obj X)))) ≫
          Functor.map (shiftFunctor D a)
              (NatTrans.app (Iso.hom (shiftFunctorCompIsoId D a (-a) ⋯)) (F.obj (G.obj (F.obj X)))) ≫
            Functor.map (shiftFunctor D a) (adj.counit.app (F.obj X)))
    (NatTrans.app (Iso.hom (Functor.commShiftIso F a)) X)

Tactic:
erw [← NatTrans.naturality_assoc]

Premises used: CategoryTheory.NatTrans.naturality_assoc
-- 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
inst_5 : F.CommShift A
a : A
X : C
a₁ :
  Eq (α :=
    F.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ⟶
      Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F.obj X))
    (F.map (Functor.map (shiftFunctor C a) (adj.unit.app X)) ≫
      CategoryStruct.comp (Y := Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F.obj (G.obj (F.obj X))))
        (NatTrans.app (Iso.hom (Functor.commShiftIso F a)) (G.obj (F.obj X)))
        (NatTrans.app (Iso.inv (shiftFunctorCompIsoId D (-a) a ⋯))
            (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F.obj (G.obj (F.obj X)))) ≫
          Functor.map (shiftFunctor D a)
              (NatTrans.app (Iso.hom (shiftFunctorCompIsoId D a (-a) ⋯)) (F.obj (G.obj (F.obj X)))) ≫
            Functor.map (shiftFunctor D a) (adj.counit.app (F.obj X))))
    (NatTrans.app (Iso.hom (Functor.commShiftIso F a)) X)
⊢ Eq (α :=
    F.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ⟶
      Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F.obj X))
    (F.map (Functor.map (shiftFunctor C a) (adj.unit.app X)) ≫
      CategoryStruct.comp (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) (F.obj (G.obj (F.obj X)))))
        (Functor.map (𝟭 D) (NatTrans.app (Iso.hom (Functor.commShiftIso F a)) (G.obj (F.obj X))))
        (NatTrans.app (Iso.inv (shiftFunctorCompIsoId D (-a) a ⋯))
            (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F.obj (G.obj (F.obj X)))) ≫
          Functor.map (shiftFunctor D a)
              (NatTrans.app (Iso.hom (shiftFunctorCompIsoId D a (-a) ⋯)) (F.obj (G.obj (F.obj X)))) ≫
            Functor.map (shiftFunctor D a) (adj.counit.app (F.obj X))))
    (NatTrans.app (Iso.hom (Functor.commShiftIso F a)) X)

Tactic:
dsimp
-- 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
inst_5 : F.CommShift A
⊢ Eq (α := shiftFunctor.{v_2, u_2, u_3} D (A := A) 0 ⋙ G ≅ G ⋙ shiftFunctor.{v_1, u_1, u_3} C (A := A) 0) (iso adj 0)
    (Functor.CommShift.isoZero G A)

Tactic:
CommShift.compatibilityUnit_unique_right adj (F.commShiftIso 0) _ _
      (compatibilityUnit_iso adj 0) ?_

Premises used: CategoryTheory.Adjunction.CommShift.compatibilityUnit_unique_right, CategoryTheory.Adjunction.RightAdjointCommShift.compatibilityUnit_iso, OfNat.ofNat, CategoryTheory.Functor.CommShift.commShiftIso
-- 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
inst_5 : F.CommShift A
refine : CommShift.CompatibilityUnit adj (Functor.commShiftIso F 0) (Functor.CommShift.isoZero G A)
⊢ Eq (α := shiftFunctor.{v_2, u_2, u_3} D (A := A) 0 ⋙ G ≅ G ⋙ shiftFunctor.{v_1, u_1, u_3} C (A := A) 0) (iso adj 0)
    (Functor.CommShift.isoZero G A)

Tactic:
refine CommShift.compatibilityUnit_unique_right adj (F.commShiftIso 0) _ _
      (compatibilityUnit_iso adj 0) ?_

Premises used: CategoryTheory.Adjunction.CommShift.compatibilityUnit_unique_right, CategoryTheory.Adjunction.RightAdjointCommShift.compatibilityUnit_iso, OfNat.ofNat, CategoryTheory.Functor.CommShift.commShiftIso
-- 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
inst_5 : F.CommShift A
rw : CommShift.CompatibilityUnit adj (Functor.CommShift.isoZero F A) (Functor.CommShift.isoZero G A)
⊢ CommShift.CompatibilityUnit adj (Functor.commShiftIso F 0) (Functor.CommShift.isoZero G A)

Tactic:
rw [F.commShiftIso_zero]

Premises used: CategoryTheory.Functor.CommShift.commShiftIso_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
inst_5 : F.CommShift A
⊢ CommShift.CompatibilityUnit adj (Functor.CommShift.isoZero F A) (Functor.CommShift.isoZero G A)

Tactic:
CommShift.compatibilityUnit_isoZero adj

Premises used: CategoryTheory.Adjunction.CommShift.compatibilityUnit_isoZero
-- 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
inst_5 : F.CommShift A
⊢ CommShift.CompatibilityUnit adj (Functor.CommShift.isoZero F A) (Functor.CommShift.isoZero G A)

Tactic:
exact CommShift.compatibilityUnit_isoZero adj

Premises used: CategoryTheory.Adjunction.CommShift.compatibilityUnit_isoZero
-- 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
inst_5 : F.CommShift A
a b : A
⊢ Eq (α := shiftFunctor D (a + b) ⋙ G ≅ G ⋙ shiftFunctor C (a + b)) (iso adj (a + b))
    (Functor.CommShift.isoAdd (iso adj a) (iso adj b))

Tactic:
CommShift.compatibilityUnit_unique_right adj (F.commShiftIso (a + b)) _ _
      (compatibilityUnit_iso adj (a + b)) ?_

Premises used: CategoryTheory.Adjunction.CommShift.compatibilityUnit_unique_right, HAdd.hAdd, CategoryTheory.Adjunction.RightAdjointCommShift.compatibilityUnit_iso, CategoryTheory.Functor.CommShift.commShiftIso
-- 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
inst_5 : F.CommShift A
a b : A
refine :
  CommShift.CompatibilityUnit adj (Functor.commShiftIso F (a + b)) (Functor.CommShift.isoAdd (iso adj a) (iso adj b))
⊢ Eq (α := shiftFunctor D (a + b) ⋙ G ≅ G ⋙ shiftFunctor C (a + b)) (iso adj (a + b))
    (Functor.CommShift.isoAdd (iso adj a) (iso adj b))

Tactic:
refine CommShift.compatibilityUnit_unique_right adj (F.commShiftIso (a + b)) _ _
      (compatibilityUnit_iso adj (a + b)) ?_

Premises used: CategoryTheory.Adjunction.CommShift.compatibilityUnit_unique_right, HAdd.hAdd, CategoryTheory.Adjunction.RightAdjointCommShift.compatibilityUnit_iso, CategoryTheory.Functor.CommShift.commShiftIso
-- 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
inst_5 : F.CommShift A
a b : A
rw :
  CommShift.CompatibilityUnit adj (Functor.CommShift.isoAdd (Functor.commShiftIso F a) (Functor.commShiftIso F b))
    (Functor.CommShift.isoAdd (iso adj a) (iso adj b))
⊢ CommShift.CompatibilityUnit adj (Functor.commShiftIso F (a + b)) (Functor.CommShift.isoAdd (iso adj a) (iso adj b))

Tactic:
rw [F.commShiftIso_add]

Premises used: CategoryTheory.Functor.CommShift.commShiftIso_add
-- 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
inst_5 : F.CommShift A
a b : A
⊢ CommShift.CompatibilityUnit adj (Functor.CommShift.isoAdd (Functor.commShiftIso F a) (Functor.commShiftIso F b))
    (Functor.CommShift.isoAdd (iso adj a) (iso adj b))

Tactic:
CommShift.compatibilityUnit_isoAdd adj _ _ _ _
      (compatibilityUnit_iso adj a) (compatibilityUnit_iso adj b)

Premises used: CategoryTheory.Adjunction.RightAdjointCommShift.compatibilityUnit_iso, CategoryTheory.Adjunction.CommShift.compatibilityUnit_isoAdd
-- 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
inst_5 : F.CommShift A
a b : A
⊢ CommShift.CompatibilityUnit adj (Functor.CommShift.isoAdd (Functor.commShiftIso F a) (Functor.commShiftIso F b))
    (Functor.CommShift.isoAdd (iso adj a) (iso adj b))

Tactic:
exact CommShift.compatibilityUnit_isoAdd adj _ _ _ _
      (compatibilityUnit_iso adj a) (compatibilityUnit_iso adj b)

Premises used: CategoryTheory.Adjunction.RightAdjointCommShift.compatibilityUnit_iso, CategoryTheory.Adjunction.CommShift.compatibilityUnit_isoAdd
-- 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
inst_5 : F.CommShift A
this : G.CommShift A := adj.rightAdjointCommShift A
⊢ adj.CommShift A

Tactic:
CommShift.mk' _ _ ⟨fun a ↦ ?_⟩

Premises used: CategoryTheory.Adjunction.CommShift.mk', CategoryTheory.NatTrans.CommShift.mk
-- 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
inst_5 : F.CommShift A
this : G.CommShift A := adj.rightAdjointCommShift A
refine :
  ∀ (a : A),
    Eq (α := shiftFunctor C a ⋙ 𝟭 C ⟶ (F ⋙ G) ⋙ shiftFunctor C a)
      (Iso.hom (Functor.commShiftIso (𝟭 C) a) ≫ Functor.whiskerRight adj.unit (shiftFunctor C a))
      (Functor.whiskerLeft (shiftFunctor C a) adj.unit ≫ Iso.hom (Functor.commShiftIso (F ⋙ G) a))
⊢ adj.CommShift A

Tactic:
refine CommShift.mk' _ _ ⟨fun a ↦ ?_⟩

Premises used: CategoryTheory.Adjunction.CommShift.mk', CategoryTheory.NatTrans.CommShift.mk
-- 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
inst_5 : F.CommShift A
this : G.CommShift A := adj.rightAdjointCommShift A
a : A
X : C
w :
  Eq (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (G.obj (F.obj X)))
    (NatTrans.app (Iso.hom (Functor.commShiftIso (𝟭 C) a)) X ≫ Functor.map (shiftFunctor C a) (adj.unit.app X) :
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X ⟶
        Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (G.obj (F.obj X)))
    (adj.unit.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ≫
        NatTrans.app (Iso.hom (Functor.commShiftIso (F ⋙ G) a)) X :
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X ⟶
        Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (G.obj (F.obj X)))
⊢ Eq (α := Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a ⋙ 𝟭 C) X ⟶ ((F ⋙ G) ⋙ shiftFunctor C a).obj X)
    (NatTrans.app (Iso.hom (Functor.commShiftIso (𝟭 C) a) ≫ Functor.whiskerRight adj.unit (shiftFunctor C a)) X)
    (NatTrans.app (Functor.whiskerLeft (shiftFunctor C a) adj.unit ≫ Iso.hom (Functor.commShiftIso (F ⋙ G) a)) X)

Tactic:
dsimp