Loogle!

Result

Found 20159 declarations mentioning CategoryTheory.Functor.obj. Of these, 2214 have a name containing "_obj". Of these, only the first 200 are shown.

• CategoryTheory.Functor.id_obj 📋 Mathlib.CategoryTheory.Functor.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (X : C) : (CategoryTheory.Functor.id C).obj X = X
• CategoryTheory.Functor.toPrefunctor_obj 📋 Mathlib.CategoryTheory.Functor.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) (a✝ : C) : F.toPrefunctor.obj a✝ = F.obj a✝
• CategoryTheory.Functor.comp_obj 📋 Mathlib.CategoryTheory.Functor.Basic
  {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) (G : CategoryTheory.Functor D E) (X : C) : (F.comp G).obj X = G.obj (F.obj X)
• CategoryTheory.Functor.flip_obj_obj 📋 Mathlib.CategoryTheory.Functor.Category
  {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 (CategoryTheory.Functor D E)) (k : D) (j : C) : (F.flip.obj k).obj j = (F.obj j).obj k
• CategoryTheory.flipFunctor_obj 📋 Mathlib.CategoryTheory.Functor.Category
  (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 (CategoryTheory.Functor D E)) : (CategoryTheory.flipFunctor C D E).obj F = F.flip
• CategoryTheory.Functor.flip_obj_map 📋 Mathlib.CategoryTheory.Functor.Category
  {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 (CategoryTheory.Functor D E)) (k : D) {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) : (F.flip.obj k).map f = (F.map f).app k
• CategoryTheory.Functor.copyObj_obj 📋 Mathlib.CategoryTheory.NatIso
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) (obj : C → D) (e : (X : C) → F.obj X ≅ obj X) (a✝ : C) : (F.copyObj obj e).obj a✝ = obj a✝
• CategoryTheory.inducedFunctor_obj 📋 Mathlib.CategoryTheory.InducedCategory
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v, u₂} D] (F : C → D) (a✝ : C) : (CategoryTheory.inducedFunctor F).obj a✝ = F a✝
• CategoryTheory.ObjectProperty.prop_map_obj 📋 Mathlib.CategoryTheory.ObjectProperty.Basic
  {C : Type u} {D : Type u'} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Category.{v', u'} D] (P : CategoryTheory.ObjectProperty C) (F : CategoryTheory.Functor C D) {X : C} (hX : P X) : P.map F (F.obj X)
• CategoryTheory.ObjectProperty.strictMap_obj 📋 Mathlib.CategoryTheory.ObjectProperty.Basic
  {C : Type u} {D : Type u'} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Category.{v', u'} D] (P : CategoryTheory.ObjectProperty C) (F : CategoryTheory.Functor C D) {X : C} (hX : P X) : P.strictMap F (F.obj X)
• CategoryTheory.ObjectProperty.ι_obj 📋 Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) {X : P.FullSubcategory} : P.ι.obj X = X.obj
• CategoryTheory.ObjectProperty.lift_obj_obj 📋 Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (P : CategoryTheory.ObjectProperty D) (F : CategoryTheory.Functor C D) (hF : ∀ (X : C), P (F.obj X)) (X : C) : ((P.lift F hF).obj X).obj = F.obj X
• CategoryTheory.ObjectProperty.ιOfLE_obj_obj 📋 Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] {P P' : CategoryTheory.ObjectProperty C} (h : P ≤ P') (X : P.FullSubcategory) : ((CategoryTheory.ObjectProperty.ιOfLE h).obj X).obj = X.obj
• CategoryTheory.ObjectProperty.ι_obj_lift_obj 📋 Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (P : CategoryTheory.ObjectProperty D) (F : CategoryTheory.Functor C D) (hF : ∀ (X : C), P (F.obj X)) (X : C) : P.ι.obj ((P.lift F hF).obj X) = F.obj X
• CategoryTheory.ObjectProperty.ι_obj_lift_map 📋 Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (P : CategoryTheory.ObjectProperty D) (F : CategoryTheory.Functor C D) (hF : ∀ (X : C), P (F.obj X)) {X Y : C} (f : X ⟶ Y) : P.ι.map ((P.lift F hF).map f) = F.map f
• 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.whiskeringLeft_obj_id 📋 Mathlib.CategoryTheory.Whiskering
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] : (CategoryTheory.Functor.whiskeringLeft C C E).obj (CategoryTheory.Functor.id C) = CategoryTheory.Functor.id (CategoryTheory.Functor C E)
• 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.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.whiskeringLeft_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] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) : ((CategoryTheory.Functor.whiskeringLeft C D E).obj F).obj G = F.comp G
• 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.whiskeringLeft_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] (F : CategoryTheory.Functor C D) {X✝ Y✝ : CategoryTheory.Functor D E} (α : X✝ ⟶ Y✝) : ((CategoryTheory.Functor.whiskeringLeft C D E).obj F).map α = F.whiskerLeft α
• 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.postcompose₂_obj_obj_obj_obj 📋 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✝ : C₁) (X✝¹ : C₂) : (((CategoryTheory.Functor.postcompose₂.obj X).obj F).obj X✝).obj X✝¹ = X.obj ((F.obj X✝).obj X✝¹)
• CategoryTheory.Functor.whiskeringLeft_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.whiskeringLeft C D' E).obj (F.comp G) = ((CategoryTheory.Functor.whiskeringLeft D D' E).obj G).comp ((CategoryTheory.Functor.whiskeringLeft C D E).obj F)
• 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.whiskeringLeft₃ObjObjObj_obj_obj_obj_obj 📋 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✝¹ : C₂) (X✝² : C₃) : ((((CategoryTheory.Functor.whiskeringLeft₃ObjObjObj E F₁ F₂ F₃).obj X).obj X✝).obj X✝¹).obj X✝² = ((X.obj (F₁.obj X✝)).obj (F₂.obj X✝¹)).obj (F₃.obj X✝²)
• CategoryTheory.Functor.postcompose₂_obj_obj_obj_map 📋 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✝ : C₁) {X✝¹ Y✝ : C₂} (f : X✝¹ ⟶ Y✝) : (((CategoryTheory.Functor.postcompose₂.obj X).obj F).obj X✝).map f = X.map ((F.obj X✝).map f)
• CategoryTheory.Functor.whiskeringLeft₃ObjObj_obj 📋 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₃) : (CategoryTheory.Functor.whiskeringLeft₃ObjObj C₃ D₃ E F₁ F₂).obj F₃ = CategoryTheory.Functor.whiskeringLeft₃ObjObjObj E F₁ F₂ F₃
• CategoryTheory.Functor.whiskeringLeft₃ObjObjObj_obj_obj_obj_map 📋 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✝¹ : C₂) {X✝² Y✝ : C₃} (f : X✝² ⟶ Y✝) : ((((CategoryTheory.Functor.whiskeringLeft₃ObjObjObj E F₁ F₂ F₃).obj X).obj X✝).obj X✝¹).map f = ((X.obj (F₁.obj X✝)).obj (F₂.obj X✝¹)).map (F₃.map f)
• CategoryTheory.Functor.whiskeringLeft₂_obj_obj_obj_obj_obj 📋 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✝ : C₁) (X✝¹ : C₂) : (((((CategoryTheory.Functor.whiskeringLeft₂ E).obj F₁).obj F₂).obj X).obj X✝).obj X✝¹ = (X.obj (F₁.obj X✝)).obj (F₂.obj X✝¹)
• CategoryTheory.Functor.postcompose₃_obj_obj_obj_obj_obj 📋 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✝¹ : C₂) (X✝² : C₃) : ((((CategoryTheory.Functor.postcompose₃.obj X).obj F).obj X✝).obj X✝¹).obj X✝² = X.obj (((F.obj X✝).obj X✝¹).obj 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.whiskeringLeft₂_obj_obj_obj_obj_map 📋 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✝ : C₁) {X✝¹ Y✝ : C₂} (f : X✝¹ ⟶ Y✝) : (((((CategoryTheory.Functor.whiskeringLeft₂ E).obj F₁).obj F₂).obj X).obj X✝).map f = (X.obj (F₁.obj X✝)).map (F₂.map f)
• CategoryTheory.Functor.postcompose₃_obj_obj_obj_obj_map 📋 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✝¹ : C₂) {X✝² Y✝ : C₃} (f : X✝² ⟶ Y✝) : ((((CategoryTheory.Functor.postcompose₃.obj X).obj F).obj X✝).obj X✝¹).map f = X.map (((F.obj X✝).obj X✝¹).map f)
• CategoryTheory.Functor.whiskeringLeft₃Obj_obj 📋 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₂) : (CategoryTheory.Functor.whiskeringLeft₃Obj C₂ C₃ D₂ D₃ E F₁).obj F₂ = CategoryTheory.Functor.whiskeringLeft₃ObjObj C₃ D₃ E F₁ F₂
• 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.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.whiskeringLeft₃_obj_obj_obj_obj_obj_obj_obj 📋 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✝¹ : C₂) (X✝² : C₃) : (((((((CategoryTheory.Functor.whiskeringLeft₃ E).obj F₁).obj F₂).obj F₃).obj X).obj X✝).obj X✝¹).obj X✝² = ((X.obj (F₁.obj X✝)).obj (F₂.obj X✝¹)).obj (F₃.obj X✝²)
• CategoryTheory.Functor.whiskeringLeft₃_obj_obj_obj_obj_obj_obj_map 📋 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✝¹ : C₂) {X✝² Y✝ : C₃} (f : X✝² ⟶ Y✝) : (((((((CategoryTheory.Functor.whiskeringLeft₃ E).obj F₁).obj F₂).obj F₃).obj X).obj X✝).obj X✝¹).map f = ((X.obj (F₁.obj X✝)).obj (F₂.obj X✝¹)).map (F₃.map f)
• 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₃_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₃_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.toEssImage_obj_obj 📋 Mathlib.CategoryTheory.EssentialImage
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) (X : C) : (F.toEssImage.obj X).obj = F.obj X
• CategoryTheory.Functor.essImage.liftFunctor_obj 📋 Mathlib.CategoryTheory.EssentialImage
  {J : Type u_1} {C : Type u_2} {D : Type u_3} [CategoryTheory.Category.{v_1, u_1} J] [CategoryTheory.Category.{v_2, u_2} C] [CategoryTheory.Category.{v_3, u_3} D] (G : CategoryTheory.Functor J D) (F : CategoryTheory.Functor C D) [F.Full] [F.Faithful] (hG : ∀ (j : J), F.essImage (G.obj j)) (j : J) : (CategoryTheory.Functor.essImage.liftFunctor G F hG).obj j = F.toEssImage.objPreimage { obj := G.obj j, property := ⋯ }
