mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar

Goal state before:
pp: G : Type u_1
inst✝⁷ : Group G
inst✝⁶ : TopologicalSpace G
inst✝⁵ : MeasurableSpace G
inst✝⁴ : BorelSpace G
inst✝³ : IsTopologicalGroup G
inst✝² : LocallyCompactSpace G
μ : Measure G
inst✝¹ : μ.IsHaarMeasure
inst✝ : μ.Regular
f : G → ℝ
φ : G ≃ₜ* G
e : G ≃ᵐ G := φ.toHomeomorph.toMeasurableEquiv
this✝ : (map (⇑e.symm) μ).IsHaarMeasure
this : (map (⇑e.symm) μ).Regular
⊢ mulEquivHaarChar φ • ∫ (a : G), f a ∂map id μ = mulEquivHaarChar φ • ∫ (a : G), f a ∂μ

Tactic:
]

Goal state after:
G : Type u_1
inst✝⁷ : Group G
inst✝⁶ : TopologicalSpace G
inst✝⁵ : MeasurableSpace G
inst✝⁴ : BorelSpace G
inst✝³ : IsTopologicalGroup G
inst✝² : LocallyCompactSpace G
μ : Measure G
inst✝¹ : μ.IsHaarMeasure
inst✝ : μ.Regular
f : G → ℝ
φ : G ≃ₜ* G
e : G ≃ᵐ G := φ.toHomeomorph.toMeasurableEquiv
this✝ : (map (⇑e.symm) μ).IsHaarMeasure
this : (map (⇑e.symm) μ).Regular
⊢ mulEquivHaarChar φ • ∫ (a : G), f a ∂map id μ = mulEquivHaarChar φ • ∫ (a : G), f a ∂μ
Module: Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar

Goal state before:
pp: G : Type u_1
inst✝⁷ : Group G
inst✝⁶ : TopologicalSpace G
inst✝⁵ : MeasurableSpace G
inst✝⁴ : BorelSpace G
inst✝³ : IsTopologicalGroup G
inst✝² : LocallyCompactSpace G
μ : Measure G
inst✝¹ : μ.IsHaarMeasure
inst✝ : μ.Regular
X : Set G
φ : G ≃ₜ* G
⊢ mulEquivHaarChar φ • μ (⇑φ ⁻¹' X) = (mulEquivHaarChar φ • map (⇑φ) μ) X

Tactic:
]

Goal state after:
G : Type u_1
inst✝⁷ : Group G
inst✝⁶ : TopologicalSpace G
inst✝⁵ : MeasurableSpace G
inst✝⁴ : BorelSpace G
inst✝³ : IsTopologicalGroup G
inst✝² : LocallyCompactSpace G
μ : Measure G
inst✝¹ : μ.IsHaarMeasure
inst✝ : μ.Regular
X : Set G
φ : G ≃ₜ* G
⊢ mulEquivHaarChar φ • μ (⇑φ ⁻¹' X) = (mulEquivHaarChar φ • map (⇑φ) μ) X
Module: Mathlib.MeasureTheory.Measure.Haar.Extension

Goal state before:
pp: A : Type u_1
B : Type u_2
C : Type u_3
E : Type u_4
inst✝¹³ : Group A
inst✝¹² : Group B
inst✝¹¹ : Group C
inst✝¹⁰ : TopologicalSpace A
inst✝⁹ : TopologicalSpace B
inst✝⁸ : TopologicalSpace C
φ : A →* B
ψ : B →* C
H : IsSES φ ψ
inst✝⁷ : IsTopologicalGroup A
inst✝⁶ : IsTopologicalGroup B
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : MeasurableSpace A
inst✝³ : BorelSpace A
μA : Measure A
hμA : μA.IsHaarMeasure
inst✝² : NormedSpace ℝ E
inst✝¹ : IsTopologicalGroup C
inst✝ : LocallyCompactSpace B
f : CompactlySupportedContinuousMap B E
this : UniformSpace B := IsTopologicalGroup.rightUniformSpace B
ε : ℝ
hε : ε > 0
U₀ : Set B
hU₀ : IsCompact U₀
K : Set B
hK : IsCompact K
hf₀ : ∀ x ∉ K, f x = 0
S : Set A := ⇑φ ⁻¹' (U₀⁻¹ * K)
hSc : IsCompact S
δ : ℝ
hδ0 : δ > 0
hδ : ENNReal.ofReal δ * μA S < ENNReal.ofReal ε
hS : ∀ {x : B}, x ∈ U₀ → ∀ {y : A}, y ∉ S → (H.pullback f x) y = 0
ha✝ : ∀ r ∈ uniformity E, ∀ᶠ (x : B × B) in uniformity B, (f x.1, f x.2) ∈ r
U : Set B
hU : U ∈ nhds 1
hf : (fun p ↦ p.2 * p.1⁻¹) ⁻¹' U ⊆ {x | (fun x ↦ (f x.1, f x.2) ∈ {p | dist p.1 p.2 < δ}) x}
t : B
ht : t ∈ U⁻¹
b : B
hb : U₀ ∈ nhds b
htb : (fun x1 x2 ↦ x1 * x2) t b ∈ U₀
a : A
ha : a ∈ S
⊢ ENNReal.ofReal (dist ((H.pullback f (t * b)) a) ((H.pullback f b) a)) ≤ ENNReal.ofReal δ

Tactic:
]

