ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹² : NormedAddCommGroup E<VAR>inst✝¹¹ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>inst✝⁹ : NormedSpace 𝕜 E<VAR>inst✝⁸ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℝ F<VAR>inst✝⁵ : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>X : Type u_6<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : FirstCountableTopology X<VAR>ν : Measure α<VAR>β : Type u_7<VAR>inst✝ : MeasurableSpace β<VAR>φ : α → β<VAR>hφ : Measurable φ<VAR>f : β → G<VAR>hfm : StronglyMeasurable f<VAR>hG : CompleteSpace G<VAR>hfi : Integrable f (Measure.map φ μ)<VAR>this✝¹ : MeasurableSpace G := borel G<VAR>this✝ : BorelSpace G<VAR>this : SeparableSpace ↑(range f ∪ {0})<GOAL>(fun n => SimpleFunc.integral (Measure.map φ μ) (approxOn f ⋯ (range f ∪ {0}) 0 ⋯ n)) = fun n => SimpleFunc.integral μ (approxOn (f ∘ φ) ⋯ (range f ∪ {0}) 0 ⋯ n)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹² : NormedAddCommGroup E<VAR>inst✝¹¹ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>inst✝⁹ : NormedSpace 𝕜 E<VAR>inst✝⁸ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℝ F<VAR>inst✝⁵ : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>X : Type u_6<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : FirstCountableTopology X<VAR>ν : Measure α<VAR>β : Type u_7<VAR>inst✝ : MeasurableSpace β<VAR>φ : α → β<VAR>hφ : Measurable φ<VAR>f : β → G<VAR>hfm : StronglyMeasurable f<VAR>hG : CompleteSpace G<VAR>hfi : Integrable f (Measure.map φ μ)<VAR>this✝¹ : MeasurableSpace G := borel G<VAR>this✝ : BorelSpace G<VAR>this : SeparableSpace ↑(range f ∪ {0})<VAR>i : ℕ<GOAL>SimpleFunc.integral (Measure.map φ μ) (approxOn f ⋯ (range f ∪ {0}) 0 ⋯ i) = SimpleFunc.integral μ (approxOn (f ∘ φ) ⋯ (range f ∪ {0}) 0 ⋯ i)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹² : NormedAddCommGroup E<VAR>inst✝¹¹ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>inst✝⁹ : NormedSpace 𝕜 E<VAR>inst✝⁸ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℝ F<VAR>inst✝⁵ : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>X : Type u_6<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : FirstCountableTopology X<VAR>ν : Measure α<VAR>β : Type u_7<VAR>inst✝ : MeasurableSpace β<VAR>φ : α → β<VAR>hφ : Measurable φ<VAR>f : β → G<VAR>hfm : StronglyMeasurable f<VAR>hG : CompleteSpace G<VAR>hfi : Integrable f (Measure.map φ μ)<VAR>this✝¹ : MeasurableSpace G := borel G<VAR>this✝ : BorelSpace G<VAR>this : SeparableSpace ↑(range f ∪ {0})<VAR>i : ℕ<GOAL>∑ x ∈ (approxOn f ⋯ (range f ∪ {0}) 0 ⋯ i).range, (μ (↑(approxOn f ⋯ (range f ∪ {0}) 0 ⋯ i) ∘ φ ⁻¹' {x})).toReal • x = ∑ x ∈ (approxOn (f ∘ φ) ⋯ (range f ∪ {0}) 0 ⋯ i).range, (μ (↑(approxOn (f ∘ φ) ⋯ (range f ∪ {0}) 0 ⋯ i) ⁻¹' {x})).toReal • x
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹² : NormedAddCommGroup E<VAR>inst✝¹¹ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>inst✝⁹ : NormedSpace 𝕜 E<VAR>inst✝⁸ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℝ F<VAR>inst✝⁵ : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>X : Type u_6<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : FirstCountableTopology X<VAR>ν : Measure α<VAR>β : Type u_7<VAR>inst✝ : MeasurableSpace β<VAR>φ : α → β<VAR>hφ : Measurable φ<VAR>f : β → G<VAR>hfm : StronglyMeasurable f<VAR>hG : CompleteSpace G<VAR>hfi : Integrable f (Measure.map φ μ)<VAR>this✝¹ : MeasurableSpace G := borel G<VAR>this✝ : BorelSpace G<VAR>this : SeparableSpace ↑(range f ∪ {0})<VAR>i : ℕ<VAR>y : G<VAR>x✝ : y ∈ (approxOn f ⋯ (range f ∪ {0}) 0 ⋯ i).range<VAR>hy : y ∉ ((approxOn f ⋯ (range f ∪ {0}) 0 ⋯ i).comp φ hφ).range<GOAL>(μ (↑(approxOn f ⋯ (range f ∪ {0}) 0 ⋯ i) ∘ φ ⁻¹' {y})).toReal • y = 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹² : NormedAddCommGroup E<VAR>inst✝¹¹ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>inst✝⁹ : NormedSpace 𝕜 E<VAR>inst✝⁸ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℝ F<VAR>inst✝⁵ : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>X : Type u_6<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : FirstCountableTopology X<VAR>ν : Measure α<VAR>β : Type u_7<VAR>inst✝ : MeasurableSpace β<VAR>φ : α → β<VAR>hφ : Measurable φ<VAR>f : β → G<VAR>hfm : StronglyMeasurable f<VAR>hG : CompleteSpace G<VAR>hfi : Integrable f (Measure.map φ μ)<VAR>this✝¹ : MeasurableSpace G := borel G<VAR>this✝ : BorelSpace G<VAR>this : SeparableSpace ↑(range f ∪ {0})<VAR>i : ℕ<VAR>y : G<VAR>x✝ : y ∈ (approxOn f ⋯ (range f ∪ {0}) 0 ⋯ i).range<VAR>hy : ↑(approxOn f ⋯ (range f ∪ {0}) 0 ⋯ i) ∘ φ ⁻¹' {y} = ∅<GOAL>(μ (↑(approxOn f ⋯ (range f ∪ {0}) 0 ⋯ i) ∘ φ ⁻¹' {y})).toReal • y = 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>V : Type u_4<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℂ V<VAR>S T : V →ₗ[ℂ] V<GOAL>(∀ (x : V), ⟪S x, x⟫_ℂ = ⟪T x, x⟫_ℂ) ↔ S = T
<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>V : Type u_4<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℂ V<VAR>S T : V →ₗ[ℂ] V<GOAL>(∀ (x : V), ⟪S x, x⟫_ℂ = ⟪T x, x⟫_ℂ) ↔ ∀ (x : V), ⟪(S - T) x, 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>V : Type u_4<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℂ V<VAR>S T : V →ₗ[ℂ] V<VAR>x : V<GOAL>⟪S x, x⟫_ℂ = ⟪T x, x⟫_ℂ ↔ ⟪(S - T) x, x⟫_ℂ = 0
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>ι : Type u_3<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>s t : Set X<VAR>inst✝ : WeaklyLocallyCompactSpace X<VAR>K : Set X<VAR>hK : IsCompact K<GOAL>∃ K', IsCompact K' ∧ K ⊆ interior K'
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>ι : Type u_3<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>s✝ t : Set X<VAR>inst✝ : WeaklyLocallyCompactSpace X<VAR>K : Set X<VAR>hK : IsCompact K<VAR>s : X → Set X<VAR>hc : ∀ (x : X), IsCompact (s x)<VAR>hmem : ∀ (x : X), s x ∈ 𝓝 x<GOAL>∃ K', IsCompact K' ∧ K ⊆ interior K'
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>ι : Type u_3<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>s✝ t : Set X<VAR>inst✝ : WeaklyLocallyCompactSpace X<VAR>K : Set X<VAR>hK : IsCompact K<VAR>s : X → Set X<VAR>hc : ∀ (x : X), IsCompact (s x)<VAR>hmem : ∀ (x : X), s x ∈ 𝓝 x<VAR>I : Finset X<VAR>hIK : K ⊆ ⋃ x ∈ I, interior (s x)<GOAL>∃ K', IsCompact K' ∧ K ⊆ interior K'
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>ι : Type u_3<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>s✝ t : Set X<VAR>inst✝ : WeaklyLocallyCompactSpace X<VAR>K : Set X<VAR>hK : IsCompact K<VAR>s : X → Set X<VAR>hc : ∀ (x : X), IsCompact (s x)<VAR>hmem : ∀ (x : X), s x ∈ 𝓝 x<VAR>I : Finset X<VAR>hIK : K ⊆ ⋃ x ∈ I, interior (s x)<GOAL>⋃ x ∈ I, interior (s x) ⊆ interior (⋃ x ∈ I, s x)
<VAR>R : Type u<VAR>a b : R<VAR>m n✝ : ℕ<VAR>inst✝ : Semiring R<VAR>p q : R[X]<VAR>n : ℕ<VAR>hn : n ≠ 1<GOAL>X.coeff n = 0
<VAR>F : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝⁹ : CommSemiring R<VAR>inst✝⁸ : StarRing R<VAR>inst✝⁷ : Semiring A<VAR>inst✝⁶ : Algebra R A<VAR>inst✝⁵ : StarRing A<VAR>inst✝⁴ : StarModule R A<VAR>inst✝³ : Semiring B<VAR>inst✝² : Algebra R B<VAR>inst✝¹ : StarRing B<VAR>inst✝ : StarModule R B<VAR>s : Set A<GOAL>Subalgebra.toSubmodule (adjoin R s).toSubalgebra = span R ↑(Submonoid.closure (s ∪ star s))
<VAR>R : Type u_1<VAR>inst✝¹ : Semiring R<VAR>inst✝ : Nontrivial R<GOAL>X.order = 1
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>C : Type u_4<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : CommRing B<VAR>inst✝³ : CommRing C<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : Algebra R B<VAR>inst✝ : Algebra R C<VAR>f : A →ₐ[R] B<VAR>hf : Surjective ⇑f<VAR>hker : (RingHom.ker f.toRingHom).FG<GOAL>f.FinitePresentation
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>n : ℕ<GOAL>∑ i ∈ Finset.range n, (1 / 2) ^ i ≤ 2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>n : ℕ<VAR>this : ∀ (i : ℕ), 0 ≤ (1 / 2) ^ i<GOAL>∑ i ∈ Finset.range n, (1 / 2) ^ i ≤ 2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>n : ℕ<VAR>this : ∀ (i : ℕ), 0 ≤ (1 / 2) ^ i<GOAL>2 = ∑' (i : ℕ), (1 / 2) ^ i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f : α → ℝ≥0∞<VAR>s t : Set α<GOAL>∫⁻ (a : α) in s ∪ t, f a ∂μ ≤ ∫⁻ (a : α) in s, f a ∂μ + ∫⁻ (a : α) in t, f a ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f : α → ℝ≥0∞<VAR>s t : Set α<GOAL>∫⁻ (a : α) in s ∪ t, f a ∂μ ≤ ∫⁻ (a : α), f a ∂(μ.restrict s + μ.restrict t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E✝ : Type u_3<VAR>F : Type u_4<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : NormedAddCommGroup E✝<VAR>f✝ g : α → E✝<VAR>s✝ t : Set α<VAR>μ ν : Measure α<VAR>E : Type u_5<VAR>inst✝ : NormedAddCommGroup E<VAR>p : ℝ≥0∞<VAR>s : Set α<VAR>f : ↥(Lp E p μ)<VAR>hp : 1 ≤ p<VAR>hμs : μ s ≠ ⊤<GOAL>IntegrableOn (↑↑f) s μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E✝ : Type u_3<VAR>F : Type u_4<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : NormedAddCommGroup E✝<VAR>f✝ g : α → E✝<VAR>s✝ t : Set α<VAR>μ ν : Measure α<VAR>E : Type u_5<VAR>inst✝ : NormedAddCommGroup E<VAR>p : ℝ≥0∞<VAR>s : Set α<VAR>f : ↥(Lp E p μ)<VAR>hp : 1 ≤ p<VAR>hμs : μ s ≠ ⊤<GOAL>Memℒp (↑↑f) 1 (μ.restrict s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E✝ : Type u_3<VAR>F : Type u_4<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : NormedAddCommGroup E✝<VAR>f✝ g : α → E✝<VAR>s✝ t : Set α<VAR>μ ν : Measure α<VAR>E : Type u_5<VAR>inst✝ : NormedAddCommGroup E<VAR>p : ℝ≥0∞<VAR>s : Set α<VAR>f : ↥(Lp E p μ)<VAR>hp : 1 ≤ p<VAR>hμs : μ s ≠ ⊤<VAR>hμ_restrict_univ : (μ.restrict s) univ < ⊤<GOAL>Memℒp (↑↑f) 1 (μ.restrict s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E✝ : Type u_3<VAR>F : Type u_4<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : NormedAddCommGroup E✝<VAR>f✝ g : α → E✝<VAR>s✝ t : Set α<VAR>μ ν : Measure α<VAR>E : Type u_5<VAR>inst✝ : NormedAddCommGroup E<VAR>p : ℝ≥0∞<VAR>s : Set α<VAR>f : ↥(Lp E p μ)<VAR>hp : 1 ≤ p<VAR>hμs : μ s ≠ ⊤<VAR>hμ_restrict_univ : (μ.restrict s) univ < ⊤<VAR>hμ_finite : IsFiniteMeasure (μ.restrict s)<GOAL>Memℒp (↑↑f) 1 (μ.restrict s)
<VAR>p q : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hq : Fact (Nat.Prime q)<VAR>n m : ℕ<VAR>neq : p ≠ q<GOAL>padicValNat p (p ^ n * q ^ m) = n
<VAR>G : Type w<VAR>inst✝² : TopologicalSpace G<VAR>μ : Content G<VAR>inst✝¹ : R1Space G<VAR>S : MeasurableSpace G<VAR>inst✝ : BorelSpace G<GOAL>S ≤ μ.outerMeasure.caratheodory
<VAR>G : Type w<VAR>inst✝² : TopologicalSpace G<VAR>μ : Content G<VAR>inst✝¹ : R1Space G<VAR>S : MeasurableSpace G<VAR>inst✝ : BorelSpace G<GOAL>borel G ≤ μ.outerMeasure.caratheodory
<VAR>G : Type w<VAR>inst✝² : TopologicalSpace G<VAR>μ : Content G<VAR>inst✝¹ : R1Space G<VAR>S : MeasurableSpace G<VAR>inst✝ : BorelSpace G<GOAL>∀ t ∈ {s | IsOpen s}, MeasurableSet t
<VAR>G : Type w<VAR>inst✝² : TopologicalSpace G<VAR>μ : Content G<VAR>inst✝¹ : R1Space G<VAR>S : MeasurableSpace G<VAR>inst✝ : BorelSpace G<VAR>U : Set G<VAR>hU : U ∈ {s | IsOpen s}<GOAL>MeasurableSet U
<VAR>G : Type w<VAR>inst✝² : TopologicalSpace G<VAR>μ : Content G<VAR>inst✝¹ : R1Space G<VAR>S : MeasurableSpace G<VAR>inst✝ : BorelSpace G<VAR>U : Set G<VAR>hU : U ∈ {s | IsOpen s}<GOAL>∀ (U_1 : Opens G), μ.outerMeasure (↑U_1 ∩ U) + μ.outerMeasure (↑U_1 \ U) ≤ μ.outerMeasure ↑U_1
<VAR>G : Type w<VAR>inst✝² : TopologicalSpace G<VAR>μ : Content G<VAR>inst✝¹ : R1Space G<VAR>S : MeasurableSpace G<VAR>inst✝ : BorelSpace G<VAR>U : Set G<VAR>hU : U ∈ {s | IsOpen s}<VAR>U' : Opens G<GOAL>μ.outerMeasure (↑U' ∩ U) + μ.outerMeasure (↑U' \ U) ≤ μ.outerMeasure ↑U'
<VAR>G : Type w<VAR>inst✝² : TopologicalSpace G<VAR>μ : Content G<VAR>inst✝¹ : R1Space G<VAR>S : MeasurableSpace G<VAR>inst✝ : BorelSpace G<VAR>U : Set G<VAR>hU : U ∈ {s | IsOpen s}<VAR>U' : Opens G<GOAL>μ.innerContent { carrier := ↑U' ∩ U, is_open' := ⋯ } + μ.outerMeasure (↑U' \ U) ≤ μ.outerMeasure ↑U'
<VAR>G : Type w<VAR>inst✝² : TopologicalSpace G<VAR>μ : Content G<VAR>inst✝¹ : R1Space G<VAR>S : MeasurableSpace G<VAR>inst✝ : BorelSpace G<VAR>U : Set G<VAR>hU : U ∈ {s | IsOpen s}<VAR>U' : Opens G<GOAL>(⨆ x, ↑(μ.toFun ↑x)) + μ.outerMeasure (↑U' \ U) ≤ μ.outerMeasure ↑U'
<VAR>G : Type w<VAR>inst✝² : TopologicalSpace G<VAR>μ : Content G<VAR>inst✝¹ : R1Space G<VAR>S : MeasurableSpace G<VAR>inst✝ : BorelSpace G<VAR>U : Set G<VAR>hU : U ∈ {s | IsOpen s}<VAR>U' : Opens G<VAR>this : Nonempty { L // ↑L ⊆ ↑U' ∩ U }<GOAL>(⨆ x, ↑(μ.toFun ↑x)) + μ.outerMeasure (↑U' \ U) ≤ μ.outerMeasure ↑U'
<VAR>G : Type w<VAR>inst✝² : TopologicalSpace G<VAR>μ : Content G<VAR>inst✝¹ : R1Space G<VAR>S : MeasurableSpace G<VAR>inst✝ : BorelSpace G<VAR>U : Set G<VAR>hU : U ∈ {s | IsOpen s}<VAR>U' : Opens G<VAR>this : Nonempty { L // ↑L ⊆ ↑U' ∩ U }<GOAL>⨆ b, ↑(μ.toFun ↑b) + μ.outerMeasure (↑U' \ U) ≤ μ.outerMeasure ↑U'
<VAR>G : Type w<VAR>inst✝² : TopologicalSpace G<VAR>μ : Content G<VAR>inst✝¹ : R1Space G<VAR>S : MeasurableSpace G<VAR>inst✝ : BorelSpace G<VAR>U : Set G<VAR>hU : U ∈ {s | IsOpen s}<VAR>U' : Opens G<VAR>this : Nonempty { L // ↑L ⊆ ↑U' ∩ U }<GOAL>∀ (i : { i // ↑i ⊆ ↑U' ∩ U }), ↑(μ.toFun ↑i) + μ.outerMeasure (↑U' \ U) ≤ μ.outerMeasure ↑U'
<VAR>G : Type w<VAR>inst✝² : TopologicalSpace G<VAR>μ : Content G<VAR>inst✝¹ : R1Space G<VAR>S : MeasurableSpace G<VAR>inst✝ : BorelSpace G<VAR>U : Set G<VAR>hU : U ∈ {s | IsOpen s}<VAR>U' : Opens G<VAR>this : Nonempty { L // ↑L ⊆ ↑U' ∩ U }<VAR>L : Compacts G<VAR>hL : ↑L ⊆ ↑U' ∩ U<GOAL>↑(μ.toFun ↑⟨L, hL⟩) + μ.outerMeasure (↑U' \ U) ≤ μ.outerMeasure ↑U'
<VAR>G : Type w<VAR>inst✝² : TopologicalSpace G<VAR>μ : Content G<VAR>inst✝¹ : R1Space G<VAR>S : MeasurableSpace G<VAR>inst✝ : BorelSpace G<VAR>U : Set G<VAR>hU : U ∈ {s | IsOpen s}<VAR>U' : Opens G<VAR>this : Nonempty { L // ↑L ⊆ ↑U' ∩ U }<VAR>L : Compacts G<VAR>hL : ↑L ⊆ ↑U' ∩ U<VAR>L' : Compacts G := { carrier := closure ↑L, isCompact' := ⋯ }<GOAL>↑(μ.toFun ↑⟨L, hL⟩) + μ.outerMeasure (↑U' \ U) ≤ μ.outerMeasure ↑U'
<VAR>G : Type w<VAR>inst✝² : TopologicalSpace G<VAR>μ : Content G<VAR>inst✝¹ : R1Space G<VAR>S : MeasurableSpace G<VAR>inst✝ : BorelSpace G<VAR>U : Set G<VAR>hU : U ∈ {s | IsOpen s}<VAR>U' : Opens G<VAR>this : Nonempty { L // ↑L ⊆ ↑U' ∩ U }<VAR>L : Compacts G<VAR>hL : ↑L ⊆ ↑U' ∩ U<VAR>L' : Compacts G := { carrier := closure ↑L, isCompact' := ⋯ }<GOAL>(fun s => ↑(μ.toFun s)) L' + μ.outerMeasure (↑U' \ U) ≤ μ.outerMeasure ↑U'
<VAR>G : Type w<VAR>inst✝² : TopologicalSpace G<VAR>μ : Content G<VAR>inst✝¹ : R1Space G<VAR>S : MeasurableSpace G<VAR>inst✝ : BorelSpace G<VAR>U : Set G<VAR>hU : U ∈ {s | IsOpen s}<VAR>U' : Opens G<VAR>this : Nonempty { L // ↑L ⊆ ↑U' ∩ U }<VAR>L : Compacts G<VAR>L' : Compacts G := { carrier := closure ↑L, isCompact' := ⋯ }<VAR>hL : ↑L ⊆ ↑U' ∧ ↑L ⊆ U<GOAL>(fun s => ↑(μ.toFun s)) L' + μ.outerMeasure (↑U' \ U) ≤ μ.outerMeasure ↑U'
<VAR>G : Type w<VAR>inst✝² : TopologicalSpace G<VAR>μ : Content G<VAR>inst✝¹ : R1Space G<VAR>S : MeasurableSpace G<VAR>inst✝ : BorelSpace G<VAR>U : Set G<VAR>hU : U ∈ {s | IsOpen s}<VAR>U' : Opens G<VAR>this : Nonempty { L // ↑L ⊆ ↑U' ∩ U }<VAR>L : Compacts G<VAR>L' : Compacts G := { carrier := closure ↑L, isCompact' := ⋯ }<VAR>hL : ↑L ⊆ ↑U' ∧ ↑L ⊆ U<VAR>hL'U : ↑L' ⊆ U<GOAL>(fun s => ↑(μ.toFun s)) L' + μ.outerMeasure (↑U' \ U) ≤ μ.outerMeasure ↑U'
<VAR>G : Type w<VAR>inst✝² : TopologicalSpace G<VAR>μ : Content G<VAR>inst✝¹ : R1Space G<VAR>S : MeasurableSpace G<VAR>inst✝ : BorelSpace G<VAR>U : Set G<VAR>hU : U ∈ {s | IsOpen s}<VAR>U' : Opens G<VAR>this : Nonempty { L // ↑L ⊆ ↑U' ∩ U }<VAR>L : Compacts G<VAR>L' : Compacts G := { carrier := closure ↑L, isCompact' := ⋯ }<VAR>hL : ↑L ⊆ ↑U' ∧ ↑L ⊆ U<VAR>hL'U : ↑L' ⊆ U<VAR>hL'U' : ↑L' ⊆ ↑U'<GOAL>(fun s => ↑(μ.toFun s)) L' + μ.outerMeasure (↑U' \ U) ≤ μ.outerMeasure ↑U'
<VAR>G : Type w<VAR>inst✝² : TopologicalSpace G<VAR>μ : Content G<VAR>inst✝¹ : R1Space G<VAR>S : MeasurableSpace G<VAR>inst✝ : BorelSpace G<VAR>U : Set G<VAR>hU : U ∈ {s | IsOpen s}<VAR>U' : Opens G<VAR>this✝ : Nonempty { L // ↑L ⊆ ↑U' ∩ U }<VAR>L : Compacts G<VAR>L' : Compacts G := { carrier := closure ↑L, isCompact' := ⋯ }<VAR>hL : ↑L ⊆ ↑U' ∧ ↑L ⊆ U<VAR>hL'U : ↑L' ⊆ U<VAR>hL'U' : ↑L' ⊆ ↑U'<VAR>this : ↑U' \ U ⊆ ↑U' \ ↑L'<GOAL>(fun s => ↑(μ.toFun s)) L' + μ.outerMeasure (↑U' \ U) ≤ μ.outerMeasure ↑U'
<VAR>G : Type w<VAR>inst✝² : TopologicalSpace G<VAR>μ : Content G<VAR>inst✝¹ : R1Space G<VAR>S : MeasurableSpace G<VAR>inst✝ : BorelSpace G<VAR>U : Set G<VAR>hU : U ∈ {s | IsOpen s}<VAR>U' : Opens G<VAR>this✝ : Nonempty { L // ↑L ⊆ ↑U' ∩ U }<VAR>L : Compacts G<VAR>L' : Compacts G := { carrier := closure ↑L, isCompact' := ⋯ }<VAR>hL : ↑L ⊆ ↑U' ∧ ↑L ⊆ U<VAR>hL'U : ↑L' ⊆ U<VAR>hL'U' : ↑L' ⊆ ↑U'<VAR>this : ↑U' \ U ⊆ ↑U' \ ↑L'<GOAL>(fun s => ↑(μ.toFun s)) L' + μ.outerMeasure (↑U' \ ↑L') ≤ μ.outerMeasure ↑U'
<VAR>G : Type w<VAR>inst✝² : TopologicalSpace G<VAR>μ : Content G<VAR>inst✝¹ : R1Space G<VAR>S : MeasurableSpace G<VAR>inst✝ : BorelSpace G<VAR>U : Set G<VAR>hU : U ∈ {s | IsOpen s}<VAR>U' : Opens G<VAR>this✝ : Nonempty { L // ↑L ⊆ ↑U' ∩ U }<VAR>L : Compacts G<VAR>L' : Compacts G := { carrier := closure ↑L, isCompact' := ⋯ }<VAR>hL : ↑L ⊆ ↑U' ∧ ↑L ⊆ U<VAR>hL'U : ↑L' ⊆ U<VAR>hL'U' : ↑L' ⊆ ↑U'<VAR>this : ↑U' \ U ⊆ ↑U' \ ↑L'<GOAL>(fun s => ↑(μ.toFun s)) L' + μ.innerContent { carrier := ↑U' \ ↑L', is_open' := ⋯ } ≤ μ.outerMeasure ↑U'
<VAR>G : Type w<VAR>inst✝² : TopologicalSpace G<VAR>μ : Content G<VAR>inst✝¹ : R1Space G<VAR>S : MeasurableSpace G<VAR>inst✝ : BorelSpace G<VAR>U : Set G<VAR>hU : U ∈ {s | IsOpen s}<VAR>U' : Opens G<VAR>this✝ : Nonempty { L // ↑L ⊆ ↑U' ∩ U }<VAR>L : Compacts G<VAR>L' : Compacts G := { carrier := closure ↑L, isCompact' := ⋯ }<VAR>hL : ↑L ⊆ ↑U' ∧ ↑L ⊆ U<VAR>hL'U : ↑L' ⊆ U<VAR>hL'U' : ↑L' ⊆ ↑U'<VAR>this : ↑U' \ U ⊆ ↑U' \ ↑L'<GOAL>↑(μ.toFun L') + ⨆ x, ↑(μ.toFun ↑x) ≤ μ.outerMeasure ↑U'
<VAR>G : Type w<VAR>inst✝² : TopologicalSpace G<VAR>μ : Content G<VAR>inst✝¹ : R1Space G<VAR>S : MeasurableSpace G<VAR>inst✝ : BorelSpace G<VAR>U : Set G<VAR>hU : U ∈ {s | IsOpen s}<VAR>U' : Opens G<VAR>this✝¹ : Nonempty { L // ↑L ⊆ ↑U' ∩ U }<VAR>L : Compacts G<VAR>L' : Compacts G := { carrier := closure ↑L, isCompact' := ⋯ }<VAR>hL : ↑L ⊆ ↑U' ∧ ↑L ⊆ U<VAR>hL'U : ↑L' ⊆ U<VAR>hL'U' : ↑L' ⊆ ↑U'<VAR>this✝ : ↑U' \ U ⊆ ↑U' \ ↑L'<VAR>this : Nonempty { M // ↑M ⊆ ↑U' \ closure ↑L }<GOAL>↑(μ.toFun L') + ⨆ x, ↑(μ.toFun ↑x) ≤ μ.outerMeasure ↑U'
<VAR>G : Type w<VAR>inst✝² : TopologicalSpace G<VAR>μ : Content G<VAR>inst✝¹ : R1Space G<VAR>S : MeasurableSpace G<VAR>inst✝ : BorelSpace G<VAR>U : Set G<VAR>hU : U ∈ {s | IsOpen s}<VAR>U' : Opens G<VAR>this✝¹ : Nonempty { L // ↑L ⊆ ↑U' ∩ U }<VAR>L : Compacts G<VAR>L' : Compacts G := { carrier := closure ↑L, isCompact' := ⋯ }<VAR>hL : ↑L ⊆ ↑U' ∧ ↑L ⊆ U<VAR>hL'U : ↑L' ⊆ U<VAR>hL'U' : ↑L' ⊆ ↑U'<VAR>this✝ : ↑U' \ U ⊆ ↑U' \ ↑L'<VAR>this : Nonempty { M // ↑M ⊆ ↑U' \ closure ↑L }<GOAL>⨆ b, ↑(μ.toFun L') + ↑(μ.toFun ↑b) ≤ μ.outerMeasure ↑U'
<VAR>G : Type w<VAR>inst✝² : TopologicalSpace G<VAR>μ : Content G<VAR>inst✝¹ : R1Space G<VAR>S : MeasurableSpace G<VAR>inst✝ : BorelSpace G<VAR>U : Set G<VAR>hU : U ∈ {s | IsOpen s}<VAR>U' : Opens G<VAR>this✝¹ : Nonempty { L // ↑L ⊆ ↑U' ∩ U }<VAR>L : Compacts G<VAR>L' : Compacts G := { carrier := closure ↑L, isCompact' := ⋯ }<VAR>hL : ↑L ⊆ ↑U' ∧ ↑L ⊆ U<VAR>hL'U : ↑L' ⊆ U<VAR>hL'U' : ↑L' ⊆ ↑U'<VAR>this✝ : ↑U' \ U ⊆ ↑U' \ ↑L'<VAR>this : Nonempty { M // ↑M ⊆ ↑U' \ closure ↑L }<GOAL>∀ (i : { i // ↑i ⊆ ↑U' \ ↑L' }), ↑(μ.toFun L') + ↑(μ.toFun ↑i) ≤ μ.outerMeasure ↑U'
<VAR>G : Type w<VAR>inst✝² : TopologicalSpace G<VAR>μ : Content G<VAR>inst✝¹ : R1Space G<VAR>S : MeasurableSpace G<VAR>inst✝ : BorelSpace G<VAR>U : Set G<VAR>hU : U ∈ {s | IsOpen s}<VAR>U' : Opens G<VAR>this✝¹ : Nonempty { L // ↑L ⊆ ↑U' ∩ U }<VAR>L : Compacts G<VAR>L' : Compacts G := { carrier := closure ↑L, isCompact' := ⋯ }<VAR>hL : ↑L ⊆ ↑U' ∧ ↑L ⊆ U<VAR>hL'U : ↑L' ⊆ U<VAR>hL'U' : ↑L' ⊆ ↑U'<VAR>this✝ : ↑U' \ U ⊆ ↑U' \ ↑L'<VAR>this : Nonempty { M // ↑M ⊆ ↑U' \ closure ↑L }<VAR>M : Compacts G<VAR>hM : ↑M ⊆ ↑U' \ ↑L'<GOAL>↑(μ.toFun L') + ↑(μ.toFun ↑⟨M, hM⟩) ≤ μ.outerMeasure ↑U'
<VAR>G : Type w<VAR>inst✝² : TopologicalSpace G<VAR>μ : Content G<VAR>inst✝¹ : R1Space G<VAR>S : MeasurableSpace G<VAR>inst✝ : BorelSpace G<VAR>U : Set G<VAR>hU : U ∈ {s | IsOpen s}<VAR>U' : Opens G<VAR>this✝¹ : Nonempty { L // ↑L ⊆ ↑U' ∩ U }<VAR>L : Compacts G<VAR>L' : Compacts G := { carrier := closure ↑L, isCompact' := ⋯ }<VAR>hL : ↑L ⊆ ↑U' ∧ ↑L ⊆ U<VAR>hL'U : ↑L' ⊆ U<VAR>hL'U' : ↑L' ⊆ ↑U'<VAR>this✝ : ↑U' \ U ⊆ ↑U' \ ↑L'<VAR>this : Nonempty { M // ↑M ⊆ ↑U' \ closure ↑L }<VAR>M : Compacts G<VAR>hM : ↑M ⊆ ↑U' \ ↑L'<VAR>M' : Compacts G := { carrier := closure ↑M, isCompact' := ⋯ }<GOAL>↑(μ.toFun L') + ↑(μ.toFun ↑⟨M, hM⟩) ≤ μ.outerMeasure ↑U'
<VAR>G : Type w<VAR>inst✝² : TopologicalSpace G<VAR>μ : Content G<VAR>inst✝¹ : R1Space G<VAR>S : MeasurableSpace G<VAR>inst✝ : BorelSpace G<VAR>U : Set G<VAR>hU : U ∈ {s | IsOpen s}<VAR>U' : Opens G<VAR>this✝¹ : Nonempty { L // ↑L ⊆ ↑U' ∩ U }<VAR>L : Compacts G<VAR>L' : Compacts G := { carrier := closure ↑L, isCompact' := ⋯ }<VAR>hL : ↑L ⊆ ↑U' ∧ ↑L ⊆ U<VAR>hL'U : ↑L' ⊆ U<VAR>hL'U' : ↑L' ⊆ ↑U'<VAR>this✝ : ↑U' \ U ⊆ ↑U' \ ↑L'<VAR>this : Nonempty { M // ↑M ⊆ ↑U' \ closure ↑L }<VAR>M : Compacts G<VAR>hM : ↑M ⊆ ↑U' \ ↑L'<VAR>M' : Compacts G := { carrier := closure ↑M, isCompact' := ⋯ }<GOAL>(fun s => ↑(μ.toFun s)) L' + (fun s => ↑(μ.toFun s)) M' ≤ μ.outerMeasure ↑U'
<VAR>G : Type w<VAR>inst✝² : TopologicalSpace G<VAR>μ : Content G<VAR>inst✝¹ : R1Space G<VAR>S : MeasurableSpace G<VAR>inst✝ : BorelSpace G<VAR>U : Set G<VAR>hU : U ∈ {s | IsOpen s}<VAR>U' : Opens G<VAR>this✝¹ : Nonempty { L // ↑L ⊆ ↑U' ∩ U }<VAR>L : Compacts G<VAR>L' : Compacts G := { carrier := closure ↑L, isCompact' := ⋯ }<VAR>hL : ↑L ⊆ ↑U' ∧ ↑L ⊆ U<VAR>hL'U : ↑L' ⊆ U<VAR>hL'U' : ↑L' ⊆ ↑U'<VAR>this✝ : ↑U' \ U ⊆ ↑U' \ ↑L'<VAR>this : Nonempty { M // ↑M ⊆ ↑U' \ closure ↑L }<VAR>M : Compacts G<VAR>hM : ↑M ⊆ ↑U' \ ↑L'<VAR>M' : Compacts G := { carrier := closure ↑M, isCompact' := ⋯ }<VAR>hM' : ↑M' ⊆ ↑U' \ ↑L'<GOAL>(fun s => ↑(μ.toFun s)) L' + (fun s => ↑(μ.toFun s)) M' ≤ μ.outerMeasure ↑U'
<VAR>G : Type w<VAR>inst✝² : TopologicalSpace G<VAR>μ : Content G<VAR>inst✝¹ : R1Space G<VAR>S : MeasurableSpace G<VAR>inst✝ : BorelSpace G<VAR>U : Set G<VAR>hU : U ∈ {s | IsOpen s}<VAR>U' : Opens G<VAR>this✝² : Nonempty { L // ↑L ⊆ ↑U' ∩ U }<VAR>L : Compacts G<VAR>L' : Compacts G := { carrier := closure ↑L, isCompact' := ⋯ }<VAR>hL : ↑L ⊆ ↑U' ∧ ↑L ⊆ U<VAR>hL'U : ↑L' ⊆ U<VAR>hL'U' : ↑L' ⊆ ↑U'<VAR>this✝¹ : ↑U' \ U ⊆ ↑U' \ ↑L'<VAR>this✝ : Nonempty { M // ↑M ⊆ ↑U' \ closure ↑L }<VAR>M : Compacts G<VAR>hM : ↑M ⊆ ↑U' \ ↑L'<VAR>M' : Compacts G := { carrier := closure ↑M, isCompact' := ⋯ }<VAR>hM' : ↑M' ⊆ ↑U' \ ↑L'<VAR>this : ↑(L' ⊔ M') ⊆ ↑U'<GOAL>(fun s => ↑(μ.toFun s)) L' + (fun s => ↑(μ.toFun s)) M' ≤ μ.outerMeasure ↑U'