Loogle!

Result

Found 6746 declarations mentioning CategoryTheory.Iso.hom. Of these, only the first 200 are shown.

• CategoryTheory.Iso.hom 📋 Mathlib.CategoryTheory.Iso
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (self : X ≅ Y) : X ⟶ Y
• CategoryTheory.Iso.isIso_hom 📋 Mathlib.CategoryTheory.Iso
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (e : X ≅ Y) : CategoryTheory.IsIso e.hom
• CategoryTheory.Iso.refl_hom 📋 Mathlib.CategoryTheory.Iso
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) : (CategoryTheory.Iso.refl X).hom = CategoryTheory.CategoryStruct.id X
• CategoryTheory.Iso.symm_hom 📋 Mathlib.CategoryTheory.Iso
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (α : X ≅ Y) : α.symm.hom = α.inv
• CategoryTheory.Iso.symm_inv 📋 Mathlib.CategoryTheory.Iso
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (α : X ≅ Y) : α.symm.inv = α.hom
• CategoryTheory.asIso_hom 📋 Mathlib.CategoryTheory.Iso
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.IsIso f] : (CategoryTheory.asIso f).hom = f
• CategoryTheory.IsIso.Iso.inv_hom 📋 Mathlib.CategoryTheory.Iso
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ≅ Y) : CategoryTheory.inv f.hom = f.inv
• CategoryTheory.IsIso.Iso.inv_inv 📋 Mathlib.CategoryTheory.Iso
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ≅ Y) : CategoryTheory.inv f.inv = f.hom
• CategoryTheory.Iso.ext 📋 Mathlib.CategoryTheory.Iso
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} ⦃α β : X ≅ Y⦄ (w : α.hom = β.hom) : α = β
• CategoryTheory.Iso.ext_iff 📋 Mathlib.CategoryTheory.Iso
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {α β : X ≅ Y} : α = β ↔ α.hom = β.hom
• CategoryTheory.Iso.hom_inv_id 📋 Mathlib.CategoryTheory.Iso
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (self : X ≅ Y) : CategoryTheory.CategoryStruct.comp self.hom self.inv = CategoryTheory.CategoryStruct.id X
• CategoryTheory.Iso.inv_hom_id 📋 Mathlib.CategoryTheory.Iso
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (self : X ≅ Y) : CategoryTheory.CategoryStruct.comp self.inv self.hom = CategoryTheory.CategoryStruct.id Y
• CategoryTheory.asIso'_inv 📋 Mathlib.CategoryTheory.Iso
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : Y ⟶ X) [CategoryTheory.IsIso f] : (CategoryTheory.asIso' f).hom = CategoryTheory.inv f
• CategoryTheory.Iso.trans_hom 📋 Mathlib.CategoryTheory.Iso
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : C} (α : X ≅ Y) (β : Y ≅ Z) : (α ≪≫ β).hom = CategoryTheory.CategoryStruct.comp α.hom β.hom
• CategoryTheory.Iso.hom_eq_inv 📋 Mathlib.CategoryTheory.Iso
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (α : X ≅ Y) (β : Y ≅ X) : α.hom = β.inv ↔ β.hom = α.inv
• CategoryTheory.Iso.hom_inv_id_assoc 📋 Mathlib.CategoryTheory.Iso
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (self : X ≅ Y) {Z : C} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp self.hom (CategoryTheory.CategoryStruct.comp self.inv h) = h
• CategoryTheory.Iso.inv_eq_hom 📋 Mathlib.CategoryTheory.Iso
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (α : X ≅ Y) (β : Y ≅ X) : α.inv = β.hom ↔ β.inv = α.hom
• CategoryTheory.Iso.inv_eq_inv 📋 Mathlib.CategoryTheory.Iso
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f g : X ≅ Y) : f.inv = g.inv ↔ f.hom = g.hom
• CategoryTheory.Iso.inv_hom_id_assoc 📋 Mathlib.CategoryTheory.Iso
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (self : X ≅ Y) {Z : C} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp self.inv (CategoryTheory.CategoryStruct.comp self.hom h) = h
• CategoryTheory.Iso.inv_ext 📋 Mathlib.CategoryTheory.Iso
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ≅ Y} {g : Y ⟶ X} (hom_inv_id : CategoryTheory.CategoryStruct.comp f.hom g = CategoryTheory.CategoryStruct.id X) : f.inv = g
• CategoryTheory.Iso.inv_ext' 📋 Mathlib.CategoryTheory.Iso
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ≅ Y} {g : Y ⟶ X} (hom_inv_id : CategoryTheory.CategoryStruct.comp f.hom g = CategoryTheory.CategoryStruct.id X) : g = f.inv
• CategoryTheory.Iso.comp_hom_eq_id 📋 Mathlib.CategoryTheory.Iso
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (α : X ≅ Y) {f : Y ⟶ X} : CategoryTheory.CategoryStruct.comp f α.hom = CategoryTheory.CategoryStruct.id Y ↔ f = α.inv
• CategoryTheory.Iso.comp_inv_eq_id 📋 Mathlib.CategoryTheory.Iso
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (α : X ≅ Y) {f : X ⟶ Y} : CategoryTheory.CategoryStruct.comp f α.inv = CategoryTheory.CategoryStruct.id X ↔ f = α.hom
• CategoryTheory.Iso.hom_comp_eq_id 📋 Mathlib.CategoryTheory.Iso
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (α : X ≅ Y) {f : Y ⟶ X} : CategoryTheory.CategoryStruct.comp α.hom f = CategoryTheory.CategoryStruct.id X ↔ f = α.inv
• CategoryTheory.Iso.inv_comp_eq_id 📋 Mathlib.CategoryTheory.Iso
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (α : X ≅ Y) {f : X ⟶ Y} : CategoryTheory.CategoryStruct.comp α.inv f = CategoryTheory.CategoryStruct.id Y ↔ f = α.hom
• CategoryTheory.Functor.mapIso_hom 📋 Mathlib.CategoryTheory.Iso
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) {X Y : C} (i : X ≅ Y) : (F.mapIso i).hom = F.map i.hom
• CategoryTheory.Iso.cancel_iso_hom_left 📋 Mathlib.CategoryTheory.Iso
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : X ≅ Y) (g g' : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp f.hom g = CategoryTheory.CategoryStruct.comp f.hom g' ↔ g = g'
• CategoryTheory.Iso.cancel_iso_hom_right 📋 Mathlib.CategoryTheory.Iso
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : C} (f f' : X ⟶ Y) (g : Y ≅ Z) : CategoryTheory.CategoryStruct.comp f g.hom = CategoryTheory.CategoryStruct.comp f' g.hom ↔ f = f'
• CategoryTheory.Iso.comp_inv_eq 📋 Mathlib.CategoryTheory.Iso
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : C} (α : X ≅ Y) {f : Z ⟶ Y} {g : Z ⟶ X} : CategoryTheory.CategoryStruct.comp f α.inv = g ↔ f = CategoryTheory.CategoryStruct.comp g α.hom
• CategoryTheory.Iso.eq_comp_inv 📋 Mathlib.CategoryTheory.Iso
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : C} (α : X ≅ Y) {f : Z ⟶ Y} {g : Z ⟶ X} : g = CategoryTheory.CategoryStruct.comp f α.inv ↔ CategoryTheory.CategoryStruct.comp g α.hom = f
• CategoryTheory.Iso.eq_inv_comp 📋 Mathlib.CategoryTheory.Iso
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : C} (α : X ≅ Y) {f : X ⟶ Z} {g : Y ⟶ Z} : g = CategoryTheory.CategoryStruct.comp α.inv f ↔ CategoryTheory.CategoryStruct.comp α.hom g = f
• CategoryTheory.Iso.inv_comp_eq 📋 Mathlib.CategoryTheory.Iso
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : C} (α : X ≅ Y) {f : X ⟶ Z} {g : Y ⟶ Z} : CategoryTheory.CategoryStruct.comp α.inv f = g ↔ f = CategoryTheory.CategoryStruct.comp α.hom g
• CategoryTheory.Functor.map_hom_inv' 📋 Mathlib.CategoryTheory.Iso
  {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.CategoryStruct.comp (F.map f.hom) (F.map f.inv) = CategoryTheory.CategoryStruct.id (F.obj X)
• CategoryTheory.Functor.map_inv_hom' 📋 Mathlib.CategoryTheory.Iso
  {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.CategoryStruct.comp (F.map f.inv) (F.map f.hom) = CategoryTheory.CategoryStruct.id (F.obj Y)
• CategoryTheory.Iso.map_hom_inv_id 📋 Mathlib.CategoryTheory.Iso
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] {X Y : C} (e : X ≅ Y) (F : CategoryTheory.Functor C D) : CategoryTheory.CategoryStruct.comp (F.map e.hom) (F.map e.inv) = CategoryTheory.CategoryStruct.id (F.obj X)
• CategoryTheory.Iso.map_inv_hom_id 📋 Mathlib.CategoryTheory.Iso
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] {X Y : C} (e : X ≅ Y) (F : CategoryTheory.Functor C D) : CategoryTheory.CategoryStruct.comp (F.map e.inv) (F.map e.hom) = CategoryTheory.CategoryStruct.id (F.obj Y)
• CategoryTheory.Functor.map_hom_inv'_assoc 📋 Mathlib.CategoryTheory.Iso
  {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) {Z : D} (h : F.obj X ⟶ Z) : CategoryTheory.CategoryStruct.comp (F.map f.hom) (CategoryTheory.CategoryStruct.comp (F.map f.inv) h) = h
