Loogle!

Result

Found 283 declarations mentioning CategoryTheory.Functor.whiskeringRight. Of these, only the first 200 are shown.

• CategoryTheory.Functor.whiskeringRight 📋 Mathlib.CategoryTheory.Whiskering
  (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (E : Type u₃) [CategoryTheory.Category.{v₃, u₃} E] : CategoryTheory.Functor (CategoryTheory.Functor D E) (CategoryTheory.Functor (CategoryTheory.Functor C D) (CategoryTheory.Functor C E))
• CategoryTheory.Functor.faithful_whiskeringRight_obj 📋 Mathlib.CategoryTheory.Whiskering
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] {F : CategoryTheory.Functor D E} [F.Faithful] : ((CategoryTheory.Functor.whiskeringRight C D E).obj F).Faithful
• CategoryTheory.Functor.whiskeringRight_obj_id 📋 Mathlib.CategoryTheory.Whiskering
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] : (CategoryTheory.Functor.whiskeringRight E C C).obj (CategoryTheory.Functor.id C) = CategoryTheory.Functor.id (CategoryTheory.Functor E C)
• CategoryTheory.Functor.FullyFaithful.whiskeringRight 📋 Mathlib.CategoryTheory.Whiskering
  {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] {F : CategoryTheory.Functor D E} (hF : F.FullyFaithful) (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] : ((CategoryTheory.Functor.whiskeringRight C D E).obj F).FullyFaithful
• CategoryTheory.Functor.full_whiskeringRight_obj 📋 Mathlib.CategoryTheory.Whiskering
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] {F : CategoryTheory.Functor D E} [F.Faithful] [F.Full] : ((CategoryTheory.Functor.whiskeringRight C D E).obj F).Full
• CategoryTheory.Functor.whiskeringRight_obj_obj 📋 Mathlib.CategoryTheory.Whiskering
  (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (E : Type u₃) [CategoryTheory.Category.{v₃, u₃} E] (H : CategoryTheory.Functor D E) (F : CategoryTheory.Functor C D) : ((CategoryTheory.Functor.whiskeringRight C D E).obj H).obj F = F.comp H
• CategoryTheory.Functor.whiskeringRightObjIdIso 📋 Mathlib.CategoryTheory.Whiskering
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] : (CategoryTheory.Functor.whiskeringRight E C C).obj (CategoryTheory.Functor.id C) ≅ CategoryTheory.Functor.id (CategoryTheory.Functor E C)
• CategoryTheory.Functor.whiskeringRight_obj_map 📋 Mathlib.CategoryTheory.Whiskering
  (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (E : Type u₃) [CategoryTheory.Category.{v₃, u₃} E] (H : CategoryTheory.Functor D E) {X✝ Y✝ : CategoryTheory.Functor C D} (α : X✝ ⟶ Y✝) : ((CategoryTheory.Functor.whiskeringRight C D E).obj H).map α = CategoryTheory.Functor.whiskerRight α H
• CategoryTheory.Functor.whiskeringRight_obj_comp 📋 Mathlib.CategoryTheory.Whiskering
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] {D' : Type u₄} [CategoryTheory.Category.{v₄, u₄} D'] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D D') : ((CategoryTheory.Functor.whiskeringRight E C D).obj F).comp ((CategoryTheory.Functor.whiskeringRight E D D').obj G) = (CategoryTheory.Functor.whiskeringRight E C D').obj (F.comp G)
• CategoryTheory.Functor.whiskeringRightObjCompIso 📋 Mathlib.CategoryTheory.Whiskering
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] {D' : Type u₄} [CategoryTheory.Category.{v₄, u₄} D'] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D D') : ((CategoryTheory.Functor.whiskeringRight E C D).obj F).comp ((CategoryTheory.Functor.whiskeringRight E D D').obj G) ≅ (CategoryTheory.Functor.whiskeringRight E C D').obj (F.comp G)
• CategoryTheory.Functor.FullyFaithful.whiskeringRight_preimage_app 📋 Mathlib.CategoryTheory.Whiskering
  {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] {F : CategoryTheory.Functor D E} (hF : F.FullyFaithful) (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] {X✝ Y✝ : CategoryTheory.Functor C D} (f : ((CategoryTheory.Functor.whiskeringRight C D E).obj F).obj X✝ ⟶ ((CategoryTheory.Functor.whiskeringRight C D E).obj F).obj Y✝) (X : C) : ((hF.whiskeringRight C).preimage f).app X = hF.preimage (f.app X)
• CategoryTheory.Functor.postcompose₂_obj_obj_map_app 📋 Mathlib.CategoryTheory.Whiskering
  {C₁ : Type u_1} {C₂ : Type u_2} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Category.{v_2, u_2} C₂] {E : Type u_7} [CategoryTheory.Category.{v_7, u_7} E] {E' : Type u_8} [CategoryTheory.Category.{v_8, u_8} E'] (X : CategoryTheory.Functor E E') (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ E)) {X✝ Y✝ : C₁} (f : X✝ ⟶ Y✝) (X✝¹ : C₂) : (((CategoryTheory.Functor.postcompose₂.obj X).obj F).map f).app X✝¹ = X.map ((F.map f).app X✝¹)
• CategoryTheory.Functor.whiskeringRight_map_app_app 📋 Mathlib.CategoryTheory.Whiskering
  (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (E : Type u₃) [CategoryTheory.Category.{v₃, u₃} E] {X✝ Y✝ : CategoryTheory.Functor D E} (τ : X✝ ⟶ Y✝) (F : CategoryTheory.Functor C D) (c : C) : (((CategoryTheory.Functor.whiskeringRight C D E).map τ).app F).app c = τ.app (F.obj c)
• CategoryTheory.Functor.whiskeringRightObjIdIso_hom_app_app 📋 Mathlib.CategoryTheory.Whiskering
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (X : CategoryTheory.Functor E C) (X✝ : E) : (CategoryTheory.Functor.whiskeringRightObjIdIso.hom.app X).app X✝ = CategoryTheory.CategoryStruct.id (X.obj X✝)
• CategoryTheory.Functor.whiskeringRightObjIdIso_inv_app_app 📋 Mathlib.CategoryTheory.Whiskering
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (X : CategoryTheory.Functor E C) (X✝ : E) : (CategoryTheory.Functor.whiskeringRightObjIdIso.inv.app X).app X✝ = CategoryTheory.CategoryStruct.id (X.obj X✝)
• CategoryTheory.Functor.postcompose₂_obj_map_app_app 📋 Mathlib.CategoryTheory.Whiskering
  {C₁ : Type u_1} {C₂ : Type u_2} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Category.{v_2, u_2} C₂] {E : Type u_7} [CategoryTheory.Category.{v_7, u_7} E] {E' : Type u_8} [CategoryTheory.Category.{v_8, u_8} E'] (X : CategoryTheory.Functor E E') {X✝ Y✝ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ E)} (α : X✝ ⟶ Y✝) (X✝¹ : C₁) (X✝² : C₂) : (((CategoryTheory.Functor.postcompose₂.obj X).map α).app X✝¹).app X✝² = X.map ((α.app X✝¹).app X✝²)
• CategoryTheory.Functor.postcompose₃_obj_obj_obj_map_app 📋 Mathlib.CategoryTheory.Whiskering
  {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Category.{v_3, u_3} C₃] {E : Type u_7} [CategoryTheory.Category.{v_7, u_7} E] {E' : Type u_8} [CategoryTheory.Category.{v_8, u_8} E'] (X : CategoryTheory.Functor E E') (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ E))) (X✝ : C₁) {X✝¹ Y✝ : C₂} (f : X✝¹ ⟶ Y✝) (X✝² : C₃) : ((((CategoryTheory.Functor.postcompose₃.obj X).obj F).obj X✝).map f).app X✝² = X.map (((F.obj X✝).map f).app X✝²)
• CategoryTheory.Functor.whiskeringLeft₂_obj_obj_obj_map_app 📋 Mathlib.CategoryTheory.Whiskering
  {C₁ : Type u_1} {C₂ : Type u_2} {D₁ : Type u_4} {D₂ : Type u_5} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Category.{v_4, u_4} D₁] [CategoryTheory.Category.{v_5, u_5} D₂] (E : Type u_7) [CategoryTheory.Category.{v_7, u_7} E] (F₁ : CategoryTheory.Functor C₁ D₁) (F₂ : CategoryTheory.Functor C₂ D₂) (X : CategoryTheory.Functor D₁ (CategoryTheory.Functor D₂ E)) {X✝ Y✝ : C₁} (f : X✝ ⟶ Y✝) (X✝¹ : C₂) : (((((CategoryTheory.Functor.whiskeringLeft₂ E).obj F₁).obj F₂).obj X).map f).app X✝¹ = (X.map (F₁.map f)).app (F₂.obj X✝¹)
• CategoryTheory.Functor.whiskeringLeft₃ObjObjObj_obj_obj_map_app 📋 Mathlib.CategoryTheory.Whiskering
  {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {D₁ : Type u_4} {D₂ : Type u_5} {D₃ : Type u_6} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Category.{v_3, u_3} C₃] [CategoryTheory.Category.{v_4, u_4} D₁] [CategoryTheory.Category.{v_5, u_5} D₂] [CategoryTheory.Category.{v_6, u_6} D₃] (E : Type u_7) [CategoryTheory.Category.{v_7, u_7} E] (F₁ : CategoryTheory.Functor C₁ D₁) (F₂ : CategoryTheory.Functor C₂ D₂) (F₃ : CategoryTheory.Functor C₃ D₃) (X : CategoryTheory.Functor D₁ (CategoryTheory.Functor D₂ (CategoryTheory.Functor D₃ E))) (X✝ : C₁) {X✝¹ Y✝ : C₂} (f : X✝¹ ⟶ Y✝) (X✝² : C₃) : ((((CategoryTheory.Functor.whiskeringLeft₃ObjObjObj E F₁ F₂ F₃).obj X).obj X✝).map f).app X✝² = ((X.obj (F₁.obj X✝)).map (F₂.map f)).app (F₃.obj X✝²)
• CategoryTheory.Functor.whiskeringRightObjCompIso_hom_app_app 📋 Mathlib.CategoryTheory.Whiskering
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] {D' : Type u₄} [CategoryTheory.Category.{v₄, u₄} D'] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D D') (X : CategoryTheory.Functor E C) (X✝ : E) : ((F.whiskeringRightObjCompIso G).hom.app X).app X✝ = CategoryTheory.CategoryStruct.id (G.obj (F.obj (X.obj X✝)))
• CategoryTheory.Functor.whiskeringRightObjCompIso_inv_app_app 📋 Mathlib.CategoryTheory.Whiskering
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] {D' : Type u₄} [CategoryTheory.Category.{v₄, u₄} D'] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D D') (X : CategoryTheory.Functor E C) (X✝ : E) : ((F.whiskeringRightObjCompIso G).inv.app X).app X✝ = CategoryTheory.CategoryStruct.id (G.obj (F.obj (X.obj X✝)))
• CategoryTheory.Functor.postcompose₃_obj_obj_map_app_app 📋 Mathlib.CategoryTheory.Whiskering
  {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Category.{v_3, u_3} C₃] {E : Type u_7} [CategoryTheory.Category.{v_7, u_7} E] {E' : Type u_8} [CategoryTheory.Category.{v_8, u_8} E'] (X : CategoryTheory.Functor E E') (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ E))) {X✝ Y✝ : C₁} (f : X✝ ⟶ Y✝) (X✝¹ : C₂) (X✝² : C₃) : ((((CategoryTheory.Functor.postcompose₃.obj X).obj F).map f).app X✝¹).app X✝² = X.map (((F.map f).app X✝¹).app X✝²)
• CategoryTheory.Functor.postcompose₂_map_app_app_app 📋 Mathlib.CategoryTheory.Whiskering
  {C₁ : Type u_1} {C₂ : Type u_2} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Category.{v_2, u_2} C₂] {E : Type u_7} [CategoryTheory.Category.{v_7, u_7} E] {E' : Type u_8} [CategoryTheory.Category.{v_8, u_8} E'] {X✝ Y✝ : CategoryTheory.Functor E E'} (f : X✝ ⟶ Y✝) (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ E)) (c : C₁) (c✝ : C₂) : (((CategoryTheory.Functor.postcompose₂.map f).app F).app c).app c✝ = f.app ((F.obj c).obj c✝)
• CategoryTheory.Functor.whiskeringLeft₂_obj_obj_map_app_app 📋 Mathlib.CategoryTheory.Whiskering
  {C₁ : Type u_1} {C₂ : Type u_2} {D₁ : Type u_4} {D₂ : Type u_5} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Category.{v_4, u_4} D₁] [CategoryTheory.Category.{v_5, u_5} D₂] (E : Type u_7) [CategoryTheory.Category.{v_7, u_7} E] (F₁ : CategoryTheory.Functor C₁ D₁) (F₂ : CategoryTheory.Functor C₂ D₂) {X✝ Y✝ : CategoryTheory.Functor D₁ (CategoryTheory.Functor D₂ E)} (f : X✝ ⟶ Y✝) (X : C₁) (X✝¹ : C₂) : (((((CategoryTheory.Functor.whiskeringLeft₂ E).obj F₁).obj F₂).map f).app X).app X✝¹ = (f.app (F₁.obj X)).app (F₂.obj X✝¹)
• CategoryTheory.Functor.postcompose₃_obj_map_app_app_app 📋 Mathlib.CategoryTheory.Whiskering
  {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Category.{v_3, u_3} C₃] {E : Type u_7} [CategoryTheory.Category.{v_7, u_7} E] {E' : Type u_8} [CategoryTheory.Category.{v_8, u_8} E'] (X : CategoryTheory.Functor E E') {X✝ Y✝ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ E))} (α : X✝ ⟶ Y✝) (X✝¹ : C₁) (X✝² : C₂) (X✝³ : C₃) : ((((CategoryTheory.Functor.postcompose₃.obj X).map α).app X✝¹).app X✝²).app X✝³ = X.map (((α.app X✝¹).app X✝²).app X✝³)
• CategoryTheory.Functor.whiskeringLeft₃_obj_obj_obj_obj_obj_map_app 📋 Mathlib.CategoryTheory.Whiskering
  {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {D₁ : Type u_4} {D₂ : Type u_5} {D₃ : Type u_6} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Category.{v_3, u_3} C₃] [CategoryTheory.Category.{v_4, u_4} D₁] [CategoryTheory.Category.{v_5, u_5} D₂] [CategoryTheory.Category.{v_6, u_6} D₃] (E : Type u_7) [CategoryTheory.Category.{v_7, u_7} E] (F₁ : CategoryTheory.Functor C₁ D₁) (F₂ : CategoryTheory.Functor C₂ D₂) (F₃ : CategoryTheory.Functor C₃ D₃) (X : CategoryTheory.Functor D₁ (CategoryTheory.Functor D₂ (CategoryTheory.Functor D₃ E))) (X✝ : C₁) {X✝¹ Y✝ : C₂} (f : X✝¹ ⟶ Y✝) (X✝² : C₃) : (((((((CategoryTheory.Functor.whiskeringLeft₃ E).obj F₁).obj F₂).obj F₃).obj X).obj X✝).map f).app X✝² = ((X.obj (F₁.obj X✝)).map (F₂.map f)).app (F₃.obj X✝²)
• CategoryTheory.Functor.whiskeringLeft₂_obj_map_app_app_app 📋 Mathlib.CategoryTheory.Whiskering
  {C₁ : Type u_1} {C₂ : Type u_2} {D₁ : Type u_4} {D₂ : Type u_5} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Category.{v_4, u_4} D₁] [CategoryTheory.Category.{v_5, u_5} D₂] (E : Type u_7) [CategoryTheory.Category.{v_7, u_7} E] (F₁ : CategoryTheory.Functor C₁ D₁) {X✝ Y✝ : CategoryTheory.Functor C₂ D₂} (φ : X✝ ⟶ Y✝) (X : CategoryTheory.Functor D₁ (CategoryTheory.Functor D₂ E)) (X✝¹ : C₁) (c : C₂) : (((((CategoryTheory.Functor.whiskeringLeft₂ E).obj F₁).map φ).app X).app X✝¹).app c = (X.obj (F₁.obj X✝¹)).map (φ.app c)
• CategoryTheory.Functor.whiskeringLeft₃ObjObjObj_obj_map_app_app 📋 Mathlib.CategoryTheory.Whiskering
  {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {D₁ : Type u_4} {D₂ : Type u_5} {D₃ : Type u_6} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Category.{v_3, u_3} C₃] [CategoryTheory.Category.{v_4, u_4} D₁] [CategoryTheory.Category.{v_5, u_5} D₂] [CategoryTheory.Category.{v_6, u_6} D₃] (E : Type u_7) [CategoryTheory.Category.{v_7, u_7} E] (F₁ : CategoryTheory.Functor C₁ D₁) (F₂ : CategoryTheory.Functor C₂ D₂) (F₃ : CategoryTheory.Functor C₃ D₃) (X : CategoryTheory.Functor D₁ (CategoryTheory.Functor D₂ (CategoryTheory.Functor D₃ E))) {X✝ Y✝ : C₁} (f : X✝ ⟶ Y✝) (X✝¹ : C₂) (X✝² : C₃) : ((((CategoryTheory.Functor.whiskeringLeft₃ObjObjObj E F₁ F₂ F₃).obj X).map f).app X✝¹).app X✝² = ((X.map (F₁.map f)).app (F₂.obj X✝¹)).app (F₃.obj X✝²)
