Loogle!

Result

Found 134 declarations mentioning CategoryTheory.Limits.IsLimit.lift.

• CategoryTheory.Limits.IsLimit.lift 📋 Mathlib.CategoryTheory.Limits.IsLimit
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} {t : CategoryTheory.Limits.Cone F} (self : CategoryTheory.Limits.IsLimit t) (s : CategoryTheory.Limits.Cone F) : s.pt ⟶ t.pt
• CategoryTheory.Limits.IsLimit.ofPointIso 📋 Mathlib.CategoryTheory.Limits.IsLimit
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} {r t : CategoryTheory.Limits.Cone F} (P : CategoryTheory.Limits.IsLimit r) [i : CategoryTheory.IsIso (P.lift t)] : CategoryTheory.Limits.IsLimit t
• CategoryTheory.Limits.IsLimit.nonempty_isLimit_iff_isIso_lift 📋 Mathlib.CategoryTheory.Limits.IsLimit
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} {s t : CategoryTheory.Limits.Cone F} (hs : CategoryTheory.Limits.IsLimit s) : Nonempty (CategoryTheory.Limits.IsLimit t) ↔ CategoryTheory.IsIso (hs.lift t)
• CategoryTheory.Limits.IsLimit.lift_self 📋 Mathlib.CategoryTheory.Limits.IsLimit
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} {c : CategoryTheory.Limits.Cone F} (t : CategoryTheory.Limits.IsLimit c) : t.lift c = CategoryTheory.CategoryStruct.id c.pt
• CategoryTheory.Limits.IsLimit.liftConeMorphism_hom 📋 Mathlib.CategoryTheory.Limits.IsLimit
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} {t : CategoryTheory.Limits.Cone F} (h : CategoryTheory.Limits.IsLimit t) (s : CategoryTheory.Limits.Cone F) : (h.liftConeMorphism s).hom = h.lift s
• CategoryTheory.Limits.IsLimit.lift_comp_conePointUniqueUpToIso_hom 📋 Mathlib.CategoryTheory.Limits.IsLimit
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} {r s t : CategoryTheory.Limits.Cone F} (P : CategoryTheory.Limits.IsLimit s) (Q : CategoryTheory.Limits.IsLimit t) : CategoryTheory.CategoryStruct.comp (P.lift r) (P.conePointUniqueUpToIso Q).hom = Q.lift r
• CategoryTheory.Limits.IsLimit.lift_comp_conePointUniqueUpToIso_inv 📋 Mathlib.CategoryTheory.Limits.IsLimit
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} {r s t : CategoryTheory.Limits.Cone F} (P : CategoryTheory.Limits.IsLimit s) (Q : CategoryTheory.Limits.IsLimit t) : CategoryTheory.CategoryStruct.comp (Q.lift r) (P.conePointUniqueUpToIso Q).inv = P.lift r
• CategoryTheory.Limits.IsLimit.ofIsoLimit_lift 📋 Mathlib.CategoryTheory.Limits.IsLimit
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} {r t : CategoryTheory.Limits.Cone F} (P : CategoryTheory.Limits.IsLimit r) (i : r ≅ t) (s : CategoryTheory.Limits.Cone F) : (P.ofIsoLimit i).lift s = CategoryTheory.CategoryStruct.comp (P.lift s) i.hom.hom
• CategoryTheory.Limits.IsLimit.fac 📋 Mathlib.CategoryTheory.Limits.IsLimit
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} {t : CategoryTheory.Limits.Cone F} (self : CategoryTheory.Limits.IsLimit t) (s : CategoryTheory.Limits.Cone F) (j : J) : CategoryTheory.CategoryStruct.comp (self.lift s) (t.π.app j) = s.π.app j
• CategoryTheory.Limits.IsLimit.lift_comp_conePointsIsoOfNatIso_hom 📋 Mathlib.CategoryTheory.Limits.IsLimit
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F G : CategoryTheory.Functor J C} {r s : CategoryTheory.Limits.Cone F} {t : CategoryTheory.Limits.Cone G} (P : CategoryTheory.Limits.IsLimit s) (Q : CategoryTheory.Limits.IsLimit t) (w : F ≅ G) : CategoryTheory.CategoryStruct.comp (P.lift r) (P.conePointsIsoOfNatIso Q w).hom = CategoryTheory.Limits.IsLimit.map r Q w.hom
• CategoryTheory.Limits.IsLimit.lift_comp_conePointsIsoOfNatIso_inv 📋 Mathlib.CategoryTheory.Limits.IsLimit
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F G : CategoryTheory.Functor J C} {r s : CategoryTheory.Limits.Cone G} {t : CategoryTheory.Limits.Cone F} (P : CategoryTheory.Limits.IsLimit t) (Q : CategoryTheory.Limits.IsLimit s) (w : F ≅ G) : CategoryTheory.CategoryStruct.comp (Q.lift r) (P.conePointsIsoOfNatIso Q w).inv = CategoryTheory.Limits.IsLimit.map r P w.inv
• CategoryTheory.Limits.IsLimit.mkConeMorphism_lift 📋 Mathlib.CategoryTheory.Limits.IsLimit
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} {t : CategoryTheory.Limits.Cone F} (lift : (s : CategoryTheory.Limits.Cone F) → s ⟶ t) (uniq : ∀ (s : CategoryTheory.Limits.Cone F) (m : s ⟶ t), m = lift s) (s : CategoryTheory.Limits.Cone F) : (CategoryTheory.Limits.IsLimit.mkConeMorphism lift uniq).lift s = (lift s).hom
• CategoryTheory.Limits.IsLimit.lift_comp_conePointUniqueUpToIso_hom_assoc 📋 Mathlib.CategoryTheory.Limits.IsLimit
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} {r s t : CategoryTheory.Limits.Cone F} (P : CategoryTheory.Limits.IsLimit s) (Q : CategoryTheory.Limits.IsLimit t) {Z : C} (h : t.pt ⟶ Z) : CategoryTheory.CategoryStruct.comp (P.lift r) (CategoryTheory.CategoryStruct.comp (P.conePointUniqueUpToIso Q).hom h) = CategoryTheory.CategoryStruct.comp (Q.lift r) h
• CategoryTheory.Limits.IsLimit.lift_comp_conePointUniqueUpToIso_inv_assoc 📋 Mathlib.CategoryTheory.Limits.IsLimit
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} {r s t : CategoryTheory.Limits.Cone F} (P : CategoryTheory.Limits.IsLimit s) (Q : CategoryTheory.Limits.IsLimit t) {Z : C} (h : s.pt ⟶ Z) : CategoryTheory.CategoryStruct.comp (Q.lift r) (CategoryTheory.CategoryStruct.comp (P.conePointUniqueUpToIso Q).inv h) = CategoryTheory.CategoryStruct.comp (P.lift r) h
• CategoryTheory.Limits.IsLimit.ofFaithful 📋 Mathlib.CategoryTheory.Limits.IsLimit
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} {t : CategoryTheory.Limits.Cone F} {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] (G : CategoryTheory.Functor C D) [G.Faithful] (ht : CategoryTheory.Limits.IsLimit (G.mapCone t)) (lift : (s : CategoryTheory.Limits.Cone F) → s.pt ⟶ t.pt) (h : ∀ (s : CategoryTheory.Limits.Cone F), G.map (lift s) = ht.lift (G.mapCone s)) : CategoryTheory.Limits.IsLimit t
• CategoryTheory.Limits.IsLimit.hom_lift 📋 Mathlib.CategoryTheory.Limits.IsLimit
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} {t : CategoryTheory.Limits.Cone F} (h : CategoryTheory.Limits.IsLimit t) {W : C} (m : W ⟶ t.pt) : m = h.lift { pt := W, π := { app := fun b => CategoryTheory.CategoryStruct.comp m (t.π.app b), naturality := ⋯ } }
• CategoryTheory.Limits.IsLimit.uniq 📋 Mathlib.CategoryTheory.Limits.IsLimit
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} {t : CategoryTheory.Limits.Cone F} (self : CategoryTheory.Limits.IsLimit t) (s : CategoryTheory.Limits.Cone F) (m : s.pt ⟶ t.pt) : (∀ (j : J), CategoryTheory.CategoryStruct.comp m (t.π.app j) = s.π.app j) → m = self.lift s
• CategoryTheory.Limits.IsLimit.fac_assoc 📋 Mathlib.CategoryTheory.Limits.IsLimit
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} {t : CategoryTheory.Limits.Cone F} (self : CategoryTheory.Limits.IsLimit t) (s : CategoryTheory.Limits.Cone F) (j : J) {Z : C} (h : F.obj j ⟶ Z) : CategoryTheory.CategoryStruct.comp (self.lift s) (CategoryTheory.CategoryStruct.comp (t.π.app j) h) = CategoryTheory.CategoryStruct.comp (s.π.app j) h
• CategoryTheory.Limits.IsLimit.lift_comp_conePointsIsoOfNatIso_hom_assoc 📋 Mathlib.CategoryTheory.Limits.IsLimit
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F G : CategoryTheory.Functor J C} {r s : CategoryTheory.Limits.Cone F} {t : CategoryTheory.Limits.Cone G} (P : CategoryTheory.Limits.IsLimit s) (Q : CategoryTheory.Limits.IsLimit t) (w : F ≅ G) {Z : C} (h : t.pt ⟶ Z) : CategoryTheory.CategoryStruct.comp (P.lift r) (CategoryTheory.CategoryStruct.comp (P.conePointsIsoOfNatIso Q w).hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.IsLimit.map r Q w.hom) h
• CategoryTheory.Limits.IsLimit.lift_comp_conePointsIsoOfNatIso_inv_assoc 📋 Mathlib.CategoryTheory.Limits.IsLimit
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F G : CategoryTheory.Functor J C} {r s : CategoryTheory.Limits.Cone G} {t : CategoryTheory.Limits.Cone F} (P : CategoryTheory.Limits.IsLimit t) (Q : CategoryTheory.Limits.IsLimit s) (w : F ≅ G) {Z : C} (h : t.pt ⟶ Z) : CategoryTheory.CategoryStruct.comp (Q.lift r) (CategoryTheory.CategoryStruct.comp (P.conePointsIsoOfNatIso Q w).inv h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.IsLimit.map r P w.inv) h
• CategoryTheory.Limits.IsLimit.conePointsIsoOfEquivalence_inv 📋 Mathlib.CategoryTheory.Limits.IsLimit
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} {s : CategoryTheory.Limits.Cone F} {G : CategoryTheory.Functor K C} {t : CategoryTheory.Limits.Cone G} (P : CategoryTheory.Limits.IsLimit s) (Q : CategoryTheory.Limits.IsLimit t) (e : J ≌ K) (w : e.functor.comp G ≅ F) : (P.conePointsIsoOfEquivalence Q e w).inv = P.lift ((CategoryTheory.Limits.Cone.equivalenceOfReindexing e w).functor.obj t)
• CategoryTheory.Limits.IsLimit.conePointsIsoOfEquivalence_hom 📋 Mathlib.CategoryTheory.Limits.IsLimit
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} {s : CategoryTheory.Limits.Cone F} {G : CategoryTheory.Functor K C} {t : CategoryTheory.Limits.Cone G} (P : CategoryTheory.Limits.IsLimit s) (Q : CategoryTheory.Limits.IsLimit t) (e : J ≌ K) (w : e.functor.comp G ≅ F) : (P.conePointsIsoOfEquivalence Q e w).hom = Q.lift ((CategoryTheory.Limits.Cone.equivalenceOfReindexing e.symm ((e.inverse.isoWhiskerLeft w).symm ≪≫ e.invFunIdAssoc G)).functor.obj s)
• CategoryTheory.Limits.IsLimit.ofConeEquiv_symm_apply_desc 📋 Mathlib.CategoryTheory.Limits.IsLimit
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] {G : CategoryTheory.Functor K D} (h : CategoryTheory.Limits.Cone G ≌ CategoryTheory.Limits.Cone F) {c : CategoryTheory.Limits.Cone G} (P : CategoryTheory.Limits.IsLimit c) (s : CategoryTheory.Limits.Cone F) : ((CategoryTheory.Limits.IsLimit.ofConeEquiv h).symm P).lift s = CategoryTheory.CategoryStruct.comp (h.counitIso.inv.app s).hom (h.functor.map (P.liftConeMorphism (h.inverse.obj s))).hom
• CategoryTheory.Limits.IsLimit.ofConeEquiv_symm_apply_lift 📋 Mathlib.CategoryTheory.Limits.IsLimit
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] {G : CategoryTheory.Functor K D} (h : CategoryTheory.Limits.Cone G ≌ CategoryTheory.Limits.Cone F) {c : CategoryTheory.Limits.Cone G} (P : CategoryTheory.Limits.IsLimit c) (s : CategoryTheory.Limits.Cone F) : ((CategoryTheory.Limits.IsLimit.ofConeEquiv h).symm P).lift s = CategoryTheory.CategoryStruct.comp (h.counitIso.inv.app s).hom (h.functor.map (P.liftConeMorphism (h.inverse.obj s))).hom
• CategoryTheory.Limits.IsLimit.ofConeEquiv_apply_desc 📋 Mathlib.CategoryTheory.Limits.IsLimit
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] {G : CategoryTheory.Functor K D} (h : CategoryTheory.Limits.Cone G ≌ CategoryTheory.Limits.Cone F) {c : CategoryTheory.Limits.Cone G} (P : CategoryTheory.Limits.IsLimit (h.functor.obj c)) (s : CategoryTheory.Limits.Cone G) : ((CategoryTheory.Limits.IsLimit.ofConeEquiv h) P).lift s = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (h.unitIso.hom.app s).hom (h.inverse.map (P.liftConeMorphism (h.functor.obj s))).hom) (h.unitIso.inv.app c).hom
• CategoryTheory.Limits.IsLimit.ofConeEquiv_apply_lift 📋 Mathlib.CategoryTheory.Limits.IsLimit
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] {G : CategoryTheory.Functor K D} (h : CategoryTheory.Limits.Cone G ≌ CategoryTheory.Limits.Cone F) {c : CategoryTheory.Limits.Cone G} (P : CategoryTheory.Limits.IsLimit (h.functor.obj c)) (s : CategoryTheory.Limits.Cone G) : ((CategoryTheory.Limits.IsLimit.ofConeEquiv h) P).lift s = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (h.unitIso.hom.app s).hom (h.inverse.map (P.liftConeMorphism (h.functor.obj s))).hom) (h.unitIso.inv.app c).hom
• CategoryTheory.Limits.limit.isLimit_lift 📋 Mathlib.CategoryTheory.Limits.HasLimits
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor J C} [CategoryTheory.Limits.HasLimit F] (c : CategoryTheory.Limits.Cone F) : (CategoryTheory.Limits.limit.isLimit F).lift c = CategoryTheory.Limits.limit.lift F c
• CategoryTheory.Limits.limit.pre_eq 📋 Mathlib.CategoryTheory.Limits.HasLimits
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor J C} [CategoryTheory.Limits.HasLimit F] {E : CategoryTheory.Functor K J} [CategoryTheory.Limits.HasLimit (E.comp F)] (s : CategoryTheory.Limits.LimitCone (E.comp F)) (t : CategoryTheory.Limits.LimitCone F) : CategoryTheory.Limits.limit.pre F E = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.isoLimitCone t).hom (CategoryTheory.CategoryStruct.comp (s.isLimit.lift (CategoryTheory.Limits.Cone.whisker E t.cone)) (CategoryTheory.Limits.limit.isoLimitCone s).inv)
• CategoryTheory.Limits.isLimitConeOfAdj_lift 📋 Mathlib.CategoryTheory.Limits.HasLimits
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [CategoryTheory.Category.{v, u} C] {L : CategoryTheory.Functor (CategoryTheory.Functor J C) C} (adj : CategoryTheory.Functor.const J ⊣ L) (F : CategoryTheory.Functor J C) (s : CategoryTheory.Limits.Cone F) : (CategoryTheory.Limits.isLimitConeOfAdj adj F).lift s = (adj.homEquiv s.pt F) s.π
• CategoryTheory.Limits.Fan.IsLimit.lift_proj 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X : β → C} {c : CategoryTheory.Limits.Fan X} (d : CategoryTheory.Limits.Fan X) (hc : CategoryTheory.Limits.IsLimit c) (i : β) : CategoryTheory.CategoryStruct.comp (hc.lift d) (c.proj i) = d.proj i
• CategoryTheory.Limits.Fan.IsLimit.lift_proj_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X : β → C} {c : CategoryTheory.Limits.Fan X} (d : CategoryTheory.Limits.Fan X) (hc : CategoryTheory.Limits.IsLimit c) (i : β) {Z : C} (h : X i ⟶ Z) : CategoryTheory.CategoryStruct.comp (hc.lift d) (CategoryTheory.CategoryStruct.comp (c.proj i) h) = CategoryTheory.CategoryStruct.comp (d.proj i) h
• CategoryTheory.Limits.Fan.IsLimit.mk_lift 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {f : β → C} (t : CategoryTheory.Limits.Fan f) (lift : (s : CategoryTheory.Limits.Fan f) → s.pt ⟶ t.pt) (fac : ∀ (s : CategoryTheory.Limits.Fan f) (j : β), CategoryTheory.CategoryStruct.comp (lift s) (t.proj j) = s.proj j := by cat_disch) (uniq : ∀ (s : CategoryTheory.Limits.Fan f) (m : s.pt ⟶ t.pt), (∀ (j : β), CategoryTheory.CategoryStruct.comp m (t.proj j) = s.proj j) → m = lift s := by cat_disch) (s : CategoryTheory.Limits.Fan f) : (CategoryTheory.Limits.Fan.IsLimit.mk t lift fac uniq).lift s = lift s
• CategoryTheory.Limits.limitConeOfUnique_isLimit_lift 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [Unique β] (f : β → C) (s : CategoryTheory.Limits.Cone (CategoryTheory.Discrete.functor f)) : (CategoryTheory.Limits.limitConeOfUnique f).isLimit.lift s = s.π.app default
• CategoryTheory.Limits.IsLimit.binaryFanSwap_lift 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryFan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {s : CategoryTheory.Limits.BinaryFan X Y} (I : CategoryTheory.Limits.IsLimit s) (t : CategoryTheory.Limits.Cone (CategoryTheory.Limits.pair Y X)) : I.binaryFanSwap.lift t = I.lift (CategoryTheory.Limits.BinaryFan.swap t)
• CategoryTheory.Limits.IsLimit.assoc_lift 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryFan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : C} {sXY : CategoryTheory.Limits.BinaryFan X Y} {sYZ : CategoryTheory.Limits.BinaryFan Y Z} (P : CategoryTheory.Limits.IsLimit sXY) (Q : CategoryTheory.Limits.IsLimit sYZ) {s : CategoryTheory.Limits.BinaryFan sXY.pt Z} (R : CategoryTheory.Limits.IsLimit s) (t : CategoryTheory.Limits.Cone (CategoryTheory.Limits.pair X sYZ.pt)) : (P.assoc Q R).lift t = R.lift (CategoryTheory.Limits.BinaryFan.assocInv P t)
• CategoryTheory.Limits.BinaryFan.IsLimit.lift'_coe 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryFan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {W X Y : C} {s : CategoryTheory.Limits.BinaryFan X Y} (h : CategoryTheory.Limits.IsLimit s) (f : W ⟶ X) (g : W ⟶ Y) : ↑(CategoryTheory.Limits.BinaryFan.IsLimit.lift' h f g) = h.lift (CategoryTheory.Limits.BinaryFan.mk f g)
• CategoryTheory.Limits.BinaryFan.assoc_snd 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryFan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : C} {sXY : CategoryTheory.Limits.BinaryFan X Y} {sYZ : CategoryTheory.Limits.BinaryFan Y Z} (Q : CategoryTheory.Limits.IsLimit sYZ) (s : CategoryTheory.Limits.BinaryFan sXY.pt Z) : (CategoryTheory.Limits.BinaryFan.assoc Q s).snd = Q.lift (CategoryTheory.Limits.BinaryFan.mk (CategoryTheory.CategoryStruct.comp s.fst sXY.snd) s.snd)
• CategoryTheory.Limits.BinaryFan.rightUnitor_inv 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryFan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {s : CategoryTheory.Limits.Cone (CategoryTheory.Functor.empty C)} (P : CategoryTheory.Limits.IsLimit s) {t : CategoryTheory.Limits.BinaryFan X s.pt} (Q : CategoryTheory.Limits.IsLimit t) : (CategoryTheory.Limits.BinaryFan.rightUnitor P Q).inv = Q.lift (CategoryTheory.Limits.BinaryFan.mk (CategoryTheory.CategoryStruct.id X) (P.lift { pt := X, π := { app := fun x => x.as.elim, naturality := ⋯ } }))
• CategoryTheory.Limits.BinaryFan.leftUnitor_inv 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryFan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {s : CategoryTheory.Limits.Cone (CategoryTheory.Functor.empty C)} (P : CategoryTheory.Limits.IsLimit s) {t : CategoryTheory.Limits.BinaryFan s.pt X} (Q : CategoryTheory.Limits.IsLimit t) : (CategoryTheory.Limits.BinaryFan.leftUnitor P Q).inv = Q.lift (CategoryTheory.Limits.BinaryFan.mk (P.lift { pt := X, π := { app := fun x => x.as.elim, naturality := ⋯ } }) (CategoryTheory.CategoryStruct.id { pt := X, π := { app := fun x => x.as.elim, naturality := ⋯ } }.pt))
• CategoryTheory.Limits.Fork.IsLimit.lift_ι 📋 Mathlib.CategoryTheory.Limits.Shapes.Equalizers
  {C : Type u} {X Y : C} [CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y} {s t : CategoryTheory.Limits.Fork f g} (hs : CategoryTheory.Limits.IsLimit s) : CategoryTheory.CategoryStruct.comp (hs.lift t) s.ι = t.ι