• CategoryTheory.Functor.map_inv_hom'_assoc 📋 Mathlib.CategoryTheory.Iso
  {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) {Z : D} (h : F.obj Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (F.map f.inv) (CategoryTheory.CategoryStruct.comp (F.map f.hom) h) = h
• CategoryTheory.Iso.map_hom_inv_id_assoc 📋 Mathlib.CategoryTheory.Iso
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] {X Y : C} (e : X ≅ Y) (F : CategoryTheory.Functor C D) {Z : D} (h : F.obj X ⟶ Z) : CategoryTheory.CategoryStruct.comp (F.map e.hom) (CategoryTheory.CategoryStruct.comp (F.map e.inv) h) = h
• CategoryTheory.Iso.map_inv_hom_id_assoc 📋 Mathlib.CategoryTheory.Iso
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] {X Y : C} (e : X ≅ Y) (F : CategoryTheory.Functor C D) {Z : D} (h : F.obj Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (F.map e.inv) (CategoryTheory.CategoryStruct.comp (F.map e.hom) h) = h
• CategoryTheory.Iso.cancel_iso_hom_right_assoc 📋 Mathlib.CategoryTheory.Iso
  {C : Type u} [CategoryTheory.Category.{v, u} C] {W X X' Y Z : C} (f : W ⟶ X) (g : X ⟶ Y) (f' : W ⟶ X') (g' : X' ⟶ Y) (h : Y ≅ Z) : CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g h.hom) = CategoryTheory.CategoryStruct.comp f' (CategoryTheory.CategoryStruct.comp g' h.hom) ↔ CategoryTheory.CategoryStruct.comp f g = CategoryTheory.CategoryStruct.comp f' g'
• CategoryTheory.Iso.homToEquiv_apply 📋 Mathlib.CategoryTheory.Iso
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (α : X ≅ Y) {Z : C} (f : Z ⟶ X) : α.homToEquiv f = CategoryTheory.CategoryStruct.comp f α.hom
• CategoryTheory.Iso.homFromEquiv_symm_apply 📋 Mathlib.CategoryTheory.Iso
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (α : X ≅ Y) {Z : C} (g : Y ⟶ Z) : α.homFromEquiv.symm g = CategoryTheory.CategoryStruct.comp α.hom g
• CategoryTheory.Functor.leftUnitor_hom_app 📋 Mathlib.CategoryTheory.Functor.Category
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) (X : C) : F.leftUnitor.hom.app X = CategoryTheory.CategoryStruct.id (F.obj X)
• CategoryTheory.Functor.rightUnitor_hom_app 📋 Mathlib.CategoryTheory.Functor.Category
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) (X : C) : F.rightUnitor.hom.app X = CategoryTheory.CategoryStruct.id (F.obj X)
• CategoryTheory.Functor.associator_hom_app 📋 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] {E' : Type u₄} [CategoryTheory.Category.{v₄, u₄} E'] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) (H : CategoryTheory.Functor E E') (x✝ : C) : (F.associator G H).hom.app x✝ = CategoryTheory.CategoryStruct.id (((F.comp G).comp H).obj x✝)
• CategoryTheory.Iso.map_hom_inv_id_app 📋 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] {X Y : C} (e : X ≅ Y) (F : CategoryTheory.Functor C (CategoryTheory.Functor D E)) (Z : D) : CategoryTheory.CategoryStruct.comp ((F.map e.hom).app Z) ((F.map e.inv).app Z) = CategoryTheory.CategoryStruct.id ((F.obj X).obj Z)
• CategoryTheory.Iso.map_inv_hom_id_app 📋 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] {X Y : C} (e : X ≅ Y) (F : CategoryTheory.Functor C (CategoryTheory.Functor D E)) (Z : D) : CategoryTheory.CategoryStruct.comp ((F.map e.inv).app Z) ((F.map e.hom).app Z) = CategoryTheory.CategoryStruct.id ((F.obj Y).obj Z)
• CategoryTheory.Iso.map_hom_inv_id_app_assoc 📋 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] {X Y : C} (e : X ≅ Y) (F : CategoryTheory.Functor C (CategoryTheory.Functor D E)) (Z : D) {Z✝ : E} (h : (F.obj X).obj Z ⟶ Z✝) : CategoryTheory.CategoryStruct.comp ((F.map e.hom).app Z) (CategoryTheory.CategoryStruct.comp ((F.map e.inv).app Z) h) = h
• CategoryTheory.Iso.map_inv_hom_id_app_assoc 📋 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] {X Y : C} (e : X ≅ Y) (F : CategoryTheory.Functor C (CategoryTheory.Functor D E)) (Z : D) {Z✝ : E} (h : (F.obj Y).obj Z ⟶ Z✝) : CategoryTheory.CategoryStruct.comp ((F.map e.inv).app Z) (CategoryTheory.CategoryStruct.comp ((F.map e.hom).app Z) h) = h
• CategoryTheory.NatIso.hom_app_isIso 📋 Mathlib.CategoryTheory.NatIso
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F G : CategoryTheory.Functor C D} (α : F ≅ G) (X : C) : CategoryTheory.IsIso (α.hom.app X)
• CategoryTheory.Iso.app_hom 📋 Mathlib.CategoryTheory.NatIso
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F G : CategoryTheory.Functor C D} (α : F ≅ G) (X : C) : (α.app X).hom = α.hom.app X
• CategoryTheory.Functor.isoCopyObj_hom_app 📋 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) (X : C) : (F.isoCopyObj obj e).hom.app X = (e X).hom
• CategoryTheory.NatIso.inv_hom_app 📋 Mathlib.CategoryTheory.NatIso
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F G : CategoryTheory.Functor C D} (e : F ≅ G) (X : C) : CategoryTheory.inv (e.hom.app X) = e.inv.app X
• CategoryTheory.NatIso.inv_inv_app 📋 Mathlib.CategoryTheory.NatIso
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F G : CategoryTheory.Functor C D} (e : F ≅ G) (X : C) : CategoryTheory.inv (e.inv.app X) = e.hom.app X
• CategoryTheory.Iso.hom_inv_id_app 📋 Mathlib.CategoryTheory.NatIso
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F G : CategoryTheory.Functor C D} (α : F ≅ G) (X : C) : CategoryTheory.CategoryStruct.comp (α.hom.app X) (α.inv.app X) = CategoryTheory.CategoryStruct.id (F.obj X)
• CategoryTheory.Iso.inv_hom_id_app 📋 Mathlib.CategoryTheory.NatIso
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F G : CategoryTheory.Functor C D} (α : F ≅ G) (X : C) : CategoryTheory.CategoryStruct.comp (α.inv.app X) (α.hom.app X) = CategoryTheory.CategoryStruct.id (G.obj X)
• CategoryTheory.Iso.hom_inv_id_app_assoc 📋 Mathlib.CategoryTheory.NatIso
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F G : CategoryTheory.Functor C D} (α : F ≅ G) (X : C) {Z : D} (h : F.obj X ⟶ Z) : CategoryTheory.CategoryStruct.comp (α.hom.app X) (CategoryTheory.CategoryStruct.comp (α.inv.app X) h) = h
• CategoryTheory.Iso.inv_hom_id_app_assoc 📋 Mathlib.CategoryTheory.NatIso
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F G : CategoryTheory.Functor C D} (α : F ≅ G) (X : C) {Z : D} (h : G.obj X ⟶ Z) : CategoryTheory.CategoryStruct.comp (α.inv.app X) (CategoryTheory.CategoryStruct.comp (α.hom.app X) h) = h
• CategoryTheory.NatTrans.naturality_1 📋 Mathlib.CategoryTheory.NatIso
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F G : CategoryTheory.Functor C D} (α : F ⟶ G) {X Y : C} (e : X ≅ Y) : CategoryTheory.CategoryStruct.comp (F.map e.inv) (CategoryTheory.CategoryStruct.comp (α.app X) (G.map e.hom)) = α.app Y
• CategoryTheory.NatTrans.naturality_2 📋 Mathlib.CategoryTheory.NatIso
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F G : CategoryTheory.Functor C D} (α : F ⟶ G) {X Y : C} (e : X ≅ Y) : CategoryTheory.CategoryStruct.comp (F.map e.hom) (CategoryTheory.CategoryStruct.comp (α.app Y) (G.map e.inv)) = α.app X
• CategoryTheory.NatIso.naturality_1 📋 Mathlib.CategoryTheory.NatIso
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F G : CategoryTheory.Functor C D} {X Y : C} (α : F ≅ G) (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp (α.inv.app X) (CategoryTheory.CategoryStruct.comp (F.map f) (α.hom.app Y)) = G.map f
• CategoryTheory.NatIso.naturality_2 📋 Mathlib.CategoryTheory.NatIso
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F G : CategoryTheory.Functor C D} {X Y : C} (α : F ≅ G) (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp (α.hom.app X) (CategoryTheory.CategoryStruct.comp (G.map f) (α.inv.app Y)) = F.map f
• CategoryTheory.NatIso.hcomp_hom 📋 Mathlib.CategoryTheory.NatIso
  {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 : CategoryTheory.Functor C D} {H I : CategoryTheory.Functor D E} (α : F ≅ G) (β : H ≅ I) : (CategoryTheory.NatIso.hcomp α β).hom = α.hom ◫ β.hom
• CategoryTheory.NatIso.cancel_natIso_hom_left 📋 Mathlib.CategoryTheory.NatIso
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F G : CategoryTheory.Functor C D} (α : F ≅ G) {X : C} {Y : D} (g g' : G.obj X ⟶ Y) : CategoryTheory.CategoryStruct.comp (α.hom.app X) g = CategoryTheory.CategoryStruct.comp (α.hom.app X) g' ↔ g = g'
• CategoryTheory.NatIso.cancel_natIso_hom_right 📋 Mathlib.CategoryTheory.NatIso
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F G : CategoryTheory.Functor C D} (α : F ≅ G) {X : C} {Y : D} (g g' : Y ⟶ F.obj X) : CategoryTheory.CategoryStruct.comp g (α.hom.app X) = CategoryTheory.CategoryStruct.comp g' (α.hom.app X) ↔ g = g'
• CategoryTheory.NatIso.ofComponents 📋 Mathlib.CategoryTheory.NatIso
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F G : CategoryTheory.Functor C D} (app : (X : C) → F.obj X ≅ G.obj X) (naturality : ∀ {X Y : C} (f : X ⟶ Y), CategoryTheory.CategoryStruct.comp (F.map f) (app Y).hom = CategoryTheory.CategoryStruct.comp (app X).hom (G.map f) := by cat_disch) : F ≅ G
• CategoryTheory.NatTrans.naturality_1_assoc 📋 Mathlib.CategoryTheory.NatIso
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F G : CategoryTheory.Functor C D} (α : F ⟶ G) {X Y : C} (e : X ≅ Y) {Z : D} (h : G.obj Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (F.map e.inv) (CategoryTheory.CategoryStruct.comp (α.app X) (CategoryTheory.CategoryStruct.comp (G.map e.hom) h)) = CategoryTheory.CategoryStruct.comp (α.app Y) h
• CategoryTheory.NatTrans.naturality_2_assoc 📋 Mathlib.CategoryTheory.NatIso
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F G : CategoryTheory.Functor C D} (α : F ⟶ G) {X Y : C} (e : X ≅ Y) {Z : D} (h : G.obj X ⟶ Z) : CategoryTheory.CategoryStruct.comp (F.map e.hom) (CategoryTheory.CategoryStruct.comp (α.app Y) (CategoryTheory.CategoryStruct.comp (G.map e.inv) h)) = CategoryTheory.CategoryStruct.comp (α.app X) h
• CategoryTheory.NatIso.ofComponents.app 📋 Mathlib.CategoryTheory.NatIso
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F G : CategoryTheory.Functor C D} (app' : (X : C) → F.obj X ≅ G.obj X) (naturality : ∀ {X Y : C} (f : X ⟶ Y), CategoryTheory.CategoryStruct.comp (F.map f) (app' Y).hom = CategoryTheory.CategoryStruct.comp (app' X).hom (G.map f)) (X : C) : (CategoryTheory.NatIso.ofComponents app' naturality).app X = app' X
• CategoryTheory.NatIso.naturality_1_assoc 📋 Mathlib.CategoryTheory.NatIso
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F G : CategoryTheory.Functor C D} {X Y : C} (α : F ≅ G) (f : X ⟶ Y) {Z : D} (h : G.obj Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (α.inv.app X) (CategoryTheory.CategoryStruct.comp (F.map f) (CategoryTheory.CategoryStruct.comp (α.hom.app Y) h)) = CategoryTheory.CategoryStruct.comp (G.map f) h
• CategoryTheory.NatIso.naturality_2_assoc 📋 Mathlib.CategoryTheory.NatIso
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F G : CategoryTheory.Functor C D} {X Y : C} (α : F ≅ G) (f : X ⟶ Y) {Z : D} (h : F.obj Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (α.hom.app X) (CategoryTheory.CategoryStruct.comp (G.map f) (CategoryTheory.CategoryStruct.comp (α.inv.app Y) h)) = CategoryTheory.CategoryStruct.comp (F.map f) h
• CategoryTheory.NatIso.ofComponents'_hom_app 📋 Mathlib.CategoryTheory.NatIso
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F G : CategoryTheory.Functor C D} (app : (X : C) → F.obj X ≅ G.obj X) (naturality : ∀ {X Y : C} (f : Y ⟶ X), CategoryTheory.CategoryStruct.comp (app Y).inv (F.map f) = CategoryTheory.CategoryStruct.comp (G.map f) (app X).inv := by cat_disch) (X : C) : (CategoryTheory.NatIso.ofComponents' app naturality).hom.app X = (app X).hom
• CategoryTheory.NatIso.ofComponents_hom_app 📋 Mathlib.CategoryTheory.NatIso
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F G : CategoryTheory.Functor C D} (app : (X : C) → F.obj X ≅ G.obj X) (naturality : ∀ {X Y : C} (f : X ⟶ Y), CategoryTheory.CategoryStruct.comp (F.map f) (app Y).hom = CategoryTheory.CategoryStruct.comp (app X).hom (G.map f) := by cat_disch) (X : C) : (CategoryTheory.NatIso.ofComponents app naturality).hom.app X = (app X).hom
• CategoryTheory.NatIso.ofComponents_inv_app 📋 Mathlib.CategoryTheory.NatIso
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F G : CategoryTheory.Functor C D} (app : (X : C) → F.obj X ≅ G.obj X) (naturality : ∀ {X Y : C} (f : X ⟶ Y), CategoryTheory.CategoryStruct.comp (F.map f) (app Y).hom = CategoryTheory.CategoryStruct.comp (app X).hom (G.map f) := by cat_disch) (X : C) : (CategoryTheory.NatIso.ofComponents app naturality).inv.app X = (app X).inv
• CategoryTheory.NatIso.cancel_natIso_hom_right_assoc 📋 Mathlib.CategoryTheory.NatIso
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F G : CategoryTheory.Functor C D} (α : F ≅ G) {W X X' : D} {Y : C} (f : W ⟶ X) (g : X ⟶ F.obj Y) (f' : W ⟶ X') (g' : X' ⟶ F.obj Y) : CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g (α.hom.app Y)) = CategoryTheory.CategoryStruct.comp f' (CategoryTheory.CategoryStruct.comp g' (α.hom.app Y)) ↔ CategoryTheory.CategoryStruct.comp f g = CategoryTheory.CategoryStruct.comp f' g'
• CategoryTheory.NatIso.inv_map_hom_app 📋 Mathlib.CategoryTheory.NatIso
  {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)) {X Y : C} (e : X ≅ Y) (Z : D) : CategoryTheory.inv ((F.map e.hom).app Z) = (F.map e.inv).app Z
• CategoryTheory.NatIso.inv_map_inv_app 📋 Mathlib.CategoryTheory.NatIso
  {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)) {X Y : C} (e : X ≅ Y) (Z : D) : CategoryTheory.inv ((F.map e.inv).app Z) = (F.map e.hom).app Z
