-- Mathlib/CategoryTheory/Shift/Adjunction.lean
@[reassoc]
lemma shift_counit_app [adj.CommShift A] (a : A) (Y : D) :
    (adj.counit.app Y)⟦a⟧' =
      (F.commShiftIso a).inv.app (G.obj Y) ≫ F.map ((G.commShiftIso a).inv.app Y) ≫
        adj.counit.app (Y⟦a⟧)

Proof state:
C : Type u_1
D : Type u_2
inst✝⁷ : Category.{u_4, u_1} C
inst✝⁶ : Category.{u_5, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
A : Type u_3
inst✝⁵ : AddMonoid A
inst✝⁴ : HasShift C A
inst✝³ : HasShift D A
inst✝² : F.CommShift A
inst✝¹ : G.CommShift A
inst✝ : adj.CommShift A
a : A
Y : D
eq :
  F.map ((G.commShiftIso a).hom.app Y) ≫
      (F.commShiftIso a).hom.app (G.obj Y) ≫ (shiftFunctor D a).map (adj.counit.app Y) =
    adj.counit.app ((shiftFunctor D a).obj Y)
⊢ (shiftFunctor D a).map (adj.counit.app Y) =
    (F.commShiftIso a).inv.app (G.obj Y) ≫
      F.map ((G.commShiftIso a).inv.app Y) ≫ adj.counit.app ((shiftFunctor D a).obj 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]

Result:
no goals

Proof state:
C : Type u_1
D : Type u_2
inst✝⁷ : Category.{u_4, u_1} C
inst✝⁶ : Category.{u_5, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
A : Type u_3
inst✝⁵ : AddMonoid A
inst✝⁴ : HasShift C A
inst✝³ : HasShift D A
inst✝² : F.CommShift A
inst✝¹ : G.CommShift A
inst✝ : adj.CommShift A
a : A
Y : D
⊢ (shiftFunctor D a).map (adj.counit.app Y) =
    (F.commShiftIso a).inv.app (G.obj Y) ≫
      F.map ((G.commShiftIso a).inv.app Y) ≫ adj.counit.app ((shiftFunctor D a).obj Y)

Tactic:
have eq := NatTrans.shift_app_comm adj.counit a Y

Result:
C : Type u_1
D : Type u_2
inst✝⁷ : Category.{u_4, u_1} C
inst✝⁶ : Category.{u_5, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
A : Type u_3
inst✝⁵ : AddMonoid A
inst✝⁴ : HasShift C A
inst✝³ : HasShift D A
inst✝² : F.CommShift A
inst✝¹ : G.CommShift A
inst✝ : adj.CommShift A
a : A
Y : D
eq :
  ((G ⋙ F).commShiftIso a).hom.app Y ≫ (shiftFunctor D a).map (adj.counit.app Y) =
    adj.counit.app ((shiftFunctor D a).obj Y) ≫ ((𝟭 D).commShiftIso a).hom.app Y
⊢ (shiftFunctor D a).map (adj.counit.app Y) =
    (F.commShiftIso a).inv.app (G.obj Y) ≫
      F.map ((G.commShiftIso a).inv.app Y) ≫ adj.counit.app ((shiftFunctor D a).obj Y)

Proof state:
C : Type u_1
D : Type u_2
inst✝⁷ : Category.{u_4, u_1} C
inst✝⁶ : Category.{u_5, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
A : Type u_3
inst✝⁵ : AddMonoid A
inst✝⁴ : HasShift C A
inst✝³ : HasShift D A
inst✝² : F.CommShift A
inst✝¹ : G.CommShift A
inst✝ : adj.CommShift A
a : A
Y : D
eq :
  ((G ⋙ F).commShiftIso a).hom.app Y ≫ (shiftFunctor D a).map (adj.counit.app Y) =
    adj.counit.app ((shiftFunctor D a).obj Y) ≫ ((𝟭 D).commShiftIso a).hom.app Y
⊢ (shiftFunctor D a).map (adj.counit.app Y) =
    (F.commShiftIso a).inv.app (G.obj Y) ≫
      F.map ((G.commShiftIso a).inv.app Y) ≫ adj.counit.app ((shiftFunctor D a).obj 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

Result:
C : Type u_1
D : Type u_2
inst✝⁷ : Category.{u_4, u_1} C
inst✝⁶ : Category.{u_5, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
A : Type u_3
inst✝⁵ : AddMonoid A
inst✝⁴ : HasShift C A
inst✝³ : HasShift D A
inst✝² : F.CommShift A
inst✝¹ : G.CommShift A
inst✝ : adj.CommShift A
a : A
Y : D
eq :
  F.map ((G.commShiftIso a).hom.app Y) ≫
      (F.commShiftIso a).hom.app (G.obj Y) ≫ (shiftFunctor D a).map (adj.counit.app Y) =
    adj.counit.app ((shiftFunctor D a).obj Y)
⊢ (shiftFunctor D a).map (adj.counit.app Y) =
    (F.commShiftIso a).inv.app (G.obj Y) ≫
      F.map ((G.commShiftIso a).inv.app Y) ≫ adj.counit.app ((shiftFunctor D a).obj Y)