Goal state after:
A : Type u_1
B : Type u_2
C : Type u_3
E : Type u_4
inst✝¹³ : Group A
inst✝¹² : Group B
inst✝¹¹ : Group C
inst✝¹⁰ : TopologicalSpace A
inst✝⁹ : TopologicalSpace B
inst✝⁸ : TopologicalSpace C
φ : A →* B
ψ : B →* C
H : IsSES φ ψ
inst✝⁷ : IsTopologicalGroup A
inst✝⁶ : IsTopologicalGroup B
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : MeasurableSpace A
inst✝³ : BorelSpace A
μA : Measure A
hμA : μA.IsHaarMeasure
inst✝² : NormedSpace ℝ E
inst✝¹ : IsTopologicalGroup C
inst✝ : LocallyCompactSpace B
f : CompactlySupportedContinuousMap B E
this : UniformSpace B := IsTopologicalGroup.rightUniformSpace B
ε : ℝ
hε : ε > 0
U₀ : Set B
hU₀ : IsCompact U₀
K : Set B
hK : IsCompact K
hf₀ : ∀ x ∉ K, f x = 0
S : Set A := ⇑φ ⁻¹' (U₀⁻¹ * K)
hSc : IsCompact S
δ : ℝ
hδ0 : δ > 0
hδ : ENNReal.ofReal δ * μA S < ENNReal.ofReal ε
hS : ∀ {x : B}, x ∈ U₀ → ∀ {y : A}, y ∉ S → (H.pullback f x) y = 0
ha✝ : ∀ r ∈ uniformity E, ∀ᶠ (x : B × B) in uniformity B, (f x.1, f x.2) ∈ r
U : Set B
hU : U ∈ nhds 1
hf : (fun p ↦ p.2 * p.1⁻¹) ⁻¹' U ⊆ {x | (fun x ↦ (f x.1, f x.2) ∈ {p | dist p.1 p.2 < δ}) x}
t : B
ht : t ∈ U⁻¹
b : B
hb : U₀ ∈ nhds b
htb : (fun x1 x2 ↦ x1 * x2) t b ∈ U₀
a : A
ha : a ∈ S
⊢ ENNReal.ofReal (dist ((H.pullback f (t * b)) a) ((H.pullback f b) a)) ≤ ENNReal.ofReal δ
Module: Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar

Goal state before:
pp: G : Type u_1
inst✝⁵ : Group G
inst✝⁴ : TopologicalSpace G
inst✝³ : MeasurableSpace G
inst✝² : BorelSpace G
inst✝¹ : IsTopologicalGroup G
inst✝ : LocallyCompactSpace G
φ ψ : G ≃ₜ* G
⊢ haar.haarScalarFactor (map (⇑(ψ.trans φ)) haar) = haar.haarScalarFactor (map (⇑ψ) haar) * mulEquivHaarChar φ

Tactic:
]

Goal state after:
G : Type u_1
inst✝⁵ : Group G
inst✝⁴ : TopologicalSpace G
inst✝³ : MeasurableSpace G
inst✝² : BorelSpace G
inst✝¹ : IsTopologicalGroup G
inst✝ : LocallyCompactSpace G
φ ψ : G ≃ₜ* G
⊢ haar.haarScalarFactor (map (⇑(ψ.trans φ)) haar) = haar.haarScalarFactor (map (⇑ψ) haar) * mulEquivHaarChar φ
Module: Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar

Goal state before:
pp: G : Type u_1
inst✝⁵ : Group G
inst✝⁴ : TopologicalSpace G
inst✝³ : MeasurableSpace G
inst✝² : BorelSpace G
inst✝¹ : IsTopologicalGroup G
inst✝ : LocallyCompactSpace G
φ ψ : G ≃ₜ* G
hφ : Measurable ⇑φ
hψ : Measurable ⇑ψ
h_reg : (map (⇑ψ) haar).Regular
⊢ haar.haarScalarFactor (map (⇑ψ) haar) * mulEquivHaarChar φ =
    haar.haarScalarFactor (map (⇑ψ) haar) * mulEquivHaarChar φ

Tactic:
]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar

Goal state before:
pp: G : Type u_1
inst✝⁶ : Group G
inst✝⁵ : TopologicalSpace G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
inst✝² : IsTopologicalGroup G
inst✝¹ : LocallyCompactSpace G
inst✝ : CompactSpace G
φ : G ≃ₜ* G
μ : Measure G := haarMeasure { carrier := univ, isCompact' := ⋯, interior_nonempty' := ⋯ }
hμ : μ univ = 1
⊢ μ.haarScalarFactor (map (⇑φ) μ) = 1

Tactic:
]

Goal state after:
G : Type u_1
inst✝⁶ : Group G
inst✝⁵ : TopologicalSpace G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
inst✝² : IsTopologicalGroup G
inst✝¹ : LocallyCompactSpace G
inst✝ : CompactSpace G
φ : G ≃ₜ* G
μ : Measure G := haarMeasure { carrier := univ, isCompact' := ⋯, interior_nonempty' := ⋯ }
hμ : μ univ = 1
⊢ μ.haarScalarFactor (map (⇑φ) μ) = 1
Module: Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar

Goal state before:
pp: G : Type u_1
inst✝⁶ : Group G
inst✝⁵ : TopologicalSpace G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
inst✝² : IsTopologicalGroup G
inst✝¹ : LocallyCompactSpace G
inst✝ : CompactSpace G
φ : G ≃ₜ* G
μ : Measure G := haarMeasure { carrier := univ, isCompact' := ⋯, interior_nonempty' := ⋯ }
hμ : μ univ = 1
⊢ ↑(μ.haarScalarFactor (map (⇑φ) μ)) = ↑(μ.haarScalarFactor (map (⇑φ) μ))

Tactic:
]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar

Goal state before:
pp: G : Type u_1
inst✝⁶ : Group G
inst✝⁵ : TopologicalSpace G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
inst✝² : IsTopologicalGroup G
inst✝¹ : LocallyCompactSpace G
inst✝ : CompactSpace G
φ : G ≃ₜ* G
μ : Measure G := haarMeasure { carrier := univ, isCompact' := ⋯, interior_nonempty' := ⋯ }
hμ : μ univ = 1
⊢ μ.haarScalarFactor (map (⇑φ) μ) • 1 = μ.haarScalarFactor (map (⇑φ) μ) • 1

Tactic:
]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric

Goal state before:
pp: case refine_2
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : PseudoMetricSpace Ω
inst✝ : OpensMeasurableSpace Ω
μs : ℕ → LevyProkhorov (ProbabilityMeasure Ω)
ν : LevyProkhorov (ProbabilityMeasure Ω)
hμs : Tendsto μs atTop (𝓝 ν)
P : ProbabilityMeasure Ω := ν.toMeasure
Ps : ℕ → ProbabilityMeasure Ω := toMeasure ∘ μs
f✝ f : Ω →ᵇ ℝ
f_nn : 0 ≤ f
f_zero : ¬‖f‖ = 0
norm_f_pos : 0 < ‖f‖
δ : ℝ
δ_pos : 0 < δ
εs : ℕ → ℝ
left✝ : StrictAnti εs
εs_lim : Tendsto εs atTop (𝓝 0)
ε_of_room : Tendsto (fun x ↦ dist (μs x) ν + εs x) atTop (𝓝 0)
ε_of_room' : Tendsto (fun n ↦ dist (μs n) ν + εs n) atTop (𝓝[>] 0)
key :
  Tendsto (fun x ↦ ∫ (t : ℝ) in Ioc 0 ‖f‖, (↑P).real (thickening (dist (μs x) ν + εs x) {a | t ≤ f a})) atTop
    (𝓝 (∫ (t : ℝ) in Ioc 0 ‖f‖, (↑P).real {a | t ≤ f a}))
aux : ∀ (z : ℝ), Iio (z + δ / 2) ∈ 𝓝 z
n : ℕ
εs_pos : 0 < εs n
hn :
  ∫ (t : ℝ) in Ioc 0 ‖f‖, (↑P).real (thickening (dist (μs n) ν + εs n) {a | t ≤ f a}) <
    (∫ (t : ℝ) in Ioc 0 ‖f‖, (↑P).real {a | t ≤ f a}) + δ / 2
hn' : dist (μs n) ν + εs n < ‖f‖⁻¹ * δ / 2
⊢ levyProkhorovEDist ↑(Ps n) ↑P + 0 < ENNReal.ofReal (dist (μs n) ν) + ENNReal.ofReal (εs n)

Tactic:
]