• CategoryTheory.Functor.whiskeringLeft₃_obj_obj_obj_obj_map_app_app 📋 Mathlib.CategoryTheory.Whiskering
  {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {D₁ : Type u_4} {D₂ : Type u_5} {D₃ : Type u_6} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Category.{v_3, u_3} C₃] [CategoryTheory.Category.{v_4, u_4} D₁] [CategoryTheory.Category.{v_5, u_5} D₂] [CategoryTheory.Category.{v_6, u_6} D₃] (E : Type u_7) [CategoryTheory.Category.{v_7, u_7} E] (F₁ : CategoryTheory.Functor C₁ D₁) (F₂ : CategoryTheory.Functor C₂ D₂) (F₃ : CategoryTheory.Functor C₃ D₃) (X : CategoryTheory.Functor D₁ (CategoryTheory.Functor D₂ (CategoryTheory.Functor D₃ E))) {X✝ Y✝ : C₁} (f : X✝ ⟶ Y✝) (X✝¹ : C₂) (X✝² : C₃) : (((((((CategoryTheory.Functor.whiskeringLeft₃ E).obj F₁).obj F₂).obj F₃).obj X).map f).app X✝¹).app X✝² = ((X.map (F₁.map f)).app (F₂.obj X✝¹)).app (F₃.obj X✝²)
• CategoryTheory.Functor.whiskeringLeft₃ObjObjMap_app 📋 Mathlib.CategoryTheory.Whiskering
  {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {D₁ : Type u_4} {D₂ : Type u_5} {D₃ : Type u_6} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Category.{v_3, u_3} C₃] [CategoryTheory.Category.{v_4, u_4} D₁] [CategoryTheory.Category.{v_5, u_5} D₂] [CategoryTheory.Category.{v_6, u_6} D₃] (E : Type u_7) [CategoryTheory.Category.{v_7, u_7} E] (F₁ : CategoryTheory.Functor C₁ D₁) (F₂ : CategoryTheory.Functor C₂ D₂) {F₃ F₃' : CategoryTheory.Functor C₃ D₃} (τ₃ : F₃ ⟶ F₃') (F : CategoryTheory.Functor D₁ (CategoryTheory.Functor D₂ (CategoryTheory.Functor D₃ E))) : (CategoryTheory.Functor.whiskeringLeft₃ObjObjMap E F₁ F₂ τ₃).app F = F₁.whiskerLeft (F.whiskerLeft (((CategoryTheory.Functor.whiskeringLeft₂ E).obj F₂).map τ₃))
• CategoryTheory.Functor.whiskeringLeft₃ObjObjObj_map_app_app_app 📋 Mathlib.CategoryTheory.Whiskering
  {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {D₁ : Type u_4} {D₂ : Type u_5} {D₃ : Type u_6} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Category.{v_3, u_3} C₃] [CategoryTheory.Category.{v_4, u_4} D₁] [CategoryTheory.Category.{v_5, u_5} D₂] [CategoryTheory.Category.{v_6, u_6} D₃] (E : Type u_7) [CategoryTheory.Category.{v_7, u_7} E] (F₁ : CategoryTheory.Functor C₁ D₁) (F₂ : CategoryTheory.Functor C₂ D₂) (F₃ : CategoryTheory.Functor C₃ D₃) {X✝ Y✝ : CategoryTheory.Functor D₁ (CategoryTheory.Functor D₂ (CategoryTheory.Functor D₃ E))} (f : X✝ ⟶ Y✝) (X : C₁) (X✝¹ : C₂) (X✝² : C₃) : ((((CategoryTheory.Functor.whiskeringLeft₃ObjObjObj E F₁ F₂ F₃).map f).app X).app X✝¹).app X✝² = ((f.app (F₁.obj X)).app (F₂.obj X✝¹)).app (F₃.obj X✝²)
• CategoryTheory.Functor.postcompose₃_map_app_app_app_app 📋 Mathlib.CategoryTheory.Whiskering
  {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Category.{v_3, u_3} C₃] {E : Type u_7} [CategoryTheory.Category.{v_7, u_7} E] {E' : Type u_8} [CategoryTheory.Category.{v_8, u_8} E'] {X✝ Y✝ : CategoryTheory.Functor E E'} (f : X✝ ⟶ Y✝) (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ E))) (c : C₁) (c✝ : C₂) (c✝¹ : C₃) : ((((CategoryTheory.Functor.postcompose₃.map f).app F).app c).app c✝).app c✝¹ = f.app (((F.obj c).obj c✝).obj c✝¹)
• CategoryTheory.Functor.whiskeringLeft₂_map_app_app_app_app 📋 Mathlib.CategoryTheory.Whiskering
  {C₁ : Type u_1} {C₂ : Type u_2} {D₁ : Type u_4} {D₂ : Type u_5} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Category.{v_4, u_4} D₁] [CategoryTheory.Category.{v_5, u_5} D₂] (E : Type u_7) [CategoryTheory.Category.{v_7, u_7} E] {X✝ Y✝ : CategoryTheory.Functor C₁ D₁} (ψ : X✝ ⟶ Y✝) (F₂ : CategoryTheory.Functor C₂ D₂) (X : CategoryTheory.Functor D₁ (CategoryTheory.Functor D₂ E)) (c : C₁) (X✝¹ : C₂) : (((((CategoryTheory.Functor.whiskeringLeft₂ E).map ψ).app F₂).app X).app c).app X✝¹ = (X.map (ψ.app c)).app (F₂.obj X✝¹)
• CategoryTheory.Functor.whiskeringLeft₃Map_app_app 📋 Mathlib.CategoryTheory.Whiskering
  {C₁ : Type u_1} (C₂ : Type u_2) (C₃ : Type u_3) {D₁ : Type u_4} (D₂ : Type u_5) (D₃ : Type u_6) [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Category.{v_3, u_3} C₃] [CategoryTheory.Category.{v_4, u_4} D₁] [CategoryTheory.Category.{v_5, u_5} D₂] [CategoryTheory.Category.{v_6, u_6} D₃] (E : Type u_7) [CategoryTheory.Category.{v_7, u_7} E] {F₁ F₁' : CategoryTheory.Functor C₁ D₁} (τ₁ : F₁ ⟶ F₁') (F₂ : CategoryTheory.Functor C₂ D₂) (F₃ : CategoryTheory.Functor C₃ D₃) : ((CategoryTheory.Functor.whiskeringLeft₃Map C₂ C₃ D₂ D₃ E τ₁).app F₂).app F₃ = ((CategoryTheory.Functor.whiskeringRight D₁ (CategoryTheory.Functor D₂ (CategoryTheory.Functor D₃ E)) (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ E))).obj (((CategoryTheory.Functor.whiskeringLeft₂ E).obj F₂).obj F₃)).whiskerLeft ((CategoryTheory.Functor.whiskeringLeft C₁ D₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ E))).map τ₁)
• CategoryTheory.Functor.whiskeringLeft₃_obj_obj_map_app_app_app_app 📋 Mathlib.CategoryTheory.Whiskering
  {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {D₁ : Type u_4} {D₂ : Type u_5} {D₃ : Type u_6} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Category.{v_3, u_3} C₃] [CategoryTheory.Category.{v_4, u_4} D₁] [CategoryTheory.Category.{v_5, u_5} D₂] [CategoryTheory.Category.{v_6, u_6} D₃] (E : Type u_7) [CategoryTheory.Category.{v_7, u_7} E] (F₁ : CategoryTheory.Functor C₁ D₁) (F₂ : CategoryTheory.Functor C₂ D₂) {X✝ Y✝ : CategoryTheory.Functor C₃ D₃} (τ₃ : X✝ ⟶ Y✝) (F : CategoryTheory.Functor D₁ (CategoryTheory.Functor D₂ (CategoryTheory.Functor D₃ E))) (X : C₁) (X✝¹ : C₂) (c : C₃) : (((((((CategoryTheory.Functor.whiskeringLeft₃ E).obj F₁).obj F₂).map τ₃).app F).app X).app X✝¹).app c = ((F.obj (F₁.obj X)).obj (F₂.obj X✝¹)).map (τ₃.app c)
• CategoryTheory.Functor.whiskeringLeft₃ObjMap_app 📋 Mathlib.CategoryTheory.Whiskering
  {C₁ : Type u_1} {C₂ : Type u_2} (C₃ : Type u_3) {D₁ : Type u_4} {D₂ : Type u_5} (D₃ : Type u_6) [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Category.{v_3, u_3} C₃] [CategoryTheory.Category.{v_4, u_4} D₁] [CategoryTheory.Category.{v_5, u_5} D₂] [CategoryTheory.Category.{v_6, u_6} D₃] (E : Type u_7) [CategoryTheory.Category.{v_7, u_7} E] (F₁ : CategoryTheory.Functor C₁ D₁) {F₂ F₂' : CategoryTheory.Functor C₂ D₂} (τ₂ : F₂ ⟶ F₂') (F₃ : CategoryTheory.Functor C₃ D₃) : (CategoryTheory.Functor.whiskeringLeft₃ObjMap C₃ D₃ E F₁ τ₂).app F₃ = CategoryTheory.Functor.whiskerRight ((CategoryTheory.Functor.whiskeringRight D₁ (CategoryTheory.Functor D₂ (CategoryTheory.Functor D₃ E)) (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ E))).map (((CategoryTheory.Functor.whiskeringLeft₂ E).map τ₂).app F₃)) ((CategoryTheory.Functor.whiskeringLeft C₁ D₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ E))).obj F₁)
• CategoryTheory.Functor.whiskeringLeft₃_obj_obj_obj_map_app_app_app 📋 Mathlib.CategoryTheory.Whiskering
  {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {D₁ : Type u_4} {D₂ : Type u_5} {D₃ : Type u_6} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Category.{v_3, u_3} C₃] [CategoryTheory.Category.{v_4, u_4} D₁] [CategoryTheory.Category.{v_5, u_5} D₂] [CategoryTheory.Category.{v_6, u_6} D₃] (E : Type u_7) [CategoryTheory.Category.{v_7, u_7} E] (F₁ : CategoryTheory.Functor C₁ D₁) (F₂ : CategoryTheory.Functor C₂ D₂) (F₃ : CategoryTheory.Functor C₃ D₃) {X✝ Y✝ : CategoryTheory.Functor D₁ (CategoryTheory.Functor D₂ (CategoryTheory.Functor D₃ E))} (f : X✝ ⟶ Y✝) (X : C₁) (X✝¹ : C₂) (X✝² : C₃) : (((((((CategoryTheory.Functor.whiskeringLeft₃ E).obj F₁).obj F₂).obj F₃).map f).app X).app X✝¹).app X✝² = ((f.app (F₁.obj X)).app (F₂.obj X✝¹)).app (F₃.obj X✝²)
• CategoryTheory.Functor.whiskeringLeft₃_obj_map_app_app_app_app_app 📋 Mathlib.CategoryTheory.Whiskering
  {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {D₁ : Type u_4} {D₂ : Type u_5} {D₃ : Type u_6} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Category.{v_3, u_3} C₃] [CategoryTheory.Category.{v_4, u_4} D₁] [CategoryTheory.Category.{v_5, u_5} D₂] [CategoryTheory.Category.{v_6, u_6} D₃] (E : Type u_7) [CategoryTheory.Category.{v_7, u_7} E] (F₁ : CategoryTheory.Functor C₁ D₁) {X✝ Y✝ : CategoryTheory.Functor C₂ D₂} (τ₂ : X✝ ⟶ Y✝) (F₃ : CategoryTheory.Functor C₃ D₃) (X : CategoryTheory.Functor D₁ (CategoryTheory.Functor D₂ (CategoryTheory.Functor D₃ E))) (X✝¹ : C₁) (c : C₂) (X✝² : C₃) : (((((((CategoryTheory.Functor.whiskeringLeft₃ E).obj F₁).map τ₂).app F₃).app X).app X✝¹).app c).app X✝² = ((X.obj (F₁.obj X✝¹)).map (τ₂.app c)).app (F₃.obj X✝²)
• CategoryTheory.Functor.whiskeringLeft₃_map_app_app_app_app_app_app 📋 Mathlib.CategoryTheory.Whiskering
  {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {D₁ : Type u_4} {D₂ : Type u_5} {D₃ : Type u_6} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Category.{v_3, u_3} C₃] [CategoryTheory.Category.{v_4, u_4} D₁] [CategoryTheory.Category.{v_5, u_5} D₂] [CategoryTheory.Category.{v_6, u_6} D₃] (E : Type u_7) [CategoryTheory.Category.{v_7, u_7} E] {X✝ Y✝ : CategoryTheory.Functor C₁ D₁} (τ₁ : X✝ ⟶ Y✝) (F₂ : CategoryTheory.Functor C₂ D₂) (F₃ : CategoryTheory.Functor C₃ D₃) (X : CategoryTheory.Functor D₁ (CategoryTheory.Functor D₂ (CategoryTheory.Functor D₃ E))) (c : C₁) (X✝¹ : C₂) (X✝² : C₃) : (((((((CategoryTheory.Functor.whiskeringLeft₃ E).map τ₁).app F₂).app F₃).app X).app c).app X✝¹).app X✝² = ((X.map (τ₁.app c)).app (F₂.obj X✝¹)).app (F₃.obj X✝²)
