Loogle!

Result

Found 141 declarations mentioning CategoryTheory.Limits.prod.fst.

• CategoryTheory.Limits.prod.fst 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} [CategoryTheory.Limits.HasBinaryProduct X Y] : X ⨯ Y ⟶ X
• CategoryTheory.Limits.prodIsProd 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X Y : C) [CategoryTheory.Limits.HasBinaryProduct X Y] : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.BinaryFan.mk CategoryTheory.Limits.prod.fst CategoryTheory.Limits.prod.snd)
• CategoryTheory.Limits.prod.rightUnitor_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasTerminal C] (P : C) [CategoryTheory.Limits.HasBinaryProduct P (⊤_ C)] : (CategoryTheory.Limits.prod.rightUnitor P).hom = CategoryTheory.Limits.prod.fst
• CategoryTheory.Limits.prod.lift_fst_snd 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} [CategoryTheory.Limits.HasBinaryProduct X Y] : CategoryTheory.Limits.prod.lift CategoryTheory.Limits.prod.fst CategoryTheory.Limits.prod.snd = CategoryTheory.CategoryStruct.id (X ⨯ Y)
• CategoryTheory.Limits.prod.lift_fst 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] {W X Y : C} [CategoryTheory.Limits.HasBinaryProduct X Y] (f : W ⟶ X) (g : W ⟶ Y) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.lift f g) CategoryTheory.Limits.prod.fst = f
• CategoryTheory.Limits.prod.braiding_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] (P Q : C) [CategoryTheory.Limits.HasBinaryProduct P Q] [CategoryTheory.Limits.HasBinaryProduct Q P] : (CategoryTheory.Limits.prod.braiding P Q).hom = CategoryTheory.Limits.prod.lift CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.fst
• CategoryTheory.Limits.prod.braiding_inv 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] (P Q : C) [CategoryTheory.Limits.HasBinaryProduct P Q] [CategoryTheory.Limits.HasBinaryProduct Q P] : (CategoryTheory.Limits.prod.braiding P Q).inv = CategoryTheory.Limits.prod.lift CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.fst
• CategoryTheory.Limits.prod.lift_fst_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] {W X Y : C} [CategoryTheory.Limits.HasBinaryProduct X Y] (f : W ⟶ X) (g : W ⟶ Y) {Z : C} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.lift f g) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst h) = CategoryTheory.CategoryStruct.comp f h
• CategoryTheory.Limits.prod.map_fst 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] {W X Y Z : C} [CategoryTheory.Limits.HasBinaryProduct W X] [CategoryTheory.Limits.HasBinaryProduct Y Z] (f : W ⟶ Y) (g : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map f g) CategoryTheory.Limits.prod.fst = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst f
• CategoryTheory.Limits.prod.symmetry' 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] (P Q : C) [CategoryTheory.Limits.HasBinaryProduct P Q] [CategoryTheory.Limits.HasBinaryProduct Q P] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.lift CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.fst) (CategoryTheory.Limits.prod.lift CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.fst) = CategoryTheory.CategoryStruct.id (P ⨯ Q)
• CategoryTheory.Limits.prod.lift_fst_comp_snd_comp 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] {W X Y Z : C} [CategoryTheory.Limits.HasBinaryProduct W Y] [CategoryTheory.Limits.HasBinaryProduct X Z] (g : W ⟶ X) (g' : Y ⟶ Z) : CategoryTheory.Limits.prod.lift (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst g) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd g') = CategoryTheory.Limits.prod.map g g'
• CategoryTheory.Limits.prod.lift' 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] {W X Y : C} [CategoryTheory.Limits.HasBinaryProduct X Y] (f : W ⟶ X) (g : W ⟶ Y) : { l // CategoryTheory.CategoryStruct.comp l CategoryTheory.Limits.prod.fst = f ∧ CategoryTheory.CategoryStruct.comp l CategoryTheory.Limits.prod.snd = g }
• CategoryTheory.Limits.prod.diag_map_fst_snd 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} [CategoryTheory.Limits.HasBinaryProduct X Y] [CategoryTheory.Limits.HasBinaryProduct (X ⨯ Y) (X ⨯ Y)] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.diag (X ⨯ Y)) (CategoryTheory.Limits.prod.map CategoryTheory.Limits.prod.fst CategoryTheory.Limits.prod.snd) = CategoryTheory.CategoryStruct.id (X ⨯ Y)
• CategoryTheory.Limits.prod.symmetry'_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] (P Q : C) [CategoryTheory.Limits.HasBinaryProduct P Q] [CategoryTheory.Limits.HasBinaryProduct Q P] {Z : C} (h : P ⨯ Q ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.lift CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.fst) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.lift CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.fst) h) = h
• CategoryTheory.Limits.prod.map_fst_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] {W X Y Z : C} [CategoryTheory.Limits.HasBinaryProduct W X] [CategoryTheory.Limits.HasBinaryProduct Y Z] (f : W ⟶ Y) (g : X ⟶ Z) {Z✝ : C} (h : Y ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map f g) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst h) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst (CategoryTheory.CategoryStruct.comp f h)
• CategoryTheory.Limits.prod.diag_map_fst_snd_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} [CategoryTheory.Limits.HasBinaryProduct X Y] [CategoryTheory.Limits.HasBinaryProduct (X ⨯ Y) (X ⨯ Y)] {Z : C} (h : X ⨯ Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.diag (X ⨯ Y)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map CategoryTheory.Limits.prod.fst CategoryTheory.Limits.prod.snd) h) = h
• CategoryTheory.Limits.prod.hom_ext 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] {W X Y : C} [CategoryTheory.Limits.HasBinaryProduct X Y] {f g : W ⟶ X ⨯ Y} (h₁ : CategoryTheory.CategoryStruct.comp f CategoryTheory.Limits.prod.fst = CategoryTheory.CategoryStruct.comp g CategoryTheory.Limits.prod.fst) (h₂ : CategoryTheory.CategoryStruct.comp f CategoryTheory.Limits.prod.snd = CategoryTheory.CategoryStruct.comp g CategoryTheory.Limits.prod.snd) : f = g
• CategoryTheory.Limits.prod.hom_ext_iff 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] {W X Y : C} [CategoryTheory.Limits.HasBinaryProduct X Y] {f g : W ⟶ X ⨯ Y} : f = g ↔ CategoryTheory.CategoryStruct.comp f CategoryTheory.Limits.prod.fst = CategoryTheory.CategoryStruct.comp g CategoryTheory.Limits.prod.fst ∧ CategoryTheory.CategoryStruct.comp f CategoryTheory.Limits.prod.snd = CategoryTheory.CategoryStruct.comp g CategoryTheory.Limits.prod.snd
• CategoryTheory.Limits.prod.associator_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryProducts C] (P Q R : C) : (CategoryTheory.Limits.prod.associator P Q R).hom = CategoryTheory.Limits.prod.lift (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst CategoryTheory.Limits.prod.fst) (CategoryTheory.Limits.prod.lift (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst CategoryTheory.Limits.prod.snd) CategoryTheory.Limits.prod.snd)
• CategoryTheory.Limits.prod.associator_inv 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryProducts C] (P Q R : C) : (CategoryTheory.Limits.prod.associator P Q R).inv = CategoryTheory.Limits.prod.lift (CategoryTheory.Limits.prod.lift CategoryTheory.Limits.prod.fst (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.fst)) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.snd)
• CategoryTheory.Limits.prod.diag_map_fst_snd_comp 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) C] {X X' Y Y' : C} (g : X ⟶ Y) (g' : X' ⟶ Y') : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.diag (X ⨯ X')) (CategoryTheory.Limits.prod.map (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst g) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd g')) = CategoryTheory.Limits.prod.map g g'
• CategoryTheory.Limits.prod.diag_map_fst_snd_comp_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) C] {X X' Y Y' : C} (g : X ⟶ Y) (g' : X' ⟶ Y') {Z : C} (h : Y ⨯ Y' ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.diag (X ⨯ X')) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst g) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd g')) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map g g') h
• CategoryTheory.Limits.prodComparison_fst 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.ProdComparison
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{w, u₂} D] (F : CategoryTheory.Functor C D) (A B : C) [CategoryTheory.Limits.HasBinaryProduct A B] [CategoryTheory.Limits.HasBinaryProduct (F.obj A) (F.obj B)] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prodComparison F A B) CategoryTheory.Limits.prod.fst = F.map CategoryTheory.Limits.prod.fst
• CategoryTheory.Limits.prodComparison_fst_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.ProdComparison
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{w, u₂} D] (F : CategoryTheory.Functor C D) (A B : C) [CategoryTheory.Limits.HasBinaryProduct A B] [CategoryTheory.Limits.HasBinaryProduct (F.obj A) (F.obj B)] {Z : D} (h : F.obj A ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prodComparison F A B) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst h) = CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.prod.fst) h
• CategoryTheory.Limits.inv_prodComparison_map_fst 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.ProdComparison
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{w, u₂} D] (F : CategoryTheory.Functor C D) {A B : C} [CategoryTheory.Limits.HasBinaryProduct A B] [CategoryTheory.Limits.HasBinaryProduct (F.obj A) (F.obj B)] [CategoryTheory.IsIso (CategoryTheory.Limits.prodComparison F A B)] : CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (CategoryTheory.Limits.prodComparison F A B)) (F.map CategoryTheory.Limits.prod.fst) = CategoryTheory.Limits.prod.fst
• CategoryTheory.Limits.inv_prodComparison_map_fst_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.ProdComparison
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{w, u₂} D] (F : CategoryTheory.Functor C D) {A B : C} [CategoryTheory.Limits.HasBinaryProduct A B] [CategoryTheory.Limits.HasBinaryProduct (F.obj A) (F.obj B)] [CategoryTheory.IsIso (CategoryTheory.Limits.prodComparison F A B)] {Z : D} (h : F.obj A ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (CategoryTheory.Limits.prodComparison F A B)) (CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.prod.fst) h) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst h
• CategoryTheory.Limits.pullbackProdFstIsoProd 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) (Z : C) [CategoryTheory.Limits.HasBinaryProduct Y Z] [CategoryTheory.Limits.HasBinaryProduct X Z] [CategoryTheory.Limits.HasPullback f CategoryTheory.Limits.prod.fst] : CategoryTheory.Limits.pullback f CategoryTheory.Limits.prod.fst ≅ X ⨯ Z
• CategoryTheory.Limits.pullbackProdFstIsoProd_inv_fst 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) (Z : C) [CategoryTheory.Limits.HasBinaryProduct Y Z] [CategoryTheory.Limits.HasBinaryProduct X Z] [CategoryTheory.Limits.HasPullback f CategoryTheory.Limits.prod.fst] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackProdFstIsoProd f Z).inv (CategoryTheory.Limits.pullback.fst f CategoryTheory.Limits.prod.fst) = CategoryTheory.Limits.prod.fst
• CategoryTheory.Limits.pullbackProdFstIsoProd_hom_fst 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) (Z : C) [CategoryTheory.Limits.HasBinaryProduct Y Z] [CategoryTheory.Limits.HasBinaryProduct X Z] [CategoryTheory.Limits.HasPullback f CategoryTheory.Limits.prod.fst] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackProdFstIsoProd f Z).hom CategoryTheory.Limits.prod.fst = CategoryTheory.Limits.pullback.fst f CategoryTheory.Limits.prod.fst
• CategoryTheory.Limits.pullbackProdFstIsoProd_inv_snd_snd 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) (Z : C) [CategoryTheory.Limits.HasBinaryProduct Y Z] [CategoryTheory.Limits.HasBinaryProduct X Z] [CategoryTheory.Limits.HasPullback f CategoryTheory.Limits.prod.fst] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackProdFstIsoProd f Z).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f CategoryTheory.Limits.prod.fst) CategoryTheory.Limits.prod.snd) = CategoryTheory.Limits.prod.snd
• CategoryTheory.Limits.pullbackProdSndIsoProd_inv_fst_fst 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) (Z : C) [CategoryTheory.Limits.HasBinaryProduct Z Y] [CategoryTheory.Limits.HasBinaryProduct Z X] [CategoryTheory.Limits.HasPullback CategoryTheory.Limits.prod.snd f] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackProdSndIsoProd f Z).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.prod.snd f) CategoryTheory.Limits.prod.fst) = CategoryTheory.Limits.prod.fst
• CategoryTheory.Limits.pullbackProdFstIsoProd_hom_snd 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) (Z : C) [CategoryTheory.Limits.HasBinaryProduct Y Z] [CategoryTheory.Limits.HasBinaryProduct X Z] [CategoryTheory.Limits.HasPullback f CategoryTheory.Limits.prod.fst] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackProdFstIsoProd f Z).hom CategoryTheory.Limits.prod.snd = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f CategoryTheory.Limits.prod.fst) CategoryTheory.Limits.prod.snd
• CategoryTheory.Limits.pullbackProdSndIsoProd_hom_fst 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) (Z : C) [CategoryTheory.Limits.HasBinaryProduct Z Y] [CategoryTheory.Limits.HasBinaryProduct Z X] [CategoryTheory.Limits.HasPullback CategoryTheory.Limits.prod.snd f] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackProdSndIsoProd f Z).hom CategoryTheory.Limits.prod.fst = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.prod.snd f) CategoryTheory.Limits.prod.fst
• CategoryTheory.Limits.pullbackProdFstIsoProd_inv_fst_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) (Z : C) [CategoryTheory.Limits.HasBinaryProduct Y Z] [CategoryTheory.Limits.HasBinaryProduct X Z] [CategoryTheory.Limits.HasPullback f CategoryTheory.Limits.prod.fst] {Z✝ : C} (h : X ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackProdFstIsoProd f Z).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f CategoryTheory.Limits.prod.fst) h) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst h
• CategoryTheory.Limits.pullbackProdFstIsoProd_inv_snd_fst 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) (Z : C) [CategoryTheory.Limits.HasBinaryProduct Y Z] [CategoryTheory.Limits.HasBinaryProduct X Z] [CategoryTheory.Limits.HasPullback f CategoryTheory.Limits.prod.fst] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackProdFstIsoProd f Z).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f CategoryTheory.Limits.prod.fst) CategoryTheory.Limits.prod.fst) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst f
• CategoryTheory.Limits.pullbackProdFstIsoProd_hom_fst_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) (Z : C) [CategoryTheory.Limits.HasBinaryProduct Y Z] [CategoryTheory.Limits.HasBinaryProduct X Z] [CategoryTheory.Limits.HasPullback f CategoryTheory.Limits.prod.fst] {Z✝ : C} (h : X ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackProdFstIsoProd f Z).hom (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f CategoryTheory.Limits.prod.fst) h
• CategoryTheory.Limits.pullbackProdFstIsoProd_inv_snd_snd_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) (Z : C) [CategoryTheory.Limits.HasBinaryProduct Y Z] [CategoryTheory.Limits.HasBinaryProduct X Z] [CategoryTheory.Limits.HasPullback f CategoryTheory.Limits.prod.fst] {Z✝ : C} (h : Z ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackProdFstIsoProd f Z).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f CategoryTheory.Limits.prod.fst) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd h)) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd h
• CategoryTheory.Limits.pullbackProdSndIsoProd_inv_fst_fst_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) (Z : C) [CategoryTheory.Limits.HasBinaryProduct Z Y] [CategoryTheory.Limits.HasBinaryProduct Z X] [CategoryTheory.Limits.HasPullback CategoryTheory.Limits.prod.snd f] {Z✝ : C} (h : Z ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackProdSndIsoProd f Z).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.prod.snd f) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst h)) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst h
• CategoryTheory.Limits.pullbackProdFstIsoProd_inv_snd_fst_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) (Z : C) [CategoryTheory.Limits.HasBinaryProduct Y Z] [CategoryTheory.Limits.HasBinaryProduct X Z] [CategoryTheory.Limits.HasPullback f CategoryTheory.Limits.prod.fst] {Z✝ : C} (h : Y ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackProdFstIsoProd f Z).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f CategoryTheory.Limits.prod.fst) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst h)) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst (CategoryTheory.CategoryStruct.comp f h)
• CategoryTheory.Limits.pullbackProdFstIsoProd_hom_snd_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) (Z : C) [CategoryTheory.Limits.HasBinaryProduct Y Z] [CategoryTheory.Limits.HasBinaryProduct X Z] [CategoryTheory.Limits.HasPullback f CategoryTheory.Limits.prod.fst] {Z✝ : C} (h : Z ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackProdFstIsoProd f Z).hom (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f CategoryTheory.Limits.prod.fst) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd h)
• CategoryTheory.Limits.pullbackProdSndIsoProd_hom_fst_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) (Z : C) [CategoryTheory.Limits.HasBinaryProduct Z Y] [CategoryTheory.Limits.HasBinaryProduct Z X] [CategoryTheory.Limits.HasPullback CategoryTheory.Limits.prod.snd f] {Z✝ : C} (h : Z ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackProdSndIsoProd f Z).hom (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.prod.snd f) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst h)
• CategoryTheory.Limits.isSplitEpi_prod_fst 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} [CategoryTheory.Limits.HasLimit (CategoryTheory.Limits.pair X Y)] : CategoryTheory.IsSplitEpi CategoryTheory.Limits.prod.fst
• CategoryTheory.Limits.prod.inl_fst 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (X Y : C) [CategoryTheory.Limits.HasBinaryProduct X Y] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.inl X Y) CategoryTheory.Limits.prod.fst = CategoryTheory.CategoryStruct.id X
• CategoryTheory.Limits.prod.inl_fst_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (X Y : C) [CategoryTheory.Limits.HasBinaryProduct X Y] {Z : C} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.inl X Y) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst h) = h
• CategoryTheory.Limits.prod.inr_fst 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (X Y : C) [CategoryTheory.Limits.HasBinaryProduct X Y] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.inr X Y) CategoryTheory.Limits.prod.fst = 0
• CategoryTheory.Limits.prod.inr_fst_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (X Y : C) [CategoryTheory.Limits.HasBinaryProduct X Y] {Z : C} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.inr X Y) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst h) = CategoryTheory.CategoryStruct.comp 0 h
• CategoryTheory.Limits.isLimitOfHasBinaryProductOfPreservesLimit 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.BinaryProducts
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) (X Y : C) [CategoryTheory.Limits.HasBinaryProduct X Y] [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.pair X Y) G] : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.BinaryFan.mk (G.map CategoryTheory.Limits.prod.fst) (G.map CategoryTheory.Limits.prod.snd))
• CategoryTheory.Limits.PreservesLimitPair.iso_inv_fst 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.BinaryProducts
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) (X Y : C) [CategoryTheory.Limits.HasBinaryProduct X Y] [CategoryTheory.Limits.HasBinaryProduct (G.obj X) (G.obj Y)] [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.pair X Y) G] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.PreservesLimitPair.iso G X Y).inv (G.map CategoryTheory.Limits.prod.fst) = CategoryTheory.Limits.prod.fst
• CategoryTheory.Limits.PreservesLimitPair.iso_inv_fst_assoc 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.BinaryProducts
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) (X Y : C) [CategoryTheory.Limits.HasBinaryProduct X Y] [CategoryTheory.Limits.HasBinaryProduct (G.obj X) (G.obj Y)] [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.pair X Y) G] {Z : D} (h : G.obj X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.PreservesLimitPair.iso G X Y).inv (CategoryTheory.CategoryStruct.comp (G.map CategoryTheory.Limits.prod.fst) h) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst h
• CategoryTheory.Limits.biprod.isoProd_inv 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
  {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} [CategoryTheory.Limits.HasBinaryBiproduct X Y] : (CategoryTheory.Limits.biprod.isoProd X Y).inv = CategoryTheory.Limits.biprod.lift CategoryTheory.Limits.prod.fst CategoryTheory.Limits.prod.snd
