ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>inst✝²¹ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝²⁰ : NormedAddCommGroup E<VAR>inst✝¹⁹ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝¹⁸ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝¹⁷ : TopologicalSpace M<VAR>inst✝¹⁶ : ChartedSpace H M<VAR>inst✝¹⁵ : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝¹⁴ : NormedAddCommGroup E'<VAR>inst✝¹³ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝¹² : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝¹¹ : TopologicalSpace M'<VAR>inst✝¹⁰ : ChartedSpace H' M'<VAR>inst✝⁹ : SmoothManifoldWithCorners I' M'<VAR>s : Set M<VAR>x : M<VAR>F : Type u_8<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>Z : M → Type u_9<VAR>inst✝⁶ : TopologicalSpace (TotalSpace F Z)<VAR>inst✝⁵ : (b : M) → TopologicalSpace (Z b)<VAR>inst✝⁴ : (b : M) → AddCommMonoid (Z b)<VAR>inst✝³ : (b : M) → Module 𝕜 (Z b)<VAR>inst✝² : FiberBundle F Z<VAR>inst✝¹ : VectorBundle 𝕜 F Z<VAR>inst✝ : SmoothVectorBundle F Z I<VAR>p : TotalSpace F Z<VAR>hs : UniqueMDiffWithinAt I s p.proj<VAR>e : Trivialization F TotalSpace.proj := trivializationAt F Z p.proj<GOAL>UniqueMDiffWithinAt (I.prod 𝓘(𝕜, F)) (TotalSpace.proj ⁻¹' s) p
<VAR>𝕜 : Type u_1<VAR>inst✝²¹ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝²⁰ : NormedAddCommGroup E<VAR>inst✝¹⁹ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝¹⁸ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝¹⁷ : TopologicalSpace M<VAR>inst✝¹⁶ : ChartedSpace H M<VAR>inst✝¹⁵ : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝¹⁴ : NormedAddCommGroup E'<VAR>inst✝¹³ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝¹² : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝¹¹ : TopologicalSpace M'<VAR>inst✝¹⁰ : ChartedSpace H' M'<VAR>inst✝⁹ : SmoothManifoldWithCorners I' M'<VAR>s : Set M<VAR>x : M<VAR>F : Type u_8<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>Z : M → Type u_9<VAR>inst✝⁶ : TopologicalSpace (TotalSpace F Z)<VAR>inst✝⁵ : (b : M) → TopologicalSpace (Z b)<VAR>inst✝⁴ : (b : M) → AddCommMonoid (Z b)<VAR>inst✝³ : (b : M) → Module 𝕜 (Z b)<VAR>inst✝² : FiberBundle F Z<VAR>inst✝¹ : VectorBundle 𝕜 F Z<VAR>inst✝ : SmoothVectorBundle F Z I<VAR>p : TotalSpace F Z<VAR>hs : UniqueMDiffWithinAt I s p.proj<VAR>e : Trivialization F TotalSpace.proj := trivializationAt F Z p.proj<VAR>hp : p ∈ e.source<GOAL>UniqueMDiffWithinAt (I.prod 𝓘(𝕜, F)) (TotalSpace.proj ⁻¹' s) p
<VAR>𝕜 : Type u_1<VAR>inst✝²¹ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝²⁰ : NormedAddCommGroup E<VAR>inst✝¹⁹ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝¹⁸ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝¹⁷ : TopologicalSpace M<VAR>inst✝¹⁶ : ChartedSpace H M<VAR>inst✝¹⁵ : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝¹⁴ : NormedAddCommGroup E'<VAR>inst✝¹³ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝¹² : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝¹¹ : TopologicalSpace M'<VAR>inst✝¹⁰ : ChartedSpace H' M'<VAR>inst✝⁹ : SmoothManifoldWithCorners I' M'<VAR>s : Set M<VAR>x : M<VAR>F : Type u_8<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>Z : M → Type u_9<VAR>inst✝⁶ : TopologicalSpace (TotalSpace F Z)<VAR>inst✝⁵ : (b : M) → TopologicalSpace (Z b)<VAR>inst✝⁴ : (b : M) → AddCommMonoid (Z b)<VAR>inst✝³ : (b : M) → Module 𝕜 (Z b)<VAR>inst✝² : FiberBundle F Z<VAR>inst✝¹ : VectorBundle 𝕜 F Z<VAR>inst✝ : SmoothVectorBundle F Z I<VAR>p : TotalSpace F Z<VAR>hs : UniqueMDiffWithinAt I s p.proj<VAR>e : Trivialization F TotalSpace.proj := trivializationAt F Z p.proj<VAR>hp : p ∈ e.source<VAR>this : UniqueMDiffWithinAt (I.prod 𝓘(𝕜, F)) (s ×ˢ univ) (↑e p)<GOAL>UniqueMDiffWithinAt (I.prod 𝓘(𝕜, F)) (TotalSpace.proj ⁻¹' s) p
<VAR>𝕜 : Type u_1<VAR>inst✝²¹ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝²⁰ : NormedAddCommGroup E<VAR>inst✝¹⁹ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝¹⁸ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝¹⁷ : TopologicalSpace M<VAR>inst✝¹⁶ : ChartedSpace H M<VAR>inst✝¹⁵ : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝¹⁴ : NormedAddCommGroup E'<VAR>inst✝¹³ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝¹² : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝¹¹ : TopologicalSpace M'<VAR>inst✝¹⁰ : ChartedSpace H' M'<VAR>inst✝⁹ : SmoothManifoldWithCorners I' M'<VAR>s : Set M<VAR>x : M<VAR>F : Type u_8<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>Z : M → Type u_9<VAR>inst✝⁶ : TopologicalSpace (TotalSpace F Z)<VAR>inst✝⁵ : (b : M) → TopologicalSpace (Z b)<VAR>inst✝⁴ : (b : M) → AddCommMonoid (Z b)<VAR>inst✝³ : (b : M) → Module 𝕜 (Z b)<VAR>inst✝² : FiberBundle F Z<VAR>inst✝¹ : VectorBundle 𝕜 F Z<VAR>inst✝ : SmoothVectorBundle F Z I<VAR>p : TotalSpace F Z<VAR>hs : UniqueMDiffWithinAt I s p.proj<VAR>e : Trivialization F TotalSpace.proj := trivializationAt F Z p.proj<VAR>hp : p ∈ e.source<VAR>this : UniqueMDiffWithinAt (I.prod 𝓘(𝕜, F)) (s ×ˢ univ) (↑e p)<GOAL>UniqueMDiffWithinAt (I.prod 𝓘(𝕜, F)) (TotalSpace.proj ⁻¹' s) (↑e.symm (↑e.toPartialHomeomorph p))
<VAR>𝕜 : Type u_1<VAR>inst✝²¹ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝²⁰ : NormedAddCommGroup E<VAR>inst✝¹⁹ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝¹⁸ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝¹⁷ : TopologicalSpace M<VAR>inst✝¹⁶ : ChartedSpace H M<VAR>inst✝¹⁵ : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝¹⁴ : NormedAddCommGroup E'<VAR>inst✝¹³ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝¹² : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝¹¹ : TopologicalSpace M'<VAR>inst✝¹⁰ : ChartedSpace H' M'<VAR>inst✝⁹ : SmoothManifoldWithCorners I' M'<VAR>s : Set M<VAR>x : M<VAR>F : Type u_8<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>Z : M → Type u_9<VAR>inst✝⁶ : TopologicalSpace (TotalSpace F Z)<VAR>inst✝⁵ : (b : M) → TopologicalSpace (Z b)<VAR>inst✝⁴ : (b : M) → AddCommMonoid (Z b)<VAR>inst✝³ : (b : M) → Module 𝕜 (Z b)<VAR>inst✝² : FiberBundle F Z<VAR>inst✝¹ : VectorBundle 𝕜 F Z<VAR>inst✝ : SmoothVectorBundle F Z I<VAR>p : TotalSpace F Z<VAR>hs : UniqueMDiffWithinAt I s p.proj<VAR>e : Trivialization F TotalSpace.proj := trivializationAt F Z p.proj<VAR>hp : p ∈ e.source<VAR>this : UniqueMDiffWithinAt (I.prod 𝓘(𝕜, F)) (s ×ˢ univ) (↑e p)<GOAL>e.symm.target ∩ ↑e.symm.symm ⁻¹' s ×ˢ univ ⊆ TotalSpace.proj ⁻¹' s
<VAR>𝕜 : Type u_1<VAR>inst✝²¹ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝²⁰ : NormedAddCommGroup E<VAR>inst✝¹⁹ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝¹⁸ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝¹⁷ : TopologicalSpace M<VAR>inst✝¹⁶ : ChartedSpace H M<VAR>inst✝¹⁵ : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝¹⁴ : NormedAddCommGroup E'<VAR>inst✝¹³ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝¹² : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝¹¹ : TopologicalSpace M'<VAR>inst✝¹⁰ : ChartedSpace H' M'<VAR>inst✝⁹ : SmoothManifoldWithCorners I' M'<VAR>s : Set M<VAR>x : M<VAR>F : Type u_8<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>Z : M → Type u_9<VAR>inst✝⁶ : TopologicalSpace (TotalSpace F Z)<VAR>inst✝⁵ : (b : M) → TopologicalSpace (Z b)<VAR>inst✝⁴ : (b : M) → AddCommMonoid (Z b)<VAR>inst✝³ : (b : M) → Module 𝕜 (Z b)<VAR>inst✝² : FiberBundle F Z<VAR>inst✝¹ : VectorBundle 𝕜 F Z<VAR>inst✝ : SmoothVectorBundle F Z I<VAR>p : TotalSpace F Z<VAR>hs : UniqueMDiffWithinAt I s p.proj<VAR>e : Trivialization F TotalSpace.proj := trivializationAt F Z p.proj<VAR>hp : p ∈ e.source<VAR>this : UniqueMDiffWithinAt (I.prod 𝓘(𝕜, F)) (s ×ˢ univ) (↑e p)<VAR>y : TotalSpace F Z<VAR>hy : y ∈ e.symm.target<VAR>hys : (↑e.symm.symm y).1 ∈ s<GOAL>y ∈ TotalSpace.proj ⁻¹' s
<VAR>R : Type u<VAR>S : Type v<VAR>K : Type w<VAR>inst✝ : CommRing R<VAR>I✝ : Ideal R<VAR>f✝ f : R[X]<VAR>I : Ideal R<VAR>x : R<VAR>this : (algebraMap R (AdjoinRoot f ⧸ Ideal.map (of f) I)) x = (Ideal.Quotient.mk (Ideal.map (of f) I)) ((mk f) (C x))<GOAL>(quotAdjoinRootEquivQuotPolynomialQuot I f) ((algebraMap R (AdjoinRoot f ⧸ Ideal.map (of f) I)) x) = (algebraMap R ((R ⧸ I)[X] ⧸ span {Polynomial.map (Ideal.Quotient.mk I) f})) x
<VAR>R : Type u<VAR>S : Type v<VAR>K : Type w<VAR>inst✝ : CommRing R<VAR>I✝ : Ideal R<VAR>f✝ f : R[X]<VAR>I : Ideal R<VAR>x : R<VAR>this : (algebraMap R (AdjoinRoot f ⧸ Ideal.map (of f) I)) x = (Ideal.Quotient.mk (Ideal.map (of f) I)) ((mk f) (C x))<GOAL>(Ideal.Quotient.mk (span {Polynomial.map (Ideal.Quotient.mk I) f})) (C ((Ideal.Quotient.mk I) x)) = (algebraMap R ((R ⧸ I)[X] ⧸ span {Polynomial.map (Ideal.Quotient.mk I) f})) x
<VAR>n' : Type u_1<VAR>inst✝² : DecidableEq n'<VAR>inst✝¹ : Fintype n'<VAR>R : Type u_2<VAR>inst✝ : CommRing R<VAR>A : M<VAR>ha : IsUnit A.det<VAR>z1 z2 : ℤ<GOAL>A ^ (z1 - z2) = A ^ z1 / A ^ z2
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>K L L' M : Set V<VAR>C : G.ComponentCompl K<GOAL>Disjoint K ↑C
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>K L L' M : Set V<VAR>C : G.ComponentCompl K<GOAL>K ∩ ↑C ⊆ ∅
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>X Y : C<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : HasBinaryCoproducts C<VAR>inst✝ : HasInitial C<VAR>P : C<GOAL>desc (𝟙 P) (initial.to P) ≫ inl = 𝟙 (P ⨿ ⊥_ C)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>M : Type u_4<VAR>inst✝ : DivisionMonoid α<VAR>a b c d : α<VAR>h : 1 / a = 1 / b<GOAL>a = b
<VAR>z : ℂ<VAR>n : ℕ<VAR>hn : 2 ≤ n<VAR>hz : z ≠ 0<GOAL>(1 - 4 * z ^ 2 / ↑n ^ 2) * ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ n = (↑n - 1) / ↑n * ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (n - 2)
<VAR>z : ℂ<VAR>n : ℕ<VAR>hn : 2 ≤ n<VAR>hz : z ≠ 0<VAR>nne : ↑n ≠ 0<GOAL>(1 - 4 * z ^ 2 / ↑n ^ 2) * ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ n = (↑n - 1) / ↑n * ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (n - 2)
<VAR>z : ℂ<VAR>n : ℕ<VAR>hn : 2 ≤ n<VAR>hz : z ≠ 0<VAR>nne : ↑n ≠ 0<VAR>this : ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ n = ↑n / (2 * z) * ∫ (x : ℝ) in 0 ..π / 2, Complex.sin (2 * z * ↑x) * ↑(sin x) * ↑(cos x) ^ (n - 1)<GOAL>(1 - 4 * z ^ 2 / ↑n ^ 2) * ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ n = (↑n - 1) / ↑n * ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (n - 2)
<VAR>z : ℂ<VAR>n : ℕ<VAR>hn : 2 ≤ n<VAR>hz : z ≠ 0<VAR>nne : ↑n ≠ 0<VAR>this : (∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ n) - ↑n / (2 * z) * (↑n / (2 * z) * ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ n) = ↑n / (2 * z) * -((↑n - 1) / (2 * z) * ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (n - 2))<GOAL>(1 - 4 * z ^ 2 / ↑n ^ 2) * ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ n = (↑n - 1) / ↑n * ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (n - 2)
<VAR>R : Type u_1<VAR>inst✝³ : NonAssocRing R<VAR>inst✝² : Pow R ℕ<VAR>inst✝¹ : BinomialRing R<VAR>inst✝ : NatPowAssoc R<VAR>r : R<GOAL>(ascPochhammer ℤ 0).smeval r = (ascPochhammer ℕ 0).smeval r
<VAR>R : Type u_1<VAR>inst✝³ : NonAssocRing R<VAR>inst✝² : Pow R ℕ<VAR>inst✝¹ : BinomialRing R<VAR>inst✝ : NatPowAssoc R<VAR>r : R<VAR>n : ℕ<GOAL>(ascPochhammer ℤ (n + 1)).smeval r = (ascPochhammer ℕ (n + 1)).smeval r
<VAR>R : Type u_1<VAR>inst✝³ : NonAssocRing R<VAR>inst✝² : Pow R ℕ<VAR>inst✝¹ : BinomialRing R<VAR>inst✝ : NatPowAssoc R<VAR>r : R<VAR>n : ℕ<GOAL>(ascPochhammer ℤ n).smeval r * (X + ↑n).smeval r = (ascPochhammer ℕ n).smeval r * (X + ↑n).smeval r
<VAR>R : Type u_1<VAR>inst✝³ : NonAssocRing R<VAR>inst✝² : Pow R ℕ<VAR>inst✝¹ : BinomialRing R<VAR>inst✝ : NatPowAssoc R<VAR>r : R<VAR>n : ℕ<GOAL>(ascPochhammer ℕ n).smeval r * (X + ↑n).smeval r = (ascPochhammer ℕ n).smeval r * (X + ↑n).smeval r
<VAR>r : ℝ≥0<VAR>p : ℝ<VAR>hp : 0 ≤ p<GOAL>r ≤ p.toNNReal ↔ ↑r ≤ p
<VAR>α : Type u<VAR>β : α → Type v<VAR>l l₁✝ l₂ : List (Sigma β)<VAR>inst✝ : DecidableEq α<VAR>l₀ l₁ : List (Sigma β)<VAR>nd₀ : l₀.NodupKeys<VAR>nd₁ : l₁.NodupKeys<VAR>h : ∀ (x : α) (y : β x), y ∈ dlookup x l₀ ↔ y ∈ dlookup x l₁<VAR>x✝ : Sigma β<VAR>a : α<VAR>b : β a<GOAL>⟨a, b⟩ ∈ l₀ ↔ ⟨a, b⟩ ∈ l₁
<VAR>R : Type u_1<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>n.divisors.card = ∏ x ∈ n.primeFactors, (n.factorization x + 1)
<VAR>R : Type u_1<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>(n.factorization.prod fun p k => (σ 0) (p ^ k)) = ∏ x ∈ n.primeFactors, (n.factorization x + 1)
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : Semiring A<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : Semiring B<VAR>inst✝ : Algebra R B<VAR>S : Subalgebra R A<VAR>h : S = ⊤<VAR>x : A<GOAL>x ∈ ⊤
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : Semiring A<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : Semiring B<VAR>inst✝ : Algebra R B<VAR>S : Subalgebra R A<VAR>h : ∀ (x : A), x ∈ S<VAR>x : A<GOAL>x ∈ S ↔ x ∈ ⊤
<VAR>x y : ℝ<VAR>hx : 0 ≤ x<VAR>hy : 0 ≤ y<GOAL>√x = y ↔ y ^ 2 = x
<VAR>R : Type u_1<VAR>inst✝¹³ : Ring R<VAR>R₂ : Type u_2<VAR>inst✝¹² : Ring R₂<VAR>R₃ : Type u_3<VAR>inst✝¹¹ : Ring R₃<VAR>M : Type u_4<VAR>inst✝¹⁰ : TopologicalSpace M<VAR>inst✝⁹ : AddCommGroup M<VAR>M₂ : Type u_5<VAR>inst✝⁸ : TopologicalSpace M₂<VAR>inst✝⁷ : AddCommGroup M₂<VAR>M₃ : Type u_6<VAR>inst✝⁶ : TopologicalSpace M₃<VAR>inst✝⁵ : AddCommGroup M₃<VAR>M₄ : Type u_7<VAR>inst✝⁴ : TopologicalSpace M₄<VAR>inst✝³ : AddCommGroup M₄<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R₂ M₂<VAR>inst✝ : Module R₃ M₃<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₃ : R₂ →+* R₃<VAR>σ₁₃ : R →+* R₃<VAR>f : M →SL[σ₁₂] M₂<VAR>x : M<GOAL>f (-x) = -f x
<VAR>n✝ b b' : ℕ<VAR>c : ℤ<VAR>h : ↑b' ≡ c [ZMOD ↑b]<VAR>n : ℕ<GOAL>↑(ofDigits b' (b'.digits n)) ≡ ofDigits c (b'.digits n) [ZMOD ↑b]
<VAR>n✝ b b' : ℕ<VAR>c : ℤ<VAR>h : ↑b' ≡ c [ZMOD ↑b]<VAR>n : ℕ<GOAL>ofDigits (↑b') (b'.digits n) ≡ ofDigits c (b'.digits n) [ZMOD ↑b]
<VAR>w x✝ y✝ z y : ℝ<VAR>hy : y ≠ 0<VAR>x : ℝ≥0<GOAL>(x ^ y) ^ (1 / y) = x
<VAR>V : Type u<VAR>W : Type v<VAR>G : SimpleGraph V<VAR>F : SimpleGraph W<VAR>inst✝ : Finite V<VAR>ι : Sort u_1<VAR>f : ι → G.Finsubgraph<GOAL>↑(⨆ i, f i) = ⨆ i, ↑(f i)
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>H : Type u_3<VAR>inst✝³ : _root_.RCLike 𝕜<VAR>inst✝² : NormedAddCommGroup H<VAR>inst✝¹ : NormedSpace 𝕜 H<VAR>inst✝ : Fintype ι<VAR>f : H → EuclideanSpace 𝕜 ι<VAR>f' : H →L[𝕜] EuclideanSpace 𝕜 ι<VAR>t : Set H<VAR>y : H<GOAL>HasStrictFDerivAt f f' y ↔ ∀ (i : ι), HasStrictFDerivAt (fun x => f x i) ((EuclideanSpace.proj i).comp f') y
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>H : Type u_3<VAR>inst✝³ : _root_.RCLike 𝕜<VAR>inst✝² : NormedAddCommGroup H<VAR>inst✝¹ : NormedSpace 𝕜 H<VAR>inst✝ : Fintype ι<VAR>f : H → EuclideanSpace 𝕜 ι<VAR>f' : H →L[𝕜] EuclideanSpace 𝕜 ι<VAR>t : Set H<VAR>y : H<GOAL>(∀ (i : ι), HasStrictFDerivAt (fun x => (⇑(EuclideanSpace.equiv ι 𝕜) ∘ f) x i) ((proj i).comp ((↑(EuclideanSpace.equiv ι 𝕜)).comp f')) y) ↔ ∀ (i : ι), HasStrictFDerivAt (fun x => f x i) ((EuclideanSpace.proj i).comp f') y
<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>n : ℕ<GOAL>derivative ↑n = 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>n : ℕ<GOAL>derivative (C ↑n) = 0
<VAR>E : Type u_1<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℂ E<VAR>V : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : FiniteDimensional ℝ V<VAR>inst✝¹ : MeasurableSpace V<VAR>inst✝ : BorelSpace V<VAR>f✝ : V → E<VAR>f : ℝ → E<VAR>hf : Integrable f volume<VAR>hf' : Integrable (fun x => x • f x) volume<VAR>w : ℝ<GOAL>HasDerivAt (𝓕 f) (𝓕 (fun x => (-2 * ↑π * I * ↑x) • f x) w) w
<VAR>E : Type u_1<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℂ E<VAR>V : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : FiniteDimensional ℝ V<VAR>inst✝¹ : MeasurableSpace V<VAR>inst✝ : BorelSpace V<VAR>f✝ : V → E<VAR>f : ℝ → E<VAR>hf : Integrable f volume<VAR>hf' : Integrable (fun x => x • f x) volume<VAR>w : ℝ<VAR>hf'' : Integrable (fun v => ‖v‖ * ‖f v‖) volume<GOAL>HasDerivAt (𝓕 f) (𝓕 (fun x => (-2 * ↑π * I * ↑x) • f x) w) w
<VAR>E : Type u_1<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℂ E<VAR>V : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : FiniteDimensional ℝ V<VAR>inst✝¹ : MeasurableSpace V<VAR>inst✝ : BorelSpace V<VAR>f✝ : V → E<VAR>f : ℝ → E<VAR>hf : Integrable f volume<VAR>hf' : Integrable (fun x => x • f x) volume<VAR>w : ℝ<VAR>hf'' : Integrable (fun v => ‖v‖ * ‖f v‖) volume<VAR>L : ℝ →L[ℝ] ℝ →L[ℝ] ℝ := ContinuousLinearMap.mul ℝ ℝ<GOAL>HasDerivAt (𝓕 f) (𝓕 (fun x => (-2 * ↑π * I * ↑x) • f x) w) w
<VAR>E : Type u_1<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℂ E<VAR>V : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : FiniteDimensional ℝ V<VAR>inst✝¹ : MeasurableSpace V<VAR>inst✝ : BorelSpace V<VAR>f✝ : V → E<VAR>f : ℝ → E<VAR>hf : Integrable f volume<VAR>hf' : Integrable (fun x => x • f x) volume<VAR>w : ℝ<VAR>hf'' : Integrable (fun v => ‖v‖ * ‖f v‖) volume<VAR>L : ℝ →L[ℝ] ℝ →L[ℝ] ℝ := ContinuousLinearMap.mul ℝ ℝ<VAR>h_int : Integrable (fun v => fourierSMulRight L f v) volume<GOAL>HasDerivAt (𝓕 f) (𝓕 (fun x => (-2 * ↑π * I * ↑x) • f x) w) w
<VAR>E : Type u_1<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℂ E<VAR>V : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : FiniteDimensional ℝ V<VAR>inst✝¹ : MeasurableSpace V<VAR>inst✝ : BorelSpace V<VAR>f✝ : V → E<VAR>f : ℝ → E<VAR>hf : Integrable f volume<VAR>hf' : Integrable (fun x => x • f x) volume<VAR>w : ℝ<VAR>hf'' : Integrable (fun v => ‖v‖ * ‖f v‖) volume<VAR>L : ℝ →L[ℝ] ℝ →L[ℝ] ℝ := ContinuousLinearMap.mul ℝ ℝ<VAR>h_int : Integrable (fun v => 𝐞 (-((LinearMap.mul ℝ ℝ) v) w) • fourierSMulRight L f v) volume<GOAL>HasDerivAt (𝓕 f) (𝓕 (fun x => (-2 * ↑π * I * ↑x) • f x) w) w
<VAR>E : Type u_1<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℂ E<VAR>V : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : FiniteDimensional ℝ V<VAR>inst✝¹ : MeasurableSpace V<VAR>inst✝ : BorelSpace V<VAR>f✝ : V → E<VAR>f : ℝ → E<VAR>hf : Integrable f volume<VAR>hf' : Integrable (fun x => x • f x) volume<VAR>w : ℝ<VAR>hf'' : Integrable (fun v => ‖v‖ * ‖f v‖) volume<VAR>L : ℝ →L[ℝ] ℝ →L[ℝ] ℝ := ContinuousLinearMap.mul ℝ ℝ<VAR>h_int : Integrable (fun v => 𝐞 (-((LinearMap.mul ℝ ℝ) v) w) • fourierSMulRight L f v) volume<GOAL>𝓕 (fun x => (-2 * ↑π * I * ↑x) • f x) w = (VectorFourier.fourierIntegral 𝐞 volume L.toLinearMap₂ (fourierSMulRight L f) w) 1
<VAR>E : Type u_1<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℂ E<VAR>V : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : FiniteDimensional ℝ V<VAR>inst✝¹ : MeasurableSpace V<VAR>inst✝ : BorelSpace V<VAR>f✝ : V → E<VAR>f : ℝ → E<VAR>hf : Integrable f volume<VAR>hf' : Integrable (fun x => x • f x) volume<VAR>w : ℝ<VAR>hf'' : Integrable (fun v => ‖v‖ * ‖f v‖) volume<VAR>L : ℝ →L[ℝ] ℝ →L[ℝ] ℝ := ContinuousLinearMap.mul ℝ ℝ<VAR>h_int : Integrable (fun v => 𝐞 (-((LinearMap.mul ℝ ℝ) v) w) • fourierSMulRight L f v) volume<GOAL>𝓕 (fun x => (-2 * ↑π * I * ↑x) • f x) w = ∫ (x : ℝ), (𝐞 (-((LinearMap.mul ℝ ℝ) x) w) • fourierSMulRight L f x) 1 ∂volume
<VAR>E : Type u_1<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℂ E<VAR>V : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : FiniteDimensional ℝ V<VAR>inst✝¹ : MeasurableSpace V<VAR>inst✝ : BorelSpace V<VAR>f✝ : V → E<VAR>f : ℝ → E<VAR>hf : Integrable f volume<VAR>hf' : Integrable (fun x => x • f x) volume<VAR>w : ℝ<VAR>hf'' : Integrable (fun v => ‖v‖ * ‖f v‖) volume<VAR>L : ℝ →L[ℝ] ℝ →L[ℝ] ℝ := ContinuousLinearMap.mul ℝ ℝ<VAR>h_int : Integrable (fun v => 𝐞 (-((LinearMap.mul ℝ ℝ) v) w) • fourierSMulRight L f v) volume<GOAL>𝓕 (fun x => -2 • ↑π • I • ↑x • f x) w = ∫ (x : ℝ), 𝐞 (-((LinearMap.mul ℝ ℝ) x) w) • -2 • ↑π • I • x • f x ∂volume
<VAR>step s m n : Nat<VAR>step0 : 0 < step<GOAL>range' s m step ⊆ range' s n step ↔ m ≤ n
<VAR>step s m n : Nat<VAR>step0 : 0 < step<VAR>h : range' s m step ⊆ range' s n step<VAR>hn : n < m<GOAL>False
<VAR>step s m n : Nat<VAR>step0 : 0 < step<VAR>h : range' s m step ⊆ range' s n step<VAR>hn : n < m<VAR>i : Nat<VAR>h' : i < n<VAR>e : s + step * n = s + step * i<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>σ : Type u_4<VAR>inst✝³ : Primcodable α<VAR>inst✝² : Primcodable β<VAR>inst✝¹ : Primcodable γ<VAR>inst✝ : Primcodable σ<VAR>f : α → Option β<VAR>g : α → β → σ<VAR>hf : Computable f<VAR>hg : Computable₂ g<GOAL>Computable fun a => Option.map (g a) (f a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>σ : Type u_4<VAR>inst✝³ : Primcodable α<VAR>inst✝² : Primcodable β<VAR>inst✝¹ : Primcodable γ<VAR>inst✝ : Primcodable σ<VAR>f : α → Option β<VAR>g : α → β → σ<VAR>hf : Computable f<VAR>hg : Computable₂ g<VAR>x✝ : α<GOAL>Option.map (g x✝) (f x✝) = (f x✝).bind fun b => Option.some (g x✝ b)
<VAR>α : Type u_1<VAR>inst✝¹¹ : TopologicalSpace α<VAR>inst✝¹⁰ : NormalSpace α<VAR>inst✝⁹ : R1Space α<VAR>inst✝⁸ : MeasurableSpace α<VAR>inst✝⁷ : BorelSpace α<VAR>E : Type u_2<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>μ : Measure α<VAR>p : ℝ≥0∞<VAR>inst✝⁵ : SecondCountableTopologyEither α E<VAR>_i : Fact (1 ≤ p)<VAR>hp : p ≠ ⊤<VAR>𝕜 : Type u_3<VAR>inst✝⁴ : NormedField 𝕜<VAR>inst✝³ : NormedAlgebra ℝ 𝕜<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : μ.WeaklyRegular<VAR>inst✝ : IsFiniteMeasure μ<VAR>this : NormedSpace ℝ E<GOAL>DenseRange ⇑(toLp p μ 𝕜)
<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>P : Submodule R M<VAR>b : Basis ι R ↥P<VAR>x : M<GOAL>x ∈ P ↔ ∃ c, x = c.sum fun i x => x • ↑(b 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>P : Submodule R M<VAR>b : Basis ι R ↥P<VAR>x : M<GOAL>x ∈ LinearMap.range (Finsupp.total ι M R (⇑P.subtype ∘ ⇑b)) ↔ ∃ c, x = c.sum fun i x => x • ↑(b i)
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>o : ℕ<VAR>p : R[X]<VAR>coeff_ne_zero : p.coeff o ≠ 0<VAR>h_natDeg_le : p.natDegree ≤ o<GOAL>p.natDegree = o
<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>m0 : MeasurableSpace α<VAR>inst✝³ : MeasurableSpace β<VAR>inst✝² : MeasurableSpace γ<VAR>μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s s' t : Set α<VAR>inst✝¹ : SemilatticeSup α<VAR>inst✝ : atTop.IsCountablyGenerated<VAR>μ : Measure α<GOAL>Tendsto (fun x => μ (Iic x)) atTop (𝓝 (μ univ))
<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>m0 : MeasurableSpace α<VAR>inst✝³ : MeasurableSpace β<VAR>inst✝² : MeasurableSpace γ<VAR>μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s s' t : Set α<VAR>inst✝¹ : SemilatticeSup α<VAR>inst✝ : atTop.IsCountablyGenerated<VAR>μ : Measure α<VAR>h✝ : IsEmpty α<GOAL>Tendsto (fun x => μ (Iic x)) atTop (𝓝 (μ univ))
<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>m0 : MeasurableSpace α<VAR>inst✝³ : MeasurableSpace β<VAR>inst✝² : MeasurableSpace γ<VAR>μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s s' t : Set α<VAR>inst✝¹ : SemilatticeSup α<VAR>inst✝ : atTop.IsCountablyGenerated<VAR>μ : Measure α<VAR>h✝ : Nonempty α<GOAL>Tendsto (fun x => μ (Iic x)) atTop (𝓝 (μ univ))