Loogle!

Result

Found 87 declarations mentioning CategoryTheory.Iso.app.

• CategoryTheory.Iso.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) : F.obj X ≅ G.obj X
• CategoryTheory.Iso.app_hom 📋 Mathlib.CategoryTheory.NatIso
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F G : CategoryTheory.Functor C D} (α : F ≅ G) (X : C) : (α.app X).hom = α.hom.app X
• CategoryTheory.Iso.app_inv 📋 Mathlib.CategoryTheory.NatIso
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F G : CategoryTheory.Functor C D} (α : F ≅ G) (X : C) : (α.app X).inv = α.inv.app X
• CategoryTheory.NatIso.trans_app 📋 Mathlib.CategoryTheory.NatIso
  {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) : (α ≪≫ β).app X = α.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 : 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.Discrete.natIso_app 📋 Mathlib.CategoryTheory.Discrete.Basic
  {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {I : Type u₁} {F G : CategoryTheory.Functor (CategoryTheory.Discrete I) C} (f : (i : CategoryTheory.Discrete I) → F.obj i ≅ G.obj i) (i : CategoryTheory.Discrete I) : (CategoryTheory.Discrete.natIso f).app i = f i
• CategoryTheory.Functor.CorepresentableBy.equivUliftCoyonedaIso_symm_apply_homEquiv 📋 Mathlib.CategoryTheory.Yoneda
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (F : CategoryTheory.Functor C (Type (max w v₁))) (X : C) (e : CategoryTheory.uliftCoyoneda.{w, v₁, u₁}.obj (Opposite.op X) ≅ F) {X✝ : C} : ((CategoryTheory.Functor.CorepresentableBy.equivUliftCoyonedaIso F X).symm e).homEquiv = Equiv.ulift.symm.trans (equivEquivIso.symm (e.app X✝))
• CategoryTheory.Functor.RepresentableBy.equivUliftYonedaIso_symm_apply_homEquiv 📋 Mathlib.CategoryTheory.Yoneda
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (F : CategoryTheory.Functor Cᵒᵖ (Type (max w v₁))) (X : C) (e : CategoryTheory.uliftYoneda.{w, v₁, u₁}.obj X ≅ F) {X✝ : C} : ((CategoryTheory.Functor.RepresentableBy.equivUliftYonedaIso F X).symm e).homEquiv = Equiv.ulift.symm.trans (equivEquivIso.symm (e.app (Opposite.op X✝)))
• CategoryTheory.Limits.Cone.functorialityEquivalence_unitIso 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] (F : CategoryTheory.Functor J C) (e : C ≌ D) : (CategoryTheory.Limits.Cone.functorialityEquivalence F e).unitIso = CategoryTheory.NatIso.ofComponents (fun c => CategoryTheory.Limits.Cone.ext (e.unitIso.app ((CategoryTheory.Functor.id (CategoryTheory.Limits.Cone F)).obj c).1) ⋯) ⋯
• CategoryTheory.Limits.Cocone.functorialityEquivalence_unitIso 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] (F : CategoryTheory.Functor J C) (e : C ≌ D) : (CategoryTheory.Limits.Cocone.functorialityEquivalence F e).unitIso = CategoryTheory.NatIso.ofComponents' (fun c => CategoryTheory.Limits.Cocone.extInv (e.unitIso.app ((CategoryTheory.Functor.id (CategoryTheory.Limits.Cocone F)).obj c).pt) ⋯) ⋯
• CategoryTheory.Limits.Cocone.functorialityEquivalence_counitIso 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] (F : CategoryTheory.Functor J C) (e : C ≌ D) : (CategoryTheory.Limits.Cocone.functorialityEquivalence F e).counitIso = CategoryTheory.NatIso.ofComponents' (fun c => CategoryTheory.Limits.Cocone.extInv (e.counitIso.app c.pt) ⋯) ⋯
• CategoryTheory.Limits.Cone.functorialityEquivalence_counitIso 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] (F : CategoryTheory.Functor J C) (e : C ≌ D) : (CategoryTheory.Limits.Cone.functorialityEquivalence F e).counitIso = CategoryTheory.NatIso.ofComponents (fun c => CategoryTheory.Limits.Cone.ext (e.counitIso.app c.pt) ⋯) ⋯
• CategoryTheory.Over.postEquiv_unitIso 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (X : T) (F : T ≌ D) : (CategoryTheory.Over.postEquiv X F).unitIso = CategoryTheory.NatIso.ofComponents (fun A => CategoryTheory.Over.isoMk (F.unitIso.app A.left) ⋯) ⋯
• CategoryTheory.Under.postEquiv_unitIso 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (X : T) (F : T ≌ D) : (CategoryTheory.Under.postEquiv X F).unitIso = CategoryTheory.NatIso.ofComponents (fun A => CategoryTheory.Under.isoMk (F.unitIso.app A.right) ⋯) ⋯
• CategoryTheory.Over.postEquiv_counitIso 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (X : T) (F : T ≌ D) : (CategoryTheory.Over.postEquiv X F).counitIso = CategoryTheory.NatIso.ofComponents (fun A => CategoryTheory.Over.isoMk (F.counitIso.app A.left) ⋯) ⋯
• CategoryTheory.Under.postEquiv_counitIso 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (X : T) (F : T ≌ D) : (CategoryTheory.Under.postEquiv X F).counitIso = CategoryTheory.NatIso.ofComponents (fun A => CategoryTheory.Under.isoMk (F.counitIso.app A.right) ⋯) ⋯
• CategoryTheory.Limits.cospanCompIso_app_left 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
  {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 : X ⟶ Z) (g : Y ⟶ Z) : (CategoryTheory.Limits.cospanCompIso F f g).app CategoryTheory.Limits.WalkingCospan.left = CategoryTheory.Iso.refl (((CategoryTheory.Limits.cospan f g).comp F).obj CategoryTheory.Limits.WalkingCospan.left)
• CategoryTheory.Limits.cospanCompIso_app_one 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
  {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 : X ⟶ Z) (g : Y ⟶ Z) : (CategoryTheory.Limits.cospanCompIso F f g).app CategoryTheory.Limits.WalkingCospan.one = CategoryTheory.Iso.refl (((CategoryTheory.Limits.cospan f g).comp F).obj CategoryTheory.Limits.WalkingCospan.one)
• CategoryTheory.Limits.cospanCompIso_app_right 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
  {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 : X ⟶ Z) (g : Y ⟶ Z) : (CategoryTheory.Limits.cospanCompIso F f g).app CategoryTheory.Limits.WalkingCospan.right = CategoryTheory.Iso.refl (((CategoryTheory.Limits.cospan f g).comp F).obj CategoryTheory.Limits.WalkingCospan.right)