• CategoryTheory.Limits.isInitialMul_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.StrictInitial
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasStrictInitialObjects C] {I : C} (X : C) [CategoryTheory.Limits.HasBinaryProduct I X] (hI : CategoryTheory.Limits.IsInitial I) : (CategoryTheory.Limits.isInitialMul X hI).hom = CategoryTheory.Limits.prod.fst
• CategoryTheory.Limits.initialMul_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.StrictInitial
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasStrictInitialObjects C] [CategoryTheory.Limits.HasInitial C] (X : C) [CategoryTheory.Limits.HasBinaryProduct (⊥_ C) X] : (CategoryTheory.Limits.initialMul X).hom = CategoryTheory.Limits.prod.fst
• prodIsoPullback_hom_fst 📋 Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasPullbacks C] (X Y : C) [CategoryTheory.Limits.HasBinaryProduct X Y] : CategoryTheory.CategoryStruct.comp (prodIsoPullback X Y).hom (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.terminal.from X) (CategoryTheory.Limits.terminal.from Y)) = CategoryTheory.Limits.prod.fst
• prodIsoPullback_inv_fst 📋 Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasPullbacks C] (X Y : C) [CategoryTheory.Limits.HasBinaryProduct X Y] : CategoryTheory.CategoryStruct.comp (prodIsoPullback X Y).inv CategoryTheory.Limits.prod.fst = CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.terminal.from X) (CategoryTheory.Limits.terminal.from Y)
• prodIsoPullback_hom_fst_assoc 📋 Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasPullbacks C] (X Y : C) [CategoryTheory.Limits.HasBinaryProduct X Y] {Z : C} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (prodIsoPullback X Y).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.terminal.from X) (CategoryTheory.Limits.terminal.from Y)) h) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst h
• prodIsoPullback_inv_fst_assoc 📋 Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasPullbacks C] (X Y : C) [CategoryTheory.Limits.HasBinaryProduct X Y] {Z : C} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (prodIsoPullback X Y).inv (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.terminal.from X) (CategoryTheory.Limits.terminal.from Y)) h
• CategoryTheory.IsPullback.of_hasBinaryProduct' 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (X Y : C) [CategoryTheory.Limits.HasBinaryProduct X Y] [CategoryTheory.Limits.HasTerminal C] : CategoryTheory.IsPullback CategoryTheory.Limits.prod.fst CategoryTheory.Limits.prod.snd (CategoryTheory.Limits.terminal.from X) (CategoryTheory.Limits.terminal.from Y)
• CategoryTheory.IsPullback.of_prod_fst_with_id 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {A B : C} (f : A ⟶ B) (X : C) [CategoryTheory.Limits.HasBinaryProduct A X] [CategoryTheory.Limits.HasBinaryProduct B X] : CategoryTheory.IsPullback CategoryTheory.Limits.prod.fst (CategoryTheory.Limits.prod.map f (CategoryTheory.CategoryStruct.id X)) f CategoryTheory.Limits.prod.fst
• CategoryTheory.coalgebraToOver_obj 📋 Mathlib.CategoryTheory.Monad.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryProducts C] (A : (CategoryTheory.prodComonad X).Coalgebra) : (CategoryTheory.coalgebraToOver X).obj A = CategoryTheory.Over.mk (CategoryTheory.CategoryStruct.comp A.a CategoryTheory.Limits.prod.fst)
• CategoryTheory.prodComonad_δ_app 📋 Mathlib.CategoryTheory.Monad.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryProducts C] (x✝ : C) : (CategoryTheory.prodComonad X).δ.app x✝ = CategoryTheory.Limits.prod.lift CategoryTheory.Limits.prod.fst (CategoryTheory.CategoryStruct.id (X ⨯ x✝))
• CategoryTheory.coalgebraToOver_map 📋 Mathlib.CategoryTheory.Monad.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryProducts C] {X✝ Y✝ : (CategoryTheory.prodComonad X).Coalgebra} (f : X✝ ⟶ Y✝) : (CategoryTheory.coalgebraToOver X).map f = CategoryTheory.Over.homMk f.f ⋯
• CategoryTheory.Over.star_obj_hom 📋 Mathlib.CategoryTheory.Comma.Over.Pullback
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryProducts C] (X✝ : C) : ((CategoryTheory.Over.star X).obj X✝).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.lift CategoryTheory.Limits.prod.fst (CategoryTheory.CategoryStruct.id (X ⨯ X✝))) CategoryTheory.Limits.prod.fst
• CategoryTheory.Over.starPullbackIsoStar_hom_app_left 📋 Mathlib.CategoryTheory.Comma.Over.Pullback
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryProducts C] [CategoryTheory.Limits.HasPullbacks C] {X Y : C} (f : X ⟶ Y) (X✝ : C) : ((CategoryTheory.Over.starPullbackIsoStar f).hom.app X✝).left = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.map (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.lift CategoryTheory.Limits.prod.fst (CategoryTheory.CategoryStruct.id (Y ⨯ X✝))) CategoryTheory.Limits.prod.fst) f CategoryTheory.Limits.prod.fst f (CategoryTheory.CategoryStruct.id (Y ⨯ X✝)) (CategoryTheory.CategoryStruct.id X) (CategoryTheory.CategoryStruct.id Y) ⋯ ⋯) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackSymmetry CategoryTheory.Limits.prod.fst f).hom (CategoryTheory.Limits.pullbackProdFstIsoProd f X✝).hom)
• CategoryTheory.Over.starPullbackIsoStar_inv_app_left 📋 Mathlib.CategoryTheory.Comma.Over.Pullback
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryProducts C] [CategoryTheory.Limits.HasPullbacks C] {X Y : C} (f : X ⟶ Y) (X✝ : C) : ((CategoryTheory.Over.starPullbackIsoStar f).inv.app X✝).left = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackProdFstIsoProd f X✝).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackSymmetry CategoryTheory.Limits.prod.fst f).inv (CategoryTheory.Limits.pullback.map CategoryTheory.Limits.prod.fst f (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.lift CategoryTheory.Limits.prod.fst (CategoryTheory.CategoryStruct.id (Y ⨯ X✝))) CategoryTheory.Limits.prod.fst) f (CategoryTheory.CategoryStruct.id (Y ⨯ X✝)) (CategoryTheory.CategoryStruct.id X) (CategoryTheory.CategoryStruct.id Y) ⋯ ⋯))
• CategoryTheory.Limits.Types.binaryProductIso_inv_comp_fst 📋 Mathlib.CategoryTheory.Limits.Types.Products
  (X Y : Type u) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Types.binaryProductIso X Y).inv CategoryTheory.Limits.prod.fst = TypeCat.ofHom Prod.fst
