Loogle!

Result

Found 148 declarations mentioning CategoryTheory.Limits.WidePullbackShape.

• CategoryTheory.Limits.WidePullbackShape 📋 Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
  (J : Type w) : Type w
• CategoryTheory.Limits.instInhabitedWidePullbackShape 📋 Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
  (J : Type w) : Inhabited (CategoryTheory.Limits.WidePullbackShape J)
• CategoryTheory.Limits.WidePullbackShape.category 📋 Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
  {J : Type w} : CategoryTheory.SmallCategory (CategoryTheory.Limits.WidePullbackShape J)
• CategoryTheory.Limits.WidePullbackShape.struct 📋 Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
  {J : Type w} : CategoryTheory.CategoryStruct.{w, w} (CategoryTheory.Limits.WidePullbackShape J)
• CategoryTheory.Limits.WidePullbackShape.Hom 📋 Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
  {J : Type w} : CategoryTheory.Limits.WidePullbackShape J → CategoryTheory.Limits.WidePullbackShape J → Type w
• CategoryTheory.Limits.WidePullbackShape.Hom.id 📋 Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
  {J : Type w} (X : CategoryTheory.Limits.WidePullbackShape J) : X.Hom X
• CategoryTheory.Limits.WidePullbackShape.subsingleton_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
  {J : Type w} : Quiver.IsThin (CategoryTheory.Limits.WidePullbackShape J)
• CategoryTheory.Limits.WidePullbackShape.instDecidableEqHom 📋 Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
  {J✝ : Type u_1} {a✝ a✝¹ : CategoryTheory.Limits.WidePullbackShape J✝} [DecidableEq J✝] : DecidableEq (a✝.Hom a✝¹)
• CategoryTheory.Limits.widePullbackShapeOp 📋 Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
  (J : Type w) : CategoryTheory.Functor (CategoryTheory.Limits.WidePullbackShape J) (CategoryTheory.Limits.WidePushoutShape J)ᵒᵖ
• CategoryTheory.Limits.widePullbackShapeOpEquiv 📋 Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
  (J : Type w) : (CategoryTheory.Limits.WidePullbackShape J)ᵒᵖ ≌ CategoryTheory.Limits.WidePushoutShape J
• CategoryTheory.Limits.widePullbackShapeUnop 📋 Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
  (J : Type w) : CategoryTheory.Functor (CategoryTheory.Limits.WidePullbackShape J)ᵒᵖ (CategoryTheory.Limits.WidePushoutShape J)
• CategoryTheory.Limits.widePushoutShapeOp 📋 Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
  (J : Type w) : CategoryTheory.Functor (CategoryTheory.Limits.WidePushoutShape J) (CategoryTheory.Limits.WidePullbackShape J)ᵒᵖ
• CategoryTheory.Limits.widePushoutShapeOpEquiv 📋 Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
  (J : Type w) : (CategoryTheory.Limits.WidePushoutShape J)ᵒᵖ ≌ CategoryTheory.Limits.WidePullbackShape J
• CategoryTheory.Limits.widePushoutShapeUnop 📋 Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
  (J : Type w) : CategoryTheory.Functor (CategoryTheory.Limits.WidePushoutShape J)ᵒᵖ (CategoryTheory.Limits.WidePullbackShape J)
