Loogle!

Result

Found 275 declarations mentioning CategoryTheory.Limits.piObj. Of these, only the first 200 are shown.

• CategoryTheory.Limits.piObj 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] (f : β → C) [CategoryTheory.Limits.HasProduct f] : C
• CategoryTheory.Limits.Pi.π 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] (f : β → C) [CategoryTheory.Limits.HasProduct f] (b : β) : ∏ᶜ f ⟶ f b
• CategoryTheory.Limits.productUniqueIso 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [Unique β] (f : β → C) : ∏ᶜ f ≅ f default
• CategoryTheory.Limits.Pi.lift 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {f : β → C} [CategoryTheory.Limits.HasProduct f] {P : C} (p : (b : β) → P ⟶ f b) : P ⟶ ∏ᶜ 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.Pi.functor_obj 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  (α : Type w₂) {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProductsOfShape α C] (f : α → C) : (CategoryTheory.Limits.Pi.functor α).obj f = ∏ᶜ f
• CategoryTheory.Limits.Pi.map 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {f g : β → C} [CategoryTheory.Limits.HasProduct f] [CategoryTheory.Limits.HasProduct g] (p : (b : β) → f b ⟶ g b) : ∏ᶜ f ⟶ ∏ᶜ g
• CategoryTheory.Limits.Pi.map' 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {α : Type w₂} {C : Type u} [CategoryTheory.Category.{v, u} C] {f : α → C} {g : β → C} [CategoryTheory.Limits.HasProduct f] [CategoryTheory.Limits.HasProduct g] (p : β → α) (q : (b : β) → f (p b) ⟶ g b) : ∏ᶜ f ⟶ ∏ᶜ g
• CategoryTheory.Limits.instHasProductSigmaFstSndOfPiObj 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] {ι : Type u_1} (f : ι → Type u_2) (g : (i : ι) → f i → C) [∀ (i : ι), CategoryTheory.Limits.HasProduct (g i)] [CategoryTheory.Limits.HasProduct fun i => ∏ᶜ g i] : CategoryTheory.Limits.HasProduct fun p => g p.fst p.snd
• CategoryTheory.Limits.Pi.map_id 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {α : Type w₂} {C : Type u} [CategoryTheory.Category.{v, u} C] {f : α → C} [CategoryTheory.Limits.HasProduct f] : (CategoryTheory.Limits.Pi.map fun a => CategoryTheory.CategoryStruct.id (f a)) = CategoryTheory.CategoryStruct.id (∏ᶜ f)
• 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.piConst_obj_obj 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] (X : C) (n : Type wᵒᵖ) : (CategoryTheory.Limits.piConst.obj X).obj n = ∏ᶜ fun x => X
• CategoryTheory.Limits.piFunctor_obj_obj 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] (X : C) (α : Type wᵒᵖ) : (CategoryTheory.Limits.piFunctor.obj X).obj α = ∏ᶜ fun t => X
• CategoryTheory.Limits.Pi.cone_pt 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {α : Type w₂} {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.Functor (CategoryTheory.Discrete α) C) [CategoryTheory.Limits.HasProduct fun j => X.obj { as := j }] : (CategoryTheory.Limits.Pi.cone X).pt = ∏ᶜ fun j => X.obj { as := j }
• CategoryTheory.Limits.Pi.map'_id_id 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {α : Type w₂} {C : Type u} [CategoryTheory.Category.{v, u} C] {f : α → C} [CategoryTheory.Limits.HasProduct f] : (CategoryTheory.Limits.Pi.map' id fun a => CategoryTheory.CategoryStruct.id (f a)) = CategoryTheory.CategoryStruct.id (∏ᶜ f)
• CategoryTheory.Limits.Pi.whiskerEquiv 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type u_1} {K : Type u_2} {f : J → C} {g : K → C} (e : J ≃ K) (w : (j : J) → g (e j) ≅ f j) [CategoryTheory.Limits.HasProduct f] [CategoryTheory.Limits.HasProduct g] : ∏ᶜ f ≅ ∏ᶜ g
• CategoryTheory.Limits.Pi.isoLimit 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {α : Type w₂} {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.Functor (CategoryTheory.Discrete α) C) [CategoryTheory.Limits.HasProduct fun j => X.obj { as := j }] [CategoryTheory.Limits.HasLimit X] : (∏ᶜ fun j => X.obj { as := j }) ≅ CategoryTheory.Limits.limit X
• CategoryTheory.Limits.Pi.map_mono 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {f g : β → C} [CategoryTheory.Limits.HasProduct f] [CategoryTheory.Limits.HasProduct g] (p : (b : β) → f b ⟶ g b) [∀ (i : β), CategoryTheory.Mono (p i)] : CategoryTheory.Mono (CategoryTheory.Limits.Pi.map p)
• CategoryTheory.Limits.piComparison 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) (f : β → C) [CategoryTheory.Limits.HasProduct f] [CategoryTheory.Limits.HasProduct fun b => G.obj (f b)] : G.obj (∏ᶜ f) ⟶ ∏ᶜ fun b => G.obj (f b)
• CategoryTheory.Limits.Pi.lift_π 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] {β : Type w} {f : β → C} [CategoryTheory.Limits.HasProduct f] {P : C} (p : (b : β) → P ⟶ f b) (b : β) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.lift p) (CategoryTheory.Limits.Pi.π f b) = p b
• CategoryTheory.Limits.Pi.map'_id 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {α : Type w₂} {C : Type u} [CategoryTheory.Category.{v, u} C] {f g : α → C} [CategoryTheory.Limits.HasProduct f] [CategoryTheory.Limits.HasProduct g] (p : (b : α) → f b ⟶ g b) : CategoryTheory.Limits.Pi.map' id p = CategoryTheory.Limits.Pi.map p
• CategoryTheory.Limits.instMonoLiftπ 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type u₂} [CategoryTheory.Category.{v₂, u₂} J] (F : CategoryTheory.Functor J C) [CategoryTheory.Limits.HasLimit F] [CategoryTheory.Limits.HasProduct F.obj] : CategoryTheory.Mono (CategoryTheory.Limits.Pi.lift (CategoryTheory.Limits.limit.π F))
• CategoryTheory.Limits.Pi.functorπ_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {α : Type w₂} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProductsOfShape α C] (a : α) (f : α → C) : (CategoryTheory.Limits.Pi.functorπ a).app f = CategoryTheory.Limits.Pi.π f a
• 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.Pi.reindex 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {γ : Type w'} (ε : β ≃ γ) (f : γ → C) [CategoryTheory.Limits.HasProduct f] [CategoryTheory.Limits.HasProduct (f ∘ ⇑ε)] : ∏ᶜ f ∘ ⇑ε ≅ ∏ᶜ f
• 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.Pi.π_comp_eqToHom 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type u_1} (f : J → C) [CategoryTheory.Limits.HasProduct f] {j j' : J} (w : j = j') : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π f j) (CategoryTheory.eqToHom ⋯) = CategoryTheory.Limits.Pi.π f j'
• CategoryTheory.Limits.piPiIso 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] {ι : Type u_1} (f : ι → Type u_2) (g : (i : ι) → f i → C) [∀ (i : ι), CategoryTheory.Limits.HasProduct (g i)] [CategoryTheory.Limits.HasProduct fun i => ∏ᶜ g i] : (∏ᶜ fun i => ∏ᶜ g i) ≅ ∏ᶜ fun p => g p.fst p.snd
• CategoryTheory.Limits.productUniqueIso_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [Unique β] (f : β → C) : (CategoryTheory.Limits.productUniqueIso f).hom = CategoryTheory.Limits.Pi.π f default
• CategoryTheory.Limits.Pi.functor_map 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  (α : Type w₂) {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProductsOfShape α C] {f g : α → C} (t : f ⟶ g) : (CategoryTheory.Limits.Pi.functor α).map t = CategoryTheory.Limits.Pi.map t
• CategoryTheory.Limits.Pi.lift_π_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] {β : Type w} {f : β → C} [CategoryTheory.Limits.HasProduct f] {P : C} (p : (b : β) → P ⟶ f b) (b : β) {Z : C} (h : f b ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.lift p) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π f b) h) = CategoryTheory.CategoryStruct.comp (p b) h
• 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.Pi.map_π 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {f g : β → C} [CategoryTheory.Limits.HasProduct f] [CategoryTheory.Limits.HasProduct g] (p : (b : β) → f b ⟶ g b) (b : β) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.map p) (CategoryTheory.Limits.Pi.π g b) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π f b) (p b)
• CategoryTheory.Limits.Pi.hom_ext 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {f : β → C} [CategoryTheory.Limits.HasProduct f] {X : C} (g₁ g₂ : X ⟶ ∏ᶜ f) (h : ∀ (b : β), CategoryTheory.CategoryStruct.comp g₁ (CategoryTheory.Limits.Pi.π f b) = CategoryTheory.CategoryStruct.comp g₂ (CategoryTheory.Limits.Pi.π f b)) : g₁ = g₂
• CategoryTheory.Limits.Pi.π_comp_eqToHom_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type u_1} (f : J → C) [CategoryTheory.Limits.HasProduct f] {j j' : J} (w : j = j') {Z : C} (h : f j' ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π f j) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π f j') h
• CategoryTheory.Limits.Pi.hom_ext_iff 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {f : β → C} [CategoryTheory.Limits.HasProduct f] {X : C} {g₁ g₂ : X ⟶ ∏ᶜ f} : g₁ = g₂ ↔ ∀ (b : β), CategoryTheory.CategoryStruct.comp g₁ (CategoryTheory.Limits.Pi.π f b) = CategoryTheory.CategoryStruct.comp g₂ (CategoryTheory.Limits.Pi.π f b)
• CategoryTheory.Limits.Pi.map'_comp_π 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {α : Type w₂} {C : Type u} [CategoryTheory.Category.{v, u} C] {f : α → C} {g : β → C} [CategoryTheory.Limits.HasProduct f] [CategoryTheory.Limits.HasProduct g] (p : β → α) (q : (b : β) → f (p b) ⟶ g b) (b : β) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.map' p q) (CategoryTheory.Limits.Pi.π g b) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π f (p b)) (q b)
• CategoryTheory.Limits.Pi.map_comp_map 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {α : Type w₂} {C : Type u} [CategoryTheory.Category.{v, u} C] {f g h : α → C} [CategoryTheory.Limits.HasProduct f] [CategoryTheory.Limits.HasProduct g] [CategoryTheory.Limits.HasProduct h] (q : (a : α) → f a ⟶ g a) (q' : (a : α) → g a ⟶ h a) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.map q) (CategoryTheory.Limits.Pi.map q') = CategoryTheory.Limits.Pi.map fun a => CategoryTheory.CategoryStruct.comp (q a) (q' a)
• CategoryTheory.Limits.Pi.map_π_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {f g : β → C} [CategoryTheory.Limits.HasProduct f] [CategoryTheory.Limits.HasProduct g] (p : (b : β) → f b ⟶ g b) (b : β) {Z : C} (h : g b ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.map p) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π g b) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π f b) (CategoryTheory.CategoryStruct.comp (p b) h)
• CategoryTheory.Limits.productUniqueIso_inv 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [Unique β] (f : β → C) (b : β) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.productUniqueIso f).inv (CategoryTheory.Limits.Pi.π f b) = CategoryTheory.eqToHom ⋯
• CategoryTheory.Limits.productUniqueIso_inv_π 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [Unique β] (f : β → C) (b : β) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.productUniqueIso f).inv (CategoryTheory.Limits.Pi.π f b) = CategoryTheory.eqToHom ⋯
• CategoryTheory.Limits.Pi.map'_comp_map 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {α : Type w₂} {C : Type u} [CategoryTheory.Category.{v, u} C] {f : α → C} {g h : β → C} [CategoryTheory.Limits.HasProduct f] [CategoryTheory.Limits.HasProduct g] [CategoryTheory.Limits.HasProduct h] (p : β → α) (q : (b : β) → f (p b) ⟶ g b) (q' : (b : β) → g b ⟶ h b) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.map' p q) (CategoryTheory.Limits.Pi.map q') = CategoryTheory.Limits.Pi.map' p fun b => CategoryTheory.CategoryStruct.comp (q b) (q' b)
• CategoryTheory.Limits.Pi.map_comp_map' 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {α : Type w₂} {C : Type u} [CategoryTheory.Category.{v, u} C] {f g : α → C} {h : β → C} [CategoryTheory.Limits.HasProduct f] [CategoryTheory.Limits.HasProduct g] [CategoryTheory.Limits.HasProduct h] (p : β → α) (q : (a : α) → f a ⟶ g a) (q' : (b : β) → g (p b) ⟶ h b) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.map q) (CategoryTheory.Limits.Pi.map' p q') = CategoryTheory.Limits.Pi.map' p fun b => CategoryTheory.CategoryStruct.comp (q (p b)) (q' b)
• CategoryTheory.Limits.piComparison_comp_π 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) (f : β → C) [CategoryTheory.Limits.HasProduct f] [CategoryTheory.Limits.HasProduct fun b => G.obj (f b)] (b : β) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.piComparison G f) (CategoryTheory.Limits.Pi.π (fun b => G.obj (f b)) b) = G.map (CategoryTheory.Limits.Pi.π f b)
• 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.Pi.whiskerEquiv_inv 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type u_1} {K : Type u_2} {f : J → C} {g : K → C} (e : J ≃ K) (w : (j : J) → g (e j) ≅ f j) [CategoryTheory.Limits.HasProduct f] [CategoryTheory.Limits.HasProduct g] : (CategoryTheory.Limits.Pi.whiskerEquiv e w).inv = CategoryTheory.Limits.Pi.map' ⇑e fun j => (w j).hom
• CategoryTheory.Limits.Pi.map'_comp_π_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {α : Type w₂} {C : Type u} [CategoryTheory.Category.{v, u} C] {f : α → C} {g : β → C} [CategoryTheory.Limits.HasProduct f] [CategoryTheory.Limits.HasProduct g] (p : β → α) (q : (b : β) → f (p b) ⟶ g b) (b : β) {Z : C} (h : g b ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.map' p q) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π g b) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π f (p b)) (CategoryTheory.CategoryStruct.comp (q b) h)
• CategoryTheory.Limits.Pi.map'_comp_map' 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {α : Type w₂} {γ : Type w₃} {C : Type u} [CategoryTheory.Category.{v, u} C] {f : α → C} {g : β → C} {h : γ → C} [CategoryTheory.Limits.HasProduct f] [CategoryTheory.Limits.HasProduct g] [CategoryTheory.Limits.HasProduct h] (p : β → α) (p' : γ → β) (q : (b : β) → f (p b) ⟶ g b) (q' : (c : γ) → g (p' c) ⟶ h c) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.map' p q) (CategoryTheory.Limits.Pi.map' p' q') = CategoryTheory.Limits.Pi.map' (p ∘ p') fun c => CategoryTheory.CategoryStruct.comp (q (p' c)) (q' c)
• CategoryTheory.Limits.Pi.map'_eq 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {α : Type w₂} {C : Type u} [CategoryTheory.Category.{v, u} C] {f : α → C} {g : β → C} [CategoryTheory.Limits.HasProduct f] [CategoryTheory.Limits.HasProduct g] {p p' : β → α} {q : (b : β) → f (p b) ⟶ g b} {q' : (b : β) → f (p' b) ⟶ g b} (hp : p = p') (hq : ∀ (b : β), CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (q b) = q' b) : CategoryTheory.Limits.Pi.map' p q = CategoryTheory.Limits.Pi.map' p' q'
• CategoryTheory.Limits.Pi.isoLimit_inv_π 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {α : Type w₂} {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.Functor (CategoryTheory.Discrete α) C) [CategoryTheory.Limits.HasProduct fun j => X.obj { as := j }] [CategoryTheory.Limits.HasLimit X] (j : α) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.isoLimit X).inv (CategoryTheory.Limits.Pi.π (fun j => X.obj { as := j }) j) = CategoryTheory.Limits.limit.π X { as := j }
• CategoryTheory.Limits.map_lift_piComparison 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) (f : β → C) [CategoryTheory.Limits.HasProduct f] [CategoryTheory.Limits.HasProduct fun b => G.obj (f b)] (P : C) (g : (j : β) → P ⟶ f j) : CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Limits.Pi.lift g)) (CategoryTheory.Limits.piComparison G f) = CategoryTheory.Limits.Pi.lift fun j => G.map (g j)
• CategoryTheory.Limits.Pi.isoLimit_hom_π 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {α : Type w₂} {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.Functor (CategoryTheory.Discrete α) C) [CategoryTheory.Limits.HasProduct fun j => X.obj { as := j }] [CategoryTheory.Limits.HasLimit X] (j : α) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.isoLimit X).hom (CategoryTheory.Limits.limit.π X { as := j }) = CategoryTheory.Limits.Pi.π (fun j => X.obj { as := j }) j
• CategoryTheory.Limits.Pi.cone_π 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {α : Type w₂} {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.Functor (CategoryTheory.Discrete α) C) [CategoryTheory.Limits.HasProduct fun j => X.obj { as := j }] : (CategoryTheory.Limits.Pi.cone X).π = CategoryTheory.Discrete.natTrans fun x => CategoryTheory.Limits.Pi.π (fun j => X.obj { as := j }) x.as
• CategoryTheory.Limits.Pi.lift_π_apply 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] {β : Type w} {f : β → C} [CategoryTheory.Limits.HasProduct f] {P : C} (p : (b : β) → P ⟶ f b) (b : β) {F : C → C → Type uF} {carrier : C → Type w_1} {instFunLike : (X Y : C) → FunLike (F X Y) (carrier X) (carrier Y)} [inst : CategoryTheory.ConcreteCategory C F] (x : carrier P) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Pi.π f b)) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Pi.lift p)) x) = (CategoryTheory.ConcreteCategory.hom (p b)) x
• CategoryTheory.Limits.piConst_obj_map 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] (X : C) {X✝ Y✝ : Type wᵒᵖ} (f : X✝ ⟶ Y✝) : (CategoryTheory.Limits.piConst.obj X).map f = CategoryTheory.Limits.Pi.map' ⇑(CategoryTheory.ConcreteCategory.hom f.unop) fun x => CategoryTheory.CategoryStruct.id X
• CategoryTheory.Limits.piFunctor_obj_map 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] (X : C) {X✝ Y✝ : Type wᵒᵖ} (f : X✝ ⟶ Y✝) : (CategoryTheory.Limits.piFunctor.obj X).map f = CategoryTheory.Limits.Pi.map' ⇑(CategoryTheory.ConcreteCategory.hom f.unop) fun x => CategoryTheory.CategoryStruct.id X
• CategoryTheory.Limits.productUniqueIso_inv_π_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [Unique β] (f : β → C) (b : β) {Z : C} (h : f b ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.productUniqueIso f).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π f b) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) h
• CategoryTheory.Limits.piComparison_comp_π_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) (f : β → C) [CategoryTheory.Limits.HasProduct f] [CategoryTheory.Limits.HasProduct fun b => G.obj (f b)] (b : β) {Z : D} (h : G.obj (f b) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.piComparison G f) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π (fun b => G.obj (f b)) b) h) = CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Limits.Pi.π f b)) 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.map_lift_piComparison_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) (f : β → C) [CategoryTheory.Limits.HasProduct f] [CategoryTheory.Limits.HasProduct fun b => G.obj (f b)] (P : C) (g : (j : β) → P ⟶ f j) {Z : D} (h : (∏ᶜ fun b => G.obj (f b)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Limits.Pi.lift g)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.piComparison G f) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.lift fun j => G.map (g j)) h
• CategoryTheory.Limits.Pi.isoLimit_inv_π_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {α : Type w₂} {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.Functor (CategoryTheory.Discrete α) C) [CategoryTheory.Limits.HasProduct fun j => X.obj { as := j }] [CategoryTheory.Limits.HasLimit X] (j : α) {Z : C} (h : X.obj { as := j } ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.isoLimit X).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π (fun j => X.obj { as := j }) j) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π X { as := j }) h
• CategoryTheory.Limits.Pi.reindex_inv_π 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {γ : Type w'} (ε : β ≃ γ) (f : γ → C) [CategoryTheory.Limits.HasProduct f] [CategoryTheory.Limits.HasProduct (f ∘ ⇑ε)] (b : β) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.reindex ε f).inv (CategoryTheory.Limits.Pi.π (f ∘ ⇑ε) b) = CategoryTheory.Limits.Pi.π f (ε b)
• CategoryTheory.Limits.Pi.isoLimit_hom_π_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {α : Type w₂} {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.Functor (CategoryTheory.Discrete α) C) [CategoryTheory.Limits.HasProduct fun j => X.obj { as := j }] [CategoryTheory.Limits.HasLimit X] (j : α) {Z : C} (h : X.obj { as := j } ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.isoLimit X).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π X { as := j }) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π (fun j => X.obj { as := j }) j) h
• CategoryTheory.Limits.Pi.reindex_hom_π 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {γ : Type w'} (ε : β ≃ γ) (f : γ → C) [CategoryTheory.Limits.HasProduct f] [CategoryTheory.Limits.HasProduct (f ∘ ⇑ε)] (b : β) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.reindex ε f).hom (CategoryTheory.Limits.Pi.π f (ε b)) = CategoryTheory.Limits.Pi.π (f ∘ ⇑ε) b
• 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.piPiIso_inv 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] {ι : Type u_1} (f : ι → Type u_2) (g : (i : ι) → f i → C) [∀ (i : ι), CategoryTheory.Limits.HasProduct (g i)] [CategoryTheory.Limits.HasProduct fun i => ∏ᶜ g i] : (CategoryTheory.Limits.piPiIso f g).inv = CategoryTheory.Limits.Pi.lift fun i => CategoryTheory.Limits.Pi.lift fun x => CategoryTheory.Limits.Pi.π (fun p => g p.fst p.snd) ⟨i, x⟩
• CategoryTheory.Limits.Pi.map_π_apply 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {f g : β → C} [CategoryTheory.Limits.HasProduct f] [CategoryTheory.Limits.HasProduct g] (p : (b : β) → f b ⟶ g b) (b : β) {F : C → C → Type uF} {carrier : C → Type w_1} {instFunLike : (X Y : C) → FunLike (F X Y) (carrier X) (carrier Y)} [inst : CategoryTheory.ConcreteCategory C F] (x : carrier (∏ᶜ f)) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Pi.π g b)) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Pi.map p)) x) = (CategoryTheory.ConcreteCategory.hom (p b)) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Pi.π f b)) x)
• CategoryTheory.Limits.Pi.reindex_inv_π_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {γ : Type w'} (ε : β ≃ γ) (f : γ → C) [CategoryTheory.Limits.HasProduct f] [CategoryTheory.Limits.HasProduct (f ∘ ⇑ε)] (b : β) {Z : C} (h : (f ∘ ⇑ε) b ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.reindex ε f).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π (f ∘ ⇑ε) b) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π f (ε b)) h
• CategoryTheory.Limits.Pi.reindex_hom_π_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {γ : Type w'} (ε : β ≃ γ) (f : γ → C) [CategoryTheory.Limits.HasProduct f] [CategoryTheory.Limits.HasProduct (f ∘ ⇑ε)] (b : β) {Z : C} (h : f (ε b) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.reindex ε f).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π f (ε b)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π (f ∘ ⇑ε) b) h
• CategoryTheory.Limits.piPiIso_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] {ι : Type u_1} (f : ι → Type u_2) (g : (i : ι) → f i → C) [∀ (i : ι), CategoryTheory.Limits.HasProduct (g i)] [CategoryTheory.Limits.HasProduct fun i => ∏ᶜ g i] : (CategoryTheory.Limits.piPiIso f g).hom = CategoryTheory.Limits.Pi.lift fun x => match x with | ⟨i, x⟩ => CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π (fun i => ∏ᶜ g i) i) (CategoryTheory.Limits.Pi.π (g i) x)
• CategoryTheory.Limits.Pi.whiskerEquiv_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type u_1} {K : Type u_2} {f : J → C} {g : K → C} (e : J ≃ K) (w : (j : J) → g (e j) ≅ f j) [CategoryTheory.Limits.HasProduct f] [CategoryTheory.Limits.HasProduct g] : (CategoryTheory.Limits.Pi.whiskerEquiv e w).hom = CategoryTheory.Limits.Pi.map' ⇑e.symm fun k => CategoryTheory.CategoryStruct.comp (w (e.symm k)).inv (CategoryTheory.eqToHom ⋯)
• CategoryTheory.Limits.piConst_map_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) (n : Type wᵒᵖ) : (CategoryTheory.Limits.piConst.map f).app n = CategoryTheory.Limits.Pi.map fun x => f
• CategoryTheory.Limits.piFunctor_map_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) (T : Type wᵒᵖ) : (CategoryTheory.Limits.piFunctor.map f).app T = CategoryTheory.Limits.Pi.map fun x => f
• 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.piComparison_comp_π_apply 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) (f : β → C) [CategoryTheory.Limits.HasProduct f] [CategoryTheory.Limits.HasProduct fun b => G.obj (f b)] (b : β) {F : D → D → Type uF} {carrier : D → Type w_1} {instFunLike : (X Y : D) → FunLike (F X Y) (carrier X) (carrier Y)} [inst : CategoryTheory.ConcreteCategory D F] (x : carrier (G.obj (∏ᶜ f))) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Pi.π (fun b => G.obj (f b)) b)) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.piComparison G f)) x) = (CategoryTheory.ConcreteCategory.hom (G.map (CategoryTheory.Limits.Pi.π f b))) x
• CategoryTheory.Limits.Pi.ι 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {β : Type w} [DecidableEq β] (f : β → C) [CategoryTheory.Limits.HasProduct f] (b : β) : f b ⟶ ∏ᶜ f
• CategoryTheory.Limits.instMonoι_1 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {β : Type w} [DecidableEq β] (f : β → C) [CategoryTheory.Limits.HasProduct f] (b : β) : CategoryTheory.Mono (CategoryTheory.Limits.Pi.ι f b)
• 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.Pi.ι_π_eq_id 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {β : Type w} [DecidableEq β] (f : β → C) [CategoryTheory.Limits.HasProduct f] (b : β) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.ι f b) (CategoryTheory.Limits.Pi.π f b) = CategoryTheory.CategoryStruct.id (f b)
• CategoryTheory.Limits.Pi.ι_π_eq_id_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {β : Type w} [DecidableEq β] (f : β → C) [CategoryTheory.Limits.HasProduct f] (b : β) {Z : C} (h : f b ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.ι f b) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π f b) h) = h
• CategoryTheory.Limits.Pi.ι_π_of_ne 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {β : Type w} [DecidableEq β] (f : β → C) [CategoryTheory.Limits.HasProduct f] {b c : β} (h : b ≠ c) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.ι f b) (CategoryTheory.Limits.Pi.π f c) = 0
• CategoryTheory.Limits.Pi.ι_π_of_ne_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {β : Type w} [DecidableEq β] (f : β → C) [CategoryTheory.Limits.HasProduct f] {b c : β} (h : b ≠ c) {Z : C} (h✝ : f c ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.ι f b) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π f c) h✝) = CategoryTheory.CategoryStruct.comp 0 h✝
• CategoryTheory.Limits.Pi.ι_π 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {β : Type w} [DecidableEq β] (f : β → C) [CategoryTheory.Limits.HasProduct f] (b c : β) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.ι f b) (CategoryTheory.Limits.Pi.π f c) = if h : b = c then CategoryTheory.eqToHom ⋯ else 0
• CategoryTheory.Limits.Pi.ι_π_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {β : Type w} [DecidableEq β] (f : β → C) [CategoryTheory.Limits.HasProduct f] (b c : β) {Z : C} (h : f c ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.ι f b) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π f c) h) = CategoryTheory.CategoryStruct.comp (if h : b = c then CategoryTheory.eqToHom ⋯ else 0) h
• CategoryTheory.Limits.biproduct.isoProduct 📋 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] : ⨁ f ≅ ∏ᶜ f
• CategoryTheory.Limits.biproductIso 📋 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] : ∏ᶜ F ≅ ∐ F
• CategoryTheory.Limits.Pi.map_epi 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
  {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {f g : J → C} [CategoryTheory.Limits.HasBiproduct f] [CategoryTheory.Limits.HasBiproduct g] (p : (j : J) → f j ⟶ g j) [∀ (j : J), CategoryTheory.Epi (p j)] : CategoryTheory.Epi (CategoryTheory.Limits.Pi.map p)
• CategoryTheory.Limits.biproduct.isoProduct_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] : (CategoryTheory.Limits.biproduct.isoProduct f).hom = CategoryTheory.Limits.Pi.lift (CategoryTheory.Limits.biproduct.π f)
• CategoryTheory.Limits.biproduct.isoProduct_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] : (CategoryTheory.Limits.biproduct.isoProduct f).inv = CategoryTheory.Limits.biproduct.lift (CategoryTheory.Limits.Pi.π f)
• CategoryTheory.Limits.HasBiproductsOfShape.colimIsoLim_hom_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
  {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasBiproductsOfShape J C] (X : CategoryTheory.Functor (CategoryTheory.Discrete J) C) : CategoryTheory.Limits.HasBiproductsOfShape.colimIsoLim.hom.app X = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.isoColimit X).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.desc (CategoryTheory.Limits.biproduct.ι fun j => X.obj { as := j })) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.lift (CategoryTheory.Limits.biproduct.π fun j => X.obj { as := j })) (CategoryTheory.Limits.Pi.isoLimit X).hom))
