Loogle!

Result

Found 85 declarations mentioning CategoryTheory.Grothendieck.base.

• CategoryTheory.Grothendieck.base 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} (self : CategoryTheory.Grothendieck F) : C
• CategoryTheory.Grothendieck.fiber 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} (self : CategoryTheory.Grothendieck F) : ↑(F.obj self.base)
• CategoryTheory.Grothendieck.transport 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} (x : CategoryTheory.Grothendieck F) {c : C} (t : x.base ⟶ c) : CategoryTheory.Grothendieck F
• CategoryTheory.Grothendieck.forget_obj 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C CategoryTheory.Cat) (X : CategoryTheory.Grothendieck F) : (CategoryTheory.Grothendieck.forget F).obj X = X.base
• CategoryTheory.Grothendieck.Hom.base 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} {X Y : CategoryTheory.Grothendieck F} (self : X.Hom Y) : X.base ⟶ Y.base
• CategoryTheory.Grothendieck.transport_base 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} (x : CategoryTheory.Grothendieck F) {c : C} (t : x.base ⟶ c) : (x.transport t).base = c
• CategoryTheory.Grothendieck.transportIso 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} (x : CategoryTheory.Grothendieck F) {c : C} (α : x.base ≅ c) : x.transport α.hom ≅ x
• CategoryTheory.Grothendieck.toTransport 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} (x : CategoryTheory.Grothendieck F) {c : C} (t : x.base ⟶ c) : x ⟶ x.transport t
• CategoryTheory.Grothendieck.toTransport_base 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} (x : CategoryTheory.Grothendieck F) {c : C} (t : x.base ⟶ c) : (x.toTransport t).base = t
• CategoryTheory.Grothendieck.id_base 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} (X : CategoryTheory.Grothendieck F) : (CategoryTheory.CategoryStruct.id X).base = CategoryTheory.CategoryStruct.id X.base
• CategoryTheory.Grothendieck.compAsSmallFunctorEquivalenceInverse_obj_base 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C CategoryTheory.Cat) (X : CategoryTheory.Grothendieck F) : ((CategoryTheory.Grothendieck.compAsSmallFunctorEquivalenceInverse F).obj X).base = X.base
• CategoryTheory.Grothendieck.grothendieckTypeToCatInverse_obj_base 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] (G : CategoryTheory.Functor C (Type w)) (X : G.Elements) : ((CategoryTheory.Grothendieck.grothendieckTypeToCatInverse G).obj X).base = X.fst
• CategoryTheory.Grothendieck.compAsSmallFunctorEquivalenceFunctor_obj_base 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C CategoryTheory.Cat) (X : CategoryTheory.Grothendieck (F.comp CategoryTheory.Cat.asSmallFunctor)) : ((CategoryTheory.Grothendieck.compAsSmallFunctorEquivalenceFunctor F).obj X).base = X.base
• CategoryTheory.Grothendieck.map_obj_base 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F G : CategoryTheory.Functor C CategoryTheory.Cat} (α : F ⟶ G) (X : CategoryTheory.Grothendieck F) : ((CategoryTheory.Grothendieck.map α).obj X).base = X.base
• CategoryTheory.Grothendieck.forget_map 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C CategoryTheory.Cat) {X✝ Y✝ : CategoryTheory.Grothendieck F} (f : X✝ ⟶ Y✝) : (CategoryTheory.Grothendieck.forget F).map f = f.base
• CategoryTheory.Grothendieck.grothendieckTypeToCatFunctor_obj_fst 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] (G : CategoryTheory.Functor C (Type w)) (X : CategoryTheory.Grothendieck (G.comp CategoryTheory.typeToCat)) : ((CategoryTheory.Grothendieck.grothendieckTypeToCatFunctor G).obj X).fst = X.base
• CategoryTheory.Grothendieck.base_eqToHom 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} {X Y : CategoryTheory.Grothendieck F} (h : X = Y) : (CategoryTheory.eqToHom h).base = CategoryTheory.eqToHom ⋯
• CategoryTheory.Grothendieck.pre_obj_base 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] (F : CategoryTheory.Functor C CategoryTheory.Cat) (G : CategoryTheory.Functor D C) (X : CategoryTheory.Grothendieck (G.comp F)) : ((CategoryTheory.Grothendieck.pre F G).obj X).base = G.obj X.base
• CategoryTheory.Grothendieck.grothendieckTypeToCat_inverse_obj_base 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] (G : CategoryTheory.Functor C (Type w)) (X : G.Elements) : ((CategoryTheory.Grothendieck.grothendieckTypeToCat G).inverse.obj X).base = X.fst
• CategoryTheory.Grothendieck.grothendieckTypeToCat_functor_obj_fst 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] (G : CategoryTheory.Functor C (Type w)) (X : CategoryTheory.Grothendieck (G.comp CategoryTheory.typeToCat)) : ((CategoryTheory.Grothendieck.grothendieckTypeToCat G).functor.obj X).fst = X.base
• CategoryTheory.Grothendieck.pre_obj_fiber 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] (F : CategoryTheory.Functor C CategoryTheory.Cat) (G : CategoryTheory.Functor D C) (X : CategoryTheory.Grothendieck (G.comp F)) : ((CategoryTheory.Grothendieck.pre F G).obj X).fiber = X.fiber
• CategoryTheory.Grothendieck.transportIso_hom_base 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} (x : CategoryTheory.Grothendieck F) {c : C} (α : x.base ≅ c) : (x.transportIso α).hom.base = α.inv
• CategoryTheory.Grothendieck.transportIso_inv_base 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} (x : CategoryTheory.Grothendieck F) {c : C} (α : x.base ≅ c) : (x.transportIso α).inv.base = α.hom
• CategoryTheory.Grothendieck.grothendieckTypeToCatFunctor_obj_snd 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] (G : CategoryTheory.Functor C (Type w)) (X : CategoryTheory.Grothendieck (G.comp CategoryTheory.typeToCat)) : ((CategoryTheory.Grothendieck.grothendieckTypeToCatFunctor G).obj X).snd = X.fiber.as
• CategoryTheory.Grothendieck.transport_fiber 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} (x : CategoryTheory.Grothendieck F) {c : C} (t : x.base ⟶ c) : (x.transport t).fiber = (F.map t).toFunctor.obj x.fiber
• CategoryTheory.Grothendieck.comp_base 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} {X Y Z : CategoryTheory.Grothendieck F} (f : X ⟶ Y) (g : Y ⟶ Z) : (CategoryTheory.CategoryStruct.comp f g).base = CategoryTheory.CategoryStruct.comp f.base g.base
• CategoryTheory.Grothendieck.grothendieckTypeToCat_functor_obj_snd 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] (G : CategoryTheory.Functor C (Type w)) (X : CategoryTheory.Grothendieck (G.comp CategoryTheory.typeToCat)) : ((CategoryTheory.Grothendieck.grothendieckTypeToCat G).functor.obj X).snd = X.fiber.as
• CategoryTheory.Grothendieck.map_obj 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F G : CategoryTheory.Functor C CategoryTheory.Cat} {α : F ⟶ G} (X : CategoryTheory.Grothendieck F) : (CategoryTheory.Grothendieck.map α).obj X = { base := X.base, fiber := (α.app X.base).toFunctor.obj X.fiber }
• CategoryTheory.Grothendieck.map_obj_fiber 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F G : CategoryTheory.Functor C CategoryTheory.Cat} (α : F ⟶ G) (X : CategoryTheory.Grothendieck F) : ((CategoryTheory.Grothendieck.map α).obj X).fiber = (α.app X.base).toFunctor.obj X.fiber
• CategoryTheory.Grothendieck.isoMk 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} {X Y : CategoryTheory.Grothendieck F} (e₁ : X.base ≅ Y.base) (e₂ : (F.map e₁.hom).toFunctor.obj X.fiber ≅ Y.fiber) : X ≅ Y
• CategoryTheory.Grothendieck.Hom.fiber 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} {X Y : CategoryTheory.Grothendieck F} (self : X.Hom Y) : (F.map self.base).toFunctor.obj X.fiber ⟶ Y.fiber
• CategoryTheory.Grothendieck.Hom.mk 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} {X Y : CategoryTheory.Grothendieck F} (base : X.base ⟶ Y.base) (fiber : (F.map base).toFunctor.obj X.fiber ⟶ Y.fiber) : X.Hom Y
• CategoryTheory.Grothendieck.compAsSmallFunctorEquivalenceInverse_obj_fiber 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C CategoryTheory.Cat) (X : CategoryTheory.Grothendieck F) : ((CategoryTheory.Grothendieck.compAsSmallFunctorEquivalenceInverse F).obj X).fiber = CategoryTheory.AsSmall.up.obj X.fiber
• CategoryTheory.Grothendieck.isoMk_hom_base 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} {X Y : CategoryTheory.Grothendieck F} (e₁ : X.base ≅ Y.base) (e₂ : (F.map e₁.hom).toFunctor.obj X.fiber ≅ Y.fiber) : (CategoryTheory.Grothendieck.isoMk e₁ e₂).hom.base = e₁.hom
• CategoryTheory.Grothendieck.isoMk_inv_base 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} {X Y : CategoryTheory.Grothendieck F} (e₁ : X.base ≅ Y.base) (e₂ : (F.map e₁.hom).toFunctor.obj X.fiber ≅ Y.fiber) : (CategoryTheory.Grothendieck.isoMk e₁ e₂).inv.base = e₁.inv
• CategoryTheory.Grothendieck.eqToHom_eq 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} {X Y : CategoryTheory.Grothendieck F} (hF : X = Y) : CategoryTheory.eqToHom hF = { base := CategoryTheory.eqToHom ⋯, fiber := CategoryTheory.eqToHom ⋯ }
• CategoryTheory.Grothendieck.compAsSmallFunctorEquivalenceFunctor_obj_fiber 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C CategoryTheory.Cat) (X : CategoryTheory.Grothendieck (F.comp CategoryTheory.Cat.asSmallFunctor)) : ((CategoryTheory.Grothendieck.compAsSmallFunctorEquivalenceFunctor F).obj X).fiber = CategoryTheory.AsSmall.down.obj X.fiber
• CategoryTheory.Grothendieck.pre_map_base 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] (F : CategoryTheory.Functor C CategoryTheory.Cat) (G : CategoryTheory.Functor D C) {X✝ Y✝ : CategoryTheory.Grothendieck (G.comp F)} (f : X✝ ⟶ Y✝) : ((CategoryTheory.Grothendieck.pre F G).map f).base = G.map f.base
• CategoryTheory.Grothendieck.map_map_base 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F G : CategoryTheory.Functor C CategoryTheory.Cat} (α : F ⟶ G) {X Y : CategoryTheory.Grothendieck F} (f : X ⟶ Y) : ((CategoryTheory.Grothendieck.map α).map f).base = f.base
• CategoryTheory.Grothendieck.compAsSmallFunctorEquivalenceInverse_map_base 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C CategoryTheory.Cat) {X✝ Y✝ : CategoryTheory.Grothendieck F} (f : X✝ ⟶ Y✝) : ((CategoryTheory.Grothendieck.compAsSmallFunctorEquivalenceInverse F).map f).base = f.base
• CategoryTheory.Grothendieck.id_fiber 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} (X : CategoryTheory.Grothendieck F) : (CategoryTheory.CategoryStruct.id X).fiber = CategoryTheory.eqToHom ⋯
• CategoryTheory.Grothendieck.fiber_eqToHom 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} {X Y : CategoryTheory.Grothendieck F} (h : X = Y) : (CategoryTheory.eqToHom h).fiber = CategoryTheory.eqToHom ⋯
• CategoryTheory.Grothendieck.isoMk_hom_fiber 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} {X Y : CategoryTheory.Grothendieck F} (e₁ : X.base ≅ Y.base) (e₂ : (F.map e₁.hom).toFunctor.obj X.fiber ≅ Y.fiber) : (CategoryTheory.Grothendieck.isoMk e₁ e₂).hom.fiber = e₂.hom
• CategoryTheory.Grothendieck.toTransport_fiber 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} (x : CategoryTheory.Grothendieck F) {c : C} (t : x.base ⟶ c) : (x.toTransport t).fiber = CategoryTheory.CategoryStruct.id ((F.map t).toFunctor.obj x.fiber)
• CategoryTheory.Grothendieck.transportIso_inv_fiber 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} (x : CategoryTheory.Grothendieck F) {c : C} (α : x.base ≅ c) : (x.transportIso α).inv.fiber = CategoryTheory.CategoryStruct.id ((F.map α.hom).toFunctor.obj x.fiber)
• CategoryTheory.Grothendieck.compAsSmallFunctorEquivalenceFunctor_map_base 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C CategoryTheory.Cat) {X✝ Y✝ : CategoryTheory.Grothendieck (F.comp CategoryTheory.Cat.asSmallFunctor)} (f : X✝ ⟶ Y✝) : ((CategoryTheory.Grothendieck.compAsSmallFunctorEquivalenceFunctor F).map f).base = f.base
• CategoryTheory.Grothendieck.ι_map 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C CategoryTheory.Cat) (c : C) {X✝ Y✝ : ↑(F.obj c)} (f : X✝ ⟶ Y✝) : (CategoryTheory.Grothendieck.ι F c).map f = { base := CategoryTheory.CategoryStruct.id { base := c, fiber := X✝ }.base, fiber := CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) f }
• CategoryTheory.Grothendieck.pre_map_fiber 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] (F : CategoryTheory.Functor C CategoryTheory.Cat) (G : CategoryTheory.Functor D C) {X✝ Y✝ : CategoryTheory.Grothendieck (G.comp F)} (f : X✝ ⟶ Y✝) : ((CategoryTheory.Grothendieck.pre F G).map f).fiber = f.fiber
• CategoryTheory.Grothendieck.transportIso_hom_fiber 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} (x : CategoryTheory.Grothendieck F) {c : C} (α : x.base ≅ c) : (x.transportIso α).hom.fiber = CategoryTheory.eqToHom ⋯
• CategoryTheory.Grothendieck.ιCompMap_hom_app_base 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F F' : CategoryTheory.Functor C CategoryTheory.Cat} (α : F ⟶ F') (c : C) (X : ↑(F.obj c)) : ((CategoryTheory.Grothendieck.ιCompMap α c).hom.app X).base = CategoryTheory.CategoryStruct.id c
• CategoryTheory.Grothendieck.ιCompMap_inv_app_base 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F F' : CategoryTheory.Functor C CategoryTheory.Cat} (α : F ⟶ F') (c : C) (X : ↑(F.obj c)) : ((CategoryTheory.Grothendieck.ιCompMap α c).inv.app X).base = CategoryTheory.CategoryStruct.id c
• CategoryTheory.Grothendieck.ext 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} {X Y : CategoryTheory.Grothendieck F} (f g : X.Hom Y) (w_base : f.base = g.base) (w_fiber : CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) f.fiber = g.fiber) : f = g
• CategoryTheory.Grothendieck.congr 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} {X Y : CategoryTheory.Grothendieck F} {f g : X ⟶ Y} (h : f = g) : f.fiber = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) g.fiber
• CategoryTheory.Grothendieck.grothendieckTypeToCat_unitIso_hom_app_base 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] (G : CategoryTheory.Functor C (Type w)) (X : CategoryTheory.Grothendieck (G.comp CategoryTheory.typeToCat)) : ((CategoryTheory.Grothendieck.grothendieckTypeToCat G).unitIso.hom.app X).base = CategoryTheory.CategoryStruct.id X.base
• CategoryTheory.Grothendieck.grothendieckTypeToCat_unitIso_inv_app_base 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] (G : CategoryTheory.Functor C (Type w)) (X : CategoryTheory.Grothendieck (G.comp CategoryTheory.typeToCat)) : ((CategoryTheory.Grothendieck.grothendieckTypeToCat G).unitIso.inv.app X).base = CategoryTheory.CategoryStruct.id X.base
• CategoryTheory.Grothendieck.isoMk_inv_fiber 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} {X Y : CategoryTheory.Grothendieck F} (e₁ : X.base ≅ Y.base) (e₂ : (F.map e₁.hom).toFunctor.obj X.fiber ≅ Y.fiber) : (CategoryTheory.Grothendieck.isoMk e₁ e₂).inv.fiber = CategoryTheory.CategoryStruct.comp ((F.map e₁.inv).toFunctor.map e₂.inv) (CategoryTheory.eqToHom ⋯)
• CategoryTheory.Grothendieck.grothendieckTypeToCatFunctor_map_coe 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] (G : CategoryTheory.Functor C (Type w)) {X✝ Y✝ : CategoryTheory.Grothendieck (G.comp CategoryTheory.typeToCat)} (f : X✝ ⟶ Y✝) : ↑((CategoryTheory.Grothendieck.grothendieckTypeToCatFunctor G).map f) = f.base
• CategoryTheory.Grothendieck.grothendieckTypeToCat_functor_map_coe 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] (G : CategoryTheory.Functor C (Type w)) {X✝ Y✝ : CategoryTheory.Grothendieck (G.comp CategoryTheory.typeToCat)} (f : X✝ ⟶ Y✝) : ↑((CategoryTheory.Grothendieck.grothendieckTypeToCat G).functor.map f) = f.base
• CategoryTheory.Grothendieck.comp_fiber 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} {X Y Z : CategoryTheory.Grothendieck F} (f : X ⟶ Y) (g : Y ⟶ Z) : (CategoryTheory.CategoryStruct.comp f g).fiber = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp ((F.map g.base).toFunctor.map f.fiber) g.fiber)
• CategoryTheory.Grothendieck.functorFrom_obj 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} {E : Type u_1} [CategoryTheory.Category.{v_1, u_1} E] (fib : (c : C) → CategoryTheory.Functor (↑(F.obj c)) E) (hom : {c c' : C} → (f : c ⟶ c') → fib c ⟶ (F.map f).toFunctor.comp (fib c')) (hom_id : ∀ (c : C), hom (CategoryTheory.CategoryStruct.id c) = CategoryTheory.eqToHom ⋯) (hom_comp : ∀ (c₁ c₂ c₃ : C) (f : c₁ ⟶ c₂) (g : c₂ ⟶ c₃), hom (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (hom f) (CategoryTheory.CategoryStruct.comp ((F.map f).toFunctor.whiskerLeft (hom g)) (CategoryTheory.eqToHom ⋯))) (X : CategoryTheory.Grothendieck F) : (CategoryTheory.Grothendieck.functorFrom fib hom hom_id hom_comp).obj X = (fib X.base).obj X.fiber
• CategoryTheory.Grothendieck.map_map 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F G : CategoryTheory.Functor C CategoryTheory.Cat} {α : F ⟶ G} {X Y : CategoryTheory.Grothendieck F} {f : X ⟶ Y} : (CategoryTheory.Grothendieck.map α).map f = { base := f.base, fiber := CategoryTheory.CategoryStruct.comp ((CategoryTheory.eqToHom ⋯).toNatTrans.app X.fiber) ((α.app Y.base).toFunctor.map f.fiber) }
• CategoryTheory.Grothendieck.functorFrom_map 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} {E : Type u_1} [CategoryTheory.Category.{v_1, u_1} E] (fib : (c : C) → CategoryTheory.Functor (↑(F.obj c)) E) (hom : {c c' : C} → (f : c ⟶ c') → fib c ⟶ (F.map f).toFunctor.comp (fib c')) (hom_id : ∀ (c : C), hom (CategoryTheory.CategoryStruct.id c) = CategoryTheory.eqToHom ⋯) (hom_comp : ∀ (c₁ c₂ c₃ : C) (f : c₁ ⟶ c₂) (g : c₂ ⟶ c₃), hom (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (hom f) (CategoryTheory.CategoryStruct.comp ((F.map f).toFunctor.whiskerLeft (hom g)) (CategoryTheory.eqToHom ⋯))) {X Y : CategoryTheory.Grothendieck F} (f : X ⟶ Y) : (CategoryTheory.Grothendieck.functorFrom fib hom hom_id hom_comp).map f = CategoryTheory.CategoryStruct.comp ((hom f.base).app X.fiber) ((fib Y.base).map f.fiber)
• CategoryTheory.Grothendieck.ιCompMap_hom_app_fiber 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F F' : CategoryTheory.Functor C CategoryTheory.Cat} (α : F ⟶ F') (c : C) (X : ↑(F.obj c)) : ((CategoryTheory.Grothendieck.ιCompMap α c).hom.app X).fiber = CategoryTheory.eqToHom ⋯
• CategoryTheory.Grothendieck.ιCompMap_inv_app_fiber 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F F' : CategoryTheory.Functor C CategoryTheory.Cat} (α : F ⟶ F') (c : C) (X : ↑(F.obj c)) : ((CategoryTheory.Grothendieck.ιCompMap α c).inv.app X).fiber = CategoryTheory.eqToHom ⋯
• CategoryTheory.Grothendieck.ιNatTrans_app_fiber 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} {X Y : C} (f : X ⟶ Y) (d : ↑(F.obj X)) : ((CategoryTheory.Grothendieck.ιNatTrans f).app d).fiber = CategoryTheory.CategoryStruct.id ((F.map f).toFunctor.obj ((CategoryTheory.Grothendieck.ι F X).obj d).fiber)
• CategoryTheory.Grothendieck.grothendieckTypeToCat_unitIso_hom_app_fiber 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] (G : CategoryTheory.Functor C (Type w)) (X : CategoryTheory.Grothendieck (G.comp CategoryTheory.typeToCat)) : ((CategoryTheory.Grothendieck.grothendieckTypeToCat G).unitIso.hom.app X).fiber = CategoryTheory.eqToHom ⋯
• CategoryTheory.Grothendieck.grothendieckTypeToCat_unitIso_inv_app_fiber 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] (G : CategoryTheory.Functor C (Type w)) (X : CategoryTheory.Grothendieck (G.comp CategoryTheory.typeToCat)) : ((CategoryTheory.Grothendieck.grothendieckTypeToCat G).unitIso.inv.app X).fiber = CategoryTheory.eqToHom ⋯
• CategoryTheory.Grothendieck.map_map_fiber 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F G : CategoryTheory.Functor C CategoryTheory.Cat} (α : F ⟶ G) {X Y : CategoryTheory.Grothendieck F} (f : X ⟶ Y) : ((CategoryTheory.Grothendieck.map α).map f).fiber = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) ((α.app Y.base).toFunctor.map f.fiber)
• CategoryTheory.Grothendieck.compAsSmallFunctorEquivalenceFunctor_map_fiber 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C CategoryTheory.Cat) {X✝ Y✝ : CategoryTheory.Grothendieck (F.comp CategoryTheory.Cat.asSmallFunctor)} (f : X✝ ⟶ Y✝) : ((CategoryTheory.Grothendieck.compAsSmallFunctorEquivalenceFunctor F).map f).fiber = CategoryTheory.AsSmall.down.map f.fiber
• CategoryTheory.Grothendieck.compAsSmallFunctorEquivalenceInverse_map_fiber 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C CategoryTheory.Cat) {X✝ Y✝ : CategoryTheory.Grothendieck F} (f : X✝ ⟶ Y✝) : ((CategoryTheory.Grothendieck.compAsSmallFunctorEquivalenceInverse F).map f).fiber = CategoryTheory.AsSmall.up.map f.fiber
• CategoryTheory.Limits.natTransIntoForgetCompFiberwiseColimit_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Grothendieck
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} {H : Type u₂} [CategoryTheory.Category.{v₂, u₂} H] (G : CategoryTheory.Functor (CategoryTheory.Grothendieck F) H) [∀ {X Y : C} (f : X ⟶ Y), CategoryTheory.Limits.HasColimit ((F.map f).toFunctor.comp ((CategoryTheory.Grothendieck.ι F Y).comp G))] (X : CategoryTheory.Grothendieck F) : (CategoryTheory.Limits.natTransIntoForgetCompFiberwiseColimit G).app X = CategoryTheory.Limits.colimit.ι ((CategoryTheory.Grothendieck.ι F X.base).comp G) X.fiber
• CategoryTheory.Limits.ι_colimitFiberwiseColimitIso_inv 📋 Mathlib.CategoryTheory.Limits.Shapes.Grothendieck
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} {H : Type u₂} [CategoryTheory.Category.{v₂, u₂} H] (G : CategoryTheory.Functor (CategoryTheory.Grothendieck F) H) [∀ {X Y : C} (f : X ⟶ Y), CategoryTheory.Limits.HasColimit ((F.map f).toFunctor.comp ((CategoryTheory.Grothendieck.ι F Y).comp G))] [CategoryTheory.Limits.HasColimit (CategoryTheory.Limits.fiberwiseColimit G)] (X : CategoryTheory.Grothendieck F) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι G X) (CategoryTheory.Limits.colimitFiberwiseColimitIso G).inv = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι ((CategoryTheory.Grothendieck.ι F X.base).comp G) X.fiber) (CategoryTheory.Limits.colimit.ι (CategoryTheory.Limits.fiberwiseColimit G) X.base)
• CategoryTheory.Limits.coconeOfCoconeFiberwiseColimit_ι_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Grothendieck
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} {H : Type u₂} [CategoryTheory.Category.{v₂, u₂} H] {G : CategoryTheory.Functor (CategoryTheory.Grothendieck F) H} [∀ {X Y : C} (f : X ⟶ Y), CategoryTheory.Limits.HasColimit ((F.map f).toFunctor.comp ((CategoryTheory.Grothendieck.ι F Y).comp G))] (c : CategoryTheory.Limits.Cocone (CategoryTheory.Limits.fiberwiseColimit G)) (X : CategoryTheory.Grothendieck F) : (CategoryTheory.Limits.coconeOfCoconeFiberwiseColimit c).ι.app X = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι ((CategoryTheory.Grothendieck.ι F X.base).comp G) X.fiber) (c.ι.app X.base)
• CategoryTheory.Limits.ι_colimitFiberwiseColimitIso_inv_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Grothendieck
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} {H : Type u₂} [CategoryTheory.Category.{v₂, u₂} H] (G : CategoryTheory.Functor (CategoryTheory.Grothendieck F) H) [∀ {X Y : C} (f : X ⟶ Y), CategoryTheory.Limits.HasColimit ((F.map f).toFunctor.comp ((CategoryTheory.Grothendieck.ι F Y).comp G))] [CategoryTheory.Limits.HasColimit (CategoryTheory.Limits.fiberwiseColimit G)] (X : CategoryTheory.Grothendieck F) {Z : H} (h : CategoryTheory.Limits.colimit (CategoryTheory.Limits.fiberwiseColimit G) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι G X) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimitFiberwiseColimitIso G).inv h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι ((CategoryTheory.Grothendieck.ι F X.base).comp G) X.fiber) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι (CategoryTheory.Limits.fiberwiseColimit G) X.base) h)
• CategoryTheory.CostructuredArrow.grothendieckProj_obj 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.Functor
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (L : CategoryTheory.Functor C D) (X : CategoryTheory.Grothendieck (CategoryTheory.CostructuredArrow.functor L)) : (CategoryTheory.CostructuredArrow.grothendieckProj L).obj X = CategoryTheory.CostructuredArrow.left X.fiber
• CategoryTheory.CostructuredArrow.commaToGrothendieckPrecompFunctor_obj_base 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.Functor
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (L : CategoryTheory.Functor C D) (R : CategoryTheory.Functor E D) (X : CategoryTheory.Comma L R) : ((CategoryTheory.CostructuredArrow.commaToGrothendieckPrecompFunctor L R).obj X).base = X.right
• CategoryTheory.CostructuredArrow.grothendieckPrecompFunctorToComma_obj_right 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.Functor
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (L : CategoryTheory.Functor C D) (R : CategoryTheory.Functor E D) (P : CategoryTheory.Grothendieck (R.comp (CategoryTheory.CostructuredArrow.functor L))) : ((CategoryTheory.CostructuredArrow.grothendieckPrecompFunctorToComma L R).obj P).right = P.base
• CategoryTheory.CostructuredArrow.grothendieckPrecompFunctorToComma_obj_left 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.Functor
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (L : CategoryTheory.Functor C D) (R : CategoryTheory.Functor E D) (P : CategoryTheory.Grothendieck (R.comp (CategoryTheory.CostructuredArrow.functor L))) : ((CategoryTheory.CostructuredArrow.grothendieckPrecompFunctorToComma L R).obj P).left = CategoryTheory.CostructuredArrow.left P.fiber
• CategoryTheory.CostructuredArrow.grothendieckPrecompFunctorToComma_obj_hom 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.Functor
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (L : CategoryTheory.Functor C D) (R : CategoryTheory.Functor E D) (P : CategoryTheory.Grothendieck (R.comp (CategoryTheory.CostructuredArrow.functor L))) : ((CategoryTheory.CostructuredArrow.grothendieckPrecompFunctorToComma L R).obj P).hom = CategoryTheory.CostructuredArrow.hom P.fiber
• CategoryTheory.CostructuredArrow.grothendieckPrecompFunctorToComma_map_right 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.Functor
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (L : CategoryTheory.Functor C D) (R : CategoryTheory.Functor E D) {X✝ Y✝ : CategoryTheory.Grothendieck (R.comp (CategoryTheory.CostructuredArrow.functor L))} (f : X✝ ⟶ Y✝) : ((CategoryTheory.CostructuredArrow.grothendieckPrecompFunctorToComma L R).map f).right = f.base
• CategoryTheory.CostructuredArrow.grothendieckProj_map 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.Functor
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (L : CategoryTheory.Functor C D) {X✝ Y✝ : CategoryTheory.Grothendieck (CategoryTheory.CostructuredArrow.functor L)} (f : X✝ ⟶ Y✝) : (CategoryTheory.CostructuredArrow.grothendieckProj L).map f = f.fiber.left
• CategoryTheory.CostructuredArrow.grothendieckPrecompFunctorToComma_map_left 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.Functor
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (L : CategoryTheory.Functor C D) (R : CategoryTheory.Functor E D) {X✝ Y✝ : CategoryTheory.Grothendieck (R.comp (CategoryTheory.CostructuredArrow.functor L))} (f : X✝ ⟶ Y✝) : ((CategoryTheory.CostructuredArrow.grothendieckPrecompFunctorToComma L R).map f).left = f.fiber.left
• CategoryTheory.CostructuredArrow.commaToGrothendieckPrecompFunctor_map_fiber 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.Functor
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (L : CategoryTheory.Functor C D) (R : CategoryTheory.Functor E D) {X✝ Y✝ : CategoryTheory.Comma L R} (f : X✝ ⟶ Y✝) : ((CategoryTheory.CostructuredArrow.commaToGrothendieckPrecompFunctor L R).map f).fiber = CategoryTheory.CostructuredArrow.homMk f.left ⋯
• CategoryTheory.Functor.ι_colimitIsoColimitGrothendieck_inv 📋 Mathlib.CategoryTheory.Functor.KanExtension.Adjunction
  {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) {H : Type u_3} [CategoryTheory.Category.{v_3, u_3} H] (G : CategoryTheory.Functor C H) [L.HasPointwiseLeftKanExtension G] [CategoryTheory.Limits.HasColimitsOfShape D H] [CategoryTheory.Limits.HasColimitsOfShape C H] (X : CategoryTheory.Grothendieck (CategoryTheory.CostructuredArrow.functor L)) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι ((CategoryTheory.CostructuredArrow.grothendieckProj L).comp G) X) (L.colimitIsoColimitGrothendieck G).inv = CategoryTheory.Limits.colimit.ι G ((CategoryTheory.CostructuredArrow.proj L X.base).obj X.fiber)
• CategoryTheory.Functor.ι_colimitIsoColimitGrothendieck_inv_assoc 📋 Mathlib.CategoryTheory.Functor.KanExtension.Adjunction
  {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) {H : Type u_3} [CategoryTheory.Category.{v_3, u_3} H] (G : CategoryTheory.Functor C H) [L.HasPointwiseLeftKanExtension G] [CategoryTheory.Limits.HasColimitsOfShape D H] [CategoryTheory.Limits.HasColimitsOfShape C H] (X : CategoryTheory.Grothendieck (CategoryTheory.CostructuredArrow.functor L)) {Z : H} (h : CategoryTheory.Limits.colimit G ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι ((CategoryTheory.CostructuredArrow.grothendieckProj L).comp G) X) (CategoryTheory.CategoryStruct.comp (L.colimitIsoColimitGrothendieck G).inv h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι G ((CategoryTheory.CostructuredArrow.proj L X.base).obj X.fiber)) h

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