• CategoryTheory.Limits.spanCompIso_app_left 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
  {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 : X ⟶ Y) (g : X ⟶ Z) : (CategoryTheory.Limits.spanCompIso F f g).app CategoryTheory.Limits.WalkingSpan.left = CategoryTheory.Iso.refl (((CategoryTheory.Limits.span f g).comp F).obj CategoryTheory.Limits.WalkingSpan.left)
• CategoryTheory.Limits.spanCompIso_app_right 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
  {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 : X ⟶ Y) (g : X ⟶ Z) : (CategoryTheory.Limits.spanCompIso F f g).app CategoryTheory.Limits.WalkingSpan.right = CategoryTheory.Iso.refl (((CategoryTheory.Limits.span f g).comp F).obj CategoryTheory.Limits.WalkingSpan.right)
• CategoryTheory.Limits.spanCompIso_app_zero 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
  {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 : X ⟶ Y) (g : X ⟶ Z) : (CategoryTheory.Limits.spanCompIso F f g).app CategoryTheory.Limits.WalkingSpan.zero = CategoryTheory.Iso.refl (((CategoryTheory.Limits.span f g).comp F).obj CategoryTheory.Limits.WalkingSpan.zero)
• CategoryTheory.Limits.cospanExt_app_left 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z X' Y' Z' : C} (iX : X ≅ X') (iY : Y ≅ Y') (iZ : Z ≅ Z') {f : X ⟶ Z} {g : Y ⟶ Z} {f' : X' ⟶ Z'} {g' : Y' ⟶ Z'} (wf : CategoryTheory.CategoryStruct.comp iX.hom f' = CategoryTheory.CategoryStruct.comp f iZ.hom) (wg : CategoryTheory.CategoryStruct.comp iY.hom g' = CategoryTheory.CategoryStruct.comp g iZ.hom) : (CategoryTheory.Limits.cospanExt iX iY iZ wf wg).app CategoryTheory.Limits.WalkingCospan.left = iX
• CategoryTheory.Limits.cospanExt_app_one 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z X' Y' Z' : C} (iX : X ≅ X') (iY : Y ≅ Y') (iZ : Z ≅ Z') {f : X ⟶ Z} {g : Y ⟶ Z} {f' : X' ⟶ Z'} {g' : Y' ⟶ Z'} (wf : CategoryTheory.CategoryStruct.comp iX.hom f' = CategoryTheory.CategoryStruct.comp f iZ.hom) (wg : CategoryTheory.CategoryStruct.comp iY.hom g' = CategoryTheory.CategoryStruct.comp g iZ.hom) : (CategoryTheory.Limits.cospanExt iX iY iZ wf wg).app CategoryTheory.Limits.WalkingCospan.one = iZ
• CategoryTheory.Limits.cospanExt_app_right 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z X' Y' Z' : C} (iX : X ≅ X') (iY : Y ≅ Y') (iZ : Z ≅ Z') {f : X ⟶ Z} {g : Y ⟶ Z} {f' : X' ⟶ Z'} {g' : Y' ⟶ Z'} (wf : CategoryTheory.CategoryStruct.comp iX.hom f' = CategoryTheory.CategoryStruct.comp f iZ.hom) (wg : CategoryTheory.CategoryStruct.comp iY.hom g' = CategoryTheory.CategoryStruct.comp g iZ.hom) : (CategoryTheory.Limits.cospanExt iX iY iZ wf wg).app CategoryTheory.Limits.WalkingCospan.right = iY
• CategoryTheory.Limits.spanExt_app_left 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z X' Y' Z' : C} (iX : X ≅ X') (iY : Y ≅ Y') (iZ : Z ≅ Z') {f : X ⟶ Y} {g : X ⟶ Z} {f' : X' ⟶ Y'} {g' : X' ⟶ Z'} (wf : CategoryTheory.CategoryStruct.comp iX.hom f' = CategoryTheory.CategoryStruct.comp f iY.hom) (wg : CategoryTheory.CategoryStruct.comp iX.hom g' = CategoryTheory.CategoryStruct.comp g iZ.hom) : (CategoryTheory.Limits.spanExt iX iY iZ wf wg).app CategoryTheory.Limits.WalkingSpan.left = iY
• CategoryTheory.Limits.spanExt_app_one 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z X' Y' Z' : C} (iX : X ≅ X') (iY : Y ≅ Y') (iZ : Z ≅ Z') {f : X ⟶ Y} {g : X ⟶ Z} {f' : X' ⟶ Y'} {g' : X' ⟶ Z'} (wf : CategoryTheory.CategoryStruct.comp iX.hom f' = CategoryTheory.CategoryStruct.comp f iY.hom) (wg : CategoryTheory.CategoryStruct.comp iX.hom g' = CategoryTheory.CategoryStruct.comp g iZ.hom) : (CategoryTheory.Limits.spanExt iX iY iZ wf wg).app CategoryTheory.Limits.WalkingSpan.zero = iX
• CategoryTheory.Limits.spanExt_app_right 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z X' Y' Z' : C} (iX : X ≅ X') (iY : Y ≅ Y') (iZ : Z ≅ Z') {f : X ⟶ Y} {g : X ⟶ Z} {f' : X' ⟶ Y'} {g' : X' ⟶ Z'} (wf : CategoryTheory.CategoryStruct.comp iX.hom f' = CategoryTheory.CategoryStruct.comp f iY.hom) (wg : CategoryTheory.CategoryStruct.comp iX.hom g' = CategoryTheory.CategoryStruct.comp g iZ.hom) : (CategoryTheory.Limits.spanExt iX iY iZ wf wg).app CategoryTheory.Limits.WalkingSpan.right = iZ
• CategoryTheory.Limits.walkingParallelPairOpEquiv_unitIso_one 📋 Mathlib.CategoryTheory.Limits.Shapes.Equalizers
  : CategoryTheory.Limits.walkingParallelPairOpEquiv.unitIso.app CategoryTheory.Limits.WalkingParallelPair.one = CategoryTheory.Iso.refl CategoryTheory.Limits.WalkingParallelPair.one
• CategoryTheory.Limits.walkingParallelPairOpEquiv_unitIso_zero 📋 Mathlib.CategoryTheory.Limits.Shapes.Equalizers
  : CategoryTheory.Limits.walkingParallelPairOpEquiv.unitIso.app CategoryTheory.Limits.WalkingParallelPair.zero = CategoryTheory.Iso.refl CategoryTheory.Limits.WalkingParallelPair.zero
• CategoryTheory.Limits.walkingParallelPairOpEquiv_counitIso_one 📋 Mathlib.CategoryTheory.Limits.Shapes.Equalizers
  : CategoryTheory.Limits.walkingParallelPairOpEquiv.counitIso.app (Opposite.op CategoryTheory.Limits.WalkingParallelPair.one) = CategoryTheory.Iso.refl (Opposite.op CategoryTheory.Limits.WalkingParallelPair.one)
