ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>inst✝² : ConditionallyCompleteLinearOrder α<VAR>f✝ : Filter α<VAR>b : α<VAR>v : Filter ι<VAR>p : ι' → Prop<VAR>s : ι' → Set ι<VAR>inst✝¹ : Countable (Subtype p)<VAR>inst✝ : Nonempty (Subtype p)<VAR>hv : v.HasBasis p s<VAR>f : ι → α<VAR>H : ¬∃ j, s ↑j = ∅<GOAL>liminf f v = if ∀ (j : Subtype p), ¬BddBelow (range fun i => f ↑i) then sSup ∅ else ⨆ j, ⨅ i, f ↑i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>inst✝² : ConditionallyCompleteLinearOrder α<VAR>f✝ : Filter α<VAR>b : α<VAR>v : Filter ι<VAR>p : ι' → Prop<VAR>s : ι' → Set ι<VAR>inst✝¹ : Countable (Subtype p)<VAR>inst✝ : Nonempty (Subtype p)<VAR>hv : v.HasBasis p s<VAR>f : ι → α<VAR>H : ¬∃ j, s ↑j = ∅<VAR>H' : ¬∀ (j : Subtype p), ¬BddBelow (range fun i => f ↑i)<GOAL>liminf f v = if ∀ (j : Subtype p), ¬BddBelow (range fun i => f ↑i) then sSup ∅ else ⨆ j, ⨅ i, f ↑i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>inst✝² : ConditionallyCompleteLinearOrder α<VAR>f✝ : Filter α<VAR>b : α<VAR>v : Filter ι<VAR>p : ι' → Prop<VAR>s : ι' → Set ι<VAR>inst✝¹ : Countable (Subtype p)<VAR>inst✝ : Nonempty (Subtype p)<VAR>hv : v.HasBasis p s<VAR>f : ι → α<VAR>H : ¬∃ j, s ↑j = ∅<VAR>H' : ¬∀ (j : Subtype p), ¬BddBelow (range fun i => f ↑i)<GOAL>liminf f v = ⨆ j, ⨅ i, f ↑i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>inst✝² : ConditionallyCompleteLinearOrder α<VAR>f✝ : Filter α<VAR>b : α<VAR>v : Filter ι<VAR>p : ι' → Prop<VAR>s : ι' → Set ι<VAR>inst✝¹ : Countable (Subtype p)<VAR>inst✝ : Nonempty (Subtype p)<VAR>hv : v.HasBasis p s<VAR>f : ι → α<VAR>H : ¬∃ j, s ↑j = ∅<VAR>H' : ¬∀ (j : Subtype p), ¬BddBelow (range fun i => f ↑i)<GOAL>∀ (j : Subtype p), (s ↑j).Nonempty
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>inst✝² : ConditionallyCompleteLinearOrder α<VAR>f✝ : Filter α<VAR>b : α<VAR>v : Filter ι<VAR>p : ι' → Prop<VAR>s : ι' → Set ι<VAR>inst✝¹ : Countable (Subtype p)<VAR>inst✝ : Nonempty (Subtype p)<VAR>hv : v.HasBasis p s<VAR>f : ι → α<VAR>H : ¬∃ j, s ↑j = ∅<VAR>H' : ¬∀ (j : Subtype p), ¬BddBelow (range fun i => f ↑i)<GOAL>∃ j, BddBelow (range fun i => f ↑i)
<VAR>a b c d m n k : ℕ<VAR>p q : ℕ → Prop<VAR>H : m * n = 1<GOAL>n * m = 1
<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>L : Type u_6<VAR>inst✝ : RCLike L<VAR>r : L<VAR>f : α → L<GOAL>∫ (a : α), f a * r ∂μ = (∫ (a : α), f a ∂μ) * r
<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>L : Type u_6<VAR>inst✝ : RCLike L<VAR>r : L<VAR>f : α → L<GOAL>∫ (a : α), r * f a ∂μ = r * ∫ (a : α), f a ∂μ
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>a : α<VAR>s t : Multiset α<GOAL>a ::ₘ s + t = a ::ₘ (s + t)
<VAR>ι : Type u<VAR>s : Finset ι<VAR>w z : ι → ℝ<VAR>x : ℝ<VAR>hw : ∀ i ∈ s, 0 ≤ w i<VAR>hw' : ∑ i ∈ s, w i = 1<VAR>hz : ∀ i ∈ s, 0 ≤ z i<VAR>hx : ∀ i ∈ s, w i ≠ 0 → z i = x<GOAL>∏ i ∈ s, z i ^ w i = ∏ i ∈ s, x ^ w i
<VAR>ι : Type u<VAR>s : Finset ι<VAR>w z : ι → ℝ<VAR>x : ℝ<VAR>hw : ∀ i ∈ s, 0 ≤ w i<VAR>hw' : ∑ i ∈ s, w i = 1<VAR>hz : ∀ i ∈ s, 0 ≤ z i<VAR>hx : ∀ i ∈ s, w i ≠ 0 → z i = x<VAR>i : ι<VAR>hi : i ∈ s<GOAL>z i ^ w i = x ^ w i
<VAR>ι : Type u<VAR>s : Finset ι<VAR>w z : ι → ℝ<VAR>x : ℝ<VAR>hw : ∀ i ∈ s, 0 ≤ w i<VAR>hw' : ∑ i ∈ s, w i = 1<VAR>hz : ∀ i ∈ s, 0 ≤ z i<VAR>hx : ∀ i ∈ s, w i ≠ 0 → z i = x<VAR>i : ι<VAR>hi : i ∈ s<VAR>h₀ : w i = 0<GOAL>z i ^ w i = x ^ w i
<VAR>ι : Type u<VAR>s : Finset ι<VAR>w z : ι → ℝ<VAR>x : ℝ<VAR>hw : ∀ i ∈ s, 0 ≤ w i<VAR>hw' : ∑ i ∈ s, w i = 1<VAR>hz : ∀ i ∈ s, 0 ≤ z i<VAR>hx : ∀ i ∈ s, w i ≠ 0 → z i = x<VAR>i : ι<VAR>hi : i ∈ s<VAR>h₀ : w i ≠ 0<GOAL>z i ^ w i = x ^ w i
<VAR>ι : Type u<VAR>s : Finset ι<VAR>w z : ι → ℝ<VAR>x : ℝ<VAR>hw : ∀ i ∈ s, 0 ≤ w i<VAR>hw' : ∑ i ∈ s, w i = 1<VAR>hz : ∀ i ∈ s, 0 ≤ z i<VAR>hx : ∀ i ∈ s, w i ≠ 0 → z i = x<GOAL>∏ i ∈ s, x ^ w i = x
<VAR>ι : Type u<VAR>s : Finset ι<VAR>w z : ι → ℝ<VAR>x : ℝ<VAR>hw : ∀ i ∈ s, 0 ≤ w i<VAR>hw' : ∑ i ∈ s, w i = 1<VAR>hz : ∀ i ∈ s, 0 ≤ z i<VAR>hx : ∀ i ∈ s, w i ≠ 0 → z i = x<GOAL>0 ≤ x
<VAR>ι : Type u<VAR>s : Finset ι<VAR>w z : ι → ℝ<VAR>x : ℝ<VAR>hw : ∀ i ∈ s, 0 ≤ w i<VAR>hw' : ∑ i ∈ s, w i = 1<VAR>hz : ∀ i ∈ s, 0 ≤ z i<VAR>hx : ∀ i ∈ s, w i ≠ 0 → z i = x<VAR>this : ∑ i ∈ s, w i ≠ 0<GOAL>0 ≤ x
<VAR>ι : Type u<VAR>s : Finset ι<VAR>w z : ι → ℝ<VAR>x : ℝ<VAR>hw : ∀ i ∈ s, 0 ≤ w i<VAR>hw' : ∑ i ∈ s, w i = 1<VAR>hz : ∀ i ∈ s, 0 ≤ z i<VAR>hx : ∀ i ∈ s, w i ≠ 0 → z i = x<VAR>this : ∑ i ∈ s, w i ≠ 0<VAR>i : ι<VAR>his : i ∈ s<VAR>hi : w i ≠ 0<GOAL>0 ≤ x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : Sub α<VAR>inst✝² : Bot α<VAR>inst✝¹ : Sub β<VAR>inst✝ : Bot β<VAR>f : α → β<VAR>h : ∀ (x y : α), f (x - y) = f x - f y<VAR>h₀ : f ⊥ = ⊥<VAR>x✝ : WithTop α<GOAL>map f (x✝ - ⊤) = map f x✝ - map f ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : Sub α<VAR>inst✝² : Bot α<VAR>inst✝¹ : Sub β<VAR>inst✝ : Bot β<VAR>f : α → β<VAR>h : ∀ (x y : α), f (x - y) = f x - f y<VAR>h₀ : f ⊥ = ⊥<VAR>x y : α<GOAL>map f (↑x - ↑y) = map f ↑x - map f ↑y
<VAR>p : GHSpace<GOAL>toGHSpace ↥(Quot.out p) = p
<VAR>p : GHSpace<GOAL>⟦Quot.out p⟧ = p
<VAR>R : Type u_1<VAR>inst✝¹⁸ : CommSemiring R<VAR>R' : Type u_2<VAR>inst✝¹⁷ : Monoid R'<VAR>R'' : Type u_3<VAR>inst✝¹⁶ : Semiring R''<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>Q : Type u_7<VAR>S : Type u_8<VAR>T : Type u_9<VAR>inst✝¹⁵ : AddCommMonoid M<VAR>inst✝¹⁴ : AddCommMonoid N<VAR>inst✝¹³ : AddCommMonoid P<VAR>inst✝¹² : AddCommMonoid Q<VAR>inst✝¹¹ : AddCommMonoid S<VAR>inst✝¹⁰ : AddCommMonoid T<VAR>inst✝⁹ : Module R M<VAR>inst✝⁸ : Module R N<VAR>inst✝⁷ : Module R P<VAR>inst✝⁶ : Module R Q<VAR>inst✝⁵ : Module R S<VAR>inst✝⁴ : Module R T<VAR>inst✝³ : DistribMulAction R' M<VAR>inst✝² : Module R'' M<VAR>inst✝¹ : SMulCommClass R R' M<VAR>inst✝ : SMulCommClass R R'' M<VAR>x : M ⊗[R] N<VAR>this : ∀ (r : R'') (m : M) (n : N), r • m ⊗ₜ[R] n = (r • m) ⊗ₜ[R] n<GOAL>0 • 0 = 0
<VAR>R : Type u_1<VAR>inst✝¹⁸ : CommSemiring R<VAR>R' : Type u_2<VAR>inst✝¹⁷ : Monoid R'<VAR>R'' : Type u_3<VAR>inst✝¹⁶ : Semiring R''<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>Q : Type u_7<VAR>S : Type u_8<VAR>T : Type u_9<VAR>inst✝¹⁵ : AddCommMonoid M<VAR>inst✝¹⁴ : AddCommMonoid N<VAR>inst✝¹³ : AddCommMonoid P<VAR>inst✝¹² : AddCommMonoid Q<VAR>inst✝¹¹ : AddCommMonoid S<VAR>inst✝¹⁰ : AddCommMonoid T<VAR>inst✝⁹ : Module R M<VAR>inst✝⁸ : Module R N<VAR>inst✝⁷ : Module R P<VAR>inst✝⁶ : Module R Q<VAR>inst✝⁵ : Module R S<VAR>inst✝⁴ : Module R T<VAR>inst✝³ : DistribMulAction R' M<VAR>inst✝² : Module R'' M<VAR>inst✝¹ : SMulCommClass R R' M<VAR>inst✝ : SMulCommClass R R'' M<VAR>x : M ⊗[R] N<VAR>this : ∀ (r : R'') (m : M) (n : N), r • m ⊗ₜ[R] n = (r • m) ⊗ₜ[R] n<VAR>m : M<VAR>n : N<GOAL>0 • m ⊗ₜ[R] n = 0
<VAR>R : Type u_1<VAR>inst✝¹⁸ : CommSemiring R<VAR>R' : Type u_2<VAR>inst✝¹⁷ : Monoid R'<VAR>R'' : Type u_3<VAR>inst✝¹⁶ : Semiring R''<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>Q : Type u_7<VAR>S : Type u_8<VAR>T : Type u_9<VAR>inst✝¹⁵ : AddCommMonoid M<VAR>inst✝¹⁴ : AddCommMonoid N<VAR>inst✝¹³ : AddCommMonoid P<VAR>inst✝¹² : AddCommMonoid Q<VAR>inst✝¹¹ : AddCommMonoid S<VAR>inst✝¹⁰ : AddCommMonoid T<VAR>inst✝⁹ : Module R M<VAR>inst✝⁸ : Module R N<VAR>inst✝⁷ : Module R P<VAR>inst✝⁶ : Module R Q<VAR>inst✝⁵ : Module R S<VAR>inst✝⁴ : Module R T<VAR>inst✝³ : DistribMulAction R' M<VAR>inst✝² : Module R'' M<VAR>inst✝¹ : SMulCommClass R R' M<VAR>inst✝ : SMulCommClass R R'' M<VAR>x✝ : M ⊗[R] N<VAR>this : ∀ (r : R'') (m : M) (n : N), r • m ⊗ₜ[R] n = (r • m) ⊗ₜ[R] n<VAR>x y : M ⊗[R] N<VAR>ihx : 0 • x = 0<VAR>ihy : 0 • y = 0<GOAL>0 • (x + y) = 0
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>A : Type u_1<VAR>B : Type u_2<VAR>inst✝³ : CommRing A<VAR>inst✝² : CommRing B<VAR>inst✝¹ : IsDomain A<VAR>inst✝ : IsDomain B<VAR>p : A[X]<VAR>f : A →+* B<VAR>h : map f p ≠ 0<GOAL>Multiset.card p.roots ≤ Multiset.card (map f p).roots
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>A : Type u_1<VAR>B : Type u_2<VAR>inst✝³ : CommRing A<VAR>inst✝² : CommRing B<VAR>inst✝¹ : IsDomain A<VAR>inst✝ : IsDomain B<VAR>p : A[X]<VAR>f : A →+* B<VAR>h : map f p ≠ 0<GOAL>Multiset.card (Multiset.map (⇑f) p.roots) ≤ Multiset.card (map f p).roots
<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>x : G<VAR>g : G →L[𝕜] E<VAR>hf : ContDiffWithinAt 𝕜 n f s (g x)<VAR>m : ℕ<VAR>hm : ↑m ≤ n<VAR>u : Set E<VAR>hu : u ∈ 𝓝[insert (g x) s] g x<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>hp : HasFTaylorSeriesUpToOn (↑m) f p u<GOAL>∃ u ∈ 𝓝[insert x (⇑g ⁻¹' s)] x, ∃ p, HasFTaylorSeriesUpToOn (↑m) (f ∘ ⇑g) p u
<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>x : G<VAR>g : G →L[𝕜] E<VAR>hf : ContDiffWithinAt 𝕜 n f s (g x)<VAR>m : ℕ<VAR>hm : ↑m ≤ n<VAR>u : Set E<VAR>hu : u ∈ 𝓝[insert (g x) s] g x<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>hp : HasFTaylorSeriesUpToOn (↑m) f p u<GOAL>⇑g ⁻¹' u ∈ 𝓝[insert x (⇑g ⁻¹' s)] 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>x : G<VAR>g : G →L[𝕜] E<VAR>hf : ContDiffWithinAt 𝕜 n f s (g x)<VAR>m : ℕ<VAR>hm : ↑m ≤ n<VAR>u : Set E<VAR>hu : u ∈ 𝓝[insert (g x) s] g x<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>hp : HasFTaylorSeriesUpToOn (↑m) f p u<GOAL>MapsTo (⇑g) (insert x (⇑g ⁻¹' s)) (insert (g x) s)
<VAR>E : Type u_1<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : MeasurableSpace E<VAR>inst✝³ : BorelSpace E<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>C D : ℝ≥0<VAR>f g : E → ℝ<VAR>s✝ : Set E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>hf : LipschitzWith C f<VAR>s : Set E<VAR>hs : s.Countable<VAR>B : Basis ↑(Basis.ofVectorSpaceIndex ℝ E) ℝ E<GOAL>∀ᵐ (x : E) ∂μ, ∃ L, ∀ v ∈ s, HasLineDerivAt ℝ f (L v) x v
<VAR>E : Type u_1<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : MeasurableSpace E<VAR>inst✝³ : BorelSpace E<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>C D : ℝ≥0<VAR>f g : E → ℝ<VAR>s✝ : Set E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>hf : LipschitzWith C f<VAR>s : Set E<VAR>hs : s.Countable<VAR>B : Basis ↑(Basis.ofVectorSpaceIndex ℝ E) ℝ E<VAR>I1 : ∀ᵐ (x : E) ∂μ, ∀ v ∈ s, lineDeriv ℝ f x (∑ i : ↑(Basis.ofVectorSpaceIndex ℝ E), (B.repr v) i • B i) = ∑ i : ↑(Basis.ofVectorSpaceIndex ℝ E), (B.repr v) i • lineDeriv ℝ f x (B i)<GOAL>∀ᵐ (x : E) ∂μ, ∃ L, ∀ v ∈ s, HasLineDerivAt ℝ f (L v) x v
<VAR>E : Type u_1<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : MeasurableSpace E<VAR>inst✝³ : BorelSpace E<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>C D : ℝ≥0<VAR>f g : E → ℝ<VAR>s✝ : Set E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>hf : LipschitzWith C f<VAR>s : Set E<VAR>hs : s.Countable<VAR>B : Basis ↑(Basis.ofVectorSpaceIndex ℝ E) ℝ E<VAR>I1 : ∀ᵐ (x : E) ∂μ, ∀ v ∈ s, lineDeriv ℝ f x (∑ i : ↑(Basis.ofVectorSpaceIndex ℝ E), (B.repr v) i • B i) = ∑ i : ↑(Basis.ofVectorSpaceIndex ℝ E), (B.repr v) i • lineDeriv ℝ f x (B i)<VAR>I2 : ∀ᵐ (x : E) ∂μ, ∀ v ∈ s, LineDifferentiableAt ℝ f x v<GOAL>∀ᵐ (x : E) ∂μ, ∃ L, ∀ v ∈ s, HasLineDerivAt ℝ f (L v) x v
<VAR>E : Type u_1<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : MeasurableSpace E<VAR>inst✝³ : BorelSpace E<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>C D : ℝ≥0<VAR>f g : E → ℝ<VAR>s✝ : Set E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>hf : LipschitzWith C f<VAR>s : Set E<VAR>hs : s.Countable<VAR>B : Basis ↑(Basis.ofVectorSpaceIndex ℝ E) ℝ E<VAR>I1 : ∀ᵐ (x : E) ∂μ, ∀ v ∈ s, lineDeriv ℝ f x (∑ i : ↑(Basis.ofVectorSpaceIndex ℝ E), (B.repr v) i • B i) = ∑ i : ↑(Basis.ofVectorSpaceIndex ℝ E), (B.repr v) i • lineDeriv ℝ f x (B i)<VAR>I2 : ∀ᵐ (x : E) ∂μ, ∀ v ∈ s, LineDifferentiableAt ℝ f x v<VAR>x : E<VAR>hx : ∀ v ∈ s, lineDeriv ℝ f x (∑ i : ↑(Basis.ofVectorSpaceIndex ℝ E), (B.repr v) i • B i) = ∑ i : ↑(Basis.ofVectorSpaceIndex ℝ E), (B.repr v) i • lineDeriv ℝ f x (B i)<VAR>h'x : ∀ v ∈ s, LineDifferentiableAt ℝ f x v<GOAL>∃ L, ∀ v ∈ s, HasLineDerivAt ℝ f (L v) x v
<VAR>E : Type u_1<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : MeasurableSpace E<VAR>inst✝³ : BorelSpace E<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>C D : ℝ≥0<VAR>f g : E → ℝ<VAR>s✝ : Set E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>hf : LipschitzWith C f<VAR>s : Set E<VAR>hs : s.Countable<VAR>B : Basis ↑(Basis.ofVectorSpaceIndex ℝ E) ℝ E<VAR>I1 : ∀ᵐ (x : E) ∂μ, ∀ v ∈ s, lineDeriv ℝ f x (∑ i : ↑(Basis.ofVectorSpaceIndex ℝ E), (B.repr v) i • B i) = ∑ i : ↑(Basis.ofVectorSpaceIndex ℝ E), (B.repr v) i • lineDeriv ℝ f x (B i)<VAR>I2 : ∀ᵐ (x : E) ∂μ, ∀ v ∈ s, LineDifferentiableAt ℝ f x v<VAR>x : E<VAR>hx : ∀ v ∈ s, lineDeriv ℝ f x (∑ i : ↑(Basis.ofVectorSpaceIndex ℝ E), (B.repr v) i • B i) = ∑ i : ↑(Basis.ofVectorSpaceIndex ℝ E), (B.repr v) i • lineDeriv ℝ f x (B i)<VAR>h'x : ∀ v ∈ s, LineDifferentiableAt ℝ f x v<VAR>L : E →L[ℝ] ℝ := LinearMap.toContinuousLinearMap ((B.constr ℝ) fun i => lineDeriv ℝ f x (B i))<VAR>v : E<VAR>hv : v ∈ s<GOAL>HasLineDerivAt ℝ f (L v) x v
<VAR>E : Type u_1<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : MeasurableSpace E<VAR>inst✝³ : BorelSpace E<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>C D : ℝ≥0<VAR>f g : E → ℝ<VAR>s✝ : Set E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>hf : LipschitzWith C f<VAR>s : Set E<VAR>hs : s.Countable<VAR>B : Basis ↑(Basis.ofVectorSpaceIndex ℝ E) ℝ E<VAR>I1 : ∀ᵐ (x : E) ∂μ, ∀ v ∈ s, lineDeriv ℝ f x (∑ i : ↑(Basis.ofVectorSpaceIndex ℝ E), (B.repr v) i • B i) = ∑ i : ↑(Basis.ofVectorSpaceIndex ℝ E), (B.repr v) i • lineDeriv ℝ f x (B i)<VAR>I2 : ∀ᵐ (x : E) ∂μ, ∀ v ∈ s, LineDifferentiableAt ℝ f x v<VAR>x : E<VAR>hx : ∀ v ∈ s, lineDeriv ℝ f x (∑ i : ↑(Basis.ofVectorSpaceIndex ℝ E), (B.repr v) i • B i) = ∑ i : ↑(Basis.ofVectorSpaceIndex ℝ E), (B.repr v) i • lineDeriv ℝ f x (B i)<VAR>h'x : ∀ v ∈ s, LineDifferentiableAt ℝ f x v<VAR>L : E →L[ℝ] ℝ := LinearMap.toContinuousLinearMap ((B.constr ℝ) fun i => lineDeriv ℝ f x (B i))<VAR>v : E<VAR>hv : v ∈ s<VAR>J : L v = lineDeriv ℝ f x v<GOAL>HasLineDerivAt ℝ f (L v) x v
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>A : Type u_3<VAR>T : Type u_4<VAR>B : Type u_5<VAR>ι : Type u_6<VAR>inst✝¹¹ : SemilatticeSup B<VAR>inst✝¹⁰ : OrderBot B<VAR>inst✝⁹ : SemilatticeInf T<VAR>inst✝⁸ : OrderTop T<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : AddMonoid A<VAR>inst✝⁵ : AddMonoid B<VAR>inst✝⁴ : CovariantClass B B (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝³ : CovariantClass B B (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝² : AddMonoid T<VAR>inst✝¹ : CovariantClass T T (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝ : CovariantClass T T (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>degb : A → B<VAR>degt : A → T<VAR>degt0 : 0 ≤ degt 0<VAR>degtm : ∀ (a b : A), degt a + degt b ≤ degt (a + b)<VAR>n : ℕ<VAR>f : R[A]<GOAL>n • f.support.inf degt ≤ (f ^ n).support.inf degt
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>A : Type u_3<VAR>T : Type u_4<VAR>B : Type u_5<VAR>ι : Type u_6<VAR>inst✝¹¹ : SemilatticeSup B<VAR>inst✝¹⁰ : OrderBot B<VAR>inst✝⁹ : SemilatticeInf T<VAR>inst✝⁸ : OrderTop T<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : AddMonoid A<VAR>inst✝⁵ : AddMonoid B<VAR>inst✝⁴ : CovariantClass B B (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝³ : CovariantClass B B (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝² : AddMonoid T<VAR>inst✝¹ : CovariantClass T T (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝ : CovariantClass T T (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>degb : A → B<VAR>degt : A → T<VAR>degt0 : 0 ≤ degt 0<VAR>degtm : ∀ (a b : A), degt a + degt b ≤ degt (a + b)<VAR>n : ℕ<VAR>f : R[A]<GOAL>OrderDual.ofDual (degt 0) ≤ OrderDual.ofDual 0
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>A : Type u_3<VAR>T : Type u_4<VAR>B : Type u_5<VAR>ι : Type u_6<VAR>inst✝¹¹ : SemilatticeSup B<VAR>inst✝¹⁰ : OrderBot B<VAR>inst✝⁹ : SemilatticeInf T<VAR>inst✝⁸ : OrderTop T<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : AddMonoid A<VAR>inst✝⁵ : AddMonoid B<VAR>inst✝⁴ : CovariantClass B B (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝³ : CovariantClass B B (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝² : AddMonoid T<VAR>inst✝¹ : CovariantClass T T (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝ : CovariantClass T T (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>degb : A → B<VAR>degt : A → T<VAR>degt0 : 0 ≤ degt 0<VAR>degtm : ∀ (a b : A), degt a + degt b ≤ degt (a + b)<VAR>n : ℕ<VAR>f : R[A]<VAR>a b : A<GOAL>OrderDual.ofDual (degt (a + b)) ≤ OrderDual.ofDual (degt a + degt b)
<VAR>f g : ℂ → ℂ<VAR>s : Set ℂ<VAR>f' g' x c : ℂ<VAR>hf : HasDerivWithinAt f f' s x<VAR>hg : HasDerivWithinAt g g' s x<VAR>h0 : f x ∈ slitPlane<GOAL>HasDerivWithinAt (fun x => f x ^ g x) (g x * f x ^ (g x - 1) * f' + f x ^ g x * Complex.log (f x) * g') s x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁴ : TopologicalSpace 𝕜<VAR>inst✝³ : LinearOrderedRing 𝕜<VAR>inst✝² : AddCommMonoid E<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : Module 𝕜 E<VAR>A B C : Set E<VAR>hAB : IsExposed 𝕜 A B<VAR>hA : Convex 𝕜 A<GOAL>Convex 𝕜 B
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁴ : TopologicalSpace 𝕜<VAR>inst✝³ : LinearOrderedRing 𝕜<VAR>inst✝² : AddCommMonoid E<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : Module 𝕜 E<VAR>A C : Set E<VAR>hA : Convex 𝕜 A<VAR>hAB : IsExposed 𝕜 A ∅<GOAL>Convex 𝕜 ∅
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁴ : TopologicalSpace 𝕜<VAR>inst✝³ : LinearOrderedRing 𝕜<VAR>inst✝² : AddCommMonoid E<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : Module 𝕜 E<VAR>A B C : Set E<VAR>hAB : IsExposed 𝕜 A B<VAR>hA : Convex 𝕜 A<VAR>hB : B.Nonempty<GOAL>Convex 𝕜 B
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁴ : TopologicalSpace 𝕜<VAR>inst✝³ : LinearOrderedRing 𝕜<VAR>inst✝² : AddCommMonoid E<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : Module 𝕜 E<VAR>A C : Set E<VAR>hA : Convex 𝕜 A<VAR>l : E →L[𝕜] 𝕜<VAR>hAB : IsExposed 𝕜 A {x | x ∈ A ∧ ∀ y ∈ A, l y ≤ l x}<VAR>hB : {x | x ∈ A ∧ ∀ y ∈ A, l y ≤ l x}.Nonempty<GOAL>Convex 𝕜 {x | x ∈ A ∧ ∀ y ∈ A, l y ≤ l x}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : Preorder α<VAR>l₁ l₁' l₂ l₂' : Filter α<VAR>Ixx : α → α → Set α<VAR>h : TendstoIxxClass Ixx l₁ l₂<VAR>h' : TendstoIxxClass Ixx l₁' l₂'<GOAL>Tendsto (fun p => Ixx p.1 p.2) ((l₁ ⊓ l₁') ×ˢ (l₁ ⊓ l₁')) (l₂ ⊓ l₂').smallSets
<VAR>α : Type u_1<VAR>M₀ : Type u_2<VAR>G₀ : Type u_3<VAR>M₀' : Type u_4<VAR>G₀' : Type u_5<VAR>F : Type u_6<VAR>F' : Type u_7<VAR>inst✝ : GroupWithZero G₀<VAR>a✝ x✝ y✝ x' y' a x y : G₀<VAR>h : SemiconjBy a x y<VAR>n : ℕ<GOAL>SemiconjBy a (x ^ ↑n) (y ^ ↑n)
<VAR>α : Type u_1<VAR>M₀ : Type u_2<VAR>G₀ : Type u_3<VAR>M₀' : Type u_4<VAR>G₀' : Type u_5<VAR>F : Type u_6<VAR>F' : Type u_7<VAR>inst✝ : GroupWithZero G₀<VAR>a✝ x✝ y✝ x' y' a x y : G₀<VAR>h : SemiconjBy a x y<VAR>n : ℕ<GOAL>SemiconjBy a (x ^ Int.negSucc n) (y ^ Int.negSucc n)
<VAR>o : Ordinal.{u_1}<VAR>ho : o.IsLimit<GOAL>aleph o = ⨆ a, aleph ↑a
<VAR>o : Ordinal.{u_1}<VAR>ho : o.IsLimit<GOAL>aleph o ≤ ⨆ i, aleph ↑i
<VAR>o : Ordinal.{u_1}<VAR>ho : o.IsLimit<GOAL>∀ (i : ↑(Iio o)), aleph ↑i ≤ aleph o
<VAR>R : Type u<VAR>S : Type u_1<VAR>inst✝ : Semiring R<VAR>s : Set R[X]<VAR>p : R[X]<VAR>hs : s.Nonempty<VAR>hp : p ∈ Submodule.span R s<GOAL>∃ p' ∈ s, p.degree ≤ p'.degree
<VAR>R : Type u<VAR>S : Type u_1<VAR>inst✝ : Semiring R<VAR>s : Set R[X]<VAR>p : R[X]<VAR>hs : s.Nonempty<VAR>hp : p ∈ Submodule.span R s<VAR>h : ∀ p' ∈ s, p'.degree < p.degree<GOAL>False
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>inst✝³ : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M✝ : Bimod A B<VAR>inst✝² : HasCoequalizers C<VAR>inst✝¹ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)<VAR>inst✝ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)<VAR>X Y : Mon_ C<VAR>M N : Bimod X Y<VAR>f : M ⟶ N<GOAL>(whiskerRight f { X := Y.X, actLeft := Y.mul, one_actLeft := ⋯, left_assoc := ⋯, actRight := Y.mul, actRight_one := ⋯, right_assoc := ⋯, middle_assoc := ⋯ }).hom = ((isoOfIso { hom := RightUnitorBimod.hom M, inv := RightUnitorBimod.inv M, hom_inv_id := ⋯, inv_hom_id := ⋯ } ⋯ ⋯).hom ≫ f ≫ (isoOfIso { hom := RightUnitorBimod.hom N, inv := RightUnitorBimod.inv N, hom_inv_id := ⋯, inv_hom_id := ⋯ } ⋯ ⋯).inv).hom