Loogle!

Result

Found 105 declarations mentioning CategoryTheory.GradedObject.mapBifunctor.

• CategoryTheory.GradedObject.mapBifunctor 📋 Mathlib.CategoryTheory.GradedObject.Bifunctor
  {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Category.{v_3, u_3} C₃] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)) (I : Type u_4) (J : Type u_5) : CategoryTheory.Functor (CategoryTheory.GradedObject I C₁) (CategoryTheory.Functor (CategoryTheory.GradedObject J C₂) (CategoryTheory.GradedObject (I × J) C₃))
• CategoryTheory.GradedObject.mapBifunctorMapObj 📋 Mathlib.CategoryTheory.GradedObject.Bifunctor
  {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Category.{v_3, u_3} C₃] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)) {I : Type u_4} {J : Type u_5} {K : Type u_6} (p : I × J → K) (X : CategoryTheory.GradedObject I C₁) (Y : CategoryTheory.GradedObject J C₂) [(((CategoryTheory.GradedObject.mapBifunctor F I J).obj X).obj Y).HasMap p] : CategoryTheory.GradedObject K C₃
• CategoryTheory.GradedObject.mapBifunctor_obj_obj 📋 Mathlib.CategoryTheory.GradedObject.Bifunctor
  {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Category.{v_3, u_3} C₃] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)) (I : Type u_4) (J : Type u_5) (X : CategoryTheory.GradedObject I C₁) (Y : CategoryTheory.GradedObject J C₂) (ij : I × J) : ((CategoryTheory.GradedObject.mapBifunctor F I J).obj X).obj Y ij = (F.obj (X ij.1)).obj (Y ij.2)
• CategoryTheory.GradedObject.mapBifunctorMap 📋 Mathlib.CategoryTheory.GradedObject.Bifunctor
  {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Category.{v_3, u_3} C₃] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)) {I : Type u_4} {J : Type u_5} {K : Type u_6} (p : I × J → K) [∀ (X : CategoryTheory.GradedObject I C₁) (Y : CategoryTheory.GradedObject J C₂), (((CategoryTheory.GradedObject.mapBifunctor F I J).obj X).obj Y).HasMap p] : CategoryTheory.Functor (CategoryTheory.GradedObject I C₁) (CategoryTheory.Functor (CategoryTheory.GradedObject J C₂) (CategoryTheory.GradedObject K C₃))
• CategoryTheory.GradedObject.ιMapBifunctorMapObj 📋 Mathlib.CategoryTheory.GradedObject.Bifunctor
  {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Category.{v_3, u_3} C₃] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)) {I : Type u_4} {J : Type u_5} {K : Type u_6} (p : I × J → K) (X : CategoryTheory.GradedObject I C₁) (Y : CategoryTheory.GradedObject J C₂) [(((CategoryTheory.GradedObject.mapBifunctor F I J).obj X).obj Y).HasMap p] (i : I) (j : J) (k : K) (h : p (i, j) = k) : (F.obj (X i)).obj (Y j) ⟶ CategoryTheory.GradedObject.mapBifunctorMapObj F p X Y k
• CategoryTheory.GradedObject.mapBifunctorMapObjDesc 📋 Mathlib.CategoryTheory.GradedObject.Bifunctor
  {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Category.{v_3, u_3} C₃] {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)} {I : Type u_4} {J : Type u_5} {K : Type u_6} {p : I × J → K} {X : CategoryTheory.GradedObject I C₁} {Y : CategoryTheory.GradedObject J C₂} {A : C₃} {k : K} [(((CategoryTheory.GradedObject.mapBifunctor F I J).obj X).obj Y).HasMap p] (f : (i : I) → (j : J) → p (i, j) = k → ((F.obj (X i)).obj (Y j) ⟶ A)) : CategoryTheory.GradedObject.mapBifunctorMapObj F p X Y k ⟶ A
• CategoryTheory.GradedObject.mapBifunctorMap_obj_obj 📋 Mathlib.CategoryTheory.GradedObject.Bifunctor
  {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Category.{v_3, u_3} C₃] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)) {I : Type u_4} {J : Type u_5} {K : Type u_6} (p : I × J → K) [∀ (X : CategoryTheory.GradedObject I C₁) (Y : CategoryTheory.GradedObject J C₂), (((CategoryTheory.GradedObject.mapBifunctor F I J).obj X).obj Y).HasMap p] (X : CategoryTheory.GradedObject I C₁) (Y : CategoryTheory.GradedObject J C₂) : ((CategoryTheory.GradedObject.mapBifunctorMap F p).obj X).obj Y = CategoryTheory.GradedObject.mapBifunctorMapObj F p X Y
• CategoryTheory.GradedObject.mapBifunctor_obj_map 📋 Mathlib.CategoryTheory.GradedObject.Bifunctor
  {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Category.{v_3, u_3} C₃] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)) (I : Type u_4) (J : Type u_5) (X : CategoryTheory.GradedObject I C₁) {X✝ Y✝ : CategoryTheory.GradedObject J C₂} (φ : X✝ ⟶ Y✝) (ij : I × J) : ((CategoryTheory.GradedObject.mapBifunctor F I J).obj X).map φ ij = (F.obj (X ij.1)).map (φ ij.2)
• CategoryTheory.GradedObject.mapBifunctorMapMapIso 📋 Mathlib.CategoryTheory.GradedObject.Bifunctor
  {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Category.{v_3, u_3} C₃] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)) {I : Type u_4} {J : Type u_5} {K : Type u_6} (p : I × J → K) {X₁ X₂ : CategoryTheory.GradedObject I C₁} {Y₁ Y₂ : CategoryTheory.GradedObject J C₂} [(((CategoryTheory.GradedObject.mapBifunctor F I J).obj X₁).obj Y₁).HasMap p] [(((CategoryTheory.GradedObject.mapBifunctor F I J).obj X₂).obj Y₂).HasMap p] (e : X₁ ≅ X₂) (e' : Y₁ ≅ Y₂) : CategoryTheory.GradedObject.mapBifunctorMapObj F p X₁ Y₁ ≅ CategoryTheory.GradedObject.mapBifunctorMapObj F p X₂ Y₂
• CategoryTheory.GradedObject.mapBifunctorMapMap 📋 Mathlib.CategoryTheory.GradedObject.Bifunctor
  {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Category.{v_3, u_3} C₃] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)) {I : Type u_4} {J : Type u_5} {K : Type u_6} (p : I × J → K) {X₁ X₂ : CategoryTheory.GradedObject I C₁} (f : X₁ ⟶ X₂) {Y₁ Y₂ : CategoryTheory.GradedObject J C₂} (g : Y₁ ⟶ Y₂) [(((CategoryTheory.GradedObject.mapBifunctor F I J).obj X₁).obj Y₁).HasMap p] [(((CategoryTheory.GradedObject.mapBifunctor F I J).obj X₂).obj Y₂).HasMap p] : CategoryTheory.GradedObject.mapBifunctorMapObj F p X₁ Y₁ ⟶ CategoryTheory.GradedObject.mapBifunctorMapObj F p X₂ Y₂
• CategoryTheory.GradedObject.ι_mapBifunctorMapObjDesc 📋 Mathlib.CategoryTheory.GradedObject.Bifunctor
  {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Category.{v_3, u_3} C₃] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)) {I : Type u_4} {J : Type u_5} {K : Type u_6} (p : I × J → K) {X : CategoryTheory.GradedObject I C₁} {Y : CategoryTheory.GradedObject J C₂} {A : C₃} {k : K} [(((CategoryTheory.GradedObject.mapBifunctor F I J).obj X).obj Y).HasMap p] (f : (i : I) → (j : J) → p (i, j) = k → ((F.obj (X i)).obj (Y j) ⟶ A)) (i : I) (j : J) (hij : p (i, j) = k) : CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.ιMapBifunctorMapObj F p X Y i j k hij) (CategoryTheory.GradedObject.mapBifunctorMapObjDesc f) = f i j hij
• CategoryTheory.GradedObject.mapBifunctorMap_obj_map 📋 Mathlib.CategoryTheory.GradedObject.Bifunctor
  {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Category.{v_3, u_3} C₃] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)) {I : Type u_4} {J : Type u_5} {K : Type u_6} (p : I × J → K) [∀ (X : CategoryTheory.GradedObject I C₁) (Y : CategoryTheory.GradedObject J C₂), (((CategoryTheory.GradedObject.mapBifunctor F I J).obj X).obj Y).HasMap p] (X : CategoryTheory.GradedObject I C₁) {X✝ Y✝ : CategoryTheory.GradedObject J C₂} (ψ : X✝ ⟶ Y✝) (i : K) : ((CategoryTheory.GradedObject.mapBifunctorMap F p).obj X).map ψ i = CategoryTheory.GradedObject.mapBifunctorMapMap F p (CategoryTheory.CategoryStruct.id X) ψ i
• CategoryTheory.GradedObject.instIsIsoMapBifunctorMapMap 📋 Mathlib.CategoryTheory.GradedObject.Bifunctor
  {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Category.{v_3, u_3} C₃] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)) {I : Type u_4} {J : Type u_5} {K : Type u_6} (p : I × J → K) {X₁ X₂ : CategoryTheory.GradedObject I C₁} {Y₁ Y₂ : CategoryTheory.GradedObject J C₂} [(((CategoryTheory.GradedObject.mapBifunctor F I J).obj X₁).obj Y₁).HasMap p] [(((CategoryTheory.GradedObject.mapBifunctor F I J).obj X₂).obj Y₂).HasMap p] (f : X₁ ⟶ X₂) (g : Y₁ ⟶ Y₂) [CategoryTheory.IsIso f] [CategoryTheory.IsIso g] : CategoryTheory.IsIso (CategoryTheory.GradedObject.mapBifunctorMapMap F p f g)
• CategoryTheory.GradedObject.ι_mapBifunctorMapObjDesc_assoc 📋 Mathlib.CategoryTheory.GradedObject.Bifunctor
  {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Category.{v_3, u_3} C₃] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)) {I : Type u_4} {J : Type u_5} {K : Type u_6} (p : I × J → K) {X : CategoryTheory.GradedObject I C₁} {Y : CategoryTheory.GradedObject J C₂} {A : C₃} {k : K} [(((CategoryTheory.GradedObject.mapBifunctor F I J).obj X).obj Y).HasMap p] (f : (i : I) → (j : J) → p (i, j) = k → ((F.obj (X i)).obj (Y j) ⟶ A)) (i : I) (j : J) (hij : p (i, j) = k) {Z : C₃} (h : A ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.ιMapBifunctorMapObj F p X Y i j k hij) (CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.mapBifunctorMapObjDesc f) h) = CategoryTheory.CategoryStruct.comp (f i j hij) h
• CategoryTheory.GradedObject.mapBifunctorMapObj_ext 📋 Mathlib.CategoryTheory.GradedObject.Bifunctor
  {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Category.{v_3, u_3} C₃] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)) {I : Type u_4} {J : Type u_5} {K : Type u_6} (p : I × J → K) {X : CategoryTheory.GradedObject I C₁} {Y : CategoryTheory.GradedObject J C₂} {A : C₃} {k : K} [(((CategoryTheory.GradedObject.mapBifunctor F I J).obj X).obj Y).HasMap p] {f g : CategoryTheory.GradedObject.mapBifunctorMapObj F p X Y k ⟶ A} (h : ∀ (i : I) (j : J) (hij : p (i, j) = k), CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.ιMapBifunctorMapObj F p X Y i j k hij) f = CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.ιMapBifunctorMapObj F p X Y i j k hij) g) : f = g
• CategoryTheory.GradedObject.mapBifunctorMapObj_ext_iff 📋 Mathlib.CategoryTheory.GradedObject.Bifunctor
  {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Category.{v_3, u_3} C₃] {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)} {I : Type u_4} {J : Type u_5} {K : Type u_6} {p : I × J → K} {X : CategoryTheory.GradedObject I C₁} {Y : CategoryTheory.GradedObject J C₂} {A : C₃} {k : K} [(((CategoryTheory.GradedObject.mapBifunctor F I J).obj X).obj Y).HasMap p] {f g : CategoryTheory.GradedObject.mapBifunctorMapObj F p X Y k ⟶ A} : f = g ↔ ∀ (i : I) (j : J) (hij : p (i, j) = k), CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.ιMapBifunctorMapObj F p X Y i j k hij) f = CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.ιMapBifunctorMapObj F p X Y i j k hij) g
• CategoryTheory.GradedObject.mapBifunctorMapMapIso_hom 📋 Mathlib.CategoryTheory.GradedObject.Bifunctor
  {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Category.{v_3, u_3} C₃] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)) {I : Type u_4} {J : Type u_5} {K : Type u_6} (p : I × J → K) {X₁ X₂ : CategoryTheory.GradedObject I C₁} {Y₁ Y₂ : CategoryTheory.GradedObject J C₂} [(((CategoryTheory.GradedObject.mapBifunctor F I J).obj X₁).obj Y₁).HasMap p] [(((CategoryTheory.GradedObject.mapBifunctor F I J).obj X₂).obj Y₂).HasMap p] (e : X₁ ≅ X₂) (e' : Y₁ ≅ Y₂) (i : K) : (CategoryTheory.GradedObject.mapBifunctorMapMapIso F p e e').hom i = CategoryTheory.GradedObject.mapBifunctorMapMap F p e.hom e'.hom i
• CategoryTheory.GradedObject.mapBifunctorMapMapIso_inv 📋 Mathlib.CategoryTheory.GradedObject.Bifunctor
  {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Category.{v_3, u_3} C₃] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)) {I : Type u_4} {J : Type u_5} {K : Type u_6} (p : I × J → K) {X₁ X₂ : CategoryTheory.GradedObject I C₁} {Y₁ Y₂ : CategoryTheory.GradedObject J C₂} [(((CategoryTheory.GradedObject.mapBifunctor F I J).obj X₁).obj Y₁).HasMap p] [(((CategoryTheory.GradedObject.mapBifunctor F I J).obj X₂).obj Y₂).HasMap p] (e : X₁ ≅ X₂) (e' : Y₁ ≅ Y₂) (i : K) : (CategoryTheory.GradedObject.mapBifunctorMapMapIso F p e e').inv i = CategoryTheory.GradedObject.mapBifunctorMapMap F p e.inv e'.inv i
• CategoryTheory.GradedObject.mapBifunctorMap_map_app 📋 Mathlib.CategoryTheory.GradedObject.Bifunctor
  {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Category.{v_3, u_3} C₃] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)) {I : Type u_4} {J : Type u_5} {K : Type u_6} (p : I × J → K) [∀ (X : CategoryTheory.GradedObject I C₁) (Y : CategoryTheory.GradedObject J C₂), (((CategoryTheory.GradedObject.mapBifunctor F I J).obj X).obj Y).HasMap p] {X₁ X₂ : CategoryTheory.GradedObject I C₁} (φ : X₁ ⟶ X₂) (Y : CategoryTheory.GradedObject J C₂) (i : K) : ((CategoryTheory.GradedObject.mapBifunctorMap F p).map φ).app Y i = CategoryTheory.GradedObject.mapBifunctorMapMap F p φ (CategoryTheory.CategoryStruct.id Y) i
• CategoryTheory.GradedObject.mapBifunctor_map_app 📋 Mathlib.CategoryTheory.GradedObject.Bifunctor
  {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Category.{v_3, u_3} C₃] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)) (I : Type u_4) (J : Type u_5) {X✝ Y✝ : CategoryTheory.GradedObject I C₁} (φ : X✝ ⟶ Y✝) (Y : CategoryTheory.GradedObject J C₂) (ij : I × J) : ((CategoryTheory.GradedObject.mapBifunctor F I J).map φ).app Y ij = (F.map (φ ij.1)).app (Y ij.2)
• CategoryTheory.GradedObject.ι_mapBifunctorMapMap 📋 Mathlib.CategoryTheory.GradedObject.Bifunctor
  {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Category.{v_3, u_3} C₃] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)) {I : Type u_4} {J : Type u_5} {K : Type u_6} (p : I × J → K) {X₁ X₂ : CategoryTheory.GradedObject I C₁} (f : X₁ ⟶ X₂) {Y₁ Y₂ : CategoryTheory.GradedObject J C₂} (g : Y₁ ⟶ Y₂) [(((CategoryTheory.GradedObject.mapBifunctor F I J).obj X₁).obj Y₁).HasMap p] [(((CategoryTheory.GradedObject.mapBifunctor F I J).obj X₂).obj Y₂).HasMap p] (i : I) (j : J) (k : K) (h : p (i, j) = k) : CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.ιMapBifunctorMapObj F p X₁ Y₁ i j k h) (CategoryTheory.GradedObject.mapBifunctorMapMap F p f g k) = CategoryTheory.CategoryStruct.comp ((F.map (f i)).app (Y₁ j)) (CategoryTheory.CategoryStruct.comp ((F.obj (X₂ i)).map (g j)) (CategoryTheory.GradedObject.ιMapBifunctorMapObj F p X₂ Y₂ i j k h))