• CategoryTheory.Equivalence.functorFunctor_obj 📋 Mathlib.CategoryTheory.Equivalence
  (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (f : C ≌ D) : (CategoryTheory.Equivalence.functorFunctor C D).obj f = f.functor
• CategoryTheory.Equivalence.congrRightFunctor_obj 📋 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) : (CategoryTheory.Equivalence.congrRightFunctor E).obj e = e.congrRight
• CategoryTheory.opOp_obj 📋 Mathlib.CategoryTheory.Opposites
  (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (X : C) : (CategoryTheory.opOp C).obj X = Opposite.op (Opposite.op X)
• CategoryTheory.unopUnop_obj 📋 Mathlib.CategoryTheory.Opposites
  (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (X : Cᵒᵖᵒᵖ) : (CategoryTheory.unopUnop C).obj X = Opposite.unop (Opposite.unop X)
• CategoryTheory.Functor.op_obj 📋 Mathlib.CategoryTheory.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) (X : Cᵒᵖ) : F.op.obj X = Opposite.op (F.obj (Opposite.unop X))
• CategoryTheory.Functor.leftOp_obj 📋 Mathlib.CategoryTheory.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C Dᵒᵖ) (X : Cᵒᵖ) : F.leftOp.obj X = Opposite.unop (F.obj (Opposite.unop X))
• CategoryTheory.Functor.rightOp_obj 📋 Mathlib.CategoryTheory.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor Cᵒᵖ D) (X : C) : F.rightOp.obj X = Opposite.op (F.obj (Opposite.op X))
• CategoryTheory.Functor.unop_obj 📋 Mathlib.CategoryTheory.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ) (X : C) : F.unop.obj X = Opposite.unop (F.obj (Opposite.op X))
• CategoryTheory.Equivalence.leftOp_functor_obj 📋 Mathlib.CategoryTheory.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ Dᵒᵖ) (X : Cᵒᵖ) : e.leftOp.functor.obj X = Opposite.unop (e.functor.obj (Opposite.unop X))
• CategoryTheory.Equivalence.leftOp_inverse_obj 📋 Mathlib.CategoryTheory.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ Dᵒᵖ) (X : D) : e.leftOp.inverse.obj X = Opposite.op (e.inverse.obj (Opposite.op X))
• CategoryTheory.Equivalence.rightOp_functor_obj 📋 Mathlib.CategoryTheory.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : Cᵒᵖ ≌ D) (X : C) : e.rightOp.functor.obj X = Opposite.op (e.functor.obj (Opposite.op X))
• CategoryTheory.Equivalence.rightOp_inverse_obj 📋 Mathlib.CategoryTheory.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : Cᵒᵖ ≌ D) (X : Dᵒᵖ) : e.rightOp.inverse.obj X = Opposite.unop (e.inverse.obj (Opposite.unop X))
• CategoryTheory.Functor.opHom_obj 📋 Mathlib.CategoryTheory.Opposites
  (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (F : (CategoryTheory.Functor C D)ᵒᵖ) : (CategoryTheory.Functor.opHom C D).obj F = (Opposite.unop F).op
• CategoryTheory.Functor.opInv_obj 📋 Mathlib.CategoryTheory.Opposites
  (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ) : (CategoryTheory.Functor.opInv C D).obj F = Opposite.op F.unop
• CategoryTheory.Functor.leftOpRightOpEquiv_inverse_obj 📋 Mathlib.CategoryTheory.Opposites
  (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C Dᵒᵖ) : (CategoryTheory.Functor.leftOpRightOpEquiv C D).inverse.obj F = Opposite.op F.leftOp
• CategoryTheory.Functor.leftOpRightOpEquiv_functor_obj_obj 📋 Mathlib.CategoryTheory.Opposites
  (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (F : (CategoryTheory.Functor Cᵒᵖ D)ᵒᵖ) (X : C) : ((CategoryTheory.Functor.leftOpRightOpEquiv C D).functor.obj F).obj X = Opposite.op ((Opposite.unop F).obj (Opposite.op X))
• CategoryTheory.Functor.leftOpRightOpEquiv_functor_obj_map 📋 Mathlib.CategoryTheory.Opposites
  (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (F : (CategoryTheory.Functor Cᵒᵖ D)ᵒᵖ) {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) : ((CategoryTheory.Functor.leftOpRightOpEquiv C D).functor.obj F).map f = ((Opposite.unop F).map f.op).op
• CategoryTheory.Functor.const_obj_obj 📋 Mathlib.CategoryTheory.Functor.Const
  (J : Type u₁) [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] (X : C) (x✝ : J) : ((CategoryTheory.Functor.const J).obj X).obj x✝ = X
• CategoryTheory.Functor.const_obj_map 📋 Mathlib.CategoryTheory.Functor.Const
  (J : Type u₁) [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] (X : C) {X✝ Y✝ : J} (x✝ : X✝ ⟶ Y✝) : ((CategoryTheory.Functor.const J).obj X).map x✝ = CategoryTheory.CategoryStruct.id X
• CategoryTheory.Functor.const.unop_functor_op_obj_map 📋 Mathlib.CategoryTheory.Functor.Const
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] (X : Cᵒᵖ) {j₁ j₂ : J} (f : j₁ ⟶ j₂) : (Opposite.unop ((CategoryTheory.Functor.const J).op.obj X)).map f = CategoryTheory.CategoryStruct.id (Opposite.unop X)
• CategoryTheory.Functor.diag_obj 📋 Mathlib.CategoryTheory.Products.Basic
  (C : Type u₃) [CategoryTheory.Category.{v₃, u₃} C] (a : C) : (CategoryTheory.Functor.diag C).obj a = (a, a)
• CategoryTheory.Prod.fst_obj 📋 Mathlib.CategoryTheory.Products.Basic
  (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (X : C × D) : (CategoryTheory.Prod.fst C D).obj X = X.1
• CategoryTheory.Prod.snd_obj 📋 Mathlib.CategoryTheory.Products.Basic
  (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (X : C × D) : (CategoryTheory.Prod.snd C D).obj X = X.2
• CategoryTheory.Prod.sectL_obj 📋 Mathlib.CategoryTheory.Products.Basic
  (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (Z : D) (X : C) : (CategoryTheory.Prod.sectL C Z).obj X = (X, Z)
• CategoryTheory.Prod.sectR_obj 📋 Mathlib.CategoryTheory.Products.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (Z : C) (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (X : D) : (CategoryTheory.Prod.sectR Z D).obj X = (Z, X)
• CategoryTheory.Prod.swap_obj 📋 Mathlib.CategoryTheory.Products.Basic
  (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (X : C × D) : (CategoryTheory.Prod.swap C D).obj X = (X.2, X.1)
• CategoryTheory.Functor.prod'_obj 📋 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 A B) (G : CategoryTheory.Functor A C) (a : A) : (F.prod' G).obj a = (F.obj a, G.obj a)
• CategoryTheory.evaluationUncurried_obj 📋 Mathlib.CategoryTheory.Products.Basic
  (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (p : C × CategoryTheory.Functor C D) : (CategoryTheory.evaluationUncurried C D).obj p = p.2.obj p.1
• CategoryTheory.evaluation_obj_obj 📋 Mathlib.CategoryTheory.Products.Basic
  (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (X : C) (F : CategoryTheory.Functor C D) : ((CategoryTheory.evaluation C D).obj X).obj F = F.obj X
• CategoryTheory.Functor.prod_obj 📋 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] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor C D) (X : A × C) : (F.prod G).obj X = (F.obj X.1, G.obj X.2)
• CategoryTheory.prodOpEquiv_inverse_obj 📋 Mathlib.CategoryTheory.Products.Basic
  (C : Type u₃) [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] (x✝ : Cᵒᵖ × Dᵒᵖ) : (CategoryTheory.prodOpEquiv C).inverse.obj x✝ = Opposite.op (Opposite.unop x✝.1, Opposite.unop x✝.2)
• CategoryTheory.prodOpEquiv_functor_obj 📋 Mathlib.CategoryTheory.Products.Basic
  (C : Type u₃) [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] (X : (C × D)ᵒᵖ) : (CategoryTheory.prodOpEquiv C).functor.obj X = (Opposite.op (Opposite.unop X).1, Opposite.op (Opposite.unop X).2)
• CategoryTheory.evaluation_obj_map 📋 Mathlib.CategoryTheory.Products.Basic
  (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (X : C) {X✝ Y✝ : CategoryTheory.Functor C D} (α : X✝ ⟶ Y✝) : ((CategoryTheory.evaluation C D).obj X).map α = α.app X
• CategoryTheory.prodFunctorToFunctorProd_obj 📋 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 A B × CategoryTheory.Functor A C) : (CategoryTheory.prodFunctorToFunctorProd A B C).obj F = F.1.prod' F.2
• CategoryTheory.functorProdToProdFunctor_obj 📋 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 A (B × C)) : (CategoryTheory.functorProdToProdFunctor A B C).obj F = (F.comp (CategoryTheory.Prod.fst B C), F.comp (CategoryTheory.Prod.snd B C))
• CategoryTheory.prodFunctor_obj 📋 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] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] (FG : CategoryTheory.Functor A B × CategoryTheory.Functor C D) : CategoryTheory.prodFunctor.obj FG = FG.1.prod FG.2
• CategoryTheory.Functor.congr_obj 📋 Mathlib.CategoryTheory.EqToHom
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F G : CategoryTheory.Functor C D} (h : F = G) (X : C) : F.obj X = G.obj X
• CategoryTheory.Equivalence.induced_inverse_obj 📋 Mathlib.CategoryTheory.EqToHom
  {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {T : Type u_2} (e : T ≃ D) (a : D) : (CategoryTheory.Equivalence.induced e).inverse.obj a = e.symm a
• CategoryTheory.Pi.eval_obj 📋 Mathlib.CategoryTheory.Pi.Basic
  {I : Type w₀} (C : I → Type u₁) [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] (i : I) (f : (i : I) → C i) : (CategoryTheory.Pi.eval C i).obj f = f i
• CategoryTheory.Pi.comap_obj 📋 Mathlib.CategoryTheory.Pi.Basic
  {I : Type w₀} (C : I → Type u₁) [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {J : Type w₁} (h : J → I) (f : (i : I) → C i) (i : J) : (CategoryTheory.Pi.comap C h).obj f i = f (h i)
• CategoryTheory.Functor.pi'_obj 📋 Mathlib.CategoryTheory.Pi.Basic
  {I : Type w₀} {C : I → Type u₁} [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {A : Type u₃} [CategoryTheory.Category.{v₃, u₃} A] (f : (i : I) → CategoryTheory.Functor A (C i)) (a : A) (i : I) : (CategoryTheory.Functor.pi' f).obj a i = (f i).obj a
• CategoryTheory.Functor.pi_obj 📋 Mathlib.CategoryTheory.Pi.Basic
  {I : Type w₀} {C : I → Type u₁} [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {D : I → Type u₂} [(i : I) → CategoryTheory.Category.{v₂, u₂} (D i)] (F : (i : I) → CategoryTheory.Functor (C i) (D i)) (f : (i : I) → C i) (i : I) : (CategoryTheory.Functor.pi F).obj f i = (F i).obj (f i)
• CategoryTheory.Pi.sum_obj_obj 📋 Mathlib.CategoryTheory.Pi.Basic
  {I : Type w₀} (C : I → Type u₁) [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {J : Type w₀} {D : J → Type u₁} [(j : J) → CategoryTheory.Category.{v₁, u₁} (D j)] (X : (i : I) → C i) (Y : (j : J) → D j) (s : I ⊕ J) : ((CategoryTheory.Pi.sum C).obj X).obj Y s = match s with | Sum.inl i => X i | Sum.inr j => Y j
• CategoryTheory.Pi.sum_obj_map 📋 Mathlib.CategoryTheory.Pi.Basic
  {I : Type w₀} (C : I → Type u₁) [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {J : Type w₀} {D : J → Type u₁} [(j : J) → CategoryTheory.Category.{v₁, u₁} (D j)] (X : (i : I) → C i) {x✝ x✝¹ : (j : J) → D j} (f : x✝ ⟶ x✝¹) (s : I ⊕ J) : ((CategoryTheory.Pi.sum C).obj X).map f s = match s with | Sum.inl i => CategoryTheory.CategoryStruct.id (X i) | Sum.inr j => f j
• CategoryTheory.Discrete.functor_obj 📋 Mathlib.CategoryTheory.Discrete.Basic
  {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {I : Type u₁} (F : I → C) (i : I) : (CategoryTheory.Discrete.functor F).obj { as := i } = F i
• CategoryTheory.Discrete.functor_obj_eq_as 📋 Mathlib.CategoryTheory.Discrete.Basic
  {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {I : Type u₁} (F : I → C) (X : CategoryTheory.Discrete I) : (CategoryTheory.Discrete.functor F).obj X = F X.as
• CategoryTheory.Discrete.opposite_inverse_obj 📋 Mathlib.CategoryTheory.Discrete.Basic
  (α : Type u₁) (a✝ : CategoryTheory.Discrete α) : (CategoryTheory.Discrete.opposite α).inverse.obj a✝ = Opposite.op a✝
• CategoryTheory.Discrete.opposite_functor_obj_as 📋 Mathlib.CategoryTheory.Discrete.Basic
  (α : Type u₁) (X : (CategoryTheory.Discrete α)ᵒᵖ) : ((CategoryTheory.Discrete.opposite α).functor.obj X).as = (Opposite.unop X).as
• CategoryTheory.piEquivalenceFunctorDiscrete_functor_obj 📋 Mathlib.CategoryTheory.Discrete.Basic
  (J : Type u₂) (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (F : J → C) : (CategoryTheory.piEquivalenceFunctorDiscrete J C).functor.obj F = CategoryTheory.Discrete.functor F
• CategoryTheory.piEquivalenceFunctorDiscrete_inverse_obj 📋 Mathlib.CategoryTheory.Discrete.Basic
  (J : Type u₂) (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (F : CategoryTheory.Functor (CategoryTheory.Discrete J) C) (j : J) : (CategoryTheory.piEquivalenceFunctorDiscrete J C).inverse.obj F j = F.obj { as := j }
• CategoryTheory.prod.leftUnitor_obj 📋 Mathlib.CategoryTheory.Products.Unitor
  (C : Type u) [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.Discrete PUnit.{w + 1} × C) : (CategoryTheory.prod.leftUnitor C).obj X = X.2
• CategoryTheory.prod.rightUnitor_obj 📋 Mathlib.CategoryTheory.Products.Unitor
  (C : Type u) [CategoryTheory.Category.{v, u} C] (X : C × CategoryTheory.Discrete PUnit.{w + 1}) : (CategoryTheory.prod.rightUnitor C).obj X = X.1
• CategoryTheory.prod.leftInverseUnitor_obj 📋 Mathlib.CategoryTheory.Products.Unitor
  (C : Type u) [CategoryTheory.Category.{v, u} C] (X : C) : (CategoryTheory.prod.leftInverseUnitor C).obj X = ({ as := PUnit.unit }, X)
• CategoryTheory.prod.rightInverseUnitor_obj 📋 Mathlib.CategoryTheory.Products.Unitor
  (C : Type u) [CategoryTheory.Category.{v, u} C] (X : C) : (CategoryTheory.prod.rightInverseUnitor C).obj X = (X, { as := PUnit.unit })
• CategoryTheory.Comma.fst_obj 📋 Mathlib.CategoryTheory.Comma.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T) (R : CategoryTheory.Functor B T) (X : CategoryTheory.Comma L R) : (CategoryTheory.Comma.fst L R).obj X = X.left
• CategoryTheory.Comma.snd_obj 📋 Mathlib.CategoryTheory.Comma.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T) (R : CategoryTheory.Functor B T) (X : CategoryTheory.Comma L R) : (CategoryTheory.Comma.snd L R).obj X = X.right
• CategoryTheory.Comma.fromProd_obj_left 📋 Mathlib.CategoryTheory.Comma.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] (L : CategoryTheory.Functor A (CategoryTheory.Discrete PUnit.{u_1 + 1})) (R : CategoryTheory.Functor B (CategoryTheory.Discrete PUnit.{u_1 + 1})) (X : A × B) : ((CategoryTheory.Comma.fromProd L R).obj X).left = X.1
• CategoryTheory.Comma.fromProd_obj_right 📋 Mathlib.CategoryTheory.Comma.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] (L : CategoryTheory.Functor A (CategoryTheory.Discrete PUnit.{u_1 + 1})) (R : CategoryTheory.Functor B (CategoryTheory.Discrete PUnit.{u_1 + 1})) (X : A × B) : ((CategoryTheory.Comma.fromProd L R).obj X).right = X.2
• CategoryTheory.Comma.toIdPUnitEquiv_inverse_obj_right 📋 Mathlib.CategoryTheory.Comma.Basic
  {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] (L : CategoryTheory.Functor (CategoryTheory.Discrete PUnit.{u_1 + 1}) (CategoryTheory.Discrete PUnit.{u_2 + 1})) (R : CategoryTheory.Functor B (CategoryTheory.Discrete PUnit.{u_2 + 1})) (X : B) : ((CategoryTheory.Comma.toIdPUnitEquiv L R).inverse.obj X).right = X
• CategoryTheory.Comma.toPUnitIdEquiv_inverse_obj_left 📋 Mathlib.CategoryTheory.Comma.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] (L : CategoryTheory.Functor A (CategoryTheory.Discrete PUnit.{u_1 + 1})) (R : CategoryTheory.Functor (CategoryTheory.Discrete PUnit.{u_2 + 1}) (CategoryTheory.Discrete PUnit.{u_1 + 1})) (X : A) : ((CategoryTheory.Comma.toPUnitIdEquiv L R).inverse.obj X).left = X
• CategoryTheory.Comma.toIdPUnitEquiv_inverse_obj_left_as 📋 Mathlib.CategoryTheory.Comma.Basic
  {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] (L : CategoryTheory.Functor (CategoryTheory.Discrete PUnit.{u_1 + 1}) (CategoryTheory.Discrete PUnit.{u_2 + 1})) (R : CategoryTheory.Functor B (CategoryTheory.Discrete PUnit.{u_2 + 1})) (X : B) : ((CategoryTheory.Comma.toIdPUnitEquiv L R).inverse.obj X).left.as = PUnit.unit
• CategoryTheory.Comma.toPUnitIdEquiv_inverse_obj_right_as 📋 Mathlib.CategoryTheory.Comma.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] (L : CategoryTheory.Functor A (CategoryTheory.Discrete PUnit.{u_1 + 1})) (R : CategoryTheory.Functor (CategoryTheory.Discrete PUnit.{u_2 + 1}) (CategoryTheory.Discrete PUnit.{u_1 + 1})) (X : A) : ((CategoryTheory.Comma.toPUnitIdEquiv L R).inverse.obj X).right.as = PUnit.unit
• CategoryTheory.Comma.equivProd_inverse_obj_left 📋 Mathlib.CategoryTheory.Comma.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] (L : CategoryTheory.Functor A (CategoryTheory.Discrete PUnit.{u_1 + 1})) (R : CategoryTheory.Functor B (CategoryTheory.Discrete PUnit.{u_1 + 1})) (X : A × B) : ((CategoryTheory.Comma.equivProd L R).inverse.obj X).left = X.1
• CategoryTheory.Comma.equivProd_inverse_obj_right 📋 Mathlib.CategoryTheory.Comma.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] (L : CategoryTheory.Functor A (CategoryTheory.Discrete PUnit.{u_1 + 1})) (R : CategoryTheory.Functor B (CategoryTheory.Discrete PUnit.{u_1 + 1})) (X : A × B) : ((CategoryTheory.Comma.equivProd L R).inverse.obj X).right = X.2
• CategoryTheory.Comma.toIdPUnitEquiv_functor_obj 📋 Mathlib.CategoryTheory.Comma.Basic
  {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] (L : CategoryTheory.Functor (CategoryTheory.Discrete PUnit.{u_1 + 1}) (CategoryTheory.Discrete PUnit.{u_2 + 1})) (R : CategoryTheory.Functor B (CategoryTheory.Discrete PUnit.{u_2 + 1})) (X : CategoryTheory.Comma L R) : (CategoryTheory.Comma.toIdPUnitEquiv L R).functor.obj X = X.right
• CategoryTheory.Comma.toPUnitIdEquiv_functor_obj 📋 Mathlib.CategoryTheory.Comma.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] (L : CategoryTheory.Functor A (CategoryTheory.Discrete PUnit.{u_1 + 1})) (R : CategoryTheory.Functor (CategoryTheory.Discrete PUnit.{u_2 + 1}) (CategoryTheory.Discrete PUnit.{u_1 + 1})) (X : CategoryTheory.Comma L R) : (CategoryTheory.Comma.toPUnitIdEquiv L R).functor.obj X = X.left
• CategoryTheory.Comma.mapLeft_obj_left 📋 Mathlib.CategoryTheory.Comma.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] (R : CategoryTheory.Functor B T) {L₁ L₂ : CategoryTheory.Functor A T} (l : L₁ ⟶ L₂) (X : CategoryTheory.Comma L₂ R) : ((CategoryTheory.Comma.mapLeft R l).obj X).left = X.left
• CategoryTheory.Comma.mapLeft_obj_right 📋 Mathlib.CategoryTheory.Comma.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] (R : CategoryTheory.Functor B T) {L₁ L₂ : CategoryTheory.Functor A T} (l : L₁ ⟶ L₂) (X : CategoryTheory.Comma L₂ R) : ((CategoryTheory.Comma.mapLeft R l).obj X).right = X.right
• CategoryTheory.Comma.mapRight_obj_left 📋 Mathlib.CategoryTheory.Comma.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T) {R₁ R₂ : CategoryTheory.Functor B T} (r : R₁ ⟶ R₂) (X : CategoryTheory.Comma L R₁) : ((CategoryTheory.Comma.mapRight L r).obj X).left = X.left
• CategoryTheory.Comma.mapRight_obj_right 📋 Mathlib.CategoryTheory.Comma.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T) {R₁ R₂ : CategoryTheory.Functor B T} (r : R₁ ⟶ R₂) (X : CategoryTheory.Comma L R₁) : ((CategoryTheory.Comma.mapRight L r).obj X).right = X.right
• CategoryTheory.Comma.equivProd_functor_obj 📋 Mathlib.CategoryTheory.Comma.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] (L : CategoryTheory.Functor A (CategoryTheory.Discrete PUnit.{u_1 + 1})) (R : CategoryTheory.Functor B (CategoryTheory.Discrete PUnit.{u_1 + 1})) (a : CategoryTheory.Comma L R) : (CategoryTheory.Comma.equivProd L R).functor.obj a = (a.left, a.right)
• CategoryTheory.Comma.fromProd_obj_hom 📋 Mathlib.CategoryTheory.Comma.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] (L : CategoryTheory.Functor A (CategoryTheory.Discrete PUnit.{u_1 + 1})) (R : CategoryTheory.Functor B (CategoryTheory.Discrete PUnit.{u_1 + 1})) (X : A × B) : ((CategoryTheory.Comma.fromProd L R).obj X).hom = CategoryTheory.Discrete.eqToHom ⋯
• CategoryTheory.Comma.preLeft_obj_right 📋 Mathlib.CategoryTheory.Comma.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {C : Type u₄} [CategoryTheory.Category.{v₄, u₄} C] (F : CategoryTheory.Functor C A) (L : CategoryTheory.Functor A T) (R : CategoryTheory.Functor B T) (X : CategoryTheory.Comma (F.comp L) R) : ((CategoryTheory.Comma.preLeft F L R).obj X).right = X.right
• CategoryTheory.Comma.preRight_obj_left 📋 Mathlib.CategoryTheory.Comma.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {C : Type u₄} [CategoryTheory.Category.{v₄, u₄} C] (L : CategoryTheory.Functor A T) (F : CategoryTheory.Functor C B) (R : CategoryTheory.Functor B T) (X : CategoryTheory.Comma L (F.comp R)) : ((CategoryTheory.Comma.preRight L F R).obj X).left = X.left
• CategoryTheory.Comma.preLeft_obj_left 📋 Mathlib.CategoryTheory.Comma.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {C : Type u₄} [CategoryTheory.Category.{v₄, u₄} C] (F : CategoryTheory.Functor C A) (L : CategoryTheory.Functor A T) (R : CategoryTheory.Functor B T) (X : CategoryTheory.Comma (F.comp L) R) : ((CategoryTheory.Comma.preLeft F L R).obj X).left = F.obj X.left
• CategoryTheory.Comma.preRight_obj_right 📋 Mathlib.CategoryTheory.Comma.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {C : Type u₄} [CategoryTheory.Category.{v₄, u₄} C] (L : CategoryTheory.Functor A T) (F : CategoryTheory.Functor C B) (R : CategoryTheory.Functor B T) (X : CategoryTheory.Comma L (F.comp R)) : ((CategoryTheory.Comma.preRight L F R).obj X).right = F.obj X.right
• CategoryTheory.Comma.mapLeftIso_functor_obj_left 📋 Mathlib.CategoryTheory.Comma.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] (R : CategoryTheory.Functor B T) {L₁ L₂ : CategoryTheory.Functor A T} (i : L₁ ≅ L₂) (X : CategoryTheory.Comma L₁ R) : ((CategoryTheory.Comma.mapLeftIso R i).functor.obj X).left = X.left
• CategoryTheory.Comma.mapLeftIso_functor_obj_right 📋 Mathlib.CategoryTheory.Comma.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] (R : CategoryTheory.Functor B T) {L₁ L₂ : CategoryTheory.Functor A T} (i : L₁ ≅ L₂) (X : CategoryTheory.Comma L₁ R) : ((CategoryTheory.Comma.mapLeftIso R i).functor.obj X).right = X.right
• CategoryTheory.Comma.mapLeftIso_inverse_obj_left 📋 Mathlib.CategoryTheory.Comma.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] (R : CategoryTheory.Functor B T) {L₁ L₂ : CategoryTheory.Functor A T} (i : L₁ ≅ L₂) (X : CategoryTheory.Comma L₂ R) : ((CategoryTheory.Comma.mapLeftIso R i).inverse.obj X).left = X.left
• CategoryTheory.Comma.mapLeftIso_inverse_obj_right 📋 Mathlib.CategoryTheory.Comma.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] (R : CategoryTheory.Functor B T) {L₁ L₂ : CategoryTheory.Functor A T} (i : L₁ ≅ L₂) (X : CategoryTheory.Comma L₂ R) : ((CategoryTheory.Comma.mapLeftIso R i).inverse.obj X).right = X.right
• CategoryTheory.Comma.mapRightIso_functor_obj_left 📋 Mathlib.CategoryTheory.Comma.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T) {R₁ R₂ : CategoryTheory.Functor B T} (i : R₁ ≅ R₂) (X : CategoryTheory.Comma L R₁) : ((CategoryTheory.Comma.mapRightIso L i).functor.obj X).left = X.left
• CategoryTheory.Comma.mapRightIso_functor_obj_right 📋 Mathlib.CategoryTheory.Comma.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T) {R₁ R₂ : CategoryTheory.Functor B T} (i : R₁ ≅ R₂) (X : CategoryTheory.Comma L R₁) : ((CategoryTheory.Comma.mapRightIso L i).functor.obj X).right = X.right
• CategoryTheory.Comma.mapRightIso_inverse_obj_left 📋 Mathlib.CategoryTheory.Comma.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T) {R₁ R₂ : CategoryTheory.Functor B T} (i : R₁ ≅ R₂) (X : CategoryTheory.Comma L R₂) : ((CategoryTheory.Comma.mapRightIso L i).inverse.obj X).left = X.left
• CategoryTheory.Comma.mapRightIso_inverse_obj_right 📋 Mathlib.CategoryTheory.Comma.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T) {R₁ R₂ : CategoryTheory.Functor B T} (i : R₁ ≅ R₂) (X : CategoryTheory.Comma L R₂) : ((CategoryTheory.Comma.mapRightIso L i).inverse.obj X).right = X.right
• CategoryTheory.Comma.post_obj_left 📋 Mathlib.CategoryTheory.Comma.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {C : Type u₄} [CategoryTheory.Category.{v₄, u₄} C] (L : CategoryTheory.Functor A T) (R : CategoryTheory.Functor B T) (F : CategoryTheory.Functor T C) (X : CategoryTheory.Comma L R) : ((CategoryTheory.Comma.post L R F).obj X).left = X.left
• CategoryTheory.Comma.post_obj_right 📋 Mathlib.CategoryTheory.Comma.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {C : Type u₄} [CategoryTheory.Category.{v₄, u₄} C] (L : CategoryTheory.Functor A T) (R : CategoryTheory.Functor B T) (F : CategoryTheory.Functor T C) (X : CategoryTheory.Comma L R) : ((CategoryTheory.Comma.post L R F).obj X).right = X.right
• CategoryTheory.Comma.preLeft_obj_hom 📋 Mathlib.CategoryTheory.Comma.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {C : Type u₄} [CategoryTheory.Category.{v₄, u₄} C] (F : CategoryTheory.Functor C A) (L : CategoryTheory.Functor A T) (R : CategoryTheory.Functor B T) (X : CategoryTheory.Comma (F.comp L) R) : ((CategoryTheory.Comma.preLeft F L R).obj X).hom = X.hom
• CategoryTheory.Comma.preRight_obj_hom 📋 Mathlib.CategoryTheory.Comma.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {C : Type u₄} [CategoryTheory.Category.{v₄, u₄} C] (L : CategoryTheory.Functor A T) (F : CategoryTheory.Functor C B) (R : CategoryTheory.Functor B T) (X : CategoryTheory.Comma L (F.comp R)) : ((CategoryTheory.Comma.preRight L F R).obj X).hom = X.hom
• CategoryTheory.Comma.map_obj_left 📋 Mathlib.CategoryTheory.Comma.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {A' : Type u₄} [CategoryTheory.Category.{v₄, u₄} A'] {B' : Type u₅} [CategoryTheory.Category.{v₅, u₅} B'] {T' : Type u₆} [CategoryTheory.Category.{v₆, u₆} T'] {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} {L' : CategoryTheory.Functor A' T'} {R' : CategoryTheory.Functor B' T'} {F₁ : CategoryTheory.Functor A A'} {F₂ : CategoryTheory.Functor B B'} {F : CategoryTheory.Functor T T'} (α : F₁.comp L' ⟶ L.comp F) (β : R.comp F ⟶ F₂.comp R') (X : CategoryTheory.Comma L R) : ((CategoryTheory.Comma.map α β).obj X).left = F₁.obj X.left
• CategoryTheory.Comma.map_obj_right 📋 Mathlib.CategoryTheory.Comma.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {A' : Type u₄} [CategoryTheory.Category.{v₄, u₄} A'] {B' : Type u₅} [CategoryTheory.Category.{v₅, u₅} B'] {T' : Type u₆} [CategoryTheory.Category.{v₆, u₆} T'] {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} {L' : CategoryTheory.Functor A' T'} {R' : CategoryTheory.Functor B' T'} {F₁ : CategoryTheory.Functor A A'} {F₂ : CategoryTheory.Functor B B'} {F : CategoryTheory.Functor T T'} (α : F₁.comp L' ⟶ L.comp F) (β : R.comp F ⟶ F₂.comp R') (X : CategoryTheory.Comma L R) : ((CategoryTheory.Comma.map α β).obj X).right = F₂.obj X.right
• CategoryTheory.Comma.mapLeft_obj_hom 📋 Mathlib.CategoryTheory.Comma.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] (R : CategoryTheory.Functor B T) {L₁ L₂ : CategoryTheory.Functor A T} (l : L₁ ⟶ L₂) (X : CategoryTheory.Comma L₂ R) : ((CategoryTheory.Comma.mapLeft R l).obj X).hom = CategoryTheory.CategoryStruct.comp (l.app X.left) X.hom
• CategoryTheory.Comma.mapRight_obj_hom 📋 Mathlib.CategoryTheory.Comma.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T) {R₁ R₂ : CategoryTheory.Functor B T} (r : R₁ ⟶ R₂) (X : CategoryTheory.Comma L R₁) : ((CategoryTheory.Comma.mapRight L r).obj X).hom = CategoryTheory.CategoryStruct.comp X.hom (r.app X.right)
• CategoryTheory.Comma.post_obj_hom 📋 Mathlib.CategoryTheory.Comma.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {C : Type u₄} [CategoryTheory.Category.{v₄, u₄} C] (L : CategoryTheory.Functor A T) (R : CategoryTheory.Functor B T) (F : CategoryTheory.Functor T C) (X : CategoryTheory.Comma L R) : ((CategoryTheory.Comma.post L R F).obj X).hom = F.map X.hom
• CategoryTheory.Comma.mapLeftIso_functor_obj_hom 📋 Mathlib.CategoryTheory.Comma.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] (R : CategoryTheory.Functor B T) {L₁ L₂ : CategoryTheory.Functor A T} (i : L₁ ≅ L₂) (X : CategoryTheory.Comma L₁ R) : ((CategoryTheory.Comma.mapLeftIso R i).functor.obj X).hom = CategoryTheory.CategoryStruct.comp (i.inv.app X.left) X.hom
• CategoryTheory.Comma.mapLeftIso_inverse_obj_hom 📋 Mathlib.CategoryTheory.Comma.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] (R : CategoryTheory.Functor B T) {L₁ L₂ : CategoryTheory.Functor A T} (i : L₁ ≅ L₂) (X : CategoryTheory.Comma L₂ R) : ((CategoryTheory.Comma.mapLeftIso R i).inverse.obj X).hom = CategoryTheory.CategoryStruct.comp (i.hom.app X.left) X.hom
• CategoryTheory.Comma.mapRightIso_functor_obj_hom 📋 Mathlib.CategoryTheory.Comma.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T) {R₁ R₂ : CategoryTheory.Functor B T} (i : R₁ ≅ R₂) (X : CategoryTheory.Comma L R₁) : ((CategoryTheory.Comma.mapRightIso L i).functor.obj X).hom = CategoryTheory.CategoryStruct.comp X.hom (i.hom.app X.right)
• CategoryTheory.Comma.mapRightIso_inverse_obj_hom 📋 Mathlib.CategoryTheory.Comma.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T) {R₁ R₂ : CategoryTheory.Functor B T} (i : R₁ ≅ R₂) (X : CategoryTheory.Comma L R₂) : ((CategoryTheory.Comma.mapRightIso L i).inverse.obj X).hom = CategoryTheory.CategoryStruct.comp X.hom (i.inv.app X.right)
• CategoryTheory.Comma.opFunctor_obj 📋 Mathlib.CategoryTheory.Comma.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T) (R : CategoryTheory.Functor B T) (X : CategoryTheory.Comma L R) : (CategoryTheory.Comma.opFunctor L R).obj X = Opposite.op { left := Opposite.op X.right, right := Opposite.op X.left, hom := Opposite.op X.hom }
• CategoryTheory.Comma.unopFunctor_obj 📋 Mathlib.CategoryTheory.Comma.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T) (R : CategoryTheory.Functor B T) (X : CategoryTheory.Comma L.op R.op) : (CategoryTheory.Comma.unopFunctor L R).obj X = Opposite.op { left := Opposite.unop X.right, right := Opposite.unop X.left, hom := X.hom.unop }
• CategoryTheory.Comma.map_obj_hom 📋 Mathlib.CategoryTheory.Comma.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {A' : Type u₄} [CategoryTheory.Category.{v₄, u₄} A'] {B' : Type u₅} [CategoryTheory.Category.{v₅, u₅} B'] {T' : Type u₆} [CategoryTheory.Category.{v₆, u₆} T'] {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} {L' : CategoryTheory.Functor A' T'} {R' : CategoryTheory.Functor B' T'} {F₁ : CategoryTheory.Functor A A'} {F₂ : CategoryTheory.Functor B B'} {F : CategoryTheory.Functor T T'} (α : F₁.comp L' ⟶ L.comp F) (β : R.comp F ⟶ F₂.comp R') (X : CategoryTheory.Comma L R) : ((CategoryTheory.Comma.map α β).obj X).hom = CategoryTheory.CategoryStruct.comp (α.app X.left) (CategoryTheory.CategoryStruct.comp (F.map X.hom) (β.app X.right))
• CategoryTheory.Arrow.leftFunc_obj 📋 Mathlib.CategoryTheory.Comma.Arrow
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.Comma (CategoryTheory.Functor.id C) (CategoryTheory.Functor.id C)) : CategoryTheory.Arrow.leftFunc.obj X = X.left
• CategoryTheory.Arrow.rightFunc_obj 📋 Mathlib.CategoryTheory.Comma.Arrow
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.Comma (CategoryTheory.Functor.id C) (CategoryTheory.Functor.id C)) : CategoryTheory.Arrow.rightFunc.obj X = X.right
• CategoryTheory.Functor.mapArrowFunctor_obj 📋 Mathlib.CategoryTheory.Comma.Arrow
  (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) : (CategoryTheory.Functor.mapArrowFunctor C D).obj F = F.mapArrow