• CategoryTheory.Limits.WidePullbackShape.equivalenceOfEquiv 📋 Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
  {J : Type w} (J' : Type w') (h : J ≃ J') : CategoryTheory.Limits.WidePullbackShape J ≌ CategoryTheory.Limits.WidePullbackShape J'
• CategoryTheory.Limits.WidePullbackShape.hom_id 📋 Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
  {J : Type w} (X : CategoryTheory.Limits.WidePullbackShape J) : CategoryTheory.Limits.WidePullbackShape.Hom.id X = CategoryTheory.CategoryStruct.id X
• CategoryTheory.Limits.WidePullbackShape.uliftEquivalence 📋 Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
  {J : Type w} : CategoryTheory.ULiftHom (ULift.{w', w} (CategoryTheory.Limits.WidePullbackShape J)) ≌ CategoryTheory.Limits.WidePullbackShape (ULift.{w', w} J)
• CategoryTheory.Limits.WidePullbackShape.instDecidableEqHom.decEq 📋 Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
  {J✝ : Type u_1} {a✝ a✝¹ : CategoryTheory.Limits.WidePullbackShape J✝} [DecidableEq J✝] (x✝ x✝¹ : a✝.Hom a✝¹) : Decidable (x✝ = x✝¹)
• CategoryTheory.Limits.WidePullbackShape.wideCospan 📋 Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
  {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] (B : C) (objs : J → C) (arrows : (j : J) → objs j ⟶ B) : CategoryTheory.Functor (CategoryTheory.Limits.WidePullbackShape J) C
• CategoryTheory.Limits.widePullbackShapeOp_obj 📋 Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
  (J : Type w) (X : CategoryTheory.Limits.WidePullbackShape J) : (CategoryTheory.Limits.widePullbackShapeOp J).obj X = Opposite.op X
• CategoryTheory.Limits.widePullbackShapeUnop_obj 📋 Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
  (J : Type w) (X : (CategoryTheory.Limits.WidePullbackShape J)ᵒᵖ) : (CategoryTheory.Limits.widePullbackShapeUnop J).obj X = Opposite.unop X
• CategoryTheory.Limits.widePushoutShapeOp_obj 📋 Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
  (J : Type w) (X : CategoryTheory.Limits.WidePushoutShape J) : (CategoryTheory.Limits.widePushoutShapeOp J).obj X = Opposite.op X
• CategoryTheory.Limits.widePushoutShapeUnop_obj 📋 Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
  (J : Type w) (X : (CategoryTheory.Limits.WidePushoutShape J)ᵒᵖ) : (CategoryTheory.Limits.widePushoutShapeUnop J).obj X = Opposite.unop X
• CategoryTheory.Limits.widePullbackShapeOpEquiv_functor 📋 Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
  (J : Type w) : (CategoryTheory.Limits.widePullbackShapeOpEquiv J).functor = CategoryTheory.Limits.widePullbackShapeUnop J
• CategoryTheory.Limits.widePullbackShapeOpEquiv_inverse 📋 Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
  (J : Type w) : (CategoryTheory.Limits.widePullbackShapeOpEquiv J).inverse = CategoryTheory.Limits.widePushoutShapeOp J
• CategoryTheory.Limits.widePushoutShapeOpEquiv_functor 📋 Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
  (J : Type w) : (CategoryTheory.Limits.widePushoutShapeOpEquiv J).functor = CategoryTheory.Limits.widePushoutShapeUnop J
• CategoryTheory.Limits.widePushoutShapeOpEquiv_inverse 📋 Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
  (J : Type w) : (CategoryTheory.Limits.widePushoutShapeOpEquiv J).inverse = CategoryTheory.Limits.widePullbackShapeOp J
• CategoryTheory.Limits.WidePullbackShape.equivalenceOfEquiv_functor_obj_none 📋 Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
  {ι : Type u_1} {ι' : Type u_2} (e : ι ≃ ι') : (CategoryTheory.Limits.WidePullbackShape.equivalenceOfEquiv ι' e).functor.obj none = none
• CategoryTheory.Limits.widePullbackShapeOpMap 📋 Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
  (J : Type w) (X Y : CategoryTheory.Limits.WidePullbackShape J) : (X ⟶ Y) → (Opposite.op X ⟶ Opposite.op Y)
• CategoryTheory.Limits.widePushoutShapeOpMap 📋 Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
  (J : Type w) (X Y : CategoryTheory.Limits.WidePushoutShape J) : (X ⟶ Y) → (Opposite.op X ⟶ Opposite.op Y)
• CategoryTheory.Limits.WidePullbackShape.wideCospan_obj 📋 Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
  {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] (B : C) (objs : J → C) (arrows : (j : J) → objs j ⟶ B) (j : CategoryTheory.Limits.WidePullbackShape J) : (CategoryTheory.Limits.WidePullbackShape.wideCospan B objs arrows).obj j = Option.casesOn j B objs
• CategoryTheory.Limits.widePullbackShapeUnopOp 📋 Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
  (J : Type w) : (CategoryTheory.Limits.widePullbackShapeOp J).comp (CategoryTheory.Limits.widePushoutShapeUnop J) ≅ CategoryTheory.Functor.id (CategoryTheory.Limits.WidePullbackShape J)
• CategoryTheory.Limits.widePushoutShapeUnopOp 📋 Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
  (J : Type w) : (CategoryTheory.Limits.widePushoutShapeOp J).comp (CategoryTheory.Limits.widePullbackShapeUnop J) ≅ CategoryTheory.Functor.id (CategoryTheory.Limits.WidePushoutShape J)
• CategoryTheory.Limits.WidePullbackCone.base 📋 Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
  {C : Type u} [CategoryTheory.Category.{v, u} C] {ι : Type u_1} {X : C} {Y : ι → C} {f : (i : ι) → Y i ⟶ X} (s : CategoryTheory.Limits.WidePullbackCone f) : s.pt ⟶ X
• CategoryTheory.Limits.WidePullbackCone.π 📋 Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
  {C : Type u} [CategoryTheory.Category.{v, u} C] {ι : Type u_1} {X : C} {Y : ι → C} {f : (i : ι) → Y i ⟶ X} (s : CategoryTheory.Limits.WidePullbackCone f) (i : ι) : s.pt ⟶ Y i
• CategoryTheory.Limits.WidePullbackShape.equivalenceOfEquiv_functor_obj_some 📋 Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
  {ι : Type u_1} {ι' : Type u_2} (e : ι ≃ ι') (i : ι) : (CategoryTheory.Limits.WidePullbackShape.equivalenceOfEquiv ι' e).functor.obj (some i) = some (e i)
• CategoryTheory.Limits.widePullbackShapeOp_map 📋 Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
  (J : Type w) {X₁ X₂ : CategoryTheory.Limits.WidePullbackShape J} (a✝ : X₁ ⟶ X₂) : (CategoryTheory.Limits.widePullbackShapeOp J).map a✝ = CategoryTheory.Limits.widePullbackShapeOpMap J X₁ X₂ a✝
• CategoryTheory.Limits.widePushoutShapeOp_map 📋 Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
  (J : Type w) {X Y : CategoryTheory.Limits.WidePushoutShape J} (a✝ : X ⟶ Y) : (CategoryTheory.Limits.widePushoutShapeOp J).map a✝ = CategoryTheory.Limits.widePushoutShapeOpMap J X Y a✝
• CategoryTheory.Limits.widePullbackShapeOpEquiv_counitIso 📋 Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
  (J : Type w) : (CategoryTheory.Limits.widePullbackShapeOpEquiv J).counitIso = CategoryTheory.Limits.widePushoutShapeUnopOp J
• CategoryTheory.Limits.widePushoutShapeOpEquiv_counitIso 📋 Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
  (J : Type w) : (CategoryTheory.Limits.widePushoutShapeOpEquiv J).counitIso = CategoryTheory.Limits.widePullbackShapeUnopOp J
• CategoryTheory.Limits.widePullbackShapeOpUnop 📋 Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
  (J : Type w) : (CategoryTheory.Limits.widePullbackShapeUnop J).comp (CategoryTheory.Limits.widePushoutShapeOp J) ≅ CategoryTheory.Functor.id (CategoryTheory.Limits.WidePullbackShape J)ᵒᵖ
• CategoryTheory.Limits.widePushoutShapeOpUnop 📋 Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
  (J : Type w) : (CategoryTheory.Limits.widePushoutShapeUnop J).comp (CategoryTheory.Limits.widePullbackShapeOp J) ≅ CategoryTheory.Functor.id (CategoryTheory.Limits.WidePushoutShape J)ᵒᵖ
• CategoryTheory.Limits.WidePullbackShape.diagramIsoWideCospan 📋 Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
  {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor (CategoryTheory.Limits.WidePullbackShape J) C) : F ≅ CategoryTheory.Limits.WidePullbackShape.wideCospan (F.obj none) (fun j => F.obj (some j)) fun j => F.map (CategoryTheory.Limits.WidePullbackShape.Hom.term j)
• CategoryTheory.Limits.WidePullbackCone.condition 📋 Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
  {C : Type u} [CategoryTheory.Category.{v, u} C] {ι : Type u_1} {X : C} {Y : ι → C} {f : (i : ι) → Y i ⟶ X} (s : CategoryTheory.Limits.WidePullbackCone f) (i : ι) : CategoryTheory.CategoryStruct.comp (s.π i) (f i) = s.base
• CategoryTheory.Limits.WidePullbackCone.mk_pt 📋 Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
  {C : Type u} [CategoryTheory.Category.{v, u} C] {ι : Type u_1} {X : C} {Y : ι → C} {f : (i : ι) → Y i ⟶ X} {W : C} (b : W ⟶ X) (π : (i : ι) → W ⟶ Y i) (h : ∀ (i : ι), CategoryTheory.CategoryStruct.comp (π i) (f i) = b) : (CategoryTheory.Limits.WidePullbackCone.mk b π h).pt = W
• CategoryTheory.Limits.WidePullbackCone.reindexIsLimitEquiv 📋 Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
  {C : Type u} [CategoryTheory.Category.{v, u} C] {ι : Type u_2} {X : C} {Y : ι → C} {f : (i : ι) → Y i ⟶ X} (s : CategoryTheory.Limits.WidePullbackCone f) {ι' : Type u_3} (e : ι' ≃ ι) : CategoryTheory.Limits.IsLimit (s.reindex e) ≃ CategoryTheory.Limits.IsLimit s
• CategoryTheory.Limits.WidePullbackCone.reindex_pt 📋 Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
  {C : Type u} [CategoryTheory.Category.{v, u} C] {ι : Type u_2} {X : C} {Y : ι → C} {f : (i : ι) → Y i ⟶ X} (s : CategoryTheory.Limits.WidePullbackCone f) {ι' : Type u_3} (e : ι' ≃ ι) : (s.reindex e).pt = s.pt
• CategoryTheory.Limits.WidePullbackCone.IsLimit.lift 📋 Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
  {C : Type u} [CategoryTheory.Category.{v, u} C] {ι : Type u_1} {X : C} {Y : ι → C} {f : (i : ι) → Y i ⟶ X} {s : CategoryTheory.Limits.WidePullbackCone f} (hs : CategoryTheory.Limits.IsLimit s) {W : C} (b : W ⟶ X) (a : (i : ι) → W ⟶ Y i) (w : ∀ (i : ι), CategoryTheory.CategoryStruct.comp (a i) (f i) = b) : W ⟶ s.pt
• CategoryTheory.Limits.WidePullbackCone.mk_base 📋 Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
  {C : Type u} [CategoryTheory.Category.{v, u} C] {ι : Type u_1} {X : C} {Y : ι → C} {f : (i : ι) → Y i ⟶ X} {W : C} (b : W ⟶ X) (π : (i : ι) → W ⟶ Y i) (h : ∀ (i : ι), CategoryTheory.CategoryStruct.comp (π i) (f i) = b) : (CategoryTheory.Limits.WidePullbackCone.mk b π h).base = b
• CategoryTheory.Limits.WidePullbackShape.equivalenceOfEquiv_functor_map_term 📋 Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
  {ι : Type u_1} {ι' : Type u_2} (e : ι ≃ ι') (i : ι) : (CategoryTheory.Limits.WidePullbackShape.equivalenceOfEquiv ι' e).functor.map (CategoryTheory.Limits.WidePullbackShape.Hom.term i) = CategoryTheory.Limits.WidePullbackShape.Hom.term (e i)
• CategoryTheory.Limits.WidePullbackCone.mk_π 📋 Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
  {C : Type u} [CategoryTheory.Category.{v, u} C] {ι : Type u_1} {X : C} {Y : ι → C} {f : (i : ι) → Y i ⟶ X} {W : C} (b : W ⟶ X) (π : (i : ι) → W ⟶ Y i) (h : ∀ (i : ι), CategoryTheory.CategoryStruct.comp (π i) (f i) = b) (i : ι) : (CategoryTheory.Limits.WidePullbackCone.mk b π h).π i = π i
• CategoryTheory.Limits.WidePullbackShape.mkCone 📋 Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
  {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor (CategoryTheory.Limits.WidePullbackShape J) C} {X : C} (f : X ⟶ F.obj none) (π : (j : J) → X ⟶ F.obj (some j)) (w : ∀ (j : J), CategoryTheory.CategoryStruct.comp (π j) (F.map (CategoryTheory.Limits.WidePullbackShape.Hom.term j)) = f) : CategoryTheory.Limits.Cone F
• CategoryTheory.Limits.WidePullbackCone.condition_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
  {C : Type u} [CategoryTheory.Category.{v, u} C] {ι : Type u_1} {X : C} {Y : ι → C} {f : (i : ι) → Y i ⟶ X} (s : CategoryTheory.Limits.WidePullbackCone f) (i : ι) {Z : C} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (s.π i) (CategoryTheory.CategoryStruct.comp (f i) h) = CategoryTheory.CategoryStruct.comp s.base h
• CategoryTheory.Limits.WidePullbackShape.mkCone_pt 📋 Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
  {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor (CategoryTheory.Limits.WidePullbackShape J) C} {X : C} (f : X ⟶ F.obj none) (π : (j : J) → X ⟶ F.obj (some j)) (w : ∀ (j : J), CategoryTheory.CategoryStruct.comp (π j) (F.map (CategoryTheory.Limits.WidePullbackShape.Hom.term j)) = f) : (CategoryTheory.Limits.WidePullbackShape.mkCone f π w).pt = X
• CategoryTheory.Limits.widePullbackShapeUnop_map 📋 Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
  (J : Type w) {X✝ Y✝ : (CategoryTheory.Limits.WidePullbackShape J)ᵒᵖ} (f : X✝ ⟶ Y✝) : (CategoryTheory.Limits.widePullbackShapeUnop J).map f = (CategoryTheory.Limits.widePullbackShapeOpMap J (Opposite.unop Y✝) (Opposite.unop X✝) f.unop).unop
• CategoryTheory.Limits.widePushoutShapeUnop_map 📋 Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
  (J : Type w) {X✝ Y✝ : (CategoryTheory.Limits.WidePushoutShape J)ᵒᵖ} (f : X✝ ⟶ Y✝) : (CategoryTheory.Limits.widePushoutShapeUnop J).map f = (CategoryTheory.Limits.widePushoutShapeOpMap J (Opposite.unop Y✝) (Opposite.unop X✝) f.unop).unop
• CategoryTheory.Limits.WidePullbackCone.IsLimit.lift_base 📋 Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
  {C : Type u} [CategoryTheory.Category.{v, u} C] {ι : Type u_1} {X : C} {Y : ι → C} {f : (i : ι) → Y i ⟶ X} {s : CategoryTheory.Limits.WidePullbackCone f} (hs : CategoryTheory.Limits.IsLimit s) {W : C} (b : W ⟶ X) (a : (i : ι) → W ⟶ Y i) (w : ∀ (i : ι), CategoryTheory.CategoryStruct.comp (a i) (f i) = b) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.WidePullbackCone.IsLimit.lift hs b a w) s.base = b
• CategoryTheory.Limits.WidePullbackCone.IsLimit.lift_π 📋 Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
  {C : Type u} [CategoryTheory.Category.{v, u} C] {ι : Type u_1} {X : C} {Y : ι → C} {f : (i : ι) → Y i ⟶ X} {s : CategoryTheory.Limits.WidePullbackCone f} (hs : CategoryTheory.Limits.IsLimit s) {W : C} (b : W ⟶ X) (a : (i : ι) → W ⟶ Y i) (w : ∀ (i : ι), CategoryTheory.CategoryStruct.comp (a i) (f i) = b) (i : ι) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.WidePullbackCone.IsLimit.lift hs b a w) (s.π i) = a i
• CategoryTheory.Limits.widePullbackShapeOpEquiv_unitIso 📋 Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
  (J : Type w) : (CategoryTheory.Limits.widePullbackShapeOpEquiv J).unitIso = (CategoryTheory.Limits.widePullbackShapeOpUnop J).symm
• CategoryTheory.Limits.widePushoutShapeOpEquiv_unitIso 📋 Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
  (J : Type w) : (CategoryTheory.Limits.widePushoutShapeOpEquiv J).unitIso = (CategoryTheory.Limits.widePushoutShapeOpUnop J).symm
• CategoryTheory.Limits.WidePullbackCone.reindex_base 📋 Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
  {C : Type u} [CategoryTheory.Category.{v, u} C] {ι : Type u_2} {X : C} {Y : ι → C} {f : (i : ι) → Y i ⟶ X} (s : CategoryTheory.Limits.WidePullbackCone f) {ι' : Type u_3} (e : ι' ≃ ι) : (s.reindex e).base = s.base
• CategoryTheory.Limits.WidePullbackCone.IsLimit.lift_base_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
  {C : Type u} [CategoryTheory.Category.{v, u} C] {ι : Type u_1} {X : C} {Y : ι → C} {f : (i : ι) → Y i ⟶ X} {s : CategoryTheory.Limits.WidePullbackCone f} (hs : CategoryTheory.Limits.IsLimit s) {W : C} (b : W ⟶ X) (a : (i : ι) → W ⟶ Y i) (w : ∀ (i : ι), CategoryTheory.CategoryStruct.comp (a i) (f i) = b) {Z : C} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.WidePullbackCone.IsLimit.lift hs b a w) (CategoryTheory.CategoryStruct.comp s.base h) = CategoryTheory.CategoryStruct.comp b h
• CategoryTheory.Limits.WidePullbackCone.IsLimit.lift_π_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
  {C : Type u} [CategoryTheory.Category.{v, u} C] {ι : Type u_1} {X : C} {Y : ι → C} {f : (i : ι) → Y i ⟶ X} {s : CategoryTheory.Limits.WidePullbackCone f} (hs : CategoryTheory.Limits.IsLimit s) {W : C} (b : W ⟶ X) (a : (i : ι) → W ⟶ Y i) (w : ∀ (i : ι), CategoryTheory.CategoryStruct.comp (a i) (f i) = b) (i : ι) {Z : C} (h : Y i ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.WidePullbackCone.IsLimit.lift hs b a w) (CategoryTheory.CategoryStruct.comp (s.π i) h) = CategoryTheory.CategoryStruct.comp (a i) h
• CategoryTheory.Limits.WidePullbackCone.reindex_π 📋 Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
  {C : Type u} [CategoryTheory.Category.{v, u} C] {ι : Type u_2} {X : C} {Y : ι → C} {f : (i : ι) → Y i ⟶ X} (s : CategoryTheory.Limits.WidePullbackCone f) {ι' : Type u_3} (e : ι' ≃ ι) (i : ι') : (s.reindex e).π i = s.π (e i)
• CategoryTheory.Limits.WidePullbackCone.IsLimit.hom_ext 📋 Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
  {C : Type u} [CategoryTheory.Category.{v, u} C] {ι : Type u_1} {X : C} {Y : ι → C} {f : (i : ι) → Y i ⟶ X} {s : CategoryTheory.Limits.WidePullbackCone f} (hs : CategoryTheory.Limits.IsLimit s) {W : C} {k l : W ⟶ s.pt} (hbase : CategoryTheory.CategoryStruct.comp k s.base = CategoryTheory.CategoryStruct.comp l s.base) (hπ : ∀ (i : ι), CategoryTheory.CategoryStruct.comp k (s.π i) = CategoryTheory.CategoryStruct.comp l (s.π i)) : k = l
• CategoryTheory.Limits.WidePullbackShape.functorExt 📋 Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
  {C : Type u} [CategoryTheory.Category.{v, u} C] {ι : Type u_1} {F G : CategoryTheory.Functor (CategoryTheory.Limits.WidePullbackShape ι) C} (base : F.obj none ≅ G.obj none) (comp : (i : ι) → F.obj (some i) ≅ G.obj (some i)) (w : ∀ (i : ι), CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.Limits.WidePullbackShape.Hom.term i)) base.hom = CategoryTheory.CategoryStruct.comp (comp i).hom (G.map (CategoryTheory.Limits.WidePullbackShape.Hom.term i)) := by cat_disch) : F ≅ G
