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

Goal state before:
pp: case map_eq.inl
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace γ
δ : Type u_4
inst✝² : MeasurableSpace δ
μb : Measure β
μc : Measure γ
μd : Measure δ
inst✝¹ : SFinite μc
f : α → β
g : α → γ → δ
hgm : Measurable (uncurry g)
this : Measurable fun p ↦ (f p.1, g p.1 p.2)
inst✝ : SFinite 0
hf : MeasurePreserving f 0 μb
hg : ∀ᵐ (a : α) ∂0, map (g a) μc = μd
⊢ map (fun p ↦ (f p.1, g p.1 p.2)) (Measure.prod 0 μc) = μb.prod μd

pp: case map_eq.inr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace γ
δ : Type u_4
inst✝² : MeasurableSpace δ
μa : Measure α
μb : Measure β
μc : Measure γ
μd : Measure δ
inst✝¹ : SFinite μa
inst✝ : SFinite μc
f : α → β
hf : MeasurePreserving f μa μb
g : α → γ → δ
hgm : Measurable (uncurry g)
hg : ∀ᵐ (a : α) ∂μa, map (g a) μc = μd
this : Measurable fun p ↦ (f p.1, g p.1 p.2)
h✝ : NeZero μa
⊢ map (fun p ↦ (f p.1, g p.1 p.2)) (μa.prod μc) = μb.prod μd

Tactic:
·

