-- Mathlib/CategoryTheory/Shift/Adjunction.lean
/-- Constructor for `Adjunction.CommShift`. -/
lemma mk' (h : NatTrans.CommShift adj.unit A) :
    adj.CommShift A where
  commShift_counit := ⟨fun a ↦ by
    ext
    simp only [Functor.comp_obj, Functor.id_obj, NatTrans.comp_app,
      Functor.commShiftIso_comp_hom_app, whiskerRight_app, assoc, whiskerLeft_app,
      Functor.commShiftIso_id_hom_app, comp_id]
    refine (compatibilityCounit_of_compatibilityUnit adj _ _ (fun X ↦ ?_) _).symm
    simpa only [NatTrans.comp_app,
      Functor.commShiftIso_id_hom_app, whiskerRight_app, id_comp,
      Functor.commShiftIso_comp_hom_app] using congr_app (h.shift_comm a) X⟩

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
h : NatTrans.CommShift adj.unit A
a : A
⊢ ((G ⋙ F).commShiftIso a).hom ≫ whiskerRight adj.counit (shiftFunctor D a) =
    whiskerLeft (shiftFunctor D a) adj.counit ≫ ((𝟭 D).commShiftIso a).hom

Tactic:
ext

Result:
case w.h
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
h : NatTrans.CommShift adj.unit A
a : A
x✝ : D
⊢ (((G ⋙ F).commShiftIso a).hom ≫ whiskerRight adj.counit (shiftFunctor D a)).app x✝ =
    (whiskerLeft (shiftFunctor D a) adj.counit ≫ ((𝟭 D).commShiftIso a).hom).app x✝

Proof state:
case w.h
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
h : NatTrans.CommShift adj.unit A
a : A
x✝ : D
⊢ (((G ⋙ F).commShiftIso a).hom ≫ whiskerRight adj.counit (shiftFunctor D a)).app x✝ =
    (whiskerLeft (shiftFunctor D a) adj.counit ≫ ((𝟭 D).commShiftIso a).hom).app x✝

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

Result:
case w.h
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
h : NatTrans.CommShift adj.unit A
a : A
x✝ : D
⊢ F.map ((G.commShiftIso a).hom.app x✝) ≫
      (F.commShiftIso a).hom.app (G.obj x✝) ≫ (shiftFunctor D a).map (adj.counit.app x✝) =
    adj.counit.app ((shiftFunctor D a).obj x✝)

Proof state:
case w.h
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
h : NatTrans.CommShift adj.unit A
a : A
x✝ : D
⊢ F.map ((G.commShiftIso a).hom.app x✝) ≫
      (F.commShiftIso a).hom.app (G.obj x✝) ≫ (shiftFunctor D a).map (adj.counit.app x✝) =
    adj.counit.app ((shiftFunctor D a).obj x✝)

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

Result:
case w.h
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
h : NatTrans.CommShift adj.unit A
a : A
x✝ : D
X : C
⊢ (shiftFunctor C a).map (adj.unit.app X) =
    adj.unit.app ((shiftFunctor C a).obj X) ≫
      G.map ((F.commShiftIso a).hom.app X) ≫ (G.commShiftIso a).hom.app (F.obj X)

Proof state:
case w.h
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
h : NatTrans.CommShift adj.unit A
a : A
x✝ : D
X : C
⊢ (shiftFunctor C a).map (adj.unit.app X) =
    adj.unit.app ((shiftFunctor C a).obj X) ≫
      G.map ((F.commShiftIso a).hom.app X) ≫ (G.commShiftIso a).hom.app (F.obj X)

Tactic:
simpa only [NatTrans.comp_app,
  Functor.commShiftIso_id_hom_app, whiskerRight_app, id_comp,
  Functor.commShiftIso_comp_hom_app] using congr_app (h.shift_comm a) X

Result:
no goals