• CategoryTheory.Limits.WidePullbackShape.mkCone_π_app 📋 Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
  {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor (CategoryTheory.Limits.WidePullbackShape J) C} {X : C} (f : X ⟶ F.obj none) (π : (j : J) → X ⟶ F.obj (some j)) (w : ∀ (j : J), CategoryTheory.CategoryStruct.comp (π j) (F.map (CategoryTheory.Limits.WidePullbackShape.Hom.term j)) = f) (j : CategoryTheory.Limits.WidePullbackShape J) : (CategoryTheory.Limits.WidePullbackShape.mkCone f π w).π.app j = match j with | none => f | some j => π j
• CategoryTheory.Limits.WidePullbackCone.ext 📋 Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
  {C : Type u} [CategoryTheory.Category.{v, u} C] {ι : Type u_2} {X : C} {Y : ι → C} {f : (i : ι) → Y i ⟶ X} {s t : CategoryTheory.Limits.WidePullbackCone f} (e : s.pt ≅ t.pt) (base : CategoryTheory.CategoryStruct.comp e.hom t.base = s.base := by cat_disch) (π : ∀ (i : ι), CategoryTheory.CategoryStruct.comp e.hom (t.π i) = s.π i := by cat_disch) : s ≅ t
• CategoryTheory.Limits.WidePullbackShape.functorExt_hom_app 📋 Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
  {C : Type u} [CategoryTheory.Category.{v, u} C] {ι : Type u_1} {F G : CategoryTheory.Functor (CategoryTheory.Limits.WidePullbackShape ι) C} (base : F.obj none ≅ G.obj none) (comp : (i : ι) → F.obj (some i) ≅ G.obj (some i)) (w : ∀ (i : ι), CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.Limits.WidePullbackShape.Hom.term i)) base.hom = CategoryTheory.CategoryStruct.comp (comp i).hom (G.map (CategoryTheory.Limits.WidePullbackShape.Hom.term i)) := by cat_disch) (X : CategoryTheory.Limits.WidePullbackShape ι) : (CategoryTheory.Limits.WidePullbackShape.functorExt base comp w).hom.app X = (match X with | none => base | some i => comp i).hom
