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
a : A
e₁ : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
e₂ : shiftFunctor D a ⋙ G ≅ G ⋙ shiftFunctor C a
h : CompatibilityUnit adj e₁ e₂
Y : D
this :
  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) (G.obj Y)) ⟶
      (shiftFunctor D a ⋙ G).obj (F.obj (G.obj Y)))
    (Functor.map (shiftFunctor C a) (adj.unit.app (G.obj Y)) ≫ e₂.inv.app (F.obj (G.obj Y)))
    (adj.unit.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (G.obj Y)) ≫ G.map (e₁.hom.app (G.obj Y)))
erw :
  e₂.inv.app Y =
    Functor.map (shiftFunctor C a) (adj.unit.app (G.obj Y)) ≫
      (G ⋙ shiftFunctor C a).map (adj.counit.app Y) ≫ e₂.inv.app (Functor.obj.{v_2, v_2, u_2, u_2} (𝟭 D) Y)
⊢ e₂.inv.app Y =
    Functor.map (shiftFunctor C a) (adj.unit.app (G.obj Y)) ≫
      e₂.inv.app (F.obj (G.obj Y)) ≫ G.map (Functor.map (shiftFunctor D a) (adj.counit.app Y))

Tactic:
erw [← e₂.inv.naturality]

Premises used: CategoryTheory.NatTrans.naturality, CategoryTheory.Iso.inv
-- 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
a : A
e₁ : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
e₂ : shiftFunctor D a ⋙ G ≅ G ⋙ shiftFunctor C a
h : CompatibilityUnit adj e₁ e₂
Y : D
this :
  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) (G.obj Y)) ⟶
      (shiftFunctor D a ⋙ G).obj (F.obj (G.obj Y)))
    (Functor.map (shiftFunctor C a) (adj.unit.app (G.obj Y)) ≫ e₂.inv.app (F.obj (G.obj Y)))
    (adj.unit.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (G.obj Y)) ≫ G.map (e₁.hom.app (G.obj Y)))
rw :
  e₂.inv.app Y ≫ e₂.hom.app Y =
    (Functor.map (shiftFunctor C a) (adj.unit.app (G.obj Y)) ≫
        (G ⋙ shiftFunctor C a).map (adj.counit.app Y) ≫ e₂.inv.app (Functor.obj.{v_2, v_2, u_2, u_2} (𝟭 D) Y)) ≫
      e₂.hom.app Y
⊢ e₂.inv.app Y =
    Functor.map (shiftFunctor C a) (adj.unit.app (G.obj Y)) ≫
      (G ⋙ shiftFunctor C a).map (adj.counit.app Y) ≫ e₂.inv.app (Functor.obj.{v_2, v_2, u_2, u_2} (𝟭 D) Y)

Tactic:
rw [← cancel_mono (e₂.hom.app _)]

Premises used: CategoryTheory.cancel_mono, 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
a : A
e₁ : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
e₂ : shiftFunctor D a ⋙ G ≅ G ⋙ shiftFunctor C a
h : CompatibilityUnit adj e₁ e₂
Y : D
this :
  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) (G.obj Y)) ⟶
      (shiftFunctor D a ⋙ G).obj (F.obj (G.obj Y)))
    (Functor.map (shiftFunctor C a) (adj.unit.app (G.obj Y)) ≫ e₂.inv.app (F.obj (G.obj Y)))
    (adj.unit.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (G.obj Y)) ≫ G.map (e₁.hom.app (G.obj Y)))
⊢ e₂.inv.app Y ≫ e₂.hom.app Y =
    (Functor.map (shiftFunctor C a) (adj.unit.app (G.obj Y)) ≫
        (G ⋙ shiftFunctor C a).map (adj.counit.app Y) ≫ e₂.inv.app (Functor.obj.{v_2, v_2, u_2, u_2} (𝟭 D) Y)) ≫
      e₂.hom.app Y

