Loogle!

Result

Found 81 declarations mentioning CategoryTheory.Limits.prod.map.

• CategoryTheory.Limits.prod.map 📋 Mathlib.CategoryTheory.Limits.Shapes.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) : W ⨯ X ⟶ Y ⨯ Z
• CategoryTheory.Limits.prod.map_id_id 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} [CategoryTheory.Limits.HasBinaryProduct X Y] : CategoryTheory.Limits.prod.map (CategoryTheory.CategoryStruct.id X) (CategoryTheory.CategoryStruct.id Y) = CategoryTheory.CategoryStruct.id (X ⨯ Y)
• CategoryTheory.Limits.isIso_prod 📋 Mathlib.CategoryTheory.Limits.Shapes.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.IsIso f] [CategoryTheory.IsIso g] : CategoryTheory.IsIso (CategoryTheory.Limits.prod.map f g)
• CategoryTheory.Limits.prod.map_mono 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {W X Y Z : C} (f : W ⟶ Y) (g : X ⟶ Z) [CategoryTheory.Mono f] [CategoryTheory.Mono g] [CategoryTheory.Limits.HasBinaryProduct W X] [CategoryTheory.Limits.HasBinaryProduct Y Z] : CategoryTheory.Mono (CategoryTheory.Limits.prod.map f g)
• CategoryTheory.Limits.prod.diag_map 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Limits.HasBinaryProduct X X] [CategoryTheory.Limits.HasBinaryProduct Y Y] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.diag X) (CategoryTheory.Limits.prod.map f f) = CategoryTheory.CategoryStruct.comp f (CategoryTheory.Limits.diag Y)
• CategoryTheory.Limits.prod.mapIso_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.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.Limits.prod.mapIso f g).hom = CategoryTheory.Limits.prod.map f.hom g.hom
• CategoryTheory.Limits.prod.mapIso_inv 📋 Mathlib.CategoryTheory.Limits.Shapes.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.Limits.prod.mapIso f g).inv = CategoryTheory.Limits.prod.map f.inv g.inv
• CategoryTheory.Limits.prod.functor_obj_map 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryProducts C] (X : C) {x✝ x✝¹ : C} (g : x✝ ⟶ x✝¹) : (CategoryTheory.Limits.prod.functor.obj X).map g = CategoryTheory.Limits.prod.map (CategoryTheory.CategoryStruct.id X) g
• CategoryTheory.Limits.prod.map_fst 📋 Mathlib.CategoryTheory.Limits.Shapes.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.map_snd 📋 Mathlib.CategoryTheory.Limits.Shapes.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.snd = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd g
• CategoryTheory.Limits.prod.lift_fst_comp_snd_comp 📋 Mathlib.CategoryTheory.Limits.Shapes.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.diag_map_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Limits.HasBinaryProduct X X] [CategoryTheory.Limits.HasBinaryProduct Y Y] {Z : C} (h : Y ⨯ Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.diag X) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map f f) h) = CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.diag Y) h)
• CategoryTheory.Limits.prod.diag_map_fst_snd 📋 Mathlib.CategoryTheory.Limits.Shapes.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.lift_map 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] {V W X Y Z : C} [CategoryTheory.Limits.HasBinaryProduct W X] [CategoryTheory.Limits.HasBinaryProduct Y Z] (f : V ⟶ W) (g : V ⟶ X) (h : W ⟶ Y) (k : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.lift f g) (CategoryTheory.Limits.prod.map h k) = CategoryTheory.Limits.prod.lift (CategoryTheory.CategoryStruct.comp f h) (CategoryTheory.CategoryStruct.comp g k)
• CategoryTheory.Limits.prod.map_fst_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.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.map_snd_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.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 : Z ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map f g) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd h) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd (CategoryTheory.CategoryStruct.comp g h)
• CategoryTheory.Limits.prod.map_comp_id 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z W : C} (f : X ⟶ Y) (g : Y ⟶ Z) [CategoryTheory.Limits.HasBinaryProduct X W] [CategoryTheory.Limits.HasBinaryProduct Z W] [CategoryTheory.Limits.HasBinaryProduct Y W] : CategoryTheory.Limits.prod.map (CategoryTheory.CategoryStruct.comp f g) (CategoryTheory.CategoryStruct.id W) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map f (CategoryTheory.CategoryStruct.id W)) (CategoryTheory.Limits.prod.map g (CategoryTheory.CategoryStruct.id W))
• CategoryTheory.Limits.prod.map_id_comp 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z W : C} (f : X ⟶ Y) (g : Y ⟶ Z) [CategoryTheory.Limits.HasBinaryProduct W X] [CategoryTheory.Limits.HasBinaryProduct W Y] [CategoryTheory.Limits.HasBinaryProduct W Z] : CategoryTheory.Limits.prod.map (CategoryTheory.CategoryStruct.id W) (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map (CategoryTheory.CategoryStruct.id W) f) (CategoryTheory.Limits.prod.map (CategoryTheory.CategoryStruct.id W) g)
• CategoryTheory.Limits.prod.diag_map_fst_snd_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.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.map_map 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] {A₁ A₂ A₃ B₁ B₂ B₃ : C} [CategoryTheory.Limits.HasBinaryProduct A₁ B₁] [CategoryTheory.Limits.HasBinaryProduct A₂ B₂] [CategoryTheory.Limits.HasBinaryProduct A₃ B₃] (f : A₁ ⟶ A₂) (g : B₁ ⟶ B₂) (h : A₂ ⟶ A₃) (k : B₂ ⟶ B₃) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map f g) (CategoryTheory.Limits.prod.map h k) = CategoryTheory.Limits.prod.map (CategoryTheory.CategoryStruct.comp f h) (CategoryTheory.CategoryStruct.comp g k)
• CategoryTheory.Limits.prod.lift_map_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] {V W X Y Z : C} [CategoryTheory.Limits.HasBinaryProduct W X] [CategoryTheory.Limits.HasBinaryProduct Y Z] (f : V ⟶ W) (g : V ⟶ X) (h : W ⟶ Y) (k : X ⟶ Z) {Z✝ : C} (h✝ : Y ⨯ Z ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.lift f g) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map h k) h✝) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.lift (CategoryTheory.CategoryStruct.comp f h) (CategoryTheory.CategoryStruct.comp g k)) h✝
• CategoryTheory.Limits.prod.map_comp_id_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z W : C} (f : X ⟶ Y) (g : Y ⟶ Z) [CategoryTheory.Limits.HasBinaryProduct X W] [CategoryTheory.Limits.HasBinaryProduct Z W] [CategoryTheory.Limits.HasBinaryProduct Y W] {Z✝ : C} (h : Z ⨯ W ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map (CategoryTheory.CategoryStruct.comp f g) (CategoryTheory.CategoryStruct.id W)) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map f (CategoryTheory.CategoryStruct.id W)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map g (CategoryTheory.CategoryStruct.id W)) h)
• CategoryTheory.Limits.prod.map_id_comp_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z W : C} (f : X ⟶ Y) (g : Y ⟶ Z) [CategoryTheory.Limits.HasBinaryProduct W X] [CategoryTheory.Limits.HasBinaryProduct W Y] [CategoryTheory.Limits.HasBinaryProduct W Z] {Z✝ : C} (h : W ⨯ Z ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map (CategoryTheory.CategoryStruct.id W) (CategoryTheory.CategoryStruct.comp f g)) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map (CategoryTheory.CategoryStruct.id W) f) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map (CategoryTheory.CategoryStruct.id W) g) h)
• CategoryTheory.Limits.prod.map_map_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] {A₁ A₂ A₃ B₁ B₂ B₃ : C} [CategoryTheory.Limits.HasBinaryProduct A₁ B₁] [CategoryTheory.Limits.HasBinaryProduct A₂ B₂] [CategoryTheory.Limits.HasBinaryProduct A₃ B₃] (f : A₁ ⟶ A₂) (g : B₁ ⟶ B₂) (h : A₂ ⟶ A₃) (k : B₂ ⟶ B₃) {Z : C} (h✝ : A₃ ⨯ B₃ ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map f g) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map h k) h✝) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map (CategoryTheory.CategoryStruct.comp f h) (CategoryTheory.CategoryStruct.comp g k)) h✝
• CategoryTheory.Limits.prod.functor_map_app 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryProducts C] {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) (T : C) : (CategoryTheory.Limits.prod.functor.map f).app T = CategoryTheory.Limits.prod.map f (CategoryTheory.CategoryStruct.id T)
• CategoryTheory.Limits.prod_rightUnitor_inv_naturality 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasBinaryProducts C] (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.rightUnitor X).inv (CategoryTheory.Limits.prod.map f (CategoryTheory.CategoryStruct.id (⊤_ C))) = CategoryTheory.CategoryStruct.comp f (CategoryTheory.Limits.prod.rightUnitor Y).inv
• CategoryTheory.Limits.prod.leftUnitor_hom_naturality 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasBinaryProducts C] (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map (CategoryTheory.CategoryStruct.id (⊤_ C)) f) (CategoryTheory.Limits.prod.leftUnitor Y).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.leftUnitor X).hom f
• CategoryTheory.Limits.prod.leftUnitor_inv_naturality 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasBinaryProducts C] (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.leftUnitor X).inv (CategoryTheory.Limits.prod.map (CategoryTheory.CategoryStruct.id (⊤_ C)) f) = CategoryTheory.CategoryStruct.comp f (CategoryTheory.Limits.prod.leftUnitor Y).inv
• CategoryTheory.Limits.prod.rightUnitor_hom_naturality 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasBinaryProducts C] (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map f (CategoryTheory.CategoryStruct.id (⊤_ C))) (CategoryTheory.Limits.prod.rightUnitor Y).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.rightUnitor X).hom f
• CategoryTheory.Limits.prodComparison_natural_of_natTrans 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
  {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)] {H : CategoryTheory.Functor C D} [CategoryTheory.Limits.HasBinaryProduct (H.obj A) (H.obj B)] (α : F ⟶ H) : CategoryTheory.CategoryStruct.comp (α.app (A ⨯ B)) (CategoryTheory.Limits.prodComparison H A B) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prodComparison F A B) (CategoryTheory.Limits.prod.map (α.app A) (α.app B))