• CategoryTheory.Limits.HasBiproductsOfShape.colimIsoLim_inv_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
  {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasBiproductsOfShape J C] (X : CategoryTheory.Functor (CategoryTheory.Discrete J) C) : CategoryTheory.Limits.HasBiproductsOfShape.colimIsoLim.inv.app X = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.isoLimit X).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.lift (CategoryTheory.Limits.Pi.π fun j => X.obj { as := j })) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.desc (CategoryTheory.Limits.Sigma.ι fun j => X.obj { as := j })) (CategoryTheory.Limits.Sigma.isoColimit X).hom))
• 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.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.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.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.inv_piComparison_comp_map_π 📋 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.IsIso (CategoryTheory.Limits.piComparison G f)] (j : J) : CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (CategoryTheory.Limits.piComparison G f)) (G.map (CategoryTheory.Limits.Pi.π f j)) = CategoryTheory.Limits.Pi.π (fun x => G.obj (f x)) j
• CategoryTheory.Limits.inv_piComparison_comp_map_π_assoc 📋 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.IsIso (CategoryTheory.Limits.piComparison G f)] (j : J) {Z : D} (h : G.obj (f j) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (CategoryTheory.Limits.piComparison G f)) (CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Limits.Pi.π f j)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π (fun x => G.obj (f x)) j) h
• 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.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.MorphismProperty.IsStableUnderProductsOfShape.mk 📋 Mathlib.CategoryTheory.MorphismProperty.Limits
  {C : Type u} [CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C) (J : Type u_1) [W.RespectsIso] (hW : ∀ (X₁ X₂ : J → C) [inst : CategoryTheory.Limits.HasProduct X₁] [inst_1 : CategoryTheory.Limits.HasProduct X₂] (f : (j : J) → X₁ j ⟶ X₂ j), (∀ (j : J), W (f j)) → W (CategoryTheory.Limits.Pi.map f)) : W.IsStableUnderProductsOfShape J