• CategoryTheory.Limits.Fork.IsLimit.lift_ι_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Equalizers
  {C : Type u} {X Y : C} [CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y} {s t : CategoryTheory.Limits.Fork f g} (hs : CategoryTheory.Limits.IsLimit s) {Z : C} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (hs.lift t) (CategoryTheory.CategoryStruct.comp s.ι h) = CategoryTheory.CategoryStruct.comp t.ι h
• CategoryTheory.Limits.splitMonoOfIdempotentOfIsLimitFork_retraction 📋 Mathlib.CategoryTheory.Limits.Shapes.Equalizers
  (C : Type u) [CategoryTheory.Category.{v, u} C] {X : C} {f : X ⟶ X} (hf : CategoryTheory.CategoryStruct.comp f f = f) {c : CategoryTheory.Limits.Fork (CategoryTheory.CategoryStruct.id X) f} (i : CategoryTheory.Limits.IsLimit c) : (CategoryTheory.Limits.splitMonoOfIdempotentOfIsLimitFork C hf i).retraction = i.lift (CategoryTheory.Limits.Fork.ofι f ⋯)
• CategoryTheory.Limits.Fork.IsLimit.mk_lift 📋 Mathlib.CategoryTheory.Limits.Shapes.Equalizers
  {C : Type u} {X Y : C} [CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y} (t : CategoryTheory.Limits.Fork f g) (lift : (s : CategoryTheory.Limits.Fork f g) → s.pt ⟶ t.pt) (fac : ∀ (s : CategoryTheory.Limits.Fork f g), CategoryTheory.CategoryStruct.comp (lift s) t.ι = s.ι) (uniq : ∀ (s : CategoryTheory.Limits.Fork f g) (m : s.pt ⟶ t.pt), CategoryTheory.CategoryStruct.comp m t.ι = s.ι → m = lift s) (s : CategoryTheory.Limits.Fork f g) : (CategoryTheory.Limits.Fork.IsLimit.mk t lift fac uniq).lift s = lift s