• CategoryTheory.Limits.WidePullbackShape.functorExt_inv_app 📋 Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
  {C : Type u} [CategoryTheory.Category.{v, u} C] {ι : Type u_1} {F G : CategoryTheory.Functor (CategoryTheory.Limits.WidePullbackShape ι) C} (base : F.obj none ≅ G.obj none) (comp : (i : ι) → F.obj (some i) ≅ G.obj (some i)) (w : ∀ (i : ι), CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.Limits.WidePullbackShape.Hom.term i)) base.hom = CategoryTheory.CategoryStruct.comp (comp i).hom (G.map (CategoryTheory.Limits.WidePullbackShape.Hom.term i)) := by cat_disch) (X : CategoryTheory.Limits.WidePullbackShape ι) : (CategoryTheory.Limits.WidePullbackShape.functorExt base comp w).inv.app X = (match X with | none => base | some i => comp i).inv
• CategoryTheory.Limits.WidePullbackCone.IsLimit.mk 📋 Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
  {C : Type u} [CategoryTheory.Category.{v, u} C] {ι : Type u_1} {X : C} {Y : ι → C} {f : (i : ι) → Y i ⟶ X} (s : CategoryTheory.Limits.WidePullbackCone f) (lift : (t : CategoryTheory.Limits.WidePullbackCone f) → t.pt ⟶ s.pt) (facbase : ∀ (t : CategoryTheory.Limits.WidePullbackCone f), CategoryTheory.CategoryStruct.comp (lift t) s.base = t.base) (facπ : ∀ (t : CategoryTheory.Limits.WidePullbackCone f) (i : ι), CategoryTheory.CategoryStruct.comp (lift t) (s.π i) = t.π i) (uniq : ∀ (t : CategoryTheory.Limits.WidePullbackCone f) (m : t.pt ⟶ s.pt), CategoryTheory.CategoryStruct.comp m s.base = t.base → (∀ (i : ι), CategoryTheory.CategoryStruct.comp m (s.π i) = t.π i) → m = lift t) : CategoryTheory.Limits.IsLimit s
• CategoryTheory.Limits.WidePullbackShape.wideCospan_map 📋 Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
  {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] (B : C) (objs : J → C) (arrows : (j : J) → objs j ⟶ B) {X✝ Y✝ : CategoryTheory.Limits.WidePullbackShape J} (f : X✝ ⟶ Y✝) : (CategoryTheory.Limits.WidePullbackShape.wideCospan B objs arrows).map f = CategoryTheory.Limits.WidePullbackShape.Hom.casesOn (motive := fun a a_1 x => X✝ = a → Y✝ = a_1 → f ≍ x → (Option.casesOn X✝ B objs ⟶ Option.casesOn Y✝ B objs)) f (fun X h => Eq.ndrec (motive := fun X => Y✝ = X → f ≍ CategoryTheory.Limits.WidePullbackShape.Hom.id X → (Option.casesOn X✝ B objs ⟶ Option.casesOn Y✝ B objs)) (fun h => Eq.ndrec (motive := fun {Y} => (f : X✝ ⟶ Y) → f ≍ CategoryTheory.Limits.WidePullbackShape.Hom.id X✝ → (Option.casesOn X✝ B objs ⟶ Option.casesOn Y B objs)) (fun f h => CategoryTheory.CategoryStruct.id (Option.casesOn X✝ B objs)) ⋯ f) h) (fun j h => Eq.ndrec (motive := fun {X} => (f : X ⟶ Y✝) → Y✝ = none → f ≍ CategoryTheory.Limits.WidePullbackShape.Hom.term j → (Option.casesOn X B objs ⟶ Option.casesOn Y✝ B objs)) (fun f h => Eq.ndrec (motive := fun {Y} => (f : some j ⟶ Y) → f ≍ CategoryTheory.Limits.WidePullbackShape.Hom.term j → (Option.casesOn (some j) B objs ⟶ Option.casesOn Y B objs)) (fun f h => arrows j) ⋯ f) ⋯ f) ⋯ ⋯ ⋯
• CategoryTheory.Limits.walkingCospanOpEquiv_functor_obj 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
  (X : (CategoryTheory.Limits.WidePullbackShape CategoryTheory.Limits.WalkingPair)ᵒᵖ) : CategoryTheory.Limits.walkingCospanOpEquiv.functor.obj X = Opposite.unop X
• CategoryTheory.Limits.walkingCospanOpEquiv_inverse_obj 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
  (X : CategoryTheory.Limits.WidePushoutShape CategoryTheory.Limits.WalkingPair) : CategoryTheory.Limits.walkingCospanOpEquiv.inverse.obj X = Opposite.op X
• CategoryTheory.Limits.walkingSpanOpEquiv_functor_obj 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
  (X : (CategoryTheory.Limits.WidePushoutShape CategoryTheory.Limits.WalkingPair)ᵒᵖ) : CategoryTheory.Limits.walkingSpanOpEquiv.functor.obj X = Opposite.unop X
• CategoryTheory.Limits.walkingSpanOpEquiv_inverse_obj 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
  (X : CategoryTheory.Limits.WidePullbackShape CategoryTheory.Limits.WalkingPair) : CategoryTheory.Limits.walkingSpanOpEquiv.inverse.obj X = Opposite.op X
• CategoryTheory.Limits.walkingCospanOpEquiv_inverse_map 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
  {X Y : CategoryTheory.Limits.WidePushoutShape CategoryTheory.Limits.WalkingPair} (a✝ : X ⟶ Y) : CategoryTheory.Limits.walkingCospanOpEquiv.inverse.map a✝ = CategoryTheory.Limits.widePushoutShapeOpMap CategoryTheory.Limits.WalkingPair X Y a✝
• CategoryTheory.Limits.walkingSpanOpEquiv_inverse_map 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
  {X₁ X₂ : CategoryTheory.Limits.WidePullbackShape CategoryTheory.Limits.WalkingPair} (a✝ : X₁ ⟶ X₂) : CategoryTheory.Limits.walkingSpanOpEquiv.inverse.map a✝ = CategoryTheory.Limits.widePullbackShapeOpMap CategoryTheory.Limits.WalkingPair X₁ X₂ a✝
