Loogle!

Result

Found 816 declarations mentioning CategoryTheory.Discrete.functor. Of these, only the first 200 are shown.

• CategoryTheory.Discrete.functor 📋 Mathlib.CategoryTheory.Discrete.Basic
  {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {I : Type u₁} (F : I → C) : CategoryTheory.Functor (CategoryTheory.Discrete I) C
• CategoryTheory.Discrete.functor_obj 📋 Mathlib.CategoryTheory.Discrete.Basic
  {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {I : Type u₁} (F : I → C) (i : I) : (CategoryTheory.Discrete.functor F).obj { as := i } = F i
• CategoryTheory.Discrete.functor_obj_eq_as 📋 Mathlib.CategoryTheory.Discrete.Basic
  {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {I : Type u₁} (F : I → C) (X : CategoryTheory.Discrete I) : (CategoryTheory.Discrete.functor F).obj X = F X.as
• CategoryTheory.Discrete.range_functor 📋 Mathlib.CategoryTheory.Discrete.Basic
  {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {I : Type u_1} (X : I → C) : Set.range (CategoryTheory.Discrete.functor X).obj = Set.range X
• CategoryTheory.Discrete.natIsoFunctor 📋 Mathlib.CategoryTheory.Discrete.Basic
  {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {I : Type u₁} {F : CategoryTheory.Functor (CategoryTheory.Discrete I) C} : F ≅ CategoryTheory.Discrete.functor (F.obj ∘ CategoryTheory.Discrete.mk)
• CategoryTheory.Discrete.equivalence_functor 📋 Mathlib.CategoryTheory.Discrete.Basic
  {I : Type u₁} {J : Type u₂} (e : I ≃ J) : (CategoryTheory.Discrete.equivalence e).functor = CategoryTheory.Discrete.functor (CategoryTheory.Discrete.mk ∘ ⇑e)
• CategoryTheory.Discrete.compNatIsoDiscrete 📋 Mathlib.CategoryTheory.Discrete.Basic
  {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {I : Type u₁} {D : Type u₃} [CategoryTheory.Category.{v₃, u₃} D] (F : I → C) (G : CategoryTheory.Functor C D) : (CategoryTheory.Discrete.functor F).comp G ≅ CategoryTheory.Discrete.functor (G.obj ∘ F)
• CategoryTheory.Discrete.equivalence_inverse 📋 Mathlib.CategoryTheory.Discrete.Basic
  {I : Type u₁} {J : Type u₂} (e : I ≃ J) : (CategoryTheory.Discrete.equivalence e).inverse = CategoryTheory.Discrete.functor (CategoryTheory.Discrete.mk ∘ ⇑e.symm)
• CategoryTheory.Discrete.functorComp 📋 Mathlib.CategoryTheory.Discrete.Basic
  {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {I : Type u₁} {J : Type u₁'} (f : J → C) (g : I → J) : CategoryTheory.Discrete.functor (f ∘ g) ≅ (CategoryTheory.Discrete.functor (CategoryTheory.Discrete.mk ∘ g)).comp (CategoryTheory.Discrete.functor f)
• CategoryTheory.piEquivalenceFunctorDiscrete_functor_obj 📋 Mathlib.CategoryTheory.Discrete.Basic
  (J : Type u₂) (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (F : J → C) : (CategoryTheory.piEquivalenceFunctorDiscrete J C).functor.obj F = CategoryTheory.Discrete.functor F
• CategoryTheory.Discrete.functor_map 📋 Mathlib.CategoryTheory.Discrete.Basic
  {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {I : Type u₁} (F : I → C) {i : CategoryTheory.Discrete I} (f : i ⟶ i) : (CategoryTheory.Discrete.functor F).map f = CategoryTheory.CategoryStruct.id (F i.as)
• CategoryTheory.Discrete.natIsoFunctor_hom_app 📋 Mathlib.CategoryTheory.Discrete.Basic
  {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {I : Type u₁} {F : CategoryTheory.Functor (CategoryTheory.Discrete I) C} (X : CategoryTheory.Discrete I) : CategoryTheory.Discrete.natIsoFunctor.hom.app X = CategoryTheory.CategoryStruct.id (F.obj X)
• CategoryTheory.Discrete.natIsoFunctor_inv_app 📋 Mathlib.CategoryTheory.Discrete.Basic
  {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {I : Type u₁} {F : CategoryTheory.Functor (CategoryTheory.Discrete I) C} (X : CategoryTheory.Discrete I) : CategoryTheory.Discrete.natIsoFunctor.inv.app X = CategoryTheory.CategoryStruct.id (F.obj X)
• CategoryTheory.piEquivalenceFunctorDiscrete_functor_map 📋 Mathlib.CategoryTheory.Discrete.Basic
  (J : Type u₂) (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] {X✝ Y✝ : J → C} (f : X✝ ⟶ Y✝) : (CategoryTheory.piEquivalenceFunctorDiscrete J C).functor.map f = CategoryTheory.Discrete.natTrans fun j => f j.as
• CategoryTheory.Discrete.compNatIsoDiscrete_hom_app 📋 Mathlib.CategoryTheory.Discrete.Basic
  {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {I : Type u₁} {D : Type u₃} [CategoryTheory.Category.{v₃, u₃} D] (F : I → C) (G : CategoryTheory.Functor C D) (X : CategoryTheory.Discrete I) : (CategoryTheory.Discrete.compNatIsoDiscrete F G).hom.app X = CategoryTheory.CategoryStruct.id (G.obj (F X.as))
• CategoryTheory.Discrete.compNatIsoDiscrete_inv_app 📋 Mathlib.CategoryTheory.Discrete.Basic
  {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {I : Type u₁} {D : Type u₃} [CategoryTheory.Category.{v₃, u₃} D] (F : I → C) (G : CategoryTheory.Functor C D) (X : CategoryTheory.Discrete I) : (CategoryTheory.Discrete.compNatIsoDiscrete F G).inv.app X = CategoryTheory.CategoryStruct.id (G.obj (F X.as))
• CategoryTheory.Discrete.functorComp_hom_app 📋 Mathlib.CategoryTheory.Discrete.Basic
  {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {I : Type u₁} {J : Type u₁'} (f : J → C) (g : I → J) (X : CategoryTheory.Discrete I) : (CategoryTheory.Discrete.functorComp f g).hom.app X = CategoryTheory.CategoryStruct.id (f (g X.as))
• CategoryTheory.Discrete.functorComp_inv_app 📋 Mathlib.CategoryTheory.Discrete.Basic
  {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {I : Type u₁} {J : Type u₁'} (f : J → C) (g : I → J) (X : CategoryTheory.Discrete I) : (CategoryTheory.Discrete.functorComp f g).inv.app X = CategoryTheory.CategoryStruct.id (f (g X.as))
• CategoryTheory.Discrete.equivalence_counitIso 📋 Mathlib.CategoryTheory.Discrete.Basic
  {I : Type u₁} {J : Type u₂} (e : I ≃ J) : (CategoryTheory.Discrete.equivalence e).counitIso = CategoryTheory.Discrete.natIso fun j => CategoryTheory.eqToIso ⋯
• CategoryTheory.Discrete.equivalence_unitIso 📋 Mathlib.CategoryTheory.Discrete.Basic
  {I : Type u₁} {J : Type u₂} (e : I ≃ J) : (CategoryTheory.Discrete.equivalence e).unitIso = CategoryTheory.Discrete.natIso fun i => CategoryTheory.eqToIso ⋯
• CategoryTheory.piEquivalenceFunctorDiscrete_counitIso 📋 Mathlib.CategoryTheory.Discrete.Basic
  (J : Type u₂) (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] : (CategoryTheory.piEquivalenceFunctorDiscrete J C).counitIso = CategoryTheory.NatIso.ofComponents (fun F => CategoryTheory.NatIso.ofComponents (fun x => CategoryTheory.Iso.refl ((({ obj := fun F j => F.obj { as := j }, map := fun {X Y} f j => f.app { as := j }, map_id := ⋯, map_comp := ⋯ }.comp { obj := fun F => CategoryTheory.Discrete.functor F, map := fun {X Y} f => CategoryTheory.Discrete.natTrans fun j => f j.as, map_id := ⋯, map_comp := ⋯ }).obj F).obj x)) ⋯) ⋯
• CategoryTheory.typeToCat_map 📋 Mathlib.CategoryTheory.Category.Cat
  {X✝ Y✝ : Type u} (f : X✝ ⟶ Y✝) : CategoryTheory.typeToCat.map f = (CategoryTheory.Discrete.functor (CategoryTheory.Discrete.mk ∘ ⇑(CategoryTheory.ConcreteCategory.hom f))).toCatHom
• CategoryTheory.Limits.colimitCoconeOfUnique 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [Unique β] (f : β → C) : CategoryTheory.Limits.ColimitCocone (CategoryTheory.Discrete.functor f)
• CategoryTheory.Limits.limitConeOfUnique 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [Unique β] (f : β → C) : CategoryTheory.Limits.LimitCone (CategoryTheory.Discrete.functor f)
• CategoryTheory.Limits.hasCoproducts_of_colimit_cofans 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] (cf : {J : Type w} → (f : J → C) → CategoryTheory.Limits.Cofan f) (cf_isColimit : {J : Type w} → (f : J → C) → CategoryTheory.Limits.IsColimit (cf f)) : CategoryTheory.Limits.HasCoproducts C
• CategoryTheory.Limits.hasProducts_of_limit_fans 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] (lf : {J : Type w} → (f : J → C) → CategoryTheory.Limits.Fan f) (lf_isLimit : {J : Type w} → (f : J → C) → CategoryTheory.Limits.IsLimit (lf f)) : CategoryTheory.Limits.HasProducts C
• CategoryTheory.Limits.Cofan.inj 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {f : β → C} (p : CategoryTheory.Limits.Cofan f) (j : β) : f j ⟶ p.pt
• CategoryTheory.Limits.Fan.proj 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {f : β → C} (p : CategoryTheory.Limits.Fan f) (j : β) : p.pt ⟶ f j
• CategoryTheory.Limits.coproductIsCoproduct 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] (f : β → C) [CategoryTheory.Limits.HasCoproduct f] : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Cofan.mk (∐ f) (CategoryTheory.Limits.Sigma.ι f))
• CategoryTheory.Limits.productIsProduct 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] (f : β → C) [CategoryTheory.Limits.HasProduct f] : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Fan.mk (∏ᶜ f) (CategoryTheory.Limits.Pi.π f))
• CategoryTheory.Limits.Cofan.isColimitMkOfUnique 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (e : X ≅ Y) (J : Type u_1) [Unique J] : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Cofan.mk Y fun x => e.hom)
• CategoryTheory.Limits.Cofan.mk_pt 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {f : β → C} (P : C) (p : (b : β) → f b ⟶ P) : (CategoryTheory.Limits.Cofan.mk P p).pt = P
• CategoryTheory.Limits.Fan.isLimitMkOfUnique 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (e : X ≅ Y) (J : Type u_1) [Unique J] : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Fan.mk X fun x => e.hom)
• CategoryTheory.Limits.Fan.mk_pt 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {f : β → C} (P : C) (p : (b : β) → P ⟶ f b) : (CategoryTheory.Limits.Fan.mk P p).pt = P
• CategoryTheory.Limits.colimitCoconeOfUnique_cocone_pt 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [Unique β] (f : β → C) : (CategoryTheory.Limits.colimitCoconeOfUnique f).cocone.pt = f default
• CategoryTheory.Limits.limitConeOfUnique_cone_pt 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [Unique β] (f : β → C) : (CategoryTheory.Limits.limitConeOfUnique f).cone.pt = f default
• CategoryTheory.Limits.Cofan.IsColimit.desc 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {F : β → C} {c : CategoryTheory.Limits.Cofan F} (hc : CategoryTheory.Limits.IsColimit c) {A : C} (f : (i : β) → F i ⟶ A) : c.pt ⟶ A
• CategoryTheory.Limits.Fan.IsLimit.lift 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {F : β → C} {c : CategoryTheory.Limits.Fan F} (hc : CategoryTheory.Limits.IsLimit c) {A : C} (f : (i : β) → A ⟶ F i) : A ⟶ c.pt
• CategoryTheory.Limits.Pi.mapIso 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {f g : β → C} [CategoryTheory.Limits.HasProductsOfShape β C] (p : (b : β) → f b ≅ g b) : ∏ᶜ f ≅ ∏ᶜ g
• CategoryTheory.Limits.Sigma.mapIso 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {f g : β → C} [CategoryTheory.Limits.HasCoproductsOfShape β C] (p : (b : β) → f b ≅ g b) : ∐ f ≅ ∐ g
• CategoryTheory.Limits.cofan_mk_inj 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {f : β → C} (P : C) (p : (b : β) → f b ⟶ P) : (CategoryTheory.Limits.Cofan.mk P p).inj = p
• CategoryTheory.Limits.fan_mk_proj 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {f : β → C} (P : C) (p : (b : β) → P ⟶ f b) : (CategoryTheory.Limits.Fan.mk P p).proj = p
• CategoryTheory.Limits.Cofan.isColimitOfIsIsoSigmaDesc 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {f : β → C} [CategoryTheory.Limits.HasCoproduct f] (c : CategoryTheory.Limits.Cofan f) [hc : CategoryTheory.IsIso (CategoryTheory.Limits.Sigma.desc c.inj)] : CategoryTheory.Limits.IsColimit c
• CategoryTheory.Limits.Fan.isLimitOfIsIsoPiLift 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {f : β → C} [CategoryTheory.Limits.HasProduct f] (c : CategoryTheory.Limits.Fan f) [hc : CategoryTheory.IsIso (CategoryTheory.Limits.Pi.lift c.proj)] : CategoryTheory.Limits.IsLimit c
• CategoryTheory.Limits.Cofan.nonempty_isColimit_iff_isIso_sigmaDesc 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {f : β → C} [CategoryTheory.Limits.HasCoproduct f] (c : CategoryTheory.Limits.Cofan f) : Nonempty (CategoryTheory.Limits.IsColimit c) ↔ CategoryTheory.IsIso (CategoryTheory.Limits.Sigma.desc c.inj)
• CategoryTheory.Limits.Fan.nonempty_isLimit_iff_isIso_piLift 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {f : β → C} [CategoryTheory.Limits.HasProduct f] (c : CategoryTheory.Limits.Fan f) : Nonempty (CategoryTheory.Limits.IsLimit c) ↔ CategoryTheory.IsIso (CategoryTheory.Limits.Pi.lift c.proj)
• CategoryTheory.Limits.Cofan.IsColimit.fac 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {F : β → C} {c : CategoryTheory.Limits.Cofan F} (hc : CategoryTheory.Limits.IsColimit c) {A : C} (f : (i : β) → F i ⟶ A) (i : β) : CategoryTheory.CategoryStruct.comp (c.inj i) (CategoryTheory.Limits.Cofan.IsColimit.desc hc f) = f i
• CategoryTheory.Limits.Fan.IsLimit.fac 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {F : β → C} {c : CategoryTheory.Limits.Fan F} (hc : CategoryTheory.Limits.IsLimit c) {A : C} (f : (i : β) → A ⟶ F i) (i : β) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fan.IsLimit.lift hc f) (c.proj i) = f i
• CategoryTheory.Limits.Cofan.mk_ι_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {f : β → C} (P : C) (p : (b : β) → f b ⟶ P) (X : CategoryTheory.Discrete β) : (CategoryTheory.Limits.Cofan.mk P p).ι.app X = p X.as
• CategoryTheory.Limits.Fan.mk_π_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {f : β → C} (P : C) (p : (b : β) → P ⟶ f b) (X : CategoryTheory.Discrete β) : (CategoryTheory.Limits.Fan.mk P p).π.app X = p X.as
• CategoryTheory.Limits.isColimitEquivCofanOfIsThin 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] [Quiver.IsThin C] {J : Type u_1} [CategoryTheory.Category.{v_1, u_1} J] {K : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cocone K) : CategoryTheory.Limits.IsColimit c ≃ CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Cofan.mk c.pt c.ι.app)
• CategoryTheory.Limits.isLimitEquivFanOfIsThin 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] [Quiver.IsThin C] {J : Type u_1} [CategoryTheory.Category.{v_1, u_1} J] {K : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cone K) : CategoryTheory.Limits.IsLimit c ≃ CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Fan.mk c.pt c.π.app)
• CategoryTheory.Limits.Pi.map_isIso 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {f g : β → C} [CategoryTheory.Limits.HasProductsOfShape β C] (p : (b : β) → f b ⟶ g b) [∀ (b : β), CategoryTheory.IsIso (p b)] : CategoryTheory.IsIso (CategoryTheory.Limits.Pi.map p)
• CategoryTheory.Limits.Sigma.map_isIso 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {f g : β → C} [CategoryTheory.Limits.HasCoproductsOfShape β C] (p : (b : β) → f b ⟶ g b) [∀ (b : β), CategoryTheory.IsIso (p b)] : CategoryTheory.IsIso (CategoryTheory.Limits.Sigma.map p)
• CategoryTheory.Limits.Cofan.IsColimit.inj_desc 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X : β → C} {c : CategoryTheory.Limits.Cofan X} (d : CategoryTheory.Limits.Cofan X) (hc : CategoryTheory.Limits.IsColimit c) (i : β) : CategoryTheory.CategoryStruct.comp (c.inj i) (hc.desc d) = d.inj i
• CategoryTheory.Limits.Fan.IsLimit.lift_proj 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X : β → C} {c : CategoryTheory.Limits.Fan X} (d : CategoryTheory.Limits.Fan X) (hc : CategoryTheory.Limits.IsLimit c) (i : β) : CategoryTheory.CategoryStruct.comp (hc.lift d) (c.proj i) = d.proj i
• CategoryTheory.Limits.Cofan.isColimitEquivOfEquiv 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {γ : Type w'} (ε : β ≃ γ) {f : γ → C} (c : CategoryTheory.Limits.Cofan f) : CategoryTheory.Limits.IsColimit c ≃ CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Cofan.mk c.pt fun i => c.inj (ε i))
• CategoryTheory.Limits.Fan.isLimitEquivOfEquiv 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {γ : Type w'} (ε : β ≃ γ) {f : γ → C} (c : CategoryTheory.Limits.Fan f) : CategoryTheory.Limits.IsLimit c ≃ CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Fan.mk c.pt fun i => c.proj (ε i))
• CategoryTheory.Limits.Cofan.IsColimit.fac_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {F : β → C} {c : CategoryTheory.Limits.Cofan F} (hc : CategoryTheory.Limits.IsColimit c) {A : C} (f : (i : β) → F i ⟶ A) (i : β) {Z : C} (h : A ⟶ Z) : CategoryTheory.CategoryStruct.comp (c.inj i) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Cofan.IsColimit.desc hc f) h) = CategoryTheory.CategoryStruct.comp (f i) h
• CategoryTheory.Limits.Fan.IsLimit.fac_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {F : β → C} {c : CategoryTheory.Limits.Fan F} (hc : CategoryTheory.Limits.IsLimit c) {A : C} (f : (i : β) → A ⟶ F i) (i : β) {Z : C} (h : F i ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fan.IsLimit.lift hc f) (CategoryTheory.CategoryStruct.comp (c.proj i) h) = CategoryTheory.CategoryStruct.comp (f i) h
• CategoryTheory.Limits.Cofan.isColimitMapCoconeEquiv 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) {ι : Type u_1} (X : ι → C) (c : CategoryTheory.Limits.Cofan X) : CategoryTheory.Limits.IsColimit (F.mapCocone c) ≃ CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Cofan.mk (F.obj c.pt) fun i => F.map (c.inj i))
• CategoryTheory.Limits.Fan.isLimitMapConeEquiv 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) {ι : Type u_1} (X : ι → C) (c : CategoryTheory.Limits.Fan X) : CategoryTheory.Limits.IsLimit (F.mapCone c) ≃ CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Fan.mk (F.obj c.pt) fun i => F.map (c.proj i))
• CategoryTheory.Limits.Pi.constCompPiIsoConst 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {α : Type w₂} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProductsOfShape α C] {I : α → Type u_1} [(i : α) → CategoryTheory.Category.{v_1, u_1} (I i)] (X : α → C) : (CategoryTheory.Functor.pi fun i => (CategoryTheory.Functor.const (I i)).obj (X i)).comp (CategoryTheory.Limits.Pi.functor α) ≅ (CategoryTheory.Functor.const ((i : α) → I i)).obj (∏ᶜ X)
• CategoryTheory.Limits.Sigma.constCompSigmaIsoConst 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {α : Type w₂} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproductsOfShape α C] {I : α → Type u_1} [(i : α) → CategoryTheory.Category.{v_1, u_1} (I i)] (X : α → C) : (CategoryTheory.Functor.pi fun i => (CategoryTheory.Functor.const (I i)).obj (X i)).comp (CategoryTheory.Limits.Sigma.functor α) ≅ (CategoryTheory.Functor.const ((i : α) → I i)).obj (∐ X)
• CategoryTheory.Limits.Cofan.IsColimit.hom_ext 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] {I : Type u_1} {F : I → C} {c : CategoryTheory.Limits.Cofan F} (hc : CategoryTheory.Limits.IsColimit c) {A : C} (f g : c.pt ⟶ A) (h : ∀ (i : I), CategoryTheory.CategoryStruct.comp (c.inj i) f = CategoryTheory.CategoryStruct.comp (c.inj i) g) : f = g
• CategoryTheory.Limits.Fan.IsLimit.hom_ext 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] {I : Type u_1} {F : I → C} {c : CategoryTheory.Limits.Fan F} (hc : CategoryTheory.Limits.IsLimit c) {A : C} (f g : A ⟶ c.pt) (h : ∀ (i : I), CategoryTheory.CategoryStruct.comp f (c.proj i) = CategoryTheory.CategoryStruct.comp g (c.proj i)) : f = g
• CategoryTheory.Limits.Cofan.ext 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {f : β → C} {c₁ c₂ : CategoryTheory.Limits.Cofan f} (e : c₁.pt ≅ c₂.pt) (w : ∀ (b : β), CategoryTheory.CategoryStruct.comp (c₁.inj b) e.hom = c₂.inj b := by cat_disch) : c₁ ≅ c₂
• CategoryTheory.Limits.Fan.ext 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {f : β → C} {c₁ c₂ : CategoryTheory.Limits.Fan f} (e : c₁.pt ≅ c₂.pt) (w : ∀ (b : β), c₁.proj b = CategoryTheory.CategoryStruct.comp e.hom (c₂.proj b) := by cat_disch) : c₁ ≅ c₂
• CategoryTheory.Limits.Cofan.IsColimit.inj_desc_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X : β → C} {c : CategoryTheory.Limits.Cofan X} (d : CategoryTheory.Limits.Cofan X) (hc : CategoryTheory.Limits.IsColimit c) (i : β) {Z : C} (h : d.pt ⟶ Z) : CategoryTheory.CategoryStruct.comp (c.inj i) (CategoryTheory.CategoryStruct.comp (hc.desc d) h) = CategoryTheory.CategoryStruct.comp (d.inj i) h
• CategoryTheory.Limits.Fan.IsLimit.lift_proj_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X : β → C} {c : CategoryTheory.Limits.Fan X} (d : CategoryTheory.Limits.Fan X) (hc : CategoryTheory.Limits.IsLimit c) (i : β) {Z : C} (h : X i ⟶ Z) : CategoryTheory.CategoryStruct.comp (hc.lift d) (CategoryTheory.CategoryStruct.comp (c.proj i) h) = CategoryTheory.CategoryStruct.comp (d.proj i) h
• CategoryTheory.Limits.Pi.mapIso_hom_π 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {f g : β → C} [CategoryTheory.Limits.HasProductsOfShape β C] (p : (b : β) → f b ≅ g b) (b : β) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.mapIso p).hom (CategoryTheory.Limits.Pi.π g b) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π f b) (p b).hom
• CategoryTheory.Limits.Pi.mapIso_inv_π 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {f g : β → C} [CategoryTheory.Limits.HasProductsOfShape β C] (p : (b : β) → f b ≅ g b) (b : β) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.mapIso p).inv (CategoryTheory.Limits.Pi.π f b) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π g b) (p b).inv
• CategoryTheory.Limits.Sigma.ι_mapIso_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {f g : β → C} [CategoryTheory.Limits.HasCoproductsOfShape β C] (p : (b : β) → f b ≅ g b) (b : β) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι f b) (CategoryTheory.Limits.Sigma.mapIso p).hom = CategoryTheory.CategoryStruct.comp (p b).hom (CategoryTheory.Limits.Sigma.ι g b)
• CategoryTheory.Limits.Sigma.ι_mapIso_inv 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {f g : β → C} [CategoryTheory.Limits.HasCoproductsOfShape β C] (p : (b : β) → f b ≅ g b) (b : β) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι g b) (CategoryTheory.Limits.Sigma.mapIso p).inv = CategoryTheory.CategoryStruct.comp (p b).inv (CategoryTheory.Limits.Sigma.ι f b)
• CategoryTheory.Limits.Cofan.ext_hom_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {f : β → C} {c₁ c₂ : CategoryTheory.Limits.Cofan f} (e : c₁.pt ≅ c₂.pt) (w : ∀ (b : β), CategoryTheory.CategoryStruct.comp (c₁.inj b) e.hom = c₂.inj b := by cat_disch) : (CategoryTheory.Limits.Cofan.ext e w).hom.hom = e.hom
• CategoryTheory.Limits.Cofan.ext_inv_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {f : β → C} {c₁ c₂ : CategoryTheory.Limits.Cofan f} (e : c₁.pt ≅ c₂.pt) (w : ∀ (b : β), CategoryTheory.CategoryStruct.comp (c₁.inj b) e.hom = c₂.inj b := by cat_disch) : (CategoryTheory.Limits.Cofan.ext e w).inv.hom = e.inv
• CategoryTheory.Limits.Fan.ext_hom_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {f : β → C} {c₁ c₂ : CategoryTheory.Limits.Fan f} (e : c₁.pt ≅ c₂.pt) (w : ∀ (b : β), c₁.proj b = CategoryTheory.CategoryStruct.comp e.hom (c₂.proj b) := by cat_disch) : (CategoryTheory.Limits.Fan.ext e w).hom.hom = e.hom
• CategoryTheory.Limits.Fan.ext_inv_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {f : β → C} {c₁ c₂ : CategoryTheory.Limits.Fan f} (e : c₁.pt ≅ c₂.pt) (w : ∀ (b : β), c₁.proj b = CategoryTheory.CategoryStruct.comp e.hom (c₂.proj b) := by cat_disch) : (CategoryTheory.Limits.Fan.ext e w).inv.hom = e.inv
• CategoryTheory.Limits.Pi.mapIso_hom_π_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {f g : β → C} [CategoryTheory.Limits.HasProductsOfShape β C] (p : (b : β) → f b ≅ g b) (b : β) {Z : C} (h : g b ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.mapIso p).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π g b) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π f b) (CategoryTheory.CategoryStruct.comp (p b).hom h)
• CategoryTheory.Limits.Pi.mapIso_inv_π_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {f g : β → C} [CategoryTheory.Limits.HasProductsOfShape β C] (p : (b : β) → f b ≅ g b) (b : β) {Z : C} (h : f b ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.mapIso p).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π f b) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π g b) (CategoryTheory.CategoryStruct.comp (p b).inv h)
• CategoryTheory.Limits.Sigma.ι_mapIso_hom_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {f g : β → C} [CategoryTheory.Limits.HasCoproductsOfShape β C] (p : (b : β) → f b ≅ g b) (b : β) {Z : C} (h : ∐ g ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι f b) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.mapIso p).hom h) = CategoryTheory.CategoryStruct.comp (p b).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι g b) h)
• CategoryTheory.Limits.Sigma.ι_mapIso_inv_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {f g : β → C} [CategoryTheory.Limits.HasCoproductsOfShape β C] (p : (b : β) → f b ≅ g b) (b : β) {Z : C} (h : ∐ f ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι g b) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.mapIso p).inv h) = CategoryTheory.CategoryStruct.comp (p b).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι f b) h)
• CategoryTheory.Limits.Cofan.isColimitTrans 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {α : Type w₂} {C : Type u} [CategoryTheory.Category.{v, u} C] {X : α → C} (c : CategoryTheory.Limits.Cofan X) (hc : CategoryTheory.Limits.IsColimit c) {β : α → Type u_1} {Y : (a : α) → β a → C} (π : (a : α) → (b : β a) → Y a b ⟶ X a) (hs : (a : α) → CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Cofan.mk (X a) (π a))) : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Cofan.mk c.pt fun x => match x with | ⟨a, b⟩ => CategoryTheory.CategoryStruct.comp (π a b) (c.inj a))
• CategoryTheory.Limits.colimitCoconeOfUnique_cocone_ι 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [Unique β] (f : β → C) : (CategoryTheory.Limits.colimitCoconeOfUnique f).cocone.ι = CategoryTheory.Discrete.natTrans fun x => match x with | { as := j } => CategoryTheory.eqToHom ⋯
• CategoryTheory.Limits.limitConeOfUnique_cone_π 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [Unique β] (f : β → C) : (CategoryTheory.Limits.limitConeOfUnique f).cone.π = CategoryTheory.Discrete.natTrans fun x => match x with | { as := j } => CategoryTheory.eqToHom ⋯
• CategoryTheory.Limits.Cofan.IsColimit.prod 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] {ι : Type u_1} {ι' : Type u_2} {X : ι → ι' → C} (c : (i : ι) → CategoryTheory.Limits.Cofan fun j => X i j) (hc : (i : ι) → CategoryTheory.Limits.IsColimit (c i)) (c' : CategoryTheory.Limits.Cofan fun i => (c i).pt) (hc' : CategoryTheory.Limits.IsColimit c') : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Cofan.mk c'.pt fun p => CategoryTheory.CategoryStruct.comp ((c p.1).inj p.2) (c'.inj p.1))
• CategoryTheory.Limits.Fan.IsLimit.prod 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] {ι : Type u_1} {ι' : Type u_2} {X : ι → ι' → C} (c : (i : ι) → CategoryTheory.Limits.Fan fun j => X i j) (hc : (i : ι) → CategoryTheory.Limits.IsLimit (c i)) (c' : CategoryTheory.Limits.Fan fun i => (c i).pt) (hc' : CategoryTheory.Limits.IsLimit c') : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Fan.mk c'.pt fun p => CategoryTheory.CategoryStruct.comp (c'.proj p.1) ((c p.1).proj p.2))
• CategoryTheory.Limits.mkCofanColimit 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {f : β → C} (s : CategoryTheory.Limits.Cofan f) (desc : (t : CategoryTheory.Limits.Cofan f) → s.pt ⟶ t.pt) (fac : ∀ (t : CategoryTheory.Limits.Cofan f) (j : β), CategoryTheory.CategoryStruct.comp (s.inj j) (desc t) = t.inj j := by cat_disch) (uniq : ∀ (t : CategoryTheory.Limits.Cofan f) (m : s.pt ⟶ t.pt), (∀ (j : β), CategoryTheory.CategoryStruct.comp (s.inj j) m = t.inj j) → m = desc t := by cat_disch) : CategoryTheory.Limits.IsColimit s
• CategoryTheory.Limits.mkFanLimit 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {f : β → C} (t : CategoryTheory.Limits.Fan f) (lift : (s : CategoryTheory.Limits.Fan f) → s.pt ⟶ t.pt) (fac : ∀ (s : CategoryTheory.Limits.Fan f) (j : β), CategoryTheory.CategoryStruct.comp (lift s) (t.proj j) = s.proj j := by cat_disch) (uniq : ∀ (s : CategoryTheory.Limits.Fan f) (m : s.pt ⟶ t.pt), (∀ (j : β), CategoryTheory.CategoryStruct.comp m (t.proj j) = s.proj j) → m = lift s := by cat_disch) : CategoryTheory.Limits.IsLimit t
• CategoryTheory.Limits.Cofan.IsColimit.mk 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {f : β → C} (s : CategoryTheory.Limits.Cofan f) (desc : (t : CategoryTheory.Limits.Cofan f) → s.pt ⟶ t.pt) (fac : ∀ (t : CategoryTheory.Limits.Cofan f) (j : β), CategoryTheory.CategoryStruct.comp (s.inj j) (desc t) = t.inj j := by cat_disch) (uniq : ∀ (t : CategoryTheory.Limits.Cofan f) (m : s.pt ⟶ t.pt), (∀ (j : β), CategoryTheory.CategoryStruct.comp (s.inj j) m = t.inj j) → m = desc t := by cat_disch) : CategoryTheory.Limits.IsColimit s
• CategoryTheory.Limits.Fan.IsLimit.mk 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {f : β → C} (t : CategoryTheory.Limits.Fan f) (lift : (s : CategoryTheory.Limits.Fan f) → s.pt ⟶ t.pt) (fac : ∀ (s : CategoryTheory.Limits.Fan f) (j : β), CategoryTheory.CategoryStruct.comp (lift s) (t.proj j) = s.proj j := by cat_disch) (uniq : ∀ (s : CategoryTheory.Limits.Fan f) (m : s.pt ⟶ t.pt), (∀ (j : β), CategoryTheory.CategoryStruct.comp m (t.proj j) = s.proj j) → m = lift s := by cat_disch) : CategoryTheory.Limits.IsLimit t
• CategoryTheory.Limits.piEquivalenceFunctorDiscreteCompColim_hom_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  (α : Type w₂) {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproductsOfShape α C] (X : α → C) : (CategoryTheory.Limits.piEquivalenceFunctorDiscreteCompColim α).hom.app X = CategoryTheory.CategoryStruct.id (CategoryTheory.Limits.colimit (CategoryTheory.Discrete.functor X))
• CategoryTheory.Limits.piEquivalenceFunctorDiscreteCompColim_inv_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  (α : Type w₂) {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproductsOfShape α C] (X : α → C) : (CategoryTheory.Limits.piEquivalenceFunctorDiscreteCompColim α).inv.app X = CategoryTheory.CategoryStruct.id (CategoryTheory.Limits.colimit (CategoryTheory.Discrete.functor X))
• CategoryTheory.Limits.piEquivalenceFunctorDiscreteCompLim_hom_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  (α : Type w₂) {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProductsOfShape α C] (X : α → C) : (CategoryTheory.Limits.piEquivalenceFunctorDiscreteCompLim α).hom.app X = CategoryTheory.CategoryStruct.id (CategoryTheory.Limits.limit (CategoryTheory.Discrete.functor X))
• CategoryTheory.Limits.piEquivalenceFunctorDiscreteCompLim_inv_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  (α : Type w₂) {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProductsOfShape α C] (X : α → C) : (CategoryTheory.Limits.piEquivalenceFunctorDiscreteCompLim α).inv.app X = CategoryTheory.CategoryStruct.id (CategoryTheory.Limits.limit (CategoryTheory.Discrete.functor X))
• CategoryTheory.Limits.Cofan.IsColimit.mk_desc 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {f : β → C} (s : CategoryTheory.Limits.Cofan f) (desc : (t : CategoryTheory.Limits.Cofan f) → s.pt ⟶ t.pt) (fac : ∀ (t : CategoryTheory.Limits.Cofan f) (j : β), CategoryTheory.CategoryStruct.comp (s.inj j) (desc t) = t.inj j := by cat_disch) (uniq : ∀ (t : CategoryTheory.Limits.Cofan f) (m : s.pt ⟶ t.pt), (∀ (j : β), CategoryTheory.CategoryStruct.comp (s.inj j) m = t.inj j) → m = desc t := by cat_disch) (t : CategoryTheory.Limits.Cofan f) : (CategoryTheory.Limits.Cofan.IsColimit.mk s desc fac uniq).desc t = desc t
• CategoryTheory.Limits.Fan.IsLimit.mk_lift 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {f : β → C} (t : CategoryTheory.Limits.Fan f) (lift : (s : CategoryTheory.Limits.Fan f) → s.pt ⟶ t.pt) (fac : ∀ (s : CategoryTheory.Limits.Fan f) (j : β), CategoryTheory.CategoryStruct.comp (lift s) (t.proj j) = s.proj j := by cat_disch) (uniq : ∀ (s : CategoryTheory.Limits.Fan f) (m : s.pt ⟶ t.pt), (∀ (j : β), CategoryTheory.CategoryStruct.comp m (t.proj j) = s.proj j) → m = lift s := by cat_disch) (s : CategoryTheory.Limits.Fan f) : (CategoryTheory.Limits.Fan.IsLimit.mk t lift fac uniq).lift s = lift s
• CategoryTheory.Limits.colimitCoconeOfUnique_isColimit_desc 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [Unique β] (f : β → C) (s : CategoryTheory.Limits.Cocone (CategoryTheory.Discrete.functor f)) : (CategoryTheory.Limits.colimitCoconeOfUnique f).isColimit.desc s = s.ι.app default
• CategoryTheory.Limits.limitConeOfUnique_isLimit_lift 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [Unique β] (f : β → C) (s : CategoryTheory.Limits.Cone (CategoryTheory.Discrete.functor f)) : (CategoryTheory.Limits.limitConeOfUnique f).isLimit.lift s = s.π.app default
• CategoryTheory.Limits.Pi.constCompPiIsoConst_hom_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {α : Type w₂} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProductsOfShape α C] {I : α → Type u_1} [(i : α) → CategoryTheory.Category.{v_1, u_1} (I i)] (X : α → C) (X✝ : (i : α) → I i) : (CategoryTheory.Limits.Pi.constCompPiIsoConst X).hom.app X✝ = CategoryTheory.CategoryStruct.id (∏ᶜ fun i => X i)
• CategoryTheory.Limits.Pi.constCompPiIsoConst_inv_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {α : Type w₂} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProductsOfShape α C] {I : α → Type u_1} [(i : α) → CategoryTheory.Category.{v_1, u_1} (I i)] (X : α → C) (X✝ : (i : α) → I i) : (CategoryTheory.Limits.Pi.constCompPiIsoConst X).inv.app X✝ = CategoryTheory.CategoryStruct.id (∏ᶜ fun i => X i)
• CategoryTheory.Limits.Sigma.constCompSigmaIsoConst_hom_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {α : Type w₂} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproductsOfShape α C] {I : α → Type u_1} [(i : α) → CategoryTheory.Category.{v_1, u_1} (I i)] (X : α → C) (X✝ : (i : α) → I i) : (CategoryTheory.Limits.Sigma.constCompSigmaIsoConst X).hom.app X✝ = CategoryTheory.CategoryStruct.id (∐ fun i => X i)
• CategoryTheory.Limits.Sigma.constCompSigmaIsoConst_inv_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {α : Type w₂} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproductsOfShape α C] {I : α → Type u_1} [(i : α) → CategoryTheory.Category.{v_1, u_1} (I i)] (X : α → C) (X✝ : (i : α) → I i) : (CategoryTheory.Limits.Sigma.constCompSigmaIsoConst X).inv.app X✝ = CategoryTheory.CategoryStruct.id (∐ fun i => X i)
• CategoryTheory.Limits.isSplitEpi_pi_π 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
  {C : Type u} [CategoryTheory.Category.{v, u} C] {β : Type u'} [CategoryTheory.Limits.HasZeroMorphisms C] (f : β → C) [CategoryTheory.Limits.HasLimit (CategoryTheory.Discrete.functor f)] (b : β) : CategoryTheory.IsSplitEpi (CategoryTheory.Limits.Pi.π f b)
• CategoryTheory.Limits.isSplitMono_sigma_ι 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
  {C : Type u} [CategoryTheory.Category.{v, u} C] {β : Type u'} [CategoryTheory.Limits.HasZeroMorphisms C] (f : β → C) [CategoryTheory.Limits.HasColimit (CategoryTheory.Discrete.functor f)] (b : β) : CategoryTheory.IsSplitMono (CategoryTheory.Limits.Sigma.ι f b)
• CategoryTheory.Limits.Bicone.toCocone 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
  {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {F : J → C} (B : CategoryTheory.Limits.Bicone F) : CategoryTheory.Limits.Cocone (CategoryTheory.Discrete.functor F)
• CategoryTheory.Limits.Bicone.toCone 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
  {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {F : J → C} (B : CategoryTheory.Limits.Bicone F) : CategoryTheory.Limits.Cone (CategoryTheory.Discrete.functor F)
• CategoryTheory.Limits.Bicone.ofColimitCocone 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
  {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {f : J → C} {t : CategoryTheory.Limits.Cocone (CategoryTheory.Discrete.functor f)} (ht : CategoryTheory.Limits.IsColimit t) : CategoryTheory.Limits.Bicone f
• CategoryTheory.Limits.Bicone.ofLimitCone 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
  {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {f : J → C} {t : CategoryTheory.Limits.Cone (CategoryTheory.Discrete.functor f)} (ht : CategoryTheory.Limits.IsLimit t) : CategoryTheory.Limits.Bicone f
• CategoryTheory.Limits.biproduct.isColimit 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
  {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] (F : J → C) [CategoryTheory.Limits.HasBiproduct F] : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.biproduct.bicone F).toCocone
• CategoryTheory.Limits.biproduct.isLimit 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
  {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] (F : J → C) [CategoryTheory.Limits.HasBiproduct F] : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.biproduct.bicone F).toCone
• CategoryTheory.Limits.Bicone.IsBilimit.isColimit 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
  {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {F : J → C} {B : CategoryTheory.Limits.Bicone F} (self : B.IsBilimit) : CategoryTheory.Limits.IsColimit B.toCocone
• CategoryTheory.Limits.Bicone.IsBilimit.isLimit 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
  {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {F : J → C} {B : CategoryTheory.Limits.Bicone F} (self : B.IsBilimit) : CategoryTheory.Limits.IsLimit B.toCone
• CategoryTheory.Limits.Bicone.toCocone_pt 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
  {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {F : J → C} (B : CategoryTheory.Limits.Bicone F) : B.toCocone.pt = B.pt
• CategoryTheory.Limits.Bicone.toCone_pt 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
  {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {F : J → C} (B : CategoryTheory.Limits.Bicone F) : B.toCone.pt = B.pt
• CategoryTheory.Limits.Bicone.toCoconeFunctor 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
  {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {F : J → C} : CategoryTheory.Functor (CategoryTheory.Limits.Bicone F) (CategoryTheory.Limits.Cocone (CategoryTheory.Discrete.functor F))
• CategoryTheory.Limits.Bicone.toConeFunctor 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
  {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {F : J → C} : CategoryTheory.Functor (CategoryTheory.Limits.Bicone F) (CategoryTheory.Limits.Cone (CategoryTheory.Discrete.functor F))
• CategoryTheory.Limits.Bicone.IsBilimit.mk 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
  {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {F : J → C} {B : CategoryTheory.Limits.Bicone F} (isLimit : CategoryTheory.Limits.IsLimit B.toCone) (isColimit : CategoryTheory.Limits.IsColimit B.toCocone) : B.IsBilimit
• CategoryTheory.Limits.Bicone.ofColimitCocone_pt 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
  {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {f : J → C} {t : CategoryTheory.Limits.Cocone (CategoryTheory.Discrete.functor f)} (ht : CategoryTheory.Limits.IsColimit t) : (CategoryTheory.Limits.Bicone.ofColimitCocone ht).pt = t.pt
• CategoryTheory.Limits.Bicone.ofLimitCone_pt 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
  {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {f : J → C} {t : CategoryTheory.Limits.Cone (CategoryTheory.Discrete.functor f)} (ht : CategoryTheory.Limits.IsLimit t) : (CategoryTheory.Limits.Bicone.ofLimitCone ht).pt = t.pt
• CategoryTheory.Limits.Bicone.toCocone_inj 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
  {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {F : J → C} (B : CategoryTheory.Limits.Bicone F) (j : J) : CategoryTheory.Limits.Cofan.inj B.toCocone j = B.ι j
• CategoryTheory.Limits.Bicone.toCone_proj 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
  {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {F : J → C} (B : CategoryTheory.Limits.Bicone F) (j : J) : CategoryTheory.Limits.Fan.proj B.toCone j = B.π j
• CategoryTheory.Limits.Bicone.IsBilimit.ext 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
  {J : Type w} {C : Type uC} {inst✝ : CategoryTheory.Category.{uC', uC} C} {inst✝¹ : CategoryTheory.Limits.HasZeroMorphisms C} {F : J → C} {B : CategoryTheory.Limits.Bicone F} {x y : B.IsBilimit} (isLimit : x.isLimit = y.isLimit) (isColimit : x.isColimit = y.isColimit) : x = y
• CategoryTheory.Limits.Bicone.IsBilimit.ext_iff 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
  {J : Type w} {C : Type uC} {inst✝ : CategoryTheory.Category.{uC', uC} C} {inst✝¹ : CategoryTheory.Limits.HasZeroMorphisms C} {F : J → C} {B : CategoryTheory.Limits.Bicone F} {x y : B.IsBilimit} : x = y ↔ x.isLimit = y.isLimit ∧ x.isColimit = y.isColimit
• CategoryTheory.Limits.limitBiconeOfUnique_isBilimit_isColimit 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
  {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [Unique J] (f : J → C) : (CategoryTheory.Limits.limitBiconeOfUnique f).isBilimit.isColimit = (CategoryTheory.Limits.colimitCoconeOfUnique f).isColimit
• CategoryTheory.Limits.limitBiconeOfUnique_isBilimit_isLimit 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
  {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [Unique J] (f : J → C) : (CategoryTheory.Limits.limitBiconeOfUnique f).isBilimit.isLimit = (CategoryTheory.Limits.limitConeOfUnique f).isLimit
• CategoryTheory.Limits.Bicone.ι_of_isLimit 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
  {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {f : J → C} {t : CategoryTheory.Limits.Bicone f} (ht : CategoryTheory.Limits.IsLimit t.toCone) (j : J) : t.ι j = ht.lift (CategoryTheory.Limits.Fan.mk (f j) fun j' => if h : j = j' then CategoryTheory.eqToHom ⋯ else 0)
• CategoryTheory.Limits.Bicone.π_of_isColimit 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
  {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {f : J → C} {t : CategoryTheory.Limits.Bicone f} (ht : CategoryTheory.Limits.IsColimit t.toCocone) (j : J) : t.π j = ht.desc (CategoryTheory.Limits.Cofan.mk (f j) fun j' => if h : j' = j then CategoryTheory.eqToHom ⋯ else 0)
• CategoryTheory.Limits.Bicone.toCocone_ι_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
  {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {F : J → C} (B : CategoryTheory.Limits.Bicone F) (j : CategoryTheory.Discrete J) : B.toCocone.ι.app j = B.ι j.as
• CategoryTheory.Limits.Bicone.toCone_π_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
  {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {F : J → C} (B : CategoryTheory.Limits.Bicone F) (j : CategoryTheory.Discrete J) : B.toCone.π.app j = B.π j.as
• CategoryTheory.Limits.Bicone.toCocone_ι_app_mk 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
  {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {F : J → C} (B : CategoryTheory.Limits.Bicone F) (j : J) : B.toCocone.ι.app { as := j } = B.ι j
• CategoryTheory.Limits.Bicone.toCone_π_app_mk 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
  {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {F : J → C} (B : CategoryTheory.Limits.Bicone F) (j : J) : B.toCone.π.app { as := j } = B.π j
• CategoryTheory.Limits.Bicone.ofColimitCocone_ι 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
  {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {f : J → C} {t : CategoryTheory.Limits.Cocone (CategoryTheory.Discrete.functor f)} (ht : CategoryTheory.Limits.IsColimit t) (j : J) : (CategoryTheory.Limits.Bicone.ofColimitCocone ht).ι j = t.ι.app { as := j }
• CategoryTheory.Limits.Bicone.ofLimitCone_π 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
  {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {f : J → C} {t : CategoryTheory.Limits.Cone (CategoryTheory.Discrete.functor f)} (ht : CategoryTheory.Limits.IsLimit t) (j : J) : (CategoryTheory.Limits.Bicone.ofLimitCone ht).π j = t.π.app { as := j }
• CategoryTheory.Limits.biproduct.conePointUniqueUpToIso_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
  {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (f : J → C) [CategoryTheory.Limits.HasBiproduct f] {b : CategoryTheory.Limits.Bicone f} (hb : b.IsBilimit) : (hb.isLimit.conePointUniqueUpToIso (CategoryTheory.Limits.biproduct.isLimit f)).hom = CategoryTheory.Limits.biproduct.lift b.π
• CategoryTheory.Limits.biproduct.conePointUniqueUpToIso_inv 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
  {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (f : J → C) [CategoryTheory.Limits.HasBiproduct f] {b : CategoryTheory.Limits.Bicone f} (hb : b.IsBilimit) : (hb.isLimit.conePointUniqueUpToIso (CategoryTheory.Limits.biproduct.isLimit f)).inv = CategoryTheory.Limits.biproduct.desc b.ι
• CategoryTheory.Limits.Bicone.ofColimitCocone_π 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
  {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {f : J → C} {t : CategoryTheory.Limits.Cocone (CategoryTheory.Discrete.functor f)} (ht : CategoryTheory.Limits.IsColimit t) (j : J) : (CategoryTheory.Limits.Bicone.ofColimitCocone ht).π j = ht.desc (CategoryTheory.Limits.Cofan.mk (f j) fun j' => if h : j' = j then CategoryTheory.eqToHom ⋯ else 0)
• CategoryTheory.Limits.Bicone.ofLimitCone_ι 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
  {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {f : J → C} {t : CategoryTheory.Limits.Cone (CategoryTheory.Discrete.functor f)} (ht : CategoryTheory.Limits.IsLimit t) (j : J) : (CategoryTheory.Limits.Bicone.ofLimitCone ht).ι j = ht.lift (CategoryTheory.Limits.Fan.mk (f j) fun j' => if h : j = j' then CategoryTheory.eqToHom ⋯ else 0)
• CategoryTheory.Limits.Bicone.whiskerToCocone 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
  {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {K : Type w'} {f : J → C} (c : CategoryTheory.Limits.Bicone f) (g : K ≃ J) : (c.whisker g).toCocone ≅ (CategoryTheory.Limits.Cocone.precompose (CategoryTheory.Discrete.functorComp f ⇑g).hom).obj (CategoryTheory.Limits.Cocone.whisker (CategoryTheory.Discrete.functor (CategoryTheory.Discrete.mk ∘ ⇑g)) c.toCocone)
• CategoryTheory.Limits.Bicone.whiskerToCone 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
  {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {K : Type w'} {f : J → C} (c : CategoryTheory.Limits.Bicone f) (g : K ≃ J) : (c.whisker g).toCone ≅ (CategoryTheory.Limits.Cone.postcompose (CategoryTheory.Discrete.functorComp f ⇑g).inv).obj (CategoryTheory.Limits.Cone.whisker (CategoryTheory.Discrete.functor (CategoryTheory.Discrete.mk ∘ ⇑g)) c.toCone)
• CategoryTheory.Limits.BinaryBicone.toBiconeIsColimit 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
  {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} (b : CategoryTheory.Limits.BinaryBicone X Y) : CategoryTheory.Limits.IsColimit b.toBicone.toCocone ≃ CategoryTheory.Limits.IsColimit b.toCocone
• CategoryTheory.Limits.BinaryBicone.toBiconeIsLimit 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
  {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} (b : CategoryTheory.Limits.BinaryBicone X Y) : CategoryTheory.Limits.IsLimit b.toBicone.toCone ≃ CategoryTheory.Limits.IsLimit b.toCone
• CategoryTheory.Limits.Bicone.toBinaryBiconeIsColimit 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
  {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} (b : CategoryTheory.Limits.Bicone (CategoryTheory.Limits.pairFunction X Y)) : CategoryTheory.Limits.IsColimit b.toBinaryBicone.toCocone ≃ CategoryTheory.Limits.IsColimit b.toCocone
• CategoryTheory.Limits.Bicone.toBinaryBiconeIsLimit 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
  {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} (b : CategoryTheory.Limits.Bicone (CategoryTheory.Limits.pairFunction X Y)) : CategoryTheory.Limits.IsLimit b.toBinaryBicone.toCone ≃ CategoryTheory.Limits.IsLimit b.toCone
• CategoryTheory.Limits.preservesColimitsOfShape_of_discrete 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.Products
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {J : Type w} (F : CategoryTheory.Functor C D) [∀ (f : J → C), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Discrete.functor f) F] : CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete J) F
• CategoryTheory.Limits.preservesLimitsOfShape_of_discrete 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.Products
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {J : Type w} (F : CategoryTheory.Functor C D) [∀ (f : J → C), CategoryTheory.Limits.PreservesLimit (CategoryTheory.Discrete.functor f) F] : CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete J) F
• CategoryTheory.Limits.PreservesCoproduct.iso 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.Products
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {J : Type w} (f : J → C) [CategoryTheory.Limits.HasCoproduct f] [CategoryTheory.Limits.HasCoproduct fun j => G.obj (f j)] [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Discrete.functor f) G] : G.obj (∐ f) ≅ ∐ fun j => G.obj (f j)
• CategoryTheory.Limits.PreservesProduct.iso 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.Products
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {J : Type w} (f : J → C) [CategoryTheory.Limits.HasProduct f] [CategoryTheory.Limits.HasProduct fun j => G.obj (f j)] [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Discrete.functor f) G] : G.obj (∏ᶜ f) ≅ ∏ᶜ fun j => G.obj (f j)
• CategoryTheory.Limits.instIsIsoPiComparison 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.Products
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {J : Type w} (f : J → C) [CategoryTheory.Limits.HasProduct f] [CategoryTheory.Limits.HasProduct fun j => G.obj (f j)] [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Discrete.functor f) G] : CategoryTheory.IsIso (CategoryTheory.Limits.piComparison G f)
• CategoryTheory.Limits.instIsIsoSigmaComparison 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.Products
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {J : Type w} (f : J → C) [CategoryTheory.Limits.HasCoproduct f] [CategoryTheory.Limits.HasCoproduct fun j => G.obj (f j)] [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Discrete.functor f) G] : CategoryTheory.IsIso (CategoryTheory.Limits.sigmaComparison G f)
• CategoryTheory.Limits.PreservesCoproduct.of_iso_comparison 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.Products
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {J : Type w} (f : J → C) [CategoryTheory.Limits.HasCoproduct f] [CategoryTheory.Limits.HasCoproduct fun j => G.obj (f j)] [i : CategoryTheory.IsIso (CategoryTheory.Limits.sigmaComparison G f)] : CategoryTheory.Limits.PreservesColimit (CategoryTheory.Discrete.functor f) G
• CategoryTheory.Limits.PreservesProduct.of_iso_comparison 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.Products
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {J : Type w} (f : J → C) [CategoryTheory.Limits.HasProduct f] [CategoryTheory.Limits.HasProduct fun j => G.obj (f j)] [i : CategoryTheory.IsIso (CategoryTheory.Limits.piComparison G f)] : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Discrete.functor f) G
• CategoryTheory.Limits.isColimitOfHasCoproductOfPreservesColimit 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.Products
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {J : Type w} (f : J → C) [CategoryTheory.Limits.HasCoproduct f] [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Discrete.functor f) G] : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Cofan.mk (G.obj (∐ f)) fun j => G.map (CategoryTheory.Limits.Sigma.ι f j))
• CategoryTheory.Limits.isLimitOfHasProductOfPreservesLimit 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.Products
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {J : Type w} (f : J → C) [CategoryTheory.Limits.HasProduct f] [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Discrete.functor f) G] : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Fan.mk (G.obj (∏ᶜ f)) fun j => G.map (CategoryTheory.Limits.Pi.π f j))
• CategoryTheory.Limits.isColimitCofanMkObjOfIsColimit 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.Products
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {J : Type w} (f : J → C) [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Discrete.functor f) G] {P : C} (g : (j : J) → f j ⟶ P) (t : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Cofan.mk P g)) : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Cofan.mk (G.obj P) fun j => G.map (g j))
• CategoryTheory.Limits.isColimitOfIsColimitCofanMkObj 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.Products
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {J : Type w} (f : J → C) [CategoryTheory.Limits.ReflectsColimit (CategoryTheory.Discrete.functor f) G] {P : C} (g : (j : J) → f j ⟶ P) (t : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Cofan.mk (G.obj P) fun j => G.map (g j))) : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Cofan.mk P g)
• CategoryTheory.Limits.isLimitFanMkObjOfIsLimit 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.Products
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {J : Type w} (f : J → C) [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Discrete.functor f) G] {P : C} (g : (j : J) → P ⟶ f j) (t : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Fan.mk P g)) : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Fan.mk (G.obj P) fun j => G.map (g j))
• CategoryTheory.Limits.isLimitOfIsLimitFanMkObj 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.Products
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {J : Type w} (f : J → C) [CategoryTheory.Limits.ReflectsLimit (CategoryTheory.Discrete.functor f) G] {P : C} (g : (j : J) → P ⟶ f j) (t : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Fan.mk (G.obj P) fun j => G.map (g j))) : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Fan.mk P g)
• CategoryTheory.Limits.isColimitMapCoconeCofanMkEquiv 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.Products
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {J : Type w} (f : J → C) {P : C} (g : (j : J) → f j ⟶ P) : CategoryTheory.Limits.IsColimit (G.mapCocone (CategoryTheory.Limits.Cofan.mk P g)) ≃ CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Cofan.mk (G.obj P) fun j => G.map (g j))
• CategoryTheory.Limits.isLimitMapConeFanMkEquiv 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.Products
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {J : Type w} (f : J → C) {P : C} (g : (j : J) → P ⟶ f j) : CategoryTheory.Limits.IsLimit (G.mapCone (CategoryTheory.Limits.Fan.mk P g)) ≃ CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Fan.mk (G.obj P) fun j => G.map (g j))
• CategoryTheory.Limits.PreservesCoproduct.inv_hom 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.Products
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {J : Type w} (f : J → C) [CategoryTheory.Limits.HasCoproduct f] [CategoryTheory.Limits.HasCoproduct fun j => G.obj (f j)] [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Discrete.functor f) G] : (CategoryTheory.Limits.PreservesCoproduct.iso G f).inv = CategoryTheory.Limits.sigmaComparison G f
• CategoryTheory.Limits.PreservesProduct.iso_hom 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.Products
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {J : Type w} (f : J → C) [CategoryTheory.Limits.HasProduct f] [CategoryTheory.Limits.HasProduct fun j => G.obj (f j)] [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Discrete.functor f) G] : (CategoryTheory.Limits.PreservesProduct.iso G f).hom = CategoryTheory.Limits.piComparison G f
• CategoryTheory.Limits.isBilimitOfIsColimit 📋 Mathlib.CategoryTheory.Preadditive.Biproducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {J : Type u_1} [Fintype J] {f : J → C} (t : CategoryTheory.Limits.Bicone f) (ht : CategoryTheory.Limits.IsColimit t.toCocone) : t.IsBilimit
• CategoryTheory.Limits.isBilimitOfIsLimit 📋 Mathlib.CategoryTheory.Preadditive.Biproducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {J : Type u_1} [Fintype J] {f : J → C} (t : CategoryTheory.Limits.Bicone f) (ht : CategoryTheory.Limits.IsLimit t.toCone) : t.IsBilimit
• CategoryTheory.Limits.biconeIsBilimitOfColimitCoconeOfIsColimit 📋 Mathlib.CategoryTheory.Preadditive.Biproducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {J : Type u_1} [Fintype J] {f : J → C} {t : CategoryTheory.Limits.Cocone (CategoryTheory.Discrete.functor f)} (ht : CategoryTheory.Limits.IsColimit t) : (CategoryTheory.Limits.Bicone.ofColimitCocone ht).IsBilimit
• CategoryTheory.Limits.biconeIsBilimitOfLimitConeOfIsLimit 📋 Mathlib.CategoryTheory.Preadditive.Biproducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {J : Type u_1} [Fintype J] {f : J → C} {t : CategoryTheory.Limits.Cone (CategoryTheory.Discrete.functor f)} (ht : CategoryTheory.Limits.IsLimit t) : (CategoryTheory.Limits.Bicone.ofLimitCone ht).IsBilimit
• CategoryTheory.Limits.preservesBiproduct_of_preservesCoproduct 📋 Mathlib.CategoryTheory.Preadditive.Biproducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] {J : Type u_1} [Finite J] {f : J → C} [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Discrete.functor f) F] : CategoryTheory.Limits.PreservesBiproduct f F
• CategoryTheory.Limits.preservesBiproduct_of_preservesProduct 📋 Mathlib.CategoryTheory.Preadditive.Biproducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] {J : Type u_1} [Finite J] {f : J → C} [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Discrete.functor f) F] : CategoryTheory.Limits.PreservesBiproduct f F
• CategoryTheory.Limits.preservesCoproduct_of_preservesBiproduct 📋 Mathlib.CategoryTheory.Preadditive.Biproducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] {J : Type u_1} [Finite J] {f : J → C} [CategoryTheory.Limits.PreservesBiproduct f F] : CategoryTheory.Limits.PreservesColimit (CategoryTheory.Discrete.functor f) F
• CategoryTheory.Limits.preservesProduct_of_preservesBiproduct 📋 Mathlib.CategoryTheory.Preadditive.Biproducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] {J : Type u_1} [Finite J] {f : J → C} [CategoryTheory.Limits.PreservesBiproduct f F] : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Discrete.functor f) F
• ModuleCat.finsuppCoconeIsColimit 📋 Mathlib.Algebra.Category.ModuleCat.Colimits
  (R : Type w) [CommRing R] (M ι : Type u) [AddCommGroup M] [Module R M] : CategoryTheory.Limits.IsColimit (ModuleCat.finsuppCocone R M ι)
• CommRingCat.piFanIsLimit 📋 Mathlib.Algebra.Category.Ring.Constructions
  {ι : Type u} (R : ι → CommRingCat) : CategoryTheory.Limits.IsLimit (CommRingCat.piFan R)
• CommRingCat.piFan_pt 📋 Mathlib.Algebra.Category.Ring.Constructions
  {ι : Type u} (R : ι → CommRingCat) : (CommRingCat.piFan R).pt = CommRingCat.of ((i : ι) → ↑(R i))
• CommRingCat.piIsoPi 📋 Mathlib.Algebra.Category.Ring.Constructions
  {ι : Type u} (R : ι → CommRingCat) : ∏ᶜ R ≅ CommRingCat.of ((i : ι) → ↑(R i))
• RingEquiv.piEquivPi 📋 Mathlib.Algebra.Category.Ring.Constructions
  {ι : Type u} (R : ι → Type u) [(i : ι) → CommRing (R i)] : ↑(∏ᶜ fun i => CommRingCat.of (R i)) ≃+* ((i : ι) → R i)
• CategoryTheory.Limits.Types.productLimitCone 📋 Mathlib.CategoryTheory.Limits.Types.Products
  {J : Type v} (F : J → Type (max v u)) : CategoryTheory.Limits.LimitCone (CategoryTheory.Discrete.functor F)
• CategoryTheory.Limits.Types.Small.productLimitCone 📋 Mathlib.CategoryTheory.Limits.Types.Products
  {J : Type v} (F : J → Type u) [Small.{u, v} J] : CategoryTheory.Limits.LimitCone (CategoryTheory.Discrete.functor F)
• CategoryTheory.Limits.Types.productIso 📋 Mathlib.CategoryTheory.Limits.Types.Products
  {J : Type v} (F : J → Type (max v u)) : ∏ᶜ F ≅ (j : J) → F j
• CategoryTheory.Limits.Types.Small.productIso 📋 Mathlib.CategoryTheory.Limits.Types.Products
  {J : Type v} (F : J → Type u) [Small.{u, v} J] : ∏ᶜ F ≅ Shrink.{u, max u v} ((j : J) → F j)
• CategoryTheory.Limits.Types.productIso_inv_comp_π 📋 Mathlib.CategoryTheory.Limits.Types.Products
  {J : Type v} (F : J → Type (max v u)) (j : J) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Types.productIso F).inv (CategoryTheory.Limits.Pi.π F j) = TypeCat.ofHom fun f => f j
• CategoryTheory.Limits.Types.productIso_hom_comp_eval 📋 Mathlib.CategoryTheory.Limits.Types.Products
  {J : Type v} (F : J → Type (max v u)) (j : J) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Types.productIso F).hom (TypeCat.ofHom fun f => f j) = CategoryTheory.Limits.Pi.π F j
• CategoryTheory.Limits.Types.Small.productIso_inv_comp_π 📋 Mathlib.CategoryTheory.Limits.Types.Products
  {J : Type v} (F : J → Type u) [Small.{u, v} J] (j : J) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Types.Small.productIso F).inv (CategoryTheory.Limits.Pi.π F j) = TypeCat.ofHom fun f => (equivShrink ((j : J) → F j)).symm f j
• CategoryTheory.Limits.Types.Small.productIso_hom_comp_eval 📋 Mathlib.CategoryTheory.Limits.Types.Products
  {J : Type v} (F : J → Type u) [Small.{u, v} J] (j : J) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Types.Small.productIso F).hom (TypeCat.ofHom fun f => (equivShrink ((j : J) → F j)).symm f j) = CategoryTheory.Limits.Pi.π F j