• CategoryTheory.Limits.isKernelCompMono_lift 📋 Mathlib.CategoryTheory.Limits.Shapes.Kernels
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} {f : X ⟶ Y} {c : CategoryTheory.Limits.KernelFork f} (i : CategoryTheory.Limits.IsLimit c) {Z : C} (g : Y ⟶ Z) [hg : CategoryTheory.Mono g] {h : X ⟶ Z} (hh : h = CategoryTheory.CategoryStruct.comp f g) (s : CategoryTheory.Limits.KernelFork h) : (CategoryTheory.Limits.isKernelCompMono i g hh).lift s = i.lift (CategoryTheory.Limits.Fork.ofι (CategoryTheory.Limits.Fork.ι s) ⋯)
• CategoryTheory.Preadditive.isLimitForkOfKernelFork_lift 📋 Mathlib.CategoryTheory.Preadditive.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {X Y : C} {f g : X ⟶ Y} {c : CategoryTheory.Limits.KernelFork (f - g)} (i : CategoryTheory.Limits.IsLimit c) (s : CategoryTheory.Limits.Fork f g) : (CategoryTheory.Preadditive.isLimitForkOfKernelFork i).lift s = i.lift (CategoryTheory.Preadditive.kernelForkOfFork s)
• CategoryTheory.Limits.Bicone.ι_of_isLimit 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
  {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {f : J → C} {t : CategoryTheory.Limits.Bicone f} (ht : CategoryTheory.Limits.IsLimit t.toCone) (j : J) : t.ι j = ht.lift (CategoryTheory.Limits.Fan.mk (f j) fun j' => if h : j = j' then CategoryTheory.eqToHom ⋯ else 0)
• CategoryTheory.Limits.Bicone.ofLimitCone_ι 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
  {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {f : J → C} {t : CategoryTheory.Limits.Cone (CategoryTheory.Discrete.functor f)} (ht : CategoryTheory.Limits.IsLimit t) (j : J) : (CategoryTheory.Limits.Bicone.ofLimitCone ht).ι j = ht.lift (CategoryTheory.Limits.Fan.mk (f j) fun j' => if h : j = j' then CategoryTheory.eqToHom ⋯ else 0)
• CategoryTheory.Limits.kernelBiproductπIso_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
  {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (f : J → C) (i : J) [CategoryTheory.Limits.HasBiproduct f] [CategoryTheory.Limits.HasBiproduct (Subtype.restrict (fun j => j ≠ i) f)] : (CategoryTheory.Limits.kernelBiproductπIso f i).hom = (CategoryTheory.Limits.biproduct.isLimitFromSubtype f i).lift (CategoryTheory.Limits.limit.cone (CategoryTheory.Limits.parallelPair (CategoryTheory.Limits.biproduct.π f i) 0))
• CategoryTheory.Limits.kernelBiproductToSubtypeIso_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {K : Type} [Finite K] [CategoryTheory.Limits.HasFiniteBiproducts C] (f : K → C) (p : K → Prop) : (CategoryTheory.Limits.kernelBiproductToSubtypeIso f p).hom = (CategoryTheory.Limits.KernelFork.IsLimit.ofι (CategoryTheory.Limits.biproduct.fromSubtype f pᶜ) ⋯ (fun {x} g x_1 => CategoryTheory.CategoryStruct.comp g (CategoryTheory.Limits.biproduct.toSubtype f pᶜ)) ⋯ ⋯).lift (CategoryTheory.Limits.limit.cone (CategoryTheory.Limits.parallelPair (CategoryTheory.Limits.biproduct.toSubtype f p) 0))
• CategoryTheory.Limits.kernelBiprodFstIso_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
  {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} [CategoryTheory.Limits.HasBinaryBiproduct X Y] : CategoryTheory.Limits.kernelBiprodFstIso.hom = (CategoryTheory.Limits.biprod.isKernelFstKernelFork X Y).lift (CategoryTheory.Limits.limit.cone (CategoryTheory.Limits.parallelPair CategoryTheory.Limits.biprod.fst 0))
• CategoryTheory.Limits.kernelBiprodSndIso_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
  {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} [CategoryTheory.Limits.HasBinaryBiproduct X Y] : CategoryTheory.Limits.kernelBiprodSndIso.hom = (CategoryTheory.Limits.biprod.isKernelSndKernelFork X Y).lift (CategoryTheory.Limits.limit.cone (CategoryTheory.Limits.parallelPair CategoryTheory.Limits.biprod.snd 0))
• CategoryTheory.Limits.Types.limitConeIsLimit_lift 📋 Mathlib.CategoryTheory.Limits.Types.Limits
  {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J (Type (max v u))) (s : CategoryTheory.Limits.Cone F) : (CategoryTheory.Limits.Types.limitConeIsLimit F).lift s = TypeCat.ofHom fun v => ⟨fun j => (CategoryTheory.ConcreteCategory.hom (s.π.app j)) v, ⋯⟩
• CategoryTheory.Limits.Types.Small.limitConeIsLimit_lift 📋 Mathlib.CategoryTheory.Limits.Types.Limits
  {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J (Type u)) [Small.{u, max u v} ↑F.sections] (s : CategoryTheory.Limits.Cone F) : (CategoryTheory.Limits.Types.Small.limitConeIsLimit F).lift s = TypeCat.ofHom fun v => (equivShrink ↑F.sections) ⟨fun j => (CategoryTheory.ConcreteCategory.hom (s.π.app j)) v, ⋯⟩
• CategoryTheory.preserves_lift_mapCone 📋 Mathlib.CategoryTheory.Limits.Preserves.Limits
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {J : Type w} [CategoryTheory.Category.{w', w} J] (F : CategoryTheory.Functor J C) [CategoryTheory.Limits.PreservesLimit F G] (c₁ c₂ : CategoryTheory.Limits.Cone F) (t : CategoryTheory.Limits.IsLimit c₁) : (CategoryTheory.Limits.isLimitOfPreserves G t).lift (G.mapCone c₂) = G.map (t.lift c₂)
• CategoryTheory.Limits.combineCones_pt_map 📋 Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] (F : CategoryTheory.Functor J (CategoryTheory.Functor K C)) (c : (k : K) → CategoryTheory.Limits.LimitCone (F.flip.obj k)) {k₁ k₂ : K} (f : k₁ ⟶ k₂) : (CategoryTheory.Limits.combineCones F c).pt.map f = (c k₂).isLimit.lift { pt := (c k₁).cone.pt, π := CategoryTheory.CategoryStruct.comp (c k₁).cone.π (F.flip.map f) }
• CategoryTheory.Limits.combineCones_π_app_app 📋 Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] (F : CategoryTheory.Functor J (CategoryTheory.Functor K C)) (c : (k : K) → CategoryTheory.Limits.LimitCone (F.flip.obj k)) (j : J) (k : K) : ((CategoryTheory.Limits.combineCones F c).π.app j).app k = (c k).cone.π.app j
• CategoryTheory.Limits.isColimitCoconeLeftOpOfCone_desc 📋 Mathlib.CategoryTheory.Limits.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [CategoryTheory.Category.{v₂, u₂} J] (F : CategoryTheory.Functor J Cᵒᵖ) {c : CategoryTheory.Limits.Cone F} (hc : CategoryTheory.Limits.IsLimit c) (s : CategoryTheory.Limits.Cocone F.leftOp) : (CategoryTheory.Limits.isColimitCoconeLeftOpOfCone F hc).desc s = (hc.lift (CategoryTheory.Limits.coneOfCoconeLeftOp s)).unop
• CategoryTheory.Limits.isLimitConeLeftOpOfCocone_lift 📋 Mathlib.CategoryTheory.Limits.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [CategoryTheory.Category.{v₂, u₂} J] (F : CategoryTheory.Functor J Cᵒᵖ) {c : CategoryTheory.Limits.Cocone F} (hc : CategoryTheory.Limits.IsColimit c) (s : CategoryTheory.Limits.Cone F.leftOp) : (CategoryTheory.Limits.isLimitConeLeftOpOfCocone F hc).lift s = (hc.desc (CategoryTheory.Limits.coconeOfConeLeftOp s)).unop
• CategoryTheory.Limits.isColimitCoconeRightOpOfCone_desc 📋 Mathlib.CategoryTheory.Limits.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [CategoryTheory.Category.{v₂, u₂} J] (F : CategoryTheory.Functor Jᵒᵖ C) {c : CategoryTheory.Limits.Cone F} (hc : CategoryTheory.Limits.IsLimit c) (s : CategoryTheory.Limits.Cocone F.rightOp) : (CategoryTheory.Limits.isColimitCoconeRightOpOfCone F hc).desc s = (hc.lift (CategoryTheory.Limits.coneOfCoconeRightOp s)).op
• CategoryTheory.Limits.isLimitConeRightOpOfCocone_lift 📋 Mathlib.CategoryTheory.Limits.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [CategoryTheory.Category.{v₂, u₂} J] (F : CategoryTheory.Functor Jᵒᵖ C) {c : CategoryTheory.Limits.Cocone F} (hc : CategoryTheory.Limits.IsColimit c) (s : CategoryTheory.Limits.Cone F.rightOp) : (CategoryTheory.Limits.isLimitConeRightOpOfCocone F hc).lift s = (hc.desc (CategoryTheory.Limits.coconeOfConeRightOp s)).op
• CategoryTheory.Limits.isColimitCoconeOfConeUnop_desc 📋 Mathlib.CategoryTheory.Limits.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [CategoryTheory.Category.{v₂, u₂} J] (F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ) {c : CategoryTheory.Limits.Cone F.unop} (hc : CategoryTheory.Limits.IsLimit c) (s : CategoryTheory.Limits.Cocone F) : (CategoryTheory.Limits.isColimitCoconeOfConeUnop F hc).desc s = (hc.lift (CategoryTheory.Limits.coneUnopOfCocone s)).op
• CategoryTheory.Limits.isLimitConeOfCoconeUnop_lift 📋 Mathlib.CategoryTheory.Limits.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [CategoryTheory.Category.{v₂, u₂} J] (F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ) {c : CategoryTheory.Limits.Cocone F.unop} (hc : CategoryTheory.Limits.IsColimit c) (s : CategoryTheory.Limits.Cone F) : (CategoryTheory.Limits.isLimitConeOfCoconeUnop F hc).lift s = (hc.desc (CategoryTheory.Limits.coconeUnopOfCone s)).op
• CategoryTheory.Limits.isColimitCoconeUnopOfCone_desc 📋 Mathlib.CategoryTheory.Limits.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [CategoryTheory.Category.{v₂, u₂} J] (F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ) {c : CategoryTheory.Limits.Cone F} (hc : CategoryTheory.Limits.IsLimit c) (s : CategoryTheory.Limits.Cocone F.unop) : (CategoryTheory.Limits.isColimitCoconeUnopOfCone F hc).desc s = (hc.lift (CategoryTheory.Limits.coneOfCoconeUnop s)).unop
• CategoryTheory.Limits.isLimitConeUnopOfCocone_lift 📋 Mathlib.CategoryTheory.Limits.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [CategoryTheory.Category.{v₂, u₂} J] (F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ) {c : CategoryTheory.Limits.Cocone F} (hc : CategoryTheory.Limits.IsColimit c) (s : CategoryTheory.Limits.Cone F.unop) : (CategoryTheory.Limits.isLimitConeUnopOfCocone F hc).lift s = (hc.desc (CategoryTheory.Limits.coconeOfConeUnop s)).unop
• CategoryTheory.Limits.isColimitOfConeRightOpOfCocone_desc 📋 Mathlib.CategoryTheory.Limits.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [CategoryTheory.Category.{v₂, u₂} J] (F : CategoryTheory.Functor Jᵒᵖ C) {c : CategoryTheory.Limits.Cocone F} (hc : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.coneRightOpOfCocone c)) (s : CategoryTheory.Limits.Cocone F) : (CategoryTheory.Limits.isColimitOfConeRightOpOfCocone F hc).desc s = (hc.lift (CategoryTheory.Limits.coneRightOpOfCocone s)).unop
• CategoryTheory.Limits.isLimitOfCoconeRightOpOfCone_lift 📋 Mathlib.CategoryTheory.Limits.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [CategoryTheory.Category.{v₂, u₂} J] (F : CategoryTheory.Functor Jᵒᵖ C) {c : CategoryTheory.Limits.Cone F} (hc : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.coconeRightOpOfCone c)) (s : CategoryTheory.Limits.Cone F) : (CategoryTheory.Limits.isLimitOfCoconeRightOpOfCone F hc).lift s = (hc.desc (CategoryTheory.Limits.coconeRightOpOfCone s)).unop
• CategoryTheory.Limits.isColimitOfConeLeftOpOfCocone_desc 📋 Mathlib.CategoryTheory.Limits.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [CategoryTheory.Category.{v₂, u₂} J] (F : CategoryTheory.Functor J Cᵒᵖ) {c : CategoryTheory.Limits.Cocone F} (hc : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.coneLeftOpOfCocone c)) (s : CategoryTheory.Limits.Cocone F) : (CategoryTheory.Limits.isColimitOfConeLeftOpOfCocone F hc).desc s = (hc.lift (CategoryTheory.Limits.coneLeftOpOfCocone s)).op
• CategoryTheory.Limits.isLimitOfCoconeLeftOpOfCone_lift 📋 Mathlib.CategoryTheory.Limits.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [CategoryTheory.Category.{v₂, u₂} J] (F : CategoryTheory.Functor J Cᵒᵖ) {c : CategoryTheory.Limits.Cone F} (hc : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.coconeLeftOpOfCone c)) (s : CategoryTheory.Limits.Cone F) : (CategoryTheory.Limits.isLimitOfCoconeLeftOpOfCone F hc).lift s = (hc.desc (CategoryTheory.Limits.coconeLeftOpOfCone s)).op
• CategoryTheory.Limits.isColimitCoconeOfConeRightOp_desc 📋 Mathlib.CategoryTheory.Limits.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [CategoryTheory.Category.{v₂, u₂} J] (F : CategoryTheory.Functor Jᵒᵖ C) {c : CategoryTheory.Limits.Cone F.rightOp} (hc : CategoryTheory.Limits.IsLimit c) (s : CategoryTheory.Limits.Cocone F) : (CategoryTheory.Limits.isColimitCoconeOfConeRightOp F hc).desc s = (hc.lift (CategoryTheory.Limits.coneRightOpOfCocone s)).unop
• CategoryTheory.Limits.isColimitOfConeOfCoconeLeftOp_desc 📋 Mathlib.CategoryTheory.Limits.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [CategoryTheory.Category.{v₂, u₂} J] (F : CategoryTheory.Functor J Cᵒᵖ) {c : CategoryTheory.Limits.Cocone F.leftOp} (hc : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.coneOfCoconeLeftOp c)) (s : CategoryTheory.Limits.Cocone F.leftOp) : (CategoryTheory.Limits.isColimitOfConeOfCoconeLeftOp F hc).desc s = (hc.lift (CategoryTheory.Limits.coneOfCoconeLeftOp s)).unop
• CategoryTheory.Limits.isColimitOfConeOfCoconeUnop_desc 📋 Mathlib.CategoryTheory.Limits.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [CategoryTheory.Category.{v₂, u₂} J] (F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ) {c : CategoryTheory.Limits.Cocone F.unop} (hc : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.coneOfCoconeUnop c)) (s : CategoryTheory.Limits.Cocone F.unop) : (CategoryTheory.Limits.isColimitOfConeOfCoconeUnop F hc).desc s = (hc.lift (CategoryTheory.Limits.coneOfCoconeUnop s)).unop
• CategoryTheory.Limits.isLimitConeOfCoconeRightOp_lift 📋 Mathlib.CategoryTheory.Limits.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [CategoryTheory.Category.{v₂, u₂} J] (F : CategoryTheory.Functor Jᵒᵖ C) {c : CategoryTheory.Limits.Cocone F.rightOp} (hc : CategoryTheory.Limits.IsColimit c) (s : CategoryTheory.Limits.Cone F) : (CategoryTheory.Limits.isLimitConeOfCoconeRightOp F hc).lift s = (hc.desc (CategoryTheory.Limits.coconeRightOpOfCone s)).unop
• CategoryTheory.Limits.isLimitOfCoconeOfConeLeftOp_lift 📋 Mathlib.CategoryTheory.Limits.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [CategoryTheory.Category.{v₂, u₂} J] (F : CategoryTheory.Functor J Cᵒᵖ) {c : CategoryTheory.Limits.Cone F.leftOp} (hc : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.coconeOfConeLeftOp c)) (s : CategoryTheory.Limits.Cone F.leftOp) : (CategoryTheory.Limits.isLimitOfCoconeOfConeLeftOp F hc).lift s = (hc.desc (CategoryTheory.Limits.coconeOfConeLeftOp s)).unop
• CategoryTheory.Limits.isLimitOfCoconeOfConeUnop_lift 📋 Mathlib.CategoryTheory.Limits.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [CategoryTheory.Category.{v₂, u₂} J] (F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ) {c : CategoryTheory.Limits.Cone F.unop} (hc : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.coconeOfConeUnop c)) (s : CategoryTheory.Limits.Cone F.unop) : (CategoryTheory.Limits.isLimitOfCoconeOfConeUnop F hc).lift s = (hc.desc (CategoryTheory.Limits.coconeOfConeUnop s)).unop
• CategoryTheory.Limits.isColimitCoconeOfConeLeftOp_desc 📋 Mathlib.CategoryTheory.Limits.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [CategoryTheory.Category.{v₂, u₂} J] (F : CategoryTheory.Functor J Cᵒᵖ) {c : CategoryTheory.Limits.Cone F.leftOp} (hc : CategoryTheory.Limits.IsLimit c) (s : CategoryTheory.Limits.Cocone F) : (CategoryTheory.Limits.isColimitCoconeOfConeLeftOp F hc).desc s = (hc.lift (CategoryTheory.Limits.coneLeftOpOfCocone s)).op
• CategoryTheory.Limits.isColimitOfConeOfCoconeRightOp_desc 📋 Mathlib.CategoryTheory.Limits.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [CategoryTheory.Category.{v₂, u₂} J] (F : CategoryTheory.Functor Jᵒᵖ C) {c : CategoryTheory.Limits.Cocone F.rightOp} (hc : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.coneOfCoconeRightOp c)) (s : CategoryTheory.Limits.Cocone F.rightOp) : (CategoryTheory.Limits.isColimitOfConeOfCoconeRightOp F hc).desc s = (hc.lift (CategoryTheory.Limits.coneOfCoconeRightOp s)).op
• CategoryTheory.Limits.isLimitConeOfCoconeLeftOp_lift 📋 Mathlib.CategoryTheory.Limits.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [CategoryTheory.Category.{v₂, u₂} J] (F : CategoryTheory.Functor J Cᵒᵖ) {c : CategoryTheory.Limits.Cocone F.leftOp} (hc : CategoryTheory.Limits.IsColimit c) (s : CategoryTheory.Limits.Cone F) : (CategoryTheory.Limits.isLimitConeOfCoconeLeftOp F hc).lift s = (hc.desc (CategoryTheory.Limits.coconeLeftOpOfCone s)).op
• CategoryTheory.Limits.isLimitOfCoconeOfConeRightOp_lift 📋 Mathlib.CategoryTheory.Limits.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [CategoryTheory.Category.{v₂, u₂} J] (F : CategoryTheory.Functor Jᵒᵖ C) {c : CategoryTheory.Limits.Cone F.rightOp} (hc : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.coconeOfConeRightOp c)) (s : CategoryTheory.Limits.Cone F.rightOp) : (CategoryTheory.Limits.isLimitOfCoconeOfConeRightOp F hc).lift s = (hc.desc (CategoryTheory.Limits.coconeOfConeRightOp s)).op
• CategoryTheory.Limits.isColimitOfConeUnopOfCocone_desc 📋 Mathlib.CategoryTheory.Limits.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [CategoryTheory.Category.{v₂, u₂} J] (F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ) {c : CategoryTheory.Limits.Cocone F} (hc : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.coneUnopOfCocone c)) (s : CategoryTheory.Limits.Cocone F) : (CategoryTheory.Limits.isColimitOfConeUnopOfCocone F hc).desc s = (hc.lift (CategoryTheory.Limits.coneUnopOfCocone s)).op
• CategoryTheory.Limits.isLimitOfCoconeUnopOfCone_lift 📋 Mathlib.CategoryTheory.Limits.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [CategoryTheory.Category.{v₂, u₂} J] (F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ) {c : CategoryTheory.Limits.Cone F} (hc : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.coconeUnopOfCone c)) (s : CategoryTheory.Limits.Cone F) : (CategoryTheory.Limits.isLimitOfCoconeUnopOfCone F hc).lift s = (hc.desc (CategoryTheory.Limits.coconeUnopOfCone s)).op
• 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.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.WithTerminal.isLimitEquiv_apply_lift_left 📋 Mathlib.CategoryTheory.WithTerminal.Cone
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type w} [CategoryTheory.Category.{w', w} J] {X : C} {K : CategoryTheory.Functor J (CategoryTheory.Over X)} {t : CategoryTheory.Limits.Cone K} (P : CategoryTheory.Limits.IsLimit (CategoryTheory.WithTerminal.coneEquiv.functor.obj t)) (s : CategoryTheory.Limits.Cone K) : ((CategoryTheory.WithTerminal.isLimitEquiv P).lift s).left = ((CategoryTheory.Limits.IsLimit.ofRightAdjoint CategoryTheory.WithTerminal.coneEquiv.toAdjunction P).lift s).left
• CategoryTheory.WithTerminal.isLimitEquiv_symm_apply_lift 📋 Mathlib.CategoryTheory.WithTerminal.Cone
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type w} [CategoryTheory.Category.{w', w} J] {X : C} {K : CategoryTheory.Functor J (CategoryTheory.Over X)} {t : CategoryTheory.Limits.Cone K} (t✝ : CategoryTheory.Limits.IsLimit t) (s : CategoryTheory.Limits.Cone (CategoryTheory.WithTerminal.liftFromOver.obj K)) : (CategoryTheory.WithTerminal.isLimitEquiv.symm t✝).lift s = ((CategoryTheory.WithTerminal.coneEquiv.symm.toAdjunction.homEquiv s t) (t✝.liftConeMorphism (CategoryTheory.WithTerminal.coneEquiv.inverse.obj s))).hom
• CategoryTheory.Limits.Types.binaryProductFunctor_obj_map 📋 Mathlib.CategoryTheory.Limits.Types.Products
  (X : Type u) {x✝ Y₂ : Type u} (f : x✝ ⟶ Y₂) : (CategoryTheory.Limits.Types.binaryProductFunctor.obj X).map f = (CategoryTheory.Limits.Types.binaryProductLimit X Y₂).lift (CategoryTheory.Limits.BinaryFan.mk (TypeCat.ofHom Prod.fst) (CategoryTheory.CategoryStruct.comp (TypeCat.ofHom Prod.snd) f))
• CategoryTheory.Limits.Types.binaryProductFunctor_map_app 📋 Mathlib.CategoryTheory.Limits.Types.Products
  {X₁ X₂ : Type u} (f : X₁ ⟶ X₂) (Y : Type u) : (CategoryTheory.Limits.Types.binaryProductFunctor.map f).app Y = CategoryTheory.Limits.BinaryFan.IsLimit.lift (CategoryTheory.Limits.Types.binaryProductLimit X₂ Y) (CategoryTheory.CategoryStruct.comp (TypeCat.ofHom Prod.fst) f) (TypeCat.ofHom Prod.snd)
• CategoryTheory.Limits.Types.binaryProductLimit_lift 📋 Mathlib.CategoryTheory.Limits.Types.Products
  (X Y : Type u) (s : CategoryTheory.Limits.BinaryFan X Y) : (CategoryTheory.Limits.Types.binaryProductLimit X Y).lift s = TypeCat.ofHom fun x => ((CategoryTheory.ConcreteCategory.hom s.fst) x, (CategoryTheory.ConcreteCategory.hom s.snd) x)
• CategoryTheory.MorphismProperty.limitsOfShape.mk 📋 Mathlib.CategoryTheory.MorphismProperty.Limits
  {C : Type u} [CategoryTheory.Category.{v, u} C] {W : CategoryTheory.MorphismProperty C} {J : Type u_1} [CategoryTheory.Category.{v_1, u_1} J] (X₁ X₂ : CategoryTheory.Functor J C) (c₁ : CategoryTheory.Limits.Cone X₁) (c₂ : CategoryTheory.Limits.Cone X₂) : ∀ (x : CategoryTheory.Limits.IsLimit c₁) (h₂ : CategoryTheory.Limits.IsLimit c₂) (f : X₁ ⟶ X₂), W.functorCategory J f → W.limitsOfShape J (h₂.lift { pt := c₁.pt, π := CategoryTheory.CategoryStruct.comp c₁.π f })
• CategoryTheory.CartesianMonoidalCategory.fullSubcategory_isTerminalTensorUnit_lift_hom 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {P : CategoryTheory.ObjectProperty C} [P.IsClosedUnderLimitsOfShape (CategoryTheory.Discrete PEmpty.{1})] [P.IsClosedUnderLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair)] (s : CategoryTheory.Limits.Cone (CategoryTheory.Functor.empty P.FullSubcategory)) : (CategoryTheory.SemiCartesianMonoidalCategory.isTerminalTensorUnit.lift s).hom = CategoryTheory.SemiCartesianMonoidalCategory.toUnit s.pt.obj
• CategoryTheory.CartesianMonoidalCategory.fullSubcategory_tensorProductIsBinaryProduct_lift_hom 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {P : CategoryTheory.ObjectProperty C} [P.IsClosedUnderLimitsOfShape (CategoryTheory.Discrete PEmpty.{1})] [P.IsClosedUnderLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair)] (X Y : P.FullSubcategory) (t : CategoryTheory.Limits.Cone (CategoryTheory.Limits.pair X Y)) : ((CategoryTheory.CartesianMonoidalCategory.tensorProductIsBinaryProduct X Y).lift t).hom = CategoryTheory.CartesianMonoidalCategory.lift (CategoryTheory.Limits.BinaryFan.fst t).hom (CategoryTheory.Limits.BinaryFan.snd t).hom
• AddCommGrpCat.HasLimit.productLimitCone_isLimit_lift 📋 Mathlib.Algebra.Category.Grp.Biproducts
  {J : Type w} (f : J → AddCommGrpCat) (s : CategoryTheory.Limits.Fan f) : (AddCommGrpCat.HasLimit.productLimitCone f).isLimit.lift s = AddCommGrpCat.HasLimit.lift f s
• AddCommGrpCat.binaryProductLimitCone_isLimit_lift 📋 Mathlib.Algebra.Category.Grp.Biproducts
  (G H : AddCommGrpCat) (t : CategoryTheory.Limits.Cone (CategoryTheory.Limits.pair G H)) : (G.binaryProductLimitCone H).isLimit.lift t = AddCommGrpCat.ofHom ((AddCommGrpCat.Hom.hom (CategoryTheory.Limits.BinaryFan.fst t)).prod (AddCommGrpCat.Hom.hom (CategoryTheory.Limits.BinaryFan.snd t)))
• CategoryTheory.ShortComplex.LeftHomologyData.wπ 📋 Mathlib.Algebra.Homology.ShortComplex.LeftHomology
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S : CategoryTheory.ShortComplex C} (self : S.LeftHomologyData) : CategoryTheory.CategoryStruct.comp (self.hi.lift (CategoryTheory.Limits.KernelFork.ofι S.f ⋯)) self.π = 0
• CategoryTheory.ShortComplex.LeftHomologyData.hπ 📋 Mathlib.Algebra.Homology.ShortComplex.LeftHomology
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S : CategoryTheory.ShortComplex C} (self : S.LeftHomologyData) : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ self.π ⋯)
• CategoryTheory.ShortComplex.LeftHomologyData.wπ_assoc 📋 Mathlib.Algebra.Homology.ShortComplex.LeftHomology
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S : CategoryTheory.ShortComplex C} (self : S.LeftHomologyData) {Z : C} (h : self.H ⟶ Z) : CategoryTheory.CategoryStruct.comp (self.hi.lift (CategoryTheory.Limits.KernelFork.ofι S.f ⋯)) (CategoryTheory.CategoryStruct.comp self.π h) = CategoryTheory.CategoryStruct.comp 0 h
• CategoryTheory.ShortComplex.LeftHomologyData.mk 📋 Mathlib.Algebra.Homology.ShortComplex.LeftHomology
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S : CategoryTheory.ShortComplex C} (K H : C) (i : K ⟶ S.X₂) (π : K ⟶ H) (wi : CategoryTheory.CategoryStruct.comp i S.g = 0) (hi : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι i wi)) (wπ : CategoryTheory.CategoryStruct.comp (hi.lift (CategoryTheory.Limits.KernelFork.ofι S.f ⋯)) π = 0) (hπ : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ π wπ)) : S.LeftHomologyData
• CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.f'_eq 📋 Mathlib.Algebra.Homology.ShortComplex.Abelian
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex C) {kf : CategoryTheory.Limits.KernelFork S.g} (hkf : CategoryTheory.Limits.IsLimit kf) : hkf.lift (CategoryTheory.Limits.KernelFork.ofι S.f ⋯) = CategoryTheory.CategoryStruct.comp S.toCycles (S.isoCyclesOfIsLimit hkf).inv
• CategoryTheory.Limits.desc_op_comp_opCoproductIsoProduct'_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {α : Type u_1} {Z : α → C} {c : CategoryTheory.Limits.Cofan Z} {f : CategoryTheory.Limits.Fan fun x => Opposite.op (Z x)} (hc : CategoryTheory.Limits.IsColimit c) (hf : CategoryTheory.Limits.IsLimit f) (c' : CategoryTheory.Limits.Cofan Z) : CategoryTheory.CategoryStruct.comp (hc.desc c').op (CategoryTheory.Limits.opCoproductIsoProduct' hc hf).hom = hf.lift c'.op
• CategoryTheory.Limits.opProductIsoCoproduct'_inv_comp_lift 📋 Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {α : Type u_1} {Z : α → C} {f : CategoryTheory.Limits.Fan Z} {c : CategoryTheory.Limits.Cofan fun x => Opposite.op (Z x)} (hf : CategoryTheory.Limits.IsLimit f) (hc : CategoryTheory.Limits.IsColimit c) (f' : CategoryTheory.Limits.Fan Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.opProductIsoCoproduct' hf hc).inv (hf.lift f').op = hc.desc f'.op
• CategoryTheory.Limits.ProductsFromFiniteCofiltered.liftToFinsetLimitCone_isLimit_lift 📋 Mathlib.CategoryTheory.Limits.Constructions.Filtered
  {C : Type u} [CategoryTheory.Category.{v, u} C] {α : Type w} [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasLimitsOfShape (Finset (CategoryTheory.Discrete α))ᵒᵖ C] (F : CategoryTheory.Functor (CategoryTheory.Discrete α) C) (s : CategoryTheory.Limits.Cone F) : (CategoryTheory.Limits.ProductsFromFiniteCofiltered.liftToFinsetLimitCone F).isLimit.lift s = CategoryTheory.Limits.limit.lift (CategoryTheory.Limits.ProductsFromFiniteCofiltered.liftToFinsetObj F) { pt := s.pt, π := { app := fun x => CategoryTheory.Limits.Pi.lift fun x_1 => s.π.app ↑x_1, naturality := ⋯ } }
