ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>inst✝¹ : CompleteSpace F<VAR>μ : Measure α<VAR>s : Set E<VAR>t : Set α<VAR>f : α → E<VAR>g✝ : E → ℝ<VAR>C : ℝ<VAR>inst✝ : IsProbabilityMeasure μ<VAR>hs : Convex ℝ s<VAR>hsc : IsClosed s<VAR>hf : ∀ᵐ (x : α) ∂μ, f x ∈ s<VAR>this✝¹ : MeasurableSpace E := borel E<VAR>this✝ : BorelSpace E<VAR>g : α → E<VAR>hfi : Integrable g μ<VAR>hgm : StronglyMeasurable g<VAR>hfg : f =ᶠ[ae μ] g<VAR>this : SeparableSpace ↑(range g ∩ s)<VAR>y₀ : E<VAR>h₀ : y₀ ∈ range g ∩ s<GOAL>∫ (a : α), g a ∂μ ∈ s
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>inst✝¹ : CompleteSpace F<VAR>μ : Measure α<VAR>s : Set E<VAR>t : Set α<VAR>f : α → E<VAR>g✝ : E → ℝ<VAR>C : ℝ<VAR>inst✝ : IsProbabilityMeasure μ<VAR>hs : Convex ℝ s<VAR>hsc : IsClosed s<VAR>hf : ∀ᵐ (x : α) ∂μ, f x ∈ s<VAR>this✝¹ : MeasurableSpace E := borel E<VAR>this✝ : BorelSpace E<VAR>g : α → E<VAR>hfi : Integrable g μ<VAR>hgm : StronglyMeasurable g<VAR>hfg : f =ᶠ[ae μ] g<VAR>this : SeparableSpace ↑(range g ∩ s)<VAR>y₀ : E<VAR>h₀ : y₀ ∈ range g ∩ s<VAR>hg : ∀ᵐ (x : α) ∂μ, g x ∈ closure (range g ∩ s)<GOAL>∫ (a : α), g a ∂μ ∈ s
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>inst✝¹ : CompleteSpace F<VAR>μ : Measure α<VAR>s : Set E<VAR>t : Set α<VAR>f : α → E<VAR>g✝ : E → ℝ<VAR>C : ℝ<VAR>inst✝ : IsProbabilityMeasure μ<VAR>hs : Convex ℝ s<VAR>hsc : IsClosed s<VAR>hf : ∀ᵐ (x : α) ∂μ, f x ∈ s<VAR>this✝¹ : MeasurableSpace E := borel E<VAR>this✝ : BorelSpace E<VAR>g : α → E<VAR>hfi : Integrable g μ<VAR>hgm : StronglyMeasurable g<VAR>hfg : f =ᶠ[ae μ] g<VAR>this : SeparableSpace ↑(range g ∩ s)<VAR>y₀ : E<VAR>h₀ : y₀ ∈ range g ∩ s<VAR>hg : ∀ᵐ (x : α) ∂μ, g x ∈ closure (range g ∩ s)<VAR>G : ℕ → SimpleFunc α E := SimpleFunc.approxOn g ⋯ (range g ∩ s) y₀ h₀<GOAL>∫ (a : α), g a ∂μ ∈ s
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>inst✝¹ : CompleteSpace F<VAR>μ : Measure α<VAR>s : Set E<VAR>t : Set α<VAR>f : α → E<VAR>g✝ : E → ℝ<VAR>C : ℝ<VAR>inst✝ : IsProbabilityMeasure μ<VAR>hs : Convex ℝ s<VAR>hsc : IsClosed s<VAR>hf : ∀ᵐ (x : α) ∂μ, f x ∈ s<VAR>this✝² : MeasurableSpace E := borel E<VAR>this✝¹ : BorelSpace E<VAR>g : α → E<VAR>hfi : Integrable g μ<VAR>hgm : StronglyMeasurable g<VAR>hfg : f =ᶠ[ae μ] g<VAR>this✝ : SeparableSpace ↑(range g ∩ s)<VAR>y₀ : E<VAR>h₀ : y₀ ∈ range g ∩ s<VAR>hg : ∀ᵐ (x : α) ∂μ, g x ∈ closure (range g ∩ s)<VAR>G : ℕ → SimpleFunc α E := SimpleFunc.approxOn g ⋯ (range g ∩ s) y₀ h₀<VAR>this : Tendsto (fun n => SimpleFunc.integral μ (G n)) atTop (𝓝 (∫ (x : α), g x ∂μ))<GOAL>∫ (a : α), g a ∂μ ∈ s
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>inst✝¹ : CompleteSpace F<VAR>μ : Measure α<VAR>s : Set E<VAR>t : Set α<VAR>f : α → E<VAR>g✝ : E → ℝ<VAR>C : ℝ<VAR>inst✝ : IsProbabilityMeasure μ<VAR>hs : Convex ℝ s<VAR>hsc : IsClosed s<VAR>hf : ∀ᵐ (x : α) ∂μ, f x ∈ s<VAR>this✝² : MeasurableSpace E := borel E<VAR>this✝¹ : BorelSpace E<VAR>g : α → E<VAR>hfi : Integrable g μ<VAR>hgm : StronglyMeasurable g<VAR>hfg : f =ᶠ[ae μ] g<VAR>this✝ : SeparableSpace ↑(range g ∩ s)<VAR>y₀ : E<VAR>h₀ : y₀ ∈ range g ∩ s<VAR>hg : ∀ᵐ (x : α) ∂μ, g x ∈ closure (range g ∩ s)<VAR>G : ℕ → SimpleFunc α E := SimpleFunc.approxOn g ⋯ (range g ∩ s) y₀ h₀<VAR>this : Tendsto (fun n => SimpleFunc.integral μ (G n)) atTop (𝓝 (∫ (x : α), g x ∂μ))<VAR>n : ℕ<GOAL>∀ i ∈ (G n).range, 0 ≤ (μ (↑(G n) ⁻¹' {i})).toReal
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>inst✝¹ : CompleteSpace F<VAR>μ : Measure α<VAR>s : Set E<VAR>t : Set α<VAR>f : α → E<VAR>g✝ : E → ℝ<VAR>C : ℝ<VAR>inst✝ : IsProbabilityMeasure μ<VAR>hs : Convex ℝ s<VAR>hsc : IsClosed s<VAR>hf : ∀ᵐ (x : α) ∂μ, f x ∈ s<VAR>this✝² : MeasurableSpace E := borel E<VAR>this✝¹ : BorelSpace E<VAR>g : α → E<VAR>hfi : Integrable g μ<VAR>hgm : StronglyMeasurable g<VAR>hfg : f =ᶠ[ae μ] g<VAR>this✝ : SeparableSpace ↑(range g ∩ s)<VAR>y₀ : E<VAR>h₀ : y₀ ∈ range g ∩ s<VAR>hg : ∀ᵐ (x : α) ∂μ, g x ∈ closure (range g ∩ s)<VAR>G : ℕ → SimpleFunc α E := SimpleFunc.approxOn g ⋯ (range g ∩ s) y₀ h₀<VAR>this : Tendsto (fun n => SimpleFunc.integral μ (G n)) atTop (𝓝 (∫ (x : α), g x ∂μ))<VAR>n : ℕ<GOAL>∑ i ∈ (G n).range, (μ (↑(G n) ⁻¹' {i})).toReal = 1
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>inst✝¹ : CompleteSpace F<VAR>μ : Measure α<VAR>s : Set E<VAR>t : Set α<VAR>f : α → E<VAR>g✝ : E → ℝ<VAR>C : ℝ<VAR>inst✝ : IsProbabilityMeasure μ<VAR>hs : Convex ℝ s<VAR>hsc : IsClosed s<VAR>hf : ∀ᵐ (x : α) ∂μ, f x ∈ s<VAR>this✝² : MeasurableSpace E := borel E<VAR>this✝¹ : BorelSpace E<VAR>g : α → E<VAR>hfi : Integrable g μ<VAR>hgm : StronglyMeasurable g<VAR>hfg : f =ᶠ[ae μ] g<VAR>this✝ : SeparableSpace ↑(range g ∩ s)<VAR>y₀ : E<VAR>h₀ : y₀ ∈ range g ∩ s<VAR>hg : ∀ᵐ (x : α) ∂μ, g x ∈ closure (range g ∩ s)<VAR>G : ℕ → SimpleFunc α E := SimpleFunc.approxOn g ⋯ (range g ∩ s) y₀ h₀<VAR>this : Tendsto (fun n => SimpleFunc.integral μ (G n)) atTop (𝓝 (∫ (x : α), g x ∂μ))<VAR>n : ℕ<GOAL>∀ i ∈ (G n).range, ↑(ContinuousLinearMap.id ℝ E) i ∈ s
<VAR>V : Type u_1<VAR>V' : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : NormedAddCommGroup V'<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : InnerProductSpace ℝ V'<VAR>inst✝¹ : Fact (finrank ℝ V = 2)<VAR>inst✝ : Fact (finrank ℝ V' = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y z : V<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<VAR>hz : z ≠ 0<GOAL>o.oangle (-x) y + o.oangle (-y) z + o.oangle (-z) x = ↑π
<VAR>a b : ℝ<VAR>n✝ m n : ℕ<VAR>hc : Continuous fun u => u ^ n * (1 - u ^ 2) ^ m<GOAL>∫ (x : ℝ) in a..b, sin x ^ (2 * m + 1) * cos x ^ n = -∫ (x : ℝ) in b..a, sin x ^ (2 * m + 1) * cos x ^ n
<VAR>a b : ℝ<VAR>n✝ m n : ℕ<VAR>hc : Continuous fun u => u ^ n * (1 - u ^ 2) ^ m<GOAL>-∫ (x : ℝ) in b..a, sin x ^ (2 * m + 1) * cos x ^ n = ∫ (x : ℝ) in b..a, (1 - cos x ^ 2) ^ m * -sin x * cos x ^ n
<VAR>a b : ℝ<VAR>n✝ m n : ℕ<VAR>hc : Continuous fun u => u ^ n * (1 - u ^ 2) ^ m<GOAL>∫ (x : ℝ) in b..a, (sin x * sin x) ^ m * sin x * cos x ^ n = ∫ (x : ℝ) in b..a, (1 - cos x * cos x) ^ m * sin x * cos x ^ n
<VAR>a b : ℝ<VAR>n✝ m n : ℕ<VAR>hc : Continuous fun u => u ^ n * (1 - u ^ 2) ^ m<VAR>x✝ : ℝ<GOAL>sin x✝ * sin x✝ = 1 - cos x✝ * cos x✝
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>D' : Type u_3<VAR>inst✝³ : Category.{u_4, u_1} C<VAR>inst✝² : Category.{u_5, u_2} D<VAR>inst✝¹ : Category.{?u.28361, u_3} D'<VAR>L : C ⥤ D<VAR>W : MorphismProperty C<VAR>inst✝ : L.IsLocalization W<VAR>Y : C<VAR>P : CostructuredArrow L (L.obj Y) → Prop<VAR>hP₀ : P (CostructuredArrow.mk (𝟙 (L.obj Y)))<VAR>hP₁ : ∀ ⦃X₁ X₂ : C⦄ (f : X₁ ⟶ X₂) (φ : L.obj X₂ ⟶ L.obj Y), P (CostructuredArrow.mk φ) → P (CostructuredArrow.mk (L.map f ≫ φ))<VAR>hP₂ : ∀ ⦃X₁ X₂ : C⦄ (w : X₁ ⟶ X₂) (hw : W w) (φ : L.obj X₁ ⟶ L.obj Y), P (CostructuredArrow.mk φ) → P (CostructuredArrow.mk ((isoOfHom L W w hw).inv ≫ φ))<VAR>g : CostructuredArrow L (L.obj Y)<VAR>g' : StructuredArrow (op ((Functor.fromPUnit (L.obj Y)).obj g.right)) L.op := StructuredArrow.mk g.hom.op<GOAL>P (CostructuredArrow.mk g'.hom.unop)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>f : r ≼i s<VAR>a : α<VAR>b : β<VAR>h : s b (f a)<GOAL>∃ a', f a' = b ∧ r a' a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>f : r ≼i s<VAR>a a' : α<VAR>h : s (f a') (f a)<GOAL>∃ a'_1, f a'_1 = f a' ∧ r a'_1 a
<VAR>a x✝ z x y : ℂ<VAR>h₁ : abs x = abs y<VAR>h₂ : x.arg = y.arg<GOAL>x = y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>𝕜 : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>inst✝⁵ : RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace 𝕜 E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : CompleteSpace F<VAR>u : α → ℝ<VAR>inst✝ : NormedSpace 𝕜 F<VAR>f : α → E → F<VAR>f' : α → E → E →L[𝕜] F<VAR>g g' : α → 𝕜 → F<VAR>v : ℕ → α → ℝ<VAR>s : Set E<VAR>t : Set 𝕜<VAR>x₀ x✝¹ : E<VAR>y₀ y : 𝕜<VAR>N : ℕ∞<VAR>hu : Summable u<VAR>hf : ∀ (n : α) (x : E), HasFDerivAt (f n) (f' n x) x<VAR>hf' : ∀ (n : α) (x : E), ‖f' n x‖ ≤ u n<VAR>hf0 : Summable fun n => f n x₀<VAR>x : E<VAR>x✝ : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E<GOAL>Summable fun n => f n x
<VAR>J : Type u_1<VAR>C : Type u_2<VAR>inst✝² : Category.{u_3, u_1} J<VAR>inst✝¹ : Category.{u_4, u_2} C<VAR>inst✝ : ChosenFiniteProducts C<VAR>F₁ F₁' F₂ F₂' : J ⥤ C<VAR>f : F₁ ⟶ F₁'<VAR>g : F₂ ⟶ F₂'<VAR>j : J<GOAL>(f ⊗ g).app j ≫ (fst F₁' F₂').app j = fst (F₁.obj j) (F₂.obj j) ≫ f.app j
<VAR>J : Type u_1<VAR>C : Type u_2<VAR>inst✝² : Category.{u_3, u_1} J<VAR>inst✝¹ : Category.{u_4, u_2} C<VAR>inst✝ : ChosenFiniteProducts C<VAR>F₁ F₁' F₂ F₂' : J ⥤ C<VAR>f : F₁ ⟶ F₁'<VAR>g : F₂ ⟶ F₂'<VAR>j : J<GOAL>(fst F₁ F₂).app j ≫ f.app j = fst (F₁.obj j) (F₂.obj j) ≫ f.app j
<VAR>α : Type u<VAR>t✝ : TopologicalSpace α<VAR>β : Type u_1<VAR>t : TopologicalSpace β<VAR>inst✝ : SecondCountableTopology β<VAR>f : α → β<GOAL>SecondCountableTopology α
<VAR>α : Type u<VAR>t✝ : TopologicalSpace α<VAR>β : Type u_1<VAR>t : TopologicalSpace β<VAR>inst✝ : SecondCountableTopology β<VAR>f : α → β<VAR>b : Set (Set β)<VAR>hb : b.Countable<VAR>eq : t = generateFrom b<GOAL>SecondCountableTopology α
<VAR>α : Type u<VAR>t✝ : TopologicalSpace α<VAR>β : Type u_1<VAR>t : TopologicalSpace β<VAR>inst✝ : SecondCountableTopology β<VAR>f : α → β<VAR>b : Set (Set β)<VAR>hb : b.Countable<VAR>eq : t = generateFrom b<VAR>this : TopologicalSpace α := induced f t<GOAL>SecondCountableTopology α
<VAR>α : Type u<VAR>t✝ : TopologicalSpace α<VAR>β : Type u_1<VAR>t : TopologicalSpace β<VAR>inst✝ : SecondCountableTopology β<VAR>f : α → β<VAR>b : Set (Set β)<VAR>hb : b.Countable<VAR>eq : t = generateFrom b<VAR>this : TopologicalSpace α := induced f t<GOAL>induced f t = generateFrom (preimage f '' b)
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>H : Type u_1<VAR>R : Type u_2<VAR>inst✝⁶ : CommSemiring k<VAR>inst✝⁵ : Monoid G<VAR>inst✝⁴ : Monoid H<VAR>A : Type u₃<VAR>inst✝³ : Semiring A<VAR>inst✝² : Algebra k A<VAR>B : Type u_3<VAR>inst✝¹ : Semiring B<VAR>inst✝ : Algebra k B<VAR>F : MonoidAlgebra k G →ₐ[k] A<VAR>f : MonoidAlgebra k G<GOAL>F f = sum f fun a b => b • F (single a 1)
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>M₂ : Type w₁<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : LieRing L<VAR>inst✝⁸ : LieAlgebra R L<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>inst✝³ : AddCommGroup M₂<VAR>inst✝² : Module R M₂<VAR>inst✝¹ : LieRingModule L M₂<VAR>inst✝ : LieModule R L M₂<VAR>N N' : LieSubmodule R L M<VAR>I J : LieIdeal R L<VAR>N₂ : LieSubmodule R L M₂<GOAL>⁅I, N ⊓ N'⁆ ≤ ⁅I, N⁆ ⊓ ⁅I, N'⁆
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>M₂ : Type w₁<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : LieRing L<VAR>inst✝⁸ : LieAlgebra R L<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>inst✝³ : AddCommGroup M₂<VAR>inst✝² : Module R M₂<VAR>inst✝¹ : LieRingModule L M₂<VAR>inst✝ : LieModule R L M₂<VAR>N N' : LieSubmodule R L M<VAR>I J : LieIdeal R L<VAR>N₂ : LieSubmodule R L M₂<GOAL>⁅I, N ⊓ N'⁆ ≤ ⁅I, N⁆ ∧ ⁅I, N ⊓ N'⁆ ≤ ⁅I, N'⁆
<VAR>𝕜 : Type u_1<VAR>inst✝⁵ : NontriviallyNormedField 𝕜<VAR>E : Type u<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace 𝕜 E<VAR>F : Type v<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace 𝕜 F<VAR>p✝ : FormalMultilinearSeries 𝕜 E F<VAR>r✝ : ℝ≥0∞<VAR>f : E → F<VAR>x : E<VAR>s : Set E<VAR>inst✝ : CompleteSpace F<VAR>h : AnalyticOn 𝕜 f s<VAR>y : E<VAR>hy : y ∈ s<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>r : ℝ≥0∞<VAR>hp : HasFPowerSeriesOnBall f p y r<GOAL>AnalyticAt 𝕜 (_root_.fderiv 𝕜 f) y
<VAR>R : Type u<VAR>inst✝² : CommRing R<VAR>𝓟 : Ideal R<VAR>f : R[X]<VAR>hf✝ : f.IsWeaklyEisensteinAt 𝓟<VAR>S : Type v<VAR>inst✝¹ : CommRing S<VAR>inst✝ : Algebra R S<VAR>p : R<VAR>x : S<VAR>hx : (aeval x) f = 0<VAR>hmo : f.Monic<VAR>hf : f.IsWeaklyEisensteinAt (Submodule.span R {p})<GOAL>∃ y ∈ adjoin R {x}, (algebraMap R S) p * y = x ^ (Polynomial.map (algebraMap R S) f).natDegree
<VAR>R : Type u<VAR>inst✝² : CommRing R<VAR>𝓟 : Ideal R<VAR>f : R[X]<VAR>hf✝ : f.IsWeaklyEisensteinAt 𝓟<VAR>S : Type v<VAR>inst✝¹ : CommRing S<VAR>inst✝ : Algebra R S<VAR>p : R<VAR>x : S<VAR>hx : x ^ (Polynomial.map (algebraMap R S) f).natDegree + ∑ i : Fin (Polynomial.map (algebraMap R S) f).natDegree, (Polynomial.map (algebraMap R S) f).coeff ↑i * x ^ ↑i = 0<VAR>hmo : f.Monic<VAR>hf : f.IsWeaklyEisensteinAt (Submodule.span R {p})<GOAL>∃ y ∈ adjoin R {x}, (algebraMap R S) p * y = x ^ (Polynomial.map (algebraMap R S) f).natDegree
<VAR>R : Type u<VAR>inst✝² : CommRing R<VAR>𝓟 : Ideal R<VAR>f : R[X]<VAR>hf✝ : f.IsWeaklyEisensteinAt 𝓟<VAR>S : Type v<VAR>inst✝¹ : CommRing S<VAR>inst✝ : Algebra R S<VAR>p : R<VAR>x : S<VAR>hmo : f.Monic<VAR>hf : f.IsWeaklyEisensteinAt (Submodule.span R {p})<VAR>hx : x ^ (Polynomial.map (algebraMap R S) f).natDegree = -∑ i : Fin (Polynomial.map (algebraMap R S) f).natDegree, (Polynomial.map (algebraMap R S) f).coeff ↑i * x ^ ↑i<GOAL>∃ y ∈ adjoin R {x}, (algebraMap R S) p * y = x ^ (Polynomial.map (algebraMap R S) f).natDegree
<VAR>R : Type u<VAR>inst✝² : CommRing R<VAR>𝓟 : Ideal R<VAR>f : R[X]<VAR>hf✝ : f.IsWeaklyEisensteinAt 𝓟<VAR>S : Type v<VAR>inst✝¹ : CommRing S<VAR>inst✝ : Algebra R S<VAR>p : R<VAR>x : S<VAR>hmo : f.Monic<VAR>hf : f.IsWeaklyEisensteinAt (Submodule.span R {p})<VAR>hx : x ^ (Polynomial.map (algebraMap R S) f).natDegree = -∑ i : Fin (Polynomial.map (algebraMap R S) f).natDegree, (Polynomial.map (algebraMap R S) f).coeff ↑i * x ^ ↑i<VAR>this : ∀ n < f.natDegree, p ∣ f.coeff n<GOAL>∃ y ∈ adjoin R {x}, (algebraMap R S) p * y = x ^ (Polynomial.map (algebraMap R S) f).natDegree
<VAR>R : Type u<VAR>inst✝² : CommRing R<VAR>𝓟 : Ideal R<VAR>f : R[X]<VAR>hf✝ : f.IsWeaklyEisensteinAt 𝓟<VAR>S : Type v<VAR>inst✝¹ : CommRing S<VAR>inst✝ : Algebra R S<VAR>p : R<VAR>x : S<VAR>hmo : f.Monic<VAR>hf : f.IsWeaklyEisensteinAt (Submodule.span R {p})<VAR>φ : ℕ → R<VAR>hx : x ^ (Polynomial.map (algebraMap R S) f).natDegree = -∑ i : Fin (Polynomial.map (algebraMap R S) f).natDegree, (algebraMap R S) p * ((algebraMap R S) (φ ↑i) * x ^ ↑i)<VAR>hφ : ∀ n < f.natDegree, f.coeff n = p * φ n<GOAL>∃ y ∈ adjoin R {x}, (algebraMap R S) p * y = x ^ (Polynomial.map (algebraMap R S) f).natDegree
<VAR>R : Type u<VAR>inst✝² : CommRing R<VAR>𝓟 : Ideal R<VAR>f : R[X]<VAR>hf✝ : f.IsWeaklyEisensteinAt 𝓟<VAR>S : Type v<VAR>inst✝¹ : CommRing S<VAR>inst✝ : Algebra R S<VAR>p : R<VAR>x : S<VAR>hmo : f.Monic<VAR>hf : f.IsWeaklyEisensteinAt (Submodule.span R {p})<VAR>φ : ℕ → R<VAR>hx : x ^ (Polynomial.map (algebraMap R S) f).natDegree = -∑ i : Fin (Polynomial.map (algebraMap R S) f).natDegree, (algebraMap R S) p * ((algebraMap R S) (φ ↑i) * x ^ ↑i)<VAR>hφ : ∀ n < f.natDegree, f.coeff n = p * φ n<GOAL>∃ y ∈ adjoin R {x}, (algebraMap R S) p * y = (algebraMap R S) p * (-1 * ∑ i : Fin (Polynomial.map (algebraMap R S) f).natDegree, (algebraMap R S) (φ ↑i) * x ^ ↑i)
<VAR>R : Type u<VAR>inst✝² : CommRing R<VAR>𝓟 : Ideal R<VAR>f : R[X]<VAR>hf✝ : f.IsWeaklyEisensteinAt 𝓟<VAR>S : Type v<VAR>inst✝¹ : CommRing S<VAR>inst✝ : Algebra R S<VAR>p : R<VAR>x : S<VAR>hmo : f.Monic<VAR>hf : f.IsWeaklyEisensteinAt (Submodule.span R {p})<VAR>φ : ℕ → R<VAR>hx : x ^ (Polynomial.map (algebraMap R S) f).natDegree = -∑ i : Fin (Polynomial.map (algebraMap R S) f).natDegree, (algebraMap R S) p * ((algebraMap R S) (φ ↑i) * x ^ ↑i)<VAR>hφ : ∀ n < f.natDegree, f.coeff n = p * φ n<GOAL>-1 * ∑ i : Fin (Polynomial.map (algebraMap R S) f).natDegree, (algebraMap R S) (φ ↑i) * x ^ ↑i ∈ adjoin R {x}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<GOAL>Tendsto (fun n => (↑n)⁻¹) atTop (𝓝 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<GOAL>Tendsto (fun a => ↑(↑a)⁻¹) atTop (𝓝 ↑0)
<VAR>H : Type u_1<VAR>M : Type u_2<VAR>H' : Type u_3<VAR>M' : Type u_4<VAR>X : Type u_5<VAR>inst✝⁶ : TopologicalSpace H<VAR>inst✝⁵ : TopologicalSpace M<VAR>inst✝⁴ : ChartedSpace H M<VAR>inst✝³ : TopologicalSpace H'<VAR>inst✝² : TopologicalSpace M'<VAR>inst✝¹ : ChartedSpace H' M'<VAR>inst✝ : TopologicalSpace X<VAR>G : StructureGroupoid H<VAR>G' : StructureGroupoid H'<VAR>e e' : PartialHomeomorph M H<VAR>f✝ f' : PartialHomeomorph M' H'<VAR>P : (H → H') → Set H → H → Prop<VAR>g g' : M → M'<VAR>s t : Set M<VAR>x✝ : M<VAR>Q : (H → H) → Set H → H → Prop<VAR>hG✝ hG : G.LocalInvariantProp G' P<VAR>U : Opens M<VAR>f : M → M'<VAR>x : ↥U<GOAL>LiftPropAt P f ↑x ↔ LiftPropAt P (f ∘ Subtype.val) x
<VAR>H : Type u_1<VAR>M : Type u_2<VAR>H' : Type u_3<VAR>M' : Type u_4<VAR>X : Type u_5<VAR>inst✝⁶ : TopologicalSpace H<VAR>inst✝⁵ : TopologicalSpace M<VAR>inst✝⁴ : ChartedSpace H M<VAR>inst✝³ : TopologicalSpace H'<VAR>inst✝² : TopologicalSpace M'<VAR>inst✝¹ : ChartedSpace H' M'<VAR>inst✝ : TopologicalSpace X<VAR>G : StructureGroupoid H<VAR>G' : StructureGroupoid H'<VAR>e e' : PartialHomeomorph M H<VAR>f✝ f' : PartialHomeomorph M' H'<VAR>P : (H → H') → Set H → H → Prop<VAR>g g' : M → M'<VAR>s t : Set M<VAR>x✝ : M<VAR>Q : (H → H) → Set H → H → Prop<VAR>hG✝ hG : G.LocalInvariantProp G' P<VAR>U : Opens M<VAR>f : M → M'<VAR>x : ↥U<GOAL>ContinuousWithinAt f univ ↑x ∧ P (↑(chartAt H' (f ↑x)) ∘ f ∘ ↑(chartAt H ↑x).symm) (↑(chartAt H ↑x).symm ⁻¹' univ) (↑(chartAt H ↑x) ↑x) ↔ ContinuousWithinAt (f ∘ Subtype.val) univ x ∧ P (↑(chartAt H' ((f ∘ Subtype.val) x)) ∘ (f ∘ Subtype.val) ∘ ↑(chartAt H x).symm) (↑(chartAt H x).symm ⁻¹' univ) (↑(chartAt H x) x)
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>γ' : Type u_6<VAR>δ : Type u_7<VAR>δ' : Type u_8<VAR>ε : Type u_9<VAR>ε' : Type u_10<VAR>ζ : Type u_11<VAR>ζ' : Type u_12<VAR>ν : Type u_13<VAR>f✝ f' : α → β → γ<VAR>g g' : α → β → γ → δ<VAR>s s' : Set α<VAR>t t' : Set β<VAR>u u' : Set γ<VAR>v : Set δ<VAR>a a' : α<VAR>b b' : β<VAR>c c' : γ<VAR>d d' : δ<VAR>hs : s.Subsingleton<VAR>ht : t.Subsingleton<VAR>f : α → β → γ<GOAL>(Set.image2 f s t).Subsingleton
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>γ' : Type u_6<VAR>δ : Type u_7<VAR>δ' : Type u_8<VAR>ε : Type u_9<VAR>ε' : Type u_10<VAR>ζ : Type u_11<VAR>ζ' : Type u_12<VAR>ν : Type u_13<VAR>f✝ f' : α → β → γ<VAR>g g' : α → β → γ → δ<VAR>s s' : Set α<VAR>t t' : Set β<VAR>u u' : Set γ<VAR>v : Set δ<VAR>a a' : α<VAR>b b' : β<VAR>c c' : γ<VAR>d d' : δ<VAR>hs : s.Subsingleton<VAR>ht : t.Subsingleton<VAR>f : α → β → γ<GOAL>((fun x => f x.1 x.2) '' s ×ˢ t).Subsingleton
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>D : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>G : Type u_6<VAR>V : Type u_7<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>k n : ℕ<VAR>f : 𝓢(E, F)<VAR>x : E<GOAL>‖x‖ ^ k * ‖iteratedFDeriv ℝ n (-⇑f) x‖ = ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖
<VAR>ι : Type u_1<VAR>α✝ : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝² : TopologicalSpace α✝<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : TopologicalSpace γ<VAR>α : Type u_5<VAR>U : Opens α<VAR>this : TopologicalSpace α := ⊤<GOAL>U = ⊥ ∨ U = ⊤
<VAR>ι : Type u_1<VAR>α✝ : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝² : TopologicalSpace α✝<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : TopologicalSpace γ<VAR>α : Type u_5<VAR>U : Opens α<VAR>this : TopologicalSpace α := ⊤<GOAL>IsOpen ↑U
<VAR>R✝ : Type u_1<VAR>A✝ : Type u_2<VAR>B : Type u_3<VAR>M✝ : Type u_4<VAR>N : Type u_5<VAR>inst✝¹¹ : Semiring R✝<VAR>inst✝¹⁰ : AddCommMonoid M✝<VAR>inst✝⁹ : Module R✝ M✝<VAR>inst✝⁸ : AddCommMonoid N<VAR>inst✝⁷ : Module R✝ N<VAR>R : Type u_6<VAR>A : Type u_7<VAR>M : Type u_8<VAR>inst✝⁶ : CommSemiring R<VAR>inst✝⁵ : Semiring A<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>inst✝² : Module A M<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : IsScalarTower R A M<VAR>hM : Finite R M<GOAL>Finite A M
<VAR>R✝ : Type u_1<VAR>A✝ : Type u_2<VAR>B : Type u_3<VAR>M✝ : Type u_4<VAR>N : Type u_5<VAR>inst✝¹¹ : Semiring R✝<VAR>inst✝¹⁰ : AddCommMonoid M✝<VAR>inst✝⁹ : Module R✝ M✝<VAR>inst✝⁸ : AddCommMonoid N<VAR>inst✝⁷ : Module R✝ N<VAR>R : Type u_6<VAR>A : Type u_7<VAR>M : Type u_8<VAR>inst✝⁶ : CommSemiring R<VAR>inst✝⁵ : Semiring A<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>inst✝² : Module A M<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : IsScalarTower R A M<VAR>hM : ∃ S, S.Finite ∧ span R S = ⊤<GOAL>∃ S, S.Finite ∧ span A S = ⊤
<VAR>R✝ : Type u_1<VAR>A✝ : Type u_2<VAR>B : Type u_3<VAR>M✝ : Type u_4<VAR>N : Type u_5<VAR>inst✝¹¹ : Semiring R✝<VAR>inst✝¹⁰ : AddCommMonoid M✝<VAR>inst✝⁹ : Module R✝ M✝<VAR>inst✝⁸ : AddCommMonoid N<VAR>inst✝⁷ : Module R✝ N<VAR>R : Type u_6<VAR>A : Type u_7<VAR>M : Type u_8<VAR>inst✝⁶ : CommSemiring R<VAR>inst✝⁵ : Semiring A<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>inst✝² : Module A M<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : IsScalarTower R A M<VAR>S : Set M<VAR>hSfin : S.Finite<VAR>hSgen : span R S = ⊤<GOAL>∃ S, S.Finite ∧ span A S = ⊤
<VAR>R✝ : Type u_1<VAR>A✝ : Type u_2<VAR>B : Type u_3<VAR>M✝ : Type u_4<VAR>N : Type u_5<VAR>inst✝¹¹ : Semiring R✝<VAR>inst✝¹⁰ : AddCommMonoid M✝<VAR>inst✝⁹ : Module R✝ M✝<VAR>inst✝⁸ : AddCommMonoid N<VAR>inst✝⁷ : Module R✝ N<VAR>R : Type u_6<VAR>A : Type u_7<VAR>M : Type u_8<VAR>inst✝⁶ : CommSemiring R<VAR>inst✝⁵ : Semiring A<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>inst✝² : Module A M<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : IsScalarTower R A M<VAR>S : Set M<VAR>hSfin : S.Finite<VAR>hSgen : span R S = ⊤<GOAL>⊤ ≤ span A S
<VAR>R✝ : Type u_1<VAR>A✝ : Type u_2<VAR>B : Type u_3<VAR>M✝ : Type u_4<VAR>N : Type u_5<VAR>inst✝¹¹ : Semiring R✝<VAR>inst✝¹⁰ : AddCommMonoid M✝<VAR>inst✝⁹ : Module R✝ M✝<VAR>inst✝⁸ : AddCommMonoid N<VAR>inst✝⁷ : Module R✝ N<VAR>R : Type u_6<VAR>A : Type u_7<VAR>M : Type u_8<VAR>inst✝⁶ : CommSemiring R<VAR>inst✝⁵ : Semiring A<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>inst✝² : Module A M<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : IsScalarTower R A M<VAR>S : Set M<VAR>hSfin : S.Finite<VAR>hSgen : span R S = ⊤<VAR>this : span R S ≤ restrictScalars R (span A S)<GOAL>⊤ ≤ span A S
<VAR>S : Type u_1<VAR>T : Type u_2<VAR>R : Type u_3<VAR>inst✝ : CommRing R<VAR>r x y z : R<VAR>a b c : ℍ[R]<GOAL>a.re * b.imJ + -1 * a.imI * b.imK + a.imJ * b.re - -1 * a.imK * b.imI = a.re * b.imJ - a.imI * b.imK + a.imJ * b.re + a.imK * b.imI
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : DistribLattice α<VAR>x y z a b c : α<GOAL>a ⊓ b ⊔ c = (a ⊔ c) ⊓ (b ⊔ c)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>ι : Type u_4<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>μ ν ν₁ ν₂ : Measure α<VAR>s t : Set α<VAR>inst✝ : IsProbabilityMeasure μ<VAR>p : α → Prop<VAR>f : β → α<VAR>hf : Injective f<VAR>hf' : ∀ᵐ (a : α) ∂μ, a ∈ range f<VAR>hf'' : ∀ (s : Set β), MeasurableSet s → MeasurableSet (f '' s)<GOAL>(Measure.comap f μ) univ = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>ι : Type u_4<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>μ ν ν₁ ν₂ : Measure α<VAR>s t : Set α<VAR>inst✝ : IsProbabilityMeasure μ<VAR>p : α → Prop<VAR>f : β → α<VAR>hf : Injective f<VAR>hf' : ∀ᵐ (a : α) ∂μ, a ∈ range f<VAR>hf'' : ∀ (s : Set β), MeasurableSet s → MeasurableSet (f '' s)<GOAL>f '' univ ∈ ae μ
<VAR>m n : ℕ<VAR>hm : Odd m<VAR>hn : Odd n<VAR>x y : ℤ<GOAL>qrSign m n * x = y ↔ x = qrSign m n * y