Loogle!

Result

Found 56 declarations mentioning CategoryTheory.GrothendieckTopology.plusObj.

• CategoryTheory.GrothendieckTopology.plusObj 📋 Mathlib.CategoryTheory.Sites.Plus
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w} [CategoryTheory.Category.{w', w} D] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] (P : CategoryTheory.Functor Cᵒᵖ D) [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] : CategoryTheory.Functor Cᵒᵖ D
• CategoryTheory.GrothendieckTopology.isoToPlus 📋 Mathlib.CategoryTheory.Sites.Plus
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w} [CategoryTheory.Category.{w', w} D] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] (P : CategoryTheory.Functor Cᵒᵖ D) [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] (hP : CategoryTheory.Presheaf.IsSheaf J P) : P ≅ J.plusObj P
• CategoryTheory.GrothendieckTopology.isIso_toPlus_of_isSheaf 📋 Mathlib.CategoryTheory.Sites.Plus
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w} [CategoryTheory.Category.{w', w} D] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] (P : CategoryTheory.Functor Cᵒᵖ D) [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] (hP : CategoryTheory.Presheaf.IsSheaf J P) : CategoryTheory.IsIso (J.toPlus P)
• CategoryTheory.GrothendieckTopology.toPlus 📋 Mathlib.CategoryTheory.Sites.Plus
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w} [CategoryTheory.Category.{w', w} D] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] (P : CategoryTheory.Functor Cᵒᵖ D) [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] : P ⟶ J.plusObj P
• CategoryTheory.GrothendieckTopology.plusFunctor_obj 📋 Mathlib.CategoryTheory.Sites.Plus
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) (D : Type w) [CategoryTheory.Category.{w', w} D] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] (P : CategoryTheory.Functor Cᵒᵖ D) : (J.plusFunctor D).obj P = J.plusObj P
• CategoryTheory.GrothendieckTopology.plusLift 📋 Mathlib.CategoryTheory.Sites.Plus
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w} [CategoryTheory.Category.{w', w} D] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] {P Q : CategoryTheory.Functor Cᵒᵖ D} (η : P ⟶ Q) (hQ : CategoryTheory.Presheaf.IsSheaf J Q) : J.plusObj P ⟶ Q
• CategoryTheory.GrothendieckTopology.plusMap 📋 Mathlib.CategoryTheory.Sites.Plus
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w} [CategoryTheory.Category.{w', w} D] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] {P Q : CategoryTheory.Functor Cᵒᵖ D} (η : P ⟶ Q) : J.plusObj P ⟶ J.plusObj Q
• CategoryTheory.GrothendieckTopology.isoToPlus_hom 📋 Mathlib.CategoryTheory.Sites.Plus
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w} [CategoryTheory.Category.{w', w} D] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] (P : CategoryTheory.Functor Cᵒᵖ D) [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] (hP : CategoryTheory.Presheaf.IsSheaf J P) : (J.isoToPlus P hP).hom = J.toPlus P
• CategoryTheory.GrothendieckTopology.plusMap_toPlus 📋 Mathlib.CategoryTheory.Sites.Plus
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w} [CategoryTheory.Category.{w', w} D] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] (P : CategoryTheory.Functor Cᵒᵖ D) [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] : J.plusMap (J.toPlus P) = J.toPlus (J.plusObj P)
• CategoryTheory.GrothendieckTopology.toPlusNatTrans_app 📋 Mathlib.CategoryTheory.Sites.Plus
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) (D : Type w) [CategoryTheory.Category.{w', w} D] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] (P : CategoryTheory.Functor Cᵒᵖ D) : (J.toPlusNatTrans D).app P = J.toPlus P
• CategoryTheory.GrothendieckTopology.plusMap_id 📋 Mathlib.CategoryTheory.Sites.Plus
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w} [CategoryTheory.Category.{w', w} D] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] (P : CategoryTheory.Functor Cᵒᵖ D) : J.plusMap (CategoryTheory.CategoryStruct.id P) = CategoryTheory.CategoryStruct.id (J.plusObj P)
• CategoryTheory.GrothendieckTopology.isoToPlus_inv 📋 Mathlib.CategoryTheory.Sites.Plus
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w} [CategoryTheory.Category.{w', w} D] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] (P : CategoryTheory.Functor Cᵒᵖ D) [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] (hP : CategoryTheory.Presheaf.IsSheaf J P) : (J.isoToPlus P hP).inv = J.plusLift (CategoryTheory.CategoryStruct.id P) hP
• CategoryTheory.GrothendieckTopology.toPlus_plusLift 📋 Mathlib.CategoryTheory.Sites.Plus
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w} [CategoryTheory.Category.{w', w} D] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] {P Q : CategoryTheory.Functor Cᵒᵖ D} (η : P ⟶ Q) (hQ : CategoryTheory.Presheaf.IsSheaf J Q) : CategoryTheory.CategoryStruct.comp (J.toPlus P) (J.plusLift η hQ) = η
• CategoryTheory.GrothendieckTopology.plusFunctor_map 📋 Mathlib.CategoryTheory.Sites.Plus
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) (D : Type w) [CategoryTheory.Category.{w', w} D] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] {X✝ Y✝ : CategoryTheory.Functor Cᵒᵖ D} (η : X✝ ⟶ Y✝) : (J.plusFunctor D).map η = J.plusMap η
• CategoryTheory.GrothendieckTopology.toPlus_naturality 📋 Mathlib.CategoryTheory.Sites.Plus
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w} [CategoryTheory.Category.{w', w} D] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] {P Q : CategoryTheory.Functor Cᵒᵖ D} (η : P ⟶ Q) : CategoryTheory.CategoryStruct.comp η (J.toPlus Q) = CategoryTheory.CategoryStruct.comp (J.toPlus P) (J.plusMap η)
• CategoryTheory.GrothendieckTopology.plusLift_unique 📋 Mathlib.CategoryTheory.Sites.Plus
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w} [CategoryTheory.Category.{w', w} D] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] {P Q : CategoryTheory.Functor Cᵒᵖ D} (η : P ⟶ Q) (hQ : CategoryTheory.Presheaf.IsSheaf J Q) (γ : J.plusObj P ⟶ Q) (hγ : CategoryTheory.CategoryStruct.comp (J.toPlus P) γ = η) : γ = J.plusLift η hQ
• CategoryTheory.GrothendieckTopology.plusMap_plusLift 📋 Mathlib.CategoryTheory.Sites.Plus
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w} [CategoryTheory.Category.{w', w} D] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] {P Q R : CategoryTheory.Functor Cᵒᵖ D} (η : P ⟶ Q) (γ : Q ⟶ R) (hR : CategoryTheory.Presheaf.IsSheaf J R) : CategoryTheory.CategoryStruct.comp (J.plusMap η) (J.plusLift γ hR) = J.plusLift (CategoryTheory.CategoryStruct.comp η γ) hR
• CategoryTheory.GrothendieckTopology.plusMap_comp 📋 Mathlib.CategoryTheory.Sites.Plus
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w} [CategoryTheory.Category.{w', w} D] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] {P Q R : CategoryTheory.Functor Cᵒᵖ D} (η : P ⟶ Q) (γ : Q ⟶ R) : J.plusMap (CategoryTheory.CategoryStruct.comp η γ) = CategoryTheory.CategoryStruct.comp (J.plusMap η) (J.plusMap γ)
• CategoryTheory.GrothendieckTopology.toPlus_plusLift_assoc 📋 Mathlib.CategoryTheory.Sites.Plus
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w} [CategoryTheory.Category.{w', w} D] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] {P Q : CategoryTheory.Functor Cᵒᵖ D} (η : P ⟶ Q) (hQ : CategoryTheory.Presheaf.IsSheaf J Q) {Z : CategoryTheory.Functor Cᵒᵖ D} (h : Q ⟶ Z) : CategoryTheory.CategoryStruct.comp (J.toPlus P) (CategoryTheory.CategoryStruct.comp (J.plusLift η hQ) h) = CategoryTheory.CategoryStruct.comp η h
• CategoryTheory.GrothendieckTopology.plus_hom_ext 📋 Mathlib.CategoryTheory.Sites.Plus
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w} [CategoryTheory.Category.{w', w} D] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] {P Q : CategoryTheory.Functor Cᵒᵖ D} (η γ : J.plusObj P ⟶ Q) (hQ : CategoryTheory.Presheaf.IsSheaf J Q) (h : CategoryTheory.CategoryStruct.comp (J.toPlus P) η = CategoryTheory.CategoryStruct.comp (J.toPlus P) γ) : η = γ
• CategoryTheory.GrothendieckTopology.plusMap_zero 📋 Mathlib.CategoryTheory.Sites.Plus
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w} [CategoryTheory.Category.{w', w} D] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] [CategoryTheory.Preadditive D] (P Q : CategoryTheory.Functor Cᵒᵖ D) : J.plusMap 0 = 0
• CategoryTheory.GrothendieckTopology.toPlus_naturality_assoc 📋 Mathlib.CategoryTheory.Sites.Plus
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w} [CategoryTheory.Category.{w', w} D] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] {P Q : CategoryTheory.Functor Cᵒᵖ D} (η : P ⟶ Q) {Z : CategoryTheory.Functor Cᵒᵖ D} (h : J.plusObj Q ⟶ Z) : CategoryTheory.CategoryStruct.comp η (CategoryTheory.CategoryStruct.comp (J.toPlus Q) h) = CategoryTheory.CategoryStruct.comp (J.toPlus P) (CategoryTheory.CategoryStruct.comp (J.plusMap η) h)
• CategoryTheory.GrothendieckTopology.plusMap_comp_assoc 📋 Mathlib.CategoryTheory.Sites.Plus
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w} [CategoryTheory.Category.{w', w} D] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] {P Q R : CategoryTheory.Functor Cᵒᵖ D} (η : P ⟶ Q) (γ : Q ⟶ R) {Z : CategoryTheory.Functor Cᵒᵖ D} (h : J.plusObj R ⟶ Z) : CategoryTheory.CategoryStruct.comp (J.plusMap (CategoryTheory.CategoryStruct.comp η γ)) h = CategoryTheory.CategoryStruct.comp (J.plusMap η) (CategoryTheory.CategoryStruct.comp (J.plusMap γ) h)
• CategoryTheory.GrothendieckTopology.Plus.mk 📋 Mathlib.CategoryTheory.Sites.ConcreteSheafification
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w} [CategoryTheory.Category.{w', w} D] {FD : D → D → Type u_1} {CD : D → Type t} [(X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] [instCC : CategoryTheory.ConcreteCategory D FD] [∀ {X : C} (S : J.Cover X), CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan S.shape) (CategoryTheory.forget D)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] {X : C} {P : CategoryTheory.Functor Cᵒᵖ D} {S : J.Cover X} (x : CategoryTheory.Meq P S) : CategoryTheory.ToType ((J.plusObj P).obj (Opposite.op X))
• CategoryTheory.GrothendieckTopology.Plus.isSheaf_plus_plus 📋 Mathlib.CategoryTheory.Sites.ConcreteSheafification
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w} [CategoryTheory.Category.{w', w} D] {FD : D → D → Type u_1} {CD : D → Type t} [(X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] [instCC : CategoryTheory.ConcreteCategory D FD] [∀ {X : C} (S : J.Cover X), CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan S.shape) (CategoryTheory.forget D)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (CategoryTheory.forget D)] [(CategoryTheory.forget D).ReflectsIsomorphisms] (P : CategoryTheory.Functor Cᵒᵖ D) : CategoryTheory.Presheaf.IsSheaf J (J.plusObj (J.plusObj P))
• CategoryTheory.GrothendieckTopology.Plus.exists_rep 📋 Mathlib.CategoryTheory.Sites.ConcreteSheafification
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w} [CategoryTheory.Category.{w', w} D] {FD : D → D → Type u_1} {CD : D → Type t} [(X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] [instCC : CategoryTheory.ConcreteCategory D FD] [∀ {X : C} (S : J.Cover X), CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan S.shape) (CategoryTheory.forget D)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (CategoryTheory.forget D)] {X : C} {P : CategoryTheory.Functor Cᵒᵖ D} (x : CategoryTheory.ToType ((J.plusObj P).obj (Opposite.op X))) : ∃ S y, x = CategoryTheory.GrothendieckTopology.Plus.mk y
• CategoryTheory.GrothendieckTopology.Plus.toPlus_mk 📋 Mathlib.CategoryTheory.Sites.ConcreteSheafification
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w} [CategoryTheory.Category.{w', w} D] {FD : D → D → Type u_1} {CD : D → Type t} [(X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] [instCC : CategoryTheory.ConcreteCategory D FD] [∀ {X : C} (S : J.Cover X), CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan S.shape) (CategoryTheory.forget D)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] {X : C} {P : CategoryTheory.Functor Cᵒᵖ D} (S : J.Cover X) (x : CategoryTheory.ToType (P.obj (Opposite.op X))) : (CategoryTheory.ConcreteCategory.hom ((J.toPlus P).app (Opposite.op X))) x = CategoryTheory.GrothendieckTopology.Plus.mk (CategoryTheory.Meq.mk S x)
• CategoryTheory.GrothendieckTopology.Plus.toPlus_eq_mk 📋 Mathlib.CategoryTheory.Sites.ConcreteSheafification
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w} [CategoryTheory.Category.{w', w} D] {FD : D → D → Type u_1} {CD : D → Type t} [(X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] [instCC : CategoryTheory.ConcreteCategory D FD] [∀ {X : C} (S : J.Cover X), CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan S.shape) (CategoryTheory.forget D)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] {X : C} {P : CategoryTheory.Functor Cᵒᵖ D} (x : CategoryTheory.ToType (P.obj (Opposite.op X))) : (CategoryTheory.ConcreteCategory.hom ((J.toPlus P).app (Opposite.op X))) x = CategoryTheory.GrothendieckTopology.Plus.mk (CategoryTheory.Meq.mk ⊤ x)
• CategoryTheory.GrothendieckTopology.Plus.eq_mk_iff_exists 📋 Mathlib.CategoryTheory.Sites.ConcreteSheafification
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w} [CategoryTheory.Category.{w', w} D] {FD : D → D → Type u_1} {CD : D → Type t} [(X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] [instCC : CategoryTheory.ConcreteCategory D FD] [∀ {X : C} (S : J.Cover X), CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan S.shape) (CategoryTheory.forget D)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (CategoryTheory.forget D)] {X : C} {P : CategoryTheory.Functor Cᵒᵖ D} {S T : J.Cover X} (x : CategoryTheory.Meq P S) (y : CategoryTheory.Meq P T) : CategoryTheory.GrothendieckTopology.Plus.mk x = CategoryTheory.GrothendieckTopology.Plus.mk y ↔ ∃ W h1 h2, x.refine h1 = y.refine h2
• CategoryTheory.GrothendieckTopology.Plus.res_mk_eq_mk_pullback 📋 Mathlib.CategoryTheory.Sites.ConcreteSheafification
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w} [CategoryTheory.Category.{w', w} D] {FD : D → D → Type u_1} {CD : D → Type t} [(X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] [instCC : CategoryTheory.ConcreteCategory D FD] [∀ {X : C} (S : J.Cover X), CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan S.shape) (CategoryTheory.forget D)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] {Y X : C} {P : CategoryTheory.Functor Cᵒᵖ D} {S : J.Cover X} (x : CategoryTheory.Meq P S) (f : Y ⟶ X) : (CategoryTheory.ConcreteCategory.hom ((J.plusObj P).map f.op)) (CategoryTheory.GrothendieckTopology.Plus.mk x) = CategoryTheory.GrothendieckTopology.Plus.mk (x.pullback f)
• CategoryTheory.GrothendieckTopology.Plus.isSheaf_of_sep 📋 Mathlib.CategoryTheory.Sites.ConcreteSheafification
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w} [CategoryTheory.Category.{w', w} D] {FD : D → D → Type u_1} {CD : D → Type t} [(X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] [instCC : CategoryTheory.ConcreteCategory D FD] [∀ {X : C} (S : J.Cover X), CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan S.shape) (CategoryTheory.forget D)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (CategoryTheory.forget D)] [(CategoryTheory.forget D).ReflectsIsomorphisms] (P : CategoryTheory.Functor Cᵒᵖ D) (hsep : ∀ (X : C) (S : J.Cover X) (x y : CategoryTheory.ToType (P.obj (Opposite.op X))), (∀ (I : S.Arrow), (CategoryTheory.ConcreteCategory.hom (P.map I.f.op)) x = (CategoryTheory.ConcreteCategory.hom (P.map I.f.op)) y) → x = y) : CategoryTheory.Presheaf.IsSheaf J (J.plusObj P)
• CategoryTheory.GrothendieckTopology.Plus.exists_of_sep 📋 Mathlib.CategoryTheory.Sites.ConcreteSheafification
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w} [CategoryTheory.Category.{w', w} D] {FD : D → D → Type u_1} {CD : D → Type t} [(X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] [instCC : CategoryTheory.ConcreteCategory D FD] [∀ {X : C} (S : J.Cover X), CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan S.shape) (CategoryTheory.forget D)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (CategoryTheory.forget D)] (P : CategoryTheory.Functor Cᵒᵖ D) (hsep : ∀ (X : C) (S : J.Cover X) (x y : CategoryTheory.ToType (P.obj (Opposite.op X))), (∀ (I : S.Arrow), (CategoryTheory.ConcreteCategory.hom (P.map I.f.op)) x = (CategoryTheory.ConcreteCategory.hom (P.map I.f.op)) y) → x = y) (X : C) (S : J.Cover X) (s : CategoryTheory.Meq (J.plusObj P) S) : ∃ t, CategoryTheory.Meq.mk S t = s
• CategoryTheory.GrothendieckTopology.Plus.sep 📋 Mathlib.CategoryTheory.Sites.ConcreteSheafification
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w} [CategoryTheory.Category.{w', w} D] {FD : D → D → Type u_1} {CD : D → Type t} [(X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] [instCC : CategoryTheory.ConcreteCategory D FD] [∀ {X : C} (S : J.Cover X), CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan S.shape) (CategoryTheory.forget D)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (CategoryTheory.forget D)] {X : C} (P : CategoryTheory.Functor Cᵒᵖ D) (S : J.Cover X) (x y : CategoryTheory.ToType ((J.plusObj P).obj (Opposite.op X))) (h : ∀ (I : S.Arrow), (CategoryTheory.ConcreteCategory.hom ((J.plusObj P).map I.f.op)) x = (CategoryTheory.ConcreteCategory.hom ((J.plusObj P).map I.f.op)) y) : x = y
• CategoryTheory.GrothendieckTopology.Plus.inj_of_sep 📋 Mathlib.CategoryTheory.Sites.ConcreteSheafification
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w} [CategoryTheory.Category.{w', w} D] {FD : D → D → Type u_1} {CD : D → Type t} [(X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] [instCC : CategoryTheory.ConcreteCategory D FD] [∀ {X : C} (S : J.Cover X), CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan S.shape) (CategoryTheory.forget D)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (CategoryTheory.forget D)] (P : CategoryTheory.Functor Cᵒᵖ D) (hsep : ∀ (X : C) (S : J.Cover X) (x y : CategoryTheory.ToType (P.obj (Opposite.op X))), (∀ (I : S.Arrow), (CategoryTheory.ConcreteCategory.hom (P.map I.f.op)) x = (CategoryTheory.ConcreteCategory.hom (P.map I.f.op)) y) → x = y) (X : C) : Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom ((J.toPlus P).app (Opposite.op X)))
• CategoryTheory.GrothendieckTopology.Plus.toPlus_apply 📋 Mathlib.CategoryTheory.Sites.ConcreteSheafification
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w} [CategoryTheory.Category.{w', w} D] {FD : D → D → Type u_1} {CD : D → Type t} [(X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] [instCC : CategoryTheory.ConcreteCategory D FD] [∀ {X : C} (S : J.Cover X), CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan S.shape) (CategoryTheory.forget D)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] {X : C} {P : CategoryTheory.Functor Cᵒᵖ D} (S : J.Cover X) (x : CategoryTheory.Meq P S) (I : S.Arrow) : (CategoryTheory.ConcreteCategory.hom ((J.toPlus P).app (Opposite.op I.Y))) (↑x I) = (CategoryTheory.ConcreteCategory.hom ((J.plusObj P).map I.f.op)) (CategoryTheory.GrothendieckTopology.Plus.mk x)
• CategoryTheory.GrothendieckTopology.Plus.meqOfSep 📋 Mathlib.CategoryTheory.Sites.ConcreteSheafification
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w} [CategoryTheory.Category.{w', w} D] {FD : D → D → Type u_1} {CD : D → Type t} [(X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] [instCC : CategoryTheory.ConcreteCategory D FD] [∀ {X : C} (S : J.Cover X), CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan S.shape) (CategoryTheory.forget D)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (CategoryTheory.forget D)] (P : CategoryTheory.Functor Cᵒᵖ D) (hsep : ∀ (X : C) (S : J.Cover X) (x y : CategoryTheory.ToType (P.obj (Opposite.op X))), (∀ (I : S.Arrow), (CategoryTheory.ConcreteCategory.hom (P.map I.f.op)) x = (CategoryTheory.ConcreteCategory.hom (P.map I.f.op)) y) → x = y) (X : C) (S : J.Cover X) (s : CategoryTheory.Meq (J.plusObj P) S) (T : (I : S.Arrow) → J.Cover I.Y) (t : (I : S.Arrow) → CategoryTheory.Meq P (T I)) (ht : ∀ (I : S.Arrow), ↑s I = CategoryTheory.GrothendieckTopology.Plus.mk (t I)) : CategoryTheory.Meq P (S.bind T)
• CategoryTheory.GrothendieckTopology.plusCompIso 📋 Mathlib.CategoryTheory.Sites.CompatiblePlus
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] {E : Type u_2} [CategoryTheory.Category.{v_2, u_2} E] (F : CategoryTheory.Functor D E) [∀ (J : CategoryTheory.Limits.MulticospanShape), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan J) D] [∀ (J : CategoryTheory.Limits.MulticospanShape), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan J) E] [∀ (X : C) (W : J.Cover X) (P : CategoryTheory.Functor Cᵒᵖ D), CategoryTheory.Limits.PreservesLimit (W.index P).multicospan F] (P : CategoryTheory.Functor Cᵒᵖ D) [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ E] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ F] : (J.plusObj P).comp F ≅ J.plusObj (P.comp F)
• CategoryTheory.GrothendieckTopology.plusFunctorWhiskerLeftIso 📋 Mathlib.CategoryTheory.Sites.CompatiblePlus
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] {E : Type u_2} [CategoryTheory.Category.{v_2, u_2} E] [∀ (J : CategoryTheory.Limits.MulticospanShape), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan J) D] [∀ (J : CategoryTheory.Limits.MulticospanShape), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan J) E] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ E] (P : CategoryTheory.Functor Cᵒᵖ D) [∀ (F : CategoryTheory.Functor D E) (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ F] [∀ (F : CategoryTheory.Functor D E) (X : C) (W : J.Cover X) (P : CategoryTheory.Functor Cᵒᵖ D), CategoryTheory.Limits.PreservesLimit (W.index P).multicospan F] : (CategoryTheory.Functor.whiskeringLeft Cᵒᵖ D E).obj (J.plusObj P) ≅ ((CategoryTheory.Functor.whiskeringLeft Cᵒᵖ D E).obj P).comp (J.plusFunctor E)
• CategoryTheory.GrothendieckTopology.toPlus_comp_plusCompIso_inv 📋 Mathlib.CategoryTheory.Sites.CompatiblePlus
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] {E : Type u_2} [CategoryTheory.Category.{v_2, u_2} E] (F : CategoryTheory.Functor D E) [∀ (J : CategoryTheory.Limits.MulticospanShape), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan J) D] [∀ (J : CategoryTheory.Limits.MulticospanShape), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan J) E] [∀ (X : C) (W : J.Cover X) (P : CategoryTheory.Functor Cᵒᵖ D), CategoryTheory.Limits.PreservesLimit (W.index P).multicospan F] (P : CategoryTheory.Functor Cᵒᵖ D) [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ E] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ F] : CategoryTheory.CategoryStruct.comp (J.toPlus (P.comp F)) (J.plusCompIso F P).inv = CategoryTheory.Functor.whiskerRight (J.toPlus P) F
• CategoryTheory.GrothendieckTopology.whiskerRight_toPlus_comp_plusCompIso_hom 📋 Mathlib.CategoryTheory.Sites.CompatiblePlus
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] {E : Type u_2} [CategoryTheory.Category.{v_2, u_2} E] (F : CategoryTheory.Functor D E) [∀ (J : CategoryTheory.Limits.MulticospanShape), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan J) D] [∀ (J : CategoryTheory.Limits.MulticospanShape), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan J) E] [∀ (X : C) (W : J.Cover X) (P : CategoryTheory.Functor Cᵒᵖ D), CategoryTheory.Limits.PreservesLimit (W.index P).multicospan F] (P : CategoryTheory.Functor Cᵒᵖ D) [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ E] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ F] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight (J.toPlus P) F) (J.plusCompIso F P).hom = J.toPlus (P.comp F)
• CategoryTheory.GrothendieckTopology.plusCompIso_inv_eq_plusLift 📋 Mathlib.CategoryTheory.Sites.CompatiblePlus
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] {E : Type u_2} [CategoryTheory.Category.{v_2, u_2} E] (F : CategoryTheory.Functor D E) [∀ (J : CategoryTheory.Limits.MulticospanShape), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan J) D] [∀ (J : CategoryTheory.Limits.MulticospanShape), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan J) E] [∀ (X : C) (W : J.Cover X) (P : CategoryTheory.Functor Cᵒᵖ D), CategoryTheory.Limits.PreservesLimit (W.index P).multicospan F] (P : CategoryTheory.Functor Cᵒᵖ D) [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ E] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ F] (hP : CategoryTheory.Presheaf.IsSheaf J ((J.plusObj P).comp F)) : (J.plusCompIso F P).inv = J.plusLift (CategoryTheory.Functor.whiskerRight (J.toPlus P) F) hP
• CategoryTheory.GrothendieckTopology.whiskerRight_toPlus_comp_plusCompIso_hom_assoc 📋 Mathlib.CategoryTheory.Sites.CompatiblePlus
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] {E : Type u_2} [CategoryTheory.Category.{v_2, u_2} E] (F : CategoryTheory.Functor D E) [∀ (J : CategoryTheory.Limits.MulticospanShape), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan J) D] [∀ (J : CategoryTheory.Limits.MulticospanShape), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan J) E] [∀ (X : C) (W : J.Cover X) (P : CategoryTheory.Functor Cᵒᵖ D), CategoryTheory.Limits.PreservesLimit (W.index P).multicospan F] (P : CategoryTheory.Functor Cᵒᵖ D) [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ E] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ F] {Z : CategoryTheory.Functor Cᵒᵖ E} (h : J.plusObj (P.comp F) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight (J.toPlus P) F) (CategoryTheory.CategoryStruct.comp (J.plusCompIso F P).hom h) = CategoryTheory.CategoryStruct.comp (J.toPlus (P.comp F)) h
• CategoryTheory.GrothendieckTopology.plusFunctorWhiskerLeftIso_hom_app 📋 Mathlib.CategoryTheory.Sites.CompatiblePlus
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] {E : Type u_2} [CategoryTheory.Category.{v_2, u_2} E] [∀ (J : CategoryTheory.Limits.MulticospanShape), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan J) D] [∀ (J : CategoryTheory.Limits.MulticospanShape), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan J) E] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ E] (P : CategoryTheory.Functor Cᵒᵖ D) [∀ (F : CategoryTheory.Functor D E) (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ F] [∀ (F : CategoryTheory.Functor D E) (X : C) (W : J.Cover X) (P : CategoryTheory.Functor Cᵒᵖ D), CategoryTheory.Limits.PreservesLimit (W.index P).multicospan F] (X : CategoryTheory.Functor D E) : (J.plusFunctorWhiskerLeftIso P).hom.app X = (J.plusCompIso X P).hom
• CategoryTheory.GrothendieckTopology.plusFunctorWhiskerLeftIso_inv_app 📋 Mathlib.CategoryTheory.Sites.CompatiblePlus
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] {E : Type u_2} [CategoryTheory.Category.{v_2, u_2} E] [∀ (J : CategoryTheory.Limits.MulticospanShape), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan J) D] [∀ (J : CategoryTheory.Limits.MulticospanShape), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan J) E] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ E] (P : CategoryTheory.Functor Cᵒᵖ D) [∀ (F : CategoryTheory.Functor D E) (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ F] [∀ (F : CategoryTheory.Functor D E) (X : C) (W : J.Cover X) (P : CategoryTheory.Functor Cᵒᵖ D), CategoryTheory.Limits.PreservesLimit (W.index P).multicospan F] (X : CategoryTheory.Functor D E) : (J.plusFunctorWhiskerLeftIso P).inv.app X = (J.plusCompIso X P).inv
• CategoryTheory.GrothendieckTopology.plusFunctorWhiskerRightIso_hom_app 📋 Mathlib.CategoryTheory.Sites.CompatiblePlus
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] {E : Type u_2} [CategoryTheory.Category.{v_2, u_2} E] (F : CategoryTheory.Functor D E) [∀ (J : CategoryTheory.Limits.MulticospanShape), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan J) D] [∀ (J : CategoryTheory.Limits.MulticospanShape), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan J) E] [∀ (X : C) (W : J.Cover X) (P : CategoryTheory.Functor Cᵒᵖ D), CategoryTheory.Limits.PreservesLimit (W.index P).multicospan F] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ E] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ F] (X : CategoryTheory.Functor Cᵒᵖ D) : (J.plusFunctorWhiskerRightIso F).hom.app X = (J.plusCompIso F X).hom
• CategoryTheory.GrothendieckTopology.plusFunctorWhiskerRightIso_inv_app 📋 Mathlib.CategoryTheory.Sites.CompatiblePlus
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] {E : Type u_2} [CategoryTheory.Category.{v_2, u_2} E] (F : CategoryTheory.Functor D E) [∀ (J : CategoryTheory.Limits.MulticospanShape), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan J) D] [∀ (J : CategoryTheory.Limits.MulticospanShape), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan J) E] [∀ (X : C) (W : J.Cover X) (P : CategoryTheory.Functor Cᵒᵖ D), CategoryTheory.Limits.PreservesLimit (W.index P).multicospan F] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ E] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ F] (X : CategoryTheory.Functor Cᵒᵖ D) : (J.plusFunctorWhiskerRightIso F).inv.app X = (J.plusCompIso F X).inv
• CategoryTheory.GrothendieckTopology.plusCompIso_whiskerLeft 📋 Mathlib.CategoryTheory.Sites.CompatiblePlus
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] {E : Type u_2} [CategoryTheory.Category.{v_2, u_2} E] [∀ (J : CategoryTheory.Limits.MulticospanShape), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan J) D] [∀ (J : CategoryTheory.Limits.MulticospanShape), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan J) E] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ E] {F G : CategoryTheory.Functor D E} (η : F ⟶ G) (P : CategoryTheory.Functor Cᵒᵖ D) [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ F] [∀ (X : C) (W : J.Cover X) (P : CategoryTheory.Functor Cᵒᵖ D), CategoryTheory.Limits.PreservesLimit (W.index P).multicospan F] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ G] [∀ (X : C) (W : J.Cover X) (P : CategoryTheory.Functor Cᵒᵖ D), CategoryTheory.Limits.PreservesLimit (W.index P).multicospan G] : CategoryTheory.CategoryStruct.comp ((J.plusObj P).whiskerLeft η) (J.plusCompIso G P).hom = CategoryTheory.CategoryStruct.comp (J.plusCompIso F P).hom (J.plusMap (P.whiskerLeft η))
• CategoryTheory.GrothendieckTopology.plusCompIso_whiskerRight 📋 Mathlib.CategoryTheory.Sites.CompatiblePlus
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] {E : Type u_2} [CategoryTheory.Category.{v_2, u_2} E] (F : CategoryTheory.Functor D E) [∀ (J : CategoryTheory.Limits.MulticospanShape), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan J) D] [∀ (J : CategoryTheory.Limits.MulticospanShape), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan J) E] [∀ (X : C) (W : J.Cover X) (P : CategoryTheory.Functor Cᵒᵖ D), CategoryTheory.Limits.PreservesLimit (W.index P).multicospan F] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ E] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ F] {P Q : CategoryTheory.Functor Cᵒᵖ D} (η : P ⟶ Q) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight (J.plusMap η) F) (J.plusCompIso F Q).hom = CategoryTheory.CategoryStruct.comp (J.plusCompIso F P).hom (J.plusMap (CategoryTheory.Functor.whiskerRight η F))
• CategoryTheory.GrothendieckTopology.plusCompIso_whiskerLeft_assoc 📋 Mathlib.CategoryTheory.Sites.CompatiblePlus
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] {E : Type u_2} [CategoryTheory.Category.{v_2, u_2} E] [∀ (J : CategoryTheory.Limits.MulticospanShape), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan J) D] [∀ (J : CategoryTheory.Limits.MulticospanShape), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan J) E] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ E] {F G : CategoryTheory.Functor D E} (η : F ⟶ G) (P : CategoryTheory.Functor Cᵒᵖ D) [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ F] [∀ (X : C) (W : J.Cover X) (P : CategoryTheory.Functor Cᵒᵖ D), CategoryTheory.Limits.PreservesLimit (W.index P).multicospan F] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ G] [∀ (X : C) (W : J.Cover X) (P : CategoryTheory.Functor Cᵒᵖ D), CategoryTheory.Limits.PreservesLimit (W.index P).multicospan G] {Z : CategoryTheory.Functor Cᵒᵖ E} (h : J.plusObj (P.comp G) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((J.plusObj P).whiskerLeft η) (CategoryTheory.CategoryStruct.comp (J.plusCompIso G P).hom h) = CategoryTheory.CategoryStruct.comp (J.plusCompIso F P).hom (CategoryTheory.CategoryStruct.comp (J.plusMap (P.whiskerLeft η)) h)
• CategoryTheory.GrothendieckTopology.plusCompIso_whiskerRight_assoc 📋 Mathlib.CategoryTheory.Sites.CompatiblePlus
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] {E : Type u_2} [CategoryTheory.Category.{v_2, u_2} E] (F : CategoryTheory.Functor D E) [∀ (J : CategoryTheory.Limits.MulticospanShape), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan J) D] [∀ (J : CategoryTheory.Limits.MulticospanShape), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan J) E] [∀ (X : C) (W : J.Cover X) (P : CategoryTheory.Functor Cᵒᵖ D), CategoryTheory.Limits.PreservesLimit (W.index P).multicospan F] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ E] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ F] {P Q : CategoryTheory.Functor Cᵒᵖ D} (η : P ⟶ Q) {Z : CategoryTheory.Functor Cᵒᵖ E} (h : J.plusObj (Q.comp F) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight (J.plusMap η) F) (CategoryTheory.CategoryStruct.comp (J.plusCompIso F Q).hom h) = CategoryTheory.CategoryStruct.comp (J.plusCompIso F P).hom (CategoryTheory.CategoryStruct.comp (J.plusMap (CategoryTheory.Functor.whiskerRight η F)) h)
• CategoryTheory.GrothendieckTopology.ι_plusCompIso_hom 📋 Mathlib.CategoryTheory.Sites.CompatiblePlus
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] {E : Type u_2} [CategoryTheory.Category.{v_2, u_2} E] (F : CategoryTheory.Functor D E) [∀ (J : CategoryTheory.Limits.MulticospanShape), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan J) D] [∀ (J : CategoryTheory.Limits.MulticospanShape), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan J) E] [∀ (X : C) (W : J.Cover X) (P : CategoryTheory.Functor Cᵒᵖ D), CategoryTheory.Limits.PreservesLimit (W.index P).multicospan F] (P : CategoryTheory.Functor Cᵒᵖ D) [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ E] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ F] (X : Cᵒᵖ) (W : (J.Cover (Opposite.unop X))ᵒᵖ) : CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.Limits.colimit.ι (J.diagram P (Opposite.unop X)) W)) ((J.plusCompIso F P).hom.app X) = CategoryTheory.CategoryStruct.comp ((J.diagramCompIso F P (Opposite.unop X)).hom.app W) (CategoryTheory.Limits.colimit.ι (J.diagram (P.comp F) (Opposite.unop X)) W)
• CategoryTheory.GrothendieckTopology.ι_plusCompIso_hom_assoc 📋 Mathlib.CategoryTheory.Sites.CompatiblePlus
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] {E : Type u_2} [CategoryTheory.Category.{v_2, u_2} E] (F : CategoryTheory.Functor D E) [∀ (J : CategoryTheory.Limits.MulticospanShape), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan J) D] [∀ (J : CategoryTheory.Limits.MulticospanShape), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan J) E] [∀ (X : C) (W : J.Cover X) (P : CategoryTheory.Functor Cᵒᵖ D), CategoryTheory.Limits.PreservesLimit (W.index P).multicospan F] (P : CategoryTheory.Functor Cᵒᵖ D) [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ E] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ F] (X : Cᵒᵖ) (W : (J.Cover (Opposite.unop X))ᵒᵖ) {Z : E} (h : (J.plusObj (P.comp F)).obj X ⟶ Z) : CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.Limits.colimit.ι (J.diagram P (Opposite.unop X)) W)) (CategoryTheory.CategoryStruct.comp ((J.plusCompIso F P).hom.app X) h) = CategoryTheory.CategoryStruct.comp ((J.diagramCompIso F P (Opposite.unop X)).hom.app W) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι (J.diagram (P.comp F) (Opposite.unop X)) W) h)
• CategoryTheory.GrothendieckTopology.liftToPlusObjLimitObj 📋 Mathlib.CategoryTheory.Sites.LeftExact
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w} [CategoryTheory.Category.{t, w} D] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] {FD : D → D → Type u_1} {CD : D → Type t} [(X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] [CategoryTheory.ConcreteCategory D FD] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (CategoryTheory.forget D)] [∀ (X : C), Small.{t, max u v} (J.Cover X)ᵒᵖ] {K : Type s} [CategoryTheory.SmallCategory K] [CategoryTheory.FinCategory K] [CategoryTheory.Limits.HasLimitsOfShape K D] [CategoryTheory.Limits.PreservesLimitsOfShape K (CategoryTheory.forget D)] [CategoryTheory.Limits.ReflectsLimitsOfShape K (CategoryTheory.forget D)] (F : CategoryTheory.Functor K (CategoryTheory.Functor Cᵒᵖ D)) (X : C) (S : CategoryTheory.Limits.Cone (F.comp ((J.plusFunctor D).comp ((CategoryTheory.evaluation Cᵒᵖ D).obj (Opposite.op X))))) : S.pt ⟶ (J.plusObj (CategoryTheory.Limits.limit F)).obj (Opposite.op X)
• CategoryTheory.GrothendieckTopology.liftToPlusObjLimitObj_fac 📋 Mathlib.CategoryTheory.Sites.LeftExact
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w} [CategoryTheory.Category.{t, w} D] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] {FD : D → D → Type u_1} {CD : D → Type t} [(X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] [CategoryTheory.ConcreteCategory D FD] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (CategoryTheory.forget D)] [∀ (X : C), Small.{t, max u v} (J.Cover X)ᵒᵖ] {K : Type s} [CategoryTheory.SmallCategory K] [CategoryTheory.FinCategory K] [CategoryTheory.Limits.HasLimitsOfShape K D] [CategoryTheory.Limits.PreservesLimitsOfShape K (CategoryTheory.forget D)] [CategoryTheory.Limits.ReflectsLimitsOfShape K (CategoryTheory.forget D)] (F : CategoryTheory.Functor K (CategoryTheory.Functor Cᵒᵖ D)) (X : C) (S : CategoryTheory.Limits.Cone (F.comp ((J.plusFunctor D).comp ((CategoryTheory.evaluation Cᵒᵖ D).obj (Opposite.op X))))) (k : K) : CategoryTheory.CategoryStruct.comp (CategoryTheory.GrothendieckTopology.liftToPlusObjLimitObj F X S) ((J.plusMap (CategoryTheory.Limits.limit.π F k)).app (Opposite.op X)) = S.π.app k
• CategoryTheory.Presheaf.isLocallyInjective_toPlus 📋 Mathlib.CategoryTheory.Sites.LocallyInjective
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) (P : CategoryTheory.Functor Cᵒᵖ (Type (max u v))) : CategoryTheory.Presheaf.IsLocallyInjective J (J.toPlus P)
• CategoryTheory.Presheaf.isLocallySurjective_toPlus 📋 Mathlib.CategoryTheory.Sites.LocallySurjective
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) (P : CategoryTheory.Functor Cᵒᵖ (Type (max u v))) : CategoryTheory.Presheaf.IsLocallySurjective J (J.toPlus P)

About

Loogle searches Lean and Mathlib definitions and theorems.

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

Usage

Loogle finds definitions and lemmas in various ways:

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

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

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

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

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

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

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

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

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

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

Source code

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

This is Loogle revision 9f11169 serving mathlib revision 69fae59