ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>inst✝⁶ : NontriviallyNormedField R<VAR>inst✝⁵ : (x : B) → AddCommMonoid (E x)<VAR>inst✝⁴ : (x : B) → Module R (E x)<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace R F<VAR>inst✝¹ : TopologicalSpace B<VAR>inst✝ : (x : B) → TopologicalSpace (E x)<VAR>a : VectorPrebundle R F E<VAR>this✝ : TopologicalSpace (TotalSpace F E) := a.totalSpaceTopology<VAR>this : FiberBundle F E := a.toFiberBundle<VAR>e : Pretrivialization F TotalSpace.proj<VAR>he : e ∈ a.toFiberPrebundle.pretrivializationAtlas<VAR>e' : Pretrivialization F TotalSpace.proj<VAR>he' : e' ∈ a.toFiberPrebundle.pretrivializationAtlas<VAR>b : B<VAR>hb : b ∈ e.baseSet ∩ e'.baseSet<VAR>v : F<GOAL>↑(Trivialization.coordChangeL R (a.toFiberPrebundle.trivializationOfMemPretrivializationAtlas he) (a.toFiberPrebundle.trivializationOfMemPretrivializationAtlas he') b) v = (a.coordChange he he' b) v
<VAR>R : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>inst✝⁶ : NontriviallyNormedField R<VAR>inst✝⁵ : (x : B) → AddCommMonoid (E x)<VAR>inst✝⁴ : (x : B) → Module R (E x)<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace R F<VAR>inst✝¹ : TopologicalSpace B<VAR>inst✝ : (x : B) → TopologicalSpace (E x)<VAR>a : VectorPrebundle R F E<VAR>this✝ : TopologicalSpace (TotalSpace F E) := a.totalSpaceTopology<VAR>this : FiberBundle F E := a.toFiberBundle<VAR>e : Pretrivialization F TotalSpace.proj<VAR>he : e ∈ a.toFiberPrebundle.pretrivializationAtlas<VAR>e' : Pretrivialization F TotalSpace.proj<VAR>he' : e' ∈ a.toFiberPrebundle.pretrivializationAtlas<VAR>b : B<VAR>hb : b ∈ e.baseSet ∩ e'.baseSet<VAR>v : F<VAR>h₁ : Trivialization.IsLinear R (a.trivializationOfMemPretrivializationAtlas he)<GOAL>↑(Trivialization.coordChangeL R (a.toFiberPrebundle.trivializationOfMemPretrivializationAtlas he) (a.toFiberPrebundle.trivializationOfMemPretrivializationAtlas he') b) v = (a.coordChange he he' b) v
<VAR>R : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>inst✝⁶ : NontriviallyNormedField R<VAR>inst✝⁵ : (x : B) → AddCommMonoid (E x)<VAR>inst✝⁴ : (x : B) → Module R (E x)<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace R F<VAR>inst✝¹ : TopologicalSpace B<VAR>inst✝ : (x : B) → TopologicalSpace (E x)<VAR>a : VectorPrebundle R F E<VAR>this✝ : TopologicalSpace (TotalSpace F E) := a.totalSpaceTopology<VAR>this : FiberBundle F E := a.toFiberBundle<VAR>e : Pretrivialization F TotalSpace.proj<VAR>he : e ∈ a.toFiberPrebundle.pretrivializationAtlas<VAR>e' : Pretrivialization F TotalSpace.proj<VAR>he' : e' ∈ a.toFiberPrebundle.pretrivializationAtlas<VAR>b : B<VAR>hb : b ∈ e.baseSet ∩ e'.baseSet<VAR>v : F<VAR>h₁ : Trivialization.IsLinear R (a.trivializationOfMemPretrivializationAtlas he)<VAR>h₂ : Trivialization.IsLinear R (a.trivializationOfMemPretrivializationAtlas he')<GOAL>↑(Trivialization.coordChangeL R (a.toFiberPrebundle.trivializationOfMemPretrivializationAtlas he) (a.toFiberPrebundle.trivializationOfMemPretrivializationAtlas he') b) v = (a.coordChange he he' b) v
<VAR>R : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>inst✝⁶ : NontriviallyNormedField R<VAR>inst✝⁵ : (x : B) → AddCommMonoid (E x)<VAR>inst✝⁴ : (x : B) → Module R (E x)<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace R F<VAR>inst✝¹ : TopologicalSpace B<VAR>inst✝ : (x : B) → TopologicalSpace (E x)<VAR>a : VectorPrebundle R F E<VAR>this✝ : TopologicalSpace (TotalSpace F E) := a.totalSpaceTopology<VAR>this : FiberBundle F E := a.toFiberBundle<VAR>e : Pretrivialization F TotalSpace.proj<VAR>he : e ∈ a.toFiberPrebundle.pretrivializationAtlas<VAR>e' : Pretrivialization F TotalSpace.proj<VAR>he' : e' ∈ a.toFiberPrebundle.pretrivializationAtlas<VAR>b : B<VAR>hb : b ∈ e.baseSet ∩ e'.baseSet<VAR>v : F<VAR>h₁ : Trivialization.IsLinear R (a.toFiberPrebundle.trivializationOfMemPretrivializationAtlas he)<VAR>h₂ : Trivialization.IsLinear R (a.toFiberPrebundle.trivializationOfMemPretrivializationAtlas he')<GOAL>↑(Trivialization.coordChangeL R (a.toFiberPrebundle.trivializationOfMemPretrivializationAtlas he) (a.toFiberPrebundle.trivializationOfMemPretrivializationAtlas he') b) v = (a.coordChange he he' b) v
<VAR>R : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>inst✝⁶ : NontriviallyNormedField R<VAR>inst✝⁵ : (x : B) → AddCommMonoid (E x)<VAR>inst✝⁴ : (x : B) → Module R (E x)<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace R F<VAR>inst✝¹ : TopologicalSpace B<VAR>inst✝ : (x : B) → TopologicalSpace (E x)<VAR>a : VectorPrebundle R F E<VAR>this✝ : TopologicalSpace (TotalSpace F E) := a.totalSpaceTopology<VAR>this : FiberBundle F E := a.toFiberBundle<VAR>e : Pretrivialization F TotalSpace.proj<VAR>he : e ∈ a.toFiberPrebundle.pretrivializationAtlas<VAR>e' : Pretrivialization F TotalSpace.proj<VAR>he' : e' ∈ a.toFiberPrebundle.pretrivializationAtlas<VAR>b : B<VAR>hb : b ∈ e.baseSet ∩ e'.baseSet<VAR>v : F<VAR>h₁ : Trivialization.IsLinear R (a.toFiberPrebundle.trivializationOfMemPretrivializationAtlas he)<VAR>h₂ : Trivialization.IsLinear R (a.toFiberPrebundle.trivializationOfMemPretrivializationAtlas he')<GOAL>(↑(a.toFiberPrebundle.trivializationOfMemPretrivializationAtlas he') { proj := b, snd := (a.toFiberPrebundle.trivializationOfMemPretrivializationAtlas he).symm b v }).2 = (↑e' { proj := b, snd := e.symm b v }).2
<VAR>R : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>inst✝⁶ : NontriviallyNormedField R<VAR>inst✝⁵ : (x : B) → AddCommMonoid (E x)<VAR>inst✝⁴ : (x : B) → Module R (E x)<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace R F<VAR>inst✝¹ : TopologicalSpace B<VAR>inst✝ : (x : B) → TopologicalSpace (E x)<VAR>a : VectorPrebundle R F E<VAR>this✝ : TopologicalSpace (TotalSpace F E) := a.totalSpaceTopology<VAR>this : FiberBundle F E := a.toFiberBundle<VAR>e : Pretrivialization F TotalSpace.proj<VAR>he : e ∈ a.toFiberPrebundle.pretrivializationAtlas<VAR>e' : Pretrivialization F TotalSpace.proj<VAR>he' : e' ∈ a.toFiberPrebundle.pretrivializationAtlas<VAR>b : B<VAR>hb : b ∈ e.baseSet ∩ e'.baseSet<VAR>v : F<VAR>h₁ : Trivialization.IsLinear R (a.toFiberPrebundle.trivializationOfMemPretrivializationAtlas he)<VAR>h₂ : Trivialization.IsLinear R (a.toFiberPrebundle.trivializationOfMemPretrivializationAtlas he')<GOAL>b ∈ (a.toFiberPrebundle.trivializationOfMemPretrivializationAtlas he).baseSet ∩ (a.toFiberPrebundle.trivializationOfMemPretrivializationAtlas he').baseSet
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>f✝ : ℂ → E<VAR>c : ℂ<VAR>r : ENNReal<VAR>hf✝ : DifferentiableOn ℂ f✝ (EMetric.ball c r)<VAR>z : ℂ<VAR>hz : z ∈ EMetric.ball c r<VAR>f : ℂ → ℂ<VAR>hf : DifferentiableOn ℂ f (EMetric.ball c r)<GOAL>∑' (n : ℕ), (↑n !)⁻¹ * iteratedDeriv n f c * (z - c) ^ n = f z
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>f✝ : ℂ → E<VAR>c : ℂ<VAR>r : ENNReal<VAR>hf✝ : DifferentiableOn ℂ f✝ (EMetric.ball c r)<VAR>z : ℂ<VAR>hz : z ∈ EMetric.ball c r<VAR>f : ℂ → ℂ<VAR>hf : DifferentiableOn ℂ f (EMetric.ball c r)<VAR>n : ℕ<GOAL>(↑n !)⁻¹ * iteratedDeriv n f c * (z - c) ^ n = (↑n !)⁻¹ • (z - c) ^ n • iteratedDeriv n f c
<VAR>R : Type u<VAR>S : Type v<VAR>k : Type y<VAR>A : Type z<VAR>a✝ b : R<VAR>n : ℕ<VAR>inst✝¹ : Field R<VAR>p q : R[X]<VAR>K : Type u_1<VAR>inst✝ : Field K<VAR>f : K[X]<VAR>a : K<GOAL>(X - C a) * (f /ₘ (X - C a)) = f - f %ₘ (X - C a)
<VAR>R : Type u<VAR>S : Type v<VAR>k : Type y<VAR>A : Type z<VAR>a✝ b : R<VAR>n : ℕ<VAR>inst✝¹ : Field R<VAR>p q : R[X]<VAR>K : Type u_1<VAR>inst✝ : Field K<VAR>f : K[X]<VAR>a : K<GOAL>(X - C a).Monic
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>M' : Type u_4<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : LieRing L<VAR>inst✝⁸ : LieAlgebra R L<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>inst✝³ : AddCommGroup M'<VAR>inst✝² : Module R M'<VAR>inst✝¹ : LieRingModule L M'<VAR>inst✝ : LieModule R L M'<VAR>N N₁ N₂ N' : LieSubmodule R L M<GOAL>⁅⊤, N⁆ ≤ N' ↔ N ≤ N'.normalizer
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>M' : Type u_4<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : LieRing L<VAR>inst✝⁸ : LieAlgebra R L<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>inst✝³ : AddCommGroup M'<VAR>inst✝² : Module R M'<VAR>inst✝¹ : LieRingModule L M'<VAR>inst✝ : LieModule R L M'<VAR>N N₁ N₂ N' : LieSubmodule R L M<GOAL>(∀ x ∈ ⊤, ∀ m ∈ N, ⁅x, m⁆ ∈ N') ↔ N ≤ N'.normalizer
<VAR>E : Type u_1<VAR>inst✝ : MeasurableSpace E<VAR>m μ : Measure E<VAR>Ω : Type u_2<VAR>x✝ : MeasurableSpace Ω<VAR>ℙ : Measure Ω<VAR>X : Ω → E<VAR>s : Set E<VAR>hms : MeasurableSet s<VAR>hu : IsUniform X s ℙ μ<VAR>hnt : ¬μ s = ⊤<VAR>hns : ¬μ s = 0<GOAL>pdf X ℙ μ =ᶠ[ae μ] s.indicator ((μ s)⁻¹ • 1)
<VAR>E : Type u_1<VAR>inst✝ : MeasurableSpace E<VAR>m μ : Measure E<VAR>Ω : Type u_2<VAR>x✝ : MeasurableSpace Ω<VAR>ℙ : Measure Ω<VAR>X : Ω → E<VAR>s : Set E<VAR>hms : MeasurableSet s<VAR>hu : IsUniform X s ℙ μ<VAR>hnt : ¬μ s = ⊤<VAR>hns : ¬μ s = 0<VAR>this : HasPDF X ℙ μ<GOAL>pdf X ℙ μ =ᶠ[ae μ] s.indicator ((μ s)⁻¹ • 1)
<VAR>E : Type u_1<VAR>inst✝ : MeasurableSpace E<VAR>m μ : Measure E<VAR>Ω : Type u_2<VAR>x✝ : MeasurableSpace Ω<VAR>ℙ : Measure Ω<VAR>X : Ω → E<VAR>s : Set E<VAR>hms : MeasurableSet s<VAR>hu : IsUniform X s ℙ μ<VAR>hnt : ¬μ s = ⊤<VAR>hns : ¬μ s = 0<VAR>this✝ : HasPDF X ℙ μ<VAR>this : IsProbabilityMeasure ℙ<GOAL>pdf X ℙ μ =ᶠ[ae μ] s.indicator ((μ s)⁻¹ • 1)
<VAR>E : Type u_1<VAR>inst✝ : MeasurableSpace E<VAR>m μ : Measure E<VAR>Ω : Type u_2<VAR>x✝ : MeasurableSpace Ω<VAR>ℙ : Measure Ω<VAR>X : Ω → E<VAR>s : Set E<VAR>hms : MeasurableSet s<VAR>hu : IsUniform X s ℙ μ<VAR>hnt : ¬μ s = ⊤<VAR>hns : ¬μ s = 0<VAR>this✝ : HasPDF X ℙ μ<VAR>this : IsProbabilityMeasure ℙ<GOAL>Measure.map X ℙ = μ.withDensity (s.indicator ((μ s)⁻¹ • 1))
<VAR>E : Type u_1<VAR>inst✝ : MeasurableSpace E<VAR>m μ : Measure E<VAR>Ω : Type u_2<VAR>x✝ : MeasurableSpace Ω<VAR>ℙ : Measure Ω<VAR>X : Ω → E<VAR>s : Set E<VAR>hms : MeasurableSet s<VAR>hu : IsUniform X s ℙ μ<VAR>hnt : ¬μ s = ⊤<VAR>hns : ¬μ s = 0<VAR>this✝ : HasPDF X ℙ μ<VAR>this : IsProbabilityMeasure ℙ<GOAL>AEMeasurable (s.indicator ((μ s)⁻¹ • 1)) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : Finite α<VAR>f : α → α<GOAL>Surjective f ↔ Bijective f
<VAR>ι : Type u_1<VAR>M : Type u_2<VAR>n : ℕ<VAR>I J : Box ι<VAR>i : ι<VAR>x : ℝ<VAR>y : ι → ℝ<VAR>h₁ : J ∈ split I i x<VAR>h₂ : y ∈ J<VAR>h₃ : x < y i<GOAL>↑J = ↑I ∩ {y | x < y i}
<VAR>ι : Type u_1<VAR>M : Type u_2<VAR>n : ℕ<VAR>I J : Box ι<VAR>i : ι<VAR>x : ℝ<VAR>y : ι → ℝ<VAR>h₁ : J ∈ split I i x<VAR>h₂ : y ∈ J<VAR>h₃ : x < y i<VAR>H : ↑J = ↑I ∩ {y | y i ≤ x}<GOAL>False
<VAR>ι : Type u_1<VAR>M : Type u_2<VAR>n : ℕ<VAR>I J : Box ι<VAR>i : ι<VAR>x : ℝ<VAR>y : ι → ℝ<VAR>h₁ : J ∈ split I i x<VAR>h₂ : y ∈ ↑I ∩ {y | y i ≤ x}<VAR>h₃ : x < y i<VAR>H : ↑J = ↑I ∩ {y | y i ≤ x}<GOAL>False
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>G : Type u_7<VAR>H : Type u_8<VAR>F : Type u_9<VAR>inst✝⁶ : MulOneClass M<VAR>inst✝⁵ : MulOneClass N<VAR>inst✝⁴ : FunLike F M N<VAR>inst✝³ : FunLike F G H<VAR>inst✝² : Group G<VAR>inst✝¹ : DivisionMonoid H<VAR>inst✝ : MonoidHomClass F G H<VAR>f : F<VAR>a b : G<GOAL>f (a * b⁻¹) = f a * (f b)⁻¹
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹⁴ : CommRing R<VAR>inst✝¹³ : AddCommGroup M<VAR>inst✝¹² : Module R M<VAR>I : Ideal R<VAR>S✝ : Type u_3<VAR>inst✝¹¹ : CommSemiring S✝<VAR>inst✝¹⁰ : Algebra S✝ R<VAR>inst✝⁹ : Module S✝ M<VAR>inst✝⁸ : IsScalarTower S✝ R M<VAR>R' : Type u_4<VAR>M' : Type u_5<VAR>inst✝⁷ : CommRing R'<VAR>inst✝⁶ : AddCommGroup M'<VAR>inst✝⁵ : Module R' M'<VAR>inst✝⁴ : Algebra R R'<VAR>inst✝³ : Module R M'<VAR>inst✝² : IsScalarTower R R' M'<VAR>S : Type u_6<VAR>inst✝¹ : CommRing S<VAR>inst✝ : Algebra S R<VAR>f : PolynomialModule S S<VAR>x : R<GOAL>(aeval x) (equivPolynomial f) = (eval x) ((map R (Algebra.linearMap S R)) f)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹⁴ : CommRing R<VAR>inst✝¹³ : AddCommGroup M<VAR>inst✝¹² : Module R M<VAR>I : Ideal R<VAR>S✝ : Type u_3<VAR>inst✝¹¹ : CommSemiring S✝<VAR>inst✝¹⁰ : Algebra S✝ R<VAR>inst✝⁹ : Module S✝ M<VAR>inst✝⁸ : IsScalarTower S✝ R M<VAR>R' : Type u_4<VAR>M' : Type u_5<VAR>inst✝⁷ : CommRing R'<VAR>inst✝⁶ : AddCommGroup M'<VAR>inst✝⁵ : Module R' M'<VAR>inst✝⁴ : Algebra R R'<VAR>inst✝³ : Module R M'<VAR>inst✝² : IsScalarTower R R' M'<VAR>S : Type u_6<VAR>inst✝¹ : CommRing S<VAR>inst✝ : Algebra S R<VAR>f : PolynomialModule S S<VAR>x : R<GOAL>(aeval x) (equivPolynomial 0) = (eval x) ((map R (Algebra.linearMap S R)) 0)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹⁴ : CommRing R<VAR>inst✝¹³ : AddCommGroup M<VAR>inst✝¹² : Module R M<VAR>I : Ideal R<VAR>S✝ : Type u_3<VAR>inst✝¹¹ : CommSemiring S✝<VAR>inst✝¹⁰ : Algebra S✝ R<VAR>inst✝⁹ : Module S✝ M<VAR>inst✝⁸ : IsScalarTower S✝ R M<VAR>R' : Type u_4<VAR>M' : Type u_5<VAR>inst✝⁷ : CommRing R'<VAR>inst✝⁶ : AddCommGroup M'<VAR>inst✝⁵ : Module R' M'<VAR>inst✝⁴ : Algebra R R'<VAR>inst✝³ : Module R M'<VAR>inst✝² : IsScalarTower R R' M'<VAR>S : Type u_6<VAR>inst✝¹ : CommRing S<VAR>inst✝ : Algebra S R<VAR>f : PolynomialModule S S<VAR>x : R<GOAL>∀ (f g : PolynomialModule S S), (aeval x) (equivPolynomial f) = (eval x) ((map R (Algebra.linearMap S R)) f) → (aeval x) (equivPolynomial g) = (eval x) ((map R (Algebra.linearMap S R)) g) → (aeval x) (equivPolynomial (f + g)) = (eval x) ((map R (Algebra.linearMap S R)) (f + g))
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹⁴ : CommRing R<VAR>inst✝¹³ : AddCommGroup M<VAR>inst✝¹² : Module R M<VAR>I : Ideal R<VAR>S✝ : Type u_3<VAR>inst✝¹¹ : CommSemiring S✝<VAR>inst✝¹⁰ : Algebra S✝ R<VAR>inst✝⁹ : Module S✝ M<VAR>inst✝⁸ : IsScalarTower S✝ R M<VAR>R' : Type u_4<VAR>M' : Type u_5<VAR>inst✝⁷ : CommRing R'<VAR>inst✝⁶ : AddCommGroup M'<VAR>inst✝⁵ : Module R' M'<VAR>inst✝⁴ : Algebra R R'<VAR>inst✝³ : Module R M'<VAR>inst✝² : IsScalarTower R R' M'<VAR>S : Type u_6<VAR>inst✝¹ : CommRing S<VAR>inst✝ : Algebra S R<VAR>f : PolynomialModule S S<VAR>x : R<GOAL>∀ (a : ℕ) (b : S), (aeval x) (equivPolynomial ((single S a) b)) = (eval x) ((map R (Algebra.linearMap S R)) ((single S a) b))
<VAR>R : Type u<VAR>S : Type v<VAR>F : Type u_1<VAR>inst✝³ : Ring R<VAR>inst✝² : Ring S<VAR>inst✝¹ : FunLike F R S<VAR>inst✝ : RingHomClass F R S<VAR>f : F<VAR>I✝ : Ideal R<VAR>hf : Function.Surjective ⇑f<VAR>I : Ideal R<VAR>r : R<VAR>h : f r ∈ map f I<VAR>s : R<VAR>hsi : s ∈ ↑I<VAR>hfsr : f s = f r<GOAL>f (r - s) = 0
<VAR>x : ℝ<GOAL>Tendsto (fun n => π * x * ∏ j ∈ Finset.range n, (1 - x ^ 2 / (↑j + 1) ^ 2)) atTop (𝓝 (sin (π * x)))
<VAR>x : ℝ<GOAL>(fun n => π * x * ∏ j ∈ Finset.range n, (1 - x ^ 2 / (↑j + 1) ^ 2)) = Complex.re ∘ fun n => ↑π * ↑x * ∏ j ∈ Finset.range n, (1 - ↑x ^ 2 / (↑j + 1) ^ 2)
<VAR>x : ℝ<GOAL>𝓝 (sin (π * x)) = 𝓝 (Complex.sin (↑π * ↑x)).re
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝⁴ : Field K<VAR>inst✝³ : LieRing L<VAR>inst✝² : LieAlgebra K L<VAR>inst✝¹ : Module.Finite K L<VAR>inst✝ : Infinite K<GOAL>∃ x, (engel K x).IsCartanSubalgebra
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝⁴ : Field K<VAR>inst✝³ : LieRing L<VAR>inst✝² : LieAlgebra K L<VAR>inst✝¹ : Module.Finite K L<VAR>inst✝ : Infinite K<GOAL>↑(finrank K L) ≤ #K
<VAR>Ω : Type u_1<VAR>inst✝⁵ : MeasurableSpace Ω<VAR>R : Type u_2<VAR>inst✝⁴ : SMul R ℝ≥0<VAR>inst✝³ : SMul R ℝ≥0∞<VAR>inst✝² : IsScalarTower R ℝ≥0 ℝ≥0∞<VAR>inst✝¹ : IsScalarTower R ℝ≥0∞ ℝ≥0∞<VAR>inst✝ : TopologicalSpace Ω<VAR>μ : FiniteMeasure Ω<GOAL>μ.testAgainstNN 0 = 0
<VAR>ι : Type u_1<VAR>V : Type u<VAR>inst✝¹¹ : Category.{v, u} V<VAR>inst✝¹⁰ : Preadditive V<VAR>W : Type u_2<VAR>inst✝⁹ : Category.{?u.143344, u_2} W<VAR>inst✝⁸ : Preadditive W<VAR>W₁ : Type u_3<VAR>W₂ : Type u_4<VAR>inst✝⁷ : Category.{u_6, u_3} W₁<VAR>inst✝⁶ : Category.{u_5, u_4} W₂<VAR>inst✝⁵ : HasZeroMorphisms W₁<VAR>inst✝⁴ : HasZeroMorphisms W₂<VAR>c✝ : ComplexShape ι<VAR>C D E : HomologicalComplex V c✝<VAR>f g : C ⟶ D<VAR>h k : D ⟶ E<VAR>i : ι<VAR>inst✝³ : HasZeroObject W₁<VAR>inst✝² : HasZeroObject W₂<VAR>F : W₁ ⥤ W₂<VAR>inst✝¹ : F.PreservesZeroMorphisms<VAR>c : ComplexShape ι<VAR>inst✝ : DecidableEq ι<VAR>j : ι<VAR>X : W₁<GOAL>((singleMapHomologicalComplex F c j).inv.app X).f j = (singleObjXSelf c j (F.obj X)).hom ≫ F.map (singleObjXSelf c j X).inv
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝³ : Countable ι<VAR>f✝ g : α → β<VAR>M : Type u_5<VAR>inst✝² : Monoid M<VAR>inst✝¹ : TopologicalSpace M<VAR>inst✝ : ContinuousMul M<VAR>m : MeasurableSpace α<VAR>f : α → M<VAR>l : List (α → M)<VAR>ihl : (∀ f ∈ l, StronglyMeasurable f) → StronglyMeasurable l.prod<VAR>hl : ∀ f_1 ∈ f :: l, StronglyMeasurable f_1<GOAL>StronglyMeasurable (f :: l).prod
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝³ : Countable ι<VAR>f✝ g : α → β<VAR>M : Type u_5<VAR>inst✝² : Monoid M<VAR>inst✝¹ : TopologicalSpace M<VAR>inst✝ : ContinuousMul M<VAR>m : MeasurableSpace α<VAR>f : α → M<VAR>l : List (α → M)<VAR>ihl : (∀ f ∈ l, StronglyMeasurable f) → StronglyMeasurable l.prod<VAR>hl : StronglyMeasurable f ∧ ∀ x ∈ l, StronglyMeasurable x<GOAL>StronglyMeasurable (f :: l).prod
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝³ : Countable ι<VAR>f✝ g : α → β<VAR>M : Type u_5<VAR>inst✝² : Monoid M<VAR>inst✝¹ : TopologicalSpace M<VAR>inst✝ : ContinuousMul M<VAR>m : MeasurableSpace α<VAR>f : α → M<VAR>l : List (α → M)<VAR>ihl : (∀ f ∈ l, StronglyMeasurable f) → StronglyMeasurable l.prod<VAR>hl : StronglyMeasurable f ∧ ∀ x ∈ l, StronglyMeasurable x<GOAL>StronglyMeasurable (f * l.prod)
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : LieRing L<VAR>inst✝⁸ : LieAlgebra R L<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : LieAlgebra K L<VAR>inst✝⁵ : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝⁴ : H.IsCartanSubalgebra<VAR>inst✝³ : IsTriangularizable K (↥H) L<VAR>inst✝² : IsKilling K L<VAR>inst✝¹ : CharZero K<VAR>inst✝ : Nontrivial L<GOAL>coroot 0 = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝ : ν.HaveLebesgueDecomposition μ<VAR>hμν : μ ≪ ν<GOAL>μ ≪ μ.withDensity (ν.rnDeriv μ)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝ : ν.HaveLebesgueDecomposition μ<VAR>hμν : μ ≪ ν.singularPart μ + μ.withDensity (ν.rnDeriv μ)<GOAL>μ ≪ μ.withDensity (ν.rnDeriv μ)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝ : ν.HaveLebesgueDecomposition μ<VAR>hμν : μ ≪ ν.singularPart μ + μ.withDensity (ν.rnDeriv μ)<VAR>s : Set α<VAR>x✝ : MeasurableSet s<VAR>hνs : (μ.withDensity (ν.rnDeriv μ)) s = 0<GOAL>μ s = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝ : ν.HaveLebesgueDecomposition μ<VAR>hμν : μ ≪ ν.singularPart μ + μ.withDensity (ν.rnDeriv μ)<VAR>s : Set α<VAR>x✝ : MeasurableSet s<VAR>hνs : (μ.withDensity (ν.rnDeriv μ)) s = 0<VAR>t : Set α<VAR>left✝ : MeasurableSet t<VAR>ht1 : (ν.singularPart μ) t = 0<VAR>ht2 : μ tᶜ = 0<GOAL>μ s = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝ : ν.HaveLebesgueDecomposition μ<VAR>hμν : μ ≪ ν.singularPart μ + μ.withDensity (ν.rnDeriv μ)<VAR>s : Set α<VAR>x✝ : MeasurableSet s<VAR>hνs : (μ.withDensity (ν.rnDeriv μ)) s = 0<VAR>t : Set α<VAR>left✝ : MeasurableSet t<VAR>ht1 : (ν.singularPart μ) t = 0<VAR>ht2 : μ tᶜ = 0<GOAL>μ (s ∩ ?intro.intro.intro ∪ s ∩ ?intro.intro.introᶜ) = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝ : ν.HaveLebesgueDecomposition μ<VAR>hμν : μ ≪ ν.singularPart μ + μ.withDensity (ν.rnDeriv μ)<VAR>s : Set α<VAR>x✝ : MeasurableSet s<VAR>hνs : (μ.withDensity (ν.rnDeriv μ)) s = 0<VAR>t : Set α<VAR>left✝ : MeasurableSet t<VAR>ht1 : (ν.singularPart μ) t = 0<VAR>ht2 : μ tᶜ = 0<GOAL>Set α
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝ : ν.HaveLebesgueDecomposition μ<VAR>hμν : μ ≪ ν.singularPart μ + μ.withDensity (ν.rnDeriv μ)<VAR>s : Set α<VAR>x✝ : MeasurableSet s<VAR>hνs : (μ.withDensity (ν.rnDeriv μ)) s = 0<VAR>t : Set α<VAR>left✝ : MeasurableSet t<VAR>ht1 : (ν.singularPart μ) t = 0<VAR>ht2 : μ tᶜ = 0<GOAL>μ (s ∩ t) + μ (s ∩ tᶜ) ≤ 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝ : ν.HaveLebesgueDecomposition μ<VAR>hμν : μ ≪ ν.singularPart μ + μ.withDensity (ν.rnDeriv μ)<VAR>s : Set α<VAR>x✝ : MeasurableSet s<VAR>hνs : (μ.withDensity (ν.rnDeriv μ)) s = 0<VAR>t : Set α<VAR>left✝ : MeasurableSet t<VAR>ht1 : (ν.singularPart μ) t = 0<VAR>ht2 : μ tᶜ = 0<GOAL>μ (s ∩ t) = 0 ∧ μ (s ∩ tᶜ) = 0
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : NormedSpace ℝ E<VAR>a b : ℝ<VAR>f g : ℝ → E<VAR>μ : Measure ℝ<VAR>hf : ¬AEStronglyMeasurable f (μ.restrict (Ι a b))<GOAL>∫ (x : ℝ) in a..b, f x ∂μ = 0
<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>E' : Type u_5<VAR>inst✝⁶ : NormedAddCommGroup E'<VAR>inst✝⁵ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝⁴ : TopologicalSpace H'<VAR>N : Type u_7<VAR>inst✝³ : TopologicalSpace N<VAR>inst✝² : ChartedSpace H' N<VAR>J : ModelWithCorners 𝕜 E' H'<VAR>inst✝¹ : SmoothManifoldWithCorners J N<VAR>x : M<VAR>y : N<VAR>inst✝ : I.Boundaryless<GOAL>(I.prod J).boundary (M × N) = univ.prod (J.boundary N)
<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>E' : Type u_5<VAR>inst✝⁶ : NormedAddCommGroup E'<VAR>inst✝⁵ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝⁴ : TopologicalSpace H'<VAR>N : Type u_7<VAR>inst✝³ : TopologicalSpace N<VAR>inst✝² : ChartedSpace H' N<VAR>J : ModelWithCorners 𝕜 E' H'<VAR>inst✝¹ : SmoothManifoldWithCorners J N<VAR>x : M<VAR>y : N<VAR>inst✝ : I.Boundaryless<GOAL>univ.prod (J.boundary N) ∪ ∅.prod univ = univ.prod (J.boundary N)
<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>E' : Type u_5<VAR>inst✝⁶ : NormedAddCommGroup E'<VAR>inst✝⁵ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝⁴ : TopologicalSpace H'<VAR>N : Type u_7<VAR>inst✝³ : TopologicalSpace N<VAR>inst✝² : ChartedSpace H' N<VAR>J : ModelWithCorners 𝕜 E' H'<VAR>inst✝¹ : SmoothManifoldWithCorners J N<VAR>x : M<VAR>y : N<VAR>inst✝ : I.Boundaryless<VAR>this : ∅.prod univ = ∅<GOAL>univ.prod (J.boundary N) ∪ ∅.prod univ = univ.prod (J.boundary N)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>inst✝⁷ : Preorder α<VAR>inst✝⁶ : Preorder β<VAR>inst✝⁵ : Preorder γ<VAR>inst✝⁴ : Preorder δ<VAR>inst✝³ : MulOneClass α<VAR>inst✝² : MulOneClass β<VAR>inst✝¹ : MulOneClass γ<VAR>inst✝ : MulOneClass δ<VAR>f✝ g✝ f g : α →*o β<VAR>h : f.toMonoidHom = g.toMonoidHom<GOAL>∀ (a : α), f a = g a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>L : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>inst✝⁷ : AddCommMonoid L<VAR>inst✝⁶ : TopologicalSpace L<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : TopologicalSpace M<VAR>inst✝³ : AddCommMonoid N<VAR>inst✝² : TopologicalSpace N<VAR>v✝ v₁ v₂ : VectorMeasure α M<VAR>w w₁ w₂ : VectorMeasure α N<VAR>inst✝¹ : T2Space N<VAR>inst✝ : ContinuousAdd M<VAR>u : Set α<VAR>hmu : MeasurableSet u<VAR>hu₁ : ∀ t ⊆ u, ↑v₁ t = 0<VAR>hu₂ : ∀ t ⊆ uᶜ, ↑w t = 0<VAR>v : Set α<VAR>hmv : MeasurableSet v<VAR>hv₁ : ∀ t ⊆ v, ↑v₂ t = 0<VAR>hv₂ : ∀ t ⊆ vᶜ, ↑w t = 0<GOAL>v₁ + v₂ ⟂ᵥ w