• CategoryTheory.Iso.hom_inv_id_app_app 📋 Mathlib.CategoryTheory.NatIso
  {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 : CategoryTheory.Functor C (CategoryTheory.Functor D E)} (e : F ≅ G) (X₁ : C) (X₂ : D) : CategoryTheory.CategoryStruct.comp ((e.hom.app X₁).app X₂) ((e.inv.app X₁).app X₂) = CategoryTheory.CategoryStruct.id ((F.obj X₁).obj X₂)
• CategoryTheory.Iso.inv_hom_id_app_app 📋 Mathlib.CategoryTheory.NatIso
  {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 : CategoryTheory.Functor C (CategoryTheory.Functor D E)} (e : F ≅ G) (X₁ : C) (X₂ : D) : CategoryTheory.CategoryStruct.comp ((e.inv.app X₁).app X₂) ((e.hom.app X₁).app X₂) = CategoryTheory.CategoryStruct.id ((G.obj X₁).obj X₂)
• CategoryTheory.Iso.hom_inv_id_app_app_assoc 📋 Mathlib.CategoryTheory.NatIso
  {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 : CategoryTheory.Functor C (CategoryTheory.Functor D E)} (e : F ≅ G) (X₁ : C) (X₂ : D) {Z : E} (h : (F.obj X₁).obj X₂ ⟶ Z) : CategoryTheory.CategoryStruct.comp ((e.hom.app X₁).app X₂) (CategoryTheory.CategoryStruct.comp ((e.inv.app X₁).app X₂) h) = h