• CategoryTheory.Limits.Types.productIso_inv_comp_π_apply 📋 Mathlib.CategoryTheory.Limits.Types.Products
  {J : Type v} (F : J → Type (max v u)) (j : J) (x : (j : J) → F j) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Pi.π F j)) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Types.productIso F).inv) x) = x j
• CategoryTheory.Limits.Types.pi_lift_π_apply 📋 Mathlib.CategoryTheory.Limits.Types.Products
  {β : Type v} [Small.{u, v} β] (f : β → Type u) {P : Type u} (s : (b : β) → P ⟶ f b) (b : β) (x : P) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Pi.π f b)) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Pi.lift s)) x) = (CategoryTheory.ConcreteCategory.hom (s b)) x
• CategoryTheory.Limits.Types.pi_lift_π_apply' 📋 Mathlib.CategoryTheory.Limits.Types.Products
  {β : Type v} (f : β → Type v) {P : Type v} (s : (b : β) → P ⟶ f b) (b : β) (x : P) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Pi.π f b)) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Pi.lift s)) x) = (CategoryTheory.ConcreteCategory.hom (s b)) x
• CategoryTheory.Limits.Types.productIso_hom_comp_eval_apply 📋 Mathlib.CategoryTheory.Limits.Types.Products
  {J : Type v} (F : J → Type (max v u)) (j : J) (x : ∏ᶜ F) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Types.productIso F).hom) x j = (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Pi.π F j)) x