• CategoryTheory.instReflectsIsomorphismsFunctorObjWhiskeringRight 📋 Mathlib.CategoryTheory.Functor.ReflectsIso.Basic
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2} [CategoryTheory.Category.{v_2, u_2} D] {E : Type u_3} [CategoryTheory.Category.{v_3, u_3} E] (F : CategoryTheory.Functor D E) [F.ReflectsIsomorphisms] : ((CategoryTheory.Functor.whiskeringRight C D E).obj F).ReflectsIsomorphisms
• CategoryTheory.Functor.instIsEquivalenceObjWhiskeringRight 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D) [F.IsEquivalence] : ((CategoryTheory.Functor.whiskeringRight E C D).obj F).IsEquivalence
• CategoryTheory.Equivalence.congrRight_functor 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (e : C ≌ D) : e.congrRight.functor = (CategoryTheory.Functor.whiskeringRight E C D).obj e.functor
• CategoryTheory.Equivalence.congrRight_inverse 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (e : C ≌ D) : e.congrRight.inverse = (CategoryTheory.Functor.whiskeringRight E D C).obj e.inverse
• CategoryTheory.Equivalence.congrRightFunctor_map 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (E : Type u₃) [CategoryTheory.Category.{v₃, u₃} E] {e f : C ≌ D} (α : e ⟶ f) : (CategoryTheory.Equivalence.congrRightFunctor E).map α = CategoryTheory.Equivalence.mkHom ((CategoryTheory.Functor.whiskeringRight E C D).map (CategoryTheory.Equivalence.asNatTrans α))
• CategoryTheory.Equivalence.congrRight_counitIso_hom_app 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (e : C ≌ D) (X : CategoryTheory.Functor E D) : e.congrRight.counitIso.hom.app X = CategoryTheory.CategoryStruct.comp (X.associator e.inverse e.functor).hom (CategoryTheory.CategoryStruct.comp (X.whiskerLeft e.counitIso.hom) X.rightUnitor.hom)
• CategoryTheory.Equivalence.congrRight_unitIso_inv_app 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (e : C ≌ D) (X : CategoryTheory.Functor E C) : e.congrRight.unitIso.inv.app X = CategoryTheory.CategoryStruct.comp (X.associator e.functor e.inverse).inv (CategoryTheory.CategoryStruct.comp (X.whiskerLeft e.unitIso.inv) X.rightUnitor.hom)
• CategoryTheory.Equivalence.congrRight_counitIso_inv_app 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (e : C ≌ D) (X : CategoryTheory.Functor E D) : e.congrRight.counitIso.inv.app X = CategoryTheory.CategoryStruct.comp X.rightUnitor.inv (CategoryTheory.CategoryStruct.comp (X.whiskerLeft e.counitIso.inv) (X.associator e.inverse e.functor).inv)
• CategoryTheory.Equivalence.congrRight_unitIso_hom_app 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (e : C ≌ D) (X : CategoryTheory.Functor E C) : e.congrRight.unitIso.hom.app X = CategoryTheory.CategoryStruct.comp X.rightUnitor.inv (CategoryTheory.CategoryStruct.comp (X.whiskerLeft e.unitIso.hom) (X.associator e.functor e.inverse).hom)
• CategoryTheory.Functor.compConstIso 📋 Mathlib.CategoryTheory.Functor.Const
  (J : Type u₁) [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [CategoryTheory.Category.{v₃, u₃} D] (F : CategoryTheory.Functor C D) : F.comp (CategoryTheory.Functor.const J) ≅ (CategoryTheory.Functor.const J).comp ((CategoryTheory.Functor.whiskeringRight J C D).obj F)
• CategoryTheory.Functor.compConstIso_hom_app_app 📋 Mathlib.CategoryTheory.Functor.Const
  (J : Type u₁) [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [CategoryTheory.Category.{v₃, u₃} D] (F : CategoryTheory.Functor C D) (X : C) (X✝ : J) : ((CategoryTheory.Functor.compConstIso J F).hom.app X).app X✝ = CategoryTheory.CategoryStruct.id (F.obj X)
• CategoryTheory.Functor.compConstIso_inv_app_app 📋 Mathlib.CategoryTheory.Functor.Const
  (J : Type u₁) [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [CategoryTheory.Category.{v₃, u₃} D] (F : CategoryTheory.Functor C D) (X : C) (X✝ : J) : ((CategoryTheory.Functor.compConstIso J F).inv.app X).app X✝ = CategoryTheory.CategoryStruct.id (F.obj X)
• CategoryTheory.whiskeringRight_comp_evaluation 📋 Mathlib.CategoryTheory.Products.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor B C) (a : A) : ((CategoryTheory.Functor.whiskeringRight A B C).obj F).comp ((CategoryTheory.evaluation A C).obj a) = ((CategoryTheory.evaluation A B).obj a).comp F
• CategoryTheory.whiskeringRightCompEvaluation 📋 Mathlib.CategoryTheory.Products.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor B C) (a : A) : ((CategoryTheory.Functor.whiskeringRight A B C).obj F).comp ((CategoryTheory.evaluation A C).obj a) ≅ ((CategoryTheory.evaluation A B).obj a).comp F
• CategoryTheory.whiskeringRightCompEvaluation_hom_app 📋 Mathlib.CategoryTheory.Products.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor B C) (a : A) (X : CategoryTheory.Functor A B) : (CategoryTheory.whiskeringRightCompEvaluation F a).hom.app X = CategoryTheory.CategoryStruct.id (F.obj (X.obj a))
• CategoryTheory.whiskeringRightCompEvaluation_inv_app 📋 Mathlib.CategoryTheory.Products.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor B C) (a : A) (X : CategoryTheory.Functor A B) : (CategoryTheory.whiskeringRightCompEvaluation F a).inv.app X = CategoryTheory.CategoryStruct.id (F.obj (X.obj a))
• CategoryTheory.largeCurriedCoyonedaLemma 📋 Mathlib.CategoryTheory.Yoneda
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] : CategoryTheory.coyoneda.rightOp.comp CategoryTheory.coyoneda ≅ (CategoryTheory.evaluation C (Type v₁)).comp ((CategoryTheory.Functor.whiskeringRight (CategoryTheory.Functor C (Type v₁)) (Type v₁) (Type (max u₁ v₁))).obj CategoryTheory.uliftFunctor.{u₁, v₁})
• CategoryTheory.uliftCoyonedaRightOpCompCoyoneda 📋 Mathlib.CategoryTheory.Yoneda
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] : CategoryTheory.uliftCoyoneda.{w, v₁, u₁}.rightOp.comp CategoryTheory.coyoneda ≅ (CategoryTheory.evaluation C (Type (max v₁ w))).comp ((CategoryTheory.Functor.whiskeringRight (CategoryTheory.Functor C (Type (max v₁ w))) (Type (max v₁ w)) (Type (max (max w u₁) v₁))).obj CategoryTheory.uliftFunctor.{u₁, max v₁ w})
• CategoryTheory.largeCurriedYonedaLemma 📋 Mathlib.CategoryTheory.Yoneda
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] : CategoryTheory.yoneda.op.comp CategoryTheory.coyoneda ≅ (CategoryTheory.evaluation Cᵒᵖ (Type v₁)).comp ((CategoryTheory.Functor.whiskeringRight (CategoryTheory.Functor Cᵒᵖ (Type v₁)) (Type v₁) (Type (max u₁ v₁))).obj CategoryTheory.uliftFunctor.{u₁, v₁})
• CategoryTheory.uliftYonedaOpCompCoyoneda 📋 Mathlib.CategoryTheory.Yoneda
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] : CategoryTheory.uliftYoneda.{w, v₁, u₁}.op.comp CategoryTheory.coyoneda ≅ (CategoryTheory.evaluation Cᵒᵖ (Type (max v₁ w))).comp ((CategoryTheory.Functor.whiskeringRight (CategoryTheory.Functor Cᵒᵖ (Type (max v₁ w))) (Type (max v₁ w)) (Type (max (max w u₁) v₁))).obj CategoryTheory.uliftFunctor.{u₁, max v₁ w})
• CategoryTheory.uliftYoneda_map_app 📋 Mathlib.CategoryTheory.Yoneda
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) (X : Cᵒᵖ) : (CategoryTheory.uliftYoneda.{w, v₁, u₁}.map f).app X = TypeCat.ofHom fun x => { down := CategoryTheory.CategoryStruct.comp x.down f }
• CategoryTheory.Limits.colimCoyoneda 📋 Mathlib.CategoryTheory.Limits.HasLimits
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimitsOfShape J C] : CategoryTheory.Limits.colim.op.comp (CategoryTheory.coyoneda.comp ((CategoryTheory.Functor.whiskeringRight C (Type v) (Type (max v u₁))).obj CategoryTheory.uliftFunctor.{u₁, v})) ≅ CategoryTheory.cocones J C
• CategoryTheory.Limits.limYoneda 📋 Mathlib.CategoryTheory.Limits.HasLimits
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasLimitsOfShape J C] : CategoryTheory.Limits.lim.comp (CategoryTheory.yoneda.comp ((CategoryTheory.Functor.whiskeringRight Cᵒᵖ (Type v) (Type (max v u₁))).obj CategoryTheory.uliftFunctor.{u₁, v})) ≅ CategoryTheory.cones J C
• CategoryTheory.ExactFunctor.whiskeringRight_obj_map 📋 Mathlib.CategoryTheory.Limits.ExactFunctor
  (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (E : Type u₃) [CategoryTheory.Category.{v₃, u₃} E] (F : D ⥤ₑ E) {X✝ Y✝ : C ⥤ₑ D} (f : X✝ ⟶ Y✝) : ((CategoryTheory.ExactFunctor.whiskeringRight C D E).obj F).map f = CategoryTheory.ObjectProperty.homMk (CategoryTheory.Functor.whiskerRight f.hom F.obj)
• CategoryTheory.LeftExactFunctor.whiskeringRight_obj_map 📋 Mathlib.CategoryTheory.Limits.ExactFunctor
  (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (E : Type u₃) [CategoryTheory.Category.{v₃, u₃} E] (F : D ⥤ₗ E) {X✝ Y✝ : C ⥤ₗ D} (f : X✝ ⟶ Y✝) : ((CategoryTheory.LeftExactFunctor.whiskeringRight C D E).obj F).map f = CategoryTheory.ObjectProperty.homMk (CategoryTheory.Functor.whiskerRight f.hom F.obj)
• CategoryTheory.RightExactFunctor.whiskeringRight_obj_map 📋 Mathlib.CategoryTheory.Limits.ExactFunctor
  (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (E : Type u₃) [CategoryTheory.Category.{v₃, u₃} E] (F : D ⥤ᵣ E) {X✝ Y✝ : C ⥤ᵣ D} (f : X✝ ⟶ Y✝) : ((CategoryTheory.RightExactFunctor.whiskeringRight C D E).obj F).map f = CategoryTheory.ObjectProperty.homMk (CategoryTheory.Functor.whiskerRight f.hom F.obj)
• CategoryTheory.ExactFunctor.whiskeringRight_map_app 📋 Mathlib.CategoryTheory.Limits.ExactFunctor
  (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (E : Type u₃) [CategoryTheory.Category.{v₃, u₃} E] {F G : D ⥤ₑ E} (η : F ⟶ G) (H : C ⥤ₑ D) : ((CategoryTheory.ExactFunctor.whiskeringRight C D E).map η).app H = CategoryTheory.ObjectProperty.homMk (((CategoryTheory.Functor.whiskeringRight C D E).map η.hom).app H.obj)
• CategoryTheory.LeftExactFunctor.whiskeringRight_map_app 📋 Mathlib.CategoryTheory.Limits.ExactFunctor
  (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (E : Type u₃) [CategoryTheory.Category.{v₃, u₃} E] {F G : D ⥤ₗ E} (η : F ⟶ G) (H : C ⥤ₗ D) : ((CategoryTheory.LeftExactFunctor.whiskeringRight C D E).map η).app H = CategoryTheory.ObjectProperty.homMk (((CategoryTheory.Functor.whiskeringRight C D E).map η.hom).app H.obj)
• CategoryTheory.RightExactFunctor.whiskeringRight_map_app 📋 Mathlib.CategoryTheory.Limits.ExactFunctor
  (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (E : Type u₃) [CategoryTheory.Category.{v₃, u₃} E] {F G : D ⥤ᵣ E} (η : F ⟶ G) (H : C ⥤ᵣ D) : ((CategoryTheory.RightExactFunctor.whiskeringRight C D E).map η).app H = CategoryTheory.ObjectProperty.homMk (((CategoryTheory.Functor.whiskeringRight C D E).map η.hom).app H.obj)
• CategoryTheory.Functor.instAdditiveWhiskeringRight 📋 Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
  {C : Type u_1} {D : Type u_2} {E : Type u_3} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.Category.{v_3, u_3} E] [CategoryTheory.Preadditive E] : (CategoryTheory.Functor.whiskeringRight C D E).Additive
• CategoryTheory.Functor.instAdditiveObjWhiskeringRight 📋 Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
  {C : Type u_1} {D : Type u_2} {E : Type u_3} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.Category.{v_3, u_3} E] [CategoryTheory.Preadditive D] [CategoryTheory.Preadditive E] (F : CategoryTheory.Functor D E) [F.Additive] : ((CategoryTheory.Functor.whiskeringRight C D E).obj F).Additive
• CategoryTheory.Functor.curry_obj_comp_flip 📋 Mathlib.CategoryTheory.Functor.Currying
  {B : Type u₁} [CategoryTheory.Category.{v₁, u₁} B] {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [CategoryTheory.Category.{v₃, u₃} D] {E : Type u₄} [CategoryTheory.Category.{v₄, u₄} E] (F : CategoryTheory.Functor (C × B) D) (G : CategoryTheory.Functor D E) : (CategoryTheory.Functor.curry.obj (F.comp G)).flip = (CategoryTheory.Functor.curry.obj F).flip.comp ((CategoryTheory.Functor.whiskeringRight C D E).obj G)
• CategoryTheory.Functor.curryObjCompIso 📋 Mathlib.CategoryTheory.Functor.Currying
  {B : Type u₁} [CategoryTheory.Category.{v₁, u₁} B] {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [CategoryTheory.Category.{v₃, u₃} D] {E : Type u₄} [CategoryTheory.Category.{v₄, u₄} E] (F : CategoryTheory.Functor (C × B) D) (G : CategoryTheory.Functor D E) : (CategoryTheory.Functor.curry.obj (F.comp G)).flip ≅ (CategoryTheory.Functor.curry.obj F).flip.comp ((CategoryTheory.Functor.whiskeringRight C D E).obj G)
• CategoryTheory.Functor.curryObjCompIso_hom_app_app 📋 Mathlib.CategoryTheory.Functor.Currying
  {B : Type u₁} [CategoryTheory.Category.{v₁, u₁} B] {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [CategoryTheory.Category.{v₃, u₃} D] {E : Type u₄} [CategoryTheory.Category.{v₄, u₄} E] (F : CategoryTheory.Functor (C × B) D) (G : CategoryTheory.Functor D E) (X : B) (X✝ : C) : ((F.curryObjCompIso G).hom.app X).app X✝ = CategoryTheory.CategoryStruct.id (G.obj (F.obj (X✝, X)))
• CategoryTheory.Functor.curryObjCompIso_inv_app_app 📋 Mathlib.CategoryTheory.Functor.Currying
  {B : Type u₁} [CategoryTheory.Category.{v₁, u₁} B] {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [CategoryTheory.Category.{v₃, u₃} D] {E : Type u₄} [CategoryTheory.Category.{v₄, u₄} E] (F : CategoryTheory.Functor (C × B) D) (G : CategoryTheory.Functor D E) (X : B) (X✝ : C) : ((F.curryObjCompIso G).inv.app X).app X✝ = CategoryTheory.CategoryStruct.id (G.obj (F.obj (X✝, X)))
• CategoryTheory.Functor.whiskeringRight₂_obj_obj_map_app 📋 Mathlib.CategoryTheory.Functor.Currying
  (B : Type u₁) [CategoryTheory.Category.{v₁, u₁} B] (C : Type u₂) [CategoryTheory.Category.{v₂, u₂} C] (D : Type u₃) [CategoryTheory.Category.{v₃, u₃} D] (E : Type u₄) [CategoryTheory.Category.{v₄, u₄} E] (X : CategoryTheory.Functor C (CategoryTheory.Functor D E)) (X✝ : CategoryTheory.Functor B C) {X✝¹ Y✝ : CategoryTheory.Functor B D} (g : X✝¹ ⟶ Y✝) (X✝² : B) : ((((CategoryTheory.Functor.whiskeringRight₂ B C D E).obj X).obj X✝).map g).app X✝² = (X.obj (X✝.obj X✝²)).map (g.app X✝²)
• CategoryTheory.Functor.whiskeringRight₂_map_app_app_app 📋 Mathlib.CategoryTheory.Functor.Currying
  (B : Type u₁) [CategoryTheory.Category.{v₁, u₁} B] (C : Type u₂) [CategoryTheory.Category.{v₂, u₂} C] (D : Type u₃) [CategoryTheory.Category.{v₃, u₃} D] (E : Type u₄) [CategoryTheory.Category.{v₄, u₄} E] {X✝ Y✝ : CategoryTheory.Functor C (CategoryTheory.Functor D E)} (f : X✝ ⟶ Y✝) (X : CategoryTheory.Functor B C) (Y : CategoryTheory.Functor B D) (c : B) : ((((CategoryTheory.Functor.whiskeringRight₂ B C D E).map f).app X).app Y).app c = (f.app (X.obj c)).app (Y.obj c)
• CategoryTheory.Functor.whiskeringRight₂_obj_map_app_app 📋 Mathlib.CategoryTheory.Functor.Currying
  (B : Type u₁) [CategoryTheory.Category.{v₁, u₁} B] (C : Type u₂) [CategoryTheory.Category.{v₂, u₂} C] (D : Type u₃) [CategoryTheory.Category.{v₃, u₃} D] (E : Type u₄) [CategoryTheory.Category.{v₄, u₄} E] (X : CategoryTheory.Functor C (CategoryTheory.Functor D E)) {X✝ Y✝ : CategoryTheory.Functor B C} (f : X✝ ⟶ Y✝) (Y : CategoryTheory.Functor B D) (X✝¹ : B) : ((((CategoryTheory.Functor.whiskeringRight₂ B C D E).obj X).map f).app Y).app X✝¹ = (X.map (f.app X✝¹)).app (Y.obj X✝¹)
• CategoryTheory.preservesColimitNatIso 📋 Mathlib.CategoryTheory.Limits.Preserves.Limits
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {J : Type w} [CategoryTheory.Category.{w', w} J] [CategoryTheory.Limits.PreservesColimitsOfShape J G] [CategoryTheory.Limits.HasColimitsOfShape J D] [CategoryTheory.Limits.HasColimitsOfShape J C] : CategoryTheory.Limits.colim.comp G ≅ ((CategoryTheory.Functor.whiskeringRight J C D).obj G).comp CategoryTheory.Limits.colim
• CategoryTheory.preservesLimitNatIso 📋 Mathlib.CategoryTheory.Limits.Preserves.Limits
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {J : Type w} [CategoryTheory.Category.{w', w} J] [CategoryTheory.Limits.PreservesLimitsOfShape J G] [CategoryTheory.Limits.HasLimitsOfShape J D] [CategoryTheory.Limits.HasLimitsOfShape J C] : CategoryTheory.Limits.lim.comp G ≅ ((CategoryTheory.Functor.whiskeringRight J C D).obj G).comp CategoryTheory.Limits.lim
• CategoryTheory.preservesColimitNatIso_hom_app 📋 Mathlib.CategoryTheory.Limits.Preserves.Limits
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {J : Type w} [CategoryTheory.Category.{w', w} J] [CategoryTheory.Limits.PreservesColimitsOfShape J G] [CategoryTheory.Limits.HasColimitsOfShape J D] [CategoryTheory.Limits.HasColimitsOfShape J C] (X : CategoryTheory.Functor J C) : (CategoryTheory.preservesColimitNatIso G).hom.app X = (CategoryTheory.preservesColimitIso G X).hom
• CategoryTheory.preservesColimitNatIso_inv_app 📋 Mathlib.CategoryTheory.Limits.Preserves.Limits
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {J : Type w} [CategoryTheory.Category.{w', w} J] [CategoryTheory.Limits.PreservesColimitsOfShape J G] [CategoryTheory.Limits.HasColimitsOfShape J D] [CategoryTheory.Limits.HasColimitsOfShape J C] (X : CategoryTheory.Functor J C) : (CategoryTheory.preservesColimitNatIso G).inv.app X = (CategoryTheory.preservesColimitIso G X).inv
• CategoryTheory.preservesLimitNatIso_hom_app 📋 Mathlib.CategoryTheory.Limits.Preserves.Limits
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {J : Type w} [CategoryTheory.Category.{w', w} J] [CategoryTheory.Limits.PreservesLimitsOfShape J G] [CategoryTheory.Limits.HasLimitsOfShape J D] [CategoryTheory.Limits.HasLimitsOfShape J C] (X : CategoryTheory.Functor J C) : (CategoryTheory.preservesLimitNatIso G).hom.app X = (CategoryTheory.preservesLimitIso G X).hom
• CategoryTheory.preservesLimitNatIso_inv_app 📋 Mathlib.CategoryTheory.Limits.Preserves.Limits
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {J : Type w} [CategoryTheory.Category.{w', w} J] [CategoryTheory.Limits.PreservesLimitsOfShape J G] [CategoryTheory.Limits.HasLimitsOfShape J D] [CategoryTheory.Limits.HasLimitsOfShape J C] (X : CategoryTheory.Functor J C) : (CategoryTheory.preservesLimitNatIso G).inv.app X = (CategoryTheory.preservesLimitIso G X).inv
• CategoryTheory.Limits.colimCompFlipIsoWhiskerColim 📋 Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] [CategoryTheory.Limits.HasColimitsOfShape J C] : (CategoryTheory.flipFunctor K J C).comp CategoryTheory.Limits.colim ≅ (CategoryTheory.Functor.whiskeringRight K (CategoryTheory.Functor J C) C).obj CategoryTheory.Limits.colim
• CategoryTheory.Limits.colimIsoFlipCompWhiskerColim 📋 Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] [CategoryTheory.Limits.HasColimitsOfShape J C] : CategoryTheory.Limits.colim ≅ (CategoryTheory.flipFunctor J K C).comp ((CategoryTheory.Functor.whiskeringRight K (CategoryTheory.Functor J C) C).obj CategoryTheory.Limits.colim)
• CategoryTheory.Limits.limCompFlipIsoWhiskerLim 📋 Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] [CategoryTheory.Limits.HasLimitsOfShape J C] : (CategoryTheory.flipFunctor K J C).comp CategoryTheory.Limits.lim ≅ (CategoryTheory.Functor.whiskeringRight K (CategoryTheory.Functor J C) C).obj CategoryTheory.Limits.lim
• CategoryTheory.Limits.limIsoFlipCompWhiskerLim 📋 Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] [CategoryTheory.Limits.HasLimitsOfShape J C] : CategoryTheory.Limits.lim ≅ (CategoryTheory.flipFunctor J K C).comp ((CategoryTheory.Functor.whiskeringRight K (CategoryTheory.Functor J C) C).obj CategoryTheory.Limits.lim)
• CategoryTheory.Limits.colimIsoFlipCompWhiskerColim_hom_app_app 📋 Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] [CategoryTheory.Limits.HasColimitsOfShape J C] (X : CategoryTheory.Functor J (CategoryTheory.Functor K C)) (X✝ : K) : (CategoryTheory.Limits.colimIsoFlipCompWhiskerColim.hom.app X).app X✝ = (CategoryTheory.Limits.colimitObjIsoColimitCompEvaluation X X✝).hom
• CategoryTheory.Limits.colimIsoFlipCompWhiskerColim_inv_app_app 📋 Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] [CategoryTheory.Limits.HasColimitsOfShape J C] (X : CategoryTheory.Functor J (CategoryTheory.Functor K C)) (X✝ : K) : (CategoryTheory.Limits.colimIsoFlipCompWhiskerColim.inv.app X).app X✝ = (CategoryTheory.Limits.colimitObjIsoColimitCompEvaluation X X✝).inv
• CategoryTheory.Limits.limIsoFlipCompWhiskerLim_hom_app_app 📋 Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] [CategoryTheory.Limits.HasLimitsOfShape J C] (X : CategoryTheory.Functor J (CategoryTheory.Functor K C)) (X✝ : K) : (CategoryTheory.Limits.limIsoFlipCompWhiskerLim.hom.app X).app X✝ = (CategoryTheory.Limits.limitObjIsoLimitCompEvaluation X X✝).hom
• CategoryTheory.Limits.limIsoFlipCompWhiskerLim_inv_app_app 📋 Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] [CategoryTheory.Limits.HasLimitsOfShape J C] (X : CategoryTheory.Functor J (CategoryTheory.Functor K C)) (X✝ : K) : (CategoryTheory.Limits.limIsoFlipCompWhiskerLim.inv.app X).app X✝ = (CategoryTheory.Limits.limitObjIsoLimitCompEvaluation X X✝).inv
• CategoryTheory.Limits.colimCompFlipIsoWhiskerColim_hom_app_app 📋 Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] [CategoryTheory.Limits.HasColimitsOfShape J C] (X : CategoryTheory.Functor K (CategoryTheory.Functor J C)) (X✝ : K) : (CategoryTheory.Limits.colimCompFlipIsoWhiskerColim.hom.app X).app X✝ = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimitObjIsoColimitCompEvaluation X.flip X✝).hom (CategoryTheory.Limits.HasColimit.isoOfNatIso (CategoryTheory.flipCompEvaluation X X✝)).hom
• CategoryTheory.Limits.colimCompFlipIsoWhiskerColim_inv_app_app 📋 Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] [CategoryTheory.Limits.HasColimitsOfShape J C] (X : CategoryTheory.Functor K (CategoryTheory.Functor J C)) (X✝ : K) : (CategoryTheory.Limits.colimCompFlipIsoWhiskerColim.inv.app X).app X✝ = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.HasColimit.isoOfNatIso (CategoryTheory.flipCompEvaluation X X✝)).inv (CategoryTheory.Limits.colimitObjIsoColimitCompEvaluation X.flip X✝).inv
• CategoryTheory.Limits.limCompFlipIsoWhiskerLim_hom_app_app 📋 Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] [CategoryTheory.Limits.HasLimitsOfShape J C] (X : CategoryTheory.Functor K (CategoryTheory.Functor J C)) (X✝ : K) : (CategoryTheory.Limits.limCompFlipIsoWhiskerLim.hom.app X).app X✝ = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limitObjIsoLimitCompEvaluation X.flip X✝).hom (CategoryTheory.Limits.HasLimit.isoOfNatIso (CategoryTheory.flipCompEvaluation X X✝)).hom
• CategoryTheory.Limits.limCompFlipIsoWhiskerLim_inv_app_app 📋 Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] [CategoryTheory.Limits.HasLimitsOfShape J C] (X : CategoryTheory.Functor K (CategoryTheory.Functor J C)) (X✝ : K) : (CategoryTheory.Limits.limCompFlipIsoWhiskerLim.inv.app X).app X✝ = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.HasLimit.isoOfNatIso (CategoryTheory.flipCompEvaluation X X✝)).inv (CategoryTheory.Limits.limitObjIsoLimitCompEvaluation X.flip X✝).inv
• CategoryTheory.shrinkYonedaUliftFunctorIso 📋 Mathlib.CategoryTheory.ShrinkYoneda
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.LocallySmall.{w, v, u} C] [CategoryTheory.LocallySmall.{max w w', v, u} C] : CategoryTheory.shrinkYoneda.{w, v, u}.comp ((CategoryTheory.Functor.whiskeringRight Cᵒᵖ (Type w) (Type (max w w'))).obj CategoryTheory.uliftFunctor.{w', w}) ≅ CategoryTheory.shrinkYoneda.{max w w', v, u}
• CategoryTheory.shrinkCoyonedaUliftFunctorIso 📋 Mathlib.CategoryTheory.ShrinkYoneda
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.LocallySmall.{w, v, u} C] [CategoryTheory.LocallySmall.{max w w', v, u} C] : CategoryTheory.shrinkCoyoneda.{w, v, u}.comp ((CategoryTheory.Functor.whiskeringRight Cᵒᵖ (Type w) (Type (max w w'))).obj CategoryTheory.uliftFunctor.{w', w}) ≅ CategoryTheory.shrinkCoyoneda.{max w w', v, u}
• CategoryTheory.Equivalence.congrFullSubcategory_counitIso 📋 Mathlib.CategoryTheory.ObjectProperty.Equivalence
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] {P : CategoryTheory.ObjectProperty C} {Q : CategoryTheory.ObjectProperty D} (e : C ≌ D) [Q.IsClosedUnderIsomorphisms] (h : Q.inverseImage e.functor = P) : (e.congrFullSubcategory h).counitIso = (Q.fullyFaithfulι.whiskeringRight Q.FullSubcategory).preimageIso (Q.ι.isoWhiskerLeft e.counitIso)
• CategoryTheory.Equivalence.congrFullSubcategory_unitIso 📋 Mathlib.CategoryTheory.ObjectProperty.Equivalence
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] {P : CategoryTheory.ObjectProperty C} {Q : CategoryTheory.ObjectProperty D} (e : C ≌ D) [Q.IsClosedUnderIsomorphisms] (h : Q.inverseImage e.functor = P) : (e.congrFullSubcategory h).unitIso = (P.fullyFaithfulι.whiskeringRight P.FullSubcategory).preimageIso (P.ι.isoWhiskerLeft e.unitIso)
• CategoryTheory.CartesianMonoidalCategory.prodComparisonBifunctorNatIso 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] [CategoryTheory.CartesianMonoidalCategory D] (F : CategoryTheory.Functor C D) [∀ (A B : C), CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.pair A B) F] : (CategoryTheory.MonoidalCategory.curriedTensor C).comp ((CategoryTheory.Functor.whiskeringRight C C D).obj F) ≅ F.comp ((CategoryTheory.MonoidalCategory.curriedTensor D).comp ((CategoryTheory.Functor.whiskeringLeft C D D).obj F))
• CategoryTheory.CartesianMonoidalCategory.prodComparisonBifunctorNatTrans 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] [CategoryTheory.CartesianMonoidalCategory D] (F : CategoryTheory.Functor C D) : (CategoryTheory.MonoidalCategory.curriedTensor C).comp ((CategoryTheory.Functor.whiskeringRight C C D).obj F) ⟶ F.comp ((CategoryTheory.MonoidalCategory.curriedTensor D).comp ((CategoryTheory.Functor.whiskeringLeft C D D).obj F))
• CategoryTheory.CartesianMonoidalCategory.instIsIsoFunctorProdComparisonBifunctorNatTransOfProdComparison 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] [CategoryTheory.CartesianMonoidalCategory D] (F : CategoryTheory.Functor C D) [∀ (A B : C), CategoryTheory.IsIso (CategoryTheory.CartesianMonoidalCategory.prodComparison F A B)] : CategoryTheory.IsIso (CategoryTheory.CartesianMonoidalCategory.prodComparisonBifunctorNatTrans F)
• CategoryTheory.CartesianMonoidalCategory.prodComparisonBifunctorNatTrans_app 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] [CategoryTheory.CartesianMonoidalCategory D] (F : CategoryTheory.Functor C D) (A : C) : (CategoryTheory.CartesianMonoidalCategory.prodComparisonBifunctorNatTrans F).app A = CategoryTheory.CartesianMonoidalCategory.prodComparisonNatTrans F A
• CategoryTheory.CartesianMonoidalCategory.prodComparisonBifunctorNatIso_hom 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] [CategoryTheory.CartesianMonoidalCategory D] (F : CategoryTheory.Functor C D) [∀ (A B : C), CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.pair A B) F] : (CategoryTheory.CartesianMonoidalCategory.prodComparisonBifunctorNatIso F).hom = CategoryTheory.CartesianMonoidalCategory.prodComparisonBifunctorNatTrans F
• CategoryTheory.CartesianMonoidalCategory.prodComparisonBifunctorNatIso_inv 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] [CategoryTheory.CartesianMonoidalCategory D] (F : CategoryTheory.Functor C D) [∀ (A B : C), CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.pair A B) F] : (CategoryTheory.CartesianMonoidalCategory.prodComparisonBifunctorNatIso F).inv = CategoryTheory.inv (CategoryTheory.CartesianMonoidalCategory.prodComparisonBifunctorNatTrans F)
• CategoryTheory.CartesianMonoidalCategory.prodComparisonBifunctorNatTrans_comp 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] [CategoryTheory.CartesianMonoidalCategory D] (F : CategoryTheory.Functor C D) {E : Type u₂} [CategoryTheory.Category.{v₂, u₂} E] [CategoryTheory.CartesianMonoidalCategory E] (G : CategoryTheory.Functor D E) : CategoryTheory.CartesianMonoidalCategory.prodComparisonBifunctorNatTrans (F.comp G) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight (CategoryTheory.CartesianMonoidalCategory.prodComparisonBifunctorNatTrans F) ((CategoryTheory.Functor.whiskeringRight C D E).obj G)) (F.whiskerLeft (CategoryTheory.Functor.whiskerRight (CategoryTheory.CartesianMonoidalCategory.prodComparisonBifunctorNatTrans G) ((CategoryTheory.Functor.whiskeringLeft C D E).obj F)))
• AddCommGrpCat.coyonedaForget 📋 Mathlib.Algebra.Category.Grp.Yoneda
  : AddCommGrpCat.coyoneda.comp ((CategoryTheory.Functor.whiskeringRight AddCommGrpCat AddCommGrpCat (Type u_1)).obj (CategoryTheory.forget AddCommGrpCat)) ≅ CategoryTheory.coyoneda