• CategoryTheory.GradedObject.ι_mapBifunctorMapMap_assoc 📋 Mathlib.CategoryTheory.GradedObject.Bifunctor
  {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Category.{v_3, u_3} C₃] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)) {I : Type u_4} {J : Type u_5} {K : Type u_6} (p : I × J → K) {X₁ X₂ : CategoryTheory.GradedObject I C₁} (f : X₁ ⟶ X₂) {Y₁ Y₂ : CategoryTheory.GradedObject J C₂} (g : Y₁ ⟶ Y₂) [(((CategoryTheory.GradedObject.mapBifunctor F I J).obj X₁).obj Y₁).HasMap p] [(((CategoryTheory.GradedObject.mapBifunctor F I J).obj X₂).obj Y₂).HasMap p] (i : I) (j : J) (k : K) (h : p (i, j) = k) {Z : C₃} (h✝ : CategoryTheory.GradedObject.mapBifunctorMapObj F p X₂ Y₂ k ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.ιMapBifunctorMapObj F p X₁ Y₁ i j k h) (CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.mapBifunctorMapMap F p f g k) h✝) = CategoryTheory.CategoryStruct.comp ((F.map (f i)).app (Y₁ j)) (CategoryTheory.CategoryStruct.comp ((F.obj (X₂ i)).map (g j)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.ιMapBifunctorMapObj F p X₂ Y₂ i j k h) h✝))
