ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>inst✝¹⁸ : CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝¹⁷ : CommRing S<VAR>inst✝¹⁶ : Algebra R S<VAR>P : Type u_3<VAR>inst✝¹⁵ : CommRing P<VAR>A : Type u_4<VAR>K : Type u_5<VAR>inst✝¹⁴ : CommRing A<VAR>inst✝¹³ : IsDomain A<VAR>L : Type u_6<VAR>inst✝¹² : IsDomain R<VAR>inst✝¹¹ : IsDomain S<VAR>inst✝¹⁰ : Field K<VAR>inst✝⁹ : Field L<VAR>inst✝⁸ : Algebra R K<VAR>inst✝⁷ : Algebra R L<VAR>inst✝⁶ : Algebra S L<VAR>inst✝⁵ : IsIntegralClosure S R L<VAR>inst✝⁴ : IsFractionRing S L<VAR>inst✝³ : Algebra K L<VAR>inst✝² : IsScalarTower R S L<VAR>inst✝¹ : IsScalarTower R K L<VAR>a : S<VAR>b : Set S<VAR>inst✝ : Algebra.IsAlgebraic R L<VAR>inj : Function.Injective ⇑(algebraMap R L)<VAR>h : ↑(Ideal.span {a}) ⊆ ↑(Submodule.span R b)<VAR>y' : S<VAR>z' : ↥S⁰<VAR>hx : (algebraMap S L) a * mk' L y' z' ∈ ↑(Ideal.span {(algebraMap S L) a})<VAR>y : S<VAR>z : R<VAR>hz0 : z ≠ 0<VAR>yz_eq : z • y' = ↑z' * y<VAR>injRS : Function.Injective ⇑(algebraMap R S)<GOAL>(algebraMap S L) a * mk' L y' z' ∈ ↑(Submodule.span K (⇑(algebraMap S L) '' b))
<VAR>R : Type u_1<VAR>inst✝¹⁸ : CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝¹⁷ : CommRing S<VAR>inst✝¹⁶ : Algebra R S<VAR>P : Type u_3<VAR>inst✝¹⁵ : CommRing P<VAR>A : Type u_4<VAR>K : Type u_5<VAR>inst✝¹⁴ : CommRing A<VAR>inst✝¹³ : IsDomain A<VAR>L : Type u_6<VAR>inst✝¹² : IsDomain R<VAR>inst✝¹¹ : IsDomain S<VAR>inst✝¹⁰ : Field K<VAR>inst✝⁹ : Field L<VAR>inst✝⁸ : Algebra R K<VAR>inst✝⁷ : Algebra R L<VAR>inst✝⁶ : Algebra S L<VAR>inst✝⁵ : IsIntegralClosure S R L<VAR>inst✝⁴ : IsFractionRing S L<VAR>inst✝³ : Algebra K L<VAR>inst✝² : IsScalarTower R S L<VAR>inst✝¹ : IsScalarTower R K L<VAR>a : S<VAR>b : Set S<VAR>inst✝ : Algebra.IsAlgebraic R L<VAR>inj : Function.Injective ⇑(algebraMap R L)<VAR>h : ↑(Ideal.span {a}) ⊆ ↑(Submodule.span R b)<VAR>y' : S<VAR>z' : ↥S⁰<VAR>hx : (algebraMap S L) a * mk' L y' z' ∈ ↑(Ideal.span {(algebraMap S L) a})<VAR>y : S<VAR>z : R<VAR>hz0 : z ≠ 0<VAR>yz_eq : z • y' = ↑z' * y<VAR>injRS : Function.Injective ⇑(algebraMap R S)<VAR>hz0' : (algebraMap R S) z ∈ S⁰<GOAL>(algebraMap S L) a * mk' L y' z' ∈ ↑(Submodule.span K (⇑(algebraMap S L) '' b))
<VAR>R : Type u_1<VAR>inst✝¹⁸ : CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝¹⁷ : CommRing S<VAR>inst✝¹⁶ : Algebra R S<VAR>P : Type u_3<VAR>inst✝¹⁵ : CommRing P<VAR>A : Type u_4<VAR>K : Type u_5<VAR>inst✝¹⁴ : CommRing A<VAR>inst✝¹³ : IsDomain A<VAR>L : Type u_6<VAR>inst✝¹² : IsDomain R<VAR>inst✝¹¹ : IsDomain S<VAR>inst✝¹⁰ : Field K<VAR>inst✝⁹ : Field L<VAR>inst✝⁸ : Algebra R K<VAR>inst✝⁷ : Algebra R L<VAR>inst✝⁶ : Algebra S L<VAR>inst✝⁵ : IsIntegralClosure S R L<VAR>inst✝⁴ : IsFractionRing S L<VAR>inst✝³ : Algebra K L<VAR>inst✝² : IsScalarTower R S L<VAR>inst✝¹ : IsScalarTower R K L<VAR>a : S<VAR>b : Set S<VAR>inst✝ : Algebra.IsAlgebraic R L<VAR>inj : Function.Injective ⇑(algebraMap R L)<VAR>h : ↑(Ideal.span {a}) ⊆ ↑(Submodule.span R b)<VAR>y' : S<VAR>z' : ↥S⁰<VAR>hx : (algebraMap S L) a * mk' L y' z' ∈ ↑(Ideal.span {(algebraMap S L) a})<VAR>y : S<VAR>z : R<VAR>hz0 : z ≠ 0<VAR>yz_eq : z • y' = ↑z' * y<VAR>injRS : Function.Injective ⇑(algebraMap R S)<VAR>hz0' : (algebraMap R S) z ∈ S⁰<VAR>mk_yz_eq : mk' L y' z' = mk' L y ⟨(algebraMap R S) z, hz0'⟩<GOAL>(algebraMap S L) a * mk' L y' z' ∈ ↑(Submodule.span K (⇑(algebraMap S L) '' b))
<VAR>R : Type u_1<VAR>inst✝¹⁸ : CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝¹⁷ : CommRing S<VAR>inst✝¹⁶ : Algebra R S<VAR>P : Type u_3<VAR>inst✝¹⁵ : CommRing P<VAR>A : Type u_4<VAR>K : Type u_5<VAR>inst✝¹⁴ : CommRing A<VAR>inst✝¹³ : IsDomain A<VAR>L : Type u_6<VAR>inst✝¹² : IsDomain R<VAR>inst✝¹¹ : IsDomain S<VAR>inst✝¹⁰ : Field K<VAR>inst✝⁹ : Field L<VAR>inst✝⁸ : Algebra R K<VAR>inst✝⁷ : Algebra R L<VAR>inst✝⁶ : Algebra S L<VAR>inst✝⁵ : IsIntegralClosure S R L<VAR>inst✝⁴ : IsFractionRing S L<VAR>inst✝³ : Algebra K L<VAR>inst✝² : IsScalarTower R S L<VAR>inst✝¹ : IsScalarTower R K L<VAR>a : S<VAR>b : Set S<VAR>inst✝ : Algebra.IsAlgebraic R L<VAR>inj : Function.Injective ⇑(algebraMap R L)<VAR>h : ↑(Ideal.span {a}) ⊆ ↑(Submodule.span R b)<VAR>y' : S<VAR>z' : ↥S⁰<VAR>hx : (algebraMap S L) a * mk' L y' z' ∈ ↑(Ideal.span {(algebraMap S L) a})<VAR>y : S<VAR>z : R<VAR>hz0 : z ≠ 0<VAR>yz_eq : z • y' = ↑z' * y<VAR>injRS : Function.Injective ⇑(algebraMap R S)<VAR>hz0' : (algebraMap R S) z ∈ S⁰<VAR>mk_yz_eq : mk' L y' z' = mk' L y ⟨(algebraMap R S) z, hz0'⟩<GOAL>(algebraMap S L) (a * y) ∈ Submodule.span K (⇑(algebraMap S L) '' b)
<VAR>R : Type u_1<VAR>inst✝¹⁸ : CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝¹⁷ : CommRing S<VAR>inst✝¹⁶ : Algebra R S<VAR>P : Type u_3<VAR>inst✝¹⁵ : CommRing P<VAR>A : Type u_4<VAR>K : Type u_5<VAR>inst✝¹⁴ : CommRing A<VAR>inst✝¹³ : IsDomain A<VAR>L : Type u_6<VAR>inst✝¹² : IsDomain R<VAR>inst✝¹¹ : IsDomain S<VAR>inst✝¹⁰ : Field K<VAR>inst✝⁹ : Field L<VAR>inst✝⁸ : Algebra R K<VAR>inst✝⁷ : Algebra R L<VAR>inst✝⁶ : Algebra S L<VAR>inst✝⁵ : IsIntegralClosure S R L<VAR>inst✝⁴ : IsFractionRing S L<VAR>inst✝³ : Algebra K L<VAR>inst✝² : IsScalarTower R S L<VAR>inst✝¹ : IsScalarTower R K L<VAR>a : S<VAR>b : Set S<VAR>inst✝ : Algebra.IsAlgebraic R L<VAR>inj : Function.Injective ⇑(algebraMap R L)<VAR>h : ↑(Ideal.span {a}) ⊆ ↑(Submodule.span R b)<VAR>y' : S<VAR>z' : ↥S⁰<VAR>hx : (algebraMap S L) a * mk' L y' z' ∈ ↑(Ideal.span {(algebraMap S L) a})<VAR>y : S<VAR>z : R<VAR>hz0 : z ≠ 0<VAR>yz_eq : z • y' = ↑z' * y<VAR>injRS : Function.Injective ⇑(algebraMap R S)<VAR>hz0' : (algebraMap R S) z ∈ S⁰<VAR>mk_yz_eq : mk' L y' z' = mk' L y ⟨(algebraMap R S) z, hz0'⟩<GOAL>(algebraMap S L) (a * y) ∈ ↑(Submodule.span R (⇑(algebraMap S L) '' b))
<VAR>R : Type u_1<VAR>inst✝¹⁸ : CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝¹⁷ : CommRing S<VAR>inst✝¹⁶ : Algebra R S<VAR>P : Type u_3<VAR>inst✝¹⁵ : CommRing P<VAR>A : Type u_4<VAR>K : Type u_5<VAR>inst✝¹⁴ : CommRing A<VAR>inst✝¹³ : IsDomain A<VAR>L : Type u_6<VAR>inst✝¹² : IsDomain R<VAR>inst✝¹¹ : IsDomain S<VAR>inst✝¹⁰ : Field K<VAR>inst✝⁹ : Field L<VAR>inst✝⁸ : Algebra R K<VAR>inst✝⁷ : Algebra R L<VAR>inst✝⁶ : Algebra S L<VAR>inst✝⁵ : IsIntegralClosure S R L<VAR>inst✝⁴ : IsFractionRing S L<VAR>inst✝³ : Algebra K L<VAR>inst✝² : IsScalarTower R S L<VAR>inst✝¹ : IsScalarTower R K L<VAR>a : S<VAR>b : Set S<VAR>inst✝ : Algebra.IsAlgebraic R L<VAR>inj : Function.Injective ⇑(algebraMap R L)<VAR>h : ↑(Ideal.span {a}) ⊆ ↑(Submodule.span R b)<VAR>y' : S<VAR>z' : ↥S⁰<VAR>hx : (algebraMap S L) a * mk' L y' z' ∈ ↑(Ideal.span {(algebraMap S L) a})<VAR>y : S<VAR>z : R<VAR>hz0 : z ≠ 0<VAR>yz_eq : z • y' = ↑z' * y<VAR>injRS : Function.Injective ⇑(algebraMap R S)<VAR>hz0' : (algebraMap R S) z ∈ S⁰<VAR>mk_yz_eq : mk' L y' z' = mk' L y ⟨(algebraMap R S) z, hz0'⟩<GOAL>(algebraMap S L) (a * y) ∈ ↑(Submodule.map (↑R (Algebra.linearMap S L)) (Submodule.span R b))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : LinearOrder β<VAR>f : α → β<VAR>s : Set α<VAR>a a₁ a₂ b b₁ b₂ c d x : α<GOAL>a ∈ Ι a b ↔ b < a
<VAR>y z : ℝ<VAR>n : ℕ<VAR>hy : 0 < y<VAR>hx : 0 ≤ 0<VAR>h : log 0 ≤ z * log y<GOAL>0 ≤ y ^ z
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝³ : Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>inst✝² : Category.{v₃, u₃} E<VAR>F : C ⥤ D<VAR>G : D ⥤ E<VAR>inst✝¹ : F.Initial<VAR>inst✝ : (F ⋙ G).Initial<GOAL>G.Initial
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝³ : Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>inst✝² : Category.{v₃, u₃} E<VAR>F : C ⥤ D<VAR>G : D ⥤ E<VAR>inst✝¹ : F.Initial<VAR>inst✝ : (F ⋙ G).Initial<GOAL>G.op.Final
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝³ : Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>inst✝² : Category.{v₃, u₃} E<VAR>F : C ⥤ D<VAR>G : D ⥤ E<VAR>inst✝¹ : F.Initial<VAR>inst✝ : (F ⋙ G).Initial<VAR>this : (F.op ⋙ G.op).Final<GOAL>G.op.Final
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>D : Type u'<VAR>inst✝¹ : Category.{v', u'} D<VAR>F : C ⥤ D<VAR>G : D ⥤ C<VAR>adj : F ⊣ G<VAR>inst✝ : G.PreservesEpimorphisms<VAR>P : C<VAR>hP : Projective P<VAR>E✝ X✝ : D<VAR>f : F.obj P ⟶ X✝<VAR>g : E✝ ⟶ X✝<VAR>x✝ : Epi g<GOAL>∃ f', f' ≫ g = f
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>D : Type u'<VAR>inst✝¹ : Category.{v', u'} D<VAR>F : C ⥤ D<VAR>G : D ⥤ C<VAR>adj : F ⊣ G<VAR>inst✝ : G.PreservesEpimorphisms<VAR>P : C<VAR>hP : Projective P<VAR>E✝ X✝ : D<VAR>f : F.obj P ⟶ X✝<VAR>g : E✝ ⟶ X✝<VAR>x✝ : Epi g<VAR>f' : P ⟶ G.obj E✝<VAR>hf' : f' ≫ G.map g = adj.unit.app P ≫ G.map f<GOAL>∃ f', f' ≫ g = f
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>D : Type u'<VAR>inst✝¹ : Category.{v', u'} D<VAR>F : C ⥤ D<VAR>G : D ⥤ C<VAR>adj : F ⊣ G<VAR>inst✝ : G.PreservesEpimorphisms<VAR>P : C<VAR>hP : Projective P<VAR>E✝ X✝ : D<VAR>f : F.obj P ⟶ X✝<VAR>g : E✝ ⟶ X✝<VAR>x✝ : Epi g<VAR>f' : P ⟶ G.obj E✝<VAR>hf' : f' ≫ G.map g = adj.unit.app P ≫ G.map f<GOAL>(F.map f' ≫ adj.counit.app E✝) ≫ g = f
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>D : Type u'<VAR>inst✝¹ : Category.{v', u'} D<VAR>F : C ⥤ D<VAR>G : D ⥤ C<VAR>adj : F ⊣ G<VAR>inst✝ : G.PreservesEpimorphisms<VAR>P : C<VAR>hP : Projective P<VAR>E✝ X✝ : D<VAR>f : F.obj P ⟶ X✝<VAR>g : E✝ ⟶ X✝<VAR>x✝ : Epi g<VAR>f' : P ⟶ G.obj E✝<VAR>hf' : f' ≫ G.map g = adj.unit.app P ≫ G.map f<GOAL>F.map (adj.unit.app P ≫ G.map f) ≫ adj.counit.app X✝ = f
<VAR>α : Type u_1<VAR>a b c d : ℝ≥0∞<VAR>r✝ p q r : ℝ≥0<GOAL>↑r = ENNReal.ofReal ↑r
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝¹¹ : CommSemiring ι<VAR>inst✝¹⁰ : Module ι (Additive ℤˣ)<VAR>inst✝⁹ : DecidableEq ι<VAR>𝒜 : ι → Type u_5<VAR>ℬ : ι → Type u_6<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : (i : ι) → AddCommGroup (𝒜 i)<VAR>inst✝⁶ : (i : ι) → AddCommGroup (ℬ i)<VAR>inst✝⁵ : (i : ι) → Module R (𝒜 i)<VAR>inst✝⁴ : (i : ι) → Module R (ℬ i)<VAR>inst✝³ : DirectSum.GRing 𝒜<VAR>inst✝² : DirectSum.GRing ℬ<VAR>inst✝¹ : DirectSum.GAlgebra R 𝒜<VAR>inst✝ : DirectSum.GAlgebra R ℬ<VAR>a : ⨁ (i : ι), 𝒜 i<VAR>b : ℬ 0<GOAL>(gradedComm R 𝒜 ℬ) (a ⊗ₜ[R] (lof R ι ℬ 0) b) = (lof R ι ℬ 0) b ⊗ₜ[R] a
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝¹¹ : CommSemiring ι<VAR>inst✝¹⁰ : Module ι (Additive ℤˣ)<VAR>inst✝⁹ : DecidableEq ι<VAR>𝒜 : ι → Type u_5<VAR>ℬ : ι → Type u_6<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : (i : ι) → AddCommGroup (𝒜 i)<VAR>inst✝⁶ : (i : ι) → AddCommGroup (ℬ i)<VAR>inst✝⁵ : (i : ι) → Module R (𝒜 i)<VAR>inst✝⁴ : (i : ι) → Module R (ℬ i)<VAR>inst✝³ : DirectSum.GRing 𝒜<VAR>inst✝² : DirectSum.GRing ℬ<VAR>inst✝¹ : DirectSum.GAlgebra R 𝒜<VAR>inst✝ : DirectSum.GAlgebra R ℬ<VAR>a : ⨁ (i : ι), 𝒜 i<VAR>b : ℬ 0<GOAL>↑(gradedComm R 𝒜 ℬ) ∘ₗ (mk R (⨁ (i : ι), 𝒜 i) (⨁ (i : ι), ℬ i)).flip ((lof R ι ℬ 0) b) = (mk R (⨁ (i : ι), ℬ i) (⨁ (i : ι), 𝒜 i)) ((lof R ι ℬ 0) b)
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝¹¹ : CommSemiring ι<VAR>inst✝¹⁰ : Module ι (Additive ℤˣ)<VAR>inst✝⁹ : DecidableEq ι<VAR>𝒜 : ι → Type u_5<VAR>ℬ : ι → Type u_6<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : (i : ι) → AddCommGroup (𝒜 i)<VAR>inst✝⁶ : (i : ι) → AddCommGroup (ℬ i)<VAR>inst✝⁵ : (i : ι) → Module R (𝒜 i)<VAR>inst✝⁴ : (i : ι) → Module R (ℬ i)<VAR>inst✝³ : DirectSum.GRing 𝒜<VAR>inst✝² : DirectSum.GRing ℬ<VAR>inst✝¹ : DirectSum.GAlgebra R 𝒜<VAR>inst✝ : DirectSum.GAlgebra R ℬ<VAR>a✝ : ⨁ (i : ι), 𝒜 i<VAR>b : ℬ 0<VAR>i : ι<VAR>a : 𝒜 i<GOAL>(gradedComm R 𝒜 ℬ) ((lof R ι 𝒜 i) a ⊗ₜ[R] (lof R ι ℬ 0) b) = (lof R ι ℬ 0) b ⊗ₜ[R] (lof R ι 𝒜 i) a
<VAR>B : Type u<VAR>inst✝ : Bicategory B<VAR>a b c d e : B<VAR>f : a ⟶ b<VAR>g : b ⟶ c<GOAL>(λ_ f).hom ▷ g = (α_ (𝟙 a) f g).hom ≫ (λ_ (f ≫ g)).hom
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>inst✝⁹ : CommRing K<VAR>inst✝⁸ : CommRing L<VAR>inst✝⁷ : CommRing M<VAR>inst✝⁶ : CommRing N<VAR>i : K →+* L<VAR>j : K →+* M<VAR>k : K →+* N<VAR>f : L →+* M<VAR>g : L →+* N<VAR>p : ℕ<VAR>inst✝⁵ : ExpChar K p<VAR>inst✝⁴ : ExpChar L p<VAR>inst✝³ : ExpChar M p<VAR>inst✝² : ExpChar N p<VAR>inst✝¹ : PerfectRing M p<VAR>inst✝ : IsPRadical i p<VAR>x : K<GOAL>(lift i j p) (i x) = j x
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>inst✝⁹ : CommRing K<VAR>inst✝⁸ : CommRing L<VAR>inst✝⁷ : CommRing M<VAR>inst✝⁶ : CommRing N<VAR>i : K →+* L<VAR>j : K →+* M<VAR>k : K →+* N<VAR>f : L →+* M<VAR>g : L →+* N<VAR>p : ℕ<VAR>inst✝⁵ : ExpChar K p<VAR>inst✝⁴ : ExpChar L p<VAR>inst✝³ : ExpChar M p<VAR>inst✝² : ExpChar N p<VAR>inst✝¹ : PerfectRing M p<VAR>inst✝ : IsPRadical i p<VAR>x : K<GOAL>(RingEquiv.refl M).symm (j x) = j x
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : Type x<VAR>inst✝ : Distrib R<VAR>a x y x' y' : R<VAR>h : SemiconjBy a x y<VAR>h' : SemiconjBy a x' y'<GOAL>SemiconjBy a (x + x') (y + y')
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>inst✝¹ : Group G<VAR>inst✝ : Group G'<VAR>H K L : Subgroup G<VAR>hH : H.index ≠ 0<VAR>hK : K.index ≠ 0<GOAL>(H ⊓ K).index ≠ 0
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>inst✝¹ : Group G<VAR>inst✝ : Group G'<VAR>H K L : Subgroup G<VAR>hH : H.relindex ⊤ ≠ 0<VAR>hK : K.relindex ⊤ ≠ 0<GOAL>(H ⊓ K).relindex ⊤ ≠ 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>σ : Type u_3<VAR>τ : Type u_4<VAR>inst✝ : TopologicalSpace α<VAR>F : Realizer α<VAR>s : F.σ<VAR>a : α<VAR>m : a ∈ F.F.f s<GOAL>𝓝 a ≤ 𝓟 (F.F.f s)
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Field E<VAR>inst✝² : Algebra F E<VAR>K : Type w<VAR>inst✝¹ : Field K<VAR>inst✝ : Algebra F K<VAR>f : F[X]<GOAL>natSepDegree 0 = 0
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>t : Set (PrimeSpectrum R)<VAR>f : R<GOAL>f ∈ ↑(vanishingIdeal t) ↔ f ∈ {f | ∀ x ∈ t, f ∈ x.asIdeal}
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>t : Set (PrimeSpectrum R)<VAR>f : R<GOAL>(∀ (i : PrimeSpectrum R), f ∈ ⨅ (_ : i ∈ t), i.asIdeal) ↔ f ∈ {f | ∀ x ∈ t, f ∈ x.asIdeal}
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>t : Set (PrimeSpectrum R)<VAR>f : R<GOAL>∀ (a : PrimeSpectrum R), f ∈ ⨅ (_ : a ∈ t), a.asIdeal ↔ a ∈ t → f ∈ a.asIdeal
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>t : Set (PrimeSpectrum R)<VAR>f : R<VAR>x : PrimeSpectrum R<GOAL>f ∈ ⨅ (_ : x ∈ t), x.asIdeal ↔ x ∈ t → f ∈ x.asIdeal
<VAR>α : Type u<VAR>inst✝² : Group α<VAR>inst✝¹ : LT α<VAR>inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>a b c : α<GOAL>a⁻¹ < 1 ↔ 1 < a
<VAR>α : Type u_1<VAR>inst✝ : OrderedCancelCommMonoid α<VAR>s t : Set α<VAR>a✝ : α<VAR>x y : ↑(s.mulAntidiagonal t a✝)<VAR>hs : s.IsPWO<VAR>ht : t.IsPWO<VAR>a : α<GOAL>(s.mulAntidiagonal t a).Finite
<VAR>α : Type u_1<VAR>inst✝ : OrderedCancelCommMonoid α<VAR>s t : Set α<VAR>a✝ : α<VAR>x y : ↑(s.mulAntidiagonal t a✝)<VAR>hs : s.IsPWO<VAR>ht : t.IsPWO<VAR>a : α<VAR>h : (s.mulAntidiagonal t a).Infinite<GOAL>False
<VAR>α : Type u_1<VAR>inst✝ : OrderedCancelCommMonoid α<VAR>s t : Set α<VAR>a✝ : α<VAR>x y : ↑(s.mulAntidiagonal t a✝)<VAR>hs : s.IsPWO<VAR>ht : t.IsPWO<VAR>a : α<VAR>h : (s.mulAntidiagonal t a).Infinite<VAR>h1 : (s.mulAntidiagonal t a).PartiallyWellOrderedOn (Prod.fst ⁻¹'o fun x x_1 => x ≤ x_1)<VAR>h2 : (s.mulAntidiagonal t a).PartiallyWellOrderedOn (Prod.snd ⁻¹'o fun x x_1 => x ≤ x_1)<GOAL>False
<VAR>α : Type u_1<VAR>inst✝ : OrderedCancelCommMonoid α<VAR>s t : Set α<VAR>a✝ : α<VAR>x y : ↑(s.mulAntidiagonal t a✝)<VAR>hs : s.IsPWO<VAR>ht : t.IsPWO<VAR>a : α<VAR>h : (s.mulAntidiagonal t a).Infinite<VAR>h1 : (s.mulAntidiagonal t a).PartiallyWellOrderedOn (Prod.fst ⁻¹'o fun x x_1 => x ≤ x_1)<VAR>h2 : (s.mulAntidiagonal t a).PartiallyWellOrderedOn (Prod.snd ⁻¹'o fun x x_1 => x ≤ x_1)<VAR>g : ℕ ↪o ℕ<VAR>hg : ∀ (m n : ℕ), m ≤ n → (Prod.fst ⁻¹'o fun x x_1 => x ≤ x_1) ↑((Infinite.natEmbedding (s.mulAntidiagonal t a) h) (g m)) ↑((Infinite.natEmbedding (s.mulAntidiagonal t a) h) (g n))<GOAL>False
<VAR>α : Type u_1<VAR>inst✝ : OrderedCancelCommMonoid α<VAR>s t : Set α<VAR>a✝ : α<VAR>x y : ↑(s.mulAntidiagonal t a✝)<VAR>hs : s.IsPWO<VAR>ht : t.IsPWO<VAR>a : α<VAR>h : (s.mulAntidiagonal t a).Infinite<VAR>h1 : (s.mulAntidiagonal t a).PartiallyWellOrderedOn (Prod.fst ⁻¹'o fun x x_1 => x ≤ x_1)<VAR>h2 : (s.mulAntidiagonal t a).PartiallyWellOrderedOn (Prod.snd ⁻¹'o fun x x_1 => x ≤ x_1)<VAR>g : ℕ ↪o ℕ<VAR>hg : ∀ (m n : ℕ), m ≤ n → (Prod.fst ⁻¹'o fun x x_1 => x ≤ x_1) ↑((Infinite.natEmbedding (s.mulAntidiagonal t a) h) (g m)) ↑((Infinite.natEmbedding (s.mulAntidiagonal t a) h) (g n))<VAR>m n : ℕ<VAR>mn : m < n<VAR>h2' : (Prod.snd ⁻¹'o fun x x_1 => x ≤ x_1) ↑((Infinite.natEmbedding (s.mulAntidiagonal t a) h) (g m)) ↑((Infinite.natEmbedding (s.mulAntidiagonal t a) h) (g n))<GOAL>False
<VAR>α : Type u_1<VAR>inst✝ : OrderedCancelCommMonoid α<VAR>s t : Set α<VAR>a✝ : α<VAR>x y : ↑(s.mulAntidiagonal t a✝)<VAR>hs : s.IsPWO<VAR>ht : t.IsPWO<VAR>a : α<VAR>h : (s.mulAntidiagonal t a).Infinite<VAR>h1 : (s.mulAntidiagonal t a).PartiallyWellOrderedOn (Prod.fst ⁻¹'o fun x x_1 => x ≤ x_1)<VAR>h2 : (s.mulAntidiagonal t a).PartiallyWellOrderedOn (Prod.snd ⁻¹'o fun x x_1 => x ≤ x_1)<VAR>g : ℕ ↪o ℕ<VAR>hg : ∀ (m n : ℕ), m ≤ n → (Prod.fst ⁻¹'o fun x x_1 => x ≤ x_1) ↑((Infinite.natEmbedding (s.mulAntidiagonal t a) h) (g m)) ↑((Infinite.natEmbedding (s.mulAntidiagonal t a) h) (g n))<VAR>m n : ℕ<VAR>mn : m < n<VAR>h2' : (Prod.snd ⁻¹'o fun x x_1 => x ≤ x_1) ↑((Infinite.natEmbedding (s.mulAntidiagonal t a) h) (g m)) ↑((Infinite.natEmbedding (s.mulAntidiagonal t a) h) (g n))<GOAL>(Infinite.natEmbedding (s.mulAntidiagonal t a) h) (g m) = (Infinite.natEmbedding (s.mulAntidiagonal t a) h) (g n)
<VAR>E : Type uE<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : FiniteDimensional ℝ E<VAR>H : Type uH<VAR>inst✝³ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : SmoothManifoldWithCorners I M<VAR>c : M<VAR>f : SmoothBumpFunction I c<VAR>x : M<VAR>s : Set M<VAR>hsc : IsClosed s<VAR>hs : s ⊆ support ↑f<GOAL>IsClosed (↑(extChartAt I c) '' s)
<VAR>E : Type uE<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : FiniteDimensional ℝ E<VAR>H : Type uH<VAR>inst✝³ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : SmoothManifoldWithCorners I M<VAR>c : M<VAR>f : SmoothBumpFunction I c<VAR>x : M<VAR>s : Set M<VAR>hsc : IsClosed s<VAR>hs : s ⊆ support ↑f<GOAL>IsClosed (closedBall (↑(extChartAt I c) c) f.rOut ∩ range ↑I ∩ ↑(extChartAt I c).symm ⁻¹' s)
<VAR>E : Type uE<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : FiniteDimensional ℝ E<VAR>H : Type uH<VAR>inst✝³ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : SmoothManifoldWithCorners I M<VAR>c : M<VAR>f : SmoothBumpFunction I c<VAR>x : M<VAR>s : Set M<VAR>hsc : IsClosed s<VAR>hs : s ⊆ support ↑f<GOAL>IsClosed (closedBall (↑(extChartAt I c) c) f.rOut ∩ range ↑I)
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>inst✝¹ : Group G<VAR>inst✝ : Group G'<VAR>H K L : Subgroup G<VAR>h : ¬H.relindex L = 0<GOAL>(H ⊓ K).relindex L ≤ H.relindex L * K.relindex L
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>inst✝¹ : Group G<VAR>inst✝ : Group G'<VAR>H K L : Subgroup G<VAR>h : ¬H.relindex L = 0<GOAL>H.relindex (K ⊓ L) * K.relindex L ≤ H.relindex L * K.relindex L
<VAR>x : ℝ≥0∞<VAR>y : ℝ<VAR>hy : 0 < y<GOAL>x ^ y = ⊤ ↔ x = ⊤
<VAR>n : ℕ<VAR>f : Vector ℕ n → ℕ<VAR>pf : Primrec' f<GOAL>Primrec f
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>F : Type u_6<VAR>inst✝³ : CommMonoid M<VAR>inst✝² : CommMonoid N<VAR>inst✝¹ : DivisionCommMonoid G<VAR>k l : ℕ+<VAR>inst✝ : CommMonoid R<VAR>ζ : ↥(rootsOfUnity k R)<VAR>m : ℕ<GOAL>↑↑(ζ ^ m) = ↑↑ζ ^ m
<VAR>ι✝¹ : Type u_1<VAR>ι' : Type u_2<VAR>R✝ : Type u_3<VAR>R₂ : Type u_4<VAR>K : Type u_5<VAR>M✝ : Type u_6<VAR>M'✝ : Type u_7<VAR>M'' : Type u_8<VAR>V : Type u<VAR>V' : Type u_9<VAR>R : Type u<VAR>M M₁ : Type v<VAR>M' : Type v'<VAR>ι✝ : Type w<VAR>inst✝⁷ : Ring R<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : AddCommGroup M'<VAR>inst✝⁴ : AddCommGroup M₁<VAR>inst✝³ : Nontrivial R<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R M'<VAR>inst✝ : Module R M₁<VAR>ι : Type w<VAR>b : Basis ι R M<VAR>κ : Type w'<VAR>v : κ → M<VAR>i : LinearIndependent R v<VAR>m : i.Maximal<GOAL>⋃ k, ↑(b.repr (v k)).support = Set.univ
<VAR>ι✝¹ : Type u_1<VAR>ι' : Type u_2<VAR>R✝ : Type u_3<VAR>R₂ : Type u_4<VAR>K : Type u_5<VAR>M✝ : Type u_6<VAR>M'✝ : Type u_7<VAR>M'' : Type u_8<VAR>V : Type u<VAR>V' : Type u_9<VAR>R : Type u<VAR>M M₁ : Type v<VAR>M' : Type v'<VAR>ι✝ : Type w<VAR>inst✝⁷ : Ring R<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : AddCommGroup M'<VAR>inst✝⁴ : AddCommGroup M₁<VAR>inst✝³ : Nontrivial R<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R M'<VAR>inst✝ : Module R M₁<VAR>ι : Type w<VAR>b : Basis ι R M<VAR>κ : Type w'<VAR>v : κ → M<VAR>i : LinearIndependent R v<VAR>m : i.Maximal<VAR>h : ¬⋃ k, ↑(b.repr (v k)).support = Set.univ<GOAL>False
<VAR>ι✝¹ : Type u_1<VAR>ι' : Type u_2<VAR>R✝ : Type u_3<VAR>R₂ : Type u_4<VAR>K : Type u_5<VAR>M✝ : Type u_6<VAR>M'✝ : Type u_7<VAR>M'' : Type u_8<VAR>V : Type u<VAR>V' : Type u_9<VAR>R : Type u<VAR>M M₁ : Type v<VAR>M' : Type v'<VAR>ι✝ : Type w<VAR>inst✝⁷ : Ring R<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : AddCommGroup M'<VAR>inst✝⁴ : AddCommGroup M₁<VAR>inst✝³ : Nontrivial R<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R M'<VAR>inst✝ : Module R M₁<VAR>ι : Type w<VAR>b : Basis ι R M<VAR>κ : Type w'<VAR>v : κ → M<VAR>i : LinearIndependent R v<VAR>m : i.Maximal<VAR>h : ∃ a, ∀ (x : κ), (b.repr (v x)) a = 0<GOAL>False
<VAR>ι✝¹ : Type u_1<VAR>ι' : Type u_2<VAR>R✝ : Type u_3<VAR>R₂ : Type u_4<VAR>K : Type u_5<VAR>M✝ : Type u_6<VAR>M'✝ : Type u_7<VAR>M'' : Type u_8<VAR>V : Type u<VAR>V' : Type u_9<VAR>R : Type u<VAR>M M₁ : Type v<VAR>M' : Type v'<VAR>ι✝ : Type w<VAR>inst✝⁷ : Ring R<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : AddCommGroup M'<VAR>inst✝⁴ : AddCommGroup M₁<VAR>inst✝³ : Nontrivial R<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R M'<VAR>inst✝ : Module R M₁<VAR>ι : Type w<VAR>b : Basis ι R M<VAR>κ : Type w'<VAR>v : κ → M<VAR>i : LinearIndependent R v<VAR>m : i.Maximal<VAR>b' : ι<VAR>w : ∀ (x : κ), (b.repr (v x)) b' = 0<VAR>v' : Option κ → M := fun o => o.elim (b b') v<GOAL>False
<VAR>ι✝¹ : Type u_1<VAR>ι' : Type u_2<VAR>R✝ : Type u_3<VAR>R₂ : Type u_4<VAR>K : Type u_5<VAR>M✝ : Type u_6<VAR>M'✝ : Type u_7<VAR>M'' : Type u_8<VAR>V : Type u<VAR>V' : Type u_9<VAR>R : Type u<VAR>M M₁ : Type v<VAR>M' : Type v'<VAR>ι✝ : Type w<VAR>inst✝⁷ : Ring R<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : AddCommGroup M'<VAR>inst✝⁴ : AddCommGroup M₁<VAR>inst✝³ : Nontrivial R<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R M'<VAR>inst✝ : Module R M₁<VAR>ι : Type w<VAR>b : Basis ι R M<VAR>κ : Type w'<VAR>v : κ → M<VAR>i : LinearIndependent R v<VAR>m : i.Maximal<VAR>b' : ι<VAR>w : ∀ (x : κ), (b.repr (v x)) b' = 0<VAR>v' : Option κ → M := fun o => o.elim (b b') v<VAR>r : range v ⊆ range v'<GOAL>False
<VAR>ι✝¹ : Type u_1<VAR>ι' : Type u_2<VAR>R✝ : Type u_3<VAR>R₂ : Type u_4<VAR>K : Type u_5<VAR>M✝ : Type u_6<VAR>M'✝ : Type u_7<VAR>M'' : Type u_8<VAR>V : Type u<VAR>V' : Type u_9<VAR>R : Type u<VAR>M M₁ : Type v<VAR>M' : Type v'<VAR>ι✝ : Type w<VAR>inst✝⁷ : Ring R<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : AddCommGroup M'<VAR>inst✝⁴ : AddCommGroup M₁<VAR>inst✝³ : Nontrivial R<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R M'<VAR>inst✝ : Module R M₁<VAR>ι : Type w<VAR>b : Basis ι R M<VAR>κ : Type w'<VAR>v : κ → M<VAR>i : LinearIndependent R v<VAR>m : i.Maximal<VAR>b' : ι<VAR>w : ∀ (x : κ), (b.repr (v x)) b' = 0<VAR>v' : Option κ → M := fun o => o.elim (b b') v<VAR>r : range v ⊆ range v'<VAR>r' : b b' ∉ range v<GOAL>False
<VAR>ι✝¹ : Type u_1<VAR>ι' : Type u_2<VAR>R✝ : Type u_3<VAR>R₂ : Type u_4<VAR>K : Type u_5<VAR>M✝ : Type u_6<VAR>M'✝ : Type u_7<VAR>M'' : Type u_8<VAR>V : Type u<VAR>V' : Type u_9<VAR>R : Type u<VAR>M M₁ : Type v<VAR>M' : Type v'<VAR>ι✝ : Type w<VAR>inst✝⁷ : Ring R<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : AddCommGroup M'<VAR>inst✝⁴ : AddCommGroup M₁<VAR>inst✝³ : Nontrivial R<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R M'<VAR>inst✝ : Module R M₁<VAR>ι : Type w<VAR>b : Basis ι R M<VAR>κ : Type w'<VAR>v : κ → M<VAR>i : LinearIndependent R v<VAR>m : i.Maximal<VAR>b' : ι<VAR>w : ∀ (x : κ), (b.repr (v x)) b' = 0<VAR>v' : Option κ → M := fun o => o.elim (b b') v<VAR>r : range v ⊆ range v'<VAR>r' : b b' ∉ range v<VAR>r'' : range v ≠ range v'<GOAL>False