• CategoryTheory.ObjectProperty.prop_pi 📋 Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.ObjectProperty C) {J : Type u_3} [P.IsClosedUnderLimitsOfShape (CategoryTheory.Discrete J)] (X : J → C) [CategoryTheory.Limits.HasProduct X] (hF : ∀ (j : J), P (X j)) : P (∏ᶜ X)
• ModuleCat.piIsoPi 📋 Mathlib.Algebra.Category.ModuleCat.Products
  {R : Type u} [Ring R] {ι : Type v} (Z : ι → ModuleCat R) [CategoryTheory.Limits.HasProduct Z] : ∏ᶜ Z ≅ ModuleCat.of R ((i : ι) → ↑(Z i))
• ModuleCat.piIsoPi_hom_ker_subtype 📋 Mathlib.Algebra.Category.ModuleCat.Products
  {R : Type u} [Ring R] {ι : Type v} (Z : ι → ModuleCat R) [CategoryTheory.Limits.HasProduct Z] (i : ι) : CategoryTheory.CategoryStruct.comp (ModuleCat.piIsoPi Z).hom (ModuleCat.ofHom (LinearMap.proj i)) = CategoryTheory.Limits.Pi.π Z i
• ModuleCat.piIsoPi_inv_kernel_ι 📋 Mathlib.Algebra.Category.ModuleCat.Products
  {R : Type u} [Ring R] {ι : Type v} (Z : ι → ModuleCat R) [CategoryTheory.Limits.HasProduct Z] (i : ι) : CategoryTheory.CategoryStruct.comp (ModuleCat.piIsoPi Z).inv (CategoryTheory.Limits.Pi.π Z i) = ModuleCat.ofHom (LinearMap.proj i)
• ModuleCat.piIsoPi_inv_kernel_ι_apply 📋 Mathlib.Algebra.Category.ModuleCat.Products
  {R : Type u} [Ring R] {ι : Type v} (Z : ι → ModuleCat R) [CategoryTheory.Limits.HasProduct Z] (i : ι) (x : (i : ι) → ↑(Z i)) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Pi.π Z i)) ((CategoryTheory.ConcreteCategory.hom (ModuleCat.piIsoPi Z).inv) x) = x i
• ModuleCat.piIsoPi_hom_ker_subtype_apply 📋 Mathlib.Algebra.Category.ModuleCat.Products
  {R : Type u} [Ring R] {ι : Type v} (Z : ι → ModuleCat R) [CategoryTheory.Limits.HasProduct Z] (i : ι) (x : ↑(∏ᶜ Z)) : (CategoryTheory.ConcreteCategory.hom (ModuleCat.piIsoPi Z).hom) x i = (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Pi.π Z i)) x
• CategoryTheory.Limits.limitSubobjectProduct 📋 Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} [CategoryTheory.SmallCategory J] [CategoryTheory.Limits.HasLimitsOfSize.{w, w, v, u} C] (F : CategoryTheory.Functor J C) : CategoryTheory.Limits.limit F ⟶ ∏ᶜ fun j => F.obj j
• CategoryTheory.Limits.limitSubobjectProduct_mono 📋 Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} [CategoryTheory.SmallCategory J] [CategoryTheory.Limits.HasLimitsOfSize.{w, w, v, u} C] (F : CategoryTheory.Functor J C) : CategoryTheory.Mono (CategoryTheory.Limits.limitSubobjectProduct F)
• FGModuleCat.instFiniteCarrierPiObjModuleCatOfFinite 📋 Mathlib.Algebra.Category.FGModuleCat.Limits
  {k : Type u} [Ring k] {J : Type} [Finite J] (Z : J → ModuleCat k) [∀ (j : J), Module.Finite k ↑(Z j)] : Module.Finite k ↑(∏ᶜ fun j => Z j)