• CategoryTheory.Limits.walkingCospanOpEquiv_functor_map 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
  {X✝ Y✝ : (CategoryTheory.Limits.WidePullbackShape CategoryTheory.Limits.WalkingPair)ᵒᵖ} (f : X✝ ⟶ Y✝) : CategoryTheory.Limits.walkingCospanOpEquiv.functor.map f = (CategoryTheory.Limits.widePullbackShapeOpMap CategoryTheory.Limits.WalkingPair (Opposite.unop Y✝) (Opposite.unop X✝) f.unop).unop
• CategoryTheory.Limits.walkingSpanOpEquiv_functor_map 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
  {X✝ Y✝ : (CategoryTheory.Limits.WidePushoutShape CategoryTheory.Limits.WalkingPair)ᵒᵖ} (f : X✝ ⟶ Y✝) : CategoryTheory.Limits.walkingSpanOpEquiv.functor.map f = (CategoryTheory.Limits.widePushoutShapeOpMap CategoryTheory.Limits.WalkingPair (Opposite.unop Y✝) (Opposite.unop X✝) f.unop).unop
• CategoryTheory.Limits.walkingCospanOpEquiv_counitIso_hom_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
  (X : CategoryTheory.Limits.WidePushoutShape CategoryTheory.Limits.WalkingPair) : CategoryTheory.Limits.walkingCospanOpEquiv.counitIso.hom.app X = CategoryTheory.CategoryStruct.id X
• CategoryTheory.Limits.walkingCospanOpEquiv_counitIso_inv_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
  (X : CategoryTheory.Limits.WidePushoutShape CategoryTheory.Limits.WalkingPair) : CategoryTheory.Limits.walkingCospanOpEquiv.counitIso.inv.app X = CategoryTheory.CategoryStruct.id X
• CategoryTheory.Limits.walkingSpanOpEquiv_counitIso_hom_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
  (X : CategoryTheory.Limits.WidePullbackShape CategoryTheory.Limits.WalkingPair) : CategoryTheory.Limits.walkingSpanOpEquiv.counitIso.hom.app X = CategoryTheory.CategoryStruct.id X
• CategoryTheory.Limits.walkingSpanOpEquiv_counitIso_inv_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
  (X : CategoryTheory.Limits.WidePullbackShape CategoryTheory.Limits.WalkingPair) : CategoryTheory.Limits.walkingSpanOpEquiv.counitIso.inv.app X = CategoryTheory.CategoryStruct.id X
• CategoryTheory.Limits.walkingCospanOpEquiv_unitIso_hom_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
  (X : (CategoryTheory.Limits.WidePullbackShape CategoryTheory.Limits.WalkingPair)ᵒᵖ) : CategoryTheory.Limits.walkingCospanOpEquiv.unitIso.hom.app X = CategoryTheory.CategoryStruct.id X
• CategoryTheory.Limits.walkingCospanOpEquiv_unitIso_inv_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
  (X : (CategoryTheory.Limits.WidePullbackShape CategoryTheory.Limits.WalkingPair)ᵒᵖ) : CategoryTheory.Limits.walkingCospanOpEquiv.unitIso.inv.app X = CategoryTheory.CategoryStruct.id X
• CategoryTheory.Limits.walkingSpanOpEquiv_unitIso_hom_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
  (X : (CategoryTheory.Limits.WidePushoutShape CategoryTheory.Limits.WalkingPair)ᵒᵖ) : CategoryTheory.Limits.walkingSpanOpEquiv.unitIso.hom.app X = CategoryTheory.CategoryStruct.id X
• CategoryTheory.Limits.walkingSpanOpEquiv_unitIso_inv_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
  (X : (CategoryTheory.Limits.WidePushoutShape CategoryTheory.Limits.WalkingPair)ᵒᵖ) : CategoryTheory.Limits.walkingSpanOpEquiv.unitIso.inv.app X = CategoryTheory.CategoryStruct.id X
• CategoryTheory.Limits.WidePullbackShape.fintypeObj 📋 Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits
  {J : Type v} [Fintype J] : Fintype (CategoryTheory.Limits.WidePullbackShape J)
• CategoryTheory.Limits.finCategoryWidePullback 📋 Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits
  {J : Type v} [Fintype J] : CategoryTheory.FinCategory (CategoryTheory.Limits.WidePullbackShape J)
• CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape 📋 Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits
  (C : Type u) [CategoryTheory.Category.{v, u} C] (J : Type) [Finite J] [CategoryTheory.Limits.HasFiniteWidePullbacks C] : CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WidePullbackShape J) C
• CategoryTheory.Limits.HasFiniteWidePullbacks.mk 📋 Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits
  {C : Type u} [CategoryTheory.Category.{v, u} C] (out : ∀ (J : Type) [Finite J], CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WidePullbackShape J) C) : CategoryTheory.Limits.HasFiniteWidePullbacks C
• CategoryTheory.Limits.HasFiniteWidePullbacks.out 📋 Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits
  {C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} [self : CategoryTheory.Limits.HasFiniteWidePullbacks C] (J : Type) [Finite J] : CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WidePullbackShape J) C
• CategoryTheory.Limits.WidePullbackShape.fintypeHom 📋 Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits
  {J : Type v} (j j' : CategoryTheory.Limits.WidePullbackShape J) : Fintype (j ⟶ j')
• CategoryTheory.Limits.opSpan_hom_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) (X✝ : CategoryTheory.Limits.WalkingSpanᵒᵖ) : (CategoryTheory.Limits.opSpan f g).hom.app X✝ = (match Opposite.unop X✝ with | none => CategoryTheory.Iso.refl (Opposite.op X) | some CategoryTheory.Limits.WalkingPair.left => CategoryTheory.Iso.refl (Opposite.op Y) | some CategoryTheory.Limits.WalkingPair.right => CategoryTheory.Iso.refl (Opposite.op Z)).inv
• CategoryTheory.Limits.opSpan_inv_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) (X✝ : CategoryTheory.Limits.WalkingSpanᵒᵖ) : (CategoryTheory.Limits.opSpan f g).inv.app X✝ = (match Opposite.unop X✝ with | none => CategoryTheory.Iso.refl (Opposite.op X) | some CategoryTheory.Limits.WalkingPair.left => CategoryTheory.Iso.refl (Opposite.op Y) | some CategoryTheory.Limits.WalkingPair.right => CategoryTheory.Iso.refl (Opposite.op Z)).hom
• CategoryTheory.WithTerminal.widePullbackShapeEquiv 📋 Mathlib.CategoryTheory.WithTerminal.Basic
  {J : Type u_1} : CategoryTheory.Limits.WidePullbackShape J ≌ CategoryTheory.WithTerminal (CategoryTheory.Discrete J)
• CategoryTheory.WithTerminal.widePullbackShapeEquiv_functor_obj 📋 Mathlib.CategoryTheory.WithTerminal.Basic
  {J : Type u_1} (a : CategoryTheory.Limits.WidePullbackShape J) : CategoryTheory.WithTerminal.widePullbackShapeEquiv.functor.obj a = match a with | some x => CategoryTheory.WithTerminal.of { as := x } | none => CategoryTheory.WithTerminal.star
• CategoryTheory.WithTerminal.widePullbackShapeEquiv_inverse_obj 📋 Mathlib.CategoryTheory.WithTerminal.Basic
  {J : Type u_1} (a : CategoryTheory.WithTerminal (CategoryTheory.Discrete J)) : CategoryTheory.WithTerminal.widePullbackShapeEquiv.inverse.obj a = CategoryTheory.WithTerminal.widePullbackShapeEquivObj✝.symm a
• CategoryTheory.widePullbackShape_connected 📋 Mathlib.CategoryTheory.Limits.Connected
  (J : Type v₁) : CategoryTheory.IsConnected (CategoryTheory.Limits.WidePullbackShape J)