• CategoryTheory.Limits.walkingParallelPairOpEquiv_counitIso_zero 📋 Mathlib.CategoryTheory.Limits.Shapes.Equalizers
  : CategoryTheory.Limits.walkingParallelPairOpEquiv.counitIso.app (Opposite.op CategoryTheory.Limits.WalkingParallelPair.zero) = CategoryTheory.Iso.refl (Opposite.op CategoryTheory.Limits.WalkingParallelPair.zero)
• CategoryTheory.Monoidal.transportStruct_rightUnitor 📋 Mathlib.CategoryTheory.Monoidal.Transport
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) (X : D) : CategoryTheory.MonoidalCategoryStruct.rightUnitor X = e.functor.mapIso (CategoryTheory.MonoidalCategory.whiskerLeftIso (e.inverse.obj X) (e.unitIso.app (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).symm ≪≫ CategoryTheory.MonoidalCategoryStruct.rightUnitor (e.inverse.obj X)) ≪≫ e.counitIso.app X
• CategoryTheory.Monoidal.transportStruct_leftUnitor 📋 Mathlib.CategoryTheory.Monoidal.Transport
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) (X : D) : CategoryTheory.MonoidalCategoryStruct.leftUnitor X = e.functor.mapIso (CategoryTheory.MonoidalCategory.whiskerRightIso (e.unitIso.app (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).symm (e.inverse.obj X) ≪≫ CategoryTheory.MonoidalCategoryStruct.leftUnitor (e.inverse.obj X)) ≪≫ e.counitIso.app X
• CategoryTheory.Monoidal.transportStruct_associator 📋 Mathlib.CategoryTheory.Monoidal.Transport
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) (X Y Z : D) : CategoryTheory.MonoidalCategoryStruct.associator X Y Z = e.functor.mapIso (CategoryTheory.MonoidalCategory.whiskerRightIso (e.unitIso.app (CategoryTheory.MonoidalCategoryStruct.tensorObj (e.inverse.obj X) (e.inverse.obj Y))).symm (e.inverse.obj Z) ≪≫ CategoryTheory.MonoidalCategoryStruct.associator (e.inverse.obj X) (e.inverse.obj Y) (e.inverse.obj Z) ≪≫ CategoryTheory.MonoidalCategory.whiskerLeftIso (e.inverse.obj X) (e.unitIso.app (CategoryTheory.MonoidalCategoryStruct.tensorObj (e.inverse.obj Y) (e.inverse.obj Z))))
• CommRingCat.tensorProdIsoPushout_app 📋 Mathlib.Algebra.Category.Ring.Under.Basic
  {R S : CommRingCat} [Algebra ↑R ↑S] (A : CategoryTheory.Under R) : (R.tensorProdIsoPushout S).app A = CommRingCat.tensorProdObjIsoPushoutObj S A