• CategoryTheory.Injective.instPiObj 📋 Mathlib.CategoryTheory.Preadditive.Injective.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {β : Type v} (c : β → C) [CategoryTheory.Limits.HasProduct c] [∀ (b : β), CategoryTheory.Injective (c b)] : CategoryTheory.Injective (∏ᶜ c)
• CategoryTheory.Limits.opCoproductIsoProduct 📋 Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {α : Type u_1} (Z : α → C) [CategoryTheory.Limits.HasCoproduct Z] : Opposite.op (∐ Z) ≅ ∏ᶜ fun x => Opposite.op (Z x)
• CategoryTheory.Limits.opProductIsoCoproduct 📋 Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {α : Type u_1} (Z : α → C) [CategoryTheory.Limits.HasProduct Z] : Opposite.op (∏ᶜ Z) ≅ ∐ fun x => Opposite.op (Z x)
• CategoryTheory.Limits.opCoproductIsoProduct_hom_comp_π 📋 Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {α : Type u_1} {Z : α → C} [CategoryTheory.Limits.HasCoproduct Z] (i : α) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.opCoproductIsoProduct Z).hom (CategoryTheory.Limits.Pi.π (fun x => Opposite.op (Z x)) i) = (CategoryTheory.Limits.Sigma.ι Z i).op
• CategoryTheory.Limits.opCoproductIsoProduct_inv_comp_ι 📋 Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {α : Type u_1} (Z : α → C) [CategoryTheory.Limits.HasCoproduct Z] (b : α) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.opCoproductIsoProduct Z).inv (CategoryTheory.Limits.Sigma.ι Z b).op = CategoryTheory.Limits.Pi.π (fun x => Opposite.op (Z x)) b
• CategoryTheory.Limits.π_comp_opProductIsoCoproduct_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {α : Type u_1} (Z : α → C) [CategoryTheory.Limits.HasProduct Z] (b : α) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π Z b).op (CategoryTheory.Limits.opProductIsoCoproduct Z).hom = CategoryTheory.Limits.Sigma.ι (fun x => Opposite.op (Z x)) b
• CategoryTheory.Limits.desc_op_comp_opCoproductIsoProduct_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {α : Type u_1} {Z : α → C} [CategoryTheory.Limits.HasCoproduct Z] {X : C} (π : (a : α) → Z a ⟶ X) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.desc π).op (CategoryTheory.Limits.opCoproductIsoProduct Z).hom = CategoryTheory.Limits.Pi.lift fun a => (π a).op
• CategoryTheory.Limits.opProductIsoCoproduct_inv_comp_lift 📋 Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {α : Type u_1} {Z : α → C} [CategoryTheory.Limits.HasProduct Z] {X : C} (π : (a : α) → X ⟶ Z a) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.opProductIsoCoproduct Z).inv (CategoryTheory.Limits.Pi.lift π).op = CategoryTheory.Limits.Sigma.desc fun a => (π a).op
• CategoryTheory.Limits.opCoproductIsoProduct_hom_comp_π_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {α : Type u_1} {Z : α → C} [CategoryTheory.Limits.HasCoproduct Z] (i : α) {Z✝ : Cᵒᵖ} (h : Opposite.op (Z i) ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.opCoproductIsoProduct Z).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π (fun x => Opposite.op (Z x)) i) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι Z i).op h
• CategoryTheory.Limits.ProductsFromFiniteCofiltered.finiteSubproductsCone_pt 📋 Mathlib.CategoryTheory.Limits.Constructions.Filtered
  {C : Type u} [CategoryTheory.Category.{v, u} C] {α : Type w} [CategoryTheory.Limits.HasFiniteProducts C] (f : α → C) [CategoryTheory.Limits.HasProduct f] : (CategoryTheory.Limits.ProductsFromFiniteCofiltered.finiteSubproductsCone f).pt = ∏ᶜ f
• CategoryTheory.Limits.ProductsFromFiniteCofiltered.liftToFinsetObj_obj 📋 Mathlib.CategoryTheory.Limits.Constructions.Filtered
  {C : Type u} [CategoryTheory.Category.{v, u} C] {α : Type w} [CategoryTheory.Limits.HasFiniteProducts C] (F : CategoryTheory.Functor (CategoryTheory.Discrete α) C) (s : (Finset (CategoryTheory.Discrete α))ᵒᵖ) : (CategoryTheory.Limits.ProductsFromFiniteCofiltered.liftToFinsetObj F).obj s = ∏ᶜ fun x => F.obj ↑x
• CategoryTheory.Limits.ProductsFromFiniteCofiltered.liftToFinset_obj_obj 📋 Mathlib.CategoryTheory.Limits.Constructions.Filtered
  (C : Type u) [CategoryTheory.Category.{v, u} C] (α : Type w) [CategoryTheory.Limits.HasFiniteProducts C] (F : CategoryTheory.Functor (CategoryTheory.Discrete α) C) (s : (Finset (CategoryTheory.Discrete α))ᵒᵖ) : ((CategoryTheory.Limits.ProductsFromFiniteCofiltered.liftToFinset C α).obj F).obj s = ∏ᶜ fun x => F.obj ↑x
• CategoryTheory.Limits.ProductsFromFiniteCofiltered.finiteSubproductsCone_π_app 📋 Mathlib.CategoryTheory.Limits.Constructions.Filtered
  {C : Type u} [CategoryTheory.Category.{v, u} C] {α : Type w} [CategoryTheory.Limits.HasFiniteProducts C] (f : α → C) [CategoryTheory.Limits.HasProduct f] (S : (Finset (CategoryTheory.Discrete α))ᵒᵖ) : (CategoryTheory.Limits.ProductsFromFiniteCofiltered.finiteSubproductsCone f).π.app S = CategoryTheory.Limits.Pi.lift fun s => CategoryTheory.Limits.Pi.π f (↑s).as
• CategoryTheory.Limits.ProductsFromFiniteCofiltered.liftToFinsetLimitCone_cone_π_app 📋 Mathlib.CategoryTheory.Limits.Constructions.Filtered
  {C : Type u} [CategoryTheory.Category.{v, u} C] {α : Type w} [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasLimitsOfShape (Finset (CategoryTheory.Discrete α))ᵒᵖ C] (F : CategoryTheory.Functor (CategoryTheory.Discrete α) C) (j : CategoryTheory.Discrete α) : (CategoryTheory.Limits.ProductsFromFiniteCofiltered.liftToFinsetLimitCone F).cone.π.app j = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π (CategoryTheory.Limits.ProductsFromFiniteCofiltered.liftToFinsetObj F) (Opposite.op {j})) (CategoryTheory.Limits.Pi.π (fun x => F.obj ↑x) ⟨j, ⋯⟩)
• CategoryTheory.Limits.ProductsFromFiniteCofiltered.liftToFinset_map_app 📋 Mathlib.CategoryTheory.Limits.Constructions.Filtered
  (C : Type u) [CategoryTheory.Category.{v, u} C] (α : Type w) [CategoryTheory.Limits.HasFiniteProducts C] {X✝ Y✝ : CategoryTheory.Functor (CategoryTheory.Discrete α) C} (β : X✝ ⟶ Y✝) (x✝ : (Finset (CategoryTheory.Discrete α))ᵒᵖ) : ((CategoryTheory.Limits.ProductsFromFiniteCofiltered.liftToFinset C α).map β).app x✝ = CategoryTheory.Limits.Pi.map fun x => β.app ↑x
• CategoryTheory.Limits.ProductsFromFiniteCofiltered.liftToFinsetObj_map 📋 Mathlib.CategoryTheory.Limits.Constructions.Filtered
  {C : Type u} [CategoryTheory.Category.{v, u} C] {α : Type w} [CategoryTheory.Limits.HasFiniteProducts C] (F : CategoryTheory.Functor (CategoryTheory.Discrete α) C) {Y x✝ : (Finset (CategoryTheory.Discrete α))ᵒᵖ} (h : Y ⟶ x✝) : (CategoryTheory.Limits.ProductsFromFiniteCofiltered.liftToFinsetObj F).map h = CategoryTheory.Limits.Pi.lift fun y => CategoryTheory.Limits.Pi.π (fun x => F.obj ↑x) ⟨↑y, ⋯⟩
• CategoryTheory.Limits.ProductsFromFiniteCofiltered.liftToFinset_obj_map 📋 Mathlib.CategoryTheory.Limits.Constructions.Filtered
  (C : Type u) [CategoryTheory.Category.{v, u} C] (α : Type w) [CategoryTheory.Limits.HasFiniteProducts C] (F : CategoryTheory.Functor (CategoryTheory.Discrete α) C) {Y x✝ : (Finset (CategoryTheory.Discrete α))ᵒᵖ} (h : Y ⟶ x✝) : ((CategoryTheory.Limits.ProductsFromFiniteCofiltered.liftToFinset C α).obj F).map h = CategoryTheory.Limits.Pi.lift fun y => CategoryTheory.Limits.Pi.π (fun x => F.obj ↑x) ⟨↑y, ⋯⟩