• CategoryTheory.Functor.isLimitConeOfIsRightKanExtension_lift 📋 Mathlib.CategoryTheory.Functor.KanExtension.Basic
  {C : Type u_1} {H : Type u_3} {D : Type u_5} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_3, u_3} H] [CategoryTheory.Category.{v_5, u_5} D] (F' : CategoryTheory.Functor D H) {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H} (α : L.comp F' ⟶ F) [F'.IsRightKanExtension α] {c : CategoryTheory.Limits.Cone F} (hc : CategoryTheory.Limits.IsLimit c) (s : CategoryTheory.Limits.Cone F') : (F'.isLimitConeOfIsRightKanExtension α hc).lift s = hc.lift { pt := s.1, π := CategoryTheory.CategoryStruct.comp (L.whiskerLeft s.π) α }
• AddGrpCat.binaryProductLimitCone_isLimit_lift 📋 Mathlib.Algebra.Category.Grp.CartesianMonoidal
  (G H : AddGrpCat) (t : CategoryTheory.Limits.Cone (CategoryTheory.Limits.pair G H)) : (G.binaryProductLimitCone H).isLimit.lift t = AddGrpCat.ofHom ((AddGrpCat.Hom.hom (CategoryTheory.Limits.BinaryFan.fst t)).prod (AddGrpCat.Hom.hom (CategoryTheory.Limits.BinaryFan.snd t)))
• GrpCat.binaryProductLimitCone_isLimit_lift 📋 Mathlib.Algebra.Category.Grp.CartesianMonoidal
  (G H : GrpCat) (t : CategoryTheory.Limits.Cone (CategoryTheory.Limits.pair G H)) : (G.binaryProductLimitCone H).isLimit.lift t = GrpCat.ofHom ((GrpCat.Hom.hom (CategoryTheory.Limits.BinaryFan.fst t)).prod (GrpCat.Hom.hom (CategoryTheory.Limits.BinaryFan.snd t)))
• CommGrpCat.binaryProductLimitCone_isLimit_lift 📋 Mathlib.Algebra.Category.Grp.CartesianMonoidal
  (G H : CommGrpCat) (t : CategoryTheory.Limits.Cone (CategoryTheory.Limits.pair G H)) : (G.binaryProductLimitCone H).isLimit.lift t = CommGrpCat.ofHom ((CommGrpCat.Hom.hom (CategoryTheory.Limits.BinaryFan.fst t)).prod (CommGrpCat.Hom.hom (CategoryTheory.Limits.BinaryFan.snd t)))
• CategoryTheory.Limits.Multifork.IsLimit.mk_lift 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} {I : CategoryTheory.Limits.MulticospanIndex J C} (K : CategoryTheory.Limits.Multifork I) (lift : (E : CategoryTheory.Limits.Multifork I) → E.pt ⟶ K.pt) (fac : ∀ (E : CategoryTheory.Limits.Multifork I) (i : J.L), CategoryTheory.CategoryStruct.comp (lift E) (K.ι i) = E.ι i) (uniq : ∀ (E : CategoryTheory.Limits.Multifork I) (m : E.pt ⟶ K.pt), (∀ (i : J.L), CategoryTheory.CategoryStruct.comp m (K.ι i) = E.ι i) → m = lift E) (E : CategoryTheory.Limits.Multifork I) : (CategoryTheory.Limits.Multifork.IsLimit.mk K lift fac uniq).lift E = lift E
• ModuleCat.HasLimit.productLimitCone_isLimit_lift 📋 Mathlib.Algebra.Category.ModuleCat.Biproducts
  {R : Type u} [Ring R] {J : Type w} (f : J → ModuleCat R) (s : CategoryTheory.Limits.Fan f) : (ModuleCat.HasLimit.productLimitCone f).isLimit.lift s = ModuleCat.HasLimit.lift f s
