Loogle!

Result

Found 105 declarations mentioning CategoryTheory.Comma.fst.

• CategoryTheory.Comma.fst 📋 Mathlib.CategoryTheory.Comma.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T) (R : CategoryTheory.Functor B T) : CategoryTheory.Functor (CategoryTheory.Comma L R) A
• CategoryTheory.Comma.fst_obj 📋 Mathlib.CategoryTheory.Comma.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T) (R : CategoryTheory.Functor B T) (X : CategoryTheory.Comma L R) : (CategoryTheory.Comma.fst L R).obj X = X.left
• CategoryTheory.Comma.toPUnitIdEquiv_functor_iso 📋 Mathlib.CategoryTheory.Comma.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {L : CategoryTheory.Functor A (CategoryTheory.Discrete PUnit.{u_1 + 1})} {R : CategoryTheory.Functor (CategoryTheory.Discrete PUnit.{u_2 + 1}) (CategoryTheory.Discrete PUnit.{u_1 + 1})} : (CategoryTheory.Comma.toPUnitIdEquiv L R).functor = CategoryTheory.Comma.fst L R
• CategoryTheory.Comma.fst_map 📋 Mathlib.CategoryTheory.Comma.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T) (R : CategoryTheory.Functor B T) {X✝ Y✝ : CategoryTheory.Comma L R} (f : X✝ ⟶ Y✝) : (CategoryTheory.Comma.fst L R).map f = f.left
• CategoryTheory.Comma.natTrans 📋 Mathlib.CategoryTheory.Comma.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T) (R : CategoryTheory.Functor B T) : (CategoryTheory.Comma.fst L R).comp L ⟶ (CategoryTheory.Comma.snd L R).comp R
• CategoryTheory.Comma.natTrans_app 📋 Mathlib.CategoryTheory.Comma.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T) (R : CategoryTheory.Functor B T) (X : CategoryTheory.Comma L R) : (CategoryTheory.Comma.natTrans L R).app X = X.hom
• CategoryTheory.Comma.leftIso_hom 📋 Mathlib.CategoryTheory.Comma.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {L₁ : CategoryTheory.Functor A T} {R₁ : CategoryTheory.Functor B T} {X Y : CategoryTheory.Comma L₁ R₁} (α : X ≅ Y) : (CategoryTheory.Comma.leftIso α).hom = α.hom.left
• CategoryTheory.Comma.leftIso_inv 📋 Mathlib.CategoryTheory.Comma.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {L₁ : CategoryTheory.Functor A T} {R₁ : CategoryTheory.Functor B T} {X Y : CategoryTheory.Comma L₁ R₁} (α : X ≅ Y) : (CategoryTheory.Comma.leftIso α).inv = α.inv.left
• CategoryTheory.Comma.map_fst 📋 Mathlib.CategoryTheory.Comma.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {A' : Type u₄} [CategoryTheory.Category.{v₄, u₄} A'] {B' : Type u₅} [CategoryTheory.Category.{v₅, u₅} B'] {T' : Type u₆} [CategoryTheory.Category.{v₆, u₆} T'] {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} {L' : CategoryTheory.Functor A' T'} {R' : CategoryTheory.Functor B' T'} {F₁ : CategoryTheory.Functor A A'} {F₂ : CategoryTheory.Functor B B'} {F : CategoryTheory.Functor T T'} (α : F₁.comp L' ⟶ L.comp F) (β : R.comp F ⟶ F₂.comp R') : (CategoryTheory.Comma.map α β).comp (CategoryTheory.Comma.fst L' R') = (CategoryTheory.Comma.fst L R).comp F₁
• CategoryTheory.Comma.mapFst 📋 Mathlib.CategoryTheory.Comma.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {A' : Type u₄} [CategoryTheory.Category.{v₄, u₄} A'] {B' : Type u₅} [CategoryTheory.Category.{v₅, u₅} B'] {T' : Type u₆} [CategoryTheory.Category.{v₆, u₆} T'] {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} {L' : CategoryTheory.Functor A' T'} {R' : CategoryTheory.Functor B' T'} {F₁ : CategoryTheory.Functor A A'} {F₂ : CategoryTheory.Functor B B'} {F : CategoryTheory.Functor T T'} (α : F₁.comp L' ⟶ L.comp F) (β : R.comp F ⟶ F₂.comp R') : (CategoryTheory.Comma.map α β).comp (CategoryTheory.Comma.fst L' R') ≅ (CategoryTheory.Comma.fst L R).comp F₁
• CategoryTheory.Comma.unopFunctorCompFst 📋 Mathlib.CategoryTheory.Comma.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T) (R : CategoryTheory.Functor B T) : (CategoryTheory.Comma.unopFunctor L R).comp (CategoryTheory.Comma.fst R L).op ≅ CategoryTheory.Comma.snd L.op R.op
• CategoryTheory.Comma.unopFunctorCompSnd 📋 Mathlib.CategoryTheory.Comma.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T) (R : CategoryTheory.Functor B T) : (CategoryTheory.Comma.unopFunctor L R).comp (CategoryTheory.Comma.snd R L).op ≅ CategoryTheory.Comma.fst L.op R.op
• CategoryTheory.Comma.opFunctorCompFst 📋 Mathlib.CategoryTheory.Comma.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T) (R : CategoryTheory.Functor B T) : (CategoryTheory.Comma.opFunctor L R).leftOp.comp (CategoryTheory.Comma.fst R.op L.op) ≅ (CategoryTheory.Comma.snd L R).op
• CategoryTheory.Comma.opFunctorCompSnd 📋 Mathlib.CategoryTheory.Comma.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T) (R : CategoryTheory.Functor B T) : (CategoryTheory.Comma.opFunctor L R).leftOp.comp (CategoryTheory.Comma.snd R.op L.op) ≅ (CategoryTheory.Comma.fst L R).op
• CategoryTheory.Comma.equivProd_functor_map 📋 Mathlib.CategoryTheory.Comma.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] (L : CategoryTheory.Functor A (CategoryTheory.Discrete PUnit.{u_1 + 1})) (R : CategoryTheory.Functor B (CategoryTheory.Discrete PUnit.{u_1 + 1})) {X✝ Y✝ : CategoryTheory.Comma L R} (f : X✝ ⟶ Y✝) : (CategoryTheory.Comma.equivProd L R).functor.map f = CategoryTheory.Prod.mkHom f.left f.right
• CategoryTheory.Comma.mapFst_hom_app 📋 Mathlib.CategoryTheory.Comma.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {A' : Type u₄} [CategoryTheory.Category.{v₄, u₄} A'] {B' : Type u₅} [CategoryTheory.Category.{v₅, u₅} B'] {T' : Type u₆} [CategoryTheory.Category.{v₆, u₆} T'] {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} {L' : CategoryTheory.Functor A' T'} {R' : CategoryTheory.Functor B' T'} {F₁ : CategoryTheory.Functor A A'} {F₂ : CategoryTheory.Functor B B'} {F : CategoryTheory.Functor T T'} (α : F₁.comp L' ⟶ L.comp F) (β : R.comp F ⟶ F₂.comp R') (X : CategoryTheory.Comma L R) : (CategoryTheory.Comma.mapFst α β).hom.app X = CategoryTheory.CategoryStruct.id (F₁.obj X.left)
• CategoryTheory.Comma.mapFst_inv_app 📋 Mathlib.CategoryTheory.Comma.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {A' : Type u₄} [CategoryTheory.Category.{v₄, u₄} A'] {B' : Type u₅} [CategoryTheory.Category.{v₅, u₅} B'] {T' : Type u₆} [CategoryTheory.Category.{v₆, u₆} T'] {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} {L' : CategoryTheory.Functor A' T'} {R' : CategoryTheory.Functor B' T'} {F₁ : CategoryTheory.Functor A A'} {F₂ : CategoryTheory.Functor B B'} {F : CategoryTheory.Functor T T'} (α : F₁.comp L' ⟶ L.comp F) (β : R.comp F ⟶ F₂.comp R') (X : CategoryTheory.Comma L R) : (CategoryTheory.Comma.mapFst α β).inv.app X = CategoryTheory.CategoryStruct.id (F₁.obj X.left)
• CategoryTheory.Comma.equivProd_counitIso_hom_app 📋 Mathlib.CategoryTheory.Comma.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] (L : CategoryTheory.Functor A (CategoryTheory.Discrete PUnit.{u_1 + 1})) (R : CategoryTheory.Functor B (CategoryTheory.Discrete PUnit.{u_1 + 1})) (X : A × B) : (CategoryTheory.Comma.equivProd L R).counitIso.hom.app X = CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.id X.1) (CategoryTheory.CategoryStruct.id X.2)
• CategoryTheory.Comma.equivProd_counitIso_inv_app 📋 Mathlib.CategoryTheory.Comma.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] (L : CategoryTheory.Functor A (CategoryTheory.Discrete PUnit.{u_1 + 1})) (R : CategoryTheory.Functor B (CategoryTheory.Discrete PUnit.{u_1 + 1})) (X : A × B) : (CategoryTheory.Comma.equivProd L R).counitIso.inv.app X = CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.id X.1) (CategoryTheory.CategoryStruct.id X.2)
• CategoryTheory.Comma.unopFunctorCompFst_hom_app 📋 Mathlib.CategoryTheory.Comma.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T) (R : CategoryTheory.Functor B T) (X : CategoryTheory.Comma L.op R.op) : (CategoryTheory.Comma.unopFunctorCompFst L R).hom.app X = CategoryTheory.CategoryStruct.id X.right
• CategoryTheory.Comma.unopFunctorCompFst_inv_app 📋 Mathlib.CategoryTheory.Comma.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T) (R : CategoryTheory.Functor B T) (X : CategoryTheory.Comma L.op R.op) : (CategoryTheory.Comma.unopFunctorCompFst L R).inv.app X = CategoryTheory.CategoryStruct.id X.right
• CategoryTheory.Comma.unopFunctorCompSnd_hom_app 📋 Mathlib.CategoryTheory.Comma.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T) (R : CategoryTheory.Functor B T) (X : CategoryTheory.Comma L.op R.op) : (CategoryTheory.Comma.unopFunctorCompSnd L R).hom.app X = CategoryTheory.CategoryStruct.id X.left
• CategoryTheory.Comma.unopFunctorCompSnd_inv_app 📋 Mathlib.CategoryTheory.Comma.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T) (R : CategoryTheory.Functor B T) (X : CategoryTheory.Comma L.op R.op) : (CategoryTheory.Comma.unopFunctorCompSnd L R).inv.app X = CategoryTheory.CategoryStruct.id X.left
• CategoryTheory.Comma.opFunctorCompFst_hom_app 📋 Mathlib.CategoryTheory.Comma.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T) (R : CategoryTheory.Functor B T) (X : (CategoryTheory.Comma L R)ᵒᵖ) : (CategoryTheory.Comma.opFunctorCompFst L R).hom.app X = CategoryTheory.CategoryStruct.id (Opposite.op (Opposite.unop X).right)
• CategoryTheory.Comma.opFunctorCompFst_inv_app 📋 Mathlib.CategoryTheory.Comma.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T) (R : CategoryTheory.Functor B T) (X : (CategoryTheory.Comma L R)ᵒᵖ) : (CategoryTheory.Comma.opFunctorCompFst L R).inv.app X = CategoryTheory.CategoryStruct.id (Opposite.op (Opposite.unop X).right)
• CategoryTheory.Comma.opFunctorCompSnd_hom_app 📋 Mathlib.CategoryTheory.Comma.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T) (R : CategoryTheory.Functor B T) (X : (CategoryTheory.Comma L R)ᵒᵖ) : (CategoryTheory.Comma.opFunctorCompSnd L R).hom.app X = CategoryTheory.CategoryStruct.id (Opposite.op (Opposite.unop X).left)
• CategoryTheory.Comma.opFunctorCompSnd_inv_app 📋 Mathlib.CategoryTheory.Comma.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T) (R : CategoryTheory.Functor B T) (X : (CategoryTheory.Comma L R)ᵒᵖ) : (CategoryTheory.Comma.opFunctorCompSnd L R).inv.app X = CategoryTheory.CategoryStruct.id (Opposite.op (Opposite.unop X).left)
• CategoryTheory.CostructuredArrow.ofCommaFstEquivalence 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor C T) (G : CategoryTheory.Functor D T) (c : C) : CategoryTheory.CostructuredArrow (CategoryTheory.Comma.fst F G) c ≌ CategoryTheory.Comma ((CategoryTheory.Over.forget c).comp F) G
• CategoryTheory.CostructuredArrow.ofCommaFstEquivalenceFunctor 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor C T) (G : CategoryTheory.Functor D T) (c : C) : CategoryTheory.Functor (CategoryTheory.CostructuredArrow (CategoryTheory.Comma.fst F G) c) (CategoryTheory.Comma ((CategoryTheory.Over.forget c).comp F) G)
• CategoryTheory.CostructuredArrow.ofCommaFstEquivalenceInverse 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor C T) (G : CategoryTheory.Functor D T) (c : C) : CategoryTheory.Functor (CategoryTheory.Comma ((CategoryTheory.Over.forget c).comp F) G) (CategoryTheory.CostructuredArrow (CategoryTheory.Comma.fst F G) c)
• CategoryTheory.StructuredArrow.ofCommaSndEquivalence 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor C T) (G : CategoryTheory.Functor D T) (c : C) : CategoryTheory.StructuredArrow c (CategoryTheory.Comma.fst F G) ≌ CategoryTheory.Comma ((CategoryTheory.Under.forget c).comp F) G
• CategoryTheory.StructuredArrow.ofCommaSndEquivalenceFunctor 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor C T) (G : CategoryTheory.Functor D T) (c : C) : CategoryTheory.Functor (CategoryTheory.StructuredArrow c (CategoryTheory.Comma.fst F G)) (CategoryTheory.Comma ((CategoryTheory.Under.forget c).comp F) G)
• CategoryTheory.StructuredArrow.ofCommaSndEquivalenceInverse 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor C T) (G : CategoryTheory.Functor D T) (c : C) : CategoryTheory.Functor (CategoryTheory.Comma ((CategoryTheory.Under.forget c).comp F) G) (CategoryTheory.StructuredArrow c (CategoryTheory.Comma.fst F G))
• CategoryTheory.CostructuredArrow.ofCommaFstEquivalenceInverse_obj_right_as 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor C T) (G : CategoryTheory.Functor D T) (c : C) (Y : CategoryTheory.Comma ((CategoryTheory.Over.forget c).comp F) G) : ((CategoryTheory.CostructuredArrow.ofCommaFstEquivalenceInverse F G c).obj Y).right.as = PUnit.unit
• CategoryTheory.StructuredArrow.ofCommaSndEquivalenceInverse_obj_left_as 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor C T) (G : CategoryTheory.Functor D T) (c : C) (Y : CategoryTheory.Comma ((CategoryTheory.Under.forget c).comp F) G) : ((CategoryTheory.StructuredArrow.ofCommaSndEquivalenceInverse F G c).obj Y).left.as = PUnit.unit
• CategoryTheory.CostructuredArrow.ofCommaFstEquivalenceFunctor_obj_right 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor C T) (G : CategoryTheory.Functor D T) (c : C) (X : CategoryTheory.CostructuredArrow (CategoryTheory.Comma.fst F G) c) : ((CategoryTheory.CostructuredArrow.ofCommaFstEquivalenceFunctor F G c).obj X).right = X.left.right
• CategoryTheory.StructuredArrow.ofCommaSndEquivalenceFunctor_obj_right 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor C T) (G : CategoryTheory.Functor D T) (c : C) (X : CategoryTheory.StructuredArrow c (CategoryTheory.Comma.fst F G)) : ((CategoryTheory.StructuredArrow.ofCommaSndEquivalenceFunctor F G c).obj X).right = X.right.right
• CategoryTheory.CostructuredArrow.ofCommaFstEquivalenceInverse_obj_left_right 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor C T) (G : CategoryTheory.Functor D T) (c : C) (Y : CategoryTheory.Comma ((CategoryTheory.Over.forget c).comp F) G) : ((CategoryTheory.CostructuredArrow.ofCommaFstEquivalenceInverse F G c).obj Y).left.right = Y.right
• CategoryTheory.StructuredArrow.ofCommaSndEquivalenceInverse_obj_right_right 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor C T) (G : CategoryTheory.Functor D T) (c : C) (Y : CategoryTheory.Comma ((CategoryTheory.Under.forget c).comp F) G) : ((CategoryTheory.StructuredArrow.ofCommaSndEquivalenceInverse F G c).obj Y).right.right = Y.right
• CategoryTheory.CostructuredArrow.ofCommaFstEquivalenceInverse_obj_left_left 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor C T) (G : CategoryTheory.Functor D T) (c : C) (Y : CategoryTheory.Comma ((CategoryTheory.Over.forget c).comp F) G) : ((CategoryTheory.CostructuredArrow.ofCommaFstEquivalenceInverse F G c).obj Y).left.left = Y.left.left
• CategoryTheory.StructuredArrow.ofCommaSndEquivalenceInverse_obj_right_left 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor C T) (G : CategoryTheory.Functor D T) (c : C) (Y : CategoryTheory.Comma ((CategoryTheory.Under.forget c).comp F) G) : ((CategoryTheory.StructuredArrow.ofCommaSndEquivalenceInverse F G c).obj Y).right.left = Y.left.right
• CategoryTheory.CostructuredArrow.ofCommaFstEquivalence_functor 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor C T) (G : CategoryTheory.Functor D T) (c : C) : (CategoryTheory.CostructuredArrow.ofCommaFstEquivalence F G c).functor = CategoryTheory.CostructuredArrow.ofCommaFstEquivalenceFunctor F G c
• CategoryTheory.CostructuredArrow.ofCommaFstEquivalence_inverse 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor C T) (G : CategoryTheory.Functor D T) (c : C) : (CategoryTheory.CostructuredArrow.ofCommaFstEquivalence F G c).inverse = CategoryTheory.CostructuredArrow.ofCommaFstEquivalenceInverse F G c
• CategoryTheory.StructuredArrow.ofCommaSndEquivalence_functor 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor C T) (G : CategoryTheory.Functor D T) (c : C) : (CategoryTheory.StructuredArrow.ofCommaSndEquivalence F G c).functor = CategoryTheory.StructuredArrow.ofCommaSndEquivalenceFunctor F G c
• CategoryTheory.StructuredArrow.ofCommaSndEquivalence_inverse 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor C T) (G : CategoryTheory.Functor D T) (c : C) : (CategoryTheory.StructuredArrow.ofCommaSndEquivalence F G c).inverse = CategoryTheory.StructuredArrow.ofCommaSndEquivalenceInverse F G c
• CategoryTheory.CostructuredArrow.ofCommaFstEquivalenceInverse_obj_hom 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor C T) (G : CategoryTheory.Functor D T) (c : C) (Y : CategoryTheory.Comma ((CategoryTheory.Over.forget c).comp F) G) : ((CategoryTheory.CostructuredArrow.ofCommaFstEquivalenceInverse F G c).obj Y).hom = Y.left.hom
• CategoryTheory.StructuredArrow.ofCommaSndEquivalenceInverse_obj_hom 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor C T) (G : CategoryTheory.Functor D T) (c : C) (Y : CategoryTheory.Comma ((CategoryTheory.Under.forget c).comp F) G) : ((CategoryTheory.StructuredArrow.ofCommaSndEquivalenceInverse F G c).obj Y).hom = Y.left.hom
• CategoryTheory.CostructuredArrow.ofCommaFstEquivalenceFunctor_obj_left 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor C T) (G : CategoryTheory.Functor D T) (c : C) (X : CategoryTheory.CostructuredArrow (CategoryTheory.Comma.fst F G) c) : ((CategoryTheory.CostructuredArrow.ofCommaFstEquivalenceFunctor F G c).obj X).left = CategoryTheory.Over.mk X.hom
• CategoryTheory.StructuredArrow.ofCommaSndEquivalenceFunctor_obj_left 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor C T) (G : CategoryTheory.Functor D T) (c : C) (X : CategoryTheory.StructuredArrow c (CategoryTheory.Comma.fst F G)) : ((CategoryTheory.StructuredArrow.ofCommaSndEquivalenceFunctor F G c).obj X).left = CategoryTheory.Under.mk X.hom
• CategoryTheory.CostructuredArrow.ofCommaFstEquivalenceFunctor_obj_hom 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor C T) (G : CategoryTheory.Functor D T) (c : C) (X : CategoryTheory.CostructuredArrow (CategoryTheory.Comma.fst F G) c) : ((CategoryTheory.CostructuredArrow.ofCommaFstEquivalenceFunctor F G c).obj X).hom = X.left.hom
• CategoryTheory.StructuredArrow.ofCommaSndEquivalenceFunctor_obj_hom 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor C T) (G : CategoryTheory.Functor D T) (c : C) (X : CategoryTheory.StructuredArrow c (CategoryTheory.Comma.fst F G)) : ((CategoryTheory.StructuredArrow.ofCommaSndEquivalenceFunctor F G c).obj X).hom = X.right.hom
• CategoryTheory.CostructuredArrow.ofCommaFstEquivalenceInverse_obj_left_hom 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor C T) (G : CategoryTheory.Functor D T) (c : C) (Y : CategoryTheory.Comma ((CategoryTheory.Over.forget c).comp F) G) : ((CategoryTheory.CostructuredArrow.ofCommaFstEquivalenceInverse F G c).obj Y).left.hom = Y.hom
• CategoryTheory.StructuredArrow.ofCommaSndEquivalenceInverse_obj_right_hom 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor C T) (G : CategoryTheory.Functor D T) (c : C) (Y : CategoryTheory.Comma ((CategoryTheory.Under.forget c).comp F) G) : ((CategoryTheory.StructuredArrow.ofCommaSndEquivalenceInverse F G c).obj Y).right.hom = Y.hom
• CategoryTheory.StructuredArrow.ofCommaSndEquivalenceFunctor_map_right 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor C T) (G : CategoryTheory.Functor D T) (c : C) {X✝ Y✝ : CategoryTheory.StructuredArrow c (CategoryTheory.Comma.fst F G)} (f : X✝ ⟶ Y✝) : ((CategoryTheory.StructuredArrow.ofCommaSndEquivalenceFunctor F G c).map f).right = (CategoryTheory.StructuredArrow.Hom.right f).right
• CategoryTheory.CostructuredArrow.ofCommaFstEquivalenceFunctor_map_right 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor C T) (G : CategoryTheory.Functor D T) (c : C) {X✝ Y✝ : CategoryTheory.CostructuredArrow (CategoryTheory.Comma.fst F G) c} (f : X✝ ⟶ Y✝) : ((CategoryTheory.CostructuredArrow.ofCommaFstEquivalenceFunctor F G c).map f).right = f.left.right
• CategoryTheory.CostructuredArrow.ofCommaFstEquivalenceInverse_map_left_right 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor C T) (G : CategoryTheory.Functor D T) (c : C) {X✝ Y✝ : CategoryTheory.Comma ((CategoryTheory.Over.forget c).comp F) G} (g : X✝ ⟶ Y✝) : ((CategoryTheory.CostructuredArrow.ofCommaFstEquivalenceInverse F G c).map g).left.right = g.right
• CategoryTheory.StructuredArrow.ofCommaSndEquivalenceInverse_map_right_right 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor C T) (G : CategoryTheory.Functor D T) (c : C) {X✝ Y✝ : CategoryTheory.Comma ((CategoryTheory.Under.forget c).comp F) G} (g : X✝ ⟶ Y✝) : ((CategoryTheory.StructuredArrow.ofCommaSndEquivalenceInverse F G c).map g).right.right = g.right
• CategoryTheory.CostructuredArrow.ofCommaFstEquivalenceInverse_map_left_left 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor C T) (G : CategoryTheory.Functor D T) (c : C) {X✝ Y✝ : CategoryTheory.Comma ((CategoryTheory.Over.forget c).comp F) G} (g : X✝ ⟶ Y✝) : ((CategoryTheory.CostructuredArrow.ofCommaFstEquivalenceInverse F G c).map g).left.left = CategoryTheory.Over.Hom.left g.left
• CategoryTheory.StructuredArrow.ofCommaSndEquivalenceInverse_map_right_left 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor C T) (G : CategoryTheory.Functor D T) (c : C) {X✝ Y✝ : CategoryTheory.Comma ((CategoryTheory.Under.forget c).comp F) G} (g : X✝ ⟶ Y✝) : ((CategoryTheory.StructuredArrow.ofCommaSndEquivalenceInverse F G c).map g).right.left = CategoryTheory.Under.Hom.right g.left
• CategoryTheory.CostructuredArrow.ofCommaFstEquivalence_unitIso 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor C T) (G : CategoryTheory.Functor D T) (c : C) : (CategoryTheory.CostructuredArrow.ofCommaFstEquivalence F G c).unitIso = CategoryTheory.NatIso.ofComponents (fun x => CategoryTheory.Iso.refl ((CategoryTheory.Functor.id (CategoryTheory.CostructuredArrow (CategoryTheory.Comma.fst F G) c)).obj x)) ⋯
• CategoryTheory.StructuredArrow.ofCommaSndEquivalence_unitIso 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor C T) (G : CategoryTheory.Functor D T) (c : C) : (CategoryTheory.StructuredArrow.ofCommaSndEquivalence F G c).unitIso = CategoryTheory.NatIso.ofComponents (fun x => CategoryTheory.Iso.refl ((CategoryTheory.Functor.id (CategoryTheory.StructuredArrow c (CategoryTheory.Comma.fst F G))).obj x)) ⋯
• CategoryTheory.CostructuredArrow.ofCommaFstEquivalence_counitIso 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor C T) (G : CategoryTheory.Functor D T) (c : C) : (CategoryTheory.CostructuredArrow.ofCommaFstEquivalence F G c).counitIso = CategoryTheory.NatIso.ofComponents (fun x => CategoryTheory.Iso.refl (((CategoryTheory.CostructuredArrow.ofCommaFstEquivalenceInverse F G c).comp (CategoryTheory.CostructuredArrow.ofCommaFstEquivalenceFunctor F G c)).obj x)) ⋯
• CategoryTheory.StructuredArrow.ofCommaSndEquivalence_counitIso 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor C T) (G : CategoryTheory.Functor D T) (c : C) : (CategoryTheory.StructuredArrow.ofCommaSndEquivalence F G c).counitIso = CategoryTheory.NatIso.ofComponents (fun x => CategoryTheory.Iso.refl (((CategoryTheory.StructuredArrow.ofCommaSndEquivalenceInverse F G c).comp (CategoryTheory.StructuredArrow.ofCommaSndEquivalenceFunctor F G c)).obj x)) ⋯
• CategoryTheory.StructuredArrow.ofCommaSndEquivalenceFunctor_map_left 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor C T) (G : CategoryTheory.Functor D T) (c : C) {X✝ Y✝ : CategoryTheory.StructuredArrow c (CategoryTheory.Comma.fst F G)} (f : X✝ ⟶ Y✝) : ((CategoryTheory.StructuredArrow.ofCommaSndEquivalenceFunctor F G c).map f).left = CategoryTheory.Under.homMk (CategoryTheory.StructuredArrow.Hom.right f).left ⋯
• CategoryTheory.CostructuredArrow.ofCommaFstEquivalenceFunctor_map_left 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor C T) (G : CategoryTheory.Functor D T) (c : C) {X✝ Y✝ : CategoryTheory.CostructuredArrow (CategoryTheory.Comma.fst F G) c} (f : X✝ ⟶ Y✝) : ((CategoryTheory.CostructuredArrow.ofCommaFstEquivalenceFunctor F G c).map f).left = CategoryTheory.Over.homMk f.left.left ⋯
• CategoryTheory.Comma.preservesColimitsOfShape_fst 📋 Mathlib.CategoryTheory.Limits.Comma
  {J : Type w} [CategoryTheory.Category.{w', w} J] {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} [CategoryTheory.Limits.HasColimitsOfShape J A] [CategoryTheory.Limits.HasColimitsOfShape J B] [CategoryTheory.Limits.PreservesColimitsOfShape J L] : CategoryTheory.Limits.PreservesColimitsOfShape J (CategoryTheory.Comma.fst L R)
• CategoryTheory.Comma.colimitAuxiliaryCocone 📋 Mathlib.CategoryTheory.Limits.Comma
  {J : Type w} [CategoryTheory.Category.{w', w} J] {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} (F : CategoryTheory.Functor J (CategoryTheory.Comma L R)) (c₂ : CategoryTheory.Limits.Cocone (F.comp (CategoryTheory.Comma.snd L R))) : CategoryTheory.Limits.Cocone ((F.comp (CategoryTheory.Comma.fst L R)).comp L)
• CategoryTheory.Comma.limitAuxiliaryCone 📋 Mathlib.CategoryTheory.Limits.Comma
  {J : Type w} [CategoryTheory.Category.{w', w} J] {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} (F : CategoryTheory.Functor J (CategoryTheory.Comma L R)) (c₁ : CategoryTheory.Limits.Cone (F.comp (CategoryTheory.Comma.fst L R))) : CategoryTheory.Limits.Cone ((F.comp (CategoryTheory.Comma.snd L R)).comp R)
• CategoryTheory.Comma.hasColimit 📋 Mathlib.CategoryTheory.Limits.Comma
  {J : Type w} [CategoryTheory.Category.{w', w} J] {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} (F : CategoryTheory.Functor J (CategoryTheory.Comma L R)) [CategoryTheory.Limits.HasColimit (F.comp (CategoryTheory.Comma.fst L R))] [CategoryTheory.Limits.HasColimit (F.comp (CategoryTheory.Comma.snd L R))] [CategoryTheory.Limits.PreservesColimit (F.comp (CategoryTheory.Comma.fst L R)) L] : CategoryTheory.Limits.HasColimit F
• CategoryTheory.Comma.hasLimit 📋 Mathlib.CategoryTheory.Limits.Comma
  {J : Type w} [CategoryTheory.Category.{w', w} J] {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} (F : CategoryTheory.Functor J (CategoryTheory.Comma L R)) [CategoryTheory.Limits.HasLimit (F.comp (CategoryTheory.Comma.fst L R))] [CategoryTheory.Limits.HasLimit (F.comp (CategoryTheory.Comma.snd L R))] [CategoryTheory.Limits.PreservesLimit (F.comp (CategoryTheory.Comma.snd L R)) R] : CategoryTheory.Limits.HasLimit F
• CategoryTheory.Comma.colimitAuxiliaryCocone_pt 📋 Mathlib.CategoryTheory.Limits.Comma
  {J : Type w} [CategoryTheory.Category.{w', w} J] {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} (F : CategoryTheory.Functor J (CategoryTheory.Comma L R)) (c₂ : CategoryTheory.Limits.Cocone (F.comp (CategoryTheory.Comma.snd L R))) : (CategoryTheory.Comma.colimitAuxiliaryCocone F c₂).pt = R.obj c₂.pt
• CategoryTheory.Comma.limitAuxiliaryCone_pt 📋 Mathlib.CategoryTheory.Limits.Comma
  {J : Type w} [CategoryTheory.Category.{w', w} J] {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} (F : CategoryTheory.Functor J (CategoryTheory.Comma L R)) (c₁ : CategoryTheory.Limits.Cone (F.comp (CategoryTheory.Comma.fst L R))) : (CategoryTheory.Comma.limitAuxiliaryCone F c₁).pt = L.obj c₁.pt
• CategoryTheory.Comma.coconeOfPreserves 📋 Mathlib.CategoryTheory.Limits.Comma
  {J : Type w} [CategoryTheory.Category.{w', w} J] {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} (F : CategoryTheory.Functor J (CategoryTheory.Comma L R)) [CategoryTheory.Limits.PreservesColimit (F.comp (CategoryTheory.Comma.fst L R)) L] {c₁ : CategoryTheory.Limits.Cocone (F.comp (CategoryTheory.Comma.fst L R))} (t₁ : CategoryTheory.Limits.IsColimit c₁) (c₂ : CategoryTheory.Limits.Cocone (F.comp (CategoryTheory.Comma.snd L R))) : CategoryTheory.Limits.Cocone F
• CategoryTheory.Comma.coneOfPreserves 📋 Mathlib.CategoryTheory.Limits.Comma
  {J : Type w} [CategoryTheory.Category.{w', w} J] {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} (F : CategoryTheory.Functor J (CategoryTheory.Comma L R)) [CategoryTheory.Limits.PreservesLimit (F.comp (CategoryTheory.Comma.snd L R)) R] (c₁ : CategoryTheory.Limits.Cone (F.comp (CategoryTheory.Comma.fst L R))) {c₂ : CategoryTheory.Limits.Cone (F.comp (CategoryTheory.Comma.snd L R))} (t₂ : CategoryTheory.Limits.IsLimit c₂) : CategoryTheory.Limits.Cone F
• CategoryTheory.Comma.fstSndJointlyReflectColimit 📋 Mathlib.CategoryTheory.Limits.Comma
  {J : Type w} [CategoryTheory.Category.{w', w} J] {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} {F : CategoryTheory.Functor J (CategoryTheory.Comma L R)} {c : CategoryTheory.Limits.Cocone F} [CategoryTheory.Limits.PreservesColimit (F.comp (CategoryTheory.Comma.fst L R)) L] (h₁ : CategoryTheory.Limits.IsColimit ((CategoryTheory.Comma.fst L R).mapCocone c)) (h₂ : CategoryTheory.Limits.IsColimit ((CategoryTheory.Comma.snd L R).mapCocone c)) : CategoryTheory.Limits.IsColimit c
• CategoryTheory.Comma.fstSndJointlyReflectLimit 📋 Mathlib.CategoryTheory.Limits.Comma
  {J : Type w} [CategoryTheory.Category.{w', w} J] {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} {F : CategoryTheory.Functor J (CategoryTheory.Comma L R)} {c : CategoryTheory.Limits.Cone F} [CategoryTheory.Limits.PreservesLimit (F.comp (CategoryTheory.Comma.snd L R)) R] (h₁ : CategoryTheory.Limits.IsLimit ((CategoryTheory.Comma.fst L R).mapCone c)) (h₂ : CategoryTheory.Limits.IsLimit ((CategoryTheory.Comma.snd L R).mapCone c)) : CategoryTheory.Limits.IsLimit c
• CategoryTheory.Comma.coconeOfPreservesIsColimit 📋 Mathlib.CategoryTheory.Limits.Comma
  {J : Type w} [CategoryTheory.Category.{w', w} J] {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} (F : CategoryTheory.Functor J (CategoryTheory.Comma L R)) [CategoryTheory.Limits.PreservesColimit (F.comp (CategoryTheory.Comma.fst L R)) L] {c₁ : CategoryTheory.Limits.Cocone (F.comp (CategoryTheory.Comma.fst L R))} (t₁ : CategoryTheory.Limits.IsColimit c₁) {c₂ : CategoryTheory.Limits.Cocone (F.comp (CategoryTheory.Comma.snd L R))} (t₂ : CategoryTheory.Limits.IsColimit c₂) : CategoryTheory.Limits.IsColimit (CategoryTheory.Comma.coconeOfPreserves F t₁ c₂)
• CategoryTheory.Comma.coneOfPreservesIsLimit 📋 Mathlib.CategoryTheory.Limits.Comma
  {J : Type w} [CategoryTheory.Category.{w', w} J] {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} (F : CategoryTheory.Functor J (CategoryTheory.Comma L R)) [CategoryTheory.Limits.PreservesLimit (F.comp (CategoryTheory.Comma.snd L R)) R] {c₁ : CategoryTheory.Limits.Cone (F.comp (CategoryTheory.Comma.fst L R))} (t₁ : CategoryTheory.Limits.IsLimit c₁) {c₂ : CategoryTheory.Limits.Cone (F.comp (CategoryTheory.Comma.snd L R))} (t₂ : CategoryTheory.Limits.IsLimit c₂) : CategoryTheory.Limits.IsLimit (CategoryTheory.Comma.coneOfPreserves F c₁ t₂)
• CategoryTheory.Comma.coconeOfPreserves_pt_left 📋 Mathlib.CategoryTheory.Limits.Comma
  {J : Type w} [CategoryTheory.Category.{w', w} J] {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} (F : CategoryTheory.Functor J (CategoryTheory.Comma L R)) [CategoryTheory.Limits.PreservesColimit (F.comp (CategoryTheory.Comma.fst L R)) L] {c₁ : CategoryTheory.Limits.Cocone (F.comp (CategoryTheory.Comma.fst L R))} (t₁ : CategoryTheory.Limits.IsColimit c₁) (c₂ : CategoryTheory.Limits.Cocone (F.comp (CategoryTheory.Comma.snd L R))) : (CategoryTheory.Comma.coconeOfPreserves F t₁ c₂).pt.left = c₁.pt
• CategoryTheory.Comma.coconeOfPreserves_pt_right 📋 Mathlib.CategoryTheory.Limits.Comma
  {J : Type w} [CategoryTheory.Category.{w', w} J] {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} (F : CategoryTheory.Functor J (CategoryTheory.Comma L R)) [CategoryTheory.Limits.PreservesColimit (F.comp (CategoryTheory.Comma.fst L R)) L] {c₁ : CategoryTheory.Limits.Cocone (F.comp (CategoryTheory.Comma.fst L R))} (t₁ : CategoryTheory.Limits.IsColimit c₁) (c₂ : CategoryTheory.Limits.Cocone (F.comp (CategoryTheory.Comma.snd L R))) : (CategoryTheory.Comma.coconeOfPreserves F t₁ c₂).pt.right = c₂.pt
• CategoryTheory.Comma.coneOfPreserves_pt_left 📋 Mathlib.CategoryTheory.Limits.Comma
  {J : Type w} [CategoryTheory.Category.{w', w} J] {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} (F : CategoryTheory.Functor J (CategoryTheory.Comma L R)) [CategoryTheory.Limits.PreservesLimit (F.comp (CategoryTheory.Comma.snd L R)) R] (c₁ : CategoryTheory.Limits.Cone (F.comp (CategoryTheory.Comma.fst L R))) {c₂ : CategoryTheory.Limits.Cone (F.comp (CategoryTheory.Comma.snd L R))} (t₂ : CategoryTheory.Limits.IsLimit c₂) : (CategoryTheory.Comma.coneOfPreserves F c₁ t₂).pt.left = c₁.pt
• CategoryTheory.Comma.coneOfPreserves_pt_right 📋 Mathlib.CategoryTheory.Limits.Comma
  {J : Type w} [CategoryTheory.Category.{w', w} J] {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} (F : CategoryTheory.Functor J (CategoryTheory.Comma L R)) [CategoryTheory.Limits.PreservesLimit (F.comp (CategoryTheory.Comma.snd L R)) R] (c₁ : CategoryTheory.Limits.Cone (F.comp (CategoryTheory.Comma.fst L R))) {c₂ : CategoryTheory.Limits.Cone (F.comp (CategoryTheory.Comma.snd L R))} (t₂ : CategoryTheory.Limits.IsLimit c₂) : (CategoryTheory.Comma.coneOfPreserves F c₁ t₂).pt.right = c₂.pt
• CategoryTheory.Comma.coconeOfPreserves_pt_hom 📋 Mathlib.CategoryTheory.Limits.Comma
  {J : Type w} [CategoryTheory.Category.{w', w} J] {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} (F : CategoryTheory.Functor J (CategoryTheory.Comma L R)) [CategoryTheory.Limits.PreservesColimit (F.comp (CategoryTheory.Comma.fst L R)) L] {c₁ : CategoryTheory.Limits.Cocone (F.comp (CategoryTheory.Comma.fst L R))} (t₁ : CategoryTheory.Limits.IsColimit c₁) (c₂ : CategoryTheory.Limits.Cocone (F.comp (CategoryTheory.Comma.snd L R))) : (CategoryTheory.Comma.coconeOfPreserves F t₁ c₂).pt.hom = (CategoryTheory.Limits.isColimitOfPreserves L t₁).desc (CategoryTheory.Comma.colimitAuxiliaryCocone F c₂)
• CategoryTheory.Comma.coneOfPreserves_pt_hom 📋 Mathlib.CategoryTheory.Limits.Comma
  {J : Type w} [CategoryTheory.Category.{w', w} J] {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} (F : CategoryTheory.Functor J (CategoryTheory.Comma L R)) [CategoryTheory.Limits.PreservesLimit (F.comp (CategoryTheory.Comma.snd L R)) R] (c₁ : CategoryTheory.Limits.Cone (F.comp (CategoryTheory.Comma.fst L R))) {c₂ : CategoryTheory.Limits.Cone (F.comp (CategoryTheory.Comma.snd L R))} (t₂ : CategoryTheory.Limits.IsLimit c₂) : (CategoryTheory.Comma.coneOfPreserves F c₁ t₂).pt.hom = (CategoryTheory.Limits.isLimitOfPreserves R t₂).lift (CategoryTheory.Comma.limitAuxiliaryCone F c₁)
• CategoryTheory.Comma.colimitAuxiliaryCocone_ι_app 📋 Mathlib.CategoryTheory.Limits.Comma
  {J : Type w} [CategoryTheory.Category.{w', w} J] {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} (F : CategoryTheory.Functor J (CategoryTheory.Comma L R)) (c₂ : CategoryTheory.Limits.Cocone (F.comp (CategoryTheory.Comma.snd L R))) (X : J) : (CategoryTheory.Comma.colimitAuxiliaryCocone F c₂).ι.app X = CategoryTheory.CategoryStruct.comp (F.obj X).hom (R.map (c₂.ι.app X))
• CategoryTheory.Comma.limitAuxiliaryCone_π_app 📋 Mathlib.CategoryTheory.Limits.Comma
  {J : Type w} [CategoryTheory.Category.{w', w} J] {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} (F : CategoryTheory.Functor J (CategoryTheory.Comma L R)) (c₁ : CategoryTheory.Limits.Cone (F.comp (CategoryTheory.Comma.fst L R))) (X : J) : (CategoryTheory.Comma.limitAuxiliaryCone F c₁).π.app X = CategoryTheory.CategoryStruct.comp (L.map (c₁.π.app X)) (F.obj X).hom
• CategoryTheory.Comma.coconeOfPreserves_ι_app_left 📋 Mathlib.CategoryTheory.Limits.Comma
  {J : Type w} [CategoryTheory.Category.{w', w} J] {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} (F : CategoryTheory.Functor J (CategoryTheory.Comma L R)) [CategoryTheory.Limits.PreservesColimit (F.comp (CategoryTheory.Comma.fst L R)) L] {c₁ : CategoryTheory.Limits.Cocone (F.comp (CategoryTheory.Comma.fst L R))} (t₁ : CategoryTheory.Limits.IsColimit c₁) (c₂ : CategoryTheory.Limits.Cocone (F.comp (CategoryTheory.Comma.snd L R))) (j : J) : ((CategoryTheory.Comma.coconeOfPreserves F t₁ c₂).ι.app j).left = c₁.ι.app j
• CategoryTheory.Comma.coconeOfPreserves_ι_app_right 📋 Mathlib.CategoryTheory.Limits.Comma
  {J : Type w} [CategoryTheory.Category.{w', w} J] {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} (F : CategoryTheory.Functor J (CategoryTheory.Comma L R)) [CategoryTheory.Limits.PreservesColimit (F.comp (CategoryTheory.Comma.fst L R)) L] {c₁ : CategoryTheory.Limits.Cocone (F.comp (CategoryTheory.Comma.fst L R))} (t₁ : CategoryTheory.Limits.IsColimit c₁) (c₂ : CategoryTheory.Limits.Cocone (F.comp (CategoryTheory.Comma.snd L R))) (j : J) : ((CategoryTheory.Comma.coconeOfPreserves F t₁ c₂).ι.app j).right = c₂.ι.app j
• CategoryTheory.Comma.coneOfPreserves_π_app_left 📋 Mathlib.CategoryTheory.Limits.Comma
  {J : Type w} [CategoryTheory.Category.{w', w} J] {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} (F : CategoryTheory.Functor J (CategoryTheory.Comma L R)) [CategoryTheory.Limits.PreservesLimit (F.comp (CategoryTheory.Comma.snd L R)) R] (c₁ : CategoryTheory.Limits.Cone (F.comp (CategoryTheory.Comma.fst L R))) {c₂ : CategoryTheory.Limits.Cone (F.comp (CategoryTheory.Comma.snd L R))} (t₂ : CategoryTheory.Limits.IsLimit c₂) (j : J) : ((CategoryTheory.Comma.coneOfPreserves F c₁ t₂).π.app j).left = c₁.π.app j
• CategoryTheory.Comma.coneOfPreserves_π_app_right 📋 Mathlib.CategoryTheory.Limits.Comma
  {J : Type w} [CategoryTheory.Category.{w', w} J] {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} (F : CategoryTheory.Functor J (CategoryTheory.Comma L R)) [CategoryTheory.Limits.PreservesLimit (F.comp (CategoryTheory.Comma.snd L R)) R] (c₁ : CategoryTheory.Limits.Cone (F.comp (CategoryTheory.Comma.fst L R))) {c₂ : CategoryTheory.Limits.Cone (F.comp (CategoryTheory.Comma.snd L R))} (t₂ : CategoryTheory.Limits.IsLimit c₂) (j : J) : ((CategoryTheory.Comma.coneOfPreserves F c₁ t₂).π.app j).right = c₂.π.app j
• CategoryTheory.CostructuredArrow.ιCompGrothendieckPrecompFunctorToCommaCompFst 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.Functor
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (L : CategoryTheory.Functor C D) (R : CategoryTheory.Functor E D) (X : E) : (CategoryTheory.Grothendieck.ι (R.comp (CategoryTheory.CostructuredArrow.functor L)) X).comp ((CategoryTheory.CostructuredArrow.grothendieckPrecompFunctorToComma L R).comp (CategoryTheory.Comma.fst L R)) ≅ CategoryTheory.CostructuredArrow.proj L (R.obj X)
• CategoryTheory.CostructuredArrow.grothendieckProj_map 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.Functor
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (L : CategoryTheory.Functor C D) {X✝ Y✝ : CategoryTheory.Grothendieck (CategoryTheory.CostructuredArrow.functor L)} (f : X✝ ⟶ Y✝) : (CategoryTheory.CostructuredArrow.grothendieckProj L).map f = f.fiber.left
• CategoryTheory.CostructuredArrow.ιCompGrothendieckProj_hom_app 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.Functor
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (L : CategoryTheory.Functor C D) (X : D) (X✝ : ↑(((CategoryTheory.Functor.id D).comp (CategoryTheory.CostructuredArrow.functor L)).obj X)) : (CategoryTheory.CostructuredArrow.ιCompGrothendieckProj L X).hom.app X✝ = CategoryTheory.CategoryStruct.id (CategoryTheory.CostructuredArrow.left X✝)
• CategoryTheory.CostructuredArrow.ιCompGrothendieckProj_inv_app 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.Functor
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (L : CategoryTheory.Functor C D) (X : D) (X✝ : ↑(((CategoryTheory.Functor.id D).comp (CategoryTheory.CostructuredArrow.functor L)).obj X)) : (CategoryTheory.CostructuredArrow.ιCompGrothendieckProj L X).inv.app X✝ = CategoryTheory.CategoryStruct.id (CategoryTheory.CostructuredArrow.left X✝)
• CategoryTheory.CostructuredArrow.ιCompGrothendieckPrecompFunctorToCommaCompFst_hom_app 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.Functor
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (L : CategoryTheory.Functor C D) (R : CategoryTheory.Functor E D) (X : E) (X✝ : ↑((R.comp (CategoryTheory.CostructuredArrow.functor L)).obj X)) : (CategoryTheory.CostructuredArrow.ιCompGrothendieckPrecompFunctorToCommaCompFst L R X).hom.app X✝ = CategoryTheory.CategoryStruct.id (CategoryTheory.CostructuredArrow.left X✝)
• CategoryTheory.CostructuredArrow.ιCompGrothendieckPrecompFunctorToCommaCompFst_inv_app 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.Functor
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (L : CategoryTheory.Functor C D) (R : CategoryTheory.Functor E D) (X : E) (X✝ : ↑((R.comp (CategoryTheory.CostructuredArrow.functor L)).obj X)) : (CategoryTheory.CostructuredArrow.ιCompGrothendieckPrecompFunctorToCommaCompFst L R X).inv.app X✝ = CategoryTheory.CategoryStruct.id (CategoryTheory.CostructuredArrow.left X✝)
• CategoryTheory.CostructuredArrow.mapCompιCompGrothendieckProj_hom_app 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.Functor
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (L : CategoryTheory.Functor C D) {X Y : D} (f : X ⟶ Y) (X✝ : CategoryTheory.CostructuredArrow L X) : (CategoryTheory.CostructuredArrow.mapCompιCompGrothendieckProj L f).hom.app X✝ = CategoryTheory.CategoryStruct.id X✝.left
• CategoryTheory.CostructuredArrow.mapCompιCompGrothendieckProj_inv_app 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.Functor
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (L : CategoryTheory.Functor C D) {X Y : D} (f : X ⟶ Y) (X✝ : CategoryTheory.CostructuredArrow L X) : (CategoryTheory.CostructuredArrow.mapCompιCompGrothendieckProj L f).inv.app X✝ = CategoryTheory.CategoryStruct.id X✝.left
• CategoryTheory.Comma.final_fst 📋 Mathlib.CategoryTheory.Comma.Final
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T) (R : CategoryTheory.Functor B T) [R.Final] : (CategoryTheory.Comma.fst L R).Final
• CategoryTheory.Comma.initial_fst 📋 Mathlib.CategoryTheory.Comma.Final
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T) (R : CategoryTheory.Functor B T) [CategoryTheory.IsCofiltered A] [CategoryTheory.IsCofiltered B] [L.Initial] : (CategoryTheory.Comma.fst L R).Initial
• CategoryTheory.Comma.final_fst_of_isConnected_structuredArrow 📋 Mathlib.CategoryTheory.Comma.Final
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T) (R : CategoryTheory.Functor B T) [∀ (a : A), CategoryTheory.IsConnected (CategoryTheory.StructuredArrow (L.obj a) R)] : (CategoryTheory.Comma.fst L R).Final
• CategoryTheory.Comma.initial_fst_of_isCofiltered_costructuredArrow 📋 Mathlib.CategoryTheory.Comma.Final
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T) (R : CategoryTheory.Functor B T) [CategoryTheory.IsCofiltered A] [CategoryTheory.IsCofiltered B] [∀ (b : B), CategoryTheory.IsCofiltered (CategoryTheory.CostructuredArrow L (R.obj b))] : (CategoryTheory.Comma.fst L R).Initial
• CategoryTheory.instAdditiveCommaFst 📋 Mathlib.CategoryTheory.Preadditive.Comma
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Preadditive A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Preadditive B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] [CategoryTheory.Preadditive T] (L : CategoryTheory.Functor A T) [L.Additive] (R : CategoryTheory.Functor B T) [R.Additive] : (CategoryTheory.Comma.fst L R).Additive
• CategoryTheory.Comma.instIsCardinalAccessibleFst 📋 Mathlib.CategoryTheory.Presentable.Comma
  {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Category.{v_3, u_3} D] (F₁ : CategoryTheory.Functor C₁ D) (F₂ : CategoryTheory.Functor C₂ D) (κ : Cardinal.{w}) [Fact κ.IsRegular] [F₁.IsCardinalAccessible κ] [CategoryTheory.HasCardinalFilteredColimits C₁ κ] [CategoryTheory.HasCardinalFilteredColimits C₂ κ] : (CategoryTheory.Comma.fst F₁ F₂).IsCardinalAccessible κ
• CategoryTheory.Comma.instPreservesCardinalPresentableFst 📋 Mathlib.CategoryTheory.Presentable.Comma
  {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Category.{v_3, u_3} D] (F₁ : CategoryTheory.Functor C₁ D) (F₂ : CategoryTheory.Functor C₂ D) (κ : Cardinal.{w}) [Fact κ.IsRegular] [CategoryTheory.IsCardinalAccessibleCategory C₁ κ] [CategoryTheory.IsCardinalAccessibleCategory C₂ κ] [F₁.IsCardinalAccessible κ] [F₂.IsCardinalAccessible κ] [F₁.PreservesCardinalPresentable κ] [CategoryTheory.LocallySmall.{w, v_3, u_3} D] : (CategoryTheory.Comma.fst F₁ F₂).PreservesCardinalPresentable κ

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