• CommGrpCat.coyonedaForget 📋 Mathlib.Algebra.Category.Grp.Yoneda
  : CommGrpCat.coyoneda.comp ((CategoryTheory.Functor.whiskeringRight CommGrpCat CommGrpCat (Type u_1)).obj (CategoryTheory.forget CommGrpCat)) ≅ CategoryTheory.coyoneda
• AddCommGrpCat.coyonedaForget_inv_app_app_hom_apply 📋 Mathlib.Algebra.Category.Grp.Yoneda
  (X : AddCommGrpCatᵒᵖ) (X✝ : AddCommGrpCat) (f : Opposite.unop X ⟶ X✝) : (CategoryTheory.ConcreteCategory.hom ((AddCommGrpCat.coyonedaForget.inv.app X).app X✝)) f = AddCommGrpCat.Hom.hom f
• CommGrpCat.coyonedaForget_inv_app_app_hom_apply 📋 Mathlib.Algebra.Category.Grp.Yoneda
  (X : CommGrpCatᵒᵖ) (X✝ : CommGrpCat) (f : Opposite.unop X ⟶ X✝) : (CategoryTheory.ConcreteCategory.hom ((CommGrpCat.coyonedaForget.inv.app X).app X✝)) f = CommGrpCat.Hom.hom f
• AddCommGrpCat.coyonedaForget_hom_app_app_hom_apply_hom 📋 Mathlib.Algebra.Category.Grp.Yoneda
  (X : AddCommGrpCatᵒᵖ) (X✝ : AddCommGrpCat) (f : ↑(Opposite.unop X) →+ ↑X✝) : AddCommGrpCat.Hom.hom ((CategoryTheory.ConcreteCategory.hom ((AddCommGrpCat.coyonedaForget.hom.app X).app X✝)) f) = f
• CommGrpCat.coyonedaForget_hom_app_app_hom_apply_hom 📋 Mathlib.Algebra.Category.Grp.Yoneda
  (X : CommGrpCatᵒᵖ) (X✝ : CommGrpCat) (f : ↑(Opposite.unop X) →* ↑X✝) : CommGrpCat.Hom.hom ((CategoryTheory.ConcreteCategory.hom ((CommGrpCat.coyonedaForget.hom.app X).app X✝)) f) = f
• CategoryTheory.whiskering_preadditiveCoyoneda 📋 Mathlib.CategoryTheory.Preadditive.Yoneda.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] : CategoryTheory.preadditiveCoyoneda.comp ((CategoryTheory.Functor.whiskeringRight C AddCommGrpCat (Type v)).obj (CategoryTheory.forget AddCommGrpCat)) = CategoryTheory.coyoneda
• CategoryTheory.whiskering_preadditiveYoneda 📋 Mathlib.CategoryTheory.Preadditive.Yoneda.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] : CategoryTheory.preadditiveYoneda.comp ((CategoryTheory.Functor.whiskeringRight Cᵒᵖ AddCommGrpCat (Type v)).obj (CategoryTheory.forget AddCommGrpCat)) = CategoryTheory.yoneda
• CategoryTheory.whiskering_linearCoyoneda 📋 Mathlib.CategoryTheory.Linear.Yoneda
  (R : Type w) [Ring R] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] : (CategoryTheory.linearCoyoneda R C).comp ((CategoryTheory.Functor.whiskeringRight C (ModuleCat R) (Type v)).obj (CategoryTheory.forget (ModuleCat R))) = CategoryTheory.coyoneda
• CategoryTheory.whiskering_linearYoneda 📋 Mathlib.CategoryTheory.Linear.Yoneda
  (R : Type w) [Ring R] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] : (CategoryTheory.linearYoneda R C).comp ((CategoryTheory.Functor.whiskeringRight Cᵒᵖ (ModuleCat R) (Type v)).obj (CategoryTheory.forget (ModuleCat R))) = CategoryTheory.yoneda
