Loogle!

Result

Found 138 declarations mentioning CategoryTheory.Limits.MulticospanIndex.left.

• CategoryTheory.Limits.MulticospanIndex.left 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {J : CategoryTheory.Limits.MulticospanShape} {C : Type u} [CategoryTheory.Category.{v, u} C] (self : CategoryTheory.Limits.MulticospanIndex J C) : J.L → C
• CategoryTheory.Limits.MulticospanIndex.fst 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {J : CategoryTheory.Limits.MulticospanShape} {C : Type u} [CategoryTheory.Category.{v, u} C] (self : CategoryTheory.Limits.MulticospanIndex J C) (b : J.R) : self.left (J.fst b) ⟶ self.right b
• CategoryTheory.Limits.MulticospanIndex.snd 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {J : CategoryTheory.Limits.MulticospanShape} {C : Type u} [CategoryTheory.Category.{v, u} C] (self : CategoryTheory.Limits.MulticospanIndex J C) (b : J.R) : self.left (J.snd b) ⟶ self.right b
• CategoryTheory.Limits.MulticospanIndex.multicospan_obj_left 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) (a : J.L) : I.multicospan.obj (CategoryTheory.Limits.WalkingMulticospan.left a) = I.left a
• CategoryTheory.Limits.MulticospanIndex.parallelPairDiagram 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] : CategoryTheory.Functor CategoryTheory.Limits.WalkingParallelPair C
• CategoryTheory.Limits.Multiequalizer.ι 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) [CategoryTheory.Limits.HasMultiequalizer I] (a : J.L) : CategoryTheory.Limits.multiequalizer I ⟶ I.left a
• CategoryTheory.Limits.Multifork.ι 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} {I : CategoryTheory.Limits.MulticospanIndex J C} (K : CategoryTheory.Limits.Multifork I) (a : J.L) : K.pt ⟶ I.left a
• CategoryTheory.Limits.MulticospanIndex.ofParallelHoms_left 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.Limits.MulticospanShape) {X Y : C} (f g : X ⟶ Y) (x✝ : J.L) : (CategoryTheory.Limits.MulticospanIndex.ofParallelHoms J f g).left x✝ = X
• CategoryTheory.Limits.MulticospanIndex.parallelPairDiagramOfIsLimit 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) (c : CategoryTheory.Limits.Fan I.left) {d : CategoryTheory.Limits.Fan I.right} (hd : CategoryTheory.Limits.IsLimit d) : CategoryTheory.Functor CategoryTheory.Limits.WalkingParallelPair C
• CategoryTheory.Limits.MulticospanIndex.fstPiMap 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] : ∏ᶜ I.left ⟶ ∏ᶜ I.right
• CategoryTheory.Limits.MulticospanIndex.sndPiMap 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] : ∏ᶜ I.left ⟶ ∏ᶜ I.right
• CategoryTheory.Limits.Multiequalizer.ιPi 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) [CategoryTheory.Limits.HasMultiequalizer I] [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] : CategoryTheory.Limits.multiequalizer I ⟶ ∏ᶜ I.left
• CategoryTheory.Limits.Multiequalizer.instMonoιPi 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) [CategoryTheory.Limits.HasMultiequalizer I] [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] : CategoryTheory.Mono (CategoryTheory.Limits.Multiequalizer.ιPi I)
• CategoryTheory.Limits.Multiequalizer.multifork_ι 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) [CategoryTheory.Limits.HasMultiequalizer I] (a : J.L) : (CategoryTheory.Limits.Multiequalizer.multifork I).ι a = CategoryTheory.Limits.Multiequalizer.ι I a
• CategoryTheory.Limits.MulticospanIndex.parallelPairDiagram_obj 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] (x : CategoryTheory.Limits.WalkingParallelPair) : I.parallelPairDiagram.obj x = CategoryTheory.Limits.parallelPair.parallelPairObj (∏ᶜ I.left) (∏ᶜ I.right) x
• CategoryTheory.Limits.Multiequalizer.instHasEqualizerFstPiMapSndPiMap 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) [CategoryTheory.Limits.HasMultiequalizer I] [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] : CategoryTheory.Limits.HasEqualizer I.fstPiMap I.sndPiMap
• CategoryTheory.Limits.Multiequalizer.isoEqualizer 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) [CategoryTheory.Limits.HasMultiequalizer I] [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] : CategoryTheory.Limits.multiequalizer I ≅ CategoryTheory.Limits.equalizer I.fstPiMap I.sndPiMap
• CategoryTheory.Limits.MulticospanIndex.fstPiMapOfIsLimit 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) (c : CategoryTheory.Limits.Fan I.left) {d : CategoryTheory.Limits.Fan I.right} (hd : CategoryTheory.Limits.IsLimit d) : c.pt ⟶ d.pt
• CategoryTheory.Limits.MulticospanIndex.sndPiMapOfIsLimit 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) (c : CategoryTheory.Limits.Fan I.left) {d : CategoryTheory.Limits.Fan I.right} (hd : CategoryTheory.Limits.IsLimit d) : c.pt ⟶ d.pt
• CategoryTheory.Limits.Multifork.ofι 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) (P : C) (ι : (a : J.L) → P ⟶ I.left a) (w : ∀ (b : J.R), CategoryTheory.CategoryStruct.comp (ι (J.fst b)) (I.fst b) = CategoryTheory.CategoryStruct.comp (ι (J.snd b)) (I.snd b)) : CategoryTheory.Limits.Multifork I
• CategoryTheory.Limits.MulticospanIndex.parallelPairDiagramOfIsLimit_obj 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) (c : CategoryTheory.Limits.Fan I.left) {d : CategoryTheory.Limits.Fan I.right} (hd : CategoryTheory.Limits.IsLimit d) (x : CategoryTheory.Limits.WalkingParallelPair) : (I.parallelPairDiagramOfIsLimit c hd).obj x = CategoryTheory.Limits.parallelPair.parallelPairObj c.pt d.pt x
• CategoryTheory.Limits.Multiequalizer.ιPi_π 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) [CategoryTheory.Limits.HasMultiequalizer I] [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] (a : J.L) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multiequalizer.ιPi I) (CategoryTheory.Limits.Pi.π I.left a) = CategoryTheory.Limits.Multiequalizer.ι I a
• CategoryTheory.Limits.Multifork.ofPiFork 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} {I : CategoryTheory.Limits.MulticospanIndex J C} {c : CategoryTheory.Limits.Fan I.left} {d : CategoryTheory.Limits.Fan I.right} {hd : CategoryTheory.Limits.IsLimit d} (a : CategoryTheory.Limits.Fork (I.fstPiMapOfIsLimit c hd) (I.sndPiMapOfIsLimit c hd)) : CategoryTheory.Limits.Multifork I
• CategoryTheory.Limits.Multiequalizer.condition 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) [CategoryTheory.Limits.HasMultiequalizer I] (b : J.R) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multiequalizer.ι I (J.fst b)) (I.fst b) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multiequalizer.ι I (J.snd b)) (I.snd b)
• CategoryTheory.Limits.Multiequalizer.lift 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) [CategoryTheory.Limits.HasMultiequalizer I] (W : C) (k : (a : J.L) → W ⟶ I.left a) (h : ∀ (b : J.R), CategoryTheory.CategoryStruct.comp (k (J.fst b)) (I.fst b) = CategoryTheory.CategoryStruct.comp (k (J.snd b)) (I.snd b)) : W ⟶ CategoryTheory.Limits.multiequalizer I
• CategoryTheory.Limits.Multifork.ofι_pt 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) (P : C) (ι : (a : J.L) → P ⟶ I.left a) (w : ∀ (b : J.R), CategoryTheory.CategoryStruct.comp (ι (J.fst b)) (I.fst b) = CategoryTheory.CategoryStruct.comp (ι (J.snd b)) (I.snd b)) : (CategoryTheory.Limits.Multifork.ofι I P ι w).pt = P
• CategoryTheory.Limits.Multiequalizer.hom_ext 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) [CategoryTheory.Limits.HasMultiequalizer I] {W : C} (i j : W ⟶ CategoryTheory.Limits.multiequalizer I) (h : ∀ (a : J.L), CategoryTheory.CategoryStruct.comp i (CategoryTheory.Limits.Multiequalizer.ι I a) = CategoryTheory.CategoryStruct.comp j (CategoryTheory.Limits.Multiequalizer.ι I a)) : i = j
• CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiFork 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] : CategoryTheory.Limits.Multifork I ≌ CategoryTheory.Limits.Fork I.fstPiMap I.sndPiMap
• CategoryTheory.Limits.Multiequalizer.hom_ext_iff 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} {I : CategoryTheory.Limits.MulticospanIndex J C} [CategoryTheory.Limits.HasMultiequalizer I] {W : C} {i j : W ⟶ CategoryTheory.Limits.multiequalizer I} : i = j ↔ ∀ (a : J.L), CategoryTheory.CategoryStruct.comp i (CategoryTheory.Limits.Multiequalizer.ι I a) = CategoryTheory.CategoryStruct.comp j (CategoryTheory.Limits.Multiequalizer.ι I a)
• CategoryTheory.Limits.Multifork.toPiFork 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} {I : CategoryTheory.Limits.MulticospanIndex J C} {c : CategoryTheory.Limits.Fan I.left} (hc : CategoryTheory.Limits.IsLimit c) {d : CategoryTheory.Limits.Fan I.right} (hd : CategoryTheory.Limits.IsLimit d) (K : CategoryTheory.Limits.Multifork I) : CategoryTheory.Limits.Fork (I.fstPiMapOfIsLimit c hd) (I.sndPiMapOfIsLimit c hd)
• CategoryTheory.Limits.Multifork.condition 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} {I : CategoryTheory.Limits.MulticospanIndex J C} (K : CategoryTheory.Limits.Multifork I) (b : J.R) : CategoryTheory.CategoryStruct.comp (K.ι (J.fst b)) (I.fst b) = CategoryTheory.CategoryStruct.comp (K.ι (J.snd b)) (I.snd b)
• CategoryTheory.Limits.Multifork.IsLimit.lift 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} {I : CategoryTheory.Limits.MulticospanIndex J C} {K : CategoryTheory.Limits.Multifork I} (hK : CategoryTheory.Limits.IsLimit K) {T : C} (k : (a : J.L) → T ⟶ I.left a) (hk : ∀ (b : J.R), CategoryTheory.CategoryStruct.comp (k (J.fst b)) (I.fst b) = CategoryTheory.CategoryStruct.comp (k (J.snd b)) (I.snd b)) : T ⟶ K.pt
• CategoryTheory.Limits.Multifork.hom_comp_ι 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} {I : CategoryTheory.Limits.MulticospanIndex J C} (K₁ K₂ : CategoryTheory.Limits.Multifork I) (f : K₁ ⟶ K₂) (j : J.L) : CategoryTheory.CategoryStruct.comp f.hom (K₂.ι j) = K₁.ι j
• CategoryTheory.Limits.MulticospanIndex.parallelPairDiagram_map 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] {X✝ Y✝ : CategoryTheory.Limits.WalkingParallelPair} (h : X✝ ⟶ Y✝) : I.parallelPairDiagram.map h = CategoryTheory.Limits.parallelPair.parallelPairHom I.fstPiMap I.sndPiMap h
• CategoryTheory.Limits.Multifork.ι_ofι 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) (P : C) (ι : (a : J.L) → P ⟶ I.left a) (w : ∀ (b : J.R), CategoryTheory.CategoryStruct.comp (ι (J.fst b)) (I.fst b) = CategoryTheory.CategoryStruct.comp (ι (J.snd b)) (I.snd b)) (i : J.L) : (CategoryTheory.Limits.Multifork.ofι I P ι w).ι i = ι i
• CategoryTheory.Limits.MulticospanIndex.fstPiMap_π 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] (b : J.R) : CategoryTheory.CategoryStruct.comp I.fstPiMap (CategoryTheory.Limits.Pi.π I.right b) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π I.left (J.fst b)) (I.fst b)
• CategoryTheory.Limits.MulticospanIndex.sndPiMap_π 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] (b : J.R) : CategoryTheory.CategoryStruct.comp I.sndPiMap (CategoryTheory.Limits.Pi.π I.right b) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π I.left (J.snd b)) (I.snd b)
• CategoryTheory.Limits.Multiequalizer.condition_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) [CategoryTheory.Limits.HasMultiequalizer I] (b : J.R) {Z : C} (h : I.right b ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multiequalizer.ι I (J.fst b)) (CategoryTheory.CategoryStruct.comp (I.fst b) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multiequalizer.ι I (J.snd b)) (CategoryTheory.CategoryStruct.comp (I.snd b) h)
• CategoryTheory.Limits.Multiequalizer.ιPi_π_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) [CategoryTheory.Limits.HasMultiequalizer I] [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] (a : J.L) {Z : C} (h : I.left a ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multiequalizer.ιPi I) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π I.left a) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multiequalizer.ι I a) h
• CategoryTheory.Limits.Multiequalizer.lift_ι 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) [CategoryTheory.Limits.HasMultiequalizer I] (W : C) (k : (a : J.L) → W ⟶ I.left a) (h : ∀ (b : J.R), CategoryTheory.CategoryStruct.comp (k (J.fst b)) (I.fst b) = CategoryTheory.CategoryStruct.comp (k (J.snd b)) (I.snd b)) (a : J.L) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multiequalizer.lift I W k h) (CategoryTheory.Limits.Multiequalizer.ι I a) = k a
• CategoryTheory.Limits.Multifork.toPiFork_pt 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} {I : CategoryTheory.Limits.MulticospanIndex J C} {c : CategoryTheory.Limits.Fan I.left} (hc : CategoryTheory.Limits.IsLimit c) {d : CategoryTheory.Limits.Fan I.right} (hd : CategoryTheory.Limits.IsLimit d) (K : CategoryTheory.Limits.Multifork I) : (CategoryTheory.Limits.Multifork.toPiFork hc hd K).pt = K.pt
• CategoryTheory.Limits.Multifork.IsLimit.hom_ext 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} {I : CategoryTheory.Limits.MulticospanIndex J C} {K : CategoryTheory.Limits.Multifork I} (hK : CategoryTheory.Limits.IsLimit K) {T : C} {f g : T ⟶ K.pt} (h : ∀ (a : J.L), CategoryTheory.CategoryStruct.comp f (K.ι a) = CategoryTheory.CategoryStruct.comp g (K.ι a)) : f = g
• CategoryTheory.Limits.Multifork.condition_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} {I : CategoryTheory.Limits.MulticospanIndex J C} (K : CategoryTheory.Limits.Multifork I) (b : J.R) {Z : C} (h : I.right b ⟶ Z) : CategoryTheory.CategoryStruct.comp (K.ι (J.fst b)) (CategoryTheory.CategoryStruct.comp (I.fst b) h) = CategoryTheory.CategoryStruct.comp (K.ι (J.snd b)) (CategoryTheory.CategoryStruct.comp (I.snd b) h)
• CategoryTheory.Limits.Multifork.ext 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} {I : CategoryTheory.Limits.MulticospanIndex J C} {t s : CategoryTheory.Limits.Multifork I} (e : t.pt ≅ s.pt) (h : ∀ (i : J.L), CategoryTheory.CategoryStruct.comp e.hom (s.ι i) = t.ι i := by cat_disch) : t ≅ s
• CategoryTheory.Limits.Multifork.IsLimit.fac 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} {I : CategoryTheory.Limits.MulticospanIndex J C} {K : CategoryTheory.Limits.Multifork I} (hK : CategoryTheory.Limits.IsLimit K) {T : C} (k : (a : J.L) → T ⟶ I.left a) (hk : ∀ (b : J.R), CategoryTheory.CategoryStruct.comp (k (J.fst b)) (I.fst b) = CategoryTheory.CategoryStruct.comp (k (J.snd b)) (I.snd b)) (a : J.L) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multifork.IsLimit.lift hK k hk) (K.ι a) = k a
• CategoryTheory.Limits.MulticospanIndex.ofPiForkFunctor 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) {c : CategoryTheory.Limits.Fan I.left} {d : CategoryTheory.Limits.Fan I.right} (hd : CategoryTheory.Limits.IsLimit d) : CategoryTheory.Functor (CategoryTheory.Limits.Fork (I.fstPiMapOfIsLimit c hd) (I.sndPiMapOfIsLimit c hd)) (CategoryTheory.Limits.Multifork I)
• CategoryTheory.Limits.Multifork.ofPiFork_pt 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} {I : CategoryTheory.Limits.MulticospanIndex J C} {c : CategoryTheory.Limits.Fan I.left} {d : CategoryTheory.Limits.Fan I.right} {hd : CategoryTheory.Limits.IsLimit d} (a : CategoryTheory.Limits.Fork (I.fstPiMapOfIsLimit c hd) (I.sndPiMapOfIsLimit c hd)) : (CategoryTheory.Limits.Multifork.ofPiFork a).pt = a.pt
• CategoryTheory.Limits.Multifork.app_right_eq_ι_comp_fst 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} {I : CategoryTheory.Limits.MulticospanIndex J C} (K : CategoryTheory.Limits.Multifork I) (b : J.R) : K.π.app (CategoryTheory.Limits.WalkingMulticospan.right b) = CategoryTheory.CategoryStruct.comp (K.ι (J.fst b)) (I.fst b)
• CategoryTheory.Limits.Multifork.app_right_eq_ι_comp_snd 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} {I : CategoryTheory.Limits.MulticospanIndex J C} (K : CategoryTheory.Limits.Multifork I) (b : J.R) : K.π.app (CategoryTheory.Limits.WalkingMulticospan.right b) = CategoryTheory.CategoryStruct.comp (K.ι (J.snd b)) (I.snd b)
• CategoryTheory.Limits.Multiequalizer.lift_ι_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) [CategoryTheory.Limits.HasMultiequalizer I] (W : C) (k : (a : J.L) → W ⟶ I.left a) (h : ∀ (b : J.R), CategoryTheory.CategoryStruct.comp (k (J.fst b)) (I.fst b) = CategoryTheory.CategoryStruct.comp (k (J.snd b)) (I.snd b)) (a : J.L) {Z : C} (h✝ : I.left a ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multiequalizer.lift I W k h) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multiequalizer.ι I a) h✝) = CategoryTheory.CategoryStruct.comp (k a) h✝
• CategoryTheory.Limits.MulticospanIndex.fstPiMap_π_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] (b : J.R) {Z : C} (h : I.right b ⟶ Z) : CategoryTheory.CategoryStruct.comp I.fstPiMap (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π I.right b) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π I.left (J.fst b)) (CategoryTheory.CategoryStruct.comp (I.fst b) h)
• CategoryTheory.Limits.MulticospanIndex.sndPiMap_π_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] (b : J.R) {Z : C} (h : I.right b ⟶ Z) : CategoryTheory.CategoryStruct.comp I.sndPiMap (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π I.right b) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π I.left (J.snd b)) (CategoryTheory.CategoryStruct.comp (I.snd b) h)
• CategoryTheory.Limits.Multifork.hom_comp_ι_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} {I : CategoryTheory.Limits.MulticospanIndex J C} (K₁ K₂ : CategoryTheory.Limits.Multifork I) (f : K₁ ⟶ K₂) (j : J.L) {Z : C} (h : I.left j ⟶ Z) : CategoryTheory.CategoryStruct.comp f.hom (CategoryTheory.CategoryStruct.comp (K₂.ι j) h) = CategoryTheory.CategoryStruct.comp (K₁.ι j) h
• CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiForkOfIsLimit 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) {c : CategoryTheory.Limits.Fan I.left} (hc : CategoryTheory.Limits.IsLimit c) {d : CategoryTheory.Limits.Fan I.right} (hd : CategoryTheory.Limits.IsLimit d) : CategoryTheory.Limits.Multifork I ≌ CategoryTheory.Limits.Fork (I.fstPiMapOfIsLimit c hd) (I.sndPiMapOfIsLimit c hd)
• CategoryTheory.Limits.MulticospanIndex.toPiForkFunctor 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) {c : CategoryTheory.Limits.Fan I.left} (hc : CategoryTheory.Limits.IsLimit c) {d : CategoryTheory.Limits.Fan I.right} (hd : CategoryTheory.Limits.IsLimit d) : CategoryTheory.Functor (CategoryTheory.Limits.Multifork I) (CategoryTheory.Limits.Fork (I.fstPiMapOfIsLimit c hd) (I.sndPiMapOfIsLimit c hd))
• CategoryTheory.Limits.MulticospanIndex.fstPiMapOfIsLimit_proj 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) (c : CategoryTheory.Limits.Fan I.left) {d : CategoryTheory.Limits.Fan I.right} (hd : CategoryTheory.Limits.IsLimit d) (i : J.R) : CategoryTheory.CategoryStruct.comp (I.fstPiMapOfIsLimit c hd) (d.proj i) = CategoryTheory.CategoryStruct.comp (c.proj (J.fst i)) (I.fst i)
• CategoryTheory.Limits.MulticospanIndex.sndPiMapOfIsLimit_proj 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) (c : CategoryTheory.Limits.Fan I.left) {d : CategoryTheory.Limits.Fan I.right} (hd : CategoryTheory.Limits.IsLimit d) (i : J.R) : CategoryTheory.CategoryStruct.comp (I.sndPiMapOfIsLimit c hd) (d.proj i) = CategoryTheory.CategoryStruct.comp (c.proj (J.snd i)) (I.snd i)
• CategoryTheory.Limits.Multifork.IsLimit.fac_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} {I : CategoryTheory.Limits.MulticospanIndex J C} {K : CategoryTheory.Limits.Multifork I} (hK : CategoryTheory.Limits.IsLimit K) {T : C} (k : (a : J.L) → T ⟶ I.left a) (hk : ∀ (b : J.R), CategoryTheory.CategoryStruct.comp (k (J.fst b)) (I.fst b) = CategoryTheory.CategoryStruct.comp (k (J.snd b)) (I.snd b)) (a : J.L) {Z : C} (h : I.left a ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multifork.IsLimit.lift hK k hk) (CategoryTheory.CategoryStruct.comp (K.ι a) h) = CategoryTheory.CategoryStruct.comp (k a) h
• CategoryTheory.Limits.MulticospanIndex.parallelPairDiagramOfIsLimit_map 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) (c : CategoryTheory.Limits.Fan I.left) {d : CategoryTheory.Limits.Fan I.right} (hd : CategoryTheory.Limits.IsLimit d) {X✝ Y✝ : CategoryTheory.Limits.WalkingParallelPair} (h : X✝ ⟶ Y✝) : (I.parallelPairDiagramOfIsLimit c hd).map h = CategoryTheory.Limits.parallelPair.parallelPairHom (I.fstPiMapOfIsLimit c hd) (I.sndPiMapOfIsLimit c hd) h
• CategoryTheory.Limits.Multifork.ext_hom_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} {I : CategoryTheory.Limits.MulticospanIndex J C} {t s : CategoryTheory.Limits.Multifork I} (e : t.pt ≅ s.pt) (h : ∀ (i : J.L), CategoryTheory.CategoryStruct.comp e.hom (s.ι i) = t.ι i := by cat_disch) : (CategoryTheory.Limits.Multifork.ext e h).hom.hom = e.hom
• CategoryTheory.Limits.Multifork.ext_inv_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} {I : CategoryTheory.Limits.MulticospanIndex J C} {t s : CategoryTheory.Limits.Multifork I} (e : t.pt ≅ s.pt) (h : ∀ (i : J.L), CategoryTheory.CategoryStruct.comp e.hom (s.ι i) = t.ι i := by cat_disch) : (CategoryTheory.Limits.Multifork.ext e h).inv.hom = e.inv
• CategoryTheory.Limits.MulticospanIndex.fstPiMapOfIsLimit_proj_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) (c : CategoryTheory.Limits.Fan I.left) {d : CategoryTheory.Limits.Fan I.right} (hd : CategoryTheory.Limits.IsLimit d) (i : J.R) {Z : C} (h : I.right i ⟶ Z) : CategoryTheory.CategoryStruct.comp (I.fstPiMapOfIsLimit c hd) (CategoryTheory.CategoryStruct.comp (d.proj i) h) = CategoryTheory.CategoryStruct.comp (c.proj (J.fst i)) (CategoryTheory.CategoryStruct.comp (I.fst i) h)
• CategoryTheory.Limits.MulticospanIndex.sndPiMapOfIsLimit_proj_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) (c : CategoryTheory.Limits.Fan I.left) {d : CategoryTheory.Limits.Fan I.right} (hd : CategoryTheory.Limits.IsLimit d) (i : J.R) {Z : C} (h : I.right i ⟶ Z) : CategoryTheory.CategoryStruct.comp (I.sndPiMapOfIsLimit c hd) (CategoryTheory.CategoryStruct.comp (d.proj i) h) = CategoryTheory.CategoryStruct.comp (c.proj (J.snd i)) (CategoryTheory.CategoryStruct.comp (I.snd i) h)
• CategoryTheory.Limits.MulticospanIndex.ofPiForkFunctor_obj 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) {c : CategoryTheory.Limits.Fan I.left} {d : CategoryTheory.Limits.Fan I.right} (hd : CategoryTheory.Limits.IsLimit d) (a : CategoryTheory.Limits.Fork (I.fstPiMapOfIsLimit c hd) (I.sndPiMapOfIsLimit c hd)) : (I.ofPiForkFunctor hd).obj a = CategoryTheory.Limits.Multifork.ofPiFork a
• CategoryTheory.Limits.Multifork.toPiFork_π_app_zero 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} {I : CategoryTheory.Limits.MulticospanIndex J C} (K : CategoryTheory.Limits.Multifork I) {c : CategoryTheory.Limits.Fan I.left} (hc : CategoryTheory.Limits.IsLimit c) {d : CategoryTheory.Limits.Fan I.right} (hd : CategoryTheory.Limits.IsLimit d) : (CategoryTheory.Limits.Multifork.toPiFork hc hd K).ι = CategoryTheory.Limits.Fan.IsLimit.lift hc K.ι
• CategoryTheory.Limits.MulticospanIndex.toPiForkFunctor_obj 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) {c : CategoryTheory.Limits.Fan I.left} (hc : CategoryTheory.Limits.IsLimit c) {d : CategoryTheory.Limits.Fan I.right} (hd : CategoryTheory.Limits.IsLimit d) (K : CategoryTheory.Limits.Multifork I) : (I.toPiForkFunctor hc hd).obj K = CategoryTheory.Limits.Multifork.toPiFork hc hd K
• CategoryTheory.Limits.Multifork.IsLimit.mk 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} {I : CategoryTheory.Limits.MulticospanIndex J C} (K : CategoryTheory.Limits.Multifork I) (lift : (E : CategoryTheory.Limits.Multifork I) → E.pt ⟶ K.pt) (fac : ∀ (E : CategoryTheory.Limits.Multifork I) (i : J.L), CategoryTheory.CategoryStruct.comp (lift E) (K.ι i) = E.ι i) (uniq : ∀ (E : CategoryTheory.Limits.Multifork I) (m : E.pt ⟶ K.pt), (∀ (i : J.L), CategoryTheory.CategoryStruct.comp m (K.ι i) = E.ι i) → m = lift E) : CategoryTheory.Limits.IsLimit K
• CategoryTheory.Limits.Multifork.pi_condition 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} {I : CategoryTheory.Limits.MulticospanIndex J C} (K : CategoryTheory.Limits.Multifork I) {c : CategoryTheory.Limits.Fan I.left} (hc : CategoryTheory.Limits.IsLimit c) {d : CategoryTheory.Limits.Fan I.right} (hd : CategoryTheory.Limits.IsLimit d) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fan.IsLimit.lift hc K.ι) (I.fstPiMapOfIsLimit c hd) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fan.IsLimit.lift hc K.ι) (I.sndPiMapOfIsLimit c hd)
• CategoryTheory.Limits.MulticospanIndex.multiforkOfParallelHomsEquivFork_inverse_obj_ι 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.Limits.MulticospanShape) [Unique J.L] [Unique J.R] {X Y : C} (f g : X ⟶ Y) (c : CategoryTheory.Limits.Fork f g) (a : J.L) : ((CategoryTheory.Limits.MulticospanIndex.multiforkOfParallelHomsEquivFork J f g).inverse.obj c).ι a = c.ι
• CategoryTheory.Limits.Multifork.ofPiFork_ι 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} {I : CategoryTheory.Limits.MulticospanIndex J C} {c : CategoryTheory.Limits.Fan I.left} {d : CategoryTheory.Limits.Fan I.right} (hd : CategoryTheory.Limits.IsLimit d) (a : CategoryTheory.Limits.Fork (I.fstPiMapOfIsLimit c hd) (I.sndPiMapOfIsLimit c hd)) (i : J.L) : (CategoryTheory.Limits.Multifork.ofPiFork a).ι i = CategoryTheory.CategoryStruct.comp a.ι (c.proj i)
• CategoryTheory.Limits.Multifork.app_right_eq_ι_comp_snd_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} {I : CategoryTheory.Limits.MulticospanIndex J C} (K : CategoryTheory.Limits.Multifork I) (b : J.R) {Z : C} (h : I.multicospan.obj (CategoryTheory.Limits.WalkingMulticospan.right b) ⟶ Z) : CategoryTheory.CategoryStruct.comp (K.π.app (CategoryTheory.Limits.WalkingMulticospan.right b)) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (K.ι (J.snd b)) (I.snd b)) h
• CategoryTheory.Limits.Multifork.ofι_π_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) (P : C) (ι : (a : J.L) → P ⟶ I.left a) (w : ∀ (b : J.R), CategoryTheory.CategoryStruct.comp (ι (J.fst b)) (I.fst b) = CategoryTheory.CategoryStruct.comp (ι (J.snd b)) (I.snd b)) (x : CategoryTheory.Limits.WalkingMulticospan J) : (CategoryTheory.Limits.Multifork.ofι I P ι w).π.app x = match x with | CategoryTheory.Limits.WalkingMulticospan.left a => ι a | CategoryTheory.Limits.WalkingMulticospan.right b => CategoryTheory.CategoryStruct.comp (ι (J.fst b)) (I.fst b)
• CategoryTheory.Limits.Multifork.IsLimit.mk_lift 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} {I : CategoryTheory.Limits.MulticospanIndex J C} (K : CategoryTheory.Limits.Multifork I) (lift : (E : CategoryTheory.Limits.Multifork I) → E.pt ⟶ K.pt) (fac : ∀ (E : CategoryTheory.Limits.Multifork I) (i : J.L), CategoryTheory.CategoryStruct.comp (lift E) (K.ι i) = E.ι i) (uniq : ∀ (E : CategoryTheory.Limits.Multifork I) (m : E.pt ⟶ K.pt), (∀ (i : J.L), CategoryTheory.CategoryStruct.comp m (K.ι i) = E.ι i) → m = lift E) (E : CategoryTheory.Limits.Multifork I) : (CategoryTheory.Limits.Multifork.IsLimit.mk K lift fac uniq).lift E = lift E
• CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiForkOfIsLimit_inverse 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) {c : CategoryTheory.Limits.Fan I.left} (hc : CategoryTheory.Limits.IsLimit c) {d : CategoryTheory.Limits.Fan I.right} (hd : CategoryTheory.Limits.IsLimit d) : (I.multiforkEquivPiForkOfIsLimit hc hd).inverse = I.ofPiForkFunctor hd
• CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiForkOfIsLimit_functor 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) {c : CategoryTheory.Limits.Fan I.left} (hc : CategoryTheory.Limits.IsLimit c) {d : CategoryTheory.Limits.Fan I.right} (hd : CategoryTheory.Limits.IsLimit d) : (I.multiforkEquivPiForkOfIsLimit hc hd).functor = I.toPiForkFunctor hc hd
• CategoryTheory.Limits.Multifork.pi_condition_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} {I : CategoryTheory.Limits.MulticospanIndex J C} (K : CategoryTheory.Limits.Multifork I) {c : CategoryTheory.Limits.Fan I.left} (hc : CategoryTheory.Limits.IsLimit c) {d : CategoryTheory.Limits.Fan I.right} (hd : CategoryTheory.Limits.IsLimit d) {Z : C} (h : d.pt ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fan.IsLimit.lift hc K.ι) (CategoryTheory.CategoryStruct.comp (I.fstPiMapOfIsLimit c hd) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fan.IsLimit.lift hc K.ι) (CategoryTheory.CategoryStruct.comp (I.sndPiMapOfIsLimit c hd) h)
• CategoryTheory.Limits.MulticospanIndex.toPiForkFunctor_map_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) {c : CategoryTheory.Limits.Fan I.left} (hc : CategoryTheory.Limits.IsLimit c) {d : CategoryTheory.Limits.Fan I.right} (hd : CategoryTheory.Limits.IsLimit d) {K₁ K₂ : CategoryTheory.Limits.Multifork I} (f : K₁ ⟶ K₂) : ((I.toPiForkFunctor hc hd).map f).hom = f.hom
• CategoryTheory.Limits.Multifork.ofPiFork_π_app_right 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} {I : CategoryTheory.Limits.MulticospanIndex J C} {c : CategoryTheory.Limits.Fan I.left} {d : CategoryTheory.Limits.Fan I.right} (hd : CategoryTheory.Limits.IsLimit d) (a : CategoryTheory.Limits.Fork (I.fstPiMapOfIsLimit c hd) (I.sndPiMapOfIsLimit c hd)) (i : J.R) : (CategoryTheory.Limits.Multifork.ofPiFork a).π.app (CategoryTheory.Limits.WalkingMulticospan.right i) = CategoryTheory.CategoryStruct.comp a.ι (CategoryTheory.CategoryStruct.comp (I.fstPiMapOfIsLimit c hd) (d.proj i))
• CategoryTheory.Limits.Multifork.isLimitEquivOfIsos 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} {I I' : CategoryTheory.Limits.MulticospanIndex J C} (c : CategoryTheory.Limits.Multifork I) (c' : CategoryTheory.Limits.Multifork I') (e : c.pt ≅ c'.pt) (el : (i : J.L) → I.left i ≅ I'.left i) (er : (i : J.R) → I.right i ≅ I'.right i) (hl : ∀ (i : J.R), CategoryTheory.CategoryStruct.comp (I.fst i) (er i).hom = CategoryTheory.CategoryStruct.comp (el (J.fst i)).hom (I'.fst i) := by cat_disch) (hr : ∀ (i : J.R), CategoryTheory.CategoryStruct.comp (I.snd i) (er i).hom = CategoryTheory.CategoryStruct.comp (el (J.snd i)).hom (I'.snd i) := by cat_disch) (he : ∀ (i : J.L), CategoryTheory.CategoryStruct.comp e.hom (c'.ι i) = CategoryTheory.CategoryStruct.comp (c.ι i) (el i).hom := by cat_disch) : CategoryTheory.Limits.IsLimit c ≃ CategoryTheory.Limits.IsLimit c'
• CategoryTheory.Limits.Multifork.toPiFork_π_app_one 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} {I : CategoryTheory.Limits.MulticospanIndex J C} (K : CategoryTheory.Limits.Multifork I) {c : CategoryTheory.Limits.Fan I.left} (hc : CategoryTheory.Limits.IsLimit c) {d : CategoryTheory.Limits.Fan I.right} (hd : CategoryTheory.Limits.IsLimit d) : (CategoryTheory.Limits.Multifork.toPiFork hc hd K).π.app CategoryTheory.Limits.WalkingParallelPair.one = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fan.IsLimit.lift hc K.ι) (I.fstPiMapOfIsLimit c hd)
• CategoryTheory.Limits.MulticospanIndex.ofPiForkFunctor_map_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) {c : CategoryTheory.Limits.Fan I.left} {d : CategoryTheory.Limits.Fan I.right} (hd : CategoryTheory.Limits.IsLimit d) {K₁ K₂ : CategoryTheory.Limits.Fork (I.fstPiMapOfIsLimit c hd) (I.sndPiMapOfIsLimit c hd)} (f : K₁ ⟶ K₂) : ((I.ofPiForkFunctor hd).map f).hom = f.hom
• CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiFork_functor_obj_pt 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] (K : CategoryTheory.Limits.Multifork I) : (I.multiforkEquivPiFork.functor.obj K).pt = K.pt
• CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiFork_inverse_obj_pt 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] (a : CategoryTheory.Limits.Fork (I.fstPiMapOfIsLimit (CategoryTheory.Limits.limit.cone (CategoryTheory.Discrete.functor I.left)) (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Discrete.functor I.right))) (I.sndPiMapOfIsLimit (CategoryTheory.Limits.limit.cone (CategoryTheory.Discrete.functor I.left)) (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Discrete.functor I.right)))) : (I.multiforkEquivPiFork.inverse.obj a).pt = a.pt
• CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiFork_functor_map_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] {K₁ K₂ : CategoryTheory.Limits.Multifork I} (f : K₁ ⟶ K₂) : (I.multiforkEquivPiFork.functor.map f).hom = f.hom
• CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiForkOfIsLimit_unitIso 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) {c : CategoryTheory.Limits.Fan I.left} (hc : CategoryTheory.Limits.IsLimit c) {d : CategoryTheory.Limits.Fan I.right} (hd : CategoryTheory.Limits.IsLimit d) : (I.multiforkEquivPiForkOfIsLimit hc hd).unitIso = CategoryTheory.NatIso.ofComponents (fun K => CategoryTheory.Limits.Cone.ext (CategoryTheory.Iso.refl ((CategoryTheory.Functor.id (CategoryTheory.Limits.Multifork I)).obj K).pt) ⋯) ⋯
• CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiFork_functor_obj_π_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] (K : CategoryTheory.Limits.Multifork I) (X : CategoryTheory.Limits.WalkingParallelPair) : (I.multiforkEquivPiFork.functor.obj K).π.app X = CategoryTheory.Limits.WalkingParallelPair.rec (motive := fun t => X = t → (K.pt ⟶ (CategoryTheory.Limits.parallelPair (I.fstPiMapOfIsLimit (CategoryTheory.Limits.limit.cone (CategoryTheory.Discrete.functor I.left)) (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Discrete.functor I.right))) (I.sndPiMapOfIsLimit (CategoryTheory.Limits.limit.cone (CategoryTheory.Discrete.functor I.left)) (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Discrete.functor I.right)))).obj X)) (fun h => ⋯ ▸ CategoryTheory.Limits.Fan.IsLimit.lift (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Discrete.functor I.left)) K.ι) (fun h => ⋯ ▸ CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fan.IsLimit.lift (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Discrete.functor I.left)) K.ι) (I.sndPiMapOfIsLimit (CategoryTheory.Limits.limit.cone (CategoryTheory.Discrete.functor I.left)) (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Discrete.functor I.right)))) X ⋯
• CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiFork_inverse_obj_π_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] (a : CategoryTheory.Limits.Fork (I.fstPiMapOfIsLimit (CategoryTheory.Limits.limit.cone (CategoryTheory.Discrete.functor I.left)) (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Discrete.functor I.right))) (I.sndPiMapOfIsLimit (CategoryTheory.Limits.limit.cone (CategoryTheory.Discrete.functor I.left)) (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Discrete.functor I.right)))) (x✝ : CategoryTheory.Limits.WalkingMulticospan J) : (I.multiforkEquivPiFork.inverse.obj a).π.app x✝ = match x✝ with | CategoryTheory.Limits.WalkingMulticospan.left a_1 => CategoryTheory.CategoryStruct.comp a.ι (CategoryTheory.Limits.Fan.proj (CategoryTheory.Limits.limit.cone (CategoryTheory.Discrete.functor I.left)) a_1) | CategoryTheory.Limits.WalkingMulticospan.right a_1 => CategoryTheory.CategoryStruct.comp a.ι (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fan.proj (CategoryTheory.Limits.limit.cone (CategoryTheory.Discrete.functor I.left)) (J.fst a_1)) (I.fst a_1))
• CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiFork_inverse_map_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] {K₁ K₂ : CategoryTheory.Limits.Fork (I.fstPiMapOfIsLimit (CategoryTheory.Limits.limit.cone (CategoryTheory.Discrete.functor I.left)) (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Discrete.functor I.right))) (I.sndPiMapOfIsLimit (CategoryTheory.Limits.limit.cone (CategoryTheory.Discrete.functor I.left)) (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Discrete.functor I.right)))} (f : K₁ ⟶ K₂) : (I.multiforkEquivPiFork.inverse.map f).hom = f.hom
• CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiFork_unitIso_hom_app_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] (X : CategoryTheory.Limits.Multifork I) : (I.multiforkEquivPiFork.unitIso.hom.app X).hom = CategoryTheory.CategoryStruct.id X.pt
• CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiFork_unitIso_inv_app_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] (X : CategoryTheory.Limits.Multifork I) : (I.multiforkEquivPiFork.unitIso.inv.app X).hom = CategoryTheory.CategoryStruct.id X.pt
• CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiForkOfIsLimit_counitIso 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) {c : CategoryTheory.Limits.Fan I.left} (hc : CategoryTheory.Limits.IsLimit c) {d : CategoryTheory.Limits.Fan I.right} (hd : CategoryTheory.Limits.IsLimit d) : (I.multiforkEquivPiForkOfIsLimit hc hd).counitIso = CategoryTheory.NatIso.ofComponents (fun K => CategoryTheory.Limits.Fork.ext (CategoryTheory.Iso.refl (((I.ofPiForkFunctor hd).comp (I.toPiForkFunctor hc hd)).obj K).pt) ⋯) ⋯
• CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiFork_counitIso_hom_app_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] (X : CategoryTheory.Limits.Fork (I.fstPiMapOfIsLimit (CategoryTheory.Limits.limit.cone (CategoryTheory.Discrete.functor I.left)) (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Discrete.functor I.right))) (I.sndPiMapOfIsLimit (CategoryTheory.Limits.limit.cone (CategoryTheory.Discrete.functor I.left)) (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Discrete.functor I.right)))) : (I.multiforkEquivPiFork.counitIso.hom.app X).hom = CategoryTheory.CategoryStruct.id X.pt
• CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiFork_counitIso_inv_app_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] (X : CategoryTheory.Limits.Fork (I.fstPiMapOfIsLimit (CategoryTheory.Limits.limit.cone (CategoryTheory.Discrete.functor I.left)) (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Discrete.functor I.right))) (I.sndPiMapOfIsLimit (CategoryTheory.Limits.limit.cone (CategoryTheory.Discrete.functor I.left)) (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Discrete.functor I.right)))) : (I.multiforkEquivPiFork.counitIso.inv.app X).hom = CategoryTheory.CategoryStruct.id X.pt
• CategoryTheory.Limits.Concrete.multiequalizer_ext 📋 Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type s} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [CategoryTheory.ConcreteCategory C FC] {J : CategoryTheory.Limits.MulticospanShape} {I : CategoryTheory.Limits.MulticospanIndex J C} [CategoryTheory.Limits.HasMultiequalizer I] [CategoryTheory.Limits.PreservesLimit I.multicospan (CategoryTheory.forget C)] (x y : CategoryTheory.ToType (CategoryTheory.Limits.multiequalizer I)) (h : ∀ (t : J.L), (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Multiequalizer.ι I t)) x = (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Multiequalizer.ι I t)) y) : x = y
• CategoryTheory.Limits.Concrete.multiequalizerEquiv 📋 Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type s} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [CategoryTheory.ConcreteCategory C FC] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) [CategoryTheory.Limits.HasMultiequalizer I] [CategoryTheory.Limits.PreservesLimit I.multicospan (CategoryTheory.forget C)] : CategoryTheory.ToType (CategoryTheory.Limits.multiequalizer I) ≃ { x // ∀ (i : J.R), (CategoryTheory.ConcreteCategory.hom (I.fst i)) (x (J.fst i)) = (CategoryTheory.ConcreteCategory.hom (I.snd i)) (x (J.snd i)) }
• CategoryTheory.Limits.Concrete.multiequalizerEquivAux 📋 Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type s} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [CategoryTheory.ConcreteCategory C FC] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) : ↑(I.multicospan.comp (CategoryTheory.forget C)).sections ≃ { x // ∀ (i : J.R), (CategoryTheory.ConcreteCategory.hom (I.fst i)) (x (J.fst i)) = (CategoryTheory.ConcreteCategory.hom (I.snd i)) (x (J.snd i)) }
• CategoryTheory.Limits.Concrete.multiequalizerEquiv_apply 📋 Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type s} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [CategoryTheory.ConcreteCategory C FC] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) [CategoryTheory.Limits.HasMultiequalizer I] [CategoryTheory.Limits.PreservesLimit I.multicospan (CategoryTheory.forget C)] (x : CategoryTheory.ToType (CategoryTheory.Limits.multiequalizer I)) (i : J.L) : ↑((CategoryTheory.Limits.Concrete.multiequalizerEquiv I) x) i = (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Multiequalizer.ι I i)) x
• CategoryTheory.GrothendieckTopology.Cover.index_left 📋 Mathlib.CategoryTheory.Sites.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {J : CategoryTheory.GrothendieckTopology C} {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] (S : J.Cover X) (P : CategoryTheory.Functor Cᵒᵖ D) (I : S.shape.L) : (S.index P).left I = P.obj (Opposite.op I.Y)
• CategoryTheory.GrothendieckTopology.diagramNatTrans_app 📋 Mathlib.CategoryTheory.Sites.Plus
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w} [CategoryTheory.Category.{w', w} D] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] {P Q : CategoryTheory.Functor Cᵒᵖ D} (η : P ⟶ Q) (X : C) (W : (J.Cover X)ᵒᵖ) : (J.diagramNatTrans η X).app W = CategoryTheory.Limits.Multiequalizer.lift ((Opposite.unop W).index Q) ((J.diagram P X).obj W) (fun x => CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multiequalizer.ι ((Opposite.unop W).index P) x) (η.app (Opposite.op x.Y))) ⋯
• CategoryTheory.Meq.equiv_apply 📋 Mathlib.CategoryTheory.Sites.ConcreteSheafification
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w} [CategoryTheory.Category.{w', w} D] {FD : D → D → Type u_1} {CD : D → Type t} [(X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] [CategoryTheory.ConcreteCategory D FD] [∀ {X : C} (S : J.Cover X), CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan S.shape) (CategoryTheory.forget D)] {X : C} {P : CategoryTheory.Functor Cᵒᵖ D} {S : J.Cover X} [CategoryTheory.Limits.HasMultiequalizer (S.index P)] (x : CategoryTheory.ToType (CategoryTheory.Limits.multiequalizer (S.index P))) (I : S.Arrow) : ↑((CategoryTheory.Meq.equiv P S) x) I = (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Multiequalizer.ι (S.index P) I)) x
• CategoryTheory.Meq.equiv_symm_eq_apply 📋 Mathlib.CategoryTheory.Sites.ConcreteSheafification
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w} [CategoryTheory.Category.{w', w} D] {FD : D → D → Type u_1} {CD : D → Type t} [(X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] [CategoryTheory.ConcreteCategory D FD] [∀ {X : C} (S : J.Cover X), CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan S.shape) (CategoryTheory.forget D)] {X : C} {P : CategoryTheory.Functor Cᵒᵖ D} {S : J.Cover X} [CategoryTheory.Limits.HasMultiequalizer (S.index P)] (x : CategoryTheory.Meq P S) (I : S.Arrow) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Multiequalizer.ι (S.index P) I)) ((CategoryTheory.Meq.equiv P S).symm x) = ↑x I
• CategoryTheory.GrothendieckTopology.diagramCompIso_hom_ι 📋 Mathlib.CategoryTheory.Sites.CompatiblePlus
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] {E : Type u_2} [CategoryTheory.Category.{v_2, u_2} E] (F : CategoryTheory.Functor D E) [∀ (J : CategoryTheory.Limits.MulticospanShape), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan J) D] [∀ (J : CategoryTheory.Limits.MulticospanShape), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan J) E] [∀ (X : C) (W : J.Cover X) (P : CategoryTheory.Functor Cᵒᵖ D), CategoryTheory.Limits.PreservesLimit (W.index P).multicospan F] (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (W : (J.Cover X)ᵒᵖ) (i : (Opposite.unop W).Arrow) : CategoryTheory.CategoryStruct.comp ((J.diagramCompIso F P X).hom.app W) (CategoryTheory.Limits.Multiequalizer.ι ((Opposite.unop W).index (P.comp F)) i) = F.map (CategoryTheory.Limits.Multiequalizer.ι ((Opposite.unop W).index P) i)
• CategoryTheory.GrothendieckTopology.diagramCompIso_hom_ι_assoc 📋 Mathlib.CategoryTheory.Sites.CompatiblePlus
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] {E : Type u_2} [CategoryTheory.Category.{v_2, u_2} E] (F : CategoryTheory.Functor D E) [∀ (J : CategoryTheory.Limits.MulticospanShape), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan J) D] [∀ (J : CategoryTheory.Limits.MulticospanShape), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan J) E] [∀ (X : C) (W : J.Cover X) (P : CategoryTheory.Functor Cᵒᵖ D), CategoryTheory.Limits.PreservesLimit (W.index P).multicospan F] (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (W : (J.Cover X)ᵒᵖ) (i : (Opposite.unop W).Arrow) {Z : E} (h : ((Opposite.unop W).index (P.comp F)).left i ⟶ Z) : CategoryTheory.CategoryStruct.comp ((J.diagramCompIso F P X).hom.app W) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multiequalizer.ι ((Opposite.unop W).index (P.comp F)) i) h) = CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.Limits.Multiequalizer.ι ((Opposite.unop W).index P) i)) h
• CategoryTheory.GrothendieckTopology.liftToDiagramLimitObjAux_fac 📋 Mathlib.CategoryTheory.Sites.LeftExact
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w} [CategoryTheory.Category.{t, w} D] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] {X : C} {K : Type s} [CategoryTheory.SmallCategory K] [CategoryTheory.Limits.HasLimitsOfShape K D] {W : (J.Cover X)ᵒᵖ} (F : CategoryTheory.Functor K (CategoryTheory.Functor Cᵒᵖ D)) (E : CategoryTheory.Limits.Cone (F.comp ((J.diagramFunctor D X).comp ((CategoryTheory.evaluation (J.Cover X)ᵒᵖ D).obj W)))) (i : (Opposite.unop W).Arrow) (k : K) : CategoryTheory.CategoryStruct.comp (CategoryTheory.GrothendieckTopology.liftToDiagramLimitObjAux F E i) ((CategoryTheory.Limits.limit.π F k).app (Opposite.op i.Y)) = CategoryTheory.CategoryStruct.comp (E.π.app k) (CategoryTheory.Limits.Multiequalizer.ι ((Opposite.unop W).index (F.obj k)) i)
• CategoryTheory.GrothendieckTopology.liftToDiagramLimitObjAux_fac_assoc 📋 Mathlib.CategoryTheory.Sites.LeftExact
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w} [CategoryTheory.Category.{t, w} D] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] {X : C} {K : Type s} [CategoryTheory.SmallCategory K] [CategoryTheory.Limits.HasLimitsOfShape K D] {W : (J.Cover X)ᵒᵖ} (F : CategoryTheory.Functor K (CategoryTheory.Functor Cᵒᵖ D)) (E : CategoryTheory.Limits.Cone (F.comp ((J.diagramFunctor D X).comp ((CategoryTheory.evaluation (J.Cover X)ᵒᵖ D).obj W)))) (i : (Opposite.unop W).Arrow) (k : K) {Z : D} (h : (F.obj k).obj (Opposite.op i.Y) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.GrothendieckTopology.liftToDiagramLimitObjAux F E i) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Limits.limit.π F k).app (Opposite.op i.Y)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (E.π.app k) (CategoryTheory.Limits.Multiequalizer.ι ((Opposite.unop W).index (F.obj k)) i)) h
• CategoryTheory.PreOneHypercover.multicospanIndex_left 📋 Mathlib.CategoryTheory.Sites.Hypercover.One
  {C : Type u} [CategoryTheory.Category.{v, u} C] {A : Type u_1} [CategoryTheory.Category.{v_1, u_1} A] {S : C} (E : CategoryTheory.PreOneHypercover S) (F : CategoryTheory.Functor Cᵒᵖ A) (i : E.multicospanShape.L) : (E.multicospanIndex F).left i = F.obj (Opposite.op (E.X i))