• CategoryTheory.WithInitial.liftToInitialUnique_hom_app 📋 Mathlib.CategoryTheory.WithTerminal.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] {Z : D} (F : CategoryTheory.Functor C D) (hZ : CategoryTheory.Limits.IsInitial Z) (G : CategoryTheory.Functor (CategoryTheory.WithInitial C) D) (h : CategoryTheory.WithInitial.incl.comp G ≅ F) (hG : G.obj CategoryTheory.WithInitial.star ≅ Z) (X : CategoryTheory.WithInitial C) : (CategoryTheory.WithInitial.liftToInitialUnique F hZ G h hG).hom.app X = (match X with | CategoryTheory.WithInitial.of x => h.app x | CategoryTheory.WithInitial.star => hG).hom
• CategoryTheory.WithInitial.liftToInitialUnique_inv_app 📋 Mathlib.CategoryTheory.WithTerminal.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] {Z : D} (F : CategoryTheory.Functor C D) (hZ : CategoryTheory.Limits.IsInitial Z) (G : CategoryTheory.Functor (CategoryTheory.WithInitial C) D) (h : CategoryTheory.WithInitial.incl.comp G ≅ F) (hG : G.obj CategoryTheory.WithInitial.star ≅ Z) (X : CategoryTheory.WithInitial C) : (CategoryTheory.WithInitial.liftToInitialUnique F hZ G h hG).inv.app X = (match X with | CategoryTheory.WithInitial.of x => h.app x | CategoryTheory.WithInitial.star => hG).inv
• CategoryTheory.WithTerminal.liftToTerminalUnique_hom_app 📋 Mathlib.CategoryTheory.WithTerminal.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] {Z : D} (F : CategoryTheory.Functor C D) (hZ : CategoryTheory.Limits.IsTerminal Z) (G : CategoryTheory.Functor (CategoryTheory.WithTerminal C) D) (h : CategoryTheory.WithTerminal.incl.comp G ≅ F) (hG : G.obj CategoryTheory.WithTerminal.star ≅ Z) (X : CategoryTheory.WithTerminal C) : (CategoryTheory.WithTerminal.liftToTerminalUnique F hZ G h hG).hom.app X = (match X with | CategoryTheory.WithTerminal.of x => h.app x | CategoryTheory.WithTerminal.star => hG).hom
• CategoryTheory.WithTerminal.liftToTerminalUnique_inv_app 📋 Mathlib.CategoryTheory.WithTerminal.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] {Z : D} (F : CategoryTheory.Functor C D) (hZ : CategoryTheory.Limits.IsTerminal Z) (G : CategoryTheory.Functor (CategoryTheory.WithTerminal C) D) (h : CategoryTheory.WithTerminal.incl.comp G ≅ F) (hG : G.obj CategoryTheory.WithTerminal.star ≅ Z) (X : CategoryTheory.WithTerminal C) : (CategoryTheory.WithTerminal.liftToTerminalUnique F hZ G h hG).inv.app X = (match X with | CategoryTheory.WithTerminal.of x => h.app x | CategoryTheory.WithTerminal.star => hG).inv
• CategoryTheory.WithInitial.equivComma_unitIso_hom_app_app 📋 Mathlib.CategoryTheory.WithTerminal.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] (X : CategoryTheory.Functor (CategoryTheory.WithInitial C) D) (X✝ : CategoryTheory.WithInitial C) : (CategoryTheory.WithInitial.equivComma.unitIso.hom.app X).app X✝ = (match X✝ with | CategoryTheory.WithInitial.of x => (CategoryTheory.Iso.refl (CategoryTheory.WithInitial.incl.comp X)).app x | CategoryTheory.WithInitial.star => CategoryTheory.Iso.refl (X.obj CategoryTheory.WithInitial.star)).hom
• CategoryTheory.WithInitial.equivComma_unitIso_inv_app_app 📋 Mathlib.CategoryTheory.WithTerminal.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] (X : CategoryTheory.Functor (CategoryTheory.WithInitial C) D) (X✝ : CategoryTheory.WithInitial C) : (CategoryTheory.WithInitial.equivComma.unitIso.inv.app X).app X✝ = (match X✝ with | CategoryTheory.WithInitial.of x => (CategoryTheory.Iso.refl (CategoryTheory.WithInitial.incl.comp X)).app x | CategoryTheory.WithInitial.star => CategoryTheory.Iso.refl (X.obj CategoryTheory.WithInitial.star)).inv
• CategoryTheory.WithTerminal.equivComma_unitIso_hom_app_app 📋 Mathlib.CategoryTheory.WithTerminal.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] (X : CategoryTheory.Functor (CategoryTheory.WithTerminal C) D) (X✝ : CategoryTheory.WithTerminal C) : (CategoryTheory.WithTerminal.equivComma.unitIso.hom.app X).app X✝ = (match X✝ with | CategoryTheory.WithTerminal.of x => (CategoryTheory.Iso.refl (CategoryTheory.WithTerminal.incl.comp X)).app x | CategoryTheory.WithTerminal.star => CategoryTheory.Iso.refl (X.obj CategoryTheory.WithTerminal.star)).hom
• CategoryTheory.WithTerminal.equivComma_unitIso_inv_app_app 📋 Mathlib.CategoryTheory.WithTerminal.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] (X : CategoryTheory.Functor (CategoryTheory.WithTerminal C) D) (X✝ : CategoryTheory.WithTerminal C) : (CategoryTheory.WithTerminal.equivComma.unitIso.inv.app X).app X✝ = (match X✝ with | CategoryTheory.WithTerminal.of x => (CategoryTheory.Iso.refl (CategoryTheory.WithTerminal.incl.comp X)).app x | CategoryTheory.WithTerminal.star => CategoryTheory.Iso.refl (X.obj CategoryTheory.WithTerminal.star)).inv
• CategoryTheory.MonoOver.congr_inverse 📋 Mathlib.CategoryTheory.Subobject.MonoOver
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (X : C) {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) : (CategoryTheory.MonoOver.congr X e).inverse = (CategoryTheory.MonoOver.lift (CategoryTheory.Over.post e.inverse) ⋯).comp (CategoryTheory.MonoOver.mapIso (e.unitIso.symm.app X)).functor
• CategoryTheory.MonoOver.congr_unitIso 📋 Mathlib.CategoryTheory.Subobject.MonoOver
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (X : C) {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) : (CategoryTheory.MonoOver.congr X e).unitIso = CategoryTheory.NatIso.ofComponents (fun Y => CategoryTheory.MonoOver.isoMk (e.unitIso.app Y.obj.left) ⋯) ⋯
• CategoryTheory.MonoOver.congr_counitIso 📋 Mathlib.CategoryTheory.Subobject.MonoOver
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (X : C) {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) : (CategoryTheory.MonoOver.congr X e).counitIso = CategoryTheory.NatIso.ofComponents (fun Y => CategoryTheory.MonoOver.isoMk (e.counitIso.app Y.obj.left) ⋯) ⋯
• CategoryTheory.Localization.equivalence_counitIso_app 📋 Mathlib.CategoryTheory.Localization.Equivalence
  {C₁ : Type u_1} {C₂ : Type u_2} {D₁ : Type u_4} {D₂ : Type u_5} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Category.{v_4, u_4} D₁] [CategoryTheory.Category.{v_5, u_5} D₂] (L₁ : CategoryTheory.Functor C₁ D₁) (W₁ : CategoryTheory.MorphismProperty C₁) [L₁.IsLocalization W₁] (L₂ : CategoryTheory.Functor C₂ D₂) (W₂ : CategoryTheory.MorphismProperty C₂) [L₂.IsLocalization W₂] (G : CategoryTheory.Functor C₁ D₂) (G' : CategoryTheory.Functor D₁ D₂) [CategoryTheory.Localization.Lifting L₁ W₁ G G'] (F : CategoryTheory.Functor C₂ D₁) (F' : CategoryTheory.Functor D₂ D₁) [CategoryTheory.Localization.Lifting L₂ W₂ F F'] (α : G.comp F' ≅ L₁) (β : F.comp G' ≅ L₂) (X : C₂) : (CategoryTheory.Localization.equivalence L₁ W₁ L₂ W₂ G G' F F' α β).counitIso.app (L₂.obj X) = (CategoryTheory.Localization.Lifting.iso L₂ W₂ (F.comp G') (F'.comp G')).app X ≪≫ β.app X
• CategoryTheory.Localization.SmallShiftedHom.equiv_apply 📋 Mathlib.CategoryTheory.Localization.SmallShiftedHom
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (W : CategoryTheory.MorphismProperty C) {M : Type w'} [AddMonoid M] [CategoryTheory.HasShift C M] [CategoryTheory.HasShift D M] (L : CategoryTheory.Functor C D) [L.IsLocalization W] [L.CommShift M] {X Y : C} [CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M X Y] {m : M} (f : CategoryTheory.Localization.SmallShiftedHom W X Y m) : (CategoryTheory.Localization.SmallShiftedHom.equiv W L) f = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Localization.SmallHom.equiv W L) f) ((CategoryTheory.Functor.commShiftIso L m).app Y).hom
• CategoryTheory.IsSifted.factorization_prodComparison_colim 📋 Mathlib.CategoryTheory.Limits.Sifted
  {C : Type u} [CategoryTheory.SmallCategory C] (X Y : CategoryTheory.Functor C (Type u)) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.HasColimit.isoOfNatIso ((CategoryTheory.MonoidalCategory.externalProductCompDiagIso C (Type u)).app (X, Y)).symm).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.pre (CategoryTheory.MonoidalCategory.externalProduct X Y) (CategoryTheory.Functor.diag C)) (CategoryTheory.Limits.PreservesColimit₂.isoColimitUncurryWhiskeringLeft₂ X Y (CategoryTheory.MonoidalCategory.curriedTensor (Type u))).hom) = CategoryTheory.CartesianMonoidalCategory.prodComparison CategoryTheory.Limits.colim X Y
