ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>A : Type u₁<VAR>B : Type u₂<VAR>C : Type u₃<VAR>D : Type u₄<VAR>E : Type u₅<VAR>F : Type u₆<VAR>inst✝⁵ : Category.{v₁, u₁} A<VAR>inst✝⁴ : Category.{v₂, u₂} B<VAR>inst✝³ : Category.{v₃, u₃} C<VAR>inst✝² : Category.{v₄, u₄} D<VAR>inst✝¹ : Category.{v₅, u₅} E<VAR>inst✝ : Category.{v₆, u₆} F<VAR>G₁ : A ⥤ C<VAR>G₂ : C ⥤ E<VAR>H₁ : B ⥤ D<VAR>H₂ : D ⥤ F<VAR>L₁ : A ⥤ B<VAR>R₁ : B ⥤ A<VAR>L₂ : C ⥤ D<VAR>R₂ : D ⥤ C<VAR>L₃ : E ⥤ F<VAR>R₃ : F ⥤ E<VAR>adj₁ : L₁ ⊣ R₁<VAR>adj₂ : L₂ ⊣ R₂<VAR>adj₃ : L₃ ⊣ R₃<VAR>α : G₁ ⋙ L₂ ⟶ L₁ ⋙ H₁<VAR>β : G₂ ⋙ L₃ ⟶ L₂ ⋙ H₂<VAR>b : B<GOAL>adj₃.unit.app (G₂.obj (G₁.obj (R₁.obj b))) ≫ R₃.map (β.app (G₁.obj (R₁.obj b))) ≫ R₃.map (H₂.map (α.app (R₁.obj b))) ≫ R₃.map (H₂.map (H₁.map (adj₁.counit.app b))) = ((adj₃.unit.app (G₂.obj (G₁.obj (R₁.obj b))) ≫ R₃.map (L₃.map ((G₂.map (adj₂.unit.app (G₁.obj (R₁.obj b))) ≫ G₂.map (R₂.map (α.app (R₁.obj b)))) ≫ G₂.map (R₂.map (H₁.map (adj₁.counit.app b)))))) ≫ R₃.map (β.app (R₂.obj (H₁.obj b)))) ≫ R₃.map (H₂.map (adj₂.counit.app (H₁.obj b)))
<VAR>A : Type u₁<VAR>B : Type u₂<VAR>C : Type u₃<VAR>D : Type u₄<VAR>E : Type u₅<VAR>F : Type u₆<VAR>inst✝⁵ : Category.{v₁, u₁} A<VAR>inst✝⁴ : Category.{v₂, u₂} B<VAR>inst✝³ : Category.{v₃, u₃} C<VAR>inst✝² : Category.{v₄, u₄} D<VAR>inst✝¹ : Category.{v₅, u₅} E<VAR>inst✝ : Category.{v₆, u₆} F<VAR>G₁ : A ⥤ C<VAR>G₂ : C ⥤ E<VAR>H₁ : B ⥤ D<VAR>H₂ : D ⥤ F<VAR>L₁ : A ⥤ B<VAR>R₁ : B ⥤ A<VAR>L₂ : C ⥤ D<VAR>R₂ : D ⥤ C<VAR>L₃ : E ⥤ F<VAR>R₃ : F ⥤ E<VAR>adj₁ : L₁ ⊣ R₁<VAR>adj₂ : L₂ ⊣ R₂<VAR>adj₃ : L₃ ⊣ R₃<VAR>α : G₁ ⋙ L₂ ⟶ L₁ ⋙ H₁<VAR>β : G₂ ⋙ L₃ ⟶ L₂ ⋙ H₂<VAR>b : B<GOAL>adj₃.unit.app (G₂.obj (G₁.obj (R₁.obj b))) ≫ R₃.map (β.app (G₁.obj (R₁.obj b))) ≫ R₃.map (H₂.map (α.app (R₁.obj b))) ≫ R₃.map (H₂.map (H₁.map (adj₁.counit.app b))) = ((adj₃.unit.app (G₂.obj (G₁.obj (R₁.obj b))) ≫ R₃.map (L₃.map (G₂.map (adj₂.unit.app (G₁.obj (R₁.obj b))) ≫ G₂.map (R₂.map (α.app (R₁.obj b))))) ≫ R₃.map (L₃.map (G₂.map (R₂.map (H₁.map (adj₁.counit.app b)))))) ≫ R₃.map (β.app (R₂.obj (H₁.obj b)))) ≫ R₃.map (H₂.map (adj₂.counit.app (H₁.obj b)))
<VAR>A : Type u₁<VAR>B : Type u₂<VAR>C : Type u₃<VAR>D : Type u₄<VAR>E : Type u₅<VAR>F : Type u₆<VAR>inst✝⁵ : Category.{v₁, u₁} A<VAR>inst✝⁴ : Category.{v₂, u₂} B<VAR>inst✝³ : Category.{v₃, u₃} C<VAR>inst✝² : Category.{v₄, u₄} D<VAR>inst✝¹ : Category.{v₅, u₅} E<VAR>inst✝ : Category.{v₆, u₆} F<VAR>G₁ : A ⥤ C<VAR>G₂ : C ⥤ E<VAR>H₁ : B ⥤ D<VAR>H₂ : D ⥤ F<VAR>L₁ : A ⥤ B<VAR>R₁ : B ⥤ A<VAR>L₂ : C ⥤ D<VAR>R₂ : D ⥤ C<VAR>L₃ : E ⥤ F<VAR>R₃ : F ⥤ E<VAR>adj₁ : L₁ ⊣ R₁<VAR>adj₂ : L₂ ⊣ R₂<VAR>adj₃ : L₃ ⊣ R₃<VAR>α : G₁ ⋙ L₂ ⟶ L₁ ⋙ H₁<VAR>β : G₂ ⋙ L₃ ⟶ L₂ ⋙ H₂<VAR>b : B<GOAL>adj₃.unit.app (G₂.obj (G₁.obj (R₁.obj b))) ≫ R₃.map (β.app (G₁.obj (R₁.obj b))) ≫ R₃.map (H₂.map (α.app (R₁.obj b))) ≫ R₃.map (H₂.map (H₁.map (adj₁.counit.app b))) = adj₃.unit.app (G₂.obj (G₁.obj (R₁.obj b))) ≫ R₃.map (β.app (G₁.obj (R₁.obj b)) ≫ (L₂ ⋙ H₂).map ((adj₂.unit.app (G₁.obj (R₁.obj b)) ≫ R₂.map (α.app (R₁.obj b))) ≫ R₂.map (H₁.map (adj₁.counit.app b)))) ≫ R₃.map (H₂.map (adj₂.counit.app (H₁.obj b)))
<VAR>A : Type u₁<VAR>B : Type u₂<VAR>C : Type u₃<VAR>D : Type u₄<VAR>E : Type u₅<VAR>F : Type u₆<VAR>inst✝⁵ : Category.{v₁, u₁} A<VAR>inst✝⁴ : Category.{v₂, u₂} B<VAR>inst✝³ : Category.{v₃, u₃} C<VAR>inst✝² : Category.{v₄, u₄} D<VAR>inst✝¹ : Category.{v₅, u₅} E<VAR>inst✝ : Category.{v₆, u₆} F<VAR>G₁ : A ⥤ C<VAR>G₂ : C ⥤ E<VAR>H₁ : B ⥤ D<VAR>H₂ : D ⥤ F<VAR>L₁ : A ⥤ B<VAR>R₁ : B ⥤ A<VAR>L₂ : C ⥤ D<VAR>R₂ : D ⥤ C<VAR>L₃ : E ⥤ F<VAR>R₃ : F ⥤ E<VAR>adj₁ : L₁ ⊣ R₁<VAR>adj₂ : L₂ ⊣ R₂<VAR>adj₃ : L₃ ⊣ R₃<VAR>α : G₁ ⋙ L₂ ⟶ L₁ ⋙ H₁<VAR>β : G₂ ⋙ L₃ ⟶ L₂ ⋙ H₂<VAR>b : B<GOAL>adj₃.unit.app (G₂.obj (G₁.obj (R₁.obj b))) ≫ R₃.map (β.app (G₁.obj (R₁.obj b))) ≫ R₃.map (H₂.map (α.app (R₁.obj b))) ≫ R₃.map (H₂.map (H₁.map (adj₁.counit.app b))) = adj₃.unit.app (G₂.obj (G₁.obj (R₁.obj b))) ≫ (R₃.map (β.app (G₁.obj (R₁.obj b))) ≫ R₃.map ((L₂ ⋙ H₂).map (adj₂.unit.app (G₁.obj (R₁.obj b)) ≫ R₂.map (α.app (R₁.obj b)))) ≫ R₃.map ((L₂ ⋙ H₂).map (R₂.map (H₁.map (adj₁.counit.app b))))) ≫ R₃.map (H₂.map (adj₂.counit.app (H₁.obj b)))
<VAR>A : Type u₁<VAR>B : Type u₂<VAR>C : Type u₃<VAR>D : Type u₄<VAR>E : Type u₅<VAR>F : Type u₆<VAR>inst✝⁵ : Category.{v₁, u₁} A<VAR>inst✝⁴ : Category.{v₂, u₂} B<VAR>inst✝³ : Category.{v₃, u₃} C<VAR>inst✝² : Category.{v₄, u₄} D<VAR>inst✝¹ : Category.{v₅, u₅} E<VAR>inst✝ : Category.{v₆, u₆} F<VAR>G₁ : A ⥤ C<VAR>G₂ : C ⥤ E<VAR>H₁ : B ⥤ D<VAR>H₂ : D ⥤ F<VAR>L₁ : A ⥤ B<VAR>R₁ : B ⥤ A<VAR>L₂ : C ⥤ D<VAR>R₂ : D ⥤ C<VAR>L₃ : E ⥤ F<VAR>R₃ : F ⥤ E<VAR>adj₁ : L₁ ⊣ R₁<VAR>adj₂ : L₂ ⊣ R₂<VAR>adj₃ : L₃ ⊣ R₃<VAR>α : G₁ ⋙ L₂ ⟶ L₁ ⋙ H₁<VAR>β : G₂ ⋙ L₃ ⟶ L₂ ⋙ H₂<VAR>b : B<GOAL>adj₃.unit.app (G₂.obj (G₁.obj (R₁.obj b))) ≫ R₃.map (β.app (G₁.obj (R₁.obj b))) ≫ R₃.map (H₂.map (α.app (R₁.obj b))) ≫ R₃.map (H₂.map (H₁.map (adj₁.counit.app b))) = adj₃.unit.app (G₂.obj (G₁.obj (R₁.obj b))) ≫ R₃.map (β.app (G₁.obj (R₁.obj b))) ≫ R₃.map ((L₂ ⋙ H₂).map (adj₂.unit.app (G₁.obj (R₁.obj b)) ≫ R₂.map (α.app (R₁.obj b)))) ≫ R₃.map (H₂.map (adj₂.counit.app (H₁.obj (L₁.obj (R₁.obj b))) ≫ (𝟭 D).map (H₁.map (adj₁.counit.app b))))
<VAR>A : Type u₁<VAR>B : Type u₂<VAR>C : Type u₃<VAR>D : Type u₄<VAR>E : Type u₅<VAR>F : Type u₆<VAR>inst✝⁵ : Category.{v₁, u₁} A<VAR>inst✝⁴ : Category.{v₂, u₂} B<VAR>inst✝³ : Category.{v₃, u₃} C<VAR>inst✝² : Category.{v₄, u₄} D<VAR>inst✝¹ : Category.{v₅, u₅} E<VAR>inst✝ : Category.{v₆, u₆} F<VAR>G₁ : A ⥤ C<VAR>G₂ : C ⥤ E<VAR>H₁ : B ⥤ D<VAR>H₂ : D ⥤ F<VAR>L₁ : A ⥤ B<VAR>R₁ : B ⥤ A<VAR>L₂ : C ⥤ D<VAR>R₂ : D ⥤ C<VAR>L₃ : E ⥤ F<VAR>R₃ : F ⥤ E<VAR>adj₁ : L₁ ⊣ R₁<VAR>adj₂ : L₂ ⊣ R₂<VAR>adj₃ : L₃ ⊣ R₃<VAR>α : G₁ ⋙ L₂ ⟶ L₁ ⋙ H₁<VAR>β : G₂ ⋙ L₃ ⟶ L₂ ⋙ H₂<VAR>b : B<GOAL>adj₃.unit.app (G₂.obj (G₁.obj (R₁.obj b))) ≫ R₃.map (β.app (G₁.obj (R₁.obj b))) ≫ R₃.map (H₂.map (α.app (R₁.obj b))) ≫ R₃.map (H₂.map (H₁.map (adj₁.counit.app b))) = adj₃.unit.app (G₂.obj (G₁.obj (R₁.obj b))) ≫ R₃.map (β.app (G₁.obj (R₁.obj b))) ≫ R₃.map (H₂.map (L₂.map (adj₂.unit.app (G₁.obj (R₁.obj b))))) ≫ R₃.map (H₂.map (L₂.map (R₂.map (α.app (R₁.obj b))))) ≫ R₃.map (H₂.map (adj₂.counit.app (H₁.obj (L₁.obj (R₁.obj b))))) ≫ R₃.map (H₂.map (H₁.map (adj₁.counit.app b)))
<VAR>A : Type u₁<VAR>B : Type u₂<VAR>C : Type u₃<VAR>D : Type u₄<VAR>E : Type u₅<VAR>F : Type u₆<VAR>inst✝⁵ : Category.{v₁, u₁} A<VAR>inst✝⁴ : Category.{v₂, u₂} B<VAR>inst✝³ : Category.{v₃, u₃} C<VAR>inst✝² : Category.{v₄, u₄} D<VAR>inst✝¹ : Category.{v₅, u₅} E<VAR>inst✝ : Category.{v₆, u₆} F<VAR>G₁ : A ⥤ C<VAR>G₂ : C ⥤ E<VAR>H₁ : B ⥤ D<VAR>H₂ : D ⥤ F<VAR>L₁ : A ⥤ B<VAR>R₁ : B ⥤ A<VAR>L₂ : C ⥤ D<VAR>R₂ : D ⥤ C<VAR>L₃ : E ⥤ F<VAR>R₃ : F ⥤ E<VAR>adj₁ : L₁ ⊣ R₁<VAR>adj₂ : L₂ ⊣ R₂<VAR>adj₃ : L₃ ⊣ R₃<VAR>α : G₁ ⋙ L₂ ⟶ L₁ ⋙ H₁<VAR>β : G₂ ⋙ L₃ ⟶ L₂ ⋙ H₂<VAR>b : B<GOAL>adj₃.unit.app (G₂.obj (G₁.obj (R₁.obj b))) ≫ R₃.map (β.app (G₁.obj (R₁.obj b))) ≫ R₃.map (H₂.map (α.app (R₁.obj b))) ≫ R₃.map (H₂.map (H₁.map (adj₁.counit.app b))) = adj₃.unit.app (G₂.obj (G₁.obj (R₁.obj b))) ≫ R₃.map (β.app (G₁.obj (R₁.obj b))) ≫ R₃.map (H₂.map (L₂.map (adj₂.unit.app (G₁.obj (R₁.obj b))))) ≫ R₃.map (H₂.map (adj₂.counit.app (L₂.obj (G₁.obj (R₁.obj b))) ≫ (𝟭 D).map (α.app (R₁.obj b)))) ≫ R₃.map (H₂.map (H₁.map (adj₁.counit.app b)))
<VAR>A : Type u₁<VAR>B : Type u₂<VAR>C : Type u₃<VAR>D : Type u₄<VAR>E : Type u₅<VAR>F : Type u₆<VAR>inst✝⁵ : Category.{v₁, u₁} A<VAR>inst✝⁴ : Category.{v₂, u₂} B<VAR>inst✝³ : Category.{v₃, u₃} C<VAR>inst✝² : Category.{v₄, u₄} D<VAR>inst✝¹ : Category.{v₅, u₅} E<VAR>inst✝ : Category.{v₆, u₆} F<VAR>G₁ : A ⥤ C<VAR>G₂ : C ⥤ E<VAR>H₁ : B ⥤ D<VAR>H₂ : D ⥤ F<VAR>L₁ : A ⥤ B<VAR>R₁ : B ⥤ A<VAR>L₂ : C ⥤ D<VAR>R₂ : D ⥤ C<VAR>L₃ : E ⥤ F<VAR>R₃ : F ⥤ E<VAR>adj₁ : L₁ ⊣ R₁<VAR>adj₂ : L₂ ⊣ R₂<VAR>adj₃ : L₃ ⊣ R₃<VAR>α : G₁ ⋙ L₂ ⟶ L₁ ⋙ H₁<VAR>β : G₂ ⋙ L₃ ⟶ L₂ ⋙ H₂<VAR>b : B<GOAL>adj₃.unit.app (G₂.obj (G₁.obj (R₁.obj b))) ≫ R₃.map (β.app (G₁.obj (R₁.obj b))) ≫ R₃.map (H₂.map (α.app (R₁.obj b))) ≫ R₃.map (H₂.map (H₁.map (adj₁.counit.app b))) = adj₃.unit.app (G₂.obj (G₁.obj (R₁.obj b))) ≫ R₃.map (β.app (G₁.obj (R₁.obj b))) ≫ R₃.map (H₂.map (L₂.map (adj₂.unit.app (G₁.obj (R₁.obj b))))) ≫ R₃.map (H₂.map (adj₂.counit.app (L₂.obj (G₁.obj (R₁.obj b))))) ≫ R₃.map (H₂.map (α.app (R₁.obj b))) ≫ R₃.map (H₂.map (H₁.map (adj₁.counit.app b)))
<VAR>A : Type u₁<VAR>B : Type u₂<VAR>C : Type u₃<VAR>D : Type u₄<VAR>E : Type u₅<VAR>F : Type u₆<VAR>inst✝⁵ : Category.{v₁, u₁} A<VAR>inst✝⁴ : Category.{v₂, u₂} B<VAR>inst✝³ : Category.{v₃, u₃} C<VAR>inst✝² : Category.{v₄, u₄} D<VAR>inst✝¹ : Category.{v₅, u₅} E<VAR>inst✝ : Category.{v₆, u₆} F<VAR>G₁ : A ⥤ C<VAR>G₂ : C ⥤ E<VAR>H₁ : B ⥤ D<VAR>H₂ : D ⥤ F<VAR>L₁ : A ⥤ B<VAR>R₁ : B ⥤ A<VAR>L₂ : C ⥤ D<VAR>R₂ : D ⥤ C<VAR>L₃ : E ⥤ F<VAR>R₃ : F ⥤ E<VAR>adj₁ : L₁ ⊣ R₁<VAR>adj₂ : L₂ ⊣ R₂<VAR>adj₃ : L₃ ⊣ R₃<VAR>α : G₁ ⋙ L₂ ⟶ L₁ ⋙ H₁<VAR>β : G₂ ⋙ L₃ ⟶ L₂ ⋙ H₂<VAR>b : B<GOAL>adj₃.unit.app (G₂.obj (G₁.obj (R₁.obj b))) ≫ R₃.map (β.app (G₁.obj (R₁.obj b))) ≫ R₃.map (H₂.map (α.app (R₁.obj b))) ≫ R₃.map (H₂.map (H₁.map (adj₁.counit.app b))) = adj₃.unit.app (G₂.obj (G₁.obj (R₁.obj b))) ≫ R₃.map (β.app (G₁.obj (R₁.obj b))) ≫ (R₃.map (H₂.map (𝟙 (L₂.obj (G₁.obj (R₁.obj b))))) ≫ R₃.map (H₂.map (α.app (R₁.obj b)))) ≫ R₃.map (H₂.map (H₁.map (adj₁.counit.app b)))
<VAR>G : Type u<VAR>inst✝ : Monoid G<VAR>n : ℕ<VAR>g : G<GOAL>g ^ n = g ^ (n % exponent G + exponent G * (n / exponent G))
<VAR>G : Type u<VAR>inst✝ : Monoid G<VAR>n : ℕ<VAR>g : G<GOAL>g ^ (n % exponent G + exponent G * (n / exponent G)) = g ^ (n % exponent G)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>inst✝² : Zero M<VAR>inst✝¹ : Zero N<VAR>inst✝ : Zero P<VAR>f : ZeroHom N P<VAR>f₂ : ZeroHom M N<GOAL>(⇑f ∘ ⇑f₂) 0 = 0
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : LieRing L<VAR>inst✝⁵ : LieAlgebra R L<VAR>H : LieSubalgebra R L<VAR>inst✝⁴ : IsNilpotent R ↥H<VAR>M : Type u_3<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<VAR>χ₁ χ₂ χ₃ : ↥H → R<VAR>hχ : χ₁ + χ₂ = χ₃<VAR>x : ↥(rootSpace H χ₁)<VAR>y : ↥(rootSpace H χ₂)<GOAL>↑((rootSpaceProduct R L H χ₁ χ₂ χ₃ hχ) (x ⊗ₜ[R] y)) = ⁅↑x, ↑y⁆
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>e : Sym2 α<VAR>f : α → β<VAR>a₁ b₁ a₂ b₂ : α<GOAL>[a₁, b₁].Perm [a₂, b₂] → a₁ = a₂ ∧ b₁ = b₂ ∨ a₁ = b₂ ∧ b₁ = a₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>e : Sym2 α<VAR>f : α → β<VAR>a₁ b₁ a₂ b₂ : α<GOAL>a₁ = a₂ ∧ b₁ = b₂ ∨ ¬a₁ = a₂ ∧ b₁ = a₂ ∧ b₂ = a₁ → a₁ = a₂ ∧ b₁ = b₂ ∨ a₁ = b₂ ∧ b₁ = a₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>e : Sym2 α<VAR>f : α → β<VAR>a₁ b₁ a₂ b₂ : α<VAR>h₁ : a₁ = b₂<VAR>h₂ : b₁ = a₂<GOAL>[b₂, a₂].Perm [a₂, b₂]
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>α : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>f : σ ↪ τ<VAR>φ : MvPolynomial σ R<VAR>d : σ →₀ ℕ<GOAL>coeff (embDomain f d) ((rename ⇑f) φ) = coeff d φ
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : Ring S<VAR>inst✝⁶ : Algebra R S<VAR>A : Type u_4<VAR>B : Type u_5<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : CommRing B<VAR>inst✝³ : IsDomain B<VAR>inst✝² : Algebra A B<VAR>K : Type u_6<VAR>inst✝¹ : Field K<VAR>inst✝ : Algebra A S<VAR>h : PowerBasis A S<VAR>p : A[X]<VAR>ne_zero : p ≠ 0<VAR>root : (aeval h.gen) p = 0<GOAL>↑h.dim ≤ p.degree
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : Ring S<VAR>inst✝⁶ : Algebra R S<VAR>A : Type u_4<VAR>B : Type u_5<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : CommRing B<VAR>inst✝³ : IsDomain B<VAR>inst✝² : Algebra A B<VAR>K : Type u_6<VAR>inst✝¹ : Field K<VAR>inst✝ : Algebra A S<VAR>h : PowerBasis A S<VAR>p : A[X]<VAR>ne_zero : p ≠ 0<VAR>root : (aeval h.gen) p = 0<GOAL>↑h.dim ≤ ↑p.natDegree
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : SFinite μ<GOAL>μ.toFinite = 0 ↔ μ = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>l : Filter α<VAR>f : α → β<VAR>ι : Sort u_5<VAR>p : ι → Prop<VAR>s : ι → Set α<VAR>h : l.HasBasis p s<GOAL>(∃ i, p i ∧ (f '' s i).Subsingleton) ↔ ∃ i, p i ∧ ∀ x ∈ s i, ∀ y ∈ s i, f x = f y
<VAR>α : Type u_1<VAR>inst✝ : LinearOrder α<VAR>s✝ t : Set α<VAR>x✝ y z : α<VAR>s : Set α<VAR>x : αᵒᵈ<GOAL>(x ∈ range fun x => ⋯.some) ↔ x ∈ ⇑ofDual ⁻¹' range fun x => ⋯.some
<VAR>α : Type u_1<VAR>inst✝ : LinearOrder α<VAR>s✝ t : Set α<VAR>x✝ y z : α<VAR>s : Set α<VAR>x : αᵒᵈ<GOAL>(∃ a, ∃ (h : a ∈ s), ⋯.some = x) ↔ ∃ a, ∃ (h : a ∈ s), ⋯.some = ofDual x
<VAR>J : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>inst✝² : Category.{v₂, u₂} K<VAR>C : Type u₃<VAR>inst✝¹ : Category.{v₃, u₃} C<VAR>D : Type u₄<VAR>inst✝ : Category.{v₄, u₄} D<VAR>F✝ F : J ⥤ C<GOAL>((fun c => ⟨op c.pt, c.π⟩) ≫ fun c => { pt := unop c.fst, π := c.snd }) = 𝟙 (Cone F)
<VAR>J : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>inst✝² : Category.{v₂, u₂} K<VAR>C : Type u₃<VAR>inst✝¹ : Category.{v₃, u₃} C<VAR>D : Type u₄<VAR>inst✝ : Category.{v₄, u₄} D<VAR>F✝ F : J ⥤ C<VAR>X : Cone F<GOAL>((fun c => ⟨op c.pt, c.π⟩) ≫ fun c => { pt := unop c.fst, π := c.snd }) X = 𝟙 (Cone F) X
<VAR>J : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>inst✝² : Category.{v₂, u₂} K<VAR>C : Type u₃<VAR>inst✝¹ : Category.{v₃, u₃} C<VAR>D : Type u₄<VAR>inst✝ : Category.{v₄, u₄} D<VAR>F✝ F : J ⥤ C<GOAL>((fun c => { pt := unop c.fst, π := c.snd }) ≫ fun c => ⟨op c.pt, c.π⟩) = 𝟙 ((X : Cᵒᵖ) × F.cones.obj X)
<VAR>J : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>inst✝² : Category.{v₂, u₂} K<VAR>C : Type u₃<VAR>inst✝¹ : Category.{v₃, u₃} C<VAR>D : Type u₄<VAR>inst✝ : Category.{v₄, u₄} D<VAR>F✝ F : J ⥤ C<VAR>X : (X : Cᵒᵖ) × F.cones.obj X<GOAL>((fun c => { pt := unop c.fst, π := c.snd }) ≫ fun c => ⟨op c.pt, c.π⟩) X = 𝟙 ((X : Cᵒᵖ) × F.cones.obj X) X
<VAR>z w : ℂ<GOAL>¬z ≤ w ↔ w.re < z.re ∨ z.im ≠ w.im
<VAR>M : Type u_1<VAR>inst✝ : Semigroup M<VAR>U : Ultrafilter M<VAR>U_idem : U * U = U<VAR>s₀ : Set M<VAR>sU : s₀ ∈ U<GOAL>∃ a, FP a ⊆ s₀
<VAR>M : Type u_1<VAR>inst✝ : Semigroup M<VAR>U : Ultrafilter M<VAR>U_idem : U * U = U<VAR>s₀ : Set M<VAR>sU : s₀ ∈ U<VAR>exists_elem : ∀ {s : Set M}, s ∈ U → (s ∩ {m | ∀ᶠ (m' : M) in ↑U, m * m' ∈ s}).Nonempty<GOAL>∃ a, FP a ⊆ s₀
<VAR>M : Type u_1<VAR>inst✝ : Semigroup M<VAR>U : Ultrafilter M<VAR>U_idem : U * U = U<VAR>s₀ : Set M<VAR>sU : s₀ ∈ U<VAR>exists_elem : ∀ {s : Set M}, s ∈ U → (s ∩ {m | ∀ᶠ (m' : M) in ↑U, m * m' ∈ s}).Nonempty<VAR>elem : { s // s ∈ U } → M := fun p => ⋯.some<GOAL>∃ a, FP a ⊆ s₀
<VAR>M : Type u_1<VAR>inst✝ : Semigroup M<VAR>U : Ultrafilter M<VAR>U_idem : U * U = U<VAR>s₀ : Set M<VAR>sU : s₀ ∈ U<VAR>exists_elem : ∀ {s : Set M}, s ∈ U → (s ∩ {m | ∀ᶠ (m' : M) in ↑U, m * m' ∈ s}).Nonempty<VAR>elem : { s // s ∈ U } → M := fun p => ⋯.some<VAR>succ : { s // s ∈ U } → { s // s ∈ U } := fun p => ⟨↑p ∩ {m | elem p * m ∈ ↑p}, ⋯⟩<GOAL>∃ a, FP a ⊆ s₀
<VAR>M : Type u_1<VAR>inst✝ : Semigroup M<VAR>U : Ultrafilter M<VAR>U_idem : U * U = U<VAR>s₀ : Set M<VAR>sU : s₀ ∈ U<VAR>exists_elem : ∀ {s : Set M}, s ∈ U → (s ∩ {m | ∀ᶠ (m' : M) in ↑U, m * m' ∈ s}).Nonempty<VAR>elem : { s // s ∈ U } → M := fun p => ⋯.some<VAR>succ : { s // s ∈ U } → { s // s ∈ U } := fun p => ⟨↑p ∩ {m | elem p * m ∈ ↑p}, ⋯⟩<GOAL>FP (Stream'.corec elem succ ⟨s₀, sU⟩) ⊆ s₀
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : MonoidalCategory C<VAR>X Y : Center C<VAR>f : X ⟶ Y<VAR>inst✝ : IsIso f.f<VAR>U : C<GOAL>inv f.f ▷ U ≫ (X.snd.β U).hom = (Y.snd.β U).hom ≫ U ◁ inv f.f
<VAR>α : Type u<VAR>J : Type w<VAR>inst✝³ : SmallCategory J<VAR>inst✝² : FinCategory J<VAR>inst✝¹ : SemilatticeInf α<VAR>inst✝ : OrderTop α<VAR>x y z : α<VAR>f : x ⟶ z<VAR>g : y ⟶ z<GOAL>limit (cospan f g) = Finset.univ.inf (cospan f g).obj
<VAR>α : Type u<VAR>J : Type w<VAR>inst✝³ : SmallCategory J<VAR>inst✝² : FinCategory J<VAR>inst✝¹ : SemilatticeInf α<VAR>inst✝ : OrderTop α<VAR>x y z : α<VAR>f : x ⟶ z<VAR>g : y ⟶ z<GOAL>z ⊓ (x ⊓ (y ⊓ ⊤)) = z ⊓ (x ⊓ y)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>u : ℕ → ℝ<VAR>c : ℝ<VAR>hc : 0 ≤ c<VAR>n : ℕ<VAR>hn : 0 < n<VAR>h : ∀ k < n, u (k + 1) < c * u k<GOAL>u n < c ^ n * u 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>u : ℕ → ℝ<VAR>c : ℝ<VAR>hc : 0 ≤ c<VAR>n : ℕ<VAR>hn : 0 < n<VAR>h : ∀ k < n, u (k + 1) < c * u k<GOAL>u 0 ≤ c ^ 0 * u 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>u : ℕ → ℝ<VAR>c : ℝ<VAR>hc : 0 ≤ c<VAR>n : ℕ<VAR>hn : 0 < n<VAR>h : ∀ k < n, u (k + 1) < c * u k<GOAL>∀ k < n, c * (c ^ k * u 0) ≤ c ^ (k + 1) * u 0
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>hR : ringChar R ≠ 0<GOAL>IsUnit ↑p ↔ ¬p ∣ ringChar R
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>hR : ringChar R ≠ 0<VAR>hch : ↑(ringChar R) = 0<GOAL>IsUnit ↑p ↔ ¬p ∣ ringChar R
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>hR : ringChar R ≠ 0<VAR>hch : ↑(ringChar R) = 0<VAR>hp : Nat.Prime p<GOAL>IsUnit ↑p ↔ ¬p ∣ ringChar R
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : BorelSpace α<VAR>inst✝¹ : SecondCountableTopologyEither α E<VAR>inst✝ : IsFiniteMeasure μ<VAR>f : α →ᵇ E<GOAL>ContinuousMap.toAEEqFun μ f.toContinuousMap ∈ Lp E p μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : BorelSpace α<VAR>inst✝¹ : SecondCountableTopologyEither α E<VAR>inst✝ : IsFiniteMeasure μ<VAR>f : α →ᵇ E<GOAL>∀ᵐ (x : α) ∂μ, ‖↑(ContinuousMap.toAEEqFun μ f.toContinuousMap) x‖ ≤ ‖f‖
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : BorelSpace α<VAR>inst✝¹ : SecondCountableTopologyEither α E<VAR>inst✝ : IsFiniteMeasure μ<VAR>f : α →ᵇ E<VAR>x : α<VAR>a✝ : ↑(ContinuousMap.toAEEqFun μ f.toContinuousMap) x = f.toContinuousMap x<GOAL>‖↑(ContinuousMap.toAEEqFun μ f.toContinuousMap) x‖ ≤ ‖f‖
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>p✝ : FormalMultilinearSeries 𝕜 E F<VAR>r✝ : ℝ≥0<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>r : ℝ≥0<VAR>h : ↑r < p.radius<GOAL>Summable fun n => ‖p n‖₊ * r ^ n
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>p✝ : FormalMultilinearSeries 𝕜 E F<VAR>r✝ : ℝ≥0<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>r : ℝ≥0<VAR>h : ↑r < p.radius<GOAL>Summable fun a => ↑(‖p a‖₊ * r ^ a)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>p✝ : FormalMultilinearSeries 𝕜 E F<VAR>r✝ : ℝ≥0<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>r : ℝ≥0<VAR>h : ↑r < p.radius<GOAL>Summable fun a => ‖p a‖ * ↑r ^ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹³ : Norm E<VAR>inst✝¹² : Norm F<VAR>inst✝¹¹ : Norm G<VAR>inst✝¹⁰ : SeminormedAddCommGroup E'<VAR>inst✝⁹ : SeminormedAddCommGroup F'<VAR>inst✝⁸ : SeminormedAddCommGroup G'<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedAddCommGroup F''<VAR>inst✝⁵ : NormedAddCommGroup G''<VAR>inst✝⁴ : SeminormedRing R<VAR>inst✝³ : SeminormedAddGroup E'''<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedDivisionRing 𝕜<VAR>inst✝ : NormedDivisionRing 𝕜'<VAR>c c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>h : f =O[cofinite] g''<GOAL>∃ C > 0, ∀ ⦃x : α⦄, g'' x ≠ 0 → ‖f x‖ ≤ C * ‖g'' x‖
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹³ : Norm E<VAR>inst✝¹² : Norm F<VAR>inst✝¹¹ : Norm G<VAR>inst✝¹⁰ : SeminormedAddCommGroup E'<VAR>inst✝⁹ : SeminormedAddCommGroup F'<VAR>inst✝⁸ : SeminormedAddCommGroup G'<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedAddCommGroup F''<VAR>inst✝⁵ : NormedAddCommGroup G''<VAR>inst✝⁴ : SeminormedRing R<VAR>inst✝³ : SeminormedAddGroup E'''<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedDivisionRing 𝕜<VAR>inst✝ : NormedDivisionRing 𝕜'<VAR>c c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>h : f =O[cofinite] g''<VAR>C : ℝ<VAR>C₀ : C > 0<VAR>hC : IsBigOWith C cofinite f g''<GOAL>∃ C > 0, ∀ ⦃x : α⦄, g'' x ≠ 0 → ‖f x‖ ≤ C * ‖g'' x‖
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹³ : Norm E<VAR>inst✝¹² : Norm F<VAR>inst✝¹¹ : Norm G<VAR>inst✝¹⁰ : SeminormedAddCommGroup E'<VAR>inst✝⁹ : SeminormedAddCommGroup F'<VAR>inst✝⁸ : SeminormedAddCommGroup G'<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedAddCommGroup F''<VAR>inst✝⁵ : NormedAddCommGroup G''<VAR>inst✝⁴ : SeminormedRing R<VAR>inst✝³ : SeminormedAddGroup E'''<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedDivisionRing 𝕜<VAR>inst✝ : NormedDivisionRing 𝕜'<VAR>c c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>h : f =O[cofinite] g''<VAR>C : ℝ<VAR>C₀ : C > 0<VAR>hC : {x | ¬‖f x‖ ≤ C * ‖g'' x‖}.Finite<GOAL>∃ C > 0, ∀ ⦃x : α⦄, g'' x ≠ 0 → ‖f x‖ ≤ C * ‖g'' x‖
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹³ : Norm E<VAR>inst✝¹² : Norm F<VAR>inst✝¹¹ : Norm G<VAR>inst✝¹⁰ : SeminormedAddCommGroup E'<VAR>inst✝⁹ : SeminormedAddCommGroup F'<VAR>inst✝⁸ : SeminormedAddCommGroup G'<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedAddCommGroup F''<VAR>inst✝⁵ : NormedAddCommGroup G''<VAR>inst✝⁴ : SeminormedRing R<VAR>inst✝³ : SeminormedAddGroup E'''<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedDivisionRing 𝕜<VAR>inst✝ : NormedDivisionRing 𝕜'<VAR>c c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>h : f =O[cofinite] g''<VAR>C : ℝ<VAR>C₀ : C > 0<VAR>hC : {x | ¬‖f x‖ ≤ C * ‖g'' x‖}.Finite<VAR>C' : ℝ<VAR>hC' : ∀ i ∈ Finset.image (fun x => ‖f x‖ / ‖g'' x‖) hC.toFinset, i ≤ C'<GOAL>∃ C > 0, ∀ ⦃x : α⦄, g'' x ≠ 0 → ‖f x‖ ≤ C * ‖g'' x‖