Goal state after:
case refine_2
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : PseudoMetricSpace Ω
inst✝ : OpensMeasurableSpace Ω
μs : ℕ → LevyProkhorov (ProbabilityMeasure Ω)
ν : LevyProkhorov (ProbabilityMeasure Ω)
hμs : Tendsto μs atTop (𝓝 ν)
P : ProbabilityMeasure Ω := ν.toMeasure
Ps : ℕ → ProbabilityMeasure Ω := toMeasure ∘ μs
f✝ f : Ω →ᵇ ℝ
f_nn : 0 ≤ f
f_zero : ¬‖f‖ = 0
norm_f_pos : 0 < ‖f‖
δ : ℝ
δ_pos : 0 < δ
εs : ℕ → ℝ
left✝ : StrictAnti εs
εs_lim : Tendsto εs atTop (𝓝 0)
ε_of_room : Tendsto (fun x ↦ dist (μs x) ν + εs x) atTop (𝓝 0)
ε_of_room' : Tendsto (fun n ↦ dist (μs n) ν + εs n) atTop (𝓝[>] 0)
key :
  Tendsto (fun x ↦ ∫ (t : ℝ) in Ioc 0 ‖f‖, (↑P).real (thickening (dist (μs x) ν + εs x) {a | t ≤ f a})) atTop
    (𝓝 (∫ (t : ℝ) in Ioc 0 ‖f‖, (↑P).real {a | t ≤ f a}))
aux : ∀ (z : ℝ), Iio (z + δ / 2) ∈ 𝓝 z
n : ℕ
εs_pos : 0 < εs n
hn :
  ∫ (t : ℝ) in Ioc 0 ‖f‖, (↑P).real (thickening (dist (μs n) ν + εs n) {a | t ≤ f a}) <
    (∫ (t : ℝ) in Ioc 0 ‖f‖, (↑P).real {a | t ≤ f a}) + δ / 2
hn' : dist (μs n) ν + εs n < ‖f‖⁻¹ * δ / 2
⊢ levyProkhorovEDist ↑(Ps n) ↑P + 0 < ENNReal.ofReal (dist (μs n) ν) + ENNReal.ofReal (εs n)
Module: Mathlib.MeasureTheory.Measure.Haar.Extension

Goal state before:
pp: A : Type u_1
B : Type u_2
C : Type u_3
E : Type u_4
inst✝¹³ : Group A
inst✝¹² : Group B
inst✝¹¹ : Group C
inst✝¹⁰ : TopologicalSpace A
inst✝⁹ : TopologicalSpace B
inst✝⁸ : TopologicalSpace C
φ : A →* B
ψ : B →* C
H : IsSES φ ψ
inst✝⁷ : IsTopologicalGroup A
inst✝⁶ : IsTopologicalGroup B
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : MeasurableSpace A
inst✝³ : BorelSpace A
μA : Measure A
hμA : μA.IsHaarMeasure
inst✝² : NormedSpace ℝ E
inst✝¹ : IsTopologicalGroup C
inst✝ : LocallyCompactSpace B
f : CompactlySupportedContinuousMap B E
this : UniformSpace B := IsTopologicalGroup.rightUniformSpace B
ε : ℝ
hε : ε > 0
U₀ : Set B
hU₀ : IsCompact U₀
K : Set B
hK : IsCompact K
hf₀ : ∀ x ∉ K, f x = 0
S : Set A := ⇑φ ⁻¹' (U₀⁻¹ * K)
hSc : IsCompact S
δ : ℝ
hδ0 : δ > 0
hδ : ENNReal.ofReal δ * μA S < ENNReal.ofReal ε
hS : ∀ {x : B}, x ∈ U₀ → ∀ {y : A}, y ∉ S → (H.pullback f x) y = 0
ha : ∀ r ∈ uniformity E, ∀ᶠ (x : B × B) in uniformity B, (f x.1, f x.2) ∈ r
U : Set B
hU : U ∈ nhds 1
hf : (fun p ↦ p.2 * p.1⁻¹) ⁻¹' U ⊆ {x | (fun x ↦ (f x.1, f x.2) ∈ {p | dist p.1 p.2 < δ}) x}
t : B
ht : t ∈ U⁻¹
b : B
hb : U₀ ∈ nhds b
htb : (fun x1 x2 ↦ x1 * x2) t b ∈ U₀
h : ∀ a ∈ S, edist ((H.pullback f (t * b)) a) ((H.pullback f b) a) ≤ ENNReal.ofReal δ
⊢ ENNReal.ofReal δ * μA S < ENNReal.ofReal ε

Tactic:
]