• CategoryTheory.sheafToPresheafCompCoyonedaCompWhiskeringLeftSheafToPresheaf_app_app 📋 Mathlib.CategoryTheory.Sites.Sheaf
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {A : Type u₂} [CategoryTheory.Category.{v₂, u₂} A] {X Y : CategoryTheory.Sheaf J A} : (CategoryTheory.sheafToPresheafCompCoyonedaCompWhiskeringLeftSheafToPresheaf.app (Opposite.op X)).app Y = CategoryTheory.Sheaf.homEquiv.symm.toIso
• CategoryTheory.sheafToPresheafCompYonedaCompWhiskeringLeftSheafToPresheaf_app_app 📋 Mathlib.CategoryTheory.Sites.Sheaf
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {A : Type u₂} [CategoryTheory.Category.{v₂, u₂} A] {X Y : CategoryTheory.Sheaf J A} : (CategoryTheory.sheafToPresheafCompYonedaCompWhiskeringLeftSheafToPresheaf.app X).app (Opposite.op Y) = CategoryTheory.Sheaf.homEquiv.symm.toIso
• CategoryTheory.Limits.colimitLimitToLimitColimitCone_hom 📋 Mathlib.CategoryTheory.Limits.ColimitLimit
  {J : Type u₁} {K : Type u₂} [CategoryTheory.Category.{v₁, u₁} J] [CategoryTheory.Category.{v₂, u₂} K] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasLimitsOfShape J C] [CategoryTheory.Limits.HasColimitsOfShape K C] (G : CategoryTheory.Functor J (CategoryTheory.Functor K C)) [CategoryTheory.Limits.HasLimit G] : (CategoryTheory.Limits.colimitLimitToLimitColimitCone G).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colim.map (CategoryTheory.Limits.limitIsoSwapCompLim G).hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimitLimitToLimitColimit (CategoryTheory.Functor.uncurry.obj G)) (CategoryTheory.Limits.lim.map (CategoryTheory.Functor.whiskerRight (CategoryTheory.Functor.currying.unitIso.app G).inv CategoryTheory.Limits.colim)))
• HomologicalComplex₂.totalShift₁Iso_trans_totalShift₂Iso 📋 Mathlib.Algebra.Homology.TotalComplexShift
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] (K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)) (x y : ℤ) [K.HasTotal (ComplexShape.up ℤ)] : ((HomologicalComplex₂.shiftFunctor₂ C y).obj K).totalShift₁Iso x ≪≫ (CategoryTheory.shiftFunctor (CochainComplex C ℤ) x).mapIso (K.totalShift₂Iso y) = (x * y).negOnePow • HomologicalComplex₂.total.mapIso ((HomologicalComplex₂.shiftFunctor₁₂CommIso C x y).app K) (ComplexShape.up ℤ) ≪≫ ((HomologicalComplex₂.shiftFunctor₁ C x).obj K).totalShift₂Iso y ≪≫ (CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) y).mapIso (K.totalShift₁Iso x) ≪≫ (CategoryTheory.shiftFunctorComm (CochainComplex C ℤ) x y).app (K.total (ComplexShape.up ℤ))
• CochainComplex.mapBifunctorShift₁Iso_trans_mapBifunctorShift₂Iso 📋 Mathlib.Algebra.Homology.BifunctorShift
  {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Category.{v_3, u_3} D] [CategoryTheory.Preadditive C₁] [CategoryTheory.Preadditive C₂] [CategoryTheory.Preadditive D] (K₁ : CochainComplex C₁ ℤ) (K₂ : CochainComplex C₂ ℤ) (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) [F.Additive] [∀ (X₁ : C₁), (F.obj X₁).Additive] (x y : ℤ) [K₁.HasMapBifunctor K₂ F] : K₁.mapBifunctorShift₁Iso ((CategoryTheory.shiftFunctor (CochainComplex C₂ ℤ) y).obj K₂) F x ≪≫ (CategoryTheory.shiftFunctor (CochainComplex D ℤ) x).mapIso (K₁.mapBifunctorShift₂Iso K₂ F y) = (x * y).negOnePow • ((CategoryTheory.shiftFunctor (CochainComplex C₁ ℤ) x).obj K₁).mapBifunctorShift₂Iso K₂ F y ≪≫ (CategoryTheory.shiftFunctor (CochainComplex D ℤ) y).mapIso (K₁.mapBifunctorShift₁Iso K₂ F x) ≪≫ (CategoryTheory.shiftFunctorComm (CochainComplex D ℤ) x y).app (K₁.mapBifunctor K₂ F)
• AlgebraicGeometry.Scheme.SpecΓIdentity_app 📋 Mathlib.AlgebraicGeometry.Scheme
  (R : CommRingCat) : AlgebraicGeometry.Scheme.SpecΓIdentity.app R = AlgebraicGeometry.Scheme.ΓSpecIso R