• CategoryTheory.Iso.inv_hom_id_app_app_assoc 📋 Mathlib.CategoryTheory.NatIso
  {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 : CategoryTheory.Functor C (CategoryTheory.Functor D E)} (e : F ≅ G) (X₁ : C) (X₂ : D) {Z : E} (h : (G.obj X₁).obj X₂ ⟶ Z) : CategoryTheory.CategoryStruct.comp ((e.inv.app X₁).app X₂) (CategoryTheory.CategoryStruct.comp ((e.hom.app X₁).app X₂) h) = h
• CategoryTheory.Iso.hom_inv_id_app_app_app 📋 Mathlib.CategoryTheory.NatIso
  {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' : Type u₄} [CategoryTheory.Category.{v₄, u₄} E'] {F G : CategoryTheory.Functor C (CategoryTheory.Functor D (CategoryTheory.Functor E E'))} (e : F ≅ G) (X₁ : C) (X₂ : D) (X₃ : E) : CategoryTheory.CategoryStruct.comp (((e.hom.app X₁).app X₂).app X₃) (((e.inv.app X₁).app X₂).app X₃) = CategoryTheory.CategoryStruct.id (((F.obj X₁).obj X₂).obj X₃)
• CategoryTheory.Iso.inv_hom_id_app_app_app 📋 Mathlib.CategoryTheory.NatIso
  {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' : Type u₄} [CategoryTheory.Category.{v₄, u₄} E'] {F G : CategoryTheory.Functor C (CategoryTheory.Functor D (CategoryTheory.Functor E E'))} (e : F ≅ G) (X₁ : C) (X₂ : D) (X₃ : E) : CategoryTheory.CategoryStruct.comp (((e.inv.app X₁).app X₂).app X₃) (((e.hom.app X₁).app X₂).app X₃) = CategoryTheory.CategoryStruct.id (((G.obj X₁).obj X₂).obj X₃)
• CategoryTheory.Iso.hom_inv_id_app_app_app_assoc 📋 Mathlib.CategoryTheory.NatIso
  {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' : Type u₄} [CategoryTheory.Category.{v₄, u₄} E'] {F G : CategoryTheory.Functor C (CategoryTheory.Functor D (CategoryTheory.Functor E E'))} (e : F ≅ G) (X₁ : C) (X₂ : D) (X₃ : E) {Z : E'} (h : ((F.obj X₁).obj X₂).obj X₃ ⟶ Z) : CategoryTheory.CategoryStruct.comp (((e.hom.app X₁).app X₂).app X₃) (CategoryTheory.CategoryStruct.comp (((e.inv.app X₁).app X₂).app X₃) h) = h
• CategoryTheory.Iso.inv_hom_id_app_app_app_assoc 📋 Mathlib.CategoryTheory.NatIso
  {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' : Type u₄} [CategoryTheory.Category.{v₄, u₄} E'] {F G : CategoryTheory.Functor C (CategoryTheory.Functor D (CategoryTheory.Functor E E'))} (e : F ≅ G) (X₁ : C) (X₂ : D) (X₃ : E) {Z : E'} (h : ((G.obj X₁).obj X₂).obj X₃ ⟶ Z) : CategoryTheory.CategoryStruct.comp (((e.inv.app X₁).app X₂).app X₃) (CategoryTheory.CategoryStruct.comp (((e.hom.app X₁).app X₂).app X₃) h) = h
• CategoryTheory.Functor.FullyFaithful.preimageIso_hom 📋 Mathlib.CategoryTheory.Functor.FullyFaithful
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} (hF : F.FullyFaithful) {X Y : C} (e : F.obj X ≅ F.obj Y) : (hF.preimageIso e).hom = hF.preimage e.hom
• CategoryTheory.Functor.preimageIso_hom 📋 Mathlib.CategoryTheory.Functor.FullyFaithful
  {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.Full] [F.Faithful] (f : F.obj X ≅ F.obj Y) : (F.preimageIso f).hom = F.preimage f.hom
• CategoryTheory.Functor.fullyFaithfulCancelRight_hom_app 📋 Mathlib.CategoryTheory.Functor.FullyFaithful
  {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 : CategoryTheory.Functor C D} {H : CategoryTheory.Functor D E} [H.Full] [H.Faithful] (comp_iso : F.comp H ≅ G.comp H) (X : C) : (CategoryTheory.Functor.fullyFaithfulCancelRight H comp_iso).hom.app X = H.preimage (comp_iso.hom.app X)
• CategoryTheory.InducedCategory.isoMk_hom 📋 Mathlib.CategoryTheory.InducedCategory
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v, u₂} D] {F : C → D} {X Y : CategoryTheory.InducedCategory D F} (f : F X ≅ F Y) : (CategoryTheory.InducedCategory.isoMk f).hom = CategoryTheory.InducedCategory.homMk f.hom
• CategoryTheory.ObjectProperty.isoMk_hom 📋 Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) {X Y : P.FullSubcategory} (e : X.obj ≅ Y.obj) : (P.isoMk e).hom = CategoryTheory.ObjectProperty.homMk e.hom
• CategoryTheory.ObjectProperty.isoHom_inv_id_hom 📋 Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C} {X Y : P.FullSubcategory} (e : X ≅ Y) : CategoryTheory.CategoryStruct.comp e.hom.hom e.inv.hom = CategoryTheory.CategoryStruct.id X.obj
• CategoryTheory.ObjectProperty.isoInv_hom_id_hom 📋 Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C} {X Y : P.FullSubcategory} (e : X ≅ Y) : CategoryTheory.CategoryStruct.comp e.inv.hom e.hom.hom = CategoryTheory.CategoryStruct.id Y.obj
• CategoryTheory.ObjectProperty.isoHom_inv_id_hom_assoc 📋 Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C} {X Y : P.FullSubcategory} (e : X ≅ Y) {Z : C} (h : X.obj ⟶ Z) : CategoryTheory.CategoryStruct.comp e.hom.hom (CategoryTheory.CategoryStruct.comp e.inv.hom h) = h
• CategoryTheory.ObjectProperty.isoInv_hom_id_hom_assoc 📋 Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C} {X Y : P.FullSubcategory} (e : X ≅ Y) {Z : C} (h : Y.obj ⟶ Z) : CategoryTheory.CategoryStruct.comp e.inv.hom (CategoryTheory.CategoryStruct.comp e.hom.hom h) = h
• CategoryTheory.Iso.hom_inv_id_apply 📋 Mathlib.CategoryTheory.Elementwise
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (self : X ≅ Y) {F : C → C → Type uF} {carrier : C → Type w} {instFunLike : (X Y : C) → FunLike (F X Y) (carrier X) (carrier Y)} [inst : CategoryTheory.ConcreteCategory C F] (x : carrier X) : (CategoryTheory.ConcreteCategory.hom self.inv) ((CategoryTheory.ConcreteCategory.hom self.hom) x) = x
• CategoryTheory.Iso.inv_hom_id_apply 📋 Mathlib.CategoryTheory.Elementwise
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (self : X ≅ Y) {F : C → C → Type uF} {carrier : C → Type w} {instFunLike : (X Y : C) → FunLike (F X Y) (carrier X) (carrier Y)} [inst : CategoryTheory.ConcreteCategory C F] (x : carrier Y) : (CategoryTheory.ConcreteCategory.hom self.hom) ((CategoryTheory.ConcreteCategory.hom self.inv) x) = x
• CategoryTheory.Functor.isoWhiskerLeft_hom 📋 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 H : CategoryTheory.Functor D E} (α : G ≅ H) : (F.isoWhiskerLeft α).hom = F.whiskerLeft α.hom
• CategoryTheory.Functor.isoWhiskerRight_hom 📋 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] {G H : CategoryTheory.Functor C D} (α : G ≅ H) (F : CategoryTheory.Functor D E) : (CategoryTheory.Functor.isoWhiskerRight α F).hom = CategoryTheory.Functor.whiskerRight α.hom F
• CategoryTheory.Functor.triangle 📋 Mathlib.CategoryTheory.Whiskering
  {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 B C) : CategoryTheory.CategoryStruct.comp (F.associator (CategoryTheory.Functor.id B) G).hom (F.whiskerLeft G.leftUnitor.hom) = CategoryTheory.Functor.whiskerRight F.rightUnitor.hom G