• CategoryTheory.isCoseparator_pi_of_isCoseparator 📋 Mathlib.CategoryTheory.Generator.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasZeroMorphisms C] {β : Type w} (f : β → C) [CategoryTheory.Limits.HasProduct f] (b : β) (hb : CategoryTheory.IsCoseparator (f b)) : CategoryTheory.IsCoseparator (∏ᶜ f)
• CategoryTheory.isCoseparator_pi 📋 Mathlib.CategoryTheory.Generator.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasZeroMorphisms C] {β : Type w} (f : β → C) [CategoryTheory.Limits.HasProduct f] : CategoryTheory.IsCoseparator (∏ᶜ f) ↔ (CategoryTheory.ObjectProperty.ofObj f).IsCoseparating
• CategoryTheory.ObjectProperty.productTo 📋 Mathlib.CategoryTheory.Generator.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (P : CategoryTheory.ObjectProperty C) (X : C) [CategoryTheory.Limits.HasProduct (P.productToFamily X)] : X ⟶ ∏ᶜ P.productToFamily X
• CategoryTheory.ObjectProperty.IsCoseparating.mono_productTo 📋 Mathlib.CategoryTheory.Generator.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.ObjectProperty C} (hP : P.IsCoseparating) (X : C) [CategoryTheory.Limits.HasProduct (P.productToFamily X)] : CategoryTheory.Mono (P.productTo X)
• CategoryTheory.ObjectProperty.isCoseparating_iff_mono 📋 Mathlib.CategoryTheory.Generator.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (P : CategoryTheory.ObjectProperty C) [∀ (X : C), CategoryTheory.Limits.HasProduct (P.productToFamily X)] : P.IsCoseparating ↔ ∀ (X : C), CategoryTheory.Mono (P.productTo X)
• CategoryTheory.ObjectProperty.πProductTo 📋 Mathlib.CategoryTheory.Generator.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (P : CategoryTheory.ObjectProperty C) {X : C} [CategoryTheory.Limits.HasProduct (P.productToFamily X)] {Y : C} (f : X ⟶ Y) (hY : P Y) : ∏ᶜ P.productToFamily X ⟶ Y
• CategoryTheory.isCoseparator_iff_mono 📋 Mathlib.CategoryTheory.Generator.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (G : C) [∀ (A : C), CategoryTheory.Limits.HasProduct fun x => G] : CategoryTheory.IsCoseparator G ↔ ∀ (A : C), CategoryTheory.Mono (CategoryTheory.Limits.Pi.lift fun f => f)
• CategoryTheory.Limits.MulticospanIndex.fstPiMap 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] : ∏ᶜ I.left ⟶ ∏ᶜ I.right
• CategoryTheory.Limits.MulticospanIndex.sndPiMap 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] : ∏ᶜ I.left ⟶ ∏ᶜ I.right
• CategoryTheory.Limits.Multiequalizer.ιPi 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) [CategoryTheory.Limits.HasMultiequalizer I] [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] : CategoryTheory.Limits.multiequalizer I ⟶ ∏ᶜ I.left
• CategoryTheory.Limits.Multiequalizer.instMonoιPi 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) [CategoryTheory.Limits.HasMultiequalizer I] [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] : CategoryTheory.Mono (CategoryTheory.Limits.Multiequalizer.ιPi I)
• CategoryTheory.Limits.MulticospanIndex.parallelPairDiagram_obj 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] (x : CategoryTheory.Limits.WalkingParallelPair) : I.parallelPairDiagram.obj x = CategoryTheory.Limits.parallelPair.parallelPairObj (∏ᶜ I.left) (∏ᶜ I.right) x
• CategoryTheory.Limits.Multiequalizer.instHasEqualizerFstPiMapSndPiMap 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) [CategoryTheory.Limits.HasMultiequalizer I] [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] : CategoryTheory.Limits.HasEqualizer I.fstPiMap I.sndPiMap
• CategoryTheory.Limits.Multiequalizer.isoEqualizer 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) [CategoryTheory.Limits.HasMultiequalizer I] [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] : CategoryTheory.Limits.multiequalizer I ≅ CategoryTheory.Limits.equalizer I.fstPiMap I.sndPiMap
• CategoryTheory.Limits.Multiequalizer.ιPi_π 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) [CategoryTheory.Limits.HasMultiequalizer I] [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] (a : J.L) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multiequalizer.ιPi I) (CategoryTheory.Limits.Pi.π I.left a) = CategoryTheory.Limits.Multiequalizer.ι I a
• CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiFork 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] : CategoryTheory.Limits.Multifork I ≌ CategoryTheory.Limits.Fork I.fstPiMap I.sndPiMap
• CategoryTheory.Limits.MulticospanIndex.parallelPairDiagram_map 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] {X✝ Y✝ : CategoryTheory.Limits.WalkingParallelPair} (h : X✝ ⟶ Y✝) : I.parallelPairDiagram.map h = CategoryTheory.Limits.parallelPair.parallelPairHom I.fstPiMap I.sndPiMap h
• CategoryTheory.Limits.MulticospanIndex.fstPiMap_π 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] (b : J.R) : CategoryTheory.CategoryStruct.comp I.fstPiMap (CategoryTheory.Limits.Pi.π I.right b) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π I.left (J.fst b)) (I.fst b)
• CategoryTheory.Limits.MulticospanIndex.sndPiMap_π 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] (b : J.R) : CategoryTheory.CategoryStruct.comp I.sndPiMap (CategoryTheory.Limits.Pi.π I.right b) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π I.left (J.snd b)) (I.snd b)
• CategoryTheory.Limits.Multiequalizer.ιPi_π_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) [CategoryTheory.Limits.HasMultiequalizer I] [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] (a : J.L) {Z : C} (h : I.left a ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multiequalizer.ιPi I) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π I.left a) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multiequalizer.ι I a) h
• CategoryTheory.Limits.MulticospanIndex.fstPiMap_π_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] (b : J.R) {Z : C} (h : I.right b ⟶ Z) : CategoryTheory.CategoryStruct.comp I.fstPiMap (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π I.right b) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π I.left (J.fst b)) (CategoryTheory.CategoryStruct.comp (I.fst b) h)
• CategoryTheory.Limits.MulticospanIndex.sndPiMap_π_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] (b : J.R) {Z : C} (h : I.right b ⟶ Z) : CategoryTheory.CategoryStruct.comp I.sndPiMap (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π I.right b) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π I.left (J.snd b)) (CategoryTheory.CategoryStruct.comp (I.snd b) h)
• CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiFork_functor_obj_pt 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] (K : CategoryTheory.Limits.Multifork I) : (I.multiforkEquivPiFork.functor.obj K).pt = K.pt
• CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiFork_inverse_obj_pt 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] (a : CategoryTheory.Limits.Fork (I.fstPiMapOfIsLimit (CategoryTheory.Limits.limit.cone (CategoryTheory.Discrete.functor I.left)) (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Discrete.functor I.right))) (I.sndPiMapOfIsLimit (CategoryTheory.Limits.limit.cone (CategoryTheory.Discrete.functor I.left)) (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Discrete.functor I.right)))) : (I.multiforkEquivPiFork.inverse.obj a).pt = a.pt
• CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiFork_functor_map_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] {K₁ K₂ : CategoryTheory.Limits.Multifork I} (f : K₁ ⟶ K₂) : (I.multiforkEquivPiFork.functor.map f).hom = f.hom
• CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiFork_functor_obj_π_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] (K : CategoryTheory.Limits.Multifork I) (X : CategoryTheory.Limits.WalkingParallelPair) : (I.multiforkEquivPiFork.functor.obj K).π.app X = CategoryTheory.Limits.WalkingParallelPair.rec (motive := fun t => X = t → (K.pt ⟶ (CategoryTheory.Limits.parallelPair (I.fstPiMapOfIsLimit (CategoryTheory.Limits.limit.cone (CategoryTheory.Discrete.functor I.left)) (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Discrete.functor I.right))) (I.sndPiMapOfIsLimit (CategoryTheory.Limits.limit.cone (CategoryTheory.Discrete.functor I.left)) (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Discrete.functor I.right)))).obj X)) (fun h => ⋯ ▸ CategoryTheory.Limits.Fan.IsLimit.lift (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Discrete.functor I.left)) K.ι) (fun h => ⋯ ▸ CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fan.IsLimit.lift (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Discrete.functor I.left)) K.ι) (I.sndPiMapOfIsLimit (CategoryTheory.Limits.limit.cone (CategoryTheory.Discrete.functor I.left)) (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Discrete.functor I.right)))) X ⋯
• CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiFork_inverse_obj_π_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] (a : CategoryTheory.Limits.Fork (I.fstPiMapOfIsLimit (CategoryTheory.Limits.limit.cone (CategoryTheory.Discrete.functor I.left)) (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Discrete.functor I.right))) (I.sndPiMapOfIsLimit (CategoryTheory.Limits.limit.cone (CategoryTheory.Discrete.functor I.left)) (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Discrete.functor I.right)))) (x✝ : CategoryTheory.Limits.WalkingMulticospan J) : (I.multiforkEquivPiFork.inverse.obj a).π.app x✝ = match x✝ with | CategoryTheory.Limits.WalkingMulticospan.left a_1 => CategoryTheory.CategoryStruct.comp a.ι (CategoryTheory.Limits.Fan.proj (CategoryTheory.Limits.limit.cone (CategoryTheory.Discrete.functor I.left)) a_1) | CategoryTheory.Limits.WalkingMulticospan.right a_1 => CategoryTheory.CategoryStruct.comp a.ι (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fan.proj (CategoryTheory.Limits.limit.cone (CategoryTheory.Discrete.functor I.left)) (J.fst a_1)) (I.fst a_1))
• CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiFork_inverse_map_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] {K₁ K₂ : CategoryTheory.Limits.Fork (I.fstPiMapOfIsLimit (CategoryTheory.Limits.limit.cone (CategoryTheory.Discrete.functor I.left)) (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Discrete.functor I.right))) (I.sndPiMapOfIsLimit (CategoryTheory.Limits.limit.cone (CategoryTheory.Discrete.functor I.left)) (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Discrete.functor I.right)))} (f : K₁ ⟶ K₂) : (I.multiforkEquivPiFork.inverse.map f).hom = f.hom
• CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiFork_unitIso_hom_app_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] (X : CategoryTheory.Limits.Multifork I) : (I.multiforkEquivPiFork.unitIso.hom.app X).hom = CategoryTheory.CategoryStruct.id X.pt
• CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiFork_unitIso_inv_app_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] (X : CategoryTheory.Limits.Multifork I) : (I.multiforkEquivPiFork.unitIso.inv.app X).hom = CategoryTheory.CategoryStruct.id X.pt
• CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiFork_counitIso_hom_app_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] (X : CategoryTheory.Limits.Fork (I.fstPiMapOfIsLimit (CategoryTheory.Limits.limit.cone (CategoryTheory.Discrete.functor I.left)) (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Discrete.functor I.right))) (I.sndPiMapOfIsLimit (CategoryTheory.Limits.limit.cone (CategoryTheory.Discrete.functor I.left)) (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Discrete.functor I.right)))) : (I.multiforkEquivPiFork.counitIso.hom.app X).hom = CategoryTheory.CategoryStruct.id X.pt
• CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiFork_counitIso_inv_app_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] (X : CategoryTheory.Limits.Fork (I.fstPiMapOfIsLimit (CategoryTheory.Limits.limit.cone (CategoryTheory.Discrete.functor I.left)) (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Discrete.functor I.right))) (I.sndPiMapOfIsLimit (CategoryTheory.Limits.limit.cone (CategoryTheory.Discrete.functor I.left)) (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Discrete.functor I.right)))) : (I.multiforkEquivPiFork.counitIso.inv.app X).hom = CategoryTheory.CategoryStruct.id X.pt
• CategoryTheory.Limits.Concrete.productEquiv 📋 Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type (max w v)} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [CategoryTheory.ConcreteCategory C FC] {J : Type w} (F : J → C) [CategoryTheory.Limits.HasProduct F] [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Discrete.functor F) (CategoryTheory.forget C)] : CategoryTheory.ToType (∏ᶜ F) ≃ ((j : J) → CategoryTheory.ToType (F j))
• CategoryTheory.Limits.Concrete.productEquiv_apply_apply 📋 Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type (max w v)} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [CategoryTheory.ConcreteCategory C FC] {J : Type w} (F : J → C) [CategoryTheory.Limits.HasProduct F] [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Discrete.functor F) (CategoryTheory.forget C)] (x : CategoryTheory.ToType (∏ᶜ F)) (j : J) : (CategoryTheory.Limits.Concrete.productEquiv F) x j = (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Pi.π F j)) x
• CategoryTheory.Limits.Concrete.productEquiv_symm_apply_π 📋 Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type (max w v)} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [CategoryTheory.ConcreteCategory C FC] {J : Type w} (F : J → C) [CategoryTheory.Limits.HasProduct F] [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Discrete.functor F) (CategoryTheory.forget C)] (x : (j : J) → CategoryTheory.ToType (F j)) (j : J) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Pi.π F j)) ((CategoryTheory.Limits.Concrete.productEquiv F).symm x) = x j
• CategoryTheory.Limits.Concrete.Pi.map_ext 📋 Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} (f : J → C) [CategoryTheory.Limits.HasProduct f] {D : Type t} [CategoryTheory.Category.{r, t} D] {FD : D → D → Type u_1} {DD : D → Type (max w r)} [(X Y : D) → FunLike (FD X Y) (DD X) (DD Y)] [CategoryTheory.ConcreteCategory D FD] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Discrete.functor f) F] [CategoryTheory.Limits.HasProduct fun j => F.obj (f j)] [CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.Limits.WalkingCospan (CategoryTheory.forget D)] [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Discrete.functor fun b => F.obj (f b)) (CategoryTheory.forget D)] (x y : CategoryTheory.ToType (F.obj (∏ᶜ f))) (h : ∀ (i : J), (CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.Limits.Pi.π f i))) x = (CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.Limits.Pi.π f i))) y) : x = y
• CategoryTheory.Pretriangulated.productTriangle_obj₁ 📋 Mathlib.CategoryTheory.Triangulated.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.HasShift C ℤ] {J : Type u_1} (T : J → CategoryTheory.Pretriangulated.Triangle C) [CategoryTheory.Limits.HasProduct fun j => (T j).obj₁] [CategoryTheory.Limits.HasProduct fun j => (T j).obj₂] [CategoryTheory.Limits.HasProduct fun j => (T j).obj₃] [CategoryTheory.Limits.HasProduct fun j => (CategoryTheory.shiftFunctor C 1).obj (T j).obj₁] : (CategoryTheory.Pretriangulated.productTriangle T).obj₁ = ∏ᶜ fun j => (T j).obj₁
• CategoryTheory.Pretriangulated.productTriangle_obj₂ 📋 Mathlib.CategoryTheory.Triangulated.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.HasShift C ℤ] {J : Type u_1} (T : J → CategoryTheory.Pretriangulated.Triangle C) [CategoryTheory.Limits.HasProduct fun j => (T j).obj₁] [CategoryTheory.Limits.HasProduct fun j => (T j).obj₂] [CategoryTheory.Limits.HasProduct fun j => (T j).obj₃] [CategoryTheory.Limits.HasProduct fun j => (CategoryTheory.shiftFunctor C 1).obj (T j).obj₁] : (CategoryTheory.Pretriangulated.productTriangle T).obj₂ = ∏ᶜ fun j => (T j).obj₂
• CategoryTheory.Pretriangulated.productTriangle_obj₃ 📋 Mathlib.CategoryTheory.Triangulated.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.HasShift C ℤ] {J : Type u_1} (T : J → CategoryTheory.Pretriangulated.Triangle C) [CategoryTheory.Limits.HasProduct fun j => (T j).obj₁] [CategoryTheory.Limits.HasProduct fun j => (T j).obj₂] [CategoryTheory.Limits.HasProduct fun j => (T j).obj₃] [CategoryTheory.Limits.HasProduct fun j => (CategoryTheory.shiftFunctor C 1).obj (T j).obj₁] : (CategoryTheory.Pretriangulated.productTriangle T).obj₃ = ∏ᶜ fun j => (T j).obj₃
• CategoryTheory.Pretriangulated.productTriangle.π_hom₁ 📋 Mathlib.CategoryTheory.Triangulated.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.HasShift C ℤ] {J : Type u_1} (T : J → CategoryTheory.Pretriangulated.Triangle C) [CategoryTheory.Limits.HasProduct fun j => (T j).obj₁] [CategoryTheory.Limits.HasProduct fun j => (T j).obj₂] [CategoryTheory.Limits.HasProduct fun j => (T j).obj₃] [CategoryTheory.Limits.HasProduct fun j => (CategoryTheory.shiftFunctor C 1).obj (T j).obj₁] (j : J) : (CategoryTheory.Pretriangulated.productTriangle.π T j).hom₁ = CategoryTheory.Limits.Pi.π (fun j => (T j).obj₁) j
• CategoryTheory.Pretriangulated.productTriangle.π_hom₂ 📋 Mathlib.CategoryTheory.Triangulated.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.HasShift C ℤ] {J : Type u_1} (T : J → CategoryTheory.Pretriangulated.Triangle C) [CategoryTheory.Limits.HasProduct fun j => (T j).obj₁] [CategoryTheory.Limits.HasProduct fun j => (T j).obj₂] [CategoryTheory.Limits.HasProduct fun j => (T j).obj₃] [CategoryTheory.Limits.HasProduct fun j => (CategoryTheory.shiftFunctor C 1).obj (T j).obj₁] (j : J) : (CategoryTheory.Pretriangulated.productTriangle.π T j).hom₂ = CategoryTheory.Limits.Pi.π (fun j => (T j).obj₂) j
• CategoryTheory.Pretriangulated.productTriangle.π_hom₃ 📋 Mathlib.CategoryTheory.Triangulated.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.HasShift C ℤ] {J : Type u_1} (T : J → CategoryTheory.Pretriangulated.Triangle C) [CategoryTheory.Limits.HasProduct fun j => (T j).obj₁] [CategoryTheory.Limits.HasProduct fun j => (T j).obj₂] [CategoryTheory.Limits.HasProduct fun j => (T j).obj₃] [CategoryTheory.Limits.HasProduct fun j => (CategoryTheory.shiftFunctor C 1).obj (T j).obj₁] (j : J) : (CategoryTheory.Pretriangulated.productTriangle.π T j).hom₃ = CategoryTheory.Limits.Pi.π (fun j => (T j).obj₃) j
• CategoryTheory.Pretriangulated.productTriangle_mor₁ 📋 Mathlib.CategoryTheory.Triangulated.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.HasShift C ℤ] {J : Type u_1} (T : J → CategoryTheory.Pretriangulated.Triangle C) [CategoryTheory.Limits.HasProduct fun j => (T j).obj₁] [CategoryTheory.Limits.HasProduct fun j => (T j).obj₂] [CategoryTheory.Limits.HasProduct fun j => (T j).obj₃] [CategoryTheory.Limits.HasProduct fun j => (CategoryTheory.shiftFunctor C 1).obj (T j).obj₁] : (CategoryTheory.Pretriangulated.productTriangle T).mor₁ = CategoryTheory.Limits.Pi.map fun j => (T j).mor₁
• CategoryTheory.Pretriangulated.productTriangle_mor₂ 📋 Mathlib.CategoryTheory.Triangulated.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.HasShift C ℤ] {J : Type u_1} (T : J → CategoryTheory.Pretriangulated.Triangle C) [CategoryTheory.Limits.HasProduct fun j => (T j).obj₁] [CategoryTheory.Limits.HasProduct fun j => (T j).obj₂] [CategoryTheory.Limits.HasProduct fun j => (T j).obj₃] [CategoryTheory.Limits.HasProduct fun j => (CategoryTheory.shiftFunctor C 1).obj (T j).obj₁] : (CategoryTheory.Pretriangulated.productTriangle T).mor₂ = CategoryTheory.Limits.Pi.map fun j => (T j).mor₂
• CategoryTheory.Pretriangulated.productTriangle.lift_hom₁ 📋 Mathlib.CategoryTheory.Triangulated.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.HasShift C ℤ] {J : Type u_1} (T : J → CategoryTheory.Pretriangulated.Triangle C) [CategoryTheory.Limits.HasProduct fun j => (T j).obj₁] [CategoryTheory.Limits.HasProduct fun j => (T j).obj₂] [CategoryTheory.Limits.HasProduct fun j => (T j).obj₃] [CategoryTheory.Limits.HasProduct fun j => (CategoryTheory.shiftFunctor C 1).obj (T j).obj₁] {T' : CategoryTheory.Pretriangulated.Triangle C} (φ : (j : J) → T' ⟶ T j) : (CategoryTheory.Pretriangulated.productTriangle.lift T φ).hom₁ = CategoryTheory.Limits.Pi.lift fun j => (φ j).hom₁
• CategoryTheory.Pretriangulated.productTriangle.lift_hom₂ 📋 Mathlib.CategoryTheory.Triangulated.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.HasShift C ℤ] {J : Type u_1} (T : J → CategoryTheory.Pretriangulated.Triangle C) [CategoryTheory.Limits.HasProduct fun j => (T j).obj₁] [CategoryTheory.Limits.HasProduct fun j => (T j).obj₂] [CategoryTheory.Limits.HasProduct fun j => (T j).obj₃] [CategoryTheory.Limits.HasProduct fun j => (CategoryTheory.shiftFunctor C 1).obj (T j).obj₁] {T' : CategoryTheory.Pretriangulated.Triangle C} (φ : (j : J) → T' ⟶ T j) : (CategoryTheory.Pretriangulated.productTriangle.lift T φ).hom₂ = CategoryTheory.Limits.Pi.lift fun j => (φ j).hom₂
• CategoryTheory.Pretriangulated.productTriangle.lift_hom₃ 📋 Mathlib.CategoryTheory.Triangulated.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.HasShift C ℤ] {J : Type u_1} (T : J → CategoryTheory.Pretriangulated.Triangle C) [CategoryTheory.Limits.HasProduct fun j => (T j).obj₁] [CategoryTheory.Limits.HasProduct fun j => (T j).obj₂] [CategoryTheory.Limits.HasProduct fun j => (T j).obj₃] [CategoryTheory.Limits.HasProduct fun j => (CategoryTheory.shiftFunctor C 1).obj (T j).obj₁] {T' : CategoryTheory.Pretriangulated.Triangle C} (φ : (j : J) → T' ⟶ T j) : (CategoryTheory.Pretriangulated.productTriangle.lift T φ).hom₃ = CategoryTheory.Limits.Pi.lift fun j => (φ j).hom₃
• CategoryTheory.Pretriangulated.productTriangle_mor₃ 📋 Mathlib.CategoryTheory.Triangulated.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.HasShift C ℤ] {J : Type u_1} (T : J → CategoryTheory.Pretriangulated.Triangle C) [CategoryTheory.Limits.HasProduct fun j => (T j).obj₁] [CategoryTheory.Limits.HasProduct fun j => (T j).obj₂] [CategoryTheory.Limits.HasProduct fun j => (T j).obj₃] [CategoryTheory.Limits.HasProduct fun j => (CategoryTheory.shiftFunctor C 1).obj (T j).obj₁] : (CategoryTheory.Pretriangulated.productTriangle T).mor₃ = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.map fun j => (T j).mor₃) (CategoryTheory.inv (CategoryTheory.Limits.piComparison (CategoryTheory.shiftFunctor C 1) fun j => (T j).obj₁))
• CategoryTheory.ObjectProperty.prop_product 📋 Mathlib.CategoryTheory.ObjectProperty.FiniteProducts
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.ObjectProperty C) [P.IsClosedUnderFiniteProducts] {J : Type u_2} [Finite J] {f : J → C} [CategoryTheory.Limits.HasProduct f] (h : ∀ (j : J), P (f j)) : P (∏ᶜ f)
• CategoryTheory.Equalizer.firstObjEqFamily_inv 📋 Mathlib.CategoryTheory.Sites.EqualizerSheafCondition
  {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.Functor Cᵒᵖ (Type (max v u))) {X : C} (R : CategoryTheory.Presieve X) : (CategoryTheory.Equalizer.firstObjEqFamily P R).inv = CategoryTheory.Limits.Pi.lift fun f => TypeCat.ofHom fun x => x ↑f.snd ⋯