• CategoryTheory.GlueData.diagramIso_app_right 📋 Mathlib.CategoryTheory.GlueData
  {C : Type u₁} [CategoryTheory.Category.{v, u₁} C] {C' : Type u₂} [CategoryTheory.Category.{v, u₂} C'] (D : CategoryTheory.GlueData C) (F : CategoryTheory.Functor C C') [∀ (i j k : D.J), CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan (D.f i j) (D.f i k)) F] (i : D.J) : (D.diagramIso F).app (CategoryTheory.Limits.WalkingMultispan.right i) = CategoryTheory.Iso.refl ((D.diagram.multispan.comp F).obj (CategoryTheory.Limits.WalkingMultispan.right i))
• CategoryTheory.GlueData.diagramIso_app_left 📋 Mathlib.CategoryTheory.GlueData
  {C : Type u₁} [CategoryTheory.Category.{v, u₁} C] {C' : Type u₂} [CategoryTheory.Category.{v, u₂} C'] (D : CategoryTheory.GlueData C) (F : CategoryTheory.Functor C C') [∀ (i j k : D.J), CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan (D.f i j) (D.f i k)) F] (i : D.J × D.J) : (D.diagramIso F).app (CategoryTheory.Limits.WalkingMultispan.left i) = CategoryTheory.Iso.refl ((D.diagram.multispan.comp F).obj (CategoryTheory.Limits.WalkingMultispan.left i))
• CategoryTheory.GrothendieckTopology.uliftYonedaOpCompCoyoneda_app_app 📋 Mathlib.CategoryTheory.Sites.Subcanonical
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) [J.Subcanonical] (X : Cᵒᵖ) (F : CategoryTheory.Sheaf J (Type (max v v'))) : (J.uliftYonedaOpCompCoyoneda.app X).app F = (J.uliftYonedaEquiv.trans Equiv.ulift.symm).toIso
• AlgebraicTopology.DoldKan.N₁Γ₀_app 📋 Mathlib.AlgebraicTopology.DoldKan.GammaCompN
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteCoproducts C] (K : ChainComplex C ℕ) : AlgebraicTopology.DoldKan.N₁Γ₀.app K = (AlgebraicTopology.DoldKan.Γ₀.splitting K).toKaroubiNondegComplexIsoN₁.symm ≪≫ (CategoryTheory.Idempotents.toKaroubi (ChainComplex C ℕ)).mapIso (AlgebraicTopology.DoldKan.Γ₀NondegComplexIso K)
• AlgebraicTopology.DoldKan.compatibility_Γ₂N₁_Γ₂N₂_natTrans 📋 Mathlib.AlgebraicTopology.DoldKan.NCompGamma
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteCoproducts C] (X : CategoryTheory.SimplicialObject C) : AlgebraicTopology.DoldKan.Γ₂N₁.natTrans.app X = CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.Γ₂N₂ToKaroubiIso.app X).inv (AlgebraicTopology.DoldKan.Γ₂N₂.natTrans.app ((CategoryTheory.Idempotents.toKaroubi (CategoryTheory.SimplicialObject C)).obj X))
• AugmentedSimplexCategory.equivAugmentedCosimplicialObject_unitIso_hom_app_app 📋 Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Basic
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (X : CategoryTheory.Functor (CategoryTheory.WithInitial SimplexCategory) C) (X✝ : CategoryTheory.WithInitial SimplexCategory) : (AugmentedSimplexCategory.equivAugmentedCosimplicialObject.unitIso.hom.app X).app X✝ = (match X✝ with | CategoryTheory.WithInitial.of x => (CategoryTheory.Iso.refl (CategoryTheory.WithInitial.incl.comp X)).app x | CategoryTheory.WithInitial.star => CategoryTheory.Iso.refl (X.obj CategoryTheory.WithInitial.star)).hom
• AugmentedSimplexCategory.equivAugmentedCosimplicialObject_unitIso_inv_app_app 📋 Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Basic
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (X : CategoryTheory.Functor (CategoryTheory.WithInitial SimplexCategory) C) (X✝ : CategoryTheory.WithInitial SimplexCategory) : (AugmentedSimplexCategory.equivAugmentedCosimplicialObject.unitIso.inv.app X).app X✝ = (match X✝ with | CategoryTheory.WithInitial.of x => (CategoryTheory.Iso.refl (CategoryTheory.WithInitial.incl.comp X)).app x | CategoryTheory.WithInitial.star => CategoryTheory.Iso.refl (X.obj CategoryTheory.WithInitial.star)).inv
• AugmentedSimplexCategory.equivAugmentedSimplicialObject_unitIso_hom_app_app 📋 Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Basic
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (X : CategoryTheory.Functor (CategoryTheory.WithInitial SimplexCategory)ᵒᵖ C) (X✝ : (CategoryTheory.WithInitial SimplexCategory)ᵒᵖ) : (AugmentedSimplexCategory.equivAugmentedSimplicialObject.unitIso.hom.app X).app X✝ = CategoryTheory.CategoryStruct.comp (X.map (match Opposite.unop X✝ with | CategoryTheory.WithInitial.of x => CategoryTheory.Iso.refl (Opposite.op (CategoryTheory.WithInitial.of x)) | CategoryTheory.WithInitial.star => CategoryTheory.Iso.refl (Opposite.op CategoryTheory.WithInitial.star)).hom) (match match Opposite.unop X✝ with | CategoryTheory.WithInitial.of x => CategoryTheory.WithTerminal.of (Opposite.op x) | CategoryTheory.WithInitial.star => CategoryTheory.WithTerminal.star with | CategoryTheory.WithTerminal.of x => (CategoryTheory.Iso.refl (CategoryTheory.WithTerminal.incl.comp ((CategoryTheory.WithInitial.opEquiv SimplexCategory).inverse.comp X))).app x | CategoryTheory.WithTerminal.star => CategoryTheory.Iso.refl (X.obj (Opposite.op CategoryTheory.WithInitial.star))).hom
• AugmentedSimplexCategory.equivAugmentedSimplicialObject_unitIso_inv_app_app 📋 Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Basic
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (X : CategoryTheory.Functor (CategoryTheory.WithInitial SimplexCategory)ᵒᵖ C) (X✝ : (CategoryTheory.WithInitial SimplexCategory)ᵒᵖ) : (AugmentedSimplexCategory.equivAugmentedSimplicialObject.unitIso.inv.app X).app X✝ = CategoryTheory.CategoryStruct.comp (match match Opposite.unop X✝ with | CategoryTheory.WithInitial.of x => CategoryTheory.WithTerminal.of (Opposite.op x) | CategoryTheory.WithInitial.star => CategoryTheory.WithTerminal.star with | CategoryTheory.WithTerminal.of x => (CategoryTheory.Iso.refl (CategoryTheory.WithTerminal.incl.comp ((CategoryTheory.WithInitial.opEquiv SimplexCategory).inverse.comp X))).app x | CategoryTheory.WithTerminal.star => CategoryTheory.Iso.refl (X.obj (Opposite.op CategoryTheory.WithInitial.star))).inv (X.map (match Opposite.unop X✝ with | CategoryTheory.WithInitial.of x => CategoryTheory.Iso.refl (Opposite.op (CategoryTheory.WithInitial.of x)) | CategoryTheory.WithInitial.star => CategoryTheory.Iso.refl (Opposite.op CategoryTheory.WithInitial.star)).inv)
• CategoryTheory.yonedaYonedaColimit_app_inv 📋 Mathlib.CategoryTheory.Limits.Preserves.Yoneda
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [CategoryTheory.Category.{v₂, u₂} J] [CategoryTheory.Limits.HasColimitsOfShape J (Type v₁)] [CategoryTheory.Limits.HasColimitsOfShape J (Type (max u₁ v₁))] (F : CategoryTheory.Functor J (CategoryTheory.Functor Cᵒᵖ (Type v₁))) {X : C} : ((CategoryTheory.yonedaYonedaColimit F).app (Opposite.op X)).inv = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimitObjIsoColimitCompEvaluation (F.comp CategoryTheory.yoneda) (CategoryTheory.yoneda.op.obj (Opposite.op X))).hom (CategoryTheory.Limits.colimit.post F (CategoryTheory.coyoneda.obj (Opposite.op (CategoryTheory.yoneda.obj X))))
• CategoryTheory.Functor.mapActionCongr_hom 📋 Mathlib.CategoryTheory.Action.Basic
  {V : Type u_1} [CategoryTheory.Category.{v_1, u_1} V] {W : Type u_2} [CategoryTheory.Category.{v_2, u_2} W] (G : Type u_3) [Monoid G] {F F' : CategoryTheory.Functor V W} (e : F ≅ F') : (CategoryTheory.Functor.mapActionCongr G e).hom = { app := fun X => (Action.mkIso (e.app X.V) ⋯).hom, naturality := ⋯ }
• CategoryTheory.Functor.mapActionCongr_inv 📋 Mathlib.CategoryTheory.Action.Basic
  {V : Type u_1} [CategoryTheory.Category.{v_1, u_1} V] {W : Type u_2} [CategoryTheory.Category.{v_2, u_2} W] (G : Type u_3) [Monoid G] {F F' : CategoryTheory.Functor V W} (e : F ≅ F') : (CategoryTheory.Functor.mapActionCongr G e).inv = { app := fun X => (Action.mkIso (e.app X.V) ⋯).inv, naturality := ⋯ }