• CategoryTheory.Subobject.wideCospan 📋 Mathlib.CategoryTheory.Subobject.Lattice
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.LocallySmall.{w, v₁, u₁} C] [CategoryTheory.WellPowered.{w, v₁, u₁} C] {A : C} (s : Set (CategoryTheory.Subobject A)) : CategoryTheory.Functor (CategoryTheory.Limits.WidePullbackShape ↑(⇑(equivShrink (CategoryTheory.Subobject A)) '' s)) C
• CategoryTheory.Subobject.leInfCone 📋 Mathlib.CategoryTheory.Subobject.Lattice
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.LocallySmall.{w, v₁, u₁} C] [CategoryTheory.WellPowered.{w, v₁, u₁} C] {A : C} (s : Set (CategoryTheory.Subobject A)) (f : CategoryTheory.Subobject A) (k : ∀ g ∈ s, f ≤ g) : CategoryTheory.Limits.Cone (CategoryTheory.Subobject.wideCospan s)
• CategoryTheory.Subobject.wideCospan_map_term 📋 Mathlib.CategoryTheory.Subobject.Lattice
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.LocallySmall.{w, v₁, u₁} C] [CategoryTheory.WellPowered.{w, v₁, u₁} C] {A : C} (s : Set (CategoryTheory.Subobject A)) (j : ↑(⇑(equivShrink (CategoryTheory.Subobject A)) '' s)) : (CategoryTheory.Subobject.wideCospan s).map (CategoryTheory.Limits.WidePullbackShape.Hom.term j) = ((equivShrink (CategoryTheory.Subobject A)).symm ↑j).arrow
• CategoryTheory.Subobject.leInfCone_π_app_none 📋 Mathlib.CategoryTheory.Subobject.Lattice
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.LocallySmall.{w, v₁, u₁} C] [CategoryTheory.WellPowered.{w, v₁, u₁} C] {A : C} (s : Set (CategoryTheory.Subobject A)) (f : CategoryTheory.Subobject A) (k : ∀ g ∈ s, f ≤ g) : (CategoryTheory.Subobject.leInfCone s f k).π.app none = f.arrow
• CategoryTheory.Limits.Concrete.widePullback_ext' 📋 Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type (max v w)} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [CategoryTheory.ConcreteCategory C FC] {B : C} {ι : Type w} [Nonempty ι] {X : ι → C} (f : (j : ι) → X j ⟶ B) [CategoryTheory.Limits.HasWidePullback B X f] [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.WidePullbackShape.wideCospan B X f) (CategoryTheory.forget C)] (x y : CategoryTheory.ToType (CategoryTheory.Limits.widePullback B X f)) (h : ∀ (j : ι), (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.WidePullback.π f j)) x = (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.WidePullback.π f j)) y) : x = y
• CategoryTheory.Limits.Concrete.widePullback_ext 📋 Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type (max v w)} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [CategoryTheory.ConcreteCategory C FC] {B : C} {ι : Type w} {X : ι → C} (f : (j : ι) → X j ⟶ B) [CategoryTheory.Limits.HasWidePullback B X f] [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.WidePullbackShape.wideCospan B X f) (CategoryTheory.forget C)] (x y : CategoryTheory.ToType (CategoryTheory.Limits.widePullback B X f)) (h₀ : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.WidePullback.base f)) x = (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.WidePullback.base f)) y) (h : ∀ (j : ι), (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.WidePullback.π f j)) x = (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.WidePullback.π f j)) y) : x = y
• CategoryTheory.instIsConnectedWidePullbackShape 📋 Mathlib.CategoryTheory.Limits.Shapes.Connected
  {J : Type u_1} : CategoryTheory.IsConnected (CategoryTheory.Limits.WidePullbackShape J)
• CategoryTheory.Over.ConstructProducts.over_product_of_widePullback 📋 Mathlib.CategoryTheory.Limits.Constructions.Over.Products
  {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WidePullbackShape J) C] {B : C} : CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Discrete J) (CategoryTheory.Over B)
• CategoryTheory.Over.ConstructProducts.widePullbackDiagramOfDiagramOver 📋 Mathlib.CategoryTheory.Limits.Constructions.Over.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] (B : C) {J : Type w} (F : CategoryTheory.Functor (CategoryTheory.Discrete J) (CategoryTheory.Over B)) : CategoryTheory.Functor (CategoryTheory.Limits.WidePullbackShape J) C
• CategoryTheory.Over.ConstructProducts.conesEquivInverseObj 📋 Mathlib.CategoryTheory.Limits.Constructions.Over.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] (B : C) {J : Type w} (F : CategoryTheory.Functor (CategoryTheory.Discrete J) (CategoryTheory.Over B)) (c : CategoryTheory.Limits.Cone F) : CategoryTheory.Limits.Cone (CategoryTheory.Over.ConstructProducts.widePullbackDiagramOfDiagramOver B F)
• CategoryTheory.Over.ConstructProducts.has_over_limit_discrete_of_widePullback_limit 📋 Mathlib.CategoryTheory.Limits.Constructions.Over.Products
  {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {B : C} (F : CategoryTheory.Functor (CategoryTheory.Discrete J) (CategoryTheory.Over B)) [CategoryTheory.Limits.HasLimit (CategoryTheory.Over.ConstructProducts.widePullbackDiagramOfDiagramOver B F)] : CategoryTheory.Limits.HasLimit F
• CategoryTheory.Over.ConstructProducts.conesEquiv 📋 Mathlib.CategoryTheory.Limits.Constructions.Over.Products
  {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] (B : C) (F : CategoryTheory.Functor (CategoryTheory.Discrete J) (CategoryTheory.Over B)) : CategoryTheory.Limits.Cone (CategoryTheory.Over.ConstructProducts.widePullbackDiagramOfDiagramOver B F) ≌ CategoryTheory.Limits.Cone F
• CategoryTheory.Over.ConstructProducts.conesEquivFunctor 📋 Mathlib.CategoryTheory.Limits.Constructions.Over.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] (B : C) {J : Type w} (F : CategoryTheory.Functor (CategoryTheory.Discrete J) (CategoryTheory.Over B)) : CategoryTheory.Functor (CategoryTheory.Limits.Cone (CategoryTheory.Over.ConstructProducts.widePullbackDiagramOfDiagramOver B F)) (CategoryTheory.Limits.Cone F)
• CategoryTheory.Over.ConstructProducts.conesEquivInverse 📋 Mathlib.CategoryTheory.Limits.Constructions.Over.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] (B : C) {J : Type w} (F : CategoryTheory.Functor (CategoryTheory.Discrete J) (CategoryTheory.Over B)) : CategoryTheory.Functor (CategoryTheory.Limits.Cone F) (CategoryTheory.Limits.Cone (CategoryTheory.Over.ConstructProducts.widePullbackDiagramOfDiagramOver B F))
• CategoryTheory.Over.ConstructProducts.conesEquivInverseObj_pt 📋 Mathlib.CategoryTheory.Limits.Constructions.Over.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] (B : C) {J : Type w} (F : CategoryTheory.Functor (CategoryTheory.Discrete J) (CategoryTheory.Over B)) (c : CategoryTheory.Limits.Cone F) : (CategoryTheory.Over.ConstructProducts.conesEquivInverseObj B F c).pt = c.pt.left
• CategoryTheory.Over.ConstructProducts.conesEquivInverse_obj 📋 Mathlib.CategoryTheory.Limits.Constructions.Over.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] (B : C) {J : Type w} (F : CategoryTheory.Functor (CategoryTheory.Discrete J) (CategoryTheory.Over B)) (c : CategoryTheory.Limits.Cone F) : (CategoryTheory.Over.ConstructProducts.conesEquivInverse B F).obj c = CategoryTheory.Over.ConstructProducts.conesEquivInverseObj B F c
• CategoryTheory.Over.ConstructProducts.conesEquiv_functor 📋 Mathlib.CategoryTheory.Limits.Constructions.Over.Products
  {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] (B : C) (F : CategoryTheory.Functor (CategoryTheory.Discrete J) (CategoryTheory.Over B)) : (CategoryTheory.Over.ConstructProducts.conesEquiv B F).functor = CategoryTheory.Over.ConstructProducts.conesEquivFunctor B F
• CategoryTheory.Over.ConstructProducts.conesEquiv_inverse 📋 Mathlib.CategoryTheory.Limits.Constructions.Over.Products
  {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] (B : C) (F : CategoryTheory.Functor (CategoryTheory.Discrete J) (CategoryTheory.Over B)) : (CategoryTheory.Over.ConstructProducts.conesEquiv B F).inverse = CategoryTheory.Over.ConstructProducts.conesEquivInverse B F