Goal state after:
case map_eq.inl
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace γ
δ : Type u_4
inst✝² : MeasurableSpace δ
μb : Measure β
μc : Measure γ
μd : Measure δ
inst✝¹ : SFinite μc
f : α → β
g : α → γ → δ
hgm : Measurable (uncurry g)
this : Measurable fun p ↦ (f p.1, g p.1 p.2)
inst✝ : SFinite 0
hf : MeasurePreserving f 0 μb
hg : ∀ᵐ (a : α) ∂0, map (g a) μc = μd
⊢ map (fun p ↦ (f p.1, g p.1 p.2)) (Measure.prod 0 μc) = μb.prod μd
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: γ : Type u_3
s : Set γ
tγ : TopologicalSpace γ
inst✝¹ : PolishSpace γ
inst✝ : BorelSpace γ
this✝ : MeasurableSpace γ := borel γ
t' : TopologicalSpace γ
t't : t' ≤ tγ
t'_polish : PolishSpace γ
left✝ : IsClosed[t'] s
s_open : IsOpen[t'] s
⊢ MeasurableSet s

pp: γ : Type u_3
s : Set γ
tγ : TopologicalSpace γ
inst✝¹ : PolishSpace γ
inst✝ : BorelSpace γ
this✝ : MeasurableSpace γ := borel γ
t' : TopologicalSpace γ
t't : t' ≤ tγ
t'_polish : PolishSpace γ
left✝ : IsClosed[t'] s
s_open : IsOpen[t'] s
⊢ PolishSpace γ

Tactic:
·

Goal state after:
γ : Type u_3
s : Set γ
tγ : TopologicalSpace γ
inst✝¹ : PolishSpace γ
inst✝ : BorelSpace γ
this✝ : MeasurableSpace γ := borel γ
t' : TopologicalSpace γ
t't : t' ≤ tγ
t'_polish : PolishSpace γ
left✝ : IsClosed[t'] s
s_open : IsOpen[t'] s
⊢ MeasurableSet s
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: case iUnion.refine_1
α : Type u_1
inst✝³ : MeasurableSpace α
inst✝² : TopologicalSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
H✝ : μ.InnerRegularWRT IsClosed[inst✝²] IsOpen[inst✝²]
hfin : ∀ {s : Set α}, μ s ≠ ∞
s : ℕ → Set α
hsd : Pairwise (Function.onFun Disjoint s)
hsm : ∀ (i : ℕ), MeasurableSet (s i)
H :
  ∀ (i : ℕ) (ε : ℝ≥0∞),
    ε ≠ 0 → ∃ F ⊆ s i, ∃ U ⊇ s i, IsClosed[inst✝²] F ∧ IsOpen[inst✝²] U ∧ μ (s i) ≤ μ F + ε ∧ μ U ≤ μ (s i) + ε
ε : ℝ≥0∞
ε0 : ε ≠ 0
ε0' : ε / 2 ≠ 0
δ : ℕ → ℝ≥0∞
δ0 : ∀ (i : ℕ), 0 < δ i
hδε : ∑' (i : ℕ), δ i < ε / 2
F : ℕ → Set α
hFs : ∀ (n : ℕ), F n ⊆ s n
U : ℕ → Set α
hsU : ∀ (n : ℕ), U n ⊇ s n
hFc : ∀ (n : ℕ), IsClosed[inst✝²] (F n)
hUo : ∀ (n : ℕ), IsOpen[inst✝²] (U n)
hF : ∀ (n : ℕ), μ (s n) ≤ μ (F n) + δ n
hU : ∀ (n : ℕ), μ (U n) ≤ μ (s n) + δ n
this : Tendsto (fun t ↦ ∑ k ∈ t, μ (s k) + ε / 2) atTop (𝓝 (μ (⋃ n, s n) + ε / 2))
t : Finset ℕ
ht : μ (⋃ n, s n) < ∑ k ∈ t, μ (s k) + ε / 2
⊢ ∑ k ∈ t, μ (s k) + ε / 2 ≤ μ (⋃ k ∈ t, F k) + ε

pp: case iUnion.refine_2
α : Type u_1
inst✝³ : MeasurableSpace α
inst✝² : TopologicalSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
H✝ : μ.InnerRegularWRT IsClosed[inst✝²] IsOpen[inst✝²]
hfin : ∀ {s : Set α}, μ s ≠ ∞
s : ℕ → Set α
hsd : Pairwise (Function.onFun Disjoint s)
hsm : ∀ (i : ℕ), MeasurableSet (s i)
H :
  ∀ (i : ℕ) (ε : ℝ≥0∞),
    ε ≠ 0 → ∃ F ⊆ s i, ∃ U ⊇ s i, IsClosed[inst✝²] F ∧ IsOpen[inst✝²] U ∧ μ (s i) ≤ μ F + ε ∧ μ U ≤ μ (s i) + ε
ε : ℝ≥0∞
ε0 : ε ≠ 0
ε0' : ε / 2 ≠ 0
δ : ℕ → ℝ≥0∞
δ0 : ∀ (i : ℕ), 0 < δ i
hδε : ∑' (i : ℕ), δ i < ε / 2
F : ℕ → Set α
hFs : ∀ (n : ℕ), F n ⊆ s n
U : ℕ → Set α
hsU : ∀ (n : ℕ), U n ⊇ s n
hFc : ∀ (n : ℕ), IsClosed[inst✝²] (F n)
hUo : ∀ (n : ℕ), IsOpen[inst✝²] (U n)
hF : ∀ (n : ℕ), μ (s n) ≤ μ (F n) + δ n
hU : ∀ (n : ℕ), μ (U n) ≤ μ (s n) + δ n
this : Tendsto (fun t ↦ ∑ k ∈ t, μ (s k) + ε / 2) atTop (𝓝 (μ (⋃ n, s n) + ε / 2))
t : Finset ℕ
ht : μ (⋃ n, s n) < ∑ k ∈ t, μ (s k) + ε / 2
⊢ μ (⋃ n, U n) ≤ μ (⋃ i, s i) + ε

Tactic:
·

Goal state after:
case iUnion.refine_1
α : Type u_1
inst✝³ : MeasurableSpace α
inst✝² : TopologicalSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
H✝ : μ.InnerRegularWRT IsClosed[inst✝²] IsOpen[inst✝²]
hfin : ∀ {s : Set α}, μ s ≠ ∞
s : ℕ → Set α
hsd : Pairwise (Function.onFun Disjoint s)
hsm : ∀ (i : ℕ), MeasurableSet (s i)
H :
  ∀ (i : ℕ) (ε : ℝ≥0∞),
    ε ≠ 0 → ∃ F ⊆ s i, ∃ U ⊇ s i, IsClosed[inst✝²] F ∧ IsOpen[inst✝²] U ∧ μ (s i) ≤ μ F + ε ∧ μ U ≤ μ (s i) + ε
ε : ℝ≥0∞
ε0 : ε ≠ 0
ε0' : ε / 2 ≠ 0
δ : ℕ → ℝ≥0∞
δ0 : ∀ (i : ℕ), 0 < δ i
hδε : ∑' (i : ℕ), δ i < ε / 2
F : ℕ → Set α
hFs : ∀ (n : ℕ), F n ⊆ s n
U : ℕ → Set α
hsU : ∀ (n : ℕ), U n ⊇ s n
hFc : ∀ (n : ℕ), IsClosed[inst✝²] (F n)
hUo : ∀ (n : ℕ), IsOpen[inst✝²] (U n)
hF : ∀ (n : ℕ), μ (s n) ≤ μ (F n) + δ n
hU : ∀ (n : ℕ), μ (U n) ≤ μ (s n) + δ n
this : Tendsto (fun t ↦ ∑ k ∈ t, μ (s k) + ε / 2) atTop (𝓝 (μ (⋃ n, s n) + ε / 2))
t : Finset ℕ
ht : μ (⋃ n, s n) < ∑ k ∈ t, μ (s k) + ε / 2
⊢ ∑ k ∈ t, μ (s k) + ε / 2 ≤ μ (⋃ k ∈ t, F k) + ε
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: α : Type u_6
β : Type u_7
t : Set α
g : α → β
inst✝¹⁰ : TopologicalSpace α
inst✝⁹ : MeasurableSpace α
inst✝⁸ : BorelSpace α
inst✝⁷ : LinearOrder α
inst✝⁶ : OrderTopology α
inst✝⁵ : PolishSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : MeasurableSpace β
inst✝² : BorelSpace β
inst✝¹ : LinearOrder β
inst✝ : OrderTopology β
ht : MeasurableSet t
hg : MonotoneOn g t
h'g : ContinuousOn g t
u : Set β := {c | ∃ x y, x ∈ t ∧ y ∈ t ∧ x < y ∧ g x = c ∧ g y = c}
hu : u.Countable
t' : Set α := t ∩ g ⁻¹' u
ht' : MeasurableSet t'
⊢ MeasurableSet (g '' t)

Tactic:
have : g '' t = g '' (t \ t') ∪ g '' t' := by simp [← image_union, t']

Goal state after:
α : Type u_6
β : Type u_7
t : Set α
g : α → β
inst✝¹⁰ : TopologicalSpace α
inst✝⁹ : MeasurableSpace α
inst✝⁸ : BorelSpace α
inst✝⁷ : LinearOrder α
inst✝⁶ : OrderTopology α
inst✝⁵ : PolishSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : MeasurableSpace β
inst✝² : BorelSpace β
inst✝¹ : LinearOrder β
inst✝ : OrderTopology β
ht : MeasurableSet t
hg : MonotoneOn g t
h'g : ContinuousOn g t
u : Set β := {c | ∃ x y, x ∈ t ∧ y ∈ t ∧ x < y ∧ g x = c ∧ g y = c}
hu : u.Countable
t' : Set α := t ∩ g ⁻¹' u
ht' : MeasurableSet t'
this : g '' t = g '' (t \ t') ∪ g '' t'
⊢ MeasurableSet (g '' t)
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: case h₁
α : Type u_6
β : Type u_7
t : Set α
g : α → β
inst✝¹⁰ : TopologicalSpace α
inst✝⁹ : MeasurableSpace α
inst✝⁸ : BorelSpace α
inst✝⁷ : LinearOrder α
inst✝⁶ : OrderTopology α
inst✝⁵ : PolishSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : MeasurableSpace β
inst✝² : BorelSpace β
inst✝¹ : LinearOrder β
inst✝ : OrderTopology β
ht : MeasurableSet t
hg : MonotoneOn g t
h'g : ContinuousOn g t
u : Set β := ⋯
hu : u.Countable
t' : Set α := ⋯
ht' : MeasurableSet t'
this : g '' t = g '' (t \ t') ∪ g '' t'
⊢ MeasurableSet (g '' (t \ t'))

pp: case h₂
α : Type u_6
β : Type u_7
t : Set α
g : α → β
inst✝¹⁰ : TopologicalSpace α
inst✝⁹ : MeasurableSpace α
inst✝⁸ : BorelSpace α
inst✝⁷ : LinearOrder α
inst✝⁶ : OrderTopology α
inst✝⁵ : PolishSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : MeasurableSpace β
inst✝² : BorelSpace β
inst✝¹ : LinearOrder β
inst✝ : OrderTopology β
ht : MeasurableSet t
hg : MonotoneOn g t
h'g : ContinuousOn g t
u : Set β := ⋯
hu : u.Countable
t' : Set α := ⋯
ht' : MeasurableSet t'
this : g '' t = g '' (t \ t') ∪ g '' t'
⊢ MeasurableSet (g '' t')

Tactic:
·

Goal state after:
case h₁
α : Type u_6
β : Type u_7
t : Set α
g : α → β
inst✝¹⁰ : TopologicalSpace α
inst✝⁹ : MeasurableSpace α
inst✝⁸ : BorelSpace α
inst✝⁷ : LinearOrder α
inst✝⁶ : OrderTopology α
inst✝⁵ : PolishSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : MeasurableSpace β
inst✝² : BorelSpace β
inst✝¹ : LinearOrder β
inst✝ : OrderTopology β
ht : MeasurableSet t
hg : MonotoneOn g t
h'g : ContinuousOn g t
u : Set β := ⋯
hu : u.Countable
t' : Set α := ⋯
ht' : MeasurableSet t'
this : g '' t = g '' (t \ t') ∪ g '' t'
⊢ MeasurableSet (g '' (t \ t'))
Module: Mathlib.MeasureTheory.Group.Measure

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝³ : MeasurableSpace G
inst✝² : MeasurableSpace H
inst✝¹ : Mul G
μ : Measure G
inst✝ : μ.IsMulRightInvariant
c : ℝ≥0∞
g : G
⊢ c • Measure.map (fun x ↦ x * g) μ = c • μ

Tactic:
map_mul_right_eq_self

Goal state after:
G : Type u_1
H : Type u_2
inst✝³ : MeasurableSpace G
inst✝² : MeasurableSpace H
inst✝¹ : Mul G
μ : Measure G
inst✝ : μ.IsMulRightInvariant
c : ℝ≥0∞
g : G
⊢ c • μ = c • μ
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: case h₁.inr
α : Type u_6
β : Type u_7
t : Set α
g : α → β
inst✝¹⁰ : TopologicalSpace α
inst✝⁹ : MeasurableSpace α
inst✝⁸ : BorelSpace α
inst✝⁷ : LinearOrder α
inst✝⁶ : OrderTopology α
inst✝⁵ : PolishSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : MeasurableSpace β
inst✝² : BorelSpace β
inst✝¹ : LinearOrder β
inst✝ : OrderTopology β
ht : MeasurableSet t
hg : MonotoneOn g t
h'g : ContinuousOn g t
u : Set β := {c | ∃ x y, x ∈ t ∧ y ∈ t ∧ x < y ∧ g x = c ∧ g y = c}
hu : u.Countable
t' : Set α := t ∩ g ⁻¹' u
ht' : MeasurableSet t'
this : g '' t = g '' (t \ t') ∪ g '' t'
x : α
hx : x ∈ t \ t'
y : α
hy : y ∈ t \ t'
hxy : x ≠ y
h : ∀ ⦃x : α⦄, x ∈ t \ t' → ∀ ⦃y : α⦄, y ∈ t \ t' → x ≠ y → x < y → g x ≠ g y
H : y ≤ x
⊢ g x ≠ g y

pp: α : Type u_6
β : Type u_7
t : Set α
g : α → β
inst✝¹⁰ : TopologicalSpace α
inst✝⁹ : MeasurableSpace α
inst✝⁸ : BorelSpace α
inst✝⁷ : LinearOrder α
inst✝⁶ : OrderTopology α
inst✝⁵ : PolishSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : MeasurableSpace β
inst✝² : BorelSpace β
inst✝¹ : LinearOrder β
inst✝ : OrderTopology β
ht : MeasurableSet t
hg : MonotoneOn g t
h'g : ContinuousOn g t
u : Set β := {c | ∃ x y, x ∈ t ∧ y ∈ t ∧ x < y ∧ g x = c ∧ g y = c}
hu : u.Countable
t' : Set α := t ∩ g ⁻¹' u
ht' : MeasurableSet t'
this : g '' t = g '' (t \ t') ∪ g '' t'
x : α
hx : x ∈ t \ t'
y : α
hy : y ∈ t \ t'
hxy : x ≠ y
H : x < y
⊢ g x ≠ g y

Tactic:
·

Goal state after:
case h₁.inr
α : Type u_6
β : Type u_7
t : Set α
g : α → β
inst✝¹⁰ : TopologicalSpace α
inst✝⁹ : MeasurableSpace α
inst✝⁸ : BorelSpace α
inst✝⁷ : LinearOrder α
inst✝⁶ : OrderTopology α
inst✝⁵ : PolishSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : MeasurableSpace β
inst✝² : BorelSpace β
inst✝¹ : LinearOrder β
inst✝ : OrderTopology β
ht : MeasurableSet t
hg : MonotoneOn g t
h'g : ContinuousOn g t
u : Set β := {c | ∃ x y, x ∈ t ∧ y ∈ t ∧ x < y ∧ g x = c ∧ g y = c}
hu : u.Countable
t' : Set α := t ∩ g ⁻¹' u
ht' : MeasurableSet t'
this : g '' t = g '' (t \ t') ∪ g '' t'
x : α
hx : x ∈ t \ t'
y : α
hy : y ∈ t \ t'
hxy : x ≠ y
h : ∀ ⦃x : α⦄, x ∈ t \ t' → ∀ ⦃y : α⦄, y ∈ t \ t' → x ≠ y → x < y → g x ≠ g y
H : y ≤ x
⊢ g x ≠ g y
Module: Mathlib.MeasureTheory.Group.Measure

Goal state before:
pp: G : Type u_1
inst✝² : MeasurableSpace G
inst✝¹ : Mul G
inst✝ : MeasurableMul G
μ : Measure G
⊢ (∀ (g : G) (A : Set G), MeasurableSet A → μ ((fun h ↦ g * h) ⁻¹' A) = μ A) ↔
    ∀ (g : G), Measure.map (fun x ↦ g * x) μ = μ

pp: G : Type u_1
inst✝² : MeasurableSpace G
inst✝¹ : Mul G
inst✝ : MeasurableMul G
μ : Measure G
⊢ (∀ (g : G), Measure.map (fun x ↦ g * x) μ = μ) ↔ μ.IsMulLeftInvariant

Tactic:
·

Goal state after:
G : Type u_1
inst✝² : MeasurableSpace G
inst✝¹ : Mul G
inst✝ : MeasurableMul G
μ : Measure G
⊢ (∀ (g : G) (A : Set G), MeasurableSet A → μ ((fun h ↦ g * h) ⁻¹' A) = μ A) ↔
    ∀ (g : G), Measure.map (fun x ↦ g * x) μ = μ
Module: Mathlib.MeasureTheory.Group.Measure

Goal state before:
pp: G : Type u_1
inst✝² : MeasurableSpace G
inst✝¹ : Mul G
inst✝ : MeasurableMul G
μ : Measure G
⊢ (∀ (g : G) (A : Set G), MeasurableSet A → μ ((fun h ↦ h * g) ⁻¹' A) = μ A) ↔
    ∀ (g : G), Measure.map (fun x ↦ x * g) μ = μ

pp: G : Type u_1
inst✝² : MeasurableSpace G
inst✝¹ : Mul G
inst✝ : MeasurableMul G
μ : Measure G
⊢ (∀ (g : G), Measure.map (fun x ↦ x * g) μ = μ) ↔ μ.IsMulRightInvariant

Tactic:
·

Goal state after:
G : Type u_1
inst✝² : MeasurableSpace G
inst✝¹ : Mul G
inst✝ : MeasurableMul G
μ : Measure G
⊢ (∀ (g : G) (A : Set G), MeasurableSet A → μ ((fun h ↦ h * g) ⁻¹' A) = μ A) ↔
    ∀ (g : G), Measure.map (fun x ↦ x * g) μ = μ
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: case h₂
α : Type u_6
β : Type u_7
t : Set α
g : α → β
inst✝¹⁰ : TopologicalSpace α
inst✝⁹ : MeasurableSpace α
inst✝⁸ : BorelSpace α
inst✝⁷ : LinearOrder α
inst✝⁶ : OrderTopology α
inst✝⁵ : PolishSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : MeasurableSpace β
inst✝² : BorelSpace β
inst✝¹ : LinearOrder β
inst✝ : OrderTopology β
ht : MeasurableSet t
hg : MonotoneOn g t
h'g : ContinuousOn g t
u : Set β := ⋯
hu : u.Countable
t' : Set α := ⋯
ht' : MeasurableSet t'
this : g '' t = g '' (t \ t') ∪ g '' t'
⊢ MeasurableSet (g '' t')

Tactic:
·

Goal state after:
case h₂
α : Type u_6
β : Type u_7
t : Set α
g : α → β
inst✝¹⁰ : TopologicalSpace α
inst✝⁹ : MeasurableSpace α
inst✝⁸ : BorelSpace α
inst✝⁷ : LinearOrder α
inst✝⁶ : OrderTopology α
inst✝⁵ : PolishSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : MeasurableSpace β
inst✝² : BorelSpace β
inst✝¹ : LinearOrder β
inst✝ : OrderTopology β
ht : MeasurableSet t
hg : MonotoneOn g t
h'g : ContinuousOn g t
u : Set β := ⋯
hu : u.Countable
t' : Set α := ⋯
ht' : MeasurableSet t'
this : g '' t = g '' (t \ t') ∪ g '' t'
⊢ MeasurableSet (g '' t')
Module: Mathlib.MeasureTheory.Group.Measure

Goal state before:
pp: G : Type u_1
inst✝⁴ : MeasurableSpace G
inst✝³ : Group G
inst✝² : MeasurableMul G
H : Subgroup G
inst✝¹ : H.FiniteIndex
hH : MeasurableSet ↑H
μ : Measure G
inst✝ : μ.IsMulLeftInvariant
s : Set G
hs : Subgroup.IsComplement s ↑H
hs' : Finite ↑s
⊢ μ (⋃ i, ↑i • ↑H) = μ univ

pp: G : Type u_1
inst✝⁴ : MeasurableSpace G
inst✝³ : Group G
inst✝² : MeasurableMul G
H : Subgroup G
inst✝¹ : H.FiniteIndex
hH : MeasurableSet ↑H
μ : Measure G
inst✝ : μ.IsMulLeftInvariant
s : Set G
hs : Subgroup.IsComplement s ↑H
hs' : Finite ↑s
⊢ Pairwise (Disjoint on fun x ↦ ↑x • ↑H)

Tactic:
·

Goal state after:
G : Type u_1
inst✝⁴ : MeasurableSpace G
inst✝³ : Group G
inst✝² : MeasurableMul G
H : Subgroup G
inst✝¹ : H.FiniteIndex
hH : MeasurableSet ↑H
μ : Measure G
inst✝ : μ.IsMulLeftInvariant
s : Set G
hs : Subgroup.IsComplement s ↑H
hs' : Finite ↑s
⊢ μ (⋃ i, ↑i • ↑H) = μ univ
Module: Mathlib.MeasureTheory.Group.Measure

Goal state before:
pp: G : Type u_1
inst✝⁴ : MeasurableSpace G
inst✝³ : Group G
inst✝² : MeasurableMul G
H : Subgroup G
inst✝¹ : H.FiniteIndex
hH : MeasurableSet ↑H
μ : Measure G
inst✝ : μ.IsMulLeftInvariant
s : Set G
hs : Subgroup.IsComplement s ↑H
hs' : Finite ↑s
⊢ Pairwise (Disjoint on fun x ↦ ↑x • ↑H)

Tactic:
·

Goal state after:
G : Type u_1
inst✝⁴ : MeasurableSpace G
inst✝³ : Group G
inst✝² : MeasurableMul G
H : Subgroup G
inst✝¹ : H.FiniteIndex
hH : MeasurableSet ↑H
μ : Measure G
inst✝ : μ.IsMulLeftInvariant
s : Set G
hs : Subgroup.IsComplement s ↑H
hs' : Finite ↑s
⊢ Pairwise (Disjoint on fun x ↦ ↑x • ↑H)
Module: Mathlib.MeasureTheory.Group.Measure

Goal state before:
pp: case mp
G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul G
H : Type u_3
inst✝² : Group H
mH : MeasurableSpace H
inst✝¹ : MeasurableMul H
μ : Measure H
inst✝ : μ.IsMulLeftInvariant
f : G →* H
hf : MeasurableEmbedding ⇑f
g : G
s : Set G
hs : MeasurableSet s
x✝ : H
⊢ x✝ ∈ ⇑f '' (fun x ↦ g * x) ⁻¹' s → x✝ ∈ (fun x ↦ f g * x) ⁻¹' ⇑f '' s

pp: case mpr
G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul G
H : Type u_3
inst✝² : Group H
mH : MeasurableSpace H
inst✝¹ : MeasurableMul H
μ : Measure H
inst✝ : μ.IsMulLeftInvariant
f : G →* H
hf : MeasurableEmbedding ⇑f
g : G
s : Set G
hs : MeasurableSet s
x✝ : H
⊢ x✝ ∈ (fun x ↦ f g * x) ⁻¹' ⇑f '' s → x✝ ∈ ⇑f '' (fun x ↦ g * x) ⁻¹' s

Tactic:
·

Goal state after:
case mp
G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul G
H : Type u_3
inst✝² : Group H
mH : MeasurableSpace H
inst✝¹ : MeasurableMul H
μ : Measure H
inst✝ : μ.IsMulLeftInvariant
f : G →* H
hf : MeasurableEmbedding ⇑f
g : G
s : Set G
hs : MeasurableSet s
x✝ : H
⊢ x✝ ∈ ⇑f '' (fun x ↦ g * x) ⁻¹' s → x✝ ∈ (fun x ↦ f g * x) ⁻¹' ⇑f '' s
Module: Mathlib.MeasureTheory.Group.Measure

Goal state before:
pp: case mpr
G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul G
H : Type u_3
inst✝² : Group H
mH : MeasurableSpace H
inst✝¹ : MeasurableMul H
μ : Measure H
inst✝ : μ.IsMulLeftInvariant
f : G →* H
hf : MeasurableEmbedding ⇑f
g : G
s : Set G
hs : MeasurableSet s
x✝ : H
⊢ x✝ ∈ (fun x ↦ f g * x) ⁻¹' ⇑f '' s → x✝ ∈ ⇑f '' (fun x ↦ g * x) ⁻¹' s

Tactic:
·

Goal state after:
case mpr
G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul G
H : Type u_3
inst✝² : Group H
mH : MeasurableSpace H
inst✝¹ : MeasurableMul H
μ : Measure H
inst✝ : μ.IsMulLeftInvariant
f : G →* H
hf : MeasurableEmbedding ⇑f
g : G
s : Set G
hs : MeasurableSet s
x✝ : H
⊢ x✝ ∈ (fun x ↦ f g * x) ⁻¹' ⇑f '' s → x✝ ∈ ⇑f '' (fun x ↦ g * x) ⁻¹' s
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: case inl
ι : Type u_2
γ : Type u_3
β : Type u_5
inst✝⁶ : MeasurableSpace β
inst✝⁵ : TopologicalSpace γ
inst✝⁴ : IsCompletelyPseudoMetrizableSpace γ
inst✝³ : SecondCountableTopology γ
inst✝² : MeasurableSpace γ
hγ : OpensMeasurableSpace γ
inst✝¹ : Countable ι
f : ι → β → γ
hf : ∀ (i : ι), Measurable (f i)
inst✝ : ⊥.IsCountablyGenerated
⊢ MeasurableSet {x | ∃ c, Tendsto (fun n ↦ f n x) ⊥ (𝓝 c)}

pp: case inr
ι : Type u_2
γ : Type u_3
β : Type u_5
inst✝⁶ : MeasurableSpace β
inst✝⁵ : TopologicalSpace γ
inst✝⁴ : IsCompletelyPseudoMetrizableSpace γ
inst✝³ : SecondCountableTopology γ
inst✝² : MeasurableSpace γ
hγ : OpensMeasurableSpace γ
inst✝¹ : Countable ι
l : Filter ι
inst✝ : l.IsCountablyGenerated
f : ι → β → γ
hf : ∀ (i : ι), Measurable (f i)
hl : l.NeBot
⊢ MeasurableSet {x | ∃ c, Tendsto (fun n ↦ f n x) l (𝓝 c)}

Tactic:
·

Goal state after:
case inl
ι : Type u_2
γ : Type u_3
β : Type u_5
inst✝⁶ : MeasurableSpace β
inst✝⁵ : TopologicalSpace γ
inst✝⁴ : IsCompletelyPseudoMetrizableSpace γ
inst✝³ : SecondCountableTopology γ
inst✝² : MeasurableSpace γ
hγ : OpensMeasurableSpace γ
inst✝¹ : Countable ι
f : ι → β → γ
hf : ∀ (i : ι), Measurable (f i)
inst✝ : ⊥.IsCountablyGenerated
⊢ MeasurableSet {x | ∃ c, Tendsto (fun n ↦ f n x) ⊥ (𝓝 c)}
Module: Mathlib.MeasureTheory.Group.Measure

Goal state before:
pp: G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul G
H : Type u_3
inst✝² : Group H
mH : MeasurableSpace H
inst✝¹ : MeasurableMul H
μ : Measure H
inst✝ : μ.IsMulLeftInvariant
f : G →* H
hf : MeasurableEmbedding ⇑f
g : G
s : Set G
hs : MeasurableSet s
this : ⇑f '' (fun x ↦ g * x) ⁻¹' s = (fun x ↦ f g * x) ⁻¹' ⇑f '' s
⊢ μ (⇑f '' (fun x ↦ g * x) ⁻¹' s) = μ (⇑f '' s)

Tactic:
rw [this, ← map_apply (by fun_prop), IsMulLeftInvariant.map_mul_left_eq_self]

Goal state after:
G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul G
H : Type u_3
inst✝² : Group H
mH : MeasurableSpace H
inst✝¹ : MeasurableMul H
μ : Measure H
inst✝ : μ.IsMulLeftInvariant
f : G →* H
hf : MeasurableEmbedding ⇑f
g : G
s : Set G
hs : MeasurableSet s
this : ⇑f '' (fun x ↦ g * x) ⁻¹' s = (fun x ↦ f g * x) ⁻¹' ⇑f '' s
⊢ MeasurableSet (⇑f '' s)
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝¹ : SFinite ν
inst✝ : SFinite μ
s : Set α
t : Set β
f : α × β → ℝ≥0∞
hf : AEMeasurable f ((μ.prod ν).restrict (s ×ˢ t))
⊢ ∫⁻ (x : β) in t, ∫⁻ (y : α) in s, f (x, y).swap ∂μ ∂ν = ∫⁻ (y : β) in t, ∫⁻ (x : α) in s, f (x, y) ∂μ ∂ν

pp: case hf
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝¹ : SFinite ν
inst✝ : SFinite μ
s : Set α
t : Set β
f : α × β → ℝ≥0∞
hf : AEMeasurable f ((μ.prod ν).restrict (s ×ˢ t))
⊢ AEMeasurable (fun z ↦ f z.swap) ((ν.prod μ).restrict (t ×ˢ s))

Tactic:
·

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝¹ : SFinite ν
inst✝ : SFinite μ
s : Set α
t : Set β
f : α × β → ℝ≥0∞
hf : AEMeasurable f ((μ.prod ν).restrict (s ×ˢ t))
⊢ ∫⁻ (x : β) in t, ∫⁻ (y : α) in s, f (x, y).swap ∂μ ∂ν = ∫⁻ (y : β) in t, ∫⁻ (x : α) in s, f (x, y) ∂μ ∂ν
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: case hf
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝¹ : SFinite ν
inst✝ : SFinite μ
s : Set α
t : Set β
f : α × β → ℝ≥0∞
hf : AEMeasurable f ((μ.prod ν).restrict (s ×ˢ t))
⊢ AEMeasurable (fun z ↦ f z.swap) ((ν.prod μ).restrict (t ×ˢ s))

Tactic:
·

Goal state after:
case hf
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝¹ : SFinite ν
inst✝ : SFinite μ
s : Set α
t : Set β
f : α × β → ℝ≥0∞
hf : AEMeasurable f ((μ.prod ν).restrict (s ×ˢ t))
⊢ AEMeasurable (fun z ↦ f z.swap) ((ν.prod μ).restrict (t ×ˢ s))
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: case iUnion.refine_2
α : Type u_1
inst✝³ : MeasurableSpace α
inst✝² : TopologicalSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
H✝ : μ.InnerRegularWRT IsClosed[inst✝²] IsOpen[inst✝²]
hfin : ∀ {s : Set α}, μ s ≠ ∞
s : ℕ → Set α
hsd : Pairwise (Function.onFun Disjoint s)
hsm : ∀ (i : ℕ), MeasurableSet (s i)
H :
  ∀ (i : ℕ) (ε : ℝ≥0∞),
    ε ≠ 0 → ∃ F ⊆ s i, ∃ U ⊇ s i, IsClosed[inst✝²] F ∧ IsOpen[inst✝²] U ∧ μ (s i) ≤ μ F + ε ∧ μ U ≤ μ (s i) + ε
ε : ℝ≥0∞
ε0 : ε ≠ 0
ε0' : ε / 2 ≠ 0
δ : ℕ → ℝ≥0∞
δ0 : ∀ (i : ℕ), 0 < δ i
hδε : ∑' (i : ℕ), δ i < ε / 2
F : ℕ → Set α
hFs : ∀ (n : ℕ), F n ⊆ s n
U : ℕ → Set α
hsU : ∀ (n : ℕ), U n ⊇ s n
hFc : ∀ (n : ℕ), IsClosed[inst✝²] (F n)
hUo : ∀ (n : ℕ), IsOpen[inst✝²] (U n)
hF : ∀ (n : ℕ), μ (s n) ≤ μ (F n) + δ n
hU : ∀ (n : ℕ), μ (U n) ≤ μ (s n) + δ n
this : Tendsto (fun t ↦ ∑ k ∈ t, μ (s k) + ε / 2) atTop (𝓝 (μ (⋃ n, s n) + ε / 2))
t : Finset ℕ
ht : μ (⋃ n, s n) < ∑ k ∈ t, μ (s k) + ε / 2
⊢ μ (⋃ n, U n) ≤ μ (⋃ i, s i) + ε

Tactic:
·

Goal state after:
case iUnion.refine_2
α : Type u_1
inst✝³ : MeasurableSpace α
inst✝² : TopologicalSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
H✝ : μ.InnerRegularWRT IsClosed[inst✝²] IsOpen[inst✝²]
hfin : ∀ {s : Set α}, μ s ≠ ∞
s : ℕ → Set α
hsd : Pairwise (Function.onFun Disjoint s)
hsm : ∀ (i : ℕ), MeasurableSet (s i)
H :
  ∀ (i : ℕ) (ε : ℝ≥0∞),
    ε ≠ 0 → ∃ F ⊆ s i, ∃ U ⊇ s i, IsClosed[inst✝²] F ∧ IsOpen[inst✝²] U ∧ μ (s i) ≤ μ F + ε ∧ μ U ≤ μ (s i) + ε
ε : ℝ≥0∞
ε0 : ε ≠ 0
ε0' : ε / 2 ≠ 0
δ : ℕ → ℝ≥0∞
δ0 : ∀ (i : ℕ), 0 < δ i
hδε : ∑' (i : ℕ), δ i < ε / 2
F : ℕ → Set α
hFs : ∀ (n : ℕ), F n ⊆ s n
U : ℕ → Set α
hsU : ∀ (n : ℕ), U n ⊇ s n
hFc : ∀ (n : ℕ), IsClosed[inst✝²] (F n)
hUo : ∀ (n : ℕ), IsOpen[inst✝²] (U n)
hF : ∀ (n : ℕ), μ (s n) ≤ μ (F n) + δ n
hU : ∀ (n : ℕ), μ (U n) ≤ μ (s n) + δ n
this : Tendsto (fun t ↦ ∑ k ∈ t, μ (s k) + ε / 2) atTop (𝓝 (μ (⋃ n, s n) + ε / 2))
t : Finset ℕ
ht : μ (⋃ n, s n) < ∑ k ∈ t, μ (s k) + ε / 2
⊢ μ (⋃ n, U n) ≤ μ (⋃ i, s i) + ε