• CategoryTheory.GradedObject.ιMapBifunctor₁₂BifunctorMapObj 📋 Mathlib.CategoryTheory.GradedObject.Trifunctor
  {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₁₂ : Type u_5} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Category.{v_3, u_3} C₃] [CategoryTheory.Category.{v_4, u_4} C₄] [CategoryTheory.Category.{v_5, u_5} C₁₂] (F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)) (G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)) {I₁ : Type u_7} {I₂ : Type u_8} {I₃ : Type u_9} {J : Type u_10} {r : I₁ × I₂ × I₃ → J} (ρ₁₂ : CategoryTheory.GradedObject.BifunctorComp₁₂IndexData r) (X₁ : CategoryTheory.GradedObject I₁ C₁) (X₂ : CategoryTheory.GradedObject I₂ C₂) (X₃ : CategoryTheory.GradedObject I₃ C₃) [(((CategoryTheory.GradedObject.mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).HasMap ρ₁₂.p] [(((CategoryTheory.GradedObject.mapBifunctor G ρ₁₂.I₁₂ I₃).obj (CategoryTheory.GradedObject.mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj X₃).HasMap ρ₁₂.q] (i₁ : I₁) (i₂ : I₂) (i₃ : I₃) (j : J) (h : r (i₁, i₂, i₃) = j) : (G.obj ((F₁₂.obj (X₁ i₁)).obj (X₂ i₂))).obj (X₃ i₃) ⟶ CategoryTheory.GradedObject.mapBifunctorMapObj G ρ₁₂.q (CategoryTheory.GradedObject.mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂) X₃ j
• CategoryTheory.GradedObject.ιMapBifunctorBifunctor₂₃MapObj 📋 Mathlib.CategoryTheory.GradedObject.Trifunctor
  {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₂₃ : Type u_6} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Category.{v_3, u_3} C₃] [CategoryTheory.Category.{v_4, u_4} C₄] [CategoryTheory.Category.{v_6, u_6} C₂₃] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄)) (G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)) {I₁ : Type u_7} {I₂ : Type u_8} {I₃ : Type u_9} {J : Type u_10} {r : I₁ × I₂ × I₃ → J} (ρ₂₃ : CategoryTheory.GradedObject.BifunctorComp₂₃IndexData r) (X₁ : CategoryTheory.GradedObject I₁ C₁) (X₂ : CategoryTheory.GradedObject I₂ C₂) (X₃ : CategoryTheory.GradedObject I₃ C₃) [(((CategoryTheory.GradedObject.mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).HasMap ρ₂₃.p] [(((CategoryTheory.GradedObject.mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj (CategoryTheory.GradedObject.mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).HasMap ρ₂₃.q] (i₁ : I₁) (i₂ : I₂) (i₃ : I₃) (j : J) (h : r (i₁, i₂, i₃) = j) : (F.obj (X₁ i₁)).obj ((G₂₃.obj (X₂ i₂)).obj (X₃ i₃)) ⟶ CategoryTheory.GradedObject.mapBifunctorMapObj F ρ₂₃.q X₁ (CategoryTheory.GradedObject.mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃) j
• CategoryTheory.GradedObject.mapBifunctor₁₂BifunctorDesc 📋 Mathlib.CategoryTheory.GradedObject.Trifunctor
  {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₁₂ : Type u_5} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Category.{v_3, u_3} C₃] [CategoryTheory.Category.{v_4, u_4} C₄] [CategoryTheory.Category.{v_5, u_5} C₁₂] {F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)} {G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)} {I₁ : Type u_7} {I₂ : Type u_8} {I₃ : Type u_9} {J : Type u_10} {r : I₁ × I₂ × I₃ → J} {ρ₁₂ : CategoryTheory.GradedObject.BifunctorComp₁₂IndexData r} {X₁ : CategoryTheory.GradedObject I₁ C₁} {X₂ : CategoryTheory.GradedObject I₂ C₂} {X₃ : CategoryTheory.GradedObject I₃ C₃} [(((CategoryTheory.GradedObject.mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).HasMap ρ₁₂.p] [(((CategoryTheory.GradedObject.mapBifunctor G ρ₁₂.I₁₂ I₃).obj (CategoryTheory.GradedObject.mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj X₃).HasMap ρ₁₂.q] [H : CategoryTheory.GradedObject.HasGoodTrifunctor₁₂Obj F₁₂ G ρ₁₂ X₁ X₂ X₃] {j : J} {A : C₄} (f : (i₁ : I₁) → (i₂ : I₂) → (i₃ : I₃) → r (i₁, i₂, i₃) = j → ((G.obj ((F₁₂.obj (X₁ i₁)).obj (X₂ i₂))).obj (X₃ i₃) ⟶ A)) : CategoryTheory.GradedObject.mapBifunctorMapObj G ρ₁₂.q (CategoryTheory.GradedObject.mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂) X₃ j ⟶ A
• CategoryTheory.GradedObject.mapBifunctorBifunctor₂₃Desc 📋 Mathlib.CategoryTheory.GradedObject.Trifunctor
  {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₂₃ : Type u_6} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Category.{v_3, u_3} C₃] [CategoryTheory.Category.{v_4, u_4} C₄] [CategoryTheory.Category.{v_6, u_6} C₂₃] {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄)} {G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)} {I₁ : Type u_7} {I₂ : Type u_8} {I₃ : Type u_9} {J : Type u_10} {r : I₁ × I₂ × I₃ → J} {ρ₂₃ : CategoryTheory.GradedObject.BifunctorComp₂₃IndexData r} {X₁ : CategoryTheory.GradedObject I₁ C₁} {X₂ : CategoryTheory.GradedObject I₂ C₂} {X₃ : CategoryTheory.GradedObject I₃ C₃} [(((CategoryTheory.GradedObject.mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).HasMap ρ₂₃.p] [(((CategoryTheory.GradedObject.mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj (CategoryTheory.GradedObject.mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).HasMap ρ₂₃.q] [H : CategoryTheory.GradedObject.HasGoodTrifunctor₂₃Obj F G₂₃ ρ₂₃ X₁ X₂ X₃] {j : J} {A : C₄} (f : (i₁ : I₁) → (i₂ : I₂) → (i₃ : I₃) → r (i₁, i₂, i₃) = j → ((F.obj (X₁ i₁)).obj ((G₂₃.obj (X₂ i₂)).obj (X₃ i₃)) ⟶ A)) : CategoryTheory.GradedObject.mapBifunctorMapObj F ρ₂₃.q X₁ (CategoryTheory.GradedObject.mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃) j ⟶ A
• CategoryTheory.GradedObject.cofan₃MapBifunctor₁₂BifunctorMapObj 📋 Mathlib.CategoryTheory.GradedObject.Trifunctor
  {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₁₂ : Type u_5} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Category.{v_3, u_3} C₃] [CategoryTheory.Category.{v_4, u_4} C₄] [CategoryTheory.Category.{v_5, u_5} C₁₂] (F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)) (G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)) {I₁ : Type u_7} {I₂ : Type u_8} {I₃ : Type u_9} {J : Type u_10} {r : I₁ × I₂ × I₃ → J} (ρ₁₂ : CategoryTheory.GradedObject.BifunctorComp₁₂IndexData r) (X₁ : CategoryTheory.GradedObject I₁ C₁) (X₂ : CategoryTheory.GradedObject I₂ C₂) (X₃ : CategoryTheory.GradedObject I₃ C₃) [(((CategoryTheory.GradedObject.mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).HasMap ρ₁₂.p] [(((CategoryTheory.GradedObject.mapBifunctor G ρ₁₂.I₁₂ I₃).obj (CategoryTheory.GradedObject.mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj X₃).HasMap ρ₁₂.q] (j : J) : ((((CategoryTheory.GradedObject.mapTrifunctor (CategoryTheory.bifunctorComp₁₂ F₁₂ G) I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).CofanMapObjFun r j
• CategoryTheory.GradedObject.HasGoodTrifunctor₁₂Obj.hasMap 📋 Mathlib.CategoryTheory.GradedObject.Trifunctor
  {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₁₂ : Type u_5} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Category.{v_3, u_3} C₃] [CategoryTheory.Category.{v_4, u_4} C₄] [CategoryTheory.Category.{v_5, u_5} C₁₂] {F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)} {G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)} {I₁ : Type u_7} {I₂ : Type u_8} {I₃ : Type u_9} {J : Type u_10} {r : I₁ × I₂ × I₃ → J} {ρ₁₂ : CategoryTheory.GradedObject.BifunctorComp₁₂IndexData r} {X₁ : CategoryTheory.GradedObject I₁ C₁} {X₂ : CategoryTheory.GradedObject I₂ C₂} {X₃ : CategoryTheory.GradedObject I₃ C₃} [(((CategoryTheory.GradedObject.mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).HasMap ρ₁₂.p] [(((CategoryTheory.GradedObject.mapBifunctor G ρ₁₂.I₁₂ I₃).obj (CategoryTheory.GradedObject.mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj X₃).HasMap ρ₁₂.q] [H : CategoryTheory.GradedObject.HasGoodTrifunctor₁₂Obj F₁₂ G ρ₁₂ X₁ X₂ X₃] : ((((CategoryTheory.GradedObject.mapTrifunctor (CategoryTheory.bifunctorComp₁₂ F₁₂ G) I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap r
• CategoryTheory.GradedObject.cofan₃MapBifunctorBifunctor₂₃MapObj 📋 Mathlib.CategoryTheory.GradedObject.Trifunctor
  {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₂₃ : Type u_6} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Category.{v_3, u_3} C₃] [CategoryTheory.Category.{v_4, u_4} C₄] [CategoryTheory.Category.{v_6, u_6} C₂₃] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄)) (G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)) {I₁ : Type u_7} {I₂ : Type u_8} {I₃ : Type u_9} {J : Type u_10} {r : I₁ × I₂ × I₃ → J} (ρ₂₃ : CategoryTheory.GradedObject.BifunctorComp₂₃IndexData r) (X₁ : CategoryTheory.GradedObject I₁ C₁) (X₂ : CategoryTheory.GradedObject I₂ C₂) (X₃ : CategoryTheory.GradedObject I₃ C₃) [(((CategoryTheory.GradedObject.mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).HasMap ρ₂₃.p] [(((CategoryTheory.GradedObject.mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj (CategoryTheory.GradedObject.mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).HasMap ρ₂₃.q] (j : J) : ((((CategoryTheory.GradedObject.mapTrifunctor (CategoryTheory.bifunctorComp₂₃ F G₂₃) I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).CofanMapObjFun r j
• CategoryTheory.GradedObject.HasGoodTrifunctor₂₃Obj.hasMap 📋 Mathlib.CategoryTheory.GradedObject.Trifunctor
  {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₂₃ : Type u_6} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Category.{v_3, u_3} C₃] [CategoryTheory.Category.{v_4, u_4} C₄] [CategoryTheory.Category.{v_6, u_6} C₂₃] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄)) (G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)) {I₁ : Type u_7} {I₂ : Type u_8} {I₃ : Type u_9} {J : Type u_10} {r : I₁ × I₂ × I₃ → J} (ρ₂₃ : CategoryTheory.GradedObject.BifunctorComp₂₃IndexData r) {X₁ : CategoryTheory.GradedObject I₁ C₁} {X₂ : CategoryTheory.GradedObject I₂ C₂} {X₃ : CategoryTheory.GradedObject I₃ C₃} [(((CategoryTheory.GradedObject.mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).HasMap ρ₂₃.p] [(((CategoryTheory.GradedObject.mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj (CategoryTheory.GradedObject.mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).HasMap ρ₂₃.q] [H : CategoryTheory.GradedObject.HasGoodTrifunctor₂₃Obj F G₂₃ ρ₂₃ X₁ X₂ X₃] : ((((CategoryTheory.GradedObject.mapTrifunctor (CategoryTheory.bifunctorComp₂₃ F G₂₃) I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap r
• CategoryTheory.GradedObject.ι_mapBifunctor₁₂BifunctorDesc 📋 Mathlib.CategoryTheory.GradedObject.Trifunctor
  {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₁₂ : Type u_5} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Category.{v_3, u_3} C₃] [CategoryTheory.Category.{v_4, u_4} C₄] [CategoryTheory.Category.{v_5, u_5} C₁₂] {F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)} {G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)} {I₁ : Type u_7} {I₂ : Type u_8} {I₃ : Type u_9} {J : Type u_10} {r : I₁ × I₂ × I₃ → J} {ρ₁₂ : CategoryTheory.GradedObject.BifunctorComp₁₂IndexData r} {X₁ : CategoryTheory.GradedObject I₁ C₁} {X₂ : CategoryTheory.GradedObject I₂ C₂} {X₃ : CategoryTheory.GradedObject I₃ C₃} [(((CategoryTheory.GradedObject.mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).HasMap ρ₁₂.p] [(((CategoryTheory.GradedObject.mapBifunctor G ρ₁₂.I₁₂ I₃).obj (CategoryTheory.GradedObject.mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj X₃).HasMap ρ₁₂.q] [H : CategoryTheory.GradedObject.HasGoodTrifunctor₁₂Obj F₁₂ G ρ₁₂ X₁ X₂ X₃] {j : J} {A : C₄} (f : (i₁ : I₁) → (i₂ : I₂) → (i₃ : I₃) → r (i₁, i₂, i₃) = j → ((G.obj ((F₁₂.obj (X₁ i₁)).obj (X₂ i₂))).obj (X₃ i₃) ⟶ A)) (i₁ : I₁) (i₂ : I₂) (i₃ : I₃) (h : r (i₁, i₂, i₃) = j) : CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.ιMapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ i₁ i₂ i₃ j h) (CategoryTheory.GradedObject.mapBifunctor₁₂BifunctorDesc f) = f i₁ i₂ i₃ h
• CategoryTheory.GradedObject.mapBifunctorComp₁₂MapObjIso 📋 Mathlib.CategoryTheory.GradedObject.Trifunctor
  {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₁₂ : Type u_5} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Category.{v_3, u_3} C₃] [CategoryTheory.Category.{v_4, u_4} C₄] [CategoryTheory.Category.{v_5, u_5} C₁₂] (F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)) (G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)) {I₁ : Type u_7} {I₂ : Type u_8} {I₃ : Type u_9} {J : Type u_10} {r : I₁ × I₂ × I₃ → J} (ρ₁₂ : CategoryTheory.GradedObject.BifunctorComp₁₂IndexData r) (X₁ : CategoryTheory.GradedObject I₁ C₁) (X₂ : CategoryTheory.GradedObject I₂ C₂) (X₃ : CategoryTheory.GradedObject I₃ C₃) [(((CategoryTheory.GradedObject.mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).HasMap ρ₁₂.p] [(((CategoryTheory.GradedObject.mapBifunctor G ρ₁₂.I₁₂ I₃).obj (CategoryTheory.GradedObject.mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj X₃).HasMap ρ₁₂.q] [H : CategoryTheory.GradedObject.HasGoodTrifunctor₁₂Obj F₁₂ G ρ₁₂ X₁ X₂ X₃] [((((CategoryTheory.GradedObject.mapTrifunctor (CategoryTheory.bifunctorComp₁₂ F₁₂ G) I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap r] : CategoryTheory.GradedObject.mapTrifunctorMapObj (CategoryTheory.bifunctorComp₁₂ F₁₂ G) r X₁ X₂ X₃ ≅ CategoryTheory.GradedObject.mapBifunctorMapObj G ρ₁₂.q (CategoryTheory.GradedObject.mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂) X₃
• CategoryTheory.GradedObject.isColimitCofan₃MapBifunctor₁₂BifunctorMapObj 📋 Mathlib.CategoryTheory.GradedObject.Trifunctor
  {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₁₂ : Type u_5} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Category.{v_3, u_3} C₃] [CategoryTheory.Category.{v_4, u_4} C₄] [CategoryTheory.Category.{v_5, u_5} C₁₂] (F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)) (G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)) {I₁ : Type u_7} {I₂ : Type u_8} {I₃ : Type u_9} {J : Type u_10} {r : I₁ × I₂ × I₃ → J} (ρ₁₂ : CategoryTheory.GradedObject.BifunctorComp₁₂IndexData r) (X₁ : CategoryTheory.GradedObject I₁ C₁) (X₂ : CategoryTheory.GradedObject I₂ C₂) (X₃ : CategoryTheory.GradedObject I₃ C₃) [(((CategoryTheory.GradedObject.mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).HasMap ρ₁₂.p] [(((CategoryTheory.GradedObject.mapBifunctor G ρ₁₂.I₁₂ I₃).obj (CategoryTheory.GradedObject.mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj X₃).HasMap ρ₁₂.q] [H : CategoryTheory.GradedObject.HasGoodTrifunctor₁₂Obj F₁₂ G ρ₁₂ X₁ X₂ X₃] (j : J) : CategoryTheory.Limits.IsColimit (CategoryTheory.GradedObject.cofan₃MapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ j)
• CategoryTheory.GradedObject.ι_mapBifunctorBifunctor₂₃Desc 📋 Mathlib.CategoryTheory.GradedObject.Trifunctor
  {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₂₃ : Type u_6} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Category.{v_3, u_3} C₃] [CategoryTheory.Category.{v_4, u_4} C₄] [CategoryTheory.Category.{v_6, u_6} C₂₃] {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄)} {G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)} {I₁ : Type u_7} {I₂ : Type u_8} {I₃ : Type u_9} {J : Type u_10} {r : I₁ × I₂ × I₃ → J} {ρ₂₃ : CategoryTheory.GradedObject.BifunctorComp₂₃IndexData r} {X₁ : CategoryTheory.GradedObject I₁ C₁} {X₂ : CategoryTheory.GradedObject I₂ C₂} {X₃ : CategoryTheory.GradedObject I₃ C₃} [(((CategoryTheory.GradedObject.mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).HasMap ρ₂₃.p] [(((CategoryTheory.GradedObject.mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj (CategoryTheory.GradedObject.mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).HasMap ρ₂₃.q] [H : CategoryTheory.GradedObject.HasGoodTrifunctor₂₃Obj F G₂₃ ρ₂₃ X₁ X₂ X₃] {j : J} {A : C₄} (f : (i₁ : I₁) → (i₂ : I₂) → (i₃ : I₃) → r (i₁, i₂, i₃) = j → ((F.obj (X₁ i₁)).obj ((G₂₃.obj (X₂ i₂)).obj (X₃ i₃)) ⟶ A)) (i₁ : I₁) (i₂ : I₂) (i₃ : I₃) (h : r (i₁, i₂, i₃) = j) : CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.ιMapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ i₁ i₂ i₃ j h) (CategoryTheory.GradedObject.mapBifunctorBifunctor₂₃Desc f) = f i₁ i₂ i₃ h
• CategoryTheory.GradedObject.mapBifunctorComp₂₃MapObjIso 📋 Mathlib.CategoryTheory.GradedObject.Trifunctor
  {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₂₃ : Type u_6} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Category.{v_3, u_3} C₃] [CategoryTheory.Category.{v_4, u_4} C₄] [CategoryTheory.Category.{v_6, u_6} C₂₃] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄)) (G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)) {I₁ : Type u_7} {I₂ : Type u_8} {I₃ : Type u_9} {J : Type u_10} {r : I₁ × I₂ × I₃ → J} (ρ₂₃ : CategoryTheory.GradedObject.BifunctorComp₂₃IndexData r) (X₁ : CategoryTheory.GradedObject I₁ C₁) (X₂ : CategoryTheory.GradedObject I₂ C₂) (X₃ : CategoryTheory.GradedObject I₃ C₃) [(((CategoryTheory.GradedObject.mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).HasMap ρ₂₃.p] [(((CategoryTheory.GradedObject.mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj (CategoryTheory.GradedObject.mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).HasMap ρ₂₃.q] [H : CategoryTheory.GradedObject.HasGoodTrifunctor₂₃Obj F G₂₃ ρ₂₃ X₁ X₂ X₃] [((((CategoryTheory.GradedObject.mapTrifunctor (CategoryTheory.bifunctorComp₂₃ F G₂₃) I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap r] : CategoryTheory.GradedObject.mapTrifunctorMapObj (CategoryTheory.bifunctorComp₂₃ F G₂₃) r X₁ X₂ X₃ ≅ CategoryTheory.GradedObject.mapBifunctorMapObj F ρ₂₃.q X₁ (CategoryTheory.GradedObject.mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)
• CategoryTheory.GradedObject.isColimitCofan₃MapBifunctorBifunctor₂₃MapObj 📋 Mathlib.CategoryTheory.GradedObject.Trifunctor
  {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₂₃ : Type u_6} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Category.{v_3, u_3} C₃] [CategoryTheory.Category.{v_4, u_4} C₄] [CategoryTheory.Category.{v_6, u_6} C₂₃] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄)) (G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)) {I₁ : Type u_7} {I₂ : Type u_8} {I₃ : Type u_9} {J : Type u_10} {r : I₁ × I₂ × I₃ → J} (ρ₂₃ : CategoryTheory.GradedObject.BifunctorComp₂₃IndexData r) (X₁ : CategoryTheory.GradedObject I₁ C₁) (X₂ : CategoryTheory.GradedObject I₂ C₂) (X₃ : CategoryTheory.GradedObject I₃ C₃) [(((CategoryTheory.GradedObject.mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).HasMap ρ₂₃.p] [(((CategoryTheory.GradedObject.mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj (CategoryTheory.GradedObject.mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).HasMap ρ₂₃.q] [H : CategoryTheory.GradedObject.HasGoodTrifunctor₂₃Obj F G₂₃ ρ₂₃ X₁ X₂ X₃] (j : J) : CategoryTheory.Limits.IsColimit (CategoryTheory.GradedObject.cofan₃MapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ j)
• CategoryTheory.GradedObject.ι_mapBifunctor₁₂BifunctorDesc_assoc 📋 Mathlib.CategoryTheory.GradedObject.Trifunctor
  {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₁₂ : Type u_5} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Category.{v_3, u_3} C₃] [CategoryTheory.Category.{v_4, u_4} C₄] [CategoryTheory.Category.{v_5, u_5} C₁₂] {F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)} {G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)} {I₁ : Type u_7} {I₂ : Type u_8} {I₃ : Type u_9} {J : Type u_10} {r : I₁ × I₂ × I₃ → J} {ρ₁₂ : CategoryTheory.GradedObject.BifunctorComp₁₂IndexData r} {X₁ : CategoryTheory.GradedObject I₁ C₁} {X₂ : CategoryTheory.GradedObject I₂ C₂} {X₃ : CategoryTheory.GradedObject I₃ C₃} [(((CategoryTheory.GradedObject.mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).HasMap ρ₁₂.p] [(((CategoryTheory.GradedObject.mapBifunctor G ρ₁₂.I₁₂ I₃).obj (CategoryTheory.GradedObject.mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj X₃).HasMap ρ₁₂.q] [H : CategoryTheory.GradedObject.HasGoodTrifunctor₁₂Obj F₁₂ G ρ₁₂ X₁ X₂ X₃] {j : J} {A : C₄} (f : (i₁ : I₁) → (i₂ : I₂) → (i₃ : I₃) → r (i₁, i₂, i₃) = j → ((G.obj ((F₁₂.obj (X₁ i₁)).obj (X₂ i₂))).obj (X₃ i₃) ⟶ A)) (i₁ : I₁) (i₂ : I₂) (i₃ : I₃) (h : r (i₁, i₂, i₃) = j) {Z : C₄} (h✝ : A ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.ιMapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ i₁ i₂ i₃ j h) (CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.mapBifunctor₁₂BifunctorDesc f) h✝) = CategoryTheory.CategoryStruct.comp (f i₁ i₂ i₃ h) h✝
• CategoryTheory.GradedObject.ι_mapBifunctorBifunctor₂₃Desc_assoc 📋 Mathlib.CategoryTheory.GradedObject.Trifunctor
  {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₂₃ : Type u_6} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Category.{v_3, u_3} C₃] [CategoryTheory.Category.{v_4, u_4} C₄] [CategoryTheory.Category.{v_6, u_6} C₂₃] {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄)} {G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)} {I₁ : Type u_7} {I₂ : Type u_8} {I₃ : Type u_9} {J : Type u_10} {r : I₁ × I₂ × I₃ → J} {ρ₂₃ : CategoryTheory.GradedObject.BifunctorComp₂₃IndexData r} {X₁ : CategoryTheory.GradedObject I₁ C₁} {X₂ : CategoryTheory.GradedObject I₂ C₂} {X₃ : CategoryTheory.GradedObject I₃ C₃} [(((CategoryTheory.GradedObject.mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).HasMap ρ₂₃.p] [(((CategoryTheory.GradedObject.mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj (CategoryTheory.GradedObject.mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).HasMap ρ₂₃.q] [H : CategoryTheory.GradedObject.HasGoodTrifunctor₂₃Obj F G₂₃ ρ₂₃ X₁ X₂ X₃] {j : J} {A : C₄} (f : (i₁ : I₁) → (i₂ : I₂) → (i₃ : I₃) → r (i₁, i₂, i₃) = j → ((F.obj (X₁ i₁)).obj ((G₂₃.obj (X₂ i₂)).obj (X₃ i₃)) ⟶ A)) (i₁ : I₁) (i₂ : I₂) (i₃ : I₃) (h : r (i₁, i₂, i₃) = j) {Z : C₄} (h✝ : A ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.ιMapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ i₁ i₂ i₃ j h) (CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.mapBifunctorBifunctor₂₃Desc f) h✝) = CategoryTheory.CategoryStruct.comp (f i₁ i₂ i₃ h) h✝
• CategoryTheory.GradedObject.ιMapBifunctorBifunctor₂₃MapObj_eq 📋 Mathlib.CategoryTheory.GradedObject.Trifunctor
  {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₂₃ : Type u_6} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Category.{v_3, u_3} C₃] [CategoryTheory.Category.{v_4, u_4} C₄] [CategoryTheory.Category.{v_6, u_6} C₂₃] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄)) (G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)) {I₁ : Type u_7} {I₂ : Type u_8} {I₃ : Type u_9} {J : Type u_10} {r : I₁ × I₂ × I₃ → J} (ρ₂₃ : CategoryTheory.GradedObject.BifunctorComp₂₃IndexData r) (X₁ : CategoryTheory.GradedObject I₁ C₁) (X₂ : CategoryTheory.GradedObject I₂ C₂) (X₃ : CategoryTheory.GradedObject I₃ C₃) [(((CategoryTheory.GradedObject.mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).HasMap ρ₂₃.p] [(((CategoryTheory.GradedObject.mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj (CategoryTheory.GradedObject.mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).HasMap ρ₂₃.q] (i₁ : I₁) (i₂ : I₂) (i₃ : I₃) (j : J) (h : r (i₁, i₂, i₃) = j) (i₂₃ : ρ₂₃.I₂₃) (h₂₃ : ρ₂₃.p (i₂, i₃) = i₂₃) : CategoryTheory.GradedObject.ιMapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ i₁ i₂ i₃ j h = CategoryTheory.CategoryStruct.comp ((F.obj (X₁ i₁)).map (CategoryTheory.GradedObject.ιMapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃ i₂ i₃ i₂₃ h₂₃)) (CategoryTheory.GradedObject.ιMapBifunctorMapObj F ρ₂₃.q X₁ (CategoryTheory.GradedObject.mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃) i₁ i₂₃ j ⋯)
• CategoryTheory.GradedObject.mapBifunctor₁₂BifunctorMapObj_ext 📋 Mathlib.CategoryTheory.GradedObject.Trifunctor
  {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₁₂ : Type u_5} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Category.{v_3, u_3} C₃] [CategoryTheory.Category.{v_4, u_4} C₄] [CategoryTheory.Category.{v_5, u_5} C₁₂] {F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)} {G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)} {I₁ : Type u_7} {I₂ : Type u_8} {I₃ : Type u_9} {J : Type u_10} {r : I₁ × I₂ × I₃ → J} {ρ₁₂ : CategoryTheory.GradedObject.BifunctorComp₁₂IndexData r} {X₁ : CategoryTheory.GradedObject I₁ C₁} {X₂ : CategoryTheory.GradedObject I₂ C₂} {X₃ : CategoryTheory.GradedObject I₃ C₃} [(((CategoryTheory.GradedObject.mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).HasMap ρ₁₂.p] [(((CategoryTheory.GradedObject.mapBifunctor G ρ₁₂.I₁₂ I₃).obj (CategoryTheory.GradedObject.mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj X₃).HasMap ρ₁₂.q] [H : CategoryTheory.GradedObject.HasGoodTrifunctor₁₂Obj F₁₂ G ρ₁₂ X₁ X₂ X₃] {j : J} {A : C₄} {f g : CategoryTheory.GradedObject.mapBifunctorMapObj G ρ₁₂.q (CategoryTheory.GradedObject.mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂) X₃ j ⟶ A} (h : ∀ (i₁ : I₁) (i₂ : I₂) (i₃ : I₃) (h : r (i₁, i₂, i₃) = j), CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.ιMapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ i₁ i₂ i₃ j h) f = CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.ιMapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ i₁ i₂ i₃ j h) g) : f = g
• CategoryTheory.GradedObject.mapBifunctor₁₂BifunctorMapObj_ext_iff 📋 Mathlib.CategoryTheory.GradedObject.Trifunctor
  {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₁₂ : Type u_5} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Category.{v_3, u_3} C₃] [CategoryTheory.Category.{v_4, u_4} C₄] [CategoryTheory.Category.{v_5, u_5} C₁₂] {F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)} {G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)} {I₁ : Type u_7} {I₂ : Type u_8} {I₃ : Type u_9} {J : Type u_10} {r : I₁ × I₂ × I₃ → J} {ρ₁₂ : CategoryTheory.GradedObject.BifunctorComp₁₂IndexData r} {X₁ : CategoryTheory.GradedObject I₁ C₁} {X₂ : CategoryTheory.GradedObject I₂ C₂} {X₃ : CategoryTheory.GradedObject I₃ C₃} [(((CategoryTheory.GradedObject.mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).HasMap ρ₁₂.p] [(((CategoryTheory.GradedObject.mapBifunctor G ρ₁₂.I₁₂ I₃).obj (CategoryTheory.GradedObject.mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj X₃).HasMap ρ₁₂.q] [H : CategoryTheory.GradedObject.HasGoodTrifunctor₁₂Obj F₁₂ G ρ₁₂ X₁ X₂ X₃] {j : J} {A : C₄} {f g : CategoryTheory.GradedObject.mapBifunctorMapObj G ρ₁₂.q (CategoryTheory.GradedObject.mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂) X₃ j ⟶ A} : f = g ↔ ∀ (i₁ : I₁) (i₂ : I₂) (i₃ : I₃) (h : r (i₁, i₂, i₃) = j), CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.ιMapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ i₁ i₂ i₃ j h) f = CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.ιMapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ i₁ i₂ i₃ j h) g
• CategoryTheory.GradedObject.mapBifunctorBifunctor₂₃MapObj_ext 📋 Mathlib.CategoryTheory.GradedObject.Trifunctor
  {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₂₃ : Type u_6} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Category.{v_3, u_3} C₃] [CategoryTheory.Category.{v_4, u_4} C₄] [CategoryTheory.Category.{v_6, u_6} C₂₃] {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄)} {G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)} {I₁ : Type u_7} {I₂ : Type u_8} {I₃ : Type u_9} {J : Type u_10} {r : I₁ × I₂ × I₃ → J} {ρ₂₃ : CategoryTheory.GradedObject.BifunctorComp₂₃IndexData r} {X₁ : CategoryTheory.GradedObject I₁ C₁} {X₂ : CategoryTheory.GradedObject I₂ C₂} {X₃ : CategoryTheory.GradedObject I₃ C₃} [(((CategoryTheory.GradedObject.mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).HasMap ρ₂₃.p] [(((CategoryTheory.GradedObject.mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj (CategoryTheory.GradedObject.mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).HasMap ρ₂₃.q] [H : CategoryTheory.GradedObject.HasGoodTrifunctor₂₃Obj F G₂₃ ρ₂₃ X₁ X₂ X₃] {j : J} {A : C₄} {f g : CategoryTheory.GradedObject.mapBifunctorMapObj F ρ₂₃.q X₁ (CategoryTheory.GradedObject.mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃) j ⟶ A} (h : ∀ (i₁ : I₁) (i₂ : I₂) (i₃ : I₃) (h : r (i₁, i₂, i₃) = j), CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.ιMapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ i₁ i₂ i₃ j h) f = CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.ιMapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ i₁ i₂ i₃ j h) g) : f = g
• CategoryTheory.GradedObject.mapBifunctorBifunctor₂₃MapObj_ext_iff 📋 Mathlib.CategoryTheory.GradedObject.Trifunctor
  {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₂₃ : Type u_6} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Category.{v_3, u_3} C₃] [CategoryTheory.Category.{v_4, u_4} C₄] [CategoryTheory.Category.{v_6, u_6} C₂₃] {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄)} {G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)} {I₁ : Type u_7} {I₂ : Type u_8} {I₃ : Type u_9} {J : Type u_10} {r : I₁ × I₂ × I₃ → J} {ρ₂₃ : CategoryTheory.GradedObject.BifunctorComp₂₃IndexData r} {X₁ : CategoryTheory.GradedObject I₁ C₁} {X₂ : CategoryTheory.GradedObject I₂ C₂} {X₃ : CategoryTheory.GradedObject I₃ C₃} [(((CategoryTheory.GradedObject.mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).HasMap ρ₂₃.p] [(((CategoryTheory.GradedObject.mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj (CategoryTheory.GradedObject.mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).HasMap ρ₂₃.q] [H : CategoryTheory.GradedObject.HasGoodTrifunctor₂₃Obj F G₂₃ ρ₂₃ X₁ X₂ X₃] {j : J} {A : C₄} {f g : CategoryTheory.GradedObject.mapBifunctorMapObj F ρ₂₃.q X₁ (CategoryTheory.GradedObject.mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃) j ⟶ A} : f = g ↔ ∀ (i₁ : I₁) (i₂ : I₂) (i₃ : I₃) (h : r (i₁, i₂, i₃) = j), CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.ιMapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ i₁ i₂ i₃ j h) f = CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.ιMapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ i₁ i₂ i₃ j h) g
• CategoryTheory.GradedObject.ιMapBifunctor₁₂BifunctorMapObj_eq 📋 Mathlib.CategoryTheory.GradedObject.Trifunctor
  {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₁₂ : Type u_5} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Category.{v_3, u_3} C₃] [CategoryTheory.Category.{v_4, u_4} C₄] [CategoryTheory.Category.{v_5, u_5} C₁₂] (F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)) (G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)) {I₁ : Type u_7} {I₂ : Type u_8} {I₃ : Type u_9} {J : Type u_10} {r : I₁ × I₂ × I₃ → J} (ρ₁₂ : CategoryTheory.GradedObject.BifunctorComp₁₂IndexData r) (X₁ : CategoryTheory.GradedObject I₁ C₁) (X₂ : CategoryTheory.GradedObject I₂ C₂) (X₃ : CategoryTheory.GradedObject I₃ C₃) [(((CategoryTheory.GradedObject.mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).HasMap ρ₁₂.p] [(((CategoryTheory.GradedObject.mapBifunctor G ρ₁₂.I₁₂ I₃).obj (CategoryTheory.GradedObject.mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj X₃).HasMap ρ₁₂.q] (i₁ : I₁) (i₂ : I₂) (i₃ : I₃) (j : J) (h : r (i₁, i₂, i₃) = j) (i₁₂ : ρ₁₂.I₁₂) (h₁₂ : ρ₁₂.p (i₁, i₂) = i₁₂) : CategoryTheory.GradedObject.ιMapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ i₁ i₂ i₃ j h = CategoryTheory.CategoryStruct.comp ((G.map (CategoryTheory.GradedObject.ιMapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂ i₁ i₂ i₁₂ h₁₂)).app (X₃ i₃)) (CategoryTheory.GradedObject.ιMapBifunctorMapObj G ρ₁₂.q (CategoryTheory.GradedObject.mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂) X₃ i₁₂ i₃ j ⋯)
• CategoryTheory.GradedObject.ι_mapBifunctorComp₁₂MapObjIso_inv 📋 Mathlib.CategoryTheory.GradedObject.Trifunctor
  {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₁₂ : Type u_5} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Category.{v_3, u_3} C₃] [CategoryTheory.Category.{v_4, u_4} C₄] [CategoryTheory.Category.{v_5, u_5} C₁₂] (F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)) (G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)) {I₁ : Type u_7} {I₂ : Type u_8} {I₃ : Type u_9} {J : Type u_10} {r : I₁ × I₂ × I₃ → J} (ρ₁₂ : CategoryTheory.GradedObject.BifunctorComp₁₂IndexData r) (X₁ : CategoryTheory.GradedObject I₁ C₁) (X₂ : CategoryTheory.GradedObject I₂ C₂) (X₃ : CategoryTheory.GradedObject I₃ C₃) [(((CategoryTheory.GradedObject.mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).HasMap ρ₁₂.p] [(((CategoryTheory.GradedObject.mapBifunctor G ρ₁₂.I₁₂ I₃).obj (CategoryTheory.GradedObject.mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj X₃).HasMap ρ₁₂.q] [H : CategoryTheory.GradedObject.HasGoodTrifunctor₁₂Obj F₁₂ G ρ₁₂ X₁ X₂ X₃] [((((CategoryTheory.GradedObject.mapTrifunctor (CategoryTheory.bifunctorComp₁₂ F₁₂ G) I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap r] (i₁ : I₁) (i₂ : I₂) (i₃ : I₃) (j : J) (h : r (i₁, i₂, i₃) = j) : CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.ιMapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ i₁ i₂ i₃ j h) ((CategoryTheory.GradedObject.mapBifunctorComp₁₂MapObjIso F₁₂ G ρ₁₂ X₁ X₂ X₃).inv j) = CategoryTheory.GradedObject.ιMapTrifunctorMapObj (CategoryTheory.bifunctorComp₁₂ F₁₂ G) r X₁ X₂ X₃ i₁ i₂ i₃ j h
• CategoryTheory.GradedObject.ι_mapBifunctorComp₂₃MapObjIso_inv 📋 Mathlib.CategoryTheory.GradedObject.Trifunctor
  {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₂₃ : Type u_6} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Category.{v_3, u_3} C₃] [CategoryTheory.Category.{v_4, u_4} C₄] [CategoryTheory.Category.{v_6, u_6} C₂₃] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄)) (G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)) {I₁ : Type u_7} {I₂ : Type u_8} {I₃ : Type u_9} {J : Type u_10} {r : I₁ × I₂ × I₃ → J} (ρ₂₃ : CategoryTheory.GradedObject.BifunctorComp₂₃IndexData r) (X₁ : CategoryTheory.GradedObject I₁ C₁) (X₂ : CategoryTheory.GradedObject I₂ C₂) (X₃ : CategoryTheory.GradedObject I₃ C₃) [(((CategoryTheory.GradedObject.mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).HasMap ρ₂₃.p] [(((CategoryTheory.GradedObject.mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj (CategoryTheory.GradedObject.mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).HasMap ρ₂₃.q] [H : CategoryTheory.GradedObject.HasGoodTrifunctor₂₃Obj F G₂₃ ρ₂₃ X₁ X₂ X₃] [((((CategoryTheory.GradedObject.mapTrifunctor (CategoryTheory.bifunctorComp₂₃ F G₂₃) I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap r] (i₁ : I₁) (i₂ : I₂) (i₃ : I₃) (j : J) (h : r (i₁, i₂, i₃) = j) : CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.ιMapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ i₁ i₂ i₃ j h) ((CategoryTheory.GradedObject.mapBifunctorComp₂₃MapObjIso F G₂₃ ρ₂₃ X₁ X₂ X₃).inv j) = CategoryTheory.GradedObject.ιMapTrifunctorMapObj (CategoryTheory.bifunctorComp₂₃ F G₂₃) r X₁ X₂ X₃ i₁ i₂ i₃ j h
• CategoryTheory.GradedObject.ιMapBifunctorBifunctor₂₃MapObj_eq_assoc 📋 Mathlib.CategoryTheory.GradedObject.Trifunctor
  {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₂₃ : Type u_6} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Category.{v_3, u_3} C₃] [CategoryTheory.Category.{v_4, u_4} C₄] [CategoryTheory.Category.{v_6, u_6} C₂₃] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄)) (G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)) {I₁ : Type u_7} {I₂ : Type u_8} {I₃ : Type u_9} {J : Type u_10} {r : I₁ × I₂ × I₃ → J} (ρ₂₃ : CategoryTheory.GradedObject.BifunctorComp₂₃IndexData r) (X₁ : CategoryTheory.GradedObject I₁ C₁) (X₂ : CategoryTheory.GradedObject I₂ C₂) (X₃ : CategoryTheory.GradedObject I₃ C₃) [(((CategoryTheory.GradedObject.mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).HasMap ρ₂₃.p] [(((CategoryTheory.GradedObject.mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj (CategoryTheory.GradedObject.mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).HasMap ρ₂₃.q] (i₁ : I₁) (i₂ : I₂) (i₃ : I₃) (j : J) (h : r (i₁, i₂, i₃) = j) (i₂₃ : ρ₂₃.I₂₃) (h₂₃ : ρ₂₃.p (i₂, i₃) = i₂₃) {Z : C₄} (h✝ : CategoryTheory.GradedObject.mapBifunctorMapObj F ρ₂₃.q X₁ (CategoryTheory.GradedObject.mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃) j ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.ιMapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ i₁ i₂ i₃ j h) h✝ = CategoryTheory.CategoryStruct.comp ((F.obj (X₁ i₁)).map (CategoryTheory.GradedObject.ιMapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃ i₂ i₃ i₂₃ h₂₃)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.ιMapBifunctorMapObj F ρ₂₃.q X₁ (CategoryTheory.GradedObject.mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃) i₁ i₂₃ j ⋯) h✝)
• CategoryTheory.GradedObject.ι_mapBifunctorComp₁₂MapObjIso_hom 📋 Mathlib.CategoryTheory.GradedObject.Trifunctor
  {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₁₂ : Type u_5} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Category.{v_3, u_3} C₃] [CategoryTheory.Category.{v_4, u_4} C₄] [CategoryTheory.Category.{v_5, u_5} C₁₂] (F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)) (G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)) {I₁ : Type u_7} {I₂ : Type u_8} {I₃ : Type u_9} {J : Type u_10} {r : I₁ × I₂ × I₃ → J} (ρ₁₂ : CategoryTheory.GradedObject.BifunctorComp₁₂IndexData r) (X₁ : CategoryTheory.GradedObject I₁ C₁) (X₂ : CategoryTheory.GradedObject I₂ C₂) (X₃ : CategoryTheory.GradedObject I₃ C₃) [(((CategoryTheory.GradedObject.mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).HasMap ρ₁₂.p] [(((CategoryTheory.GradedObject.mapBifunctor G ρ₁₂.I₁₂ I₃).obj (CategoryTheory.GradedObject.mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj X₃).HasMap ρ₁₂.q] [H : CategoryTheory.GradedObject.HasGoodTrifunctor₁₂Obj F₁₂ G ρ₁₂ X₁ X₂ X₃] [((((CategoryTheory.GradedObject.mapTrifunctor (CategoryTheory.bifunctorComp₁₂ F₁₂ G) I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap r] (i₁ : I₁) (i₂ : I₂) (i₃ : I₃) (j : J) (h : r (i₁, i₂, i₃) = j) : CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.ιMapTrifunctorMapObj (CategoryTheory.bifunctorComp₁₂ F₁₂ G) r X₁ X₂ X₃ i₁ i₂ i₃ j h) ((CategoryTheory.GradedObject.mapBifunctorComp₁₂MapObjIso F₁₂ G ρ₁₂ X₁ X₂ X₃).hom j) = CategoryTheory.GradedObject.ιMapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ i₁ i₂ i₃ j h
• CategoryTheory.GradedObject.ιMapBifunctor₁₂BifunctorMapObj_eq_assoc 📋 Mathlib.CategoryTheory.GradedObject.Trifunctor
  {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₁₂ : Type u_5} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Category.{v_3, u_3} C₃] [CategoryTheory.Category.{v_4, u_4} C₄] [CategoryTheory.Category.{v_5, u_5} C₁₂] (F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)) (G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)) {I₁ : Type u_7} {I₂ : Type u_8} {I₃ : Type u_9} {J : Type u_10} {r : I₁ × I₂ × I₃ → J} (ρ₁₂ : CategoryTheory.GradedObject.BifunctorComp₁₂IndexData r) (X₁ : CategoryTheory.GradedObject I₁ C₁) (X₂ : CategoryTheory.GradedObject I₂ C₂) (X₃ : CategoryTheory.GradedObject I₃ C₃) [(((CategoryTheory.GradedObject.mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).HasMap ρ₁₂.p] [(((CategoryTheory.GradedObject.mapBifunctor G ρ₁₂.I₁₂ I₃).obj (CategoryTheory.GradedObject.mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj X₃).HasMap ρ₁₂.q] (i₁ : I₁) (i₂ : I₂) (i₃ : I₃) (j : J) (h : r (i₁, i₂, i₃) = j) (i₁₂ : ρ₁₂.I₁₂) (h₁₂ : ρ₁₂.p (i₁, i₂) = i₁₂) {Z : C₄} (h✝ : CategoryTheory.GradedObject.mapBifunctorMapObj G ρ₁₂.q (CategoryTheory.GradedObject.mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂) X₃ j ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.ιMapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ i₁ i₂ i₃ j h) h✝ = CategoryTheory.CategoryStruct.comp ((G.map (CategoryTheory.GradedObject.ιMapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂ i₁ i₂ i₁₂ h₁₂)).app (X₃ i₃)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.ιMapBifunctorMapObj G ρ₁₂.q (CategoryTheory.GradedObject.mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂) X₃ i₁₂ i₃ j ⋯) h✝)
• CategoryTheory.GradedObject.ι_mapBifunctorComp₂₃MapObjIso_hom 📋 Mathlib.CategoryTheory.GradedObject.Trifunctor
  {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₂₃ : Type u_6} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Category.{v_3, u_3} C₃] [CategoryTheory.Category.{v_4, u_4} C₄] [CategoryTheory.Category.{v_6, u_6} C₂₃] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄)) (G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)) {I₁ : Type u_7} {I₂ : Type u_8} {I₃ : Type u_9} {J : Type u_10} {r : I₁ × I₂ × I₃ → J} (ρ₂₃ : CategoryTheory.GradedObject.BifunctorComp₂₃IndexData r) (X₁ : CategoryTheory.GradedObject I₁ C₁) (X₂ : CategoryTheory.GradedObject I₂ C₂) (X₃ : CategoryTheory.GradedObject I₃ C₃) [(((CategoryTheory.GradedObject.mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).HasMap ρ₂₃.p] [(((CategoryTheory.GradedObject.mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj (CategoryTheory.GradedObject.mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).HasMap ρ₂₃.q] [H : CategoryTheory.GradedObject.HasGoodTrifunctor₂₃Obj F G₂₃ ρ₂₃ X₁ X₂ X₃] [((((CategoryTheory.GradedObject.mapTrifunctor (CategoryTheory.bifunctorComp₂₃ F G₂₃) I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap r] (i₁ : I₁) (i₂ : I₂) (i₃ : I₃) (j : J) (h : r (i₁, i₂, i₃) = j) : CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.ιMapTrifunctorMapObj (CategoryTheory.bifunctorComp₂₃ F G₂₃) r X₁ X₂ X₃ i₁ i₂ i₃ j h) ((CategoryTheory.GradedObject.mapBifunctorComp₂₃MapObjIso F G₂₃ ρ₂₃ X₁ X₂ X₃).hom j) = CategoryTheory.GradedObject.ιMapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ i₁ i₂ i₃ j h
• CategoryTheory.GradedObject.ι_mapBifunctorComp₁₂MapObjIso_inv_assoc 📋 Mathlib.CategoryTheory.GradedObject.Trifunctor
  {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₁₂ : Type u_5} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Category.{v_3, u_3} C₃] [CategoryTheory.Category.{v_4, u_4} C₄] [CategoryTheory.Category.{v_5, u_5} C₁₂] (F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)) (G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)) {I₁ : Type u_7} {I₂ : Type u_8} {I₃ : Type u_9} {J : Type u_10} {r : I₁ × I₂ × I₃ → J} (ρ₁₂ : CategoryTheory.GradedObject.BifunctorComp₁₂IndexData r) (X₁ : CategoryTheory.GradedObject I₁ C₁) (X₂ : CategoryTheory.GradedObject I₂ C₂) (X₃ : CategoryTheory.GradedObject I₃ C₃) [(((CategoryTheory.GradedObject.mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).HasMap ρ₁₂.p] [(((CategoryTheory.GradedObject.mapBifunctor G ρ₁₂.I₁₂ I₃).obj (CategoryTheory.GradedObject.mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj X₃).HasMap ρ₁₂.q] [H : CategoryTheory.GradedObject.HasGoodTrifunctor₁₂Obj F₁₂ G ρ₁₂ X₁ X₂ X₃] [((((CategoryTheory.GradedObject.mapTrifunctor (CategoryTheory.bifunctorComp₁₂ F₁₂ G) I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap r] (i₁ : I₁) (i₂ : I₂) (i₃ : I₃) (j : J) (h : r (i₁, i₂, i₃) = j) {Z : C₄} (h✝ : CategoryTheory.GradedObject.mapTrifunctorMapObj (CategoryTheory.bifunctorComp₁₂ F₁₂ G) r X₁ X₂ X₃ j ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.ιMapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ i₁ i₂ i₃ j h) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.GradedObject.mapBifunctorComp₁₂MapObjIso F₁₂ G ρ₁₂ X₁ X₂ X₃).inv j) h✝) = CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.ιMapTrifunctorMapObj (CategoryTheory.bifunctorComp₁₂ F₁₂ G) r X₁ X₂ X₃ i₁ i₂ i₃ j h) h✝
• CategoryTheory.GradedObject.ι_mapBifunctorComp₂₃MapObjIso_inv_assoc 📋 Mathlib.CategoryTheory.GradedObject.Trifunctor
  {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₂₃ : Type u_6} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Category.{v_3, u_3} C₃] [CategoryTheory.Category.{v_4, u_4} C₄] [CategoryTheory.Category.{v_6, u_6} C₂₃] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄)) (G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)) {I₁ : Type u_7} {I₂ : Type u_8} {I₃ : Type u_9} {J : Type u_10} {r : I₁ × I₂ × I₃ → J} (ρ₂₃ : CategoryTheory.GradedObject.BifunctorComp₂₃IndexData r) (X₁ : CategoryTheory.GradedObject I₁ C₁) (X₂ : CategoryTheory.GradedObject I₂ C₂) (X₃ : CategoryTheory.GradedObject I₃ C₃) [(((CategoryTheory.GradedObject.mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).HasMap ρ₂₃.p] [(((CategoryTheory.GradedObject.mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj (CategoryTheory.GradedObject.mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).HasMap ρ₂₃.q] [H : CategoryTheory.GradedObject.HasGoodTrifunctor₂₃Obj F G₂₃ ρ₂₃ X₁ X₂ X₃] [((((CategoryTheory.GradedObject.mapTrifunctor (CategoryTheory.bifunctorComp₂₃ F G₂₃) I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap r] (i₁ : I₁) (i₂ : I₂) (i₃ : I₃) (j : J) (h : r (i₁, i₂, i₃) = j) {Z : C₄} (h✝ : CategoryTheory.GradedObject.mapTrifunctorMapObj (CategoryTheory.bifunctorComp₂₃ F G₂₃) r X₁ X₂ X₃ j ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.ιMapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ i₁ i₂ i₃ j h) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.GradedObject.mapBifunctorComp₂₃MapObjIso F G₂₃ ρ₂₃ X₁ X₂ X₃).inv j) h✝) = CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.ιMapTrifunctorMapObj (CategoryTheory.bifunctorComp₂₃ F G₂₃) r X₁ X₂ X₃ i₁ i₂ i₃ j h) h✝
• CategoryTheory.GradedObject.ι_mapBifunctorComp₁₂MapObjIso_hom_assoc 📋 Mathlib.CategoryTheory.GradedObject.Trifunctor
  {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₁₂ : Type u_5} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Category.{v_3, u_3} C₃] [CategoryTheory.Category.{v_4, u_4} C₄] [CategoryTheory.Category.{v_5, u_5} C₁₂] (F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)) (G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)) {I₁ : Type u_7} {I₂ : Type u_8} {I₃ : Type u_9} {J : Type u_10} {r : I₁ × I₂ × I₃ → J} (ρ₁₂ : CategoryTheory.GradedObject.BifunctorComp₁₂IndexData r) (X₁ : CategoryTheory.GradedObject I₁ C₁) (X₂ : CategoryTheory.GradedObject I₂ C₂) (X₃ : CategoryTheory.GradedObject I₃ C₃) [(((CategoryTheory.GradedObject.mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).HasMap ρ₁₂.p] [(((CategoryTheory.GradedObject.mapBifunctor G ρ₁₂.I₁₂ I₃).obj (CategoryTheory.GradedObject.mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj X₃).HasMap ρ₁₂.q] [H : CategoryTheory.GradedObject.HasGoodTrifunctor₁₂Obj F₁₂ G ρ₁₂ X₁ X₂ X₃] [((((CategoryTheory.GradedObject.mapTrifunctor (CategoryTheory.bifunctorComp₁₂ F₁₂ G) I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap r] (i₁ : I₁) (i₂ : I₂) (i₃ : I₃) (j : J) (h : r (i₁, i₂, i₃) = j) {Z : C₄} (h✝ : CategoryTheory.GradedObject.mapBifunctorMapObj G ρ₁₂.q (CategoryTheory.GradedObject.mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂) X₃ j ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.ιMapTrifunctorMapObj (CategoryTheory.bifunctorComp₁₂ F₁₂ G) r X₁ X₂ X₃ i₁ i₂ i₃ j h) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.GradedObject.mapBifunctorComp₁₂MapObjIso F₁₂ G ρ₁₂ X₁ X₂ X₃).hom j) h✝) = CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.ιMapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ i₁ i₂ i₃ j h) h✝
• CategoryTheory.GradedObject.ι_mapBifunctorComp₂₃MapObjIso_hom_assoc 📋 Mathlib.CategoryTheory.GradedObject.Trifunctor
  {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₂₃ : Type u_6} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Category.{v_3, u_3} C₃] [CategoryTheory.Category.{v_4, u_4} C₄] [CategoryTheory.Category.{v_6, u_6} C₂₃] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄)) (G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)) {I₁ : Type u_7} {I₂ : Type u_8} {I₃ : Type u_9} {J : Type u_10} {r : I₁ × I₂ × I₃ → J} (ρ₂₃ : CategoryTheory.GradedObject.BifunctorComp₂₃IndexData r) (X₁ : CategoryTheory.GradedObject I₁ C₁) (X₂ : CategoryTheory.GradedObject I₂ C₂) (X₃ : CategoryTheory.GradedObject I₃ C₃) [(((CategoryTheory.GradedObject.mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).HasMap ρ₂₃.p] [(((CategoryTheory.GradedObject.mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj (CategoryTheory.GradedObject.mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).HasMap ρ₂₃.q] [H : CategoryTheory.GradedObject.HasGoodTrifunctor₂₃Obj F G₂₃ ρ₂₃ X₁ X₂ X₃] [((((CategoryTheory.GradedObject.mapTrifunctor (CategoryTheory.bifunctorComp₂₃ F G₂₃) I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap r] (i₁ : I₁) (i₂ : I₂) (i₃ : I₃) (j : J) (h : r (i₁, i₂, i₃) = j) {Z : C₄} (h✝ : CategoryTheory.GradedObject.mapBifunctorMapObj F ρ₂₃.q X₁ (CategoryTheory.GradedObject.mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃) j ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.ιMapTrifunctorMapObj (CategoryTheory.bifunctorComp₂₃ F G₂₃) r X₁ X₂ X₃ i₁ i₂ i₃ j h) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.GradedObject.mapBifunctorComp₂₃MapObjIso F G₂₃ ρ₂₃ X₁ X₂ X₃).hom j) h✝) = CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.ιMapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ i₁ i₂ i₃ j h) h✝
• CategoryTheory.Functor.mapBifunctorHomologicalComplex_obj_obj_toGradedObject 📋 Mathlib.Algebra.Homology.Bifunctor
  {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Category.{v_3, u_3} D] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Limits.HasZeroMorphisms D] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) {I₁ : Type u_4} {I₂ : Type u_5} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} [F.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) : (((F.mapBifunctorHomologicalComplex c₁ c₂).obj K₁).obj K₂).toGradedObject = ((CategoryTheory.GradedObject.mapBifunctor F I₁ I₂).obj K₁.X).obj K₂.X
• CategoryTheory.Functor.mapBifunctorHomologicalComplex_map_app_f_f 📋 Mathlib.Algebra.Homology.Bifunctor
  {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Category.{v_3, u_3} D] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Limits.HasZeroMorphisms D] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) {I₁ : Type u_4} {I₂ : Type u_5} (c₁ : ComplexShape I₁) (c₂ : ComplexShape I₂) [F.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] {K₁ K₁' : HomologicalComplex C₁ c₁} (f : K₁ ⟶ K₁') (K₂ : HomologicalComplex C₂ c₂) (i₁ : I₁) (i₂ : I₂) : ((((F.mapBifunctorHomologicalComplex c₁ c₂).map f).app K₂).f i₁).f i₂ = (F.map (f.f i₁)).app (K₂.X i₂)
• CategoryTheory.Functor.mapBifunctorHomologicalComplexObj_obj_d_f 📋 Mathlib.Algebra.Homology.Bifunctor
  {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Category.{v_3, u_3} D] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Limits.HasZeroMorphisms D] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) {I₁ : Type u_4} {I₂ : Type u_5} {c₁ : ComplexShape I₁} (c₂ : ComplexShape I₂) [F.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (i₁ i₁' : I₁) (i₂ : I₂) : (((F.mapBifunctorHomologicalComplexObj c₂ K₁).obj K₂).d i₁ i₁').f i₂ = (F.map (K₁.d i₁ i₁')).app (K₂.X i₂)
• CategoryTheory.Functor.mapBifunctorHomologicalComplex_obj_obj_d_f 📋 Mathlib.Algebra.Homology.Bifunctor
  {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Category.{v_3, u_3} D] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Limits.HasZeroMorphisms D] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) {I₁ : Type u_4} {I₂ : Type u_5} (c₁ : ComplexShape I₁) (c₂ : ComplexShape I₂) [F.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (i₁ i₁' : I₁) (i₂ : I₂) : ((((F.mapBifunctorHomologicalComplex c₁ c₂).obj K₁).obj K₂).d i₁ i₁').f i₂ = (F.map (K₁.d i₁ i₁')).app (K₂.X i₂)
• CategoryTheory.Functor.mapBifunctorHomologicalComplexObj_map_f_f 📋 Mathlib.Algebra.Homology.Bifunctor
  {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Category.{v_3, u_3} D] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Limits.HasZeroMorphisms D] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) {I₁ : Type u_4} {I₂ : Type u_5} {c₁ : ComplexShape I₁} (c₂ : ComplexShape I₂) [F.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] (K₁ : HomologicalComplex C₁ c₁) {K₂ K₂' : HomologicalComplex C₂ c₂} {φ : K₂ ⟶ K₂'} (i₁ : I₁) (i₂ : I₂) : (((F.mapBifunctorHomologicalComplexObj c₂ K₁).map φ).f i₁).f i₂ = (F.obj (K₁.X i₁)).map (φ.f i₂)
• CategoryTheory.Functor.mapBifunctorHomologicalComplex_obj_map_f_f 📋 Mathlib.Algebra.Homology.Bifunctor
  {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Category.{v_3, u_3} D] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Limits.HasZeroMorphisms D] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) {I₁ : Type u_4} {I₂ : Type u_5} (c₁ : ComplexShape I₁) (c₂ : ComplexShape I₂) [F.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] (K₁ : HomologicalComplex C₁ c₁) {K₂ K₂' : HomologicalComplex C₂ c₂} {φ : K₂ ⟶ K₂'} (i₁ : I₁) (i₂ : I₂) : ((((F.mapBifunctorHomologicalComplex c₁ c₂).obj K₁).map φ).f i₁).f i₂ = (F.obj (K₁.X i₁)).map (φ.f i₂)
• CategoryTheory.GradedObject.mapBifunctorAssociator 📋 Mathlib.CategoryTheory.GradedObject.Associator
  {C₁ : Type u_1} {C₂ : Type u_2} {C₁₂ : Type u_3} {C₂₃ : Type u_4} {C₃ : Type u_5} {C₄ : Type u_6} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Category.{v_3, u_5} C₃] [CategoryTheory.Category.{v_4, u_6} C₄] [CategoryTheory.Category.{v_5, u_3} C₁₂] [CategoryTheory.Category.{v_6, u_4} C₂₃] {F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)} {G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)} {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄)} {G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)} (associator : CategoryTheory.bifunctorComp₁₂ F₁₂ G ≅ CategoryTheory.bifunctorComp₂₃ F G₂₃) {I₁ : Type u_7} {I₂ : Type u_8} {I₃ : Type u_9} {J : Type u_10} {r : I₁ × I₂ × I₃ → J} (ρ₁₂ : CategoryTheory.GradedObject.BifunctorComp₁₂IndexData r) (ρ₂₃ : CategoryTheory.GradedObject.BifunctorComp₂₃IndexData r) (X₁ : CategoryTheory.GradedObject I₁ C₁) (X₂ : CategoryTheory.GradedObject I₂ C₂) (X₃ : CategoryTheory.GradedObject I₃ C₃) [(((CategoryTheory.GradedObject.mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).HasMap ρ₁₂.p] [(((CategoryTheory.GradedObject.mapBifunctor G ρ₁₂.I₁₂ I₃).obj (CategoryTheory.GradedObject.mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj X₃).HasMap ρ₁₂.q] [(((CategoryTheory.GradedObject.mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).HasMap ρ₂₃.p] [(((CategoryTheory.GradedObject.mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj (CategoryTheory.GradedObject.mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).HasMap ρ₂₃.q] [H₁₂ : CategoryTheory.GradedObject.HasGoodTrifunctor₁₂Obj F₁₂ G ρ₁₂ X₁ X₂ X₃] [H₂₃ : CategoryTheory.GradedObject.HasGoodTrifunctor₂₃Obj F G₂₃ ρ₂₃ X₁ X₂ X₃] : CategoryTheory.GradedObject.mapBifunctorMapObj G ρ₁₂.q (CategoryTheory.GradedObject.mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂) X₃ ≅ CategoryTheory.GradedObject.mapBifunctorMapObj F ρ₂₃.q X₁ (CategoryTheory.GradedObject.mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)
• CategoryTheory.GradedObject.ι_mapBifunctorAssociator_hom 📋 Mathlib.CategoryTheory.GradedObject.Associator
  {C₁ : Type u_1} {C₂ : Type u_2} {C₁₂ : Type u_3} {C₂₃ : Type u_4} {C₃ : Type u_5} {C₄ : Type u_6} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Category.{v_3, u_5} C₃] [CategoryTheory.Category.{v_4, u_6} C₄] [CategoryTheory.Category.{v_5, u_3} C₁₂] [CategoryTheory.Category.{v_6, u_4} C₂₃] {F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)} {G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)} {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄)} {G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)} (associator : CategoryTheory.bifunctorComp₁₂ F₁₂ G ≅ CategoryTheory.bifunctorComp₂₃ F G₂₃) {I₁ : Type u_7} {I₂ : Type u_8} {I₃ : Type u_9} {J : Type u_10} {r : I₁ × I₂ × I₃ → J} (ρ₁₂ : CategoryTheory.GradedObject.BifunctorComp₁₂IndexData r) (ρ₂₃ : CategoryTheory.GradedObject.BifunctorComp₂₃IndexData r) (X₁ : CategoryTheory.GradedObject I₁ C₁) (X₂ : CategoryTheory.GradedObject I₂ C₂) (X₃ : CategoryTheory.GradedObject I₃ C₃) [(((CategoryTheory.GradedObject.mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).HasMap ρ₁₂.p] [(((CategoryTheory.GradedObject.mapBifunctor G ρ₁₂.I₁₂ I₃).obj (CategoryTheory.GradedObject.mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj X₃).HasMap ρ₁₂.q] [(((CategoryTheory.GradedObject.mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).HasMap ρ₂₃.p] [(((CategoryTheory.GradedObject.mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj (CategoryTheory.GradedObject.mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).HasMap ρ₂₃.q] [H₁₂ : CategoryTheory.GradedObject.HasGoodTrifunctor₁₂Obj F₁₂ G ρ₁₂ X₁ X₂ X₃] [H₂₃ : CategoryTheory.GradedObject.HasGoodTrifunctor₂₃Obj F G₂₃ ρ₂₃ X₁ X₂ X₃] (i₁ : I₁) (i₂ : I₂) (i₃ : I₃) (j : J) (h : r (i₁, i₂, i₃) = j) : CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.ιMapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ i₁ i₂ i₃ j h) ((CategoryTheory.GradedObject.mapBifunctorAssociator associator ρ₁₂ ρ₂₃ X₁ X₂ X₃).hom j) = CategoryTheory.CategoryStruct.comp (((associator.hom.app (X₁ i₁)).app (X₂ i₂)).app (X₃ i₃)) (CategoryTheory.GradedObject.ιMapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ i₁ i₂ i₃ j h)
• CategoryTheory.GradedObject.ι_mapBifunctorAssociator_inv 📋 Mathlib.CategoryTheory.GradedObject.Associator
  {C₁ : Type u_1} {C₂ : Type u_2} {C₁₂ : Type u_3} {C₂₃ : Type u_4} {C₃ : Type u_5} {C₄ : Type u_6} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Category.{v_3, u_5} C₃] [CategoryTheory.Category.{v_4, u_6} C₄] [CategoryTheory.Category.{v_5, u_3} C₁₂] [CategoryTheory.Category.{v_6, u_4} C₂₃] {F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)} {G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)} {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄)} {G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)} (associator : CategoryTheory.bifunctorComp₁₂ F₁₂ G ≅ CategoryTheory.bifunctorComp₂₃ F G₂₃) {I₁ : Type u_7} {I₂ : Type u_8} {I₃ : Type u_9} {J : Type u_10} {r : I₁ × I₂ × I₃ → J} (ρ₁₂ : CategoryTheory.GradedObject.BifunctorComp₁₂IndexData r) (ρ₂₃ : CategoryTheory.GradedObject.BifunctorComp₂₃IndexData r) (X₁ : CategoryTheory.GradedObject I₁ C₁) (X₂ : CategoryTheory.GradedObject I₂ C₂) (X₃ : CategoryTheory.GradedObject I₃ C₃) [(((CategoryTheory.GradedObject.mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).HasMap ρ₁₂.p] [(((CategoryTheory.GradedObject.mapBifunctor G ρ₁₂.I₁₂ I₃).obj (CategoryTheory.GradedObject.mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj X₃).HasMap ρ₁₂.q] [(((CategoryTheory.GradedObject.mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).HasMap ρ₂₃.p] [(((CategoryTheory.GradedObject.mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj (CategoryTheory.GradedObject.mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).HasMap ρ₂₃.q] [H₁₂ : CategoryTheory.GradedObject.HasGoodTrifunctor₁₂Obj F₁₂ G ρ₁₂ X₁ X₂ X₃] [H₂₃ : CategoryTheory.GradedObject.HasGoodTrifunctor₂₃Obj F G₂₃ ρ₂₃ X₁ X₂ X₃] (i₁ : I₁) (i₂ : I₂) (i₃ : I₃) (j : J) (h : r (i₁, i₂, i₃) = j) : CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.ιMapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ i₁ i₂ i₃ j h) ((CategoryTheory.GradedObject.mapBifunctorAssociator associator ρ₁₂ ρ₂₃ X₁ X₂ X₃).inv j) = CategoryTheory.CategoryStruct.comp (((associator.inv.app (X₁ i₁)).app (X₂ i₂)).app (X₃ i₃)) (CategoryTheory.GradedObject.ιMapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ i₁ i₂ i₃ j h)
• CategoryTheory.GradedObject.ι_mapBifunctorAssociator_hom_assoc 📋 Mathlib.CategoryTheory.GradedObject.Associator
  {C₁ : Type u_1} {C₂ : Type u_2} {C₁₂ : Type u_3} {C₂₃ : Type u_4} {C₃ : Type u_5} {C₄ : Type u_6} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Category.{v_3, u_5} C₃] [CategoryTheory.Category.{v_4, u_6} C₄] [CategoryTheory.Category.{v_5, u_3} C₁₂] [CategoryTheory.Category.{v_6, u_4} C₂₃] {F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)} {G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)} {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄)} {G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)} (associator : CategoryTheory.bifunctorComp₁₂ F₁₂ G ≅ CategoryTheory.bifunctorComp₂₃ F G₂₃) {I₁ : Type u_7} {I₂ : Type u_8} {I₃ : Type u_9} {J : Type u_10} {r : I₁ × I₂ × I₃ → J} (ρ₁₂ : CategoryTheory.GradedObject.BifunctorComp₁₂IndexData r) (ρ₂₃ : CategoryTheory.GradedObject.BifunctorComp₂₃IndexData r) (X₁ : CategoryTheory.GradedObject I₁ C₁) (X₂ : CategoryTheory.GradedObject I₂ C₂) (X₃ : CategoryTheory.GradedObject I₃ C₃) [(((CategoryTheory.GradedObject.mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).HasMap ρ₁₂.p] [(((CategoryTheory.GradedObject.mapBifunctor G ρ₁₂.I₁₂ I₃).obj (CategoryTheory.GradedObject.mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj X₃).HasMap ρ₁₂.q] [(((CategoryTheory.GradedObject.mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).HasMap ρ₂₃.p] [(((CategoryTheory.GradedObject.mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj (CategoryTheory.GradedObject.mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).HasMap ρ₂₃.q] [H₁₂ : CategoryTheory.GradedObject.HasGoodTrifunctor₁₂Obj F₁₂ G ρ₁₂ X₁ X₂ X₃] [H₂₃ : CategoryTheory.GradedObject.HasGoodTrifunctor₂₃Obj F G₂₃ ρ₂₃ X₁ X₂ X₃] (i₁ : I₁) (i₂ : I₂) (i₃ : I₃) (j : J) (h : r (i₁, i₂, i₃) = j) {Z : C₄} (h✝ : CategoryTheory.GradedObject.mapBifunctorMapObj F ρ₂₃.q X₁ (CategoryTheory.GradedObject.mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃) j ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.ιMapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ i₁ i₂ i₃ j h) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.GradedObject.mapBifunctorAssociator associator ρ₁₂ ρ₂₃ X₁ X₂ X₃).hom j) h✝) = CategoryTheory.CategoryStruct.comp (((associator.hom.app (X₁ i₁)).app (X₂ i₂)).app (X₃ i₃)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.ιMapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ i₁ i₂ i₃ j h) h✝)
• CategoryTheory.GradedObject.ι_mapBifunctorAssociator_inv_assoc 📋 Mathlib.CategoryTheory.GradedObject.Associator
  {C₁ : Type u_1} {C₂ : Type u_2} {C₁₂ : Type u_3} {C₂₃ : Type u_4} {C₃ : Type u_5} {C₄ : Type u_6} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Category.{v_3, u_5} C₃] [CategoryTheory.Category.{v_4, u_6} C₄] [CategoryTheory.Category.{v_5, u_3} C₁₂] [CategoryTheory.Category.{v_6, u_4} C₂₃] {F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)} {G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)} {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄)} {G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)} (associator : CategoryTheory.bifunctorComp₁₂ F₁₂ G ≅ CategoryTheory.bifunctorComp₂₃ F G₂₃) {I₁ : Type u_7} {I₂ : Type u_8} {I₃ : Type u_9} {J : Type u_10} {r : I₁ × I₂ × I₃ → J} (ρ₁₂ : CategoryTheory.GradedObject.BifunctorComp₁₂IndexData r) (ρ₂₃ : CategoryTheory.GradedObject.BifunctorComp₂₃IndexData r) (X₁ : CategoryTheory.GradedObject I₁ C₁) (X₂ : CategoryTheory.GradedObject I₂ C₂) (X₃ : CategoryTheory.GradedObject I₃ C₃) [(((CategoryTheory.GradedObject.mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).HasMap ρ₁₂.p] [(((CategoryTheory.GradedObject.mapBifunctor G ρ₁₂.I₁₂ I₃).obj (CategoryTheory.GradedObject.mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj X₃).HasMap ρ₁₂.q] [(((CategoryTheory.GradedObject.mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).HasMap ρ₂₃.p] [(((CategoryTheory.GradedObject.mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj (CategoryTheory.GradedObject.mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).HasMap ρ₂₃.q] [H₁₂ : CategoryTheory.GradedObject.HasGoodTrifunctor₁₂Obj F₁₂ G ρ₁₂ X₁ X₂ X₃] [H₂₃ : CategoryTheory.GradedObject.HasGoodTrifunctor₂₃Obj F G₂₃ ρ₂₃ X₁ X₂ X₃] (i₁ : I₁) (i₂ : I₂) (i₃ : I₃) (j : J) (h : r (i₁, i₂, i₃) = j) {Z : C₄} (h✝ : CategoryTheory.GradedObject.mapBifunctorMapObj G ρ₁₂.q (CategoryTheory.GradedObject.mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂) X₃ j ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.ιMapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ i₁ i₂ i₃ j h) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.GradedObject.mapBifunctorAssociator associator ρ₁₂ ρ₂₃ X₁ X₂ X₃).inv j) h✝) = CategoryTheory.CategoryStruct.comp (((associator.inv.app (X₁ i₁)).app (X₂ i₂)).app (X₃ i₃)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.ιMapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ i₁ i₂ i₃ j h) h✝)
• HomologicalComplex.instHasMapProdObjGradedObjectFunctorMapBifunctorXπ 📋 Mathlib.Algebra.Homology.BifunctorAssociator
  {C₁ : Type u_1} {C₂ : Type u_2} {C₁₂ : Type u_3} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Category.{v_5, u_3} C₁₂] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Preadditive C₁₂] {F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)} [F₁₂.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F₁₂.obj X₁).PreservesZeroMorphisms] {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₁₂ : Type u_10} {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂} (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (c₁₂ : ComplexShape ι₁₂) [TotalComplexShape c₁ c₂ c₁₂] [K₁.HasMapBifunctor K₂ F₁₂ c₁₂] : (((CategoryTheory.GradedObject.mapBifunctor F₁₂ ι₁ ι₂).obj K₁.X).obj K₂.X).HasMap (c₁.π c₂ c₁₂)
• HomologicalComplex.instHasMapProdObjGradedObjectFunctorMapBifunctorMapBifunctorMapObjπX 📋 Mathlib.Algebra.Homology.BifunctorAssociator
  {C₁ : Type u_1} {C₂ : Type u_2} {C₁₂ : Type u_3} {C₃ : Type u_5} {C₄ : Type u_6} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Category.{v_3, u_5} C₃] [CategoryTheory.Category.{v_4, u_6} C₄] [CategoryTheory.Category.{v_5, u_3} C₁₂] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Limits.HasZeroMorphisms C₃] [CategoryTheory.Preadditive C₁₂] [CategoryTheory.Preadditive C₄] {F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)} {G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)} [F₁₂.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F₁₂.obj X₁).PreservesZeroMorphisms] [G.Additive] [∀ (X₁₂ : C₁₂), (G.obj X₁₂).PreservesZeroMorphisms] {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9} {ι₁₂ : Type u_10} {ι₄ : Type u_12} {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂} {c₃ : ComplexShape ι₃} (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (K₃ : HomologicalComplex C₃ c₃) (c₁₂ : ComplexShape ι₁₂) (c₄ : ComplexShape ι₄) [TotalComplexShape c₁ c₂ c₁₂] [TotalComplexShape c₁₂ c₃ c₄] [K₁.HasMapBifunctor K₂ F₁₂ c₁₂] [DecidableEq ι₁₂] [(K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄] : (((CategoryTheory.GradedObject.mapBifunctor G ι₁₂ ι₃).obj (CategoryTheory.GradedObject.mapBifunctorMapObj F₁₂ (c₁.π c₂ c₁₂) K₁.X K₂.X)).obj K₃.X).HasMap (c₁₂.π c₃ c₄)
• HomologicalComplex.instHasMapProdObjGradedObjectFunctorMapBifunctorXMapBifunctorMapObjπ 📋 Mathlib.Algebra.Homology.BifunctorAssociator
  {C₁ : Type u_1} {C₂ : Type u_2} {C₂₃ : Type u_4} {C₃ : Type u_5} {C₄ : Type u_6} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Category.{v_3, u_5} C₃] [CategoryTheory.Category.{v_4, u_6} C₄] [CategoryTheory.Category.{v_6, u_4} C₂₃] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Limits.HasZeroMorphisms C₃] [CategoryTheory.Preadditive C₂₃] [CategoryTheory.Preadditive C₄] {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄)} {G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)} [G₂₃.PreservesZeroMorphisms] [∀ (X₂ : C₂), (G₂₃.obj X₂).PreservesZeroMorphisms] [F.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F.obj X₁).Additive] {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9} {ι₂₃ : Type u_11} {ι₄ : Type u_12} {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂} {c₃ : ComplexShape ι₃} (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (K₃ : HomologicalComplex C₃ c₃) (c₂₃ : ComplexShape ι₂₃) (c₄ : ComplexShape ι₄) [TotalComplexShape c₂ c₃ c₂₃] [TotalComplexShape c₁ c₂₃ c₄] [K₂.HasMapBifunctor K₃ G₂₃ c₂₃] [DecidableEq ι₂₃] [K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄] : (((CategoryTheory.GradedObject.mapBifunctor F ι₁ ι₂₃).obj K₁.X).obj (CategoryTheory.GradedObject.mapBifunctorMapObj G₂₃ (c₂.π c₃ c₂₃) K₂.X K₃.X)).HasMap (c₁.π c₂₃ c₄)
• CategoryTheory.GradedObject.mapBifunctorObjObjSingle₀IsInitial 📋 Mathlib.CategoryTheory.GradedObject.Unitor
  {C : Type u_1} {D : Type u_2} {I : Type u_3} {J : Type u_4} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] [Zero I] [DecidableEq I] [CategoryTheory.Limits.HasInitial C] (F : CategoryTheory.Functor D (CategoryTheory.Functor C D)) (Y : C) [∀ (X : D), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) (F.obj X)] (X : CategoryTheory.GradedObject J D) (a : J × I) (ha : a.2 ≠ 0) : CategoryTheory.Limits.IsInitial (((CategoryTheory.GradedObject.mapBifunctor F J I).obj X).obj ((CategoryTheory.GradedObject.single₀ I).obj Y) a)
• CategoryTheory.GradedObject.mapBifunctorObjSingle₀ObjIso 📋 Mathlib.CategoryTheory.GradedObject.Unitor
  {C : Type u_1} {D : Type u_2} {I : Type u_3} {J : Type u_4} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] [Zero I] [DecidableEq I] [CategoryTheory.Limits.HasInitial C] (F : CategoryTheory.Functor C (CategoryTheory.Functor D D)) (X : C) (e : F.obj X ≅ CategoryTheory.Functor.id D) (Y : CategoryTheory.GradedObject J D) (a : I × J) (ha : a.1 = 0) : ((CategoryTheory.GradedObject.mapBifunctor F I J).obj ((CategoryTheory.GradedObject.single₀ I).obj X)).obj Y a ≅ Y a.2
• CategoryTheory.GradedObject.mapBifunctorObjSingle₀ObjIsInitial 📋 Mathlib.CategoryTheory.GradedObject.Unitor
  {C : Type u_1} {D : Type u_2} {I : Type u_3} {J : Type u_4} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] [Zero I] [DecidableEq I] [CategoryTheory.Limits.HasInitial C] (F : CategoryTheory.Functor C (CategoryTheory.Functor D D)) (X : C) [∀ (Y : D), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) (F.flip.obj Y)] (Y : CategoryTheory.GradedObject J D) (a : I × J) (ha : a.1 ≠ 0) : CategoryTheory.Limits.IsInitial (((CategoryTheory.GradedObject.mapBifunctor F I J).obj ((CategoryTheory.GradedObject.single₀ I).obj X)).obj Y a)
• CategoryTheory.GradedObject.mapBifunctorObjObjSingle₀Iso 📋 Mathlib.CategoryTheory.GradedObject.Unitor
  {C : Type u_1} {D : Type u_2} {I : Type u_3} {J : Type u_4} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] [Zero I] [DecidableEq I] [CategoryTheory.Limits.HasInitial C] (F : CategoryTheory.Functor D (CategoryTheory.Functor C D)) (Y : C) (e : F.flip.obj Y ≅ CategoryTheory.Functor.id D) (X : CategoryTheory.GradedObject J D) (a : J × I) (ha : a.2 = 0) : ((CategoryTheory.GradedObject.mapBifunctor F J I).obj X).obj ((CategoryTheory.GradedObject.single₀ I).obj Y) a ≅ X a.1
• CategoryTheory.GradedObject.mapBifunctorLeftUnitor_hasMap 📋 Mathlib.CategoryTheory.GradedObject.Unitor
  {C : Type u_1} {D : Type u_2} {I : Type u_3} {J : Type u_4} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] [Zero I] [DecidableEq I] [CategoryTheory.Limits.HasInitial C] (F : CategoryTheory.Functor C (CategoryTheory.Functor D D)) (X : C) (e : F.obj X ≅ CategoryTheory.Functor.id D) [∀ (Y : D), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) (F.flip.obj Y)] (p : I × J → J) (hp : ∀ (j : J), p (0, j) = j) (Y : CategoryTheory.GradedObject J D) : (((CategoryTheory.GradedObject.mapBifunctor F I J).obj ((CategoryTheory.GradedObject.single₀ I).obj X)).obj Y).HasMap p
• CategoryTheory.GradedObject.mapBifunctorRightUnitor_hasMap 📋 Mathlib.CategoryTheory.GradedObject.Unitor
  {C : Type u_1} {D : Type u_2} {I : Type u_3} {J : Type u_4} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] [Zero I] [DecidableEq I] [CategoryTheory.Limits.HasInitial C] (F : CategoryTheory.Functor D (CategoryTheory.Functor C D)) (Y : C) (e : F.flip.obj Y ≅ CategoryTheory.Functor.id D) [∀ (X : D), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) (F.obj X)] (p : J × I → J) (hp : ∀ (j : J), p (j, 0) = j) (X : CategoryTheory.GradedObject J D) : (((CategoryTheory.GradedObject.mapBifunctor F J I).obj X).obj ((CategoryTheory.GradedObject.single₀ I).obj Y)).HasMap p
• CategoryTheory.GradedObject.mapBifunctorLeftUnitorCofan 📋 Mathlib.CategoryTheory.GradedObject.Unitor
  {C : Type u_1} {D : Type u_2} {I : Type u_3} {J : Type u_4} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] [Zero I] [DecidableEq I] [CategoryTheory.Limits.HasInitial C] (F : CategoryTheory.Functor C (CategoryTheory.Functor D D)) (X : C) (e : F.obj X ≅ CategoryTheory.Functor.id D) [∀ (Y : D), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) (F.flip.obj Y)] (p : I × J → J) (hp : ∀ (j : J), p (0, j) = j) (Y : CategoryTheory.GradedObject J D) (j : J) : (((CategoryTheory.GradedObject.mapBifunctor F I J).obj ((CategoryTheory.GradedObject.single₀ I).obj X)).obj Y).CofanMapObjFun p j
• CategoryTheory.GradedObject.mapBifunctorRightUnitorCofan 📋 Mathlib.CategoryTheory.GradedObject.Unitor
  {C : Type u_1} {D : Type u_2} {I : Type u_3} {J : Type u_4} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] [Zero I] [DecidableEq I] [CategoryTheory.Limits.HasInitial C] (F : CategoryTheory.Functor D (CategoryTheory.Functor C D)) (Y : C) (e : F.flip.obj Y ≅ CategoryTheory.Functor.id D) [∀ (X : D), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) (F.obj X)] (p : J × I → J) (hp : ∀ (j : J), p (j, 0) = j) (X : CategoryTheory.GradedObject J D) (j : J) : (((CategoryTheory.GradedObject.mapBifunctor F J I).obj X).obj ((CategoryTheory.GradedObject.single₀ I).obj Y)).CofanMapObjFun p j
• CategoryTheory.GradedObject.mapBifunctorLeftUnitor 📋 Mathlib.CategoryTheory.GradedObject.Unitor
  {C : Type u_1} {D : Type u_2} {I : Type u_3} {J : Type u_4} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] [Zero I] [DecidableEq I] [CategoryTheory.Limits.HasInitial C] (F : CategoryTheory.Functor C (CategoryTheory.Functor D D)) (X : C) (e : F.obj X ≅ CategoryTheory.Functor.id D) [∀ (Y : D), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) (F.flip.obj Y)] (p : I × J → J) (hp : ∀ (j : J), p (0, j) = j) (Y : CategoryTheory.GradedObject J D) [(((CategoryTheory.GradedObject.mapBifunctor F I J).obj ((CategoryTheory.GradedObject.single₀ I).obj X)).obj Y).HasMap p] : CategoryTheory.GradedObject.mapBifunctorMapObj F p ((CategoryTheory.GradedObject.single₀ I).obj X) Y ≅ Y
• CategoryTheory.GradedObject.mapBifunctorRightUnitor 📋 Mathlib.CategoryTheory.GradedObject.Unitor
  {C : Type u_1} {D : Type u_2} {I : Type u_3} {J : Type u_4} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] [Zero I] [DecidableEq I] [CategoryTheory.Limits.HasInitial C] (F : CategoryTheory.Functor D (CategoryTheory.Functor C D)) (Y : C) (e : F.flip.obj Y ≅ CategoryTheory.Functor.id D) [∀ (X : D), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) (F.obj X)] (p : J × I → J) (hp : ∀ (j : J), p (j, 0) = j) (X : CategoryTheory.GradedObject J D) [(((CategoryTheory.GradedObject.mapBifunctor F J I).obj X).obj ((CategoryTheory.GradedObject.single₀ I).obj Y)).HasMap p] : CategoryTheory.GradedObject.mapBifunctorMapObj F p X ((CategoryTheory.GradedObject.single₀ I).obj Y) ≅ X
• CategoryTheory.GradedObject.mapBifunctorLeftUnitorCofanIsColimit 📋 Mathlib.CategoryTheory.GradedObject.Unitor
  {C : Type u_1} {D : Type u_2} {I : Type u_3} {J : Type u_4} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] [Zero I] [DecidableEq I] [CategoryTheory.Limits.HasInitial C] (F : CategoryTheory.Functor C (CategoryTheory.Functor D D)) (X : C) (e : F.obj X ≅ CategoryTheory.Functor.id D) [∀ (Y : D), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) (F.flip.obj Y)] (p : I × J → J) (hp : ∀ (j : J), p (0, j) = j) (Y : CategoryTheory.GradedObject J D) (j : J) : CategoryTheory.Limits.IsColimit (CategoryTheory.GradedObject.mapBifunctorLeftUnitorCofan F X e p hp Y j)
• CategoryTheory.GradedObject.mapBifunctorRightUnitorCofanIsColimit 📋 Mathlib.CategoryTheory.GradedObject.Unitor
  {C : Type u_1} {D : Type u_2} {I : Type u_3} {J : Type u_4} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] [Zero I] [DecidableEq I] [CategoryTheory.Limits.HasInitial C] (F : CategoryTheory.Functor D (CategoryTheory.Functor C D)) (Y : C) (e : F.flip.obj Y ≅ CategoryTheory.Functor.id D) [∀ (X : D), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) (F.obj X)] (p : J × I → J) (hp : ∀ (j : J), p (j, 0) = j) (X : CategoryTheory.GradedObject J D) (j : J) : CategoryTheory.Limits.IsColimit (CategoryTheory.GradedObject.mapBifunctorRightUnitorCofan F Y e p hp X j)
• CategoryTheory.GradedObject.mapBifunctorObjObjSingle₀Iso_hom 📋 Mathlib.CategoryTheory.GradedObject.Unitor
  {C : Type u_1} {D : Type u_2} {I : Type u_3} {J : Type u_4} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] [Zero I] [DecidableEq I] [CategoryTheory.Limits.HasInitial C] (F : CategoryTheory.Functor D (CategoryTheory.Functor C D)) (Y : C) (e : F.flip.obj Y ≅ CategoryTheory.Functor.id D) (X : CategoryTheory.GradedObject J D) (a : J × I) (ha : a.2 = 0) : (CategoryTheory.GradedObject.mapBifunctorObjObjSingle₀Iso F Y e X a ha).hom = CategoryTheory.CategoryStruct.comp ((F.obj (X a.1)).map (CategoryTheory.GradedObject.singleObjApplyIsoOfEq 0 Y a.2 ha).hom) (e.hom.app (X a.1))
• CategoryTheory.GradedObject.mapBifunctorObjObjSingle₀Iso_inv 📋 Mathlib.CategoryTheory.GradedObject.Unitor
  {C : Type u_1} {D : Type u_2} {I : Type u_3} {J : Type u_4} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] [Zero I] [DecidableEq I] [CategoryTheory.Limits.HasInitial C] (F : CategoryTheory.Functor D (CategoryTheory.Functor C D)) (Y : C) (e : F.flip.obj Y ≅ CategoryTheory.Functor.id D) (X : CategoryTheory.GradedObject J D) (a : J × I) (ha : a.2 = 0) : (CategoryTheory.GradedObject.mapBifunctorObjObjSingle₀Iso F Y e X a ha).inv = CategoryTheory.CategoryStruct.comp (e.inv.app (X a.1)) ((F.obj (X a.1)).map (CategoryTheory.GradedObject.singleObjApplyIsoOfEq 0 Y a.2 ha).inv)
• CategoryTheory.GradedObject.mapBifunctorObjSingle₀ObjIso_hom 📋 Mathlib.CategoryTheory.GradedObject.Unitor
  {C : Type u_1} {D : Type u_2} {I : Type u_3} {J : Type u_4} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] [Zero I] [DecidableEq I] [CategoryTheory.Limits.HasInitial C] (F : CategoryTheory.Functor C (CategoryTheory.Functor D D)) (X : C) (e : F.obj X ≅ CategoryTheory.Functor.id D) (Y : CategoryTheory.GradedObject J D) (a : I × J) (ha : a.1 = 0) : (CategoryTheory.GradedObject.mapBifunctorObjSingle₀ObjIso F X e Y a ha).hom = CategoryTheory.CategoryStruct.comp ((F.map (CategoryTheory.GradedObject.singleObjApplyIsoOfEq 0 X a.1 ha).hom).app (Y a.2)) (e.hom.app (Y a.2))
• CategoryTheory.GradedObject.mapBifunctorObjSingle₀ObjIso_inv 📋 Mathlib.CategoryTheory.GradedObject.Unitor
  {C : Type u_1} {D : Type u_2} {I : Type u_3} {J : Type u_4} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] [Zero I] [DecidableEq I] [CategoryTheory.Limits.HasInitial C] (F : CategoryTheory.Functor C (CategoryTheory.Functor D D)) (X : C) (e : F.obj X ≅ CategoryTheory.Functor.id D) (Y : CategoryTheory.GradedObject J D) (a : I × J) (ha : a.1 = 0) : (CategoryTheory.GradedObject.mapBifunctorObjSingle₀ObjIso F X e Y a ha).inv = CategoryTheory.CategoryStruct.comp (e.inv.app (Y a.2)) ((F.map (CategoryTheory.GradedObject.singleObjApplyIsoOfEq 0 X a.1 ha).inv).app (Y a.2))
• CategoryTheory.GradedObject.ι_mapBifunctorRightUnitor_hom_apply 📋 Mathlib.CategoryTheory.GradedObject.Unitor
  {C : Type u_1} {D : Type u_2} {I : Type u_3} {J : Type u_4} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] [Zero I] [DecidableEq I] [CategoryTheory.Limits.HasInitial C] (F : CategoryTheory.Functor D (CategoryTheory.Functor C D)) (Y : C) (e : F.flip.obj Y ≅ CategoryTheory.Functor.id D) [∀ (X : D), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) (F.obj X)] (p : J × I → J) (hp : ∀ (j : J), p (j, 0) = j) (X : CategoryTheory.GradedObject J D) [(((CategoryTheory.GradedObject.mapBifunctor F J I).obj X).obj ((CategoryTheory.GradedObject.single₀ I).obj Y)).HasMap p] (j : J) : CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.ιMapBifunctorMapObj F p X ((CategoryTheory.GradedObject.single₀ I).obj Y) j 0 j ⋯) ((CategoryTheory.GradedObject.mapBifunctorRightUnitor F Y e p hp X).hom j) = CategoryTheory.CategoryStruct.comp ((F.obj (X j)).map (CategoryTheory.GradedObject.singleObjApplyIso 0 Y).hom) (e.hom.app (X j))
• CategoryTheory.GradedObject.mapBifunctorLeftUnitor_inv_naturality 📋 Mathlib.CategoryTheory.GradedObject.Unitor
  {C : Type u_1} {D : Type u_2} {I : Type u_3} {J : Type u_4} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] [Zero I] [DecidableEq I] [CategoryTheory.Limits.HasInitial C] (F : CategoryTheory.Functor C (CategoryTheory.Functor D D)) (X : C) (e : F.obj X ≅ CategoryTheory.Functor.id D) [∀ (Y : D), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) (F.flip.obj Y)] (p : I × J → J) (hp : ∀ (j : J), p (0, j) = j) {Y Y' : CategoryTheory.GradedObject J D} (φ : Y ⟶ Y') [(((CategoryTheory.GradedObject.mapBifunctor F I J).obj ((CategoryTheory.GradedObject.single₀ I).obj X)).obj Y).HasMap p] [(((CategoryTheory.GradedObject.mapBifunctor F I J).obj ((CategoryTheory.GradedObject.single₀ I).obj X)).obj Y').HasMap p] : CategoryTheory.CategoryStruct.comp φ (CategoryTheory.GradedObject.mapBifunctorLeftUnitor F X e p hp Y').inv = CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.mapBifunctorLeftUnitor F X e p hp Y).inv (CategoryTheory.GradedObject.mapBifunctorMapMap F p (CategoryTheory.CategoryStruct.id ((CategoryTheory.GradedObject.single₀ I).obj X)) φ)
• CategoryTheory.GradedObject.mapBifunctorLeftUnitor_naturality 📋 Mathlib.CategoryTheory.GradedObject.Unitor
  {C : Type u_1} {D : Type u_2} {I : Type u_3} {J : Type u_4} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] [Zero I] [DecidableEq I] [CategoryTheory.Limits.HasInitial C] (F : CategoryTheory.Functor C (CategoryTheory.Functor D D)) (X : C) (e : F.obj X ≅ CategoryTheory.Functor.id D) [∀ (Y : D), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) (F.flip.obj Y)] (p : I × J → J) (hp : ∀ (j : J), p (0, j) = j) {Y Y' : CategoryTheory.GradedObject J D} (φ : Y ⟶ Y') [(((CategoryTheory.GradedObject.mapBifunctor F I J).obj ((CategoryTheory.GradedObject.single₀ I).obj X)).obj Y).HasMap p] [(((CategoryTheory.GradedObject.mapBifunctor F I J).obj ((CategoryTheory.GradedObject.single₀ I).obj X)).obj Y').HasMap p] : CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.mapBifunctorMapMap F p (CategoryTheory.CategoryStruct.id ((CategoryTheory.GradedObject.single₀ I).obj X)) φ) (CategoryTheory.GradedObject.mapBifunctorLeftUnitor F X e p hp Y').hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.mapBifunctorLeftUnitor F X e p hp Y).hom φ
• CategoryTheory.GradedObject.mapBifunctorRightUnitor_inv_naturality 📋 Mathlib.CategoryTheory.GradedObject.Unitor
  {C : Type u_1} {D : Type u_2} {I : Type u_3} {J : Type u_4} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] [Zero I] [DecidableEq I] [CategoryTheory.Limits.HasInitial C] (F : CategoryTheory.Functor D (CategoryTheory.Functor C D)) {Y : C} (e : F.flip.obj Y ≅ CategoryTheory.Functor.id D) [∀ (X : D), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) (F.obj X)] (p : J × I → J) (hp : ∀ (j : J), p (j, 0) = j) (X X' : CategoryTheory.GradedObject J D) (φ : X ⟶ X') [(((CategoryTheory.GradedObject.mapBifunctor F J I).obj X).obj ((CategoryTheory.GradedObject.single₀ I).obj Y)).HasMap p] [(((CategoryTheory.GradedObject.mapBifunctor F J I).obj X').obj ((CategoryTheory.GradedObject.single₀ I).obj Y)).HasMap p] : CategoryTheory.CategoryStruct.comp φ (CategoryTheory.GradedObject.mapBifunctorRightUnitor F Y e p hp X').inv = CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.mapBifunctorRightUnitor F Y e p hp X).inv (CategoryTheory.GradedObject.mapBifunctorMapMap F p φ (CategoryTheory.CategoryStruct.id ((CategoryTheory.GradedObject.single₀ I).obj Y)))
• CategoryTheory.GradedObject.mapBifunctorRightUnitor_naturality 📋 Mathlib.CategoryTheory.GradedObject.Unitor
  {C : Type u_1} {D : Type u_2} {I : Type u_3} {J : Type u_4} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] [Zero I] [DecidableEq I] [CategoryTheory.Limits.HasInitial C] (F : CategoryTheory.Functor D (CategoryTheory.Functor C D)) {Y : C} (e : F.flip.obj Y ≅ CategoryTheory.Functor.id D) [∀ (X : D), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) (F.obj X)] (p : J × I → J) (hp : ∀ (j : J), p (j, 0) = j) (X X' : CategoryTheory.GradedObject J D) (φ : X ⟶ X') [(((CategoryTheory.GradedObject.mapBifunctor F J I).obj X).obj ((CategoryTheory.GradedObject.single₀ I).obj Y)).HasMap p] [(((CategoryTheory.GradedObject.mapBifunctor F J I).obj X').obj ((CategoryTheory.GradedObject.single₀ I).obj Y)).HasMap p] : CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.mapBifunctorMapMap F p φ (CategoryTheory.CategoryStruct.id ((CategoryTheory.GradedObject.single₀ I).obj Y))) (CategoryTheory.GradedObject.mapBifunctorRightUnitor F Y e p hp X').hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.mapBifunctorRightUnitor F Y e p hp X).hom φ
• CategoryTheory.GradedObject.mapBifunctorRightUnitor_inv_apply 📋 Mathlib.CategoryTheory.GradedObject.Unitor
  {C : Type u_1} {D : Type u_2} {I : Type u_3} {J : Type u_4} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] [Zero I] [DecidableEq I] [CategoryTheory.Limits.HasInitial C] (F : CategoryTheory.Functor D (CategoryTheory.Functor C D)) (Y : C) (e : F.flip.obj Y ≅ CategoryTheory.Functor.id D) [∀ (X : D), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) (F.obj X)] (p : J × I → J) (hp : ∀ (j : J), p (j, 0) = j) (X : CategoryTheory.GradedObject J D) [(((CategoryTheory.GradedObject.mapBifunctor F J I).obj X).obj ((CategoryTheory.GradedObject.single₀ I).obj Y)).HasMap p] (j : J) : (CategoryTheory.GradedObject.mapBifunctorRightUnitor F Y e p hp X).inv j = CategoryTheory.CategoryStruct.comp (e.inv.app (X j)) (CategoryTheory.CategoryStruct.comp ((F.obj (X j)).map (CategoryTheory.GradedObject.singleObjApplyIso 0 Y).inv) (CategoryTheory.GradedObject.ιMapBifunctorMapObj F p X ((CategoryTheory.GradedObject.single₀ I).obj Y) j 0 j ⋯))
• CategoryTheory.GradedObject.ι_mapBifunctorLeftUnitor_hom_apply 📋 Mathlib.CategoryTheory.GradedObject.Unitor
  {C : Type u_1} {D : Type u_2} {I : Type u_3} {J : Type u_4} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] [Zero I] [DecidableEq I] [CategoryTheory.Limits.HasInitial C] (F : CategoryTheory.Functor C (CategoryTheory.Functor D D)) (X : C) (e : F.obj X ≅ CategoryTheory.Functor.id D) [∀ (Y : D), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) (F.flip.obj Y)] (p : I × J → J) (hp : ∀ (j : J), p (0, j) = j) (Y : CategoryTheory.GradedObject J D) [(((CategoryTheory.GradedObject.mapBifunctor F I J).obj ((CategoryTheory.GradedObject.single₀ I).obj X)).obj Y).HasMap p] (j : J) : CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.ιMapBifunctorMapObj F p ((CategoryTheory.GradedObject.single₀ I).obj X) Y 0 j j ⋯) ((CategoryTheory.GradedObject.mapBifunctorLeftUnitor F X e p hp Y).hom j) = CategoryTheory.CategoryStruct.comp ((F.map (CategoryTheory.GradedObject.singleObjApplyIso 0 X).hom).app (Y j)) (e.hom.app (Y j))
• CategoryTheory.GradedObject.mapBifunctorLeftUnitor_inv_apply 📋 Mathlib.CategoryTheory.GradedObject.Unitor
  {C : Type u_1} {D : Type u_2} {I : Type u_3} {J : Type u_4} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] [Zero I] [DecidableEq I] [CategoryTheory.Limits.HasInitial C] (F : CategoryTheory.Functor C (CategoryTheory.Functor D D)) (X : C) (e : F.obj X ≅ CategoryTheory.Functor.id D) [∀ (Y : D), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) (F.flip.obj Y)] (p : I × J → J) (hp : ∀ (j : J), p (0, j) = j) (Y : CategoryTheory.GradedObject J D) [(((CategoryTheory.GradedObject.mapBifunctor F I J).obj ((CategoryTheory.GradedObject.single₀ I).obj X)).obj Y).HasMap p] (j : J) : (CategoryTheory.GradedObject.mapBifunctorLeftUnitor F X e p hp Y).inv j = CategoryTheory.CategoryStruct.comp (e.inv.app (Y j)) (CategoryTheory.CategoryStruct.comp ((F.map (CategoryTheory.GradedObject.singleObjApplyIso 0 X).inv).app (Y j)) (CategoryTheory.GradedObject.ιMapBifunctorMapObj F p ((CategoryTheory.GradedObject.single₀ I).obj X) Y 0 j j ⋯))
• CategoryTheory.GradedObject.ι_mapBifunctorRightUnitor_hom_apply_assoc 📋 Mathlib.CategoryTheory.GradedObject.Unitor
  {C : Type u_1} {D : Type u_2} {I : Type u_3} {J : Type u_4} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] [Zero I] [DecidableEq I] [CategoryTheory.Limits.HasInitial C] (F : CategoryTheory.Functor D (CategoryTheory.Functor C D)) (Y : C) (e : F.flip.obj Y ≅ CategoryTheory.Functor.id D) [∀ (X : D), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) (F.obj X)] (p : J × I → J) (hp : ∀ (j : J), p (j, 0) = j) (X : CategoryTheory.GradedObject J D) [(((CategoryTheory.GradedObject.mapBifunctor F J I).obj X).obj ((CategoryTheory.GradedObject.single₀ I).obj Y)).HasMap p] (j : J) {Z : D} (h : X j ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.ιMapBifunctorMapObj F p X ((CategoryTheory.GradedObject.single₀ I).obj Y) j 0 j ⋯) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.GradedObject.mapBifunctorRightUnitor F Y e p hp X).hom j) h) = CategoryTheory.CategoryStruct.comp ((F.obj (X j)).map (CategoryTheory.GradedObject.singleObjApplyIso 0 Y).hom) (CategoryTheory.CategoryStruct.comp (e.hom.app (X j)) h)
• CategoryTheory.GradedObject.mapBifunctorLeftUnitor_inv_naturality_assoc 📋 Mathlib.CategoryTheory.GradedObject.Unitor
  {C : Type u_1} {D : Type u_2} {I : Type u_3} {J : Type u_4} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] [Zero I] [DecidableEq I] [CategoryTheory.Limits.HasInitial C] (F : CategoryTheory.Functor C (CategoryTheory.Functor D D)) (X : C) (e : F.obj X ≅ CategoryTheory.Functor.id D) [∀ (Y : D), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) (F.flip.obj Y)] (p : I × J → J) (hp : ∀ (j : J), p (0, j) = j) {Y Y' : CategoryTheory.GradedObject J D} (φ : Y ⟶ Y') [(((CategoryTheory.GradedObject.mapBifunctor F I J).obj ((CategoryTheory.GradedObject.single₀ I).obj X)).obj Y).HasMap p] [(((CategoryTheory.GradedObject.mapBifunctor F I J).obj ((CategoryTheory.GradedObject.single₀ I).obj X)).obj Y').HasMap p] {Z : CategoryTheory.GradedObject J D} (h : CategoryTheory.GradedObject.mapBifunctorMapObj F p ((CategoryTheory.GradedObject.single₀ I).obj X) Y' ⟶ Z) : CategoryTheory.CategoryStruct.comp φ (CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.mapBifunctorLeftUnitor F X e p hp Y').inv h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.mapBifunctorLeftUnitor F X e p hp Y).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.mapBifunctorMapMap F p (CategoryTheory.CategoryStruct.id ((CategoryTheory.GradedObject.single₀ I).obj X)) φ) h)
• CategoryTheory.GradedObject.mapBifunctorLeftUnitor_naturality_assoc 📋 Mathlib.CategoryTheory.GradedObject.Unitor
  {C : Type u_1} {D : Type u_2} {I : Type u_3} {J : Type u_4} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] [Zero I] [DecidableEq I] [CategoryTheory.Limits.HasInitial C] (F : CategoryTheory.Functor C (CategoryTheory.Functor D D)) (X : C) (e : F.obj X ≅ CategoryTheory.Functor.id D) [∀ (Y : D), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) (F.flip.obj Y)] (p : I × J → J) (hp : ∀ (j : J), p (0, j) = j) {Y Y' : CategoryTheory.GradedObject J D} (φ : Y ⟶ Y') [(((CategoryTheory.GradedObject.mapBifunctor F I J).obj ((CategoryTheory.GradedObject.single₀ I).obj X)).obj Y).HasMap p] [(((CategoryTheory.GradedObject.mapBifunctor F I J).obj ((CategoryTheory.GradedObject.single₀ I).obj X)).obj Y').HasMap p] {Z : CategoryTheory.GradedObject J D} (h : Y' ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.mapBifunctorMapMap F p (CategoryTheory.CategoryStruct.id ((CategoryTheory.GradedObject.single₀ I).obj X)) φ) (CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.mapBifunctorLeftUnitor F X e p hp Y').hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.mapBifunctorLeftUnitor F X e p hp Y).hom (CategoryTheory.CategoryStruct.comp φ h)
• CategoryTheory.GradedObject.mapBifunctorRightUnitor_inv_naturality_assoc 📋 Mathlib.CategoryTheory.GradedObject.Unitor
  {C : Type u_1} {D : Type u_2} {I : Type u_3} {J : Type u_4} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] [Zero I] [DecidableEq I] [CategoryTheory.Limits.HasInitial C] (F : CategoryTheory.Functor D (CategoryTheory.Functor C D)) {Y : C} (e : F.flip.obj Y ≅ CategoryTheory.Functor.id D) [∀ (X : D), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) (F.obj X)] (p : J × I → J) (hp : ∀ (j : J), p (j, 0) = j) (X X' : CategoryTheory.GradedObject J D) (φ : X ⟶ X') [(((CategoryTheory.GradedObject.mapBifunctor F J I).obj X).obj ((CategoryTheory.GradedObject.single₀ I).obj Y)).HasMap p] [(((CategoryTheory.GradedObject.mapBifunctor F J I).obj X').obj ((CategoryTheory.GradedObject.single₀ I).obj Y)).HasMap p] {Z : CategoryTheory.GradedObject J D} (h : CategoryTheory.GradedObject.mapBifunctorMapObj F p X' ((CategoryTheory.GradedObject.single₀ I).obj Y) ⟶ Z) : CategoryTheory.CategoryStruct.comp φ (CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.mapBifunctorRightUnitor F Y e p hp X').inv h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.mapBifunctorRightUnitor F Y e p hp X).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.mapBifunctorMapMap F p φ (CategoryTheory.CategoryStruct.id ((CategoryTheory.GradedObject.single₀ I).obj Y))) h)
• CategoryTheory.GradedObject.mapBifunctorRightUnitor_naturality_assoc 📋 Mathlib.CategoryTheory.GradedObject.Unitor
  {C : Type u_1} {D : Type u_2} {I : Type u_3} {J : Type u_4} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] [Zero I] [DecidableEq I] [CategoryTheory.Limits.HasInitial C] (F : CategoryTheory.Functor D (CategoryTheory.Functor C D)) {Y : C} (e : F.flip.obj Y ≅ CategoryTheory.Functor.id D) [∀ (X : D), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) (F.obj X)] (p : J × I → J) (hp : ∀ (j : J), p (j, 0) = j) (X X' : CategoryTheory.GradedObject J D) (φ : X ⟶ X') [(((CategoryTheory.GradedObject.mapBifunctor F J I).obj X).obj ((CategoryTheory.GradedObject.single₀ I).obj Y)).HasMap p] [(((CategoryTheory.GradedObject.mapBifunctor F J I).obj X').obj ((CategoryTheory.GradedObject.single₀ I).obj Y)).HasMap p] {Z : CategoryTheory.GradedObject J D} (h : X' ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.mapBifunctorMapMap F p φ (CategoryTheory.CategoryStruct.id ((CategoryTheory.GradedObject.single₀ I).obj Y))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.mapBifunctorRightUnitor F Y e p hp X').hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.mapBifunctorRightUnitor F Y e p hp X).hom (CategoryTheory.CategoryStruct.comp φ h)
• CategoryTheory.GradedObject.ι_mapBifunctorLeftUnitor_hom_apply_assoc 📋 Mathlib.CategoryTheory.GradedObject.Unitor
  {C : Type u_1} {D : Type u_2} {I : Type u_3} {J : Type u_4} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] [Zero I] [DecidableEq I] [CategoryTheory.Limits.HasInitial C] (F : CategoryTheory.Functor C (CategoryTheory.Functor D D)) (X : C) (e : F.obj X ≅ CategoryTheory.Functor.id D) [∀ (Y : D), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) (F.flip.obj Y)] (p : I × J → J) (hp : ∀ (j : J), p (0, j) = j) (Y : CategoryTheory.GradedObject J D) [(((CategoryTheory.GradedObject.mapBifunctor F I J).obj ((CategoryTheory.GradedObject.single₀ I).obj X)).obj Y).HasMap p] (j : J) {Z : D} (h : Y j ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.ιMapBifunctorMapObj F p ((CategoryTheory.GradedObject.single₀ I).obj X) Y 0 j j ⋯) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.GradedObject.mapBifunctorLeftUnitor F X e p hp Y).hom j) h) = CategoryTheory.CategoryStruct.comp ((F.map (CategoryTheory.GradedObject.singleObjApplyIso 0 X).hom).app (Y j)) (CategoryTheory.CategoryStruct.comp (e.hom.app (Y j)) h)
• CategoryTheory.GradedObject.mapBifunctorRightUnitorCofan_inj 📋 Mathlib.CategoryTheory.GradedObject.Unitor
  {C : Type u_1} {D : Type u_2} {I : Type u_3} {J : Type u_4} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] [Zero I] [DecidableEq I] [CategoryTheory.Limits.HasInitial C] (F : CategoryTheory.Functor D (CategoryTheory.Functor C D)) (Y : C) (e : F.flip.obj Y ≅ CategoryTheory.Functor.id D) [∀ (X : D), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) (F.obj X)] (p : J × I → J) (hp : ∀ (j : J), p (j, 0) = j) (X : CategoryTheory.GradedObject J D) (j : J) : CategoryTheory.Limits.Cofan.inj (CategoryTheory.GradedObject.mapBifunctorRightUnitorCofan F Y e p hp X j) ⟨(j, 0), ⋯⟩ = CategoryTheory.CategoryStruct.comp ((F.obj (X j)).map (CategoryTheory.GradedObject.singleObjApplyIso 0 Y).hom) (e.hom.app (X j))
• CategoryTheory.GradedObject.mapBifunctorLeftUnitorCofan_inj 📋 Mathlib.CategoryTheory.GradedObject.Unitor
  {C : Type u_1} {D : Type u_2} {I : Type u_3} {J : Type u_4} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] [Zero I] [DecidableEq I] [CategoryTheory.Limits.HasInitial C] (F : CategoryTheory.Functor C (CategoryTheory.Functor D D)) (X : C) (e : F.obj X ≅ CategoryTheory.Functor.id D) [∀ (Y : D), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) (F.flip.obj Y)] (p : I × J → J) (hp : ∀ (j : J), p (0, j) = j) (Y : CategoryTheory.GradedObject J D) (j : J) : CategoryTheory.Limits.Cofan.inj (CategoryTheory.GradedObject.mapBifunctorLeftUnitorCofan F X e p hp Y j) ⟨(0, j), ⋯⟩ = CategoryTheory.CategoryStruct.comp ((F.map (CategoryTheory.GradedObject.singleObjApplyIso 0 X).hom).app (Y j)) (e.hom.app (Y j))
