ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>C₃ : Type u_3<VAR>D : Type u_4<VAR>I₁ : Type u_5<VAR>I₂ : Type u_6<VAR>I₃ : Type u_7<VAR>J : Type u_8<VAR>inst✝¹⁵ : Category.{u_10, u_1} C₁<VAR>inst✝¹⁴ : Category.{u_12, u_2} C₂<VAR>inst✝¹³ : Category.{u_11, u_3} C₃<VAR>inst✝¹² : Category.{u_9, u_4} D<VAR>inst✝¹¹ : Zero I₂<VAR>inst✝¹⁰ : DecidableEq I₂<VAR>inst✝⁹ : HasInitial C₂<VAR>F₁ : C₁ ⥤ C₂ ⥤ C₁<VAR>F₂ : C₂ ⥤ C₃ ⥤ C₃<VAR>G : C₁ ⥤ C₃ ⥤ D<VAR>associator : bifunctorComp₁₂ F₁ G ≅ bifunctorComp₂₃ G F₂<VAR>X₂ : C₂<VAR>e₁ : F₁.flip.obj X₂ ≅ 𝟭 C₁<VAR>e₂ : F₂.obj X₂ ≅ 𝟭 C₃<VAR>inst✝⁸ : (X₁ : C₁) → PreservesColimit (Functor.empty C₂) (F₁.obj X₁)<VAR>inst✝⁷ : (X₃ : C₃) → PreservesColimit (Functor.empty C₂) (F₂.flip.obj X₃)<VAR>r : I₁ × I₂ × I₃ → J<VAR>π : I₁ × I₃ → J<VAR>τ : TriangleIndexData r π<VAR>X₁ : GradedObject I₁ C₁<VAR>X₃ : GradedObject I₃ C₃<VAR>inst✝⁶ : (((mapBifunctor F₁ I₁ I₂).obj X₁).obj ((single₀ I₂).obj X₂)).HasMap τ.p₁₂<VAR>inst✝⁵ : (((mapBifunctor G I₁ I₃).obj (mapBifunctorMapObj F₁ τ.p₁₂ X₁ ((single₀ I₂).obj X₂))).obj X₃).HasMap π<VAR>inst✝⁴ : (((mapBifunctor F₂ I₂ I₃).obj ((single₀ I₂).obj X₂)).obj X₃).HasMap τ.p₂₃<VAR>inst✝³ : (((mapBifunctor G I₁ I₃).obj X₁).obj (mapBifunctorMapObj F₂ τ.p₂₃ ((single₀ I₂).obj X₂) X₃)).HasMap π<VAR>inst✝² : HasGoodTrifunctor₁₂Obj F₁ G τ.ρ₁₂ X₁ ((single₀ I₂).obj X₂) X₃<VAR>inst✝¹ : HasGoodTrifunctor₂₃Obj G F₂ τ.ρ₂₃ X₁ ((single₀ I₂).obj X₂) X₃<VAR>inst✝ : (((mapBifunctor G I₁ I₃).obj X₁).obj X₃).HasMap π<VAR>triangle : ∀ (X₁ : C₁) (X₃ : C₃), ((associator.hom.app X₁).app X₂).app X₃ ≫ (G.obj X₁).map (e₂.hom.app X₃) = (G.map (e₁.hom.app X₁)).app X₃<VAR>j : J<VAR>i₁ : I₁<VAR>i₃ : I₃<VAR>hj : π (i₁, i₃) = j<GOAL>(G.map (e₁.inv.app (X₁ i₁))).app (X₃ i₃) ≫ (G.map ((F₁.obj (X₁ i₁)).map (singleObjApplyIso 0 X₂).inv)).app (X₃ i₃) ≫ (G.map (ιMapBifunctorMapObj F₁ τ.p₁₂ X₁ ((single₀ I₂).obj X₂) i₁ 0 i₁ ⋯)).app (X₃ i₃) ≫ ιMapBifunctorMapObj G π (mapBifunctorMapObj F₁ τ.p₁₂ X₁ ((single₀ I₂).obj X₂)) X₃ i₁ i₃ j hj ≫ (mapBifunctorAssociator associator τ.ρ₁₂ τ.ρ₂₃ X₁ ((single₀ I₂).obj X₂) X₃).hom j ≫ mapBifunctorMapMap G π (𝟙 X₁) (mapBifunctorLeftUnitor F₂ X₂ e₂ τ.p₂₃ ⋯ X₃).hom j = (G.map (e₁.inv.app (X₁ i₁))).app (X₃ i₃) ≫ (G.map ((F₁.obj (X₁ i₁)).map (singleObjApplyIso 0 X₂).inv)).app (X₃ i₃) ≫ (G.map (ιMapBifunctorMapObj F₁ τ.p₁₂ X₁ ((single₀ I₂).obj X₂) i₁ 0 i₁ ⋯)).app (X₃ i₃) ≫ (G.map ((mapBifunctorRightUnitor F₁ X₂ e₁ τ.p₁₂ ⋯ X₁).hom i₁)).app (X₃ i₃) ≫ ιMapBifunctorMapObj G π X₁ X₃ i₁ i₃ j hj
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>C₃ : Type u_3<VAR>D : Type u_4<VAR>I₁ : Type u_5<VAR>I₂ : Type u_6<VAR>I₃ : Type u_7<VAR>J : Type u_8<VAR>inst✝¹⁵ : Category.{u_10, u_1} C₁<VAR>inst✝¹⁴ : Category.{u_12, u_2} C₂<VAR>inst✝¹³ : Category.{u_11, u_3} C₃<VAR>inst✝¹² : Category.{u_9, u_4} D<VAR>inst✝¹¹ : Zero I₂<VAR>inst✝¹⁰ : DecidableEq I₂<VAR>inst✝⁹ : HasInitial C₂<VAR>F₁ : C₁ ⥤ C₂ ⥤ C₁<VAR>F₂ : C₂ ⥤ C₃ ⥤ C₃<VAR>G : C₁ ⥤ C₃ ⥤ D<VAR>associator : bifunctorComp₁₂ F₁ G ≅ bifunctorComp₂₃ G F₂<VAR>X₂ : C₂<VAR>e₁ : F₁.flip.obj X₂ ≅ 𝟭 C₁<VAR>e₂ : F₂.obj X₂ ≅ 𝟭 C₃<VAR>inst✝⁸ : (X₁ : C₁) → PreservesColimit (Functor.empty C₂) (F₁.obj X₁)<VAR>inst✝⁷ : (X₃ : C₃) → PreservesColimit (Functor.empty C₂) (F₂.flip.obj X₃)<VAR>r : I₁ × I₂ × I₃ → J<VAR>π : I₁ × I₃ → J<VAR>τ : TriangleIndexData r π<VAR>X₁ : GradedObject I₁ C₁<VAR>X₃ : GradedObject I₃ C₃<VAR>inst✝⁶ : (((mapBifunctor F₁ I₁ I₂).obj X₁).obj ((single₀ I₂).obj X₂)).HasMap τ.p₁₂<VAR>inst✝⁵ : (((mapBifunctor G I₁ I₃).obj (mapBifunctorMapObj F₁ τ.p₁₂ X₁ ((single₀ I₂).obj X₂))).obj X₃).HasMap π<VAR>inst✝⁴ : (((mapBifunctor F₂ I₂ I₃).obj ((single₀ I₂).obj X₂)).obj X₃).HasMap τ.p₂₃<VAR>inst✝³ : (((mapBifunctor G I₁ I₃).obj X₁).obj (mapBifunctorMapObj F₂ τ.p₂₃ ((single₀ I₂).obj X₂) X₃)).HasMap π<VAR>inst✝² : HasGoodTrifunctor₁₂Obj F₁ G τ.ρ₁₂ X₁ ((single₀ I₂).obj X₂) X₃<VAR>inst✝¹ : HasGoodTrifunctor₂₃Obj G F₂ τ.ρ₂₃ X₁ ((single₀ I₂).obj X₂) X₃<VAR>inst✝ : (((mapBifunctor G I₁ I₃).obj X₁).obj X₃).HasMap π<VAR>triangle : ∀ (X₁ : C₁) (X₃ : C₃), ((associator.hom.app X₁).app X₂).app X₃ ≫ (G.obj X₁).map (e₂.hom.app X₃) = (G.map (e₁.hom.app X₁)).app X₃<VAR>j : J<VAR>i₁ : I₁<VAR>i₃ : I₃<VAR>hj : π (i₁, i₃) = j<GOAL>(G.map (ιMapBifunctorMapObj F₁ τ.p₁₂ X₁ ((single₀ I₂).obj X₂) i₁ 0 i₁ ⋯)).app (X₃ i₃) ≫ ιMapBifunctorMapObj G π (mapBifunctorMapObj F₁ τ.p₁₂ X₁ ((single₀ I₂).obj X₂)) X₃ i₁ i₃ j hj ≫ (mapBifunctorAssociator associator τ.ρ₁₂ τ.ρ₂₃ X₁ ((single₀ I₂).obj X₂) X₃).hom j ≫ mapBifunctorMapMap G π (𝟙 X₁) (mapBifunctorLeftUnitor F₂ X₂ e₂ τ.p₂₃ ⋯ X₃).hom j = (G.map (ιMapBifunctorMapObj F₁ τ.p₁₂ X₁ ((single₀ I₂).obj X₂) i₁ 0 i₁ ⋯)).app (X₃ i₃) ≫ (G.map ((mapBifunctorRightUnitor F₁ X₂ e₁ τ.p₁₂ ⋯ X₁).hom i₁)).app (X₃ i₃) ≫ ιMapBifunctorMapObj G π X₁ X₃ i₁ i₃ j hj
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>C₃ : Type u_3<VAR>D : Type u_4<VAR>I₁ : Type u_5<VAR>I₂ : Type u_6<VAR>I₃ : Type u_7<VAR>J : Type u_8<VAR>inst✝¹⁵ : Category.{u_10, u_1} C₁<VAR>inst✝¹⁴ : Category.{u_12, u_2} C₂<VAR>inst✝¹³ : Category.{u_11, u_3} C₃<VAR>inst✝¹² : Category.{u_9, u_4} D<VAR>inst✝¹¹ : Zero I₂<VAR>inst✝¹⁰ : DecidableEq I₂<VAR>inst✝⁹ : HasInitial C₂<VAR>F₁ : C₁ ⥤ C₂ ⥤ C₁<VAR>F₂ : C₂ ⥤ C₃ ⥤ C₃<VAR>G : C₁ ⥤ C₃ ⥤ D<VAR>associator : bifunctorComp₁₂ F₁ G ≅ bifunctorComp₂₃ G F₂<VAR>X₂ : C₂<VAR>e₁ : F₁.flip.obj X₂ ≅ 𝟭 C₁<VAR>e₂ : F₂.obj X₂ ≅ 𝟭 C₃<VAR>inst✝⁸ : (X₁ : C₁) → PreservesColimit (Functor.empty C₂) (F₁.obj X₁)<VAR>inst✝⁷ : (X₃ : C₃) → PreservesColimit (Functor.empty C₂) (F₂.flip.obj X₃)<VAR>r : I₁ × I₂ × I₃ → J<VAR>π : I₁ × I₃ → J<VAR>τ : TriangleIndexData r π<VAR>X₁ : GradedObject I₁ C₁<VAR>X₃ : GradedObject I₃ C₃<VAR>inst✝⁶ : (((mapBifunctor F₁ I₁ I₂).obj X₁).obj ((single₀ I₂).obj X₂)).HasMap τ.p₁₂<VAR>inst✝⁵ : (((mapBifunctor G I₁ I₃).obj (mapBifunctorMapObj F₁ τ.p₁₂ X₁ ((single₀ I₂).obj X₂))).obj X₃).HasMap π<VAR>inst✝⁴ : (((mapBifunctor F₂ I₂ I₃).obj ((single₀ I₂).obj X₂)).obj X₃).HasMap τ.p₂₃<VAR>inst✝³ : (((mapBifunctor G I₁ I₃).obj X₁).obj (mapBifunctorMapObj F₂ τ.p₂₃ ((single₀ I₂).obj X₂) X₃)).HasMap π<VAR>inst✝² : HasGoodTrifunctor₁₂Obj F₁ G τ.ρ₁₂ X₁ ((single₀ I₂).obj X₂) X₃<VAR>inst✝¹ : HasGoodTrifunctor₂₃Obj G F₂ τ.ρ₂₃ X₁ ((single₀ I₂).obj X₂) X₃<VAR>inst✝ : (((mapBifunctor G I₁ I₃).obj X₁).obj X₃).HasMap π<VAR>triangle : ∀ (X₁ : C₁) (X₃ : C₃), ((associator.hom.app X₁).app X₂).app X₃ ≫ (G.obj X₁).map (e₂.hom.app X₃) = (G.map (e₁.hom.app X₁)).app X₃<VAR>j : J<VAR>i₁ : I₁<VAR>i₃ : I₃<VAR>hj : π (i₁, i₃) = j<GOAL>((associator.hom.app (X₁ i₁)).app ((single₀ I₂).obj X₂ 0)).app (X₃ i₃) ≫ (G.obj (X₁ i₁)).map (ιMapBifunctorMapObj F₂ τ.ρ₂₃.p ((single₀ I₂).obj X₂) X₃ 0 i₃ i₃ ⋯) ≫ (G.map (𝟙 X₁ i₁)).app (mapBifunctorMapObj F₂ τ.ρ₂₃.p ((single₀ I₂).obj X₂) X₃ i₃) ≫ (G.obj (X₁ i₁)).map ((mapBifunctorLeftUnitor F₂ X₂ e₂ τ.p₂₃ ⋯ X₃).hom i₃) ≫ ιMapBifunctorMapObj G τ.ρ₂₃.q X₁ X₃ i₁ i₃ j ⋯ = (G.map (ιMapBifunctorMapObj F₁ τ.p₁₂ X₁ ((single₀ I₂).obj X₂) i₁ 0 i₁ ⋯)).app (X₃ i₃) ≫ (G.map ((mapBifunctorRightUnitor F₁ X₂ e₁ τ.p₁₂ ⋯ X₁).hom i₁)).app (X₃ i₃) ≫ ιMapBifunctorMapObj G π X₁ X₃ i₁ i₃ j hj
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>C₃ : Type u_3<VAR>D : Type u_4<VAR>I₁ : Type u_5<VAR>I₂ : Type u_6<VAR>I₃ : Type u_7<VAR>J : Type u_8<VAR>inst✝¹⁵ : Category.{u_10, u_1} C₁<VAR>inst✝¹⁴ : Category.{u_12, u_2} C₂<VAR>inst✝¹³ : Category.{u_11, u_3} C₃<VAR>inst✝¹² : Category.{u_9, u_4} D<VAR>inst✝¹¹ : Zero I₂<VAR>inst✝¹⁰ : DecidableEq I₂<VAR>inst✝⁹ : HasInitial C₂<VAR>F₁ : C₁ ⥤ C₂ ⥤ C₁<VAR>F₂ : C₂ ⥤ C₃ ⥤ C₃<VAR>G : C₁ ⥤ C₃ ⥤ D<VAR>associator : bifunctorComp₁₂ F₁ G ≅ bifunctorComp₂₃ G F₂<VAR>X₂ : C₂<VAR>e₁ : F₁.flip.obj X₂ ≅ 𝟭 C₁<VAR>e₂ : F₂.obj X₂ ≅ 𝟭 C₃<VAR>inst✝⁸ : (X₁ : C₁) → PreservesColimit (Functor.empty C₂) (F₁.obj X₁)<VAR>inst✝⁷ : (X₃ : C₃) → PreservesColimit (Functor.empty C₂) (F₂.flip.obj X₃)<VAR>r : I₁ × I₂ × I₃ → J<VAR>π : I₁ × I₃ → J<VAR>τ : TriangleIndexData r π<VAR>X₁ : GradedObject I₁ C₁<VAR>X₃ : GradedObject I₃ C₃<VAR>inst✝⁶ : (((mapBifunctor F₁ I₁ I₂).obj X₁).obj ((single₀ I₂).obj X₂)).HasMap τ.p₁₂<VAR>inst✝⁵ : (((mapBifunctor G I₁ I₃).obj (mapBifunctorMapObj F₁ τ.p₁₂ X₁ ((single₀ I₂).obj X₂))).obj X₃).HasMap π<VAR>inst✝⁴ : (((mapBifunctor F₂ I₂ I₃).obj ((single₀ I₂).obj X₂)).obj X₃).HasMap τ.p₂₃<VAR>inst✝³ : (((mapBifunctor G I₁ I₃).obj X₁).obj (mapBifunctorMapObj F₂ τ.p₂₃ ((single₀ I₂).obj X₂) X₃)).HasMap π<VAR>inst✝² : HasGoodTrifunctor₁₂Obj F₁ G τ.ρ₁₂ X₁ ((single₀ I₂).obj X₂) X₃<VAR>inst✝¹ : HasGoodTrifunctor₂₃Obj G F₂ τ.ρ₂₃ X₁ ((single₀ I₂).obj X₂) X₃<VAR>inst✝ : (((mapBifunctor G I₁ I₃).obj X₁).obj X₃).HasMap π<VAR>triangle : ∀ (X₁ : C₁) (X₃ : C₃), ((associator.hom.app X₁).app X₂).app X₃ ≫ (G.obj X₁).map (e₂.hom.app X₃) = (G.map (e₁.hom.app X₁)).app X₃<VAR>j : J<VAR>i₁ : I₁<VAR>i₃ : I₃<VAR>hj : π (i₁, i₃) = j<GOAL>((associator.hom.app (X₁ i₁)).app ((single₀ I₂).obj X₂ 0)).app (X₃ i₃) ≫ (G.obj (X₁ i₁)).map (ιMapBifunctorMapObj F₂ τ.p₂₃ ((single₀ I₂).obj X₂) X₃ 0 i₃ i₃ ⋯) ≫ (G.map (𝟙 (X₁ i₁))).app ((((mapBifunctor F₂ I₂ I₃).obj ((single₀ I₂).obj X₂)).obj X₃).mapObj τ.p₂₃ i₃) ≫ (G.obj (X₁ i₁)).map ((mapBifunctorLeftUnitor F₂ X₂ e₂ τ.p₂₃ ⋯ X₃).hom i₃) ≫ ιMapBifunctorMapObj G π X₁ X₃ i₁ i₃ j ⋯ = (G.map (ιMapBifunctorMapObj F₁ τ.p₁₂ X₁ ((single₀ I₂).obj X₂) i₁ 0 i₁ ⋯)).app (X₃ i₃) ≫ (G.map ((mapBifunctorRightUnitor F₁ X₂ e₁ τ.p₁₂ ⋯ X₁).hom i₁)).app (X₃ i₃) ≫ ιMapBifunctorMapObj G π X₁ X₃ i₁ i₃ j hj
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>C₃ : Type u_3<VAR>D : Type u_4<VAR>I₁ : Type u_5<VAR>I₂ : Type u_6<VAR>I₃ : Type u_7<VAR>J : Type u_8<VAR>inst✝¹⁵ : Category.{u_10, u_1} C₁<VAR>inst✝¹⁴ : Category.{u_12, u_2} C₂<VAR>inst✝¹³ : Category.{u_11, u_3} C₃<VAR>inst✝¹² : Category.{u_9, u_4} D<VAR>inst✝¹¹ : Zero I₂<VAR>inst✝¹⁰ : DecidableEq I₂<VAR>inst✝⁹ : HasInitial C₂<VAR>F₁ : C₁ ⥤ C₂ ⥤ C₁<VAR>F₂ : C₂ ⥤ C₃ ⥤ C₃<VAR>G : C₁ ⥤ C₃ ⥤ D<VAR>associator : bifunctorComp₁₂ F₁ G ≅ bifunctorComp₂₃ G F₂<VAR>X₂ : C₂<VAR>e₁ : F₁.flip.obj X₂ ≅ 𝟭 C₁<VAR>e₂ : F₂.obj X₂ ≅ 𝟭 C₃<VAR>inst✝⁸ : (X₁ : C₁) → PreservesColimit (Functor.empty C₂) (F₁.obj X₁)<VAR>inst✝⁷ : (X₃ : C₃) → PreservesColimit (Functor.empty C₂) (F₂.flip.obj X₃)<VAR>r : I₁ × I₂ × I₃ → J<VAR>π : I₁ × I₃ → J<VAR>τ : TriangleIndexData r π<VAR>X₁ : GradedObject I₁ C₁<VAR>X₃ : GradedObject I₃ C₃<VAR>inst✝⁶ : (((mapBifunctor F₁ I₁ I₂).obj X₁).obj ((single₀ I₂).obj X₂)).HasMap τ.p₁₂<VAR>inst✝⁵ : (((mapBifunctor G I₁ I₃).obj (mapBifunctorMapObj F₁ τ.p₁₂ X₁ ((single₀ I₂).obj X₂))).obj X₃).HasMap π<VAR>inst✝⁴ : (((mapBifunctor F₂ I₂ I₃).obj ((single₀ I₂).obj X₂)).obj X₃).HasMap τ.p₂₃<VAR>inst✝³ : (((mapBifunctor G I₁ I₃).obj X₁).obj (mapBifunctorMapObj F₂ τ.p₂₃ ((single₀ I₂).obj X₂) X₃)).HasMap π<VAR>inst✝² : HasGoodTrifunctor₁₂Obj F₁ G τ.ρ₁₂ X₁ ((single₀ I₂).obj X₂) X₃<VAR>inst✝¹ : HasGoodTrifunctor₂₃Obj G F₂ τ.ρ₂₃ X₁ ((single₀ I₂).obj X₂) X₃<VAR>inst✝ : (((mapBifunctor G I₁ I₃).obj X₁).obj X₃).HasMap π<VAR>triangle : ∀ (X₁ : C₁) (X₃ : C₃), ((associator.hom.app X₁).app X₂).app X₃ ≫ (G.obj X₁).map (e₂.hom.app X₃) = (G.map (e₁.hom.app X₁)).app X₃<VAR>j : J<VAR>i₁ : I₁<VAR>i₃ : I₃<VAR>hj : π (i₁, i₃) = j<GOAL>((associator.hom.app (X₁ i₁)).app ((single₀ I₂).obj X₂ 0)).app (X₃ i₃) ≫ (G.obj (X₁ i₁)).map ((F₂.map (singleObjApplyIso 0 X₂).hom).app (X₃ i₃) ≫ e₂.hom.app (X₃ i₃)) ≫ ιMapBifunctorMapObj G π X₁ X₃ i₁ i₃ j ⋯ = (G.map ((F₁.obj (X₁ i₁)).map (singleObjApplyIso 0 X₂).hom ≫ e₁.hom.app (X₁ i₁))).app (X₃ i₃) ≫ ιMapBifunctorMapObj G π X₁ X₃ i₁ i₃ j hj
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>C₃ : Type u_3<VAR>D : Type u_4<VAR>I₁ : Type u_5<VAR>I₂ : Type u_6<VAR>I₃ : Type u_7<VAR>J : Type u_8<VAR>inst✝¹⁵ : Category.{u_10, u_1} C₁<VAR>inst✝¹⁴ : Category.{u_12, u_2} C₂<VAR>inst✝¹³ : Category.{u_11, u_3} C₃<VAR>inst✝¹² : Category.{u_9, u_4} D<VAR>inst✝¹¹ : Zero I₂<VAR>inst✝¹⁰ : DecidableEq I₂<VAR>inst✝⁹ : HasInitial C₂<VAR>F₁ : C₁ ⥤ C₂ ⥤ C₁<VAR>F₂ : C₂ ⥤ C₃ ⥤ C₃<VAR>G : C₁ ⥤ C₃ ⥤ D<VAR>associator : bifunctorComp₁₂ F₁ G ≅ bifunctorComp₂₃ G F₂<VAR>X₂ : C₂<VAR>e₁ : F₁.flip.obj X₂ ≅ 𝟭 C₁<VAR>e₂ : F₂.obj X₂ ≅ 𝟭 C₃<VAR>inst✝⁸ : (X₁ : C₁) → PreservesColimit (Functor.empty C₂) (F₁.obj X₁)<VAR>inst✝⁷ : (X₃ : C₃) → PreservesColimit (Functor.empty C₂) (F₂.flip.obj X₃)<VAR>r : I₁ × I₂ × I₃ → J<VAR>π : I₁ × I₃ → J<VAR>τ : TriangleIndexData r π<VAR>X₁ : GradedObject I₁ C₁<VAR>X₃ : GradedObject I₃ C₃<VAR>inst✝⁶ : (((mapBifunctor F₁ I₁ I₂).obj X₁).obj ((single₀ I₂).obj X₂)).HasMap τ.p₁₂<VAR>inst✝⁵ : (((mapBifunctor G I₁ I₃).obj (mapBifunctorMapObj F₁ τ.p₁₂ X₁ ((single₀ I₂).obj X₂))).obj X₃).HasMap π<VAR>inst✝⁴ : (((mapBifunctor F₂ I₂ I₃).obj ((single₀ I₂).obj X₂)).obj X₃).HasMap τ.p₂₃<VAR>inst✝³ : (((mapBifunctor G I₁ I₃).obj X₁).obj (mapBifunctorMapObj F₂ τ.p₂₃ ((single₀ I₂).obj X₂) X₃)).HasMap π<VAR>inst✝² : HasGoodTrifunctor₁₂Obj F₁ G τ.ρ₁₂ X₁ ((single₀ I₂).obj X₂) X₃<VAR>inst✝¹ : HasGoodTrifunctor₂₃Obj G F₂ τ.ρ₂₃ X₁ ((single₀ I₂).obj X₂) X₃<VAR>inst✝ : (((mapBifunctor G I₁ I₃).obj X₁).obj X₃).HasMap π<VAR>triangle : ∀ (X₁ : C₁) (X₃ : C₃), ((associator.hom.app X₁).app X₂).app X₃ ≫ (G.obj X₁).map (e₂.hom.app X₃) = (G.map (e₁.hom.app X₁)).app X₃<VAR>j : J<VAR>i₁ : I₁<VAR>i₃ : I₃<VAR>hj : π (i₁, i₃) = j<GOAL>((((associator.hom.app (X₁ i₁)).app ((single₀ I₂).obj X₂ 0)).app (X₃ i₃) ≫ (G.obj (X₁ i₁)).map ((F₂.map (singleObjApplyIso 0 X₂).hom).app (X₃ i₃))) ≫ (G.obj (X₁ i₁)).map (e₂.hom.app (X₃ i₃))) ≫ ιMapBifunctorMapObj G π X₁ X₃ i₁ i₃ j ⋯ = (((G.map ((F₁.obj (X₁ i₁)).map (singleObjApplyIso 0 X₂).hom)).app (X₃ i₃) ≫ ((associator.hom.app (X₁ i₁)).app X₂).app (X₃ i₃)) ≫ (G.obj (X₁ i₁)).map (e₂.hom.app (X₃ i₃))) ≫ ιMapBifunctorMapObj G π X₁ X₃ i₁ i₃ j hj
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>C₃ : Type u_3<VAR>D : Type u_4<VAR>I₁ : Type u_5<VAR>I₂ : Type u_6<VAR>I₃ : Type u_7<VAR>J : Type u_8<VAR>inst✝¹⁵ : Category.{u_10, u_1} C₁<VAR>inst✝¹⁴ : Category.{u_12, u_2} C₂<VAR>inst✝¹³ : Category.{u_11, u_3} C₃<VAR>inst✝¹² : Category.{u_9, u_4} D<VAR>inst✝¹¹ : Zero I₂<VAR>inst✝¹⁰ : DecidableEq I₂<VAR>inst✝⁹ : HasInitial C₂<VAR>F₁ : C₁ ⥤ C₂ ⥤ C₁<VAR>F₂ : C₂ ⥤ C₃ ⥤ C₃<VAR>G : C₁ ⥤ C₃ ⥤ D<VAR>associator : bifunctorComp₁₂ F₁ G ≅ bifunctorComp₂₃ G F₂<VAR>X₂ : C₂<VAR>e₁ : F₁.flip.obj X₂ ≅ 𝟭 C₁<VAR>e₂ : F₂.obj X₂ ≅ 𝟭 C₃<VAR>inst✝⁸ : (X₁ : C₁) → PreservesColimit (Functor.empty C₂) (F₁.obj X₁)<VAR>inst✝⁷ : (X₃ : C₃) → PreservesColimit (Functor.empty C₂) (F₂.flip.obj X₃)<VAR>r : I₁ × I₂ × I₃ → J<VAR>π : I₁ × I₃ → J<VAR>τ : TriangleIndexData r π<VAR>X₁ : GradedObject I₁ C₁<VAR>X₃ : GradedObject I₃ C₃<VAR>inst✝⁶ : (((mapBifunctor F₁ I₁ I₂).obj X₁).obj ((single₀ I₂).obj X₂)).HasMap τ.p₁₂<VAR>inst✝⁵ : (((mapBifunctor G I₁ I₃).obj (mapBifunctorMapObj F₁ τ.p₁₂ X₁ ((single₀ I₂).obj X₂))).obj X₃).HasMap π<VAR>inst✝⁴ : (((mapBifunctor F₂ I₂ I₃).obj ((single₀ I₂).obj X₂)).obj X₃).HasMap τ.p₂₃<VAR>inst✝³ : (((mapBifunctor G I₁ I₃).obj X₁).obj (mapBifunctorMapObj F₂ τ.p₂₃ ((single₀ I₂).obj X₂) X₃)).HasMap π<VAR>inst✝² : HasGoodTrifunctor₁₂Obj F₁ G τ.ρ₁₂ X₁ ((single₀ I₂).obj X₂) X₃<VAR>inst✝¹ : HasGoodTrifunctor₂₃Obj G F₂ τ.ρ₂₃ X₁ ((single₀ I₂).obj X₂) X₃<VAR>inst✝ : (((mapBifunctor G I₁ I₃).obj X₁).obj X₃).HasMap π<VAR>triangle : ∀ (X₁ : C₁) (X₃ : C₃), ((associator.hom.app X₁).app X₂).app X₃ ≫ (G.obj X₁).map (e₂.hom.app X₃) = (G.map (e₁.hom.app X₁)).app X₃<VAR>j : J<VAR>i₁ : I₁<VAR>i₃ : I₃<VAR>hj : π (i₁, i₃) = j<GOAL>(G.map ((F₁.obj (X₁ i₁)).map (singleObjApplyIso 0 X₂).hom)).app (X₃ i₃) ≫ ((associator.hom.app (X₁ i₁)).app X₂).app (X₃ i₃) = ((associator.hom.app (X₁ i₁)).app ((single₀ I₂).obj X₂ 0)).app (X₃ i₃) ≫ (G.obj (X₁ i₁)).map ((F₂.map (singleObjApplyIso 0 X₂).hom).app (X₃ i₃))
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹⁰ : CommSemiring R<VAR>inst✝⁹ : AddCommMonoid M<VAR>inst✝⁸ : Module R M<VAR>R₁ : Type u_3<VAR>M₁ : Type u_4<VAR>inst✝⁷ : CommRing R₁<VAR>inst✝⁶ : AddCommGroup M₁<VAR>inst✝⁵ : Module R₁ M₁<VAR>V : Type u_5<VAR>K : Type u_6<VAR>inst✝⁴ : Field K<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module K V<VAR>B✝ : BilinForm R M<VAR>B₁ : BilinForm R₁ M₁<VAR>M₂' : Type u_7<VAR>inst✝¹ : AddCommMonoid M₂'<VAR>inst✝ : Module R M₂'<VAR>B : BilinForm K V<VAR>W : Subspace K V<VAR>x : V<GOAL>x ∈ (range (domRestrict B W)).dualCoannihilator ↔ x ∈ B.orthogonal W
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹⁰ : CommSemiring R<VAR>inst✝⁹ : AddCommMonoid M<VAR>inst✝⁸ : Module R M<VAR>R₁ : Type u_3<VAR>M₁ : Type u_4<VAR>inst✝⁷ : CommRing R₁<VAR>inst✝⁶ : AddCommGroup M₁<VAR>inst✝⁵ : Module R₁ M₁<VAR>V : Type u_5<VAR>K : Type u_6<VAR>inst✝⁴ : Field K<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module K V<VAR>B✝ : BilinForm R M<VAR>B₁ : BilinForm R₁ M₁<VAR>M₂' : Type u_7<VAR>inst✝¹ : AddCommMonoid M₂'<VAR>inst✝ : Module R M₂'<VAR>B : BilinForm K V<VAR>W : Subspace K V<VAR>x : V<VAR>hx : x ∈ (range (domRestrict B W)).dualCoannihilator<GOAL>∀ n ∈ W, B.IsOrtho n x
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹⁰ : CommSemiring R<VAR>inst✝⁹ : AddCommMonoid M<VAR>inst✝⁸ : Module R M<VAR>R₁ : Type u_3<VAR>M₁ : Type u_4<VAR>inst✝⁷ : CommRing R₁<VAR>inst✝⁶ : AddCommGroup M₁<VAR>inst✝⁵ : Module R₁ M₁<VAR>V : Type u_5<VAR>K : Type u_6<VAR>inst✝⁴ : Field K<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module K V<VAR>B✝ : BilinForm R M<VAR>B₁ : BilinForm R₁ M₁<VAR>M₂' : Type u_7<VAR>inst✝¹ : AddCommMonoid M₂'<VAR>inst✝ : Module R M₂'<VAR>B : BilinForm K V<VAR>W : Subspace K V<VAR>x : V<VAR>hx : ∀ n ∈ W, B.IsOrtho n x<GOAL>x ∈ (range (domRestrict B W)).dualCoannihilator
<VAR>α : Type u_1<VAR>inst✝² : CanonicallyLinearOrderedAddCommMonoid α<VAR>inst✝¹ : Sub α<VAR>inst✝ : OrderedSub α<VAR>a b c d : α<GOAL>a - min a b = a - b
<VAR>α : Type u_1<VAR>inst✝² : CanonicallyLinearOrderedAddCommMonoid α<VAR>inst✝¹ : Sub α<VAR>inst✝ : OrderedSub α<VAR>a b c d : α<VAR>h : a ≤ b<GOAL>a - min a b = a - b
<VAR>α : Type u_1<VAR>inst✝² : CanonicallyLinearOrderedAddCommMonoid α<VAR>inst✝¹ : Sub α<VAR>inst✝ : OrderedSub α<VAR>a b c d : α<VAR>h : b ≤ a<GOAL>a - min a b = a - b
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>W : ℤ → R<VAR>f : R →+* S<VAR>b c d : R<GOAL>normEDS b c d 2 = b
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>M : Type u_4<VAR>inst✝⁸ : CommSemiring R<VAR>inst✝⁷ : CommSemiring A<VAR>inst✝⁶ : CommSemiring B<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : Algebra R A<VAR>inst✝³ : Algebra R B<VAR>inst✝² : Module A M<VAR>inst✝¹ : Module B M<VAR>inst✝ : Module R M<VAR>D D1 D2 : Derivation R A M<VAR>r : R<VAR>a b : A<VAR>P : R[X]<VAR>x : A<GOAL>D ((aeval x) P) = (aeval x) (derivative P) • D x
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>M : Type u_4<VAR>inst✝⁸ : CommSemiring R<VAR>inst✝⁷ : CommSemiring A<VAR>inst✝⁶ : CommSemiring B<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : Algebra R A<VAR>inst✝³ : Algebra R B<VAR>inst✝² : Module A M<VAR>inst✝¹ : Module B M<VAR>inst✝ : Module R M<VAR>D D1 D2 : Derivation R A M<VAR>r : R<VAR>a b x : A<VAR>a✝ : R<GOAL>D ((aeval x) (C a✝)) = (aeval x) (derivative (C a✝)) • D x
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>M : Type u_4<VAR>inst✝⁸ : CommSemiring R<VAR>inst✝⁷ : CommSemiring A<VAR>inst✝⁶ : CommSemiring B<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : Algebra R A<VAR>inst✝³ : Algebra R B<VAR>inst✝² : Module A M<VAR>inst✝¹ : Module B M<VAR>inst✝ : Module R M<VAR>D D1 D2 : Derivation R A M<VAR>r : R<VAR>a b x : A<VAR>p✝ q✝ : R[X]<VAR>a✝¹ : D ((aeval x) p✝) = (aeval x) (derivative p✝) • D x<VAR>a✝ : D ((aeval x) q✝) = (aeval x) (derivative q✝) • D x<GOAL>D ((aeval x) (p✝ + q✝)) = (aeval x) (derivative (p✝ + q✝)) • D x
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>M : Type u_4<VAR>inst✝⁸ : CommSemiring R<VAR>inst✝⁷ : CommSemiring A<VAR>inst✝⁶ : CommSemiring B<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : Algebra R A<VAR>inst✝³ : Algebra R B<VAR>inst✝² : Module A M<VAR>inst✝¹ : Module B M<VAR>inst✝ : Module R M<VAR>D D1 D2 : Derivation R A M<VAR>r : R<VAR>a b x : A<VAR>n✝ : ℕ<VAR>a✝¹ : R<VAR>a✝ : D ((aeval x) (C a✝¹ * X ^ n✝)) = (aeval x) (derivative (C a✝¹ * X ^ n✝)) • D x<GOAL>D ((aeval x) (C a✝¹ * X ^ (n✝ + 1))) = (aeval x) (derivative (C a✝¹ * X ^ (n✝ + 1))) • D x
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Sort w<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : X<VAR>s s₁ s₂ t : Set X<VAR>p✝ p₁ p₂ : X → Prop<VAR>inst✝ : TopologicalSpace X<VAR>p : X → Prop<GOAL>(∃ t ⊆ {x | (fun y => p y) x}, IsOpen t ∧ x ∈ t) ↔ ∃ t, (∀ y ∈ t, p y) ∧ IsOpen t ∧ x ∈ t
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝³ : Preorder ι<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>f✝ g : ι → Ω → E<VAR>ℱ : Filtration ι m0<VAR>f : ι → Ω → ℝ<VAR>hf : Submartingale f ℱ μ<VAR>i j : ι<VAR>hij : i ≤ j<GOAL>0 ≤ᶠ[ae μ] μ[f j - f i|↑ℱ i]
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝³ : Preorder ι<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>f✝ g : ι → Ω → E<VAR>ℱ : Filtration ι m0<VAR>f : ι → Ω → ℝ<VAR>hf : Submartingale f ℱ μ<VAR>i j : ι<VAR>hij : i ≤ j<VAR>h : SigmaFinite (μ.trim ⋯)<GOAL>0 ≤ᶠ[ae μ] μ[f j - f i|↑ℱ i]
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝³ : Preorder ι<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>f✝ g : ι → Ω → E<VAR>ℱ : Filtration ι m0<VAR>f : ι → Ω → ℝ<VAR>hf : Submartingale f ℱ μ<VAR>i j : ι<VAR>hij : i ≤ j<VAR>h : ¬SigmaFinite (μ.trim ⋯)<GOAL>0 ≤ᶠ[ae μ] μ[f j - f i|↑ℱ i]
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝³ : Preorder ι<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>f✝ g : ι → Ω → E<VAR>ℱ : Filtration ι m0<VAR>f : ι → Ω → ℝ<VAR>hf : Submartingale f ℱ μ<VAR>i j : ι<VAR>hij : i ≤ j<VAR>h : SigmaFinite (μ.trim ⋯)<GOAL>0 ≤ᶠ[ae μ] μ[f j|↑ℱ i] - μ[f i|↑ℱ i]
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝³ : Preorder ι<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>f✝ g : ι → Ω → E<VAR>ℱ : Filtration ι m0<VAR>f : ι → Ω → ℝ<VAR>hf : Submartingale f ℱ μ<VAR>i j : ι<VAR>hij : i ≤ j<VAR>h : SigmaFinite (μ.trim ⋯)<GOAL>f i ≤ᶠ[ae μ] μ[f j|↑ℱ i]
<VAR>R A : Type u<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : CommRing A<VAR>inst✝² : IsDomain A<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : NoZeroSMulDivisors R A<GOAL>#{ x // IsAlgebraic R x } ≤ max #R ℵ₀
<VAR>R A : Type u<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : CommRing A<VAR>inst✝² : IsDomain A<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : NoZeroSMulDivisors R A<GOAL>lift.{u, u} #{ x // IsAlgebraic R x } ≤ max (lift.{u, u} #R) ℵ₀
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>D : Type u'<VAR>inst✝⁵ : Category.{v, u'} D<VAR>inst✝⁴ : HasFiniteProducts C<VAR>inst✝³ : HasFiniteProducts D<VAR>F : C ⥤ D<VAR>L : D ⥤ C<VAR>inst✝² : CartesianClosed C<VAR>inst✝¹ : CartesianClosed D<VAR>inst✝ : PreservesLimitsOfShape (Discrete WalkingPair) F<VAR>A B : C<GOAL>uncurry ((expComparison F A).app B) = inv (prodComparison F A (A ⟹ B)) ≫ F.map ((exp.ev A).app B)
<VAR>α : Type u_1<VAR>β : ?m.6008<VAR>inst✝² : Preorder α<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : IsLower α<VAR>s : Set α<VAR>h : IsOpen s<GOAL>IsLowerSet s
<VAR>α : Type u_1<VAR>β : ?m.6008<VAR>inst✝² : Preorder α<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : IsLower α<VAR>s : Set α<VAR>h : GenerateOpen {t | ∃ a, (Ici a)ᶜ = t} s<GOAL>IsLowerSet s
<VAR>z w : ℍ<VAR>r R : ℝ<GOAL>dist z w = r ↔ dist ↑z ↑w / (2 * √(z.im * w.im)) = sinh (r / 2)
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : Monoid γ<VAR>inst✝¹ : (i : ι) → AddMonoid (β i)<VAR>inst✝ : (i : ι) → DistribMulAction γ (β i)<VAR>i✝ : ι<VAR>c : γ<VAR>x : β i✝<VAR>i : ι<GOAL>(single i✝ (c • x)) i = (c • single i✝ x) i
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : Monoid γ<VAR>inst✝¹ : (i : ι) → AddMonoid (β i)<VAR>inst✝ : (i : ι) → DistribMulAction γ (β i)<VAR>i✝ : ι<VAR>c : γ<VAR>x : β i✝<VAR>i : ι<GOAL>(if h : i✝ = i then ⋯ ▸ (c • x) else 0) = c • if h : i✝ = i then ⋯ ▸ x else 0
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>ι : Type u_3<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s✝ t s : Set X<GOAL>IsSigmaCompact s ↔ IsSigmaCompact univ
<VAR>α : Type u_1<VAR>𝒜 : Set (Set α)<VAR>s t : Set α<GOAL>generateFrom (generateSetAlgebra 𝒜) = generateFrom 𝒜
<VAR>α : Type u_1<VAR>𝒜 : Set (Set α)<VAR>s✝ t s : Set α<VAR>ms : MeasurableSet s<GOAL>MeasurableSet s
<VAR>α : Type u_1<VAR>𝒜 : Set (Set α)<VAR>s✝ t✝ s : Set α<VAR>ms : MeasurableSet s<VAR>t : Set α<VAR>ht : t ∈ generateSetAlgebra 𝒜<GOAL>MeasurableSet t