Goal state after:
A : Type u_1
B : Type u_2
C : Type u_3
E : Type u_4
inst✝¹³ : Group A
inst✝¹² : Group B
inst✝¹¹ : Group C
inst✝¹⁰ : TopologicalSpace A
inst✝⁹ : TopologicalSpace B
inst✝⁸ : TopologicalSpace C
φ : A →* B
ψ : B →* C
H : IsSES φ ψ
inst✝⁷ : IsTopologicalGroup A
inst✝⁶ : IsTopologicalGroup B
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : MeasurableSpace A
inst✝³ : BorelSpace A
μA : Measure A
hμA : μA.IsHaarMeasure
inst✝² : NormedSpace ℝ E
inst✝¹ : IsTopologicalGroup C
inst✝ : LocallyCompactSpace B
f : CompactlySupportedContinuousMap B E
this : UniformSpace B := IsTopologicalGroup.rightUniformSpace B
ε : ℝ
hε : ε > 0
U₀ : Set B
hU₀ : IsCompact U₀
K : Set B
hK : IsCompact K
hf₀ : ∀ x ∉ K, f x = 0
S : Set A := ⇑φ ⁻¹' (U₀⁻¹ * K)
hSc : IsCompact S
δ : ℝ
hδ0 : δ > 0
hδ : ENNReal.ofReal δ * μA S < ENNReal.ofReal ε
hS : ∀ {x : B}, x ∈ U₀ → ∀ {y : A}, y ∉ S → (H.pullback f x) y = 0
ha : ∀ r ∈ uniformity E, ∀ᶠ (x : B × B) in uniformity B, (f x.1, f x.2) ∈ r
U : Set B
hU : U ∈ nhds 1
hf : (fun p ↦ p.2 * p.1⁻¹) ⁻¹' U ⊆ {x | (fun x ↦ (f x.1, f x.2) ∈ {p | dist p.1 p.2 < δ}) x}
t : B
ht : t ∈ U⁻¹
b : B
hb : U₀ ∈ nhds b
htb : (fun x1 x2 ↦ x1 * x2) t b ∈ U₀
h : ∀ a ∈ S, edist ((H.pullback f (t * b)) a) ((H.pullback f b) a) ≤ ENNReal.ofReal δ
⊢ ENNReal.ofReal δ * μA S < ENNReal.ofReal ε
Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric

Goal state before:
pp: Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : PseudoMetricSpace Ω
inst✝ : OpensMeasurableSpace Ω
μs : ℕ → LevyProkhorov (ProbabilityMeasure Ω)
ν : LevyProkhorov (ProbabilityMeasure Ω)
hμs : Tendsto μs atTop (𝓝 ν)
P : ProbabilityMeasure Ω := ν.toMeasure
Ps : ℕ → ProbabilityMeasure Ω := toMeasure ∘ μs
f✝ f : Ω →ᵇ ℝ
f_nn : 0 ≤ f
f_zero : ¬‖f‖ = 0
norm_f_pos : 0 < ‖f‖
δ : ℝ
δ_pos : 0 < δ
εs : ℕ → ℝ
left✝ : StrictAnti εs
εs_lim : Tendsto εs atTop (𝓝 0)
ε_of_room : Tendsto (fun x ↦ dist (μs x) ν + εs x) atTop (𝓝 0)
ε_of_room' : Tendsto (fun n ↦ dist (μs n) ν + εs n) atTop (𝓝[>] 0)
key :
  Tendsto (fun x ↦ ∫ (t : ℝ) in Ioc 0 ‖f‖, (↑P).real (thickening (dist (μs x) ν + εs x) {a | t ≤ f a})) atTop
    (𝓝 (∫ (t : ℝ) in Ioc 0 ‖f‖, (↑P).real {a | t ≤ f a}))
aux : ∀ (z : ℝ), Iio (z + δ / 2) ∈ 𝓝 z
n : ℕ
εs_pos : 0 < εs n
hn :
  ∫ (t : ℝ) in Ioc 0 ‖f‖, (↑P).real (thickening (dist (μs n) ν + εs n) {a | t ≤ f a}) <
    (∫ (t : ℝ) in Ioc 0 ‖f‖, (↑P).real {a | t ≤ f a}) + δ / 2
hn' : dist (μs n) ν + εs n < ‖f‖⁻¹ * δ / 2
⊢ levyProkhorovEDist ↑(Ps n) ↑P = levyProkhorovEDist ↑(μs n).toMeasure ↑ν.toMeasure

Tactic:
]

Goal state after:
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : PseudoMetricSpace Ω
inst✝ : OpensMeasurableSpace Ω
μs : ℕ → LevyProkhorov (ProbabilityMeasure Ω)
ν : LevyProkhorov (ProbabilityMeasure Ω)
hμs : Tendsto μs atTop (𝓝 ν)
P : ProbabilityMeasure Ω := ν.toMeasure
Ps : ℕ → ProbabilityMeasure Ω := toMeasure ∘ μs
f✝ f : Ω →ᵇ ℝ
f_nn : 0 ≤ f
f_zero : ¬‖f‖ = 0
norm_f_pos : 0 < ‖f‖
δ : ℝ
δ_pos : 0 < δ
εs : ℕ → ℝ
left✝ : StrictAnti εs
εs_lim : Tendsto εs atTop (𝓝 0)
ε_of_room : Tendsto (fun x ↦ dist (μs x) ν + εs x) atTop (𝓝 0)
ε_of_room' : Tendsto (fun n ↦ dist (μs n) ν + εs n) atTop (𝓝[>] 0)
key :
  Tendsto (fun x ↦ ∫ (t : ℝ) in Ioc 0 ‖f‖, (↑P).real (thickening (dist (μs x) ν + εs x) {a | t ≤ f a})) atTop
    (𝓝 (∫ (t : ℝ) in Ioc 0 ‖f‖, (↑P).real {a | t ≤ f a}))
