Loogle!

Result

Found 182 declarations mentioning CategoryTheory.Discrete.as.

• CategoryTheory.Discrete.as 📋 Mathlib.CategoryTheory.Discrete.Basic
  {α : Type u₁} (self : CategoryTheory.Discrete α) : α
• CategoryTheory.Discrete.as_bijective 📋 Mathlib.CategoryTheory.Discrete.Basic
  {α : Type u_1} : Function.Bijective CategoryTheory.Discrete.as
• CategoryTheory.Discrete.mk_as 📋 Mathlib.CategoryTheory.Discrete.Basic
  {α : Type u₁} (X : CategoryTheory.Discrete α) : { as := X.as } = X
• CategoryTheory.Discrete.ext 📋 Mathlib.CategoryTheory.Discrete.Basic
  {α : Type u₁} {x y : CategoryTheory.Discrete α} (as : x.as = y.as) : x = y
• CategoryTheory.Discrete.ext_iff 📋 Mathlib.CategoryTheory.Discrete.Basic
  {α : Type u₁} {x y : CategoryTheory.Discrete α} : x = y ↔ x.as = y.as
• CategoryTheory.Discrete.eqToIso 📋 Mathlib.CategoryTheory.Discrete.Basic
  {α : Type u₁} {X Y : CategoryTheory.Discrete α} (h : X.as = Y.as) : X ≅ Y
• CategoryTheory.Discrete.eqToHom 📋 Mathlib.CategoryTheory.Discrete.Basic
  {α : Type u₁} {X Y : CategoryTheory.Discrete α} (h : X.as = Y.as) : X ⟶ Y
• CategoryTheory.Discrete.eq_of_hom 📋 Mathlib.CategoryTheory.Discrete.Basic
  {α : Type u₁} {X Y : CategoryTheory.Discrete α} (i : X ⟶ Y) : X.as = Y.as
• CategoryTheory.Discrete.functor_obj_eq_as 📋 Mathlib.CategoryTheory.Discrete.Basic
  {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {I : Type u₁} (F : I → C) (X : CategoryTheory.Discrete I) : (CategoryTheory.Discrete.functor F).obj X = F X.as
• CategoryTheory.discreteEquiv_apply 📋 Mathlib.CategoryTheory.Discrete.Basic
  {α : Type u₁} (self : CategoryTheory.Discrete α) : CategoryTheory.discreteEquiv self = self.as
• CategoryTheory.Discrete.id_def 📋 Mathlib.CategoryTheory.Discrete.Basic
  {α : Type u₁} (X : CategoryTheory.Discrete α) : { eq := ⋯ } = CategoryTheory.CategoryStruct.id X
• CategoryTheory.discreteEquiv_symm_apply_as 📋 Mathlib.CategoryTheory.Discrete.Basic
  {α : Type u₁} (as : α) : (CategoryTheory.discreteEquiv.symm as).as = as
• CategoryTheory.Discrete.opposite_functor_obj_as 📋 Mathlib.CategoryTheory.Discrete.Basic
  (α : Type u₁) (X : (CategoryTheory.Discrete α)ᵒᵖ) : ((CategoryTheory.Discrete.opposite α).functor.obj X).as = (Opposite.unop X).as
• CategoryTheory.Discrete.equivOfEquivalence_apply 📋 Mathlib.CategoryTheory.Discrete.Basic
  {α : Type u₁} {β : Type u₂} (h : CategoryTheory.Discrete α ≌ CategoryTheory.Discrete β) (a✝ : α) : (CategoryTheory.Discrete.equivOfEquivalence h) a✝ = (CategoryTheory.Discrete.as ∘ h.functor.obj ∘ CategoryTheory.Discrete.mk) a✝
• CategoryTheory.Discrete.equivOfEquivalence_symm_apply 📋 Mathlib.CategoryTheory.Discrete.Basic
  {α : Type u₁} {β : Type u₂} (h : CategoryTheory.Discrete α ≌ CategoryTheory.Discrete β) (a✝ : β) : (CategoryTheory.Discrete.equivOfEquivalence h).symm a✝ = (CategoryTheory.Discrete.as ∘ h.inverse.obj ∘ CategoryTheory.Discrete.mk) a✝
• CategoryTheory.Discrete.functor_map 📋 Mathlib.CategoryTheory.Discrete.Basic
  {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {I : Type u₁} (F : I → C) {i : CategoryTheory.Discrete I} (f : i ⟶ i) : (CategoryTheory.Discrete.functor F).map f = CategoryTheory.CategoryStruct.id (F i.as)
• CategoryTheory.piEquivalenceFunctorDiscrete_functor_map 📋 Mathlib.CategoryTheory.Discrete.Basic
  (J : Type u₂) (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] {X✝ Y✝ : J → C} (f : X✝ ⟶ Y✝) : (CategoryTheory.piEquivalenceFunctorDiscrete J C).functor.map f = CategoryTheory.Discrete.natTrans fun j => f j.as
• CategoryTheory.Discrete.compNatIsoDiscrete_hom_app 📋 Mathlib.CategoryTheory.Discrete.Basic
  {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {I : Type u₁} {D : Type u₃} [CategoryTheory.Category.{v₃, u₃} D] (F : I → C) (G : CategoryTheory.Functor C D) (X : CategoryTheory.Discrete I) : (CategoryTheory.Discrete.compNatIsoDiscrete F G).hom.app X = CategoryTheory.CategoryStruct.id (G.obj (F X.as))
• CategoryTheory.Discrete.compNatIsoDiscrete_inv_app 📋 Mathlib.CategoryTheory.Discrete.Basic
  {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {I : Type u₁} {D : Type u₃} [CategoryTheory.Category.{v₃, u₃} D] (F : I → C) (G : CategoryTheory.Functor C D) (X : CategoryTheory.Discrete I) : (CategoryTheory.Discrete.compNatIsoDiscrete F G).inv.app X = CategoryTheory.CategoryStruct.id (G.obj (F X.as))
• CategoryTheory.Discrete.functorComp_hom_app 📋 Mathlib.CategoryTheory.Discrete.Basic
  {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {I : Type u₁} {J : Type u₁'} (f : J → C) (g : I → J) (X : CategoryTheory.Discrete I) : (CategoryTheory.Discrete.functorComp f g).hom.app X = CategoryTheory.CategoryStruct.id (f (g X.as))
• CategoryTheory.Discrete.functorComp_inv_app 📋 Mathlib.CategoryTheory.Discrete.Basic
  {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {I : Type u₁} {J : Type u₁'} (f : J → C) (g : I → J) (X : CategoryTheory.Discrete I) : (CategoryTheory.Discrete.functorComp f g).inv.app X = CategoryTheory.CategoryStruct.id (f (g X.as))
• CategoryTheory.piEquivalenceFunctorDiscrete_counitIso 📋 Mathlib.CategoryTheory.Discrete.Basic
  (J : Type u₂) (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] : (CategoryTheory.piEquivalenceFunctorDiscrete J C).counitIso = CategoryTheory.NatIso.ofComponents (fun F => CategoryTheory.NatIso.ofComponents (fun x => CategoryTheory.Iso.refl ((({ obj := fun F j => F.obj { as := j }, map := fun {X Y} f j => f.app { as := j }, map_id := ⋯, map_comp := ⋯ }.comp { obj := fun F => CategoryTheory.Discrete.functor F, map := fun {X Y} f => CategoryTheory.Discrete.natTrans fun j => f j.as, map_id := ⋯, map_comp := ⋯ }).obj F).obj x)) ⋯) ⋯
• CategoryTheory.Limits.Cofan.mk_ι_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {f : β → C} (P : C) (p : (b : β) → f b ⟶ P) (X : CategoryTheory.Discrete β) : (CategoryTheory.Limits.Cofan.mk P p).ι.app X = p X.as
• CategoryTheory.Limits.Fan.mk_π_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {f : β → C} (P : C) (p : (b : β) → P ⟶ f b) (X : CategoryTheory.Discrete β) : (CategoryTheory.Limits.Fan.mk P p).π.app X = p X.as
• CategoryTheory.Limits.Pi.cone_π 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {α : Type w₂} {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.Functor (CategoryTheory.Discrete α) C) [CategoryTheory.Limits.HasProduct fun j => X.obj { as := j }] : (CategoryTheory.Limits.Pi.cone X).π = CategoryTheory.Discrete.natTrans fun x => CategoryTheory.Limits.Pi.π (fun j => X.obj { as := j }) x.as
• CategoryTheory.Limits.Sigma.cocone_ι 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {α : Type w₂} {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.Functor (CategoryTheory.Discrete α) C) [CategoryTheory.Limits.HasCoproduct fun j => X.obj { as := j }] : (CategoryTheory.Limits.Sigma.cocone X).ι = CategoryTheory.Discrete.natTrans fun x => CategoryTheory.Limits.Sigma.ι (fun j => X.obj { as := j }) x.as
• CategoryTheory.Functor.star_obj_as 📋 Mathlib.CategoryTheory.PUnit
  (C : Type u) [CategoryTheory.Category.{v, u} C] (x✝ : C) : ((CategoryTheory.Functor.star C).obj x✝).as = PUnit.unit
• CategoryTheory.Comma.costructuredArrowSndInclusion_obj_right_as 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.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) (b : B) (X : CategoryTheory.CostructuredArrow L (R.obj b)) : ((CategoryTheory.Comma.costructuredArrowSndInclusion L R b).obj X).right.as = PUnit.unit
• CategoryTheory.StructuredArrow.preEquivalenceFunctor_obj_left_as 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D) {G : CategoryTheory.Functor D E} {e : E} (f : CategoryTheory.StructuredArrow e G) (g : CategoryTheory.StructuredArrow f (CategoryTheory.StructuredArrow.pre e F G)) : ((CategoryTheory.StructuredArrow.preEquivalenceFunctor F f).obj g).left.as = PUnit.unit
• CategoryTheory.CostructuredArrow.preEquivalence.functor_obj_right_as 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D) {G : CategoryTheory.Functor D E} {e : E} (f : CategoryTheory.CostructuredArrow G e) (g : CategoryTheory.CostructuredArrow (CategoryTheory.CostructuredArrow.pre F G e) f) : ((CategoryTheory.CostructuredArrow.preEquivalence.functor F f).obj g).right.as = PUnit.unit
• CategoryTheory.StructuredArrow.preEquivalenceInverse_obj_left_as 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D) {G : CategoryTheory.Functor D E} {e : E} (f : CategoryTheory.StructuredArrow e G) (g : CategoryTheory.StructuredArrow f.right F) : ((CategoryTheory.StructuredArrow.preEquivalenceInverse F f).obj g).left.as = PUnit.unit
• CategoryTheory.CostructuredArrow.preEquivalence.inverse_obj_right_as 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D) {G : CategoryTheory.Functor D E} {e : E} (f : CategoryTheory.CostructuredArrow G e) (g : CategoryTheory.CostructuredArrow F f.left) : ((CategoryTheory.CostructuredArrow.preEquivalence.inverse F f).obj g).right.as = PUnit.unit
• CategoryTheory.StructuredArrow.preEquivalenceInverse_obj_right_left_as 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D) {G : CategoryTheory.Functor D E} {e : E} (f : CategoryTheory.StructuredArrow e G) (g : CategoryTheory.StructuredArrow f.right F) : ((CategoryTheory.StructuredArrow.preEquivalenceInverse F f).obj g).right.left.as = PUnit.unit
• CategoryTheory.CostructuredArrow.preEquivalence.inverse_obj_left_right_as 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D) {G : CategoryTheory.Functor D E} {e : E} (f : CategoryTheory.CostructuredArrow G e) (g : CategoryTheory.CostructuredArrow F f.left) : ((CategoryTheory.CostructuredArrow.preEquivalence.inverse F f).obj g).left.right.as = PUnit.unit
• CategoryTheory.CostructuredArrow.ofDiagEquivalence.functor_obj_right_as 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] (X : T × T) (Y : CategoryTheory.CostructuredArrow (CategoryTheory.Functor.diag T) X) : ((CategoryTheory.CostructuredArrow.ofDiagEquivalence.functor X).obj Y).right.as = PUnit.unit
• CategoryTheory.StructuredArrow.ofDiagEquivalence.functor_obj_left_as 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] (X : T × T) (Y : CategoryTheory.StructuredArrow X (CategoryTheory.Functor.diag T)) : ((CategoryTheory.StructuredArrow.ofDiagEquivalence.functor X).obj Y).left.as = PUnit.unit
• CategoryTheory.CostructuredArrow.ofDiagEquivalence.inverse_obj_right_as 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] (X : T × T) (Y : CategoryTheory.CostructuredArrow (CategoryTheory.Over.forget X.1) X.2) : ((CategoryTheory.CostructuredArrow.ofDiagEquivalence.inverse X).obj Y).right.as = PUnit.unit
• CategoryTheory.StructuredArrow.ofDiagEquivalence.inverse_obj_left_as 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] (X : T × T) (Y : CategoryTheory.StructuredArrow X.2 (CategoryTheory.Under.forget X.1)) : ((CategoryTheory.StructuredArrow.ofDiagEquivalence.inverse X).obj Y).left.as = PUnit.unit
• CategoryTheory.CostructuredArrow.ofDiagEquivalence.functor_obj_left_right_as 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] (X : T × T) (Y : CategoryTheory.CostructuredArrow (CategoryTheory.Functor.diag T) X) : ((CategoryTheory.CostructuredArrow.ofDiagEquivalence.functor X).obj Y).left.right.as = PUnit.unit
• CategoryTheory.StructuredArrow.ofDiagEquivalence.functor_obj_right_left_as 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] (X : T × T) (Y : CategoryTheory.StructuredArrow X (CategoryTheory.Functor.diag T)) : ((CategoryTheory.StructuredArrow.ofDiagEquivalence.functor X).obj Y).right.left.as = PUnit.unit
• CategoryTheory.CostructuredArrow.ofCostructuredArrowProjEquivalence.functor_obj_right_as 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor T D) (Y : D) (X : T) (Y✝ : CategoryTheory.CostructuredArrow (CategoryTheory.CostructuredArrow.proj F Y) X) : ((CategoryTheory.CostructuredArrow.ofCostructuredArrowProjEquivalence.functor F Y X).obj Y✝).right.as = PUnit.unit
• CategoryTheory.CostructuredArrow.ofCostructuredArrowProjEquivalence.inverse_obj_right_as 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor T D) (Y : D) (X : T) (Y✝ : CategoryTheory.CostructuredArrow ((CategoryTheory.Over.forget X).comp F) Y) : ((CategoryTheory.CostructuredArrow.ofCostructuredArrowProjEquivalence.inverse F Y X).obj Y✝).right.as = PUnit.unit
• CategoryTheory.StructuredArrow.ofStructuredArrowProjEquivalence.functor_obj_left_as 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor D T) (Y : T) (X : D) (Y✝ : CategoryTheory.StructuredArrow X (CategoryTheory.StructuredArrow.proj Y F)) : ((CategoryTheory.StructuredArrow.ofStructuredArrowProjEquivalence.functor F Y X).obj Y✝).left.as = PUnit.unit
• CategoryTheory.StructuredArrow.ofStructuredArrowProjEquivalence.inverse_obj_left_as 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor D T) (Y : T) (X : D) (Y✝ : CategoryTheory.StructuredArrow Y ((CategoryTheory.Under.forget X).comp F)) : ((CategoryTheory.StructuredArrow.ofStructuredArrowProjEquivalence.inverse F Y X).obj Y✝).left.as = PUnit.unit
• CategoryTheory.CostructuredArrow.ofCostructuredArrowProjEquivalence.inverse_obj_left_right_as 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor T D) (Y : D) (X : T) (Y✝ : CategoryTheory.CostructuredArrow ((CategoryTheory.Over.forget X).comp F) Y) : ((CategoryTheory.CostructuredArrow.ofCostructuredArrowProjEquivalence.inverse F Y X).obj Y✝).left.right.as = PUnit.unit
• CategoryTheory.StructuredArrow.ofStructuredArrowProjEquivalence.inverse_obj_right_left_as 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor D T) (Y : T) (X : D) (Y✝ : CategoryTheory.StructuredArrow Y ((CategoryTheory.Under.forget X).comp F)) : ((CategoryTheory.StructuredArrow.ofStructuredArrowProjEquivalence.inverse F Y X).obj Y✝).right.left.as = PUnit.unit
• CategoryTheory.CostructuredArrow.ofCostructuredArrowProjEquivalence.functor_obj_left_right_as 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor T D) (Y : D) (X : T) (Y✝ : CategoryTheory.CostructuredArrow (CategoryTheory.CostructuredArrow.proj F Y) X) : ((CategoryTheory.CostructuredArrow.ofCostructuredArrowProjEquivalence.functor F Y X).obj Y✝).left.right.as = PUnit.unit
• CategoryTheory.StructuredArrow.ofStructuredArrowProjEquivalence.functor_obj_right_left_as 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor D T) (Y : T) (X : D) (Y✝ : CategoryTheory.StructuredArrow X (CategoryTheory.StructuredArrow.proj Y F)) : ((CategoryTheory.StructuredArrow.ofStructuredArrowProjEquivalence.functor F Y X).obj Y✝).right.left.as = PUnit.unit
• 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.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.Bicone.toCocone_ι_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
  {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {F : J → C} (B : CategoryTheory.Limits.Bicone F) (j : CategoryTheory.Discrete J) : B.toCocone.ι.app j = B.ι j.as
• CategoryTheory.Limits.Bicone.toCone_π_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
  {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {F : J → C} (B : CategoryTheory.Limits.Bicone F) (j : CategoryTheory.Discrete J) : B.toCone.π.app j = B.π j.as
• CategoryTheory.Discrete.addMonoidal_tensorUnit_as 📋 Mathlib.CategoryTheory.Monoidal.Discrete
  (M : Type u) [AddMonoid M] : (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Discrete M)).as = 0
• CategoryTheory.Discrete.monoidal_tensorUnit_as 📋 Mathlib.CategoryTheory.Monoidal.Discrete
  (M : Type u) [Monoid M] : (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Discrete M)).as = 1