• CategoryTheory.Limits.Types.binaryProductIso_hom_comp_fst 📋 Mathlib.CategoryTheory.Limits.Types.Products
  (X Y : Type u) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Types.binaryProductIso X Y).hom (TypeCat.ofHom Prod.fst) = CategoryTheory.Limits.prod.fst
• CategoryTheory.Limits.Types.binaryProductIso_inv_comp_fst_apply 📋 Mathlib.CategoryTheory.Limits.Types.Products
  (X Y : Type u) (x : X × Y) : (CategoryTheory.ConcreteCategory.hom CategoryTheory.Limits.prod.fst) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Types.binaryProductIso X Y).inv) x) = x.1
• CategoryTheory.Limits.Types.binaryProductIso_hom_comp_fst_apply 📋 Mathlib.CategoryTheory.Limits.Types.Products
  (X Y : Type u) (x : X ⨯ Y) : ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Types.binaryProductIso X Y).hom) x).1 = (CategoryTheory.ConcreteCategory.hom CategoryTheory.Limits.prod.fst) x
• CategoryTheory.ProdPreservesConnectedLimits.γ₁_app 📋 Mathlib.CategoryTheory.Limits.Connected
  {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] [CategoryTheory.Limits.HasBinaryProducts C] {J : Type v₂} [CategoryTheory.SmallCategory J] {K : CategoryTheory.Functor J C} (X : C) (x✝ : J) : (CategoryTheory.ProdPreservesConnectedLimits.γ₁ X).app x✝ = CategoryTheory.Limits.prod.fst