aux : ∀ (z : ℝ), Iio (z + δ / 2) ∈ 𝓝 z
n : ℕ
εs_pos : 0 < εs n
hn :
  ∫ (t : ℝ) in Ioc 0 ‖f‖, (↑P).real (thickening (dist (μs n) ν + εs n) {a | t ≤ f a}) <
    (∫ (t : ℝ) in Ioc 0 ‖f‖, (↑P).real {a | t ≤ f a}) + δ / 2
hn' : dist (μs n) ν + εs n < ‖f‖⁻¹ * δ / 2
⊢ levyProkhorovEDist ↑(Ps n) ↑P = levyProkhorovEDist ↑(μs n).toMeasure ↑ν.toMeasure
Module: Mathlib.MeasureTheory.Measure.Haar.Extension

Goal state before:
pp: A : Type u_1
B : Type u_2
C : Type u_3
E : Type u_4
inst✝¹³ : Group A
inst✝¹² : Group B
inst✝¹¹ : Group C
inst✝¹⁰ : TopologicalSpace A
inst✝⁹ : TopologicalSpace B
inst✝⁸ : TopologicalSpace C
φ : A →* B
ψ : B →* C
H : IsSES φ ψ
inst✝⁷ : IsTopologicalGroup A
inst✝⁶ : IsTopologicalGroup B
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : MeasurableSpace A
inst✝³ : BorelSpace A
μA : Measure A
hμA : μA.IsHaarMeasure
inst✝² : NormedSpace ℝ E
inst✝¹ : IsTopologicalGroup C
inst✝ : LocallyCompactSpace B
f : CompactlySupportedContinuousMap B E
this : UniformSpace B := IsTopologicalGroup.rightUniformSpace B
ε : ℝ
hε : ε > 0
U₀ : Set B
hU₀ : IsCompact U₀
K : Set B
hK : IsCompact K
hf₀ : ∀ x ∉ K, f x = 0
S : Set A := ⇑φ ⁻¹' (U₀⁻¹ * K)
hSc : IsCompact S
δ : ℝ
hδ0 : δ > 0
hδ : ENNReal.ofReal δ * μA S < ENNReal.ofReal ε
hS : ∀ {x : B}, x ∈ U₀ → ∀ {y : A}, y ∉ S → (H.pullback f x) y = 0
ha : ∀ r ∈ uniformity E, ∀ᶠ (x : B × B) in uniformity B, (f x.1, f x.2) ∈ r
U : Set B
hU : U ∈ nhds 1
hf : (fun p ↦ p.2 * p.1⁻¹) ⁻¹' U ⊆ {x | (fun x ↦ (f x.1, f x.2) ∈ {p | dist p.1 p.2 < δ}) x}
t : B
ht : t ∈ U⁻¹
b : B
hb : U₀ ∈ nhds b
htb : (fun x1 x2 ↦ x1 * x2) t b ∈ U₀
h : ∀ a ∈ S, edist ((H.pullback f (t * b)) a) ((H.pullback f b) a) ≤ ENNReal.ofReal δ
y : A
hy : y ∉ S
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Haar.Extension

Goal state before:
pp: A : Type u_1
B : Type u_2
C : Type u_3
E : Type u_4
inst✝¹³ : Group A
inst✝¹² : Group B
inst✝¹¹ : Group C
inst✝¹⁰ : TopologicalSpace A
inst✝⁹ : TopologicalSpace B
inst✝⁸ : TopologicalSpace C
φ : A →* B
ψ : B →* C
H : IsSES φ ψ
inst✝⁷ : IsTopologicalGroup A
inst✝⁶ : IsTopologicalGroup B
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : MeasurableSpace A
inst✝³ : BorelSpace A
μA : Measure A
hμA : μA.IsHaarMeasure
inst✝² : NormedSpace ℝ E
inst✝¹ : IsTopologicalGroup C
inst✝ : LocallyCompactSpace B
f : CompactlySupportedContinuousMap B E
K : Set B
hK : IsCompact K
hf : ∀ x ∉ K, f x = 0
x : C
hx : x ∉ ⇑ψ '' K
a : A
⊢ x ∉ ⇑ψ '' K

Tactic:
]