Tactic:
simp only [Functor.comp_obj, Iso.inv_hom_id_app, Functor.id_obj, Functor.comp_map, assoc, comp_id,
    ← (shiftFunctor C a).map_comp, right_triangle_components, Functor.map_id]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Category.assoc, CategoryTheory.shiftFunctor, CategoryTheory.Category.comp_id, CategoryTheory.Functor.map_id, CategoryTheory.Functor.id_obj, CategoryTheory.Functor.map_comp, CategoryTheory.Adjunction.right_triangle_components, CategoryTheory.Iso.inv_hom_id_app, CategoryTheory.Functor.comp_map
-- 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
a : A
e₁ : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
e₂ : shiftFunctor D a ⋙ G ≅ G ⋙ shiftFunctor C a
h : CompatibilityCounit adj e₁ e₂
X : C
⊢ Eq (α :=
    (G ⋙ F).obj (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} (𝟭 D) (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F.obj X)))
    (adj.counit.app (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F.obj X)))
    (F.map (e₂.hom.app (F.obj X)) ≫
      e₁.hom.app (G.obj (F.obj X)) ≫ Functor.map (shiftFunctor D a) (adj.counit.app (F.obj X)))

Tactic:
have := h (F.obj X)
-- 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
a : A
e₁ : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
e₂ : shiftFunctor D a ⋙ G ≅ G ⋙ shiftFunctor C a
h : CompatibilityCounit adj e₁ e₂
X : C
this :
  Eq (α :=
    (G ⋙ F).obj (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} (𝟭 D) (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F.obj X)))
    (adj.counit.app (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F.obj X)))
    (F.map (e₂.hom.app (F.obj X)) ≫
      e₁.hom.app (G.obj (F.obj X)) ≫ Functor.map (shiftFunctor D a) (adj.counit.app (F.obj X)))
⊢ Eq (α :=
    F.obj ((G ⋙ shiftFunctor C a).obj (F.obj X)) ⟶
      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 X)))
    (F.map (e₂.inv.app (F.obj X)) ≫ adj.counit.app (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F.obj X)))
    (e₁.hom.app (G.obj (F.obj X)) ≫ Functor.map (shiftFunctor D a) (adj.counit.app (F.obj X)))

Tactic:
rw [← cancel_epi (F.map (e₂.inv.app _)), ← assoc, ← F.map_comp, Iso.inv_hom_id_app, F.map_id,
    id_comp] at this

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Functor.map, CategoryTheory.Functor.map_id, CategoryTheory.Functor.map_comp, CategoryTheory.Iso.inv_hom_id_app, CategoryTheory.cancel_epi, CategoryTheory.Iso.inv, CategoryTheory.NatTrans.app, 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 : AddMonoid 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
e₁ : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
e₂ : shiftFunctor D a ⋙ G ≅ G ⋙ shiftFunctor C a
h : CompatibilityCounit adj e₁ e₂
X : C
this :
  Eq (α :=
    F.obj ((G ⋙ shiftFunctor C a).obj (F.obj X)) ⟶
      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 X)))
    (F.map (e₂.inv.app (F.obj X)) ≫ adj.counit.app (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F.obj X)))
    (e₁.hom.app (G.obj (F.obj X)) ≫ Functor.map (shiftFunctor D a) (adj.counit.app (F.obj X)))
dsimp :
  e₁.hom.app X =
    F.map (Functor.map (shiftFunctor C a) (adj.unit.app X)) ≫
      F.map (e₂.inv.app (F.obj X)) ≫ adj.counit.app (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F.obj X))
⊢ e₁.hom.app X =
    F.map (Functor.map (shiftFunctor C a) (adj.unit.app X)) ≫
      F.map (e₂.inv.app (F.obj X)) ≫ adj.counit.app (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F.obj X))

Tactic:
dsimp only [Functor.comp_obj, Functor.id_obj]

Premises used: CategoryTheory.Functor.comp_obj, 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
a : A
e₁ : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
e₂ : shiftFunctor D a ⋙ G ≅ G ⋙ shiftFunctor C a
h : CompatibilityCounit adj e₁ e₂
X : C
this :
  Eq (α :=
    F.obj ((G ⋙ shiftFunctor C a).obj (F.obj X)) ⟶
      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 X)))
    (F.map (e₂.inv.app (F.obj X)) ≫ adj.counit.app (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F.obj X)))
    (e₁.hom.app (G.obj (F.obj X)) ≫ Functor.map (shiftFunctor D a) (adj.counit.app (F.obj X)))
