Loogle!

Result

Found 16566 declarations mentioning CategoryTheory.CategoryStruct.comp. Of these, only the first 200 are shown.

• CategoryTheory.CategoryStruct.comp 📋 Mathlib.CategoryTheory.Category.Basic
  {obj : Type u} [self : CategoryTheory.CategoryStruct.{v, u} obj] {X Y Z : obj} : (X ⟶ Y) → (Y ⟶ Z) → (X ⟶ Z)
• CategoryTheory.Category.comp_id 📋 Mathlib.CategoryTheory.Category.Basic
  {obj : Type u} [self : CategoryTheory.Category.{v, u} obj] {X Y : obj} (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.id Y) = f
• CategoryTheory.Category.id_comp 📋 Mathlib.CategoryTheory.Category.Basic
  {obj : Type u} [self : CategoryTheory.Category.{v, u} obj] {X Y : obj} (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id X) f = f
• CategoryTheory.epi_of_epi 📋 Mathlib.CategoryTheory.Category.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [CategoryTheory.Epi (CategoryTheory.CategoryStruct.comp f g)] : CategoryTheory.Epi g
• CategoryTheory.mono_of_mono 📋 Mathlib.CategoryTheory.Category.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : C} (g : Z ⟶ Y) (f : Y ⟶ X) [CategoryTheory.Mono (CategoryTheory.CategoryStruct.comp g f)] : CategoryTheory.Mono g
• CategoryTheory.epi_comp 📋 Mathlib.CategoryTheory.Category.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : X ⟶ Y) [CategoryTheory.Epi f] (g : Y ⟶ Z) [CategoryTheory.Epi g] : CategoryTheory.Epi (CategoryTheory.CategoryStruct.comp f g)
• CategoryTheory.epi_comp' 📋 Mathlib.CategoryTheory.Category.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : X ⟶ Y} {g : Y ⟶ Z} (hf : CategoryTheory.Epi f) (hg : CategoryTheory.Epi g) : CategoryTheory.Epi (CategoryTheory.CategoryStruct.comp f g)
• CategoryTheory.mono_comp 📋 Mathlib.CategoryTheory.Category.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : C} (g : Z ⟶ Y) [CategoryTheory.Mono g] (f : Y ⟶ X) [CategoryTheory.Mono f] : CategoryTheory.Mono (CategoryTheory.CategoryStruct.comp g f)
• CategoryTheory.mono_comp' 📋 Mathlib.CategoryTheory.Category.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : Y ⟶ X} {g : Z ⟶ Y} (hg : CategoryTheory.Mono g) (hf : CategoryTheory.Mono f) : CategoryTheory.Mono (CategoryTheory.CategoryStruct.comp g f)
• CategoryTheory.epi_iff_forall_injective 📋 Mathlib.CategoryTheory.Category.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) : CategoryTheory.Epi f ↔ ∀ (Z : C), Function.Injective fun g => CategoryTheory.CategoryStruct.comp f g
• CategoryTheory.mono_iff_forall_injective 📋 Mathlib.CategoryTheory.Category.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : Y ⟶ X) : CategoryTheory.Mono f ↔ ∀ (Z : C), Function.Injective fun g => CategoryTheory.CategoryStruct.comp g f
• CategoryTheory.id_of_comp_left_id 📋 Mathlib.CategoryTheory.Category.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} (f : X ⟶ X) (w : ∀ {Y : C} (g : X ⟶ Y), CategoryTheory.CategoryStruct.comp f g = g) : f = CategoryTheory.CategoryStruct.id X
• CategoryTheory.id_of_comp_right_id 📋 Mathlib.CategoryTheory.Category.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} (f : X ⟶ X) (w : ∀ {Y : C} (g : Y ⟶ X), CategoryTheory.CategoryStruct.comp g f = g) : f = CategoryTheory.CategoryStruct.id X
• CategoryTheory.epi_of_epi_fac 📋 Mathlib.CategoryTheory.Category.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : X ⟶ Y} {g : Y ⟶ Z} {h : X ⟶ Z} [CategoryTheory.Epi h] (w : CategoryTheory.CategoryStruct.comp f g = h) : CategoryTheory.Epi g
• CategoryTheory.mono_of_mono_fac 📋 Mathlib.CategoryTheory.Category.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : Y ⟶ X} {g : Z ⟶ Y} {h : Z ⟶ X} [CategoryTheory.Mono h] (w : CategoryTheory.CategoryStruct.comp g f = h) : CategoryTheory.Mono g
• CategoryTheory.cancel_epi_id 📋 Mathlib.CategoryTheory.Category.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Epi f] {h : Y ⟶ Y} : CategoryTheory.CategoryStruct.comp f h = f ↔ h = CategoryTheory.CategoryStruct.id Y
• CategoryTheory.cancel_mono_id 📋 Mathlib.CategoryTheory.Category.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : Y ⟶ X) [CategoryTheory.Mono f] {h : Y ⟶ Y} : CategoryTheory.CategoryStruct.comp h f = f ↔ h = CategoryTheory.CategoryStruct.id Y
• CategoryTheory.eq_of_comp_left_eq 📋 Mathlib.CategoryTheory.Category.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} (w : ∀ {Z : C} (h : Y ⟶ Z), CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp g h) : f = g
• CategoryTheory.eq_of_comp_right_eq 📋 Mathlib.CategoryTheory.Category.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f g : Y ⟶ X} (w : ∀ {Z : C} (h : Z ⟶ Y), CategoryTheory.CategoryStruct.comp h f = CategoryTheory.CategoryStruct.comp h g) : f = g
• CategoryTheory.eq_whisker 📋 Mathlib.CategoryTheory.Category.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : C} {f g : X ⟶ Y} (w : f = g) (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp g h
• CategoryTheory.whisker_eq 📋 Mathlib.CategoryTheory.Category.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : C} {f g : Y ⟶ X} (h : Z ⟶ Y) (w : f = g) : CategoryTheory.CategoryStruct.comp h f = CategoryTheory.CategoryStruct.comp h g
• CategoryTheory.Epi.left_cancellation 📋 Mathlib.CategoryTheory.Category.Basic
  {C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} {X Y : C} {f : X ⟶ Y} [self : CategoryTheory.Epi f] {Z : C} (g h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp f g = CategoryTheory.CategoryStruct.comp f h → g = h
• CategoryTheory.Epi.mk 📋 Mathlib.CategoryTheory.Category.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} (left_cancellation : ∀ {Z : C} (g h : Y ⟶ Z), CategoryTheory.CategoryStruct.comp f g = CategoryTheory.CategoryStruct.comp f h → g = h) : CategoryTheory.Epi f
• CategoryTheory.Mono.mk 📋 Mathlib.CategoryTheory.Category.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} (right_cancellation : ∀ {Z : C} (g h : Z ⟶ X), CategoryTheory.CategoryStruct.comp g f = CategoryTheory.CategoryStruct.comp h f → g = h) : CategoryTheory.Mono f
• CategoryTheory.Mono.right_cancellation 📋 Mathlib.CategoryTheory.Category.Basic
  {C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} {X Y : C} {f : X ⟶ Y} [self : CategoryTheory.Mono f] {Z : C} (g h : Z ⟶ X) : CategoryTheory.CategoryStruct.comp g f = CategoryTheory.CategoryStruct.comp h f → g = h