Goal state after:
A : Type u_1
B : Type u_2
C : Type u_3
E : Type u_4
inst✝¹³ : Group A
inst✝¹² : Group B
inst✝¹¹ : Group C
inst✝¹⁰ : TopologicalSpace A
inst✝⁹ : TopologicalSpace B
inst✝⁸ : TopologicalSpace C
φ : A →* B
ψ : B →* C
H : IsSES φ ψ
inst✝⁷ : IsTopologicalGroup A
inst✝⁶ : IsTopologicalGroup B
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : MeasurableSpace A
inst✝³ : BorelSpace A
μA : Measure A
hμA : μA.IsHaarMeasure
inst✝² : NormedSpace ℝ E
inst✝¹ : IsTopologicalGroup C
inst✝ : LocallyCompactSpace B
f : CompactlySupportedContinuousMap B E
K : Set B
hK : IsCompact K
hf : ∀ x ∉ K, f x = 0
x : C
hx : x ∉ ⇑ψ '' K
a : A
⊢ x ∉ ⇑ψ '' K
Module: Mathlib.MeasureTheory.Measure.Haar.Extension

Goal state before:
pp: A : Type u_1
B : Type u_2
C : Type u_3
E : Type u_4
inst✝¹⁵ : Group A
inst✝¹⁴ : Group B
inst✝¹³ : Group C
inst✝¹² : TopologicalSpace A
inst✝¹¹ : TopologicalSpace B
inst✝¹⁰ : TopologicalSpace C
φ : A →* B
ψ : B →* C
H : IsSES φ ψ
inst✝⁹ : IsTopologicalGroup A
inst✝⁸ : IsTopologicalGroup B
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : MeasurableSpace A
inst✝⁵ : BorelSpace A
μA : Measure A
hμA : μA.IsHaarMeasure
inst✝⁴ : NormedSpace ℝ E
inst✝³ : IsTopologicalGroup C
inst✝² : LocallyCompactSpace B
inst✝¹ : MeasurableSpace C
inst✝ : BorelSpace C
μC : Measure C
hμC : μC.IsHaarMeasure
f g : CompactlySupportedContinuousMap B E
⊢ ∫ (c : C), ((H.pushforward μA) f + (H.pushforward μA) g) c ∂μC =
    ∫ (c : C), ((H.pushforward μA) f) c ∂μC + ∫ (c : C), ((H.pushforward μA) g) c ∂μC

Tactic:
]

Goal state after:
A : Type u_1
B : Type u_2
C : Type u_3
E : Type u_4
inst✝¹⁵ : Group A
inst✝¹⁴ : Group B
inst✝¹³ : Group C
inst✝¹² : TopologicalSpace A
inst✝¹¹ : TopologicalSpace B
inst✝¹⁰ : TopologicalSpace C
φ : A →* B
ψ : B →* C
H : IsSES φ ψ
inst✝⁹ : IsTopologicalGroup A
inst✝⁸ : IsTopologicalGroup B
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : MeasurableSpace A
inst✝⁵ : BorelSpace A
μA : Measure A
hμA : μA.IsHaarMeasure
inst✝⁴ : NormedSpace ℝ E
inst✝³ : IsTopologicalGroup C
inst✝² : LocallyCompactSpace B
inst✝¹ : MeasurableSpace C
inst✝ : BorelSpace C
μC : Measure C
hμC : μC.IsHaarMeasure
f g : CompactlySupportedContinuousMap B E
⊢ ∫ (c : C), ((H.pushforward μA) f + (H.pushforward μA) g) c ∂μC =
    ∫ (c : C), ((H.pushforward μA) f) c ∂μC + ∫ (c : C), ((H.pushforward μA) g) c ∂μC
Module: Mathlib.MeasureTheory.Measure.Haar.Extension

Goal state before:
pp: A : Type u_1
B : Type u_2
C : Type u_3
E : Type u_4
inst✝¹⁵ : Group A
inst✝¹⁴ : Group B
inst✝¹³ : Group C
inst✝¹² : TopologicalSpace A
inst✝¹¹ : TopologicalSpace B
inst✝¹⁰ : TopologicalSpace C
φ : A →* B
ψ : B →* C
H : IsSES φ ψ
inst✝⁹ : IsTopologicalGroup A
inst✝⁸ : IsTopologicalGroup B
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : MeasurableSpace A
inst✝⁵ : BorelSpace A
μA : Measure A
hμA : μA.IsHaarMeasure
inst✝⁴ : NormedSpace ℝ E
inst✝³ : IsTopologicalGroup C
inst✝² : LocallyCompactSpace B
inst✝¹ : MeasurableSpace C
inst✝ : BorelSpace C
μC : Measure C
hμC : μC.IsHaarMeasure
x : ℝ
f : CompactlySupportedContinuousMap B E
⊢ ∫ (c : C), (x • (H.pushforward μA) f) c ∂μC = (RingHom.id ℝ) x • ∫ (c : C), ((H.pushforward μA) f) c ∂μC

Tactic:
]