• CategoryTheory.whiskering_linearCoyoneda₂ 📋 Mathlib.CategoryTheory.Linear.Yoneda
  (R : Type w) [Ring R] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] : (CategoryTheory.linearCoyoneda R C).comp ((CategoryTheory.Functor.whiskeringRight C (ModuleCat R) AddCommGrpCat).obj (CategoryTheory.forget₂ (ModuleCat R) AddCommGrpCat)) = CategoryTheory.preadditiveCoyoneda
• CategoryTheory.whiskering_linearYoneda₂ 📋 Mathlib.CategoryTheory.Linear.Yoneda
  (R : Type w) [Ring R] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] : (CategoryTheory.linearYoneda R C).comp ((CategoryTheory.Functor.whiskeringRight Cᵒᵖ (ModuleCat R) AddCommGrpCat).obj (CategoryTheory.forget₂ (ModuleCat R) AddCommGrpCat)) = CategoryTheory.preadditiveYoneda
• CategoryTheory.Limits.whiskeringLimYonedaIsoCones 📋 Mathlib.CategoryTheory.Limits.Types.Yoneda
  (J : Type v) [CategoryTheory.SmallCategory J] (C : Type u) [CategoryTheory.Category.{v, u} C] : (CategoryTheory.Functor.whiskeringLeft J C (Type v)).comp (((CategoryTheory.Functor.whiskeringRight (CategoryTheory.Functor C (Type v)) (CategoryTheory.Functor J (Type v)) (Type v)).obj CategoryTheory.Limits.lim).comp ((CategoryTheory.Functor.whiskeringLeft Cᵒᵖ (CategoryTheory.Functor C (Type v)) (Type v)).obj CategoryTheory.coyoneda)) ≅ CategoryTheory.cones J C
• CategoryTheory.Limits.opHomCompWhiskeringLimYonedaIsoCocones 📋 Mathlib.CategoryTheory.Limits.Types.Yoneda
  (J : Type v) [CategoryTheory.SmallCategory J] (C : Type u) [CategoryTheory.Category.{v, u} C] : (CategoryTheory.Functor.opHom J C).comp ((CategoryTheory.Functor.whiskeringLeft Jᵒᵖ Cᵒᵖ (Type v)).comp (((CategoryTheory.Functor.whiskeringRight (CategoryTheory.Functor Cᵒᵖ (Type v)) (CategoryTheory.Functor Jᵒᵖ (Type v)) (Type v)).obj CategoryTheory.Limits.lim).comp ((CategoryTheory.Functor.whiskeringLeft C (CategoryTheory.Functor Cᵒᵖ (Type v)) (Type v)).obj CategoryTheory.yoneda))) ≅ CategoryTheory.cocones J C
• CategoryTheory.Limits.whiskeringLimYonedaIsoCones_hom_app_app_hom_apply_app 📋 Mathlib.CategoryTheory.Limits.Types.Yoneda
  (J : Type v) [CategoryTheory.SmallCategory J] (C : Type u) [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.Functor J C) (X✝ : Cᵒᵖ) (a : CategoryTheory.Limits.limit (X.comp (CategoryTheory.coyoneda.obj (Opposite.op (Opposite.unop X✝))))) (j : J) : ((CategoryTheory.ConcreteCategory.hom (((CategoryTheory.Limits.whiskeringLimYonedaIsoCones J C).hom.app X).app X✝)) a).app j = (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.limit.π (X.comp (CategoryTheory.coyoneda.obj X✝)) j)) a
• CategoryTheory.Limits.whiskeringLimYonedaIsoCones_inv_app_app_hom_apply 📋 Mathlib.CategoryTheory.Limits.Types.Yoneda
  (J : Type v) [CategoryTheory.SmallCategory J] (C : Type u) [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.Functor J C) (X✝ : Cᵒᵖ) (t : (CategoryTheory.Functor.const J).obj (Opposite.unop X✝) ⟶ X) : (CategoryTheory.ConcreteCategory.hom (((CategoryTheory.Limits.whiskeringLimYonedaIsoCones J C).inv.app X).app X✝)) t = (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.limit.lift (X.comp (CategoryTheory.coyoneda.obj X✝)) (CategoryTheory.Limits.Types.coneOfSection ⋯))) PUnit.unit
• CategoryTheory.Limits.opHomCompWhiskeringLimYonedaIsoCocones_hom_app_app_hom_apply_app 📋 Mathlib.CategoryTheory.Limits.Types.Yoneda
  (J : Type v) [CategoryTheory.SmallCategory J] (C : Type u) [CategoryTheory.Category.{v, u} C] (X : (CategoryTheory.Functor J C)ᵒᵖ) (X✝ : C) (a : CategoryTheory.Limits.limit ((Opposite.unop X).op.comp (CategoryTheory.yoneda.obj X✝))) (j : J) : ((CategoryTheory.ConcreteCategory.hom (((CategoryTheory.Limits.opHomCompWhiskeringLimYonedaIsoCocones J C).hom.app X).app X✝)) a).app j = (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.limit.π ((Opposite.unop X).op.comp (CategoryTheory.yoneda.obj X✝)) (Opposite.op j))) a
• CategoryTheory.Limits.opHomCompWhiskeringLimYonedaIsoCocones_inv_app_app_hom_apply 📋 Mathlib.CategoryTheory.Limits.Types.Yoneda
  (J : Type v) [CategoryTheory.SmallCategory J] (C : Type u) [CategoryTheory.Category.{v, u} C] (X : (CategoryTheory.Functor J C)ᵒᵖ) (X✝ : C) (t : Opposite.unop X ⟶ (CategoryTheory.Functor.const J).obj X✝) : (CategoryTheory.ConcreteCategory.hom (((CategoryTheory.Limits.opHomCompWhiskeringLimYonedaIsoCocones J C).inv.app X).app X✝)) t = (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.limit.lift ((Opposite.unop X).op.comp (CategoryTheory.yoneda.obj X✝)) (CategoryTheory.Limits.Types.coneOfSection ⋯))) PUnit.unit
• CategoryTheory.Functor.LeftExtension.postcompose₂_obj_hom_app 📋 Mathlib.CategoryTheory.Functor.KanExtension.Basic
  {C : Type u_1} {H : Type u_3} {D : Type u_5} {D' : Type u_6} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_3, u_3} H] [CategoryTheory.Category.{v_5, u_5} D] [CategoryTheory.Category.{v_6, u_6} D'] (L : CategoryTheory.Functor C D) (F : CategoryTheory.Functor C H) (G : CategoryTheory.Functor H D') (X : CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit F) ((CategoryTheory.Functor.whiskeringLeft C D H).obj L)) (X✝ : C) : ((CategoryTheory.Functor.LeftExtension.postcompose₂ L F G).obj X).hom.app X✝ = G.map (X.hom.app X✝)
• CategoryTheory.Functor.RightExtension.postcompose₂_obj_hom_app 📋 Mathlib.CategoryTheory.Functor.KanExtension.Basic
  {C : Type u_1} {H : Type u_3} {D : Type u_5} {D' : Type u_6} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_3, u_3} H] [CategoryTheory.Category.{v_5, u_5} D] [CategoryTheory.Category.{v_6, u_6} D'] (L : CategoryTheory.Functor C D) (F : CategoryTheory.Functor C H) (G : CategoryTheory.Functor H D') (X : CategoryTheory.Comma ((CategoryTheory.Functor.whiskeringLeft C D H).obj L) (CategoryTheory.Functor.fromPUnit F)) (X✝ : C) : ((CategoryTheory.Functor.RightExtension.postcompose₂ L F G).obj X).hom.app X✝ = G.map (X.hom.app X✝)
• CategoryTheory.Functor.LeftExtension.postcompose₂_map_left 📋 Mathlib.CategoryTheory.Functor.KanExtension.Basic
  {C : Type u_1} {H : Type u_3} {D : Type u_5} {D' : Type u_6} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_3, u_3} H] [CategoryTheory.Category.{v_5, u_5} D] [CategoryTheory.Category.{v_6, u_6} D'] (L : CategoryTheory.Functor C D) (F : CategoryTheory.Functor C H) (G : CategoryTheory.Functor H D') {X Y : CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit F) ((CategoryTheory.Functor.whiskeringLeft C D H).obj L)} (φ : X ⟶ Y) : ((CategoryTheory.Functor.LeftExtension.postcompose₂ L F G).map φ).left = CategoryTheory.CategoryStruct.id X.left
• CategoryTheory.Functor.RightExtension.postcompose₂_map_right 📋 Mathlib.CategoryTheory.Functor.KanExtension.Basic
  {C : Type u_1} {H : Type u_3} {D : Type u_5} {D' : Type u_6} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_3, u_3} H] [CategoryTheory.Category.{v_5, u_5} D] [CategoryTheory.Category.{v_6, u_6} D'] (L : CategoryTheory.Functor C D) (F : CategoryTheory.Functor C H) (G : CategoryTheory.Functor H D') {X Y : CategoryTheory.Comma ((CategoryTheory.Functor.whiskeringLeft C D H).obj L) (CategoryTheory.Functor.fromPUnit F)} (φ : X ⟶ Y) : ((CategoryTheory.Functor.RightExtension.postcompose₂ L F G).map φ).right = CategoryTheory.CategoryStruct.id X.right
• CategoryTheory.Functor.LeftExtension.postcompose₂_map_right_app 📋 Mathlib.CategoryTheory.Functor.KanExtension.Basic
  {C : Type u_1} {H : Type u_3} {D : Type u_5} {D' : Type u_6} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_3, u_3} H] [CategoryTheory.Category.{v_5, u_5} D] [CategoryTheory.Category.{v_6, u_6} D'] (L : CategoryTheory.Functor C D) (F : CategoryTheory.Functor C H) (G : CategoryTheory.Functor H D') {X Y : CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit F) ((CategoryTheory.Functor.whiskeringLeft C D H).obj L)} (φ : X ⟶ Y) (X✝ : D) : ((CategoryTheory.Functor.LeftExtension.postcompose₂ L F G).map φ).right.app X✝ = G.map (φ.right.app X✝)
• CategoryTheory.Functor.RightExtension.postcompose₂_map_left_app 📋 Mathlib.CategoryTheory.Functor.KanExtension.Basic
  {C : Type u_1} {H : Type u_3} {D : Type u_5} {D' : Type u_6} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_3, u_3} H] [CategoryTheory.Category.{v_5, u_5} D] [CategoryTheory.Category.{v_6, u_6} D'] (L : CategoryTheory.Functor C D) (F : CategoryTheory.Functor C H) (G : CategoryTheory.Functor H D') {X Y : CategoryTheory.Comma ((CategoryTheory.Functor.whiskeringLeft C D H).obj L) (CategoryTheory.Functor.fromPUnit F)} (φ : X ⟶ Y) (X✝ : D) : ((CategoryTheory.Functor.RightExtension.postcompose₂ L F G).map φ).left.app X✝ = G.map (φ.left.app X✝)
• CategoryTheory.whiskeringRightPreservesColimits 📋 Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2} [CategoryTheory.Category.{v_2, u_2} D] {E : Type u_3} [CategoryTheory.Category.{v_3, u_3} E] (F : CategoryTheory.Functor D E) [CategoryTheory.Limits.HasColimitsOfSize.{w, w', v_2, u_2} D] [CategoryTheory.Limits.PreservesColimitsOfSize.{w, w', v_2, v_3, u_2, u_3} F] : CategoryTheory.Limits.PreservesColimitsOfSize.{w, w', max u_1 v_2, max u_1 v_3, max (max (max u_1 u_2) v_1) v_2, max (max (max u_1 u_3) v_1) v_3} ((CategoryTheory.Functor.whiskeringRight C D E).obj F)
• CategoryTheory.whiskeringRightPreservesLimits 📋 Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2} [CategoryTheory.Category.{v_2, u_2} D] {E : Type u_3} [CategoryTheory.Category.{v_3, u_3} E] (F : CategoryTheory.Functor D E) [CategoryTheory.Limits.HasLimitsOfSize.{w, w', v_2, u_2} D] [CategoryTheory.Limits.PreservesLimitsOfSize.{w, w', v_2, v_3, u_2, u_3} F] : CategoryTheory.Limits.PreservesLimitsOfSize.{w, w', max u_1 v_2, max u_1 v_3, max (max (max u_1 u_2) v_1) v_2, max (max (max u_1 u_3) v_1) v_3} ((CategoryTheory.Functor.whiskeringRight C D E).obj F)
• CategoryTheory.instReflectsLimitsOfShapeFunctorObjWhiskeringRightOfHasLimitsOfShape 📋 Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2} [CategoryTheory.Category.{v_2, u_2} D] {E : Type u_3} [CategoryTheory.Category.{v_3, u_3} E] {J : Type u_4} [CategoryTheory.Category.{v_4, u_4} J] [CategoryTheory.Limits.HasLimitsOfShape J E] (F : CategoryTheory.Functor D E) [CategoryTheory.Limits.ReflectsLimitsOfShape J F] : CategoryTheory.Limits.ReflectsLimitsOfShape J ((CategoryTheory.Functor.whiskeringRight C D E).obj F)
• CategoryTheory.whiskeringRight_preservesColimitsOfShape 📋 Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2} [CategoryTheory.Category.{v_2, u_2} D] {E : Type u_3} [CategoryTheory.Category.{v_3, u_3} E] {J : Type u_4} [CategoryTheory.Category.{v_4, u_4} J] [CategoryTheory.Limits.HasColimitsOfShape J D] (F : CategoryTheory.Functor D E) [CategoryTheory.Limits.PreservesColimitsOfShape J F] : CategoryTheory.Limits.PreservesColimitsOfShape J ((CategoryTheory.Functor.whiskeringRight C D E).obj F)
• CategoryTheory.whiskeringRight_preservesLimitsOfShape 📋 Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2} [CategoryTheory.Category.{v_2, u_2} D] {E : Type u_3} [CategoryTheory.Category.{v_3, u_3} E] {J : Type u_4} [CategoryTheory.Category.{v_4, u_4} J] [CategoryTheory.Limits.HasLimitsOfShape J D] (F : CategoryTheory.Functor D E) [CategoryTheory.Limits.PreservesLimitsOfShape J F] : CategoryTheory.Limits.PreservesLimitsOfShape J ((CategoryTheory.Functor.whiskeringRight C D E).obj F)
• CategoryTheory.instReflectsLimitsOfShapeFunctorObjWhiskeringRightOfHasLimitsOfShapeOfReflectsIsomorphismsOfPreservesLimitsOfShape 📋 Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2} [CategoryTheory.Category.{v_2, u_2} D] {E : Type u_3} [CategoryTheory.Category.{v_3, u_3} E] {J : Type u_4} [CategoryTheory.Category.{v_4, u_4} J] [CategoryTheory.Limits.HasLimitsOfShape J D] (F : CategoryTheory.Functor D E) [F.ReflectsIsomorphisms] [CategoryTheory.Limits.PreservesLimitsOfShape J F] : CategoryTheory.Limits.ReflectsLimitsOfShape J ((CategoryTheory.Functor.whiskeringRight C D E).obj F)
• CategoryTheory.colimitCompWhiskeringRightIsoColimitComp 📋 Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2} [CategoryTheory.Category.{v_2, u_2} D] {E : Type u_3} [CategoryTheory.Category.{v_3, u_3} E] {J : Type u_4} [CategoryTheory.Category.{v_4, u_4} J] [CategoryTheory.Limits.HasColimitsOfShape J D] (F : CategoryTheory.Functor D E) [CategoryTheory.Limits.PreservesColimitsOfShape J F] (G : CategoryTheory.Functor J (CategoryTheory.Functor C D)) : CategoryTheory.Limits.colimit (G.comp ((CategoryTheory.Functor.whiskeringRight C D E).obj F)) ≅ (CategoryTheory.Limits.colimit G).comp F
• CategoryTheory.limitCompWhiskeringRightIsoLimitComp 📋 Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2} [CategoryTheory.Category.{v_2, u_2} D] {E : Type u_3} [CategoryTheory.Category.{v_3, u_3} E] {J : Type u_4} [CategoryTheory.Category.{v_4, u_4} J] [CategoryTheory.Limits.HasLimitsOfShape J D] (F : CategoryTheory.Functor D E) [CategoryTheory.Limits.PreservesLimitsOfShape J F] (G : CategoryTheory.Functor J (CategoryTheory.Functor C D)) : CategoryTheory.Limits.limit (G.comp ((CategoryTheory.Functor.whiskeringRight C D E).obj F)) ≅ (CategoryTheory.Limits.limit G).comp F
• CategoryTheory.limitCompWhiskeringRightIsoLimitComp_inv_π 📋 Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2} [CategoryTheory.Category.{v_2, u_2} D] {E : Type u_3} [CategoryTheory.Category.{v_3, u_3} E] {J : Type u_4} [CategoryTheory.Category.{v_4, u_4} J] [CategoryTheory.Limits.HasLimitsOfShape J D] (F : CategoryTheory.Functor D E) [CategoryTheory.Limits.PreservesLimitsOfShape J F] (G : CategoryTheory.Functor J (CategoryTheory.Functor C D)) (j : J) : CategoryTheory.CategoryStruct.comp (CategoryTheory.limitCompWhiskeringRightIsoLimitComp F G).inv (CategoryTheory.Limits.limit.π (G.comp ((CategoryTheory.Functor.whiskeringRight C D E).obj F)) j) = CategoryTheory.Functor.whiskerRight (CategoryTheory.Limits.limit.π G j) F
• CategoryTheory.ι_colimitCompWhiskeringRightIsoColimitComp_hom 📋 Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2} [CategoryTheory.Category.{v_2, u_2} D] {E : Type u_3} [CategoryTheory.Category.{v_3, u_3} E] {J : Type u_4} [CategoryTheory.Category.{v_4, u_4} J] [CategoryTheory.Limits.HasColimitsOfShape J D] (F : CategoryTheory.Functor D E) [CategoryTheory.Limits.PreservesColimitsOfShape J F] (G : CategoryTheory.Functor J (CategoryTheory.Functor C D)) (j : J) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι (G.comp ((CategoryTheory.Functor.whiskeringRight C D E).obj F)) j) (CategoryTheory.colimitCompWhiskeringRightIsoColimitComp F G).hom = CategoryTheory.Functor.whiskerRight (CategoryTheory.Limits.colimit.ι G j) F
• CategoryTheory.limitCompWhiskeringRightIsoLimitComp_hom_whiskerRight_π 📋 Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2} [CategoryTheory.Category.{v_2, u_2} D] {E : Type u_3} [CategoryTheory.Category.{v_3, u_3} E] {J : Type u_4} [CategoryTheory.Category.{v_4, u_4} J] [CategoryTheory.Limits.HasLimitsOfShape J D] (F : CategoryTheory.Functor D E) [CategoryTheory.Limits.PreservesLimitsOfShape J F] (G : CategoryTheory.Functor J (CategoryTheory.Functor C D)) (j : J) : CategoryTheory.CategoryStruct.comp (CategoryTheory.limitCompWhiskeringRightIsoLimitComp F G).hom (CategoryTheory.Functor.whiskerRight (CategoryTheory.Limits.limit.π G j) F) = CategoryTheory.Limits.limit.π (G.comp ((CategoryTheory.Functor.whiskeringRight C D E).obj F)) j
• CategoryTheory.whiskerRight_ι_colimitCompWhiskeringRightIsoColimitComp_inv 📋 Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2} [CategoryTheory.Category.{v_2, u_2} D] {E : Type u_3} [CategoryTheory.Category.{v_3, u_3} E] {J : Type u_4} [CategoryTheory.Category.{v_4, u_4} J] [CategoryTheory.Limits.HasColimitsOfShape J D] (F : CategoryTheory.Functor D E) [CategoryTheory.Limits.PreservesColimitsOfShape J F] (G : CategoryTheory.Functor J (CategoryTheory.Functor C D)) (j : J) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight (CategoryTheory.Limits.colimit.ι G j) F) (CategoryTheory.colimitCompWhiskeringRightIsoColimitComp F G).inv = CategoryTheory.Limits.colimit.ι (G.comp ((CategoryTheory.Functor.whiskeringRight C D E).obj F)) j
• CategoryTheory.limitCompWhiskeringRightIsoLimitComp_inv_π_assoc 📋 Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2} [CategoryTheory.Category.{v_2, u_2} D] {E : Type u_3} [CategoryTheory.Category.{v_3, u_3} E] {J : Type u_4} [CategoryTheory.Category.{v_4, u_4} J] [CategoryTheory.Limits.HasLimitsOfShape J D] (F : CategoryTheory.Functor D E) [CategoryTheory.Limits.PreservesLimitsOfShape J F] (G : CategoryTheory.Functor J (CategoryTheory.Functor C D)) (j : J) {Z : CategoryTheory.Functor C E} (h : ((CategoryTheory.Functor.whiskeringRight C D E).obj F).obj (G.obj j) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.limitCompWhiskeringRightIsoLimitComp F G).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π (G.comp ((CategoryTheory.Functor.whiskeringRight C D E).obj F)) j) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight (CategoryTheory.Limits.limit.π G j) F) h
• CategoryTheory.ι_colimitCompWhiskeringRightIsoColimitComp_hom_assoc 📋 Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2} [CategoryTheory.Category.{v_2, u_2} D] {E : Type u_3} [CategoryTheory.Category.{v_3, u_3} E] {J : Type u_4} [CategoryTheory.Category.{v_4, u_4} J] [CategoryTheory.Limits.HasColimitsOfShape J D] (F : CategoryTheory.Functor D E) [CategoryTheory.Limits.PreservesColimitsOfShape J F] (G : CategoryTheory.Functor J (CategoryTheory.Functor C D)) (j : J) {Z : CategoryTheory.Functor C E} (h : (CategoryTheory.Limits.colimit G).comp F ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι (G.comp ((CategoryTheory.Functor.whiskeringRight C D E).obj F)) j) (CategoryTheory.CategoryStruct.comp (CategoryTheory.colimitCompWhiskeringRightIsoColimitComp F G).hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight (CategoryTheory.Limits.colimit.ι G j) F) h
• CategoryTheory.limitCompWhiskeringRightIsoLimitComp_hom_whiskerRight_π_assoc 📋 Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2} [CategoryTheory.Category.{v_2, u_2} D] {E : Type u_3} [CategoryTheory.Category.{v_3, u_3} E] {J : Type u_4} [CategoryTheory.Category.{v_4, u_4} J] [CategoryTheory.Limits.HasLimitsOfShape J D] (F : CategoryTheory.Functor D E) [CategoryTheory.Limits.PreservesLimitsOfShape J F] (G : CategoryTheory.Functor J (CategoryTheory.Functor C D)) (j : J) {Z : CategoryTheory.Functor C E} (h : (G.obj j).comp F ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.limitCompWhiskeringRightIsoLimitComp F G).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight (CategoryTheory.Limits.limit.π G j) F) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π (G.comp ((CategoryTheory.Functor.whiskeringRight C D E).obj F)) j) h
• CategoryTheory.whiskerRight_ι_colimitCompWhiskeringRightIsoColimitComp_inv_assoc 📋 Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2} [CategoryTheory.Category.{v_2, u_2} D] {E : Type u_3} [CategoryTheory.Category.{v_3, u_3} E] {J : Type u_4} [CategoryTheory.Category.{v_4, u_4} J] [CategoryTheory.Limits.HasColimitsOfShape J D] (F : CategoryTheory.Functor D E) [CategoryTheory.Limits.PreservesColimitsOfShape J F] (G : CategoryTheory.Functor J (CategoryTheory.Functor C D)) (j : J) {Z : CategoryTheory.Functor C E} (h : CategoryTheory.Limits.colimit (G.comp ((CategoryTheory.Functor.whiskeringRight C D E).obj F)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight (CategoryTheory.Limits.colimit.ι G j) F) (CategoryTheory.CategoryStruct.comp (CategoryTheory.colimitCompWhiskeringRightIsoColimitComp F G).inv h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι (G.comp ((CategoryTheory.Functor.whiskeringRight C D E).obj F)) j) h
• CategoryTheory.instPreservesMonomorphismsFunctorObjWhiskeringRight 📋 Mathlib.CategoryTheory.Limits.FunctorCategory.EpiMono
  {K : Type u} [CategoryTheory.Category.{v, u} K] {C : Type u'} [CategoryTheory.Category.{v', u'} C] {D : Type u''} [CategoryTheory.Category.{v'', u''} D] [CategoryTheory.Limits.HasPullbacks C] (F : CategoryTheory.Functor C D) [F.PreservesMonomorphisms] : ((CategoryTheory.Functor.whiskeringRight K C D).obj F).PreservesMonomorphisms
• CategoryTheory.instMonoidalFunctorObjWhiskeringRight 📋 Mathlib.CategoryTheory.Monoidal.FunctorCategory
  {C : Type u_1} {D : Type u_2} {E : Type u_3} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.Category.{v_3, u_3} E] [CategoryTheory.MonoidalCategory D] [CategoryTheory.MonoidalCategory E] (L : CategoryTheory.Functor D E) [L.Monoidal] : ((CategoryTheory.Functor.whiskeringRight C D E).obj L).Monoidal
• CategoryTheory.Functor.LaxMonoidal.whiskeringRight 📋 Mathlib.CategoryTheory.Monoidal.FunctorCategory
  {C : Type u_1} {D : Type u_2} {E : Type u_3} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.Category.{v_3, u_3} E] [CategoryTheory.MonoidalCategory D] [CategoryTheory.MonoidalCategory E] (L : CategoryTheory.Functor D E) [L.LaxMonoidal] : ((CategoryTheory.Functor.whiskeringRight C D E).obj L).LaxMonoidal