• CategoryTheory.Over.ConstructProducts.conesEquivFunctor_obj_pt 📋 Mathlib.CategoryTheory.Limits.Constructions.Over.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] (B : C) {J : Type w} (F : CategoryTheory.Functor (CategoryTheory.Discrete J) (CategoryTheory.Over B)) (c : CategoryTheory.Limits.Cone (CategoryTheory.Over.ConstructProducts.widePullbackDiagramOfDiagramOver B F)) : ((CategoryTheory.Over.ConstructProducts.conesEquivFunctor B F).obj c).pt = CategoryTheory.Over.mk (c.π.app none)
• CategoryTheory.Over.ConstructProducts.conesEquivUnitIso 📋 Mathlib.CategoryTheory.Limits.Constructions.Over.Products
  {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] (B : C) (F : CategoryTheory.Functor (CategoryTheory.Discrete J) (CategoryTheory.Over B)) : CategoryTheory.Functor.id (CategoryTheory.Limits.Cone (CategoryTheory.Over.ConstructProducts.widePullbackDiagramOfDiagramOver B F)) ≅ (CategoryTheory.Over.ConstructProducts.conesEquivFunctor B F).comp (CategoryTheory.Over.ConstructProducts.conesEquivInverse B F)
• CategoryTheory.Over.ConstructProducts.conesEquivCounitIso 📋 Mathlib.CategoryTheory.Limits.Constructions.Over.Products
  {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] (B : C) (F : CategoryTheory.Functor (CategoryTheory.Discrete J) (CategoryTheory.Over B)) : (CategoryTheory.Over.ConstructProducts.conesEquivInverse B F).comp (CategoryTheory.Over.ConstructProducts.conesEquivFunctor B F) ≅ CategoryTheory.Functor.id (CategoryTheory.Limits.Cone F)
• CategoryTheory.Over.ConstructProducts.conesEquivInverse_map_hom 📋 Mathlib.CategoryTheory.Limits.Constructions.Over.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] (B : C) {J : Type w} (F : CategoryTheory.Functor (CategoryTheory.Discrete J) (CategoryTheory.Over B)) {X✝ Y✝ : CategoryTheory.Limits.Cone F} (f : X✝ ⟶ Y✝) : ((CategoryTheory.Over.ConstructProducts.conesEquivInverse B F).map f).hom = CategoryTheory.Over.Hom.left f.hom
• CategoryTheory.Over.ConstructProducts.conesEquiv_unitIso 📋 Mathlib.CategoryTheory.Limits.Constructions.Over.Products
  {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] (B : C) (F : CategoryTheory.Functor (CategoryTheory.Discrete J) (CategoryTheory.Over B)) : (CategoryTheory.Over.ConstructProducts.conesEquiv B F).unitIso = CategoryTheory.Over.ConstructProducts.conesEquivUnitIso B F
• CategoryTheory.Over.ConstructProducts.conesEquiv_counitIso 📋 Mathlib.CategoryTheory.Limits.Constructions.Over.Products
  {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] (B : C) (F : CategoryTheory.Functor (CategoryTheory.Discrete J) (CategoryTheory.Over B)) : (CategoryTheory.Over.ConstructProducts.conesEquiv B F).counitIso = CategoryTheory.Over.ConstructProducts.conesEquivCounitIso B F
• CategoryTheory.Over.ConstructProducts.conesEquivInverseObj_π_app 📋 Mathlib.CategoryTheory.Limits.Constructions.Over.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] (B : C) {J : Type w} (F : CategoryTheory.Functor (CategoryTheory.Discrete J) (CategoryTheory.Over B)) (c : CategoryTheory.Limits.Cone F) (X : CategoryTheory.Limits.WidePullbackShape J) : (CategoryTheory.Over.ConstructProducts.conesEquivInverseObj B F c).π.app X = Option.casesOn X c.pt.hom fun j => CategoryTheory.Over.Hom.left (c.π.app { as := j })
• CategoryTheory.Over.ConstructProducts.conesEquivUnitIso_hom_app_hom 📋 Mathlib.CategoryTheory.Limits.Constructions.Over.Products
  {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] (B : C) (F : CategoryTheory.Functor (CategoryTheory.Discrete J) (CategoryTheory.Over B)) (X : CategoryTheory.Limits.Cone (CategoryTheory.Over.ConstructProducts.widePullbackDiagramOfDiagramOver B F)) : ((CategoryTheory.Over.ConstructProducts.conesEquivUnitIso B F).hom.app X).hom = CategoryTheory.CategoryStruct.id X.pt
• CategoryTheory.Over.ConstructProducts.conesEquivUnitIso_inv_app_hom 📋 Mathlib.CategoryTheory.Limits.Constructions.Over.Products
  {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] (B : C) (F : CategoryTheory.Functor (CategoryTheory.Discrete J) (CategoryTheory.Over B)) (X : CategoryTheory.Limits.Cone (CategoryTheory.Over.ConstructProducts.widePullbackDiagramOfDiagramOver B F)) : ((CategoryTheory.Over.ConstructProducts.conesEquivUnitIso B F).inv.app X).hom = CategoryTheory.CategoryStruct.id X.pt
• CategoryTheory.Over.ConstructProducts.conesEquivFunctor_obj_π_app 📋 Mathlib.CategoryTheory.Limits.Constructions.Over.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] (B : C) {J : Type w} (F : CategoryTheory.Functor (CategoryTheory.Discrete J) (CategoryTheory.Over B)) (c : CategoryTheory.Limits.Cone (CategoryTheory.Over.ConstructProducts.widePullbackDiagramOfDiagramOver B F)) (x✝ : CategoryTheory.Discrete J) : ((CategoryTheory.Over.ConstructProducts.conesEquivFunctor B F).obj c).π.app x✝ = match x✝ with | { as := j } => CategoryTheory.Over.homMk (c.π.app (some j)) ⋯
• CategoryTheory.Over.ConstructProducts.conesEquivCounitIso_inv_app_hom_left 📋 Mathlib.CategoryTheory.Limits.Constructions.Over.Products
  {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] (B : C) (F : CategoryTheory.Functor (CategoryTheory.Discrete J) (CategoryTheory.Over B)) (X : CategoryTheory.Limits.Cone F) : ((CategoryTheory.Over.ConstructProducts.conesEquivCounitIso B F).inv.app X).hom.left = CategoryTheory.CategoryStruct.id X.pt.left
• CategoryTheory.Over.ConstructProducts.conesEquivCounitIso_hom_app_hom_left 📋 Mathlib.CategoryTheory.Limits.Constructions.Over.Products
  {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] (B : C) (F : CategoryTheory.Functor (CategoryTheory.Discrete J) (CategoryTheory.Over B)) (X : CategoryTheory.Limits.Cone F) : ((CategoryTheory.Over.ConstructProducts.conesEquivCounitIso B F).hom.app X).hom.left = CategoryTheory.CategoryStruct.id X.pt.left