rw : e₁.hom.app X = e₁.hom.app X ≫ Functor.map (shiftFunctor D a) (𝟙 (F.obj X))
⊢ e₁.hom.app X =
    F.map (Functor.map (shiftFunctor C a) (adj.unit.app X)) ≫
      F.map (e₂.inv.app (F.obj X)) ≫ adj.counit.app (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F.obj X))

Tactic:
rw [this, dsimp% e₁.hom.naturality_assoc, ← Functor.map_comp, left_triangle_components]

Premises used: CategoryTheory.Functor.map_comp, CategoryTheory.Iso.hom, CategoryTheory.NatTrans.naturality_assoc, CategoryTheory.Adjunction.left_triangle_components
-- 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
a : A
e₁ : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
e₂ : shiftFunctor D a ⋙ G ≅ G ⋙ shiftFunctor C a
h : CompatibilityCounit adj e₁ e₂
X : C
this :
  Eq (α :=
    F.obj ((G ⋙ shiftFunctor C a).obj (F.obj X)) ⟶
      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 X)))
    (F.map (e₂.inv.app (F.obj X)) ≫ adj.counit.app (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F.obj X)))
    (e₁.hom.app (G.obj (F.obj X)) ≫ Functor.map (shiftFunctor D a) (adj.counit.app (F.obj X)))
⊢ e₁.hom.app X = e₁.hom.app X ≫ Functor.map (shiftFunctor D a) (𝟙 (F.obj X))

Tactic:
simp only [Functor.map_id, comp_id]

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.Functor.map_id
-- 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
a : A
e₁ : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
e₂ e₂' : shiftFunctor D a ⋙ G ≅ G ⋙ shiftFunctor C a
h : CompatibilityUnit adj e₁ e₂
h' : CompatibilityUnit adj e₁ e₂'
rw : e₂.symm = e₂'.symm
⊢ e₂ = e₂'

Tactic:
rw [← Iso.symm_eq_iff]

Premises used: CategoryTheory.Iso.symm_eq_iff
-- 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
a : A
e₁ : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
e₂ e₂' : shiftFunctor D a ⋙ G ≅ G ⋙ shiftFunctor C a
h : CompatibilityUnit adj e₁ e₂
h' : CompatibilityUnit adj e₁ e₂'
w : ∀ (x : D), e₂.symm.hom.app x = e₂'.symm.hom.app x
⊢ e₂.symm = e₂'.symm

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
a : A
e₁ : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
e₂ e₂' : shiftFunctor D a ⋙ G ≅ G ⋙ shiftFunctor C a
h : CompatibilityUnit adj e₁ e₂
h' : CompatibilityUnit adj e₁ e₂'
x : D
w : e₂.inv.app x = e₂'.symm.hom.app x
w₁ : e₂.inv.app x = e₂'.inv.app x
w₂ :
  adj.unit.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (G.obj x)) ≫
      G.map (e₁.hom.app (G.obj x)) ≫ G.map (Functor.map (shiftFunctor D a) (adj.counit.app x)) =
    e₂'.inv.app x
w₃ w₄ :
  adj.unit.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (G.obj x)) ≫
      G.map (e₁.hom.app (G.obj x)) ≫ G.map (Functor.map (shiftFunctor D a) (adj.counit.app x)) =
    adj.unit.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (G.obj x)) ≫
      G.map (e₁.hom.app (G.obj x)) ≫ G.map (Functor.map (shiftFunctor D a) (adj.counit.app x))
⊢ e₂.symm.hom.app x = e₂'.symm.hom.app x

Tactic:
rw [Iso.symm_hom, Iso.symm_hom, compatibilityUnit_right adj e₁ e₂ h,
    compatibilityUnit_right adj e₁ e₂' h']

