chore(CategoryTheory/Whiskering): correct the type of some whiskering lemmas (#23698)

RHS of lemmas `whiskerLeft_twice`, `whiskerRight_twice` and `whiskerRight_left` are modified so that the type of the RHS do not abuse the defeq `(F ⋙ G) ⋙ K = F ⋙ G ⋙ K`.

Author: robin-carlier

Mathlib/CategoryTheory/Closed/Functor.lean

@@ -145,7 +145,8 @@ theorem frobeniusMorphism_mate (h : L ⊣ F) (A : C) :
   rw [← F.map_comp, ← F.map_comp]
   simp only [Functor.map_comp]
   apply IsIso.eq_inv_of_inv_hom_id
-  simp only [assoc]
+  simp only [assoc, Functor.associator_inv_app, Functor.associator_hom_app, Functor.comp_obj,
+    curriedTensor_obj_obj, tensorLeft_obj, Functor.map_id, id_comp]
   rw [prodComparison_natural_whiskerLeft, prodComparison_natural_whiskerRight_assoc]
   slice_lhs 2 3 => rw [← prodComparison_comp]
   simp only [assoc]

Mathlib/CategoryTheory/Shift/CommShift.lean

@@ -331,8 +331,8 @@ instance comp [NatTrans.CommShift τ A] [NatTrans.CommShift τ' A] :
 instance whiskerRight [NatTrans.CommShift τ A] :
     NatTrans.CommShift (whiskerRight τ G) A := ⟨fun a => by
   ext X
-  simp only [whiskerRight_twice, comp_app,
-    whiskerRight_app, Functor.comp_map, whiskerLeft_app,
+  simp only [whiskerRight_twice, Functor.associator_hom_app, Functor.associator_inv_app, id_comp,
+    comp_id, comp_app, whiskerRight_app, Functor.comp_map, whiskerLeft_app,
     Functor.commShiftIso_comp_hom_app, Category.assoc,
     ← Functor.commShiftIso_hom_naturality,
     ← G.map_comp_assoc, shift_app_comm]⟩

Mathlib/CategoryTheory/Sites/Equivalence.lean

@@ -265,8 +265,10 @@ lemma PreservesSheafification.transport
   le P Q f hf := by
     rw [← J.W_whiskerLeft_iff (G := G) (K := K)] at hf
     have := K.W_of_preservesSheafification F (whiskerLeft G.op f) hf
-    rwa [whiskerRight_left,
-      K.W_whiskerLeft_iff (G := G) (J := J) (f := whiskerRight f F)] at this
+    rw [whiskerRight_left] at this
+    haveI := K.W.of_postcomp (W' := MorphismProperty.isomorphisms _) _ _ (Iso.isIso_inv _) <|
+      K.W.of_precomp (W' := MorphismProperty.isomorphisms _) _ _ (Iso.isIso_hom _) this
+    rwa [K.W_whiskerLeft_iff (G := G) (J := J) (f := whiskerRight f F)] at this
 
 variable [Functor.IsContinuous.{v₃} G K J] [(G.sheafPushforwardContinuous A K J).EssSurj]
 variable [G.IsCocontinuous K J] {FA : A → A → Type*} {CA : A → Type*}

Mathlib/CategoryTheory/Whiskering.lean

@@ -249,17 +249,21 @@ variable {B : Type u₄} [Category.{v₄} B]
 
 @[simp]
 theorem whiskerLeft_twice (F : B ⥤ C) (G : C ⥤ D) {H K : D ⥤ E} (α : H ⟶ K) :
-    whiskerLeft F (whiskerLeft G α) = whiskerLeft (F ⋙ G) α :=
-  rfl
+    whiskerLeft F (whiskerLeft G α) =
+    (Functor.associator _ _ _).inv ≫ whiskerLeft (F ⋙ G) α ≫ (Functor.associator _ _ _).hom := by
+  aesop_cat
 
 @[simp]
 theorem whiskerRight_twice {H K : B ⥤ C} (F : C ⥤ D) (G : D ⥤ E) (α : H ⟶ K) :
-    whiskerRight (whiskerRight α F) G = whiskerRight α (F ⋙ G) :=
-  rfl
+    whiskerRight (whiskerRight α F) G =
+    (Functor.associator _ _ _).hom ≫ whiskerRight α (F ⋙ G) ≫ (Functor.associator _ _ _).inv := by
+  aesop_cat
 
 theorem whiskerRight_left (F : B ⥤ C) {G H : C ⥤ D} (α : G ⟶ H) (K : D ⥤ E) :
-    whiskerRight (whiskerLeft F α) K = whiskerLeft F (whiskerRight α K) :=
-  rfl
+    whiskerRight (whiskerLeft F α) K =
+    (Functor.associator _ _ _).hom ≫ whiskerLeft F (whiskerRight α K) ≫
+      (Functor.associator _ _ _).inv := by
+  aesop_cat
 
 end