ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>C₃ : Type u_3<VAR>C₄ : Type u_4<VAR>C₁₂ : Type u_5<VAR>CategoryTheory.Category.{u_7, u_1} C₁<VAR>CategoryTheory.Category.{u_8, u_2} C₂<VAR>CategoryTheory.Category.{u_9, u_3} C₃<VAR>CategoryTheory.Category.{u_10, u_4} C₄<VAR>CategoryTheory.Category.{u_11, u_5} C₁₂<VAR>F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)<VAR>G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)<VAR>X₁ : C₁<VAR>X₂ : C₂<VAR>X₃ Y₃ : C₃<VAR>φ : X₃ ⟶ Y₃<GOAL>((CategoryTheory.bifunctorComp₁₂Obj F₁₂ G X₁).obj X₂).map φ = (G.obj ((F₁₂.obj X₁).obj X₂)).map φ
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>C₃ : Type u_3<VAR>C₄ : Type u_4<VAR>C₁₂ : Type u_5<VAR>CategoryTheory.Category.{u_7, u_1} C₁<VAR>CategoryTheory.Category.{u_8, u_2} C₂<VAR>CategoryTheory.Category.{u_9, u_3} C₃<VAR>CategoryTheory.Category.{u_10, u_4} C₄<VAR>CategoryTheory.Category.{u_11, u_5} C₁₂<VAR>F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)<VAR>G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)<VAR>X₁ Y₁ : C₁<VAR>φ : X₁ ⟶ Y₁<VAR>X₂ : C₂<VAR>X₃ : C₃<GOAL>(((CategoryTheory.bifunctorComp₁₂ F₁₂ G).map φ).app X₂).app X₃ = (G.map ((F₁₂.map φ).app X₂)).app X₃
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>C₃ : Type u_3<VAR>C₄ : Type u_4<VAR>C₁₂ : Type u_5<VAR>CategoryTheory.Category.{u_7, u_1} C₁<VAR>CategoryTheory.Category.{u_8, u_2} C₂<VAR>CategoryTheory.Category.{u_9, u_3} C₃<VAR>CategoryTheory.Category.{u_10, u_4} C₄<VAR>CategoryTheory.Category.{u_11, u_5} C₁₂<VAR>F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)<VAR>G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)<VAR>X₁ : C₁<GOAL>(CategoryTheory.bifunctorComp₁₂ F₁₂ G).obj X₁ = CategoryTheory.bifunctorComp₁₂Obj F₁₂ G X₁
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>C₃ : Type u_3<VAR>C₄ : Type u_4<VAR>C₂₃ : Type u_6<VAR>CategoryTheory.Category.{u_7, u_1} C₁<VAR>CategoryTheory.Category.{u_8, u_2} C₂<VAR>CategoryTheory.Category.{u_9, u_3} C₃<VAR>CategoryTheory.Category.{u_10, u_4} C₄<VAR>CategoryTheory.Category.{u_11, u_6} C₂₃<VAR>F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄)<VAR>G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)<VAR>X₁ : C₁<VAR>X₂ : C₂<VAR>X₃ Y₃ : C₃<VAR>φ : X₃ ⟶ Y₃<GOAL>((CategoryTheory.bifunctorComp₂₃Obj F G₂₃ X₁).obj X₂).map φ = (F.obj X₁).map ((G₂₃.obj X₂).map φ)
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>C₃ : Type u_3<VAR>C₄ : Type u_4<VAR>C₂₃ : Type u_6<VAR>CategoryTheory.Category.{u_7, u_1} C₁<VAR>CategoryTheory.Category.{u_8, u_2} C₂<VAR>CategoryTheory.Category.{u_9, u_3} C₃<VAR>CategoryTheory.Category.{u_10, u_4} C₄<VAR>CategoryTheory.Category.{u_11, u_6} C₂₃<VAR>F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄)<VAR>G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)<VAR>X₁ : C₁<VAR>X₂ Y₂ : C₂<VAR>φ : X₂ ⟶ Y₂<VAR>X₃ : C₃<GOAL>((CategoryTheory.bifunctorComp₂₃Obj F G₂₃ X₁).map φ).app X₃ = (F.obj X₁).map ((G₂₃.map φ).app X₃)
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>C₃ : Type u_3<VAR>C₄ : Type u_4<VAR>C₂₃ : Type u_6<VAR>CategoryTheory.Category.{u_7, u_1} C₁<VAR>CategoryTheory.Category.{u_8, u_2} C₂<VAR>CategoryTheory.Category.{u_9, u_3} C₃<VAR>CategoryTheory.Category.{u_10, u_4} C₄<VAR>CategoryTheory.Category.{u_11, u_6} C₂₃<VAR>F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄)<VAR>G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)<VAR>X₁ : C₁<VAR>X₂ : C₂<VAR>X₃ : C₃<GOAL>((CategoryTheory.bifunctorComp₂₃Obj F G₂₃ X₁).obj X₂).obj X₃ = (F.obj X₁).obj ((G₂₃.obj X₂).obj X₃)
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>C₃ : Type u_3<VAR>C₄ : Type u_4<VAR>C₂₃ : Type u_6<VAR>CategoryTheory.Category.{u_7, u_1} C₁<VAR>CategoryTheory.Category.{u_8, u_2} C₂<VAR>CategoryTheory.Category.{u_9, u_3} C₃<VAR>CategoryTheory.Category.{u_10, u_4} C₄<VAR>CategoryTheory.Category.{u_11, u_6} C₂₃<VAR>F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄)<VAR>G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)<VAR>X₁ : C₁<GOAL>(CategoryTheory.bifunctorComp₂₃ F G₂₃).obj X₁ = CategoryTheory.bifunctorComp₂₃Obj F G₂₃ X₁
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>C₃ : Type u_3<VAR>C₄ : Type u_4<VAR>C₂₃ : Type u_6<VAR>CategoryTheory.Category.{u_7, u_1} C₁<VAR>CategoryTheory.Category.{u_8, u_2} C₂<VAR>CategoryTheory.Category.{u_9, u_3} C₃<VAR>CategoryTheory.Category.{u_10, u_4} C₄<VAR>CategoryTheory.Category.{u_11, u_6} C₂₃<VAR>F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄)<VAR>G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)<VAR>X₁ Y₁ : C₁<VAR>φ : X₁ ⟶ Y₁<VAR>X₂ : C₂<VAR>X₃ : C₃<GOAL>(((CategoryTheory.bifunctorComp₂₃ F G₂₃).map φ).app X₂).app X₃ = (F.map φ).app ((G₂₃.obj X₂).obj X₃)
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>C₃ : Type u_3<VAR>C₄ : Type u_4<VAR>CategoryTheory.Category.{u_10, u_1} C₁<VAR>CategoryTheory.Category.{u_11, u_2} C₂<VAR>CategoryTheory.Category.{u_12, u_3} C₃<VAR>CategoryTheory.Category.{u_13, u_4} C₄<VAR>F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₄))<VAR>I₁ : Type u_7<VAR>X₁ : CategoryTheory.GradedObject I₁ C₁<VAR>I₂ : Type u_8<VAR>I₃ : Type u_9<VAR>X₂ Y₂ : CategoryTheory.GradedObject I₂ C₂<VAR>φ : X₂ ⟶ Y₂<VAR>X₃ : CategoryTheory.GradedObject I₃ C₃<VAR>x : I₁ × I₂ × I₃<GOAL>((CategoryTheory.GradedObject.mapTrifunctorObj F X₁ I₂ I₃).map φ).app X₃ x = ((F.obj (X₁ x.1)).map (φ x.2.1)).app (X₃ x.2.2)
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>C₃ : Type u_3<VAR>C₄ : Type u_4<VAR>CategoryTheory.Category.{u_10, u_1} C₁<VAR>CategoryTheory.Category.{u_11, u_2} C₂<VAR>CategoryTheory.Category.{u_12, u_3} C₃<VAR>CategoryTheory.Category.{u_13, u_4} C₄<VAR>F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₄))<VAR>I₁ : Type u_7<VAR>X₁ : CategoryTheory.GradedObject I₁ C₁<VAR>I₂ : Type u_8<VAR>I₃ : Type u_9<VAR>X₂ : CategoryTheory.GradedObject I₂ C₂<VAR>X₃ : CategoryTheory.GradedObject I₃ C₃<VAR>x : I₁ × I₂ × I₃<GOAL>((CategoryTheory.GradedObject.mapTrifunctorObj F X₁ I₂ I₃).obj X₂).obj X₃ x = ((F.obj (X₁ x.1)).obj (X₂ x.2.1)).obj (X₃ x.2.2)
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>C₃ : Type u_3<VAR>C₄ : Type u_4<VAR>CategoryTheory.Category.{u_10, u_1} C₁<VAR>CategoryTheory.Category.{u_11, u_2} C₂<VAR>CategoryTheory.Category.{u_12, u_3} C₃<VAR>CategoryTheory.Category.{u_13, u_4} C₄<VAR>F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₄))<VAR>I₁ : Type u_7<VAR>X₁ : CategoryTheory.GradedObject I₁ C₁<VAR>I₂ : Type u_8<VAR>I₃ : Type u_9<VAR>X₂ : CategoryTheory.GradedObject I₂ C₂<VAR>X₃ Y₃ : CategoryTheory.GradedObject I₃ C₃<VAR>φ : X₃ ⟶ Y₃<VAR>x : I₁ × I₂ × I₃<GOAL>((CategoryTheory.GradedObject.mapTrifunctorObj F X₁ I₂ I₃).obj X₂).map φ x = ((F.obj (X₁ x.1)).obj (X₂ x.2.1)).map (φ x.2.2)
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>C₃ : Type u_3<VAR>C₄ : Type u_4<VAR>CategoryTheory.Category.{u_10, u_1} C₁<VAR>CategoryTheory.Category.{u_11, u_2} C₂<VAR>CategoryTheory.Category.{u_12, u_3} C₃<VAR>CategoryTheory.Category.{u_13, u_4} C₄<VAR>F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₄))<VAR>I₁ : Type u_7<VAR>I₂ : Type u_8<VAR>I₃ : Type u_9<VAR>X₁ Y₁ : CategoryTheory.GradedObject I₁ C₁<VAR>φ : X₁ ⟶ Y₁<VAR>X₂ : CategoryTheory.GradedObject I₂ C₂<VAR>X₃ : CategoryTheory.GradedObject I₃ C₃<VAR>x : I₁ × I₂ × I₃<GOAL>(((CategoryTheory.GradedObject.mapTrifunctor F I₁ I₂ I₃).map φ).app X₂).app X₃ x = ((F.map (φ x.1)).app (X₂ x.2.1)).app (X₃ x.2.2)
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>C₃ : Type u_3<VAR>C₄ : Type u_4<VAR>CategoryTheory.Category.{u_10, u_1} C₁<VAR>CategoryTheory.Category.{u_11, u_2} C₂<VAR>CategoryTheory.Category.{u_12, u_3} C₃<VAR>CategoryTheory.Category.{u_13, u_4} C₄<VAR>F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₄))<VAR>I₁ : Type u_7<VAR>I₂ : Type u_8<VAR>I₃ : Type u_9<VAR>X₁ : CategoryTheory.GradedObject I₁ C₁<GOAL>(CategoryTheory.GradedObject.mapTrifunctor F I₁ I₂ I₃).obj X₁ = CategoryTheory.GradedObject.mapTrifunctorObj F X₁ I₂ I₃
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>C₃ : Type u_3<VAR>C₄ : Type u_4<VAR>CategoryTheory.Category.{u_10, u_1} C₁<VAR>CategoryTheory.Category.{u_11, u_2} C₂<VAR>CategoryTheory.Category.{u_12, u_3} C₃<VAR>CategoryTheory.Category.{u_13, u_4} C₄<VAR>F F' : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₄))<VAR>α : F ⟶ F'<VAR>I₁ : Type u_7<VAR>I₂ : Type u_8<VAR>I₃ : Type u_9<VAR>X₁ : CategoryTheory.GradedObject I₁ C₁<VAR>X₂ : CategoryTheory.GradedObject I₂ C₂<VAR>X₃ : CategoryTheory.GradedObject I₃ C₃<VAR>i : I₁ × I₂ × I₃<GOAL>(((CategoryTheory.GradedObject.mapTrifunctorMapNatTrans α I₁ I₂ I₃).app X₁).app X₂).app X₃ i = ((α.app (X₁ i.1)).app (X₂ i.2.1)).app (X₃ i.2.2)
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>C₃ : Type u_3<VAR>C₄ : Type u_4<VAR>CategoryTheory.Category.{u_10, u_1} C₁<VAR>CategoryTheory.Category.{u_11, u_2} C₂<VAR>CategoryTheory.Category.{u_12, u_3} C₃<VAR>CategoryTheory.Category.{u_13, u_4} C₄<VAR>F F' : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₄))<VAR>e : F ≅ F'<VAR>I₁ : Type u_7<VAR>I₂ : Type u_8<VAR>I₃ : Type u_9<GOAL>(CategoryTheory.GradedObject.mapTrifunctorMapIso e I₁ I₂ I₃).hom = CategoryTheory.GradedObject.mapTrifunctorMapNatTrans e.hom I₁ I₂ I₃
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>C₃ : Type u_3<VAR>C₄ : Type u_4<VAR>CategoryTheory.Category.{u_10, u_1} C₁<VAR>CategoryTheory.Category.{u_11, u_2} C₂<VAR>CategoryTheory.Category.{u_12, u_3} C₃<VAR>CategoryTheory.Category.{u_13, u_4} C₄<VAR>F F' : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₄))<VAR>e : F ≅ F'<VAR>I₁ : Type u_7<VAR>I₂ : Type u_8<VAR>I₃ : Type u_9<GOAL>(CategoryTheory.GradedObject.mapTrifunctorMapIso e I₁ I₂ I₃).inv = CategoryTheory.GradedObject.mapTrifunctorMapNatTrans e.inv I₁ I₂ I₃
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>C₃ : Type u_3<VAR>C₄ : Type u_4<VAR>CategoryTheory.Category.{u_11, u_1} C₁<VAR>CategoryTheory.Category.{u_12, u_2} C₂<VAR>CategoryTheory.Category.{u_13, u_3} C₃<VAR>CategoryTheory.Category.{u_14, u_4} C₄<VAR>F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₄))<VAR>I₁ : Type u_7<VAR>I₂ : Type u_8<VAR>I₃ : Type u_9<VAR>J : Type u_10<VAR>p : I₁ × I₂ × I₃ → J<VAR>X₁ Y₁ : CategoryTheory.GradedObject I₁ C₁<VAR>f₁ : X₁ ⟶ Y₁<VAR>X₂ Y₂ : CategoryTheory.GradedObject I₂ C₂<VAR>f₂ : X₂ ⟶ Y₂<VAR>X₃ Y₃ : CategoryTheory.GradedObject I₃ C₃<VAR>f₃ : X₃ ⟶ Y₃<VAR>((((CategoryTheory.GradedObject.mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap p<VAR>((((CategoryTheory.GradedObject.mapTrifunctor F I₁ I₂ I₃).obj Y₁).obj Y₂).obj Y₃).HasMap p<VAR>i₁ : I₁<VAR>i₂ : I₂<VAR>i₃ : I₃<VAR>j : J<VAR>h : p (i₁, i₂, i₃) = j<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.ιMapTrifunctorMapObj F p X₁ X₂ X₃ i₁ i₂ i₃ j h) (CategoryTheory.GradedObject.mapTrifunctorMapMap F p f₁ f₂ f₃ j) = CategoryTheory.CategoryStruct.comp (((F.map (f₁ i₁)).app (X₂ i₂)).app (X₃ i₃)) (CategoryTheory.CategoryStruct.comp (((F.obj (Y₁ i₁)).map (f₂ i₂)).app (X₃ i₃)) (CategoryTheory.CategoryStruct.comp (((F.obj (Y₁ i₁)).obj (Y₂ i₂)).map (f₃ i₃)) (CategoryTheory.GradedObject.ιMapTrifunctorMapObj F p Y₁ Y₂ Y₃ i₁ i₂ i₃ j h)))
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>C₃ : Type u_3<VAR>C₄ : Type u_4<VAR>CategoryTheory.Category.{u_14, u_1} C₁<VAR>CategoryTheory.Category.{u_13, u_2} C₂<VAR>CategoryTheory.Category.{u_12, u_3} C₃<VAR>CategoryTheory.Category.{u_11, u_4} C₄<VAR>F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₄))<VAR>I₁ : Type u_7<VAR>I₂ : Type u_8<VAR>I₃ : Type u_9<VAR>J : Type u_10<VAR>p : I₁ × I₂ × I₃ → J<VAR>X₁ : CategoryTheory.GradedObject I₁ C₁<VAR>X₂ : CategoryTheory.GradedObject I₂ C₂<VAR>X₃ : CategoryTheory.GradedObject I₃ C₃<VAR>Y : C₄<VAR>j : J<VAR>((((CategoryTheory.GradedObject.mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap p<VAR>φ φ' : CategoryTheory.GradedObject.mapTrifunctorMapObj F p X₁ X₂ X₃ j ⟶ Y<VAR>h : ∀ (i₁ : I₁) (i₂ : I₂) (i₃ : I₃) (h : p (i₁, i₂, i₃) = j), CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.ιMapTrifunctorMapObj F p X₁ X₂ X₃ i₁ i₂ i₃ j h) φ = CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.ιMapTrifunctorMapObj F p X₁ X₂ X₃ i₁ i₂ i₃ j h) φ'<GOAL>φ = φ'
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>C₃ : Type u_3<VAR>C₄ : Type u_4<VAR>CategoryTheory.Category.{u_11, u_1} C₁<VAR>CategoryTheory.Category.{u_12, u_2} C₂<VAR>CategoryTheory.Category.{u_13, u_3} C₃<VAR>CategoryTheory.Category.{u_14, u_4} C₄<VAR>F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₄))<VAR>I₁ : Type u_7<VAR>I₂ : Type u_8<VAR>I₃ : Type u_9<VAR>J : Type u_10<VAR>p : I₁ × I₂ × I₃ → J<VAR>X₁ : CategoryTheory.GradedObject I₁ C₁<VAR>∀ (X₂ : CategoryTheory.GradedObject I₂ C₂) (X₃ : CategoryTheory.GradedObject I₃ C₃), ((((CategoryTheory.GradedObject.mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap p<VAR>X₂ : CategoryTheory.GradedObject I₂ C₂<VAR>X₃ : CategoryTheory.GradedObject I₃ C₃<GOAL>((CategoryTheory.GradedObject.mapTrifunctorMapFunctorObj F p X₁).obj X₂).obj X₃ = CategoryTheory.GradedObject.mapTrifunctorMapObj F p X₁ X₂ X₃
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>C₃ : Type u_3<VAR>C₄ : Type u_4<VAR>CategoryTheory.Category.{u_11, u_1} C₁<VAR>CategoryTheory.Category.{u_12, u_2} C₂<VAR>CategoryTheory.Category.{u_13, u_3} C₃<VAR>CategoryTheory.Category.{u_14, u_4} C₄<VAR>F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₄))<VAR>I₁ : Type u_7<VAR>I₂ : Type u_8<VAR>I₃ : Type u_9<VAR>J : Type u_10<VAR>p : I₁ × I₂ × I₃ → J<VAR>X₁ : CategoryTheory.GradedObject I₁ C₁<VAR>∀ (X₂ : CategoryTheory.GradedObject I₂ C₂) (X₃ : CategoryTheory.GradedObject I₃ C₃), ((((CategoryTheory.GradedObject.mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap p<VAR>X₂ : CategoryTheory.GradedObject I₂ C₂<VAR>X₃ Y₃ : CategoryTheory.GradedObject I₃ C₃<VAR>φ : X₃ ⟶ Y₃<VAR>i : J<GOAL>((CategoryTheory.GradedObject.mapTrifunctorMapFunctorObj F p X₁).obj X₂).map φ i = CategoryTheory.GradedObject.mapTrifunctorMapMap F p (CategoryTheory.CategoryStruct.id X₁) (CategoryTheory.CategoryStruct.id X₂) φ i
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>C₃ : Type u_3<VAR>C₄ : Type u_4<VAR>CategoryTheory.Category.{u_11, u_1} C₁<VAR>CategoryTheory.Category.{u_12, u_2} C₂<VAR>CategoryTheory.Category.{u_13, u_3} C₃<VAR>CategoryTheory.Category.{u_14, u_4} C₄<VAR>F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₄))<VAR>I₁ : Type u_7<VAR>I₂ : Type u_8<VAR>I₃ : Type u_9<VAR>J : Type u_10<VAR>p : I₁ × I₂ × I₃ → J<VAR>X₁ : CategoryTheory.GradedObject I₁ C₁<VAR>∀ (X₂ : CategoryTheory.GradedObject I₂ C₂) (X₃ : CategoryTheory.GradedObject I₃ C₃), ((((CategoryTheory.GradedObject.mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap p<VAR>X₂ Y₂ : CategoryTheory.GradedObject I₂ C₂<VAR>φ : X₂ ⟶ Y₂<VAR>X₃ : CategoryTheory.GradedObject I₃ C₃<VAR>i : J<GOAL>((CategoryTheory.GradedObject.mapTrifunctorMapFunctorObj F p X₁).map φ).app X₃ i = CategoryTheory.GradedObject.mapTrifunctorMapMap F p (CategoryTheory.CategoryStruct.id X₁) φ (CategoryTheory.CategoryStruct.id X₃) i
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>C₃ : Type u_3<VAR>C₄ : Type u_4<VAR>CategoryTheory.Category.{u_11, u_1} C₁<VAR>CategoryTheory.Category.{u_12, u_2} C₂<VAR>CategoryTheory.Category.{u_13, u_3} C₃<VAR>CategoryTheory.Category.{u_14, u_4} C₄<VAR>F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₄))<VAR>I₁ : Type u_7<VAR>I₂ : Type u_8<VAR>I₃ : Type u_9<VAR>J : Type u_10<VAR>p : I₁ × I₂ × I₃ → J<VAR>∀ (X₁ : CategoryTheory.GradedObject I₁ C₁) (X₂ : CategoryTheory.GradedObject I₂ C₂) (X₃ : CategoryTheory.GradedObject I₃ C₃), ((((CategoryTheory.GradedObject.mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap p<VAR>X₁ : CategoryTheory.GradedObject I₁ C₁<GOAL>(CategoryTheory.GradedObject.mapTrifunctorMap F p).obj X₁ = CategoryTheory.GradedObject.mapTrifunctorMapFunctorObj F p X₁
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>C₃ : Type u_3<VAR>C₄ : Type u_4<VAR>CategoryTheory.Category.{u_11, u_1} C₁<VAR>CategoryTheory.Category.{u_12, u_2} C₂<VAR>CategoryTheory.Category.{u_13, u_3} C₃<VAR>CategoryTheory.Category.{u_14, u_4} C₄<VAR>F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₄))<VAR>I₁ : Type u_7<VAR>I₂ : Type u_8<VAR>I₃ : Type u_9<VAR>J : Type u_10<VAR>p : I₁ × I₂ × I₃ → J<VAR>∀ (X₁ : CategoryTheory.GradedObject I₁ C₁) (X₂ : CategoryTheory.GradedObject I₂ C₂) (X₃ : CategoryTheory.GradedObject I₃ C₃), ((((CategoryTheory.GradedObject.mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap p<VAR>X₁ Y₁ : CategoryTheory.GradedObject I₁ C₁<VAR>φ : X₁ ⟶ Y₁<VAR>X₂ : CategoryTheory.GradedObject I₂ C₂<VAR>X₃ : CategoryTheory.GradedObject I₃ C₃<VAR>i : J<GOAL>(((CategoryTheory.GradedObject.mapTrifunctorMap F p).map φ).app X₂).app X₃ i = CategoryTheory.GradedObject.mapTrifunctorMapMap F p φ (CategoryTheory.CategoryStruct.id X₂) (CategoryTheory.CategoryStruct.id X₃) i
<VAR>I₁ : Type u_7<VAR>I₂ : Type u_8<VAR>I₃ : Type u_9<VAR>J : Type u_10<VAR>r : I₁ × I₂ × I₃ → J<VAR>self : CategoryTheory.GradedObject.BifunctorComp₁₂IndexData r<VAR>i : I₁ × I₂ × I₃<GOAL>self.q (self.p (i.1, i.2.1), i.2.2) = r i
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>C₃ : Type u_3<VAR>C₄ : Type u_4<VAR>C₁₂ : Type u_5<VAR>CategoryTheory.Category.{u_16, u_1} C₁<VAR>CategoryTheory.Category.{u_15, u_2} C₂<VAR>CategoryTheory.Category.{u_13, u_3} C₃<VAR>CategoryTheory.Category.{u_12, u_4} C₄<VAR>CategoryTheory.Category.{u_14, u_5} C₁₂<VAR>F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)<VAR>G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)<VAR>I₁ : Type u_7<VAR>I₂ : Type u_8<VAR>I₃ : Type u_9<VAR>J : Type u_10<VAR>r : I₁ × I₂ × I₃ → J<VAR>ρ₁₂ : CategoryTheory.GradedObject.BifunctorComp₁₂IndexData r<VAR>X₁ : CategoryTheory.GradedObject I₁ C₁<VAR>X₂ : CategoryTheory.GradedObject I₂ C₂<VAR>X₃ : CategoryTheory.GradedObject I₃ C₃<VAR>(((CategoryTheory.GradedObject.mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).HasMap ρ₁₂.p<VAR>(((CategoryTheory.GradedObject.mapBifunctor G ρ₁₂.I₁₂ I₃).obj (CategoryTheory.GradedObject.mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj X₃).HasMap ρ₁₂.q<VAR>i₁ : I₁<VAR>i₂ : I₂<VAR>i₃ : I₃<VAR>j : J<VAR>h : r (i₁, i₂, i₃) = j<VAR>i₁₂ : ρ₁₂.I₁₂<VAR>h₁₂ : ρ₁₂.p (i₁, i₂) = i₁₂<GOAL>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 ⋯)
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>C₃ : Type u_3<VAR>C₄ : Type u_4<VAR>C₁₂ : Type u_5<VAR>CategoryTheory.Category.{u_14, u_1} C₁<VAR>CategoryTheory.Category.{u_13, u_2} C₂<VAR>CategoryTheory.Category.{u_12, u_3} C₃<VAR>CategoryTheory.Category.{u_11, u_4} C₄<VAR>CategoryTheory.Category.{u_15, u_5} C₁₂<VAR>F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)<VAR>G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)<VAR>I₁ : Type u_7<VAR>I₂ : Type u_8<VAR>I₃ : Type u_9<VAR>J : Type u_10<VAR>r : I₁ × I₂ × I₃ → J<VAR>ρ₁₂ : CategoryTheory.GradedObject.BifunctorComp₁₂IndexData r<VAR>X₁ : CategoryTheory.GradedObject I₁ C₁<VAR>X₂ : CategoryTheory.GradedObject I₂ C₂<VAR>X₃ : CategoryTheory.GradedObject I₃ C₃<VAR>(((CategoryTheory.GradedObject.mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).HasMap ρ₁₂.p<VAR>(((CategoryTheory.GradedObject.mapBifunctor G ρ₁₂.I₁₂ I₃).obj (CategoryTheory.GradedObject.mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj X₃).HasMap ρ₁₂.q<VAR>H : CategoryTheory.GradedObject.HasGoodTrifunctor₁₂Obj F₁₂ G ρ₁₂ X₁ X₂ X₃<GOAL>((((CategoryTheory.GradedObject.mapTrifunctor (CategoryTheory.bifunctorComp₁₂ F₁₂ G) I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap r
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>C₃ : Type u_3<VAR>C₄ : Type u_4<VAR>C₁₂ : Type u_5<VAR>CategoryTheory.Category.{u_14, u_1} C₁<VAR>CategoryTheory.Category.{u_13, u_2} C₂<VAR>CategoryTheory.Category.{u_12, u_3} C₃<VAR>CategoryTheory.Category.{u_11, u_4} C₄<VAR>CategoryTheory.Category.{u_15, u_5} C₁₂<VAR>F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)<VAR>G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)<VAR>I₁ : Type u_7<VAR>I₂ : Type u_8<VAR>I₃ : Type u_9<VAR>J : Type u_10<VAR>r : I₁ × I₂ × I₃ → J<VAR>ρ₁₂ : CategoryTheory.GradedObject.BifunctorComp₁₂IndexData r<VAR>X₁ : CategoryTheory.GradedObject I₁ C₁<VAR>X₂ : CategoryTheory.GradedObject I₂ C₂<VAR>X₃ : CategoryTheory.GradedObject I₃ C₃<VAR>(((CategoryTheory.GradedObject.mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).HasMap ρ₁₂.p<VAR>(((CategoryTheory.GradedObject.mapBifunctor G ρ₁₂.I₁₂ I₃).obj (CategoryTheory.GradedObject.mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj X₃).HasMap ρ₁₂.q<VAR>H : CategoryTheory.GradedObject.HasGoodTrifunctor₁₂Obj F₁₂ G ρ₁₂ X₁ X₂ X₃<VAR>((((CategoryTheory.GradedObject.mapTrifunctor (CategoryTheory.bifunctorComp₁₂ F₁₂ G) I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap r<VAR>i₁ : I₁<VAR>i₂ : I₂<VAR>i₃ : I₃<VAR>j : J<VAR>h : r (i₁, i₂, i₃) = j<GOAL>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
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>C₃ : Type u_3<VAR>C₄ : Type u_4<VAR>C₁₂ : Type u_5<VAR>CategoryTheory.Category.{u_15, u_1} C₁<VAR>CategoryTheory.Category.{u_14, u_2} C₂<VAR>CategoryTheory.Category.{u_12, u_3} C₃<VAR>CategoryTheory.Category.{u_11, u_4} C₄<VAR>CategoryTheory.Category.{u_13, u_5} C₁₂<VAR>F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)<VAR>G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)<VAR>I₁ : Type u_7<VAR>I₂ : Type u_8<VAR>I₃ : Type u_9<VAR>J : Type u_10<VAR>r : I₁ × I₂ × I₃ → J<VAR>ρ₁₂ : CategoryTheory.GradedObject.BifunctorComp₁₂IndexData r<VAR>X₁ : CategoryTheory.GradedObject I₁ C₁<VAR>X₂ : CategoryTheory.GradedObject I₂ C₂<VAR>X₃ : CategoryTheory.GradedObject I₃ C₃<VAR>(((CategoryTheory.GradedObject.mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).HasMap ρ₁₂.p<VAR>(((CategoryTheory.GradedObject.mapBifunctor G ρ₁₂.I₁₂ I₃).obj (CategoryTheory.GradedObject.mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj X₃).HasMap ρ₁₂.q<VAR>H : CategoryTheory.GradedObject.HasGoodTrifunctor₁₂Obj F₁₂ G ρ₁₂ X₁ X₂ X₃<VAR>((((CategoryTheory.GradedObject.mapTrifunctor (CategoryTheory.bifunctorComp₁₂ F₁₂ G) I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap r<VAR>i₁ : I₁<VAR>i₂ : I₂<VAR>i₃ : I₃<VAR>j : J<VAR>h : r (i₁, i₂, i₃) = j<GOAL>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