• CategoryTheory.cancel_epi 📋 Mathlib.CategoryTheory.Category.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : X ⟶ Y) [CategoryTheory.Epi f] {g h : Y ⟶ Z} : CategoryTheory.CategoryStruct.comp f g = CategoryTheory.CategoryStruct.comp f h ↔ g = h
• CategoryTheory.cancel_mono 📋 Mathlib.CategoryTheory.Category.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : Y ⟶ X) [CategoryTheory.Mono f] {g h : Z ⟶ Y} : CategoryTheory.CategoryStruct.comp g f = CategoryTheory.CategoryStruct.comp h f ↔ g = h
• CategoryTheory.Category.assoc 📋 Mathlib.CategoryTheory.Category.Basic
  {obj : Type u} [self : CategoryTheory.Category.{v, u} obj] {W X Y Z : obj} (f : W ⟶ X) (g : X ⟶ Y) (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g) h = CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g h)
• CategoryTheory.Category.assoc' 📋 Mathlib.CategoryTheory.Category.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {W X Y Z : C} (f : X ⟶ W) (g : Y ⟶ X) (h : Z ⟶ Y) : CategoryTheory.CategoryStruct.comp h (CategoryTheory.CategoryStruct.comp g f) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp h g) f
• CategoryTheory.eq_of_comp_left_eq' 📋 Mathlib.CategoryTheory.Category.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f g : X ⟶ Y) (w : (fun {Z} h => CategoryTheory.CategoryStruct.comp f h) = fun {Z} h => CategoryTheory.CategoryStruct.comp g h) : f = g
• CategoryTheory.eq_of_comp_right_eq' 📋 Mathlib.CategoryTheory.Category.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f g : Y ⟶ X) (w : (fun {Z} h => CategoryTheory.CategoryStruct.comp h f) = fun {Z} h => CategoryTheory.CategoryStruct.comp h g) : f = g
• CategoryTheory.comp_ite 📋 Mathlib.CategoryTheory.Category.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {P : Prop} [Decidable P] {X Y Z : C} (f : X ⟶ Y) (g g' : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp f (if P then g else g') = if P then CategoryTheory.CategoryStruct.comp f g else CategoryTheory.CategoryStruct.comp f g'
• CategoryTheory.ite_comp 📋 Mathlib.CategoryTheory.Category.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {P : Prop} [Decidable P] {X Y Z : C} (g g' : Z ⟶ Y) (f : Y ⟶ X) : CategoryTheory.CategoryStruct.comp (if P then g else g') f = if P then CategoryTheory.CategoryStruct.comp g f else CategoryTheory.CategoryStruct.comp g' f
• CategoryTheory.comp_dite 📋 Mathlib.CategoryTheory.Category.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {P : Prop} [Decidable P] {X Y Z : C} (f : X ⟶ Y) (g : P → (Y ⟶ Z)) (g' : ¬P → (Y ⟶ Z)) : CategoryTheory.CategoryStruct.comp f (if h : P then g h else g' h) = if h : P then CategoryTheory.CategoryStruct.comp f (g h) else CategoryTheory.CategoryStruct.comp f (g' h)
• CategoryTheory.dite_comp 📋 Mathlib.CategoryTheory.Category.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {P : Prop} [Decidable P] {X Y Z : C} (g : P → (Z ⟶ Y)) (g' : ¬P → (Z ⟶ Y)) (f : Y ⟶ X) : CategoryTheory.CategoryStruct.comp (if h : P then g h else g' h) f = if h : P then CategoryTheory.CategoryStruct.comp (g h) f else CategoryTheory.CategoryStruct.comp (g' h) f
• CategoryTheory.Category.mk' 📋 Mathlib.CategoryTheory.Category.Basic
  {obj : Type u} [CategoryTheory.CategoryStruct.{v, u} obj] (id_comp : ∀ {X Y : obj} (f : Y ⟶ X), CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.id X) = f) (comp_id : ∀ {X Y : obj} (f : Y ⟶ X), CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id Y) f = f) (assoc : ∀ {W X Y Z : obj} (f : X ⟶ W) (g : Y ⟶ X) (h : Z ⟶ Y), CategoryTheory.CategoryStruct.comp h (CategoryTheory.CategoryStruct.comp g f) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp h g) f) : CategoryTheory.Category.{v, u} obj
• CategoryTheory.Category.mk 📋 Mathlib.CategoryTheory.Category.Basic
  {obj : Type u} [toCategoryStruct : CategoryTheory.CategoryStruct.{v, u} obj] (id_comp : ∀ {X Y : obj} (f : X ⟶ Y), CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id X) f = f := by cat_disch) (comp_id : ∀ {X Y : obj} (f : X ⟶ Y), CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.id Y) = f := by cat_disch) (assoc : ∀ {W X Y Z : obj} (f : W ⟶ X) (g : X ⟶ Y) (h : Y ⟶ Z), CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g) h = CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g h) := by cat_disch) : CategoryTheory.Category.{v, u} obj