• CategoryTheory.Discrete.addMonoidal_tensorObj_as 📋 Mathlib.CategoryTheory.Monoidal.Discrete
  (M : Type u) [AddMonoid M] (X Y : CategoryTheory.Discrete M) : (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).as = X.as + Y.as
• CategoryTheory.Discrete.monoidal_tensorObj_as 📋 Mathlib.CategoryTheory.Monoidal.Discrete
  (M : Type u) [Monoid M] (X Y : CategoryTheory.Discrete M) : (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).as = X.as * Y.as
• CategoryTheory.Discrete.addMonoidal_leftUnitor 📋 Mathlib.CategoryTheory.Monoidal.Discrete
  (M : Type u) [AddMonoid M] (X : CategoryTheory.Discrete M) : CategoryTheory.MonoidalCategoryStruct.leftUnitor X = CategoryTheory.Discrete.eqToIso ⋯
• CategoryTheory.Discrete.addMonoidal_rightUnitor 📋 Mathlib.CategoryTheory.Monoidal.Discrete
  (M : Type u) [AddMonoid M] (X : CategoryTheory.Discrete M) : CategoryTheory.MonoidalCategoryStruct.rightUnitor X = CategoryTheory.Discrete.eqToIso ⋯
• CategoryTheory.Discrete.monoidal_leftUnitor 📋 Mathlib.CategoryTheory.Monoidal.Discrete
  (M : Type u) [Monoid M] (X : CategoryTheory.Discrete M) : CategoryTheory.MonoidalCategoryStruct.leftUnitor X = CategoryTheory.Discrete.eqToIso ⋯
• CategoryTheory.Discrete.monoidal_rightUnitor 📋 Mathlib.CategoryTheory.Monoidal.Discrete
  (M : Type u) [Monoid M] (X : CategoryTheory.Discrete M) : CategoryTheory.MonoidalCategoryStruct.rightUnitor X = CategoryTheory.Discrete.eqToIso ⋯
• CategoryTheory.Discrete.addMonoidal_associator 📋 Mathlib.CategoryTheory.Monoidal.Discrete
  (M : Type u) [AddMonoid M] (x✝ x✝¹ x✝² : CategoryTheory.Discrete M) : CategoryTheory.MonoidalCategoryStruct.associator x✝ x✝¹ x✝² = CategoryTheory.Discrete.eqToIso ⋯
• CategoryTheory.Discrete.monoidal_associator 📋 Mathlib.CategoryTheory.Monoidal.Discrete
  (M : Type u) [Monoid M] (x✝ x✝¹ x✝² : CategoryTheory.Discrete M) : CategoryTheory.MonoidalCategoryStruct.associator x✝ x✝¹ x✝² = CategoryTheory.Discrete.eqToIso ⋯
