ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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)<VAR>hφ : AECover (μ.restrict (Iic b)) l φ<GOAL>Tendsto (fun i => ∫ (x : ℝ) in a i..b, f x ∂μ) l (𝓝 (∫ (x : ℝ) in Iic b, f x ∂μ))
<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)<VAR>hφ : AECover (μ.restrict (Iic b)) l φ<GOAL>(fun i => ∫ (x : ℝ) in φ i, f x ∂μ.restrict (Iic b)) =ᶠ[l] fun i => ∫ (x : ℝ) in a i..b, f x ∂μ
<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)<VAR>hφ : AECover (μ.restrict (Iic b)) l φ<VAR>i : ι<VAR>hai : a i ≤ b<GOAL>∫ (x : ℝ) in φ i, f x ∂μ.restrict (Iic b) = ∫ (x : ℝ) in a i..b, f x ∂μ
<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)<VAR>hφ : AECover (μ.restrict (Iic b)) l φ<VAR>i : ι<VAR>hai : a i ≤ b<GOAL>∫ (x : ℝ) in φ i ∩ Iic b, f x ∂μ = ∫ (x : ℝ) in Ioc (a i) b, f x ∂μ
<VAR>𝕜 : Type u<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f f₀ f₁ g : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x : 𝕜<VAR>s t : Set 𝕜<VAR>L : Filter 𝕜<VAR>hf : HasStrictDerivAt f f' x<VAR>hg : HasStrictDerivAt g g' x<GOAL>HasStrictDerivAt (fun y => f y + g y) (f' + g') x
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : HasShift C ℤ<VAR>T₁ T₂ T₃ A B : Triangle C<VAR>iso₁ : A.obj₁ ≅ B.obj₁<VAR>iso₂ : A.obj₂ ≅ B.obj₂<VAR>iso₃ : A.obj₃ ≅ B.obj₃<VAR>comm₁ : autoParam (A.mor₁ ≫ iso₂.hom = iso₁.hom ≫ B.mor₁) _auto✝<VAR>comm₂ : autoParam (A.mor₂ ≫ iso₃.hom = iso₂.hom ≫ B.mor₂) _auto✝<VAR>comm₃ : autoParam (A.mor₃ ≫ (shiftFunctor C 1).map iso₁.hom = iso₃.hom ≫ B.mor₃) _auto✝<GOAL>B.mor₁ ≫ iso₂.inv = iso₁.inv ≫ A.mor₁
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : HasShift C ℤ<VAR>T₁ T₂ T₃ A B : Triangle C<VAR>iso₁ : A.obj₁ ≅ B.obj₁<VAR>iso₂ : A.obj₂ ≅ B.obj₂<VAR>iso₃ : A.obj₃ ≅ B.obj₃<VAR>comm₁ : autoParam (A.mor₁ ≫ iso₂.hom = iso₁.hom ≫ B.mor₁) _auto✝<VAR>comm₂ : autoParam (A.mor₂ ≫ iso₃.hom = iso₂.hom ≫ B.mor₂) _auto✝<VAR>comm₃ : autoParam (A.mor₃ ≫ (shiftFunctor C 1).map iso₁.hom = iso₃.hom ≫ B.mor₃) _auto✝<GOAL>B.mor₂ ≫ iso₃.inv = iso₂.inv ≫ A.mor₂
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : HasShift C ℤ<VAR>T₁ T₂ T₃ A B : Triangle C<VAR>iso₁ : A.obj₁ ≅ B.obj₁<VAR>iso₂ : A.obj₂ ≅ B.obj₂<VAR>iso₃ : A.obj₃ ≅ B.obj₃<VAR>comm₁ : autoParam (A.mor₁ ≫ iso₂.hom = iso₁.hom ≫ B.mor₁) _auto✝<VAR>comm₂ : autoParam (A.mor₂ ≫ iso₃.hom = iso₂.hom ≫ B.mor₂) _auto✝<VAR>comm₃ : autoParam (A.mor₃ ≫ (shiftFunctor C 1).map iso₁.hom = iso₃.hom ≫ B.mor₃) _auto✝<GOAL>B.mor₃ ≫ (shiftFunctor C 1).map iso₁.inv = iso₃.inv ≫ A.mor₃
<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>α : ↥H → K<VAR>x : L<VAR>hx : x ∈ rootSpace H α<VAR>hx' : ∀ y ∈ rootSpace H (-α), ((killingForm K L) x) y = 0<GOAL>x ∈ LinearMap.ker (killingForm K L)
<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>α : ↥H → K<VAR>x : L<VAR>hx : x ∈ rootSpace H α<VAR>hx' : ∀ y ∈ rootSpace H (-α), ((killingForm K L) x) y = 0<GOAL>(killingForm K L) x = 0
<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>α : ↥H → K<VAR>x : L<VAR>hx : x ∈ rootSpace H α<VAR>hx' : ∀ y ∈ rootSpace H (-α), ((killingForm K L) x) y = 0<VAR>y : L<GOAL>((killingForm K L) x) y = 0 y
<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>α : ↥H → K<VAR>x : L<VAR>hx : x ∈ rootSpace H α<VAR>hx' : ∀ y ∈ rootSpace H (-α), ((killingForm K L) x) y = 0<VAR>y : L<VAR>hy : y ∈ ⨆ β, rootSpace H β<GOAL>((killingForm K L) x) y = 0 y
<VAR>K : Type u<VAR>inst✝ : Field K<VAR>x y : RatFunc K<GOAL>(x * y).denom ∣ x.denom * y.denom
<VAR>K : Type u<VAR>inst✝ : Field K<VAR>x y : RatFunc K<GOAL>∃ p, x * y = (algebraMap K[X] (RatFunc K)) p / (algebraMap K[X] (RatFunc K)) (x.denom * y.denom)
<VAR>a : UnitAddCircle<GOAL>Tendsto (fun s => s * completedHurwitzZetaEven a s) (𝓝[≠] 0) (𝓝 (if a = 0 then -1 else 0))
<VAR>a : UnitAddCircle<VAR>h1 : Tendsto (fun s => s * (hurwitzEvenFEPair a).Λ s) (𝓝[≠] 0) (𝓝 (-if a = 0 then 1 else 0))<GOAL>Tendsto (fun s => s * completedHurwitzZetaEven a s) (𝓝[≠] 0) (𝓝 (if a = 0 then -1 else 0))
<VAR>a : UnitAddCircle<VAR>h1 : Tendsto (fun s => s * (hurwitzEvenFEPair a).Λ s) (𝓝[≠] 0) (𝓝 (-if a = 0 then 1 else 0))<VAR>this : (-if a = 0 then 1 else 0) = if a = 0 then -1 else 0<GOAL>Tendsto (fun s => s * completedHurwitzZetaEven a s) (𝓝[≠] 0) (𝓝 (if a = 0 then -1 else 0))
<VAR>a : UnitAddCircle<VAR>this : (-if a = 0 then 1 else 0) = if a = 0 then -1 else 0<VAR>h1 : Tendsto (fun s => s * (hurwitzEvenFEPair a).Λ s) (𝓝[≠] 0) (𝓝 (if a = 0 then -1 else 0))<GOAL>Tendsto (fun s => s * completedHurwitzZetaEven a s) (𝓝[≠] 0) (𝓝 (if a = 0 then -1 else 0))
<VAR>a : UnitAddCircle<VAR>this : (-if a = 0 then 1 else 0) = if a = 0 then -1 else 0<VAR>h1 : Tendsto (fun s => s * (hurwitzEvenFEPair a).Λ s) (𝓝[≠] 0) (𝓝 (if a = 0 then -1 else 0))<VAR>s : ℂ<GOAL>((fun s => s * (hurwitzEvenFEPair a).Λ s) ∘ fun s => s / 2) s = s * completedHurwitzZetaEven a s
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>R : Type u_5<VAR>inst✝¹⁰ : MeasurableSpace X<VAR>inst✝⁹ : TopologicalSpace X<VAR>inst✝⁸ : MeasurableSpace Y<VAR>inst✝⁷ : TopologicalSpace Y<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>f✝ g✝ : X → E<VAR>μ : Measure X<VAR>s : Set X<VAR>inst✝⁴ : OpensMeasurableSpace X<VAR>A K : Set X<VAR>𝕜 : Type u_6<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : T2Space X<VAR>inst✝ : SecondCountableTopologyEither X 𝕜<VAR>g : X → E<VAR>hg : IntegrableOn g K μ<VAR>f : X → 𝕜<VAR>hf : ContinuousOn f K<VAR>hK : IsCompact K<GOAL>IntegrableOn (fun x => f x • g x) K μ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>R : Type u_5<VAR>inst✝¹⁰ : MeasurableSpace X<VAR>inst✝⁹ : TopologicalSpace X<VAR>inst✝⁸ : MeasurableSpace Y<VAR>inst✝⁷ : TopologicalSpace Y<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>f✝ g✝ : X → E<VAR>μ : Measure X<VAR>s : Set X<VAR>inst✝⁴ : OpensMeasurableSpace X<VAR>A K : Set X<VAR>𝕜 : Type u_6<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : T2Space X<VAR>inst✝ : SecondCountableTopologyEither X 𝕜<VAR>g : X → E<VAR>hg : IntegrableOn g K μ<VAR>f : X → 𝕜<VAR>hf : ContinuousOn f K<VAR>hK : IsCompact K<GOAL>Integrable (fun a => ‖f a • g a‖) (μ.restrict K)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>R : Type u_5<VAR>inst✝¹⁰ : MeasurableSpace X<VAR>inst✝⁹ : TopologicalSpace X<VAR>inst✝⁸ : MeasurableSpace Y<VAR>inst✝⁷ : TopologicalSpace Y<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>f✝ g✝ : X → E<VAR>μ : Measure X<VAR>s : Set X<VAR>inst✝⁴ : OpensMeasurableSpace X<VAR>A K : Set X<VAR>𝕜 : Type u_6<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : T2Space X<VAR>inst✝ : SecondCountableTopologyEither X 𝕜<VAR>g : X → E<VAR>hg : IntegrableOn g K μ<VAR>f : X → 𝕜<VAR>hf : ContinuousOn f K<VAR>hK : IsCompact K<GOAL>AEStronglyMeasurable (fun x => f x • g x) (μ.restrict K)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>xs✝ ys✝ : List α<VAR>n✝¹ n✝ : ℕ<VAR>xs ys : List α<VAR>h : xs <+ ys<VAR>n : ℕ<GOAL>List.sym (n + 1) [] <+ List.sym (n + 1) []
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>xs✝¹ ys✝ : List α<VAR>n✝¹ n✝ : ℕ<VAR>xs✝ ys : List α<VAR>h✝ : xs✝ <+ ys<VAR>xs : List α<VAR>n : ℕ<VAR>l₂✝ : List α<VAR>a : α<VAR>h : xs <+ l₂✝<GOAL>List.sym (n + 1) xs <+ List.sym (n + 1) (a :: l₂✝)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>xs✝¹ ys✝ : List α<VAR>n✝¹ n✝ : ℕ<VAR>xs✝ ys : List α<VAR>h✝ : xs✝ <+ ys<VAR>xs : List α<VAR>n : ℕ<VAR>l₂✝ : List α<VAR>a : α<VAR>h : xs <+ l₂✝<GOAL>[] ++ List.sym (n + 1) xs <+ List.map (fun p => a ::ₛ p) (List.sym n (a :: l₂✝)) ++ List.sym (n + 1) l₂✝
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>xs✝¹ ys✝ : List α<VAR>n✝¹ n✝ : ℕ<VAR>xs✝ ys : List α<VAR>h✝ : xs✝ <+ ys<VAR>xs : List α<VAR>n : ℕ<VAR>l₂✝ : List α<VAR>a : α<VAR>h : xs <+ l₂✝<GOAL>List.sym (n + 1) xs <+ List.sym (n + 1) l₂✝
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>xs✝ ys✝ : List α<VAR>n✝¹ n✝ : ℕ<VAR>xs ys : List α<VAR>h✝ : xs <+ ys<VAR>n : ℕ<VAR>l₁✝ l₂✝ : List α<VAR>a : α<VAR>h : l₁✝ <+ l₂✝<GOAL>List.map (fun p => a ::ₛ p) (List.sym n (a :: l₁✝)) ++ List.sym (n + 1) l₁✝ <+ List.map (fun p => a ::ₛ p) (List.sym n (a :: l₂✝)) ++ List.sym (n + 1) l₂✝
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>xs✝ ys✝ : List α<VAR>n✝¹ n✝ : ℕ<VAR>xs ys : List α<VAR>h✝ : xs <+ ys<VAR>n : ℕ<VAR>l₁✝ l₂✝ : List α<VAR>a : α<VAR>h : l₁✝ <+ l₂✝<GOAL>List.map (fun p => a ::ₛ p) (List.sym n (a :: l₁✝)) <+ List.map (fun p => a ::ₛ p) (List.sym n (a :: l₂✝))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>xs✝ ys✝ : List α<VAR>n✝¹ n✝ : ℕ<VAR>xs ys : List α<VAR>h✝ : xs <+ ys<VAR>n : ℕ<VAR>l₁✝ l₂✝ : List α<VAR>a : α<VAR>h : l₁✝ <+ l₂✝<GOAL>List.sym (n + 1) l₁✝ <+ List.sym (n + 1) l₂✝
<VAR>R : Type u_1<VAR>inst✝¹⁷ : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M'' : Type u_4<VAR>inst✝¹⁶ : AddCommMonoid M<VAR>inst✝¹⁵ : AddCommMonoid M'<VAR>inst✝¹⁴ : AddCommMonoid M''<VAR>A : Type u_5<VAR>inst✝¹³ : CommSemiring A<VAR>inst✝¹² : Algebra R A<VAR>inst✝¹¹ : Module A M'<VAR>inst✝¹⁰ : IsLocalization S A<VAR>inst✝⁹ : Module R M<VAR>inst✝⁸ : Module R M'<VAR>inst✝⁷ : Module R M''<VAR>inst✝⁶ : IsScalarTower R A M'<VAR>f : M →ₗ[R] M'<VAR>g✝ : M →ₗ[R] M''<VAR>inst✝⁵ : IsLocalizedModule S f<VAR>N : Type u_6<VAR>N' : Type u_7<VAR>inst✝⁴ : AddCommGroup N<VAR>inst✝³ : AddCommGroup N'<VAR>inst✝² : Module R N<VAR>inst✝¹ : Module R N'<VAR>g : N →ₗ[R] N'<VAR>inst✝ : IsLocalizedModule S g<VAR>h : M →ₗ[R] N<VAR>x : M<VAR>s : ↥S<GOAL>((map S f g) h) (mk' f x s) = mk' g (h x) s
<VAR>R : Type u_1<VAR>inst✝¹⁷ : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M'' : Type u_4<VAR>inst✝¹⁶ : AddCommMonoid M<VAR>inst✝¹⁵ : AddCommMonoid M'<VAR>inst✝¹⁴ : AddCommMonoid M''<VAR>A : Type u_5<VAR>inst✝¹³ : CommSemiring A<VAR>inst✝¹² : Algebra R A<VAR>inst✝¹¹ : Module A M'<VAR>inst✝¹⁰ : IsLocalization S A<VAR>inst✝⁹ : Module R M<VAR>inst✝⁸ : Module R M'<VAR>inst✝⁷ : Module R M''<VAR>inst✝⁶ : IsScalarTower R A M'<VAR>f : M →ₗ[R] M'<VAR>g✝ : M →ₗ[R] M''<VAR>inst✝⁵ : IsLocalizedModule S f<VAR>N : Type u_6<VAR>N' : Type u_7<VAR>inst✝⁴ : AddCommGroup N<VAR>inst✝³ : AddCommGroup N'<VAR>inst✝² : Module R N<VAR>inst✝¹ : Module R N'<VAR>g : N →ₗ[R] N'<VAR>inst✝ : IsLocalizedModule S g<VAR>h : M →ₗ[R] N<VAR>x : M<VAR>s : ↥S<GOAL>(LocalizedModule.lift S (g ∘ₗ h) ⋯) ((iso S f).symm (mk' f x s)) = mk' g (h x) s
<VAR>R : Type u_1<VAR>inst✝¹⁷ : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M'' : Type u_4<VAR>inst✝¹⁶ : AddCommMonoid M<VAR>inst✝¹⁵ : AddCommMonoid M'<VAR>inst✝¹⁴ : AddCommMonoid M''<VAR>A : Type u_5<VAR>inst✝¹³ : CommSemiring A<VAR>inst✝¹² : Algebra R A<VAR>inst✝¹¹ : Module A M'<VAR>inst✝¹⁰ : IsLocalization S A<VAR>inst✝⁹ : Module R M<VAR>inst✝⁸ : Module R M'<VAR>inst✝⁷ : Module R M''<VAR>inst✝⁶ : IsScalarTower R A M'<VAR>f : M →ₗ[R] M'<VAR>g✝ : M →ₗ[R] M''<VAR>inst✝⁵ : IsLocalizedModule S f<VAR>N : Type u_6<VAR>N' : Type u_7<VAR>inst✝⁴ : AddCommGroup N<VAR>inst✝³ : AddCommGroup N'<VAR>inst✝² : Module R N<VAR>inst✝¹ : Module R N'<VAR>g : N →ₗ[R] N'<VAR>inst✝ : IsLocalizedModule S g<VAR>h : M →ₗ[R] N<VAR>x : M<VAR>s : ↥S<GOAL>↑⋯.unit⁻¹ ((g ∘ₗ h) x) = mk' g (h x) s
<VAR>s : Set Surreal<VAR>inst✝ : Small.{u, u + 1} ↑s<GOAL>BddAbove s
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>f : α → β → α<VAR>a : α<VAR>l : List β<VAR>L : List (List β)<GOAL>foldl f a (l :: L).join = foldl (foldl f) a (l :: L)
<VAR>n : Nat<GOAL>iota (n + 1) = (range' 1 (n + 1)).reverse
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>x y : E<GOAL>⟪x, y⟫_𝕜 = 0 ↔ ⟪y, x⟫_𝕜 = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>x y : E<GOAL>(starRingEnd 𝕜) ⟪y, x⟫_𝕜 = 0 ↔ ⟪y, x⟫_𝕜 = 0
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>I J : Ideal R<VAR>f : R →+* S<VAR>hf : Function.Injective ⇑f<VAR>p : Ideal R<VAR>H : p ∈ minimalPrimes R<GOAL>∃ p', p'.IsPrime ∧ comap f p' = p
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>I J : Ideal R<VAR>f : R →+* S<VAR>hf : Function.Injective ⇑f<VAR>p : Ideal R<VAR>H : p ∈ minimalPrimes R<VAR>this : p.IsPrime<GOAL>∃ p', p'.IsPrime ∧ comap f p' = p
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>I J : Ideal R<VAR>f : R →+* S<VAR>hf : Function.Injective ⇑f<VAR>p : Ideal R<VAR>H : p ∈ minimalPrimes R<VAR>this✝ : p.IsPrime<VAR>this : Nontrivial (Localization (Submonoid.map f p.primeCompl))<GOAL>∃ p', p'.IsPrime ∧ comap f p' = p
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>I J : Ideal R<VAR>f : R →+* S<VAR>hf : Function.Injective ⇑f<VAR>p : Ideal R<VAR>H : p ∈ minimalPrimes R<VAR>this✝ : p.IsPrime<VAR>this : Nontrivial (Localization (Submonoid.map f p.primeCompl))<VAR>M : Ideal (Localization (Submonoid.map f p.primeCompl))<VAR>hM : M.IsMaximal<GOAL>∃ p', p'.IsPrime ∧ comap f p' = p
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>I J : Ideal R<VAR>f : R →+* S<VAR>hf : Function.Injective ⇑f<VAR>p : Ideal R<VAR>H : p ∈ minimalPrimes R<VAR>this✝ : p.IsPrime<VAR>this : Nontrivial (Localization (Submonoid.map f p.primeCompl))<VAR>M : Ideal (Localization (Submonoid.map f p.primeCompl))<VAR>hM : M.IsMaximal<GOAL>comap f (comap (algebraMap S (Localization (Submonoid.map f p.primeCompl))) M) = p
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>I J : Ideal R<VAR>f : R →+* S<VAR>hf : Function.Injective ⇑f<VAR>p : Ideal R<VAR>H : p ∈ minimalPrimes R<VAR>this✝ : p.IsPrime<VAR>this : Nontrivial (Localization (Submonoid.map f p.primeCompl))<VAR>M : Ideal (Localization (Submonoid.map f p.primeCompl))<VAR>hM : M.IsMaximal<GOAL>comap (algebraMap R (Localization p.primeCompl)) (comap (IsLocalization.map (Localization (Submonoid.map f p.primeCompl)) f ⋯) M) = p
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>I J : Ideal R<VAR>f : R →+* S<VAR>hf : Function.Injective ⇑f<VAR>p : Ideal R<VAR>H : p ∈ minimalPrimes R<VAR>this✝ : p.IsPrime<VAR>this : Nontrivial (Localization (Submonoid.map f p.primeCompl))<VAR>M : Ideal (Localization (Submonoid.map f p.primeCompl))<VAR>hM : M.IsMaximal<GOAL>comap (algebraMap R (Localization p.primeCompl)) (comap (IsLocalization.map (Localization (Submonoid.map f p.primeCompl)) f ⋯) M) ≤ p
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>I J : Ideal R<VAR>f : R →+* S<VAR>hf : Function.Injective ⇑f<VAR>p : Ideal R<VAR>H : p ∈ minimalPrimes R<VAR>this✝ : p.IsPrime<VAR>this : Nontrivial (Localization (Submonoid.map f p.primeCompl))<VAR>M : Ideal (Localization (Submonoid.map f p.primeCompl))<VAR>hM : M.IsMaximal<VAR>x : R<VAR>hx : x ∈ comap (algebraMap R (Localization p.primeCompl)) (comap (IsLocalization.map (Localization (Submonoid.map f p.primeCompl)) f ⋯) M)<GOAL>x ∈ p
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>I J : Ideal R<VAR>f : R →+* S<VAR>hf : Function.Injective ⇑f<VAR>p : Ideal R<VAR>H : p ∈ minimalPrimes R<VAR>this✝ : p.IsPrime<VAR>this : Nontrivial (Localization (Submonoid.map f p.primeCompl))<VAR>M : Ideal (Localization (Submonoid.map f p.primeCompl))<VAR>hM : M.IsMaximal<VAR>x : R<VAR>hx : x ∈ comap (algebraMap R (Localization p.primeCompl)) (comap (IsLocalization.map (Localization (Submonoid.map f p.primeCompl)) f ⋯) M)<VAR>h : x ∉ p<GOAL>False
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>I J : Ideal R<VAR>f : R →+* S<VAR>hf : Function.Injective ⇑f<VAR>p : Ideal R<VAR>H : p ∈ minimalPrimes R<VAR>this✝ : p.IsPrime<VAR>this : Nontrivial (Localization (Submonoid.map f p.primeCompl))<VAR>M : Ideal (Localization (Submonoid.map f p.primeCompl))<VAR>hM : M.IsMaximal<VAR>x : R<VAR>hx : x ∈ comap (algebraMap R (Localization p.primeCompl)) (comap (IsLocalization.map (Localization (Submonoid.map f p.primeCompl)) f ⋯) M)<VAR>h : x ∉ p<GOAL>M = ⊤
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>I J : Ideal R<VAR>f : R →+* S<VAR>hf : Function.Injective ⇑f<VAR>p : Ideal R<VAR>H : p ∈ minimalPrimes R<VAR>this✝ : p.IsPrime<VAR>this : Nontrivial (Localization (Submonoid.map f p.primeCompl))<VAR>M : Ideal (Localization (Submonoid.map f p.primeCompl))<VAR>hM : M.IsMaximal<VAR>x : R<VAR>hx : x ∈ comap (algebraMap R (Localization p.primeCompl)) (comap (IsLocalization.map (Localization (Submonoid.map f p.primeCompl)) f ⋯) M)<VAR>h : x ∉ p<GOAL>IsUnit ((IsLocalization.map (Localization (Submonoid.map f p.primeCompl)) f ⋯) ((algebraMap R (Localization p.primeCompl)) x))
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>I J : Ideal R<VAR>f : R →+* S<VAR>hf : Function.Injective ⇑f<VAR>p : Ideal R<VAR>H : p ∈ minimalPrimes R<VAR>this✝ : p.IsPrime<VAR>this : Nontrivial (Localization (Submonoid.map f p.primeCompl))<VAR>M : Ideal (Localization (Submonoid.map f p.primeCompl))<VAR>hM : M.IsMaximal<VAR>x : R<VAR>hx : x ∈ comap (algebraMap R (Localization p.primeCompl)) (comap (IsLocalization.map (Localization (Submonoid.map f p.primeCompl)) f ⋯) M)<VAR>h : x ∉ p<GOAL>IsUnit ((algebraMap R (Localization p.primeCompl)) x)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>hst : μ s = μ t<VAR>x : F<GOAL>(weightedSMul μ s) x = (weightedSMul μ t) x
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>hst : μ s = μ t<VAR>x : F<GOAL>(μ s).toReal • x = (μ t).toReal • x
<VAR>f : ℝ → ℝ<VAR>hf : Monotone f<GOAL>∀ᵐ (x : ℝ), HasDerivAt f (hf.stieltjesFunction.measure.rnDeriv volume x).toReal x
<VAR>f : ℝ → ℝ<VAR>hf : Monotone f<VAR>x : ℝ<VAR>hx : HasDerivAt (↑hf.stieltjesFunction) (hf.stieltjesFunction.measure.rnDeriv volume x).toReal x<VAR>h'x : ¬¬ContinuousAt f x<GOAL>HasDerivAt f (hf.stieltjesFunction.measure.rnDeriv volume x).toReal x
<VAR>f : ℝ → ℝ<VAR>hf : Monotone f<VAR>x : ℝ<VAR>hx : HasDerivAt (↑hf.stieltjesFunction) (hf.stieltjesFunction.measure.rnDeriv volume x).toReal x<VAR>h'x : ¬¬ContinuousAt f x<VAR>A : ↑hf.stieltjesFunction x = f x<GOAL>HasDerivAt f (hf.stieltjesFunction.measure.rnDeriv volume x).toReal x
<VAR>f : ℝ → ℝ<VAR>hf : Monotone f<VAR>x : ℝ<VAR>hx : Tendsto (fun b => (↑hf.stieltjesFunction b - f x) / (b - x)) (𝓝[<] x) (𝓝 (hf.stieltjesFunction.measure.rnDeriv volume x).toReal) ∧ Tendsto (fun b => (↑hf.stieltjesFunction b - f x) / (b - x)) (𝓝[>] x) (𝓝 (hf.stieltjesFunction.measure.rnDeriv volume x).toReal)<VAR>h'x : ¬¬ContinuousAt f x<VAR>A : ↑hf.stieltjesFunction x = f x<GOAL>HasDerivAt f (hf.stieltjesFunction.measure.rnDeriv volume x).toReal x
<VAR>f : ℝ → ℝ<VAR>hf : Monotone f<VAR>x : ℝ<VAR>hx : Tendsto (fun b => (↑hf.stieltjesFunction b - f x) / (b - x)) (𝓝[<] x) (𝓝 (hf.stieltjesFunction.measure.rnDeriv volume x).toReal) ∧ Tendsto (fun b => (↑hf.stieltjesFunction b - f x) / (b - x)) (𝓝[>] x) (𝓝 (hf.stieltjesFunction.measure.rnDeriv volume x).toReal)<VAR>h'x : ¬¬ContinuousAt f x<VAR>A : ↑hf.stieltjesFunction x = f x<VAR>L1 : Tendsto (fun y => (f y - f x) / (y - x)) (𝓝[>] x) (𝓝 (hf.stieltjesFunction.measure.rnDeriv volume x).toReal)<VAR>L2 : Tendsto (fun y => (f y - f x) / (y - x)) (𝓝[<] x) (𝓝 (hf.stieltjesFunction.measure.rnDeriv volume x).toReal)<GOAL>HasDerivAt f (hf.stieltjesFunction.measure.rnDeriv volume x).toReal x
<VAR>f : ℝ → ℝ<VAR>hf : Monotone f<VAR>x : ℝ<VAR>hx : Tendsto (fun b => (↑hf.stieltjesFunction b - f x) / (b - x)) (𝓝[<] x) (𝓝 (hf.stieltjesFunction.measure.rnDeriv volume x).toReal) ∧ Tendsto (fun b => (↑hf.stieltjesFunction b - f x) / (b - x)) (𝓝[>] x) (𝓝 (hf.stieltjesFunction.measure.rnDeriv volume x).toReal)<VAR>h'x : ¬¬ContinuousAt f x<VAR>A : ↑hf.stieltjesFunction x = f x<VAR>L1 : Tendsto (fun y => (f y - f x) / (y - x)) (𝓝[>] x) (𝓝 (hf.stieltjesFunction.measure.rnDeriv volume x).toReal)<VAR>L2 : Tendsto (fun y => (f y - f x) / (y - x)) (𝓝[<] x) (𝓝 (hf.stieltjesFunction.measure.rnDeriv volume x).toReal)<GOAL>Tendsto (fun b => (f b - f x) / (b - x)) (𝓝[<] x) (𝓝 (hf.stieltjesFunction.measure.rnDeriv volume x).toReal) ∧ Tendsto (fun b => (f b - f x) / (b - x)) (𝓝[>] x) (𝓝 (hf.stieltjesFunction.measure.rnDeriv volume x).toReal)
<VAR>ι✝ : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝² : EMetricSpace X<VAR>inst✝¹ : EMetricSpace Y<VAR>ι : Sort u_4<VAR>inst✝ : Countable ι<VAR>s : ι → Set X<VAR>this✝¹ : MeasurableSpace X := borel X<VAR>this✝ : BorelSpace X<GOAL>dimH (⋃ i, s i) = ⨆ i, dimH (s i)
<VAR>ι✝ : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝² : EMetricSpace X<VAR>inst✝¹ : EMetricSpace Y<VAR>ι : Sort u_4<VAR>inst✝ : Countable ι<VAR>s : ι → Set X<VAR>this✝¹ : MeasurableSpace X := borel X<VAR>this✝ : BorelSpace X<VAR>d : ℝ≥0<VAR>hd : μH[↑d] (⋃ i, s i) = ⊤<GOAL>↑d ≤ ⨆ i, dimH (s i)
<VAR>ι✝ : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝² : EMetricSpace X<VAR>inst✝¹ : EMetricSpace Y<VAR>ι : Sort u_4<VAR>inst✝ : Countable ι<VAR>s : ι → Set X<VAR>this✝¹ : MeasurableSpace X := borel X<VAR>this✝ : BorelSpace X<VAR>d : ℝ≥0<VAR>hd : ⨆ i, dimH (s i) < ↑d<GOAL>μH[↑d] (⋃ i, s i) ≠ ⊤
<VAR>ι✝ : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝² : EMetricSpace X<VAR>inst✝¹ : EMetricSpace Y<VAR>ι : Sort u_4<VAR>inst✝ : Countable ι<VAR>s : ι → Set X<VAR>this✝¹ : MeasurableSpace X := borel X<VAR>this✝ : BorelSpace X<VAR>d : ℝ≥0<VAR>hd : ⨆ i, dimH (s i) < ↑d<VAR>this : ∀ (i : ι), μH[↑d] (s i) = 0<GOAL>μH[↑d] (⋃ i, s i) ≠ ⊤