• CategoryTheory.Limits.Types.Small.productIso_inv_comp_π_apply 📋 Mathlib.CategoryTheory.Limits.Types.Products
  {J : Type v} (F : J → Type u) [Small.{u, v} J] (j : J) (x : Shrink.{u, max u v} ((j : J) → F j)) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Pi.π F j)) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Types.Small.productIso F).inv) x) = (equivShrink ((j : J) → F j)).symm x j
• CategoryTheory.Limits.Types.Small.productIso_hom_comp_eval_apply 📋 Mathlib.CategoryTheory.Limits.Types.Products
  {J : Type v} (F : J → Type u) [Small.{u, v} J] (j : J) (x : ∏ᶜ F) : (equivShrink ((j : J) → F j)).symm ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Types.Small.productIso F).hom) x) j = (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Pi.π F j)) x
• CategoryTheory.Limits.Types.pi_map_π_apply 📋 Mathlib.CategoryTheory.Limits.Types.Products
  {β : Type v} [Small.{u, v} β] {f g : β → Type u} (α : (j : β) → f j ⟶ g j) (b : β) (x : (fun X => X) (∏ᶜ f)) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Pi.π g b)) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Pi.map α)) x) = (CategoryTheory.ConcreteCategory.hom (α b)) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Pi.π f b)) x)
• CategoryTheory.Limits.Types.pi_map_π_apply' 📋 Mathlib.CategoryTheory.Limits.Types.Products
  {β : Type v} {f g : β → Type v} (α : (j : β) → f j ⟶ g j) (b : β) (x : (fun X => X) (∏ᶜ f)) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Pi.π g b)) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Pi.map α)) x) = (CategoryTheory.ConcreteCategory.hom (α b)) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Pi.π f b)) x)
• CategoryTheory.preservesFinOfPreservesBinaryAndTerminal 📋 Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) F] [CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete PEmpty.{1}) F] [CategoryTheory.Limits.HasFiniteProducts C] (n : ℕ) (f : Fin n → C) : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Discrete.functor f) F
• CategoryTheory.preserves_fin_of_preserves_binary_and_initial 📋 Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) F] [CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete PEmpty.{1}) F] [CategoryTheory.Limits.HasFiniteCoproducts C] (n : ℕ) (f : Fin n → C) : CategoryTheory.Limits.PreservesColimit (CategoryTheory.Discrete.functor f) F
• CategoryTheory.extendCofan 📋 Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] {n : ℕ} {f : Fin (n + 1) → C} (c₁ : CategoryTheory.Limits.Cofan fun i => f i.succ) (c₂ : CategoryTheory.Limits.BinaryCofan (f 0) c₁.pt) : CategoryTheory.Limits.Cofan f
• CategoryTheory.extendFan 📋 Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] {n : ℕ} {f : Fin (n + 1) → C} (c₁ : CategoryTheory.Limits.Fan fun i => f i.succ) (c₂ : CategoryTheory.Limits.BinaryFan (f 0) c₁.pt) : CategoryTheory.Limits.Fan f
• CategoryTheory.extendCofan_pt 📋 Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] {n : ℕ} {f : Fin (n + 1) → C} (c₁ : CategoryTheory.Limits.Cofan fun i => f i.succ) (c₂ : CategoryTheory.Limits.BinaryCofan (f 0) c₁.pt) : (CategoryTheory.extendCofan c₁ c₂).pt = c₂.pt
• CategoryTheory.extendFan_pt 📋 Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] {n : ℕ} {f : Fin (n + 1) → C} (c₁ : CategoryTheory.Limits.Fan fun i => f i.succ) (c₂ : CategoryTheory.Limits.BinaryFan (f 0) c₁.pt) : (CategoryTheory.extendFan c₁ c₂).pt = c₂.pt
• CategoryTheory.extendCofanIsColimit 📋 Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] {n : ℕ} (f : Fin (n + 1) → C) {c₁ : CategoryTheory.Limits.Cofan fun i => f i.succ} {c₂ : CategoryTheory.Limits.BinaryCofan (f 0) c₁.pt} (t₁ : CategoryTheory.Limits.IsColimit c₁) (t₂ : CategoryTheory.Limits.IsColimit c₂) : CategoryTheory.Limits.IsColimit (CategoryTheory.extendCofan c₁ c₂)
• CategoryTheory.extendFanIsLimit 📋 Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] {n : ℕ} (f : Fin (n + 1) → C) {c₁ : CategoryTheory.Limits.Fan fun i => f i.succ} {c₂ : CategoryTheory.Limits.BinaryFan (f 0) c₁.pt} (t₁ : CategoryTheory.Limits.IsLimit c₁) (t₂ : CategoryTheory.Limits.IsLimit c₂) : CategoryTheory.Limits.IsLimit (CategoryTheory.extendFan c₁ c₂)
• CategoryTheory.extendCofan_ι_app 📋 Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] {n : ℕ} {f : Fin (n + 1) → C} (c₁ : CategoryTheory.Limits.Cofan fun i => f i.succ) (c₂ : CategoryTheory.Limits.BinaryCofan (f 0) c₁.pt) (X : CategoryTheory.Discrete (Fin (n + 1))) : (CategoryTheory.extendCofan c₁ c₂).ι.app X = Fin.cases c₂.inl (fun i => CategoryTheory.CategoryStruct.comp (c₁.ι.app { as := i }) c₂.inr) X.as

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