• CategoryTheory.PreOneHypercover.multifork_ι 📋 Mathlib.CategoryTheory.Sites.Hypercover.One
  {C : Type u} [CategoryTheory.Category.{v, u} C] {A : Type u_1} [CategoryTheory.Category.{v_1, u_1} A] {S : C} (E : CategoryTheory.PreOneHypercover S) (F : CategoryTheory.Functor Cᵒᵖ A) (i : E.I₀) : (E.multifork F).ι i = F.map (E.f i).op
• CategoryTheory.PreOneHypercover.Hom.mapMultiforkOfIsLimit_ι 📋 Mathlib.CategoryTheory.Sites.Hypercover.One
  {C : Type u} [CategoryTheory.Category.{v, u} C] {A : Type u_1} [CategoryTheory.Category.{v_1, u_1} A] {S : C} {E : CategoryTheory.PreOneHypercover S} {F : CategoryTheory.PreOneHypercover S} (f : E.Hom F) (P : CategoryTheory.Functor Cᵒᵖ A) {c : CategoryTheory.Limits.Multifork (E.multicospanIndex P)} (hc : CategoryTheory.Limits.IsLimit c) (d : CategoryTheory.Limits.Multifork (F.multicospanIndex P)) (a : E.I₀) : CategoryTheory.CategoryStruct.comp (f.mapMultiforkOfIsLimit P hc d) (c.ι a) = CategoryTheory.CategoryStruct.comp (d.ι (f.s₀ a)) (P.map (f.h₀ a).op)