Goal state after:
A : Type u_1
B : Type u_2
C : Type u_3
E : Type u_4
inst✝¹⁵ : Group A
inst✝¹⁴ : Group B
inst✝¹³ : Group C
inst✝¹² : TopologicalSpace A
inst✝¹¹ : TopologicalSpace B
inst✝¹⁰ : TopologicalSpace C
φ : A →* B
ψ : B →* C
H : IsSES φ ψ
inst✝⁹ : IsTopologicalGroup A
inst✝⁸ : IsTopologicalGroup B
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : MeasurableSpace A
inst✝⁵ : BorelSpace A
μA : Measure A
hμA : μA.IsHaarMeasure
inst✝⁴ : NormedSpace ℝ E
inst✝³ : IsTopologicalGroup C
inst✝² : LocallyCompactSpace B
inst✝¹ : MeasurableSpace C
inst✝ : BorelSpace C
μC : Measure C
hμC : μC.IsHaarMeasure
x : ℝ
f : CompactlySupportedContinuousMap B E
⊢ ∫ (c : C), (x • (H.pushforward μA) f) c ∂μC = (RingHom.id ℝ) x • ∫ (c : C), ((H.pushforward μA) f) c ∂μC
Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric

Goal state before:
pp: case inl.refine_1
Ω : Type u_1
inst✝³ : PseudoMetricSpace Ω
inst✝² : MeasurableSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
inst✝ : SeparableSpace Ω
ε : ℝ
ε_pos : 0 < ε
h✝ : IsEmpty Ω
⊢ ∀ (n : ℕ), diam ((fun x ↦ ∅) n) ≤ ε

pp: case inl.refine_2
Ω : Type u_1
inst✝³ : PseudoMetricSpace Ω
inst✝² : MeasurableSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
inst✝ : SeparableSpace Ω
ε : ℝ
ε_pos : 0 < ε
h✝ : IsEmpty Ω
⊢ ⋃ n, (fun x ↦ ∅) n = univ

Tactic:
· intro n
      simpa only [diam_empty] using ε_pos.le

Goal state after:
case inl.refine_2
Ω : Type u_1
inst✝³ : PseudoMetricSpace Ω
inst✝² : MeasurableSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
inst✝ : SeparableSpace Ω
ε : ℝ
ε_pos : 0 < ε
h✝ : IsEmpty Ω
⊢ ⋃ n, (fun x ↦ ∅) n = univ
Module: Mathlib.MeasureTheory.Measure.Haar.Extension

Goal state before:
pp: A : Type u_1
B : Type u_2
C : Type u_3
E : Type u_4
inst✝¹⁸ : Group A
inst✝¹⁷ : Group B
inst✝¹⁶ : Group C
inst✝¹⁵ : TopologicalSpace A
inst✝¹⁴ : TopologicalSpace B
inst✝¹³ : TopologicalSpace C
φ : A →* B
ψ : B →* C
H : IsSES φ ψ
inst✝¹² : IsTopologicalGroup A
inst✝¹¹ : IsTopologicalGroup B
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : MeasurableSpace A
inst✝⁸ : BorelSpace A
μA : Measure A
hμA : μA.IsHaarMeasure
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : IsTopologicalGroup C
inst✝⁵ : LocallyCompactSpace B
inst✝⁴ : MeasurableSpace C
inst✝³ : BorelSpace C
μC : Measure C
hμC : μC.IsHaarMeasure
inst✝² : T2Space B
inst✝¹ : MeasurableSpace B
inst✝ : BorelSpace B
b : B
this : (map (fun x ↦ b * x) (H.inducedMeasure μA μC)).Regular
f : CompactlySupportedContinuousMap B ℝ
⊢ ∫ (x : B), f (b * x) ∂H.inducedMeasure μA μC = ∫ (x : B), f x ∂H.inducedMeasure μA μC

Tactic:
]

Goal state after:
A : Type u_1
B : Type u_2
C : Type u_3
E : Type u_4
inst✝¹⁸ : Group A
inst✝¹⁷ : Group B
inst✝¹⁶ : Group C
inst✝¹⁵ : TopologicalSpace A
inst✝¹⁴ : TopologicalSpace B
inst✝¹³ : TopologicalSpace C
φ : A →* B
ψ : B →* C
H : IsSES φ ψ
inst✝¹² : IsTopologicalGroup A
inst✝¹¹ : IsTopologicalGroup B
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : MeasurableSpace A
inst✝⁸ : BorelSpace A
μA : Measure A
hμA : μA.IsHaarMeasure
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : IsTopologicalGroup C
inst✝⁵ : LocallyCompactSpace B
inst✝⁴ : MeasurableSpace C
inst✝³ : BorelSpace C
μC : Measure C
hμC : μC.IsHaarMeasure
inst✝² : T2Space B
inst✝¹ : MeasurableSpace B
inst✝ : BorelSpace B
b : B
this : (map (fun x ↦ b * x) (H.inducedMeasure μA μC)).Regular
f : CompactlySupportedContinuousMap B ℝ
⊢ ∫ (x : B), f (b * x) ∂H.inducedMeasure μA μC = ∫ (x : B), f x ∂H.inducedMeasure μA μC