• CategoryTheory.Limits.prodComparison_natural 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{w, u₂} D] (F : CategoryTheory.Functor C D) {A A' B B' : C} [CategoryTheory.Limits.HasBinaryProduct A B] [CategoryTheory.Limits.HasBinaryProduct A' B'] [CategoryTheory.Limits.HasBinaryProduct (F.obj A) (F.obj B)] [CategoryTheory.Limits.HasBinaryProduct (F.obj A') (F.obj B')] (f : A ⟶ A') (g : B ⟶ B') : CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.Limits.prod.map f g)) (CategoryTheory.Limits.prodComparison F A' B') = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prodComparison F A B) (CategoryTheory.Limits.prod.map (F.map f) (F.map g))
• CategoryTheory.Limits.prod_rightUnitor_inv_naturality_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasBinaryProducts C] (f : X ⟶ Y) {Z : C} (h : Y ⨯ ⊤_ C ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.rightUnitor X).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map f (CategoryTheory.CategoryStruct.id (⊤_ C))) h) = CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.rightUnitor Y).inv h)
• CategoryTheory.Limits.prod.leftUnitor_hom_naturality_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasBinaryProducts C] (f : X ⟶ Y) {Z : C} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map (CategoryTheory.CategoryStruct.id (⊤_ C)) f) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.leftUnitor Y).hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.leftUnitor X).hom (CategoryTheory.CategoryStruct.comp f h)
• CategoryTheory.Limits.prod.leftUnitor_inv_naturality_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasBinaryProducts C] (f : X ⟶ Y) {Z : C} (h : (⊤_ C) ⨯ Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.leftUnitor X).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map (CategoryTheory.CategoryStruct.id (⊤_ C)) f) h) = CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.leftUnitor Y).inv h)
• CategoryTheory.Limits.prod.rightUnitor_hom_naturality_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasBinaryProducts C] (f : X ⟶ Y) {Z : C} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map f (CategoryTheory.CategoryStruct.id (⊤_ C))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.rightUnitor Y).hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.rightUnitor X).hom (CategoryTheory.CategoryStruct.comp f h)
• CategoryTheory.Limits.prod.map_swap 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] {A B X Y : C} (f : A ⟶ B) (g : X ⟶ Y) [CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) C] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map (CategoryTheory.CategoryStruct.id X) f) (CategoryTheory.Limits.prod.map g (CategoryTheory.CategoryStruct.id B)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map g (CategoryTheory.CategoryStruct.id A)) (CategoryTheory.Limits.prod.map (CategoryTheory.CategoryStruct.id Y) f)
• CategoryTheory.Limits.prodComparison_natural_of_natTrans_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
  {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)] {H : CategoryTheory.Functor C D} [CategoryTheory.Limits.HasBinaryProduct (H.obj A) (H.obj B)] (α : F ⟶ H) {Z : D} (h : H.obj A ⨯ H.obj B ⟶ Z) : CategoryTheory.CategoryStruct.comp (α.app (A ⨯ B)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prodComparison H A B) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prodComparison F A B) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map (α.app A) (α.app B)) h)
