ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>inst✝⁶ : CommRing A<VAR>S : Submonoid A<VAR>hS : S ≤ A⁰<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : Algebra A K<VAR>inst✝³ : IsFractionRing A K<VAR>B : Type u_3<VAR>inst✝² : CommRing B<VAR>inst✝¹ : Algebra A B<VAR>inst✝ : IsLocalization S B<VAR>x : K<VAR>x✝² x✝¹ : A<VAR>x✝ : x✝¹ ∈ S<GOAL>((algebraMap A K) x✝¹)⁻¹ = ↑((IsUnit.liftRight ((IsLocalization.toLocalizationMap A⁰ K).toMap.restrict A⁰) ⋯) ⟨x✝¹, ⋯⟩)⁻¹
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>inst✝⁶ : CommRing A<VAR>S : Submonoid A<VAR>hS : S ≤ A⁰<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : Algebra A K<VAR>inst✝³ : IsFractionRing A K<VAR>B : Type u_3<VAR>inst✝² : CommRing B<VAR>inst✝¹ : Algebra A B<VAR>inst✝ : IsLocalization S B<VAR>x : K<VAR>x✝² x✝¹ : A<VAR>x✝ : x✝¹ ∈ S<GOAL>((algebraMap A K) x✝¹)⁻¹ = (↑((IsUnit.liftRight ((IsLocalization.toLocalizationMap A⁰ K).toMap.restrict A⁰) ⋯) ⟨x✝¹, ⋯⟩))⁻¹
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : NormedAddCommGroup F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : NormedAddCommGroup G<VAR>m✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>T : Set α → F →L[ℝ] F'<VAR>hT_empty : T ∅ = 0<VAR>m : MeasurableSpace α<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>x : F<GOAL>setToSimpleFunc T (piecewise s hs (const α x) (const α 0)) = (T s) x
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : NormedAddCommGroup F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : NormedAddCommGroup G<VAR>m✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>T : Set α → F →L[ℝ] F'<VAR>hT_empty : T ∅ = 0<VAR>m : MeasurableSpace α<VAR>x : F<VAR>hs : MeasurableSet ∅<GOAL>setToSimpleFunc T (piecewise ∅ hs (const α x) (const α 0)) = (T ∅) x
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : NormedAddCommGroup F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : NormedAddCommGroup G<VAR>m✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>T : Set α → F →L[ℝ] F'<VAR>hT_empty : T ∅ = 0<VAR>m : MeasurableSpace α<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>x : F<VAR>hs_empty : s.Nonempty<GOAL>setToSimpleFunc T (piecewise s hs (const α x) (const α 0)) = (T s) x
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : NormedAddCommGroup F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : NormedAddCommGroup G<VAR>m✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>T : Set α → F →L[ℝ] F'<VAR>hT_empty : T ∅ = 0<VAR>m : MeasurableSpace α<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>x : F<VAR>hs_empty : s.Nonempty<GOAL>∑ x_1 ∈ (piecewise s hs (const α x) (const α 0)).range, (T (↑(piecewise s hs (const α x) (const α 0)) ⁻¹' {x_1})) x_1 = (T s) x
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : NormedAddCommGroup F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : NormedAddCommGroup G<VAR>m✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>T : Set α → F →L[ℝ] F'<VAR>hT_empty : T ∅ = 0<VAR>m : MeasurableSpace α<VAR>x : F<VAR>hs : MeasurableSet Set.univ<VAR>hs_empty : Set.univ.Nonempty<GOAL>∑ x_1 ∈ (piecewise Set.univ hs (const α x) (const α 0)).range, (T (↑(piecewise Set.univ hs (const α x) (const α 0)) ⁻¹' {x_1})) x_1 = (T Set.univ) x
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : NormedAddCommGroup F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : NormedAddCommGroup G<VAR>m✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>T : Set α → F →L[ℝ] F'<VAR>hT_empty : T ∅ = 0<VAR>m : MeasurableSpace α<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>x : F<VAR>hs_empty : s.Nonempty<VAR>hs_univ : s ≠ Set.univ<GOAL>∑ x_1 ∈ (piecewise s hs (const α x) (const α 0)).range, (T (↑(piecewise s hs (const α x) (const α 0)) ⁻¹' {x_1})) x_1 = (T s) x
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : NormedAddCommGroup F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : NormedAddCommGroup G<VAR>m✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>T : Set α → F →L[ℝ] F'<VAR>hT_empty : T ∅ = 0<VAR>m : MeasurableSpace α<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>x : F<VAR>hs_empty : s.Nonempty<VAR>hs_univ : s ≠ Set.univ<GOAL>∑ x_1 ∈ {x, 0}, (T (↑(piecewise s hs (const α x) (const α 0)) ⁻¹' {x_1})) x_1 = (T s) x
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : NormedAddCommGroup F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : NormedAddCommGroup G<VAR>m✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>T : Set α → F →L[ℝ] F'<VAR>hT_empty : T ∅ = 0<VAR>m : MeasurableSpace α<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>x : F<VAR>hs_empty : s.Nonempty<VAR>hs_univ : s ≠ Set.univ<VAR>hx0 : ¬x = 0<GOAL>∑ x_1 ∈ {x, 0}, (T (↑(piecewise s hs (const α x) (const α 0)) ⁻¹' {x_1})) x_1 = (T s) x
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : NormedAddCommGroup F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : NormedAddCommGroup G<VAR>m✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>T : Set α → F →L[ℝ] F'<VAR>hT_empty : T ∅ = 0<VAR>m : MeasurableSpace α<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>x : F<VAR>hs_empty : s.Nonempty<VAR>hs_univ : s ≠ Set.univ<VAR>hx0 : ¬x = 0<GOAL>(T (↑(piecewise s hs (const α x) (const α 0)) ⁻¹' {x})) x + ∑ x_1 ∈ {0}, (T (↑(piecewise s hs (const α x) (const α 0)) ⁻¹' {x_1})) x_1 = (T s) x
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : NormedAddCommGroup F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : NormedAddCommGroup G<VAR>m✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>T : Set α → F →L[ℝ] F'<VAR>hT_empty : T ∅ = 0<VAR>m : MeasurableSpace α<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>x : F<VAR>hs_empty : s.Nonempty<VAR>hs_univ : s ≠ Set.univ<VAR>hx0 : ¬x = 0<GOAL>x ∉ {0}
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : NormedAddCommGroup F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : NormedAddCommGroup G<VAR>m✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>T : Set α → F →L[ℝ] F'<VAR>hT_empty : T ∅ = 0<VAR>m : MeasurableSpace α<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>x : F<VAR>hs_empty : s.Nonempty<VAR>hs_univ : s ≠ Set.univ<VAR>hx0 : ¬x = 0<GOAL>(T (↑(piecewise s hs (const α x) (const α 0)) ⁻¹' {x})) x = (T s) x
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : NormedAddCommGroup F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : NormedAddCommGroup G<VAR>m✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>T : Set α → F →L[ℝ] F'<VAR>hT_empty : T ∅ = 0<VAR>m : MeasurableSpace α<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>x : F<VAR>hs_empty : s.Nonempty<VAR>hs_univ : s ≠ Set.univ<VAR>hx0 : ¬x = 0<GOAL>↑(piecewise s hs (const α x) (const α 0)) ⁻¹' {x} = s
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : NormedAddCommGroup F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : NormedAddCommGroup G<VAR>m✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>T : Set α → F →L[ℝ] F'<VAR>hT_empty : T ∅ = 0<VAR>m : MeasurableSpace α<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>x : F<VAR>hs_empty : s.Nonempty<VAR>hs_univ : s ≠ Set.univ<VAR>hx0 : ¬x = 0<GOAL>s.indicator (Function.const α x) ⁻¹' {x} = s
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : NormedAddCommGroup F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : NormedAddCommGroup G<VAR>m✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>T : Set α → F →L[ℝ] F'<VAR>hT_empty : T ∅ = 0<VAR>m : MeasurableSpace α<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>x : F<VAR>hs_empty : s.Nonempty<VAR>hs_univ : s ≠ Set.univ<VAR>hx0 : ¬x = 0<GOAL>s.ite Set.univ (0 ⁻¹' {x}) = s
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : NormedAddCommGroup F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : NormedAddCommGroup G<VAR>m✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>T : Set α → F →L[ℝ] F'<VAR>hT_empty : T ∅ = 0<VAR>m : MeasurableSpace α<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>x : F<VAR>hs_empty : s.Nonempty<VAR>hs_univ : s ≠ Set.univ<VAR>hx0 : ¬x = 0<GOAL>x ∈ {x}
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : NormedAddCommGroup F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : NormedAddCommGroup G<VAR>m✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>T : Set α → F →L[ℝ] F'<VAR>hT_empty : T ∅ = 0<VAR>m : MeasurableSpace α<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>x : F<VAR>hs_empty : s.Nonempty<VAR>hs_univ : s ≠ Set.univ<VAR>hx0 : ¬x = 0<GOAL>s.ite Set.univ ∅ = s
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : NormedAddCommGroup F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : NormedAddCommGroup G<VAR>m✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>T : Set α → F →L[ℝ] F'<VAR>hT_empty : T ∅ = 0<VAR>m : MeasurableSpace α<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>x : F<VAR>hs_empty : s.Nonempty<VAR>hs_univ : s ≠ Set.univ<VAR>hx0 : ¬x = 0<GOAL>0 ∉ {x}
<VAR>y z : ℝ<VAR>hyz : y < z<VAR>x : ℝ≥0<VAR>hx : 1 < ↑x<GOAL>↑x ^ y < ↑x ^ z
<VAR>y z : ℝ<VAR>hyz : y < z<VAR>x : ℝ≥0<VAR>hx : 1 < x<GOAL>↑x ^ y < ↑x ^ z
<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : Fintype α<VAR>s✝ t✝ : Finset α<VAR>a b : α<VAR>inst✝ : DecidableEq α<VAR>s t : Finset α<GOAL>(s ∪ t).dens + (s ∩ t).dens = s.dens + t.dens
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>a : α<VAR>l : List α<GOAL>(a :: l).sublists'.length = 2 ^ (a :: l).length
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>hm : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>inst✝¹⁰ : TopologicalSpace α<VAR>inst✝⁹ : BorelSpace α<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>g✝ : α → E<VAR>l : Filter ι<VAR>x₀ : α<VAR>s t : Set α<VAR>φ✝ : ι → α → ℝ<VAR>a : E<VAR>inst✝⁶ : CompleteSpace E<VAR>F : Type u_4<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace ℝ F<VAR>inst✝³ : FiniteDimensional ℝ F<VAR>inst✝² : MeasurableSpace F<VAR>inst✝¹ : BorelSpace F<VAR>μ : Measure F<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>φ : F → ℝ<VAR>hφ : ∀ (x : F), 0 ≤ φ x<VAR>h'φ : ∫ (x : F), φ x ∂μ = 1<VAR>h : Tendsto (fun x => ‖x‖ ^ finrank ℝ F * φ x) (cobounded F) (𝓝 0)<VAR>g : F → E<VAR>hg : Integrable g μ<VAR>h'g : ContinuousAt g 0<GOAL>Tendsto (fun c => ∫ (x : F), (c ^ finrank ℝ F * φ (c • x)) • g x ∂μ) atTop (𝓝 (g 0))
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>hm : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>inst✝¹⁰ : TopologicalSpace α<VAR>inst✝⁹ : BorelSpace α<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>g✝ : α → E<VAR>l : Filter ι<VAR>x₀ : α<VAR>s t : Set α<VAR>φ✝ : ι → α → ℝ<VAR>a : E<VAR>inst✝⁶ : CompleteSpace E<VAR>F : Type u_4<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace ℝ F<VAR>inst✝³ : FiniteDimensional ℝ F<VAR>inst✝² : MeasurableSpace F<VAR>inst✝¹ : BorelSpace F<VAR>μ : Measure F<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>φ : F → ℝ<VAR>hφ : ∀ (x : F), 0 ≤ φ x<VAR>h'φ : ∫ (x : F), φ x ∂μ = 1<VAR>h : Tendsto (fun x => ‖x‖ ^ finrank ℝ F * φ x) (cobounded F) (𝓝 0)<VAR>g : F → E<VAR>hg : Integrable g μ<VAR>h'g : ContinuousAt g 0<VAR>I : Integrable φ μ<GOAL>Tendsto (fun c => ∫ (x : F), (c ^ finrank ℝ F * φ (c • x)) • g x ∂μ) atTop (𝓝 (g 0))
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>hm : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>inst✝¹⁰ : TopologicalSpace α<VAR>inst✝⁹ : BorelSpace α<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>g✝ : α → E<VAR>l : Filter ι<VAR>x₀ : α<VAR>s t : Set α<VAR>φ✝ : ι → α → ℝ<VAR>a : E<VAR>inst✝⁶ : CompleteSpace E<VAR>F : Type u_4<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace ℝ F<VAR>inst✝³ : FiniteDimensional ℝ F<VAR>inst✝² : MeasurableSpace F<VAR>inst✝¹ : BorelSpace F<VAR>μ : Measure F<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>φ : F → ℝ<VAR>hφ : ∀ (x : F), 0 ≤ φ x<VAR>h'φ : ∫ (x : F), φ x ∂μ = 1<VAR>h : Tendsto (fun x => ‖x‖ ^ finrank ℝ F * φ x) (cobounded F) (𝓝 0)<VAR>g : F → E<VAR>hg : Integrable g μ<VAR>h'g : ContinuousAt g 0<VAR>I : Integrable φ μ<GOAL>MeasurableSet (closedBall 0 1)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>hm : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>inst✝¹⁰ : TopologicalSpace α<VAR>inst✝⁹ : BorelSpace α<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>g✝ : α → E<VAR>l : Filter ι<VAR>x₀ : α<VAR>s t : Set α<VAR>φ✝ : ι → α → ℝ<VAR>a : E<VAR>inst✝⁶ : CompleteSpace E<VAR>F : Type u_4<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace ℝ F<VAR>inst✝³ : FiniteDimensional ℝ F<VAR>inst✝² : MeasurableSpace F<VAR>inst✝¹ : BorelSpace F<VAR>μ : Measure F<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>φ : F → ℝ<VAR>hφ : ∀ (x : F), 0 ≤ φ x<VAR>h'φ : ∫ (x : F), φ x ∂μ = 1<VAR>h : Tendsto (fun x => ‖x‖ ^ finrank ℝ F * φ x) (cobounded F) (𝓝 0)<VAR>g : F → E<VAR>hg : Integrable g μ<VAR>h'g : ContinuousAt g 0<VAR>I : Integrable φ μ<GOAL>closedBall 0 1 ∈ 𝓝 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>hm : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>inst✝¹⁰ : TopologicalSpace α<VAR>inst✝⁹ : BorelSpace α<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>g✝ : α → E<VAR>l : Filter ι<VAR>x₀ : α<VAR>s t : Set α<VAR>φ✝ : ι → α → ℝ<VAR>a : E<VAR>inst✝⁶ : CompleteSpace E<VAR>F : Type u_4<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace ℝ F<VAR>inst✝³ : FiniteDimensional ℝ F<VAR>inst✝² : MeasurableSpace F<VAR>inst✝¹ : BorelSpace F<VAR>μ : Measure F<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>φ : F → ℝ<VAR>hφ : ∀ (x : F), 0 ≤ φ x<VAR>h'φ : ∫ (x : F), φ x ∂μ = 1<VAR>h : Tendsto (fun x => ‖x‖ ^ finrank ℝ F * φ x) (cobounded F) (𝓝 0)<VAR>g : F → E<VAR>hg : Integrable g μ<VAR>h'g : ContinuousAt g 0<VAR>I : Integrable φ μ<GOAL>μ (closedBall 0 1) ≠ ⊤
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>hm : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>inst✝¹⁰ : TopologicalSpace α<VAR>inst✝⁹ : BorelSpace α<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>g✝ : α → E<VAR>l : Filter ι<VAR>x₀ : α<VAR>s t : Set α<VAR>φ✝ : ι → α → ℝ<VAR>a : E<VAR>inst✝⁶ : CompleteSpace E<VAR>F : Type u_4<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace ℝ F<VAR>inst✝³ : FiniteDimensional ℝ F<VAR>inst✝² : MeasurableSpace F<VAR>inst✝¹ : BorelSpace F<VAR>μ : Measure F<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>φ : F → ℝ<VAR>hφ : ∀ (x : F), 0 ≤ φ x<VAR>h'φ : ∫ (x : F), φ x ∂μ = 1<VAR>h : Tendsto (fun x => ‖x‖ ^ finrank ℝ F * φ x) (cobounded F) (𝓝 0)<VAR>g : F → E<VAR>hg : Integrable g μ<VAR>h'g : ContinuousAt g 0<VAR>I : Integrable φ μ<GOAL>∀ᶠ (i : ℝ) in atTop, ∀ (x : F), 0 ≤ i ^ finrank ℝ F * φ (i • x)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>hm : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>inst✝¹⁰ : TopologicalSpace α<VAR>inst✝⁹ : BorelSpace α<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>g✝ : α → E<VAR>l : Filter ι<VAR>x₀ : α<VAR>s t : Set α<VAR>φ✝ : ι → α → ℝ<VAR>a : E<VAR>inst✝⁶ : CompleteSpace E<VAR>F : Type u_4<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace ℝ F<VAR>inst✝³ : FiniteDimensional ℝ F<VAR>inst✝² : MeasurableSpace F<VAR>inst✝¹ : BorelSpace F<VAR>μ : Measure F<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>φ : F → ℝ<VAR>hφ : ∀ (x : F), 0 ≤ φ x<VAR>h'φ : ∫ (x : F), φ x ∂μ = 1<VAR>h : Tendsto (fun x => ‖x‖ ^ finrank ℝ F * φ x) (cobounded F) (𝓝 0)<VAR>g : F → E<VAR>hg : Integrable g μ<VAR>h'g : ContinuousAt g 0<VAR>I : Integrable φ μ<GOAL>∀ (u : Set F), IsOpen u → 0 ∈ u → TendstoUniformlyOn (fun i x => i ^ finrank ℝ F * φ (i • x)) 0 atTop uᶜ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>hm : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>inst✝¹⁰ : TopologicalSpace α<VAR>inst✝⁹ : BorelSpace α<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>g✝ : α → E<VAR>l : Filter ι<VAR>x₀ : α<VAR>s t : Set α<VAR>φ✝ : ι → α → ℝ<VAR>a : E<VAR>inst✝⁶ : CompleteSpace E<VAR>F : Type u_4<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace ℝ F<VAR>inst✝³ : FiniteDimensional ℝ F<VAR>inst✝² : MeasurableSpace F<VAR>inst✝¹ : BorelSpace F<VAR>μ : Measure F<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>φ : F → ℝ<VAR>hφ : ∀ (x : F), 0 ≤ φ x<VAR>h'φ : ∫ (x : F), φ x ∂μ = 1<VAR>h : Tendsto (fun x => ‖x‖ ^ finrank ℝ F * φ x) (cobounded F) (𝓝 0)<VAR>g : F → E<VAR>hg : Integrable g μ<VAR>h'g : ContinuousAt g 0<VAR>I : Integrable φ μ<GOAL>Tendsto (fun i => ∫ (x : F) in closedBall 0 1, i ^ finrank ℝ F * φ (i • x) ∂μ) atTop (𝓝 1)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>hm : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>inst✝¹⁰ : TopologicalSpace α<VAR>inst✝⁹ : BorelSpace α<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>g✝ : α → E<VAR>l : Filter ι<VAR>x₀ : α<VAR>s t : Set α<VAR>φ✝ : ι → α → ℝ<VAR>a : E<VAR>inst✝⁶ : CompleteSpace E<VAR>F : Type u_4<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace ℝ F<VAR>inst✝³ : FiniteDimensional ℝ F<VAR>inst✝² : MeasurableSpace F<VAR>inst✝¹ : BorelSpace F<VAR>μ : Measure F<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>φ : F → ℝ<VAR>hφ : ∀ (x : F), 0 ≤ φ x<VAR>h'φ : ∫ (x : F), φ x ∂μ = 1<VAR>h : Tendsto (fun x => ‖x‖ ^ finrank ℝ F * φ x) (cobounded F) (𝓝 0)<VAR>g : F → E<VAR>hg : Integrable g μ<VAR>h'g : ContinuousAt g 0<VAR>I : Integrable φ μ<GOAL>∀ᶠ (i : ℝ) in atTop, AEStronglyMeasurable (fun x => i ^ finrank ℝ F * φ (i • x)) μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>hm : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>inst✝¹⁰ : TopologicalSpace α<VAR>inst✝⁹ : BorelSpace α<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>g✝ : α → E<VAR>l : Filter ι<VAR>x₀ : α<VAR>s t : Set α<VAR>φ✝ : ι → α → ℝ<VAR>a : E<VAR>inst✝⁶ : CompleteSpace E<VAR>F : Type u_4<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace ℝ F<VAR>inst✝³ : FiniteDimensional ℝ F<VAR>inst✝² : MeasurableSpace F<VAR>inst✝¹ : BorelSpace F<VAR>μ : Measure F<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>φ : F → ℝ<VAR>hφ : ∀ (x : F), 0 ≤ φ x<VAR>h'φ : ∫ (x : F), φ x ∂μ = 1<VAR>h : Tendsto (fun x => ‖x‖ ^ finrank ℝ F * φ x) (cobounded F) (𝓝 0)<VAR>g : F → E<VAR>hg : Integrable g μ<VAR>h'g : ContinuousAt g 0<VAR>I : Integrable φ μ<GOAL>Integrable g μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>hm : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>inst✝¹⁰ : TopologicalSpace α<VAR>inst✝⁹ : BorelSpace α<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>g✝ : α → E<VAR>l : Filter ι<VAR>x₀ : α<VAR>s t : Set α<VAR>φ✝ : ι → α → ℝ<VAR>a : E<VAR>inst✝⁶ : CompleteSpace E<VAR>F : Type u_4<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace ℝ F<VAR>inst✝³ : FiniteDimensional ℝ F<VAR>inst✝² : MeasurableSpace F<VAR>inst✝¹ : BorelSpace F<VAR>μ : Measure F<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>φ : F → ℝ<VAR>hφ : ∀ (x : F), 0 ≤ φ x<VAR>h'φ : ∫ (x : F), φ x ∂μ = 1<VAR>h : Tendsto (fun x => ‖x‖ ^ finrank ℝ F * φ x) (cobounded F) (𝓝 0)<VAR>g : F → E<VAR>hg : Integrable g μ<VAR>h'g : ContinuousAt g 0<VAR>I : Integrable φ μ<GOAL>Tendsto g (𝓝 0) (𝓝 (g 0))
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝⁴ : Lattice α<VAR>inst✝³ : BoundedOrder α<VAR>inst✝² : IsModularLattice α<VAR>inst✝¹ : ComplementedLattice α<VAR>inst✝ : IsAtomic α<VAR>x : α<GOAL>x = ⊤ ∨ ∃ a, IsCoatom a ∧ x ≤ a
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝⁴ : Lattice α<VAR>inst✝³ : BoundedOrder α<VAR>inst✝² : IsModularLattice α<VAR>inst✝¹ : ComplementedLattice α<VAR>inst✝ : IsAtomic α<VAR>x y : α<VAR>xy : IsCompl x y<GOAL>x = ⊤ ∨ ∃ a, IsCoatom a ∧ x ≤ a
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝⁴ : Lattice α<VAR>inst✝³ : BoundedOrder α<VAR>inst✝² : IsModularLattice α<VAR>inst✝¹ : ComplementedLattice α<VAR>inst✝ : IsAtomic α<VAR>x y : α<VAR>xy : IsCompl x y<GOAL>y = ⊥ → x = ⊤
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝⁴ : Lattice α<VAR>inst✝³ : BoundedOrder α<VAR>inst✝² : IsModularLattice α<VAR>inst✝¹ : ComplementedLattice α<VAR>inst✝ : IsAtomic α<VAR>x y : α<VAR>xy : IsCompl x y<GOAL>(∃ a, IsAtom a ∧ a ≤ y) → ∃ a, IsCoatom a ∧ x ≤ a
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>α✝ : Type u_4<VAR>inst✝ : TopologicalSpace X<VAR>α : Type u_5<VAR>β : Type u_6<VAR>f : X → α<VAR>g : α → β<VAR>h : IsLocallyConstant (g ∘ f)<VAR>inj : Function.Injective g<VAR>s : Set α<GOAL>IsOpen (f ⁻¹' s)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>α✝ : Type u_4<VAR>inst✝ : TopologicalSpace X<VAR>α : Type u_5<VAR>β : Type u_6<VAR>f : X → α<VAR>g : α → β<VAR>h : IsLocallyConstant (g ∘ f)<VAR>inj : Function.Injective g<VAR>s : Set α<GOAL>IsOpen ((fun x => g (f x)) ⁻¹' (g '' s))
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : Abelian C<VAR>S : ShortComplex C<VAR>hS : ∀ (b : Pseudoelement S.X₂), pseudoApply S.g b = 0 → ∃ a, pseudoApply S.f a = b<GOAL>kernel.ι S.g ≫ cokernel.π S.f = 0
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : Abelian C<VAR>S : ShortComplex C<VAR>hS : ∀ (b : Pseudoelement S.X₂), pseudoApply S.g b = 0 → ∃ a, pseudoApply S.f a = b<VAR>this : pseudoApply S.g (Quot.mk (PseudoEqual S.X₂) (Over.mk (kernel.ι S.g))) = 0<GOAL>kernel.ι S.g ≫ cokernel.π S.f = 0
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : Abelian C<VAR>S : ShortComplex C<VAR>hS : ∀ (b : Pseudoelement S.X₂), pseudoApply S.g b = 0 → ∃ a, pseudoApply S.f a = b<VAR>this : pseudoApply S.g (Quot.mk (PseudoEqual S.X₂) (Over.mk (kernel.ι S.g))) = 0<VAR>a' : Pseudoelement S.X₁<VAR>ha : pseudoApply S.f a' = Quot.mk (PseudoEqual S.X₂) (Over.mk (kernel.ι S.g))<GOAL>kernel.ι S.g ≫ cokernel.π S.f = 0