Loogle!

Result

Found 44 declarations mentioning CategoryTheory.eComp.

• CategoryTheory.eComp 📋 Mathlib.CategoryTheory.Enriched.Basic
  (V : Type v) [CategoryTheory.Category.{w, v} V] [CategoryTheory.MonoidalCategory V] {C : Type u₁} [CategoryTheory.EnrichedCategory V C] (X Y Z : C) : CategoryTheory.MonoidalCategoryStruct.tensorObj (X ⟶[V] Y) (Y ⟶[V] Z) ⟶ X ⟶[V] Z
• CategoryTheory.e_comp_id 📋 Mathlib.CategoryTheory.Enriched.Basic
  (V : Type v) [CategoryTheory.Category.{w, v} V] [CategoryTheory.MonoidalCategory V] {C : Type u₁} [CategoryTheory.EnrichedCategory V C] (X Y : C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor (X ⟶[V] Y)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (X ⟶[V] Y) (CategoryTheory.eId V Y)) (CategoryTheory.eComp V X Y Y)) = CategoryTheory.CategoryStruct.id (X ⟶[V] Y)
• CategoryTheory.e_id_comp 📋 Mathlib.CategoryTheory.Enriched.Basic
  (V : Type v) [CategoryTheory.Category.{w, v} V] [CategoryTheory.MonoidalCategory V] {C : Type u₁} [CategoryTheory.EnrichedCategory V C] (X Y : C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor (X ⟶[V] Y)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.eId V X) (X ⟶[V] Y)) (CategoryTheory.eComp V X X Y)) = CategoryTheory.CategoryStruct.id (X ⟶[V] Y)
• CategoryTheory.e_comp_id_assoc 📋 Mathlib.CategoryTheory.Enriched.Basic
  (V : Type v) [CategoryTheory.Category.{w, v} V] [CategoryTheory.MonoidalCategory V] {C : Type u₁} [CategoryTheory.EnrichedCategory V C] (X Y : C) {Z : V} (h : (X ⟶[V] Y) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor (X ⟶[V] Y)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (X ⟶[V] Y) (CategoryTheory.eId V Y)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eComp V X Y Y) h)) = h
• CategoryTheory.e_id_comp_assoc 📋 Mathlib.CategoryTheory.Enriched.Basic
  (V : Type v) [CategoryTheory.Category.{w, v} V] [CategoryTheory.MonoidalCategory V] {C : Type u₁} [CategoryTheory.EnrichedCategory V C] (X Y : C) {Z : V} (h : (X ⟶[V] Y) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor (X ⟶[V] Y)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.eId V X) (X ⟶[V] Y)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eComp V X X Y) h)) = h
• CategoryTheory.TransportEnrichment.eComp_eq 📋 Mathlib.CategoryTheory.Enriched.Basic
  {V : Type v} [CategoryTheory.Category.{w, v} V] [CategoryTheory.MonoidalCategory V] {C : Type u₁} [CategoryTheory.EnrichedCategory V C] {W : Type v'} [CategoryTheory.Category.{w', v'} W] [CategoryTheory.MonoidalCategory W] (F : CategoryTheory.Functor V W) [F.LaxMonoidal] (X Y Z : CategoryTheory.TransportEnrichment F C) : CategoryTheory.eComp W X Y Z = CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ F (X ⟶[V] Y) (Y ⟶[V] Z)) (F.map (CategoryTheory.eComp V X Y Z))
• CategoryTheory.ForgetEnrichment.homOf_comp 📋 Mathlib.CategoryTheory.Enriched.Basic
  {C : Type u₁} (W : Type v) [CategoryTheory.Category.{w, v} W] [CategoryTheory.MonoidalCategory W] [CategoryTheory.EnrichedCategory W C] {X Y Z : C} (f : CategoryTheory.MonoidalCategoryStruct.tensorUnit W ⟶ X ⟶[W] Y) (g : CategoryTheory.MonoidalCategoryStruct.tensorUnit W ⟶ Y ⟶[W] Z) : CategoryTheory.ForgetEnrichment.homOf W (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit W)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f g) (CategoryTheory.eComp W X Y Z))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ForgetEnrichment.homOf W f) (CategoryTheory.ForgetEnrichment.homOf W g)