• CategoryTheory.Functor.OplaxMonoidal.whiskeringRight 📋 Mathlib.CategoryTheory.Monoidal.FunctorCategory
  {C : Type u_1} {D : Type u_2} {E : Type u_3} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.Category.{v_3, u_3} E] [CategoryTheory.MonoidalCategory D] [CategoryTheory.MonoidalCategory E] (L : CategoryTheory.Functor D E) [L.OplaxMonoidal] : ((CategoryTheory.Functor.whiskeringRight C D E).obj L).OplaxMonoidal
• CategoryTheory.Functor.LaxMonoidal.whiskeringRight_ε_app 📋 Mathlib.CategoryTheory.Monoidal.FunctorCategory
  {C : Type u_1} {D : Type u_2} {E : Type u_3} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.Category.{v_3, u_3} E] [CategoryTheory.MonoidalCategory D] [CategoryTheory.MonoidalCategory E] (L : CategoryTheory.Functor D E) [L.LaxMonoidal] (X : C) : (CategoryTheory.Functor.LaxMonoidal.ε ((CategoryTheory.Functor.whiskeringRight C D E).obj L)).app X = CategoryTheory.Functor.LaxMonoidal.ε L
• CategoryTheory.Functor.OplaxMonoidal.whiskeringRight_η_app 📋 Mathlib.CategoryTheory.Monoidal.FunctorCategory
  {C : Type u_1} {D : Type u_2} {E : Type u_3} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.Category.{v_3, u_3} E] [CategoryTheory.MonoidalCategory D] [CategoryTheory.MonoidalCategory E] (L : CategoryTheory.Functor D E) [L.OplaxMonoidal] (X : C) : (CategoryTheory.Functor.OplaxMonoidal.η ((CategoryTheory.Functor.whiskeringRight C D E).obj L)).app X = CategoryTheory.Functor.OplaxMonoidal.η L
• CategoryTheory.Functor.LaxMonoidal.whiskeringRight_μ_app 📋 Mathlib.CategoryTheory.Monoidal.FunctorCategory
  {C : Type u_1} {D : Type u_2} {E : Type u_3} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.Category.{v_3, u_3} E] [CategoryTheory.MonoidalCategory D] [CategoryTheory.MonoidalCategory E] (L : CategoryTheory.Functor D E) [L.LaxMonoidal] (F G : CategoryTheory.Functor C D) (X : C) : (CategoryTheory.Functor.LaxMonoidal.μ ((CategoryTheory.Functor.whiskeringRight C D E).obj L) F G).app X = CategoryTheory.Functor.LaxMonoidal.μ L (F.obj X) (G.obj X)
• CategoryTheory.Functor.OplaxMonoidal.whiskeringRight_δ_app 📋 Mathlib.CategoryTheory.Monoidal.FunctorCategory
  {C : Type u_1} {D : Type u_2} {E : Type u_3} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.Category.{v_3, u_3} E] [CategoryTheory.MonoidalCategory D] [CategoryTheory.MonoidalCategory E] (L : CategoryTheory.Functor D E) [L.OplaxMonoidal] (F G : CategoryTheory.Functor C D) (X : C) : (CategoryTheory.Functor.OplaxMonoidal.δ ((CategoryTheory.Functor.whiskeringRight C D E).obj L) F G).app X = CategoryTheory.Functor.OplaxMonoidal.δ L (F.obj X) (G.obj X)
• CategoryTheory.MonoidalCategory.externalProductBifunctorCurried_obj_obj_map_app 📋 Mathlib.CategoryTheory.Monoidal.ExternalProduct.Basic
  (J₁ : Type u₁) (J₂ : Type u₂) (C : Type u₃) [CategoryTheory.Category.{v₁, u₁} J₁] [CategoryTheory.Category.{v₂, u₂} J₂] [CategoryTheory.Category.{v₃, u₃} C] [CategoryTheory.MonoidalCategory C] (X : CategoryTheory.Functor J₁ C) (X✝ : CategoryTheory.Functor J₂ C) {X✝¹ Y✝ : J₁} (f : X✝¹ ⟶ Y✝) (X✝² : J₂) : ((((CategoryTheory.MonoidalCategory.externalProductBifunctorCurried J₁ J₂ C).obj X).obj X✝).map f).app X✝² = CategoryTheory.MonoidalCategoryStruct.whiskerRight (X.map f) (X✝.obj X✝²)
• CategoryTheory.MonoidalCategory.externalProductBifunctorCurried_obj_map_app_app 📋 Mathlib.CategoryTheory.Monoidal.ExternalProduct.Basic
  (J₁ : Type u₁) (J₂ : Type u₂) (C : Type u₃) [CategoryTheory.Category.{v₁, u₁} J₁] [CategoryTheory.Category.{v₂, u₂} J₂] [CategoryTheory.Category.{v₃, u₃} C] [CategoryTheory.MonoidalCategory C] (X : CategoryTheory.Functor J₁ C) {X✝ Y✝ : CategoryTheory.Functor J₂ C} (f : X✝ ⟶ Y✝) (X✝¹ : J₁) (c : J₂) : ((((CategoryTheory.MonoidalCategory.externalProductBifunctorCurried J₁ J₂ C).obj X).map f).app X✝¹).app c = CategoryTheory.MonoidalCategoryStruct.whiskerLeft (X.obj X✝¹) (f.app c)
• CategoryTheory.MonoidalCategory.externalProductBifunctorCurried_map_app_app_app 📋 Mathlib.CategoryTheory.Monoidal.ExternalProduct.Basic
  (J₁ : Type u₁) (J₂ : Type u₂) (C : Type u₃) [CategoryTheory.Category.{v₁, u₁} J₁] [CategoryTheory.Category.{v₂, u₂} J₂] [CategoryTheory.Category.{v₃, u₃} C] [CategoryTheory.MonoidalCategory C] {X✝ Y✝ : CategoryTheory.Functor J₁ C} (f : X✝ ⟶ Y✝) (X : CategoryTheory.Functor J₂ C) (c : J₁) (X✝¹ : J₂) : ((((CategoryTheory.MonoidalCategory.externalProductBifunctorCurried J₁ J₂ C).map f).app X).app c).app X✝¹ = CategoryTheory.MonoidalCategoryStruct.whiskerRight (f.app c) (X.obj X✝¹)
