ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R✝ : Type u_1<VAR>M✝ : Type u_2<VAR>inst✝⁵ : Semiring R✝<VAR>inst✝⁴ : AddCommMonoid M✝<VAR>inst✝³ : Module R✝ M✝<VAR>R : Type u_3<VAR>inst✝² : CommRing R<VAR>M : Type u_4<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>I : Ideal R<VAR>N : Submodule R M<VAR>s✝ : Set M<VAR>hfs : s✝.Finite<VAR>i : M<VAR>s : Set M<VAR>x✝¹ : i ∉ s<VAR>x✝ : s.Finite<VAR>ih : (∃ r, r - 1 ∈ I ∧ N ≤ comap ((LinearMap.lsmul R M) r) (I • span R s) ∧ s ⊆ ↑N) → ∃ r, r - 1 ∈ I ∧ ∀ n ∈ N, r • n = 0<VAR>r : R<VAR>hr1 : r - 1 ∈ I<VAR>hrn : N ≤ comap ((LinearMap.lsmul R M) r) (I • span R {i} ⊔ I • span R s)<VAR>hs : i ∈ ↑N ∧ s ⊆ ↑N<VAR>c : R<VAR>hc1 : c - 1 ∈ I<VAR>hci : c • i ∈ I • span R s<GOAL>N ≤ comap ((LinearMap.lsmul R M) (c * r)) (I • span R s)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>R₂ : Type u_4<VAR>K : Type u_5<VAR>M : Type u_6<VAR>M' : Type u_7<VAR>M'' : Type u_8<VAR>V : Type u<VAR>V' : Type u_9<VAR>inst✝⁴ : Semiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommMonoid M'<VAR>inst✝ : Module R M'<VAR>b b₁ : Basis ι R M<VAR>i✝ : ι<VAR>c : R<VAR>x✝ : M<VAR>b' : Basis ι' R M'<VAR>e : ι ≃ ι'<VAR>x : M<VAR>i : ι<VAR>a✝ : Nontrivial R<GOAL>(b.reindexRange.repr x) ⟨b i, ⋯⟩ = (b.repr x) i
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>R₂ : Type u_4<VAR>K : Type u_5<VAR>M : Type u_6<VAR>M' : Type u_7<VAR>M'' : Type u_8<VAR>V : Type u<VAR>V' : Type u_9<VAR>inst✝⁴ : Semiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommMonoid M'<VAR>inst✝ : Module R M'<VAR>b b₁ : Basis ι R M<VAR>i✝ : ι<VAR>c : R<VAR>x✝ : M<VAR>b' : Basis ι' R M'<VAR>e : ι ≃ ι'<VAR>x : M<VAR>i : ι<VAR>a✝ : Nontrivial R<GOAL>∀ (x y : M), (fun x i => (b.reindexRange.repr x) ⟨b i, ⋯⟩) (x + y) = (fun x i => (b.reindexRange.repr x) ⟨b i, ⋯⟩) x + (fun x i => (b.reindexRange.repr x) ⟨b i, ⋯⟩) y
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>R₂ : Type u_4<VAR>K : Type u_5<VAR>M : Type u_6<VAR>M' : Type u_7<VAR>M'' : Type u_8<VAR>V : Type u<VAR>V' : Type u_9<VAR>inst✝⁴ : Semiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommMonoid M'<VAR>inst✝ : Module R M'<VAR>b b₁ : Basis ι R M<VAR>i✝ : ι<VAR>c : R<VAR>x✝ : M<VAR>b' : Basis ι' R M'<VAR>e : ι ≃ ι'<VAR>x : M<VAR>i : ι<VAR>a✝ : Nontrivial R<GOAL>∀ (c : R) (x : M), (fun x i => (b.reindexRange.repr x) ⟨b i, ⋯⟩) (c • x) = c • (fun x i => (b.reindexRange.repr x) ⟨b i, ⋯⟩) x
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>R₂ : Type u_4<VAR>K : Type u_5<VAR>M : Type u_6<VAR>M' : Type u_7<VAR>M'' : Type u_8<VAR>V : Type u<VAR>V' : Type u_9<VAR>inst✝⁴ : Semiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommMonoid M'<VAR>inst✝ : Module R M'<VAR>b b₁ : Basis ι R M<VAR>i✝ : ι<VAR>c : R<VAR>x✝ : M<VAR>b' : Basis ι' R M'<VAR>e : ι ≃ ι'<VAR>x : M<VAR>i : ι<VAR>a✝ : Nontrivial R<GOAL>∀ (i : ι), (fun x i => (b.reindexRange.repr x) ⟨b i, ⋯⟩) (b i) = ⇑(Finsupp.single i 1)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>hs : s.Finite<GOAL>Nat.card ↑s = hs.toFinset.card
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : PartialOrder β<VAR>f : α → β<VAR>h_mono : Monotone f<VAR>h_surj : Surjective f<VAR>a b : α<GOAL>SurjOn f (Ioc a b) (Ioc (f a) (f b))
<VAR>𝕜 : Type u_1<VAR>A✝¹ : Type u_2<VAR>A✝ : Type u_3<VAR>inst✝³ : Ring A✝<VAR>A : Type u_4<VAR>inst✝² : NormedRing A<VAR>inst✝¹ : NormedAlgebra ℝ A<VAR>inst✝ : CompleteSpace A<VAR>a : A<VAR>ha : (spectrum ℝ a).Nonempty<GOAL>(spectralRadius ℝ a).toReal ∈ spectrum ℝ a ∨ -(spectralRadius ℝ a).toReal ∈ spectrum ℝ a
<VAR>𝕜 : Type u_1<VAR>A✝¹ : Type u_2<VAR>A✝ : Type u_3<VAR>inst✝³ : Ring A✝<VAR>A : Type u_4<VAR>inst✝² : NormedRing A<VAR>inst✝¹ : NormedAlgebra ℝ A<VAR>inst✝ : CompleteSpace A<VAR>a : A<VAR>ha : (spectrum ℝ a).Nonempty<VAR>x : ℝ<VAR>hx₁ : x ∈ spectrum ℝ a<VAR>hx₂ : ↑‖x‖₊ = spectralRadius ℝ a<GOAL>(spectralRadius ℝ a).toReal ∈ spectrum ℝ a ∨ -(spectralRadius ℝ a).toReal ∈ spectrum ℝ a
<VAR>𝕜 : Type u_1<VAR>A✝¹ : Type u_2<VAR>A✝ : Type u_3<VAR>inst✝³ : Ring A✝<VAR>A : Type u_4<VAR>inst✝² : NormedRing A<VAR>inst✝¹ : NormedAlgebra ℝ A<VAR>inst✝ : CompleteSpace A<VAR>a : A<VAR>ha : (spectrum ℝ a).Nonempty<VAR>x : ℝ<VAR>hx₁ : x ∈ spectrum ℝ a<VAR>hx₂ : ↑‖x‖₊ = spectralRadius ℝ a<GOAL>|x| ∈ spectrum ℝ a ∨ -|x| ∈ spectrum ℝ a
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝¹ : SeminormedAddCommGroup M<VAR>inst✝ : SeminormedAddCommGroup N<VAR>S : AddSubgroup M<VAR>x y : M ⧸ S<GOAL>‖x + y‖ ≤ ‖x‖ + ‖y‖
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝¹ : SeminormedAddCommGroup M<VAR>inst✝ : SeminormedAddCommGroup N<VAR>S : AddSubgroup M<VAR>x y : M<GOAL>‖↑x + ↑y‖ ≤ ‖↑x‖ + ‖↑y‖
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝¹ : SeminormedAddCommGroup M<VAR>inst✝ : SeminormedAddCommGroup N<VAR>S : AddSubgroup M<VAR>x y : M<GOAL>⨅ a, ‖x + y + ↑a‖ ≤ (⨅ a, ‖x + ↑a‖) + ⨅ a, ‖y + ↑a‖
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝¹ : SeminormedAddCommGroup M<VAR>inst✝ : SeminormedAddCommGroup N<VAR>S : AddSubgroup M<VAR>x y : M<VAR>a b : ↑↑S<GOAL>⨅ a, ‖x + y + ↑a‖ ≤ ‖x + ↑a‖ + ‖y + ↑b‖
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝¹ : SeminormedAddCommGroup M<VAR>inst✝ : SeminormedAddCommGroup N<VAR>S : AddSubgroup M<VAR>x y : M<VAR>a b : ↑↑S<GOAL>‖x + y + ↑(a + b)‖ ≤ ‖x + ↑a‖ + ‖y + ↑b‖
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>inst✝² : Preorder α<VAR>inst✝¹ : Preorder β<VAR>inst✝ : Preorder γ<VAR>f✝ : α ≃o β<VAR>s t : LowerSet α<VAR>a : α<VAR>b✝ : β<VAR>f : α ≃o β<VAR>b : β<GOAL>b ∈ (map f) s ↔ f.symm b ∈ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>inst✝² : Preorder α<VAR>inst✝¹ : Preorder β<VAR>inst✝ : Preorder γ<VAR>f✝ : α ≃o β<VAR>s t : LowerSet α<VAR>a : α<VAR>b✝ : β<VAR>f : α ≃o β<VAR>b : β<GOAL>b ∈ (map f.symm).symm s ↔ f.symm b ∈ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set ℕ<VAR>inst✝¹ : Infinite ↑s<VAR>inst✝ : DecidablePred fun x => x ∈ s<GOAL>Set.range (Subtype.val ∘ ofNat s) = s
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_4, u_1} C<VAR>inst✝³ : Category.{u_5, u_2} D<VAR>L✝ : C ⥤ D<VAR>W✝ : MorphismProperty C<VAR>E : Type u_3<VAR>inst✝² : Category.{u_6, u_3} E<VAR>inst✝¹ : L✝.IsLocalization W✝<VAR>L : C ⥤ D<VAR>W : MorphismProperty C<VAR>inst✝ : L.IsLocalization W<VAR>F₁ F₂ : D ⥤ E<VAR>τ τ' : F₁ ⟶ F₂<VAR>h : ∀ (X : C), τ.app (L.obj X) = τ'.app (L.obj X)<GOAL>τ = τ'
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_4, u_1} C<VAR>inst✝³ : Category.{u_5, u_2} D<VAR>L✝ : C ⥤ D<VAR>W✝ : MorphismProperty C<VAR>E : Type u_3<VAR>inst✝² : Category.{u_6, u_3} E<VAR>inst✝¹ : L✝.IsLocalization W✝<VAR>L : C ⥤ D<VAR>W : MorphismProperty C<VAR>inst✝ : L.IsLocalization W<VAR>F₁ F₂ : D ⥤ E<VAR>τ τ' : F₁ ⟶ F₂<VAR>h : ∀ (X : C), τ.app (L.obj X) = τ'.app (L.obj X)<VAR>this : L.EssSurj<GOAL>τ = τ'
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_4, u_1} C<VAR>inst✝³ : Category.{u_5, u_2} D<VAR>L✝ : C ⥤ D<VAR>W✝ : MorphismProperty C<VAR>E : Type u_3<VAR>inst✝² : Category.{u_6, u_3} E<VAR>inst✝¹ : L✝.IsLocalization W✝<VAR>L : C ⥤ D<VAR>W : MorphismProperty C<VAR>inst✝ : L.IsLocalization W<VAR>F₁ F₂ : D ⥤ E<VAR>τ τ' : F₁ ⟶ F₂<VAR>h : ∀ (X : C), τ.app (L.obj X) = τ'.app (L.obj X)<VAR>this : L.EssSurj<VAR>Y : D<GOAL>τ.app Y = τ'.app Y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s✝ t s : Set α<VAR>inst✝ : Fintype ↑s<GOAL>s.toFinset.Nonempty ↔ s.Nonempty
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>a b : α<VAR>s✝ s₁✝ s₂✝ t✝ t₁ t₂ u t s₁ s₂ s : Set α<VAR>h : s₁ ∩ s = s₂ ∩ s<GOAL>t.ite s₁ s₂ ∩ s = s₁ ∩ s
<VAR>ι : Sort u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>s t u : Set E<VAR>x y a b c : E<GOAL>convexJoin 𝕜 {a} (segment 𝕜 b c) = (convexHull 𝕜) {a, b, c}
<VAR>s : ℂ<VAR>hs : 0 < s.re<VAR>X : ℝ<VAR>hX : 0 ≤ X<GOAL>IntervalIntegrable (fun x => -(↑(rexp (-x)) * ↑x ^ s)) volume 0 X
<VAR>s : ℂ<VAR>hs : 0 < s.re<VAR>X : ℝ<VAR>hX : 0 ≤ X<VAR>x✝ : ℝ<GOAL>-(↑(rexp (-x✝)) * ↑x✝ ^ s) = (-fun x => ↑(rexp (-x)) * ↑x ^ (s + 1 - 1)) x✝
<VAR>s : ℂ<VAR>hs : 0 < s.re<VAR>X : ℝ<VAR>hX : 0 ≤ X<GOAL>0 < (s + 1).re
<VAR>m n✝ n : ℕ<GOAL>1⁻¹ = 1
<VAR>m n : ℕ<GOAL>1⁻¹ = 1
<VAR>m n✝ n : ℕ<VAR>hn : n ≠ 1<GOAL>1⁻¹ = 1
<VAR>α : Type u<VAR>β : Type u_1<VAR>t : TopologicalSpace α<VAR>B : Set (Set α)<VAR>s✝ : Set α<VAR>b : Set (Set α)<VAR>hb : IsTopologicalBasis b<VAR>a : α<VAR>s : Set α<GOAL>(∃ t ∈ b, a ∈ t ∧ t ⊆ s) ↔ ∃ i, (i ∈ b ∧ a ∈ i) ∧ i ⊆ s
<VAR>α : Type u<VAR>inst✝ : CompleteLattice α<VAR>f : α →o α<VAR>x : α<GOAL>lfp f ∈ Set.range (lfpApprox f ⊥)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p✝ : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>f : α → F<VAR>g : α → G<VAR>c : ℝ<VAR>h : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c * ‖g x‖<VAR>hc : c < 0<VAR>p : ℝ≥0∞<GOAL>eLpNorm f p μ = 0 ∧ eLpNorm g p μ = 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p✝ : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>f : α → F<VAR>g : α → G<VAR>c : ℝ<VAR>hc : c < 0<VAR>p : ℝ≥0∞<VAR>h : (∀ᵐ (x : α) ∂μ, f x = 0) ∧ ∀ᵐ (x : α) ∂μ, g x = 0<GOAL>eLpNorm f p μ = 0 ∧ eLpNorm g p μ = 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p✝ : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>f : α → F<VAR>g : α → G<VAR>c : ℝ<VAR>hc : c < 0<VAR>p : ℝ≥0∞<VAR>h : f =ᶠ[ae μ] 0 ∧ g =ᶠ[ae μ] 0<GOAL>eLpNorm f p μ = 0 ∧ eLpNorm g p μ = 0
<GOAL>∫ (x : ℝ) in Ioi 0, rexp (-x) = 1
<VAR>α : Type u_1<VAR>inst✝² : CanonicallyLinearOrderedAddCommMonoid α<VAR>inst✝¹ : Sub α<VAR>inst✝ : OrderedSub α<VAR>a b c d : α<VAR>hc : AddLECancellable c<VAR>h : c ≤ a<GOAL>a - c < b - c ↔ a < b
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>E' : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹³ : RCLike 𝕜<VAR>inst✝¹² : NormedAddCommGroup E<VAR>inst✝¹¹ : InnerProductSpace 𝕜 E<VAR>inst✝¹⁰ : CompleteSpace E<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : InnerProductSpace 𝕜 E'<VAR>inst✝⁷ : CompleteSpace E'<VAR>inst✝⁶ : NormedSpace ℝ E'<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedAddCommGroup G'<VAR>inst✝¹ : NormedSpace ℝ G'<VAR>inst✝ : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>hm : m ≤ m0<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>f : ↥(Lp ℝ 2 μ)<VAR>hf : ↑↑f =ᶠ[ae (μ.restrict s)] 0<GOAL>∫⁻ (x : α) in s, ↑‖↑↑↑((condexpL2 ℝ ℝ hm) f) x‖₊ ∂μ = 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>E' : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹³ : RCLike 𝕜<VAR>inst✝¹² : NormedAddCommGroup E<VAR>inst✝¹¹ : InnerProductSpace 𝕜 E<VAR>inst✝¹⁰ : CompleteSpace E<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : InnerProductSpace 𝕜 E'<VAR>inst✝⁷ : CompleteSpace E'<VAR>inst✝⁶ : NormedSpace ℝ E'<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedAddCommGroup G'<VAR>inst✝¹ : NormedSpace ℝ G'<VAR>inst✝ : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>hm : m ≤ m0<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>f : ↥(Lp ℝ 2 μ)<VAR>hf : ↑↑f =ᶠ[ae (μ.restrict s)] 0<GOAL>∫⁻ (x : α) in s, ↑‖↑↑↑((condexpL2 ℝ ℝ hm) f) x‖₊ ∂μ ≤ 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>E' : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹³ : RCLike 𝕜<VAR>inst✝¹² : NormedAddCommGroup E<VAR>inst✝¹¹ : InnerProductSpace 𝕜 E<VAR>inst✝¹⁰ : CompleteSpace E<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : InnerProductSpace 𝕜 E'<VAR>inst✝⁷ : CompleteSpace E'<VAR>inst✝⁶ : NormedSpace ℝ E'<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedAddCommGroup G'<VAR>inst✝¹ : NormedSpace ℝ G'<VAR>inst✝ : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>hm : m ≤ m0<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>f : ↥(Lp ℝ 2 μ)<VAR>hf : ↑↑f =ᶠ[ae (μ.restrict s)] 0<GOAL>∫⁻ (x : α) in s, ↑‖↑↑f x‖₊ ∂μ = 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>E' : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹³ : RCLike 𝕜<VAR>inst✝¹² : NormedAddCommGroup E<VAR>inst✝¹¹ : InnerProductSpace 𝕜 E<VAR>inst✝¹⁰ : CompleteSpace E<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : InnerProductSpace 𝕜 E'<VAR>inst✝⁷ : CompleteSpace E'<VAR>inst✝⁶ : NormedSpace ℝ E'<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedAddCommGroup G'<VAR>inst✝¹ : NormedSpace ℝ G'<VAR>inst✝ : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>hm : m ≤ m0<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>f : ↥(Lp ℝ 2 μ)<VAR>hf : ↑↑f =ᶠ[ae (μ.restrict s)] 0<GOAL>(fun x => ↑‖↑↑f x‖₊) =ᶠ[ae (μ.restrict s)] 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>E' : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹³ : RCLike 𝕜<VAR>inst✝¹² : NormedAddCommGroup E<VAR>inst✝¹¹ : InnerProductSpace 𝕜 E<VAR>inst✝¹⁰ : CompleteSpace E<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : InnerProductSpace 𝕜 E'<VAR>inst✝⁷ : CompleteSpace E'<VAR>inst✝⁶ : NormedSpace ℝ E'<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedAddCommGroup G'<VAR>inst✝¹ : NormedSpace ℝ G'<VAR>inst✝ : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>hm : m ≤ m0<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>f : ↥(Lp ℝ 2 μ)<VAR>hf : ↑↑f =ᶠ[ae (μ.restrict s)] 0<GOAL>Measurable fun x => ↑‖↑↑f x‖₊
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s t : Set α<VAR>inst✝³ : DecidableEq α<VAR>inst✝² : Fintype ↑s<VAR>inst✝¹ : Fintype ↑t<VAR>inst✝ : Fintype ↑(s ∆ t)<VAR>a✝ : α<GOAL>a✝ ∈ (s ∆ t).toFinset ↔ a✝ ∈ s.toFinset ∆ t.toFinset
<VAR>R : Type u1<VAR>inst✝³ : CommRing R<VAR>M : Type u2<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>Q Q' Q'' : QuadraticForm R M<VAR>B B' : BilinForm R M<VAR>h : BilinMap.toQuadraticMap B = Q' - Q<VAR>h' : BilinMap.toQuadraticMap B' = Q'' - Q'<VAR>inst✝ : Invertible 2<GOAL>(QuadraticMap.associated (-Q)).toQuadraticMap = 0 - Q
<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>f : E → E<VAR>f' : E →L[𝕜] E<VAR>hf : HasFDerivWithinAt f f' s x<VAR>hx : f x = x<VAR>hs : MapsTo f s s<VAR>n : ℕ<GOAL>HasFDerivWithinAt f^[n] (f' ^ n) s 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>f : E → E<VAR>f' : E →L[𝕜] E<VAR>hf : HasFDerivWithinAt f f' s x<VAR>hx : f x = x<VAR>hs : MapsTo f s s<VAR>n : ℕ<GOAL>Tendsto f (𝓝[s] x) (𝓝[s] 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>f : E → E<VAR>f' : E →L[𝕜] E<VAR>hf : HasFDerivWithinAt f f' s x<VAR>hx : f x = x<VAR>hs : MapsTo f s s<VAR>n : ℕ<GOAL>Tendsto f (𝓝 x ⊓ 𝓟 s) (𝓝 x ⊓ 𝓟 s)
<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>f : E → E<VAR>f' : E →L[𝕜] E<VAR>hf : HasFDerivWithinAt f f' s x<VAR>hx : f x = x<VAR>hs : MapsTo f s s<VAR>n : ℕ<GOAL>x = 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>f : E → E<VAR>f' : E →L[𝕜] E<VAR>hf : HasFDerivWithinAt f f' s x<VAR>hx : f x = x<VAR>hs : MapsTo f s s<VAR>n : ℕ<GOAL>Tendsto f (𝓝[s] x) (𝓟 s)
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Preadditive C<VAR>X : SimplicialObject C<VAR>Y : C<VAR>n q : ℕ<VAR>φ : Y ⟶ X _[n + 1]<VAR>v : HigherFacesVanish q φ<VAR>j : Fin (n + 2)<VAR>hj₁ : j ≠ 0<VAR>hj₂ : n + 2 ≤ ↑j + q<GOAL>φ ≫ X.δ j = 0
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Preadditive C<VAR>X : SimplicialObject C<VAR>Y : C<VAR>n q : ℕ<VAR>φ : Y ⟶ X _[n + 1]<VAR>v : HigherFacesVanish q φ<VAR>i : Fin (n + 1)<VAR>hj₁ : i.succ ≠ 0<VAR>hj₂ : n + 2 ≤ ↑i.succ + q<GOAL>φ ≫ X.δ i.succ = 0
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Preadditive C<VAR>X : SimplicialObject C<VAR>Y : C<VAR>n q : ℕ<VAR>φ : Y ⟶ X _[n + 1]<VAR>v : HigherFacesVanish q φ<VAR>i : Fin (n + 1)<VAR>hj₁ : i.succ ≠ 0<VAR>hj₂ : n + 2 ≤ ↑i.succ + q<GOAL>n + 1 ≤ ↑i + q
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Preadditive C<VAR>X : SimplicialObject C<VAR>Y : C<VAR>n q : ℕ<VAR>φ : Y ⟶ X _[n + 1]<VAR>v : HigherFacesVanish q φ<VAR>i : Fin (n + 1)<VAR>hj₁ : i.succ ≠ 0<VAR>hj₂ : n + 2 ≤ ↑i + 1 + q<GOAL>n + 1 ≤ ↑i + q
<VAR>R : Type u_1<VAR>inst✝¹ : CommMonoid R<VAR>R' : Type u_2<VAR>inst✝ : CommMonoidWithZero R'<VAR>χ : MulChar R R'<VAR>a✝ : Rˣ<GOAL>(χ * 1) ↑a✝ = χ ↑a✝
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>a b : R<VAR>m n✝ : ℕ<VAR>inst✝¹ : Semiring R<VAR>p q r : R[X]<VAR>inst✝ : Semiring S<VAR>f : R →+* S<VAR>x : S<VAR>n : ℕ<GOAL>eval₂ f x (X ^ n) = x ^ n
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>a b : R<VAR>m n✝ : ℕ<VAR>inst✝¹ : Semiring R<VAR>p q r : R[X]<VAR>inst✝ : Semiring S<VAR>f : R →+* S<VAR>x : S<VAR>n : ℕ<GOAL>eval₂ f x ((monomial n) 1) = x ^ n
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>a b : R<VAR>m n✝ : ℕ<VAR>inst✝¹ : Semiring R<VAR>p q r : R[X]<VAR>inst✝ : Semiring S<VAR>f : R →+* S<VAR>x : S<VAR>n : ℕ<GOAL>x ^ n = f 1 * x ^ n
<VAR>s : ℂ<VAR>hs : 1 < s.re<GOAL>L (fun n => ↑(ζ n)) s = riemannZeta s
<VAR>s : ℂ<VAR>hs : 1 < s.re<GOAL>∑' (n : ℕ), term (fun n => if n = 0 then 0 else 1) s n = ∑' (n : ℕ), 1 / ↑n ^ s
<VAR>s : ℂ<VAR>hs : 1 < s.re<VAR>n : ℕ<GOAL>term (fun n => if n = 0 then 0 else 1) s n = 1 / ↑n ^ s
<VAR>s : ℂ<VAR>hs : 1 < s.re<GOAL>term (fun n => if n = 0 then 0 else 1) s 0 = 1 / ↑0 ^ s
<VAR>s : ℂ<VAR>hs : 1 < s.re<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>term (fun n => if n = 0 then 0 else 1) s n = 1 / ↑n ^ s
<VAR>C : Type u₁<VAR>inst✝² : Category.{u₂, u₁} C<VAR>I : Type v₁<VAR>inst✝¹ : Category.{v₂, v₁} I<VAR>F : Iᵒᵖ ⥤ C<VAR>inst✝ : HasColimit F<VAR>i : I<GOAL>(coyonedaOpColimitIsoLimitCoyoneda' F).inv ≫ coyoneda.map (colimit.ι F (op i)).op = limit.π (F.rightOp ⋙ coyoneda) i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f g : α → β<VAR>c c₁ c₂ x✝ : α<VAR>inst✝¹ : AddMonoid α<VAR>inst✝ : InvolutiveNeg β<VAR>h : Antiperiodic f c<VAR>n : ℕ<VAR>x : α<GOAL>f (x + (2 * n + 1) • c) = -f x
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : ι → Type u_3<VAR>inst✝³ : Fintype ι<VAR>m✝¹ : (i : ι) → OuterMeasure (α i)<VAR>m✝ : (i : ι) → MeasurableSpace (α i)<VAR>μ✝ : (i : ι) → Measure (α i)<VAR>inst✝² : ∀ (i : ι), SigmaFinite (μ✝ i)<VAR>inst✝¹ : Fintype ι'<VAR>π : ι ⊕ ι' → Type u_4<VAR>m : (i : ι ⊕ ι') → MeasurableSpace (π i)<VAR>μ : (i : ι ⊕ ι') → Measure (π i)<VAR>inst✝ : ∀ (i : ι ⊕ ι'), SigmaFinite (μ i)<GOAL>Measure.map (⇑(MeasurableEquiv.sumPiEquivProdPi π).symm) ((Measure.pi fun i => μ (Sum.inl i)).prod (Measure.pi fun i => μ (Sum.inr i))) = Measure.pi μ
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : ι → Type u_3<VAR>inst✝³ : Fintype ι<VAR>m✝¹ : (i : ι) → OuterMeasure (α i)<VAR>m✝ : (i : ι) → MeasurableSpace (α i)<VAR>μ✝ : (i : ι) → Measure (α i)<VAR>inst✝² : ∀ (i : ι), SigmaFinite (μ✝ i)<VAR>inst✝¹ : Fintype ι'<VAR>π : ι ⊕ ι' → Type u_4<VAR>m : (i : ι ⊕ ι') → MeasurableSpace (π i)<VAR>μ : (i : ι ⊕ ι') → Measure (π i)<VAR>inst✝ : ∀ (i : ι ⊕ ι'), SigmaFinite (μ i)<VAR>s : (i : ι ⊕ ι') → Set (π i)<VAR>x✝ : ∀ (i : ι ⊕ ι'), MeasurableSet (s i)<GOAL>(Measure.map (⇑(MeasurableEquiv.sumPiEquivProdPi π).symm) ((Measure.pi fun i => μ (Sum.inl i)).prod (Measure.pi fun i => μ (Sum.inr i)))) (univ.pi s) = ∏ i : ι ⊕ ι', (μ i) (s i)
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>p : ℝ≥0∞<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : NormedAddCommGroup G<VAR>f : α → G<VAR>hf : Memℒp f p μ<VAR>hf_meas : StronglyMeasurable f<VAR>hp_ne_zero : p ≠ 0<VAR>hp_ne_top : p ≠ ⊤<VAR>this✝¹ : MeasurableSpace G := borel G<VAR>this✝ : BorelSpace G<GOAL>FinStronglyMeasurable f μ
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>p : ℝ≥0∞<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : NormedAddCommGroup G<VAR>f : α → G<VAR>hf : Memℒp f p μ<VAR>hf_meas : StronglyMeasurable f<VAR>hp_ne_zero : p ≠ 0<VAR>hp_ne_top : p ≠ ⊤<VAR>this✝¹ : MeasurableSpace G := borel G<VAR>this✝ : BorelSpace G<VAR>this : SeparableSpace ↑(Set.range f ∪ {0})<GOAL>FinStronglyMeasurable f μ
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>p : ℝ≥0∞<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : NormedAddCommGroup G<VAR>f : α → G<VAR>hf : Memℒp f p μ<VAR>hf_meas : StronglyMeasurable f<VAR>hp_ne_zero : p ≠ 0<VAR>hp_ne_top : p ≠ ⊤<VAR>this✝¹ : MeasurableSpace G := borel G<VAR>this✝ : BorelSpace G<VAR>this : SeparableSpace ↑(Set.range f ∪ {0})<VAR>fs : ℕ → α →ₛ G := SimpleFunc.approxOn f ⋯ (Set.range f ∪ {0}) 0 ⋯<GOAL>FinStronglyMeasurable f μ
<VAR>s : String<VAR>c : Char<GOAL>s.contains c = true ↔ c ∈ s.data
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedRing α<VAR>inst✝ : FloorRing α<VAR>z : ℤ<VAR>a : α<GOAL>⌈a⌉ = z ↔ ↑z - 1 < a ∧ a ≤ ↑z
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝¹ : CommRing P<VAR>inst✝ : Algebra R P<VAR>loc : IsLocalization S P<VAR>I : Submodule R P<VAR>h : I ≤ 1<GOAL>IsFractional S I
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝¹ : CommRing P<VAR>inst✝ : Algebra R P<VAR>loc : IsLocalization S P<VAR>I : Submodule R P<VAR>h : I ≤ 1<GOAL>∀ b ∈ I, IsInteger R (1 • b)
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝¹ : CommRing P<VAR>inst✝ : Algebra R P<VAR>loc : IsLocalization S P<VAR>I : Submodule R P<VAR>h : I ≤ 1<VAR>b : P<VAR>hb : b ∈ I<GOAL>IsInteger R (1 • b)
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝¹ : CommRing P<VAR>inst✝ : Algebra R P<VAR>loc : IsLocalization S P<VAR>I : Submodule R P<VAR>h : I ≤ 1<VAR>b : P<VAR>hb : b ∈ I<GOAL>IsInteger R b