• CategoryTheory.Limits.hasLimit_cospan_of_hasLimit_pair_of_hasLimit_parallelPair 📋 Mathlib.CategoryTheory.Limits.Constructions.Pullbacks
  {C : Type u} [𝒞 : CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [CategoryTheory.Limits.HasLimit (CategoryTheory.Limits.pair X Y)] [CategoryTheory.Limits.HasLimit (CategoryTheory.Limits.parallelPair (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst f) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd g))] : CategoryTheory.Limits.HasLimit (CategoryTheory.Limits.cospan f g)
• CategoryTheory.Limits.inl_opProdIsoCoprod_inv 📋 Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {A B : C} [CategoryTheory.Limits.HasBinaryProduct A B] : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl (CategoryTheory.Limits.opProdIsoCoprod A B).inv = CategoryTheory.Limits.prod.fst.op
• CategoryTheory.Limits.fst_opProdIsoCoprod_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {A B : C} [CategoryTheory.Limits.HasBinaryProduct A B] : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst.op (CategoryTheory.Limits.opProdIsoCoprod A B).hom = CategoryTheory.Limits.coprod.inl
• CategoryTheory.Limits.opProdIsoCoprod_inv_inl 📋 Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {A B : C} [CategoryTheory.Limits.HasBinaryProduct A B] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.opProdIsoCoprod A B).inv.unop CategoryTheory.Limits.coprod.inl.unop = CategoryTheory.Limits.prod.fst
• CategoryTheory.Limits.opProdIsoCoprod_hom_fst 📋 Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {A B : C} [CategoryTheory.Limits.HasBinaryProduct A B] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.opProdIsoCoprod A B).hom.unop CategoryTheory.Limits.prod.fst = CategoryTheory.Limits.coprod.inl.unop
• CategoryTheory.Limits.inl_opProdIsoCoprod_inv_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {A B : C} [CategoryTheory.Limits.HasBinaryProduct A B] {Z : Cᵒᵖ} (h : Opposite.op (A ⨯ B) ⟶ Z) : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.opProdIsoCoprod A B).inv h) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst.op h
• CategoryTheory.Limits.fst_opProdIsoCoprod_hom_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {A B : C} [CategoryTheory.Limits.HasBinaryProduct A B] {Z : Cᵒᵖ} (h : Opposite.op A ⨿ Opposite.op B ⟶ Z) : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst.op (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.opProdIsoCoprod A B).hom h) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl h
• CategoryTheory.Limits.opProdIsoCoprod_inv_inl_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {A B : C} [CategoryTheory.Limits.HasBinaryProduct A B] {Z : C} (h : A ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.opProdIsoCoprod A B).inv.unop (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl.unop h) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst h
• CategoryTheory.Limits.opProdIsoCoprod_hom_fst_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {A B : C} [CategoryTheory.Limits.HasBinaryProduct A B] {Z : C} (h : A ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.opProdIsoCoprod A B).hom.unop (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst h) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl.unop h
• CategoryTheory.Limits.Concrete.prodEquiv_apply_fst 📋 Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type w} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [CategoryTheory.ConcreteCategory C FC] (X₁ X₂ : C) [CategoryTheory.Limits.HasBinaryProduct X₁ X₂] [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.pair X₁ X₂) (CategoryTheory.forget C)] (x : CategoryTheory.ToType (X₁ ⨯ X₂)) : ((CategoryTheory.Limits.Concrete.prodEquiv X₁ X₂) x).1 = (CategoryTheory.ConcreteCategory.hom CategoryTheory.Limits.prod.fst) x
• CategoryTheory.Limits.Concrete.prodEquiv_symm_apply_fst 📋 Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type w} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [CategoryTheory.ConcreteCategory C FC] (X₁ X₂ : C) [CategoryTheory.Limits.HasBinaryProduct X₁ X₂] [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.pair X₁ X₂) (CategoryTheory.forget C)] (x : CategoryTheory.ToType X₁ × CategoryTheory.ToType X₂) : (CategoryTheory.ConcreteCategory.hom CategoryTheory.Limits.prod.fst) ((CategoryTheory.Limits.Concrete.prodEquiv X₁ X₂).symm x) = x.1
• CategoryTheory.Pretriangulated.binaryProductTriangleIsoBinaryBiproductTriangle_hom_hom₂ 📋 Mathlib.CategoryTheory.Triangulated.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.HasShift C ℤ] (X₁ X₂ : C) [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasBinaryBiproduct X₁ X₂] : (CategoryTheory.Pretriangulated.binaryProductTriangleIsoBinaryBiproductTriangle X₁ X₂).hom.hom₂ = CategoryTheory.Limits.biprod.lift CategoryTheory.Limits.prod.fst CategoryTheory.Limits.prod.snd
• TopCat.prodIsoProd_inv_fst 📋 Mathlib.Topology.Category.TopCat.Limits.Products
  (X Y : TopCat) : CategoryTheory.CategoryStruct.comp (X.prodIsoProd Y).inv CategoryTheory.Limits.prod.fst = TopCat.prodFst
