mathlib-initiative/mathlib-tactics huggingface dataset:
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 μ
ν' : Measure β
inst✝ : SFinite ν'
⊢ μ.prod (ν + ν') = μ.prod ν + μ.prod ν'

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: γ : Type u_3
inst✝⁵ : TopologicalSpace γ
inst✝⁴ : PolishSpace γ
β : Type u_4
inst✝³ : TopologicalSpace β
inst✝² : T2Space β
inst✝¹ : MeasurableSpace β
inst✝ : OpensMeasurableSpace β
s : Set γ
hs : IsClosed[inst✝⁵] s
f : γ → β
f_cont : ContinuousOn f s
f_inj : InjOn f s
⊢ MeasurableSet (f '' s)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: γ : Type u_3
β : Type u_5
inst✝⁵ : MeasurableSpace β
tβ : TopologicalSpace β
inst✝⁴ : T2Space β
s : Set γ
f : γ → β
inst✝³ : OpensMeasurableSpace β
tγ : TopologicalSpace γ
inst✝² : PolishSpace γ
inst✝¹ : MeasurableSpace γ
inst✝ : BorelSpace γ
hs : MeasurableSet s
f_cont : ContinuousOn f s
f_inj : InjOn f s
⊢ MeasurableSet (f '' s)

Tactic:
by

Goal state after:
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 μ
μ' : Measure α
inst✝ : SFinite μ'
⊢ (μ + μ').prod ν = μ.prod ν + μ'.prod ν

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
ν : Measure β
⊢ Measure.prod 0 ν = 0

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
⊢ μ.prod 0 = 0

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: γ : Type u_3
α : Type u_4
inst✝³ : MeasurableSpace α
s : Set γ
f : γ → α
inst✝² : MeasurableSpace.CountablySeparated α
inst✝¹ : MeasurableSpace γ
inst✝ : StandardBorelSpace γ
hs : MeasurableSet s
f_meas : Measurable f
f_inj : InjOn f s
this : UpgradedStandardBorel γ := upgradeStandardBorel γ
tγ : TopologicalSpace γ := inferInstance
τ : TopologicalSpace α
left✝¹ : SecondCountableTopology α
left✝ : T4Space α
right✝ : OpensMeasurableSpace α
t' : TopologicalSpace γ
t't : t' ≤ tγ
f_cont : Continuous[t', τ] f
t'_polish : PolishSpace γ
⊢ MeasurableSet s

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: γ : Type u_3
α : Type u_4
inst✝³ : MeasurableSpace α
s : Set γ
f : γ → α
inst✝² : MeasurableSpace.CountablySeparated α
inst✝¹ : MeasurableSpace γ
inst✝ : StandardBorelSpace γ
hs : MeasurableSet s
f_meas : Measurable f
f_inj : InjOn f s
⊢ MeasurableSet (f '' s)

Tactic:
let := upgradeStandardBorel γ
  let tγ : TopologicalSpace γ := inferInstance
  rcases exists_opensMeasurableSpace_of_countablySeparated α with ⟨τ, _, _, _⟩
  -- for a finer Polish topology, `f` is continuous. Therefore, one may apply the corresponding
  -- result for continuous maps.
  obtain ⟨t', t't, f_cont, t'_polish⟩ :
      ∃ t' : TopologicalSpace γ, t' ≤ tγ ∧ @Continuous γ _ t' _ f ∧ @PolishSpace γ t' :=
    f_meas.exists_continuous
  have hs' := (borel_anti t't s) <| by rwa [← eq_borel_upgradeStandardBorel γ]
  let : MeasurableSpace γ := @borel γ t'
  let : BorelSpace γ := ⟨rfl⟩
  exact hs'.image_of_continuousOn_injOn f_cont.continuousOn f_inj

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: γ : Type u_3
α : Type u_4
inst✝³ : MeasurableSpace α
s : Set γ
f : γ → α
inst✝² : MeasurableSpace.CountablySeparated α
inst✝¹ : MeasurableSpace γ
inst✝ : StandardBorelSpace γ
hs : MeasurableSet s
f_meas : Measurable f
f_inj : InjOn f s
⊢ MeasurableSet (f '' s)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace γ
δ : Type u_4
inst✝² : MeasurableSpace δ
f : α → β
g : γ → δ
μa : Measure α
μc : Measure γ
inst✝¹ : SFinite μa
inst✝ : SFinite μc
hf : Measurable f
hg : Measurable g
⊢ (map f μa).prod (map g μc) = map (Prod.map f g) (μa.prod μc)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: γ : Type u_3
β : Type u_5
inst✝⁶ : MeasurableSpace β
tβ : TopologicalSpace β
inst✝⁵ : T2Space β
s : Set γ
f : γ → β
inst✝⁴ : BorelSpace β
inst✝³ : TopologicalSpace γ
inst✝² : PolishSpace γ
inst✝¹ : MeasurableSpace γ
inst✝ : BorelSpace γ
hs : MeasurableSet s
f_cont : ContinuousOn f s
f_inj : InjOn f s
⊢ ∀ ⦃s_1 : Set ↑s⦄, MeasurableSet s_1 → MeasurableSet (s.domRestrict f '' s_1)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: γ : Type u_3
t t' : TopologicalSpace γ
ht : PolishSpace γ
ht' : PolishSpace γ
hle : t ≤ t'
⊢ borel γ = borel γ

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
ν : Measure β
inst✝² : SFinite ν
μ : Measure α
R : Type u_4
inst✝¹ : SMul R ℝ≥0∞
inst✝ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
c : R
⊢ (c • μ).prod ν = c • μ.prod ν

Tactic:
by

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

Goal state before:
pp: α : 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
⊢ Tendsto (fun t ↦ ∑ k ∈ t, μ (s k) + ε / 2) atTop (𝓝 (μ (⋃ n, s n) + ε / 2))

Tactic:
by

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

Goal state before:
pp: α : 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
⊢ SFinite μd

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: γ : Type u_3
s : Set γ
tγ : TopologicalSpace γ
inst✝² : PolishSpace γ
inst✝¹ : MeasurableSpace γ
inst✝ : BorelSpace γ
⊢ IsClopenable s ↔ MeasurableSet s

Tactic:
by

Goal state after:
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
⊢ t' = ⋃ c ∈ u, t ∩ g ⁻¹' {c}

Tactic:
by

Goal state after:
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
⊢ MeasurableSet t'

Tactic:
by

Goal state after:
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'
⊢ g '' t = g '' (t \ t') ∪ g '' t'

Tactic:
by

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

Goal state before:
pp: α : 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
⊢ MeasurePreserving (fun p ↦ (f p.1, g p.1 p.2)) (μa.prod μc) (μb.prod μd)

Tactic:
by

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

Goal state before:
pp: α : 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) + ∑ k ∈ t, δ k + ε / 2

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
f : α × β → γ
μ : Measure α
ν : Measure β
τ : Measure γ
hf : Measurable f
inst✝ : SFinite ν
h2f : ∀ᵐ (x : α) ∂μ, QuasiMeasurePreserving (fun y ↦ f (x, y)) ν τ
⊢ QuasiMeasurePreserving f (μ.prod ν) τ

Tactic:
by

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

Goal state before:
pp: α : 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, μ (F k) + ∑ k ∈ t, δ k + ε / 2 ≤ ∑ k ∈ t, μ (F k) + ε / 2 + ε / 2

Tactic:
by

Goal state after:
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✝ : μ.IsMulLeftInvariant
c : ℝ≥0∞
g : G
⊢ Measure.map (fun x ↦ g * x) (c • μ) = c • μ

Tactic:
by

Goal state after:
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
⊢ Measure.map (fun x ↦ x * g) (c • μ) = c • μ

Tactic:
by

Goal state after:
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✝⁴ : MeasurableMul G✝
G : Type u_3
α : Type u_4
inst✝³ : Group G
inst✝² : MulAction G α
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : SMulInvariantMeasure G α μ
H : Subgroup G
y : ↥H
s : Set α
hs : MeasurableSet s
⊢ μ ((fun x ↦ y • x) ⁻¹' s) = μ s

Tactic:
by

Goal state after:
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) ↔ μ.IsMulLeftInvariant

Tactic:
by

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

Goal state before:
pp: α : Type u_4
β : Type u_5
γ : Type u_6
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
f : α × β → γ
μ : Measure α
ν : Measure β
τ : Measure γ
hf : Measurable f
inst✝¹ : SFinite μ
inst✝ : SFinite ν
h2f : ∀ᵐ (y : β) ∂ν, QuasiMeasurePreserving (fun x ↦ f (x, y)) μ τ
⊢ QuasiMeasurePreserving f (μ.prod ν) τ

Tactic:
by

Goal state after:
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) ↔ μ.IsMulRightInvariant

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace γ
μ : Measure α
ν : Measure β
τ : Measure γ
ω : Type u_4
mω : MeasurableSpace ω
υ : Measure ω
inst✝² : SFinite μ
inst✝¹ : SFinite τ
inst✝ : SFinite υ
f : α → β
g : γ → ω
hf : QuasiMeasurePreserving f μ ν
hg : QuasiMeasurePreserving g τ υ
⊢ Measurable (Prod.map f g)

Tactic:
by

Goal state after:
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✝⁶ : MeasurableMul G
inst✝⁵ : μ.IsMulLeftInvariant
inst✝⁴ : SFinite μ
H : Type u_3
inst✝³ : Mul H
mH : MeasurableSpace H
ν : Measure H
inst✝² : MeasurableMul H
inst✝¹ : ν.IsMulLeftInvariant
inst✝ : SFinite ν
⊢ (μ.prod ν).IsMulLeftInvariant

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace γ
μ : Measure α
ν : Measure β
τ : Measure γ
ω : Type u_4
mω : MeasurableSpace ω
υ : Measure ω
inst✝² : SFinite μ
inst✝¹ : SFinite τ
inst✝ : SFinite υ
f : α → β
g : γ → ω
hf : QuasiMeasurePreserving f μ ν
hg : QuasiMeasurePreserving g τ υ
⊢ Measurable f

Tactic:
by

Goal state after:
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'
this : g '' t = g '' (t \ t') ∪ g '' t'
x : α
hx : x ∈ t \ t'
y : α
hy : y ∈ t \ t'
hxy : x ≠ y
H : x < y
h : g x = g y
⊢ False

Tactic:
exact hx.2 ⟨hx.1, x, y, hx.1, hy.1, H, rfl, h.symm⟩

Goal state after:
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✝⁶ : MeasurableMul G
inst✝⁵ : μ.IsMulRightInvariant
inst✝⁴ : SFinite μ
H : Type u_3
inst✝³ : Mul H
mH : MeasurableSpace H
ν : Measure H
inst✝² : MeasurableMul H
inst✝¹ : ν.IsMulRightInvariant
inst✝ : SFinite ν
⊢ (μ.prod ν).IsMulRightInvariant

Tactic:
by

Goal state after:
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'
this : g '' t = g '' (t \ t') ∪ g '' t'
⊢ g '' t' ⊆ u

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace γ
μ : Measure α
ν : Measure β
τ : Measure γ
ω : Type u_4
mω : MeasurableSpace ω
υ : Measure ω
inst✝² : SFinite μ
inst✝¹ : SFinite τ
inst✝ : SFinite υ
f : α → β
g : γ → ω
hf : QuasiMeasurePreserving f μ ν
hg : QuasiMeasurePreserving g τ υ
⊢ Measurable g

Tactic:
by

Goal state after:
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
⊢ MeasurableSet (g '' t)

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝⁶ : MeasurableSpace G
inst✝⁵ : Mul G
μ : Measure G
inst✝⁴ : MeasurableMul G
H : Type u_3
inst✝³ : MeasurableSpace H
inst✝² : Mul H
inst✝¹ : MeasurableMul H
inst✝ : μ.IsMulLeftInvariant
f : G →ₙ* H
hf : Measurable ⇑f
h_surj : Surjective ⇑f
⊢ (Measure.map (⇑f) μ).IsMulLeftInvariant

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝² : MeasurableSpace G
inst✝¹ : DivInvMonoid G
μ : Measure G
inst✝ : μ.IsMulRightInvariant
g : G
⊢ Measure.map (fun x ↦ x / g) μ = μ

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝³ : MeasurableSpace G
inst✝² : Group G
inst✝¹ : MeasurableMul G
μ : Measure G
inst✝ : μ.IsMulRightInvariant
g : G
⊢ MeasurePreserving (fun x ↦ x / g) μ μ

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝³ : MeasurableSpace G
inst✝² : Group G
inst✝¹ : MeasurableMul G
μ : Measure G
inst✝ : μ.IsMulLeftInvariant
g : G
A : Set G
⊢ (Measure.map (fun h ↦ g * h) μ) A = μ A

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝³ : MeasurableSpace G
inst✝² : Group G
inst✝¹ : MeasurableMul G
μ : Measure G
inst✝ : μ.IsMulRightInvariant
g : G
A : Set G
⊢ (Measure.map (fun h ↦ h * g) μ) A = μ A

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace γ
μ : Measure α
ν : Measure β
τ : Measure γ
ω : Type u_4
mω : MeasurableSpace ω
υ : Measure ω
inst✝² : SFinite μ
inst✝¹ : SFinite τ
inst✝ : SFinite υ
f : α → β
g : γ → ω
hf : QuasiMeasurePreserving f μ ν
hg : QuasiMeasurePreserving g τ υ
⊢ QuasiMeasurePreserving (Prod.map f g) (μ.prod τ) (ν.prod υ)

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝³ : MeasurableSpace G
inst✝² : Group G
inst✝¹ : MeasurableMul G
μ : Measure G
inst✝ : μ.IsMulLeftInvariant
t : G
p : G → Prop
⊢ (∀ᵐ (x : G) ∂μ, p (t * x)) ↔ ∀ᵐ (x : G) ∂μ, p x

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝³ : MeasurableSpace G
inst✝² : Group G
inst✝¹ : MeasurableMul G
μ : Measure G
inst✝ : μ.IsMulRightInvariant
t : G
p : G → Prop
⊢ (∀ᵐ (x : G) ∂μ, p (x * t)) ↔ ∀ᵐ (x : G) ∂μ, p x

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
μ : Measure α
ν : Measure β
inst✝¹ : SFinite μ
inst✝ : SFinite ν
f : β × α → γ
hf : AEMeasurable f (ν.prod μ)
⊢ AEMeasurable (fun z ↦ f z.swap) (μ.prod ν)

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝³ : MeasurableSpace G
inst✝² : Group G
inst✝¹ : MeasurableMul G
μ : Measure G
inst✝ : μ.IsMulRightInvariant
t : G
p : G → Prop
⊢ (∀ᵐ (x : G) ∂μ, p (x / t)) ↔ ∀ᵐ (x : G) ∂μ, p x

Tactic:
by

Goal state after:
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
⊢ ↑H.index * μ ↑H = ∑' (a : ↑s), μ (↑a • ↑H)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝ : SFinite ν
f g : α × β → ℝ≥0∞
hg : Measurable g
hfg : f =ᵐ[μ.prod ν] g
⊢ Measurable fun x ↦ ∫⁻ (y : β), g (x, y) ∂ν

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝ : SFinite ν
f : α × β → ℝ≥0∞
hf : AEMeasurable f (μ.prod ν)
⊢ AEMeasurable (fun x ↦ ∫⁻ (y : β), f (x, y) ∂ν) μ

Tactic:
by

Goal state after:
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
⊢ ∑' (a : ↑s), μ (↑a • ↑H) = μ univ

Tactic:
by

Goal state after:
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 β
inst✝ : SecondCountableTopology β
ht : MeasurableSet t
hg : MonotoneOn g t
t' : Set α := {x | x ∈ t ∧ ¬ContinuousWithinAt g t x}
ht' : t'.Countable
⊢ g '' t = g '' (t \ t') ∪ g '' t'

Tactic:
by

Goal state after:
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
⊢ ↑H.index * μ ↑H = μ univ

Tactic:
by

Goal state after: