ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>𝕜 : Type u_4<VAR>E : Type u_5<VAR>s : Finset ℕ<VAR>k n M N : ℕ<GOAL>rothNumberNat (M + N) ≤ rothNumberNat M + rothNumberNat N
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>𝕜 : Type u_4<VAR>E : Type u_5<VAR>s : Finset ℕ<VAR>k n M N : ℕ<GOAL>addRothNumber (range (M + N)) ≤ addRothNumber (range M) + addRothNumber (range N)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>𝕜 : Type u_4<VAR>E : Type u_5<VAR>s : Finset ℕ<VAR>k n M N : ℕ<GOAL>addRothNumber (range M ∪ map (addLeftEmbedding M) (range N)) ≤ addRothNumber (range M) + addRothNumber (map (addLeftEmbedding M) (range N))
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>n : ℕ<VAR>g : Perm α<VAR>hn2 : Fintype.card α < n + 2<VAR>hng : n ∈ g.cycleType<GOAL>g.cycleType = {n}
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>c g' : Perm α<VAR>hd : c.Disjoint g'<VAR>hc : c.IsCycle<VAR>hn2 : Fintype.card α < c.support.card + 2<VAR>hng : c.support.card ∈ (c * g').cycleType<GOAL>(c * g').cycleType = {c.support.card}
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>c g' : Perm α<VAR>hd : c.Disjoint g'<VAR>hc : c.IsCycle<VAR>hn2 : Fintype.card α < c.support.card + 2<VAR>hng : c.support.card ∈ (c * g').cycleType<GOAL>g' = 1
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>c g' : Perm α<VAR>hd : c.Disjoint g'<VAR>hc : c.IsCycle<VAR>hng : c.support.card ∈ (c * g').cycleType<VAR>g'1 : g' ≠ 1<GOAL>c.support.card + 2 ≤ Fintype.card α
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>c g' : Perm α<VAR>hd : c.Disjoint g'<VAR>hc : c.IsCycle<VAR>hng : c.support.card ∈ (c * g').cycleType<VAR>g'1 : g' ≠ 1<GOAL>c.support.card + 2 ≤ (c * g').support.card
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>c g' : Perm α<VAR>hd : c.Disjoint g'<VAR>hc : c.IsCycle<VAR>hng : c.support.card ∈ (c * g').cycleType<VAR>g'1 : g' ≠ 1<GOAL>c.support.card + 2 ≤ c.support.card + g'.support.card
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>p✝ q✝ p q : R[X]<VAR>x : R<VAR>hpq : p * q ≠ 0<GOAL>rootMultiplicity x (p * q) = rootMultiplicity x p + rootMultiplicity x q
<VAR>R S : Type u<VAR>M : Type v<VAR>M' : Type v'<VAR>M₁ : Type v<VAR>ι✝ : Type w<VAR>ι' : Type w'<VAR>η : Type u₁'<VAR>φ : η → Type u_1<VAR>inst✝¹⁰ : Ring R<VAR>inst✝⁹ : CommRing S<VAR>inst✝⁸ : AddCommGroup M<VAR>inst✝⁷ : AddCommGroup M'<VAR>inst✝⁶ : AddCommGroup M₁<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : Module R M'<VAR>inst✝³ : Module R M₁<VAR>inst✝² : StrongRankCondition R<VAR>inst✝¹ : Module.Free R M<VAR>inst✝ : Module.Free R M'<VAR>ι : Type v<GOAL>Module.rank R (ι →₀ M) = #ι * Module.rank R M
<VAR>z : ℂ<VAR>x : ℝ<GOAL>(z / ↑x).re = z.re / x
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>A : Type z<VAR>a b : R<VAR>n✝ : ℕ<VAR>inst✝¹ : Semiring R<VAR>inst✝ : NoZeroSMulDivisors ℕ R<VAR>p : R[X]<VAR>n : ℕ<GOAL>n ∈ (derivative p).support ↔ n + 1 ∈ p.support
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>A : Type z<VAR>a b : R<VAR>n✝ : ℕ<VAR>inst✝¹ : Semiring R<VAR>inst✝ : NoZeroSMulDivisors ℕ R<VAR>p : R[X]<VAR>n : ℕ<GOAL>¬p.coeff (n + 1) * ↑(n + 1) = 0 ↔ p.coeff (n + 1) ≠ 0
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>A : Type z<VAR>a b : R<VAR>n✝ : ℕ<VAR>inst✝¹ : Semiring R<VAR>inst✝ : NoZeroSMulDivisors ℕ R<VAR>p : R[X]<VAR>n : ℕ<GOAL>¬(n + 1 = 0 ∨ p.coeff (n + 1) = 0) ↔ p.coeff (n + 1) ≠ 0
<VAR>V : Type v<VAR>inst✝² : Category.{w, v} V<VAR>inst✝¹ : MonoidalCategory V<VAR>C : Type u₁<VAR>inst✝ : EnrichedCategory V C<VAR>W X Y Z : C<GOAL>(α_ (EnrichedCategory.Hom W X) (EnrichedCategory.Hom X Y) (EnrichedCategory.Hom Y Z)).hom ≫ EnrichedCategory.Hom W X ◁ eComp V X Y Z ≫ eComp V W X Z = eComp V W X Y ▷ EnrichedCategory.Hom Y Z ≫ eComp V W Y Z
<VAR>R : Type u<VAR>S : Type u_1<VAR>σ : Type v<VAR>M : Type w<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing S<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>r : R<VAR>hr : Prime r<GOAL>Prime (C r)
<VAR>R : Type u<VAR>S : Type u_1<VAR>σ : Type v<VAR>M : Type w<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing S<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>r : R<VAR>hr : Prime r<VAR>this : r ≠ 0<GOAL>Prime (C r)
<VAR>R : Type u<VAR>S : Type u_1<VAR>σ : Type v<VAR>M : Type w<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing S<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>r : R<VAR>hr : (Ideal.span {r}).IsPrime<VAR>this : r ≠ 0<GOAL>(Ideal.span {C r}).IsPrime
<VAR>R : Type u<VAR>S : Type u_1<VAR>σ : Type v<VAR>M : Type w<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing S<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>r : R<VAR>hr : (Ideal.span {r}).IsPrime<VAR>this : r ≠ 0<GOAL>C r ≠ 0
<VAR>R : Type u<VAR>S : Type u_1<VAR>σ : Type v<VAR>M : Type w<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing S<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>r : R<VAR>hr : Prime r<VAR>this : r ≠ 0<GOAL>r ≠ 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a a₁ a₂ : α<VAR>b b₁ b₂ : β<VAR>inst✝³ : OrderedRing α<VAR>inst✝² : OrderedAddCommGroup β<VAR>inst✝¹ : Module α β<VAR>inst✝ : PosSMulReflectLT α β<VAR>h : a • b₁ < a • b₂<VAR>ha : a ≤ 0<GOAL>b₂ < b₁
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a a₁ a₂ : α<VAR>b b₁ b₂ : β<VAR>inst✝³ : OrderedRing α<VAR>inst✝² : OrderedAddCommGroup β<VAR>inst✝¹ : Module α β<VAR>inst✝ : PosSMulReflectLT α β<VAR>h : -a • b₂ < -a • b₁<VAR>ha : a ≤ 0<GOAL>b₂ < b₁
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝² : Ring k<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module k V<VAR>S : AffineSpace V P<VAR>p₁ p₂ : P<VAR>s1 s2 : AffineSubspace k P<VAR>h1 : (↑s1).Nonempty<VAR>h2 : (↑s2).Nonempty<VAR>hd : IsCompl s1.direction s2.direction<GOAL>∃ p, ↑s1 ∩ ↑s2 = {p}
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝² : Ring k<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module k V<VAR>S : AffineSpace V P<VAR>p₁ p₂ : P<VAR>s1 s2 : AffineSubspace k P<VAR>h1 : (↑s1).Nonempty<VAR>h2 : (↑s2).Nonempty<VAR>hd : IsCompl s1.direction s2.direction<VAR>p : P<VAR>hp : p ∈ ↑s1 ∩ ↑s2<GOAL>∃ p, ↑s1 ∩ ↑s2 = {p}
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝² : Ring k<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module k V<VAR>S : AffineSpace V P<VAR>p₁ p₂ : P<VAR>s1 s2 : AffineSubspace k P<VAR>h1 : (↑s1).Nonempty<VAR>h2 : (↑s2).Nonempty<VAR>hd : IsCompl s1.direction s2.direction<VAR>p : P<VAR>hp : p ∈ ↑s1 ∩ ↑s2<GOAL>↑s1 ∩ ↑s2 = {p}
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝² : Ring k<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module k V<VAR>S : AffineSpace V P<VAR>p₁ p₂ : P<VAR>s1 s2 : AffineSubspace k P<VAR>h1 : (↑s1).Nonempty<VAR>h2 : (↑s2).Nonempty<VAR>hd : IsCompl s1.direction s2.direction<VAR>p : P<VAR>hp : p ∈ ↑s1 ∩ ↑s2<VAR>q : P<GOAL>q ∈ ↑s1 ∩ ↑s2 ↔ q ∈ {p}
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝² : Ring k<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module k V<VAR>S : AffineSpace V P<VAR>p₁ p₂ : P<VAR>s1 s2 : AffineSubspace k P<VAR>h1 : (↑s1).Nonempty<VAR>h2 : (↑s2).Nonempty<VAR>hd : IsCompl s1.direction s2.direction<VAR>p : P<VAR>hp : p ∈ ↑s1 ∩ ↑s2<VAR>q : P<GOAL>q ∈ ↑s1 ∩ ↑s2 ↔ q = p
<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>inst✝⁸ : DecidableEq α'<VAR>inst✝⁷ : DecidableEq β'<VAR>inst✝⁶ : DecidableEq γ<VAR>inst✝⁵ : DecidableEq γ'<VAR>inst✝⁴ : DecidableEq δ<VAR>inst✝³ : DecidableEq δ'<VAR>inst✝² : DecidableEq ε<VAR>inst✝¹ : DecidableEq ε'<VAR>f f' : α → β → γ<VAR>g g' : α → β → γ → δ<VAR>s s' : Finset α<VAR>t t' : Finset β<VAR>u u' : Finset γ<VAR>a a' : α<VAR>b b' : β<VAR>c : γ<VAR>inst✝ : DecidableEq β<VAR>t₁ t₂ : Finset β<VAR>hf : Injective (f a)<GOAL>image₂ f {a} (t₁ ∩ t₂) = image₂ f {a} t₁ ∩ image₂ f {a} t₂
<VAR>Γ : Type u_1<VAR>Γ' : Type u_2<VAR>R : Type u_3<VAR>V : Type u_4<VAR>inst✝¹ : OrderedCancelAddCommMonoid Γ<VAR>inst✝ : NonUnitalNonAssocSemiring R<VAR>r : R<VAR>x : HahnSeries Γ R<VAR>a : Γ<GOAL>(x * (single 0) r).coeff a = x.coeff a * r
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁶ : OrderedRing R<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module R V<VAR>inst✝³ : AddTorsor V P<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module R V'<VAR>inst✝ : AddTorsor V' P'<VAR>x : P<GOAL>affineSegment R x x = {x}
<VAR>α : Type u<VAR>a : α<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>inst✝¹ : Group G<VAR>inst✝ : Group G'<VAR>g : G<VAR>hg : ∀ (x : G), x ∈ zpowers g<VAR>g' : G'<VAR>hg' : orderOf g' ∣ orderOf g<GOAL>(monoidHomOfForallMemZpowers hg hg') g = g'
<VAR>α : Type u<VAR>a : α<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>inst✝¹ : Group G<VAR>inst✝ : Group G'<VAR>g : G<VAR>hg : ∀ (x : G), x ∈ zpowers g<VAR>g' : G'<VAR>hg' : orderOf g' ∣ orderOf g<GOAL>g' ^ Classical.choose ⋯ = g'
<VAR>α : Type u<VAR>a : α<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>inst✝¹ : Group G<VAR>inst✝ : Group G'<VAR>g : G<VAR>hg : ∀ (x : G), x ∈ zpowers g<VAR>g' : G'<VAR>hg' : orderOf g' ∣ orderOf g<GOAL>g' ^ Classical.choose ⋯ = g' ^ 1
<VAR>α : Type u<VAR>a : α<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>inst✝¹ : Group G<VAR>inst✝ : Group G'<VAR>g : G<VAR>hg : ∀ (x : G), x ∈ zpowers g<VAR>g' : G'<VAR>hg' : orderOf g' ∣ orderOf g<GOAL>Classical.choose ⋯ ≡ 1 [ZMOD ↑(orderOf g')]
<VAR>α : Type u<VAR>a : α<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>inst✝¹ : Group G<VAR>inst✝ : Group G'<VAR>g : G<VAR>hg : ∀ (x : G), x ∈ zpowers g<VAR>g' : G'<VAR>hg' : orderOf g' ∣ orderOf g<GOAL>Classical.choose ⋯ ≡ 1 [ZMOD ↑(orderOf g)]
<VAR>α : Type u<VAR>a : α<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>inst✝¹ : Group G<VAR>inst✝ : Group G'<VAR>g : G<VAR>hg : ∀ (x : G), x ∈ zpowers g<VAR>g' : G'<VAR>hg' : orderOf g' ∣ orderOf g<GOAL>g ^ Classical.choose ⋯ = g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m : MeasurableSpace α<VAR>μ μ₁ μ₂ : Measure α<VAR>s✝ s₁ s₂ t : Set α<VAR>I : Set β<VAR>hc : I.Countable<VAR>s : β → Set α<VAR>this : Encodable ↑I<GOAL>μ (⋃ b ∈ I, toMeasurable μ (s b)) = μ (⋃ b ∈ I, s b)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹⁴ : NormedAddCommGroup E<VAR>inst✝¹³ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>inst✝¹¹ : NormedSpace 𝕜 E<VAR>inst✝¹⁰ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>inst✝⁸ : NormedSpace ℝ F<VAR>inst✝⁷ : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝⁶ : NormedAddCommGroup G<VAR>inst✝⁵ : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>X : Type u_6<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : FirstCountableTopology X<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>f : α → E<VAR>s : Set E<VAR>inst✝ : SeparableSpace ↑s<VAR>hfi : Integrable f μ<VAR>hfm : Measurable f<VAR>hs : ∀ᵐ (x : α) ∂μ, f x ∈ closure s<VAR>y₀ : E<VAR>h₀ : y₀ ∈ s<VAR>h₀i : Integrable (fun x => y₀) μ<GOAL>Tendsto (fun n => SimpleFunc.integral μ (approxOn f hfm s y₀ h₀ n)) atTop (𝓝 (∫ (x : α), f x ∂μ))
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹⁴ : NormedAddCommGroup E<VAR>inst✝¹³ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>inst✝¹¹ : NormedSpace 𝕜 E<VAR>inst✝¹⁰ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>inst✝⁸ : NormedSpace ℝ F<VAR>inst✝⁷ : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝⁶ : NormedAddCommGroup G<VAR>inst✝⁵ : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>X : Type u_6<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : FirstCountableTopology X<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>f : α → E<VAR>s : Set E<VAR>inst✝ : SeparableSpace ↑s<VAR>hfi : Integrable f μ<VAR>hfm : Measurable f<VAR>hs : ∀ᵐ (x : α) ∂μ, f x ∈ closure s<VAR>y₀ : E<VAR>h₀ : y₀ ∈ s<VAR>h₀i : Integrable (fun x => y₀) μ<VAR>hfi' : ∀ (n : ℕ), Integrable (↑(approxOn f hfm s y₀ h₀ n)) μ<GOAL>Tendsto (fun n => SimpleFunc.integral μ (approxOn f hfm s y₀ h₀ n)) atTop (𝓝 (∫ (x : α), f x ∂μ))
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹⁴ : NormedAddCommGroup E<VAR>inst✝¹³ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>inst✝¹¹ : NormedSpace 𝕜 E<VAR>inst✝¹⁰ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>inst✝⁸ : NormedSpace ℝ F<VAR>inst✝⁷ : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝⁶ : NormedAddCommGroup G<VAR>inst✝⁵ : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>X : Type u_6<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : FirstCountableTopology X<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>f : α → E<VAR>s : Set E<VAR>inst✝ : SeparableSpace ↑s<VAR>hfi : Integrable f μ<VAR>hfm : Measurable f<VAR>hs : ∀ᵐ (x : α) ∂μ, f x ∈ closure s<VAR>y₀ : E<VAR>h₀ : y₀ ∈ s<VAR>h₀i : Integrable (fun x => y₀) μ<VAR>hfi' : ∀ (n : ℕ), Integrable (↑(approxOn f hfm s y₀ h₀ n)) μ<GOAL>Tendsto (fun n => if h : True then if hf : Integrable (fun x => ↑(approxOn f hfm s y₀ h₀ n) x) μ then L1.integralCLM (Integrable.toL1 (fun x => ↑(approxOn f hfm s y₀ h₀ n) x) hf) else 0 else 0) atTop (𝓝 (if h : True then if hf : Integrable (fun x => f x) μ then L1.integralCLM (Integrable.toL1 (fun x => f x) hf) else 0 else 0))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : TopologicalSpace β<VAR>a : α<GOAL>𝓝[<] a ⊔ 𝓝[>] a = 𝓝[≠] a
<VAR>𝕜 : Type u_1<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>s : E<VAR>p q : FormalMultilinearSeries 𝕜 𝕜 E<VAR>f g : 𝕜 → E<VAR>n : ℕ<VAR>z z₀ : 𝕜<VAR>hp : HasFPowerSeriesAt f p z₀<GOAL>HasFPowerSeriesAt (dslope f z₀) p.fslope z₀
<VAR>𝕜 : Type u_1<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>s : E<VAR>p q : FormalMultilinearSeries 𝕜 𝕜 E<VAR>f g : 𝕜 → E<VAR>n : ℕ<VAR>z z₀ : 𝕜<VAR>hp : HasFPowerSeriesAt f p z₀<VAR>hpd : deriv f z₀ = p.coeff 1<GOAL>HasFPowerSeriesAt (dslope f z₀) p.fslope z₀
<VAR>𝕜 : Type u_1<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>s : E<VAR>p q : FormalMultilinearSeries 𝕜 𝕜 E<VAR>f g : 𝕜 → E<VAR>n : ℕ<VAR>z z₀ : 𝕜<VAR>hp : HasFPowerSeriesAt f p z₀<VAR>hpd : deriv f z₀ = p.coeff 1<VAR>hp0 : p.coeff 0 = f z₀<GOAL>HasFPowerSeriesAt (dslope f z₀) p.fslope z₀
<VAR>𝕜 : Type u_1<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>s : E<VAR>p q : FormalMultilinearSeries 𝕜 𝕜 E<VAR>f g : 𝕜 → E<VAR>n : ℕ<VAR>z z₀ : 𝕜<VAR>hpd : deriv f z₀ = p.coeff 1<VAR>hp0 : p.coeff 0 = f z₀<VAR>hp : ∀ᶠ (z : 𝕜) in 𝓝 0, HasSum (fun n => z ^ n • p.coeff n) (f (z₀ + z))<GOAL>∀ᶠ (z : 𝕜) in 𝓝 0, HasSum (fun n => z ^ n • p.coeff (n + 1)) (dslope f z₀ (z₀ + z))
<VAR>𝕜 : Type u_1<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>s : E<VAR>p q : FormalMultilinearSeries 𝕜 𝕜 E<VAR>f g : 𝕜 → E<VAR>n : ℕ<VAR>z z₀ : 𝕜<VAR>hpd : deriv f z₀ = p.coeff 1<VAR>hp0 : p.coeff 0 = f z₀<VAR>hp : ∀ᶠ (z : 𝕜) in 𝓝 0, HasSum (fun n => z ^ n • p.coeff n) (f (z₀ + z))<VAR>x : 𝕜<VAR>hx : HasSum (fun n => x ^ n • p.coeff n) (f (z₀ + x))<GOAL>HasSum (fun n => x ^ n • p.coeff (n + 1)) (dslope f z₀ (z₀ + x))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁴ : TopologicalSpace α<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : (i : ι) → TopologicalSpace (π i)<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : TopologicalSpace δ<VAR>f : α → β<GOAL>Continuous f ↔ ContinuousOn f univ
<VAR>α : Type u_1<VAR>inst✝¹ : BEq α<VAR>inst✝ : LawfulBEq α<VAR>l₁ l₂ l₃ : List α<GOAL>l₁.diff (l₂ ++ l₃) = (l₁.diff l₂).diff l₃
<VAR>α : Type u_1<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : BorelSpace α<VAR>μ : Measure α<VAR>inst✝¹ : μ.WeaklyRegular<VAR>inst✝ : SigmaFinite μ<VAR>f : α → ℝ≥0<VAR>fmeas : AEMeasurable f μ<VAR>ε : ℝ≥0∞<VAR>ε0 : ε ≠ 0<GOAL>∃ g, (∀ (x : α), ↑(f x) < g x) ∧ LowerSemicontinuous g ∧ ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), ↑(f x) ∂μ + ε
<VAR>α : Type u_1<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : BorelSpace α<VAR>μ : Measure α<VAR>inst✝¹ : μ.WeaklyRegular<VAR>inst✝ : SigmaFinite μ<VAR>f : α → ℝ≥0<VAR>fmeas : AEMeasurable f μ<VAR>ε : ℝ≥0∞<VAR>ε0 : ε ≠ 0<VAR>this : ε / 2 ≠ 0<GOAL>∃ g, (∀ (x : α), ↑(f x) < g x) ∧ LowerSemicontinuous g ∧ ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), ↑(f x) ∂μ + ε
<VAR>α : Type u_1<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : BorelSpace α<VAR>μ : Measure α<VAR>inst✝¹ : μ.WeaklyRegular<VAR>inst✝ : SigmaFinite μ<VAR>f : α → ℝ≥0<VAR>fmeas : AEMeasurable f μ<VAR>ε : ℝ≥0∞<VAR>ε0 : ε ≠ 0<VAR>this : ε / 2 ≠ 0<VAR>g0 : α → ℝ≥0∞<VAR>f_lt_g0 : ∀ (x : α), ↑(AEMeasurable.mk f fmeas x) < g0 x<VAR>g0_cont : LowerSemicontinuous g0<VAR>g0_int : ∫⁻ (x : α), g0 x ∂μ ≤ ∫⁻ (x : α), ↑(AEMeasurable.mk f fmeas x) ∂μ + ε / 2<GOAL>∃ g, (∀ (x : α), ↑(f x) < g x) ∧ LowerSemicontinuous g ∧ ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), ↑(f x) ∂μ + ε
<VAR>α : Type u_1<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : BorelSpace α<VAR>μ : Measure α<VAR>inst✝¹ : μ.WeaklyRegular<VAR>inst✝ : SigmaFinite μ<VAR>f : α → ℝ≥0<VAR>fmeas : AEMeasurable f μ<VAR>ε : ℝ≥0∞<VAR>ε0 : ε ≠ 0<VAR>this : ε / 2 ≠ 0<VAR>g0 : α → ℝ≥0∞<VAR>f_lt_g0 : ∀ (x : α), ↑(AEMeasurable.mk f fmeas x) < g0 x<VAR>g0_cont : LowerSemicontinuous g0<VAR>g0_int : ∫⁻ (x : α), g0 x ∂μ ≤ ∫⁻ (x : α), ↑(AEMeasurable.mk f fmeas x) ∂μ + ε / 2<VAR>s : Set α<VAR>hs : {x | (fun x => f x = AEMeasurable.mk f fmeas x) x}ᶜ ⊆ s<VAR>smeas : MeasurableSet s<VAR>μs : μ s = 0<GOAL>∃ g, (∀ (x : α), ↑(f x) < g x) ∧ LowerSemicontinuous g ∧ ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), ↑(f x) ∂μ + ε
<VAR>α : Type u_1<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : BorelSpace α<VAR>μ : Measure α<VAR>inst✝¹ : μ.WeaklyRegular<VAR>inst✝ : SigmaFinite μ<VAR>f : α → ℝ≥0<VAR>fmeas : AEMeasurable f μ<VAR>ε : ℝ≥0∞<VAR>ε0 : ε ≠ 0<VAR>this : ε / 2 ≠ 0<VAR>g0 : α → ℝ≥0∞<VAR>f_lt_g0 : ∀ (x : α), ↑(AEMeasurable.mk f fmeas x) < g0 x<VAR>g0_cont : LowerSemicontinuous g0<VAR>g0_int : ∫⁻ (x : α), g0 x ∂μ ≤ ∫⁻ (x : α), ↑(AEMeasurable.mk f fmeas x) ∂μ + ε / 2<VAR>s : Set α<VAR>hs : {x | (fun x => f x = AEMeasurable.mk f fmeas x) x}ᶜ ⊆ s<VAR>smeas : MeasurableSet s<VAR>μs : μ s = 0<VAR>g1 : α → ℝ≥0∞<VAR>le_g1 : ∀ (x : α), s.indicator (fun _x => ⊤) x ≤ g1 x<VAR>g1_cont : LowerSemicontinuous g1<VAR>g1_int : ∫⁻ (x : α), g1 x ∂μ ≤ ∫⁻ (x : α), s.indicator (fun _x => ⊤) x ∂μ + ε / 2<GOAL>∃ g, (∀ (x : α), ↑(f x) < g x) ∧ LowerSemicontinuous g ∧ ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), ↑(f x) ∂μ + ε
<VAR>α : Type u_1<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : BorelSpace α<VAR>μ : Measure α<VAR>inst✝¹ : μ.WeaklyRegular<VAR>inst✝ : SigmaFinite μ<VAR>f : α → ℝ≥0<VAR>fmeas : AEMeasurable f μ<VAR>ε : ℝ≥0∞<VAR>ε0 : ε ≠ 0<VAR>this : ε / 2 ≠ 0<VAR>g0 : α → ℝ≥0∞<VAR>f_lt_g0 : ∀ (x : α), ↑(AEMeasurable.mk f fmeas x) < g0 x<VAR>g0_cont : LowerSemicontinuous g0<VAR>g0_int : ∫⁻ (x : α), g0 x ∂μ ≤ ∫⁻ (x : α), ↑(AEMeasurable.mk f fmeas x) ∂μ + ε / 2<VAR>s : Set α<VAR>hs : {x | (fun x => f x = AEMeasurable.mk f fmeas x) x}ᶜ ⊆ s<VAR>smeas : MeasurableSet s<VAR>μs : μ s = 0<VAR>g1 : α → ℝ≥0∞<VAR>le_g1 : ∀ (x : α), s.indicator (fun _x => ⊤) x ≤ g1 x<VAR>g1_cont : LowerSemicontinuous g1<VAR>g1_int : ∫⁻ (x : α), g1 x ∂μ ≤ ∫⁻ (x : α), s.indicator (fun _x => ⊤) x ∂μ + ε / 2<VAR>x : α<GOAL>↑(f x) < (fun x => g0 x + g1 x) x
<VAR>α : Type u_1<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : BorelSpace α<VAR>μ : Measure α<VAR>inst✝¹ : μ.WeaklyRegular<VAR>inst✝ : SigmaFinite μ<VAR>f : α → ℝ≥0<VAR>fmeas : AEMeasurable f μ<VAR>ε : ℝ≥0∞<VAR>ε0 : ε ≠ 0<VAR>this : ε / 2 ≠ 0<VAR>g0 : α → ℝ≥0∞<VAR>f_lt_g0 : ∀ (x : α), ↑(AEMeasurable.mk f fmeas x) < g0 x<VAR>g0_cont : LowerSemicontinuous g0<VAR>g0_int : ∫⁻ (x : α), g0 x ∂μ ≤ ∫⁻ (x : α), ↑(AEMeasurable.mk f fmeas x) ∂μ + ε / 2<VAR>s : Set α<VAR>hs : {x | (fun x => f x = AEMeasurable.mk f fmeas x) x}ᶜ ⊆ s<VAR>smeas : MeasurableSet s<VAR>μs : μ s = 0<VAR>g1 : α → ℝ≥0∞<VAR>le_g1 : ∀ (x : α), s.indicator (fun _x => ⊤) x ≤ g1 x<VAR>g1_cont : LowerSemicontinuous g1<VAR>g1_int : ∫⁻ (x : α), g1 x ∂μ ≤ ∫⁻ (x : α), s.indicator (fun _x => ⊤) x ∂μ + ε / 2<GOAL>∫⁻ (x : α), (fun x => g0 x + g1 x) x ∂μ ≤ ∫⁻ (x : α), ↑(f x) ∂μ + ε
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝² : Field 𝕜<VAR>inst✝¹ : Ring A<VAR>inst✝ : Algebra 𝕜 A<VAR>p : 𝕜[X]<VAR>a : A<GOAL>p ∈ annIdeal 𝕜 a ↔ ∃ s, p = s • annIdealGenerator 𝕜 a
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>X : Type u_3<VAR>X' : Type u_4<VAR>Y : Type u_5<VAR>Z : 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>tX : TopologicalSpace X<VAR>tY : TopologicalSpace Y<VAR>tZ : TopologicalSpace Z<VAR>uα : UniformSpace α<VAR>uβ : UniformSpace β<VAR>uγ : UniformSpace γ<VAR>p : κ → Prop<VAR>s : κ → Set X<VAR>F : ι → X → α<VAR>x₀ : X<VAR>hX : (𝓝 x₀).HasBasis p s<GOAL>EquicontinuousAt F x₀ ↔ ∀ U ∈ 𝓤 α, ∃ k, p k ∧ ∀ x ∈ s k, ∀ (i : ι), (F i x₀, F i x) ∈ U
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>X : Type u_3<VAR>X' : Type u_4<VAR>Y : Type u_5<VAR>Z : 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>tX : TopologicalSpace X<VAR>tY : TopologicalSpace Y<VAR>tZ : TopologicalSpace Z<VAR>uα : UniformSpace α<VAR>uβ : UniformSpace β<VAR>uγ : UniformSpace γ<VAR>p : κ → Prop<VAR>s : κ → Set X<VAR>F : ι → X → α<VAR>x₀ : X<VAR>hX : (𝓝 x₀).HasBasis p s<GOAL>(∀ ib ∈ 𝓤 α, ∃ ia, p ia ∧ ∀ x ∈ s ia, (⇑UniformFun.ofFun ∘ swap F) x ∈ {g | ((⇑UniformFun.ofFun ∘ swap F) x₀, g) ∈ UniformFun.gen ι α ib}) ↔ ∀ U ∈ 𝓤 α, ∃ k, p k ∧ ∀ x ∈ s k, ∀ (i : ι), (F i x₀, F i x) ∈ U
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : PseudoEMetricSpace α<VAR>δ : ℝ<VAR>s : Set α<VAR>x✝ : α<VAR>E : Set α<VAR>x : α<VAR>h : x ∉ closure E<GOAL>∀ᶠ (δ : ℝ) in 𝓝 0, x ∉ thickening δ E
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : PseudoEMetricSpace α<VAR>δ : ℝ<VAR>s : Set α<VAR>x✝ : α<VAR>E : Set α<VAR>x : α<VAR>h : x ∉ closure E<VAR>ε : ℝ<VAR>ε_pos : 0 < ε<VAR>ε_lt : ENNReal.ofReal ε < infEdist x E<GOAL>∀ᶠ (δ : ℝ) in 𝓝 0, x ∉ thickening δ E
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : PseudoEMetricSpace α<VAR>δ✝ : ℝ<VAR>s : Set α<VAR>x✝ : α<VAR>E : Set α<VAR>x : α<VAR>h : x ∉ closure E<VAR>ε : ℝ<VAR>ε_pos : 0 < ε<VAR>ε_lt : ENNReal.ofReal ε < infEdist x E<VAR>δ : ℝ<VAR>hδ : δ < ε<GOAL>x ∉ thickening δ E
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : PseudoEMetricSpace α<VAR>δ✝ : ℝ<VAR>s : Set α<VAR>x✝ : α<VAR>E : Set α<VAR>x : α<VAR>h : x ∉ closure E<VAR>ε : ℝ<VAR>ε_pos : 0 < ε<VAR>ε_lt : ENNReal.ofReal ε < infEdist x E<VAR>δ : ℝ<VAR>hδ : δ < ε<GOAL>ENNReal.ofReal δ ≤ infEdist x E
<VAR>b x✝ y : ℝ<VAR>b_pos : 0 < b<VAR>b_ne_one : b ≠ 1<VAR>x : ℝ<VAR>a✝ : x ∈ univ<GOAL>x ∈ logb b '' Iio 0
<VAR>b x✝ y : ℝ<VAR>b_pos : 0 < b<VAR>b_ne_one : b ≠ 1<VAR>x : ℝ<VAR>a✝ : x ∈ univ<GOAL>-b ^ x ∈ Iio 0 ∧ logb b (-b ^ x) = x
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m : MeasurableSpace α<VAR>inst✝ : NormedAddCommGroup E<VAR>p✝ : ℝ≥0∞<VAR>q : ℝ<VAR>μ : Measure α<VAR>f g : α → E<VAR>hf : AEStronglyMeasurable f μ<VAR>hg : AEStronglyMeasurable g μ<VAR>p : ℝ≥0∞<GOAL>eLpNorm (f - g) p μ ≤ LpAddConst p * (eLpNorm f p μ + eLpNorm g p μ)
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : MonoidalCategory C<VAR>inst✝ : BraidedCategory C<VAR>M : Mon_ C<GOAL>(tensor_μ C (𝟙_ C, M.X) (𝟙_ C, M.X) ≫ ((λ_ (𝟙_ C)).hom ⊗ M.mul)) ≫ (λ_ M.X).hom = ((λ_ M.X).hom ⊗ (λ_ M.X).hom) ≫ M.mul
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : MonoidalCategory C<VAR>inst✝ : BraidedCategory C<VAR>M : Mon_ C<GOAL>(tensor_μ C (𝟙_ C, M.X) (𝟙_ C, M.X) ≫ ((λ_ (𝟙_ C)).hom ⊗ 𝟙 (M.X ⊗ M.X)) ≫ (𝟙 (𝟙_ C) ⊗ M.mul)) ≫ (λ_ M.X).hom = ((λ_ M.X).hom ⊗ (λ_ M.X).hom) ≫ 𝟙 (M.X ⊗ M.X) ≫ M.mul