• CategoryTheory.Functor.mapArrow_obj 📋 Mathlib.CategoryTheory.Comma.Arrow
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) (a : CategoryTheory.Arrow C) : F.mapArrow.obj a = CategoryTheory.Arrow.mk (F.map a.hom)
• CategoryTheory.Groupoid.invFunctor_obj 📋 Mathlib.CategoryTheory.Groupoid
  (C : Type u) [CategoryTheory.Groupoid C] (unop : C) : (CategoryTheory.Groupoid.invFunctor C).obj unop = Opposite.op unop
• CategoryTheory.Groupoid.invEquivalence_functor_obj 📋 Mathlib.CategoryTheory.Groupoid
  (C : Type u) [CategoryTheory.Groupoid C] (unop : C) : (CategoryTheory.Groupoid.invEquivalence C).functor.obj unop = Opposite.op unop
• CategoryTheory.Groupoid.invEquivalence_inverse_obj 📋 Mathlib.CategoryTheory.Groupoid
  (C : Type u) [CategoryTheory.Groupoid C] (self : Cᵒᵖ) : (CategoryTheory.Groupoid.invEquivalence C).inverse.obj self = Opposite.unop self
• CategoryTheory.uliftFunctor_obj 📋 Mathlib.CategoryTheory.Types.Basic
  {X : Type u} : CategoryTheory.uliftFunctor.{v, u}.obj X = ULift.{v, u} X
