ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>E : Type u_1<VAR>ι : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>U K : Set ℂ<VAR>z : ℂ<VAR>M r δ : ℝ<VAR>φ : Filter ι<VAR>F : ι → ℂ → E<VAR>f g : ℂ → E<VAR>hr : 0 < r<VAR>hf : ∀ w ∈ sphere z r, ‖f w‖ ≤ M<VAR>hM : 0 ≤ M<VAR>h1 : ∀ w ∈ sphere z r, ‖((w - z) ^ 2)⁻¹ • f w‖ ≤ M / r ^ 2<VAR>h2 : ‖∮ (z_1 : ℂ) in C(z, r), ((z_1 - z) ^ 2)⁻¹ • f z_1‖ ≤ 2 * π * r * (M / r ^ 2)<GOAL>‖cderiv r f z‖ ≤ M / r
<VAR>E : Type u_1<VAR>ι : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>U K : Set ℂ<VAR>z : ℂ<VAR>M r δ : ℝ<VAR>φ : Filter ι<VAR>F : ι → ℂ → E<VAR>f g : ℂ → E<VAR>hr : 0 < r<VAR>hf : ∀ w ∈ sphere z r, ‖f w‖ ≤ M<VAR>hM : 0 ≤ M<VAR>h1 : ∀ w ∈ sphere z r, ‖((w - z) ^ 2)⁻¹ • f w‖ ≤ M / r ^ 2<VAR>h2 : ‖∮ (z_1 : ℂ) in C(z, r), ((z_1 - z) ^ 2)⁻¹ • f z_1‖ ≤ 2 * π * r * (M / r ^ 2)<GOAL>‖(2 * ↑π * I)⁻¹‖ * ‖∮ (w : ℂ) in C(z, r), ((w - z) ^ 2)⁻¹ • f w‖ ≤ M / r
<VAR>E : Type u_1<VAR>ι : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>U K : Set ℂ<VAR>z : ℂ<VAR>M r δ : ℝ<VAR>φ : Filter ι<VAR>F : ι → ℂ → E<VAR>f g : ℂ → E<VAR>hr : 0 < r<VAR>hf : ∀ w ∈ sphere z r, ‖f w‖ ≤ M<VAR>hM : 0 ≤ M<VAR>h1 : ∀ w ∈ sphere z r, ‖((w - z) ^ 2)⁻¹ • f w‖ ≤ M / r ^ 2<VAR>h2 : ‖∮ (z_1 : ℂ) in C(z, r), ((z_1 - z) ^ 2)⁻¹ • f z_1‖ ≤ 2 * π * r * (M / r ^ 2)<GOAL>‖(2 * ↑π * I)⁻¹‖ * (2 * π * r * (M / r ^ 2)) = M / r
<VAR>E : Type u_1<VAR>ι : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>U K : Set ℂ<VAR>z : ℂ<VAR>M r δ : ℝ<VAR>φ : Filter ι<VAR>F : ι → ℂ → E<VAR>f g : ℂ → E<VAR>hr : 0 < r<VAR>hf : ∀ w ∈ sphere z r, ‖f w‖ ≤ M<VAR>hM : 0 ≤ M<VAR>h1 : ∀ w ∈ sphere z r, ‖((w - z) ^ 2)⁻¹ • f w‖ ≤ M / r ^ 2<VAR>h2 : ‖∮ (z_1 : ℂ) in C(z, r), ((z_1 - z) ^ 2)⁻¹ • f z_1‖ ≤ 2 * π * r * (M / r ^ 2)<GOAL>2 * π * r * M * r = M * (2 * π * r ^ 2)
<VAR>R : Type u_1<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : NoZeroDivisors R<VAR>r : R<GOAL>span {r} ∈ (Ideal R)⁰ ↔ r ∈ R⁰
<VAR>R : Type u_1<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : NoZeroDivisors R<VAR>r : R<VAR>h✝ : Subsingleton R<GOAL>span {r} ∈ (Ideal R)⁰ ↔ r ∈ R⁰
<VAR>R : Type u_1<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : NoZeroDivisors R<VAR>r : R<VAR>h✝ : Nontrivial R<GOAL>span {r} ∈ (Ideal R)⁰ ↔ r ∈ R⁰
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>A : Type u_4<VAR>B : Type u_5<VAR>α : Type u_6<VAR>β : Type u_7<VAR>γ : Type u_8<VAR>δ : Type u_9<VAR>inst✝² : Monoid M<VAR>inst✝¹ : AddGroup A<VAR>inst✝ : DistribMulAction M A<VAR>r : M<VAR>x y : A<GOAL>r • (x - y) = r • x - r • y
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>inst✝ : MeasurableSpace E<VAR>x✝ : MeasurableSpace Ω<VAR>ℙ : Measure Ω<VAR>μ : Measure E<VAR>X : Ω → E<VAR>hX : ¬AEMeasurable X ℙ<GOAL>pdf X ℙ μ =ᶠ[ae μ] 0
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>inst✝ : MeasurableSpace E<VAR>x✝ : MeasurableSpace Ω<VAR>ℙ : Measure Ω<VAR>μ : Measure E<VAR>X : Ω → E<VAR>hX : ¬AEMeasurable X ℙ<GOAL>rnDeriv 0 μ =ᶠ[ae μ] 0
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>𝒜 ℬ : Finset (Finset α)<VAR>s✝ : Finset α<VAR>a : α<VAR>h : IsLowerSet ↑𝒜<VAR>s t : Finset α<VAR>hts : t ≤ s<GOAL>s ∈ ↑(Finset.nonMemberSubfamily a 𝒜) → t ∈ ↑(Finset.nonMemberSubfamily a 𝒜)
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>𝒜 ℬ : Finset (Finset α)<VAR>s✝ : Finset α<VAR>a : α<VAR>h : IsLowerSet ↑𝒜<VAR>s t : Finset α<VAR>hts : t ≤ s<GOAL>s ∈ 𝒜 ∧ a ∉ s → t ∈ 𝒜 ∧ a ∉ t
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>f : α → α<VAR>a : α<VAR>tl : List α<VAR>r : Array α<GOAL>go f (tl ++ [a]) r = r.toListAppend (go f (tl ++ [a]) #[])
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>G : Type u_4<VAR>M : Type u_5<VAR>N : Type u_6<VAR>inst✝² : CommMonoid M<VAR>inst✝¹ : CommMonoid N<VAR>f : α → M<VAR>s : Set α<VAR>inst✝ : DecidablePred fun x => x ∈ s<VAR>hf : (mulSupport f).Finite<VAR>x : α<GOAL>x ∈ s ∩ mulSupport f ↔ x ∈ ↑(Finset.filter (fun x => x ∈ s) hf.toFinset) ∩ mulSupport f
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>ι : Type u_6<VAR>inst✝⁶ : OrderedSemiring 𝕜<VAR>inst✝⁵ : AddCommMonoid E<VAR>inst✝⁴ : AddCommMonoid F<VAR>inst✝³ : LinearOrderedCancelAddCommMonoid β<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : Module 𝕜 β<VAR>inst✝ : OrderedSMul 𝕜 β<VAR>s : Set E<VAR>f g : E → β<VAR>hf : ConvexOn 𝕜 s f<VAR>x y : E<VAR>hx : x ∈ s<VAR>hy : y ∈ s<VAR>a b : 𝕜<VAR>ha : 0 < a<VAR>hb : 0 < b<VAR>hab : a + b = 1<VAR>hxz : f x < f (a • x + b • y)<GOAL>f (a • x + b • y) < f y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort u_5<VAR>κ : ι → Sort u_6<VAR>inst✝¹ : PartialOrder α<VAR>inst✝ : PartialOrder β<VAR>s t : NonemptyInterval α<VAR>x : α × α<VAR>a b : α<GOAL>b ∈ pure a ↔ b = a
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedField α<VAR>a✝ a b c : α<VAR>h : 0 < c<GOAL>(fun x => c * x) ⁻¹' Ioo a b = Ioo (a / c) (b / c)
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : Affine R<GOAL>evalEval 0 0 W.polynomialX = -W.a₄
<VAR>G : Type u_1<VAR>M : Type u_2<VAR>F : Type u_3<VAR>inst✝⁵ : Group G<VAR>inst✝⁴ : Fintype G<VAR>inst✝³ : Monoid M<VAR>inst✝² : DecidableEq M<VAR>inst✝¹ : FunLike F G M<VAR>inst✝ : MonoidHomClass F G M<VAR>f : F<VAR>x y : G<GOAL>(filter (fun g => f g = f x) univ).card = (filter (fun g => f g = f y) univ).card
<VAR>G : Type u_1<VAR>M : Type u_2<VAR>F : Type u_3<VAR>inst✝⁵ : Group G<VAR>inst✝⁴ : Fintype G<VAR>inst✝³ : Monoid M<VAR>inst✝² : DecidableEq M<VAR>inst✝¹ : FunLike F G M<VAR>inst✝ : MonoidHomClass F G M<VAR>f : F<VAR>x y : G<GOAL>(filter (fun g => f g = f x) univ).card = (filter (fun g => f g = f ((fun x_1 => x * x_1) y)) univ).card
<VAR>G : Type u_1<VAR>M : Type u_2<VAR>F : Type u_3<VAR>inst✝⁵ : Group G<VAR>inst✝⁴ : Fintype G<VAR>inst✝³ : Monoid M<VAR>inst✝² : DecidableEq M<VAR>inst✝¹ : FunLike F G M<VAR>inst✝ : MonoidHomClass F G M<VAR>f : F<VAR>x y : G<GOAL>(filter ((fun g => f g = f x) ∘ ⇑(Equiv.toEmbedding (Equiv.mulRight y⁻¹))) univ).card = (filter (fun g => f g = f ((fun x_1 => x * x_1) y)) univ).card
<VAR>G : Type u_1<VAR>M : Type u_2<VAR>F : Type u_3<VAR>inst✝⁵ : Group G<VAR>inst✝⁴ : Fintype G<VAR>inst✝³ : Monoid M<VAR>inst✝² : DecidableEq M<VAR>inst✝¹ : FunLike F G M<VAR>inst✝ : MonoidHomClass F G M<VAR>f : F<VAR>x y g : G<GOAL>((fun g => f g = f x) ∘ ⇑(Equiv.toEmbedding (Equiv.mulRight y⁻¹))) g ↔ f g = f ((fun x_1 => x * x_1) y)
<VAR>G : Type u_1<VAR>M : Type u_2<VAR>F : Type u_3<VAR>inst✝⁵ : Group G<VAR>inst✝⁴ : Fintype G<VAR>inst✝³ : Monoid M<VAR>inst✝² : DecidableEq M<VAR>inst✝¹ : FunLike F G M<VAR>inst✝ : MonoidHomClass F G M<VAR>f : F<VAR>x y g : G<GOAL>f g * f y⁻¹ = f x ↔ f g = f x * f y
<VAR>G : Type u_1<VAR>M : Type u_2<VAR>F : Type u_3<VAR>inst✝⁵ : Group G<VAR>inst✝⁴ : Fintype G<VAR>inst✝³ : Monoid M<VAR>inst✝² : DecidableEq M<VAR>inst✝¹ : FunLike F G M<VAR>inst✝ : MonoidHomClass F G M<VAR>f : F<VAR>x y g : G<VAR>f' : G →* M := ↑f<GOAL>f' g * f' y⁻¹ = f' x ↔ f' g = f' x * f' y
<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>inst✝ : Subsingleton E'<VAR>c : ℝ<VAR>hc : 0 < c<GOAL>∀ᶠ (x : α) in l, ‖f' x‖ ≤ c * ‖g' x‖
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>p : PMF α<VAR>f : (a : α) → a ∈ p.support → PMF β<VAR>s : Set β<GOAL>(p.bindOnSupport f).toOuterMeasure s = ∑' (a : α), p a * if h : p a = 0 then 0 else (f a h).toOuterMeasure s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>p : PMF α<VAR>f : (a : α) → a ∈ p.support → PMF β<VAR>s : Set β<GOAL>(∑' (x : β), if x ∈ s then ∑' (a : α), p a * if h : p a = 0 then 0 else (f a h) x else 0) = ∑' (a : α), p a * if h : p a = 0 then 0 else ∑' (x : β), if x ∈ s then (f a ⋯) x else 0
<VAR>𝕜 : Type u_1<VAR>inst✝² : RCLike 𝕜<VAR>n : Type u_2<VAR>inst✝¹ : Fintype n<VAR>A : Matrix n n 𝕜<VAR>inst✝ : DecidableEq n<VAR>hA : A.IsHermitian<GOAL>A.rank = Fintype.card { i // hA.eigenvalues i ≠ 0 }
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>β : Type u_4<VAR>inst✝⁴ : LinearOrderedField 𝕜<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : AddCommGroup F<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : Module 𝕜 F<VAR>s : Set E<VAR>h_conv : Convex 𝕜 s<VAR>p q : 𝕜<VAR>hp : 0 ≤ p<VAR>hq : 0 ≤ q<VAR>v₁ : E<VAR>h₁ : v₁ ∈ s<VAR>v₂ : E<VAR>h₂ : v₂ ∈ s<GOAL>(fun x x_1 => x + x_1) ((fun x => p • x) v₁) ((fun x => q • x) v₂) ∈ (p + q) • s
<VAR>V : Type u<VAR>inst✝² : Category.{v, u} V<VAR>inst✝¹ : HasZeroMorphisms V<VAR>inst✝ : HasZeroObject V<VAR>C : ChainComplex V ℕ<VAR>X : V<VAR>φ : C ⟶ (single₀ V).obj X<GOAL>C.d 1 0 ≫ φ.f 0 = 0
<VAR>V : Type u<VAR>inst✝² : Category.{v, u} V<VAR>inst✝¹ : HasZeroMorphisms V<VAR>inst✝ : HasZeroObject V<VAR>C : ChainComplex V ℕ<VAR>X : V<VAR>f : { f // C.d 1 0 ≫ f = 0 }<VAR>i : ℕ<VAR>hi : (ComplexShape.down ℕ).Rel i 0<GOAL>C.d i 0 ≫ ↑f = 0
<VAR>V : Type u<VAR>inst✝² : Category.{v, u} V<VAR>inst✝¹ : HasZeroMorphisms V<VAR>inst✝ : HasZeroObject V<VAR>C : ChainComplex V ℕ<VAR>X : V<VAR>f : { f // C.d 1 0 ≫ f = 0 }<VAR>hi : (ComplexShape.down ℕ).Rel 1 0<GOAL>C.d 1 0 ≫ ↑f = 0
<VAR>R : Type u_1<VAR>inst✝²⁰ : CommSemiring R<VAR>R' : Type u_2<VAR>inst✝¹⁹ : Monoid R'<VAR>R'' : Type u_3<VAR>inst✝¹⁸ : Semiring R''<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>Q : Type u_7<VAR>S : Type u_8<VAR>T : Type u_9<VAR>inst✝¹⁷ : AddCommMonoid M<VAR>inst✝¹⁶ : AddCommMonoid N<VAR>inst✝¹⁵ : AddCommMonoid P<VAR>inst✝¹⁴ : AddCommMonoid Q<VAR>inst✝¹³ : AddCommMonoid S<VAR>inst✝¹² : AddCommMonoid T<VAR>inst✝¹¹ : Module R M<VAR>inst✝¹⁰ : Module R N<VAR>inst✝⁹ : Module R P<VAR>inst✝⁸ : Module R Q<VAR>inst✝⁷ : Module R S<VAR>inst✝⁶ : Module R T<VAR>inst✝⁵ : DistribMulAction R' M<VAR>inst✝⁴ : Module R'' M<VAR>P' : Type u_10<VAR>Q' : Type u_11<VAR>inst✝³ : AddCommMonoid P'<VAR>inst✝² : Module R P'<VAR>inst✝¹ : AddCommMonoid Q'<VAR>inst✝ : Module R Q'<VAR>r : R<VAR>f : M →ₗ[R] P<VAR>g : N →ₗ[R] Q<VAR>x✝¹ : M<VAR>x✝ : N<GOAL>(((mk R M N).compr₂ (map f (r • g))) x✝¹) x✝ = (((mk R M N).compr₂ (r • map f g)) x✝¹) x✝
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>inst✝ : LE α<VAR>s t : LowerSet α<VAR>a : α<VAR>S : Set (LowerSet α)<GOAL>↑(sSup S).compl = ↑(⨆ s ∈ S, s.compl)
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>a b : α<VAR>n : Nat<VAR>h✝ : a = b<GOAL>count a (replicate n b) = n
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>a b : α<VAR>n : Nat<VAR>h✝ : ¬a = b<GOAL>count a (replicate n b) = 0
<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>inst✝ : Nontrivial A<VAR>pb : PowerBasis A S<GOAL>(minpoly A pb.gen).natDegree = pb.dim
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : Semiring A<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : Semiring B<VAR>inst✝ : Algebra R B<VAR>S : Subalgebra R A<VAR>f : A →ₐ[R] B<GOAL>(f.comp S.val).range = map f S
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ✝ μ : Measure α<VAR>inst✝ : SFinite μ<VAR>s : Set α<GOAL>μ.toFinite s = (μ.toFiniteAux Set.univ)⁻¹ * μ.toFiniteAux s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>K : Type u_3<VAR>inst✝ : DivisionRing K<VAR>a✝ b✝ c d a b : K<VAR>h : b ≠ 0<GOAL>(b - a) / b = 1 - a / b
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>f : R[X]<VAR>h : f.eraseLead = 0<GOAL>f.nextCoeff = 0
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>f : R[X]<VAR>h : f.eraseLead = 0<VAR>h₂ : ¬f.nextCoeff = 0<GOAL>False
<VAR>α : Type u_1<VAR>inst✝⁶ : Zero α<VAR>inst✝⁵ : LinearOrder α<VAR>a✝ : α<VAR>β : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : Zero β<VAR>inst✝³ : Preorder β<VAR>inst✝² : DecidableRel fun x x_1 => x < x_1<VAR>inst✝¹ : FunLike F α β<VAR>inst✝ : ZeroHomClass F α β<VAR>f : F<VAR>hf : StrictMono ⇑f<VAR>a : α<GOAL>sign (f a) = sign a
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsJacobson R<VAR>P : Ideal R[X]<VAR>hP : P.IsMaximal<VAR>inst✝ : Nontrivial R<VAR>hR : IsJacobson R<VAR>hP' : ∀ (x : R), C x ∈ P → x = 0<GOAL>((Quotient.mk P).comp C).IsIntegral
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsJacobson R<VAR>P : Ideal R[X]<VAR>hP : P.IsMaximal<VAR>inst✝ : Nontrivial R<VAR>hR : IsJacobson R<VAR>hP' : ∀ (x : R), C x ∈ P → x = 0<GOAL>(quotientMap P C ⋯).IsIntegral
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsJacobson R<VAR>P : Ideal R[X]<VAR>hP : P.IsMaximal<VAR>inst✝ : Nontrivial R<VAR>hR : IsJacobson R<VAR>hP' : ∀ (x : R), C x ∈ P → x = 0<VAR>P' : Ideal R := comap C P<GOAL>(quotientMap P C ⋯).IsIntegral
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsJacobson R<VAR>P : Ideal R[X]<VAR>hP : P.IsMaximal<VAR>inst✝ : Nontrivial R<VAR>hR : IsJacobson R<VAR>hP' : ∀ (x : R), C x ∈ P → x = 0<VAR>P' : Ideal R := comap C P<VAR>pX : R[X]<VAR>hpX : pX ∈ P<VAR>hp0 : Polynomial.map (Quotient.mk (comap C P)) pX ≠ 0<GOAL>(quotientMap P C ⋯).IsIntegral
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsJacobson R<VAR>P : Ideal R[X]<VAR>hP : P.IsMaximal<VAR>inst✝ : Nontrivial R<VAR>hR : IsJacobson R<VAR>hP' : ∀ (x : R), C x ∈ P → x = 0<VAR>P' : Ideal R := comap C P<VAR>pX : R[X]<VAR>hpX : pX ∈ P<VAR>hp0 : Polynomial.map (Quotient.mk (comap C P)) pX ≠ 0<VAR>a : R ⧸ P' := (Polynomial.map (Quotient.mk P') pX).leadingCoeff<VAR>M : Submonoid (R ⧸ P') := Submonoid.powers a<GOAL>(quotientMap P C ⋯).IsIntegral
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsJacobson R<VAR>P : Ideal R[X]<VAR>hP : P.IsMaximal<VAR>inst✝ : Nontrivial R<VAR>hR : IsJacobson R<VAR>hP' : ∀ (x : R), C x ∈ P → x = 0<VAR>P' : Ideal R := comap C P<VAR>pX : R[X]<VAR>hpX : pX ∈ P<VAR>hp0 : Polynomial.map (Quotient.mk (comap C P)) pX ≠ 0<VAR>a : R ⧸ P' := (Polynomial.map (Quotient.mk P') pX).leadingCoeff<VAR>M : Submonoid (R ⧸ P') := Submonoid.powers a<VAR>φ : R ⧸ P' →+* R[X] ⧸ P := quotientMap P C ⋯<GOAL>(quotientMap P C ⋯).IsIntegral
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsJacobson R<VAR>P : Ideal R[X]<VAR>hP : P.IsMaximal<VAR>inst✝ : Nontrivial R<VAR>hR : IsJacobson R<VAR>hP' : ∀ (x : R), C x ∈ P → x = 0<VAR>P' : Ideal R := comap C P<VAR>pX : R[X]<VAR>hpX : pX ∈ P<VAR>hp0 : Polynomial.map (Quotient.mk (comap C P)) pX ≠ 0<VAR>a : R ⧸ P' := (Polynomial.map (Quotient.mk P') pX).leadingCoeff<VAR>M : Submonoid (R ⧸ P') := Submonoid.powers a<VAR>φ : R ⧸ P' →+* R[X] ⧸ P := quotientMap P C ⋯<VAR>hP'_prime : P'.IsPrime<GOAL>(quotientMap P C ⋯).IsIntegral
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsJacobson R<VAR>P : Ideal R[X]<VAR>hP : P.IsMaximal<VAR>inst✝ : Nontrivial R<VAR>hR : IsJacobson R<VAR>hP' : ∀ (x : R), C x ∈ P → x = 0<VAR>P' : Ideal R := comap C P<VAR>pX : R[X]<VAR>hpX : pX ∈ P<VAR>hp0 : Polynomial.map (Quotient.mk (comap C P)) pX ≠ 0<VAR>a : R ⧸ P' := (Polynomial.map (Quotient.mk P') pX).leadingCoeff<VAR>M : Submonoid (R ⧸ P') := Submonoid.powers a<VAR>φ : R ⧸ P' →+* R[X] ⧸ P := quotientMap P C ⋯<VAR>hP'_prime : P'.IsPrime<VAR>hM : 0 ∉ M<GOAL>(quotientMap P C ⋯).IsIntegral
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsJacobson R<VAR>P : Ideal R[X]<VAR>hP : P.IsMaximal<VAR>inst✝ : Nontrivial R<VAR>hR : IsJacobson R<VAR>hP' : ∀ (x : R), C x ∈ P → x = 0<VAR>P' : Ideal R := comap C P<VAR>pX : R[X]<VAR>hpX : pX ∈ P<VAR>hp0 : Polynomial.map (Quotient.mk (comap C P)) pX ≠ 0<VAR>a : R ⧸ P' := (Polynomial.map (Quotient.mk P') pX).leadingCoeff<VAR>M : Submonoid (R ⧸ P') := Submonoid.powers a<VAR>φ : R ⧸ P' →+* R[X] ⧸ P := quotientMap P C ⋯<VAR>hP'_prime : P'.IsPrime<VAR>hM : 0 ∉ M<VAR>M' : Submonoid (R[X] ⧸ P) := Submonoid.map φ M<GOAL>(quotientMap P C ⋯).IsIntegral
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsJacobson R<VAR>P : Ideal R[X]<VAR>hP : P.IsMaximal<VAR>inst✝ : Nontrivial R<VAR>hR : IsJacobson R<VAR>hP' : ∀ (x : R), C x ∈ P → x = 0<VAR>P' : Ideal R := comap C P<VAR>pX : R[X]<VAR>hpX : pX ∈ P<VAR>hp0 : Polynomial.map (Quotient.mk (comap C P)) pX ≠ 0<VAR>a : R ⧸ P' := (Polynomial.map (Quotient.mk P') pX).leadingCoeff<VAR>M : Submonoid (R ⧸ P') := Submonoid.powers a<VAR>φ : R ⧸ P' →+* R[X] ⧸ P := quotientMap P C ⋯<VAR>hP'_prime : P'.IsPrime<VAR>hM : 0 ∉ M<VAR>M' : Submonoid (R[X] ⧸ P) := Submonoid.map φ M<GOAL>Function.Injective ⇑(algebraMap (R[X] ⧸ P) (Localization M'))
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsJacobson R<VAR>P : Ideal R[X]<VAR>hP : P.IsMaximal<VAR>inst✝ : Nontrivial R<VAR>hR : IsJacobson R<VAR>hP' : ∀ (x : R), C x ∈ P → x = 0<VAR>P' : Ideal R := comap C P<VAR>pX : R[X]<VAR>hpX : pX ∈ P<VAR>hp0 : Polynomial.map (Quotient.mk (comap C P)) pX ≠ 0<VAR>a : R ⧸ P' := (Polynomial.map (Quotient.mk P') pX).leadingCoeff<VAR>M : Submonoid (R ⧸ P') := Submonoid.powers a<VAR>φ : R ⧸ P' →+* R[X] ⧸ P := quotientMap P C ⋯<VAR>hP'_prime : P'.IsPrime<VAR>hM : 0 ∉ M<VAR>M' : Submonoid (R[X] ⧸ P) := Submonoid.map φ M<GOAL>((algebraMap (R[X] ⧸ P) (Localization M')).comp φ).IsIntegral
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : (i : ι) → Zero (β i)<VAR>s : Finset ι<VAR>x : (i : ↑↑s) → β ↑i<VAR>i✝ i i' : ι<VAR>b : β i<GOAL>(single i b) i' = if h : i = i' then Eq.recOn h b else 0
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : (i : ι) → Zero (β i)<VAR>s : Finset ι<VAR>x : (i : ↑↑s) → β ↑i<VAR>i✝ i i' : ι<VAR>b : β i<GOAL>(if h : i' = i then ⋯ ▸ b else 0 i') = if h : i = i' then Eq.recOn h b else 0
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>inst✝¹⁰ : MeasurableSpace α<VAR>inst✝⁹ : MeasurableSpace α'<VAR>inst✝⁸ : MeasurableSpace β<VAR>inst✝⁷ : MeasurableSpace β'<VAR>inst✝⁶ : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : SFinite ν<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : SFinite μ<VAR>E' : Type u_7<VAR>inst✝¹ : NormedAddCommGroup E'<VAR>inst✝ : NormedSpace ℝ E'<VAR>f g : α × β → E<VAR>F : E → E'<VAR>hf : Integrable f (μ.prod ν)<VAR>hg : Integrable g (μ.prod ν)<GOAL>∫ (x : α), F (∫ (y : β), f (x, y) - g (x, y) ∂ν) ∂μ = ∫ (x : α), F (∫ (y : β), f (x, y) ∂ν - ∫ (y : β), g (x, y) ∂ν) ∂μ
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>inst✝¹⁰ : MeasurableSpace α<VAR>inst✝⁹ : MeasurableSpace α'<VAR>inst✝⁸ : MeasurableSpace β<VAR>inst✝⁷ : MeasurableSpace β'<VAR>inst✝⁶ : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : SFinite ν<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : SFinite μ<VAR>E' : Type u_7<VAR>inst✝¹ : NormedAddCommGroup E'<VAR>inst✝ : NormedSpace ℝ E'<VAR>f g : α × β → E<VAR>F : E → E'<VAR>hf : Integrable f (μ.prod ν)<VAR>hg : Integrable g (μ.prod ν)<GOAL>(fun x => F (∫ (y : β), f (x, y) - g (x, y) ∂ν)) =ᶠ[ae μ] fun x => F (∫ (y : β), f (x, y) ∂ν - ∫ (y : β), g (x, y) ∂ν)
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>inst✝¹⁰ : MeasurableSpace α<VAR>inst✝⁹ : MeasurableSpace α'<VAR>inst✝⁸ : MeasurableSpace β<VAR>inst✝⁷ : MeasurableSpace β'<VAR>inst✝⁶ : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : SFinite ν<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : SFinite μ<VAR>E' : Type u_7<VAR>inst✝¹ : NormedAddCommGroup E'<VAR>inst✝ : NormedSpace ℝ E'<VAR>f g : α × β → E<VAR>F : E → E'<VAR>hf : Integrable f (μ.prod ν)<VAR>hg : Integrable g (μ.prod ν)<VAR>a✝ : α<VAR>h2f : Integrable (fun y => f (a✝, y)) ν<VAR>h2g : Integrable (fun y => g (a✝, y)) ν<GOAL>F (∫ (y : β), f (a✝, y) - g (a✝, y) ∂ν) = F (∫ (y : β), f (a✝, y) ∂ν - ∫ (y : β), g (a✝, y) ∂ν)
<VAR>K R : Type v<VAR>V M : Type w<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : Field K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>f : End R M<VAR>p : Submodule R M<VAR>k : ℕ<VAR>μ : R<VAR>hfp : ∀ x ∈ p, f x ∈ p<GOAL>p ⊓ (f.genEigenspace μ) k = Submodule.map p.subtype ((genEigenspace (LinearMap.restrict f hfp) μ) k)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>f g : ι → α → β<VAR>p : ℝ≥0∞<VAR>hf : UnifTight f p μ<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<VAR>hε_top : ¬ε = ⊤<GOAL>∀ᶠ (s : Set α) in μ.cofinite.smallSets, ∀ (i : ι), eLpNorm (s.indicator (f i)) p μ ≤ ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>f g : ι → α → β<VAR>p : ℝ≥0∞<VAR>hf : UnifTight f p μ<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<VAR>hε_top : ¬ε = ⊤<VAR>s : Set α<VAR>hμs : μ s ≠ ⊤<VAR>hfs : ∀ (i : ι), eLpNorm (sᶜ.indicator (f i)) p μ ≤ ↑ε.toNNReal<GOAL>∀ᶠ (s : Set α) in μ.cofinite.smallSets, ∀ (i : ι), eLpNorm (s.indicator (f i)) p μ ≤ ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>f g : ι → α → β<VAR>p : ℝ≥0∞<VAR>hf : UnifTight f p μ<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<VAR>hε_top : ¬ε = ⊤<VAR>s : Set α<VAR>hμs : μ s ≠ ⊤<VAR>hfs : ∀ (i : ι), eLpNorm (sᶜ.indicator (f i)) p μ ≤ ↑ε.toNNReal<GOAL>∀ ⦃s t : Set α⦄, s ⊆ t → (∀ (i : ι), eLpNorm (t.indicator (f i)) p μ ≤ ε) → ∀ (i : ι), eLpNorm (s.indicator (f i)) p μ ≤ ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>f g : ι → α → β<VAR>p : ℝ≥0∞<VAR>hf : UnifTight f p μ<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<VAR>hε_top : ¬ε = ⊤<VAR>s : Set α<VAR>hμs : μ s ≠ ⊤<VAR>hfs : ∀ (i : ι), eLpNorm (sᶜ.indicator (f i)) p μ ≤ ↑ε.toNNReal<GOAL>sᶜ ∈ μ.cofinite
<VAR>q : ℕ+<VAR>w : 1 < q<VAR>this : Fact (1 < ↑q)<GOAL>Fintype.card (X q)ˣ < ↑q ^ 2
<VAR>q : ℕ+<VAR>w : 1 < q<VAR>this : Fact (1 < ↑q)<GOAL>↑q ^ 2 = Fintype.card (X q)
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>inst✝⁵ : AddCommMonoid ι<VAR>inst✝⁴ : DecidableEq ι<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ι → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>x : Submonoid A<VAR>y1 y2 : NumDenSameDeg 𝒜 x<GOAL>(Quotient.mk'' y1 + Quotient.mk'' y2).val = val (Quotient.mk'' y1) + val (Quotient.mk'' y2)
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>inst✝⁵ : AddCommMonoid ι<VAR>inst✝⁴ : DecidableEq ι<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ι → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>x : Submonoid A<VAR>y1 y2 : NumDenSameDeg 𝒜 x<GOAL>Localization.mk ↑(y1 + y2).num ⟨↑(y1 + y2).den, ⋯⟩ = Localization.mk (↑⟨↑y1.den, ⋯⟩ * ↑y2.num + ↑⟨↑y2.den, ⋯⟩ * ↑y1.num) (⟨↑y1.den, ⋯⟩ * ⟨↑y2.den, ⋯⟩)
<VAR>a b c : ℤ<VAR>hab : IsCoprime a b<VAR>k : ℕ<VAR>hk : Odd k<VAR>h : a * b = c ^ k<GOAL>∃ d, a = d ^ k
<VAR>a b c : ℤ<VAR>hab : IsCoprime a b<VAR>k : ℕ<VAR>hk : Odd k<VAR>h : a * b = c ^ k<VAR>d : ℤ<VAR>hd : Associated (d ^ k) a<GOAL>∃ d, a = d ^ k
<VAR>a b c : ℤ<VAR>hab : IsCoprime a b<VAR>k : ℕ<VAR>hk : Odd k<VAR>h : a * b = c ^ k<VAR>d : ℤ<VAR>hd : Associated a (d ^ k)<GOAL>∃ d, a = d ^ k
<VAR>a b c : ℤ<VAR>hab : IsCoprime a b<VAR>k : ℕ<VAR>hk : Odd k<VAR>h : a * b = c ^ k<VAR>d : ℤ<VAR>hd : a = d ^ k ∨ a = (-d) ^ k<GOAL>∃ d, a = d ^ k