• CategoryTheory.Limits.prodComparison_natural_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{w, u₂} D] (F : CategoryTheory.Functor C D) {A A' B B' : C} [CategoryTheory.Limits.HasBinaryProduct A B] [CategoryTheory.Limits.HasBinaryProduct A' B'] [CategoryTheory.Limits.HasBinaryProduct (F.obj A) (F.obj B)] [CategoryTheory.Limits.HasBinaryProduct (F.obj A') (F.obj B')] (f : A ⟶ A') (g : B ⟶ B') {Z : D} (h : F.obj A' ⨯ F.obj B' ⟶ Z) : CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.Limits.prod.map f g)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prodComparison F A' B') h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prodComparison F A B) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map (F.map f) (F.map g)) h)
• CategoryTheory.Limits.braid_natural 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryProducts C] {W X Y Z : C} (f : X ⟶ Y) (g : Z ⟶ W) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map f g) (CategoryTheory.Limits.prod.braiding Y W).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.braiding X Z).hom (CategoryTheory.Limits.prod.map g f)
• CategoryTheory.Limits.prod.map_swap_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] {A B X Y : C} (f : A ⟶ B) (g : X ⟶ Y) [CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) C] {Z : C} (h : Y ⨯ B ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map (CategoryTheory.CategoryStruct.id X) f) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map g (CategoryTheory.CategoryStruct.id B)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map g (CategoryTheory.CategoryStruct.id A)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map (CategoryTheory.CategoryStruct.id Y) f) h)
• CategoryTheory.Limits.braid_natural_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryProducts C] {W X Y Z : C} (f : X ⟶ Y) (g : Z ⟶ W) {Z✝ : C} (h : W ⨯ Y ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map f g) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.braiding Y W).hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.braiding X Z).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map g f) h)
• CategoryTheory.Limits.prodComparison_inv_natural 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{w, u₂} D] (F : CategoryTheory.Functor C D) {A A' B B' : C} [CategoryTheory.Limits.HasBinaryProduct A B] [CategoryTheory.Limits.HasBinaryProduct A' B'] [CategoryTheory.Limits.HasBinaryProduct (F.obj A) (F.obj B)] [CategoryTheory.Limits.HasBinaryProduct (F.obj A') (F.obj B')] (f : A ⟶ A') (g : B ⟶ B') [CategoryTheory.IsIso (CategoryTheory.Limits.prodComparison F A 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.map f g)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map (F.map f) (F.map g)) (CategoryTheory.inv (CategoryTheory.Limits.prodComparison F A' B'))
• CategoryTheory.Limits.prod.diag_map_fst_snd_comp 📋 Mathlib.CategoryTheory.Limits.Shapes.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.prodComparison_inv_natural_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{w, u₂} D] (F : CategoryTheory.Functor C D) {A A' B B' : C} [CategoryTheory.Limits.HasBinaryProduct A B] [CategoryTheory.Limits.HasBinaryProduct A' B'] [CategoryTheory.Limits.HasBinaryProduct (F.obj A) (F.obj B)] [CategoryTheory.Limits.HasBinaryProduct (F.obj A') (F.obj B')] (f : A ⟶ A') (g : B ⟶ B') [CategoryTheory.IsIso (CategoryTheory.Limits.prodComparison F A B)] [CategoryTheory.IsIso (CategoryTheory.Limits.prodComparison F A' B')] {Z : D} (h : F.obj (A' ⨯ B') ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (CategoryTheory.Limits.prodComparison F A B)) (CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.Limits.prod.map f g)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map (F.map f) (F.map g)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (CategoryTheory.Limits.prodComparison F A' B')) h)
• CategoryTheory.Limits.prod.diag_map_fst_snd_comp_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.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.prod.triangle 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasBinaryProducts C] (X Y : C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.associator X (⊤_ C) Y).hom (CategoryTheory.Limits.prod.map (CategoryTheory.CategoryStruct.id X) (CategoryTheory.Limits.prod.leftUnitor Y).hom) = CategoryTheory.Limits.prod.map (CategoryTheory.Limits.prod.rightUnitor X).hom (CategoryTheory.CategoryStruct.id Y)
• CategoryTheory.Limits.prod.associator_naturality 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryProducts C] {X₁ X₂ X₃ Y₁ Y₂ Y₃ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (f₃ : X₃ ⟶ Y₃) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map (CategoryTheory.Limits.prod.map f₁ f₂) f₃) (CategoryTheory.Limits.prod.associator Y₁ Y₂ Y₃).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.associator X₁ X₂ X₃).hom (CategoryTheory.Limits.prod.map f₁ (CategoryTheory.Limits.prod.map f₂ f₃))
• CategoryTheory.Limits.prod.associator_naturality_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryProducts C] {X₁ X₂ X₃ Y₁ Y₂ Y₃ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (f₃ : X₃ ⟶ Y₃) {Z : C} (h : Y₁ ⨯ Y₂ ⨯ Y₃ ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map (CategoryTheory.Limits.prod.map f₁ f₂) f₃) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.associator Y₁ Y₂ Y₃).hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.associator X₁ X₂ X₃).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map f₁ (CategoryTheory.Limits.prod.map f₂ f₃)) h)
• CategoryTheory.Limits.prod.pentagon 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryProducts C] (W X Y Z : C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map (CategoryTheory.Limits.prod.associator W X Y).hom (CategoryTheory.CategoryStruct.id Z)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.associator W (X ⨯ Y) Z).hom (CategoryTheory.Limits.prod.map (CategoryTheory.CategoryStruct.id W) (CategoryTheory.Limits.prod.associator X Y Z).hom)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.associator (W ⨯ X) Y Z).hom (CategoryTheory.Limits.prod.associator W X (Y ⨯ Z)).hom
• CategoryTheory.Limits.prod.pentagon_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryProducts C] (W X Y Z : C) {Z✝ : C} (h : W ⨯ X ⨯ Y ⨯ Z ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map (CategoryTheory.Limits.prod.associator W X Y).hom (CategoryTheory.CategoryStruct.id Z)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.associator W (X ⨯ Y) Z).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map (CategoryTheory.CategoryStruct.id W) (CategoryTheory.Limits.prod.associator X Y Z).hom) h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.associator (W ⨯ X) Y Z).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.associator W X (Y ⨯ Z)).hom h)
• CategoryTheory.Limits.prod.map_epi 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
  {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {W X Y Z : C} (f : W ⟶ Y) (g : X ⟶ Z) [CategoryTheory.Epi f] [CategoryTheory.Epi g] [CategoryTheory.Limits.HasBinaryBiproduct W X] [CategoryTheory.Limits.HasBinaryBiproduct Y Z] : CategoryTheory.Epi (CategoryTheory.Limits.prod.map f g)
• 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.prodComonad_map 📋 Mathlib.CategoryTheory.Monad.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryProducts C] {x✝ x✝¹ : C} (g : x✝ ⟶ x✝¹) : (CategoryTheory.prodComonad X).map g = CategoryTheory.Limits.prod.map (CategoryTheory.CategoryStruct.id X) g
• CategoryTheory.Over.star_map_left 📋 Mathlib.CategoryTheory.Comma.Over.Pullback
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryProducts C] {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) : ((CategoryTheory.Over.star X).map f).left = CategoryTheory.Limits.prod.map (CategoryTheory.CategoryStruct.id X) f
• CategoryTheory.NonPreadditiveAbelian.σ_comp 📋 Mathlib.CategoryTheory.Abelian.NonPreadditive
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.NonPreadditiveAbelian C] {X Y : C} (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp CategoryTheory.NonPreadditiveAbelian.σ f = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map f f) CategoryTheory.NonPreadditiveAbelian.σ
• CategoryTheory.NonPreadditiveAbelian.lift_map 📋 Mathlib.CategoryTheory.Abelian.NonPreadditive
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.NonPreadditiveAbelian C] {X Y : C} (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.lift (CategoryTheory.CategoryStruct.id X) 0) (CategoryTheory.Limits.prod.map f f) = CategoryTheory.CategoryStruct.comp f (CategoryTheory.Limits.prod.lift (CategoryTheory.CategoryStruct.id Y) 0)
• CategoryTheory.NonPreadditiveAbelian.lift_map_assoc 📋 Mathlib.CategoryTheory.Abelian.NonPreadditive
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.NonPreadditiveAbelian C] {X Y : C} (f : X ⟶ Y) {Z : C} (h : Y ⨯ Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.lift (CategoryTheory.CategoryStruct.id X) 0) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map f f) h) = CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.lift (CategoryTheory.CategoryStruct.id Y) 0) h)
• TopCat.isEmbedding_prodMap 📋 Mathlib.Topology.Category.TopCat.Limits.Products
  {W X Y Z : TopCat} {f : W ⟶ X} {g : Y ⟶ Z} (hf : Topology.IsEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) (hg : Topology.IsEmbedding ⇑(CategoryTheory.ConcreteCategory.hom g)) : Topology.IsEmbedding ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.prod.map f g))
• TopCat.isInducing_prodMap 📋 Mathlib.Topology.Category.TopCat.Limits.Products
  {W X Y Z : TopCat} {f : W ⟶ X} {g : Y ⟶ Z} (hf : Topology.IsInducing ⇑(CategoryTheory.ConcreteCategory.hom f)) (hg : Topology.IsInducing ⇑(CategoryTheory.ConcreteCategory.hom g)) : Topology.IsInducing ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.prod.map f g))
• 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)
• HomotopicalAlgebra.instFibrationMapOfIsWeakFactorizationSystemTrivialCofibrationsFibrations_1 📋 Mathlib.AlgebraicTopology.ModelCategory.Instances
  (C : Type u) [CategoryTheory.Category.{v, u} C] [HomotopicalAlgebra.CategoryWithWeakEquivalences C] [HomotopicalAlgebra.CategoryWithCofibrations C] [HomotopicalAlgebra.CategoryWithFibrations C] {X₁ X₂ Y₁ Y₂ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) [(HomotopicalAlgebra.trivialCofibrations C).IsWeakFactorizationSystem (HomotopicalAlgebra.fibrations C)] [h₁ : HomotopicalAlgebra.Fibration f₁] [h₂ : HomotopicalAlgebra.Fibration f₂] [CategoryTheory.Limits.HasBinaryProduct X₁ X₂] [CategoryTheory.Limits.HasBinaryProduct Y₁ Y₂] : HomotopicalAlgebra.Fibration (CategoryTheory.Limits.prod.map f₁ f₂)