• CategoryTheory.Equalizer.Presieve.Arrows.FirstObj.ext 📋 Mathlib.CategoryTheory.Sites.EqualizerSheafCondition
  {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.Functor Cᵒᵖ (Type w)) {I : Type t} [Small.{w, t} I] (X : I → C) (z₁ z₂ : CategoryTheory.Equalizer.Presieve.Arrows.FirstObj P X) (h : ∀ (i : I), (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Pi.π (fun i => P.obj (Opposite.op (X i))) i)) z₁ = (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Pi.π (fun i => P.obj (Opposite.op (X i))) i)) z₂) : z₁ = z₂
• CategoryTheory.Equalizer.Presieve.Arrows.FirstObj.ext_iff 📋 Mathlib.CategoryTheory.Sites.EqualizerSheafCondition
  {C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {I : Type t} [Small.{w, t} I] {X : I → C} {z₁ z₂ : CategoryTheory.Equalizer.Presieve.Arrows.FirstObj P X} : z₁ = z₂ ↔ ∀ (i : I), (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Pi.π (fun i => P.obj (Opposite.op (X i))) i)) z₁ = (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Pi.π (fun i => P.obj (Opposite.op (X i))) i)) z₂
• CategoryTheory.Equalizer.Presieve.Arrows.compatible_iff 📋 Mathlib.CategoryTheory.Sites.EqualizerSheafCondition
  {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.Functor Cᵒᵖ (Type w)) {B : C} {I : Type w} (X : I → C) (π : (i : I) → X i ⟶ B) [(CategoryTheory.Presieve.ofArrows X π).HasPairwisePullbacks] (x : CategoryTheory.Equalizer.Presieve.Arrows.FirstObj P X) : CategoryTheory.Presieve.Arrows.Compatible P π ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Types.productIso fun i => P.obj (Opposite.op (X i))).hom) x) ↔ (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Equalizer.Presieve.Arrows.firstMap P X π)) x = (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Equalizer.Presieve.Arrows.secondMap P X π)) x
