-- Mathlib/CategoryTheory/Shift/Adjunction.lean
lemma commShift_of_rightAdjoint [G.CommShift A] :
    letI := adj.leftAdjointCommShift A
    adj.CommShift A

Proof state:
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{u_5, u_1} C
inst✝⁴ : Category.{u_4, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
A : Type u_3
inst✝³ : AddGroup A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
inst✝ : G.CommShift A
this : F.CommShift A := adj.leftAdjointCommShift A
a : A
⊢ ((𝟭 C).commShiftIso a).hom ≫ whiskerRight adj.unit (shiftFunctor C a) =
    whiskerLeft (shiftFunctor C a) adj.unit ≫ ((F ⋙ G).commShiftIso a).hom

Tactic:
ext X

Result:
case w.h
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{u_5, u_1} C
inst✝⁴ : Category.{u_4, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
A : Type u_3
inst✝³ : AddGroup A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
inst✝ : G.CommShift A
this : F.CommShift A := adj.leftAdjointCommShift A
a : A
X : C
⊢ (((𝟭 C).commShiftIso a).hom ≫ whiskerRight adj.unit (shiftFunctor C a)).app X =
    (whiskerLeft (shiftFunctor C a) adj.unit ≫ ((F ⋙ G).commShiftIso a).hom).app X

Proof state:
case w.h
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{u_5, u_1} C
inst✝⁴ : Category.{u_4, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
A : Type u_3
inst✝³ : AddGroup A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
inst✝ : G.CommShift A
this : F.CommShift A := adj.leftAdjointCommShift A
a : A
X : C
⊢ (((𝟭 C).commShiftIso a).hom ≫ whiskerRight adj.unit (shiftFunctor C a)).app X =
    (whiskerLeft (shiftFunctor C a) adj.unit ≫ ((F ⋙ G).commShiftIso a).hom).app X

Tactic:
dsimp

Result:
case w.h
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{u_5, u_1} C
inst✝⁴ : Category.{u_4, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
A : Type u_3
inst✝³ : AddGroup A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
inst✝ : G.CommShift A
this : F.CommShift A := adj.leftAdjointCommShift A
a : A
X : C
⊢ ((𝟭 C).commShiftIso a).hom.app X ≫ (shiftFunctor C a).map (adj.unit.app X) =
    adj.unit.app ((shiftFunctor C a).obj X) ≫ ((F ⋙ G).commShiftIso a).hom.app X

Proof state:
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{u_5, u_1} C
inst✝⁴ : Category.{u_4, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
A : Type u_3
inst✝³ : AddGroup A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
inst✝ : G.CommShift A
this : F.CommShift A := adj.leftAdjointCommShift A
⊢ adj.CommShift A

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

Result:
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{u_5, u_1} C
inst✝⁴ : Category.{u_4, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
A : Type u_3
inst✝³ : AddGroup A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
inst✝ : G.CommShift A
this : F.CommShift A := adj.leftAdjointCommShift A
a : A
⊢ ((𝟭 C).commShiftIso a).hom ≫ whiskerRight adj.unit (shiftFunctor C a) =
    whiskerLeft (shiftFunctor C a) adj.unit ≫ ((F ⋙ G).commShiftIso a).hom

Proof state:
case w.h
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{u_5, u_1} C
inst✝⁴ : Category.{u_4, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
A : Type u_3
inst✝³ : AddGroup A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
inst✝ : G.CommShift A
this : F.CommShift A := adj.leftAdjointCommShift A
a : A
X : C
⊢ ((𝟭 C).commShiftIso a).hom.app X ≫ (shiftFunctor C a).map (adj.unit.app X) =
    adj.unit.app ((shiftFunctor C a).obj X) ≫ ((F ⋙ G).commShiftIso a).hom.app X

Tactic:
simpa only [Functor.commShiftIso_id_hom_app, Functor.comp_obj, Functor.id_obj, id_comp,
  Functor.commShiftIso_comp_hom_app] using LeftAdjointCommShift.compatibilityUnit_iso adj a X

Result:
no goals

Proof state:
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{u_5, u_1} C
inst✝⁴ : Category.{u_4, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
A : Type u_3
inst✝³ : AddGroup A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
inst✝ : G.CommShift A
⊢ adj.CommShift A

Tactic:
letI := adj.leftAdjointCommShift A

Result:
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{u_5, u_1} C
inst✝⁴ : Category.{u_4, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
A : Type u_3
inst✝³ : AddGroup A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
inst✝ : G.CommShift A
this : F.CommShift A := adj.leftAdjointCommShift A
⊢ adj.CommShift A