• CategoryTheory.GradedObject.mapBifunctorRightUnitorCofan_inj_assoc 📋 Mathlib.CategoryTheory.GradedObject.Unitor
  {C : Type u_1} {D : Type u_2} {I : Type u_3} {J : Type u_4} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] [Zero I] [DecidableEq I] [CategoryTheory.Limits.HasInitial C] (F : CategoryTheory.Functor D (CategoryTheory.Functor C D)) (Y : C) (e : F.flip.obj Y ≅ CategoryTheory.Functor.id D) [∀ (X : D), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) (F.obj X)] (p : J × I → J) (hp : ∀ (j : J), p (j, 0) = j) (X : CategoryTheory.GradedObject J D) (j : J) {Z : D} (h : (CategoryTheory.GradedObject.mapBifunctorRightUnitorCofan F Y e p hp X j).pt ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Cofan.inj (CategoryTheory.GradedObject.mapBifunctorRightUnitorCofan F Y e p hp X j) ⟨(j, 0), ⋯⟩) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp ((F.obj (X j)).map (CategoryTheory.GradedObject.singleObjApplyIso 0 Y).hom) (e.hom.app (X j))) h
• CategoryTheory.GradedObject.mapBifunctorLeftUnitorCofan_inj_assoc 📋 Mathlib.CategoryTheory.GradedObject.Unitor
  {C : Type u_1} {D : Type u_2} {I : Type u_3} {J : Type u_4} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] [Zero I] [DecidableEq I] [CategoryTheory.Limits.HasInitial C] (F : CategoryTheory.Functor C (CategoryTheory.Functor D D)) (X : C) (e : F.obj X ≅ CategoryTheory.Functor.id D) [∀ (Y : D), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) (F.flip.obj Y)] (p : I × J → J) (hp : ∀ (j : J), p (0, j) = j) (Y : CategoryTheory.GradedObject J D) (j : J) {Z : D} (h : (CategoryTheory.GradedObject.mapBifunctorLeftUnitorCofan F X e p hp Y j).pt ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Cofan.inj (CategoryTheory.GradedObject.mapBifunctorLeftUnitorCofan F X e p hp Y j) ⟨(0, j), ⋯⟩) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp ((F.map (CategoryTheory.GradedObject.singleObjApplyIso 0 X).hom).app (Y j)) (e.hom.app (Y j))) h
