ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : DecidableEq β<VAR>r : α → β → Prop<VAR>inst✝ : (a : α) → Fintype ↑(Rel.image r {a})<VAR>r' : α → Finset β := fun a => (Rel.image r {a}).toFinset<VAR>h : ∀ (A : Finset α), card ↑(Rel.image r ↑A) = (A.biUnion r').card<VAR>h' : ∀ (f : α → β) (x : α), r x (f x) ↔ f x ∈ r' x<GOAL>(∀ (A : Finset α), A.card ≤ (A.biUnion r').card) ↔ ∃ f, Function.Injective f ∧ ∀ (x : α), f x ∈ r' x
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>ε : Type u_6<VAR>inst✝ : Monoid α<VAR>f g : Filter α<VAR>s : Set α<VAR>a : α<VAR>m n : ℕ<VAR>hs : s ∈ f<GOAL>s ^ 0 ∈ f ^ 0
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>ε : Type u_6<VAR>inst✝ : Monoid α<VAR>f g : Filter α<VAR>s : Set α<VAR>a : α<VAR>m n : ℕ<VAR>hs : s ∈ f<GOAL>1 ∈ f ^ 0
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>ε : Type u_6<VAR>inst✝ : Monoid α<VAR>f g : Filter α<VAR>s : Set α<VAR>a : α<VAR>m n✝ : ℕ<VAR>hs : s ∈ f<VAR>n : ℕ<GOAL>s ^ (n + 1) ∈ f ^ (n + 1)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>ε : Type u_6<VAR>inst✝ : Monoid α<VAR>f g : Filter α<VAR>s : Set α<VAR>a : α<VAR>m n✝ : ℕ<VAR>hs : s ∈ f<VAR>n : ℕ<GOAL>s ^ n * s ∈ f ^ (n + 1)
<VAR>X : Type u<VAR>Y : Type v<VAR>inst✝⁵ : MetricSpace X<VAR>inst✝⁴ : CompactSpace X<VAR>inst✝³ : Nonempty X<VAR>inst✝² : MetricSpace Y<VAR>inst✝¹ : CompactSpace Y<VAR>inst✝ : Nonempty Y<VAR>f✝ : GromovHausdorff.ProdSpaceFun X Y<VAR>x y z t : X ⊕ Y<VAR>f g : GromovHausdorff.Cb X Y<GOAL>⨆ y, ⨅ x, f (inl x, inr y) ≤ (⨆ y, ⨅ x, g (inl x, inr y)) + dist f g
<VAR>X : Type u<VAR>Y : Type v<VAR>inst✝⁵ : MetricSpace X<VAR>inst✝⁴ : CompactSpace X<VAR>inst✝³ : Nonempty X<VAR>inst✝² : MetricSpace Y<VAR>inst✝¹ : CompactSpace Y<VAR>inst✝ : Nonempty Y<VAR>f✝ : GromovHausdorff.ProdSpaceFun X Y<VAR>x y z t : X ⊕ Y<VAR>f g : GromovHausdorff.Cb X Y<VAR>cg : ℝ<VAR>hcg : cg ∈ lowerBounds (range ⇑g)<GOAL>⨆ y, ⨅ x, f (inl x, inr y) ≤ (⨆ y, ⨅ x, g (inl x, inr y)) + dist f g
<VAR>X : Type u<VAR>Y : Type v<VAR>inst✝⁵ : MetricSpace X<VAR>inst✝⁴ : CompactSpace X<VAR>inst✝³ : Nonempty X<VAR>inst✝² : MetricSpace Y<VAR>inst✝¹ : CompactSpace Y<VAR>inst✝ : Nonempty Y<VAR>f✝ : GromovHausdorff.ProdSpaceFun X Y<VAR>x y z t : X ⊕ Y<VAR>f g : GromovHausdorff.Cb X Y<VAR>cg : ℝ<VAR>hcg : cg ∈ lowerBounds (range ⇑g)<VAR>Hcg : ∀ (x : (X ⊕ Y) × (X ⊕ Y)), cg ≤ g x<GOAL>⨆ y, ⨅ x, f (inl x, inr y) ≤ (⨆ y, ⨅ x, g (inl x, inr y)) + dist f g
<VAR>X : Type u<VAR>Y : Type v<VAR>inst✝⁵ : MetricSpace X<VAR>inst✝⁴ : CompactSpace X<VAR>inst✝³ : Nonempty X<VAR>inst✝² : MetricSpace Y<VAR>inst✝¹ : CompactSpace Y<VAR>inst✝ : Nonempty Y<VAR>f✝ : GromovHausdorff.ProdSpaceFun X Y<VAR>x y z t : X ⊕ Y<VAR>f g : GromovHausdorff.Cb X Y<VAR>cg : ℝ<VAR>hcg : cg ∈ lowerBounds (range ⇑g)<VAR>Hcg : ∀ (x : (X ⊕ Y) × (X ⊕ Y)), cg ≤ g x<VAR>cf : ℝ<VAR>hcf : cf ∈ lowerBounds (range ⇑f)<GOAL>⨆ y, ⨅ x, f (inl x, inr y) ≤ (⨆ y, ⨅ x, g (inl x, inr y)) + dist f g
<VAR>X : Type u<VAR>Y : Type v<VAR>inst✝⁵ : MetricSpace X<VAR>inst✝⁴ : CompactSpace X<VAR>inst✝³ : Nonempty X<VAR>inst✝² : MetricSpace Y<VAR>inst✝¹ : CompactSpace Y<VAR>inst✝ : Nonempty Y<VAR>f✝ : GromovHausdorff.ProdSpaceFun X Y<VAR>x y z t : X ⊕ Y<VAR>f g : GromovHausdorff.Cb X Y<VAR>cg : ℝ<VAR>hcg : cg ∈ lowerBounds (range ⇑g)<VAR>Hcg : ∀ (x : (X ⊕ Y) × (X ⊕ Y)), cg ≤ g x<VAR>cf : ℝ<VAR>hcf : cf ∈ lowerBounds (range ⇑f)<VAR>Hcf : ∀ (x : (X ⊕ Y) × (X ⊕ Y)), cf ≤ f x<GOAL>⨆ y, ⨅ x, f (inl x, inr y) ≤ (⨆ y, ⨅ x, g (inl x, inr y)) + dist f g
<VAR>X : Type u<VAR>Y : Type v<VAR>inst✝⁵ : MetricSpace X<VAR>inst✝⁴ : CompactSpace X<VAR>inst✝³ : Nonempty X<VAR>inst✝² : MetricSpace Y<VAR>inst✝¹ : CompactSpace Y<VAR>inst✝ : Nonempty Y<VAR>f✝ : GromovHausdorff.ProdSpaceFun X Y<VAR>x y z t : X ⊕ Y<VAR>f g : GromovHausdorff.Cb X Y<VAR>cg : ℝ<VAR>hcg : cg ∈ lowerBounds (range ⇑g)<VAR>Hcg : ∀ (x : (X ⊕ Y) × (X ⊕ Y)), cg ≤ g x<VAR>cf : ℝ<VAR>hcf : cf ∈ lowerBounds (range ⇑f)<VAR>Hcf : ∀ (x : (X ⊕ Y) × (X ⊕ Y)), cf ≤ f x<VAR>Z : ⨆ y, ⨅ x, f (inl x, inr y) ≤ ⨆ y, ⨅ x, g (inl x, inr y) + dist f g<GOAL>⨆ y, ⨅ x, f (inl x, inr y) ≤ (⨆ y, ⨅ x, g (inl x, inr y)) + dist f g
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>inst✝¹ : Fintype F<VAR>inst✝ : DecidableEq F<VAR>hF : ringChar F ≠ 2<VAR>a : F<VAR>ha : a ≠ 0<GOAL>quadraticCharFun F a = if a ^ (Fintype.card F / 2) = 1 then 1 else -1
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>inst✝¹ : Fintype F<VAR>inst✝ : DecidableEq F<VAR>hF : ringChar F ≠ 2<VAR>a : F<VAR>ha : a ≠ 0<GOAL>(if IsSquare a then 1 else -1) = if a ^ (Fintype.card F / 2) = 1 then 1 else -1
<VAR>J : Type v<VAR>inst✝ : SmallCategory J<VAR>F : J ⥤ RingCat<VAR>j j' : J<VAR>f : j ⟶ j'<VAR>x : ↑(F.obj j)<GOAL>(coconeMorphism F j') ((F.map f) x) = (coconeMorphism F j) x
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>A : Type u_3<VAR>K : Type u_4<VAR>inst✝³ : Semiring S<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Field K<VAR>p : S[X]<VAR>f : S →+* R<VAR>r : R<VAR>s : S<VAR>hr : eval₂ f r p = 0<GOAL>eval₂ f (f s * r) (p.scaleRoots s) = 0
<VAR>z : ℂ<GOAL>HasSum (fun n => (-1) ^ n * z ^ (2 * n) / ↑(2 * n)!) (cos z)
<VAR>z : ℂ<GOAL>(fun n => (-1) ^ n * z ^ (2 * n) / ↑(2 * n)!) = fun n => (z * I) ^ (2 * n) / ↑(2 * n)!
<VAR>α : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>o : Ordinal.{u_3}<GOAL>0 < o.card ↔ 0 < o
<VAR>ι : Type u<VAR>s : Finset ι<VAR>w z : ι → ℝ≥0∞<VAR>hw' : ∑ i ∈ s, w i = 1<VAR>p : ℝ<VAR>hp : 1 ≤ p<VAR>hp_pos : 0 < p<VAR>hp_nonneg : 0 ≤ p<VAR>hp_not_neg : ¬p < 0<GOAL>(∑ i ∈ s, w i * z i) ^ p ≤ ∑ i ∈ s, w i * z i ^ p
<VAR>ι : Type u<VAR>s : Finset ι<VAR>w z : ι → ℝ≥0∞<VAR>hw' : ∑ i ∈ s, w i = 1<VAR>p : ℝ<VAR>hp : 1 ≤ p<VAR>hp_pos : 0 < p<VAR>hp_nonneg : 0 ≤ p<VAR>hp_not_neg : ¬p < 0<VAR>h_top_iff_rpow_top : ∀ i ∈ s, w i * z i = ⊤ ↔ w i * z i ^ p = ⊤<GOAL>(∑ i ∈ s, w i * z i) ^ p ≤ ∑ i ∈ s, w i * z i ^ p
<VAR>ι : Type u<VAR>s : Finset ι<VAR>w z : ι → ℝ≥0∞<VAR>hw' : ∑ i ∈ s, w i = 1<VAR>p : ℝ<VAR>hp : 1 ≤ p<VAR>hp_pos : 0 < p<VAR>hp_nonneg : 0 ≤ p<VAR>hp_not_neg : ¬p < 0<VAR>h_top_iff_rpow_top : ∀ i ∈ s, w i * z i = ⊤ ↔ w i * z i ^ p = ⊤<GOAL>(∑ i ∈ s, w i * z i) ^ p = ⊤ → ∑ i ∈ s, w i * z i ^ p = ⊤
<VAR>ι : Type u<VAR>s : Finset ι<VAR>w z : ι → ℝ≥0∞<VAR>hw' : ∑ i ∈ s, w i = 1<VAR>p : ℝ<VAR>hp : 1 ≤ p<VAR>hp_pos : 0 < p<VAR>hp_nonneg : 0 ≤ p<VAR>hp_not_neg : ¬p < 0<VAR>h_top_iff_rpow_top : ∀ i ∈ s, w i * z i = ⊤ ↔ w i * z i ^ p = ⊤<GOAL>(∑ i ∈ s, w i * z i) ^ p ≠ ⊤ → ∑ i ∈ s, w i * z i ^ p ≠ ⊤ → ((∑ i ∈ s, w i * z i) ^ p).toNNReal ≤ (∑ i ∈ s, w i * z i ^ p).toNNReal
<VAR>f g : 𝓢(ℝ, ℂ)<VAR>hfg : 𝓕 ⇑f = ⇑g<VAR>x : ℝ<GOAL>∑' (n : ℤ), f (x + ↑n) = ∑' (n : ℤ), g ↑n * (fourier n) ↑x
<VAR>α β : Type u<VAR>a b : Cardinal.{u_1}<VAR>hb : 1 ≤ b<GOAL>a ≤ a ^ b
<VAR>α β : Type u<VAR>b : Cardinal.{u_1}<VAR>hb : 1 ≤ b<GOAL>0 ≤ 0 ^ b
<VAR>α β : Type u<VAR>a b : Cardinal.{u_1}<VAR>hb : 1 ≤ b<VAR>ha : a ≠ 0<GOAL>a ≤ a ^ b
<VAR>α : Type u<VAR>β✝ : Type u_1<VAR>t : TopologicalSpace α<VAR>B✝ : Set (Set α)<VAR>s : Set α<VAR>β : Type u_2<VAR>inst✝ : TopologicalSpace β<VAR>B : Set (Set β)<VAR>hB : IsTopologicalBasis B<VAR>f : α → β<GOAL>Continuous f ↔ ∀ s ∈ B, IsOpen (f ⁻¹' s)
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t : Set X<VAR>f : X → Y<VAR>hf : Inducing f<VAR>hf' : IsClosed (range f)<VAR>K : Set Y<VAR>hK : IsCompact K<GOAL>IsCompact (f ⁻¹' K)
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t : Set X<VAR>f : X → Y<VAR>hf : Inducing f<VAR>hf' : IsClosed (range f)<VAR>K : Set Y<VAR>hK : IsCompact (K ∩ range f)<GOAL>IsCompact (f ⁻¹' K)
<VAR>a b c d m n✝ k : ℕ<VAR>p q : ℕ → Prop<VAR>inst✝² : DecidablePred p<VAR>H : ∃ n, p n<VAR>inst✝¹ : DecidablePred p<VAR>inst✝ : DecidablePred q<VAR>h : ∃ n, p n<VAR>n : ℕ<GOAL>n < Nat.find h ↔ ∀ (m : ℕ), m ≤ n → ¬p m
<VAR>a r : ℝ<VAR>ha : 0 < a<VAR>hr : 0 < r<GOAL>(gammaMeasure a r) univ = 1
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>R I J X Y : Set α<VAR>N : Matroid α<VAR>h : N ≤r M<VAR>hne : N.E ≠ M.E<GOAL>N <r M
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>R I J X Y : Set α<VAR>N : Matroid α<VAR>h : N ≤r M<VAR>hne : N.E ≠ M.E<GOAL>M ↾ N.E <r M
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : EDist α<VAR>x y : α<VAR>s : Set α<VAR>hs : 0 < s.infsep<GOAL>s.Nontrivial
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : EDist α<VAR>x y : α<VAR>s : Set α<VAR>hs : ¬s.Nontrivial<GOAL>¬0 < s.infsep
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : EDist α<VAR>x y : α<VAR>s : Set α<VAR>hs : s.Subsingleton<GOAL>¬0 < s.infsep
<VAR>R✝ : Type u<VAR>S : Type v<VAR>a b : R✝<VAR>m n✝ : ℕ<VAR>ι : Type y<VAR>inst✝² : Ring R✝<VAR>p : R✝[X]<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : Nontrivial R<VAR>n : ℕ<VAR>h : IsUnit (X ^ n - 1)<GOAL>False
<VAR>R✝ : Type u<VAR>S : Type v<VAR>a b : R✝<VAR>m n : ℕ<VAR>ι : Type y<VAR>inst✝² : Ring R✝<VAR>p : R✝[X]<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : Nontrivial R<VAR>h : IsUnit (X ^ 0 - 1)<GOAL>False
<VAR>R✝ : Type u<VAR>S : Type v<VAR>a b : R✝<VAR>m n✝ : ℕ<VAR>ι : Type y<VAR>inst✝² : Ring R✝<VAR>p : R✝[X]<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : Nontrivial R<VAR>n : ℕ<VAR>h : IsUnit (X ^ n - 1)<VAR>hn : n ≠ 0<GOAL>False
<VAR>R✝ : Type u<VAR>S : Type v<VAR>a b : R✝<VAR>m n✝ : ℕ<VAR>ι : Type y<VAR>inst✝² : Ring R✝<VAR>p : R✝[X]<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : Nontrivial R<VAR>n : ℕ<VAR>h : IsUnit (X ^ n - 1)<VAR>hn : n ≠ 0<GOAL>n = 0
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>hs : UniqueDiffWithinAt 𝕜 s x<VAR>h : DifferentiableAt 𝕜 f x<GOAL>fderivWithin 𝕜 f s x = fderiv 𝕜 f x
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>hs : UniqueDiffWithinAt 𝕜 s x<VAR>h : DifferentiableAt 𝕜 f x<GOAL>fderivWithin 𝕜 f s x = fderivWithin 𝕜 f univ x
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Sort w<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : X<VAR>s s₁ s₂ t : Set X<VAR>p p₁ p₂ : X → Prop<VAR>inst✝ : TopologicalSpace X<GOAL>x ∈ closure s ↔ ∀ t ∈ 𝓝 x, ∃ y, ↑y ∈ t
<VAR>b : ℕ<VAR>hb : b ≤ 1<VAR>n : ℕ<GOAL>clog b 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>g : P ≃ₗ[R] Q<VAR>f : N ≃ₗ[R] P<VAR>m : M<VAR>n : N<VAR>p : P<VAR>x : M ⊗[R] N<VAR>y : N ⊗[R] M<GOAL>(lTensor M (refl R N)) x = x
<VAR>C : Type u₁<VAR>inst✝ : Category.{v₁, u₁} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>hf : ∀ (T : C), Function.Bijective fun x => x ≫ f<GOAL>IsIso f
<VAR>C : Type u₁<VAR>inst✝ : Category.{v₁, u₁} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>hf : ∀ (T : C), Function.Bijective fun x => x ≫ f<VAR>g : Y ⟶ X<VAR>hg : g ≫ f = 𝟙 Y<GOAL>IsIso f
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>H : Type u_6<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>inst✝¹ : NormedAddCommGroup H<VAR>inst✝ : NormedSpace 𝕜 H<VAR>f : E → F<VAR>s : Set E<VAR>x : E<VAR>h : {x} ∈ 𝓝[s] x<GOAL>AnalyticWithinAt 𝕜 f s x
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>H : Type u_6<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>inst✝¹ : NormedAddCommGroup H<VAR>inst✝ : NormedSpace 𝕜 H<VAR>f : E → F<VAR>s : Set E<VAR>x : E<VAR>h : {x} ∈ 𝓝[s] x<VAR>fc : ContinuousWithinAt f s x<GOAL>AnalyticWithinAt 𝕜 f s x
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>H : Type u_6<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>inst✝¹ : NormedAddCommGroup H<VAR>inst✝ : NormedSpace 𝕜 H<VAR>f : E → F<VAR>s : Set E<VAR>x : E<VAR>h : {x} ∈ 𝓝[s] x<VAR>fc : ContinuousWithinAt f s x<VAR>t : Set E<VAR>ot : IsOpen t<VAR>xt : x ∈ t<VAR>st : t ∩ s ⊆ {x}<GOAL>AnalyticWithinAt 𝕜 f s x
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>H : Type u_6<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>inst✝¹ : NormedAddCommGroup H<VAR>inst✝ : NormedSpace 𝕜 H<VAR>f : E → F<VAR>s : Set E<VAR>x : E<VAR>h : {x} ∈ 𝓝[s] x<VAR>fc : ContinuousWithinAt f s x<VAR>t : Set E<VAR>ot : IsOpen t<VAR>xt : x ∈ t<VAR>st : t ∩ s ⊆ {x}<VAR>r : ℝ<VAR>r0 : r > 0<VAR>rt : Metric.ball x r ⊆ t<GOAL>AnalyticWithinAt 𝕜 f s x
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>inst✝ : Semiring R<VAR>φ : MvPowerSeries σ R<VAR>s : σ<VAR>this : ¬single s 1 ≤ 0<GOAL>(coeff R 0) (φ * X s) = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : LinearOrderedField α<VAR>inst✝¹ : Ring β<VAR>abv : β → α<VAR>inst✝ : IsAbsoluteValue abv<VAR>f1 f2 g1 g2 : CauSeq β abv<VAR>hf : f1 ≈ f2<VAR>hg : g1 ≈ g2<GOAL>(f1 * g1 - f2 * g2).LimZero
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : LinearOrderedField α<VAR>inst✝¹ : Ring β<VAR>abv : β → α<VAR>inst✝ : IsAbsoluteValue abv<VAR>f1 f2 g1 g2 : CauSeq β abv<VAR>hf : f1 ≈ f2<VAR>hg : g1 ≈ g2<GOAL>f1 * g1 - f2 * g2 = (f1 - f2) * g1 + f2 * (g1 - g2)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : LinearOrderedField α<VAR>inst✝¹ : Ring β<VAR>abv : β → α<VAR>inst✝ : IsAbsoluteValue abv<VAR>f1 f2 g1 g2 : CauSeq β abv<VAR>hf : f1 ≈ f2<VAR>hg : g1 ≈ g2<GOAL>f1 * g1 - f2 * g2 = f1 * g1 - f2 * g1 + (f2 * g1 - f2 * g2)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>π : ι → Type u_4<VAR>inst✝ : GeneralizedCoheytingAlgebra α<VAR>a b c d : α<GOAL>a ∆ ⊥ = a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n d k N : ℕ<VAR>x : Fin n → ℕ<VAR>hN : 64 ≤ N<GOAL>3 ≤ nValue N
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n d k N : ℕ<VAR>x : Fin n → ℕ<VAR>hN : 64 ≤ N<GOAL>2 < √(log ↑N)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n d k N : ℕ<VAR>x : Fin n → ℕ<VAR>hN : 64 ≤ N<GOAL>2 ^ 2 < log ↑N
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n d k N : ℕ<VAR>x : Fin n → ℕ<VAR>hN : 64 ≤ N<VAR>this : 2 ^ ↑6 ≤ ↑N<GOAL>2 ^ 2 < log ↑N
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n d k N : ℕ<VAR>x : Fin n → ℕ<VAR>hN : 64 ≤ N<VAR>this : 2 ^ ↑6 ≤ ↑N<GOAL>2 ^ 2 < log (2 ^ ↑6)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n d k N : ℕ<VAR>x : Fin n → ℕ<VAR>hN : 64 ≤ N<VAR>this : 2 ^ ↑6 ≤ ↑N<GOAL>2 ^ 2 / ↑6 < log 2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n d k N : ℕ<VAR>x : Fin n → ℕ<VAR>hN : 64 ≤ N<VAR>this : 2 ^ ↑6 ≤ ↑N<GOAL>0 < ↑6
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>R : Type u_4<VAR>inst✝¹ : Monoid α<VAR>inst✝ : HasDistribNeg α<VAR>n : ℕ<VAR>a : α<VAR>h : Even n<GOAL>(-1) ^ n = 1
<VAR>α : Type u<VAR>b : Ultrafilter α<GOAL>comap pure (𝓝 b) ≤ ↑b
<VAR>α : Type u<VAR>b : Ultrafilter α<GOAL>comap pure (⨅ s ∈ {s | b ∈ s ∧ s ∈ ultrafilterBasis α}, 𝓟 s) ≤ ↑b
<VAR>α : Type u<VAR>b : Ultrafilter α<GOAL>⨅ i ∈ {s | b ∈ s ∧ s ∈ ultrafilterBasis α}, 𝓟 (pure ⁻¹' i) ≤ ↑b
<VAR>α : Type u<VAR>b : Ultrafilter α<VAR>s : Set α<VAR>hs : s ∈ ↑b<GOAL>s ∈ ⨅ i ∈ {s | b ∈ s ∧ s ∈ ultrafilterBasis α}, 𝓟 (pure ⁻¹' i)
<VAR>α : Type u<VAR>b : Ultrafilter α<VAR>s : Set α<VAR>hs : s ∈ ↑b<GOAL>⨅ i ∈ {s | b ∈ s ∧ s ∈ ultrafilterBasis α}, 𝓟 (pure ⁻¹' i) ≤ 𝓟 s
<VAR>α : Type u<VAR>b : Ultrafilter α<VAR>s : Set α<VAR>hs : s ∈ ↑b<GOAL>⨅ (_ : {u | s ∈ u} ∈ {s | b ∈ s ∧ s ∈ ultrafilterBasis α}), 𝓟 (pure ⁻¹' {u | s ∈ u}) ≤ 𝓟 s
<VAR>α : Type u<VAR>b : Ultrafilter α<VAR>s : Set α<VAR>hs : s ∈ ↑b<GOAL>𝓟 (pure ⁻¹' {u | s ∈ u}) ≤ 𝓟 s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrderedField α<VAR>a₁ b₁ a₂ b₂ : CauSeq α abs<VAR>ha : a₁ ≈ a₂<VAR>hb : b₁ ≈ b₂<VAR>ε : α<VAR>ε0 : ε > 0<VAR>ai : ℕ<VAR>hai : ∀ j ≥ ai, |↑(a₁ - a₂) j| < ε<VAR>bi : ℕ<VAR>hbi : ∀ j ≥ bi, |↑(b₁ - b₂) j| < ε<GOAL>∃ i, ∀ j ≥ i, |↑(a₁ ⊔ b₁ - a₂ ⊔ b₂) j| < ε
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>p q : α → Prop<VAR>l✝ : List α<VAR>h : ∀ (x : α), p x → q x<VAR>x : α<VAR>l : List α<GOAL>Forall p (x :: l) → Forall q (x :: l)
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>p q : α → Prop<VAR>l✝ : List α<VAR>h : ∀ (x : α), p x → q x<VAR>x : α<VAR>l : List α<GOAL>p x → Forall p l → q x ∧ Forall q l
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>p q : α → Prop<VAR>l✝ : List α<VAR>h : ∀ (x : α), p x → q x<VAR>x : α<VAR>l : List α<GOAL>p x ∧ Forall p l → q x ∧ Forall q l
<VAR>n : ℕ<GOAL>(hermite n).degree = ↑n
<VAR>n : ℕ<GOAL>(hermite n).degree ≤ ↑n
<VAR>n : ℕ<GOAL>(hermite n).coeff n ≠ 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>K : Type u_3<VAR>inst✝ : DivisionRing K<VAR>a✝ b c d a : K<VAR>h : a ≠ 0<GOAL>-a / a = -1
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁵ : _root_.RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : InnerProductSpace ℝ F<VAR>K : Submodule 𝕜 E<VAR>inst✝ : HasOrthogonalProjection K<VAR>x✝ : E<GOAL>(reflection Kᗮ) x✝ = ((reflection K).trans (LinearIsometryEquiv.neg 𝕜)) x✝
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoEMetricSpace α<VAR>inst✝ : PseudoEMetricSpace β<VAR>x y : α<VAR>s t : Set α<VAR>Φ : α → β<VAR>d : ℝ≥0∞<GOAL>d ≤ infEdist x s ↔ ∀ y ∈ s, d ≤ edist x y
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>E'' : Type uE''<VAR>F : Type uF<VAR>F' : Type uF'<VAR>F'' : Type uF''<VAR>P : Type uP<VAR>inst✝¹⁵ : NormedAddCommGroup E<VAR>inst✝¹⁴ : NormedAddCommGroup E'<VAR>inst✝¹³ : NormedAddCommGroup E''<VAR>inst✝¹² : NormedAddCommGroup F<VAR>f f' : G → E<VAR>g g' : G → E'<VAR>x x' : G<VAR>y y' : E<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁰ : NormedSpace 𝕜 E<VAR>inst✝⁹ : NormedSpace 𝕜 E'<VAR>inst✝⁸ : NormedSpace 𝕜 E''<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>inst✝⁶ : MeasurableSpace G<VAR>μ ν : Measure G<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>inst✝⁴ : AddGroup G<VAR>inst✝³ : TopologicalSpace G<VAR>inst✝² : TopologicalAddGroup G<VAR>inst✝¹ : BorelSpace G<VAR>inst✝ : TopologicalSpace P<VAR>hcg : HasCompactSupport g<VAR>hf : LocallyIntegrable f μ<VAR>hg : Continuous g<GOAL>Continuous (f ⋆[L, μ] g)
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>E'' : Type uE''<VAR>F : Type uF<VAR>F' : Type uF'<VAR>F'' : Type uF''<VAR>P : Type uP<VAR>inst✝¹⁵ : NormedAddCommGroup E<VAR>inst✝¹⁴ : NormedAddCommGroup E'<VAR>inst✝¹³ : NormedAddCommGroup E''<VAR>inst✝¹² : NormedAddCommGroup F<VAR>f f' : G → E<VAR>g g' : G → E'<VAR>x x' : G<VAR>y y' : E<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁰ : NormedSpace 𝕜 E<VAR>inst✝⁹ : NormedSpace 𝕜 E'<VAR>inst✝⁸ : NormedSpace 𝕜 E''<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>inst✝⁶ : MeasurableSpace G<VAR>μ ν : Measure G<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>inst✝⁴ : AddGroup G<VAR>inst✝³ : TopologicalSpace G<VAR>inst✝² : TopologicalAddGroup G<VAR>inst✝¹ : BorelSpace G<VAR>inst✝ : TopologicalSpace P<VAR>hcg : HasCompactSupport g<VAR>hf : LocallyIntegrable f μ<VAR>hg : Continuous g<GOAL>ContinuousOn (f ⋆[L, μ] g) univ
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>E'' : Type uE''<VAR>F : Type uF<VAR>F' : Type uF'<VAR>F'' : Type uF''<VAR>P : Type uP<VAR>inst✝¹⁵ : NormedAddCommGroup E<VAR>inst✝¹⁴ : NormedAddCommGroup E'<VAR>inst✝¹³ : NormedAddCommGroup E''<VAR>inst✝¹² : NormedAddCommGroup F<VAR>f f' : G → E<VAR>g g'✝ : G → E'<VAR>x x' : G<VAR>y y' : E<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁰ : NormedSpace 𝕜 E<VAR>inst✝⁹ : NormedSpace 𝕜 E'<VAR>inst✝⁸ : NormedSpace 𝕜 E''<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>inst✝⁶ : MeasurableSpace G<VAR>μ ν : Measure G<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>inst✝⁴ : AddGroup G<VAR>inst✝³ : TopologicalSpace G<VAR>inst✝² : TopologicalAddGroup G<VAR>inst✝¹ : BorelSpace G<VAR>inst✝ : TopologicalSpace P<VAR>hcg : HasCompactSupport g<VAR>hf : LocallyIntegrable f μ<VAR>hg : Continuous g<VAR>g' : G → G → E' := fun x q => g q<GOAL>ContinuousOn (f ⋆[L, μ] g) univ
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>E'' : Type uE''<VAR>F : Type uF<VAR>F' : Type uF'<VAR>F'' : Type uF''<VAR>P : Type uP<VAR>inst✝¹⁵ : NormedAddCommGroup E<VAR>inst✝¹⁴ : NormedAddCommGroup E'<VAR>inst✝¹³ : NormedAddCommGroup E''<VAR>inst✝¹² : NormedAddCommGroup F<VAR>f f' : G → E<VAR>g g'✝ : G → E'<VAR>x x' : G<VAR>y y' : E<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁰ : NormedSpace 𝕜 E<VAR>inst✝⁹ : NormedSpace 𝕜 E'<VAR>inst✝⁸ : NormedSpace 𝕜 E''<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>inst✝⁶ : MeasurableSpace G<VAR>μ ν : Measure G<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>inst✝⁴ : AddGroup G<VAR>inst✝³ : TopologicalSpace G<VAR>inst✝² : TopologicalAddGroup G<VAR>inst✝¹ : BorelSpace G<VAR>inst✝ : TopologicalSpace P<VAR>hcg : HasCompactSupport g<VAR>hf : LocallyIntegrable f μ<VAR>hg : Continuous g<VAR>g' : G → G → E' := fun x q => g q<VAR>this : ContinuousOn (↿g') (univ ×ˢ univ)<GOAL>ContinuousOn (f ⋆[L, μ] g) univ
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : DecidableEq β<VAR>𝒜 ℬ : Finset (Finset α)<VAR>s✝ t✝ : Finset α<VAR>a : α<VAR>s t u : Finset α<GOAL>u ∈ (s ∩ t).powerset ↔ u ∈ s.powerset ⊼ t.powerset
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : DecidableEq β<VAR>𝒜 ℬ : Finset (Finset α)<VAR>s✝ t✝ : Finset α<VAR>a : α<VAR>s t u : Finset α<GOAL>u ⊆ s ∩ t ↔ ∃ a ⊆ s, ∃ b ⊆ t, a ∩ b = u
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : DecidableEq β<VAR>𝒜 ℬ : Finset (Finset α)<VAR>s✝ t✝ : Finset α<VAR>a : α<VAR>s t u : Finset α<VAR>h : u ⊆ s ∩ t<GOAL>s ∩ u ∩ (t ∩ u) = u
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : DecidableEq β<VAR>𝒜 ℬ : Finset (Finset α)<VAR>s✝ t✝ : Finset α<VAR>a : α<VAR>s t u : Finset α<GOAL>(∃ a ⊆ s, ∃ b ⊆ t, a ∩ b = u) → u ⊆ s ∩ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Semiquot α<VAR>h : t.IsPure<VAR>st : s ≤ t<GOAL>t ≤ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Semiquot α<VAR>h : t.IsPure<VAR>st : s ≤ t<GOAL>pure (t.get h) ≤ pure (s.get ⋯)
<VAR>ι : Type u_1<VAR>E : Type u_2<VAR>μ : Measure ℝ<VAR>l : Filter ι<VAR>inst✝³ : l.IsCountablyGenerated<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>a b✝ : ι → ℝ<VAR>f : ℝ → E<VAR>b : ℝ<VAR>hfi : IntegrableOn f (Iic b) μ<VAR>ha : Tendsto a l atBot<VAR>φ : ι → Set ℝ := fun i => Ioi (a i)<GOAL>Tendsto (fun i => ∫ (x : ℝ) in a i..b, f x ∂μ) l (𝓝 (∫ (x : ℝ) in Iic b, f x ∂μ))