• CategoryTheory.cancel_epi_assoc_iff 📋 Mathlib.CategoryTheory.Category.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : X ⟶ Y) [CategoryTheory.Epi f] {g h : Y ⟶ Z} {W : C} {k l : Z ⟶ W} : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g) k = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f h) l ↔ CategoryTheory.CategoryStruct.comp g k = CategoryTheory.CategoryStruct.comp h l
• CategoryTheory.cancel_mono_assoc_iff 📋 Mathlib.CategoryTheory.Category.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : Y ⟶ X) [CategoryTheory.Mono f] {g h : Z ⟶ Y} {W : C} {k l : W ⟶ Z} : CategoryTheory.CategoryStruct.comp k (CategoryTheory.CategoryStruct.comp g f) = CategoryTheory.CategoryStruct.comp l (CategoryTheory.CategoryStruct.comp h f) ↔ CategoryTheory.CategoryStruct.comp k g = CategoryTheory.CategoryStruct.comp l h
• CategoryTheory.Functor.map_comp 📋 Mathlib.CategoryTheory.Functor.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (self : CategoryTheory.Functor C D) {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) : self.map (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (self.map f) (self.map g)
• CategoryTheory.Functor.mk 📋 Mathlib.CategoryTheory.Functor.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (obj : C → D) (map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)) (map_id : ∀ (X : C), map (CategoryTheory.CategoryStruct.id X) = CategoryTheory.CategoryStruct.id (obj X) := by cat_disch) (map_comp : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), map (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (map f) (map g) := by cat_disch) : CategoryTheory.Functor C D
• CategoryTheory.Functor.map_comp_assoc 📋 Mathlib.CategoryTheory.Functor.Basic
  {C : Type u₁} [CategoryTheory.Category.{v_1, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v_2, u₂} D] (F : CategoryTheory.Functor C D) {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) {W : D} (h : F.obj Z ⟶ W) : CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.CategoryStruct.comp f g)) h = CategoryTheory.CategoryStruct.comp (F.map f) (CategoryTheory.CategoryStruct.comp (F.map g) h)
• Mathlib.Tactic.Reassoc.eq_whisker' 📋 Mathlib.Tactic.CategoryTheory.Reassoc
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {X Y : C} {f g : X ⟶ Y} (w : f = g) {Z : C} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp g h
• CategoryTheory.NatTrans.vcomp_app 📋 Mathlib.CategoryTheory.NatTrans
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F G H : CategoryTheory.Functor C D} (α : CategoryTheory.NatTrans F G) (β : CategoryTheory.NatTrans G H) (X : C) : (α.vcomp β).app X = CategoryTheory.CategoryStruct.comp (α.app X) (β.app X)
• CategoryTheory.NatTrans.naturality 📋 Mathlib.CategoryTheory.NatTrans
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F G : CategoryTheory.Functor C D} (self : CategoryTheory.NatTrans F G) ⦃X Y : C⦄ (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp (F.map f) (self.app Y) = CategoryTheory.CategoryStruct.comp (self.app X) (G.map f)
• CategoryTheory.NatTrans.naturality' 📋 Mathlib.CategoryTheory.NatTrans
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F G : CategoryTheory.Functor C D} (self : CategoryTheory.NatTrans G F) ⦃X Y : C⦄ (f : Y ⟶ X) : CategoryTheory.CategoryStruct.comp (self.app Y) (F.map f) = CategoryTheory.CategoryStruct.comp (G.map f) (self.app X)
• CategoryTheory.NatTrans.mk' 📋 Mathlib.CategoryTheory.NatTrans
  {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) → G.obj X ⟶ F.obj X) (naturality : ∀ ⦃X Y : C⦄ (f : Y ⟶ X), CategoryTheory.CategoryStruct.comp (app Y) (F.map f) = CategoryTheory.CategoryStruct.comp (G.map f) (app X)) : CategoryTheory.NatTrans G F
• CategoryTheory.NatTrans.mk 📋 Mathlib.CategoryTheory.NatTrans
  {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) = CategoryTheory.CategoryStruct.comp (app X) (G.map f) := by cat_disch) : CategoryTheory.NatTrans F G
• CategoryTheory.NatTrans.naturality_assoc 📋 Mathlib.CategoryTheory.NatTrans
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F G : CategoryTheory.Functor C D} (self : CategoryTheory.NatTrans F G) ⦃X Y : C⦄ (f : X ⟶ Y) {Z : D} (h : G.obj Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (F.map f) (CategoryTheory.CategoryStruct.comp (self.app Y) h) = CategoryTheory.CategoryStruct.comp (self.app X) (CategoryTheory.CategoryStruct.comp (G.map f) h)
• 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.IsIso.comp_isIso 📋 Mathlib.CategoryTheory.Iso
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : X ⟶ Y} {h : Y ⟶ Z} [CategoryTheory.IsIso f] [CategoryTheory.IsIso h] : CategoryTheory.IsIso (CategoryTheory.CategoryStruct.comp f h)
• CategoryTheory.IsIso.comp_isIso' 📋 Mathlib.CategoryTheory.Iso
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : X ⟶ Y} {h : Y ⟶ Z} : CategoryTheory.IsIso f → CategoryTheory.IsIso h → CategoryTheory.IsIso (CategoryTheory.CategoryStruct.comp f h)
• CategoryTheory.IsIso.of_isIso_comp_left 📋 Mathlib.CategoryTheory.Iso
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [CategoryTheory.IsIso f] [CategoryTheory.IsIso (CategoryTheory.CategoryStruct.comp f g)] : CategoryTheory.IsIso g
• CategoryTheory.IsIso.of_isIso_comp_right 📋 Mathlib.CategoryTheory.Iso
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : C} (g : Z ⟶ Y) (f : Y ⟶ X) [CategoryTheory.IsIso f] [CategoryTheory.IsIso (CategoryTheory.CategoryStruct.comp g f)] : CategoryTheory.IsIso g
• CategoryTheory.isIso_comp_left_iff 📋 Mathlib.CategoryTheory.Iso
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [CategoryTheory.IsIso f] : CategoryTheory.IsIso (CategoryTheory.CategoryStruct.comp f g) ↔ CategoryTheory.IsIso g
• CategoryTheory.isIso_comp_right_iff 📋 Mathlib.CategoryTheory.Iso
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : C} (g : Z ⟶ Y) (f : Y ⟶ X) [CategoryTheory.IsIso f] : CategoryTheory.IsIso (CategoryTheory.CategoryStruct.comp g f) ↔ CategoryTheory.IsIso g
• CategoryTheory.IsIso.hom_inv_id 📋 Mathlib.CategoryTheory.Iso
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [I : CategoryTheory.IsIso f] : CategoryTheory.CategoryStruct.comp f (CategoryTheory.inv f) = CategoryTheory.CategoryStruct.id X
• CategoryTheory.IsIso.inv_hom_id 📋 Mathlib.CategoryTheory.Iso
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [I : CategoryTheory.IsIso f] : CategoryTheory.CategoryStruct.comp (CategoryTheory.inv f) f = CategoryTheory.CategoryStruct.id Y
• 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.trans_inv 📋 Mathlib.CategoryTheory.Iso
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : C} (α : X ≅ Y) (β : Y ≅ Z) : (α ≪≫ β).inv = CategoryTheory.CategoryStruct.comp β.inv α.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_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.isIso_of_comp_hom_eq_id 📋 Mathlib.CategoryTheory.Iso
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (g : Y ⟶ X) [CategoryTheory.IsIso g] {f : X ⟶ Y} (h : CategoryTheory.CategoryStruct.comp f g = CategoryTheory.CategoryStruct.id X) : CategoryTheory.IsIso f
• CategoryTheory.isIso_of_hom_comp_eq_id 📋 Mathlib.CategoryTheory.Iso
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (g : X ⟶ Y) [CategoryTheory.IsIso g] {f : Y ⟶ X} (h : CategoryTheory.CategoryStruct.comp g f = CategoryTheory.CategoryStruct.id X) : CategoryTheory.IsIso f
• CategoryTheory.IsIso.hom_inv_id_assoc 📋 Mathlib.CategoryTheory.Iso
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [I : CategoryTheory.IsIso f] {Z : C} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (CategoryTheory.inv f) h) = h
• CategoryTheory.IsIso.inv_hom_id_assoc 📋 Mathlib.CategoryTheory.Iso
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [I : CategoryTheory.IsIso f] {Z : C} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.inv f) (CategoryTheory.CategoryStruct.comp f 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.IsIso.of_isIso_fac_left 📋 Mathlib.CategoryTheory.Iso
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : X ⟶ Y} {g : Y ⟶ Z} {h : X ⟶ Z} [CategoryTheory.IsIso f] [hh : CategoryTheory.IsIso h] (w : CategoryTheory.CategoryStruct.comp f g = h) : CategoryTheory.IsIso g
• CategoryTheory.IsIso.of_isIso_fac_right 📋 Mathlib.CategoryTheory.Iso
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : Y ⟶ X} {g : Z ⟶ Y} {h : Z ⟶ X} [CategoryTheory.IsIso f] [hh : CategoryTheory.IsIso h] (w : CategoryTheory.CategoryStruct.comp g f = h) : CategoryTheory.IsIso g
• CategoryTheory.IsIso.eq_inv_of_hom_inv_id 📋 Mathlib.CategoryTheory.Iso
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} [CategoryTheory.IsIso f] {g : Y ⟶ X} (hom_inv_id : CategoryTheory.CategoryStruct.comp f g = CategoryTheory.CategoryStruct.id X) : g = CategoryTheory.inv f
• CategoryTheory.IsIso.eq_inv_of_inv_hom_id 📋 Mathlib.CategoryTheory.Iso
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : Y ⟶ X} [CategoryTheory.IsIso f] {g : X ⟶ Y} (hom_inv_id : CategoryTheory.CategoryStruct.comp g f = CategoryTheory.CategoryStruct.id X) : g = CategoryTheory.inv f
• CategoryTheory.IsIso.inv_eq_of_hom_inv_id 📋 Mathlib.CategoryTheory.Iso
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} [CategoryTheory.IsIso f] {g : Y ⟶ X} (hom_inv_id : CategoryTheory.CategoryStruct.comp f g = CategoryTheory.CategoryStruct.id X) : CategoryTheory.inv f = g
• CategoryTheory.IsIso.inv_eq_of_inv_hom_id 📋 Mathlib.CategoryTheory.Iso
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : Y ⟶ X} [CategoryTheory.IsIso f] {g : X ⟶ Y} (hom_inv_id : CategoryTheory.CategoryStruct.comp g f = CategoryTheory.CategoryStruct.id X) : CategoryTheory.inv f = g
• CategoryTheory.comp_hom_eq_id 📋 Mathlib.CategoryTheory.Iso
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (g : Y ⟶ X) [CategoryTheory.IsIso g] {f : X ⟶ Y} : CategoryTheory.CategoryStruct.comp f g = CategoryTheory.CategoryStruct.id X ↔ f = CategoryTheory.inv g
• CategoryTheory.comp_inv_eq_id 📋 Mathlib.CategoryTheory.Iso
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (g : Y ⟶ X) [CategoryTheory.IsIso g] {f : Y ⟶ X} : CategoryTheory.CategoryStruct.comp f (CategoryTheory.inv g) = CategoryTheory.CategoryStruct.id Y ↔ f = g
• CategoryTheory.hom_comp_eq_id 📋 Mathlib.CategoryTheory.Iso
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (g : X ⟶ Y) [CategoryTheory.IsIso g] {f : Y ⟶ X} : CategoryTheory.CategoryStruct.comp g f = CategoryTheory.CategoryStruct.id X ↔ f = CategoryTheory.inv g
• CategoryTheory.inv_comp_eq_id 📋 Mathlib.CategoryTheory.Iso
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (g : X ⟶ Y) [CategoryTheory.IsIso g] {f : X ⟶ Y} : CategoryTheory.CategoryStruct.comp (CategoryTheory.inv g) f = CategoryTheory.CategoryStruct.id Y ↔ f = g
• 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.cancel_iso_inv_left 📋 Mathlib.CategoryTheory.Iso
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : C} (g : Y ≅ Z) (f f' : Y ⟶ X) : CategoryTheory.CategoryStruct.comp g.inv f = CategoryTheory.CategoryStruct.comp g.inv f' ↔ f = f'
• CategoryTheory.Iso.cancel_iso_inv_right 📋 Mathlib.CategoryTheory.Iso
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : C} (g g' : Z ⟶ Y) (f : X ≅ Y) : CategoryTheory.CategoryStruct.comp g f.inv = CategoryTheory.CategoryStruct.comp g' f.inv ↔ g = g'
• 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.Iso.mk 📋 Mathlib.CategoryTheory.Iso
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (hom : X ⟶ Y) (inv : Y ⟶ X) (hom_inv_id : CategoryTheory.CategoryStruct.comp hom inv = CategoryTheory.CategoryStruct.id X := by cat_disch) (inv_hom_id : CategoryTheory.CategoryStruct.comp inv hom = CategoryTheory.CategoryStruct.id Y := by cat_disch) : X ≅ Y
• CategoryTheory.IsIso.comp_inv_eq 📋 Mathlib.CategoryTheory.Iso
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : C} (α : Y ⟶ X) [CategoryTheory.IsIso α] {f : Z ⟶ X} {g : Z ⟶ Y} : CategoryTheory.CategoryStruct.comp f (CategoryTheory.inv α) = g ↔ f = CategoryTheory.CategoryStruct.comp g α
• CategoryTheory.IsIso.eq_comp_inv 📋 Mathlib.CategoryTheory.Iso
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : C} (α : Y ⟶ X) [CategoryTheory.IsIso α] {f : Z ⟶ X} {g : Z ⟶ Y} : g = CategoryTheory.CategoryStruct.comp f (CategoryTheory.inv α) ↔ CategoryTheory.CategoryStruct.comp g α = f
• CategoryTheory.IsIso.eq_inv_comp 📋 Mathlib.CategoryTheory.Iso
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : C} (α : X ⟶ Y) [CategoryTheory.IsIso α] {f : X ⟶ Z} {g : Y ⟶ Z} : g = CategoryTheory.CategoryStruct.comp (CategoryTheory.inv α) f ↔ CategoryTheory.CategoryStruct.comp α g = f
• CategoryTheory.IsIso.inv_comp_eq 📋 Mathlib.CategoryTheory.Iso
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : C} (α : X ⟶ Y) [CategoryTheory.IsIso α] {f : X ⟶ Z} {g : Y ⟶ Z} : CategoryTheory.CategoryStruct.comp (CategoryTheory.inv α) f = g ↔ f = CategoryTheory.CategoryStruct.comp α g
• CategoryTheory.IsIso.mk 📋 Mathlib.CategoryTheory.Iso
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} (out : ∃ inv, CategoryTheory.CategoryStruct.comp f inv = CategoryTheory.CategoryStruct.id X ∧ CategoryTheory.CategoryStruct.comp inv f = CategoryTheory.CategoryStruct.id Y) : CategoryTheory.IsIso f
• CategoryTheory.IsIso.mk' 📋 Mathlib.CategoryTheory.Iso
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : Y ⟶ X} (out : ∃ inv, CategoryTheory.CategoryStruct.comp inv f = CategoryTheory.CategoryStruct.id X ∧ CategoryTheory.CategoryStruct.comp f inv = CategoryTheory.CategoryStruct.id Y) : CategoryTheory.IsIso f
• CategoryTheory.IsIso.out 📋 Mathlib.CategoryTheory.Iso
  {C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} {X Y : C} {f : X ⟶ Y} [self : CategoryTheory.IsIso f] : ∃ inv, CategoryTheory.CategoryStruct.comp f inv = CategoryTheory.CategoryStruct.id X ∧ CategoryTheory.CategoryStruct.comp inv f = CategoryTheory.CategoryStruct.id Y
• CategoryTheory.IsIso.inv_comp 📋 Mathlib.CategoryTheory.Iso
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : X ⟶ Y} {h : Y ⟶ Z} [CategoryTheory.IsIso f] [CategoryTheory.IsIso h] : CategoryTheory.inv (CategoryTheory.CategoryStruct.comp f h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.inv h) (CategoryTheory.inv f)
• CategoryTheory.Iso.symm_mk 📋 Mathlib.CategoryTheory.Iso
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (hom : X ⟶ Y) (inv : Y ⟶ X) (hom_inv_id : CategoryTheory.CategoryStruct.comp hom inv = CategoryTheory.CategoryStruct.id X) (inv_hom_id : CategoryTheory.CategoryStruct.comp inv hom = CategoryTheory.CategoryStruct.id Y) : { hom := hom, inv := inv, hom_inv_id := hom_inv_id, inv_hom_id := inv_hom_id }.symm = { hom := inv, inv := hom, hom_inv_id := inv_hom_id, inv_hom_id := hom_inv_id }
• 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 📋 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.IsIso f] : CategoryTheory.CategoryStruct.comp (F.map f) (F.map (CategoryTheory.inv f)) = 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 : Y ⟶ X) [CategoryTheory.IsIso f] : CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.inv f)) (F.map f) = CategoryTheory.CategoryStruct.id (F.obj X)
• 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.IsIso.inv_comp_assoc 📋 Mathlib.CategoryTheory.Iso
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : X ⟶ Y} {h : Y ⟶ Z} [CategoryTheory.IsIso f] [CategoryTheory.IsIso h] {Z✝ : C} (h✝ : X ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (CategoryTheory.CategoryStruct.comp f h)) h✝ = CategoryTheory.CategoryStruct.comp (CategoryTheory.inv h) (CategoryTheory.CategoryStruct.comp (CategoryTheory.inv f) h✝)
• 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) [CategoryTheory.IsIso f] {Z : D} (h : F.obj X ⟶ Z) : CategoryTheory.CategoryStruct.comp (F.map f) (CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.inv f)) 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 : Y ⟶ X) [CategoryTheory.IsIso f] {Z : D} (h : F.obj X ⟶ Z) : CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.inv f)) (CategoryTheory.CategoryStruct.comp (F.map f) 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.cancel_iso_inv_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 : Z ≅ Y) : CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g h.inv) = CategoryTheory.CategoryStruct.comp f' (CategoryTheory.CategoryStruct.comp g' h.inv) ↔ CategoryTheory.CategoryStruct.comp f g = CategoryTheory.CategoryStruct.comp f' g'
• CategoryTheory.Iso.homFromEquiv_apply 📋 Mathlib.CategoryTheory.Iso
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (α : X ≅ Y) {Z : C} (f : X ⟶ Z) : α.homFromEquiv f = CategoryTheory.CategoryStruct.comp α.inv f
• 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.Iso.homToEquiv_symm_apply 📋 Mathlib.CategoryTheory.Iso
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (α : X ≅ Y) {Z : C} (g : Z ⟶ Y) : α.homToEquiv.symm g = CategoryTheory.CategoryStruct.comp g α.inv
• CategoryTheory.Iso.trans_mk 📋 Mathlib.CategoryTheory.Iso
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : C} (hom : X ⟶ Y) (inv : Y ⟶ X) (hom_inv_id : CategoryTheory.CategoryStruct.comp hom inv = CategoryTheory.CategoryStruct.id X) (inv_hom_id : CategoryTheory.CategoryStruct.comp inv hom = CategoryTheory.CategoryStruct.id Y) (hom' : Y ⟶ Z) (inv' : Z ⟶ Y) (hom_inv_id' : CategoryTheory.CategoryStruct.comp hom' inv' = CategoryTheory.CategoryStruct.id Y) (inv_hom_id' : CategoryTheory.CategoryStruct.comp inv' hom' = CategoryTheory.CategoryStruct.id Z) (hom_inv_id'' : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp hom hom') (CategoryTheory.CategoryStruct.comp inv' inv) = CategoryTheory.CategoryStruct.id X) (inv_hom_id'' : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp inv' inv) (CategoryTheory.CategoryStruct.comp hom hom') = CategoryTheory.CategoryStruct.id Z) : { hom := hom, inv := inv, hom_inv_id := hom_inv_id, inv_hom_id := inv_hom_id } ≪≫ { hom := hom', inv := inv', hom_inv_id := hom_inv_id', inv_hom_id := inv_hom_id' } = { hom := CategoryTheory.CategoryStruct.comp hom hom', inv := CategoryTheory.CategoryStruct.comp inv' inv, hom_inv_id := hom_inv_id'', inv_hom_id := inv_hom_id'' }
• CategoryTheory.NatTrans.vcomp_eq_comp 📋 Mathlib.CategoryTheory.Functor.Category
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F G H : CategoryTheory.Functor C D} (α : F ⟶ G) (β : G ⟶ H) : CategoryTheory.NatTrans.vcomp α β = CategoryTheory.CategoryStruct.comp α β
• CategoryTheory.NatTrans.id_comm 📋 Mathlib.CategoryTheory.Functor.Category
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (α β : CategoryTheory.Functor.id C ⟶ CategoryTheory.Functor.id C) : CategoryTheory.CategoryStruct.comp α β = CategoryTheory.CategoryStruct.comp β α
• CategoryTheory.NatTrans.comp_app 📋 Mathlib.CategoryTheory.Functor.Category
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F G H : CategoryTheory.Functor C D} (α : F ⟶ G) (β : G ⟶ H) (X : C) : (CategoryTheory.CategoryStruct.comp α β).app X = CategoryTheory.CategoryStruct.comp (α.app X) (β.app X)
• CategoryTheory.NatTrans.vcomp_app' 📋 Mathlib.CategoryTheory.Functor.Category
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F G H : CategoryTheory.Functor C D} (α : F ⟶ G) (β : G ⟶ H) (X : C) : (CategoryTheory.CategoryStruct.comp α β).app X = CategoryTheory.CategoryStruct.comp (α.app X) (β.app X)
• CategoryTheory.NatTrans.comp_app_assoc 📋 Mathlib.CategoryTheory.Functor.Category
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F G H : CategoryTheory.Functor C D} (α : F ⟶ G) (β : G ⟶ H) (X : C) {Z : D} (h : H.obj X ⟶ Z) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.CategoryStruct.comp α β).app X) h = CategoryTheory.CategoryStruct.comp (α.app X) (CategoryTheory.CategoryStruct.comp (β.app X) h)
• CategoryTheory.NatTrans.hcomp_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] {F G : CategoryTheory.Functor C D} {H I : CategoryTheory.Functor D E} (α : F ⟶ G) (β : H ⟶ I) (X : C) : (α ◫ β).app X = CategoryTheory.CategoryStruct.comp (β.app (F.obj X)) (I.map (α.app X))
• CategoryTheory.NatTrans.hcomp_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] {F G : CategoryTheory.Functor C D} {H I : CategoryTheory.Functor D E} (α : F ⟶ G) (β : H ⟶ I) (X : C) : (α ◫ β).app X = CategoryTheory.CategoryStruct.comp (H.map (α.app X)) (β.app (G.obj X))
• CategoryTheory.NatTrans.naturality_inv 📋 Mathlib.CategoryTheory.Functor.Category
  {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} (f : X ⟶ Y) [CategoryTheory.IsIso (α.app X)] [CategoryTheory.IsIso (α.app Y)] : CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (α.app X)) (F.map f) = CategoryTheory.CategoryStruct.comp (G.map f) (CategoryTheory.inv (α.app Y))
• 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.NatTrans.naturality_inv_assoc 📋 Mathlib.CategoryTheory.Functor.Category
  {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} (f : X ⟶ Y) [CategoryTheory.IsIso (α.app X)] [CategoryTheory.IsIso (α.app Y)] {Z : D} (h : F.obj Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (α.app X)) (CategoryTheory.CategoryStruct.comp (F.map f) h) = CategoryTheory.CategoryStruct.comp (G.map f) (CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (α.app Y)) h)
• 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.NatTrans.exchange 📋 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 G H : CategoryTheory.Functor C D} {I J K : CategoryTheory.Functor D E} (α : F ⟶ G) (β : G ⟶ H) (γ : I ⟶ J) (δ : J ⟶ K) : CategoryTheory.CategoryStruct.comp α β ◫ CategoryTheory.CategoryStruct.comp γ δ = CategoryTheory.CategoryStruct.comp (α ◫ γ) (β ◫ δ)
• CategoryTheory.NatTrans.app_naturality 📋 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 G : CategoryTheory.Functor C (CategoryTheory.Functor D E)} (T : F ⟶ G) (X : C) {Y Z : D} (f : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp ((F.obj X).map f) ((T.app X).app Z) = CategoryTheory.CategoryStruct.comp ((T.app X).app Y) ((G.obj X).map f)
• CategoryTheory.NatTrans.naturality_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] {F G : CategoryTheory.Functor C (CategoryTheory.Functor D E)} (T : F ⟶ G) (Z : D) {X Y : C} (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp ((F.map f).app Z) ((T.app Y).app Z) = CategoryTheory.CategoryStruct.comp ((T.app X).app Z) ((G.map f).app Z)
• CategoryTheory.NatTrans.app_naturality_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] {F G : CategoryTheory.Functor C (CategoryTheory.Functor D E)} (T : F ⟶ G) (X : C) {Y Z : D} (f : Y ⟶ Z) {Z✝ : E} (h : (G.obj X).obj Z ⟶ Z✝) : CategoryTheory.CategoryStruct.comp ((F.obj X).map f) (CategoryTheory.CategoryStruct.comp ((T.app X).app Z) h) = CategoryTheory.CategoryStruct.comp ((T.app X).app Y) (CategoryTheory.CategoryStruct.comp ((G.obj X).map f) h)
• CategoryTheory.NatTrans.naturality_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] {F G : CategoryTheory.Functor C (CategoryTheory.Functor D E)} (T : F ⟶ G) (Z : D) {X Y : C} (f : X ⟶ Y) {Z✝ : E} (h : (G.obj Y).obj Z ⟶ Z✝) : CategoryTheory.CategoryStruct.comp ((F.map f).app Z) (CategoryTheory.CategoryStruct.comp ((T.app Y).app Z) h) = CategoryTheory.CategoryStruct.comp ((T.app X).app Z) (CategoryTheory.CategoryStruct.comp ((G.map f).app Z) h)
• CategoryTheory.NatTrans.naturality_app_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 G : CategoryTheory.Functor C (CategoryTheory.Functor D (CategoryTheory.Functor E E'))} (α : F ⟶ G) {X₁ Y₁ : C} (f : X₁ ⟶ Y₁) (X₂ : D) (X₃ : E) : CategoryTheory.CategoryStruct.comp (((F.map f).app X₂).app X₃) (((α.app Y₁).app X₂).app X₃) = CategoryTheory.CategoryStruct.comp (((α.app X₁).app X₂).app X₃) (((G.map f).app X₂).app X₃)
• CategoryTheory.NatTrans.naturality_app_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] {E' : Type u₄} [CategoryTheory.Category.{v₄, u₄} E'] {F G : CategoryTheory.Functor C (CategoryTheory.Functor D (CategoryTheory.Functor E E'))} (α : F ⟶ G) {X₁ Y₁ : C} (f : X₁ ⟶ Y₁) (X₂ : D) (X₃ : E) {Z : E'} (h : ((G.obj Y₁).obj X₂).obj X₃ ⟶ Z) : CategoryTheory.CategoryStruct.comp (((F.map f).app X₂).app X₃) (CategoryTheory.CategoryStruct.comp (((α.app Y₁).app X₂).app X₃) h) = CategoryTheory.CategoryStruct.comp (((α.app X₁).app X₂).app X₃) (CategoryTheory.CategoryStruct.comp (((G.map f).app X₂).app X₃) h)
• 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.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.cancel_natIso_inv_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' : F.obj X ⟶ Y) : CategoryTheory.CategoryStruct.comp (α.inv.app X) g = CategoryTheory.CategoryStruct.comp (α.inv.app X) g' ↔ g = g'
• CategoryTheory.NatIso.cancel_natIso_inv_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 ⟶ G.obj X) : CategoryTheory.CategoryStruct.comp g (α.inv.app X) = CategoryTheory.CategoryStruct.comp g' (α.inv.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.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 : Y ⟶ X), CategoryTheory.CategoryStruct.comp (app Y).inv (F.map f) = CategoryTheory.CategoryStruct.comp (G.map f) (app X).inv := by cat_disch) : F ≅ G
• 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) {x✝ : CategoryTheory.IsIso (α.app X)} : CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (α.app X)) (CategoryTheory.CategoryStruct.comp (F.map f) (α.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) {x✝ : CategoryTheory.IsIso (α.app Y)} : CategoryTheory.CategoryStruct.comp (α.app X) (CategoryTheory.CategoryStruct.comp (G.map f) (CategoryTheory.inv (α.app Y))) = F.map f
• 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.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 : Y ⟶ X), CategoryTheory.CategoryStruct.comp (app' Y).inv (F.map f) = CategoryTheory.CategoryStruct.comp (G.map f) (app' X).inv) (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.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) {x✝ : CategoryTheory.IsIso (α.app X)} {Z : D} (h : G.obj Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (α.app X)) (CategoryTheory.CategoryStruct.comp (F.map f) (CategoryTheory.CategoryStruct.comp (α.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) {x✝ : CategoryTheory.IsIso (α.app Y)} {Z : D} (h : F.obj Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (α.app X) (CategoryTheory.CategoryStruct.comp (G.map f) (CategoryTheory.CategoryStruct.comp (CategoryTheory.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'_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 : 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).inv.app X = (app X).inv
• 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.cancel_natIso_inv_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 ⟶ G.obj Y) (f' : W ⟶ X') (g' : X' ⟶ G.obj Y) : CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g (α.inv.app Y)) = CategoryTheory.CategoryStruct.comp f' (CategoryTheory.CategoryStruct.comp g' (α.inv.app Y)) ↔ CategoryTheory.CategoryStruct.comp f g = CategoryTheory.CategoryStruct.comp f' g'
• 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.preimage_comp 📋 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 Z : C} (f : F.obj X ⟶ F.obj Y) (g : F.obj Y ⟶ F.obj Z) : hF.preimage (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (hF.preimage f) (hF.preimage g)
• CategoryTheory.Functor.preimage_comp 📋 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 Z : C} [F.Full] [F.Faithful] (f : F.obj X ⟶ F.obj Y) (g : F.obj Y ⟶ F.obj Z) : F.preimage (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (F.preimage f) (F.preimage g)
• CategoryTheory.Functor.FullyFaithful.preimage_comp_assoc 📋 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 Z : C} (f : F.obj X ⟶ F.obj Y) (g : F.obj Y ⟶ F.obj Z) {Z✝ : C} (h : Z ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (hF.preimage (CategoryTheory.CategoryStruct.comp f g)) h = CategoryTheory.CategoryStruct.comp (hF.preimage f) (CategoryTheory.CategoryStruct.comp (hF.preimage g) h)
• CategoryTheory.InducedCategory.comp_hom 📋 Mathlib.CategoryTheory.InducedCategory
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v, u₂} D] {F : C → D} {X✝ Y✝ Z✝ : CategoryTheory.InducedCategory D F} (f : X✝.Hom Y✝) (g : Y✝.Hom Z✝) : (CategoryTheory.CategoryStruct.comp f g).hom = CategoryTheory.CategoryStruct.comp f.hom g.hom
• CategoryTheory.InducedCategory.comp_hom_assoc 📋 Mathlib.CategoryTheory.InducedCategory
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v, u₂} D] {F : C → D} {X✝ Y✝ Z✝ : CategoryTheory.InducedCategory D F} (f : X✝.Hom Y✝) (g : Y✝.Hom Z✝) {Z : D} (h : F Z✝ ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g).hom h = CategoryTheory.CategoryStruct.comp f.hom (CategoryTheory.CategoryStruct.comp g.hom h)
• 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.ObjectProperty.FullSubcategory.comp_hom 📋 Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) {X Y Z : P.FullSubcategory} (f : X ⟶ Y) (g : Y ⟶ Z) : (CategoryTheory.CategoryStruct.comp f g).hom = CategoryTheory.CategoryStruct.comp f.hom g.hom
• CategoryTheory.ObjectProperty.FullSubcategory.comp_hom_assoc 📋 Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) {X Y Z : P.FullSubcategory} (f : X ⟶ Y) (g : Y ⟶ Z) {Z✝ : C} (h : Z.obj ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g).hom h = CategoryTheory.CategoryStruct.comp f.hom (CategoryTheory.CategoryStruct.comp g.hom h)
• CategoryTheory.ConcreteCategory.comp_apply 📋 Mathlib.CategoryTheory.ConcreteCategory.Basic
  {C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} {FC : outParam (C → C → Type u_1)} {CC : outParam (C → Type w)} {inst✝¹ : outParam ((X Y : C) → FunLike (FC X Y) (CC X) (CC Y))} [self : CategoryTheory.ConcreteCategory C FC] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) (x : CC X) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) x = (CategoryTheory.ConcreteCategory.hom g) ((CategoryTheory.ConcreteCategory.hom f) x)
• CategoryTheory.hom_comp 📋 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 Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) : ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) = ⇑(CategoryTheory.ConcreteCategory.hom g) ∘ ⇑(CategoryTheory.ConcreteCategory.hom f)
• CategoryTheory.ConcreteCategory.coe_comp 📋 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 Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) : ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) = ⇑(CategoryTheory.ConcreteCategory.hom g) ∘ ⇑(CategoryTheory.ConcreteCategory.hom f)
• CategoryTheory.comp_apply 📋 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 Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) (x : CategoryTheory.ToType X) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) x = (CategoryTheory.ConcreteCategory.hom g) ((CategoryTheory.ConcreteCategory.hom f) x)
• CategoryTheory.ConcreteCategory.mk 📋 Mathlib.CategoryTheory.ConcreteCategory.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {FC : outParam (C → C → Type u_1)} {CC : outParam (C → Type w)} [outParam ((X Y : C) → FunLike (FC X Y) (CC X) (CC Y))] (hom : {X Y : C} → (X ⟶ Y) → FC X Y) (ofHom : {X Y : C} → FC X Y → (X ⟶ Y)) (hom_ofHom : ∀ {X Y : C} (f : FC X Y), hom (ofHom f) = f := by cat_disch) (ofHom_hom : ∀ {X Y : C} (f : X ⟶ Y), ofHom (hom f) = f := by cat_disch) (id_apply : ∀ {X : C} (x : CC X), (hom (CategoryTheory.CategoryStruct.id X)) x = x := by cat_disch) (comp_apply : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) (x : CC X), (hom (CategoryTheory.CategoryStruct.comp f g)) x = (hom g) ((hom f) x) := by cat_disch) : CategoryTheory.ConcreteCategory C FC
• CategoryTheory.Functor.NatTrans.hcomp_eq_whiskerLeft_comp_whiskerRight 📋 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 G : CategoryTheory.Functor C D} {H K : CategoryTheory.Functor D E} (α : F ⟶ G) (β : H ⟶ K) : α ◫ β = CategoryTheory.CategoryStruct.comp (F.whiskerLeft β) (CategoryTheory.Functor.whiskerRight α K)
• CategoryTheory.Functor.NatTrans.hcomp_eq_whiskerRight_comp_whiskerLeft 📋 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 G : CategoryTheory.Functor C D} {H K : CategoryTheory.Functor D E} (α : G ⟶ F) (β : K ⟶ H) : α ◫ β = CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight α K) (F.whiskerLeft β)
• CategoryTheory.Functor.whiskerLeft_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] (F : CategoryTheory.Functor C D) {G H K : CategoryTheory.Functor D E} (α : G ⟶ H) (β : H ⟶ K) : F.whiskerLeft (CategoryTheory.CategoryStruct.comp α β) = CategoryTheory.CategoryStruct.comp (F.whiskerLeft α) (F.whiskerLeft β)
• CategoryTheory.Functor.whiskerRight_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] {G H K : CategoryTheory.Functor C D} (α : G ⟶ H) (β : H ⟶ K) (F : CategoryTheory.Functor D E) : CategoryTheory.Functor.whiskerRight (CategoryTheory.CategoryStruct.comp α β) F = CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight α F) (CategoryTheory.Functor.whiskerRight β F)
• CategoryTheory.Functor.whiskerLeft_comp_whiskerRight 📋 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 G : CategoryTheory.Functor C D} {H K : CategoryTheory.Functor D E} (α : F ⟶ G) (β : H ⟶ K) : CategoryTheory.CategoryStruct.comp (F.whiskerLeft β) (CategoryTheory.Functor.whiskerRight α K) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight α H) (G.whiskerLeft β)

About

Loogle searches Lean and Mathlib definitions and theorems.

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

Usage

Loogle finds definitions and lemmas in various ways:

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

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

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

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

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

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

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

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

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

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

Source code

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

This is Loogle revision 9f11169 serving mathlib revision ce5dd8c