• CategoryTheory.GradedObject.mapBifunctor_triangle 📋 Mathlib.CategoryTheory.GradedObject.Unitor
  {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {D : Type u_4} {I₁ : Type u_5} {I₂ : Type u_6} {I₃ : Type u_7} {J : Type u_8} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Category.{v_3, u_3} C₃] [CategoryTheory.Category.{v_4, u_4} D] [Zero I₂] [DecidableEq I₂] [CategoryTheory.Limits.HasInitial C₂] {F₁ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁)} {F₂ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₃)} {G : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₃ D)} (associator : CategoryTheory.bifunctorComp₁₂ F₁ G ≅ CategoryTheory.bifunctorComp₂₃ G F₂) (X₂ : C₂) (e₁ : F₁.flip.obj X₂ ≅ CategoryTheory.Functor.id C₁) (e₂ : F₂.obj X₂ ≅ CategoryTheory.Functor.id C₃) [∀ (X₁ : C₁), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C₂) (F₁.obj X₁)] [∀ (X₃ : C₃), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C₂) (F₂.flip.obj X₃)] {r : I₁ × I₂ × I₃ → J} {π : I₁ × I₃ → J} (τ : CategoryTheory.GradedObject.TriangleIndexData r π) (X₁ : CategoryTheory.GradedObject I₁ C₁) (X₃ : CategoryTheory.GradedObject I₃ C₃) [(((CategoryTheory.GradedObject.mapBifunctor F₁ I₁ I₂).obj X₁).obj ((CategoryTheory.GradedObject.single₀ I₂).obj X₂)).HasMap τ.p₁₂] [(((CategoryTheory.GradedObject.mapBifunctor G I₁ I₃).obj (CategoryTheory.GradedObject.mapBifunctorMapObj F₁ τ.p₁₂ X₁ ((CategoryTheory.GradedObject.single₀ I₂).obj X₂))).obj X₃).HasMap π] [(((CategoryTheory.GradedObject.mapBifunctor F₂ I₂ I₃).obj ((CategoryTheory.GradedObject.single₀ I₂).obj X₂)).obj X₃).HasMap τ.p₂₃] [(((CategoryTheory.GradedObject.mapBifunctor G I₁ I₃).obj X₁).obj (CategoryTheory.GradedObject.mapBifunctorMapObj F₂ τ.p₂₃ ((CategoryTheory.GradedObject.single₀ I₂).obj X₂) X₃)).HasMap π] [CategoryTheory.GradedObject.HasGoodTrifunctor₁₂Obj F₁ G τ.ρ₁₂ X₁ ((CategoryTheory.GradedObject.single₀ I₂).obj X₂) X₃] [CategoryTheory.GradedObject.HasGoodTrifunctor₂₃Obj G F₂ τ.ρ₂₃ X₁ ((CategoryTheory.GradedObject.single₀ I₂).obj X₂) X₃] [(((CategoryTheory.GradedObject.mapBifunctor G I₁ I₃).obj X₁).obj X₃).HasMap π] (triangle : ∀ (X₁ : C₁) (X₃ : C₃), CategoryTheory.CategoryStruct.comp (((associator.hom.app X₁).app X₂).app X₃) ((G.obj X₁).map (e₂.hom.app X₃)) = (G.map (e₁.hom.app X₁)).app X₃) : CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.mapBifunctorAssociator associator τ.ρ₁₂ τ.ρ₂₃ X₁ ((CategoryTheory.GradedObject.single₀ I₂).obj X₂) X₃).hom (CategoryTheory.GradedObject.mapBifunctorMapMap G π (CategoryTheory.CategoryStruct.id X₁) (CategoryTheory.GradedObject.mapBifunctorLeftUnitor F₂ X₂ e₂ τ.p₂₃ ⋯ X₃).hom) = CategoryTheory.GradedObject.mapBifunctorMapMap G π (CategoryTheory.GradedObject.mapBifunctorRightUnitor F₁ X₂ e₁ τ.p₁₂ ⋯ X₁).hom (CategoryTheory.CategoryStruct.id X₃)