• CategoryTheory.PreOneHypercover.Hom.mapMultiforkOfIsLimit_ι_assoc 📋 Mathlib.CategoryTheory.Sites.Hypercover.One
  {C : Type u} [CategoryTheory.Category.{v, u} C] {A : Type u_1} [CategoryTheory.Category.{v_1, u_1} A] {S : C} {E : CategoryTheory.PreOneHypercover S} {F : CategoryTheory.PreOneHypercover S} (f : E.Hom F) (P : CategoryTheory.Functor Cᵒᵖ A) {c : CategoryTheory.Limits.Multifork (E.multicospanIndex P)} (hc : CategoryTheory.Limits.IsLimit c) (d : CategoryTheory.Limits.Multifork (F.multicospanIndex P)) (a : E.I₀) {Z : A} (h : (E.multicospanIndex P).left a ⟶ Z) : CategoryTheory.CategoryStruct.comp (f.mapMultiforkOfIsLimit P hc d) (CategoryTheory.CategoryStruct.comp (c.ι a) h) = CategoryTheory.CategoryStruct.comp (d.ι (f.s₀ a)) (CategoryTheory.CategoryStruct.comp (P.map (f.h₀ a).op) h)
• CategoryTheory.RanIsSheafOfIsCocontinuous.liftAux_map 📋 Mathlib.CategoryTheory.Sites.CoverLifting
  {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] {G : CategoryTheory.Functor C D} {A : Type w} [CategoryTheory.Category.{w', w} A] {J : CategoryTheory.GrothendieckTopology C} {K : CategoryTheory.GrothendieckTopology D} [G.IsCocontinuous J K] {F : CategoryTheory.Functor Cᵒᵖ A} (hF : CategoryTheory.Presheaf.IsSheaf J F) {R : CategoryTheory.Functor Dᵒᵖ A} (α : G.op.comp R ⟶ F) {X : D} {S : K.Cover X} (s : CategoryTheory.Limits.Multifork (S.index R)) {Y : C} (f : G.obj Y ⟶ X) {W : C} (g : W ⟶ Y) (i : S.Arrow) (h : G.obj W ⟶ i.Y) (w : CategoryTheory.CategoryStruct.comp h i.f = CategoryTheory.CategoryStruct.comp (G.map g) f) : CategoryTheory.CategoryStruct.comp (CategoryTheory.RanIsSheafOfIsCocontinuous.liftAux hF α s f) (F.map g.op) = CategoryTheory.CategoryStruct.comp (s.ι i) (CategoryTheory.CategoryStruct.comp (R.map h.op) (α.app (Opposite.op W)))
• CategoryTheory.Limits.MulticospanIndex.sections.val 📋 Mathlib.CategoryTheory.Limits.Types.Multiequalizer
  {J : CategoryTheory.Limits.MulticospanShape} {I : CategoryTheory.Limits.MulticospanIndex J (Type u)} (self : I.sections) (i : J.L) : I.left i
• CategoryTheory.Limits.MulticospanIndex.sections.ext 📋 Mathlib.CategoryTheory.Limits.Types.Multiequalizer
  {J : CategoryTheory.Limits.MulticospanShape} {I : CategoryTheory.Limits.MulticospanIndex J (Type u)} {x y : I.sections} (val : x.val = y.val) : x = y
• CategoryTheory.Limits.MulticospanIndex.sections.ext_iff 📋 Mathlib.CategoryTheory.Limits.Types.Multiequalizer
  {J : CategoryTheory.Limits.MulticospanShape} {I : CategoryTheory.Limits.MulticospanIndex J (Type u)} {x y : I.sections} : x = y ↔ x.val = y.val
• CategoryTheory.Limits.Multifork.toSections_val 📋 Mathlib.CategoryTheory.Limits.Types.Multiequalizer
  {J : CategoryTheory.Limits.MulticospanShape} {I : CategoryTheory.Limits.MulticospanIndex J (Type u)} (c : CategoryTheory.Limits.Multifork I) (x : c.pt) (i : J.L) : (c.toSections x).val i = (CategoryTheory.ConcreteCategory.hom (c.ι i)) x
• CategoryTheory.Limits.MulticospanIndex.sections.property 📋 Mathlib.CategoryTheory.Limits.Types.Multiequalizer
  {J : CategoryTheory.Limits.MulticospanShape} {I : CategoryTheory.Limits.MulticospanIndex J (Type u)} (self : I.sections) (r : J.R) : (CategoryTheory.ConcreteCategory.hom (I.fst r)) (self.val (J.fst r)) = (CategoryTheory.ConcreteCategory.hom (I.snd r)) (self.val (J.snd r))
• CategoryTheory.Limits.MulticospanIndex.sections.mk 📋 Mathlib.CategoryTheory.Limits.Types.Multiequalizer
  {J : CategoryTheory.Limits.MulticospanShape} {I : CategoryTheory.Limits.MulticospanIndex J (Type u)} (val : (i : J.L) → I.left i) (property : ∀ (r : J.R), (CategoryTheory.ConcreteCategory.hom (I.fst r)) (val (J.fst r)) = (CategoryTheory.ConcreteCategory.hom (I.snd r)) (val (J.snd r))) : I.sections
• CategoryTheory.Limits.Multifork.IsLimit.sectionsEquiv_apply_val 📋 Mathlib.CategoryTheory.Limits.Types.Multiequalizer
  {J : CategoryTheory.Limits.MulticospanShape} {I : CategoryTheory.Limits.MulticospanIndex J (Type u)} {c : CategoryTheory.Limits.Multifork I} (hc : CategoryTheory.Limits.IsLimit c) (s : I.sections) (i : J.L) : (CategoryTheory.ConcreteCategory.hom (c.ι i)) ((CategoryTheory.Limits.Multifork.IsLimit.sectionsEquiv hc) s) = s.val i
• CategoryTheory.Limits.Multifork.IsLimit.sectionsEquiv_symm_apply_val 📋 Mathlib.CategoryTheory.Limits.Types.Multiequalizer
  {J : CategoryTheory.Limits.MulticospanShape} {I : CategoryTheory.Limits.MulticospanIndex J (Type u)} {c : CategoryTheory.Limits.Multifork I} (hc : CategoryTheory.Limits.IsLimit c) (x : c.pt) (i : J.L) : ((CategoryTheory.Limits.Multifork.IsLimit.sectionsEquiv hc).symm x).val i = (CategoryTheory.ConcreteCategory.hom (c.ι i)) x
• CategoryTheory.Limits.MulticospanIndex.sectionsEquiv_apply_coe 📋 Mathlib.CategoryTheory.Limits.Types.Multiequalizer
  {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J (Type u)) (s : I.sections) (i : CategoryTheory.Limits.WalkingMulticospan J) : ↑(I.sectionsEquiv s) i = match i with | CategoryTheory.Limits.WalkingMulticospan.left i => s.val i | CategoryTheory.Limits.WalkingMulticospan.right j => (CategoryTheory.ConcreteCategory.hom (I.fst j)) (s.val (J.fst j))
• CategoryTheory.PreZeroHypercover.sectionsEquivOfHasPullbacks_apply_coe 📋 Mathlib.CategoryTheory.Sites.Hypercover.SheafOfTypes
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {S : C} (E : CategoryTheory.PreZeroHypercover S) [E.HasPullbacks] (F : CategoryTheory.Functor Cᵒᵖ (Type u_2)) (s : (E.toPreOneHypercover.multicospanIndex F).sections) (i : E.toPreOneHypercover.multicospanShape.L) : ↑((E.sectionsEquivOfHasPullbacks F) s) i = s.val i
• CategoryTheory.Functor.PreOneHypercoverDenseData.multicospanIndex_left 📋 Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
  {C₀ : Type u₀} {C : Type u} [CategoryTheory.Category.{v₀, u₀} C₀] [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C₀ C} {A : Type u'} [CategoryTheory.Category.{v', u'} A] {X : C} (data : F.PreOneHypercoverDenseData X) (P : CategoryTheory.Functor C₀ᵒᵖ A) (i : data.multicospanShape.L) : (data.multicospanIndex P).left i = P.obj (Opposite.op (data.X i))
• CategoryTheory.Limits.MulticospanIndex.map_left 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.Multiequalizer
  {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] {J : CategoryTheory.Limits.MulticospanShape} (d : CategoryTheory.Limits.MulticospanIndex J C) (F : CategoryTheory.Functor C D) (i : J.L) : (d.map F).left i = F.obj (d.left i)
• CategoryTheory.Limits.MulticospanIndex.map_fst 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.Multiequalizer
  {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] {J : CategoryTheory.Limits.MulticospanShape} (d : CategoryTheory.Limits.MulticospanIndex J C) (F : CategoryTheory.Functor C D) (i : J.R) : (d.map F).fst i = F.map (d.fst i)
• CategoryTheory.Limits.MulticospanIndex.map_snd 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.Multiequalizer
  {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] {J : CategoryTheory.Limits.MulticospanShape} (d : CategoryTheory.Limits.MulticospanIndex J C) (F : CategoryTheory.Functor C D) (i : J.R) : (d.map F).snd i = F.map (d.snd i)
• CategoryTheory.Limits.MulticospanIndex.multicospanMapIso_hom_app 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.Multiequalizer
  {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] {J : CategoryTheory.Limits.MulticospanShape} (d : CategoryTheory.Limits.MulticospanIndex J C) (F : CategoryTheory.Functor C D) (X : CategoryTheory.Limits.WalkingMulticospan J) : (d.multicospanMapIso F).hom.app X = (match X with | CategoryTheory.Limits.WalkingMulticospan.left a => CategoryTheory.Iso.refl (F.obj (d.left a)) | CategoryTheory.Limits.WalkingMulticospan.right a => CategoryTheory.Iso.refl (F.obj (d.right a))).hom
• CategoryTheory.Limits.MulticospanIndex.multicospanMapIso_inv_app 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.Multiequalizer
  {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] {J : CategoryTheory.Limits.MulticospanShape} (d : CategoryTheory.Limits.MulticospanIndex J C) (F : CategoryTheory.Functor C D) (X : CategoryTheory.Limits.WalkingMulticospan J) : (d.multicospanMapIso F).inv.app X = (match X with | CategoryTheory.Limits.WalkingMulticospan.left a => CategoryTheory.Iso.refl (F.obj (d.left a)) | CategoryTheory.Limits.WalkingMulticospan.right a => CategoryTheory.Iso.refl (F.obj (d.right a))).inv
• CategoryTheory.Limits.Multifork.map_π_app 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.Multiequalizer
  {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] {J : CategoryTheory.Limits.MulticospanShape} {d : CategoryTheory.Limits.MulticospanIndex J C} (c : CategoryTheory.Limits.Multifork d) (F : CategoryTheory.Functor C D) (x : CategoryTheory.Limits.WalkingMulticospan J) : (c.map F).π.app x = match x with | CategoryTheory.Limits.WalkingMulticospan.left a => F.map (c.ι a) | CategoryTheory.Limits.WalkingMulticospan.right b => CategoryTheory.CategoryStruct.comp (F.map (c.ι (J.fst b))) (F.map (d.fst b))
• CategoryTheory.Limits.multicospanIndexEnd_left 📋 Mathlib.CategoryTheory.Limits.Shapes.End
  {J : Type u} [CategoryTheory.Category.{v, u} J] {C : Type u'} [CategoryTheory.Category.{v', u'} C] (F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)) (j : (CategoryTheory.Limits.multicospanShapeEnd J).L) : (CategoryTheory.Limits.multicospanIndexEnd F).left j = (F.obj (Opposite.op j)).obj j
• CategoryTheory.Limits.Wedge.IsLimit.hom_ext 📋 Mathlib.CategoryTheory.Limits.Shapes.End
  {J : Type u} [CategoryTheory.Category.{v, u} J] {C : Type u'} [CategoryTheory.Category.{v', u'} C] {F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)} {c : CategoryTheory.Limits.Wedge F} (hc : CategoryTheory.Limits.IsLimit c) {X : C} {f g : X ⟶ c.pt} (h : ∀ (j : (CategoryTheory.Limits.multicospanShapeEnd J).L), CategoryTheory.CategoryStruct.comp f (CategoryTheory.Limits.Multifork.ι c j) = CategoryTheory.CategoryStruct.comp g (CategoryTheory.Limits.Multifork.ι c j)) : f = g
• CategoryTheory.Limits.Wedge.ext 📋 Mathlib.CategoryTheory.Limits.Shapes.End
  {J : Type u} [CategoryTheory.Category.{v, u} J] {C : Type u'} [CategoryTheory.Category.{v', u'} C] {F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)} {W₁ W₂ : CategoryTheory.Limits.Wedge F} (e : W₁.pt ≅ W₂.pt) (he : ∀ (j : J), CategoryTheory.Limits.Multifork.ι W₁ j = CategoryTheory.CategoryStruct.comp e.hom (CategoryTheory.Limits.Multifork.ι W₂ j) := by cat_disch) : W₁ ≅ W₂
• CategoryTheory.Limits.Wedge.condition 📋 Mathlib.CategoryTheory.Limits.Shapes.End
  {J : Type u} [CategoryTheory.Category.{v, u} J] {C : Type u'} [CategoryTheory.Category.{v', u'} C] {F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)} (c : CategoryTheory.Limits.Wedge F) {i j : J} (f : i ⟶ j) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multifork.ι c i) ((F.obj (Opposite.op i)).map f) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multifork.ι c j) ((F.map f.op).app j)
• CategoryTheory.Limits.Wedge.mk_ι 📋 Mathlib.CategoryTheory.Limits.Shapes.End
  {J : Type u} [CategoryTheory.Category.{v, u} J] {C : Type u'} [CategoryTheory.Category.{v', u'} C] {F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)} (pt : C) (π : (j : J) → pt ⟶ (F.obj (Opposite.op j)).obj j) (hπ : ∀ ⦃i j : J⦄ (f : i ⟶ j), CategoryTheory.CategoryStruct.comp (π i) ((F.obj (Opposite.op i)).map f) = CategoryTheory.CategoryStruct.comp (π j) ((F.map f.op).app j)) (j : J) : CategoryTheory.Limits.Multifork.ι (CategoryTheory.Limits.Wedge.mk pt π hπ) j = π j
• CategoryTheory.Limits.Wedge.condition_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.End
  {J : Type u} [CategoryTheory.Category.{v, u} J] {C : Type u'} [CategoryTheory.Category.{v', u'} C] {F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)} (c : CategoryTheory.Limits.Wedge F) {i j : J} (f : i ⟶ j) {Z : C} (h : (F.obj (Opposite.op i)).obj j ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multifork.ι c i) (CategoryTheory.CategoryStruct.comp ((F.obj (Opposite.op i)).map f) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multifork.ι c j) (CategoryTheory.CategoryStruct.comp ((F.map f.op).app j) h)
• CategoryTheory.Limits.Wedge.ext_hom_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.End
  {J : Type u} [CategoryTheory.Category.{v, u} J] {C : Type u'} [CategoryTheory.Category.{v', u'} C] {F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)} {W₁ W₂ : CategoryTheory.Limits.Wedge F} (e : W₁.pt ≅ W₂.pt) (he : ∀ (j : J), CategoryTheory.Limits.Multifork.ι W₁ j = CategoryTheory.CategoryStruct.comp e.hom (CategoryTheory.Limits.Multifork.ι W₂ j) := by cat_disch) : (CategoryTheory.Limits.Wedge.ext e he).hom.hom = e.hom
• CategoryTheory.Limits.Wedge.ext_inv_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.End
  {J : Type u} [CategoryTheory.Category.{v, u} J] {C : Type u'} [CategoryTheory.Category.{v', u'} C] {F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)} {W₁ W₂ : CategoryTheory.Limits.Wedge F} (e : W₁.pt ≅ W₂.pt) (he : ∀ (j : J), CategoryTheory.Limits.Multifork.ι W₁ j = CategoryTheory.CategoryStruct.comp e.hom (CategoryTheory.Limits.Multifork.ι W₂ j) := by cat_disch) : (CategoryTheory.Limits.Wedge.ext e he).inv.hom = e.inv
• CategoryTheory.Limits.Wedge.IsLimit.lift_ι 📋 Mathlib.CategoryTheory.Limits.Shapes.End
  {J : Type u} [CategoryTheory.Category.{v, u} J] {C : Type u'} [CategoryTheory.Category.{v', u'} C] {F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)} {c : CategoryTheory.Limits.Wedge F} (hc : CategoryTheory.Limits.IsLimit c) {X : C} (f : (j : J) → X ⟶ (F.obj (Opposite.op j)).obj j) (hf : ∀ ⦃i j : J⦄ (g : i ⟶ j), CategoryTheory.CategoryStruct.comp (f i) ((F.obj (Opposite.op i)).map g) = CategoryTheory.CategoryStruct.comp (f j) ((F.map g.op).app j)) (j : J) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Wedge.IsLimit.lift hc f hf) (CategoryTheory.Limits.Multifork.ι c j) = f j
• CategoryTheory.Limits.Wedge.IsLimit.lift_ι_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.End
  {J : Type u} [CategoryTheory.Category.{v, u} J] {C : Type u'} [CategoryTheory.Category.{v', u'} C] {F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)} {c : CategoryTheory.Limits.Wedge F} (hc : CategoryTheory.Limits.IsLimit c) {X : C} (f : (j : J) → X ⟶ (F.obj (Opposite.op j)).obj j) (hf : ∀ ⦃i j : J⦄ (g : i ⟶ j), CategoryTheory.CategoryStruct.comp (f i) ((F.obj (Opposite.op i)).map g) = CategoryTheory.CategoryStruct.comp (f j) ((F.map g.op).app j)) (j : J) {Z : C} (h : (CategoryTheory.Limits.multicospanIndexEnd F).left j ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Wedge.IsLimit.lift hc f hf) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multifork.ι c j) h) = CategoryTheory.CategoryStruct.comp (f j) h
• CategoryTheory.PreZeroHypercover.sectionsSaturateEquiv_apply_coe 📋 Mathlib.CategoryTheory.Sites.Hypercover.Saturate
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {S : C} (E : CategoryTheory.PreZeroHypercover S) (F : CategoryTheory.Functor Cᵒᵖ (Type u_3)) (s : (E.saturate.multicospanIndex F).sections) (i : E.saturate.multicospanShape.L) : ↑((E.sectionsSaturateEquiv F) s) i = s.val i

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