• CategoryTheory.Over.ConstructProducts.conesEquivFunctor_map_hom 📋 Mathlib.CategoryTheory.Limits.Constructions.Over.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] (B : C) {J : Type w} (F : CategoryTheory.Functor (CategoryTheory.Discrete J) (CategoryTheory.Over B)) {X✝ Y✝ : CategoryTheory.Limits.Cone (CategoryTheory.Over.ConstructProducts.widePullbackDiagramOfDiagramOver B F)} (f : X✝ ⟶ Y✝) : ((CategoryTheory.Over.ConstructProducts.conesEquivFunctor B F).map f).hom = CategoryTheory.Over.homMk f.hom ⋯
• CategoryTheory.CechNerveTerminalFrom.wideCospan 📋 Mathlib.AlgebraicTopology.CechNerve
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasTerminal C] (ι : Type w) (X : C) : CategoryTheory.Functor (CategoryTheory.Limits.WidePullbackShape ι) C
• CategoryTheory.CechNerveTerminalFrom.hasLimit_wideCospan 📋 Mathlib.AlgebraicTopology.CechNerve
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasTerminal C] (ι : Type w) [CategoryTheory.Limits.HasFiniteProducts C] [Finite ι] (X : C) : CategoryTheory.Limits.HasLimit (CategoryTheory.CechNerveTerminalFrom.wideCospan ι X)
• CategoryTheory.CechNerveTerminalFrom.wideCospan.limitCone 📋 Mathlib.AlgebraicTopology.CechNerve
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasTerminal C] (ι : Type w) [CategoryTheory.Limits.HasFiniteProducts C] [Finite ι] (X : C) : CategoryTheory.Limits.LimitCone (CategoryTheory.CechNerveTerminalFrom.wideCospan ι X)
• CategoryTheory.CechNerveTerminalFrom.uniqueToWideCospanNone 📋 Mathlib.AlgebraicTopology.CechNerve
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasTerminal C] (ι : Type w) (X Y : C) : Unique (Y ⟶ (CategoryTheory.CechNerveTerminalFrom.wideCospan ι X).obj none)
• CategoryTheory.CechNerveTerminalFrom.wideCospan.limitIsoPi 📋 Mathlib.AlgebraicTopology.CechNerve
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasTerminal C] (ι : Type w) [CategoryTheory.Limits.HasFiniteProducts C] [Finite ι] (X : C) : CategoryTheory.Limits.limit (CategoryTheory.CechNerveTerminalFrom.wideCospan ι X) ≅ ∏ᶜ fun x => X
• CategoryTheory.CechNerveTerminalFrom.wideCospan.limitIsoPi_hom_comp_pi 📋 Mathlib.AlgebraicTopology.CechNerve
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasTerminal C] (ι : Type w) [CategoryTheory.Limits.HasFiniteProducts C] [Finite ι] (X : C) (j : ι) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CechNerveTerminalFrom.wideCospan.limitIsoPi ι X).hom (CategoryTheory.Limits.Pi.π (fun x => X) j) = CategoryTheory.Limits.WidePullback.π (fun x => CategoryTheory.Limits.terminal.from X) j
• CategoryTheory.CechNerveTerminalFrom.wideCospan.limitIsoPi_inv_comp_pi 📋 Mathlib.AlgebraicTopology.CechNerve
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasTerminal C] (ι : Type w) [CategoryTheory.Limits.HasFiniteProducts C] [Finite ι] (X : C) (j : ι) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CechNerveTerminalFrom.wideCospan.limitIsoPi ι X).inv (CategoryTheory.Limits.WidePullback.π (fun x => CategoryTheory.Limits.terminal.from X) j) = CategoryTheory.Limits.Pi.π (fun x => X) j
• CategoryTheory.CechNerveTerminalFrom.wideCospan.limitIsoPi_hom_comp_pi_assoc 📋 Mathlib.AlgebraicTopology.CechNerve
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasTerminal C] (ι : Type w) [CategoryTheory.Limits.HasFiniteProducts C] [Finite ι] (X : C) (j : ι) {Z : C} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CechNerveTerminalFrom.wideCospan.limitIsoPi ι X).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π (fun x => X) j) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.WidePullback.π (fun x => CategoryTheory.Limits.terminal.from X) j) h
• CategoryTheory.CechNerveTerminalFrom.wideCospan.limitIsoPi_inv_comp_pi_assoc 📋 Mathlib.AlgebraicTopology.CechNerve
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasTerminal C] (ι : Type w) [CategoryTheory.Limits.HasFiniteProducts C] [Finite ι] (X : C) (j : ι) {Z : C} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CechNerveTerminalFrom.wideCospan.limitIsoPi ι X).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.WidePullback.π (fun x => CategoryTheory.Limits.terminal.from X) j) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π (fun x => X) j) h
• CategoryTheory.IsGrothendieckAbelian.isColimitMapCoconeOfSubobjectMkEqISup 📋 Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Subobject
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.IsGrothendieckAbelian.{w, v, u} C] {X : C} {J : Type w} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J (CategoryTheory.MonoOver X)) [CategoryTheory.IsFiltered J] (c : CategoryTheory.Limits.Cocone (F.comp (CategoryTheory.MonoOver.forget X))) [CategoryTheory.Mono c.pt.hom] (h : CategoryTheory.Subobject.mk c.pt.hom = ⨆ j, CategoryTheory.Subobject.mk (F.obj j).obj.hom) : CategoryTheory.Limits.IsColimit ((CategoryTheory.Over.forget X).mapCocone c)
• CategoryTheory.IsGrothendieckAbelian.subobjectMk_of_isColimit_eq_iSup 📋 Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Subobject
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.IsGrothendieckAbelian.{w, v, u} C] {X : C} {J : Type w} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J (CategoryTheory.MonoOver X)) [CategoryTheory.IsFiltered J] {c : CategoryTheory.Limits.Cocone (F.comp ((CategoryTheory.MonoOver.forget X).comp (CategoryTheory.Over.forget X)))} (hc : CategoryTheory.Limits.IsColimit c) (f : c.pt ⟶ X) (hf : ∀ (j : J), CategoryTheory.CategoryStruct.comp (c.ι.app j) f = (F.obj j).obj.hom) : CategoryTheory.Subobject.mk f = ⨆ j, CategoryTheory.Subobject.mk (F.obj j).obj.hom
• CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms.top_mem_range 📋 Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives
  {C : Type u} [CategoryTheory.Category.{v, u} C] {G : C} [CategoryTheory.Abelian C] (hG : CategoryTheory.IsSeparator G) {X : C} [CategoryTheory.IsGrothendieckAbelian.{w, v, u} C] (A₀ : CategoryTheory.Subobject X) {J : Type w} [LinearOrder J] [OrderBot J] [SuccOrder J] [WellFoundedLT J] (hJ : HasCardinalLT (CategoryTheory.Subobject X) (Cardinal.mk J)) : ∃ j, transfiniteIterate (CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms.largerSubobject hG) j A₀ = ⊤
• CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms.exists_ordinal 📋 Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives
  {C : Type u} [CategoryTheory.Category.{v, u} C] {G : C} [CategoryTheory.Abelian C] (hG : CategoryTheory.IsSeparator G) {X : C} [CategoryTheory.IsGrothendieckAbelian.{w, v, u} C] (A₀ : CategoryTheory.Subobject X) : ∃ o j, transfiniteIterate (CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms.largerSubobject hG) j A₀ = ⊤
• CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms.transfiniteCompositionOfShapeOfEqTop 📋 Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives
  {C : Type u} [CategoryTheory.Category.{v, u} C] {G : C} [CategoryTheory.Abelian C] (hG : CategoryTheory.IsSeparator G) {X : C} [CategoryTheory.IsGrothendieckAbelian.{w, v, u} C] {A : C} {f : A ⟶ X} [CategoryTheory.Mono f] {J : Type w} [LinearOrder J] [OrderBot J] [SuccOrder J] [WellFoundedLT J] {j : J} (hj : transfiniteIterate (CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms.largerSubobject hG) j (CategoryTheory.Subobject.mk f) = ⊤) : (CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms G).pushouts.TransfiniteCompositionOfShape (↑(Set.Iic j)) f
• CategoryTheory.Limits.WidePullbackCone.isLimitOfFan 📋 Mathlib.CategoryTheory.Limits.Constructions.WidePullbackOfTerminal
  {C : Type u} [CategoryTheory.Category.{v, u} C] {ι : Type w} {B : C} {objs : ι → C} (arrows : (j : ι) → objs j ⟶ B) {c : CategoryTheory.Limits.Fan objs} (hc : CategoryTheory.Limits.IsLimit c) (hB : CategoryTheory.Limits.IsTerminal B) : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.WidePullbackCone.ofFan arrows c hB)
• CategoryTheory.Limits.FormalCoproduct.instHasLimitWidePullbackShapeToTypeSimplexCategoryOrderHomFinHAddNatLenOfNatWideCospanObjInclFromIsTerminalIncl 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.ExtraDegeneracy
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] (U : CategoryTheory.Limits.FormalCoproduct C) {T : C} (hT : CategoryTheory.Limits.IsTerminal T) (n : SimplexCategory) : CategoryTheory.Limits.HasLimit (CategoryTheory.Limits.WidePullbackShape.wideCospan ((CategoryTheory.Limits.FormalCoproduct.incl C).obj T) (fun x => U) fun x => (CategoryTheory.Limits.FormalCoproduct.isTerminalIncl T hT).from U)
• CategoryTheory.Limits.PreservesLimitsOfShape.ofWidePullbacks 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.Over
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {J : Type u_1} [CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Limits.WidePullbackShape J) F] : CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.WithTerminal (CategoryTheory.Discrete J)) F

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