• TopCat.prodIsoProd_hom_fst 📋 Mathlib.Topology.Category.TopCat.Limits.Products
  (X Y : TopCat) : CategoryTheory.CategoryStruct.comp (X.prodIsoProd Y).hom TopCat.prodFst = CategoryTheory.Limits.prod.fst
• TopCat.prodIsoProd_inv_fst_assoc 📋 Mathlib.Topology.Category.TopCat.Limits.Products
  (X Y : TopCat) {Z : TopCat} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.prodIsoProd Y).inv (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst h) = CategoryTheory.CategoryStruct.comp TopCat.prodFst h
• TopCat.prodIsoProd_hom_fst_assoc 📋 Mathlib.Topology.Category.TopCat.Limits.Products
  (X Y : TopCat) {Z : TopCat} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.prodIsoProd Y).hom (CategoryTheory.CategoryStruct.comp TopCat.prodFst h) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst h
• TopCat.prodIsoProd_inv_fst_apply 📋 Mathlib.Topology.Category.TopCat.Limits.Products
  (X Y : TopCat) (x : ↑X × ↑Y) : (CategoryTheory.ConcreteCategory.hom CategoryTheory.Limits.prod.fst) ((CategoryTheory.ConcreteCategory.hom (X.prodIsoProd Y).inv) x) = x.1
• TopCat.prod_topology 📋 Mathlib.Topology.Category.TopCat.Limits.Products
  {X Y : TopCat} : (X ⨯ Y).str = TopologicalSpace.induced (⇑(CategoryTheory.ConcreteCategory.hom CategoryTheory.Limits.prod.fst)) X.str ⊓ TopologicalSpace.induced (⇑(CategoryTheory.ConcreteCategory.hom CategoryTheory.Limits.prod.snd)) Y.str
• TopCat.prodIsoProd_hom_apply 📋 Mathlib.Topology.Category.TopCat.Limits.Products
  {X Y : TopCat} (x : ↑(X ⨯ Y)) : (CategoryTheory.ConcreteCategory.hom (X.prodIsoProd Y).hom) x = ((CategoryTheory.ConcreteCategory.hom CategoryTheory.Limits.prod.fst) x, (CategoryTheory.ConcreteCategory.hom CategoryTheory.Limits.prod.snd) x)
• TopCat.range_prod_map 📋 Mathlib.Topology.Category.TopCat.Limits.Products
  {W X Y Z : TopCat} (f : W ⟶ Y) (g : X ⟶ Z) : Set.range ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.prod.map f g)) = ⇑(CategoryTheory.ConcreteCategory.hom CategoryTheory.Limits.prod.fst) ⁻¹' Set.range ⇑(CategoryTheory.ConcreteCategory.hom f) ∩ ⇑(CategoryTheory.ConcreteCategory.hom CategoryTheory.Limits.prod.snd) ⁻¹' Set.range ⇑(CategoryTheory.ConcreteCategory.hom g)
• TopCat.range_pullback_to_prod 📋 Mathlib.Topology.Category.TopCat.Limits.Pullbacks
  {X Y Z : TopCat} (f : X ⟶ Z) (g : Y ⟶ Z) : Set.range ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.prod.lift (CategoryTheory.Limits.pullback.fst f g) (CategoryTheory.Limits.pullback.snd f g))) = {x | (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst f)) x = (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd g)) x}