• CategoryTheory.ofTypeFunctor_obj 📋 Mathlib.CategoryTheory.Types.Basic
  (m : Type u → Type v) [Functor m] [LawfulFunctor m] : (CategoryTheory.ofTypeFunctor m).obj = m
• CategoryTheory.Functor.sectionsFunctor_obj 📋 Mathlib.CategoryTheory.Types.Basic
  (J : Type u) [CategoryTheory.Category.{v, u} J] (F : CategoryTheory.Functor J (Type w)) : (CategoryTheory.Functor.sectionsFunctor J).obj F = ↑F.sections
• CategoryTheory.forget_obj 📋 Mathlib.CategoryTheory.ConcreteCategory.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type w} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [CategoryTheory.ConcreteCategory C FC] (X : C) : (CategoryTheory.forget C).obj X = CategoryTheory.ToType X
• AddCommMonCat.uliftFunctor_obj_coe 📋 Mathlib.Algebra.Category.MonCat.Basic
  (X : AddCommMonCat) : ↑(AddCommMonCat.uliftFunctor.obj X) = ULift.{u, v} ↑X
• AddMonCat.uliftFunctor_obj_coe 📋 Mathlib.Algebra.Category.MonCat.Basic
  (X : AddMonCat) : ↑(AddMonCat.uliftFunctor.obj X) = ULift.{u, v} ↑X
• CommMonCat.uliftFunctor_obj_coe 📋 Mathlib.Algebra.Category.MonCat.Basic
  (X : CommMonCat) : ↑(CommMonCat.uliftFunctor.obj X) = ULift.{u, v} ↑X
• MonCat.uliftFunctor_obj_coe 📋 Mathlib.Algebra.Category.MonCat.Basic
  (X : MonCat) : ↑(MonCat.uliftFunctor.obj X) = ULift.{u, v} ↑X
• AddCommMonCat.equivalence_functor_obj_coe 📋 Mathlib.Algebra.Category.MonCat.Basic
  (X : AddCommMonCat) : ↑(AddCommMonCat.equivalence.functor.obj X) = Multiplicative ↑X
• AddCommMonCat.equivalence_inverse_obj_coe 📋 Mathlib.Algebra.Category.MonCat.Basic
  (X : CommMonCat) : ↑(AddCommMonCat.equivalence.inverse.obj X) = Additive ↑X
• AddMonCat.equivalence_functor_obj_coe 📋 Mathlib.Algebra.Category.MonCat.Basic
  (X : AddMonCat) : ↑(AddMonCat.equivalence.functor.obj X) = Multiplicative ↑X
• AddMonCat.equivalence_inverse_obj_coe 📋 Mathlib.Algebra.Category.MonCat.Basic
  (X : MonCat) : ↑(AddMonCat.equivalence.inverse.obj X) = Additive ↑X
• AddCommMonCat.coe_forget₂_obj 📋 Mathlib.Algebra.Category.MonCat.Basic
  (X : AddCommMonCat) : ↑((CategoryTheory.forget₂ AddCommMonCat AddMonCat).obj X) = ↑X
• CommMonCat.coe_forget₂_obj 📋 Mathlib.Algebra.Category.MonCat.Basic
  (X : CommMonCat) : ↑((CategoryTheory.forget₂ CommMonCat MonCat).obj X) = ↑X
• AddCommGrpCat.uliftFunctor_obj 📋 Mathlib.Algebra.Category.Grp.Basic
  (X : AddCommGrpCat) : AddCommGrpCat.uliftFunctor.obj X = AddCommGrpCat.of (ULift.{u, v} ↑X)
• AddGrpCat.uliftFunctor_obj 📋 Mathlib.Algebra.Category.Grp.Basic
  (X : AddGrpCat) : AddGrpCat.uliftFunctor.obj X = AddGrpCat.of (ULift.{u, v} ↑X)
• CommGrpCat.uliftFunctor_obj 📋 Mathlib.Algebra.Category.Grp.Basic
  (X : CommGrpCat) : CommGrpCat.uliftFunctor.obj X = CommGrpCat.of (ULift.{u, v} ↑X)
• GrpCat.uliftFunctor_obj 📋 Mathlib.Algebra.Category.Grp.Basic
  (X : GrpCat) : GrpCat.uliftFunctor.obj X = GrpCat.of (ULift.{u, v} ↑X)
• SemiRingCat.forget_obj 📋 Mathlib.Algebra.Category.Ring.Basic
  {R : SemiRingCat} : (CategoryTheory.forget SemiRingCat).obj R = ↑R
• CommSemiRingCat.forget_obj 📋 Mathlib.Algebra.Category.Ring.Basic
  {R : CommSemiRingCat} : (CategoryTheory.forget CommSemiRingCat).obj R = ↑R
• RingCat.forget_obj 📋 Mathlib.Algebra.Category.Ring.Basic
  {R : RingCat} : (CategoryTheory.forget RingCat).obj R = ↑R
• CommRingCat.forget_obj 📋 Mathlib.Algebra.Category.Ring.Basic
  {R : CommRingCat} : (CategoryTheory.forget CommRingCat).obj R = ↑R
• CommRingCat.forgetToRingCat_obj 📋 Mathlib.Algebra.Category.Ring.Basic
  {R : CommRingCat} : ↑((CategoryTheory.forget₂ CommRingCat RingCat).obj R) = ↑R
• CommRingCat.forget₂_obj_coe 📋 Mathlib.Algebra.Category.Ring.Basic
  (M : CommRingCat) : ↑(CategoryTheory.HasForget₂.forget₂.obj M) = ↑M
