ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>E' : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>𝕜 : Type u_5<VAR>p : ℝ≥0∞<VAR>inst✝¹⁰ : RCLike 𝕜<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : InnerProductSpace 𝕜 E'<VAR>inst✝⁷ : CompleteSpace E'<VAR>inst✝⁶ : NormedSpace ℝ E'<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace 𝕜 F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : CompleteSpace F'<VAR>ι : Type u_6<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>hm : m ≤ m0<VAR>c : 𝕜<VAR>f : ↥(lpMeas F 𝕜 m p μ)<GOAL>↑↑(lpMeasToLpTrim F 𝕜 p μ hm (c • f)) =ᶠ[ae μ] c • ↑↑(lpMeasToLpTrim F 𝕜 p μ hm f)
<VAR>α : Type u_1<VAR>E' : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>𝕜 : Type u_5<VAR>p : ℝ≥0∞<VAR>inst✝¹⁰ : RCLike 𝕜<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : InnerProductSpace 𝕜 E'<VAR>inst✝⁷ : CompleteSpace E'<VAR>inst✝⁶ : NormedSpace ℝ E'<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace 𝕜 F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : CompleteSpace F'<VAR>ι : Type u_6<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>hm : m ≤ m0<VAR>c : 𝕜<VAR>f : ↥(lpMeas F 𝕜 m p μ)<GOAL>↑↑↑(c • f) =ᶠ[ae μ] c • ↑↑(lpMeasToLpTrim F 𝕜 p μ hm f)
<VAR>α : Type u_1<VAR>E' : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>𝕜 : Type u_5<VAR>p : ℝ≥0∞<VAR>inst✝¹⁰ : RCLike 𝕜<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : InnerProductSpace 𝕜 E'<VAR>inst✝⁷ : CompleteSpace E'<VAR>inst✝⁶ : NormedSpace ℝ E'<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace 𝕜 F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : CompleteSpace F'<VAR>ι : Type u_6<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>hm : m ≤ m0<VAR>c : 𝕜<VAR>f : ↥(lpMeas F 𝕜 m p μ)<GOAL>c • ↑↑↑f =ᶠ[ae μ] c • ↑↑(lpMeasToLpTrim F 𝕜 p μ hm f)
<VAR>α : Type u_1<VAR>E' : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>𝕜 : Type u_5<VAR>p : ℝ≥0∞<VAR>inst✝¹⁰ : RCLike 𝕜<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : InnerProductSpace 𝕜 E'<VAR>inst✝⁷ : CompleteSpace E'<VAR>inst✝⁶ : NormedSpace ℝ E'<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace 𝕜 F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : CompleteSpace F'<VAR>ι : Type u_6<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>hm : m ≤ m0<VAR>c : 𝕜<VAR>f : ↥(lpMeas F 𝕜 m p μ)<VAR>x : α<VAR>hx : ↑↑(lpMeasToLpTrim F 𝕜 p μ hm f) x = ↑↑↑f x<GOAL>(c • ↑↑↑f) x = (c • ↑↑(lpMeasToLpTrim F 𝕜 p μ hm f)) x
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : MeasurableSpace E<VAR>inst✝⁵ : BorelSpace E<VAR>inst✝⁴ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝³ : μ.IsAddHaarMeasure<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>r : ℝ<VAR>hr : r ≠ 0<VAR>s : Set E<GOAL>(map (fun x => r • x) μ) s = ENNReal.ofReal |(r ^ finrank ℝ E)⁻¹| * μ s
<VAR>C✝ : Type u<VAR>𝒞 : Category.{v, u} C✝<VAR>inst✝² : MonoidalCategory C✝<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : MonoidalCategory C<VAR>U V✝ W✝ X✝ Y✝ Z✝ V W X Y Z : C<VAR>f : V ≅ W<VAR>g : X ⟶ Y<VAR>h : Y ⟶ Z<GOAL>(g ⊗ f.inv) ≫ (h ⊗ f.hom) = (g ⊗ 𝟙 W) ≫ (h ⊗ 𝟙 W)
<VAR>C✝ : Type u<VAR>𝒞 : Category.{v, u} C✝<VAR>inst✝² : MonoidalCategory C✝<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : MonoidalCategory C<VAR>U V✝ W✝ X✝ Y✝ Z✝ V W X Y Z : C<VAR>f : V ≅ W<VAR>g : X ⟶ Y<VAR>h : Y ⟶ Z<GOAL>g ≫ h ⊗ 𝟙 W = (g ⊗ 𝟙 W) ≫ (h ⊗ 𝟙 W)
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝¹ : PseudoMetricSpace α<VAR>x y z : α<VAR>δ ε ε₁ ε₂ : ℝ<VAR>s : Set α<VAR>inst✝ : TopologicalSpace β<VAR>F : ι → β → α<VAR>f : β → α<VAR>p : Filter ι<GOAL>TendstoLocallyUniformly F f p ↔ ∀ ε > 0, ∀ (x : β), ∃ t ∈ 𝓝 x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, dist (f y) (F n y) < ε
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>a✝ a b : α<VAR>i j : ℕ<VAR>c : α<VAR>l : List α<VAR>h₀ : i + 1 ≤ j + 1<VAR>h₁ : j + 1 ≤ (c :: l).length<GOAL>insertNth (j + 1 + 1) b (insertNth (i + 1) a (c :: l)) = insertNth (i + 1) a (insertNth (j + 1) b (c :: l))
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>a✝ a b : α<VAR>i j : ℕ<VAR>c : α<VAR>l : List α<VAR>h₀ : i + 1 ≤ j + 1<VAR>h₁ : j + 1 ≤ (c :: l).length<GOAL>insertNth (j + 1) b (insertNth i a l) = insertNth i a (insertNth j b l)
<VAR>n✝ b b' : ℕ<VAR>c : ℤ<VAR>h : ↑b ∣ ↑b' - c<VAR>n : ℕ<GOAL>b ∣ n ↔ ↑b ∣ ofDigits c (b'.digits n)
<VAR>n✝ b b' : ℕ<VAR>c : ℤ<VAR>h : ↑b ∣ ↑b' - c<VAR>n : ℕ<GOAL>↑b ∣ ↑n ↔ ↑b ∣ ofDigits c (b'.digits n)
<VAR>R : Type u<VAR>S : Type v<VAR>a✝ b c d : R<VAR>n m : ℕ<VAR>inst✝ : Semiring R<VAR>p✝¹ p✝ q : R[X]<VAR>ι : Type u_1<VAR>a : R<VAR>p : R[X]<GOAL>(a • p).degree ≤ p.degree
<VAR>R : Type u<VAR>S : Type v<VAR>a✝ b c d : R<VAR>n m✝ : ℕ<VAR>inst✝ : Semiring R<VAR>p✝¹ p✝ q : R[X]<VAR>ι : Type u_1<VAR>a : R<VAR>p : R[X]<VAR>m : ℕ<VAR>hm : p.degree < ↑m<GOAL>(a • p).coeff m = 0
<VAR>R : Type u<VAR>S : Type v<VAR>a✝ b c d : R<VAR>n m✝ : ℕ<VAR>inst✝ : Semiring R<VAR>p✝¹ p✝ q : R[X]<VAR>ι : Type u_1<VAR>a : R<VAR>p : R[X]<VAR>m : ℕ<VAR>hm : ∀ (m_1 : ℕ), m ≤ m_1 → p.coeff m_1 = 0<GOAL>(a • p).coeff m = 0
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f✝ f₀ f₁ : E → F<VAR>f'✝ : F<VAR>s t : Set E<VAR>x v : E<VAR>L : E →L[𝕜] F<VAR>f : E → F<VAR>f' : F<VAR>x₀ : E<VAR>hf : HasLineDerivAt 𝕜 f f' x₀ v<VAR>C : ℝ<VAR>hC₀ : 0 ≤ C<VAR>hlip : ∀ᶠ (x : E) in 𝓝 x₀, ‖f x - f x₀‖ ≤ C * ‖x - x₀‖<GOAL>‖f'‖ ≤ C * ‖v‖
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f✝ f₀ f₁ : E → F<VAR>f'✝ : F<VAR>s t : Set E<VAR>x v : E<VAR>L : E →L[𝕜] F<VAR>f : E → F<VAR>f' : F<VAR>x₀ : E<VAR>hf : HasLineDerivAt 𝕜 f f' x₀ v<VAR>C : ℝ<VAR>hC₀ : 0 ≤ C<VAR>hlip : ∀ᶠ (x : E) in 𝓝 x₀, ‖f x - f x₀‖ ≤ C * ‖x - x₀‖<GOAL>∀ᶠ (x : 𝕜) in 𝓝 0, ‖f (x₀ + x • v) - f (x₀ + 0 • v)‖ ≤ C * ‖v‖ * ‖x - 0‖
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f✝ f₀ f₁ : E → F<VAR>f'✝ : F<VAR>s t : Set E<VAR>x v : E<VAR>L : E →L[𝕜] F<VAR>f : E → F<VAR>f' : F<VAR>x₀ : E<VAR>hf : HasLineDerivAt 𝕜 f f' x₀ v<VAR>C : ℝ<VAR>hC₀ : 0 ≤ C<VAR>hlip : ∀ᶠ (x : E) in 𝓝 x₀, ‖f x - f x₀‖ ≤ C * ‖x - x₀‖<VAR>A : Continuous fun t => x₀ + t • v<VAR>this : ∀ᶠ (x : E) in 𝓝 (x₀ + 0 • v), ‖f x - f x₀‖ ≤ C * ‖x - x₀‖<GOAL>∀ᶠ (x : 𝕜) in 𝓝 0, ‖f (x₀ + x • v) - f (x₀ + 0 • v)‖ ≤ C * ‖v‖ * ‖x - 0‖
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f✝ f₀ f₁ : E → F<VAR>f'✝ : F<VAR>s t✝ : Set E<VAR>x v : E<VAR>L : E →L[𝕜] F<VAR>f : E → F<VAR>f' : F<VAR>x₀ : E<VAR>hf : HasLineDerivAt 𝕜 f f' x₀ v<VAR>C : ℝ<VAR>hC₀ : 0 ≤ C<VAR>hlip : ∀ᶠ (x : E) in 𝓝 x₀, ‖f x - f x₀‖ ≤ C * ‖x - x₀‖<VAR>A : Continuous fun t => x₀ + t • v<VAR>this : ∀ᶠ (x : E) in 𝓝 (x₀ + 0 • v), ‖f x - f x₀‖ ≤ C * ‖x - x₀‖<VAR>t : 𝕜<VAR>ht : t ∈ (fun t => x₀ + t • v) ⁻¹' {x | ‖f x - f x₀‖ ≤ C * ‖x - x₀‖}<GOAL>‖f (x₀ + t • v) - f (x₀ + 0 • v)‖ ≤ C * ‖v‖ * ‖t - 0‖
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f✝ f₀ f₁ : E → F<VAR>f'✝ : F<VAR>s t✝ : Set E<VAR>x v : E<VAR>L : E →L[𝕜] F<VAR>f : E → F<VAR>f' : F<VAR>x₀ : E<VAR>hf : HasLineDerivAt 𝕜 f f' x₀ v<VAR>C : ℝ<VAR>hC₀ : 0 ≤ C<VAR>hlip : ∀ᶠ (x : E) in 𝓝 x₀, ‖f x - f x₀‖ ≤ C * ‖x - x₀‖<VAR>A : Continuous fun t => x₀ + t • v<VAR>this : ∀ᶠ (x : E) in 𝓝 (x₀ + 0 • v), ‖f x - f x₀‖ ≤ C * ‖x - x₀‖<VAR>t : 𝕜<VAR>ht : ‖f (x₀ + t • v) - f x₀‖ ≤ C * (‖v‖ * ‖t‖)<GOAL>‖f (x₀ + t • v) - f (x₀ + 0 • v)‖ ≤ C * ‖v‖ * ‖t - 0‖
<VAR>M : Type u_1<VAR>inst✝² : Zero M<VAR>l : List M<VAR>inst✝¹ : DecidablePred fun x => l.getD x 0 ≠ 0<VAR>n : ℕ<VAR>x : M<VAR>inst✝ : DecidablePred fun x_1 => [x].getD x_1 0 ≠ 0<GOAL>[x].toFinsupp = Finsupp.single 0 x
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>a b : α<VAR>s s₁ s₂ t t₁ t₂ u : Set α<GOAL>(s ∩ t).Nonempty ↔ ∃ x ∈ t, x ∈ s
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>M : Type u_3<VAR>inst✝⁶ : Semiring R<VAR>inst✝⁵ : Semiring S<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>inst✝² : Module S M<VAR>inst✝¹ : SMul S R<VAR>inst✝ : IsScalarTower S R M<VAR>p✝ q : Submodule R M<VAR>s : Set (Submodule R M)<VAR>p : Submodule R M := { toAddSubmonoid := sSup (toAddSubmonoid '' s), smul_mem' := ⋯ }<GOAL>(sSup s).toAddSubmonoid = sSup (toAddSubmonoid '' s)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>M : Type u_3<VAR>inst✝⁶ : Semiring R<VAR>inst✝⁵ : Semiring S<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>inst✝² : Module S M<VAR>inst✝¹ : SMul S R<VAR>inst✝ : IsScalarTower S R M<VAR>p✝ q : Submodule R M<VAR>s : Set (Submodule R M)<VAR>p : Submodule R M := { toAddSubmonoid := sSup (toAddSubmonoid '' s), smul_mem' := ⋯ }<GOAL>sSup s ≤ p
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>M : Type u_3<VAR>inst✝⁶ : Semiring R<VAR>inst✝⁵ : Semiring S<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>inst✝² : Module S M<VAR>inst✝¹ : SMul S R<VAR>inst✝ : IsScalarTower S R M<VAR>p✝ q : Submodule R M<VAR>s : Set (Submodule R M)<VAR>p : Submodule R M := { toAddSubmonoid := sSup (toAddSubmonoid '' s), smul_mem' := ⋯ }<GOAL>sSup (toAddSubmonoid '' s) ≤ (sSup s).toAddSubmonoid
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>δ : Type u_3<VAR>σ✝ : α → Type u_4<VAR>a : α<VAR>s : Multiset α<VAR>t✝ : (a : α) → Multiset (σ✝ a)<VAR>σ : α → Type u_5<VAR>t : (a : α) → Multiset (σ a)<VAR>l₁ : List α<GOAL>Nodup (Quot.mk Setoid.r l₁) → (∀ (a : α), (t a).Nodup) → (Multiset.sigma (Quot.mk Setoid.r l₁) t).Nodup
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>δ : Type u_3<VAR>σ✝ : α → Type u_4<VAR>a : α<VAR>s : Multiset α<VAR>t✝ : (a : α) → Multiset (σ✝ a)<VAR>σ : α → Type u_5<VAR>t : (a : α) → Multiset (σ a)<VAR>l₁ : List α<VAR>f : (a : α) → List (σ a)<VAR>hf : ∀ (a : α), ⟦f a⟧ = t a<GOAL>Nodup (Quot.mk Setoid.r l₁) → (∀ (a : α), (t a).Nodup) → (Multiset.sigma (Quot.mk Setoid.r l₁) t).Nodup
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α → ℝ≥0<VAR>hf : Summable f<VAR>s : Set α<GOAL>Summable (s.indicator f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α → ℝ≥0<VAR>hf : Summable f<VAR>s : Set α<VAR>a : α<GOAL>(if a ∈ s then f a else 0) ≤ f a
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedSemifield α<VAR>a b c d e : α<VAR>m n : ℤ<VAR>ha : 0 < a<VAR>hb : 0 < b<GOAL>a⁻¹ ≤ b⁻¹ ↔ b ≤ a
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n m : ℕ<VAR>inst✝ : Ring R<VAR>p q : R[X]<VAR>h : p.degree < q.degree<GOAL>(p - q).leadingCoeff = -q.leadingCoeff
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n m : ℕ<VAR>inst✝ : Ring R<VAR>p q : R[X]<VAR>h : p.degree < (-q).degree<GOAL>(p - q).leadingCoeff = -q.leadingCoeff
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>C : Type u_4<VAR>inst✝⁶ : CommSemiring R<VAR>inst✝⁵ : Semiring A<VAR>inst✝⁴ : Algebra R A<VAR>inst✝³ : Semiring B<VAR>inst✝² : Algebra R B<VAR>inst✝¹ : Semiring C<VAR>inst✝ : Algebra R C<VAR>f : A →ₐ[R] B<VAR>g : A →ₐ[R] C<VAR>r : R<GOAL>(↑↑__src✝).toFun ((algebraMap R A) r) = (algebraMap R (B × C)) r
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : LinearOrderedField α<VAR>inst✝¹ : Ring β<VAR>abv : β → α<VAR>inst✝ : IsAbsoluteValue abv<VAR>f g : CauSeq β abv<VAR>hfg : (f - g).LimZero<GOAL>(g - f).LimZero
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>p : F[X]<VAR>sp : Polynomial.IsSplittingField F E p<VAR>hp : p.Separable<GOAL>IsGalois F E
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>p : F[X]<VAR>sp : Polynomial.IsSplittingField F E p<VAR>hp : p.Separable<VAR>hFE : FiniteDimensional F E<GOAL>IsGalois F E
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>p : F[X]<VAR>sp : Polynomial.IsSplittingField F E p<VAR>hp : p.Separable<VAR>hFE : FiniteDimensional F E<VAR>this : DecidableEq E := Classical.decEq E<VAR>s : Set E := p.rootSet E<GOAL>IsGalois F E
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>p : F[X]<VAR>sp : Polynomial.IsSplittingField F E p<VAR>hp : p.Separable<VAR>hFE : FiniteDimensional F E<VAR>this : DecidableEq E := Classical.decEq E<VAR>s : Set E := p.rootSet E<VAR>adjoin_root : IntermediateField.adjoin F s = ⊤<GOAL>IsGalois F E
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>p : F[X]<VAR>sp : Polynomial.IsSplittingField F E p<VAR>hp : p.Separable<VAR>hFE : FiniteDimensional F E<VAR>this : DecidableEq E := Classical.decEq E<VAR>s : Set E := p.rootSet E<VAR>adjoin_root : IntermediateField.adjoin F s = ⊤<VAR>P : IntermediateField F E → Prop := fun K => Fintype.card (↥K →ₐ[F] E) = finrank F ↥K<GOAL>IsGalois F E
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>p : F[X]<VAR>sp : Polynomial.IsSplittingField F E p<VAR>hp : p.Separable<VAR>hFE : FiniteDimensional F E<VAR>this : DecidableEq E := Classical.decEq E<VAR>s : Set E := p.rootSet E<VAR>adjoin_root : IntermediateField.adjoin F s = ⊤<VAR>P : IntermediateField F E → Prop := fun K => Fintype.card (↥K →ₐ[F] E) = finrank F ↥K<GOAL>P (IntermediateField.adjoin F s)
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>p : F[X]<VAR>sp : Polynomial.IsSplittingField F E p<VAR>hp : p.Separable<VAR>hFE : FiniteDimensional F E<VAR>this : DecidableEq E := Classical.decEq E<VAR>s : Set E := p.rootSet E<VAR>adjoin_root : IntermediateField.adjoin F s = ⊤<VAR>P : IntermediateField F E → Prop := fun K => Fintype.card (↥K →ₐ[F] E) = finrank F ↥K<GOAL>P ⊥
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>p : F[X]<VAR>sp : Polynomial.IsSplittingField F E p<VAR>hp : p.Separable<VAR>hFE : FiniteDimensional F E<VAR>this : DecidableEq E := Classical.decEq E<VAR>s : Set E := p.rootSet E<VAR>adjoin_root : IntermediateField.adjoin F s = ⊤<VAR>P : IntermediateField F E → Prop := fun K => Fintype.card (↥K →ₐ[F] E) = finrank F ↥K<GOAL>∀ (K : IntermediateField F E), ∀ x ∈ (p.aroots E).toFinset, P K → P (IntermediateField.restrictScalars F (↥K)⟮x⟯)
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>p : F[X]<VAR>sp : Polynomial.IsSplittingField F E p<VAR>hp : p.Separable<VAR>hFE : FiniteDimensional F E<VAR>this✝¹ : DecidableEq E := Classical.decEq E<VAR>s : Set E := p.rootSet E<VAR>adjoin_root : IntermediateField.adjoin F s = ⊤<VAR>P : IntermediateField F E → Prop := fun K => Fintype.card (↥K →ₐ[F] E) = finrank F ↥K<VAR>K : IntermediateField F E<VAR>x : E<VAR>hx : x ∈ (p.aroots E).toFinset<VAR>hK : Fintype.card (↥K →ₐ[F] E) = finrank F ↥K<VAR>this✝ : Module ↥K ↥(↥K)⟮x⟯ := (↥K)⟮x⟯.module<VAR>this : IsScalarTower F ↥K ↥(↥K)⟮x⟯ := IntermediateField.isScalarTower (↥K)⟮x⟯<GOAL>Fintype.card (↥(IntermediateField.restrictScalars F (↥K)⟮x⟯) →ₐ[F] E) = finrank F ↥(IntermediateField.restrictScalars F (↥K)⟮x⟯)
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>p : F[X]<VAR>sp : Polynomial.IsSplittingField F E p<VAR>hp : p.Separable<VAR>hFE : FiniteDimensional F E<VAR>this✝¹ : DecidableEq E := Classical.decEq E<VAR>s : Set E := p.rootSet E<VAR>adjoin_root : IntermediateField.adjoin F s = ⊤<VAR>P : IntermediateField F E → Prop := fun K => Fintype.card (↥K →ₐ[F] E) = finrank F ↥K<VAR>K : IntermediateField F E<VAR>x : E<VAR>hx : x ∈ (p.aroots E).toFinset<VAR>hK : Fintype.card (↥K →ₐ[F] E) = finrank F ↥K<VAR>this✝ : Module ↥K ↥(↥K)⟮x⟯ := (↥K)⟮x⟯.module<VAR>this : IsScalarTower F ↥K ↥(↥K)⟮x⟯ := IntermediateField.isScalarTower (↥K)⟮x⟯<GOAL>finrank F ↥(↥K)⟮x⟯ = finrank F ↥(IntermediateField.restrictScalars F (↥K)⟮x⟯)
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>p : F[X]<VAR>sp : Polynomial.IsSplittingField F E p<VAR>hp : p.Separable<VAR>hFE : FiniteDimensional F E<VAR>this✝¹ : DecidableEq E := Classical.decEq E<VAR>s : Set E := p.rootSet E<VAR>adjoin_root : IntermediateField.adjoin F s = ⊤<VAR>P : IntermediateField F E → Prop := fun K => Fintype.card (↥K →ₐ[F] E) = finrank F ↥K<VAR>K : IntermediateField F E<VAR>x : E<VAR>hx : x ∈ (p.aroots E).toFinset<VAR>hK : Fintype.card (↥K →ₐ[F] E) = finrank F ↥K<VAR>this✝ : Module ↥K ↥(↥K)⟮x⟯ := (↥K)⟮x⟯.module<VAR>this : IsScalarTower F ↥K ↥(↥K)⟮x⟯ := IntermediateField.isScalarTower (↥K)⟮x⟯<GOAL>finrank F ↥(IntermediateField.restrictScalars F (↥K)⟮x⟯) = finrank F ↥(↥K)⟮x⟯
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>p : F[X]<VAR>sp : Polynomial.IsSplittingField F E p<VAR>hp : p.Separable<VAR>hFE : FiniteDimensional F E<VAR>this✝¹ : DecidableEq E := Classical.decEq E<VAR>s : Set E := p.rootSet E<VAR>adjoin_root : IntermediateField.adjoin F s = ⊤<VAR>P : IntermediateField F E → Prop := fun K => Fintype.card (↥K →ₐ[F] E) = finrank F ↥K<VAR>K : IntermediateField F E<VAR>x : E<VAR>hx : x ∈ (p.aroots E).toFinset<VAR>hK : Fintype.card (↥K →ₐ[F] E) = finrank F ↥K<VAR>this✝ : Module ↥K ↥(↥K)⟮x⟯ := (↥K)⟮x⟯.module<VAR>this : IsScalarTower F ↥K ↥(↥K)⟮x⟯ := IntermediateField.isScalarTower (↥K)⟮x⟯<GOAL>↥(IntermediateField.restrictScalars F (↥K)⟮x⟯) ≃ₗ[F] ↥(↥K)⟮x⟯
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝⁹ : NormedAddCommGroup D<VAR>inst✝⁸ : NormedSpace 𝕜 D<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type u_2<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f f₁ : E → F<VAR>g : F → G<VAR>x x₀ : E<VAR>c : F<VAR>b : E × F → G<VAR>m n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>f₂ : 𝕜 → F<VAR>s₂ : Set 𝕜<GOAL>ContDiff 𝕜 ⊤ f₂ ↔ Differentiable 𝕜 f₂ ∧ ContDiff 𝕜 ⊤ (deriv f₂)
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝⁹ : NormedAddCommGroup D<VAR>inst✝⁸ : NormedSpace 𝕜 D<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type u_2<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f f₁ : E → F<VAR>g : F → G<VAR>x x₀ : E<VAR>c : F<VAR>b : E × F → G<VAR>m n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>f₂ : 𝕜 → F<VAR>s₂ : Set 𝕜<GOAL>ContDiffOn 𝕜 ⊤ f₂ univ ↔ DifferentiableOn 𝕜 f₂ univ ∧ ContDiffOn 𝕜 ⊤ (derivWithin f₂ univ) univ
<VAR>a b m n✝ p✝ n p : ℕ<VAR>hn : n ≠ 0<GOAL>0 < n / p ^ n.factorization p
<VAR>E : Type u_1<VAR>X : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : TopologicalSpace X<VAR>a✝ b✝ b₀✝ b₁ b₂ : ℝ<VAR>μ : Measure ℝ<VAR>f : ℝ → E<VAR>inst✝ : FirstCountableTopology X<VAR>F : X → ℝ → E<VAR>bound : ℝ → ℝ<VAR>a b a₀ b₀ : ℝ<VAR>x₀ : X<VAR>hF_meas : ∀ (x : X), AEStronglyMeasurable (F x) (μ.restrict (Ι a b))<VAR>h_bound : ∀ᶠ (x : X) in 𝓝 x₀, ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), ‖F x t‖ ≤ bound t<VAR>bound_integrable : IntervalIntegrable bound μ a b<VAR>h_cont : ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), ContinuousAt (fun x => F x t) x₀<VAR>ha₀ : a₀ ∈ Ioo a b<VAR>hb₀ : b₀ ∈ Ioo a b<VAR>hμb₀ : μ {b₀} = 0<GOAL>ContinuousAt (fun p => ∫ (t : ℝ) in a₀..p.2, F p.1 t ∂μ) (x₀, b₀)
<VAR>E : Type u_1<VAR>X : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : TopologicalSpace X<VAR>a✝ b✝ b₀✝ b₁ b₂ : ℝ<VAR>μ : Measure ℝ<VAR>f : ℝ → E<VAR>inst✝ : FirstCountableTopology X<VAR>F : X → ℝ → E<VAR>bound : ℝ → ℝ<VAR>a b a₀ b₀ : ℝ<VAR>x₀ : X<VAR>hF_meas : ∀ (x : X), AEStronglyMeasurable (F x) (μ.restrict (Ι a b))<VAR>h_bound : ∀ᶠ (x : X) in 𝓝 x₀, ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), ‖F x t‖ ≤ bound t<VAR>bound_integrable : IntervalIntegrable bound μ a b<VAR>h_cont : ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), ContinuousAt (fun x => F x t) x₀<VAR>ha₀ : a₀ ∈ Ioo a b<VAR>hb₀ : b₀ ∈ Ioo a b<VAR>hμb₀ : μ {b₀} = 0<VAR>hsub : ∀ {a₀ b₀ : ℝ}, a₀ ∈ Ioo a b → b₀ ∈ Ioo a b → Ι a₀ b₀ ⊆ Ι a b<GOAL>ContinuousAt (fun p => ∫ (t : ℝ) in a₀..p.2, F p.1 t ∂μ) (x₀, b₀)
<VAR>E : Type u_1<VAR>X : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : TopologicalSpace X<VAR>a✝ b✝ b₀✝ b₁ b₂ : ℝ<VAR>μ : Measure ℝ<VAR>f : ℝ → E<VAR>inst✝ : FirstCountableTopology X<VAR>F : X → ℝ → E<VAR>bound : ℝ → ℝ<VAR>a b a₀ b₀ : ℝ<VAR>x₀ : X<VAR>hF_meas : ∀ (x : X), AEStronglyMeasurable (F x) (μ.restrict (Ι a b))<VAR>h_bound : ∀ᶠ (x : X) in 𝓝 x₀, ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), ‖F x t‖ ≤ bound t<VAR>bound_integrable : IntervalIntegrable bound μ a b<VAR>h_cont : ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), ContinuousAt (fun x => F x t) x₀<VAR>ha₀ : a₀ ∈ Ioo a b<VAR>hb₀ : b₀ ∈ Ioo a b<VAR>hμb₀ : μ {b₀} = 0<VAR>hsub : ∀ {a₀ b₀ : ℝ}, a₀ ∈ Ioo a b → b₀ ∈ Ioo a b → Ι a₀ b₀ ⊆ Ι a b<VAR>Ioo_nhds : Ioo a b ∈ 𝓝 b₀<GOAL>ContinuousAt (fun p => ∫ (t : ℝ) in a₀..p.2, F p.1 t ∂μ) (x₀, b₀)
<VAR>E : Type u_1<VAR>X : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : TopologicalSpace X<VAR>a✝ b✝ b₀✝ b₁ b₂ : ℝ<VAR>μ : Measure ℝ<VAR>f : ℝ → E<VAR>inst✝ : FirstCountableTopology X<VAR>F : X → ℝ → E<VAR>bound : ℝ → ℝ<VAR>a b a₀ b₀ : ℝ<VAR>x₀ : X<VAR>hF_meas : ∀ (x : X), AEStronglyMeasurable (F x) (μ.restrict (Ι a b))<VAR>h_bound : ∀ᶠ (x : X) in 𝓝 x₀, ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), ‖F x t‖ ≤ bound t<VAR>bound_integrable : IntervalIntegrable bound μ a b<VAR>h_cont : ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), ContinuousAt (fun x => F x t) x₀<VAR>ha₀ : a₀ ∈ Ioo a b<VAR>hb₀ : b₀ ∈ Ioo a b<VAR>hμb₀ : μ {b₀} = 0<VAR>hsub : ∀ {a₀ b₀ : ℝ}, a₀ ∈ Ioo a b → b₀ ∈ Ioo a b → Ι a₀ b₀ ⊆ Ι a b<VAR>Ioo_nhds : Ioo a b ∈ 𝓝 b₀<VAR>Icc_nhds : Icc a b ∈ 𝓝 b₀<GOAL>ContinuousAt (fun p => ∫ (t : ℝ) in a₀..p.2, F p.1 t ∂μ) (x₀, b₀)
<VAR>E : Type u_1<VAR>X : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : TopologicalSpace X<VAR>a✝ b✝ b₀✝ b₁ b₂ : ℝ<VAR>μ : Measure ℝ<VAR>f : ℝ → E<VAR>inst✝ : FirstCountableTopology X<VAR>F : X → ℝ → E<VAR>bound : ℝ → ℝ<VAR>a b a₀ b₀ : ℝ<VAR>x₀ : X<VAR>hF_meas : ∀ (x : X), AEStronglyMeasurable (F x) (μ.restrict (Ι a b))<VAR>h_bound : ∀ᶠ (x : X) in 𝓝 x₀, ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), ‖F x t‖ ≤ bound t<VAR>bound_integrable : IntervalIntegrable bound μ a b<VAR>h_cont : ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), ContinuousAt (fun x => F x t) x₀<VAR>ha₀ : a₀ ∈ Ioo a b<VAR>hb₀ : b₀ ∈ Ioo a b<VAR>hμb₀ : μ {b₀} = 0<VAR>hsub : ∀ {a₀ b₀ : ℝ}, a₀ ∈ Ioo a b → b₀ ∈ Ioo a b → Ι a₀ b₀ ⊆ Ι a b<VAR>Ioo_nhds : Ioo a b ∈ 𝓝 b₀<VAR>Icc_nhds : Icc a b ∈ 𝓝 b₀<VAR>hx₀ : ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), ‖F x₀ t‖ ≤ bound t<GOAL>ContinuousAt (fun p => ∫ (t : ℝ) in a₀..p.2, F p.1 t ∂μ) (x₀, b₀)