• CategoryTheory.Over.prodLeftIsoPullback_hom_fst 📋 Mathlib.CategoryTheory.Limits.Constructions.Over.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} (Y Z : CategoryTheory.Over X) [CategoryTheory.Limits.HasPullback Y.hom Z.hom] [CategoryTheory.Limits.HasBinaryProduct Y Z] : CategoryTheory.CategoryStruct.comp (Y.prodLeftIsoPullback Z).hom (CategoryTheory.Limits.pullback.fst Y.hom Z.hom) = CategoryTheory.Over.Hom.left CategoryTheory.Limits.prod.fst
• CategoryTheory.Over.prodLeftIsoPullback_inv_fst 📋 Mathlib.CategoryTheory.Limits.Constructions.Over.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} (Y Z : CategoryTheory.Over X) [CategoryTheory.Limits.HasPullback Y.hom Z.hom] [CategoryTheory.Limits.HasBinaryProduct Y Z] : CategoryTheory.CategoryStruct.comp (Y.prodLeftIsoPullback Z).inv (CategoryTheory.Over.Hom.left CategoryTheory.Limits.prod.fst) = CategoryTheory.Limits.pullback.fst Y.hom Z.hom
• CategoryTheory.Over.prodLeftIsoPullback_hom_fst_assoc 📋 Mathlib.CategoryTheory.Limits.Constructions.Over.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} (Y Z : CategoryTheory.Over X) [CategoryTheory.Limits.HasPullback Y.hom Z.hom] [CategoryTheory.Limits.HasBinaryProduct Y Z] {Z✝ : C} (h : Y.left ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (Y.prodLeftIsoPullback Z).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst Y.hom Z.hom) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left CategoryTheory.Limits.prod.fst) h
• CategoryTheory.Over.prodLeftIsoPullback_inv_fst_assoc 📋 Mathlib.CategoryTheory.Limits.Constructions.Over.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} (Y Z : CategoryTheory.Over X) [CategoryTheory.Limits.HasPullback Y.hom Z.hom] [CategoryTheory.Limits.HasBinaryProduct Y Z] {Z✝ : C} (h : Y.left ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (Y.prodLeftIsoPullback Z).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left CategoryTheory.Limits.prod.fst) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst Y.hom Z.hom) h
• HomotopicalAlgebra.instFibrationFstOfIsFibrant 📋 Mathlib.AlgebraicTopology.ModelCategory.IsCofibrant
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [HomotopicalAlgebra.CategoryWithFibrations C] [CategoryTheory.Limits.HasTerminal C] (X Y : C) [(HomotopicalAlgebra.fibrations C).IsStableUnderBaseChange] [CategoryTheory.Limits.HasBinaryProduct X Y] [hY : HomotopicalAlgebra.IsFibrant Y] : HomotopicalAlgebra.Fibration CategoryTheory.Limits.prod.fst
• HomotopicalAlgebra.PrepathObject.p_fst 📋 Mathlib.AlgebraicTopology.ModelCategory.PathObject
  {C : Type u} [CategoryTheory.Category.{v, u} C] {A : C} (P : HomotopicalAlgebra.PrepathObject A) [CategoryTheory.Limits.HasBinaryProduct A A] : CategoryTheory.CategoryStruct.comp P.p CategoryTheory.Limits.prod.fst = P.p₀
• HomotopicalAlgebra.PrepathObject.p_fst_assoc 📋 Mathlib.AlgebraicTopology.ModelCategory.PathObject
  {C : Type u} [CategoryTheory.Category.{v, u} C] {A : C} (P : HomotopicalAlgebra.PrepathObject A) [CategoryTheory.Limits.HasBinaryProduct A A] {Z : C} (h : A ⟶ Z) : CategoryTheory.CategoryStruct.comp P.p (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst h) = CategoryTheory.CategoryStruct.comp P.p₀ h
• HomotopicalAlgebra.PathObject.ofFactorizationData_p₀ 📋 Mathlib.AlgebraicTopology.ModelCategory.PathObject
  {C : Type u} [CategoryTheory.Category.{v, u} C] [HomotopicalAlgebra.ModelCategory C] {A : C} (h : (HomotopicalAlgebra.trivialCofibrations C).MapFactorizationData (HomotopicalAlgebra.fibrations C) (CategoryTheory.Limits.diag A)) : (HomotopicalAlgebra.PathObject.ofFactorizationData h).p₀ = CategoryTheory.CategoryStruct.comp h.p CategoryTheory.Limits.prod.fst
• HomotopicalAlgebra.FibrantBrownFactorization.mk'_p 📋 Mathlib.AlgebraicTopology.ModelCategory.BrownLemma
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [HomotopicalAlgebra.ModelCategory C] {X Y : C} (f : X ⟶ Y) [HomotopicalAlgebra.IsFibrant X] [HomotopicalAlgebra.IsFibrant Y] (h : (HomotopicalAlgebra.trivialCofibrations C).MapFactorizationData (HomotopicalAlgebra.fibrations C) (CategoryTheory.Limits.prod.lift f (CategoryTheory.CategoryStruct.id X))) : (HomotopicalAlgebra.FibrantBrownFactorization.mk' f h).p = CategoryTheory.CategoryStruct.comp h.p CategoryTheory.Limits.prod.fst
• CategoryTheory.Limits.prodZeroIso_hom 📋 Mathlib.CategoryTheory.Limits.Constructions.ZeroObjects
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] (X : C) : (CategoryTheory.Limits.prodZeroIso X).hom = CategoryTheory.Limits.prod.fst
• CategoryTheory.Limits.prodZeroIso_iso_inv_snd 📋 Mathlib.CategoryTheory.Limits.Constructions.ZeroObjects
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] (X : C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prodZeroIso X).inv CategoryTheory.Limits.prod.fst = CategoryTheory.CategoryStruct.id X
• CategoryTheory.Limits.pullbackZeroZeroIso_inv_fst 📋 Mathlib.CategoryTheory.Limits.Constructions.ZeroObjects
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] (X Y : C) [CategoryTheory.Limits.HasBinaryProduct X Y] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackZeroZeroIso X Y).inv (CategoryTheory.Limits.pullback.fst 0 0) = CategoryTheory.Limits.prod.fst
• CategoryTheory.Limits.pullbackZeroZeroIso_hom_fst 📋 Mathlib.CategoryTheory.Limits.Constructions.ZeroObjects
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] (X Y : C) [CategoryTheory.Limits.HasBinaryProduct X Y] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackZeroZeroIso X Y).hom CategoryTheory.Limits.prod.fst = CategoryTheory.Limits.pullback.fst 0 0
• AlgebraicGeometry.Scheme.coprodPresheafObjIso_hom_fst 📋 Mathlib.AlgebraicGeometry.Limits
  {X Y : AlgebraicGeometry.Scheme} (U : (X ⨿ Y).Opens) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.coprodPresheafObjIso U).hom CategoryTheory.Limits.prod.fst = AlgebraicGeometry.Scheme.Hom.app CategoryTheory.Limits.coprod.inl U
• AlgebraicGeometry.Scheme.coprodPresheafObjIso_hom_fst_assoc 📋 Mathlib.AlgebraicGeometry.Limits
  {X Y : AlgebraicGeometry.Scheme} (U : (X ⨿ Y).Opens) {Z : CommRingCat} (h : X.presheaf.obj (Opposite.op ((TopologicalSpace.Opens.map CategoryTheory.Limits.coprod.inl.base).obj U)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.coprodPresheafObjIso U).hom (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst h) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.app CategoryTheory.Limits.coprod.inl U) h
