Loogle!

Result

Found 75 declarations mentioning CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.snd.

• CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.snd 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
  {A : Type u₁} {B : Type u₂} {C : Type u₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} {X : Type u₄} [CategoryTheory.Category.{v₄, u₄} X] (self : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X) : CategoryTheory.Functor X C
• CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.asSquare 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
  {A : Type u₁} {B : Type u₂} {C : Type u₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} (X : Type u₄) [CategoryTheory.Category.{v₄, u₄} X] (S : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X) : CategoryTheory.CatCommSq S.fst S.snd F G
• CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.iso 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
  {A : Type u₁} {B : Type u₂} {C : Type u₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} {X : Type u₄} [CategoryTheory.Category.{v₄, u₄} X] (self : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X) : self.fst.comp F ≅ self.snd.comp G
• CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.sndFunctor_obj 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
  {A : Type u₁} {B : Type u₂} {C : Type u₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor C B) (X : Type u₄) [CategoryTheory.Category.{v₄, u₄} X] (S : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X) : (CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.sndFunctor F G X).obj S = S.snd
• CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.Hom.snd 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
  {A : Type u₁} {B : Type u₂} {C : Type u₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} {X : Type u₄} [CategoryTheory.Category.{v₄, u₄} X] {x y : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X} (self : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.Hom X x y) : x.snd ⟶ y.snd
• CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.asSquare_iso 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
  {A : Type u₁} {B : Type u₂} {C : Type u₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} (X : Type u₄) [CategoryTheory.Category.{v₄, u₄} X] (S : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X) : CategoryTheory.CatCommSq.iso S.fst S.snd F G = S.iso
• CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.toFunctorToCategoricalPullback_obj_obj_snd 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
  {A : Type u₁} {B : Type u₂} {C : Type u₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor C B) (X : Type u₄) [CategoryTheory.Category.{v₄, u₄} X] (S : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X) (x : X) : (((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.toFunctorToCategoricalPullback F G X).obj S).obj x).snd = S.snd.obj x
• CategoryTheory.Limits.CategoricalPullback.toCatCommSqOver_obj_snd_obj 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
  {A : Type u₁} {B : Type u₂} {C : Type u₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor C B) (X : Type u₄) [CategoryTheory.Category.{v₄, u₄} X] (J : CategoryTheory.Functor X (CategoryTheory.Limits.CategoricalPullback F G)) (X✝ : X) : ((CategoryTheory.Limits.CategoricalPullback.toCatCommSqOver F G X).obj J).snd.obj X✝ = (J.obj X✝).snd
• CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.id_snd_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
  {A : Type u₁} {B : Type u₂} {C : Type u₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} (X : Type u₄) [CategoryTheory.Category.{v₄, u₄} X] (x : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X) (X✝ : X) : (CategoryTheory.CategoryStruct.id x).snd.app X✝ = CategoryTheory.CategoryStruct.id (x.snd.obj X✝)
• CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.sndFunctor_map 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
  {A : Type u₁} {B : Type u₂} {C : Type u₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor C B) (X : Type u₄) [CategoryTheory.Category.{v₄, u₄} X] {X✝ Y✝ : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X} (f : X✝ ⟶ Y✝) : (CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.sndFunctor F G X).map f = f.snd
• CategoryTheory.Limits.CategoricalPullback.functorEquiv_inverse_obj_obj_snd 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
  {A : Type u₁} {B : Type u₂} {C : Type u₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor C B) (X : Type u₄) [CategoryTheory.Category.{v₄, u₄} X] (S : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X) (x : X) : (((CategoryTheory.Limits.CategoricalPullback.functorEquiv F G X).inverse.obj S).obj x).snd = S.snd.obj x
• CategoryTheory.Limits.CategoricalPullback.functorEquiv_functor_obj_snd_obj 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
  {A : Type u₁} {B : Type u₂} {C : Type u₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor C B) (X : Type u₄) [CategoryTheory.Category.{v₄, u₄} X] (J : CategoryTheory.Functor X (CategoryTheory.Limits.CategoricalPullback F G)) (X✝ : X) : ((CategoryTheory.Limits.CategoricalPullback.functorEquiv F G X).functor.obj J).snd.obj X✝ = (J.obj X✝).snd
• CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.Hom.ext 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
  {A : Type u₁} {B : Type u₂} {C : Type u₃} {inst✝ : CategoryTheory.Category.{v₁, u₁} A} {inst✝¹ : CategoryTheory.Category.{v₂, u₂} B} {inst✝² : CategoryTheory.Category.{v₃, u₃} C} {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} {X : Type u₄} {inst✝³ : CategoryTheory.Category.{v₄, u₄} X} {x y : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X} {x✝ y✝ : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.Hom X x y} (fst : x✝.fst = y✝.fst) (snd : x✝.snd = y✝.snd) : x✝ = y✝
• CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.Hom.ext_iff 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
  {A : Type u₁} {B : Type u₂} {C : Type u₃} {inst✝ : CategoryTheory.Category.{v₁, u₁} A} {inst✝¹ : CategoryTheory.Category.{v₂, u₂} B} {inst✝² : CategoryTheory.Category.{v₃, u₃} C} {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} {X : Type u₄} {inst✝³ : CategoryTheory.Category.{v₄, u₄} X} {x y : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X} {x✝ y✝ : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.Hom X x y} : x✝ = y✝ ↔ x✝.fst = y✝.fst ∧ x✝.snd = y✝.snd
• CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose_obj_obj_snd_obj 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
  {A : Type u₁} {B : Type u₂} {C : Type u₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor C B) {X : Type u₄} {Y : Type u₅} [CategoryTheory.Category.{v₄, u₄} X] [CategoryTheory.Category.{v₅, u₅} Y] (U : CategoryTheory.Functor X Y) (S : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G Y) (X✝ : X) : (((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F G).obj U).obj S).snd.obj X✝ = S.snd.obj (U.obj X✝)
• CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform_obj_obj_snd_obj 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
  {A : Type u₁} {B : Type u₂} {C : Type u₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} {A₁ : Type u₄} {B₁ : Type u₅} {C₁ : Type u₆} [CategoryTheory.Category.{v₄, u₄} A₁] [CategoryTheory.Category.{v₅, u₅} B₁] [CategoryTheory.Category.{v₆, u₆} C₁] {F₁ : CategoryTheory.Functor A₁ B₁} {G₁ : CategoryTheory.Functor C₁ B₁} (X : Type u₇) [CategoryTheory.Category.{v₇, u₇} X] (ψ : CategoryTheory.Limits.CatCospanTransform F G F₁ G₁) (S : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X) (X✝ : X) : (((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform X).obj ψ).obj S).snd.obj X✝ = ψ.right.obj (S.snd.obj X✝)
• CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose_obj_obj_snd_map 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
  {A : Type u₁} {B : Type u₂} {C : Type u₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor C B) {X : Type u₄} {Y : Type u₅} [CategoryTheory.Category.{v₄, u₄} X] [CategoryTheory.Category.{v₅, u₅} Y] (U : CategoryTheory.Functor X Y) (S : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G Y) {X✝ Y✝ : X} (f : X✝ ⟶ Y✝) : (((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F G).obj U).obj S).snd.map f = S.snd.map (U.map f)
• CategoryTheory.Limits.CategoricalPullback.toCatCommSqOver_obj_snd_map 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
  {A : Type u₁} {B : Type u₂} {C : Type u₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor C B) (X : Type u₄) [CategoryTheory.Category.{v₄, u₄} X] (J : CategoryTheory.Functor X (CategoryTheory.Limits.CategoricalPullback F G)) {X✝ Y✝ : X} (f : X✝ ⟶ Y✝) : ((CategoryTheory.Limits.CategoricalPullback.toCatCommSqOver F G X).obj J).snd.map f = (J.map f).snd
• CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.hom_ext 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
  {A : Type u₁} {B : Type u₂} {C : Type u₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} (X : Type u₄) [CategoryTheory.Category.{v₄, u₄} X] {S S' : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X} {f g : S ⟶ S'} (h₁ : f.fst = g.fst) (h₂ : f.snd = g.snd) : f = g
• CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.hom_ext_iff 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
  {A : Type u₁} {B : Type u₂} {C : Type u₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} {X : Type u₄} [CategoryTheory.Category.{v₄, u₄} X] {S S' : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X} {f g : S ⟶ S'} : f = g ↔ f.fst = g.fst ∧ f.snd = g.snd
• CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.comp_snd_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
  {A : Type u₁} {B : Type u₂} {C : Type u₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} (X : Type u₄) [CategoryTheory.Category.{v₄, u₄} X] {X✝ Y✝ Z✝ : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X} (f : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.Hom X X✝ Y✝) (g : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.Hom X Y✝ Z✝) (X✝¹ : X) : (CategoryTheory.CategoryStruct.comp f g).snd.app X✝¹ = CategoryTheory.CategoryStruct.comp (f.snd.app X✝¹) (g.snd.app X✝¹)
• CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.toFunctorToCategoricalPullback_obj_obj_iso_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
  {A : Type u₁} {B : Type u₂} {C : Type u₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor C B) (X : Type u₄) [CategoryTheory.Category.{v₄, u₄} X] (S : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X) (x : X) : (((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.toFunctorToCategoricalPullback F G X).obj S).obj x).iso.hom = S.iso.hom.app x
• CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.toFunctorToCategoricalPullback_obj_obj_iso_inv 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
  {A : Type u₁} {B : Type u₂} {C : Type u₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor C B) (X : Type u₄) [CategoryTheory.Category.{v₄, u₄} X] (S : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X) (x : X) : (((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.toFunctorToCategoricalPullback F G X).obj S).obj x).iso.inv = S.iso.inv.app x
• CategoryTheory.Limits.CategoricalPullback.functorEquiv_functor_obj_snd_map 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
  {A : Type u₁} {B : Type u₂} {C : Type u₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor C B) (X : Type u₄) [CategoryTheory.Category.{v₄, u₄} X] (J : CategoryTheory.Functor X (CategoryTheory.Limits.CategoricalPullback F G)) {X✝ Y✝ : X} (f : X✝ ⟶ Y✝) : ((CategoryTheory.Limits.CategoricalPullback.functorEquiv F G X).functor.obj J).snd.map f = (J.map f).snd
• CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.toFunctorToCategoricalPullback_obj_map_fst 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
  {A : Type u₁} {B : Type u₂} {C : Type u₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor C B) (X : Type u₄) [CategoryTheory.Category.{v₄, u₄} X] (S : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X) {x y : X} (f : x ⟶ y) : (((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.toFunctorToCategoricalPullback F G X).obj S).map f).fst = S.fst.map f
• CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.toFunctorToCategoricalPullback_obj_map_snd 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
  {A : Type u₁} {B : Type u₂} {C : Type u₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor C B) (X : Type u₄) [CategoryTheory.Category.{v₄, u₄} X] (S : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X) {x y : X} (f : x ⟶ y) : (((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.toFunctorToCategoricalPullback F G X).obj S).map f).snd = S.snd.map f
• CategoryTheory.Limits.CategoricalPullback.functorEquiv_inverse_obj_obj_iso_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
  {A : Type u₁} {B : Type u₂} {C : Type u₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor C B) (X : Type u₄) [CategoryTheory.Category.{v₄, u₄} X] (S : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X) (x : X) : (((CategoryTheory.Limits.CategoricalPullback.functorEquiv F G X).inverse.obj S).obj x).iso.hom = S.iso.hom.app x
• CategoryTheory.Limits.CategoricalPullback.functorEquiv_inverse_obj_obj_iso_inv 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
  {A : Type u₁} {B : Type u₂} {C : Type u₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor C B) (X : Type u₄) [CategoryTheory.Category.{v₄, u₄} X] (S : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X) (x : X) : (((CategoryTheory.Limits.CategoricalPullback.functorEquiv F G X).inverse.obj S).obj x).iso.inv = S.iso.inv.app x
• CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform_obj_obj_snd_map 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
  {A : Type u₁} {B : Type u₂} {C : Type u₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} {A₁ : Type u₄} {B₁ : Type u₅} {C₁ : Type u₆} [CategoryTheory.Category.{v₄, u₄} A₁] [CategoryTheory.Category.{v₅, u₅} B₁] [CategoryTheory.Category.{v₆, u₆} C₁] {F₁ : CategoryTheory.Functor A₁ B₁} {G₁ : CategoryTheory.Functor C₁ B₁} (X : Type u₇) [CategoryTheory.Category.{v₇, u₇} X] (ψ : CategoryTheory.Limits.CatCospanTransform F G F₁ G₁) (S : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X) {X✝ Y✝ : X} (f : X✝ ⟶ Y✝) : (((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform X).obj ψ).obj S).snd.map f = ψ.right.map (S.snd.map f)
• CategoryTheory.Limits.CategoricalPullback.functorEquiv_inverse_obj_map_fst 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
  {A : Type u₁} {B : Type u₂} {C : Type u₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor C B) (X : Type u₄) [CategoryTheory.Category.{v₄, u₄} X] (S : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X) {x y : X} (f : x ⟶ y) : (((CategoryTheory.Limits.CategoricalPullback.functorEquiv F G X).inverse.obj S).map f).fst = S.fst.map f
• CategoryTheory.Limits.CategoricalPullback.functorEquiv_inverse_obj_map_snd 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
  {A : Type u₁} {B : Type u₂} {C : Type u₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor C B) (X : Type u₄) [CategoryTheory.Category.{v₄, u₄} X] (S : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X) {x y : X} (f : x ⟶ y) : (((CategoryTheory.Limits.CategoricalPullback.functorEquiv F G X).inverse.obj S).map f).snd = S.snd.map f
• CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.Hom.w 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
  {A : Type u₁} {B : Type u₂} {C : Type u₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} {X : Type u₄} [CategoryTheory.Category.{v₄, u₄} X] {x y : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X} (self : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.Hom X x y) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight self.fst F) y.iso.hom = CategoryTheory.CategoryStruct.comp x.iso.hom (CategoryTheory.Functor.whiskerRight self.snd G)
• CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose_obj_obj_iso_hom_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
  {A : Type u₁} {B : Type u₂} {C : Type u₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor C B) {X : Type u₄} {Y : Type u₅} [CategoryTheory.Category.{v₄, u₄} X] [CategoryTheory.Category.{v₅, u₅} Y] (U : CategoryTheory.Functor X Y) (S : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G Y) (X✝ : X) : (((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F G).obj U).obj S).iso.hom.app X✝ = S.iso.hom.app (U.obj X✝)
• CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose_obj_obj_iso_inv_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
  {A : Type u₁} {B : Type u₂} {C : Type u₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor C B) {X : Type u₄} {Y : Type u₅} [CategoryTheory.Category.{v₄, u₄} X] [CategoryTheory.Category.{v₅, u₅} Y] (U : CategoryTheory.Functor X Y) (S : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G Y) (X✝ : X) : (((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F G).obj U).obj S).iso.inv.app X✝ = S.iso.inv.app (U.obj X✝)
• CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.Hom.mk 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
  {A : Type u₁} {B : Type u₂} {C : Type u₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} {X : Type u₄} [CategoryTheory.Category.{v₄, u₄} X] {x y : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X} (fst : x.fst ⟶ y.fst) (snd : x.snd ⟶ y.snd) (w : CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight fst F) y.iso.hom = CategoryTheory.CategoryStruct.comp x.iso.hom (CategoryTheory.Functor.whiskerRight snd G) := by cat_disch) : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.Hom X x y
• CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.Hom.w_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
  {A : Type u₁} {B : Type u₂} {C : Type u₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} {X : Type u₄} [CategoryTheory.Category.{v₄, u₄} X] {x y : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X} (self : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.Hom X x y) {Z : CategoryTheory.Functor X B} (h : y.snd.comp G ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight self.fst F) (CategoryTheory.CategoryStruct.comp y.iso.hom h) = CategoryTheory.CategoryStruct.comp x.iso.hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight self.snd G) h)
• CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.iso_hom_naturality 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
  {A : Type u₁} {B : Type u₂} {C : Type u₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} (X : Type u₄) [CategoryTheory.Category.{v₄, u₄} X] (S : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X) {x x' : X} (f : x ⟶ x') : CategoryTheory.CategoryStruct.comp (F.map (S.fst.map f)) (S.iso.hom.app x') = CategoryTheory.CategoryStruct.comp (S.iso.hom.app x) (G.map (S.snd.map f))
• CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.mkIso 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
  {A : Type u₁} {B : Type u₂} {C : Type u₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} {X : Type u₄} [CategoryTheory.Category.{v₄, u₄} X] {S S' : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X} (eₗ : S.fst ≅ S'.fst) (eᵣ : S.snd ≅ S'.snd) (w : CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight eₗ.hom F) S'.iso.hom = CategoryTheory.CategoryStruct.comp S.iso.hom (CategoryTheory.Functor.whiskerRight eᵣ.hom G) := by cat_disch) : S ≅ S'
• CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.iso_hom_naturality_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
  {A : Type u₁} {B : Type u₂} {C : Type u₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} (X : Type u₄) [CategoryTheory.Category.{v₄, u₄} X] (S : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X) {x x' : X} (f : x ⟶ x') {Z : B} (h : G.obj (S.snd.obj x') ⟶ Z) : CategoryTheory.CategoryStruct.comp (F.map (S.fst.map f)) (CategoryTheory.CategoryStruct.comp (S.iso.hom.app x') h) = CategoryTheory.CategoryStruct.comp (S.iso.hom.app x) (CategoryTheory.CategoryStruct.comp (G.map (S.snd.map f)) h)
• CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.w_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
  {A : Type u₁} {B : Type u₂} {C : Type u₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} (X : Type u₄) [CategoryTheory.Category.{v₄, u₄} X] {S S' : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X} (φ : S ⟶ S') (x : X) : CategoryTheory.CategoryStruct.comp (F.map (φ.fst.app x)) (S'.iso.hom.app x) = CategoryTheory.CategoryStruct.comp (S.iso.hom.app x) (G.map (φ.snd.app x))
• CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.mkIso_hom_fst 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
  {A : Type u₁} {B : Type u₂} {C : Type u₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} {X : Type u₄} [CategoryTheory.Category.{v₄, u₄} X] {S S' : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X} (eₗ : S.fst ≅ S'.fst) (eᵣ : S.snd ≅ S'.snd) (w : CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight eₗ.hom F) S'.iso.hom = CategoryTheory.CategoryStruct.comp S.iso.hom (CategoryTheory.Functor.whiskerRight eᵣ.hom G) := by cat_disch) : (CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.mkIso eₗ eᵣ w).hom.fst = eₗ.hom
• CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.mkIso_hom_snd 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
  {A : Type u₁} {B : Type u₂} {C : Type u₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} {X : Type u₄} [CategoryTheory.Category.{v₄, u₄} X] {S S' : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X} (eₗ : S.fst ≅ S'.fst) (eᵣ : S.snd ≅ S'.snd) (w : CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight eₗ.hom F) S'.iso.hom = CategoryTheory.CategoryStruct.comp S.iso.hom (CategoryTheory.Functor.whiskerRight eᵣ.hom G) := by cat_disch) : (CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.mkIso eₗ eᵣ w).hom.snd = eᵣ.hom
• CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.mkIso_inv_fst 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
  {A : Type u₁} {B : Type u₂} {C : Type u₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} {X : Type u₄} [CategoryTheory.Category.{v₄, u₄} X] {S S' : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X} (eₗ : S.fst ≅ S'.fst) (eᵣ : S.snd ≅ S'.snd) (w : CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight eₗ.hom F) S'.iso.hom = CategoryTheory.CategoryStruct.comp S.iso.hom (CategoryTheory.Functor.whiskerRight eᵣ.hom G) := by cat_disch) : (CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.mkIso eₗ eᵣ w).inv.fst = eₗ.inv
• CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.mkIso_inv_snd 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
  {A : Type u₁} {B : Type u₂} {C : Type u₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} {X : Type u₄} [CategoryTheory.Category.{v₄, u₄} X] {S S' : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X} (eₗ : S.fst ≅ S'.fst) (eᵣ : S.snd ≅ S'.snd) (w : CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight eₗ.hom F) S'.iso.hom = CategoryTheory.CategoryStruct.comp S.iso.hom (CategoryTheory.Functor.whiskerRight eᵣ.hom G) := by cat_disch) : (CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.mkIso eₗ eᵣ w).inv.snd = eᵣ.inv
• CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.w_app_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
  {A : Type u₁} {B : Type u₂} {C : Type u₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} (X : Type u₄) [CategoryTheory.Category.{v₄, u₄} X] {S S' : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X} (φ : S ⟶ S') (x : X) {Z : B} (h : G.obj (S'.snd.obj x) ⟶ Z) : CategoryTheory.CategoryStruct.comp (F.map (φ.fst.app x)) (CategoryTheory.CategoryStruct.comp (S'.iso.hom.app x) h) = CategoryTheory.CategoryStruct.comp (S.iso.hom.app x) (CategoryTheory.CategoryStruct.comp (G.map (φ.snd.app x)) h)
• CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.e_hom_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
  {A : Type u₁} {B : Type u₂} {C : Type u₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor C B) (X : Type u₄) [CategoryTheory.Category.{v₄, u₄} X] (X✝ : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X) : (CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.e F G X).hom.app X✝ = X✝.iso.hom
• CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.e_inv_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
  {A : Type u₁} {B : Type u₂} {C : Type u₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor C B) (X : Type u₄) [CategoryTheory.Category.{v₄, u₄} X] (X✝ : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X) : (CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.e F G X).inv.app X✝ = X✝.iso.inv
• CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precomposeObjId_hom_app_snd_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
  {A : Type u₁} {B : Type u₂} {C : Type u₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor C B) (X : Type u₄) [CategoryTheory.Category.{v₄, u₄} X] (X✝ : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X) (X✝¹ : X) : ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precomposeObjId F G X).hom.app X✝).snd.app X✝¹ = CategoryTheory.CategoryStruct.id (X✝.snd.obj X✝¹)
• CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precomposeObjId_inv_app_snd_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
  {A : Type u₁} {B : Type u₂} {C : Type u₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor C B) (X : Type u₄) [CategoryTheory.Category.{v₄, u₄} X] (X✝ : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X) (X✝¹ : X) : ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precomposeObjId F G X).inv.app X✝).snd.app X✝¹ = CategoryTheory.CategoryStruct.id (X✝.snd.obj X✝¹)
• CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transformObjId_hom_app_snd_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
  {A : Type u₁} {B : Type u₂} {C : Type u₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] (X : Type u₄) [CategoryTheory.Category.{v₄, u₄} X] (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor C B) (X✝ : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X) (X✝¹ : X) : ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transformObjId X F G).hom.app X✝).snd.app X✝¹ = CategoryTheory.CategoryStruct.id (X✝.snd.obj X✝¹)
• CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transformObjId_inv_app_snd_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
  {A : Type u₁} {B : Type u₂} {C : Type u₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] (X : Type u₄) [CategoryTheory.Category.{v₄, u₄} X] (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor C B) (X✝ : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X) (X✝¹ : X) : ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transformObjId X F G).inv.app X✝).snd.app X✝¹ = CategoryTheory.CategoryStruct.id (X✝.snd.obj X✝¹)
• CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose_obj_map_fst_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
  {A : Type u₁} {B : Type u₂} {C : Type u₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor C B) {X : Type u₄} {Y : Type u₅} [CategoryTheory.Category.{v₄, u₄} X] [CategoryTheory.Category.{v₅, u₅} Y] (U : CategoryTheory.Functor X Y) {S S' : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G Y} (φ : S ⟶ S') (X✝ : X) : (((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F G).obj U).map φ).fst.app X✝ = φ.fst.app (U.obj X✝)
• CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose_obj_map_snd_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
  {A : Type u₁} {B : Type u₂} {C : Type u₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor C B) {X : Type u₄} {Y : Type u₅} [CategoryTheory.Category.{v₄, u₄} X] [CategoryTheory.Category.{v₅, u₅} Y] (U : CategoryTheory.Functor X Y) {S S' : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G Y} (φ : S ⟶ S') (X✝ : X) : (((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F G).obj U).map φ).snd.app X✝ = φ.snd.app (U.obj X✝)
• CategoryTheory.Limits.CategoricalPullback.functorEquiv_counitIso_hom_app_snd_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
  {A : Type u₁} {B : Type u₂} {C : Type u₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor C B) (X : Type u₄) [CategoryTheory.Category.{v₄, u₄} X] (X✝ : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X) (X✝¹ : X) : ((CategoryTheory.Limits.CategoricalPullback.functorEquiv F G X).counitIso.hom.app X✝).snd.app X✝¹ = CategoryTheory.CategoryStruct.id (X✝.snd.obj X✝¹)
• CategoryTheory.Limits.CategoricalPullback.functorEquiv_counitIso_inv_app_snd_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
  {A : Type u₁} {B : Type u₂} {C : Type u₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor C B) (X : Type u₄) [CategoryTheory.Category.{v₄, u₄} X] (X✝ : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X) (X✝¹ : X) : ((CategoryTheory.Limits.CategoricalPullback.functorEquiv F G X).counitIso.inv.app X✝).snd.app X✝¹ = CategoryTheory.CategoryStruct.id (X✝.snd.obj X✝¹)
• CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform_obj_obj_iso_hom_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
  {A : Type u₁} {B : Type u₂} {C : Type u₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} {A₁ : Type u₄} {B₁ : Type u₅} {C₁ : Type u₆} [CategoryTheory.Category.{v₄, u₄} A₁] [CategoryTheory.Category.{v₅, u₅} B₁] [CategoryTheory.Category.{v₆, u₆} C₁] {F₁ : CategoryTheory.Functor A₁ B₁} {G₁ : CategoryTheory.Functor C₁ B₁} (X : Type u₇) [CategoryTheory.Category.{v₇, u₇} X] (ψ : CategoryTheory.Limits.CatCospanTransform F G F₁ G₁) (S : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X) (X✝ : X) : (((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform X).obj ψ).obj S).iso.hom.app X✝ = CategoryTheory.CategoryStruct.comp ((CategoryTheory.CatCommSq.iso F ψ.left ψ.base F₁).inv.app (S.fst.obj X✝)) (CategoryTheory.CategoryStruct.comp (ψ.base.map (S.iso.hom.app X✝)) ((CategoryTheory.CatCommSq.iso G ψ.right ψ.base G₁).hom.app (S.snd.obj X✝)))
• CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform_obj_obj_iso_inv_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
  {A : Type u₁} {B : Type u₂} {C : Type u₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} {A₁ : Type u₄} {B₁ : Type u₅} {C₁ : Type u₆} [CategoryTheory.Category.{v₄, u₄} A₁] [CategoryTheory.Category.{v₅, u₅} B₁] [CategoryTheory.Category.{v₆, u₆} C₁] {F₁ : CategoryTheory.Functor A₁ B₁} {G₁ : CategoryTheory.Functor C₁ B₁} (X : Type u₇) [CategoryTheory.Category.{v₇, u₇} X] (ψ : CategoryTheory.Limits.CatCospanTransform F G F₁ G₁) (S : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X) (X✝ : X) : (((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform X).obj ψ).obj S).iso.inv.app X✝ = CategoryTheory.CategoryStruct.comp ((CategoryTheory.CatCommSq.iso G ψ.right ψ.base G₁).inv.app (S.snd.obj X✝)) (CategoryTheory.CategoryStruct.comp (ψ.base.map (S.iso.inv.app X✝)) ((CategoryTheory.CatCommSq.iso F ψ.left ψ.base F₁).hom.app (S.fst.obj X✝)))
• CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.toFunctorToCategoricalPullback_map_app_fst 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
  {A : Type u₁} {B : Type u₂} {C : Type u₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor C B) (X : Type u₄) [CategoryTheory.Category.{v₄, u₄} X] {S S' : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X} (φ : S ⟶ S') (x : X) : (((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.toFunctorToCategoricalPullback F G X).map φ).app x).fst = φ.fst.app x
• CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.toFunctorToCategoricalPullback_map_app_snd 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
  {A : Type u₁} {B : Type u₂} {C : Type u₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor C B) (X : Type u₄) [CategoryTheory.Category.{v₄, u₄} X] {S S' : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X} (φ : S ⟶ S') (x : X) : (((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.toFunctorToCategoricalPullback F G X).map φ).app x).snd = φ.snd.app x
• CategoryTheory.Limits.CategoricalPullback.functorEquiv_inverse_map_app_fst 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
  {A : Type u₁} {B : Type u₂} {C : Type u₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor C B) (X : Type u₄) [CategoryTheory.Category.{v₄, u₄} X] {S S' : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X} (φ : S ⟶ S') (x : X) : (((CategoryTheory.Limits.CategoricalPullback.functorEquiv F G X).inverse.map φ).app x).fst = φ.fst.app x
• CategoryTheory.Limits.CategoricalPullback.functorEquiv_inverse_map_app_snd 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
  {A : Type u₁} {B : Type u₂} {C : Type u₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor C B) (X : Type u₄) [CategoryTheory.Category.{v₄, u₄} X] {S S' : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X} (φ : S ⟶ S') (x : X) : (((CategoryTheory.Limits.CategoricalPullback.functorEquiv F G X).inverse.map φ).app x).snd = φ.snd.app x
• CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precomposeObjComp_hom_app_snd_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
  {A : Type u₁} {B : Type u₂} {C : Type u₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor C B) {X : Type u₄} {Y : Type u₅} {Z : Type u₆} [CategoryTheory.Category.{v₄, u₄} X] [CategoryTheory.Category.{v₅, u₅} Y] [CategoryTheory.Category.{v₆, u₆} Z] (U : CategoryTheory.Functor X Y) (V : CategoryTheory.Functor Y Z) (X✝ : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G Z) (x✝ : X) : ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precomposeObjComp F G U V).hom.app X✝).snd.app x✝ = CategoryTheory.CategoryStruct.id (X✝.snd.obj (V.obj (U.obj x✝)))
• CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precomposeObjComp_inv_app_snd_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
  {A : Type u₁} {B : Type u₂} {C : Type u₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor C B) {X : Type u₄} {Y : Type u₅} {Z : Type u₆} [CategoryTheory.Category.{v₄, u₄} X] [CategoryTheory.Category.{v₅, u₅} Y] [CategoryTheory.Category.{v₆, u₆} Z] (U : CategoryTheory.Functor X Y) (V : CategoryTheory.Functor Y Z) (X✝ : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G Z) (x✝ : X) : ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precomposeObjComp F G U V).inv.app X✝).snd.app x✝ = CategoryTheory.CategoryStruct.id (X✝.snd.obj (V.obj (U.obj x✝)))
• CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transformObjComp_hom_app_snd_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
  {A : Type u₁} {B : Type u₂} {C : Type u₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} {A₁ : Type u₄} {B₁ : Type u₅} {C₁ : Type u₆} [CategoryTheory.Category.{v₄, u₄} A₁] [CategoryTheory.Category.{v₅, u₅} B₁] [CategoryTheory.Category.{v₆, u₆} C₁] {F₁ : CategoryTheory.Functor A₁ B₁} {G₁ : CategoryTheory.Functor C₁ B₁} {A₂ : Type u₇} {B₂ : Type u₈} {C₂ : Type u₉} [CategoryTheory.Category.{v₇, u₇} A₂] [CategoryTheory.Category.{v₈, u₈} B₂] [CategoryTheory.Category.{v₉, u₉} C₂] {F₂ : CategoryTheory.Functor A₂ B₂} {G₂ : CategoryTheory.Functor C₂ B₂} (X : Type u₁₀) [CategoryTheory.Category.{v₁₀, u₁₀} X] (ψ : CategoryTheory.Limits.CatCospanTransform F G F₁ G₁) (ψ' : CategoryTheory.Limits.CatCospanTransform F₁ G₁ F₂ G₂) (X✝ : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X) (x✝ : X) : ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transformObjComp X ψ ψ').hom.app X✝).snd.app x✝ = CategoryTheory.CategoryStruct.id (ψ'.right.obj (ψ.right.obj (X✝.snd.obj x✝)))
• CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transformObjComp_inv_app_snd_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
  {A : Type u₁} {B : Type u₂} {C : Type u₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} {A₁ : Type u₄} {B₁ : Type u₅} {C₁ : Type u₆} [CategoryTheory.Category.{v₄, u₄} A₁] [CategoryTheory.Category.{v₅, u₅} B₁] [CategoryTheory.Category.{v₆, u₆} C₁] {F₁ : CategoryTheory.Functor A₁ B₁} {G₁ : CategoryTheory.Functor C₁ B₁} {A₂ : Type u₇} {B₂ : Type u₈} {C₂ : Type u₉} [CategoryTheory.Category.{v₇, u₇} A₂] [CategoryTheory.Category.{v₈, u₈} B₂] [CategoryTheory.Category.{v₉, u₉} C₂] {F₂ : CategoryTheory.Functor A₂ B₂} {G₂ : CategoryTheory.Functor C₂ B₂} (X : Type u₁₀) [CategoryTheory.Category.{v₁₀, u₁₀} X] (ψ : CategoryTheory.Limits.CatCospanTransform F G F₁ G₁) (ψ' : CategoryTheory.Limits.CatCospanTransform F₁ G₁ F₂ G₂) (X✝ : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X) (x✝ : X) : ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transformObjComp X ψ ψ').inv.app X✝).snd.app x✝ = CategoryTheory.CategoryStruct.id (ψ'.right.obj (ψ.right.obj (X✝.snd.obj x✝)))
• CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precomposeObjTransformObjSquare_iso_hom_app_snd_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
  {A : Type u₁} {B : Type u₂} {C : Type u₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} {A₁ : Type u₄} {B₁ : Type u₅} {C₁ : Type u₆} [CategoryTheory.Category.{v₄, u₄} A₁] [CategoryTheory.Category.{v₅, u₅} B₁] [CategoryTheory.Category.{v₆, u₆} C₁] {F₁ : CategoryTheory.Functor A₁ B₁} {G₁ : CategoryTheory.Functor C₁ B₁} {X : Type u₇} {Y : Type u₈} [CategoryTheory.Category.{v₇, u₇} X] [CategoryTheory.Category.{v₈, u₈} Y] (ψ : CategoryTheory.Limits.CatCospanTransform F G F₁ G₁) (U : CategoryTheory.Functor X Y) (X✝ : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G Y) (x✝ : X) : ((CategoryTheory.CatCommSq.iso ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F G).obj U) ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform Y).obj ψ) ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform X).obj ψ) ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F₁ G₁).obj U)).hom.app X✝).snd.app x✝ = CategoryTheory.CategoryStruct.id (ψ.right.obj (X✝.snd.obj (U.obj x✝)))
• CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precomposeObjTransformObjSquare_iso_inv_app_snd_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
  {A : Type u₁} {B : Type u₂} {C : Type u₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} {A₁ : Type u₄} {B₁ : Type u₅} {C₁ : Type u₆} [CategoryTheory.Category.{v₄, u₄} A₁] [CategoryTheory.Category.{v₅, u₅} B₁] [CategoryTheory.Category.{v₆, u₆} C₁] {F₁ : CategoryTheory.Functor A₁ B₁} {G₁ : CategoryTheory.Functor C₁ B₁} {X : Type u₇} {Y : Type u₈} [CategoryTheory.Category.{v₇, u₇} X] [CategoryTheory.Category.{v₈, u₈} Y] (ψ : CategoryTheory.Limits.CatCospanTransform F G F₁ G₁) (U : CategoryTheory.Functor X Y) (X✝ : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G Y) (x✝ : X) : ((CategoryTheory.CatCommSq.iso ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F G).obj U) ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform Y).obj ψ) ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform X).obj ψ) ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F₁ G₁).obj U)).inv.app X✝).snd.app x✝ = CategoryTheory.CategoryStruct.id (ψ.right.obj (X✝.snd.obj (U.obj x✝)))
• CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transformObjPrecomposeObjSquare_iso_hom_app_snd_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
  {A : Type u₁} {B : Type u₂} {C : Type u₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} {A₁ : Type u₄} {B₁ : Type u₅} {C₁ : Type u₆} [CategoryTheory.Category.{v₄, u₄} A₁] [CategoryTheory.Category.{v₅, u₅} B₁] [CategoryTheory.Category.{v₆, u₆} C₁] {F₁ : CategoryTheory.Functor A₁ B₁} {G₁ : CategoryTheory.Functor C₁ B₁} {X : Type u₇} {Y : Type u₈} [CategoryTheory.Category.{v₇, u₇} X] [CategoryTheory.Category.{v₈, u₈} Y] (U : CategoryTheory.Functor X Y) (ψ : CategoryTheory.Limits.CatCospanTransform F G F₁ G₁) (X✝ : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G Y) (x✝ : X) : ((CategoryTheory.CatCommSq.iso ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform Y).obj ψ) ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F G).obj U) ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F₁ G₁).obj U) ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform X).obj ψ)).hom.app X✝).snd.app x✝ = CategoryTheory.CategoryStruct.id (ψ.right.obj (X✝.snd.obj (U.obj x✝)))
• CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transformObjPrecomposeObjSquare_iso_inv_app_snd_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
  {A : Type u₁} {B : Type u₂} {C : Type u₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} {A₁ : Type u₄} {B₁ : Type u₅} {C₁ : Type u₆} [CategoryTheory.Category.{v₄, u₄} A₁] [CategoryTheory.Category.{v₅, u₅} B₁] [CategoryTheory.Category.{v₆, u₆} C₁] {F₁ : CategoryTheory.Functor A₁ B₁} {G₁ : CategoryTheory.Functor C₁ B₁} {X : Type u₇} {Y : Type u₈} [CategoryTheory.Category.{v₇, u₇} X] [CategoryTheory.Category.{v₈, u₈} Y] (U : CategoryTheory.Functor X Y) (ψ : CategoryTheory.Limits.CatCospanTransform F G F₁ G₁) (X✝ : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G Y) (x✝ : X) : ((CategoryTheory.CatCommSq.iso ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform Y).obj ψ) ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F G).obj U) ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F₁ G₁).obj U) ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform X).obj ψ)).inv.app X✝).snd.app x✝ = CategoryTheory.CategoryStruct.id (ψ.right.obj (X✝.snd.obj (U.obj x✝)))
• CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform_obj_map_fst_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
  {A : Type u₁} {B : Type u₂} {C : Type u₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} {A₁ : Type u₄} {B₁ : Type u₅} {C₁ : Type u₆} [CategoryTheory.Category.{v₄, u₄} A₁] [CategoryTheory.Category.{v₅, u₅} B₁] [CategoryTheory.Category.{v₆, u₆} C₁] {F₁ : CategoryTheory.Functor A₁ B₁} {G₁ : CategoryTheory.Functor C₁ B₁} (X : Type u₇) [CategoryTheory.Category.{v₇, u₇} X] (ψ : CategoryTheory.Limits.CatCospanTransform F G F₁ G₁) {x y : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X} (f : x ⟶ y) (X✝ : X) : (((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform X).obj ψ).map f).fst.app X✝ = ψ.left.map (f.fst.app X✝)
• CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform_obj_map_snd_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
  {A : Type u₁} {B : Type u₂} {C : Type u₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} {A₁ : Type u₄} {B₁ : Type u₅} {C₁ : Type u₆} [CategoryTheory.Category.{v₄, u₄} A₁] [CategoryTheory.Category.{v₅, u₅} B₁] [CategoryTheory.Category.{v₆, u₆} C₁] {F₁ : CategoryTheory.Functor A₁ B₁} {G₁ : CategoryTheory.Functor C₁ B₁} (X : Type u₇) [CategoryTheory.Category.{v₇, u₇} X] (ψ : CategoryTheory.Limits.CatCospanTransform F G F₁ G₁) {x y : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X} (f : x ⟶ y) (X✝ : X) : (((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform X).obj ψ).map f).snd.app X✝ = ψ.right.map (f.snd.app X✝)
• CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose_map_app_fst_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
  {A : Type u₁} {B : Type u₂} {C : Type u₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor C B) {X : Type u₄} {Y : Type u₅} [CategoryTheory.Category.{v₄, u₄} X] [CategoryTheory.Category.{v₅, u₅} Y] {U V : CategoryTheory.Functor X Y} (α : U ⟶ V) (x : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G Y) (X✝ : X) : (((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F G).map α).app x).fst.app X✝ = x.fst.map (α.app X✝)
• CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose_map_app_snd_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
  {A : Type u₁} {B : Type u₂} {C : Type u₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor C B) {X : Type u₄} {Y : Type u₅} [CategoryTheory.Category.{v₄, u₄} X] [CategoryTheory.Category.{v₅, u₅} Y] {U V : CategoryTheory.Functor X Y} (α : U ⟶ V) (x : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G Y) (X✝ : X) : (((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F G).map α).app x).snd.app X✝ = x.snd.map (α.app X✝)
• CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform_map_app_fst_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
  {A : Type u₁} {B : Type u₂} {C : Type u₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} {A₁ : Type u₄} {B₁ : Type u₅} {C₁ : Type u₆} [CategoryTheory.Category.{v₄, u₄} A₁] [CategoryTheory.Category.{v₅, u₅} B₁] [CategoryTheory.Category.{v₆, u₆} C₁] {F₁ : CategoryTheory.Functor A₁ B₁} {G₁ : CategoryTheory.Functor C₁ B₁} (X : Type u₇) [CategoryTheory.Category.{v₇, u₇} X] {ψ ψ' : CategoryTheory.Limits.CatCospanTransform F G F₁ G₁} (η : ψ ⟶ ψ') (S : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X) (y : X) : (((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform X).map η).app S).fst.app y = η.left.app (S.fst.obj y)
• CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform_map_app_snd_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
  {A : Type u₁} {B : Type u₂} {C : Type u₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} {A₁ : Type u₄} {B₁ : Type u₅} {C₁ : Type u₆} [CategoryTheory.Category.{v₄, u₄} A₁] [CategoryTheory.Category.{v₅, u₅} B₁] [CategoryTheory.Category.{v₆, u₆} C₁] {F₁ : CategoryTheory.Functor A₁ B₁} {G₁ : CategoryTheory.Functor C₁ B₁} (X : Type u₇) [CategoryTheory.Category.{v₇, u₇} X] {ψ ψ' : CategoryTheory.Limits.CatCospanTransform F G F₁ G₁} (η : ψ ⟶ ψ') (S : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X) (y : X) : (((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform X).map η).app S).snd.app y = η.right.app (S.snd.obj y)

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