• PresheafOfModules.freeAdjunction 📋 Mathlib.Algebra.Category.ModuleCat.Presheaf.Free
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (R : CategoryTheory.Functor Cᵒᵖ RingCat) : PresheafOfModules.free R ⊣ (PresheafOfModules.toPresheaf R).comp ((CategoryTheory.Functor.whiskeringRight Cᵒᵖ Ab (Type u)).obj (CategoryTheory.forget Ab))
• PresheafOfModules.freeAdjunction_homEquiv 📋 Mathlib.Algebra.Category.ModuleCat.Presheaf.Free
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} (F : CategoryTheory.Functor Cᵒᵖ (Type u)) (G : PresheafOfModules R) : (PresheafOfModules.freeAdjunction R).homEquiv F G = PresheafOfModules.freeHomEquiv
• PresheafOfModules.freeAdjunction_unit_app 📋 Mathlib.Algebra.Category.ModuleCat.Presheaf.Free
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (R : CategoryTheory.Functor Cᵒᵖ RingCat) (F : CategoryTheory.Functor Cᵒᵖ (Type u)) : (PresheafOfModules.freeAdjunction R).unit.app F = PresheafOfModules.freeAdjunctionUnit R F
• CategoryTheory.Sieve.shrinkFunctorUliftFunctorIso_inv_ι 📋 Mathlib.CategoryTheory.Sites.Sieves.Shrink
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {S : CategoryTheory.Sieve X} [CategoryTheory.LocallySmall.{w, v₁, u₁} C] [CategoryTheory.LocallySmall.{max w' w, v₁, u₁} C] : CategoryTheory.CategoryStruct.comp S.shrinkFunctorUliftFunctorIso.inv (CategoryTheory.Functor.whiskerRight (CategoryTheory.Sieve.shrinkFunctor.{w, v₁, u₁} S).ι CategoryTheory.uliftFunctor.{w', w}) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Sieve.shrinkFunctor.{max w' w, v₁, u₁} S).ι (CategoryTheory.shrinkYonedaUliftFunctorIso.inv.app X)
• CategoryTheory.Sieve.shrinkFunctorUliftFunctorIso_inv_ι_assoc 📋 Mathlib.CategoryTheory.Sites.Sieves.Shrink
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {S : CategoryTheory.Sieve X} [CategoryTheory.LocallySmall.{w, v₁, u₁} C] [CategoryTheory.LocallySmall.{max w' w, v₁, u₁} C] {Z : CategoryTheory.Functor Cᵒᵖ (Type (max w w'))} (h : (CategoryTheory.shrinkYoneda.{w, v₁, u₁}.obj X).comp CategoryTheory.uliftFunctor.{w', w} ⟶ Z) : CategoryTheory.CategoryStruct.comp S.shrinkFunctorUliftFunctorIso.inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight (CategoryTheory.Sieve.shrinkFunctor.{w, v₁, u₁} S).ι CategoryTheory.uliftFunctor.{w', w}) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Sieve.shrinkFunctor.{max w' w, v₁, u₁} S).ι (CategoryTheory.CategoryStruct.comp (CategoryTheory.shrinkYonedaUliftFunctorIso.inv.app X) h)
• CategoryTheory.sheafCompose_map_hom 📋 Mathlib.CategoryTheory.Sites.Whiskering
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {A : Type u₂} [CategoryTheory.Category.{v₂, u₂} A] {B : Type u₃} [CategoryTheory.Category.{v₃, u₃} B] (J : CategoryTheory.GrothendieckTopology C) (F : CategoryTheory.Functor A B) [J.HasSheafCompose F] {X✝ Y✝ : CategoryTheory.Sheaf J A} (f : X✝ ⟶ Y✝) : ((CategoryTheory.sheafCompose J F).map f).hom = CategoryTheory.Functor.whiskerRight f.hom F
• CategoryTheory.GrothendieckTopology.plusFunctorWhiskerRightIso 📋 Mathlib.CategoryTheory.Sites.CompatiblePlus
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] {E : Type u_2} [CategoryTheory.Category.{v_2, u_2} E] (F : CategoryTheory.Functor D E) [∀ (J : CategoryTheory.Limits.MulticospanShape), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan J) D] [∀ (J : CategoryTheory.Limits.MulticospanShape), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan J) E] [∀ (X : C) (W : J.Cover X) (P : CategoryTheory.Functor Cᵒᵖ D), CategoryTheory.Limits.PreservesLimit (W.index P).multicospan F] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ E] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ F] : (J.plusFunctor D).comp ((CategoryTheory.Functor.whiskeringRight Cᵒᵖ D E).obj F) ≅ ((CategoryTheory.Functor.whiskeringRight Cᵒᵖ D E).obj F).comp (J.plusFunctor E)
• CategoryTheory.GrothendieckTopology.plusFunctorWhiskerRightIso_hom_app 📋 Mathlib.CategoryTheory.Sites.CompatiblePlus
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] {E : Type u_2} [CategoryTheory.Category.{v_2, u_2} E] (F : CategoryTheory.Functor D E) [∀ (J : CategoryTheory.Limits.MulticospanShape), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan J) D] [∀ (J : CategoryTheory.Limits.MulticospanShape), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan J) E] [∀ (X : C) (W : J.Cover X) (P : CategoryTheory.Functor Cᵒᵖ D), CategoryTheory.Limits.PreservesLimit (W.index P).multicospan F] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ E] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ F] (X : CategoryTheory.Functor Cᵒᵖ D) : (J.plusFunctorWhiskerRightIso F).hom.app X = (J.plusCompIso F X).hom
• CategoryTheory.GrothendieckTopology.plusFunctorWhiskerRightIso_inv_app 📋 Mathlib.CategoryTheory.Sites.CompatiblePlus
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] {E : Type u_2} [CategoryTheory.Category.{v_2, u_2} E] (F : CategoryTheory.Functor D E) [∀ (J : CategoryTheory.Limits.MulticospanShape), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan J) D] [∀ (J : CategoryTheory.Limits.MulticospanShape), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan J) E] [∀ (X : C) (W : J.Cover X) (P : CategoryTheory.Functor Cᵒᵖ D), CategoryTheory.Limits.PreservesLimit (W.index P).multicospan F] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ E] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ F] (X : CategoryTheory.Functor Cᵒᵖ D) : (J.plusFunctorWhiskerRightIso F).inv.app X = (J.plusCompIso F X).inv
• CategoryTheory.GrothendieckTopology.sheafificationWhiskerRightIso 📋 Mathlib.CategoryTheory.Sites.CompatibleSheafification
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] {E : Type u_2} [CategoryTheory.Category.{v_2, u_2} E] (F : CategoryTheory.Functor D E) [∀ (J : CategoryTheory.Limits.MulticospanShape), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan J) D] [∀ (J : CategoryTheory.Limits.MulticospanShape), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan J) E] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ E] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ F] [∀ (X : C) (W : J.Cover X) (P : CategoryTheory.Functor Cᵒᵖ D), CategoryTheory.Limits.PreservesLimit (W.index P).multicospan F] : (J.sheafification D).comp ((CategoryTheory.Functor.whiskeringRight Cᵒᵖ D E).obj F) ≅ ((CategoryTheory.Functor.whiskeringRight Cᵒᵖ D E).obj F).comp (J.sheafification E)
• CategoryTheory.GrothendieckTopology.sheafificationWhiskerRightIso_hom_app 📋 Mathlib.CategoryTheory.Sites.CompatibleSheafification
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] {E : Type u_2} [CategoryTheory.Category.{v_2, u_2} E] (F : CategoryTheory.Functor D E) [∀ (J : CategoryTheory.Limits.MulticospanShape), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan J) D] [∀ (J : CategoryTheory.Limits.MulticospanShape), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan J) E] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ E] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ F] [∀ (X : C) (W : J.Cover X) (P : CategoryTheory.Functor Cᵒᵖ D), CategoryTheory.Limits.PreservesLimit (W.index P).multicospan F] (P : CategoryTheory.Functor Cᵒᵖ D) : (J.sheafificationWhiskerRightIso F).hom.app P = (J.sheafifyCompIso F P).hom
• CategoryTheory.GrothendieckTopology.sheafificationWhiskerRightIso_inv_app 📋 Mathlib.CategoryTheory.Sites.CompatibleSheafification
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] {E : Type u_2} [CategoryTheory.Category.{v_2, u_2} E] (F : CategoryTheory.Functor D E) [∀ (J : CategoryTheory.Limits.MulticospanShape), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan J) D] [∀ (J : CategoryTheory.Limits.MulticospanShape), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan J) E] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ E] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ F] [∀ (X : C) (W : J.Cover X) (P : CategoryTheory.Functor Cᵒᵖ D), CategoryTheory.Limits.PreservesLimit (W.index P).multicospan F] (P : CategoryTheory.Functor Cᵒᵖ D) : (J.sheafificationWhiskerRightIso F).inv.app P = (J.sheafifyCompIso F P).inv
• CategoryTheory.GrothendieckTopology.W_isInvertedBy_whiskeringRight_presheafToSheaf 📋 Mathlib.CategoryTheory.Sites.PreservesSheafification
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {A : Type u_1} {B : Type u_2} [CategoryTheory.Category.{v_1, u_1} A] [CategoryTheory.Category.{v_2, u_2} B] (F : CategoryTheory.Functor A B) [J.PreservesSheafification F] [CategoryTheory.HasWeakSheafify J B] : J.W.IsInvertedBy (((CategoryTheory.Functor.whiskeringRight Cᵒᵖ A B).obj F).comp (CategoryTheory.presheafToSheaf J B))
• CategoryTheory.instLiftingFunctorOppositeSheafPresheafToSheafWCompObjWhiskeringRightComposeAndSheafify 📋 Mathlib.CategoryTheory.Sites.PreservesSheafification
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {A : Type u_1} {B : Type u_2} [CategoryTheory.Category.{v_1, u_1} A] [CategoryTheory.Category.{v_2, u_2} B] (F : CategoryTheory.Functor A B) [CategoryTheory.HasWeakSheafify J B] [CategoryTheory.HasWeakSheafify J A] [J.PreservesSheafification F] : CategoryTheory.Localization.Lifting (CategoryTheory.presheafToSheaf J A) J.W (((CategoryTheory.Functor.whiskeringRight Cᵒᵖ A B).obj F).comp (CategoryTheory.presheafToSheaf J B)) (CategoryTheory.Sheaf.composeAndSheafify J F)
• CategoryTheory.presheafToSheafCompComposeAndSheafifyIso 📋 Mathlib.CategoryTheory.Sites.PreservesSheafification
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {A : Type u_1} {B : Type u_2} [CategoryTheory.Category.{v_1, u_1} A] [CategoryTheory.Category.{v_2, u_2} B] (F : CategoryTheory.Functor A B) [CategoryTheory.HasWeakSheafify J B] [CategoryTheory.HasWeakSheafify J A] [J.PreservesSheafification F] : (CategoryTheory.presheafToSheaf J A).comp (CategoryTheory.Sheaf.composeAndSheafify J F) ≅ ((CategoryTheory.Functor.whiskeringRight Cᵒᵖ A B).obj F).comp (CategoryTheory.presheafToSheaf J B)
• CategoryTheory.instIsIsoFunctorOppositeSheafToPresheafToSheafCompComposeAndSheafify 📋 Mathlib.CategoryTheory.Sites.PreservesSheafification
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {A : Type u_1} {B : Type u_2} [CategoryTheory.Category.{v_1, u_1} A] [CategoryTheory.Category.{v_2, u_2} B] (F : CategoryTheory.Functor A B) [CategoryTheory.HasWeakSheafify J B] [CategoryTheory.HasWeakSheafify J A] [J.PreservesSheafification F] : CategoryTheory.IsIso (CategoryTheory.toPresheafToSheafCompComposeAndSheafify J F)
• CategoryTheory.GrothendieckTopology.PreservesSheafification.le 📋 Mathlib.CategoryTheory.Sites.PreservesSheafification
  {C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} {J : CategoryTheory.GrothendieckTopology C} {A : Type u_1} {B : Type u_2} {inst✝¹ : CategoryTheory.Category.{v_1, u_1} A} {inst✝² : CategoryTheory.Category.{v_2, u_2} B} {F : CategoryTheory.Functor A B} [self : J.PreservesSheafification F] : J.W ≤ J.W.inverseImage ((CategoryTheory.Functor.whiskeringRight Cᵒᵖ A B).obj F)
• CategoryTheory.GrothendieckTopology.PreservesSheafification.mk 📋 Mathlib.CategoryTheory.Sites.PreservesSheafification
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {A : Type u_1} {B : Type u_2} [CategoryTheory.Category.{v_1, u_1} A] [CategoryTheory.Category.{v_2, u_2} B] {F : CategoryTheory.Functor A B} (le : J.W ≤ J.W.inverseImage ((CategoryTheory.Functor.whiskeringRight Cᵒᵖ A B).obj F)) : J.PreservesSheafification F
• CategoryTheory.toPresheafToSheafCompComposeAndSheafify 📋 Mathlib.CategoryTheory.Sites.PreservesSheafification
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {A : Type u_1} {B : Type u_2} [CategoryTheory.Category.{v_1, u_1} A] [CategoryTheory.Category.{v_2, u_2} B] (F : CategoryTheory.Functor A B) [CategoryTheory.HasWeakSheafify J B] [CategoryTheory.HasWeakSheafify J A] : ((CategoryTheory.Functor.whiskeringRight Cᵒᵖ A B).obj F).comp (CategoryTheory.presheafToSheaf J B) ⟶ (CategoryTheory.presheafToSheaf J A).comp (CategoryTheory.Sheaf.composeAndSheafify J F)
• CategoryTheory.sheafComposeNatIso 📋 Mathlib.CategoryTheory.Sites.PreservesSheafification
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {A : Type u_1} {B : Type u_2} [CategoryTheory.Category.{v_1, u_1} A] [CategoryTheory.Category.{v_2, u_2} B] (F : CategoryTheory.Functor A B) {G₁ : CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ A) (CategoryTheory.Sheaf J A)} (adj₁ : G₁ ⊣ CategoryTheory.sheafToPresheaf J A) {G₂ : CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ B) (CategoryTheory.Sheaf J B)} (adj₂ : G₂ ⊣ CategoryTheory.sheafToPresheaf J B) [J.HasSheafCompose F] [J.PreservesSheafification F] : ((CategoryTheory.Functor.whiskeringRight Cᵒᵖ A B).obj F).comp G₂ ≅ G₁.comp (CategoryTheory.sheafCompose J F)
• CategoryTheory.instIsIsoFunctorOppositeSheafSheafComposeNatTrans 📋 Mathlib.CategoryTheory.Sites.PreservesSheafification
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {A : Type u_1} {B : Type u_2} [CategoryTheory.Category.{v_1, u_1} A] [CategoryTheory.Category.{v_2, u_2} B] (F : CategoryTheory.Functor A B) {G₁ : CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ A) (CategoryTheory.Sheaf J A)} (adj₁ : G₁ ⊣ CategoryTheory.sheafToPresheaf J A) {G₂ : CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ B) (CategoryTheory.Sheaf J B)} (adj₂ : G₂ ⊣ CategoryTheory.sheafToPresheaf J B) [J.HasSheafCompose F] [J.PreservesSheafification F] : CategoryTheory.IsIso (CategoryTheory.sheafComposeNatTrans J F adj₁ adj₂)
• CategoryTheory.GrothendieckTopology.preservesSheafification_iff_of_adjunctions_of_hasSheafCompose 📋 Mathlib.CategoryTheory.Sites.PreservesSheafification
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {A : Type u_1} {B : Type u_2} [CategoryTheory.Category.{v_1, u_1} A] [CategoryTheory.Category.{v_2, u_2} B] (F : CategoryTheory.Functor A B) {G₁ : CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ A) (CategoryTheory.Sheaf J A)} (adj₁ : G₁ ⊣ CategoryTheory.sheafToPresheaf J A) {G₂ : CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ B) (CategoryTheory.Sheaf J B)} (adj₂ : G₂ ⊣ CategoryTheory.sheafToPresheaf J B) [J.HasSheafCompose F] : J.PreservesSheafification F ↔ CategoryTheory.IsIso (CategoryTheory.sheafComposeNatTrans J F adj₁ adj₂)
• CategoryTheory.sheafComposeNatTrans 📋 Mathlib.CategoryTheory.Sites.PreservesSheafification
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {A : Type u_1} {B : Type u_2} [CategoryTheory.Category.{v_1, u_1} A] [CategoryTheory.Category.{v_2, u_2} B] (F : CategoryTheory.Functor A B) {G₁ : CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ A) (CategoryTheory.Sheaf J A)} (adj₁ : G₁ ⊣ CategoryTheory.sheafToPresheaf J A) {G₂ : CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ B) (CategoryTheory.Sheaf J B)} (adj₂ : G₂ ⊣ CategoryTheory.sheafToPresheaf J B) [J.HasSheafCompose F] : ((CategoryTheory.Functor.whiskeringRight Cᵒᵖ A B).obj F).comp G₂ ⟶ G₁.comp (CategoryTheory.sheafCompose J F)
• CategoryTheory.toPresheafToSheafCompComposeAndSheafify_app 📋 Mathlib.CategoryTheory.Sites.PreservesSheafification
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {A : Type u_1} {B : Type u_2} [CategoryTheory.Category.{v_1, u_1} A] [CategoryTheory.Category.{v_2, u_2} B] (F : CategoryTheory.Functor A B) [CategoryTheory.HasWeakSheafify J B] [CategoryTheory.HasWeakSheafify J A] (X : CategoryTheory.Functor Cᵒᵖ A) : (CategoryTheory.toPresheafToSheafCompComposeAndSheafify J F).app X = (CategoryTheory.presheafToSheaf J B).map (CategoryTheory.Functor.whiskerRight (CategoryTheory.toSheafify J X) F)
• CategoryTheory.GrothendieckTopology.instIsIsoFunctorOppositeSheafSheafComposeNatTransPlusPlusAdjunction 📋 Mathlib.CategoryTheory.Sites.PreservesSheafification
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_3} {E : Type u_4} [CategoryTheory.Category.{v_3, u_3} D] [CategoryTheory.Category.{v_4, u_4} E] (F : CategoryTheory.Functor D E) [∀ (J : CategoryTheory.Limits.MulticospanShape), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan J) D] [∀ (J : CategoryTheory.Limits.MulticospanShape), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan J) E] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ E] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ F] [∀ (X : C) (W : J.Cover X) (P : CategoryTheory.Functor Cᵒᵖ D), CategoryTheory.Limits.PreservesLimit (W.index P).multicospan F] {FD : D → D → Type u_5} {CD : D → Type u_6} {FE : E → E → Type u_7} {CE : E → Type u_8} [(X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] [(X Y : E) → FunLike (FE X Y) (CE X) (CE Y)] [instCCD : CategoryTheory.ConcreteCategory D FD] [instCCE : CategoryTheory.ConcreteCategory E FE] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (CategoryTheory.forget D)] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (CategoryTheory.forget E)] [CategoryTheory.Limits.PreservesLimitsOfSize.{max v u, max v u, v_3, u_6, u_3, u_6 + 1} (CategoryTheory.forget D)] [CategoryTheory.Limits.PreservesLimitsOfSize.{max v u, max v u, v_4, u_8, u_4, u_8 + 1} (CategoryTheory.forget E)] [(CategoryTheory.forget D).ReflectsIsomorphisms] [(CategoryTheory.forget E).ReflectsIsomorphisms] : CategoryTheory.IsIso (CategoryTheory.sheafComposeNatTrans J F (CategoryTheory.plusPlusAdjunction J D) (CategoryTheory.plusPlusAdjunction J E))
• CategoryTheory.presheafToSheafCompComposeAndSheafifyIso_inv_app 📋 Mathlib.CategoryTheory.Sites.PreservesSheafification
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {A : Type u_1} {B : Type u_2} [CategoryTheory.Category.{v_1, u_1} A] [CategoryTheory.Category.{v_2, u_2} B] (F : CategoryTheory.Functor A B) [CategoryTheory.HasWeakSheafify J B] [CategoryTheory.HasWeakSheafify J A] [J.PreservesSheafification F] (X : CategoryTheory.Functor Cᵒᵖ A) : (CategoryTheory.presheafToSheafCompComposeAndSheafifyIso J F).inv.app X = (CategoryTheory.presheafToSheaf J B).map (CategoryTheory.Functor.whiskerRight (CategoryTheory.toSheafify J X) F)
• CategoryTheory.GrothendieckTopology.instIsIsoSheafAppFunctorOppositeSheafComposeNatTransPlusPlusAdjunction 📋 Mathlib.CategoryTheory.Sites.PreservesSheafification
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_3} {E : Type u_4} [CategoryTheory.Category.{v_3, u_3} D] [CategoryTheory.Category.{v_4, u_4} E] (F : CategoryTheory.Functor D E) [∀ (J : CategoryTheory.Limits.MulticospanShape), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan J) D] [∀ (J : CategoryTheory.Limits.MulticospanShape), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan J) E] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ E] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ F] [∀ (X : C) (W : J.Cover X) (P : CategoryTheory.Functor Cᵒᵖ D), CategoryTheory.Limits.PreservesLimit (W.index P).multicospan F] {FD : D → D → Type u_5} {CD : D → Type u_6} {FE : E → E → Type u_7} {CE : E → Type u_8} [(X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] [(X Y : E) → FunLike (FE X Y) (CE X) (CE Y)] [instCCD : CategoryTheory.ConcreteCategory D FD] [instCCE : CategoryTheory.ConcreteCategory E FE] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (CategoryTheory.forget D)] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (CategoryTheory.forget E)] [CategoryTheory.Limits.PreservesLimitsOfSize.{max v u, max v u, v_3, u_6, u_3, u_6 + 1} (CategoryTheory.forget D)] [CategoryTheory.Limits.PreservesLimitsOfSize.{max v u, max v u, v_4, u_8, u_4, u_8 + 1} (CategoryTheory.forget E)] [(CategoryTheory.forget D).ReflectsIsomorphisms] [(CategoryTheory.forget E).ReflectsIsomorphisms] (P : CategoryTheory.Functor Cᵒᵖ D) : CategoryTheory.IsIso ((CategoryTheory.sheafComposeNatTrans J F (CategoryTheory.plusPlusAdjunction J D) (CategoryTheory.plusPlusAdjunction J E)).app P)
• CategoryTheory.sheafComposeNatTrans_fac 📋 Mathlib.CategoryTheory.Sites.PreservesSheafification
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {A : Type u_1} {B : Type u_2} [CategoryTheory.Category.{v_1, u_1} A] [CategoryTheory.Category.{v_2, u_2} B] (F : CategoryTheory.Functor A B) {G₁ : CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ A) (CategoryTheory.Sheaf J A)} (adj₁ : G₁ ⊣ CategoryTheory.sheafToPresheaf J A) {G₂ : CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ B) (CategoryTheory.Sheaf J B)} (adj₂ : G₂ ⊣ CategoryTheory.sheafToPresheaf J B) [J.HasSheafCompose F] (P : CategoryTheory.Functor Cᵒᵖ A) : CategoryTheory.CategoryStruct.comp (adj₂.unit.app (P.comp F)) ((CategoryTheory.sheafToPresheaf J B).map ((CategoryTheory.sheafComposeNatTrans J F adj₁ adj₂).app P)) = CategoryTheory.Functor.whiskerRight (adj₁.unit.app P) F
• CategoryTheory.sheafComposeNatTrans_app_uniq 📋 Mathlib.CategoryTheory.Sites.PreservesSheafification
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {A : Type u_1} {B : Type u_2} [CategoryTheory.Category.{v_1, u_1} A] [CategoryTheory.Category.{v_2, u_2} B] (F : CategoryTheory.Functor A B) {G₁ : CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ A) (CategoryTheory.Sheaf J A)} (adj₁ : G₁ ⊣ CategoryTheory.sheafToPresheaf J A) {G₂ : CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ B) (CategoryTheory.Sheaf J B)} (adj₂ : G₂ ⊣ CategoryTheory.sheafToPresheaf J B) [J.HasSheafCompose F] (P : CategoryTheory.Functor Cᵒᵖ A) (α : G₂.obj (P.comp F) ⟶ (CategoryTheory.sheafCompose J F).obj (G₁.obj P)) (hα : CategoryTheory.CategoryStruct.comp (adj₂.unit.app (P.comp F)) ((CategoryTheory.sheafToPresheaf J B).map α) = CategoryTheory.Functor.whiskerRight (adj₁.unit.app P) F) : α = (CategoryTheory.sheafComposeNatTrans J F adj₁ adj₂).app P
• CategoryTheory.GrothendieckTopology.sheafToPresheaf_map_sheafComposeNatTrans_eq_sheafifyCompIso_inv 📋 Mathlib.CategoryTheory.Sites.PreservesSheafification
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_3} {E : Type u_4} [CategoryTheory.Category.{v_3, u_3} D] [CategoryTheory.Category.{v_4, u_4} E] (F : CategoryTheory.Functor D E) [∀ (J : CategoryTheory.Limits.MulticospanShape), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan J) D] [∀ (J : CategoryTheory.Limits.MulticospanShape), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan J) E] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ E] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ F] [∀ (X : C) (W : J.Cover X) (P : CategoryTheory.Functor Cᵒᵖ D), CategoryTheory.Limits.PreservesLimit (W.index P).multicospan F] {FD : D → D → Type u_5} {CD : D → Type u_6} {FE : E → E → Type u_7} {CE : E → Type u_8} [(X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] [(X Y : E) → FunLike (FE X Y) (CE X) (CE Y)] [instCCD : CategoryTheory.ConcreteCategory D FD] [instCCE : CategoryTheory.ConcreteCategory E FE] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (CategoryTheory.forget D)] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (CategoryTheory.forget E)] [CategoryTheory.Limits.PreservesLimitsOfSize.{max v u, max v u, v_3, u_6, u_3, u_6 + 1} (CategoryTheory.forget D)] [CategoryTheory.Limits.PreservesLimitsOfSize.{max v u, max v u, v_4, u_8, u_4, u_8 + 1} (CategoryTheory.forget E)] [(CategoryTheory.forget D).ReflectsIsomorphisms] [(CategoryTheory.forget E).ReflectsIsomorphisms] (P : CategoryTheory.Functor Cᵒᵖ D) : (CategoryTheory.sheafToPresheaf J E).map ((CategoryTheory.sheafComposeNatTrans J F (CategoryTheory.plusPlusAdjunction J D) (CategoryTheory.plusPlusAdjunction J E)).app P) = (J.sheafifyCompIso F P).inv
• CategoryTheory.Adjunction.whiskerRight 📋 Mathlib.CategoryTheory.Adjunction.Whiskering
  (C : Type u_1) {D : Type u_2} {E : Type u_3} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.Category.{v_3, u_3} E] {F : CategoryTheory.Functor D E} {G : CategoryTheory.Functor E D} (adj : F ⊣ G) : (CategoryTheory.Functor.whiskeringRight C D E).obj F ⊣ (CategoryTheory.Functor.whiskeringRight C E D).obj G