• CategoryTheory.Dial.comp_F 📋 Mathlib.CategoryTheory.Dialectica.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasPullbacks C] {x✝ x✝¹ x✝² : CategoryTheory.Dial C} (F : x✝.Hom x✝¹) (G : x✝¹.Hom x✝²) : (CategoryTheory.CategoryStruct.comp F G).F = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.lift CategoryTheory.Limits.prod.fst (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map F.f (CategoryTheory.CategoryStruct.id x✝².tgt)) G.F)) F.F
• CategoryTheory.Dial.Hom.le 📋 Mathlib.CategoryTheory.Dialectica.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasPullbacks C] {X Y : CategoryTheory.Dial C} (self : X.Hom Y) : (CategoryTheory.Subobject.pullback (CategoryTheory.Limits.prod.lift CategoryTheory.Limits.prod.fst self.F)).obj X.rel ≤ (CategoryTheory.Subobject.pullback (CategoryTheory.Limits.prod.map self.f (CategoryTheory.CategoryStruct.id Y.tgt))).obj Y.rel
• CategoryTheory.Dial.Hom.mk 📋 Mathlib.CategoryTheory.Dialectica.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasPullbacks C] {X Y : CategoryTheory.Dial C} (f : X.src ⟶ Y.src) (F : X.src ⨯ Y.tgt ⟶ X.tgt) (le : (CategoryTheory.Subobject.pullback (CategoryTheory.Limits.prod.lift CategoryTheory.Limits.prod.fst F)).obj X.rel ≤ (CategoryTheory.Subobject.pullback (CategoryTheory.Limits.prod.map f (CategoryTheory.CategoryStruct.id Y.tgt))).obj Y.rel) : X.Hom Y
• CategoryTheory.Dial.comp_le_lemma 📋 Mathlib.CategoryTheory.Dialectica.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasPullbacks C] {X Y Z : CategoryTheory.Dial C} (F : X.Hom Y) (G : Y.Hom Z) : (CategoryTheory.Subobject.pullback (CategoryTheory.Limits.prod.lift CategoryTheory.Limits.prod.fst (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.lift CategoryTheory.Limits.prod.fst (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map F.f (CategoryTheory.CategoryStruct.id Z.tgt)) G.F)) F.F))).obj X.rel ≤ (CategoryTheory.Subobject.pullback (CategoryTheory.Limits.prod.map (CategoryTheory.CategoryStruct.comp F.f G.f) (CategoryTheory.CategoryStruct.id Z.tgt))).obj Z.rel
• CategoryTheory.Dial.rightUnitorImpl_hom_f 📋 Mathlib.CategoryTheory.Dialectica.Monoidal
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasPullbacks C] (X : CategoryTheory.Dial C) : X.rightUnitorImpl.hom.f = CategoryTheory.Limits.prod.fst
• CategoryTheory.Dial.rightUnitor_hom_f 📋 Mathlib.CategoryTheory.Dialectica.Monoidal
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasPullbacks C] (X : CategoryTheory.Dial C) : (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom.f = CategoryTheory.Limits.prod.fst
• CategoryTheory.Dial.braiding_hom_f 📋 Mathlib.CategoryTheory.Dialectica.Monoidal
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasPullbacks C] (X Y : CategoryTheory.Dial C) : (X.braiding Y).hom.f = CategoryTheory.Limits.prod.lift CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.fst
• CategoryTheory.Dial.braiding_inv_f 📋 Mathlib.CategoryTheory.Dialectica.Monoidal
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasPullbacks C] (X Y : CategoryTheory.Dial C) : (X.braiding Y).inv.f = CategoryTheory.Limits.prod.lift CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.fst
• CategoryTheory.Dial.rightUnitorImpl_inv_F 📋 Mathlib.CategoryTheory.Dialectica.Monoidal
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasPullbacks C] (X : CategoryTheory.Dial C) : X.rightUnitorImpl.inv.F = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.fst
• CategoryTheory.Dial.rightUnitor_inv_F 📋 Mathlib.CategoryTheory.Dialectica.Monoidal
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasPullbacks C] (X : CategoryTheory.Dial C) : (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).inv.F = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.fst
• CategoryTheory.Dial.tensorHomImpl_F 📋 Mathlib.CategoryTheory.Dialectica.Monoidal
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasPullbacks C] {X₁ X₂ Y₁ Y₂ : CategoryTheory.Dial C} (f : X₁ ⟶ X₂) (g : Y₁ ⟶ Y₂) : (CategoryTheory.Dial.tensorHomImpl f g).F = CategoryTheory.Limits.prod.lift (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map CategoryTheory.Limits.prod.fst CategoryTheory.Limits.prod.fst) f.F) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.snd) g.F)
• CategoryTheory.Dial.whiskerLeft_F 📋 Mathlib.CategoryTheory.Dialectica.Monoidal
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasPullbacks C] (X x✝ x✝¹ : CategoryTheory.Dial C) (f : x✝ ⟶ x✝¹) : (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f).F = CategoryTheory.Limits.prod.lift (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.fst) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.snd) f.F)
• CategoryTheory.Dial.whiskerRight_F 📋 Mathlib.CategoryTheory.Dialectica.Monoidal
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasPullbacks C] {X₁✝ X₂✝ : CategoryTheory.Dial C} (f : X₁✝ ⟶ X₂✝) (Y : CategoryTheory.Dial C) : (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Y).F = CategoryTheory.Limits.prod.lift (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map CategoryTheory.Limits.prod.fst CategoryTheory.Limits.prod.fst) f.F) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.snd)
• CategoryTheory.Dial.tensorHom_F 📋 Mathlib.CategoryTheory.Dialectica.Monoidal
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasPullbacks C] {X₁✝ Y₁✝ X₂✝ Y₂✝ : CategoryTheory.Dial C} (f : X₁✝ ⟶ Y₁✝) (g : X₂✝ ⟶ Y₂✝) : (CategoryTheory.MonoidalCategoryStruct.tensorHom f g).F = CategoryTheory.Limits.prod.lift (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map CategoryTheory.Limits.prod.fst CategoryTheory.Limits.prod.fst) f.F) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.snd) g.F)
• CategoryTheory.Dial.braiding_hom_F 📋 Mathlib.CategoryTheory.Dialectica.Monoidal
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasPullbacks C] (X Y : CategoryTheory.Dial C) : (X.braiding Y).hom.F = CategoryTheory.Limits.prod.lift (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.snd) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.fst)
• CategoryTheory.Dial.braiding_inv_F 📋 Mathlib.CategoryTheory.Dialectica.Monoidal
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasPullbacks C] (X Y : CategoryTheory.Dial C) : (X.braiding Y).inv.F = CategoryTheory.Limits.prod.lift (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.snd) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.fst)
• CategoryTheory.Dial.associatorImpl_hom_f 📋 Mathlib.CategoryTheory.Dialectica.Monoidal
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasPullbacks C] (X Y Z : CategoryTheory.Dial C) : (X.associatorImpl Y Z).hom.f = CategoryTheory.Limits.prod.lift (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst CategoryTheory.Limits.prod.fst) (CategoryTheory.Limits.prod.lift (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst CategoryTheory.Limits.prod.snd) CategoryTheory.Limits.prod.snd)
• CategoryTheory.Dial.associatorImpl_inv_f 📋 Mathlib.CategoryTheory.Dialectica.Monoidal
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasPullbacks C] (X Y Z : CategoryTheory.Dial C) : (X.associatorImpl Y Z).inv.f = CategoryTheory.Limits.prod.lift (CategoryTheory.Limits.prod.lift CategoryTheory.Limits.prod.fst (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.fst)) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.snd)
• CategoryTheory.Dial.associator_hom_f 📋 Mathlib.CategoryTheory.Dialectica.Monoidal
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasPullbacks C] (X Y Z : CategoryTheory.Dial C) : (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom.f = CategoryTheory.Limits.prod.lift (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst CategoryTheory.Limits.prod.fst) (CategoryTheory.Limits.prod.lift (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst CategoryTheory.Limits.prod.snd) CategoryTheory.Limits.prod.snd)
• CategoryTheory.Dial.associator_inv_f 📋 Mathlib.CategoryTheory.Dialectica.Monoidal
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasPullbacks C] (X Y Z : CategoryTheory.Dial C) : (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).inv.f = CategoryTheory.Limits.prod.lift (CategoryTheory.Limits.prod.lift CategoryTheory.Limits.prod.fst (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.fst)) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.snd)
• CategoryTheory.Dial.tensorObjImpl_rel 📋 Mathlib.CategoryTheory.Dialectica.Monoidal
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasPullbacks C] (X Y : CategoryTheory.Dial C) : (X.tensorObjImpl Y).rel = (CategoryTheory.Subobject.pullback (CategoryTheory.Limits.prod.map CategoryTheory.Limits.prod.fst CategoryTheory.Limits.prod.fst)).obj X.rel ⊓ (CategoryTheory.Subobject.pullback (CategoryTheory.Limits.prod.map CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.snd)).obj Y.rel
• CategoryTheory.Dial.tensorObj_rel 📋 Mathlib.CategoryTheory.Dialectica.Monoidal
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasPullbacks C] (X Y : CategoryTheory.Dial C) : (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).rel = (CategoryTheory.Subobject.pullback (CategoryTheory.Limits.prod.map CategoryTheory.Limits.prod.fst CategoryTheory.Limits.prod.fst)).obj X.rel ⊓ (CategoryTheory.Subobject.pullback (CategoryTheory.Limits.prod.map CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.snd)).obj Y.rel
• CategoryTheory.Dial.associatorImpl_hom_F 📋 Mathlib.CategoryTheory.Dialectica.Monoidal
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasPullbacks C] (X Y Z : CategoryTheory.Dial C) : (X.associatorImpl Y Z).hom.F = CategoryTheory.Limits.prod.lift (CategoryTheory.Limits.prod.lift (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.fst) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.fst))) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.snd))
• CategoryTheory.Dial.associatorImpl_inv_F 📋 Mathlib.CategoryTheory.Dialectica.Monoidal
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasPullbacks C] (X Y Z : CategoryTheory.Dial C) : (X.associatorImpl Y Z).inv.F = CategoryTheory.Limits.prod.lift (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst CategoryTheory.Limits.prod.fst)) (CategoryTheory.Limits.prod.lift (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst CategoryTheory.Limits.prod.snd)) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.snd))
• CategoryTheory.Dial.associator_hom_F 📋 Mathlib.CategoryTheory.Dialectica.Monoidal
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasPullbacks C] (X Y Z : CategoryTheory.Dial C) : (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom.F = CategoryTheory.Limits.prod.lift (CategoryTheory.Limits.prod.lift (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.fst) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.fst))) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.snd))
• CategoryTheory.Dial.associator_inv_F 📋 Mathlib.CategoryTheory.Dialectica.Monoidal
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasPullbacks C] (X Y Z : CategoryTheory.Dial C) : (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).inv.F = CategoryTheory.Limits.prod.lift (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst CategoryTheory.Limits.prod.fst)) (CategoryTheory.Limits.prod.lift (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst CategoryTheory.Limits.prod.snd)) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.snd))
• CategoryTheory.PreGaloisCategory.fiberBinaryProductEquiv_symm_fst_apply 📋 Mathlib.CategoryTheory.Galois.Basic
  {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.PreGaloisCategory C] [CategoryTheory.PreGaloisCategory.FiberFunctor F] {X Y : C} (x : (F.obj X).obj) (y : (F.obj Y).obj) : (CategoryTheory.ConcreteCategory.hom (F.map CategoryTheory.Limits.prod.fst)) ((CategoryTheory.PreGaloisCategory.fiberBinaryProductEquiv F X Y).symm (x, y)) = x