• CategoryTheory.EnrichedFunctor.mk 📋 Mathlib.CategoryTheory.Enriched.Basic
  {V : Type v} [CategoryTheory.Category.{w, v} V] [CategoryTheory.MonoidalCategory V] {C : Type u₁} [CategoryTheory.EnrichedCategory V C] {D : Type u₂} [CategoryTheory.EnrichedCategory V D] (obj : C → D) (map : (X Y : C) → (X ⟶[V] Y) ⟶ obj X ⟶[V] obj Y) (map_id : ∀ (X : C), CategoryTheory.CategoryStruct.comp (CategoryTheory.eId V X) (map X X) = CategoryTheory.eId V (obj X) := by cat_disch) (map_comp : ∀ (X Y Z : C), CategoryTheory.CategoryStruct.comp (CategoryTheory.eComp V X Y Z) (map X Z) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (map X Y) (map Y Z)) (CategoryTheory.eComp V (obj X) (obj Y) (obj Z)) := by cat_disch) : CategoryTheory.EnrichedFunctor V C D
• CategoryTheory.EnrichedFunctor.map_comp 📋 Mathlib.CategoryTheory.Enriched.Basic
  {V : Type v} [CategoryTheory.Category.{w, v} V] [CategoryTheory.MonoidalCategory V] {C : Type u₁} [CategoryTheory.EnrichedCategory V C] {D : Type u₂} [CategoryTheory.EnrichedCategory V D] (self : CategoryTheory.EnrichedFunctor V C D) (X Y Z : C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.eComp V X Y Z) (self.map X Z) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (self.map X Y) (self.map Y Z)) (CategoryTheory.eComp V (self.obj X) (self.obj Y) (self.obj Z))
• CategoryTheory.ForgetEnrichment.homTo_comp 📋 Mathlib.CategoryTheory.Enriched.Basic
  {C : Type u₁} (W : Type v) [CategoryTheory.Category.{w, v} W] [CategoryTheory.MonoidalCategory W] [CategoryTheory.EnrichedCategory W C] {X Y Z : CategoryTheory.ForgetEnrichment W C} (f : X ⟶ Y) (g : Y ⟶ Z) : CategoryTheory.ForgetEnrichment.homTo W (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit W)).inv (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.ForgetEnrichment.homTo W f) (CategoryTheory.ForgetEnrichment.homTo W g))) (CategoryTheory.eComp W (CategoryTheory.ForgetEnrichment.to W X) (CategoryTheory.ForgetEnrichment.to W Y) (CategoryTheory.ForgetEnrichment.to W Z))
• CategoryTheory.EnrichedFunctor.map_comp_assoc 📋 Mathlib.CategoryTheory.Enriched.Basic
  {V : Type v} [CategoryTheory.Category.{w, v} V] [CategoryTheory.MonoidalCategory V] {C : Type u₁} [CategoryTheory.EnrichedCategory V C] {D : Type u₂} [CategoryTheory.EnrichedCategory V D] (self : CategoryTheory.EnrichedFunctor V C D) (X Y Z : C) {Z✝ : V} (h : (self.obj X ⟶[V] self.obj Z) ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (CategoryTheory.eComp V X Y Z) (CategoryTheory.CategoryStruct.comp (self.map X Z) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (self.map X Y) (self.map Y Z)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eComp V (self.obj X) (self.obj Y) (self.obj Z)) h)
• CategoryTheory.e_assoc 📋 Mathlib.CategoryTheory.Enriched.Basic
  (V : Type v) [CategoryTheory.Category.{w, v} V] [CategoryTheory.MonoidalCategory V] {C : Type u₁} [CategoryTheory.EnrichedCategory V C] (W X Y Z : C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator (W ⟶[V] X) (X ⟶[V] Y) (Y ⟶[V] Z)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.eComp V W X Y) (Y ⟶[V] Z)) (CategoryTheory.eComp V W Y Z)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (W ⟶[V] X) (CategoryTheory.eComp V X Y Z)) (CategoryTheory.eComp V W X Z)
• CategoryTheory.e_assoc' 📋 Mathlib.CategoryTheory.Enriched.Basic
  (V : Type v) [CategoryTheory.Category.{w, v} V] [CategoryTheory.MonoidalCategory V] {C : Type u₁} [CategoryTheory.EnrichedCategory V C] (W X Y Z : C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator (W ⟶[V] X) (X ⟶[V] Y) (Y ⟶[V] Z)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (W ⟶[V] X) (CategoryTheory.eComp V X Y Z)) (CategoryTheory.eComp V W X Z)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.eComp V W X Y) (Y ⟶[V] Z)) (CategoryTheory.eComp V W Y Z)