• CategoryTheory.Discrete.addMonoidalFunctor_δ 📋 Mathlib.CategoryTheory.Monoidal.Discrete
  {M : Type u} [AddMonoid M] {N : Type u'} [AddMonoid N] (F : M →+ N) (m₁ m₂ : CategoryTheory.Discrete M) : CategoryTheory.Functor.OplaxMonoidal.δ (CategoryTheory.Discrete.addMonoidalFunctor F) m₁ m₂ = CategoryTheory.Discrete.eqToHom ⋯
• CategoryTheory.Discrete.monoidalFunctor_δ 📋 Mathlib.CategoryTheory.Monoidal.Discrete
  {M : Type u} [Monoid M] {N : Type u'} [Monoid N] (F : M →* N) (m₁ m₂ : CategoryTheory.Discrete M) : CategoryTheory.Functor.OplaxMonoidal.δ (CategoryTheory.Discrete.monoidalFunctor F) m₁ m₂ = CategoryTheory.Discrete.eqToHom ⋯
• CategoryTheory.Discrete.addMonoidalFunctor_μ 📋 Mathlib.CategoryTheory.Monoidal.Discrete
  {M : Type u} [AddMonoid M] {N : Type u'} [AddMonoid N] (F : M →+ N) (m₁ m₂ : CategoryTheory.Discrete M) : CategoryTheory.Functor.LaxMonoidal.μ (CategoryTheory.Discrete.addMonoidalFunctor F) m₁ m₂ = CategoryTheory.Discrete.eqToHom ⋯
• CategoryTheory.Discrete.monoidalFunctor_μ 📋 Mathlib.CategoryTheory.Monoidal.Discrete
  {M : Type u} [Monoid M] {N : Type u'} [Monoid N] (F : M →* N) (m₁ m₂ : CategoryTheory.Discrete M) : CategoryTheory.Functor.LaxMonoidal.μ (CategoryTheory.Discrete.monoidalFunctor F) m₁ m₂ = CategoryTheory.Discrete.eqToHom ⋯
• CommRingCat.coproductCocone_ι 📋 Mathlib.Algebra.Category.Ring.Constructions
  (A B : CommRingCat) : (A.coproductCocone B).ι = { app := fun x => match x.as with | CategoryTheory.Limits.WalkingPair.left => CommRingCat.ofHom ↑Algebra.TensorProduct.includeLeft | CategoryTheory.Limits.WalkingPair.right => CommRingCat.ofHom ↑Algebra.TensorProduct.includeRight, naturality := ⋯ }
• CategoryTheory.WithInitial.coconeEquiv_inverse_obj_pt_left_as 📋 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.Under X)} (t : CategoryTheory.Limits.Cocone (CategoryTheory.WithInitial.liftFromUnder.obj K)) : (CategoryTheory.WithInitial.coconeEquiv.inverse.obj t).pt.left.as = PUnit.unit
• CategoryTheory.WithTerminal.coneEquiv_inverse_obj_pt_right_as 📋 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 (CategoryTheory.WithTerminal.liftFromOver.obj K)) : (CategoryTheory.WithTerminal.coneEquiv.inverse.obj t).pt.right.as = PUnit.unit
• CategoryTheory.eq_of_zag 📋 Mathlib.CategoryTheory.IsConnected
  (X : Type u_1) {a b : CategoryTheory.Discrete X} (h : CategoryTheory.Zag a b) : a.as = b.as
• CategoryTheory.eq_of_zigzag 📋 Mathlib.CategoryTheory.IsConnected
  (X : Type u_1) {a b : CategoryTheory.Discrete X} (h : CategoryTheory.Zigzag a b) : a.as = b.as
• CategoryTheory.Grothendieck.grothendieckTypeToCatInverse_obj_fiber_as 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] (G : CategoryTheory.Functor C (Type w)) (X : G.Elements) : ((CategoryTheory.Grothendieck.grothendieckTypeToCatInverse G).obj X).fiber.as = X.snd
• CategoryTheory.Grothendieck.grothendieckTypeToCatFunctor_obj_snd 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] (G : CategoryTheory.Functor C (Type w)) (X : CategoryTheory.Grothendieck (G.comp CategoryTheory.typeToCat)) : ((CategoryTheory.Grothendieck.grothendieckTypeToCatFunctor G).obj X).snd = X.fiber.as
• CategoryTheory.Grothendieck.grothendieckTypeToCat_inverse_obj_fiber_as 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] (G : CategoryTheory.Functor C (Type w)) (X : G.Elements) : ((CategoryTheory.Grothendieck.grothendieckTypeToCat G).inverse.obj X).fiber.as = X.snd
• CategoryTheory.Grothendieck.grothendieckTypeToCat_functor_obj_snd 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] (G : CategoryTheory.Functor C (Type w)) (X : CategoryTheory.Grothendieck (G.comp CategoryTheory.typeToCat)) : ((CategoryTheory.Grothendieck.grothendieckTypeToCat G).functor.obj X).snd = X.fiber.as
• CategoryTheory.Grothendieck.grothendieckTypeToCat_unitIso_hom_app_base 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] (G : CategoryTheory.Functor C (Type w)) (X : CategoryTheory.Grothendieck (G.comp CategoryTheory.typeToCat)) : ((CategoryTheory.Grothendieck.grothendieckTypeToCat G).unitIso.hom.app X).base = CategoryTheory.CategoryStruct.id X.base
• CategoryTheory.Grothendieck.grothendieckTypeToCat_unitIso_inv_app_base 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] (G : CategoryTheory.Functor C (Type w)) (X : CategoryTheory.Grothendieck (G.comp CategoryTheory.typeToCat)) : ((CategoryTheory.Grothendieck.grothendieckTypeToCat G).unitIso.inv.app X).base = CategoryTheory.CategoryStruct.id X.base
• CategoryTheory.Grothendieck.grothendieckTypeToCatFunctor_map_coe 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] (G : CategoryTheory.Functor C (Type w)) {X✝ Y✝ : CategoryTheory.Grothendieck (G.comp CategoryTheory.typeToCat)} (f : X✝ ⟶ Y✝) : ↑((CategoryTheory.Grothendieck.grothendieckTypeToCatFunctor G).map f) = f.base
• CategoryTheory.Grothendieck.grothendieckTypeToCat_functor_map_coe 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] (G : CategoryTheory.Functor C (Type w)) {X✝ Y✝ : CategoryTheory.Grothendieck (G.comp CategoryTheory.typeToCat)} (f : X✝ ⟶ Y✝) : ↑((CategoryTheory.Grothendieck.grothendieckTypeToCat G).functor.map f) = f.base
• CategoryTheory.Grothendieck.grothendieckTypeToCat_unitIso_hom_app_fiber 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] (G : CategoryTheory.Functor C (Type w)) (X : CategoryTheory.Grothendieck (G.comp CategoryTheory.typeToCat)) : ((CategoryTheory.Grothendieck.grothendieckTypeToCat G).unitIso.hom.app X).fiber = CategoryTheory.eqToHom ⋯
• CategoryTheory.Grothendieck.grothendieckTypeToCat_unitIso_inv_app_fiber 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] (G : CategoryTheory.Functor C (Type w)) (X : CategoryTheory.Grothendieck (G.comp CategoryTheory.typeToCat)) : ((CategoryTheory.Grothendieck.grothendieckTypeToCat G).unitIso.inv.app X).fiber = CategoryTheory.eqToHom ⋯
• CategoryTheory.extendCofan_ι_app 📋 Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] {n : ℕ} {f : Fin (n + 1) → C} (c₁ : CategoryTheory.Limits.Cofan fun i => f i.succ) (c₂ : CategoryTheory.Limits.BinaryCofan (f 0) c₁.pt) (X : CategoryTheory.Discrete (Fin (n + 1))) : (CategoryTheory.extendCofan c₁ c₂).ι.app X = Fin.cases c₂.inl (fun i => CategoryTheory.CategoryStruct.comp (c₁.ι.app { as := i }) c₂.inr) X.as
• CategoryTheory.extendFan_π_app 📋 Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] {n : ℕ} {f : Fin (n + 1) → C} (c₁ : CategoryTheory.Limits.Fan fun i => f i.succ) (c₂ : CategoryTheory.Limits.BinaryFan (f 0) c₁.pt) (X : CategoryTheory.Discrete (Fin (n + 1))) : (CategoryTheory.extendFan c₁ c₂).π.app X = Fin.cases c₂.fst (fun i => CategoryTheory.CategoryStruct.comp c₂.snd (c₁.π.app { as := i })) X.as
• CategoryTheory.Limits.HasLimitOfHasProductsOfHasEqualizers.buildLimit 📋 Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} [CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J C} {c₁ : CategoryTheory.Limits.Fan F.obj} {c₂ : CategoryTheory.Limits.Fan fun f => F.obj f.fst.2} (s t : c₁.pt ⟶ c₂.pt) (hs : ∀ (f : (p : J × J) × (p.1 ⟶ p.2)), CategoryTheory.CategoryStruct.comp s (c₂.π.app { as := f }) = CategoryTheory.CategoryStruct.comp (c₁.π.app { as := f.fst.1 }) (F.map f.snd)) (ht : ∀ (f : (p : J × J) × (p.1 ⟶ p.2)), CategoryTheory.CategoryStruct.comp t (c₂.π.app { as := f }) = c₁.π.app { as := f.fst.2 }) (i : CategoryTheory.Limits.Fork s t) : CategoryTheory.Limits.Cone F
• CategoryTheory.Limits.HasLimitOfHasProductsOfHasEqualizers.buildLimit_pt 📋 Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} [CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J C} {c₁ : CategoryTheory.Limits.Fan F.obj} {c₂ : CategoryTheory.Limits.Fan fun f => F.obj f.fst.2} (s t : c₁.pt ⟶ c₂.pt) (hs : ∀ (f : (p : J × J) × (p.1 ⟶ p.2)), CategoryTheory.CategoryStruct.comp s (c₂.π.app { as := f }) = CategoryTheory.CategoryStruct.comp (c₁.π.app { as := f.fst.1 }) (F.map f.snd)) (ht : ∀ (f : (p : J × J) × (p.1 ⟶ p.2)), CategoryTheory.CategoryStruct.comp t (c₂.π.app { as := f }) = c₁.π.app { as := f.fst.2 }) (i : CategoryTheory.Limits.Fork s t) : (CategoryTheory.Limits.HasLimitOfHasProductsOfHasEqualizers.buildLimit s t hs ht i).pt = i.pt
• CategoryTheory.Limits.HasLimitOfHasProductsOfHasEqualizers.buildIsLimit 📋 Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} [CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J C} {c₁ : CategoryTheory.Limits.Fan F.obj} {c₂ : CategoryTheory.Limits.Fan fun f => F.obj f.fst.2} (s t : c₁.pt ⟶ c₂.pt) (hs : ∀ (f : (p : J × J) × (p.1 ⟶ p.2)), CategoryTheory.CategoryStruct.comp s (c₂.π.app { as := f }) = CategoryTheory.CategoryStruct.comp (c₁.π.app { as := f.fst.1 }) (F.map f.snd)) (ht : ∀ (f : (p : J × J) × (p.1 ⟶ p.2)), CategoryTheory.CategoryStruct.comp t (c₂.π.app { as := f }) = c₁.π.app { as := f.fst.2 }) {i : CategoryTheory.Limits.Fork s t} (t₁ : CategoryTheory.Limits.IsLimit c₁) (t₂ : CategoryTheory.Limits.IsLimit c₂) (hi : CategoryTheory.Limits.IsLimit i) : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.HasLimitOfHasProductsOfHasEqualizers.buildLimit s t hs ht i)
• CategoryTheory.Limits.HasLimitOfHasProductsOfHasEqualizers.buildLimit_π_app 📋 Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} [CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J C} {c₁ : CategoryTheory.Limits.Fan F.obj} {c₂ : CategoryTheory.Limits.Fan fun f => F.obj f.fst.2} (s t : c₁.pt ⟶ c₂.pt) (hs : ∀ (f : (p : J × J) × (p.1 ⟶ p.2)), CategoryTheory.CategoryStruct.comp s (c₂.π.app { as := f }) = CategoryTheory.CategoryStruct.comp (c₁.π.app { as := f.fst.1 }) (F.map f.snd)) (ht : ∀ (f : (p : J × J) × (p.1 ⟶ p.2)), CategoryTheory.CategoryStruct.comp t (c₂.π.app { as := f }) = c₁.π.app { as := f.fst.2 }) (i : CategoryTheory.Limits.Fork s t) (x✝ : J) : (CategoryTheory.Limits.HasLimitOfHasProductsOfHasEqualizers.buildLimit s t hs ht i).π.app x✝ = CategoryTheory.CategoryStruct.comp i.ι (c₁.π.app { as := x✝ })
• 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.HasLimit.productLimitCone_cone_π 📋 Mathlib.Algebra.Category.Grp.Biproducts
  {J : Type w} (f : J → AddCommGrpCat) : (AddCommGrpCat.HasLimit.productLimitCone f).cone.π = CategoryTheory.Discrete.natTrans fun j => AddCommGrpCat.ofHom (Pi.evalAddMonoidHom (fun j => ↑(f j)) j.as)