• CategoryTheory.Functor.mapContActionCongr_hom 📋 Mathlib.CategoryTheory.Action.Continuous
  {V : Type u_5} {W : Type u_6} [CategoryTheory.Category.{v_2, u_5} V] {FV : V → V → Type u_7} {CV : V → Type u_8} [(X Y : V) → FunLike (FV X Y) (CV X) (CV Y)] [CategoryTheory.ConcreteCategory V FV] [CategoryTheory.HasForget₂ V TopCat] [CategoryTheory.Category.{v_3, u_6} W] {FW : W → W → Type u_9} {CW : W → Type u_10} [(X Y : W) → FunLike (FW X Y) (CW X) (CW Y)] [CategoryTheory.ConcreteCategory W FW] [CategoryTheory.HasForget₂ W TopCat] (G : Type u_11) [Monoid G] [TopologicalSpace G] {F F' : CategoryTheory.Functor V W} (e : F ≅ F') (H : ∀ (X : ContAction V G), ((F.mapAction G).obj X.obj).IsContinuous) (H' : ∀ (X : ContAction V G), ((F'.mapAction G).obj X.obj).IsContinuous) : (CategoryTheory.Functor.mapContActionCongr G e H H').hom = { app := fun X => CategoryTheory.ObjectProperty.homMk (Action.mkIso (e.app X.obj.V) ⋯).hom, naturality := ⋯ }
• CategoryTheory.Functor.mapContActionCongr_inv 📋 Mathlib.CategoryTheory.Action.Continuous
  {V : Type u_5} {W : Type u_6} [CategoryTheory.Category.{v_2, u_5} V] {FV : V → V → Type u_7} {CV : V → Type u_8} [(X Y : V) → FunLike (FV X Y) (CV X) (CV Y)] [CategoryTheory.ConcreteCategory V FV] [CategoryTheory.HasForget₂ V TopCat] [CategoryTheory.Category.{v_3, u_6} W] {FW : W → W → Type u_9} {CW : W → Type u_10} [(X Y : W) → FunLike (FW X Y) (CW X) (CW Y)] [CategoryTheory.ConcreteCategory W FW] [CategoryTheory.HasForget₂ W TopCat] (G : Type u_11) [Monoid G] [TopologicalSpace G] {F F' : CategoryTheory.Functor V W} (e : F ≅ F') (H : ∀ (X : ContAction V G), ((F.mapAction G).obj X.obj).IsContinuous) (H' : ∀ (X : ContAction V G), ((F'.mapAction G).obj X.obj).IsContinuous) : (CategoryTheory.Functor.mapContActionCongr G e H H').inv = { app := fun X => CategoryTheory.ObjectProperty.homMk (Action.mkIso (e.app X.obj.V) ⋯).inv, naturality := ⋯ }
• CategoryTheory.PreGaloisCategory.autEmbedding_apply 📋 Mathlib.CategoryTheory.Galois.Topology
  {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat) (σ : CategoryTheory.Aut F) (X : C) : (CategoryTheory.PreGaloisCategory.autEmbedding F) σ X = CategoryTheory.Iso.app σ X
• CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.toFunctorToCategoricalPullback_obj_map_fst 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
  {A : Type u₁} {B : Type u₂} {C : Type u₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor C B) (X : Type u₄) [CategoryTheory.Category.{v₄, u₄} X] (S : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X) {x y : X} (f : x ⟶ y) : (((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.toFunctorToCategoricalPullback F G X).obj S).map f).fst = S.fst.map f
• CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.toFunctorToCategoricalPullback_obj_map_snd 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
  {A : Type u₁} {B : Type u₂} {C : Type u₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor C B) (X : Type u₄) [CategoryTheory.Category.{v₄, u₄} X] (S : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X) {x y : X} (f : x ⟶ y) : (((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.toFunctorToCategoricalPullback F G X).obj S).map f).snd = S.snd.map f
• CategoryTheory.Limits.CategoricalPullback.functorEquiv_inverse_obj_map_fst 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
  {A : Type u₁} {B : Type u₂} {C : Type u₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor C B) (X : Type u₄) [CategoryTheory.Category.{v₄, u₄} X] (S : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X) {x y : X} (f : x ⟶ y) : (((CategoryTheory.Limits.CategoricalPullback.functorEquiv F G X).inverse.obj S).map f).fst = S.fst.map f
• CategoryTheory.Limits.CategoricalPullback.functorEquiv_inverse_obj_map_snd 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
  {A : Type u₁} {B : Type u₂} {C : Type u₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor C B) (X : Type u₄) [CategoryTheory.Category.{v₄, u₄} X] (S : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X) {x y : X} (f : x ⟶ y) : (((CategoryTheory.Limits.CategoricalPullback.functorEquiv F G X).inverse.obj S).map f).snd = S.snd.map f
• CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.toFunctorToCategoricalPullback_map_app_fst 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
  {A : Type u₁} {B : Type u₂} {C : Type u₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor C B) (X : Type u₄) [CategoryTheory.Category.{v₄, u₄} X] {S S' : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X} (φ : S ⟶ S') (x : X) : (((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.toFunctorToCategoricalPullback F G X).map φ).app x).fst = φ.fst.app x
• CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.toFunctorToCategoricalPullback_map_app_snd 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
  {A : Type u₁} {B : Type u₂} {C : Type u₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor C B) (X : Type u₄) [CategoryTheory.Category.{v₄, u₄} X] {S S' : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X} (φ : S ⟶ S') (x : X) : (((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.toFunctorToCategoricalPullback F G X).map φ).app x).snd = φ.snd.app x
• CategoryTheory.Limits.CategoricalPullback.functorEquiv_inverse_map_app_fst 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
  {A : Type u₁} {B : Type u₂} {C : Type u₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor C B) (X : Type u₄) [CategoryTheory.Category.{v₄, u₄} X] {S S' : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X} (φ : S ⟶ S') (x : X) : (((CategoryTheory.Limits.CategoricalPullback.functorEquiv F G X).inverse.map φ).app x).fst = φ.fst.app x
• CategoryTheory.Limits.CategoricalPullback.functorEquiv_inverse_map_app_snd 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
  {A : Type u₁} {B : Type u₂} {C : Type u₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor C B) (X : Type u₄) [CategoryTheory.Category.{v₄, u₄} X] {S S' : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X} (φ : S ⟶ S') (x : X) : (((CategoryTheory.Limits.CategoricalPullback.functorEquiv F G X).inverse.map φ).app x).snd = φ.snd.app x
• CategoryTheory.Localization.Monoidal.map_hexagon_forward_assoc 📋 Mathlib.CategoryTheory.Localization.Monoidal.Braided
  {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] (L : CategoryTheory.Functor C D) (W : CategoryTheory.MorphismProperty C) [CategoryTheory.MonoidalCategory C] [W.IsMonoidal] [L.IsLocalization W] {unit : D} (ε : L.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) ≅ unit) [CategoryTheory.BraidedCategory C] (X Y Z : C) {Z✝ : CategoryTheory.LocalizedMonoidal L W ε} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj Y) (CategoryTheory.MonoidalCategoryStruct.tensorObj ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj Z) ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj X)) ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj X) ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj Y) ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj Z)).hom (CategoryTheory.CategoryStruct.comp (((CategoryTheory.Localization.Monoidal.braidingNatIso L W ε).app ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj X)).app (CategoryTheory.MonoidalCategoryStruct.tensorObj ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj Y) ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj Z))).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj Y) ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj Z) ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj X)).hom h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (((CategoryTheory.Localization.Monoidal.braidingNatIso L W ε).app ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj X)).app ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj Y)).hom ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj Z)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj Y) ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj X) ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj Z)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj Y) (((CategoryTheory.Localization.Monoidal.braidingNatIso L W ε).app ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj X)).app ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj Z)).hom) h))