• CategoryTheory.e_assoc'_assoc 📋 Mathlib.CategoryTheory.Enriched.Basic
  (V : Type v) [CategoryTheory.Category.{w, v} V] [CategoryTheory.MonoidalCategory V] {C : Type u₁} [CategoryTheory.EnrichedCategory V C] (W X Y Z : C) {Z✝ : V} (h : (W ⟶[V] Z) ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator (W ⟶[V] X) (X ⟶[V] Y) (Y ⟶[V] Z)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (W ⟶[V] X) (CategoryTheory.eComp V X Y Z)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eComp V W X Z) h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.eComp V W X Y) (Y ⟶[V] Z)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eComp V W Y Z) h)
• CategoryTheory.e_assoc_assoc 📋 Mathlib.CategoryTheory.Enriched.Basic
  (V : Type v) [CategoryTheory.Category.{w, v} V] [CategoryTheory.MonoidalCategory V] {C : Type u₁} [CategoryTheory.EnrichedCategory V C] (W X Y Z : C) {Z✝ : V} (h : (W ⟶[V] Z) ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator (W ⟶[V] X) (X ⟶[V] Y) (Y ⟶[V] Z)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.eComp V W X Y) (Y ⟶[V] Z)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eComp V W Y Z) h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (W ⟶[V] X) (CategoryTheory.eComp V X Y Z)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eComp V W X Z) h)
• CategoryTheory.GradedNatTrans.naturality 📋 Mathlib.CategoryTheory.Enriched.Basic
  {V : Type v} [CategoryTheory.Category.{w, v} V] [CategoryTheory.MonoidalCategory V] {C : Type u₁} [CategoryTheory.EnrichedCategory V C] {D : Type u₂} [CategoryTheory.EnrichedCategory V D] {A : CategoryTheory.Center V} {F G : CategoryTheory.EnrichedFunctor V C D} (self : CategoryTheory.GradedNatTrans A F G) (X Y : C) : CategoryTheory.CategoryStruct.comp (A.snd.β (X ⟶[V] Y)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (F.map X Y) (self.app Y)) (CategoryTheory.eComp V (F.obj X) (F.obj Y) (G.obj Y))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (self.app X) (G.map X Y)) (CategoryTheory.eComp V (F.obj X) (G.obj X) (G.obj Y))
• CategoryTheory.GradedNatTrans.mk 📋 Mathlib.CategoryTheory.Enriched.Basic
  {V : Type v} [CategoryTheory.Category.{w, v} V] [CategoryTheory.MonoidalCategory V] {C : Type u₁} [CategoryTheory.EnrichedCategory V C] {D : Type u₂} [CategoryTheory.EnrichedCategory V D] {A : CategoryTheory.Center V} {F G : CategoryTheory.EnrichedFunctor V C D} (app : (X : C) → A.fst ⟶ F.obj X ⟶[V] G.obj X) (naturality : ∀ (X Y : C), CategoryTheory.CategoryStruct.comp (A.snd.β (X ⟶[V] Y)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (F.map X Y) (app Y)) (CategoryTheory.eComp V (F.obj X) (F.obj Y) (G.obj Y))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (app X) (G.map X Y)) (CategoryTheory.eComp V (F.obj X) (G.obj X) (G.obj Y))) : CategoryTheory.GradedNatTrans A F G
• CategoryTheory.GradedNatTrans.naturality_assoc 📋 Mathlib.CategoryTheory.Enriched.Basic
  {V : Type v} [CategoryTheory.Category.{w, v} V] [CategoryTheory.MonoidalCategory V] {C : Type u₁} [CategoryTheory.EnrichedCategory V C] {D : Type u₂} [CategoryTheory.EnrichedCategory V D] {A : CategoryTheory.Center V} {F G : CategoryTheory.EnrichedFunctor V C D} (self : CategoryTheory.GradedNatTrans A F G) (X Y : C) {Z : V} (h : (F.obj X ⟶[V] G.obj Y) ⟶ Z) : CategoryTheory.CategoryStruct.comp (A.snd.β (X ⟶[V] Y)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (F.map X Y) (self.app Y)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eComp V (F.obj X) (F.obj Y) (G.obj Y)) h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (self.app X) (G.map X Y)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eComp V (F.obj X) (G.obj X) (G.obj Y)) h)
• CategoryTheory.eComp_eHomWhiskerLeft 📋 Mathlib.CategoryTheory.Enriched.Ordinary.Basic
  (V : Type u') [CategoryTheory.Category.{v', u'} V] [CategoryTheory.MonoidalCategory V] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.EnrichedOrdinaryCategory V C] (X Y : C) {Z Z' : C} (g : Z ⟶ Z') : CategoryTheory.CategoryStruct.comp (CategoryTheory.eComp V X Y Z) (CategoryTheory.eHomWhiskerLeft V X g) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (X ⟶[V] Y) (CategoryTheory.eHomWhiskerLeft V Y g)) (CategoryTheory.eComp V X Y Z')
• CategoryTheory.eComp_eHomWhiskerRight 📋 Mathlib.CategoryTheory.Enriched.Ordinary.Basic
  (V : Type u') [CategoryTheory.Category.{v', u'} V] [CategoryTheory.MonoidalCategory V] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.EnrichedOrdinaryCategory V C] {X X' : C} (f : X ⟶ X') (Y Z : C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.eComp V X' Y Z) (CategoryTheory.eHomWhiskerRight V f Z) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.eHomWhiskerRight V f Y) (Y ⟶[V] Z)) (CategoryTheory.eComp V X Y Z)
• CategoryTheory.eComp_eHomWhiskerLeft_assoc 📋 Mathlib.CategoryTheory.Enriched.Ordinary.Basic
  (V : Type u') [CategoryTheory.Category.{v', u'} V] [CategoryTheory.MonoidalCategory V] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.EnrichedOrdinaryCategory V C] (X Y : C) {Z Z' : C} (g : Z ⟶ Z') {Z✝ : V} (h : (X ⟶[V] Z') ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (CategoryTheory.eComp V X Y Z) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eHomWhiskerLeft V X g) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (X ⟶[V] Y) (CategoryTheory.eHomWhiskerLeft V Y g)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eComp V X Y Z') h)
• CategoryTheory.eComp_eHomWhiskerRight_assoc 📋 Mathlib.CategoryTheory.Enriched.Ordinary.Basic
  (V : Type u') [CategoryTheory.Category.{v', u'} V] [CategoryTheory.MonoidalCategory V] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.EnrichedOrdinaryCategory V C] {X X' : C} (f : X ⟶ X') (Y Z : C) {Z✝ : V} (h : (X ⟶[V] Z) ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (CategoryTheory.eComp V X' Y Z) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eHomWhiskerRight V f Z) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.eHomWhiskerRight V f Y) (Y ⟶[V] Z)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eComp V X Y Z) h)
• CategoryTheory.eHom_whisker_cancel 📋 Mathlib.CategoryTheory.Enriched.Ordinary.Basic
  (V : Type u') [CategoryTheory.Category.{v', u'} V] [CategoryTheory.MonoidalCategory V] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.EnrichedOrdinaryCategory V C] {X Y Y₁ Z : C} (α : Y ≅ Y₁) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.eHomWhiskerLeft V X α.hom) (Y ⟶[V] Z)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (X ⟶[V] Y₁) (CategoryTheory.eHomWhiskerRight V α.inv Z)) (CategoryTheory.eComp V X Y₁ Z)) = CategoryTheory.eComp V X Y Z
• CategoryTheory.eHom_whisker_cancel_inv 📋 Mathlib.CategoryTheory.Enriched.Ordinary.Basic
  (V : Type u') [CategoryTheory.Category.{v', u'} V] [CategoryTheory.MonoidalCategory V] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.EnrichedOrdinaryCategory V C] {X Y Y₁ Z : C} (α : Y ≅ Y₁) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.eHomWhiskerLeft V X α.inv) (Y₁ ⟶[V] Z)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (X ⟶[V] Y) (CategoryTheory.eHomWhiskerRight V α.hom Z)) (CategoryTheory.eComp V X Y Z)) = CategoryTheory.eComp V X Y₁ Z
• CategoryTheory.eHom_whisker_cancel_assoc 📋 Mathlib.CategoryTheory.Enriched.Ordinary.Basic
  (V : Type u') [CategoryTheory.Category.{v', u'} V] [CategoryTheory.MonoidalCategory V] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.EnrichedOrdinaryCategory V C] {X Y Y₁ Z : C} (α : Y ≅ Y₁) {Z✝ : V} (h : (X ⟶[V] Z) ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.eHomWhiskerLeft V X α.hom) (Y ⟶[V] Z)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (X ⟶[V] Y₁) (CategoryTheory.eHomWhiskerRight V α.inv Z)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eComp V X Y₁ Z) h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eComp V X Y Z) h
• CategoryTheory.eHom_whisker_cancel_inv_assoc 📋 Mathlib.CategoryTheory.Enriched.Ordinary.Basic
  (V : Type u') [CategoryTheory.Category.{v', u'} V] [CategoryTheory.MonoidalCategory V] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.EnrichedOrdinaryCategory V C] {X Y Y₁ Z : C} (α : Y ≅ Y₁) {Z✝ : V} (h : (X ⟶[V] Z) ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.eHomWhiskerLeft V X α.inv) (Y₁ ⟶[V] Z)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (X ⟶[V] Y) (CategoryTheory.eHomWhiskerRight V α.hom Z)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eComp V X Y Z) h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eComp V X Y₁ Z) h
• CategoryTheory.eHomEquiv_comp 📋 Mathlib.CategoryTheory.Enriched.Ordinary.Basic
  (V : Type u') [CategoryTheory.Category.{v', u'} V] [CategoryTheory.MonoidalCategory V] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.EnrichedOrdinaryCategory V C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) : (CategoryTheory.eHomEquiv V) (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit V)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom ((CategoryTheory.eHomEquiv V) f) ((CategoryTheory.eHomEquiv V) g)) (CategoryTheory.eComp V X Y Z))
• CategoryTheory.EnrichedOrdinaryCategory.homEquiv_comp 📋 Mathlib.CategoryTheory.Enriched.Ordinary.Basic
  {V : Type u'} {inst✝ : CategoryTheory.Category.{v', u'} V} {inst✝¹ : CategoryTheory.MonoidalCategory V} {C : Type u} {inst✝² : CategoryTheory.Category.{v, u} C} [self : CategoryTheory.EnrichedOrdinaryCategory V C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) : CategoryTheory.EnrichedOrdinaryCategory.homEquiv (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit V)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.EnrichedOrdinaryCategory.homEquiv f) (CategoryTheory.EnrichedOrdinaryCategory.homEquiv g)) (CategoryTheory.eComp V X Y Z))
• CategoryTheory.eHomEquiv_comp_assoc 📋 Mathlib.CategoryTheory.Enriched.Ordinary.Basic
  (V : Type u') [CategoryTheory.Category.{v', u'} V] [CategoryTheory.MonoidalCategory V] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.EnrichedOrdinaryCategory V C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) {Z✝ : V} (h : (X ⟶[V] Z) ⟶ Z✝) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.eHomEquiv V) (CategoryTheory.CategoryStruct.comp f g)) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit V)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom ((CategoryTheory.eHomEquiv V) f) ((CategoryTheory.eHomEquiv V) g)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eComp V X Y Z) h))
• CategoryTheory.EnrichedOrdinaryCategory.mk 📋 Mathlib.CategoryTheory.Enriched.Ordinary.Basic
  {V : Type u'} [CategoryTheory.Category.{v', u'} V] [CategoryTheory.MonoidalCategory V] {C : Type u} [CategoryTheory.Category.{v, u} C] [toEnrichedCategory : CategoryTheory.EnrichedCategory V C] (homEquiv : {X Y : C} → (X ⟶ Y) ≃ (CategoryTheory.MonoidalCategoryStruct.tensorUnit V ⟶ X ⟶[V] Y)) (homEquiv_id : ∀ (X : C), homEquiv (CategoryTheory.CategoryStruct.id X) = CategoryTheory.eId V X := by cat_disch) (homEquiv_comp : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), homEquiv (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit V)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (homEquiv f) (homEquiv g)) (CategoryTheory.eComp V X Y Z)) := by cat_disch) : CategoryTheory.EnrichedOrdinaryCategory V C
• CategoryTheory.CatEnriched.comp_eq 📋 Mathlib.CategoryTheory.Bicategory.CatEnriched
  {C : Type u_1} [CategoryTheory.EnrichedCategory CategoryTheory.Cat C] {X Y Z : CategoryTheory.CatEnriched C} (f : X ⟶ Y) (g : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp f g = (CategoryTheory.eComp CategoryTheory.Cat X Y Z).toFunctor.obj (f, g)
• CategoryTheory.Enriched.FunctorCategory.enrichedComp_π 📋 Mathlib.CategoryTheory.Enriched.FunctorCategory
  (V : Type u₁) [CategoryTheory.Category.{v₁, u₁} V] [CategoryTheory.MonoidalCategory V] {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {J : Type u₃} [CategoryTheory.Category.{v₃, u₃} J] [CategoryTheory.EnrichedOrdinaryCategory V C] (F₁ F₂ F₃ : CategoryTheory.Functor J C) [CategoryTheory.Enriched.FunctorCategory.HasEnrichedHom V F₁ F₂] [CategoryTheory.Enriched.FunctorCategory.HasEnrichedHom V F₂ F₃] [CategoryTheory.Enriched.FunctorCategory.HasEnrichedHom V F₁ F₃] (j : J) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Enriched.FunctorCategory.enrichedComp V F₁ F₂ F₃) (CategoryTheory.Limits.end_.π (CategoryTheory.Enriched.FunctorCategory.diagram V F₁ F₃) j) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.Limits.end_.π (CategoryTheory.Enriched.FunctorCategory.diagram V F₁ F₂) j) (CategoryTheory.Limits.end_.π (CategoryTheory.Enriched.FunctorCategory.diagram V F₂ F₃) j)) (CategoryTheory.eComp V (Opposite.unop (F₁.op.obj (Opposite.op j))) (F₂.obj j) (F₃.obj j))
• CategoryTheory.Enriched.FunctorCategory.enrichedComp_π_assoc 📋 Mathlib.CategoryTheory.Enriched.FunctorCategory
  (V : Type u₁) [CategoryTheory.Category.{v₁, u₁} V] [CategoryTheory.MonoidalCategory V] {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {J : Type u₃} [CategoryTheory.Category.{v₃, u₃} J] [CategoryTheory.EnrichedOrdinaryCategory V C] (F₁ F₂ F₃ : CategoryTheory.Functor J C) [CategoryTheory.Enriched.FunctorCategory.HasEnrichedHom V F₁ F₂] [CategoryTheory.Enriched.FunctorCategory.HasEnrichedHom V F₂ F₃] [CategoryTheory.Enriched.FunctorCategory.HasEnrichedHom V F₁ F₃] (j : J) {Z : V} (h : ((CategoryTheory.Enriched.FunctorCategory.diagram V F₁ F₃).obj (Opposite.op j)).obj j ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Enriched.FunctorCategory.enrichedComp V F₁ F₂ F₃) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.end_.π (CategoryTheory.Enriched.FunctorCategory.diagram V F₁ F₃) j) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.Limits.end_.π (CategoryTheory.Enriched.FunctorCategory.diagram V F₁ F₂) j) (CategoryTheory.Limits.end_.π (CategoryTheory.Enriched.FunctorCategory.diagram V F₂ F₃) j)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eComp V (Opposite.unop (F₁.op.obj (Opposite.op j))) (F₂.obj j) (F₃.obj j)) h)
• CategoryTheory.Enriched.FunctorCategory.enrichedHom_condition' 📋 Mathlib.CategoryTheory.Enriched.FunctorCategory
  (V : Type u₁) [CategoryTheory.Category.{v₁, u₁} V] [CategoryTheory.MonoidalCategory V] {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {J : Type u₃} [CategoryTheory.Category.{v₃, u₃} J] [CategoryTheory.EnrichedOrdinaryCategory V C] (F₁ F₂ : CategoryTheory.Functor J C) [CategoryTheory.Enriched.FunctorCategory.HasEnrichedHom V F₁ F₂] {i j : J} (f : i ⟶ j) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Enriched.FunctorCategory.enrichedHomπ V F₁ F₂ i) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor (F₁.obj i ⟶[V] F₂.obj i)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (F₁.obj i ⟶[V] F₂.obj i) ((CategoryTheory.eHomEquiv V) (F₂.map f))) (CategoryTheory.eComp V (F₁.obj i) (F₂.obj i) (F₂.obj j)))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Enriched.FunctorCategory.enrichedHomπ V F₁ F₂ j) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor (F₁.obj j ⟶[V] F₂.obj j)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight ((CategoryTheory.eHomEquiv V) (F₁.map f)) (F₁.obj j ⟶[V] F₂.obj j)) (CategoryTheory.eComp V (F₁.obj i) (F₁.obj j) (F₂.obj j))))
• CategoryTheory.Enriched.FunctorCategory.enrichedHom_condition'_assoc 📋 Mathlib.CategoryTheory.Enriched.FunctorCategory
  (V : Type u₁) [CategoryTheory.Category.{v₁, u₁} V] [CategoryTheory.MonoidalCategory V] {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {J : Type u₃} [CategoryTheory.Category.{v₃, u₃} J] [CategoryTheory.EnrichedOrdinaryCategory V C] (F₁ F₂ : CategoryTheory.Functor J C) [CategoryTheory.Enriched.FunctorCategory.HasEnrichedHom V F₁ F₂] {i j : J} (f : i ⟶ j) {Z : V} (h : (F₁.obj i ⟶[V] F₂.obj j) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Enriched.FunctorCategory.enrichedHomπ V F₁ F₂ i) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor (F₁.obj i ⟶[V] F₂.obj i)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (F₁.obj i ⟶[V] F₂.obj i) ((CategoryTheory.eHomEquiv V) (F₂.map f))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eComp V (F₁.obj i) (F₂.obj i) (F₂.obj j)) h))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Enriched.FunctorCategory.enrichedHomπ V F₁ F₂ j) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor (F₁.obj j ⟶[V] F₂.obj j)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight ((CategoryTheory.eHomEquiv V) (F₁.map f)) (F₁.obj j ⟶[V] F₂.obj j)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eComp V (F₁.obj i) (F₁.obj j) (F₂.obj j)) h)))
• CategoryTheory.Iso.eHomCongr_comp 📋 Mathlib.CategoryTheory.Enriched.HomCongr
  (V : Type u') [CategoryTheory.Category.{v', u'} V] [CategoryTheory.MonoidalCategory V] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.EnrichedOrdinaryCategory V C] {X Y Z X₁ Y₁ Z₁ : C} (α : X ≅ X₁) (β : Y ≅ Y₁) (γ : Z ≅ Z₁) (f : X ⟶ Y) (g : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.eHomEquiv V) (CategoryTheory.CategoryStruct.comp f g)) (CategoryTheory.Iso.eHomCongr V α γ).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit V)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.CategoryStruct.comp ((CategoryTheory.eHomEquiv V) f) (CategoryTheory.Iso.eHomCongr V α β).hom) (CategoryTheory.MonoidalCategoryStruct.tensorUnit V)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (X₁ ⟶[V] Y₁) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.eHomEquiv V) g) (CategoryTheory.Iso.eHomCongr V β γ).hom)) (CategoryTheory.eComp V X₁ Y₁ Z₁)))
• CategoryTheory.Iso.eHomCongr_inv_comp 📋 Mathlib.CategoryTheory.Enriched.HomCongr
  (V : Type u') [CategoryTheory.Category.{v', u'} V] [CategoryTheory.MonoidalCategory V] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.EnrichedOrdinaryCategory V C] {X Y Z X₁ Y₁ Z₁ : C} (α : X ≅ X₁) (β : Y ≅ Y₁) (γ : Z ≅ Z₁) (f : X₁ ⟶ Y₁) (g : Y₁ ⟶ Z₁) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.eHomEquiv V) (CategoryTheory.CategoryStruct.comp f g)) (CategoryTheory.Iso.eHomCongr V α γ).inv = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit V)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.CategoryStruct.comp ((CategoryTheory.eHomEquiv V) f) (CategoryTheory.Iso.eHomCongr V α β).inv) (CategoryTheory.MonoidalCategoryStruct.tensorUnit V)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (X ⟶[V] Y) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.eHomEquiv V) g) (CategoryTheory.Iso.eHomCongr V β γ).inv)) (CategoryTheory.eComp V X Y Z)))
• CategoryTheory.Iso.eHomCongr_comp_assoc 📋 Mathlib.CategoryTheory.Enriched.HomCongr
  (V : Type u') [CategoryTheory.Category.{v', u'} V] [CategoryTheory.MonoidalCategory V] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.EnrichedOrdinaryCategory V C] {X Y Z X₁ Y₁ Z₁ : C} (α : X ≅ X₁) (β : Y ≅ Y₁) (γ : Z ≅ Z₁) (f : X ⟶ Y) (g : Y ⟶ Z) {Z✝ : V} (h : (X₁ ⟶[V] Z₁) ⟶ Z✝) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.eHomEquiv V) (CategoryTheory.CategoryStruct.comp f g)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Iso.eHomCongr V α γ).hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit V)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.CategoryStruct.comp ((CategoryTheory.eHomEquiv V) f) (CategoryTheory.Iso.eHomCongr V α β).hom) (CategoryTheory.MonoidalCategoryStruct.tensorUnit V)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (X₁ ⟶[V] Y₁) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.eHomEquiv V) g) (CategoryTheory.Iso.eHomCongr V β γ).hom)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eComp V X₁ Y₁ Z₁) h)))
• CategoryTheory.Iso.eHomCongr_inv_comp_assoc 📋 Mathlib.CategoryTheory.Enriched.HomCongr
  (V : Type u') [CategoryTheory.Category.{v', u'} V] [CategoryTheory.MonoidalCategory V] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.EnrichedOrdinaryCategory V C] {X Y Z X₁ Y₁ Z₁ : C} (α : X ≅ X₁) (β : Y ≅ Y₁) (γ : Z ≅ Z₁) (f : X₁ ⟶ Y₁) (g : Y₁ ⟶ Z₁) {Z✝ : V} (h : (X ⟶[V] Z) ⟶ Z✝) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.eHomEquiv V) (CategoryTheory.CategoryStruct.comp f g)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Iso.eHomCongr V α γ).inv h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit V)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.CategoryStruct.comp ((CategoryTheory.eHomEquiv V) f) (CategoryTheory.Iso.eHomCongr V α β).inv) (CategoryTheory.MonoidalCategoryStruct.tensorUnit V)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (X ⟶[V] Y) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.eHomEquiv V) g) (CategoryTheory.Iso.eHomCongr V β γ).inv)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eComp V X Y Z) h)))
• CategoryTheory.eComp_op_eq 📋 Mathlib.CategoryTheory.Enriched.Opposite
  (V : Type u₁) [CategoryTheory.Category.{v₁, u₁} V] [CategoryTheory.MonoidalCategory V] [CategoryTheory.BraidedCategory V] {C : Type u} [CategoryTheory.EnrichedCategory V C] (x y z : Cᵒᵖ) : CategoryTheory.eComp V z y x = CategoryTheory.CategoryStruct.comp (β_ (Opposite.unop y ⟶[V] Opposite.unop z) (Opposite.unop x ⟶[V] Opposite.unop y)).hom (CategoryTheory.eComp V (Opposite.unop x) (Opposite.unop y) (Opposite.unop z))
• CategoryTheory.eComp_op_eq_assoc 📋 Mathlib.CategoryTheory.Enriched.Opposite
  (V : Type u₁) [CategoryTheory.Category.{v₁, u₁} V] [CategoryTheory.MonoidalCategory V] [CategoryTheory.BraidedCategory V] {C : Type u} [CategoryTheory.EnrichedCategory V C] (x y z : Cᵒᵖ) {Z : V} (h : (z ⟶[V] x) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.eComp V z y x) h = CategoryTheory.CategoryStruct.comp (β_ (Opposite.unop y ⟶[V] Opposite.unop z) (Opposite.unop x ⟶[V] Opposite.unop y)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.eComp V (Opposite.unop x) (Opposite.unop y) (Opposite.unop z)) h)
• CategoryTheory.tensorHom_eComp_op_eq 📋 Mathlib.CategoryTheory.Enriched.Opposite
  (V : Type u₁) [CategoryTheory.Category.{v₁, u₁} V] [CategoryTheory.MonoidalCategory V] [CategoryTheory.BraidedCategory V] {C : Type u} [CategoryTheory.EnrichedCategory V C] {x y z : Cᵒᵖ} {v w : V} (f : v ⟶ z ⟶[V] y) (g : w ⟶ y ⟶[V] x) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f g) (CategoryTheory.eComp V z y x) = CategoryTheory.CategoryStruct.comp (β_ v w).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom g f) (CategoryTheory.eComp V (Opposite.unop x) (Opposite.unop y) (Opposite.unop z)))
• CategoryTheory.tensorHom_eComp_op_eq_assoc 📋 Mathlib.CategoryTheory.Enriched.Opposite
  (V : Type u₁) [CategoryTheory.Category.{v₁, u₁} V] [CategoryTheory.MonoidalCategory V] [CategoryTheory.BraidedCategory V] {C : Type u} [CategoryTheory.EnrichedCategory V C] {x y z : Cᵒᵖ} {v w : V} (f : v ⟶ z ⟶[V] y) (g : w ⟶ y ⟶[V] x) {Z : V} (h : (z ⟶[V] x) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f g) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eComp V z y x) h) = CategoryTheory.CategoryStruct.comp (β_ v w).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom g f) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eComp V (Opposite.unop x) (Opposite.unop y) (Opposite.unop z)) h))
• CategoryTheory.MonoidalClosed.enrichedCategorySelf_comp 📋 Mathlib.CategoryTheory.Monoidal.Closed.Enrichment
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalClosed C] (X Y Z : C) : CategoryTheory.eComp C X Y Z = CategoryTheory.MonoidalClosed.comp X Y Z

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