• CategoryTheory.Limits.CoproductsFromFiniteFiltered.finiteSubcoproductsCocone_ι_app 📋 Mathlib.CategoryTheory.Limits.Constructions.Filtered
  {C : Type u} [CategoryTheory.Category.{v, u} C] {α : Type w} [CategoryTheory.Limits.HasFiniteCoproducts C] (f : α → C) [CategoryTheory.Limits.HasCoproduct f] (S : Finset (CategoryTheory.Discrete α)) : (CategoryTheory.Limits.CoproductsFromFiniteFiltered.finiteSubcoproductsCocone f).ι.app S = CategoryTheory.Limits.Sigma.desc fun s => CategoryTheory.Limits.Sigma.ι f (↑s).as
• CategoryTheory.Limits.ProductsFromFiniteCofiltered.finiteSubproductsCone_π_app 📋 Mathlib.CategoryTheory.Limits.Constructions.Filtered
  {C : Type u} [CategoryTheory.Category.{v, u} C] {α : Type w} [CategoryTheory.Limits.HasFiniteProducts C] (f : α → C) [CategoryTheory.Limits.HasProduct f] (S : (Finset (CategoryTheory.Discrete α))ᵒᵖ) : (CategoryTheory.Limits.ProductsFromFiniteCofiltered.finiteSubproductsCone f).π.app S = CategoryTheory.Limits.Pi.lift fun s => CategoryTheory.Limits.Pi.π f (↑s).as