• CategoryTheory.Adjunction.whiskerRight_counit_app_app 📋 Mathlib.CategoryTheory.Adjunction.Whiskering
  (C : Type u_1) {D : Type u_2} {E : Type u_3} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.Category.{v_3, u_3} E] {F : CategoryTheory.Functor D E} {G : CategoryTheory.Functor E D} (adj : F ⊣ G) (X : CategoryTheory.Functor C E) (X✝ : C) : ((CategoryTheory.Adjunction.whiskerRight C adj).counit.app X).app X✝ = adj.counit.app (X.obj X✝)
• CategoryTheory.Adjunction.whiskerRight_unit_app_app 📋 Mathlib.CategoryTheory.Adjunction.Whiskering
  (C : Type u_1) {D : Type u_2} {E : Type u_3} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.Category.{v_3, u_3} E] {F : CategoryTheory.Functor D E} {G : CategoryTheory.Functor E D} (adj : F ⊣ G) (X : CategoryTheory.Functor C D) (X✝ : C) : ((CategoryTheory.Adjunction.whiskerRight C adj).unit.app X).app X✝ = adj.unit.app (X.obj X✝)
• CategoryTheory.Functor.lanCompIsoOfPreserves 📋 Mathlib.CategoryTheory.Functor.KanExtension.Preserves
  {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [CategoryTheory.Category.{v_1, u_1} A] [CategoryTheory.Category.{v_2, u_2} B] [CategoryTheory.Category.{v_3, u_3} C] [CategoryTheory.Category.{v_4, u_4} D] (G : CategoryTheory.Functor B D) (L : CategoryTheory.Functor A C) [G.PreservesLeftKanExtensions L] [∀ (F : CategoryTheory.Functor A B), L.HasLeftKanExtension F] [∀ (F : CategoryTheory.Functor A D), L.HasLeftKanExtension F] : L.lan.comp ((CategoryTheory.Functor.whiskeringRight C B D).obj G) ≅ ((CategoryTheory.Functor.whiskeringRight A B D).obj G).comp L.lan
• CategoryTheory.Functor.ranCompIsoOfPreserves 📋 Mathlib.CategoryTheory.Functor.KanExtension.Preserves
  {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [CategoryTheory.Category.{v_1, u_1} A] [CategoryTheory.Category.{v_2, u_2} B] [CategoryTheory.Category.{v_3, u_3} C] [CategoryTheory.Category.{v_4, u_4} D] (G : CategoryTheory.Functor B D) (L : CategoryTheory.Functor A C) [G.PreservesRightKanExtensions L] [∀ (F : CategoryTheory.Functor A B), L.HasRightKanExtension F] [∀ (F : CategoryTheory.Functor A D), L.HasRightKanExtension F] : L.ran.comp ((CategoryTheory.Functor.whiskeringRight C B D).obj G) ≅ ((CategoryTheory.Functor.whiskeringRight A B D).obj G).comp L.ran
• CategoryTheory.Functor.lanCompIsoOfPreserves_hom_app 📋 Mathlib.CategoryTheory.Functor.KanExtension.Preserves
  {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [CategoryTheory.Category.{v_1, u_1} A] [CategoryTheory.Category.{v_2, u_2} B] [CategoryTheory.Category.{v_3, u_3} C] [CategoryTheory.Category.{v_4, u_4} D] (G : CategoryTheory.Functor B D) (L : CategoryTheory.Functor A C) [G.PreservesLeftKanExtensions L] [∀ (F : CategoryTheory.Functor A B), L.HasLeftKanExtension F] [∀ (F : CategoryTheory.Functor A D), L.HasLeftKanExtension F] (X : CategoryTheory.Functor A B) : (G.lanCompIsoOfPreserves L).hom.app X = (G.leftKanExtensionCompIsoOfPreserves X L).hom
• CategoryTheory.Functor.lanCompIsoOfPreserves_inv_app 📋 Mathlib.CategoryTheory.Functor.KanExtension.Preserves
  {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [CategoryTheory.Category.{v_1, u_1} A] [CategoryTheory.Category.{v_2, u_2} B] [CategoryTheory.Category.{v_3, u_3} C] [CategoryTheory.Category.{v_4, u_4} D] (G : CategoryTheory.Functor B D) (L : CategoryTheory.Functor A C) [G.PreservesLeftKanExtensions L] [∀ (F : CategoryTheory.Functor A B), L.HasLeftKanExtension F] [∀ (F : CategoryTheory.Functor A D), L.HasLeftKanExtension F] (X : CategoryTheory.Functor A B) : (G.lanCompIsoOfPreserves L).inv.app X = (G.leftKanExtensionCompIsoOfPreserves X L).inv
• CategoryTheory.Functor.ranCompIsoOfPreserves_hom_app 📋 Mathlib.CategoryTheory.Functor.KanExtension.Preserves
  {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [CategoryTheory.Category.{v_1, u_1} A] [CategoryTheory.Category.{v_2, u_2} B] [CategoryTheory.Category.{v_3, u_3} C] [CategoryTheory.Category.{v_4, u_4} D] (G : CategoryTheory.Functor B D) (L : CategoryTheory.Functor A C) [G.PreservesRightKanExtensions L] [∀ (F : CategoryTheory.Functor A B), L.HasRightKanExtension F] [∀ (F : CategoryTheory.Functor A D), L.HasRightKanExtension F] (X : CategoryTheory.Functor A B) : (G.ranCompIsoOfPreserves L).hom.app X = (G.rightKanExtensionCompIsoOfPreserves X L).hom
• CategoryTheory.Functor.ranCompIsoOfPreserves_inv_app 📋 Mathlib.CategoryTheory.Functor.KanExtension.Preserves
  {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [CategoryTheory.Category.{v_1, u_1} A] [CategoryTheory.Category.{v_2, u_2} B] [CategoryTheory.Category.{v_3, u_3} C] [CategoryTheory.Category.{v_4, u_4} D] (G : CategoryTheory.Functor B D) (L : CategoryTheory.Functor A C) [G.PreservesRightKanExtensions L] [∀ (F : CategoryTheory.Functor A B), L.HasRightKanExtension F] [∀ (F : CategoryTheory.Functor A D), L.HasRightKanExtension F] (X : CategoryTheory.Functor A B) : (G.ranCompIsoOfPreserves L).inv.app X = (G.rightKanExtensionCompIsoOfPreserves X L).inv
• AddCommMonCat.coyonedaForget 📋 Mathlib.Algebra.Category.MonCat.Yoneda
  : AddCommMonCat.coyoneda.comp ((CategoryTheory.Functor.whiskeringRight AddCommMonCat AddCommMonCat (Type u_1)).obj (CategoryTheory.forget AddCommMonCat)) ≅ CategoryTheory.coyoneda
• CommMonCat.coyonedaForget 📋 Mathlib.Algebra.Category.MonCat.Yoneda
  : CommMonCat.coyoneda.comp ((CategoryTheory.Functor.whiskeringRight CommMonCat CommMonCat (Type u_1)).obj (CategoryTheory.forget CommMonCat)) ≅ CategoryTheory.coyoneda
• AddCommMonCat.coyonedaForget_inv_app_app_hom_apply 📋 Mathlib.Algebra.Category.MonCat.Yoneda
  (X : AddCommMonCatᵒᵖ) (X✝ : AddCommMonCat) (f : Opposite.unop X ⟶ X✝) : (CategoryTheory.ConcreteCategory.hom ((AddCommMonCat.coyonedaForget.inv.app X).app X✝)) f = AddCommMonCat.Hom.hom f
• CommMonCat.coyonedaForget_inv_app_app_hom_apply 📋 Mathlib.Algebra.Category.MonCat.Yoneda
  (X : CommMonCatᵒᵖ) (X✝ : CommMonCat) (f : Opposite.unop X ⟶ X✝) : (CategoryTheory.ConcreteCategory.hom ((CommMonCat.coyonedaForget.inv.app X).app X✝)) f = CommMonCat.Hom.hom f

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using the Loogle command from the command palette. You can also try the #loogle command from LeanSearchClient, the CLI version, the Loogle VS Code extension, the lean.nvim integration or the Zulip bot.

Usage

Loogle finds definitions and lemmas in various ways:

1. By constant:
   🔍 Real.sin
   finds all lemmas whose statement somehow mentions the sine function.

2. By lemma name substring:
   🔍 "differ"
   finds all lemmas that have "differ" somewhere in their lemma name.

3. By subexpression:
   🔍 _ * (_ ^ _)
   finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.

   The pattern can also be non-linear, as in
   🔍 Real.sqrt ?a * Real.sqrt ?a

   If the pattern has parameters, they are matched in any order. Both of these will find List.map:
   🔍 (?a -> ?b) -> List ?a -> List ?b
   🔍 List ?a -> (?a -> ?b) -> List ?b

4. By main conclusion:
   🔍 |- tsum _ = _ * tsum _
   finds all lemmas where the conclusion (the subexpression to the right of all → and ∀) has the given shape.

   As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
   🔍 |- _ < _ → tsum _ < tsum _
   will find tsum_lt_tsum even though the hypothesis f i < g i is not the last.

5. You can filter for definitions vs theorems: Using ⊢ (_ : Type _) finds all definitions which provide data while ⊢ (_ : Prop) finds all theorems (and definitions of proofs).

If you pass more than one such search filter, separated by commas Loogle will return lemmas which match all of them. The search
🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _
would find all lemmas which mention the constants Real.sin and tsum, have "two" as a substring of the lemma name, include a product and a power somewhere in the type, and have a hypothesis of the form _ < _ (if there were any such lemmas). Metavariables (?a) are assigned independently in each filter.

The #lucky button will directly send you to the documentation of the first hit.

Source code

You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is provided by the Lean FRO. Please review the Lean FRO Terms of Use and Privacy Policy.

This is Loogle revision 9f11169 serving mathlib revision ce5dd8c