Premises used: CategoryTheory.Iso.symm_hom, CategoryTheory.Adjunction.CommShift.compatibilityUnit_right
-- 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
a : A
e₁ e₁' : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
e₂ : shiftFunctor D a ⋙ G ≅ G ⋙ shiftFunctor C a
h : CompatibilityUnit adj e₁ e₂
h' : CompatibilityUnit adj e₁' e₂
w : ∀ (x : C), e₁.hom.app x = e₁'.hom.app x
⊢ e₁ = e₁'

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
a : A
e₁ e₁' : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
e₂ : shiftFunctor D a ⋙ G ≅ G ⋙ shiftFunctor C a
h : CompatibilityUnit adj e₁ e₂
h' : CompatibilityUnit adj e₁' e₂
x : C
w :
  F.map (Functor.map (shiftFunctor C a) (adj.unit.app x)) ≫
      F.map (e₂.inv.app (F.obj x)) ≫ adj.counit.app (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F.obj x)) =
    e₁'.hom.app x
w₁ w₂ :
  F.map (Functor.map (shiftFunctor C a) (adj.unit.app x)) ≫
      F.map (e₂.inv.app (F.obj x)) ≫ adj.counit.app (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)) ≫
      F.map (e₂.inv.app (F.obj x)) ≫ adj.counit.app (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F.obj x))
⊢ e₁.hom.app x = e₁'.hom.app x

Tactic:
rw [compatibilityCounit_left adj e₁ e₂ (compatibilityCounit_of_compatibilityUnit adj _ _ h),
    compatibilityCounit_left adj e₁' e₂ (compatibilityCounit_of_compatibilityUnit adj _ _ h')]

Premises used: CategoryTheory.Adjunction.CommShift.compatibilityCounit_of_compatibilityUnit, CategoryTheory.Adjunction.CommShift.compatibilityCounit_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 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_3} C A
inst_4 : HasShift.{v_2, u_2, u_3} D A
X : C
⊢ Eq (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor.{v_1, u_1, u_3} C (A := A) 0)
        (Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 C) X) ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor.{v_1, u_1, u_3} C (A := A) 0) ((F ⋙ G).obj X))
    (Functor.map (shiftFunctor.{v_1, u_1, u_3} C (A := A) 0) (adj.unit.app X))
    (adj.unit.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor.{v_1, u_1, u_3} C (A := A) 0) X) ≫
      CategoryStruct.comp (Y := G.obj ((F ⋙ shiftFunctor.{v_2, u_2, u_3} D (A := A) 0).obj X))
        (G.map (NatTrans.app (Iso.hom (Functor.CommShift.isoZero F A)) X))
        (NatTrans.app (Iso.hom (Functor.CommShift.isoZero G A)) (F.obj X)))

Tactic:
simp only [Functor.id_obj, Functor.comp_obj, Functor.CommShift.isoZero_hom_app,
    Functor.map_comp, assoc, unit_naturality_assoc,
    ← cancel_mono ((shiftFunctorZero C A).hom.app _), ← G.map_comp_assoc, Iso.inv_hom_id_app,
    Functor.id_obj, Functor.map_id, id_comp, NatTrans.naturality, Functor.id_map, assoc, comp_id]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Category.assoc, CategoryTheory.Functor.CommShift.isoZero_hom_app, CategoryTheory.Functor.id_map, CategoryTheory.shiftFunctorZero, CategoryTheory.cancel_mono, CategoryTheory.Category.comp_id, CategoryTheory.Functor.map_comp_assoc, CategoryTheory.Functor.map_id, CategoryTheory.NatTrans.naturality, CategoryTheory.Functor.id_obj, CategoryTheory.Functor.map_comp, CategoryTheory.Iso.inv_hom_id_app, CategoryTheory.Iso.hom, CategoryTheory.NatTrans.app, CategoryTheory.Category.id_comp, CategoryTheory.Adjunction.unit_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 : AddMonoid 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