• ModuleCat.binaryProductLimitCone_isLimit_lift 📋 Mathlib.Algebra.Category.ModuleCat.Biproducts
  {R : Type u} [Ring R] (M N : ModuleCat R) (s : CategoryTheory.Limits.Cone (CategoryTheory.Limits.pair M N)) : (M.binaryProductLimitCone N).isLimit.lift s = ModuleCat.ofHom ((ModuleCat.Hom.hom (s.π.app { as := CategoryTheory.Limits.WalkingPair.left })).prod (ModuleCat.Hom.hom (s.π.app { as := CategoryTheory.Limits.WalkingPair.right })))
• CategoryTheory.Comonad.beckEqualizer_lift 📋 Mathlib.CategoryTheory.Monad.Equalizer
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Comonad C} (X : T.Coalgebra) (s : CategoryTheory.Limits.Fork (T.map X.a) (T.δ.app X.A)) : (CategoryTheory.Comonad.beckEqualizer X).lift s = CategoryTheory.CategoryStruct.comp s.ι (T.ε.app X.A)
• CategoryTheory.Monad.ForgetCreatesLimits.conePoint_a 📋 Mathlib.CategoryTheory.Monad.Limits
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} {J : Type u} [CategoryTheory.Category.{v, u} J] (D : CategoryTheory.Functor J T.Algebra) (c : CategoryTheory.Limits.Cone (D.comp T.forget)) (t : CategoryTheory.Limits.IsLimit c) : (CategoryTheory.Monad.ForgetCreatesLimits.conePoint D c t).a = t.lift (CategoryTheory.Monad.ForgetCreatesLimits.newCone D c)
• CategoryTheory.Monad.ForgetCreatesLimits.liftedConeIsLimit_lift_f 📋 Mathlib.CategoryTheory.Monad.Limits
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} {J : Type u} [CategoryTheory.Category.{v, u} J] (D : CategoryTheory.Functor J T.Algebra) (c : CategoryTheory.Limits.Cone (D.comp T.forget)) (t : CategoryTheory.Limits.IsLimit c) (s : CategoryTheory.Limits.Cone D) : ((CategoryTheory.Monad.ForgetCreatesLimits.liftedConeIsLimit D c t).lift s).f = t.lift (T.forget.mapCone s)
• CategoryTheory.Comonad.ForgetCreatesLimits'.liftedConeIsLimit_lift_f 📋 Mathlib.CategoryTheory.Monad.Limits
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u} [CategoryTheory.Category.{v, u} J] {T : CategoryTheory.Comonad C} {D : CategoryTheory.Functor J T.Coalgebra} (c : CategoryTheory.Limits.Cone (D.comp T.forget)) (t : CategoryTheory.Limits.IsLimit c) [CategoryTheory.Limits.PreservesLimit (D.comp T.forget) T.toFunctor] [CategoryTheory.Limits.PreservesLimit ((D.comp T.forget).comp T.toFunctor) T.toFunctor] (s : CategoryTheory.Limits.Cone D) : ((CategoryTheory.Comonad.ForgetCreatesLimits'.liftedConeIsLimit c t).lift s).f = t.lift (T.forget.mapCone s)
• CategoryTheory.Comonad.ComonadicityInternal.comparisonAdjunction_counit_f 📋 Mathlib.CategoryTheory.Monad.Comonadicity
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₁, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} {adj : F ⊣ G} [∀ (A : adj.toComonad.Coalgebra), CategoryTheory.Limits.HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))] (A : adj.toComonad.Coalgebra) : ((CategoryTheory.Comonad.ComonadicityInternal.comparisonAdjunction adj).counit.app A).f = (CategoryTheory.Comonad.beckEqualizer A).lift (CategoryTheory.Comonad.ComonadicityInternal.counitFork A)
• HomologicalComplex.extend.leftHomologyData.cokernelCofork 📋 Mathlib.Algebra.Homology.Embedding.ExtendHomology
  {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{v_1, u_3} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] (K : HomologicalComplex C c) (e : c.Embedding c') {i j k : ι} {i' j' k' : ι'} (hj' : e.f j = j') (hi : c.prev j = i) (hi' : c'.prev j' = i') (hk : c.next j = k) (hk' : c'.next j' = k') (cone : CategoryTheory.Limits.KernelFork (K.d j k)) (hcone : CategoryTheory.Limits.IsLimit cone) (cocone : CategoryTheory.Limits.CokernelCofork (hcone.lift (CategoryTheory.Limits.KernelFork.ofι (K.d i j) ⋯))) : CategoryTheory.Limits.CokernelCofork ((HomologicalComplex.extend.leftHomologyData.isLimitKernelFork K e hj' hk hk' cone hcone).lift (CategoryTheory.Limits.KernelFork.ofι ((K.extend e).d i' j') ⋯))
• HomologicalComplex.extend.leftHomologyData.lift_d_comp_eq_zero_iff 📋 Mathlib.Algebra.Homology.Embedding.ExtendHomology
  {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{v_1, u_3} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] (K : HomologicalComplex C c) (e : c.Embedding c') {i j k : ι} {i' j' k' : ι'} (hj' : e.f j = j') (hi : c.prev j = i) (hi' : c'.prev j' = i') (hk : c.next j = k) (hk' : c'.next j' = k') (cone : CategoryTheory.Limits.KernelFork (K.d j k)) (hcone : CategoryTheory.Limits.IsLimit cone) ⦃W : C⦄ (φ : cone.pt ⟶ W) : CategoryTheory.CategoryStruct.comp (hcone.lift (CategoryTheory.Limits.KernelFork.ofι (K.d i j) ⋯)) φ = 0 ↔ CategoryTheory.CategoryStruct.comp ((HomologicalComplex.extend.leftHomologyData.isLimitKernelFork K e hj' hk hk' cone hcone).lift (CategoryTheory.Limits.KernelFork.ofι ((K.extend e).d i' j') ⋯)) φ = 0
• HomologicalComplex.extend.leftHomologyData.isColimitCokernelCofork 📋 Mathlib.Algebra.Homology.Embedding.ExtendHomology
  {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{v_1, u_3} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] (K : HomologicalComplex C c) (e : c.Embedding c') {i j k : ι} {i' j' k' : ι'} (hj' : e.f j = j') (hi : c.prev j = i) (hi' : c'.prev j' = i') (hk : c.next j = k) (hk' : c'.next j' = k') (cone : CategoryTheory.Limits.KernelFork (K.d j k)) (hcone : CategoryTheory.Limits.IsLimit cone) (cocone : CategoryTheory.Limits.CokernelCofork (hcone.lift (CategoryTheory.Limits.KernelFork.ofι (K.d i j) ⋯))) (hcocone : CategoryTheory.Limits.IsColimit cocone) : CategoryTheory.Limits.IsColimit (HomologicalComplex.extend.leftHomologyData.cokernelCofork K e hj' hi hi' hk hk' cone hcone cocone)
• CategoryTheory.Limits.coneOfConeUncurry_π_app 📋 Mathlib.CategoryTheory.Limits.Fubini
  {J : Type u_1} {K : Type u_2} [CategoryTheory.Category.{v_1, u_1} J] [CategoryTheory.Category.{v_2, u_2} K] {C : Type u_3} [CategoryTheory.Category.{v_3, u_3} C] {F : CategoryTheory.Functor J (CategoryTheory.Functor K C)} {D : CategoryTheory.Limits.DiagramOfCones F} (Q : (j : J) → CategoryTheory.Limits.IsLimit (D.obj j)) (c : CategoryTheory.Limits.Cone (CategoryTheory.Functor.uncurry.obj F)) (j : J) : (CategoryTheory.Limits.coneOfConeUncurry Q c).π.app j = (Q j).lift { pt := c.pt, π := { app := fun k => c.π.app (j, k), naturality := ⋯ } }
• CategoryTheory.Limits.coneOfConeCurry_π_app 📋 Mathlib.CategoryTheory.Limits.Fubini
  {J : Type u_1} {K : Type u_2} [CategoryTheory.Category.{v_1, u_1} J] [CategoryTheory.Category.{v_2, u_2} K] {C : Type u_3} [CategoryTheory.Category.{v_3, u_3} C] (G : CategoryTheory.Functor (J × K) C) {D : CategoryTheory.Limits.DiagramOfCones (CategoryTheory.Functor.curry.obj G)} (Q : (j : J) → CategoryTheory.Limits.IsLimit (D.obj j)) (c : CategoryTheory.Limits.Cone G) (j : J) : (CategoryTheory.Limits.coneOfConeCurry G Q c).π.app j = (Q j).lift { pt := c.pt, π := { app := fun k => c.π.app (j, k), naturality := ⋯ } }
• CategoryTheory.Limits.CompleteLattice.finiteLimitCone_isLimit_lift 📋 Mathlib.CategoryTheory.Limits.Lattice
  {α : Type u} {J : Type w} [CategoryTheory.SmallCategory J] [CategoryTheory.FinCategory J] [SemilatticeInf α] [OrderTop α] (F : CategoryTheory.Functor J α) (s : CategoryTheory.Limits.Cone F) : (CategoryTheory.Limits.CompleteLattice.finiteLimitCone F).isLimit.lift s = CategoryTheory.homOfLE ⋯
• CategoryTheory.Limits.CompleteLattice.limitCone_isLimit_lift 📋 Mathlib.CategoryTheory.Limits.Lattice
  {α : Type u} [CompleteLattice α] {J : Type w} [CategoryTheory.Category.{w', w} J] (F : CategoryTheory.Functor J α) (s : CategoryTheory.Limits.Cone F) : (CategoryTheory.Limits.CompleteLattice.limitCone F).isLimit.lift s = CategoryTheory.homOfLE ⋯
• CategoryTheory.Limits.IsLimit.pullbackConeEquivBinaryFanFunctor_lift_left 📋 Mathlib.CategoryTheory.Limits.Constructions.Over.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : Y ⟶ X} {g : Z ⟶ X} {c : CategoryTheory.Limits.PullbackCone f g} (hc : CategoryTheory.Limits.IsLimit c) (s : CategoryTheory.Limits.BinaryFan (CategoryTheory.Over.mk f) (CategoryTheory.Over.mk g)) : (hc.pullbackConeEquivBinaryFanFunctor.lift s).left = hc.lift (CategoryTheory.Limits.PullbackCone.mk (CategoryTheory.Over.Hom.left s.fst) (CategoryTheory.Over.Hom.left s.snd) ⋯)
• CategoryTheory.StructuredArrow.isClosedUnderLimitsOfShape 📋 Mathlib.CategoryTheory.Limits.MorphismProperty
  {T : Type u_1} [CategoryTheory.Category.{v_1, u_1} T] {A : Type u_2} [CategoryTheory.Category.{v_2, u_2} A] {L : CategoryTheory.Functor A T} {J : Type u_3} [CategoryTheory.Category.{v_3, u_3} J] {P : CategoryTheory.MorphismProperty T} [P.RespectsIso] [CategoryTheory.Limits.PreservesLimitsOfShape J L] [CategoryTheory.Limits.HasLimitsOfShape J A] (c : (D : CategoryTheory.Functor J T) → [CategoryTheory.Limits.HasLimit D] → CategoryTheory.Limits.Cone D) (hc : (D : CategoryTheory.Functor J T) → [inst : CategoryTheory.Limits.HasLimit D] → CategoryTheory.Limits.IsLimit (c D)) (H : ∀ (D : CategoryTheory.Functor J T) [inst : CategoryTheory.Limits.HasLimit D] {X : T} (s : (CategoryTheory.Functor.const J).obj X ⟶ D), (∀ (j : J), P (s.app j)) → P ((hc D).lift { pt := X, π := s })) (X : T) : (CategoryTheory.MorphismProperty.structuredArrowObj L P).IsClosedUnderLimitsOfShape J
• CategoryTheory.Limits.PullbackCone.combine_pt_map 📋 Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Pullbacks
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F G H : CategoryTheory.Functor D C} (f : F ⟶ H) (g : G ⟶ H) (c : (X : D) → CategoryTheory.Limits.PullbackCone (f.app X) (g.app X)) (hc : (X : D) → CategoryTheory.Limits.IsLimit (c X)) {X Y : D} (h : X ⟶ Y) : (CategoryTheory.Limits.PullbackCone.combine f g c hc).pt.map h = (hc Y).lift { pt := (c X).pt, π := CategoryTheory.CategoryStruct.comp (c X).π (CategoryTheory.Limits.cospanHomMk (H.map h) (F.map h) (G.map h) ⋯ ⋯) }
• CategoryTheory.Limits.PullbackCone.combine_π_app 📋 Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Pullbacks
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F G H : CategoryTheory.Functor D C} (f : F ⟶ H) (g : G ⟶ H) (c : (X : D) → CategoryTheory.Limits.PullbackCone (f.app X) (g.app X)) (hc : (X : D) → CategoryTheory.Limits.IsLimit (c X)) (j : CategoryTheory.Limits.WalkingCospan) : (CategoryTheory.Limits.PullbackCone.combine f g c hc).π.app j = Option.rec (CategoryTheory.CategoryStruct.comp { app := fun X => (c X).fst, naturality := ⋯ } f) (fun val => CategoryTheory.Limits.WalkingPair.rec { app := fun X => (c X).fst, naturality := ⋯ } { app := fun X => (c X).snd, naturality := ⋯ } val) j
• CategoryTheory.Limits.FormalCoproduct.homPullbackEquiv_symm_apply_φ 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : CategoryTheory.Limits.FormalCoproduct C} (f : X ⟶ Z) (g : Y ⟶ Z) (pb : (i : Function.Pullback f.f g.f) → CategoryTheory.Limits.PullbackCone (CategoryTheory.CategoryStruct.comp (f.φ (↑i).1) (CategoryTheory.eqToHom ⋯)) (g.φ (↑i).2)) (hpb : (i : Function.Pullback f.f g.f) → CategoryTheory.Limits.IsLimit (pb i)) (T : CategoryTheory.Limits.FormalCoproduct C) (s : { p // CategoryTheory.CategoryStruct.comp p.1 f = CategoryTheory.CategoryStruct.comp p.2 g }) (i : T.I) : ((CategoryTheory.Limits.FormalCoproduct.homPullbackEquiv f g pb hpb T).symm s).φ i = (hpb ⟨((↑s).1.f i, (↑s).2.f i), ⋯⟩).lift (CategoryTheory.Limits.PullbackCone.mk ((↑s).1.φ i) ((↑s).2.φ i) ⋯)
• CategoryTheory.FunctorToTypes.binaryProductLimit_lift 📋 Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes
  {C : Type u} [CategoryTheory.Category.{v, u} C] (F G : CategoryTheory.Functor C (Type w)) (s : CategoryTheory.Limits.BinaryFan F G) : (CategoryTheory.FunctorToTypes.binaryProductLimit F G).lift s = CategoryTheory.FunctorToTypes.prod.lift s.fst s.snd
• CategoryTheory.Mon.limitConeIsLimit_lift_hom 📋 Mathlib.CategoryTheory.Monoidal.Internal.Limits
  {J : Type w} [CategoryTheory.Category.{v_1, w} J] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (F : CategoryTheory.Functor J (CategoryTheory.Mon C)) (c : CategoryTheory.Limits.Cone (F.comp (CategoryTheory.Mon.forget C))) (hc : CategoryTheory.Limits.IsLimit c) (s : CategoryTheory.Limits.Cone F) : ((CategoryTheory.Mon.limitConeIsLimit F c hc).lift s).hom = hc.lift ((CategoryTheory.Mon.forget C).mapCone s)
• CategoryTheory.Mon.limit_mon_one 📋 Mathlib.CategoryTheory.Monoidal.Internal.Limits
  {J : Type w} [CategoryTheory.Category.{v_1, w} J] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (F : CategoryTheory.Functor J (CategoryTheory.Mon C)) (c : CategoryTheory.Limits.Cone (F.comp (CategoryTheory.Mon.forget C))) (hc : CategoryTheory.Limits.IsLimit c) : CategoryTheory.MonObj.one = hc.lift { pt := CategoryTheory.MonoidalCategoryStruct.tensorUnit C, π := { app := fun X => CategoryTheory.MonObj.one, naturality := ⋯ } }
• CategoryTheory.Mon.limit_mon_mul 📋 Mathlib.CategoryTheory.Monoidal.Internal.Limits
  {J : Type w} [CategoryTheory.Category.{v_1, w} J] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (F : CategoryTheory.Functor J (CategoryTheory.Mon C)) (c : CategoryTheory.Limits.Cone (F.comp (CategoryTheory.Mon.forget C))) (hc : CategoryTheory.Limits.IsLimit c) : CategoryTheory.MonObj.mul = hc.lift { pt := CategoryTheory.MonoidalCategoryStruct.tensorObj c.1 c.1, π := { app := fun X => CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (c.π.app X) (c.π.app X)) CategoryTheory.MonObj.mul, naturality := ⋯ } }
• CompHausLike.pullback.isLimit_lift 📋 Mathlib.Topology.Category.CompHausLike.Limits
  {P : TopCat → Prop} {X Y B : CompHausLike P} (f : X ⟶ B) (g : Y ⟶ B) [CompHausLike.HasExplicitPullback f g] (s : CategoryTheory.Limits.PullbackCone f g) : (CompHausLike.pullback.isLimit f g).lift s = CompHausLike.pullback.lift f g s.fst s.snd ⋯
• Profinite.isIso_asLimitCone_lift 📋 Mathlib.Topology.Category.Profinite.AsLimit
  (X : Profinite) : CategoryTheory.IsIso ((Profinite.limitConeIsLimit X.diagram).lift X.asLimitCone)
• Condensed.isoFinYoneda_inv_app_hom_apply 📋 Mathlib.Condensed.Discrete.Colimit
  (F : CategoryTheory.Functor Profiniteᵒᵖ (Type (u + 1))) [CategoryTheory.Limits.PreservesFiniteProducts F] (X : FintypeCatᵒᵖ) (a✝ : (CategoryTheory.Limits.Types.productLimitCone fun x => F.obj (Opposite.op (Profinite.of PUnit.{u + 1}))).cone.pt) : (CategoryTheory.ConcreteCategory.hom ((Condensed.isoFinYoneda F).inv.app X)) a✝ = (CategoryTheory.CategoryStruct.id (F.obj (Opposite.op (Condensed.fintypeCatAsCofan (Profinite.of (Opposite.unop X).obj)).pt))).hom' ((((CategoryTheory.Limits.IsLimit.postcomposeHomEquiv (CategoryTheory.Discrete.natIso fun j => CategoryTheory.Iso.refl (F.obj (Opposite.op (Profinite.of PUnit.{u + 1})))) (F.mapCone (CategoryTheory.Limits.Fan.mk (Opposite.op (Condensed.fintypeCatAsCofan (Profinite.of (Opposite.unop X).obj)).pt) fun a => ((Condensed.fintypeCatAsCofan (Profinite.of (Opposite.unop X).obj)).inj a).op))).symm (CategoryTheory.Limits.isLimitOfPreserves F (CategoryTheory.Limits.Cofan.IsColimit.op (Condensed.fintypeCatAsCofanIsColimit (Profinite.of (Opposite.unop X).obj))))).lift (CategoryTheory.Limits.Types.productLimitCone fun x => F.obj (Opposite.op (Profinite.of PUnit.{u + 1}))).cone).hom' a✝)