• 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.isoMk 📋 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} (e₁ : X.src ≅ Y.src) (e₂ : X.tgt ≅ Y.tgt) (eq : X.rel = (CategoryTheory.Subobject.pullback (CategoryTheory.Limits.prod.map e₁.hom e₂.hom)).obj Y.rel) : X ≅ Y
• CategoryTheory.Dial.isoMk_hom_f 📋 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} (e₁ : X.src ≅ Y.src) (e₂ : X.tgt ≅ Y.tgt) (eq : X.rel = (CategoryTheory.Subobject.pullback (CategoryTheory.Limits.prod.map e₁.hom e₂.hom)).obj Y.rel) : (CategoryTheory.Dial.isoMk e₁ e₂ eq).hom.f = e₁.hom
• CategoryTheory.Dial.isoMk_inv_f 📋 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} (e₁ : X.src ≅ Y.src) (e₂ : X.tgt ≅ Y.tgt) (eq : X.rel = (CategoryTheory.Subobject.pullback (CategoryTheory.Limits.prod.map e₁.hom e₂.hom)).obj Y.rel) : (CategoryTheory.Dial.isoMk e₁ e₂ eq).inv.f = e₁.inv
• CategoryTheory.Dial.isoMk_hom_F 📋 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} (e₁ : X.src ≅ Y.src) (e₂ : X.tgt ≅ Y.tgt) (eq : X.rel = (CategoryTheory.Subobject.pullback (CategoryTheory.Limits.prod.map e₁.hom e₂.hom)).obj Y.rel) : (CategoryTheory.Dial.isoMk e₁ e₂ eq).hom.F = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd e₂.inv
• CategoryTheory.Dial.isoMk_inv_F 📋 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} (e₁ : X.src ≅ Y.src) (e₂ : X.tgt ≅ Y.tgt) (eq : X.rel = (CategoryTheory.Subobject.pullback (CategoryTheory.Limits.prod.map e₁.hom e₂.hom)).obj Y.rel) : (CategoryTheory.Dial.isoMk e₁ e₂ eq).inv.F = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd e₂.hom
• 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.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.map (CategoryTheory.CategoryStruct.id X.src) 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.map f.f (CategoryTheory.CategoryStruct.id Y.src)
• 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.map f.f g.f
• 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.map f.f g.f
• 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.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.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)

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using (by default) Ctrl-K Ctrl-S. 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 88c39f3 serving mathlib revision 9977002