• CategoryTheory.Functor.LeftExtension.mk_left_as 📋 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} (α : F ⟶ L.comp F') : (CategoryTheory.Functor.LeftExtension.mk F' α).left.as = PUnit.unit
• CategoryTheory.Functor.RightExtension.mk_right_as 📋 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) : (CategoryTheory.Functor.RightExtension.mk F' α).right.as = PUnit.unit
• CategoryTheory.Limits.CofanTypes.sigma_ι_fst 📋 Mathlib.CategoryTheory.Limits.Types.Coproducts
  {C : Type u} (F : C → Type v) (x✝ : CategoryTheory.Discrete C) (x : (CategoryTheory.Discrete.functor F).obj x✝) : ((CategoryTheory.Limits.CofanTypes.sigma F).ι x✝ x).fst = x✝.as
• CategoryTheory.Limits.Types.binaryCoproductCocone_ι_app 📋 Mathlib.CategoryTheory.Limits.Types.Coproducts
  (X Y : Type u) (x✝ : CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) : (CategoryTheory.Limits.Types.binaryCoproductCocone X Y).ι.app x✝ = match x✝.as with | CategoryTheory.Limits.WalkingPair.left => TypeCat.ofHom Sum.inl | CategoryTheory.Limits.WalkingPair.right => TypeCat.ofHom Sum.inr
• ModuleCat.HasLimit.productLimitCone_cone_π 📋 Mathlib.Algebra.Category.ModuleCat.Biproducts
  {R : Type u} [Ring R] {J : Type w} (f : J → ModuleCat R) : (ModuleCat.HasLimit.productLimitCone f).cone.π = CategoryTheory.Discrete.natTrans fun j => ModuleCat.ofHom (LinearMap.proj j.as)
• 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
• CochainComplex.shiftFunctor_obj_d' 📋 Mathlib.Algebra.Homology.HomotopyCategory.Shift
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (K : CochainComplex C ℤ) (n i j : ℤ) : ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj K).d i j = n.negOnePow • K.d (i + { as := n }.as) (j + { as := n }.as)
• CochainComplex.shiftFunctorZero_hom_app_f 📋 Mathlib.Algebra.Homology.HomotopyCategory.Shift
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (K : CochainComplex C ℤ) (n : ℤ) : ((CategoryTheory.shiftFunctorZero (CochainComplex C ℤ) ℤ).hom.app K).f n = (HomologicalComplex.XIsoOfEq K ⋯).hom
• CochainComplex.shiftFunctorZero_inv_app_f 📋 Mathlib.Algebra.Homology.HomotopyCategory.Shift
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (K : CochainComplex C ℤ) (n : ℤ) : ((CategoryTheory.shiftFunctorZero (CochainComplex C ℤ) ℤ).inv.app K).f n = (HomologicalComplex.XIsoOfEq K ⋯).hom
• CochainComplex.shiftFunctorAdd'_hom_app_f' 📋 Mathlib.Algebra.Homology.HomotopyCategory.Shift
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (K : CochainComplex C ℤ) (a b ab : ℤ) (h : a + b = ab) (n : ℤ) : ((CategoryTheory.shiftFunctorAdd' (CochainComplex C ℤ) a b ab h).hom.app K).f n = (HomologicalComplex.XIsoOfEq K ⋯).hom
• CochainComplex.shiftFunctorAdd'_inv_app_f' 📋 Mathlib.Algebra.Homology.HomotopyCategory.Shift
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (K : CochainComplex C ℤ) (a b ab : ℤ) (h : a + b = ab) (n : ℤ) : ((CategoryTheory.shiftFunctorAdd' (CochainComplex C ℤ) a b ab h).inv.app K).f n = (HomologicalComplex.XIsoOfEq K ⋯).hom
• CochainComplex.shiftFunctorAdd_hom_app_f 📋 Mathlib.Algebra.Homology.HomotopyCategory.Shift
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (K : CochainComplex C ℤ) (a b n : ℤ) : ((CategoryTheory.shiftFunctorAdd (CochainComplex C ℤ) a b).hom.app K).f n = (HomologicalComplex.XIsoOfEq K ⋯).hom
• CochainComplex.shiftFunctorAdd_inv_app_f 📋 Mathlib.Algebra.Homology.HomotopyCategory.Shift
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (K : CochainComplex C ℤ) (a b n : ℤ) : ((CategoryTheory.shiftFunctorAdd (CochainComplex C ℤ) a b).inv.app K).f n = (HomologicalComplex.XIsoOfEq K ⋯).hom
• CochainComplex.mappingCone.cocycleOfDegreewiseSplit_triangleRotateShortComplexSplitting_v 📋 Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit
  {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {K L : CochainComplex C ℤ} (φ : K ⟶ L) (p : ℤ) : (↑(CochainComplex.cocycleOfDegreewiseSplit (CochainComplex.mappingCone.triangleRotateShortComplex φ) (CochainComplex.mappingCone.triangleRotateShortComplexSplitting φ))).v p (p + 1) ⋯ = -φ.f (p + { as := 1 }.as)
• CategoryTheory.ShiftedHom.opEquiv'_add_symm 📋 Mathlib.CategoryTheory.Shift.ShiftedHomOpposite
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.HasShift C ℤ] {X Y : C} (n m a a' a'' : ℤ) (ha' : n + a = a') (ha'' : m + a' = a'') (x : Opposite.op ((CategoryTheory.shiftFunctor C a).obj Y) ⟶ (CategoryTheory.shiftFunctor Cᵒᵖ (m + n)).obj (Opposite.op X)) : (CategoryTheory.ShiftedHom.opEquiv' (m + n) a a'' ⋯).symm x = (CategoryTheory.ShiftedHom.opEquiv' m a' a'' ha'').symm (Quiver.Hom.op ((CategoryTheory.ShiftedHom.opEquiv' n a a' ha').symm (CategoryTheory.CategoryStruct.comp x ((CategoryTheory.shiftFunctorAdd Cᵒᵖ m n).hom.app (Opposite.op X)))))
• TopCat.piFan_π_app 📋 Mathlib.Topology.Category.TopCat.Limits.Products
  {ι : Type v} (α : ι → TopCat) (X : CategoryTheory.Discrete ι) : (TopCat.piFan α).π.app X = TopCat.piπ α X.as
• TopCat.sigmaCofan_ι_app 📋 Mathlib.Topology.Category.TopCat.Limits.Products
  {ι : Type v} (α : ι → TopCat) (X : CategoryTheory.Discrete ι) : (TopCat.sigmaCofan α).ι.app X = TopCat.sigmaι α X.as
• CategoryTheory.LocallyDiscrete.id_as 📋 Mathlib.CategoryTheory.Bicategory.LocallyDiscrete
  {C : Type u} [CategoryTheory.CategoryStruct.{v, u} C] (a : CategoryTheory.LocallyDiscrete C) : (CategoryTheory.CategoryStruct.id a).as = CategoryTheory.CategoryStruct.id a.as
• Quiver.Hom.toLoc_as 📋 Mathlib.CategoryTheory.Bicategory.LocallyDiscrete
  {C : Type u} [CategoryTheory.CategoryStruct.{v, u} C] {a b : C} (f : a ⟶ b) : f.toLoc.as = f
• CategoryTheory.LocallyDiscrete.comp_as 📋 Mathlib.CategoryTheory.Bicategory.LocallyDiscrete
  {C : Type u} [CategoryTheory.CategoryStruct.{v, u} C] {a b c : CategoryTheory.LocallyDiscrete C} (f : a ⟶ b) (g : b ⟶ c) : (CategoryTheory.CategoryStruct.comp f g).as = CategoryTheory.CategoryStruct.comp f.as g.as
• CategoryTheory.LocallyDiscrete.mkPseudofunctor_map 📋 Mathlib.CategoryTheory.Bicategory.Functor.LocallyDiscrete
  {B₀ : Type u_1} {C : Type u_2} [CategoryTheory.Category.{v_1, u_1} B₀] [CategoryTheory.Bicategory C] (obj : B₀ → C) (map : {b b' : B₀} → (b ⟶ b') → (obj b ⟶ obj b')) (mapId : (b : B₀) → map (CategoryTheory.CategoryStruct.id b) ≅ CategoryTheory.CategoryStruct.id (obj b)) (mapComp : {b₀ b₁ b₂ : B₀} → (f : b₀ ⟶ b₁) → (g : b₁ ⟶ b₂) → map (CategoryTheory.CategoryStruct.comp f g) ≅ CategoryTheory.CategoryStruct.comp (map f) (map g)) (map₂_associator : ∀ {b₀ b₁ b₂ b₃ : B₀} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) (h : b₂ ⟶ b₃), CategoryTheory.CategoryStruct.comp (mapComp (CategoryTheory.CategoryStruct.comp f g) h).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (mapComp f g).hom (map h)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (map f) (map g) (map h)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (map f) (mapComp g h).inv) (mapComp f (CategoryTheory.CategoryStruct.comp g h)).inv))) = CategoryTheory.eqToHom ⋯ := by cat_disch) (map₂_left_unitor : ∀ {b₀ b₁ : B₀} (f : b₀ ⟶ b₁), CategoryTheory.CategoryStruct.comp (mapComp (CategoryTheory.CategoryStruct.id b₀) f).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (mapId b₀).hom (map f)) (CategoryTheory.Bicategory.leftUnitor (map f)).hom) = CategoryTheory.eqToHom ⋯ := by cat_disch) (map₂_right_unitor : ∀ {b₀ b₁ : B₀} (f : b₀ ⟶ b₁), CategoryTheory.CategoryStruct.comp (mapComp f (CategoryTheory.CategoryStruct.id b₁)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (map f) (mapId b₁).hom) (CategoryTheory.Bicategory.rightUnitor (map f)).hom) = CategoryTheory.eqToHom ⋯ := by cat_disch) {X✝ Y✝ : CategoryTheory.LocallyDiscrete B₀} (f : X✝ ⟶ Y✝) : (CategoryTheory.LocallyDiscrete.mkPseudofunctor obj map mapId mapComp map₂_associator map₂_left_unitor map₂_right_unitor).map f = map f.as
• CategoryTheory.LocallyDiscrete.mkPseudofunctor_mapComp 📋 Mathlib.CategoryTheory.Bicategory.Functor.LocallyDiscrete
  {B₀ : Type u_1} {C : Type u_2} [CategoryTheory.Category.{v_1, u_1} B₀] [CategoryTheory.Bicategory C] (obj : B₀ → C) (map : {b b' : B₀} → (b ⟶ b') → (obj b ⟶ obj b')) (mapId : (b : B₀) → map (CategoryTheory.CategoryStruct.id b) ≅ CategoryTheory.CategoryStruct.id (obj b)) (mapComp : {b₀ b₁ b₂ : B₀} → (f : b₀ ⟶ b₁) → (g : b₁ ⟶ b₂) → map (CategoryTheory.CategoryStruct.comp f g) ≅ CategoryTheory.CategoryStruct.comp (map f) (map g)) (map₂_associator : ∀ {b₀ b₁ b₂ b₃ : B₀} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) (h : b₂ ⟶ b₃), CategoryTheory.CategoryStruct.comp (mapComp (CategoryTheory.CategoryStruct.comp f g) h).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (mapComp f g).hom (map h)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (map f) (map g) (map h)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (map f) (mapComp g h).inv) (mapComp f (CategoryTheory.CategoryStruct.comp g h)).inv))) = CategoryTheory.eqToHom ⋯ := by cat_disch) (map₂_left_unitor : ∀ {b₀ b₁ : B₀} (f : b₀ ⟶ b₁), CategoryTheory.CategoryStruct.comp (mapComp (CategoryTheory.CategoryStruct.id b₀) f).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (mapId b₀).hom (map f)) (CategoryTheory.Bicategory.leftUnitor (map f)).hom) = CategoryTheory.eqToHom ⋯ := by cat_disch) (map₂_right_unitor : ∀ {b₀ b₁ : B₀} (f : b₀ ⟶ b₁), CategoryTheory.CategoryStruct.comp (mapComp f (CategoryTheory.CategoryStruct.id b₁)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (map f) (mapId b₁).hom) (CategoryTheory.Bicategory.rightUnitor (map f)).hom) = CategoryTheory.eqToHom ⋯ := by cat_disch) {a✝ b✝ c✝ : CategoryTheory.LocallyDiscrete B₀} (x✝ : a✝ ⟶ b✝) (x✝¹ : b✝ ⟶ c✝) : (CategoryTheory.LocallyDiscrete.mkPseudofunctor obj map mapId mapComp map₂_associator map₂_left_unitor map₂_right_unitor).mapComp x✝ x✝¹ = mapComp x✝.as x✝¹.as
• CommRingCat.moduleCatExtendScalarsPseudofunctor_map 📋 Mathlib.Algebra.Category.ModuleCat.Pseudofunctor
  {X✝ Y✝ : CategoryTheory.LocallyDiscrete CommRingCat} (f : X✝ ⟶ Y✝) : CommRingCat.moduleCatExtendScalarsPseudofunctor.map f = (ModuleCat.extendScalars (CommRingCat.Hom.hom f.as)).toCatHom
• RingCat.moduleCatRestrictScalarsPseudofunctor_map 📋 Mathlib.Algebra.Category.ModuleCat.Pseudofunctor
  {X✝ Y✝ : CategoryTheory.LocallyDiscrete RingCatᵒᵖ} (f : X✝ ⟶ Y✝) : RingCat.moduleCatRestrictScalarsPseudofunctor.map f = (ModuleCat.restrictScalars (RingCat.Hom.hom f.as.unop)).toCatHom
• CommRingCat.moduleCatRestrictScalarsPseudofunctor_map 📋 Mathlib.Algebra.Category.ModuleCat.Pseudofunctor
  {X✝ Y✝ : CategoryTheory.LocallyDiscrete CommRingCatᵒᵖ} (f : X✝ ⟶ Y✝) : CommRingCat.moduleCatRestrictScalarsPseudofunctor.map f = (ModuleCat.restrictScalars (CommRingCat.Hom.hom f.as.unop)).toCatHom
• CommRingCat.moduleCatExtendScalarsPseudofunctor_mapComp 📋 Mathlib.Algebra.Category.ModuleCat.Pseudofunctor
  {a✝ b✝ c✝ : CategoryTheory.LocallyDiscrete CommRingCat} (x✝ : a✝ ⟶ b✝) (x✝¹ : b✝ ⟶ c✝) : CommRingCat.moduleCatExtendScalarsPseudofunctor.mapComp x✝ x✝¹ = CategoryTheory.Cat.Hom.isoMk (ModuleCat.extendScalarsComp (CommRingCat.Hom.hom x✝.as) (CommRingCat.Hom.hom x✝¹.as))
• RingCat.moduleCatRestrictScalarsPseudofunctor_mapComp 📋 Mathlib.Algebra.Category.ModuleCat.Pseudofunctor
  {a✝ b✝ c✝ : CategoryTheory.LocallyDiscrete RingCatᵒᵖ} (x✝ : a✝ ⟶ b✝) (x✝¹ : b✝ ⟶ c✝) : RingCat.moduleCatRestrictScalarsPseudofunctor.mapComp x✝ x✝¹ = CategoryTheory.Cat.Hom.isoMk (ModuleCat.restrictScalarsComp (RingCat.Hom.hom x✝¹.as.unop) (RingCat.Hom.hom x✝.as.unop))
• CommRingCat.moduleCatRestrictScalarsPseudofunctor_mapComp 📋 Mathlib.Algebra.Category.ModuleCat.Pseudofunctor
  {a✝ b✝ c✝ : CategoryTheory.LocallyDiscrete CommRingCatᵒᵖ} (x✝ : a✝ ⟶ b✝) (x✝¹ : b✝ ⟶ c✝) : CommRingCat.moduleCatRestrictScalarsPseudofunctor.mapComp x✝ x✝¹ = CategoryTheory.Cat.Hom.isoMk (ModuleCat.restrictScalarsComp (CommRingCat.Hom.hom x✝¹.as.unop) (CommRingCat.Hom.hom x✝.as.unop))
• TopCat.Presheaf.generateEquivalenceOpensLe_inverse'_obj_obj_right_as 📋 Mathlib.Topology.Sheaves.SheafCondition.OpensLeCover
  {X : TopCat} {ι : Type u_2} (U : ι → TopologicalSpace.Opens ↑X) {Y : TopologicalSpace.Opens ↑X} (hY : Y = iSup U) (V : TopCat.Presheaf.SheafCondition.OpensLeCover U) : ((TopCat.Presheaf.generateEquivalenceOpensLe_inverse' U hY).obj V).obj.right.as = PUnit.unit
• CategoryTheory.TwoSquare.structuredArrowRightwardsOpEquivalence.functor_obj_right_as 📋 Mathlib.CategoryTheory.GuitartExact.Opposite
  {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} {C₄ : Type u₄} [CategoryTheory.Category.{v₁, u₁} C₁] [CategoryTheory.Category.{v₂, u₂} C₂] [CategoryTheory.Category.{v₃, u₃} C₃] [CategoryTheory.Category.{v₄, u₄} C₄] {T : CategoryTheory.Functor C₁ C₂} {L : CategoryTheory.Functor C₁ C₃} {R : CategoryTheory.Functor C₂ C₄} {B : CategoryTheory.Functor C₃ C₄} (w : CategoryTheory.TwoSquare T L R B) {X₃ : C₃ᵒᵖ} {X₂ : C₂ᵒᵖ} (g : B.op.obj X₃ ⟶ R.op.obj X₂) (f : (w.op.StructuredArrowRightwards g)ᵒᵖ) : ((CategoryTheory.TwoSquare.structuredArrowRightwardsOpEquivalence.functor w g).obj f).right.as = PUnit.unit
• CategoryTheory.TwoSquare.structuredArrowRightwardsOpEquivalence.functor_obj_left_left_as 📋 Mathlib.CategoryTheory.GuitartExact.Opposite
  {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} {C₄ : Type u₄} [CategoryTheory.Category.{v₁, u₁} C₁] [CategoryTheory.Category.{v₂, u₂} C₂] [CategoryTheory.Category.{v₃, u₃} C₃] [CategoryTheory.Category.{v₄, u₄} C₄] {T : CategoryTheory.Functor C₁ C₂} {L : CategoryTheory.Functor C₁ C₃} {R : CategoryTheory.Functor C₂ C₄} {B : CategoryTheory.Functor C₃ C₄} (w : CategoryTheory.TwoSquare T L R B) {X₃ : C₃ᵒᵖ} {X₂ : C₂ᵒᵖ} (g : B.op.obj X₃ ⟶ R.op.obj X₂) (f : (w.op.StructuredArrowRightwards g)ᵒᵖ) : ((CategoryTheory.TwoSquare.structuredArrowRightwardsOpEquivalence.functor w g).obj f).left.left.as = PUnit.unit
• HomologicalComplex.homologicalComplexToDGO_obj_d 📋 Mathlib.Algebra.Homology.DifferentialObject
  {β : Type u_1} [AddCommGroup β] (b : β) (V : Type u_2) [CategoryTheory.Category.{v_1, u_2} V] [CategoryTheory.Limits.HasZeroMorphisms V] (X : HomologicalComplex V (ComplexShape.up' b)) (i : β) : ((HomologicalComplex.homologicalComplexToDGO b V).obj X).d i = X.d i ((fun b_1 => b_1 + { as := 1 }.as • b) i)
• HomologicalComplex.homologicalComplexToDGO_map_f 📋 Mathlib.Algebra.Homology.DifferentialObject
  {β : Type u_1} [AddCommGroup β] (b : β) (V : Type u_2) [CategoryTheory.Category.{v_1, u_2} V] [CategoryTheory.Limits.HasZeroMorphisms V] {X Y : HomologicalComplex V (ComplexShape.up' b)} (f : X ⟶ Y) (i : β) : ((HomologicalComplex.homologicalComplexToDGO b V).map f).f i = f.f i
• CategoryTheory.DifferentialObject.objEqToHom_d 📋 Mathlib.Algebra.Homology.DifferentialObject
  {β : Type u_1} [AddCommGroup β] {b : β} {V : Type u_2} [CategoryTheory.Category.{v_1, u_2} V] [CategoryTheory.Limits.HasZeroMorphisms V] (X : CategoryTheory.DifferentialObject ℤ (CategoryTheory.GradedObjectWithShift b V)) {x y : β} (h : x = y) : CategoryTheory.CategoryStruct.comp (X.objEqToHom h) (X.d y) = CategoryTheory.CategoryStruct.comp (X.d x) (X.objEqToHom ⋯)
• HomologicalComplex.dgoToHomologicalComplex_obj_d 📋 Mathlib.Algebra.Homology.DifferentialObject
  {β : Type u_1} [AddCommGroup β] (b : β) (V : Type u_2) [CategoryTheory.Category.{v_1, u_2} V] [CategoryTheory.Limits.HasZeroMorphisms V] (X : CategoryTheory.DifferentialObject ℤ (CategoryTheory.GradedObjectWithShift b V)) (i j : β) : ((HomologicalComplex.dgoToHomologicalComplex b V).obj X).d i j = if h : i + b = j then CategoryTheory.CategoryStruct.comp (X.d i) (X.objEqToHom ⋯) else 0
• CategoryTheory.DifferentialObject.d_squared_apply 📋 Mathlib.Algebra.Homology.DifferentialObject
  {β : Type u_1} [AddCommGroup β] {b : β} {V : Type u_2} [CategoryTheory.Category.{v_1, u_2} V] [CategoryTheory.Limits.HasZeroMorphisms V] (X : CategoryTheory.DifferentialObject ℤ (CategoryTheory.GradedObjectWithShift b V)) {x : β} : CategoryTheory.CategoryStruct.comp (X.d x) (X.d ((fun b_1 => b_1 + { as := 1 }.as • b) x)) = 0
• CategoryTheory.DifferentialObject.d_squared_apply_assoc 📋 Mathlib.Algebra.Homology.DifferentialObject
  {β : Type u_1} [AddCommGroup β] {b : β} {V : Type u_2} [CategoryTheory.Category.{v_1, u_2} V] [CategoryTheory.Limits.HasZeroMorphisms V] (X : CategoryTheory.DifferentialObject ℤ (CategoryTheory.GradedObjectWithShift b V)) {x : β} {Z : V} (h : (CategoryTheory.shiftFunctor (CategoryTheory.GradedObjectWithShift b V) 1).obj X.obj (x + 1 • b) ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.d x) (CategoryTheory.CategoryStruct.comp (X.d (x + 1 • b)) h) = CategoryTheory.CategoryStruct.comp 0 h
• HomologicalComplex.dgoToHomologicalComplex_map_f 📋 Mathlib.Algebra.Homology.DifferentialObject
  {β : Type u_1} [AddCommGroup β] (b : β) (V : Type u_2) [CategoryTheory.Category.{v_1, u_2} V] [CategoryTheory.Limits.HasZeroMorphisms V] {X Y : CategoryTheory.DifferentialObject ℤ (CategoryTheory.GradedObjectWithShift b V)} (f : X ⟶ Y) (i : β) : ((HomologicalComplex.dgoToHomologicalComplex b V).map f).f i = f.f i
• TopologicalSpace.Opens.overEquivalence_inverse_obj_right_as 📋 Mathlib.Topology.Sheaves.Over
  {X : Type u} [TopologicalSpace X] (U : TopologicalSpace.Opens X) (W : TopologicalSpace.Opens ↥U) : (U.overEquivalence.inverse.obj W).right.as = PUnit.unit
• AlgebraicGeometry.Scheme.Modules.pseudofunctor_map_l 📋 Mathlib.AlgebraicGeometry.Modules.Sheaf
  {X✝ Y✝ : CategoryTheory.LocallyDiscrete AlgebraicGeometry.Schemeᵒᵖ} (f : X✝ ⟶ Y✝) : (AlgebraicGeometry.Scheme.Modules.pseudofunctor.map f).l = (AlgebraicGeometry.Scheme.Modules.pullback f.as.unop).toCatHom
• AlgebraicGeometry.Scheme.Modules.pseudofunctor_map_r 📋 Mathlib.AlgebraicGeometry.Modules.Sheaf
  {X✝ Y✝ : CategoryTheory.LocallyDiscrete AlgebraicGeometry.Schemeᵒᵖ} (f : X✝ ⟶ Y✝) : (AlgebraicGeometry.Scheme.Modules.pseudofunctor.map f).r = (AlgebraicGeometry.Scheme.Modules.pushforward f.as.unop).toCatHom
• AlgebraicGeometry.Scheme.Modules.pseudofunctor_map_adj 📋 Mathlib.AlgebraicGeometry.Modules.Sheaf
  {X✝ Y✝ : CategoryTheory.LocallyDiscrete AlgebraicGeometry.Schemeᵒᵖ} (f : X✝ ⟶ Y✝) : (AlgebraicGeometry.Scheme.Modules.pseudofunctor.map f).adj = (AlgebraicGeometry.Scheme.Modules.pullbackPushforwardAdjunction f.as.unop).toCat
• AlgebraicGeometry.Scheme.Modules.pseudofunctor_mapComp_hom_τl 📋 Mathlib.AlgebraicGeometry.Modules.Sheaf
  {a✝ b✝ c✝ : CategoryTheory.LocallyDiscrete AlgebraicGeometry.Schemeᵒᵖ} (x✝ : a✝ ⟶ b✝) (x✝¹ : b✝ ⟶ c✝) : (AlgebraicGeometry.Scheme.Modules.pseudofunctor.mapComp x✝ x✝¹).hom.τl = CategoryTheory.NatTrans.toCatHom₂ (AlgebraicGeometry.Scheme.Modules.pullbackComp x✝¹.as.unop x✝.as.unop).inv
• AlgebraicGeometry.Scheme.Modules.pseudofunctor_mapComp_inv_τl 📋 Mathlib.AlgebraicGeometry.Modules.Sheaf
  {a✝ b✝ c✝ : CategoryTheory.LocallyDiscrete AlgebraicGeometry.Schemeᵒᵖ} (x✝ : a✝ ⟶ b✝) (x✝¹ : b✝ ⟶ c✝) : (AlgebraicGeometry.Scheme.Modules.pseudofunctor.mapComp x✝ x✝¹).inv.τl = CategoryTheory.NatTrans.toCatHom₂ (AlgebraicGeometry.Scheme.Modules.pullbackComp x✝¹.as.unop x✝.as.unop).hom
• AlgebraicGeometry.Scheme.Modules.pseudofunctor_mapComp_hom_τr 📋 Mathlib.AlgebraicGeometry.Modules.Sheaf
  {a✝ b✝ c✝ : CategoryTheory.LocallyDiscrete AlgebraicGeometry.Schemeᵒᵖ} (x✝ : a✝ ⟶ b✝) (x✝¹ : b✝ ⟶ c✝) : (AlgebraicGeometry.Scheme.Modules.pseudofunctor.mapComp x✝ x✝¹).hom.τr = CategoryTheory.NatTrans.toCatHom₂ (AlgebraicGeometry.Scheme.Modules.pushforwardComp x✝¹.as.unop x✝.as.unop).hom
• AlgebraicGeometry.Scheme.Modules.pseudofunctor_mapComp_inv_τr 📋 Mathlib.AlgebraicGeometry.Modules.Sheaf
  {a✝ b✝ c✝ : CategoryTheory.LocallyDiscrete AlgebraicGeometry.Schemeᵒᵖ} (x✝ : a✝ ⟶ b✝) (x✝¹ : b✝ ⟶ c✝) : (AlgebraicGeometry.Scheme.Modules.pseudofunctor.mapComp x✝ x✝¹).inv.τr = CategoryTheory.NatTrans.toCatHom₂ (AlgebraicGeometry.Scheme.Modules.pushforwardComp x✝¹.as.unop x✝.as.unop).inv
• AlgebraicGeometry.Scheme.AffineEtale.mk_right_as 📋 Mathlib.AlgebraicGeometry.Sites.AffineEtale
  {S : AlgebraicGeometry.Scheme} {R : CommRingCat} (f : AlgebraicGeometry.Spec R ⟶ S) [AlgebraicGeometry.Etale f] : (AlgebraicGeometry.Scheme.AffineEtale.mk f).right.as = PUnit.unit
• AlgebraicGeometry.Scheme.ProEt.mk_right_as 📋 Mathlib.AlgebraicGeometry.Sites.Proetale
  {S X : AlgebraicGeometry.Scheme} (f : X ⟶ S) [AlgebraicGeometry.WeaklyEtale f] : (AlgebraicGeometry.Scheme.ProEt.mk f).right.as = PUnit.unit
• CategoryTheory.SimplicialObject.Truncated.rightExtensionInclusion_right_as 📋 Mathlib.AlgebraicTopology.SimplicialObject.Coskeletal
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.SimplicialObject C) (n : ℕ) : (CategoryTheory.SimplicialObject.Truncated.rightExtensionInclusion X n).right.as = PUnit.unit
• SSet.Truncated.rightExtensionInclusion_right_as 📋 Mathlib.AlgebraicTopology.SimplicialSet.Coskeletal
  (X : SSet) (n : ℕ) : (SSet.Truncated.rightExtensionInclusion X n).right.as = PUnit.unit
• CategoryTheory.Limits.IndObjectPresentation.toCostructuredArrow_obj_right_as 📋 Mathlib.CategoryTheory.Limits.Indization.IndObject
  {C : Type u} [CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)} (P : CategoryTheory.Limits.IndObjectPresentation A) (X : P.I) : (P.toCostructuredArrow.obj X).right.as = PUnit.unit
• CategoryTheory.Limits.CoproductsFromFiniteFiltered.finiteSubcoproductsCocone_ι_app_eq_sum 📋 Mathlib.CategoryTheory.Preadditive.LiftToFinset
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteCoproducts C] {α : Type w} [DecidableEq α] (f : α → C) [CategoryTheory.Limits.HasCoproduct f] (S : Finset (CategoryTheory.Discrete α)) : (CategoryTheory.Limits.CoproductsFromFiniteFiltered.finiteSubcoproductsCocone f).ι.app S = ∑ a ∈ S.attach, CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.π (fun a => f (↑a).as) a) (CategoryTheory.Limits.Sigma.ι f (↑a).as)
• CategoryTheory.Limits.ProductsFromFiniteCofiltered.finiteSubproductsCocone_π_app_eq_sum 📋 Mathlib.CategoryTheory.Preadditive.LiftToFinset
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteProducts C] {α : Type w} [DecidableEq α] (f : α → C) [CategoryTheory.Limits.HasProduct f] (S : (Finset (CategoryTheory.Discrete α))ᵒᵖ) : (CategoryTheory.Limits.ProductsFromFiniteCofiltered.finiteSubproductsCone f).π.app S = ∑ a ∈ (Opposite.unop S).attach, CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π f (↑a).as) (CategoryTheory.Limits.Pi.ι (fun a => f (↑a).as) a)
• CategoryTheory.Bicategory.LeftExtension.ofCompId_left_as 📋 Mathlib.CategoryTheory.Bicategory.Extension
  {B : Type u} [CategoryTheory.Bicategory B] {a b c : B} {f : a ⟶ b} {g : a ⟶ c} (t : CategoryTheory.Bicategory.LeftExtension f (CategoryTheory.CategoryStruct.comp g (CategoryTheory.CategoryStruct.id c))) : t.ofCompId.left.as = PUnit.unit
• CategoryTheory.Bicategory.LeftLift.ofIdComp_left_as 📋 Mathlib.CategoryTheory.Bicategory.Extension
  {B : Type u} [CategoryTheory.Bicategory B] {a b c : B} {f : b ⟶ a} {g : c ⟶ a} (t : CategoryTheory.Bicategory.LeftLift f (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id c) g)) : t.ofIdComp.left.as = PUnit.unit
• CategoryTheory.Bicategory.RightLift.ofIdComp_right_as 📋 Mathlib.CategoryTheory.Bicategory.Extension
  {B : Type u} [CategoryTheory.Bicategory B] {a b c : B} {f : b ⟶ a} {g : c ⟶ a} (t : CategoryTheory.Bicategory.RightLift f (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id c) g)) : t.ofIdComp.right.as = PUnit.unit
• CategoryTheory.Discrete.productEquiv_inverse_obj_as 📋 Mathlib.CategoryTheory.Discrete.SumsProducts
  {J : Type u_1} {K : Type u_2} (x✝ : CategoryTheory.Discrete J × CategoryTheory.Discrete K) : (CategoryTheory.Discrete.productEquiv.inverse.obj x✝).as = (x✝.1.as, x✝.2.as)
• CategoryTheory.Discrete.productEquiv_functor_obj 📋 Mathlib.CategoryTheory.Discrete.SumsProducts
  {J : Type u_1} {K : Type u_2} (a✝ : CategoryTheory.Discrete (J × K)) : CategoryTheory.Discrete.productEquiv.functor.obj a✝ = ({ as := a✝.as.1 }, { as := a✝.as.2 })
• CategoryTheory.Discrete.sumEquiv_functor_obj 📋 Mathlib.CategoryTheory.Discrete.SumsProducts
  {J : Type u_1} {K : Type u_2} (a✝ : CategoryTheory.Discrete (J ⊕ K)) : CategoryTheory.Discrete.sumEquiv.functor.obj a✝ = match a✝.as with | Sum.inl j => Sum.inl { as := j } | Sum.inr k => Sum.inr { as := k }
• CategoryTheory.Discrete.sumEquiv_inverse_obj 📋 Mathlib.CategoryTheory.Discrete.SumsProducts
  {J : Type u_1} {K : Type u_2} (x✝ : CategoryTheory.Discrete J ⊕ CategoryTheory.Discrete K) : CategoryTheory.Discrete.sumEquiv.inverse.obj x✝ = match x✝ with | Sum.inl X => { as := Sum.inl X.as } | Sum.inr X => { as := Sum.inr X.as }
• CategoryTheory.Discrete.productEquiv_inverse_map 📋 Mathlib.CategoryTheory.Discrete.SumsProducts
  {J : Type u_1} {K : Type u_2} {X✝ Y✝ : CategoryTheory.Discrete J × CategoryTheory.Discrete K} (x✝ : X✝ ⟶ Y✝) : CategoryTheory.Discrete.productEquiv.inverse.map x✝ = match x✝ with | (f₁, f₂) => CategoryTheory.eqToHom ⋯
• CategoryTheory.Discrete.productEquiv_functor_map 📋 Mathlib.CategoryTheory.Discrete.SumsProducts
  {J : Type u_1} {K : Type u_2} {X Y : CategoryTheory.Discrete (J × K)} (f : X ⟶ Y) : CategoryTheory.Discrete.productEquiv.functor.map f = CategoryTheory.Discrete.Hom.rec (fun eq => CategoryTheory.eqToHom ⋯) f
• CategoryTheory.Discrete.sumEquiv_functor_map 📋 Mathlib.CategoryTheory.Discrete.SumsProducts
  {J : Type u_1} {K : Type u_2} {X Y : CategoryTheory.Discrete (J ⊕ K)} (f : X ⟶ Y) : CategoryTheory.Discrete.sumEquiv.functor.map f = CategoryTheory.Discrete.Hom.rec (fun eq => CategoryTheory.eqToHom ⋯) f
• CategoryTheory.Discrete.sumEquiv_inverse_map 📋 Mathlib.CategoryTheory.Discrete.SumsProducts
  {J : Type u_1} {K : Type u_2} {X Y : CategoryTheory.Discrete J ⊕ CategoryTheory.Discrete K} (f : X ⟶ Y) : CategoryTheory.Discrete.sumEquiv.inverse.map f = CategoryTheory.Sum.homInduction (fun x x_1 f => (CategoryTheory.Discrete.functor fun t => { as := Sum.inl t }).map f) (fun x x_1 g => (CategoryTheory.Discrete.functor fun t => { as := Sum.inr t }).map g) f
• CategoryTheory.Discrete.sumEquiv_unitIso_hom_app 📋 Mathlib.CategoryTheory.Discrete.SumsProducts
  {J : Type u_1} {K : Type u_2} (X : CategoryTheory.Discrete (J ⊕ K)) : CategoryTheory.Discrete.sumEquiv.unitIso.hom.app X = (match X.as with | Sum.inl x => CategoryTheory.Iso.refl { as := Sum.inl x } | Sum.inr x => CategoryTheory.Iso.refl { as := Sum.inr x }).hom
• CategoryTheory.Discrete.sumEquiv_unitIso_inv_app 📋 Mathlib.CategoryTheory.Discrete.SumsProducts
  {J : Type u_1} {K : Type u_2} (X : CategoryTheory.Discrete (J ⊕ K)) : CategoryTheory.Discrete.sumEquiv.unitIso.inv.app X = (match X.as with | Sum.inl x => CategoryTheory.Iso.refl { as := Sum.inl x } | Sum.inr x => CategoryTheory.Iso.refl { as := Sum.inr x }).inv
• CategoryTheory.Discrete.sumEquiv_counitIso_hom_app 📋 Mathlib.CategoryTheory.Discrete.SumsProducts
  {J : Type u_1} {K : Type u_2} (X : CategoryTheory.Discrete J ⊕ CategoryTheory.Discrete K) : CategoryTheory.Discrete.sumEquiv.counitIso.hom.app X = (match X with | Sum.inl x => CategoryTheory.Iso.refl (Sum.inl x) | Sum.inr x => CategoryTheory.Iso.refl (Sum.inr x)).hom
• CategoryTheory.Discrete.sumEquiv_counitIso_inv_app 📋 Mathlib.CategoryTheory.Discrete.SumsProducts
  {J : Type u_1} {K : Type u_2} (X : CategoryTheory.Discrete J ⊕ CategoryTheory.Discrete K) : CategoryTheory.Discrete.sumEquiv.counitIso.inv.app X = (match X with | Sum.inl x => CategoryTheory.Iso.refl (Sum.inl x) | Sum.inr x => CategoryTheory.Iso.refl (Sum.inr x)).inv
• CategoryTheory.Discrete.productEquiv_counitIso_hom_app 📋 Mathlib.CategoryTheory.Discrete.SumsProducts
  {J : Type u_1} {K : Type u_2} (X : CategoryTheory.Discrete J × CategoryTheory.Discrete K) : CategoryTheory.Discrete.productEquiv.counitIso.hom.app X = CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.id X.1) (CategoryTheory.CategoryStruct.id X.2)
• CategoryTheory.Discrete.productEquiv_counitIso_inv_app 📋 Mathlib.CategoryTheory.Discrete.SumsProducts
  {J : Type u_1} {K : Type u_2} (X : CategoryTheory.Discrete J × CategoryTheory.Discrete K) : CategoryTheory.Discrete.productEquiv.counitIso.inv.app X = CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.id X.1) (CategoryTheory.CategoryStruct.id X.2)
• CategoryTheory.FunctorToTypes.binaryCoproductCocone_ι_app 📋 Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes
  {C : Type u} [CategoryTheory.Category.{v, u} C] (F G : CategoryTheory.Functor C (Type w)) (x✝ : CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) : (CategoryTheory.FunctorToTypes.binaryCoproductCocone F G).ι.app x✝ = match x✝.as with | CategoryTheory.Limits.WalkingPair.left => CategoryTheory.FunctorToTypes.coprod.inl | CategoryTheory.Limits.WalkingPair.right => CategoryTheory.FunctorToTypes.coprod.inr
• CategoryTheory.FunctorToTypes.binaryProductCone_π_app 📋 Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes
  {C : Type u} [CategoryTheory.Category.{v, u} C] (F G : CategoryTheory.Functor C (Type w)) (x✝ : CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) : (CategoryTheory.FunctorToTypes.binaryProductCone F G).π.app x✝ = match x✝.as with | CategoryTheory.Limits.WalkingPair.left => CategoryTheory.FunctorToTypes.prod.fst | CategoryTheory.Limits.WalkingPair.right => CategoryTheory.FunctorToTypes.prod.snd
• CategoryTheory.ChosenPullbacksAlong.isoInv_pullback_obj_right_as 📋 Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {Y X : C} (f : Y ≅ X) (Z : CategoryTheory.Over Y) : ((CategoryTheory.ChosenPullbacksAlong.pullback f.inv).obj Z).right.as = PUnit.unit
• CategoryTheory.FreeMonoidalCategory.inclusion_obj 📋 Mathlib.CategoryTheory.Monoidal.Free.Coherence
  {C : Type u} (X : (CategoryTheory.Discrete ∘ CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject) C) : CategoryTheory.FreeMonoidalCategory.inclusion.obj X = CategoryTheory.FreeMonoidalCategory.inclusionObj X.as
• CategoryTheory.FreeMonoidalCategory.as_obj_normalizeObj' 📋 Mathlib.CategoryTheory.Monoidal.Free.Coherence
  {C : Type u} (X : CategoryTheory.FreeMonoidalCategory C) (n : (CategoryTheory.Discrete ∘ CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject) C) : (X.normalizeObj'.obj n).as = X.normalizeObj n.as
• CategoryTheory.FreeMonoidalCategory.normalizeIsoApp_eq 📋 Mathlib.CategoryTheory.Monoidal.Free.Coherence
  (C : Type u) (X : CategoryTheory.FreeMonoidalCategory C) (n : (CategoryTheory.Discrete ∘ CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject) C) : CategoryTheory.FreeMonoidalCategory.normalizeIsoApp C X n = CategoryTheory.FreeMonoidalCategory.normalizeIsoApp' C X n.as
• CategoryTheory.FreeMonoidalCategory.normalizeIsoApp_unitor 📋 Mathlib.CategoryTheory.Monoidal.Free.Coherence
  (C : Type u) (n : (CategoryTheory.Discrete ∘ CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject) C) : CategoryTheory.FreeMonoidalCategory.normalizeIsoApp C (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.FreeMonoidalCategory C)) n = CategoryTheory.MonoidalCategoryStruct.rightUnitor (CategoryTheory.FreeMonoidalCategory.inclusion.obj { as := n.as })
• CategoryTheory.FreeMonoidalCategory.tensorFunc_map_app 📋 Mathlib.CategoryTheory.Monoidal.Free.Coherence
  (C : Type u) {X Y : CategoryTheory.FreeMonoidalCategory C} (f : X ⟶ Y) (n : (CategoryTheory.Discrete ∘ CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject) C) : ((CategoryTheory.FreeMonoidalCategory.tensorFunc C).map f).app n = CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.FreeMonoidalCategory.inclusion.obj { as := n.as }) f
• CategoryTheory.FreeMonoidalCategory.normalizeIsoAux_hom_app 📋 Mathlib.CategoryTheory.Monoidal.Free.Coherence
  (C : Type u) (X : CategoryTheory.FreeMonoidalCategory C) (X✝ : (CategoryTheory.Discrete ∘ CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject) C) : (CategoryTheory.FreeMonoidalCategory.normalizeIsoAux C X).hom.app X✝ = (CategoryTheory.FreeMonoidalCategory.normalizeIsoApp C X X✝).hom
• CategoryTheory.FreeMonoidalCategory.normalizeIsoAux_inv_app 📋 Mathlib.CategoryTheory.Monoidal.Free.Coherence
  (C : Type u) (X : CategoryTheory.FreeMonoidalCategory C) (X✝ : (CategoryTheory.Discrete ∘ CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject) C) : (CategoryTheory.FreeMonoidalCategory.normalizeIsoAux C X).inv.app X✝ = (CategoryTheory.FreeMonoidalCategory.normalizeIsoApp C X X✝).inv
• CategoryTheory.FreeMonoidalCategory.normalizeIsoApp_tensor 📋 Mathlib.CategoryTheory.Monoidal.Free.Coherence
  (C : Type u) (X Y : CategoryTheory.FreeMonoidalCategory C) (n : (CategoryTheory.Discrete ∘ CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject) C) : CategoryTheory.FreeMonoidalCategory.normalizeIsoApp C (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) n = (CategoryTheory.MonoidalCategoryStruct.associator (CategoryTheory.FreeMonoidalCategory.inclusion.obj { as := n.as }) X Y).symm ≪≫ CategoryTheory.MonoidalCategory.whiskerRightIso (CategoryTheory.FreeMonoidalCategory.normalizeIsoApp C X n) Y ≪≫ CategoryTheory.FreeMonoidalCategory.normalizeIsoApp C Y { as := X.normalizeObj n.as }
• CategoryTheory.GrothendieckTopology.pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_obj_obj_obj 📋 Mathlib.CategoryTheory.Sites.PseudofunctorSheafOver
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) (A : Type u') [CategoryTheory.Category.{v', u'} A] {X✝ Y✝ : CategoryTheory.LocallyDiscrete Cᵒᵖ} (f : X✝ ⟶ Y✝) (X : CategoryTheory.Sheaf (J.over (Opposite.unop X✝.as)) A) (X✝¹ : (CategoryTheory.Over (Opposite.unop Y✝.as))ᵒᵖ) : (((J.pseudofunctorOver A).map f).toFunctor.obj X).obj.obj X✝¹ = X.obj.obj (Opposite.op ((CategoryTheory.Over.map f.as.unop).obj (Opposite.unop X✝¹)))
• CategoryTheory.GrothendieckTopology.pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_obj_obj_map 📋 Mathlib.CategoryTheory.Sites.PseudofunctorSheafOver
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) (A : Type u') [CategoryTheory.Category.{v', u'} A] {X✝ Y✝ : CategoryTheory.LocallyDiscrete Cᵒᵖ} (f : X✝ ⟶ Y✝) (X : CategoryTheory.Sheaf (J.over (Opposite.unop X✝.as)) A) {X✝¹ Y✝¹ : (CategoryTheory.Over (Opposite.unop Y✝.as))ᵒᵖ} (f✝ : X✝¹ ⟶ Y✝¹) : (((J.pseudofunctorOver A).map f).toFunctor.obj X).obj.map f✝ = X.obj.map ((CategoryTheory.Over.map f.as.unop).map f✝.unop).op
• CategoryTheory.GrothendieckTopology.pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_map₂ 📋 Mathlib.CategoryTheory.Sites.PseudofunctorSheafOver
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) (A : Type u') [CategoryTheory.Category.{v', u'} A] {a✝ b✝ : CategoryTheory.LocallyDiscrete Cᵒᵖ} {f✝ g✝ : a✝ ⟶ b✝} (φ : f✝ ⟶ g✝) : (J.pseudofunctorOver A).map₂ φ = CategoryTheory.eqToHom ⋯
• CategoryTheory.GrothendieckTopology.pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_map_hom_app 📋 Mathlib.CategoryTheory.Sites.PseudofunctorSheafOver
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) (A : Type u') [CategoryTheory.Category.{v', u'} A] {X✝ Y✝ : CategoryTheory.LocallyDiscrete Cᵒᵖ} (f : X✝ ⟶ Y✝) {X✝¹ Y✝¹ : CategoryTheory.Sheaf (J.over (Opposite.unop X✝.as)) A} (f✝ : X✝¹ ⟶ Y✝¹) (X : (CategoryTheory.Over (Opposite.unop Y✝.as))ᵒᵖ) : (((J.pseudofunctorOver A).map f).toFunctor.map f✝).hom.app X = f✝.hom.app (Opposite.op ((CategoryTheory.Over.map f.as.unop).obj (Opposite.unop X)))
• CategoryTheory.GrothendieckTopology.pseudofunctorOver_mapComp_hom_toNatTrans_app_hom_app 📋 Mathlib.CategoryTheory.Sites.PseudofunctorSheafOver
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) (A : Type u') [CategoryTheory.Category.{v', u'} A] {a✝ b✝ c✝ : CategoryTheory.LocallyDiscrete Cᵒᵖ} (x✝ : a✝ ⟶ b✝) (x✝¹ : b✝ ⟶ c✝) (X : CategoryTheory.Sheaf (J.over (Opposite.unop a✝.as)) A) (X✝ : (CategoryTheory.Over (Opposite.unop c✝.as))ᵒᵖ) : (((J.pseudofunctorOver A).mapComp x✝ x✝¹).hom.toNatTrans.app X).hom.app X✝ = X.obj.map ((CategoryTheory.Over.mapComp x✝¹.as.unop x✝.as.unop).inv.app (Opposite.unop X✝)).op
• CategoryTheory.GrothendieckTopology.pseudofunctorOver_mapComp_inv_toNatTrans_app_hom_app 📋 Mathlib.CategoryTheory.Sites.PseudofunctorSheafOver
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) (A : Type u') [CategoryTheory.Category.{v', u'} A] {a✝ b✝ c✝ : CategoryTheory.LocallyDiscrete Cᵒᵖ} (x✝ : a✝ ⟶ b✝) (x✝¹ : b✝ ⟶ c✝) (X : CategoryTheory.Sheaf (J.over (Opposite.unop a✝.as)) A) (X✝ : (CategoryTheory.Over (Opposite.unop c✝.as))ᵒᵖ) : (((J.pseudofunctorOver A).mapComp x✝ x✝¹).inv.toNatTrans.app X).hom.app X✝ = X.obj.map ((CategoryTheory.Over.mapComp x✝¹.as.unop x✝.as.unop).hom.app (Opposite.unop X✝)).op
• 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✝)

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