• CategoryTheory.Functor.whiskerLeft_twice 📋 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] {B : Type u₄} [CategoryTheory.Category.{v₄, u₄} B] (F : CategoryTheory.Functor B C) (G : CategoryTheory.Functor C D) {H K : CategoryTheory.Functor D E} (α : H ⟶ K) : F.whiskerLeft (G.whiskerLeft α) = CategoryTheory.CategoryStruct.comp (F.associator G H).inv (CategoryTheory.CategoryStruct.comp ((F.comp G).whiskerLeft α) (F.associator G K).hom)
• CategoryTheory.Functor.whiskerRight_twice 📋 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] {B : Type u₄} [CategoryTheory.Category.{v₄, u₄} B] {H K : CategoryTheory.Functor B C} (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) (α : H ⟶ K) : CategoryTheory.Functor.whiskerRight (CategoryTheory.Functor.whiskerRight α F) G = CategoryTheory.CategoryStruct.comp (H.associator F G).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight α (F.comp G)) (K.associator F G).inv)
• CategoryTheory.Functor.whiskerRight_left 📋 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] {B : Type u₄} [CategoryTheory.Category.{v₄, u₄} B] (F : CategoryTheory.Functor B C) {G H : CategoryTheory.Functor C D} (α : G ⟶ H) (K : CategoryTheory.Functor D E) : CategoryTheory.Functor.whiskerRight (F.whiskerLeft α) K = CategoryTheory.CategoryStruct.comp (F.associator G K).hom (CategoryTheory.CategoryStruct.comp (F.whiskerLeft (CategoryTheory.Functor.whiskerRight α K)) (F.associator H K).inv)
• CategoryTheory.Functor.whiskeringLeftObjIdIso_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 C E) (X✝ : C) : (CategoryTheory.Functor.whiskeringLeftObjIdIso.hom.app X).app X✝ = CategoryTheory.CategoryStruct.id (X.obj X✝)
• 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.pentagon 📋 Mathlib.CategoryTheory.Whiskering
  {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] {E : Type u₅} [CategoryTheory.Category.{v₅, u₅} E] (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor B C) (H : CategoryTheory.Functor C D) (K : CategoryTheory.Functor D E) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight (F.associator G H).hom K) (CategoryTheory.CategoryStruct.comp (F.associator (G.comp H) K).hom (F.whiskerLeft (G.associator H K).hom)) = CategoryTheory.CategoryStruct.comp ((F.comp G).associator H K).hom (F.associator G (H.comp K)).hom