e₁ : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
f₁ : shiftFunctor C b ⋙ F ≅ F ⋙ shiftFunctor D b
e₂ : shiftFunctor D a ⋙ G ≅ G ⋙ shiftFunctor C a
f₂ : shiftFunctor D b ⋙ G ≅ G ⋙ shiftFunctor C b
h : CompatibilityUnit adj e₁ e₂
h' : CompatibilityUnit adj f₁ f₂
X : C
⊢ Eq (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b)
        (Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 C) (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 b)
        ((F ⋙ G).obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)))
    (Functor.map (shiftFunctor C b) (adj.unit.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)))
    (adj.unit.app
        (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b) (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ≫
      G.map (f₁.hom.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ≫
        f₂.hom.app (F.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)))

Tactic:
have := h' (X⟦a⟧)
-- 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
a b : A
e₁ : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
f₁ : shiftFunctor C b ⋙ F ≅ F ⋙ shiftFunctor D b
e₂ : shiftFunctor D a ⋙ G ≅ G ⋙ shiftFunctor C a
f₂ : shiftFunctor D b ⋙ G ≅ G ⋙ shiftFunctor C b
h : CompatibilityUnit adj e₁ e₂
h' : CompatibilityUnit adj f₁ f₂
X : C
this :
  Eq (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b)
        (Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 C) (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 b)
        ((F ⋙ G).obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)))
    (Functor.map (shiftFunctor C b) (adj.unit.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)))
    (adj.unit.app
        (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b) (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ≫
      G.map (f₁.hom.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ≫
        f₂.hom.app (F.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)))
⊢ Eq (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b) (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ⟶
      G.obj
        (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D b)
          (F.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X))))
    (Functor.map (shiftFunctor C b) (adj.unit.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ≫
      f₂.inv.app (F.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)))
    (adj.unit.app
        (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b) (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ≫
      G.map (f₁.hom.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)))

Tactic:
simp only [← cancel_mono (f₂.inv.app _), assoc, Iso.hom_inv_id_app,
    Functor.id_obj, Functor.comp_obj, comp_id] at this

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Category.assoc, CategoryTheory.Iso.hom_inv_id_app, CategoryTheory.cancel_mono, CategoryTheory.Category.comp_id, CategoryTheory.Functor.id_obj, 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 : AddMonoid 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
e₁ : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
f₁ : shiftFunctor C b ⋙ F ≅ F ⋙ shiftFunctor D b
e₂ : shiftFunctor D a ⋙ G ≅ G ⋙ shiftFunctor C a
f₂ : shiftFunctor D b ⋙ G ≅ G ⋙ shiftFunctor C b
h : CompatibilityUnit adj e₁ e₂
h' : CompatibilityUnit adj f₁ f₂
X : C
this :
  Eq (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b) (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ⟶
      G.obj
        (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D b)
          (F.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X))))
    (Functor.map (shiftFunctor C b) (adj.unit.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ≫
      f₂.inv.app (F.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)))
    (adj.unit.app
        (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b) (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ≫
      G.map (f₁.hom.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)))
simp :
  Functor.map (shiftFunctor C (a + b)) (adj.unit.app X) =
    NatTrans.app (Iso.hom (shiftFunctorAdd C a b)) X ≫
      adj.unit.app
          (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b)
            (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ≫
        G.map (f₁.hom.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ≫
          G.map (Functor.map (shiftFunctor D b) (e₁.hom.app X)) ≫
            G.map (NatTrans.app (Iso.inv (shiftFunctorAdd D a b)) (F.obj X)) ≫
              G.map (NatTrans.app (Iso.hom (shiftFunctorAdd D a b)) (F.obj X)) ≫
                f₂.hom.app (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F.obj X)) ≫
                  Functor.map (shiftFunctor C b) (e₂.hom.app (F.obj X)) ≫
                    NatTrans.app (Iso.inv (shiftFunctorAdd C a b)) (G.obj (F.obj X))
⊢ Functor.map (shiftFunctor C (a + b)) (adj.unit.app X) =
    adj.unit.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (a + b)) X) ≫
      G.map ((Functor.CommShift.isoAdd e₁ f₁).hom.app X) ≫ (Functor.CommShift.isoAdd e₂ f₂).hom.app (F.obj X)

Tactic:
simp only [Functor.id_obj, Functor.comp_obj, Functor.CommShift.isoAdd_hom_app,
    Functor.map_comp, assoc, unit_naturality_assoc]

Premises used: CategoryTheory.Functor.CommShift.isoAdd_hom_app, CategoryTheory.Functor.comp_obj, CategoryTheory.Category.assoc, CategoryTheory.Functor.id_obj, CategoryTheory.Functor.map_comp, CategoryTheory.Adjunction.unit_naturality_assoc