• CategoryTheory.GradedObject.Monoidal.instHasMapProdObjFunctorMapBifunctorCurriedTensorSingle₀TensorUnit_1 📋 Mathlib.CategoryTheory.GradedObject.Monoidal
  {I : Type u} [AddMonoid I] {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.MonoidalCategory C] [DecidableEq I] [CategoryTheory.Limits.HasInitial C] [∀ (X₁ : C), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) ((CategoryTheory.MonoidalCategory.curriedTensor C).obj X₁)] (X : CategoryTheory.GradedObject I C) : (((CategoryTheory.GradedObject.mapBifunctor (CategoryTheory.MonoidalCategory.curriedTensor C) I I).obj X).obj ((CategoryTheory.GradedObject.single₀ I).obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))).HasMap fun x => match x with | (i₁, i₂) => i₁ + i₂
• CategoryTheory.GradedObject.Monoidal.instHasMapProdObjFunctorMapBifunctorCurriedTensorSingle₀TensorUnit 📋 Mathlib.CategoryTheory.GradedObject.Monoidal
  {I : Type u} [AddMonoid I] {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.MonoidalCategory C] [DecidableEq I] [CategoryTheory.Limits.HasInitial C] [∀ (X₂ : C), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) ((CategoryTheory.MonoidalCategory.curriedTensor C).flip.obj X₂)] (X : CategoryTheory.GradedObject I C) : (((CategoryTheory.GradedObject.mapBifunctor (CategoryTheory.MonoidalCategory.curriedTensor C) I I).obj ((CategoryTheory.GradedObject.single₀ I).obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))).obj X).HasMap fun x => match x with | (i₁, i₂) => i₁ + 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 69fae59