• CategoryTheory.Functor.whiskeringLeftObjCompIso_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 D' E) (X✝ : C) : ((F.whiskeringLeftObjCompIso G).hom.app X).app X✝ = CategoryTheory.CategoryStruct.id (X.obj (G.obj (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.toEssImageCompι_hom_app 📋 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.toEssImageCompι.hom.app X = CategoryTheory.CategoryStruct.id (F.obj X)
• CategoryTheory.Functor.essImage.liftFunctorCompIso_hom_app 📋 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)) (X : J) : (CategoryTheory.Functor.essImage.liftFunctorCompIso G F hG).hom.app X = (F.toEssImage.objObjPreimageIso { obj := G.obj X, property := ⋯ }).hom.hom
• CategoryTheory.Functor.essImage.liftFunctor_map 📋 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)) {i j : J} (f : i ⟶ j) : (CategoryTheory.Functor.essImage.liftFunctor G F hG).map f = F.preimage (CategoryTheory.CategoryStruct.comp (F.toEssImage.objObjPreimageIso { obj := G.obj i, property := ⋯ }).hom.hom (CategoryTheory.CategoryStruct.comp (G.map f) (F.toEssImage.objObjPreimageIso { obj := G.obj j, property := ⋯ }).inv.hom))
• CategoryTheory.Equivalence.mkIso_hom 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {e f : C ≌ D} (η : e.functor ≅ f.functor) : (CategoryTheory.Equivalence.mkIso η).hom = CategoryTheory.Equivalence.mkHom η.hom
• CategoryTheory.Functor.asEquivalence_counitIso_hom_app 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [F.IsEquivalence] (X : D) : F.asEquivalence.counitIso.hom.app X = (F.objObjPreimageIso X).hom
• CategoryTheory.Functor.asEquivalence_unitIso_hom_app 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [F.IsEquivalence] (X : C) : F.asEquivalence.unitIso.hom.app X = F.preimage (F.objObjPreimageIso (F.obj X)).inv
• CategoryTheory.Functor.asEquivalence_unitIso_inv_app 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [F.IsEquivalence] (X : C) : F.asEquivalence.unitIso.inv.app X = F.preimage (F.objObjPreimageIso (F.obj X)).hom
• CategoryTheory.Equivalence.funInvIdAssoc_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) (F : CategoryTheory.Functor C E) (X : C) : (e.funInvIdAssoc F).hom.app X = F.map (e.unitInv.app X)
• CategoryTheory.Equivalence.invFunIdAssoc_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) (F : CategoryTheory.Functor D E) (X : D) : (e.invFunIdAssoc F).hom.app X = F.map (e.counit.app X)
• CategoryTheory.Equivalence.mk' 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] (functor : CategoryTheory.Functor C D) (inverse : CategoryTheory.Functor D C) (unitIso : CategoryTheory.Functor.id C ≅ functor.comp inverse) (counitIso : inverse.comp functor ≅ CategoryTheory.Functor.id D) (functor_unitIso_comp : ∀ (X : C), CategoryTheory.CategoryStruct.comp (functor.map (unitIso.hom.app X)) (counitIso.hom.app (functor.obj X)) = CategoryTheory.CategoryStruct.id (functor.obj X) := by cat_disch) : C ≌ D
• CategoryTheory.Equivalence.adjointify_η_ε_assoc 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (η : CategoryTheory.Functor.id C ≅ F.comp G) (ε : G.comp F ≅ CategoryTheory.Functor.id D) (X : C) {Z : D} (h : F.obj X ⟶ Z) : CategoryTheory.CategoryStruct.comp (F.map ((CategoryTheory.Equivalence.adjointifyη η ε).hom.app X)) (CategoryTheory.CategoryStruct.comp (ε.hom.app (F.obj X)) h) = h
• CategoryTheory.Equivalence.changeFunctor_counitIso_hom_app 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) {G : CategoryTheory.Functor C D} (iso : e.functor ≅ G) (X : D) : (e.changeFunctor iso).counitIso.hom.app X = CategoryTheory.CategoryStruct.comp (iso.inv.app (e.inverse.obj X)) (e.counitIso.hom.app X)
• CategoryTheory.Equivalence.changeFunctor_counitIso_inv_app 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) {G : CategoryTheory.Functor C D} (iso : e.functor ≅ G) (X : D) : (e.changeFunctor iso).counitIso.inv.app X = CategoryTheory.CategoryStruct.comp (e.counitIso.inv.app X) (iso.hom.app (e.inverse.obj X))
• CategoryTheory.Equivalence.changeInverse_unitIso_hom_app 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) {G : CategoryTheory.Functor D C} (iso : e.inverse ≅ G) (X : C) : (e.changeInverse iso).unitIso.hom.app X = CategoryTheory.CategoryStruct.comp (e.unitIso.hom.app X) (iso.hom.app (e.functor.obj X))
• CategoryTheory.Equivalence.adjointify_η_ε 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (η : CategoryTheory.Functor.id C ≅ F.comp G) (ε : G.comp F ≅ CategoryTheory.Functor.id D) (X : C) : CategoryTheory.CategoryStruct.comp (F.map ((CategoryTheory.Equivalence.adjointifyη η ε).hom.app X)) (ε.hom.app (F.obj X)) = CategoryTheory.CategoryStruct.id (F.obj X)
• CategoryTheory.Equivalence.functor_unitIso_comp 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] (self : C ≌ D) (X : C) : CategoryTheory.CategoryStruct.comp (self.functor.map (self.unitIso.hom.app X)) (self.counitIso.hom.app (self.functor.obj X)) = CategoryTheory.CategoryStruct.id (self.functor.obj X)
• CategoryTheory.Equivalence.changeFunctor_unitIso_hom_app 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) {G : CategoryTheory.Functor C D} (iso : e.functor ≅ G) (X : C) : (e.changeFunctor iso).unitIso.hom.app X = CategoryTheory.CategoryStruct.comp (e.unitIso.hom.app X) (e.inverse.map (iso.hom.app X))
• CategoryTheory.Equivalence.changeInverse_counitIso_hom_app 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) {G : CategoryTheory.Functor D C} (iso : e.inverse ≅ G) (X : D) : (e.changeInverse iso).counitIso.hom.app X = CategoryTheory.CategoryStruct.comp (e.functor.map (iso.inv.app X)) (e.counitIso.hom.app X)
• CategoryTheory.Equivalence.changeInverse_counitIso_inv_app 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) {G : CategoryTheory.Functor D C} (iso : e.inverse ≅ G) (X : D) : (e.changeInverse iso).counitIso.inv.app X = CategoryTheory.CategoryStruct.comp (e.counitIso.inv.app X) (e.functor.map (iso.hom.app X))
• CategoryTheory.Equivalence.Equivalence_mk'_counit 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (functor : CategoryTheory.Functor C D) (inverse : CategoryTheory.Functor D C) (unit_iso : CategoryTheory.Functor.id C ≅ functor.comp inverse) (counit_iso : inverse.comp functor ≅ CategoryTheory.Functor.id D) (f : ∀ (X : C), CategoryTheory.CategoryStruct.comp (functor.map (unit_iso.hom.app X)) (counit_iso.hom.app (functor.obj X)) = CategoryTheory.CategoryStruct.id (functor.obj X)) : { functor := functor, inverse := inverse, unitIso := unit_iso, counitIso := counit_iso, functor_unitIso_comp := f }.counit = counit_iso.hom
• CategoryTheory.Equivalence.Equivalence_mk'_counitInv 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (functor : CategoryTheory.Functor C D) (inverse : CategoryTheory.Functor D C) (unit_iso : CategoryTheory.Functor.id C ≅ functor.comp inverse) (counit_iso : inverse.comp functor ≅ CategoryTheory.Functor.id D) (f : ∀ (X : C), CategoryTheory.CategoryStruct.comp (functor.map (unit_iso.hom.app X)) (counit_iso.hom.app (functor.obj X)) = CategoryTheory.CategoryStruct.id (functor.obj X)) : { functor := functor, inverse := inverse, unitIso := unit_iso, counitIso := counit_iso, functor_unitIso_comp := f }.counitInv = counit_iso.inv
• CategoryTheory.Equivalence.Equivalence_mk'_unit 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (functor : CategoryTheory.Functor C D) (inverse : CategoryTheory.Functor D C) (unit_iso : CategoryTheory.Functor.id C ≅ functor.comp inverse) (counit_iso : inverse.comp functor ≅ CategoryTheory.Functor.id D) (f : ∀ (X : C), CategoryTheory.CategoryStruct.comp (functor.map (unit_iso.hom.app X)) (counit_iso.hom.app (functor.obj X)) = CategoryTheory.CategoryStruct.id (functor.obj X)) : { functor := functor, inverse := inverse, unitIso := unit_iso, counitIso := counit_iso, functor_unitIso_comp := f }.unit = unit_iso.hom
• CategoryTheory.Equivalence.Equivalence_mk'_unitInv 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (functor : CategoryTheory.Functor C D) (inverse : CategoryTheory.Functor D C) (unit_iso : CategoryTheory.Functor.id C ≅ functor.comp inverse) (counit_iso : inverse.comp functor ≅ CategoryTheory.Functor.id D) (f : ∀ (X : C), CategoryTheory.CategoryStruct.comp (functor.map (unit_iso.hom.app X)) (counit_iso.hom.app (functor.obj X)) = CategoryTheory.CategoryStruct.id (functor.obj X)) : { functor := functor, inverse := inverse, unitIso := unit_iso, counitIso := counit_iso, functor_unitIso_comp := f }.unitInv = unit_iso.inv
• CategoryTheory.Iso.inverseCompIso_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] {F : CategoryTheory.Functor C E} {H : CategoryTheory.Functor D E} {G : C ≌ D} (i : F ≅ G.functor.comp H) (X : D) : i.inverseCompIso.hom.app X = CategoryTheory.CategoryStruct.comp (i.hom.app (G.inverse.obj X)) (H.map (G.counitIso.hom.app X))
• CategoryTheory.Iso.isoInverseComp_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] {F : CategoryTheory.Functor C E} {H : CategoryTheory.Functor D E} {G : C ≌ D} (i : G.functor.comp H ≅ F) (X : D) : i.isoInverseComp.hom.app X = CategoryTheory.CategoryStruct.comp (H.map (G.counitIso.inv.app X)) (i.hom.app (G.inverse.obj X))
• CategoryTheory.Iso.isoInverseComp_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] {F : CategoryTheory.Functor C E} {H : CategoryTheory.Functor D E} {G : C ≌ D} (i : G.functor.comp H ≅ F) (X : D) : i.isoInverseComp.inv.app X = CategoryTheory.CategoryStruct.comp (i.inv.app (G.inverse.obj X)) (H.map (G.counitIso.hom.app X))
• CategoryTheory.Iso.compInverseIso_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] {F : CategoryTheory.Functor C E} {G : CategoryTheory.Functor C D} {H : D ≌ E} (i : F ≅ G.comp H.functor) (X : C) : i.compInverseIso.hom.app X = CategoryTheory.CategoryStruct.comp (H.inverse.map (i.hom.app X)) (H.unitIso.inv.app (G.obj X))
• CategoryTheory.Iso.compInverseIso_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] {F : CategoryTheory.Functor C E} {G : CategoryTheory.Functor C D} {H : D ≌ E} (i : F ≅ G.comp H.functor) (X : C) : i.compInverseIso.inv.app X = CategoryTheory.CategoryStruct.comp (H.unitIso.hom.app (G.obj X)) (H.inverse.map (i.inv.app X))
• CategoryTheory.Iso.isoCompInverse_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] {F : CategoryTheory.Functor C E} {G : CategoryTheory.Functor C D} {H : D ≌ E} (i : G.comp H.functor ≅ F) (X : C) : i.isoCompInverse.hom.app X = CategoryTheory.CategoryStruct.comp (H.unitIso.hom.app (G.obj X)) (H.inverse.map (i.hom.app X))
• CategoryTheory.Iso.isoInverseOfIsoFunctor_hom_app 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {G G' : C ≌ D} (i : G.functor ≅ G'.functor) (X : D) : i.isoInverseOfIsoFunctor.hom.app X = CategoryTheory.CategoryStruct.comp (G'.unitIso.hom.app (G.inverse.obj X)) (CategoryTheory.CategoryStruct.comp (G'.inverse.map (i.inv.app (G.inverse.obj X))) (G'.inverse.map (G.counitIso.hom.app X)))
• CategoryTheory.Iso.isoInverseOfIsoFunctor_inv_app 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {G G' : C ≌ D} (i : G.functor ≅ G'.functor) (X : D) : i.isoInverseOfIsoFunctor.inv.app X = CategoryTheory.CategoryStruct.comp (G'.inverse.map (G.counitIso.inv.app X)) (CategoryTheory.CategoryStruct.comp (G'.inverse.map (i.hom.app (G.inverse.obj X))) (G'.unitIso.inv.app (G.inverse.obj X)))
• CategoryTheory.Iso.isoFunctorOfIsoInverse_hom_app 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {G G' : C ≌ D} (i : G.inverse ≅ G'.inverse) (X : C) : i.isoFunctorOfIsoInverse.hom.app X = CategoryTheory.CategoryStruct.comp (G'.counitIso.inv.app (G.functor.obj X)) (CategoryTheory.CategoryStruct.comp (G'.functor.map (i.inv.app (G.functor.obj X))) (G'.functor.map (G.unitIso.inv.app X)))
• CategoryTheory.Iso.isoFunctorOfIsoInverse_inv_app 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {G G' : C ≌ D} (i : G.inverse ≅ G'.inverse) (X : C) : i.isoFunctorOfIsoInverse.inv.app X = CategoryTheory.CategoryStruct.comp (G'.functor.map (G.unitIso.hom.app X)) (CategoryTheory.CategoryStruct.comp (G'.functor.map (i.hom.app (G.functor.obj X))) (G'.counitIso.hom.app (G.functor.obj X)))
• CategoryTheory.Equivalence.congrLeft_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 D E) : e.congrLeft.counitIso.hom.app X = (e.invFunIdAssoc X).hom
• CategoryTheory.Equivalence.congrLeft_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 C E) : e.congrLeft.unitIso.hom.app X = (e.funInvIdAssoc X).inv
• CategoryTheory.Equivalence.congrLeft_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 C E) : e.congrLeft.unitIso.inv.app X = (e.funInvIdAssoc X).hom
• 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_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.Iso.op_hom 📋 Mathlib.CategoryTheory.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (α : X ≅ Y) : α.op.hom = α.hom.op
• CategoryTheory.Iso.unop_hom 📋 Mathlib.CategoryTheory.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : Cᵒᵖ} (f : X ≅ Y) : f.unop.hom = f.hom.unop
• CategoryTheory.Functor.opUnopIso_hom_app 📋 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.opUnopIso.hom.app X = CategoryTheory.CategoryStruct.id (F.obj X)
• CategoryTheory.Functor.unopId_hom_app 📋 Mathlib.CategoryTheory.Opposites
  (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (X : C) : (CategoryTheory.Functor.unopId C).hom.app X = CategoryTheory.CategoryStruct.id X
• CategoryTheory.Functor.rightOpLeftOpIso_hom_app 📋 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.rightOpLeftOpIso.hom.app X = CategoryTheory.CategoryStruct.id (F.obj X)
• CategoryTheory.Functor.leftOpRightOpIso_hom_app 📋 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.leftOpRightOpIso.hom.app X = CategoryTheory.CategoryStruct.id (F.obj X)
• CategoryTheory.Functor.opId_hom_app 📋 Mathlib.CategoryTheory.Opposites
  (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (X : Cᵒᵖ) : (CategoryTheory.Functor.opId C).hom.app X = CategoryTheory.CategoryStruct.id X
• CategoryTheory.NatIso.removeOp_hom 📋 Mathlib.CategoryTheory.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F G : CategoryTheory.Functor C D} (α : F.op ≅ G.op) : (CategoryTheory.NatIso.removeOp α).hom = CategoryTheory.NatTrans.removeOp α.hom
• CategoryTheory.NatIso.op_hom 📋 Mathlib.CategoryTheory.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F G : CategoryTheory.Functor C D} (α : F ≅ G) : (CategoryTheory.NatIso.op α).hom = CategoryTheory.NatTrans.op α.hom
• CategoryTheory.NatIso.unop_hom 📋 Mathlib.CategoryTheory.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F G : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ} (α : F ≅ G) : (CategoryTheory.NatIso.unop α).hom = CategoryTheory.NatTrans.unop α.hom
• CategoryTheory.Functor.unopOpIso_hom_app 📋 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.unopOpIso.hom.app X = CategoryTheory.CategoryStruct.id (F.obj X)
• CategoryTheory.Functor.leftOpId_hom_app 📋 Mathlib.CategoryTheory.Opposites
  (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (X : Cᵒᵖᵒᵖ) : (CategoryTheory.Functor.leftOpId C).hom.app X = CategoryTheory.CategoryStruct.id (Opposite.unop (Opposite.unop X))
• CategoryTheory.Functor.rightOpId_hom_app 📋 Mathlib.CategoryTheory.Opposites
  (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (X : C) : (CategoryTheory.Functor.rightOpId C).hom.app X = CategoryTheory.CategoryStruct.id (Opposite.op (Opposite.op X))
• CategoryTheory.Functor.leftOpComp_hom_app 📋 Mathlib.CategoryTheory.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u_1} [CategoryTheory.Category.{v_1, u_1} E] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D Eᵒᵖ) (X : Cᵒᵖ) : (F.leftOpComp G).hom.app X = CategoryTheory.CategoryStruct.id (Opposite.unop (G.obj (F.obj (Opposite.unop X))))
• CategoryTheory.Functor.opComp_hom_app 📋 Mathlib.CategoryTheory.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u_1} [CategoryTheory.Category.{v_1, u_1} E] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) (X : Cᵒᵖ) : (F.opComp G).hom.app X = CategoryTheory.CategoryStruct.id (Opposite.op (G.obj (F.obj (Opposite.unop X))))
• CategoryTheory.Functor.rightOpComp_hom_app 📋 Mathlib.CategoryTheory.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u_1} [CategoryTheory.Category.{v_1, u_1} E] (F : CategoryTheory.Functor Cᵒᵖ D) (G : CategoryTheory.Functor D E) (X : C) : (F.rightOpComp G).hom.app X = CategoryTheory.CategoryStruct.id (Opposite.op (G.obj (F.obj (Opposite.op X))))
• CategoryTheory.Functor.unopComp_hom_app 📋 Mathlib.CategoryTheory.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u_1} [CategoryTheory.Category.{v_1, u_1} E] (F : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ) (G : CategoryTheory.Functor Dᵒᵖ Eᵒᵖ) (X : C) : (F.unopComp G).hom.app X = CategoryTheory.CategoryStruct.id (Opposite.unop (G.obj (F.obj (Opposite.op X))))
• CategoryTheory.Iso.unop_hom_inv_id_app 📋 Mathlib.CategoryTheory.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] {F G : CategoryTheory.Functor C Dᵒᵖ} (e : F ≅ G) (X : C) : CategoryTheory.CategoryStruct.comp (e.hom.app X).unop (e.inv.app X).unop = CategoryTheory.CategoryStruct.id (Opposite.unop (G.obj X))
• CategoryTheory.Iso.unop_inv_hom_id_app 📋 Mathlib.CategoryTheory.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] {F G : CategoryTheory.Functor C Dᵒᵖ} (e : F ≅ G) (X : C) : CategoryTheory.CategoryStruct.comp (e.inv.app X).unop (e.hom.app X).unop = CategoryTheory.CategoryStruct.id (Opposite.unop (F.obj X))
• CategoryTheory.Iso.unop_hom_inv_id_app_assoc 📋 Mathlib.CategoryTheory.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] {F G : CategoryTheory.Functor C Dᵒᵖ} (e : F ≅ G) (X : C) {Z : D} (h : Opposite.unop (G.obj X) ⟶ Z) : CategoryTheory.CategoryStruct.comp (e.hom.app X).unop (CategoryTheory.CategoryStruct.comp (e.inv.app X).unop h) = h
• CategoryTheory.Iso.unop_inv_hom_id_app_assoc 📋 Mathlib.CategoryTheory.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] {F G : CategoryTheory.Functor C Dᵒᵖ} (e : F ≅ G) (X : C) {Z : D} (h : Opposite.unop (F.obj X) ⟶ Z) : CategoryTheory.CategoryStruct.comp (e.inv.app X).unop (CategoryTheory.CategoryStruct.comp (e.hom.app X).unop h) = h
• CategoryTheory.NatTrans.leftOpWhiskerRight 📋 Mathlib.CategoryTheory.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F G : CategoryTheory.Functor C Dᵒᵖ} {E : Type u_1} [CategoryTheory.Category.{v_1, u_1} E] {H : CategoryTheory.Functor E C} (α : F ⟶ G) : CategoryTheory.NatTrans.leftOp (H.whiskerLeft α) = CategoryTheory.CategoryStruct.comp (H.leftOpComp G).hom (CategoryTheory.CategoryStruct.comp (H.op.whiskerLeft (CategoryTheory.NatTrans.leftOp α)) (H.leftOpComp F).inv)
• CategoryTheory.NatTrans.rightOpWhiskerRight 📋 Mathlib.CategoryTheory.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F G : CategoryTheory.Functor Cᵒᵖ D} {E : Type u_1} [CategoryTheory.Category.{v_1, u_1} E] {H : CategoryTheory.Functor D E} (α : F ⟶ G) : CategoryTheory.NatTrans.rightOp (CategoryTheory.Functor.whiskerRight α H) = CategoryTheory.CategoryStruct.comp (G.rightOpComp H).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight (CategoryTheory.NatTrans.rightOp α) H.op) (F.rightOpComp H).inv)
• CategoryTheory.NatTrans.unop_whiskerLeft 📋 Mathlib.CategoryTheory.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F G : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ} {E : Type u_1} [CategoryTheory.Category.{v_1, u_1} E] {H : CategoryTheory.Functor Eᵒᵖ Cᵒᵖ} (α : F ⟶ G) : CategoryTheory.NatTrans.unop (H.whiskerLeft α) = CategoryTheory.CategoryStruct.comp (H.unopComp G).hom (CategoryTheory.CategoryStruct.comp (H.unop.whiskerLeft (CategoryTheory.NatTrans.unop α)) (H.unopComp F).inv)
• CategoryTheory.NatTrans.unop_whiskerRight 📋 Mathlib.CategoryTheory.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F G : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ} {E : Type u_1} [CategoryTheory.Category.{v_1, u_1} E] {H : CategoryTheory.Functor Dᵒᵖ Eᵒᵖ} (α : F ⟶ G) : CategoryTheory.NatTrans.unop (CategoryTheory.Functor.whiskerRight α H) = CategoryTheory.CategoryStruct.comp (G.unopComp H).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight (CategoryTheory.NatTrans.unop α) H.unop) (F.unopComp H).inv)
• CategoryTheory.NatTrans.op_whiskerLeft 📋 Mathlib.CategoryTheory.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F G : CategoryTheory.Functor C D} {E : Type u_1} [CategoryTheory.Category.{v_1, u_1} E] {H : CategoryTheory.Functor E C} (α : F ⟶ G) : CategoryTheory.NatTrans.op (H.whiskerLeft α) = CategoryTheory.CategoryStruct.comp (H.opComp G).hom (CategoryTheory.CategoryStruct.comp (H.op.whiskerLeft (CategoryTheory.NatTrans.op α)) (H.opComp F).inv)
• CategoryTheory.NatTrans.op_whiskerRight 📋 Mathlib.CategoryTheory.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F G : CategoryTheory.Functor C D} {E : Type u_1} [CategoryTheory.Category.{v_1, u_1} E] {H : CategoryTheory.Functor D E} (α : F ⟶ G) : CategoryTheory.NatTrans.op (CategoryTheory.Functor.whiskerRight α H) = CategoryTheory.CategoryStruct.comp (G.opComp H).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight (CategoryTheory.NatTrans.op α) H.op) (F.opComp H).inv)
• CategoryTheory.Equivalence.leftOp_counitIso_hom_app 📋 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.counitIso.hom.app X = (e.counitIso.inv.app (Opposite.op X)).unop
• CategoryTheory.Equivalence.leftOp_counitIso_inv_app 📋 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.counitIso.inv.app X = (e.counitIso.hom.app (Opposite.op X)).unop
• CategoryTheory.Equivalence.leftOp_unitIso_hom_app 📋 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.unitIso.hom.app X = (e.unitIso.inv.app (Opposite.unop X)).op
• CategoryTheory.Equivalence.leftOp_unitIso_inv_app 📋 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.unitIso.inv.app X = (e.unitIso.hom.app (Opposite.unop X)).op
• CategoryTheory.NatTrans.unop_whiskerLeft_assoc 📋 Mathlib.CategoryTheory.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F G : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ} {E : Type u_1} [CategoryTheory.Category.{v_1, u_1} E] {H : CategoryTheory.Functor Eᵒᵖ Cᵒᵖ} (α : F ⟶ G) {Z : CategoryTheory.Functor E D} (h : (H.comp F).unop ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.NatTrans.unop (H.whiskerLeft α)) h = CategoryTheory.CategoryStruct.comp (H.unopComp G).hom (CategoryTheory.CategoryStruct.comp (H.unop.whiskerLeft (CategoryTheory.NatTrans.unop α)) (CategoryTheory.CategoryStruct.comp (H.unopComp F).inv h))
• CategoryTheory.NatTrans.unop_whiskerRight_assoc 📋 Mathlib.CategoryTheory.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F G : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ} {E : Type u_1} [CategoryTheory.Category.{v_1, u_1} E] {H : CategoryTheory.Functor Dᵒᵖ Eᵒᵖ} (α : F ⟶ G) {Z : CategoryTheory.Functor C E} (h : (F.comp H).unop ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.NatTrans.unop (CategoryTheory.Functor.whiskerRight α H)) h = CategoryTheory.CategoryStruct.comp (G.unopComp H).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight (CategoryTheory.NatTrans.unop α) H.unop) (CategoryTheory.CategoryStruct.comp (F.unopComp H).inv h))
• CategoryTheory.NatTrans.leftOpWhiskerRight_assoc 📋 Mathlib.CategoryTheory.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F G : CategoryTheory.Functor C Dᵒᵖ} {E : Type u_1} [CategoryTheory.Category.{v_1, u_1} E] {H : CategoryTheory.Functor E C} (α : F ⟶ G) {Z : CategoryTheory.Functor Eᵒᵖ D} (h : (H.comp F).leftOp ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.NatTrans.leftOp (H.whiskerLeft α)) h = CategoryTheory.CategoryStruct.comp (H.leftOpComp G).hom (CategoryTheory.CategoryStruct.comp (H.op.whiskerLeft (CategoryTheory.NatTrans.leftOp α)) (CategoryTheory.CategoryStruct.comp (H.leftOpComp F).inv h))
• CategoryTheory.NatTrans.rightOpWhiskerRight_assoc 📋 Mathlib.CategoryTheory.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F G : CategoryTheory.Functor Cᵒᵖ D} {E : Type u_1} [CategoryTheory.Category.{v_1, u_1} E] {H : CategoryTheory.Functor D E} (α : F ⟶ G) {Z : CategoryTheory.Functor C Eᵒᵖ} (h : (F.comp H).rightOp ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.NatTrans.rightOp (CategoryTheory.Functor.whiskerRight α H)) h = CategoryTheory.CategoryStruct.comp (G.rightOpComp H).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight (CategoryTheory.NatTrans.rightOp α) H.op) (CategoryTheory.CategoryStruct.comp (F.rightOpComp H).inv h))
• CategoryTheory.Equivalence.rightOp_unitIso_hom_app 📋 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.unitIso.hom.app X = (e.unitIso.inv.app (Opposite.op X)).unop
• CategoryTheory.Equivalence.rightOp_unitIso_inv_app 📋 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.unitIso.inv.app X = (e.unitIso.hom.app (Opposite.op X)).unop
• CategoryTheory.Equivalence.rightOp_counitIso_hom_app 📋 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.counitIso.hom.app X = (e.counitIso.inv.app (Opposite.unop X)).op
• CategoryTheory.Equivalence.rightOp_counitIso_inv_app 📋 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.counitIso.inv.app X = (e.counitIso.hom.app (Opposite.unop X)).op
• CategoryTheory.NatTrans.op_whiskerLeft_assoc 📋 Mathlib.CategoryTheory.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F G : CategoryTheory.Functor C D} {E : Type u_1} [CategoryTheory.Category.{v_1, u_1} E] {H : CategoryTheory.Functor E C} (α : F ⟶ G) {Z : CategoryTheory.Functor Eᵒᵖ Dᵒᵖ} (h : (H.comp F).op ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.NatTrans.op (H.whiskerLeft α)) h = CategoryTheory.CategoryStruct.comp (H.opComp G).hom (CategoryTheory.CategoryStruct.comp (H.op.whiskerLeft (CategoryTheory.NatTrans.op α)) (CategoryTheory.CategoryStruct.comp (H.opComp F).inv h))
• CategoryTheory.NatTrans.op_whiskerRight_assoc 📋 Mathlib.CategoryTheory.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F G : CategoryTheory.Functor C D} {E : Type u_1} [CategoryTheory.Category.{v_1, u_1} E] {H : CategoryTheory.Functor D E} (α : F ⟶ G) {Z : CategoryTheory.Functor Cᵒᵖ Eᵒᵖ} (h : (F.comp H).op ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.NatTrans.op (CategoryTheory.Functor.whiskerRight α H)) h = CategoryTheory.CategoryStruct.comp (G.opComp H).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight (CategoryTheory.NatTrans.op α) H.op) (CategoryTheory.CategoryStruct.comp (F.opComp H).inv h))
• CategoryTheory.Functor.leftOpRightOpEquiv_counitIso_hom_app_app 📋 Mathlib.CategoryTheory.Opposites
  (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (X : CategoryTheory.Functor C Dᵒᵖ) (X✝ : C) : ((CategoryTheory.Functor.leftOpRightOpEquiv C D).counitIso.hom.app X).app X✝ = CategoryTheory.CategoryStruct.id (X.obj X✝)
• CategoryTheory.Functor.leftOpRightOpEquiv_unitIso_hom_app 📋 Mathlib.CategoryTheory.Opposites
  (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (X : (CategoryTheory.Functor Cᵒᵖ D)ᵒᵖ) : (CategoryTheory.Functor.leftOpRightOpEquiv C D).unitIso.hom.app X = (Opposite.unop X).rightOpLeftOpIso.hom.op
• CategoryTheory.eqToIso.hom 📋 Mathlib.CategoryTheory.EqToHom
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (p : X = Y) : (CategoryTheory.eqToIso p).hom = CategoryTheory.eqToHom p
• CategoryTheory.eqToHom_iso_hom_naturality 📋 Mathlib.CategoryTheory.EqToHom
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {β : Sort u_1} {f g : β → C} (z : (b : β) → f b ≅ g b) {j j' : β} (w : j = j') : CategoryTheory.CategoryStruct.comp (z j).hom (CategoryTheory.eqToHom ⋯) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (z j').hom
• CategoryTheory.Functor.ext_of_iso 📋 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} (e : F ≅ G) (hobj : ∀ (X : C), F.obj X = G.obj X) (happ : ∀ (X : C), e.hom.app X = CategoryTheory.eqToHom ⋯ := by cat_disch) : F = G
• CategoryTheory.eqToHom_iso_hom_naturality_assoc 📋 Mathlib.CategoryTheory.EqToHom
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {β : Sort u_1} {f g : β → C} (z : (b : β) → f b ≅ g b) {j j' : β} (w : j = j') {Z : C} (h : g j' ⟶ Z) : CategoryTheory.CategoryStruct.comp (z j).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (z j').hom h)
• CategoryTheory.Functor.congr_inv_of_congr_hom 📋 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) {X Y : C} (e : X ≅ Y) (hX : F.obj X = G.obj X) (hY : F.obj Y = G.obj Y) (h₂ : F.map e.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (G.map e.hom) (CategoryTheory.eqToHom ⋯))) : F.map e.inv = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (G.map e.inv) (CategoryTheory.eqToHom ⋯))
• CategoryTheory.Functor.constComp_hom_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] (X : C) (F : CategoryTheory.Functor C D) (x✝ : J) : (CategoryTheory.Functor.constComp J X F).hom.app x✝ = CategoryTheory.CategoryStruct.id ((((CategoryTheory.Functor.const J).obj X).comp F).obj x✝)
• CategoryTheory.Functor.const.opObjUnop_hom_app 📋 Mathlib.CategoryTheory.Functor.Const
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] (X : Cᵒᵖ) (j : Jᵒᵖ) : (CategoryTheory.Functor.const.opObjUnop X).hom.app j = CategoryTheory.CategoryStruct.id (((CategoryTheory.Functor.const Jᵒᵖ).obj (Opposite.unop X)).obj j)
• CategoryTheory.Functor.const.opObjOp_hom_app 📋 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.opObjOp X).hom.app x✝ = CategoryTheory.CategoryStruct.id (((CategoryTheory.Functor.const Jᵒᵖ).obj (Opposite.op X)).obj x✝)
• CategoryTheory.Functor.constCompWhiskeringLeftIso_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 J D) (X : C) (X✝ : J) : ((CategoryTheory.Functor.constCompWhiskeringLeftIso J F).hom.app X).app X✝ = CategoryTheory.CategoryStruct.id X
• 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)

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 69fae59