• CategoryTheory.FunctorToTypes.binaryProductIso_inv_comp_fst 📋 Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes
  {C : Type u} [CategoryTheory.Category.{v, u} C] (F G : CategoryTheory.Functor C (Type w)) : CategoryTheory.CategoryStruct.comp (CategoryTheory.FunctorToTypes.binaryProductIso F G).inv CategoryTheory.Limits.prod.fst = CategoryTheory.FunctorToTypes.prod.fst
• CategoryTheory.FunctorToTypes.binaryProductIso_hom_comp_fst 📋 Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes
  {C : Type u} [CategoryTheory.Category.{v, u} C] (F G : CategoryTheory.Functor C (Type w)) : CategoryTheory.CategoryStruct.comp (CategoryTheory.FunctorToTypes.binaryProductIso F G).hom CategoryTheory.FunctorToTypes.prod.fst = CategoryTheory.Limits.prod.fst
• CategoryTheory.FunctorToTypes.prodMk_fst 📋 Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F G : CategoryTheory.Functor C (Type w)} {a : C} (x : F.obj a) (y : G.obj a) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.prod.fst.app a)) (CategoryTheory.FunctorToTypes.prodMk x y) = x
• CategoryTheory.FunctorToTypes.binaryProductIso_inv_comp_fst_apply 📋 Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes
  {C : Type u} [CategoryTheory.Category.{v, u} C] (F G : CategoryTheory.Functor C (Type w)) (a : C) (z : (CategoryTheory.FunctorToTypes.prod F G).obj a) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.prod.fst.app a)) ((CategoryTheory.ConcreteCategory.hom ((CategoryTheory.FunctorToTypes.binaryProductIso F G).inv.app a)) z) = z.1
• CategoryTheory.FunctorToTypes.prod_ext' 📋 Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes
  {C : Type u} [CategoryTheory.Category.{v, u} C] (F G : CategoryTheory.Functor C (Type w)) (a : C) (z w : (F ⨯ G).obj a) (h1 : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.prod.fst.app a)) z = (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.prod.fst.app a)) w) (h2 : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.prod.snd.app a)) z = (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.prod.snd.app a)) w) : z = w
• CategoryTheory.FunctorToTypes.prod_ext'_iff 📋 Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F G : CategoryTheory.Functor C (Type w)} {a : C} {z w : (F ⨯ G).obj a} : z = w ↔ (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.prod.fst.app a)) z = (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.prod.fst.app a)) w ∧ (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.prod.snd.app a)) z = (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.prod.snd.app a)) w
• CategoryTheory.Limits.Pi.map_eq_prod_map 📋 Mathlib.CategoryTheory.Limits.Shapes.PiProd
  {C : Type u_1} {I : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] {X Y : I → C} (f : (i : I) → X i ⟶ Y i) (P : I → Prop) [CategoryTheory.Limits.HasProduct X] [CategoryTheory.Limits.HasProduct Y] [CategoryTheory.Limits.HasProduct fun i => X ↑i] [CategoryTheory.Limits.HasProduct fun i => X ↑i] [CategoryTheory.Limits.HasProduct fun i => Y ↑i] [CategoryTheory.Limits.HasProduct fun i => Y ↑i] [(i : I) → Decidable (P i)] : CategoryTheory.Limits.Pi.map f = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Limits.Pi.binaryFanOfPropIsLimit X P).conePointUniqueUpToIso (CategoryTheory.Limits.prodIsProd (∏ᶜ fun i => X ↑i) (∏ᶜ fun i => X ↑i))).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map (CategoryTheory.Limits.Pi.map fun i => f ↑i) (CategoryTheory.Limits.Pi.map fun i => f ↑i)) ((CategoryTheory.Limits.Pi.binaryFanOfPropIsLimit Y P).conePointUniqueUpToIso (CategoryTheory.Limits.prodIsProd (∏ᶜ fun i => Y ↑i) (∏ᶜ fun i => Y ↑i))).inv)
• CategoryTheory.IsPullback.of_hasBinaryProduct 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} [CategoryTheory.Limits.HasBinaryProduct X Y] : CategoryTheory.IsPullback CategoryTheory.Limits.prod.fst CategoryTheory.Limits.prod.snd 0 0
• CategoryTheory.Limits.hasWeakLimit_cospan_of_hasLimit_pair_of_hasWeakLimit_parallelPair 📋 Mathlib.CategoryTheory.Limits.WeakLimits.WeakPullbacks
  (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [CategoryTheory.Limits.HasLimit (CategoryTheory.Limits.pair X Y)] [CategoryTheory.Limits.HasWeakLimit (CategoryTheory.Limits.parallelPair (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst f) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd g))] : CategoryTheory.Limits.HasWeakLimit (CategoryTheory.Limits.cospan f g)

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