ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>Ω : Type u_1<VAR>MeasurableSpace Ω<VAR>μ ν : MeasureTheory.FiniteMeasure Ω<GOAL>↑(μ + ν) = ↑μ + ↑ν
<VAR>Ω : Type u_1<VAR>MeasurableSpace Ω<VAR>R : Type u_2<VAR>SMul R ℝ≥0<VAR>SMul R ℝ≥0∞<VAR>IsScalarTower R ℝ≥0 ℝ≥0∞<VAR>IsScalarTower R ℝ≥0∞ ℝ≥0∞<VAR>c : R<VAR>μ : MeasureTheory.FiniteMeasure Ω<GOAL>↑(c • μ) = c • ↑μ
<VAR>Ω : Type u_1<VAR>MeasurableSpace Ω<VAR>μ ν : MeasureTheory.FiniteMeasure Ω<GOAL>⇑(μ + ν) = ⇑μ + ⇑ν
<VAR>Ω : Type u_1<VAR>MeasurableSpace Ω<VAR>R : Type u_2<VAR>SMul R ℝ≥0<VAR>SMul R ℝ≥0∞<VAR>IsScalarTower R ℝ≥0 ℝ≥0∞<VAR>IsScalarTower R ℝ≥0∞ ℝ≥0∞<VAR>IsScalarTower R ℝ≥0 ℝ≥0<VAR>c : R<VAR>μ : MeasureTheory.FiniteMeasure Ω<GOAL>⇑(c • μ) = c • ⇑μ
<VAR>Ω : Type u_1<VAR>MeasurableSpace Ω<GOAL>∀ (a : MeasureTheory.FiniteMeasure Ω), MeasureTheory.FiniteMeasure.toMeasureAddMonoidHom a = ↑a
<VAR>Ω : Type u_1<VAR>MeasurableSpace Ω<VAR>R : Type u_2<VAR>SMul R ℝ≥0<VAR>SMul R ℝ≥0∞<VAR>IsScalarTower R ℝ≥0 ℝ≥0∞<VAR>IsScalarTower R ℝ≥0∞ ℝ≥0∞<VAR>IsScalarTower R ℝ≥0 ℝ≥0<VAR>c : R<VAR>μ : MeasureTheory.FiniteMeasure Ω<VAR>s : Set Ω<GOAL>(c • μ) s = c • μ s
<VAR>Ω : Type u_1<VAR>MeasurableSpace Ω<VAR>μ : MeasureTheory.FiniteMeasure Ω<VAR>A : Set Ω<GOAL>↑(μ.restrict A) = (↑μ).restrict A
<VAR>Ω : Type u_1<VAR>MeasurableSpace Ω<VAR>μ : MeasureTheory.FiniteMeasure Ω<VAR>A : Set Ω<VAR>s : Set Ω<VAR>s_mble : MeasurableSet s<GOAL>↑(μ.restrict A) s = ↑μ (s ∩ A)
<VAR>Ω : Type u_1<VAR>MeasurableSpace Ω<VAR>μ : MeasureTheory.FiniteMeasure Ω<VAR>A : Set Ω<VAR>s : Set Ω<VAR>s_mble : MeasurableSet s<GOAL>(μ.restrict A) s = μ (s ∩ A)
<VAR>Ω : Type u_1<VAR>MeasurableSpace Ω<VAR>μ : MeasureTheory.FiniteMeasure Ω<VAR>A : Set Ω<GOAL>(μ.restrict A).mass = μ A
<VAR>Ω : Type u_1<VAR>MeasurableSpace Ω<VAR>μ : MeasureTheory.FiniteMeasure Ω<VAR>A : Set Ω<GOAL>μ.restrict A = 0 ↔ μ A = 0
<VAR>Ω : Type u_1<VAR>MeasurableSpace Ω<VAR>μ : MeasureTheory.FiniteMeasure Ω<VAR>A : Set Ω<GOAL>μ.restrict A ≠ 0 ↔ μ A ≠ 0
<VAR>Ω : Type u_1<VAR>MeasurableSpace Ω<VAR>TopologicalSpace Ω<VAR>HasOuterApproxClosed Ω<VAR>BorelSpace Ω<VAR>μ ν : MeasureTheory.FiniteMeasure Ω<VAR>h : ∀ (f : Ω →ᵇ ℝ≥0), ∫⁻ (x : Ω), ↑(f x) ∂↑μ = ∫⁻ (x : Ω), ↑(f x) ∂↑ν<GOAL>μ = ν
<VAR>Ω : Type u_1<VAR>MeasurableSpace Ω<VAR>TopologicalSpace Ω<VAR>μ : MeasureTheory.FiniteMeasure Ω<VAR>f : Ω →ᵇ ℝ≥0<GOAL>↑(μ.testAgainstNN f) = ∫⁻ (ω : Ω), ↑(f ω) ∂↑μ
<VAR>Ω : Type u_1<VAR>MeasurableSpace Ω<VAR>TopologicalSpace Ω<VAR>μ : MeasureTheory.FiniteMeasure Ω<VAR>c : ℝ≥0<GOAL>μ.testAgainstNN (BoundedContinuousFunction.const Ω c) = c * μ.mass
<VAR>Ω : Type u_1<VAR>MeasurableSpace Ω<VAR>TopologicalSpace Ω<VAR>μ : MeasureTheory.FiniteMeasure Ω<VAR>f g : Ω →ᵇ ℝ≥0<VAR>f_le_g : ⇑f ≤ ⇑g<GOAL>μ.testAgainstNN f ≤ μ.testAgainstNN g
<VAR>Ω : Type u_1<VAR>MeasurableSpace Ω<VAR>TopologicalSpace Ω<VAR>μ : MeasureTheory.FiniteMeasure Ω<GOAL>μ.testAgainstNN 0 = 0
<VAR>Ω : Type u_1<VAR>MeasurableSpace Ω<VAR>TopologicalSpace Ω<VAR>μ : MeasureTheory.FiniteMeasure Ω<GOAL>μ.testAgainstNN 1 = μ.mass
<VAR>Ω : Type u_1<VAR>MeasurableSpace Ω<VAR>TopologicalSpace Ω<VAR>f : Ω →ᵇ ℝ≥0<GOAL>MeasureTheory.FiniteMeasure.testAgainstNN 0 f = 0
<VAR>Ω : Type u_1<VAR>MeasurableSpace Ω<VAR>TopologicalSpace Ω<GOAL>MeasureTheory.FiniteMeasure.testAgainstNN 0 = 0
<VAR>Ω : Type u_1<VAR>MeasurableSpace Ω<VAR>TopologicalSpace Ω<VAR>c : ℝ≥0<VAR>μ : MeasureTheory.FiniteMeasure Ω<VAR>f : Ω →ᵇ ℝ≥0<GOAL>(c • μ).testAgainstNN f = c • μ.testAgainstNN f
<VAR>Ω : Type u_1<VAR>MeasurableSpace Ω<VAR>TopologicalSpace Ω<VAR>OpensMeasurableSpace Ω<VAR>μ : MeasureTheory.FiniteMeasure Ω<VAR>f₁ f₂ : Ω →ᵇ ℝ≥0<GOAL>μ.testAgainstNN (f₁ + f₂) = μ.testAgainstNN f₁ + μ.testAgainstNN f₂
<VAR>Ω : Type u_1<VAR>MeasurableSpace Ω<VAR>R : Type u_2<VAR>SMul R ℝ≥0<VAR>SMul R ℝ≥0∞<VAR>IsScalarTower R ℝ≥0 ℝ≥0∞<VAR>IsScalarTower R ℝ≥0∞ ℝ≥0∞<VAR>TopologicalSpace Ω<VAR>OpensMeasurableSpace Ω<VAR>IsScalarTower R ℝ≥0 ℝ≥0<VAR>PseudoMetricSpace R<VAR>Zero R<VAR>BoundedSMul R ℝ≥0<VAR>μ : MeasureTheory.FiniteMeasure Ω<VAR>c : R<VAR>f : Ω →ᵇ ℝ≥0<GOAL>μ.testAgainstNN (c • f) = c • μ.testAgainstNN f
<VAR>Ω : Type u_1<VAR>MeasurableSpace Ω<VAR>TopologicalSpace Ω<VAR>OpensMeasurableSpace Ω<VAR>μ : MeasureTheory.FiniteMeasure Ω<VAR>f g : Ω →ᵇ ℝ≥0<GOAL>μ.testAgainstNN f ≤ μ.testAgainstNN g + nndist f g * μ.mass
<VAR>Ω : Type u_1<VAR>MeasurableSpace Ω<VAR>TopologicalSpace Ω<VAR>OpensMeasurableSpace Ω<VAR>μ : MeasureTheory.FiniteMeasure Ω<GOAL>LipschitzWith μ.mass fun f => μ.testAgainstNN f
<VAR>Ω : Type u_1<VAR>MeasurableSpace Ω<VAR>TopologicalSpace Ω<VAR>OpensMeasurableSpace Ω<VAR>μ : MeasureTheory.FiniteMeasure Ω<GOAL>⇑μ.toWeakDualBCNN = μ.testAgainstNN
<VAR>Ω : Type u_1<VAR>MeasurableSpace Ω<VAR>TopologicalSpace Ω<VAR>OpensMeasurableSpace Ω<VAR>μ : MeasureTheory.FiniteMeasure Ω<VAR>f : Ω →ᵇ ℝ≥0<GOAL>μ.toWeakDualBCNN f = (∫⁻ (x : Ω), ↑(f x) ∂↑μ).toNNReal
<VAR>Ω : Type u_1<VAR>MeasurableSpace Ω<VAR>TopologicalSpace Ω<VAR>OpensMeasurableSpace Ω<GOAL>Continuous MeasureTheory.FiniteMeasure.toWeakDualBCNN
<VAR>Ω : Type u_1<VAR>MeasurableSpace Ω<VAR>TopologicalSpace Ω<VAR>OpensMeasurableSpace Ω<VAR>f : Ω →ᵇ ℝ≥0<GOAL>Continuous fun μ => μ.testAgainstNN f
<VAR>Ω : Type u_1<VAR>MeasurableSpace Ω<VAR>TopologicalSpace Ω<VAR>OpensMeasurableSpace Ω<GOAL>Continuous fun μ => μ.mass
<VAR>Ω : Type u_1<VAR>MeasurableSpace Ω<VAR>TopologicalSpace Ω<VAR>OpensMeasurableSpace Ω<VAR>γ : Type u_3<VAR>F : Filter γ<VAR>μs : γ → MeasureTheory.FiniteMeasure Ω<VAR>μ : MeasureTheory.FiniteMeasure Ω<VAR>h : Filter.Tendsto μs F (𝓝 μ)<GOAL>Filter.Tendsto (fun i => (μs i).mass) F (𝓝 μ.mass)
<VAR>Ω : Type u_1<VAR>MeasurableSpace Ω<VAR>TopologicalSpace Ω<VAR>OpensMeasurableSpace Ω<VAR>γ : Type u_3<VAR>F : Filter γ<VAR>μs : γ → MeasureTheory.FiniteMeasure Ω<VAR>μ : MeasureTheory.FiniteMeasure Ω<GOAL>Filter.Tendsto μs F (𝓝 μ) ↔ Filter.Tendsto (fun i => (μs i).toWeakDualBCNN) F (𝓝 μ.toWeakDualBCNN)
<VAR>Ω : Type u_1<VAR>MeasurableSpace Ω<VAR>TopologicalSpace Ω<VAR>OpensMeasurableSpace Ω<VAR>γ : Type u_3<VAR>F : Filter γ<VAR>μs : γ → MeasureTheory.FiniteMeasure Ω<VAR>μ : MeasureTheory.FiniteMeasure Ω<GOAL>Filter.Tendsto μs F (𝓝 μ) ↔ ∀ (f : Ω →ᵇ ℝ≥0), Filter.Tendsto (fun i => (μs i).toWeakDualBCNN f) F (𝓝 (μ.toWeakDualBCNN f))
<VAR>Ω : Type u_1<VAR>MeasurableSpace Ω<VAR>TopologicalSpace Ω<VAR>OpensMeasurableSpace Ω<VAR>γ : Type u_3<VAR>F : Filter γ<VAR>μs : γ → MeasureTheory.FiniteMeasure Ω<VAR>μ : MeasureTheory.FiniteMeasure Ω<GOAL>Filter.Tendsto μs F (𝓝 μ) ↔ ∀ (f : Ω →ᵇ ℝ≥0), Filter.Tendsto (fun i => (μs i).testAgainstNN f) F (𝓝 (μ.testAgainstNN f))
<VAR>Ω : Type u_1<VAR>MeasurableSpace Ω<VAR>TopologicalSpace Ω<VAR>OpensMeasurableSpace Ω<VAR>γ : Type u_3<VAR>F : Filter γ<VAR>μs : γ → MeasureTheory.FiniteMeasure Ω<VAR>mass_lim : Filter.Tendsto (fun i => (μs i).mass) F (𝓝 0)<VAR>f : Ω →ᵇ ℝ≥0<GOAL>Filter.Tendsto (fun i => (μs i).testAgainstNN f) F (𝓝 0)
<VAR>Ω : Type u_1<VAR>MeasurableSpace Ω<VAR>TopologicalSpace Ω<VAR>OpensMeasurableSpace Ω<VAR>γ : Type u_3<VAR>F : Filter γ<VAR>μs : γ → MeasureTheory.FiniteMeasure Ω<VAR>mass_lim : Filter.Tendsto (fun i => (μs i).mass) F (𝓝 0)<GOAL>Filter.Tendsto μs F (𝓝 0)
<VAR>Ω : Type u_1<VAR>MeasurableSpace Ω<VAR>TopologicalSpace Ω<VAR>OpensMeasurableSpace Ω<VAR>γ : Type u_3<VAR>F : Filter γ<VAR>μs : γ → MeasureTheory.FiniteMeasure Ω<VAR>μ : MeasureTheory.FiniteMeasure Ω<GOAL>Filter.Tendsto μs F (𝓝 μ) ↔ ∀ (f : Ω →ᵇ ℝ≥0), Filter.Tendsto (fun i => ∫⁻ (x : Ω), ↑(f x) ∂↑(μs i)) F (𝓝 (∫⁻ (x : Ω), ↑(f x) ∂↑μ))
<VAR>Ω : Type u_1<VAR>MeasurableSpace Ω<VAR>TopologicalSpace Ω<VAR>HasOuterApproxClosed Ω<VAR>BorelSpace Ω<GOAL>Function.Injective MeasureTheory.FiniteMeasure.toWeakDualBCNN
<VAR>Ω : Type u_1<VAR>MeasurableSpace Ω<VAR>TopologicalSpace Ω<VAR>HasOuterApproxClosed Ω<VAR>BorelSpace Ω<GOAL>Embedding MeasureTheory.FiniteMeasure.toWeakDualBCNN
<VAR>Ω : Type u_1<VAR>MeasurableSpace Ω<VAR>TopologicalSpace Ω<VAR>OpensMeasurableSpace Ω<VAR>μ : MeasureTheory.FiniteMeasure Ω<VAR>fs : ℕ → Ω →ᵇ ℝ≥0<VAR>c : ℝ≥0<VAR>fs_le_const : ∀ (n : ℕ) (ω : Ω), (fs n) ω ≤ c<VAR>f : Ω → ℝ≥0<VAR>fs_lim : ∀ (ω : Ω), Filter.Tendsto (fun n => (fs n) ω) Filter.atTop (𝓝 (f ω))<GOAL>Filter.Tendsto (fun n => ∫⁻ (ω : Ω), ↑((fs n) ω) ∂↑μ) Filter.atTop (𝓝 (∫⁻ (ω : Ω), ↑(f ω) ∂↑μ))
<VAR>Ω : Type u_1<VAR>MeasurableSpace Ω<VAR>TopologicalSpace Ω<VAR>OpensMeasurableSpace Ω<VAR>ι : Type u_2<VAR>L : Filter ι<VAR>L.IsCountablyGenerated<VAR>μ : MeasureTheory.FiniteMeasure Ω<VAR>fs : ι → Ω →ᵇ ℝ≥0<VAR>c : ℝ≥0<VAR>fs_le_const : ∀ᶠ (i : ι) in L, ∀ᵐ (ω : Ω) ∂↑μ, (fs i) ω ≤ c<VAR>f : Ω →ᵇ ℝ≥0<VAR>fs_lim : ∀ᵐ (ω : Ω) ∂↑μ, Filter.Tendsto (fun i => (fs i) ω) L (𝓝 (f ω))<GOAL>Filter.Tendsto (fun i => μ.testAgainstNN (fs i)) L (𝓝 (μ.testAgainstNN f))
<VAR>Ω : Type u_1<VAR>MeasurableSpace Ω<VAR>TopologicalSpace Ω<VAR>OpensMeasurableSpace Ω<VAR>μ : MeasureTheory.FiniteMeasure Ω<VAR>fs : ℕ → Ω →ᵇ ℝ≥0<VAR>c : ℝ≥0<VAR>fs_le_const : ∀ (n : ℕ) (ω : Ω), (fs n) ω ≤ c<VAR>f : Ω →ᵇ ℝ≥0<VAR>fs_lim : ∀ (ω : Ω), Filter.Tendsto (fun n => (fs n) ω) Filter.atTop (𝓝 (f ω))<GOAL>Filter.Tendsto (fun n => μ.testAgainstNN (fs n)) Filter.atTop (𝓝 (μ.testAgainstNN f))
<VAR>Ω : Type u_1<VAR>MeasurableSpace Ω<VAR>TopologicalSpace Ω<VAR>OpensMeasurableSpace Ω<VAR>γ : Type u_2<VAR>F : Filter γ<VAR>μs : γ → MeasureTheory.FiniteMeasure Ω<VAR>μ : MeasureTheory.FiniteMeasure Ω<VAR>h : ∀ (f : Ω →ᵇ ℝ), Filter.Tendsto (fun i => ∫ (x : Ω), f x ∂↑(μs i)) F (𝓝 (∫ (x : Ω), f x ∂↑μ))<GOAL>Filter.Tendsto μs F (𝓝 μ)
<VAR>Ω : Type u_1<VAR>MeasurableSpace Ω<VAR>TopologicalSpace Ω<VAR>OpensMeasurableSpace Ω<VAR>γ : Type u_2<VAR>F : Filter γ<VAR>μs : γ → MeasureTheory.FiniteMeasure Ω<VAR>μ : MeasureTheory.FiniteMeasure Ω<GOAL>Filter.Tendsto μs F (𝓝 μ) ↔ ∀ (f : Ω →ᵇ ℝ), Filter.Tendsto (fun i => ∫ (x : Ω), f x ∂↑(μs i)) F (𝓝 (∫ (x : Ω), f x ∂↑μ))
<VAR>Ω : Type u_1<VAR>Ω' : Type u_2<VAR>MeasurableSpace Ω<VAR>MeasurableSpace Ω'<VAR>ν : MeasureTheory.FiniteMeasure Ω<VAR>f : Ω → Ω'<GOAL>↑(ν.map f) = MeasureTheory.Measure.map f ↑ν
<VAR>Ω : Type u_1<VAR>Ω' : Type u_2<VAR>MeasurableSpace Ω<VAR>MeasurableSpace Ω'<VAR>ν : MeasureTheory.FiniteMeasure Ω<VAR>f : Ω → Ω'<VAR>f_aemble : AEMeasurable f ↑ν<VAR>A : Set Ω'<VAR>A_mble : MeasurableSet A<GOAL>↑(ν.map f) A = ↑ν (f ⁻¹' A)
<VAR>Ω : Type u_1<VAR>Ω' : Type u_2<VAR>MeasurableSpace Ω<VAR>MeasurableSpace Ω'<VAR>ν : MeasureTheory.FiniteMeasure Ω<VAR>f : Ω → Ω'<VAR>f_aemble : AEMeasurable f ↑ν<VAR>A : Set Ω'<VAR>A_mble : MeasurableSet A<GOAL>(ν.map f) A = ν (f ⁻¹' A)
<VAR>Ω : Type u_1<VAR>Ω' : Type u_2<VAR>MeasurableSpace Ω<VAR>MeasurableSpace Ω'<VAR>ν : MeasureTheory.FiniteMeasure Ω<VAR>f : Ω → Ω'<VAR>f_mble : Measurable f<VAR>A : Set Ω'<VAR>A_mble : MeasurableSet A<GOAL>(ν.map f) A = ν (f ⁻¹' A)
<VAR>Ω : Type u_1<VAR>Ω' : Type u_2<VAR>MeasurableSpace Ω<VAR>MeasurableSpace Ω'<VAR>f : Ω → Ω'<VAR>f_mble : Measurable f<VAR>ν₁ ν₂ : MeasureTheory.FiniteMeasure Ω<GOAL>(ν₁ + ν₂).map f = ν₁.map f + ν₂.map f
<VAR>Ω : Type u_1<VAR>Ω' : Type u_2<VAR>MeasurableSpace Ω<VAR>MeasurableSpace Ω'<VAR>f : Ω → Ω'<VAR>c : ℝ≥0<VAR>ν : MeasureTheory.FiniteMeasure Ω<GOAL>(c • ν).map f = c • ν.map f
<VAR>Ω : Type u_1<VAR>Ω' : Type u_2<VAR>MeasurableSpace Ω<VAR>MeasurableSpace Ω'<VAR>TopologicalSpace Ω<VAR>OpensMeasurableSpace Ω<VAR>TopologicalSpace Ω'<VAR>BorelSpace Ω'<VAR>ι : Type u_3<VAR>L : Filter ι<VAR>νs : ι → MeasureTheory.FiniteMeasure Ω<VAR>ν : MeasureTheory.FiniteMeasure Ω<VAR>lim : Filter.Tendsto νs L (𝓝 ν)<VAR>f : Ω → Ω'<VAR>f_cont : Continuous f<GOAL>Filter.Tendsto (fun i => (νs i).map f) L (𝓝 (ν.map f))
<VAR>Ω : Type u_1<VAR>Ω' : Type u_2<VAR>MeasurableSpace Ω<VAR>MeasurableSpace Ω'<VAR>TopologicalSpace Ω<VAR>OpensMeasurableSpace Ω<VAR>TopologicalSpace Ω'<VAR>BorelSpace Ω'<VAR>f : Ω → Ω'<VAR>f_cont : Continuous f<GOAL>Continuous fun ν => ν.map f
<VAR>E : Type u_1<VAR>L : Type u_2<VAR>MeasurableSpace E<VAR>μ : MeasureTheory.Measure E<VAR>F s : Set E<VAR>AddCommGroup L<VAR>Countable L<VAR>AddAction L E<VAR>MeasurableSpace L<VAR>MeasurableVAdd L E<VAR>MeasureTheory.VAddInvariantMeasure L E μ<VAR>fund : MeasureTheory.IsAddFundamentalDomain L F μ<VAR>hS : MeasureTheory.NullMeasurableSet s μ<VAR>h : μ F < μ s<GOAL>∃ x y, x ≠ y ∧ ¬Disjoint (x +ᵥ s) (y +ᵥ s)
<VAR>E : Type u_1<VAR>MeasurableSpace E<VAR>μ : MeasureTheory.Measure E<VAR>F s : Set E<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>BorelSpace E<VAR>FiniteDimensional ℝ E<VAR>μ.IsAddHaarMeasure<VAR>L : AddSubgroup E<VAR>Countable ↥L<VAR>fund : MeasureTheory.IsAddFundamentalDomain (↥L) F μ<VAR>h_symm : ∀ x ∈ s, -x ∈ s<VAR>h_conv : Convex ℝ s<VAR>h : μ F * 2 ^ FiniteDimensional.finrank ℝ E < μ s<GOAL>∃ x, x ≠ 0 ∧ ↑x ∈ s
<VAR>E : Type u_1<VAR>MeasurableSpace E<VAR>μ : MeasureTheory.Measure E<VAR>F s : Set E<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>BorelSpace E<VAR>FiniteDimensional ℝ E<VAR>Nontrivial E<VAR>μ.IsAddHaarMeasure<VAR>L : AddSubgroup E<VAR>Countable ↥L<VAR>DiscreteTopology ↥L<VAR>fund : MeasureTheory.IsAddFundamentalDomain (↥L) F μ<VAR>h_symm : ∀ x ∈ s, -x ∈ s<VAR>h_conv : Convex ℝ s<VAR>h_cpt : IsCompact s<VAR>h : μ F * 2 ^ FiniteDimensional.finrank ℝ E ≤ μ s<GOAL>∃ x, x ≠ 0 ∧ ↑x ∈ s
<VAR>G : Type u_1<VAR>MeasurableSpace G<VAR>Group G<VAR>MeasurableMul₂ G<VAR>μ ν : MeasureTheory.Measure G<VAR>MeasureTheory.SFinite ν<VAR>MeasureTheory.SFinite μ<VAR>ν.IsMulLeftInvariant<GOAL>MeasureTheory.MeasurePreserving (fun z => (z.1, z.1 * z.2)) (μ.prod ν) (μ.prod ν)
<VAR>G : Type u_1<VAR>MeasurableSpace G<VAR>AddGroup G<VAR>MeasurableAdd₂ G<VAR>μ ν : MeasureTheory.Measure G<VAR>MeasureTheory.SFinite ν<VAR>MeasureTheory.SFinite μ<VAR>ν.IsAddLeftInvariant<GOAL>MeasureTheory.MeasurePreserving (fun z => (z.1, z.1 + z.2)) (μ.prod ν) (μ.prod ν)
<VAR>G : Type u_1<VAR>MeasurableSpace G<VAR>Group G<VAR>MeasurableMul₂ G<VAR>μ ν : MeasureTheory.Measure G<VAR>MeasureTheory.SFinite ν<VAR>MeasureTheory.SFinite μ<VAR>μ.IsMulLeftInvariant<GOAL>MeasureTheory.MeasurePreserving (fun z => (z.2, z.2 * z.1)) (μ.prod ν) (ν.prod μ)
<VAR>G : Type u_1<VAR>MeasurableSpace G<VAR>AddGroup G<VAR>MeasurableAdd₂ G<VAR>μ ν : MeasureTheory.Measure G<VAR>MeasureTheory.SFinite ν<VAR>MeasureTheory.SFinite μ<VAR>μ.IsAddLeftInvariant<GOAL>MeasureTheory.MeasurePreserving (fun z => (z.2, z.2 + z.1)) (μ.prod ν) (ν.prod μ)
<VAR>G : Type u_1<VAR>MeasurableSpace G<VAR>Group G<VAR>MeasurableMul₂ G<VAR>μ : MeasureTheory.Measure G<VAR>MeasureTheory.SFinite μ<VAR>s : Set G<VAR>hs : MeasurableSet s<GOAL>Measurable fun x => μ ((fun y => y * x) ⁻¹' s)
<VAR>G : Type u_1<VAR>MeasurableSpace G<VAR>AddGroup G<VAR>MeasurableAdd₂ G<VAR>μ : MeasureTheory.Measure G<VAR>MeasureTheory.SFinite μ<VAR>s : Set G<VAR>hs : MeasurableSet s<GOAL>Measurable fun x => μ ((fun y => y + x) ⁻¹' s)
<VAR>G : Type u_1<VAR>MeasurableSpace G<VAR>AddGroup G<VAR>MeasurableAdd₂ G<VAR>μ ν : MeasureTheory.Measure G<VAR>MeasureTheory.SFinite ν<VAR>MeasureTheory.SFinite μ<VAR>MeasurableNeg G<VAR>ν.IsAddLeftInvariant<GOAL>MeasureTheory.MeasurePreserving (fun z => (z.1, -z.1 + z.2)) (μ.prod ν) (μ.prod ν)
<VAR>G : Type u_1<VAR>MeasurableSpace G<VAR>Group G<VAR>MeasurableMul₂ G<VAR>μ ν : MeasureTheory.Measure G<VAR>MeasureTheory.SFinite ν<VAR>MeasureTheory.SFinite μ<VAR>MeasurableInv G<VAR>ν.IsMulLeftInvariant<GOAL>MeasureTheory.MeasurePreserving (fun z => (z.1, z.1⁻¹ * z.2)) (μ.prod ν) (μ.prod ν)
<VAR>G : Type u_1<VAR>MeasurableSpace G<VAR>Group G<VAR>MeasurableMul₂ G<VAR>μ ν : MeasureTheory.Measure G<VAR>MeasureTheory.SFinite ν<VAR>MeasureTheory.SFinite μ<VAR>MeasurableInv G<VAR>μ.IsMulLeftInvariant<GOAL>MeasureTheory.MeasurePreserving (fun z => (z.2, z.2⁻¹ * z.1)) (μ.prod ν) (ν.prod μ)
<VAR>G : Type u_1<VAR>MeasurableSpace G<VAR>AddGroup G<VAR>MeasurableAdd₂ G<VAR>μ ν : MeasureTheory.Measure G<VAR>MeasureTheory.SFinite ν<VAR>MeasureTheory.SFinite μ<VAR>MeasurableNeg G<VAR>μ.IsAddLeftInvariant<GOAL>MeasureTheory.MeasurePreserving (fun z => (z.2, -z.2 + z.1)) (μ.prod ν) (ν.prod μ)
<VAR>G : Type u_1<VAR>MeasurableSpace G<VAR>Group G<VAR>MeasurableMul₂ G<VAR>μ ν : MeasureTheory.Measure G<VAR>MeasureTheory.SFinite ν<VAR>MeasureTheory.SFinite μ<VAR>MeasurableInv G<VAR>μ.IsMulLeftInvariant<VAR>ν.IsMulLeftInvariant<GOAL>MeasureTheory.MeasurePreserving (fun z => (z.2 * z.1, z.1⁻¹)) (μ.prod ν) (μ.prod ν)
<VAR>G : Type u_1<VAR>MeasurableSpace G<VAR>AddGroup G<VAR>MeasurableAdd₂ G<VAR>μ ν : MeasureTheory.Measure G<VAR>MeasureTheory.SFinite ν<VAR>MeasureTheory.SFinite μ<VAR>MeasurableNeg G<VAR>μ.IsAddLeftInvariant<VAR>ν.IsAddLeftInvariant<GOAL>MeasureTheory.MeasurePreserving (fun z => (z.2 + z.1, -z.1)) (μ.prod ν) (μ.prod ν)
<VAR>G : Type u_1<VAR>MeasurableSpace G<VAR>Group G<VAR>MeasurableMul₂ G<VAR>μ : MeasureTheory.Measure G<VAR>MeasureTheory.SFinite μ<VAR>MeasurableInv G<VAR>μ.IsMulLeftInvariant<GOAL>MeasureTheory.Measure.QuasiMeasurePreserving Inv.inv μ μ
<VAR>G : Type u_1<VAR>MeasurableSpace G<VAR>AddGroup G<VAR>MeasurableAdd₂ G<VAR>μ : MeasureTheory.Measure G<VAR>MeasureTheory.SFinite μ<VAR>MeasurableNeg G<VAR>μ.IsAddLeftInvariant<GOAL>MeasureTheory.Measure.QuasiMeasurePreserving Neg.neg μ μ
<VAR>G : Type u_1<VAR>MeasurableSpace G<VAR>AddGroup G<VAR>MeasurableAdd₂ G<VAR>μ : MeasureTheory.Measure G<VAR>MeasureTheory.SFinite μ<VAR>s : Set G<VAR>MeasurableNeg G<VAR>μ.IsAddLeftInvariant<GOAL>μ (-s) = 0 ↔ μ s = 0
<VAR>G : Type u_1<VAR>MeasurableSpace G<VAR>Group G<VAR>MeasurableMul₂ G<VAR>μ : MeasureTheory.Measure G<VAR>MeasureTheory.SFinite μ<VAR>s : Set G<VAR>MeasurableInv G<VAR>μ.IsMulLeftInvariant<GOAL>μ s⁻¹ = 0 ↔ μ s = 0
<VAR>G : Type u_1<VAR>MeasurableSpace G<VAR>AddGroup G<VAR>MeasurableAdd₂ G<VAR>μ : MeasureTheory.Measure G<VAR>MeasureTheory.SFinite μ<VAR>MeasurableNeg G<VAR>μ.IsAddLeftInvariant<GOAL>-MeasureTheory.ae μ = MeasureTheory.ae μ
<VAR>G : Type u_1<VAR>MeasurableSpace G<VAR>Group G<VAR>MeasurableMul₂ G<VAR>μ : MeasureTheory.Measure G<VAR>MeasureTheory.SFinite μ<VAR>MeasurableInv G<VAR>μ.IsMulLeftInvariant<GOAL>(MeasureTheory.ae μ)⁻¹ = MeasureTheory.ae μ
<VAR>G : Type u_1<VAR>MeasurableSpace G<VAR>Group G<VAR>MeasurableMul₂ G<VAR>μ : MeasureTheory.Measure G<VAR>MeasureTheory.SFinite μ<VAR>s : Set G<VAR>MeasurableInv G<VAR>μ.IsMulLeftInvariant<GOAL>Filter.EventuallyConst s⁻¹ (MeasureTheory.ae μ) ↔ Filter.EventuallyConst s (MeasureTheory.ae μ)
<VAR>G : Type u_1<VAR>MeasurableSpace G<VAR>AddGroup G<VAR>MeasurableAdd₂ G<VAR>μ : MeasureTheory.Measure G<VAR>MeasureTheory.SFinite μ<VAR>s : Set G<VAR>MeasurableNeg G<VAR>μ.IsAddLeftInvariant<GOAL>Filter.EventuallyConst (-s) (MeasureTheory.ae μ) ↔ Filter.EventuallyConst s (MeasureTheory.ae μ)
<VAR>G : Type u_1<VAR>MeasurableSpace G<VAR>AddGroup G<VAR>MeasurableAdd₂ G<VAR>μ : MeasureTheory.Measure G<VAR>MeasureTheory.SFinite μ<VAR>MeasurableNeg G<VAR>μ.IsAddLeftInvariant<GOAL>μ.neg ≪ μ
<VAR>G : Type u_1<VAR>MeasurableSpace G<VAR>Group G<VAR>MeasurableMul₂ G<VAR>μ : MeasureTheory.Measure G<VAR>MeasureTheory.SFinite μ<VAR>MeasurableInv G<VAR>μ.IsMulLeftInvariant<GOAL>μ.inv ≪ μ
<VAR>G : Type u_1<VAR>MeasurableSpace G<VAR>AddGroup G<VAR>MeasurableAdd₂ G<VAR>μ : MeasureTheory.Measure G<VAR>MeasureTheory.SFinite μ<VAR>MeasurableNeg G<VAR>μ.IsAddLeftInvariant<GOAL>μ ≪ μ.neg
<VAR>G : Type u_1<VAR>MeasurableSpace G<VAR>Group G<VAR>MeasurableMul₂ G<VAR>μ : MeasureTheory.Measure G<VAR>MeasureTheory.SFinite μ<VAR>MeasurableInv G<VAR>μ.IsMulLeftInvariant<GOAL>μ ≪ μ.inv
<VAR>G : Type u_1<VAR>MeasurableSpace G<VAR>AddGroup G<VAR>MeasurableAdd₂ G<VAR>μ ν : MeasureTheory.Measure G<VAR>MeasureTheory.SFinite ν<VAR>MeasureTheory.SFinite μ<VAR>MeasurableNeg G<VAR>μ.IsAddLeftInvariant<VAR>ν.IsAddLeftInvariant<VAR>f : G → G → ℝ≥0∞<VAR>hf : AEMeasurable (Function.uncurry f) (μ.prod ν)<GOAL>∫⁻ (x : G), ∫⁻ (y : G), f (y + x) (-x) ∂ν ∂μ = ∫⁻ (x : G), ∫⁻ (y : G), f x y ∂ν ∂μ
<VAR>G : Type u_1<VAR>MeasurableSpace G<VAR>Group G<VAR>MeasurableMul₂ G<VAR>μ ν : MeasureTheory.Measure G<VAR>MeasureTheory.SFinite ν<VAR>MeasureTheory.SFinite μ<VAR>MeasurableInv G<VAR>μ.IsMulLeftInvariant<VAR>ν.IsMulLeftInvariant<VAR>f : G → G → ℝ≥0∞<VAR>hf : AEMeasurable (Function.uncurry f) (μ.prod ν)<GOAL>∫⁻ (x : G), ∫⁻ (y : G), f (y * x) x⁻¹ ∂ν ∂μ = ∫⁻ (x : G), ∫⁻ (y : G), f x y ∂ν ∂μ
<VAR>G : Type u_1<VAR>MeasurableSpace G<VAR>AddGroup G<VAR>MeasurableAdd₂ G<VAR>μ : MeasureTheory.Measure G<VAR>MeasureTheory.SFinite μ<VAR>s : Set G<VAR>MeasurableNeg G<VAR>μ.IsAddLeftInvariant<VAR>y : G<GOAL>μ ((fun x => x + y) ⁻¹' s) = 0 ↔ μ s = 0
<VAR>G : Type u_1<VAR>MeasurableSpace G<VAR>Group G<VAR>MeasurableMul₂ G<VAR>μ : MeasureTheory.Measure G<VAR>MeasureTheory.SFinite μ<VAR>s : Set G<VAR>MeasurableInv G<VAR>μ.IsMulLeftInvariant<VAR>y : G<GOAL>μ ((fun x => x * y) ⁻¹' s) = 0 ↔ μ s = 0
<VAR>G : Type u_1<VAR>MeasurableSpace G<VAR>AddGroup G<VAR>MeasurableAdd₂ G<VAR>μ : MeasureTheory.Measure G<VAR>MeasureTheory.SFinite μ<VAR>s : Set G<VAR>MeasurableNeg G<VAR>μ.IsAddLeftInvariant<VAR>h2s : μ s ≠ 0<VAR>y : G<GOAL>μ ((fun x => x + y) ⁻¹' s) ≠ 0
<VAR>G : Type u_1<VAR>MeasurableSpace G<VAR>Group G<VAR>MeasurableMul₂ G<VAR>μ : MeasureTheory.Measure G<VAR>MeasureTheory.SFinite μ<VAR>s : Set G<VAR>MeasurableInv G<VAR>μ.IsMulLeftInvariant<VAR>h2s : μ s ≠ 0<VAR>y : G<GOAL>μ ((fun x => x * y) ⁻¹' s) ≠ 0
<VAR>G : Type u_1<VAR>MeasurableSpace G<VAR>Group G<VAR>MeasurableMul₂ G<VAR>μ : MeasureTheory.Measure G<VAR>MeasureTheory.SFinite μ<VAR>MeasurableInv G<VAR>μ.IsMulLeftInvariant<VAR>g : G<GOAL>μ ≪ MeasureTheory.Measure.map (fun x => x * g) μ
<VAR>G : Type u_1<VAR>MeasurableSpace G<VAR>AddGroup G<VAR>MeasurableAdd₂ G<VAR>μ : MeasureTheory.Measure G<VAR>MeasureTheory.SFinite μ<VAR>MeasurableNeg G<VAR>μ.IsAddLeftInvariant<VAR>g : G<GOAL>μ ≪ MeasureTheory.Measure.map (fun x => x + g) μ
<VAR>G : Type u_1<VAR>MeasurableSpace G<VAR>AddGroup G<VAR>MeasurableAdd₂ G<VAR>μ : MeasureTheory.Measure G<VAR>MeasureTheory.SFinite μ<VAR>MeasurableNeg G<VAR>μ.IsAddLeftInvariant<VAR>g : G<GOAL>μ ≪ MeasureTheory.Measure.map (fun h => g - h) μ
<VAR>G : Type u_1<VAR>MeasurableSpace G<VAR>Group G<VAR>MeasurableMul₂ G<VAR>μ : MeasureTheory.Measure G<VAR>MeasureTheory.SFinite μ<VAR>MeasurableInv G<VAR>μ.IsMulLeftInvariant<VAR>g : G<GOAL>μ ≪ MeasureTheory.Measure.map (fun h => g / h) μ
<VAR>G : Type u_1<VAR>MeasurableSpace G<VAR>Group G<VAR>MeasurableMul₂ G<VAR>μ ν : MeasureTheory.Measure G<VAR>MeasureTheory.SFinite ν<VAR>MeasureTheory.SFinite μ<VAR>s : Set G<VAR>MeasurableInv G<VAR>μ.IsMulLeftInvariant<VAR>ν.IsMulLeftInvariant<VAR>sm : MeasurableSet s<VAR>f : G → ℝ≥0∞<VAR>hf : Measurable f<GOAL>μ s * ∫⁻ (y : G), f y ∂ν = ∫⁻ (x : G), ν ((fun z => z * x) ⁻¹' s) * f x⁻¹ ∂μ
<VAR>G : Type u_1<VAR>MeasurableSpace G<VAR>AddGroup G<VAR>MeasurableAdd₂ G<VAR>μ ν : MeasureTheory.Measure G<VAR>MeasureTheory.SFinite ν<VAR>MeasureTheory.SFinite μ<VAR>s : Set G<VAR>MeasurableNeg G<VAR>μ.IsAddLeftInvariant<VAR>ν.IsAddLeftInvariant<VAR>sm : MeasurableSet s<VAR>f : G → ℝ≥0∞<VAR>hf : Measurable f<GOAL>μ s * ∫⁻ (y : G), f y ∂ν = ∫⁻ (x : G), ν ((fun z => z + x) ⁻¹' s) * f (-x) ∂μ
<VAR>G : Type u_1<VAR>MeasurableSpace G<VAR>AddGroup G<VAR>MeasurableAdd₂ G<VAR>μ ν : MeasureTheory.Measure G<VAR>MeasureTheory.SFinite ν<VAR>MeasureTheory.SFinite μ<VAR>MeasurableNeg G<VAR>μ.IsAddLeftInvariant<VAR>ν.IsAddLeftInvariant<VAR>hν : ν ≠ 0<GOAL>μ ≪ ν
<VAR>G : Type u_1<VAR>MeasurableSpace G<VAR>Group G<VAR>MeasurableMul₂ G<VAR>μ ν : MeasureTheory.Measure G<VAR>MeasureTheory.SFinite ν<VAR>MeasureTheory.SFinite μ<VAR>MeasurableInv G<VAR>μ.IsMulLeftInvariant<VAR>ν.IsMulLeftInvariant<VAR>hν : ν ≠ 0<GOAL>μ ≪ ν
<VAR>G : Type u_1<VAR>MeasurableSpace G<VAR>Group G<VAR>MeasurableMul₂ G<VAR>s : Set G<VAR>MeasurableInv G<VAR>μ' ν' : MeasureTheory.Measure G<VAR>MeasureTheory.SigmaFinite μ'<VAR>MeasureTheory.SigmaFinite ν'<VAR>μ'.IsMulLeftInvariant<VAR>ν'.IsMulLeftInvariant<VAR>hμs : μ' s ≠ ⊤<GOAL>∀ᵐ (x : G) ∂μ', ν' ((fun x_1 => x_1 * x) ⁻¹' s) < ⊤
<VAR>G : Type u_1<VAR>MeasurableSpace G<VAR>AddGroup G<VAR>MeasurableAdd₂ G<VAR>s : Set G<VAR>MeasurableNeg G<VAR>μ' ν' : MeasureTheory.Measure G<VAR>MeasureTheory.SigmaFinite μ'<VAR>MeasureTheory.SigmaFinite ν'<VAR>μ'.IsAddLeftInvariant<VAR>ν'.IsAddLeftInvariant<VAR>hμs : μ' s ≠ ⊤<GOAL>∀ᵐ (x : G) ∂μ', ν' ((fun x_1 => x_1 + x) ⁻¹' s) < ⊤
<VAR>G : Type u_1<VAR>MeasurableSpace G<VAR>AddGroup G<VAR>MeasurableAdd₂ G<VAR>s : Set G<VAR>MeasurableNeg G<VAR>μ' ν' : MeasureTheory.Measure G<VAR>MeasureTheory.SigmaFinite μ'<VAR>MeasureTheory.SigmaFinite ν'<VAR>μ'.IsAddLeftInvariant<VAR>ν'.IsAddLeftInvariant<VAR>h2s : ν' s ≠ 0<VAR>h3s : ν' s ≠ ⊤<GOAL>∀ᵐ (x : G) ∂μ', ν' ((fun y => y + x) ⁻¹' s) < ⊤