ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝¹ : IsFiniteMeasure μ<VAR>inst✝ : IsFiniteMeasure ν<VAR>i : Set α<VAR>hi : MeasurableSet i<GOAL>↑(μ.toSignedMeasure - ν.toSignedMeasure) i = (μ i).toReal - (ν i).toReal
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>ι : Type u_2<VAR>s : Finset ι<VAR>v : ι → R<VAR>x : R<GOAL>eval x (nodal s v) = ∏ i ∈ s, (x - v i)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝ : UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>s s' : Set α<VAR>x : α<VAR>p : Filter ι<VAR>p' : Filter α<VAR>g : ι → α<VAR>l : Filter ι<VAR>h : TendstoUniformlyOn F f l s<VAR>u : ℕ → ι<VAR>hu : Tendsto u atTop l<GOAL>TendstoUniformlyOn (fun n => F (u n)) f atTop s
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝ : UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>s s' : Set α<VAR>x : α<VAR>p : Filter ι<VAR>p' : Filter α<VAR>g : ι → α<VAR>l : Filter ι<VAR>h : Tendsto (fun q => (f q.2, F q.1 q.2)) (l ×ˢ 𝓟 s) (𝓤 β)<VAR>u : ℕ → ι<VAR>hu : Tendsto u atTop l<GOAL>Tendsto (fun q => (f q.2, F (u q.1) q.2)) (atTop ×ˢ 𝓟 s) (𝓤 β)
<VAR>R : Type u_1<VAR>inst✝ : NonUnitalNonAssocRing R<VAR>I : TwoSidedIdeal R<VAR>x y : R<VAR>hx : x ∈ I<GOAL>x * y ∈ I
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>p p₀ p₁ p₂ : P<VAR>v₁ v₂ v₃ : V<GOAL>∠ (-v₁) (-v₂) (-v₃) = ∠ v₁ v₂ v₃
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : Type x<VAR>inst✝ : Ring α<VAR>a✝ b✝ a b : α<VAR>u : αˣ<GOAL>a + b /ₚ u = (a * ↑u + b) /ₚ u
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>F : Type u_6<VAR>inst✝⁴ : CommMonoid M<VAR>inst✝³ : CommMonoid N<VAR>inst✝² : DivisionCommMonoid G<VAR>k : ℕ<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<GOAL>primitiveRoots 0 R = ∅
<VAR>m n : ℕ<VAR>cop : m.Coprime n<VAR>hm : 1 < m<VAR>hn : 1 < n<GOAL>FrobeniusNumber (m * n - m - n) {m, n}
<VAR>m n : ℕ<VAR>cop : m.Coprime n<VAR>hm : 1 < m<VAR>hn : 1 < n<GOAL>IsGreatest {k | ¬∃ m_1 n_1, m_1 • m + n_1 • n = k} (m * n - m - n)
<VAR>m n : ℕ<VAR>cop : m.Coprime n<VAR>hm : 1 < m<VAR>hn : 1 < n<VAR>hmn : m + n ≤ m * n<GOAL>IsGreatest {k | ¬∃ m_1 n_1, m_1 • m + n_1 • n = k} (m * n - m - n)
<VAR>R : Type u<VAR>K : Type u'<VAR>M : Type v<VAR>V : Type v'<VAR>M₂ : Type w<VAR>V₂ : Type w'<VAR>M₃ : Type y<VAR>V₃ : Type y'<VAR>M₄ : Type z<VAR>ι : Type x<VAR>M₅ : Type u_1<VAR>M₆ : Type u_2<VAR>inst✝⁴ : Semiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : AddCommMonoid M₂<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R M₂<VAR>p : Submodule R M<VAR>q : Submodule R M₂<GOAL>map (snd R M M₂) (fst R M M₂) = ⊥
<VAR>R : Type u<VAR>K : Type u'<VAR>M : Type v<VAR>V : Type v'<VAR>M₂ : Type w<VAR>V₂ : Type w'<VAR>M₃ : Type y<VAR>V₃ : Type y'<VAR>M₄ : Type z<VAR>ι : Type x<VAR>M₅ : Type u_1<VAR>M₆ : Type u_2<VAR>inst✝⁴ : Semiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : AddCommMonoid M₂<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R M₂<VAR>p : Submodule R M<VAR>q : Submodule R M₂<GOAL>map (snd R M M₂) (fst R M M₂) ≤ ⊥
<VAR>R : Type u<VAR>K : Type u'<VAR>M : Type v<VAR>V : Type v'<VAR>M₂ : Type w<VAR>V₂ : Type w'<VAR>M₃ : Type y<VAR>V₃ : Type y'<VAR>M₄ : Type z<VAR>ι : Type x<VAR>M₅ : Type u_1<VAR>M₆ : Type u_2<VAR>inst✝⁴ : Semiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : AddCommMonoid M₂<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R M₂<VAR>p : Submodule R M<VAR>q : Submodule R M₂<VAR>x : M₂<GOAL>x ∈ map (snd R M M₂) (fst R M M₂) → x ∈ ⊥
<VAR>R : Type u_1<VAR>inst✝¹⁴ : Semiring R<VAR>M : Type u_2<VAR>inst✝¹³ : AddCommMonoid M<VAR>inst✝¹² : Module R M<VAR>N : Type u_3<VAR>inst✝¹¹ : AddCommMonoid N<VAR>inst✝¹⁰ : Module R N<VAR>P : Type u_4<VAR>inst✝⁹ : AddCommMonoid P<VAR>inst✝⁸ : Module R P<VAR>M' : Type u_5<VAR>inst✝⁷ : AddCommGroup M'<VAR>inst✝⁶ : Module R M'<VAR>N' : Type u_6<VAR>inst✝⁵ : AddCommGroup N'<VAR>inst✝⁴ : Module R N'<VAR>ι : Type u_7<VAR>ι' : Type u_8<VAR>ι'' : Type u_9<VAR>M₂ : Type u_10<VAR>inst✝³ : AddCommMonoid M₂<VAR>inst✝² : Module R M₂<VAR>M₃ : Type u_11<VAR>inst✝¹ : AddCommMonoid M₃<VAR>inst✝ : Module R M₃<VAR>f₁ f₂ : M [⋀^ι]→ₗ[R] N<VAR>g : M₂ →ₗ[R] M<VAR>x✝ : ι → M₂<GOAL>((f₁ + f₂).compLinearMap g) x✝ = (f₁.compLinearMap g + f₂.compLinearMap g) x✝
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>κ : ι → Sort w'<VAR>inst✝ : Frame α<VAR>s t : Set α<VAR>a b : α<VAR>f : (i : ι) → κ i → α<GOAL>Disjoint a (⨆ i, ⨆ j, f i j) ↔ ∀ (i : ι) (j : κ i), Disjoint a (f i j)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>κ : ι → Sort u_1<VAR>a a₁ a₂ : α<VAR>b b₁ b₂ : β<VAR>inst✝¹ : Preorder α<VAR>inst✝ : Preorder β<VAR>l : α → β<VAR>u : β → α<VAR>gc : GaloisConnection l u<VAR>s : Set α<VAR>x✝ : BddAbove (l '' s)<VAR>x : β<VAR>hx : x ∈ upperBounds (l '' s)<GOAL>u x ∈ upperBounds s
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : CompleteSpace E<VAR>p : ℝ≥0∞<VAR>inst✝ : SigmaFinite μ<VAR>f g : α → ℝ≥0∞<VAR>hf : AEMeasurable f μ<VAR>hg : AEMeasurable g μ<VAR>h : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α) in s, g x ∂μ<GOAL>f =ᶠ[ae μ] g
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : CompleteSpace E<VAR>p : ℝ≥0∞<VAR>inst✝ : SigmaFinite μ<VAR>f g : α → ℝ≥0∞<VAR>hf : AEMeasurable f μ<VAR>hg : AEMeasurable g μ<VAR>h : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α) in s, g x ∂μ<VAR>A : f ≤ᶠ[ae μ] g<GOAL>f =ᶠ[ae μ] g
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : CompleteSpace E<VAR>p : ℝ≥0∞<VAR>inst✝ : SigmaFinite μ<VAR>f g : α → ℝ≥0∞<VAR>hf : AEMeasurable f μ<VAR>hg : AEMeasurable g μ<VAR>h : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α) in s, g x ∂μ<VAR>A : f ≤ᶠ[ae μ] g<VAR>B : g ≤ᶠ[ae μ] f<GOAL>f =ᶠ[ae μ] g
<VAR>R : Type u_1<VAR>l : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>α : Type u_5<VAR>β : Type u_6<VAR>ι : Type u_7<VAR>inst✝⁵ : Fintype l<VAR>inst✝⁴ : Fintype m<VAR>inst✝³ : Fintype n<VAR>inst✝² : Unique ι<VAR>inst✝¹ : SeminormedAddCommGroup α<VAR>inst✝ : SeminormedAddCommGroup β<VAR>A : Matrix m n α<GOAL>↑((∑ i : m, ∑ j : n, ‖A i j‖₊ ^ 2) ^ (1 / 2)) = (∑ i : m, ∑ j : n, ‖A i j‖ ^ 2) ^ (1 / 2)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝¹ : Group α<VAR>inst✝ : MulAction α β<VAR>s✝ t A B : Set β<VAR>a : α<VAR>x : β<VAR>s : Set β<GOAL>⋃ g, g • s = {a | ∃ g, g • a ∈ s}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : SeminormedAddCommGroup α<VAR>r✝ C✝ : ℝ<VAR>f : ℕ → α<VAR>C : ℝ<VAR>u : ℕ → α<VAR>N : ℕ<VAR>r : ℝ<VAR>hr₀ : 0 < r<VAR>hr₁ : r < 1<VAR>h : ∀ n ≥ N, ‖u n‖ ≤ C * r ^ n<VAR>v : ℕ → α := fun n => if n < N then 0 else u n<GOAL>CauchySeq fun n => ∑ k ∈ Finset.range (n + 1), u k
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : SeminormedAddCommGroup α<VAR>r✝ C✝ : ℝ<VAR>f : ℕ → α<VAR>C : ℝ<VAR>u : ℕ → α<VAR>N : ℕ<VAR>r : ℝ<VAR>hr₀ : 0 < r<VAR>hr₁ : r < 1<VAR>h : ∀ n ≥ N, ‖u n‖ ≤ C * r ^ n<VAR>v : ℕ → α := fun n => if n < N then 0 else u n<VAR>hC : 0 ≤ C<GOAL>CauchySeq fun n => ∑ k ∈ Finset.range (n + 1), u k
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : SeminormedAddCommGroup α<VAR>r✝ C✝ : ℝ<VAR>f : ℕ → α<VAR>C : ℝ<VAR>u : ℕ → α<VAR>N : ℕ<VAR>r : ℝ<VAR>hr₀ : 0 < r<VAR>hr₁ : r < 1<VAR>h : ∀ n ≥ N, ‖u n‖ ≤ C * r ^ n<VAR>v : ℕ → α := fun n => if n < N then 0 else u n<VAR>hC : 0 ≤ C<VAR>this : ∀ n ≥ N, u n = v n<GOAL>CauchySeq fun n => ∑ k ∈ Finset.range (n + 1), u k
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : SeminormedAddCommGroup α<VAR>r✝ C✝ : ℝ<VAR>f : ℕ → α<VAR>C : ℝ<VAR>u : ℕ → α<VAR>N : ℕ<VAR>r : ℝ<VAR>hr₀ : 0 < r<VAR>hr₁ : r < 1<VAR>h : ∀ n ≥ N, ‖u n‖ ≤ C * r ^ n<VAR>v : ℕ → α := fun n => if n < N then 0 else u n<VAR>hC : 0 ≤ C<VAR>this : ∀ n ≥ N, u n = v n<GOAL>ℝ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : SeminormedAddCommGroup α<VAR>r✝ C✝ : ℝ<VAR>f : ℕ → α<VAR>C : ℝ<VAR>u : ℕ → α<VAR>N : ℕ<VAR>r : ℝ<VAR>hr₀ : 0 < r<VAR>hr₁ : r < 1<VAR>h : ∀ n ≥ N, ‖u n‖ ≤ C * r ^ n<VAR>v : ℕ → α := fun n => if n < N then 0 else u n<VAR>hC : 0 ≤ C<VAR>this : ∀ n ≥ N, u n = v n<GOAL>∀ (n : ℕ), ‖v n‖ ≤ ?m.158269 * r ^ n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>inst✝⁵ : MetricSpace β<VAR>μ : Measure α<VAR>inst✝⁴ : SemilatticeSup ι<VAR>inst✝³ : Nonempty ι<VAR>inst✝² : Countable ι<VAR>γ : Type u_4<VAR>inst✝¹ : TopologicalSpace γ<VAR>f : ι → α → β<VAR>g : α → β<VAR>s : Set α<VAR>inst✝ : IsFiniteMeasure μ<VAR>hf : ∀ (n : ι), StronglyMeasurable (f n)<VAR>hg : StronglyMeasurable g<VAR>hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))<VAR>ε : ℝ<VAR>hε : 0 < ε<GOAL>∃ t, MeasurableSet t ∧ μ t ≤ ENNReal.ofReal ε ∧ TendstoUniformlyOn f g atTop tᶜ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>inst✝⁵ : MetricSpace β<VAR>μ : Measure α<VAR>inst✝⁴ : SemilatticeSup ι<VAR>inst✝³ : Nonempty ι<VAR>inst✝² : Countable ι<VAR>γ : Type u_4<VAR>inst✝¹ : TopologicalSpace γ<VAR>f : ι → α → β<VAR>g : α → β<VAR>s : Set α<VAR>inst✝ : IsFiniteMeasure μ<VAR>hf : ∀ (n : ι), StronglyMeasurable (f n)<VAR>hg : StronglyMeasurable g<VAR>hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>t : Set α<VAR>left✝ : t ⊆ univ<VAR>ht : MeasurableSet t<VAR>htendsto : μ t ≤ ENNReal.ofReal ε ∧ TendstoUniformlyOn f g atTop (univ \ t)<GOAL>∃ t, MeasurableSet t ∧ μ t ≤ ENNReal.ofReal ε ∧ TendstoUniformlyOn f g atTop tᶜ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>inst✝⁵ : MetricSpace β<VAR>μ : Measure α<VAR>inst✝⁴ : SemilatticeSup ι<VAR>inst✝³ : Nonempty ι<VAR>inst✝² : Countable ι<VAR>γ : Type u_4<VAR>inst✝¹ : TopologicalSpace γ<VAR>f : ι → α → β<VAR>g : α → β<VAR>s : Set α<VAR>inst✝ : IsFiniteMeasure μ<VAR>hf : ∀ (n : ι), StronglyMeasurable (f n)<VAR>hg : StronglyMeasurable g<VAR>hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>t : Set α<VAR>left✝ : t ⊆ univ<VAR>ht : MeasurableSet t<VAR>htendsto : μ t ≤ ENNReal.ofReal ε ∧ TendstoUniformlyOn f g atTop (univ \ t)<GOAL>μ t ≤ ENNReal.ofReal ε ∧ TendstoUniformlyOn f g atTop tᶜ
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<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✝³ : Module.Free R M<VAR>inst✝² : Module.Finite R M<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : IsPrincipalIdealRing R<VAR>N : LieSubmodule R L M<VAR>I : LieIdeal R L<VAR>h : I ≤ N.idealizer<VAR>x✝ y✝ : L<VAR>hy✝ : y✝ ∈ I<VAR>x : L<VAR>hx : x ∈ ↑I<VAR>y : L<VAR>hy : y ∈ ↑I<GOAL>((traceForm R ↥↑I ↥↑N) ⟨x, hx⟩) ⟨y, hy⟩ = (trace R M) (φ x ∘ₗ φ y)
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<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✝³ : Module.Free R M<VAR>inst✝² : Module.Finite R M<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : IsPrincipalIdealRing R<VAR>N : LieSubmodule R L M<VAR>I : LieIdeal R L<VAR>h : I ≤ N.idealizer<VAR>x✝ y✝ : L<VAR>hy✝ : y✝ ∈ I<VAR>x : L<VAR>hx : x ∈ ↑I<VAR>y : L<VAR>hy : y ∈ ↑I<GOAL>((traceForm R ↥↑I ↥↑N) ⟨x, hx⟩) ⟨y, hy⟩ = (trace R ↥↑N) ((φ x ∘ₗ φ y).restrict ⋯)
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>S : Type u_3<VAR>R : Type u_4<VAR>inst✝⁸ : DecidableEq ι<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : SetLike σ R<VAR>inst✝⁵ : AddSubmonoidClass σ R<VAR>A : ι → σ<VAR>inst✝⁴ : CanonicallyOrderedAddCommMonoid ι<VAR>inst✝³ : SetLike.GradedMonoid A<VAR>inst✝² : Sub ι<VAR>inst✝¹ : OrderedSub ι<VAR>inst✝ : ContravariantClass ι ι (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>i : ι<VAR>r : ↥(A i)<VAR>r' : ⨁ (i : ι), ↥(A i)<VAR>n : ι<VAR>h : i ≤ n<VAR>x : ι<GOAL>i + x = n ↔ x = n - i
<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>F : Type u_7<VAR>G : Type u_8<VAR>inst✝¹ : SeminormedCommGroup E<VAR>inst✝ : SeminormedCommGroup F<VAR>a a₁ a₂ b✝ b₁ b₂ : E<VAR>r r₁ r₂ : ℝ<VAR>s : Subgroup E<VAR>hg : a ∈ closure ↑s<VAR>b : ℕ → ℝ<VAR>b_pos : ∀ (n : ℕ), 0 < b n<GOAL>∃ v, Tendsto (fun n => ∏ i ∈ range (n + 1), v i) atTop (𝓝 a) ∧ (∀ (n : ℕ), v n ∈ s) ∧ ‖v 0 / a‖ < b 0 ∧ ∀ (n : ℕ), 0 < n → ‖v n‖ < b n
<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>F : Type u_7<VAR>G : Type u_8<VAR>inst✝¹ : SeminormedCommGroup E<VAR>inst✝ : SeminormedCommGroup F<VAR>a a₁ a₂ b✝ b₁ b₂ : E<VAR>r r₁ r₂ : ℝ<VAR>s : Subgroup E<VAR>hg : a ∈ closure ↑s<VAR>b : ℕ → ℝ<VAR>b_pos : ∀ (n : ℕ), 0 < b n<VAR>u : ℕ → E<VAR>u_in : ∀ (n : ℕ), u n ∈ s<VAR>lim_u : Tendsto u atTop (𝓝 a)<GOAL>∃ v, Tendsto (fun n => ∏ i ∈ range (n + 1), v i) atTop (𝓝 a) ∧ (∀ (n : ℕ), v n ∈ s) ∧ ‖v 0 / a‖ < b 0 ∧ ∀ (n : ℕ), 0 < n → ‖v n‖ < b n
<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>F : Type u_7<VAR>G : Type u_8<VAR>inst✝¹ : SeminormedCommGroup E<VAR>inst✝ : SeminormedCommGroup F<VAR>a a₁ a₂ b✝ b₁ b₂ : E<VAR>r r₁ r₂ : ℝ<VAR>s : Subgroup E<VAR>hg : a ∈ closure ↑s<VAR>b : ℕ → ℝ<VAR>b_pos : ∀ (n : ℕ), 0 < b n<VAR>u : ℕ → E<VAR>u_in : ∀ (n : ℕ), u n ∈ s<VAR>lim_u : Tendsto u atTop (𝓝 a)<VAR>n₀ : ℕ<VAR>hn₀ : ∀ n ≥ n₀, ‖u n / a‖ < b 0<GOAL>∃ v, Tendsto (fun n => ∏ i ∈ range (n + 1), v i) atTop (𝓝 a) ∧ (∀ (n : ℕ), v n ∈ s) ∧ ‖v 0 / a‖ < b 0 ∧ ∀ (n : ℕ), 0 < n → ‖v n‖ < b n
<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>F : Type u_7<VAR>G : Type u_8<VAR>inst✝¹ : SeminormedCommGroup E<VAR>inst✝ : SeminormedCommGroup F<VAR>a a₁ a₂ b✝ b₁ b₂ : E<VAR>r r₁ r₂ : ℝ<VAR>s : Subgroup E<VAR>hg : a ∈ closure ↑s<VAR>b : ℕ → ℝ<VAR>b_pos : ∀ (n : ℕ), 0 < b n<VAR>u : ℕ → E<VAR>u_in : ∀ (n : ℕ), u n ∈ s<VAR>lim_u : Tendsto u atTop (𝓝 a)<VAR>n₀ : ℕ<VAR>hn₀ : ∀ n ≥ n₀, ‖u n / a‖ < b 0<VAR>z : ℕ → E := fun n => u (n + n₀)<GOAL>∃ v, Tendsto (fun n => ∏ i ∈ range (n + 1), v i) atTop (𝓝 a) ∧ (∀ (n : ℕ), v n ∈ s) ∧ ‖v 0 / a‖ < b 0 ∧ ∀ (n : ℕ), 0 < n → ‖v n‖ < b n
<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>F : Type u_7<VAR>G : Type u_8<VAR>inst✝¹ : SeminormedCommGroup E<VAR>inst✝ : SeminormedCommGroup F<VAR>a a₁ a₂ b✝ b₁ b₂ : E<VAR>r r₁ r₂ : ℝ<VAR>s : Subgroup E<VAR>hg : a ∈ closure ↑s<VAR>b : ℕ → ℝ<VAR>b_pos : ∀ (n : ℕ), 0 < b n<VAR>u : ℕ → E<VAR>u_in : ∀ (n : ℕ), u n ∈ s<VAR>lim_u : Tendsto u atTop (𝓝 a)<VAR>n₀ : ℕ<VAR>hn₀ : ∀ n ≥ n₀, ‖u n / a‖ < b 0<VAR>z : ℕ → E := fun n => u (n + n₀)<VAR>lim_z : Tendsto z atTop (𝓝 a)<GOAL>∃ v, Tendsto (fun n => ∏ i ∈ range (n + 1), v i) atTop (𝓝 a) ∧ (∀ (n : ℕ), v n ∈ s) ∧ ‖v 0 / a‖ < b 0 ∧ ∀ (n : ℕ), 0 < n → ‖v n‖ < b n
<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>F : Type u_7<VAR>G : Type u_8<VAR>inst✝¹ : SeminormedCommGroup E<VAR>inst✝ : SeminormedCommGroup F<VAR>a a₁ a₂ b✝ b₁ b₂ : E<VAR>r r₁ r₂ : ℝ<VAR>s : Subgroup E<VAR>hg : a ∈ closure ↑s<VAR>b : ℕ → ℝ<VAR>b_pos : ∀ (n : ℕ), 0 < b n<VAR>u : ℕ → E<VAR>u_in : ∀ (n : ℕ), u n ∈ s<VAR>lim_u : Tendsto u atTop (𝓝 a)<VAR>n₀ : ℕ<VAR>hn₀ : ∀ n ≥ n₀, ‖u n / a‖ < b 0<VAR>z : ℕ → E := fun n => u (n + n₀)<VAR>lim_z : Tendsto z atTop (𝓝 a)<VAR>mem_𝓤 : ∀ (n : ℕ), {p | ‖p.1 / p.2‖ < b (n + 1)} ∈ 𝓤 E<GOAL>∃ v, Tendsto (fun n => ∏ i ∈ range (n + 1), v i) atTop (𝓝 a) ∧ (∀ (n : ℕ), v n ∈ s) ∧ ‖v 0 / a‖ < b 0 ∧ ∀ (n : ℕ), 0 < n → ‖v n‖ < b n
<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>F : Type u_7<VAR>G : Type u_8<VAR>inst✝¹ : SeminormedCommGroup E<VAR>inst✝ : SeminormedCommGroup F<VAR>a a₁ a₂ b✝ b₁ b₂ : E<VAR>r r₁ r₂ : ℝ<VAR>s : Subgroup E<VAR>hg : a ∈ closure ↑s<VAR>b : ℕ → ℝ<VAR>b_pos : ∀ (n : ℕ), 0 < b n<VAR>u : ℕ → E<VAR>u_in : ∀ (n : ℕ), u n ∈ s<VAR>lim_u : Tendsto u atTop (𝓝 a)<VAR>n₀ : ℕ<VAR>hn₀ : ∀ n ≥ n₀, ‖u n / a‖ < b 0<VAR>z : ℕ → E := fun n => u (n + n₀)<VAR>lim_z : Tendsto z atTop (𝓝 a)<VAR>mem_𝓤 : ∀ (n : ℕ), {p | ‖p.1 / p.2‖ < b (n + 1)} ∈ 𝓤 E<VAR>φ : ℕ → ℕ<VAR>φ_extr : StrictMono φ<VAR>hφ : ∀ (n : ℕ), ‖z (φ (n + 1)) / z (φ n)‖ < b (n + 1)<GOAL>∃ v, Tendsto (fun n => ∏ i ∈ range (n + 1), v i) atTop (𝓝 a) ∧ (∀ (n : ℕ), v n ∈ s) ∧ ‖v 0 / a‖ < b 0 ∧ ∀ (n : ℕ), 0 < n → ‖v n‖ < b n
<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>F : Type u_7<VAR>G : Type u_8<VAR>inst✝¹ : SeminormedCommGroup E<VAR>inst✝ : SeminormedCommGroup F<VAR>a a₁ a₂ b✝ b₁ b₂ : E<VAR>r r₁ r₂ : ℝ<VAR>s : Subgroup E<VAR>hg : a ∈ closure ↑s<VAR>b : ℕ → ℝ<VAR>b_pos : ∀ (n : ℕ), 0 < b n<VAR>u : ℕ → E<VAR>u_in : ∀ (n : ℕ), u n ∈ s<VAR>lim_u : Tendsto u atTop (𝓝 a)<VAR>n₀ : ℕ<VAR>hn₀ : ∀ n ≥ n₀, ‖u n / a‖ < b 0<VAR>z : ℕ → E := fun n => u (n + n₀)<VAR>lim_z : Tendsto z atTop (𝓝 a)<VAR>mem_𝓤 : ∀ (n : ℕ), {p | ‖p.1 / p.2‖ < b (n + 1)} ∈ 𝓤 E<VAR>φ : ℕ → ℕ<VAR>φ_extr : StrictMono φ<VAR>hφ : ∀ (n : ℕ), ‖z (φ (n + 1)) / z (φ n)‖ < b (n + 1)<VAR>w : ℕ → E := z ∘ φ<GOAL>∃ v, Tendsto (fun n => ∏ i ∈ range (n + 1), v i) atTop (𝓝 a) ∧ (∀ (n : ℕ), v n ∈ s) ∧ ‖v 0 / a‖ < b 0 ∧ ∀ (n : ℕ), 0 < n → ‖v n‖ < b n
<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>F : Type u_7<VAR>G : Type u_8<VAR>inst✝¹ : SeminormedCommGroup E<VAR>inst✝ : SeminormedCommGroup F<VAR>a a₁ a₂ b✝ b₁ b₂ : E<VAR>r r₁ r₂ : ℝ<VAR>s : Subgroup E<VAR>hg : a ∈ closure ↑s<VAR>b : ℕ → ℝ<VAR>b_pos : ∀ (n : ℕ), 0 < b n<VAR>u : ℕ → E<VAR>u_in : ∀ (n : ℕ), u n ∈ s<VAR>lim_u : Tendsto u atTop (𝓝 a)<VAR>n₀ : ℕ<VAR>hn₀ : ∀ n ≥ n₀, ‖u n / a‖ < b 0<VAR>z : ℕ → E := fun n => u (n + n₀)<VAR>lim_z : Tendsto z atTop (𝓝 a)<VAR>mem_𝓤 : ∀ (n : ℕ), {p | ‖p.1 / p.2‖ < b (n + 1)} ∈ 𝓤 E<VAR>φ : ℕ → ℕ<VAR>φ_extr : StrictMono φ<VAR>hφ : ∀ (n : ℕ), ‖z (φ (n + 1)) / z (φ n)‖ < b (n + 1)<VAR>w : ℕ → E := z ∘ φ<VAR>hw : Tendsto w atTop (𝓝 a)<GOAL>∃ v, Tendsto (fun n => ∏ i ∈ range (n + 1), v i) atTop (𝓝 a) ∧ (∀ (n : ℕ), v n ∈ s) ∧ ‖v 0 / a‖ < b 0 ∧ ∀ (n : ℕ), 0 < n → ‖v n‖ < b n
<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>F : Type u_7<VAR>G : Type u_8<VAR>inst✝¹ : SeminormedCommGroup E<VAR>inst✝ : SeminormedCommGroup F<VAR>a a₁ a₂ b✝ b₁ b₂ : E<VAR>r r₁ r₂ : ℝ<VAR>s : Subgroup E<VAR>hg : a ∈ closure ↑s<VAR>b : ℕ → ℝ<VAR>b_pos : ∀ (n : ℕ), 0 < b n<VAR>u : ℕ → E<VAR>u_in : ∀ (n : ℕ), u n ∈ s<VAR>lim_u : Tendsto u atTop (𝓝 a)<VAR>n₀ : ℕ<VAR>hn₀ : ∀ n ≥ n₀, ‖u n / a‖ < b 0<VAR>z : ℕ → E := fun n => u (n + n₀)<VAR>lim_z : Tendsto z atTop (𝓝 a)<VAR>mem_𝓤 : ∀ (n : ℕ), {p | ‖p.1 / p.2‖ < b (n + 1)} ∈ 𝓤 E<VAR>φ : ℕ → ℕ<VAR>φ_extr : StrictMono φ<VAR>hφ : ∀ (n : ℕ), ‖z (φ (n + 1)) / z (φ n)‖ < b (n + 1)<VAR>w : ℕ → E := z ∘ φ<VAR>hw : Tendsto w atTop (𝓝 a)<VAR>v : ℕ → E := fun i => if i = 0 then w 0 else w i / w (i - 1)<GOAL>∃ v, Tendsto (fun n => ∏ i ∈ range (n + 1), v i) atTop (𝓝 a) ∧ (∀ (n : ℕ), v n ∈ s) ∧ ‖v 0 / a‖ < b 0 ∧ ∀ (n : ℕ), 0 < n → ‖v n‖ < b n
<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>F : Type u_7<VAR>G : Type u_8<VAR>inst✝¹ : SeminormedCommGroup E<VAR>inst✝ : SeminormedCommGroup F<VAR>a a₁ a₂ b✝ b₁ b₂ : E<VAR>r r₁ r₂ : ℝ<VAR>s : Subgroup E<VAR>hg : a ∈ closure ↑s<VAR>b : ℕ → ℝ<VAR>b_pos : ∀ (n : ℕ), 0 < b n<VAR>u : ℕ → E<VAR>u_in : ∀ (n : ℕ), u n ∈ s<VAR>lim_u : Tendsto u atTop (𝓝 a)<VAR>n₀ : ℕ<VAR>hn₀ : ∀ n ≥ n₀, ‖u n / a‖ < b 0<VAR>z : ℕ → E := fun n => u (n + n₀)<VAR>lim_z : Tendsto z atTop (𝓝 a)<VAR>mem_𝓤 : ∀ (n : ℕ), {p | ‖p.1 / p.2‖ < b (n + 1)} ∈ 𝓤 E<VAR>φ : ℕ → ℕ<VAR>φ_extr : StrictMono φ<VAR>hφ : ∀ (n : ℕ), ‖z (φ (n + 1)) / z (φ n)‖ < b (n + 1)<VAR>w : ℕ → E := z ∘ φ<VAR>hw : Tendsto w atTop (𝓝 a)<VAR>v : ℕ → E := fun i => if i = 0 then w 0 else w i / w (i - 1)<GOAL>∀ (n : ℕ), v n ∈ s
<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>F : Type u_7<VAR>G : Type u_8<VAR>inst✝¹ : SeminormedCommGroup E<VAR>inst✝ : SeminormedCommGroup F<VAR>a a₁ a₂ b✝ b₁ b₂ : E<VAR>r r₁ r₂ : ℝ<VAR>s : Subgroup E<VAR>hg : a ∈ closure ↑s<VAR>b : ℕ → ℝ<VAR>b_pos : ∀ (n : ℕ), 0 < b n<VAR>u : ℕ → E<VAR>u_in : ∀ (n : ℕ), u n ∈ s<VAR>lim_u : Tendsto u atTop (𝓝 a)<VAR>n₀ : ℕ<VAR>hn₀ : ∀ n ≥ n₀, ‖u n / a‖ < b 0<VAR>z : ℕ → E := fun n => u (n + n₀)<VAR>lim_z : Tendsto z atTop (𝓝 a)<VAR>mem_𝓤 : ∀ (n : ℕ), {p | ‖p.1 / p.2‖ < b (n + 1)} ∈ 𝓤 E<VAR>φ : ℕ → ℕ<VAR>φ_extr : StrictMono φ<VAR>hφ : ∀ (n : ℕ), ‖z (φ (n + 1)) / z (φ n)‖ < b (n + 1)<VAR>w : ℕ → E := z ∘ φ<VAR>hw : Tendsto w atTop (𝓝 a)<VAR>v : ℕ → E := fun i => if i = 0 then w 0 else w i / w (i - 1)<GOAL>∀ (n : ℕ), 0 < n → ‖v n‖ < b n
<VAR>s : ℂ<VAR>hs : 0 < s.re<GOAL>(s + 1).GammaIntegral = s * s.GammaIntegral
<VAR>s : ℂ<VAR>hs : 0 < s.re<GOAL>Tendsto (s + 1).partialGamma atTop (𝓝 (s * s.GammaIntegral))
<VAR>s : ℂ<VAR>hs : 0 < s.re<VAR>this : (fun X => s * s.partialGamma X - ↑X ^ s * ↑(rexp (-X))) =ᶠ[atTop] (s + 1).partialGamma<GOAL>Tendsto (s + 1).partialGamma atTop (𝓝 (s * s.GammaIntegral))
<VAR>s : ℂ<VAR>hs : 0 < s.re<VAR>this : (fun X => s * s.partialGamma X - ↑X ^ s * ↑(rexp (-X))) =ᶠ[atTop] (s + 1).partialGamma<GOAL>Tendsto (fun X => s * s.partialGamma X - ↑X ^ s * ↑(rexp (-X))) atTop (𝓝 (s * s.GammaIntegral))
<VAR>s : ℂ<VAR>hs : 0 < s.re<VAR>this : (fun X => s * s.partialGamma X - ↑X ^ s * ↑(rexp (-X))) =ᶠ[atTop] (s + 1).partialGamma<GOAL>Tendsto (fun X => -↑X ^ s * ↑(rexp (-X))) atTop (𝓝 0)
<VAR>s : ℂ<VAR>hs : 0 < s.re<VAR>this : (fun X => s * s.partialGamma X - ↑X ^ s * ↑(rexp (-X))) =ᶠ[atTop] (s + 1).partialGamma<GOAL>Tendsto (fun x => ‖-↑x ^ s * ↑(rexp (-x))‖) atTop (𝓝 0)
<VAR>s : ℂ<VAR>hs : 0 < s.re<VAR>this✝ : (fun X => s * s.partialGamma X - ↑X ^ s * ↑(rexp (-X))) =ᶠ[atTop] (s + 1).partialGamma<VAR>this : (fun e => ‖-↑e ^ s * ↑(rexp (-e))‖) =ᶠ[atTop] fun e => e ^ s.re * rexp (-1 * e)<GOAL>Tendsto (fun x => ‖-↑x ^ s * ↑(rexp (-x))‖) atTop (𝓝 0)
<VAR>a n✝ n k : ℕ<VAR>ih : (2 ^ k * n).bitIndices = map (fun x => x + k) n.bitIndices<GOAL>(2 ^ (k + 1) * n).bitIndices = map (fun x => x + (k + 1)) n.bitIndices
<VAR>a n✝ n k : ℕ<VAR>ih : (2 ^ k * n).bitIndices = map (fun x => x + k) n.bitIndices<GOAL>map (fun x => x + (k + 1)) n.bitIndices = map (fun x => x + (1 + k)) n.bitIndices
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>R : Type u_3<VAR>S : Type u_4<VAR>A : Type u_5<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Ring A<VAR>inst✝³ : Algebra R S<VAR>inst✝² : Algebra S A<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : IsScalarTower R S A<VAR>hinj : Function.Injective ⇑(algebraMap R S)<VAR>x : A<VAR>A_alg : IsAlgebraic R x<VAR>p : R[X]<VAR>hp₁ : p ≠ 0<VAR>hp₂ : (aeval x) p = 0<GOAL>map (algebraMap R S) p ≠ 0
<VAR>p q x y : ℝ<VAR>r : ℚ<VAR>m : ℤ<VAR>n : ℕ<VAR>h : LiouvilleWith p x<VAR>hn : n ≠ 0<GOAL>LiouvilleWith p (↑n * x)
<VAR>p q x y : ℝ<VAR>r : ℚ<VAR>m : ℤ<VAR>n : ℕ<VAR>h : LiouvilleWith p x<VAR>hn : n ≠ 0<GOAL>LiouvilleWith p (x * ↑n)
<VAR>R : Type u_3<VAR>A : Type u_1<VAR>M : Type u_2<VAR>inst✝⁷ : CommSemiring R<VAR>inst✝⁶ : Semiring A<VAR>a : A<VAR>inst✝⁵ : Algebra R A<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module A M<VAR>inst✝² : Module R M<VAR>inst✝¹ : IsScalarTower R A M<VAR>inst✝ : FaithfulSMul A M<VAR>p : R[X]<GOAL>p ∈ ⊤.annihilator ↔ p ∈ RingHom.ker (aeval a)
<VAR>R : Type u_3<VAR>A : Type u_1<VAR>M : Type u_2<VAR>inst✝⁷ : CommSemiring R<VAR>inst✝⁶ : Semiring A<VAR>a : A<VAR>inst✝⁵ : Algebra R A<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module A M<VAR>inst✝² : Module R M<VAR>inst✝¹ : IsScalarTower R A M<VAR>inst✝ : FaithfulSMul A M<VAR>p : R[X]<GOAL>(∀ (n : AEval R M a), p • n = 0) ↔ (aeval a) p = 0
<VAR>ι : Type u_1<VAR>inst✝⁴ : Fintype ι<VAR>M : Type u_2<VAR>inst✝³ : AddCommGroup M<VAR>R : Type u_3<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Module R M<VAR>I : Ideal R<VAR>b : ι → M<VAR>hb : Submodule.span R (Set.range b) = ⊤<VAR>inst✝ : DecidableEq ι<VAR>r : R<GOAL>Represents b ((_root_.algebraMap R (Matrix ι ι R)) r) ((_root_.algebraMap R (Module.End R M)) r)