• CategoryTheory.Localization.Monoidal.map_hexagon_forward 📋 Mathlib.CategoryTheory.Localization.Monoidal.Braided
  {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] (L : CategoryTheory.Functor C D) (W : CategoryTheory.MorphismProperty C) [CategoryTheory.MonoidalCategory C] [W.IsMonoidal] [L.IsLocalization W] {unit : D} (ε : L.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) ≅ unit) [CategoryTheory.BraidedCategory C] (X Y Z : C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj X) ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj Y) ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj Z)).hom (CategoryTheory.CategoryStruct.comp (((CategoryTheory.Localization.Monoidal.braidingNatIso L W ε).app ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj X)).app (CategoryTheory.MonoidalCategoryStruct.tensorObj ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj Y) ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj Z))).hom (CategoryTheory.MonoidalCategoryStruct.associator ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj Y) ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj Z) ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj X)).hom) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (((CategoryTheory.Localization.Monoidal.braidingNatIso L W ε).app ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj X)).app ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj Y)).hom ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj Z)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj Y) ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj X) ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj Z)).hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj Y) (((CategoryTheory.Localization.Monoidal.braidingNatIso L W ε).app ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj X)).app ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj Z)).hom))
• CategoryTheory.Localization.Monoidal.map_hexagon_reverse_assoc 📋 Mathlib.CategoryTheory.Localization.Monoidal.Braided
  {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] (L : CategoryTheory.Functor C D) (W : CategoryTheory.MorphismProperty C) [CategoryTheory.MonoidalCategory C] [W.IsMonoidal] [L.IsLocalization W] {unit : D} (ε : L.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) ≅ unit) [CategoryTheory.BraidedCategory C] (X Y Z : C) {Z✝ : CategoryTheory.LocalizedMonoidal L W ε} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj Z) ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj X)) ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj Y) ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj X) ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj Y) ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj Z)).inv (CategoryTheory.CategoryStruct.comp (((CategoryTheory.Localization.Monoidal.braidingNatIso L W ε).app (CategoryTheory.MonoidalCategoryStruct.tensorObj ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj X) ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj Y))).app ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj Z)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj Z) ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj X) ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj Y)).inv h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj X) (((CategoryTheory.Localization.Monoidal.braidingNatIso L W ε).app ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj Y)).app ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj Z)).hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj X) ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj Z) ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj Y)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (((CategoryTheory.Localization.Monoidal.braidingNatIso L W ε).app ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj X)).app ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj Z)).hom ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj Y)) h))
• CategoryTheory.Localization.Monoidal.map_hexagon_reverse 📋 Mathlib.CategoryTheory.Localization.Monoidal.Braided
  {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] (L : CategoryTheory.Functor C D) (W : CategoryTheory.MorphismProperty C) [CategoryTheory.MonoidalCategory C] [W.IsMonoidal] [L.IsLocalization W] {unit : D} (ε : L.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) ≅ unit) [CategoryTheory.BraidedCategory C] (X Y Z : C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj X) ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj Y) ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj Z)).inv (CategoryTheory.CategoryStruct.comp (((CategoryTheory.Localization.Monoidal.braidingNatIso L W ε).app (CategoryTheory.MonoidalCategoryStruct.tensorObj ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj X) ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj Y))).app ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj Z)).hom (CategoryTheory.MonoidalCategoryStruct.associator ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj Z) ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj X) ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj Y)).inv) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj X) (((CategoryTheory.Localization.Monoidal.braidingNatIso L W ε).app ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj Y)).app ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj Z)).hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj X) ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj Z) ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj Y)).inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight (((CategoryTheory.Localization.Monoidal.braidingNatIso L W ε).app ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj X)).app ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj Z)).hom ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj Y)))
• CategoryTheory.MonoidalCategory.endofunctorMonoidalCategory.evaluationRightAction_actionUnitIso 📋 Mathlib.CategoryTheory.Monoidal.Action.End
  (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] (d : C) : CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionUnitIso d = ((CategoryTheory.Functor.Monoidal.εIso (CategoryTheory.Functor.id (CategoryTheory.Functor C C))).app d).symm
• CategoryTheory.MonoidalCategory.endofunctorMonoidalCategory.evaluationRightAction_actionAssocIso 📋 Mathlib.CategoryTheory.Monoidal.Action.End
  (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] (d : C) (c c' : CategoryTheory.Functor C C) : CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso d c c' = ((CategoryTheory.Functor.Monoidal.μIso (CategoryTheory.Functor.id (CategoryTheory.Functor C C)) c c').app d).symm
• CategoryTheory.Sum.natIsoOfWhiskerLeftInlInr_eq 📋 Mathlib.CategoryTheory.Sums.Products
  {A : Type u_1} [CategoryTheory.Category.{v_1, u_1} A] {A' : Type u_2} [CategoryTheory.Category.{v_2, u_2} A'] {B : Type u} [CategoryTheory.Category.{v, u} B] {F G : CategoryTheory.Functor (A ⊕ A') B} (η₁ : (CategoryTheory.Sum.inl_ A A').comp F ≅ (CategoryTheory.Sum.inl_ A A').comp G) (η₂ : (CategoryTheory.Sum.inr_ A A').comp F ≅ (CategoryTheory.Sum.inr_ A A').comp G) : CategoryTheory.Sum.natIsoOfWhiskerLeftInlInr η₁ η₂ = (CategoryTheory.Sum.functorEquiv A A' B).unitIso.app F ≪≫ (CategoryTheory.Sum.functorEquiv A A' B).inverse.mapIso (η₁.prod η₂) ≪≫ (CategoryTheory.Sum.functorEquiv A A' B).unitIso.symm.app G

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