• CategoryTheory.Equalizer.firstObjEqFamily_hom 📋 Mathlib.CategoryTheory.Sites.EqualizerSheafCondition
  {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.Functor Cᵒᵖ (Type (max v u))) {X : C} (R : CategoryTheory.Presieve X) : (CategoryTheory.Equalizer.firstObjEqFamily P R).hom = TypeCat.ofHom fun t x x_1 hf => (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Pi.π (fun f => P.obj (Opposite.op f.fst)) ⟨x, ⟨x_1, hf⟩⟩)) t
• CategoryTheory.Equalizer.Presieve.Arrows.SecondObj.ext 📋 Mathlib.CategoryTheory.Sites.EqualizerSheafCondition
  {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.Functor Cᵒᵖ (Type w)) {B : C} {I : Type t} [Small.{w, t} I] (X : I → C) (π : (i : I) → X i ⟶ B) [(CategoryTheory.Presieve.ofArrows X π).HasPairwisePullbacks] (z₁ z₂ : CategoryTheory.Equalizer.Presieve.Arrows.SecondObj P X π) (h : ∀ (ij : I × I), (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Pi.π (fun ij => P.obj (Opposite.op (CategoryTheory.Limits.pullback (π ij.1) (π ij.2)))) ij)) z₁ = (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Pi.π (fun ij => P.obj (Opposite.op (CategoryTheory.Limits.pullback (π ij.1) (π ij.2)))) ij)) z₂) : z₁ = z₂
• CategoryTheory.Equalizer.Presieve.Arrows.SecondObj.ext_iff 📋 Mathlib.CategoryTheory.Sites.EqualizerSheafCondition
  {C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {B : C} {I : Type t} [Small.{w, t} I] {X : I → C} {π : (i : I) → X i ⟶ B} [(CategoryTheory.Presieve.ofArrows X π).HasPairwisePullbacks] {z₁ z₂ : CategoryTheory.Equalizer.Presieve.Arrows.SecondObj P X π} : z₁ = z₂ ↔ ∀ (ij : I × I), (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Pi.π (fun ij => P.obj (Opposite.op (CategoryTheory.Limits.pullback (π ij.1) (π ij.2)))) ij)) z₁ = (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Pi.π (fun ij => P.obj (Opposite.op (CategoryTheory.Limits.pullback (π ij.1) (π ij.2)))) ij)) z₂

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