• LightCondensed.isoFinYoneda_inv_app_hom_apply 📋 Mathlib.Condensed.Discrete.Colimit
  (F : CategoryTheory.Functor LightProfiniteᵒᵖ (Type u)) [CategoryTheory.Limits.PreservesFiniteProducts F] (X : FintypeCatᵒᵖ) (a✝ : (CategoryTheory.Limits.Types.productLimitCone fun x => F.obj (Opposite.op (LightProfinite.of PUnit.{u + 1}))).cone.pt) : (CategoryTheory.ConcreteCategory.hom ((LightCondensed.isoFinYoneda F).inv.app X)) a✝ = (CategoryTheory.CategoryStruct.id (F.obj (Opposite.op (LightCondensed.fintypeCatAsCofan (LightProfinite.of (Opposite.unop X).obj)).pt))).hom' ((((CategoryTheory.Limits.IsLimit.postcomposeHomEquiv (CategoryTheory.Discrete.natIso fun j => CategoryTheory.Iso.refl (F.obj (Opposite.op (LightProfinite.of PUnit.{u + 1})))) (F.mapCone (CategoryTheory.Limits.Fan.mk (Opposite.op (LightCondensed.fintypeCatAsCofan (LightProfinite.of (Opposite.unop X).obj)).pt) fun a => ((LightCondensed.fintypeCatAsCofan (LightProfinite.of (Opposite.unop X).obj)).inj a).op))).symm (CategoryTheory.Limits.isLimitOfPreserves F (CategoryTheory.Limits.Cofan.IsColimit.op (LightCondensed.fintypeCatAsCofanIsColimit (LightProfinite.of (Opposite.unop X).obj))))).lift (CategoryTheory.Limits.Types.productLimitCone fun x => F.obj (Opposite.op (LightProfinite.of PUnit.{u + 1}))).cone).hom' a✝)
• Profinite.isIso_indexCone_lift 📋 Mathlib.Topology.Category.Profinite.Product
  {ι : Type u} {X : ι → Type} [(i : ι) → TopologicalSpace (X i)] {C : Set ((i : ι) → X i)} [∀ (i : ι), T2Space (X i)] [∀ (i : ι), TotallyDisconnectedSpace (X i)] (hC : IsCompact C) : CategoryTheory.IsIso ((Profinite.limitConeIsLimit (Profinite.indexFunctor hC)).lift (Profinite.indexCone hC))

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