• CategoryTheory.Functor.hom_obj 📋 Mathlib.CategoryTheory.Functor.Hom
  (C : Type u) [CategoryTheory.Category.{v, u} C] (p : Cᵒᵖ × C) : (CategoryTheory.Functor.hom C).obj p = (Opposite.unop p.1 ⟶ p.2)
• CategoryTheory.yoneda_obj_obj 📋 Mathlib.CategoryTheory.Yoneda
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (X : C) (Y : Cᵒᵖ) : (CategoryTheory.yoneda.obj X).obj Y = (Opposite.unop Y ⟶ X)
• CategoryTheory.uliftYoneda_obj_obj 📋 Mathlib.CategoryTheory.Yoneda
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (X : C) (X✝ : Cᵒᵖ) : (CategoryTheory.uliftYoneda.{w, v₁, u₁}.obj X).obj X✝ = ULift.{w, v₁} (Opposite.unop X✝ ⟶ X)
• CategoryTheory.yoneda_obj_map 📋 Mathlib.CategoryTheory.Yoneda
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (X : C) {X✝ Y✝ : Cᵒᵖ} (f : X✝ ⟶ Y✝) (g : Opposite.unop X✝ ⟶ X) : (CategoryTheory.yoneda.obj X).map f g = CategoryTheory.CategoryStruct.comp f.unop g
• CategoryTheory.uliftYoneda_obj_map_down 📋 Mathlib.CategoryTheory.Yoneda
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (X : C) {X✝ Y✝ : Cᵒᵖ} (f : X✝ ⟶ Y✝) (a✝ : CategoryTheory.uliftFunctor.{w, v₁}.obj ((CategoryTheory.yoneda.obj X).obj X✝)) : ((CategoryTheory.uliftYoneda.{w, v₁, u₁}.obj X).map f a✝).down = CategoryTheory.CategoryStruct.comp f.unop a✝.down
• CategoryTheory.Adjunction.leftAdjointOfEquiv_obj 📋 Mathlib.CategoryTheory.Adjunction.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {G : CategoryTheory.Functor D C} {F_obj : C → D} (e : (X : C) → (Y : D) → (F_obj X ⟶ Y) ≃ (X ⟶ G.obj Y)) (he : ∀ (X : C) (Y Y' : D) (g : Y ⟶ Y') (h : F_obj X ⟶ Y), (e X Y') (CategoryTheory.CategoryStruct.comp h g) = CategoryTheory.CategoryStruct.comp ((e X Y) h) (G.map g)) (a✝ : C) : (CategoryTheory.Adjunction.leftAdjointOfEquiv e he).obj a✝ = F_obj a✝
• CategoryTheory.Adjunction.rightAdjointOfEquiv_obj 📋 Mathlib.CategoryTheory.Adjunction.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G_obj : D → C} (e : (X : C) → (Y : D) → (F.obj X ⟶ Y) ≃ (X ⟶ G_obj Y)) (he : ∀ (X' X : C) (Y : D) (f : X' ⟶ X) (g : F.obj X ⟶ Y), (e X' Y) (CategoryTheory.CategoryStruct.comp (F.map f) g) = CategoryTheory.CategoryStruct.comp f ((e X Y) g)) (a✝ : D) : (CategoryTheory.Adjunction.rightAdjointOfEquiv e he).obj a✝ = G_obj a✝
• CategoryTheory.Limits.Cocones.forget_obj 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor J C) (t : CategoryTheory.Limits.Cocone F) : (CategoryTheory.Limits.Cocones.forget F).obj t = t.pt
• CategoryTheory.Limits.Cones.forget_obj 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor J C) (t : CategoryTheory.Limits.Cone F) : (CategoryTheory.Limits.Cones.forget F).obj t = t.pt
• CategoryTheory.Functor.cocones_obj 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor J C) (X : C) : F.cocones.obj X = (F ⟶ (CategoryTheory.Functor.const J).obj X)
• CategoryTheory.Functor.cones_obj 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor J C) (X : Cᵒᵖ) : F.cones.obj X = ((CategoryTheory.Functor.const J).obj (Opposite.unop X) ⟶ F)
• CategoryTheory.Limits.Cocones.precompose_obj_pt 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F G : CategoryTheory.Functor J C} (α : G ⟶ F) (c : CategoryTheory.Limits.Cocone F) : ((CategoryTheory.Limits.Cocones.precompose α).obj c).pt = c.pt
• CategoryTheory.Limits.Cones.postcompose_obj_pt 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F G : CategoryTheory.Functor J C} (α : F ⟶ G) (c : CategoryTheory.Limits.Cone F) : ((CategoryTheory.Limits.Cones.postcompose α).obj c).pt = c.pt
• CategoryTheory.Limits.Cocones.whiskering_obj 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (E : CategoryTheory.Functor K J) (c : CategoryTheory.Limits.Cocone F) : (CategoryTheory.Limits.Cocones.whiskering E).obj c = CategoryTheory.Limits.Cocone.whisker E c
• CategoryTheory.Limits.Cones.whiskering_obj 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (E : CategoryTheory.Functor K J) (c : CategoryTheory.Limits.Cone F) : (CategoryTheory.Limits.Cones.whiskering E).obj c = CategoryTheory.Limits.Cone.whisker E c

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using (by default) Ctrl-K Ctrl-S. 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.

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.

This is Loogle revision 6ff4759 serving mathlib revision 519f454