ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>E : Type u_1<VAR>inst✝ : MeasurableSpace E<VAR>m μ : Measure E<VAR>Ω : Type u_2<VAR>x✝ : MeasurableSpace Ω<VAR>ℙ : Measure Ω<VAR>X : Ω → E<VAR>s : Set E<VAR>hns : μ s ≠ 0<VAR>hnt : μ s ≠ ⊤<VAR>hu : Measure.map X ℙ = (μ s)⁻¹ • μ.restrict s<GOAL>AEMeasurable X ℙ
<VAR>E : Type u_1<VAR>inst✝ : MeasurableSpace E<VAR>m μ : Measure E<VAR>Ω : Type u_2<VAR>x✝ : MeasurableSpace Ω<VAR>ℙ : Measure Ω<VAR>X : Ω → E<VAR>s : Set E<VAR>hns : μ s ≠ 0<VAR>hnt : μ s ≠ ⊤<VAR>hu : Measure.map X ℙ = (μ s)⁻¹ • μ.restrict s<VAR>h : ¬AEMeasurable X ℙ<GOAL>False
<VAR>E : Type u_1<VAR>inst✝ : MeasurableSpace E<VAR>m μ : Measure E<VAR>Ω : Type u_2<VAR>x✝ : MeasurableSpace Ω<VAR>ℙ : Measure Ω<VAR>X : Ω → E<VAR>s : Set E<VAR>hns : μ s ≠ 0<VAR>hnt : μ s ≠ ⊤<VAR>hu : 0 = (μ s)⁻¹ • μ.restrict s<VAR>h : ¬AEMeasurable X ℙ<GOAL>False
<VAR>E : Type u_1<VAR>inst✝ : MeasurableSpace E<VAR>m μ : Measure E<VAR>Ω : Type u_2<VAR>x✝ : MeasurableSpace Ω<VAR>ℙ : Measure Ω<VAR>X : Ω → E<VAR>s : Set E<VAR>hns : μ s ≠ 0<VAR>hnt : μ s ≠ ⊤<VAR>hu : 0 = (μ s)⁻¹ • μ.restrict s<VAR>h : ¬AEMeasurable X ℙ<GOAL>0 = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : DistribLattice α<VAR>inst✝² : BoundedOrder α<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : DecidableRel fun x x_1 => x ≤ x_1<VAR>s t : Finset α<VAR>a : α<GOAL>a ∈ lowerClosure ↑(s ⊼ t) ↔ a ∈ lowerClosure ↑s ∧ a ∈ lowerClosure ↑t
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>𝕜₃ : Type u_5<VAR>𝕝 : Type u_6<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>E₃ : Type u_9<VAR>F : Type u_10<VAR>G : Type u_11<VAR>ι : Type u_12<VAR>inst✝¹⁸ : SeminormedRing 𝕜<VAR>inst✝¹⁷ : SeminormedRing 𝕜₂<VAR>inst✝¹⁶ : SeminormedRing 𝕜₃<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>inst✝¹⁵ : RingHomIsometric σ₁₂<VAR>σ₂₃ : 𝕜₂ →+* 𝕜₃<VAR>inst✝¹⁴ : RingHomIsometric σ₂₃<VAR>σ₁₃ : 𝕜 →+* 𝕜₃<VAR>inst✝¹³ : RingHomIsometric σ₁₃<VAR>inst✝¹² : AddCommGroup E<VAR>inst✝¹¹ : AddCommGroup E₂<VAR>inst✝¹⁰ : AddCommGroup E₃<VAR>inst✝⁹ : AddCommGroup F<VAR>inst✝⁸ : AddCommGroup G<VAR>inst✝⁷ : Module 𝕜 E<VAR>inst✝⁶ : Module 𝕜₂ E₂<VAR>inst✝⁵ : Module 𝕜₃ E₃<VAR>inst✝⁴ : Module 𝕜 F<VAR>inst✝³ : Module 𝕜 G<VAR>inst✝² : SMul R ℝ<VAR>inst✝¹ : SMul R ℝ≥0<VAR>inst✝ : IsScalarTower R ℝ≥0 ℝ<VAR>p : ι → Seminorm 𝕜 E<VAR>s : Finset ι<VAR>x : E<GOAL>(s.sup p) x = 0 ∨ ∃ i ∈ s, (s.sup p) x = (p i) x
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>𝕜₃ : Type u_5<VAR>𝕝 : Type u_6<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>E₃ : Type u_9<VAR>F : Type u_10<VAR>G : Type u_11<VAR>ι : Type u_12<VAR>inst✝¹⁸ : SeminormedRing 𝕜<VAR>inst✝¹⁷ : SeminormedRing 𝕜₂<VAR>inst✝¹⁶ : SeminormedRing 𝕜₃<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>inst✝¹⁵ : RingHomIsometric σ₁₂<VAR>σ₂₃ : 𝕜₂ →+* 𝕜₃<VAR>inst✝¹⁴ : RingHomIsometric σ₂₃<VAR>σ₁₃ : 𝕜 →+* 𝕜₃<VAR>inst✝¹³ : RingHomIsometric σ₁₃<VAR>inst✝¹² : AddCommGroup E<VAR>inst✝¹¹ : AddCommGroup E₂<VAR>inst✝¹⁰ : AddCommGroup E₃<VAR>inst✝⁹ : AddCommGroup F<VAR>inst✝⁸ : AddCommGroup G<VAR>inst✝⁷ : Module 𝕜 E<VAR>inst✝⁶ : Module 𝕜₂ E₂<VAR>inst✝⁵ : Module 𝕜₃ E₃<VAR>inst✝⁴ : Module 𝕜 F<VAR>inst✝³ : Module 𝕜 G<VAR>inst✝² : SMul R ℝ<VAR>inst✝¹ : SMul R ℝ≥0<VAR>inst✝ : IsScalarTower R ℝ≥0 ℝ<VAR>p : ι → Seminorm 𝕜 E<VAR>x : E<GOAL>(∅.sup p) x = 0 ∨ ∃ i ∈ ∅, (∅.sup p) x = (p i) x
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>𝕜₃ : Type u_5<VAR>𝕝 : Type u_6<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>E₃ : Type u_9<VAR>F : Type u_10<VAR>G : Type u_11<VAR>ι : Type u_12<VAR>inst✝¹⁸ : SeminormedRing 𝕜<VAR>inst✝¹⁷ : SeminormedRing 𝕜₂<VAR>inst✝¹⁶ : SeminormedRing 𝕜₃<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>inst✝¹⁵ : RingHomIsometric σ₁₂<VAR>σ₂₃ : 𝕜₂ →+* 𝕜₃<VAR>inst✝¹⁴ : RingHomIsometric σ₂₃<VAR>σ₁₃ : 𝕜 →+* 𝕜₃<VAR>inst✝¹³ : RingHomIsometric σ₁₃<VAR>inst✝¹² : AddCommGroup E<VAR>inst✝¹¹ : AddCommGroup E₂<VAR>inst✝¹⁰ : AddCommGroup E₃<VAR>inst✝⁹ : AddCommGroup F<VAR>inst✝⁸ : AddCommGroup G<VAR>inst✝⁷ : Module 𝕜 E<VAR>inst✝⁶ : Module 𝕜₂ E₂<VAR>inst✝⁵ : Module 𝕜₃ E₃<VAR>inst✝⁴ : Module 𝕜 F<VAR>inst✝³ : Module 𝕜 G<VAR>inst✝² : SMul R ℝ<VAR>inst✝¹ : SMul R ℝ≥0<VAR>inst✝ : IsScalarTower R ℝ≥0 ℝ<VAR>p : ι → Seminorm 𝕜 E<VAR>s : Finset ι<VAR>x : E<VAR>hs : s.Nonempty<GOAL>(s.sup p) x = 0 ∨ ∃ i ∈ s, (s.sup p) x = (p i) x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : PartialOrder α<VAR>a b c : α<VAR>h : a ≤ b<GOAL>Ioo a b ∪ {a, b} = Icc a b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : PartialOrder α<VAR>a b c : α<VAR>h : a ≤ b<VAR>this : Icc a b \ {a, b} ∪ {a, b} = Icc a b<GOAL>Ioo a b ∪ {a, b} = Icc a b
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>k : Type u_1<VAR>inst✝ : CommRing k<VAR>n : ℕ<VAR>this : ↑p ^ (n + 1) = C (↑p ^ (n + 1))<GOAL>(polyOfInterest p n).vars = (↑p ^ (n + 1) * (wittMul p (n + 1) + ↑p ^ (n + 1) * X (0, n + 1) * X (1, n + 1) - X (0, n + 1) * (rename (Prod.mk 1)) (wittPolynomial p ℤ (n + 1)) - X (1, n + 1) * (rename (Prod.mk 0)) (wittPolynomial p ℤ (n + 1)))).vars
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>k : Type u_1<VAR>inst✝ : CommRing k<VAR>n : ℕ<VAR>this : ↑p ^ (n + 1) = C (↑p ^ (n + 1))<GOAL>↑p ^ (n + 1) ≠ 0
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>k : Type u_1<VAR>inst✝ : CommRing k<VAR>n : ℕ<VAR>this : ↑p ^ (n + 1) = C (↑p ^ (n + 1))<GOAL>↑p ≠ 0
<VAR>R : Type u_1<VAR>inst✝¹¹ : CommRing R<VAR>M : Type u_2<VAR>inst✝¹⁰ : AddCommGroup M<VAR>inst✝⁹ : Module R M<VAR>M' : Type u_3<VAR>inst✝⁸ : AddCommGroup M'<VAR>inst✝⁷ : Module R M'<VAR>ι : Type u_4<VAR>inst✝⁶ : DecidableEq ι<VAR>inst✝⁵ : Fintype ι<VAR>e : Basis ι R M<VAR>A✝ : Type u_5<VAR>inst✝⁴ : CommRing A✝<VAR>inst✝³ : Module A✝ M<VAR>κ : Type u_6<VAR>inst✝² : Fintype κ<VAR>A : Type u_7<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Module A M<VAR>f : M →ₗ[A] M<VAR>hf : IsUnit f<GOAL>IsUnit (LinearMap.det f)
<VAR>R : Type u_1<VAR>inst✝¹¹ : CommRing R<VAR>M : Type u_2<VAR>inst✝¹⁰ : AddCommGroup M<VAR>inst✝⁹ : Module R M<VAR>M' : Type u_3<VAR>inst✝⁸ : AddCommGroup M'<VAR>inst✝⁷ : Module R M'<VAR>ι : Type u_4<VAR>inst✝⁶ : DecidableEq ι<VAR>inst✝⁵ : Fintype ι<VAR>e : Basis ι R M<VAR>A✝ : Type u_5<VAR>inst✝⁴ : CommRing A✝<VAR>inst✝³ : Module A✝ M<VAR>κ : Type u_6<VAR>inst✝² : Fintype κ<VAR>A : Type u_7<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Module A M<VAR>f : M →ₗ[A] M<VAR>hf : IsUnit f<VAR>g : M →ₗ[A] M<VAR>hg : f ∘ₗ g = 1<GOAL>IsUnit (LinearMap.det f)
<VAR>R : Type u_1<VAR>inst✝¹¹ : CommRing R<VAR>M : Type u_2<VAR>inst✝¹⁰ : AddCommGroup M<VAR>inst✝⁹ : Module R M<VAR>M' : Type u_3<VAR>inst✝⁸ : AddCommGroup M'<VAR>inst✝⁷ : Module R M'<VAR>ι : Type u_4<VAR>inst✝⁶ : DecidableEq ι<VAR>inst✝⁵ : Fintype ι<VAR>e : Basis ι R M<VAR>A✝ : Type u_5<VAR>inst✝⁴ : CommRing A✝<VAR>inst✝³ : Module A✝ M<VAR>κ : Type u_6<VAR>inst✝² : Fintype κ<VAR>A : Type u_7<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Module A M<VAR>f : M →ₗ[A] M<VAR>hf : IsUnit f<VAR>g : M →ₗ[A] M<VAR>hg : f ∘ₗ g = 1<VAR>this : LinearMap.det f * LinearMap.det g = 1<GOAL>IsUnit (LinearMap.det f)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>p : α → Prop<VAR>fs : β → Filter α<GOAL>(∃ᶠ (x : α) in ⨆ b, fs b, p x) ↔ ∃ b, ∃ᶠ (x : α) in fs b, p x
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>G : Type u_7<VAR>j : ℕ<VAR>L : List ℕ<VAR>IH : (∀ i ∈ L, 1 ≤ i) → L.length ≤ L.sum<VAR>h : ∀ i ∈ j :: L, 1 ≤ i<GOAL>(j :: L).length ≤ (j :: L).sum
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>G : Type u_7<VAR>j : ℕ<VAR>L : List ℕ<VAR>IH : (∀ i ∈ L, 1 ≤ i) → L.length ≤ L.sum<VAR>h : ∀ i ∈ j :: L, 1 ≤ i<GOAL>1 + L.length ≤ j + L.sum
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>F : Type u_3<VAR>K : Type u_4<VAR>P Q : Cubic R<VAR>a b c d a' b' c' d' : R<VAR>inst✝ : Semiring R<VAR>ha : P.a = 0<VAR>hb : P.b = 0<VAR>hc : P.c ≠ 0<GOAL>P.toPoly.degree = 1
<VAR>ι : Sort u_1<VAR>V : Type u<VAR>W : Type v<VAR>G : SimpleGraph V<VAR>v w : V<VAR>hvw : G.Adj v w<VAR>v✝ w✝ : V<VAR>h : (fun a b => s(v, w) = s(a, b)) v✝ w✝<GOAL>G.Adj v✝ w✝
<VAR>ι : Sort u_1<VAR>V : Type u<VAR>W : Type v<VAR>G : SimpleGraph V<VAR>v w : V<VAR>hvw : G.Adj v w<VAR>v✝ w✝ : V<VAR>h : (fun a b => s(v, w) = s(a, b)) v✝ w✝<GOAL>s(v, w) ∈ G.edgeSet
<VAR>ι : Sort u_1<VAR>V : Type u<VAR>W : Type v<VAR>G : SimpleGraph V<VAR>v w : V<VAR>hvw : G.Adj v w<VAR>a b : V<VAR>h : (a ∈ s(v, w)) = (a ∈ s(a, b))<GOAL>a ∈ {v, w}
<VAR>ι : Sort u_1<VAR>V : Type u<VAR>W : Type v<VAR>G : SimpleGraph V<VAR>v w : V<VAR>hvw : G.Adj v w<VAR>a b : V<VAR>h : a = v ∨ a = w<GOAL>a ∈ {v, w}
<VAR>K : Type u<VAR>inst✝ : CommRing K<VAR>P : Sort v<VAR>f : K[X] → K[X] → P<VAR>H : ∀ {p q a : K[X]}, q ≠ 0 → a ≠ 0 → f (a * p) (a * q) = f p q<VAR>p q p' q' : K[X]<VAR>hq : q ≠ 0<VAR>hq' : q' ≠ 0<VAR>h : q' * p = q * p'<GOAL>f (q' * p) (q' * q) = f (q * p') (q * q')
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>inst✝¹ : SemilatticeSup α<VAR>inst✝ : SemilatticeSup β<VAR>f : α → β<VAR>hf : LeftOrdContinuous f<VAR>h : Injective f<VAR>x y : α<GOAL>f x < f y ↔ x < y
<VAR>F : Type u_1<VAR>E : Type u_2<VAR>K : Type u_3<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Field E<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra F E<VAR>inst✝ : Algebra F K<VAR>S : Set E<VAR>hK : ∀ s ∈ S, IsIntegral F s ∧ Splits (algebraMap F K) (minpoly F s)<VAR>hK' : ∀ (s : E), IsIntegral F s ∧ Splits (algebraMap F K) (minpoly F s)<VAR>L : IntermediateField F E<VAR>f : ↥L →ₐ[F] K<VAR>hL : L ≤ adjoin F S<VAR>hS : adjoin F S = ⊤<VAR>x : E<VAR>hx : x ∈ adjoin F S<VAR>y : K<VAR>hy : (aeval y) (minpoly F x) = 0<GOAL>∃ φ, φ ⟨x, hx⟩ = y
<VAR>F : Type u_1<VAR>E : Type u_2<VAR>K : Type u_3<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Field E<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra F E<VAR>inst✝ : Algebra F K<VAR>S : Set E<VAR>hK : ∀ s ∈ S, IsIntegral F s ∧ Splits (algebraMap F K) (minpoly F s)<VAR>hK' : ∀ (s : E), IsIntegral F s ∧ Splits (algebraMap F K) (minpoly F s)<VAR>L : IntermediateField F E<VAR>f : ↥L →ₐ[F] K<VAR>hL : L ≤ adjoin F S<VAR>hS : adjoin F S = ⊤<VAR>x : E<VAR>hx : x ∈ adjoin F S<VAR>y : K<VAR>hy : (aeval y) (minpoly F x) = 0<VAR>this : Algebra.IsAlgebraic F ↥(adjoin F S)<GOAL>∃ φ, φ ⟨x, hx⟩ = y
<VAR>F : Type u_1<VAR>E : Type u_2<VAR>K : Type u_3<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Field E<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra F E<VAR>inst✝ : Algebra F K<VAR>S : Set E<VAR>hK : ∀ s ∈ S, IsIntegral F s ∧ Splits (algebraMap F K) (minpoly F s)<VAR>hK' : ∀ (s : E), IsIntegral F s ∧ Splits (algebraMap F K) (minpoly F s)<VAR>L : IntermediateField F E<VAR>f : ↥L →ₐ[F] K<VAR>hL : L ≤ adjoin F S<VAR>hS : adjoin F S = ⊤<VAR>x : E<VAR>hx : x ∈ adjoin F S<VAR>y : K<VAR>hy : (aeval y) (minpoly F x) = 0<VAR>this : Algebra.IsAlgebraic F ↥(adjoin F S)<VAR>ix : IsAlgebraic F ⟨x, hx⟩<GOAL>∃ φ, φ ⟨x, hx⟩ = y
<VAR>F : Type u_1<VAR>E : Type u_2<VAR>K : Type u_3<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Field E<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra F E<VAR>inst✝ : Algebra F K<VAR>S : Set E<VAR>hK : ∀ s ∈ S, IsIntegral F s ∧ Splits (algebraMap F K) (minpoly F s)<VAR>hK' : ∀ (s : E), IsIntegral F s ∧ Splits (algebraMap F K) (minpoly F s)<VAR>L : IntermediateField F E<VAR>f : ↥L →ₐ[F] K<VAR>hL : L ≤ adjoin F S<VAR>hS : adjoin F S = ⊤<VAR>x : E<VAR>hx : x ∈ adjoin F S<VAR>y : K<VAR>hy : (aeval y) (minpoly F x) = 0<VAR>this : Algebra.IsAlgebraic F ↥(adjoin F S)<VAR>ix : IsIntegral F ↑⟨x, hx⟩<GOAL>∃ φ, φ ⟨x, hx⟩ = y
<VAR>F : Type u_1<VAR>E : Type u_2<VAR>K : Type u_3<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Field E<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra F E<VAR>inst✝ : Algebra F K<VAR>S : Set E<VAR>hK : ∀ s ∈ S, IsIntegral F s ∧ Splits (algebraMap F K) (minpoly F s)<VAR>hK' : ∀ (s : E), IsIntegral F s ∧ Splits (algebraMap F K) (minpoly F s)<VAR>L : IntermediateField F E<VAR>f : ↥L →ₐ[F] K<VAR>hL : L ≤ adjoin F S<VAR>hS : adjoin F S = ⊤<VAR>x : E<VAR>hx : x ∈ adjoin F S<VAR>y : K<VAR>hy : (aeval y) (minpoly F x) = 0<VAR>this : Algebra.IsAlgebraic F ↥(adjoin F S)<VAR>ix : IsIntegral F ↑⟨x, hx⟩<VAR>φ : ↥(adjoin F S) →ₐ[F] K<VAR>hφ : φ.comp (inclusion ⋯) = (algHomAdjoinIntegralEquiv F ix).symm ⟨y, ⋯⟩<GOAL>∃ φ, φ ⟨x, hx⟩ = y
<VAR>C : Type u₁<VAR>inst✝ : Category.{v₁, u₁} C<VAR>P Q : Cᵒᵖ ⥤ Type v₁<VAR>f g : P ⟶ Q<VAR>h : ∀ (X : C) (p : yoneda.obj X ⟶ P), p ≫ f = p ≫ g<VAR>X : Cᵒᵖ<VAR>x : P.obj X<GOAL>f.app X x = g.app X x
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : Abelian C<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>factorThruImage f ≫ (coimageIsoImage' f).inv = cokernel.π (kernel.ι f)
<VAR>E : Type u_1<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℂ E<VAR>V : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : InnerProductSpace ℝ V<VAR>inst✝³ : FiniteDimensional ℝ V<VAR>inst✝² : MeasurableSpace V<VAR>inst✝¹ : BorelSpace V<VAR>f : V → E<VAR>inst✝ : FiniteDimensional ℝ V<VAR>K N : ℕ∞<VAR>hf : ContDiff ℝ N f<VAR>h'f : ∀ (k n : ℕ), ↑k ≤ K → ↑n ≤ N → Integrable (fun v => ‖v‖ ^ k * ‖iteratedFDeriv ℝ n f v‖) volume<VAR>k n : ℕ<VAR>hk : ↑k ≤ K<VAR>hn : ↑n ≤ N<VAR>w : V<GOAL>‖w‖ ^ n * ‖iteratedFDeriv ℝ k (𝓕 f) w‖ ≤ (2 * π) ^ k * (2 * ↑k + 2) ^ n * ∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1), ∫ (v : V), ‖v‖ ^ p.1 * ‖iteratedFDeriv ℝ p.2 f v‖
<VAR>E : Type u_1<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℂ E<VAR>V : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : InnerProductSpace ℝ V<VAR>inst✝³ : FiniteDimensional ℝ V<VAR>inst✝² : MeasurableSpace V<VAR>inst✝¹ : BorelSpace V<VAR>f : V → E<VAR>inst✝ : FiniteDimensional ℝ V<VAR>K N : ℕ∞<VAR>hf : ContDiff ℝ N f<VAR>h'f : ∀ (k n : ℕ), ↑k ≤ K → ↑n ≤ N → Integrable (fun v => ‖v‖ ^ k * ‖iteratedFDeriv ℝ n f v‖) volume<VAR>k n : ℕ<VAR>hk : ↑k ≤ K<VAR>hn : ↑n ≤ N<VAR>w : V<VAR>Z : ‖w‖ ^ n * (‖w‖ ^ n * ‖iteratedFDeriv ℝ k (𝓕 f) w‖) ≤ ‖w‖ ^ n * ((2 * (π * ‖innerSL ℝ‖)) ^ k * ((2 * ↑k + 2) ^ n * ∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1), ∫ (v : V), ‖v‖ ^ p.1 * ‖iteratedFDeriv ℝ p.2 f v‖))<GOAL>‖w‖ ^ n * ‖iteratedFDeriv ℝ k (𝓕 f) w‖ ≤ (2 * π) ^ k * (2 * ↑k + 2) ^ n * ∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1), ∫ (v : V), ‖v‖ ^ p.1 * ‖iteratedFDeriv ℝ p.2 f v‖
<VAR>E : Type u_1<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℂ E<VAR>V : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : InnerProductSpace ℝ V<VAR>inst✝³ : FiniteDimensional ℝ V<VAR>inst✝² : MeasurableSpace V<VAR>inst✝¹ : BorelSpace V<VAR>f : V → E<VAR>inst✝ : FiniteDimensional ℝ V<VAR>K N : ℕ∞<VAR>hf : ContDiff ℝ N f<VAR>h'f : ∀ (k n : ℕ), ↑k ≤ K → ↑n ≤ N → Integrable (fun v => ‖v‖ ^ k * ‖iteratedFDeriv ℝ n f v‖) volume<VAR>k : ℕ<VAR>hk : ↑k ≤ K<VAR>w : V<VAR>hn : ↑0 ≤ N<VAR>Z : ‖w‖ ^ 0 * (‖w‖ ^ 0 * ‖iteratedFDeriv ℝ k (𝓕 f) w‖) ≤ ‖w‖ ^ 0 * ((2 * (π * ‖innerSL ℝ‖)) ^ k * ((2 * ↑k + 2) ^ 0 * ∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (0 + 1), ∫ (v : V), ‖v‖ ^ p.1 * ‖iteratedFDeriv ℝ p.2 f v‖))<GOAL>‖w‖ ^ 0 * ‖iteratedFDeriv ℝ k (𝓕 f) w‖ ≤ (2 * π) ^ k * (2 * ↑k + 2) ^ 0 * ∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (0 + 1), ∫ (v : V), ‖v‖ ^ p.1 * ‖iteratedFDeriv ℝ p.2 f v‖
<VAR>E : Type u_1<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℂ E<VAR>V : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : InnerProductSpace ℝ V<VAR>inst✝³ : FiniteDimensional ℝ V<VAR>inst✝² : MeasurableSpace V<VAR>inst✝¹ : BorelSpace V<VAR>f : V → E<VAR>inst✝ : FiniteDimensional ℝ V<VAR>K N : ℕ∞<VAR>hf : ContDiff ℝ N f<VAR>h'f : ∀ (k n : ℕ), ↑k ≤ K → ↑n ≤ N → Integrable (fun v => ‖v‖ ^ k * ‖iteratedFDeriv ℝ n f v‖) volume<VAR>k n : ℕ<VAR>hk : ↑k ≤ K<VAR>hn✝ : ↑n ≤ N<VAR>w : V<VAR>Z : ‖w‖ ^ n * (‖w‖ ^ n * ‖iteratedFDeriv ℝ k (𝓕 f) w‖) ≤ ‖w‖ ^ n * ((2 * (π * ‖innerSL ℝ‖)) ^ k * ((2 * ↑k + 2) ^ n * ∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1), ∫ (v : V), ‖v‖ ^ p.1 * ‖iteratedFDeriv ℝ p.2 f v‖))<VAR>hn : n ≠ 0<GOAL>‖w‖ ^ n * ‖iteratedFDeriv ℝ k (𝓕 f) w‖ ≤ (2 * π) ^ k * (2 * ↑k + 2) ^ n * ∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1), ∫ (v : V), ‖v‖ ^ p.1 * ‖iteratedFDeriv ℝ p.2 f v‖
<VAR>E : Type u_1<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℂ E<VAR>V : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : InnerProductSpace ℝ V<VAR>inst✝³ : FiniteDimensional ℝ V<VAR>inst✝² : MeasurableSpace V<VAR>inst✝¹ : BorelSpace V<VAR>f : V → E<VAR>inst✝ : FiniteDimensional ℝ V<VAR>K N : ℕ∞<VAR>hf : ContDiff ℝ N f<VAR>h'f : ∀ (k n : ℕ), ↑k ≤ K → ↑n ≤ N → Integrable (fun v => ‖v‖ ^ k * ‖iteratedFDeriv ℝ n f v‖) volume<VAR>k n : ℕ<VAR>hk : ↑k ≤ K<VAR>hn✝ : ↑n ≤ N<VAR>hn : n ≠ 0<VAR>Z : ‖0‖ ^ n * (‖0‖ ^ n * ‖iteratedFDeriv ℝ k (𝓕 f) 0‖) ≤ ‖0‖ ^ n * ((2 * (π * ‖innerSL ℝ‖)) ^ k * ((2 * ↑k + 2) ^ n * ∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1), ∫ (v : V), ‖v‖ ^ p.1 * ‖iteratedFDeriv ℝ p.2 f v‖))<GOAL>‖0‖ ^ n * ‖iteratedFDeriv ℝ k (𝓕 f) 0‖ ≤ (2 * π) ^ k * (2 * ↑k + 2) ^ n * ∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1), ∫ (v : V), ‖v‖ ^ p.1 * ‖iteratedFDeriv ℝ p.2 f v‖
<VAR>E : Type u_1<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℂ E<VAR>V : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : InnerProductSpace ℝ V<VAR>inst✝³ : FiniteDimensional ℝ V<VAR>inst✝² : MeasurableSpace V<VAR>inst✝¹ : BorelSpace V<VAR>f : V → E<VAR>inst✝ : FiniteDimensional ℝ V<VAR>K N : ℕ∞<VAR>hf : ContDiff ℝ N f<VAR>h'f : ∀ (k n : ℕ), ↑k ≤ K → ↑n ≤ N → Integrable (fun v => ‖v‖ ^ k * ‖iteratedFDeriv ℝ n f v‖) volume<VAR>k n : ℕ<VAR>hk : ↑k ≤ K<VAR>hn✝ : ↑n ≤ N<VAR>w : V<VAR>Z : ‖w‖ ^ n * (‖w‖ ^ n * ‖iteratedFDeriv ℝ k (𝓕 f) w‖) ≤ ‖w‖ ^ n * ((2 * (π * ‖innerSL ℝ‖)) ^ k * ((2 * ↑k + 2) ^ n * ∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1), ∫ (v : V), ‖v‖ ^ p.1 * ‖iteratedFDeriv ℝ p.2 f v‖))<VAR>hn : n ≠ 0<VAR>hw : w ≠ 0<GOAL>‖w‖ ^ n * ‖iteratedFDeriv ℝ k (𝓕 f) w‖ ≤ (2 * π) ^ k * (2 * ↑k + 2) ^ n * ∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1), ∫ (v : V), ‖v‖ ^ p.1 * ‖iteratedFDeriv ℝ p.2 f v‖
<VAR>E : Type u_1<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℂ E<VAR>V : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : InnerProductSpace ℝ V<VAR>inst✝³ : FiniteDimensional ℝ V<VAR>inst✝² : MeasurableSpace V<VAR>inst✝¹ : BorelSpace V<VAR>f : V → E<VAR>inst✝ : FiniteDimensional ℝ V<VAR>K N : ℕ∞<VAR>hf : ContDiff ℝ N f<VAR>h'f : ∀ (k n : ℕ), ↑k ≤ K → ↑n ≤ N → Integrable (fun v => ‖v‖ ^ k * ‖iteratedFDeriv ℝ n f v‖) volume<VAR>k n : ℕ<VAR>hk : ↑k ≤ K<VAR>hn✝ : ↑n ≤ N<VAR>w : V<VAR>Z : ‖w‖ ^ n * ‖iteratedFDeriv ℝ k (𝓕 f) w‖ ≤ (2 * (π * ‖innerSL ℝ‖)) ^ k * ((2 * ↑k + 2) ^ n * ∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1), ∫ (v : V), ‖v‖ ^ p.1 * ‖iteratedFDeriv ℝ p.2 f v‖)<VAR>hn : n ≠ 0<VAR>hw : w ≠ 0<GOAL>‖w‖ ^ n * ‖iteratedFDeriv ℝ k (𝓕 f) w‖ ≤ (2 * π) ^ k * (2 * ↑k + 2) ^ n * ∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1), ∫ (v : V), ‖v‖ ^ p.1 * ‖iteratedFDeriv ℝ p.2 f v‖
<VAR>E : Type u_1<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℂ E<VAR>V : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : InnerProductSpace ℝ V<VAR>inst✝³ : FiniteDimensional ℝ V<VAR>inst✝² : MeasurableSpace V<VAR>inst✝¹ : BorelSpace V<VAR>f : V → E<VAR>inst✝ : FiniteDimensional ℝ V<VAR>K N : ℕ∞<VAR>hf : ContDiff ℝ N f<VAR>h'f : ∀ (k n : ℕ), ↑k ≤ K → ↑n ≤ N → Integrable (fun v => ‖v‖ ^ k * ‖iteratedFDeriv ℝ n f v‖) volume<VAR>k n : ℕ<VAR>hk : ↑k ≤ K<VAR>hn✝ : ↑n ≤ N<VAR>w : V<VAR>Z : ‖w‖ ^ n * ‖iteratedFDeriv ℝ k (𝓕 f) w‖ ≤ (2 * (π * ‖innerSL ℝ‖)) ^ k * ((2 * ↑k + 2) ^ n * ∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1), ∫ (v : V), ‖v‖ ^ p.1 * ‖iteratedFDeriv ℝ p.2 f v‖)<VAR>hn : n ≠ 0<VAR>hw : w ≠ 0<GOAL>(2 * (π * ‖innerSL ℝ‖)) ^ k * ((2 * ↑k + 2) ^ n * ∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1), ∫ (v : V), ‖v‖ ^ p.1 * ‖iteratedFDeriv ℝ p.2 f v‖) ≤ (2 * π) ^ k * (2 * ↑k + 2) ^ n * ∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1), ∫ (v : V), ‖v‖ ^ p.1 * ‖iteratedFDeriv ℝ p.2 f v‖
<VAR>E : Type u_1<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℂ E<VAR>V : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : InnerProductSpace ℝ V<VAR>inst✝³ : FiniteDimensional ℝ V<VAR>inst✝² : MeasurableSpace V<VAR>inst✝¹ : BorelSpace V<VAR>f : V → E<VAR>inst✝ : FiniteDimensional ℝ V<VAR>K N : ℕ∞<VAR>hf : ContDiff ℝ N f<VAR>h'f : ∀ (k n : ℕ), ↑k ≤ K → ↑n ≤ N → Integrable (fun v => ‖v‖ ^ k * ‖iteratedFDeriv ℝ n f v‖) volume<VAR>k n : ℕ<VAR>hk : ↑k ≤ K<VAR>hn✝ : ↑n ≤ N<VAR>w : V<VAR>Z : ‖w‖ ^ n * ‖iteratedFDeriv ℝ k (𝓕 f) w‖ ≤ (2 * (π * ‖innerSL ℝ‖)) ^ k * ((2 * ↑k + 2) ^ n * ∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1), ∫ (v : V), ‖v‖ ^ p.1 * ‖iteratedFDeriv ℝ p.2 f v‖)<VAR>hn : n ≠ 0<VAR>hw : w ≠ 0<GOAL>(2 * (π * ‖innerSL ℝ‖)) ^ k * ((2 * ↑k + 2) ^ n * ∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1), ∫ (v : V), ‖v‖ ^ p.1 * ‖iteratedFDeriv ℝ p.2 f v‖) ≤ (2 * (π * 1)) ^ k * (2 * ↑k + 2) ^ n * ∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1), ∫ (v : V), ‖v‖ ^ p.1 * ‖iteratedFDeriv ℝ p.2 f v‖
<VAR>E : Type u_1<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℂ E<VAR>V : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : InnerProductSpace ℝ V<VAR>inst✝³ : FiniteDimensional ℝ V<VAR>inst✝² : MeasurableSpace V<VAR>inst✝¹ : BorelSpace V<VAR>f : V → E<VAR>inst✝ : FiniteDimensional ℝ V<VAR>K N : ℕ∞<VAR>hf : ContDiff ℝ N f<VAR>h'f : ∀ (k n : ℕ), ↑k ≤ K → ↑n ≤ N → Integrable (fun v => ‖v‖ ^ k * ‖iteratedFDeriv ℝ n f v‖) volume<VAR>k n : ℕ<VAR>hk : ↑k ≤ K<VAR>hn✝ : ↑n ≤ N<VAR>w : V<VAR>Z : ‖w‖ ^ n * ‖iteratedFDeriv ℝ k (𝓕 f) w‖ ≤ (2 * (π * ‖innerSL ℝ‖)) ^ k * ((2 * ↑k + 2) ^ n * ∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1), ∫ (v : V), ‖v‖ ^ p.1 * ‖iteratedFDeriv ℝ p.2 f v‖)<VAR>hn : n ≠ 0<VAR>hw : w ≠ 0<GOAL>(2 * (π * ‖innerSL ℝ‖)) ^ k * ((2 * ↑k + 2) ^ n * ∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1), ∫ (v : V), ‖v‖ ^ p.1 * ‖iteratedFDeriv ℝ p.2 f v‖) ≤ (2 * (π * 1)) ^ k * ((2 * ↑k + 2) ^ n * ∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1), ∫ (v : V), ‖v‖ ^ p.1 * ‖iteratedFDeriv ℝ p.2 f v‖)
<VAR>E : Type u_1<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℂ E<VAR>V : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : InnerProductSpace ℝ V<VAR>inst✝³ : FiniteDimensional ℝ V<VAR>inst✝² : MeasurableSpace V<VAR>inst✝¹ : BorelSpace V<VAR>f : V → E<VAR>inst✝ : FiniteDimensional ℝ V<VAR>K N : ℕ∞<VAR>hf : ContDiff ℝ N f<VAR>h'f : ∀ (k n : ℕ), ↑k ≤ K → ↑n ≤ N → Integrable (fun v => ‖v‖ ^ k * ‖iteratedFDeriv ℝ n f v‖) volume<VAR>k n : ℕ<VAR>hk : ↑k ≤ K<VAR>hn✝ : ↑n ≤ N<VAR>w : V<VAR>Z : ‖w‖ ^ n * ‖iteratedFDeriv ℝ k (𝓕 f) w‖ ≤ (2 * (π * ‖innerSL ℝ‖)) ^ k * ((2 * ↑k + 2) ^ n * ∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1), ∫ (v : V), ‖v‖ ^ p.1 * ‖iteratedFDeriv ℝ p.2 f v‖)<VAR>hn : n ≠ 0<VAR>hw : w ≠ 0<GOAL>‖innerSL ℝ‖ ≤ 1
<VAR>d✝ : ℤ<VAR>c d x y z w : ℕ<VAR>xy : SqLe x c y d<VAR>zw : SqLe z c w d<GOAL>SqLe (x + z) c (y + w) d
<VAR>d✝ : ℤ<VAR>c d x y z w : ℕ<VAR>xy : SqLe x c y d<VAR>zw : SqLe z c w d<VAR>xz : c * (x * z) ≤ d * (y * w)<GOAL>SqLe (x + z) c (y + w) d
<VAR>d✝ : ℤ<VAR>c d x y z w : ℕ<VAR>xz : c * (x * z) ≤ d * (y * w)<VAR>xy : c * (x * x) ≤ d * (y * y)<VAR>zw : c * (z * z) ≤ d * (w * w)<GOAL>SqLe (x + z) c (y + w) d
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>F : Type u_3<VAR>K : Type u_4<VAR>P Q : Cubic R<VAR>a b c d a' b' c' d' : R<VAR>inst✝ : Semiring R<VAR>ha : P.a = 0<VAR>hb : P.b = 0<VAR>hc : P.c = 0<VAR>hd : P.d ≠ 0<GOAL>P.toPoly.degree = 0
<VAR>α : Type u<VAR>L✝ L₁ L₂ L₃ L₄ : List (α × Bool)<VAR>p : α × Bool<VAR>L : List (α × Bool)<GOAL>Red (p :: L ++ L₁) (p :: L ++ L₂) ↔ Red L₁ L₂
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : CommRing A<VAR>inst✝² : Field K<VAR>T : Type u_4<VAR>inst✝¹ : CommRing T<VAR>inst✝ : IsDedekindDomain T<VAR>I J : Ideal T<VAR>hI : I ≠ ⊥<VAR>hJ : J ≠ ⊥<GOAL>I ⊔ J = (normalizedFactors I ∩ normalizedFactors J).prod
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : CommRing A<VAR>inst✝² : Field K<VAR>T : Type u_4<VAR>inst✝¹ : CommRing T<VAR>inst✝ : IsDedekindDomain T<VAR>I J : Ideal T<VAR>hI : I ≠ ⊥<VAR>hJ : J ≠ ⊥<VAR>H : normalizedFactors (normalizedFactors I ∩ normalizedFactors J).prod = normalizedFactors I ∩ normalizedFactors J<GOAL>I ⊔ J = (normalizedFactors I ∩ normalizedFactors J).prod
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : CommRing A<VAR>inst✝² : Field K<VAR>T : Type u_4<VAR>inst✝¹ : CommRing T<VAR>inst✝ : IsDedekindDomain T<VAR>I J : Ideal T<VAR>hI : I ≠ ⊥<VAR>hJ : J ≠ ⊥<VAR>H : normalizedFactors (normalizedFactors I ∩ normalizedFactors J).prod = normalizedFactors I ∩ normalizedFactors J<VAR>this : (normalizedFactors I ∩ normalizedFactors J).prod ≠ 0<GOAL>I ⊔ J = (normalizedFactors I ∩ normalizedFactors J).prod