mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Group.Convolution

Goal state before:
pp: M : Type u_1
inst✝³ : Monoid M
inst✝² : MeasurableSpace M
inst✝¹ : MeasurableMul₂ M
μ : Measure M
inst✝ : SFinite μ
x : M
⊢ Measurable fun x_1 ↦ (x_1, x)

Tactic:
by

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

Goal state before:
pp: M : Type u_1
inst✝³ : Monoid M
inst✝² : MeasurableSpace M
inst✝¹ : MeasurableMul₂ M
μ : Measure M
inst✝ : SFinite μ
x : M
⊢ μ ∗ₘ dirac x = map (fun y ↦ y * x) μ

Tactic:
by

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

Goal state before:
pp: M : Type u_1
inst✝² : Monoid M
inst✝¹ : MeasurableSpace M
inst✝ : MeasurableMul₂ M
x y : M
⊢ Measurable fun y_1 ↦ y_1 * y

Tactic:
by

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

Goal state before:
pp: M : Type u_1
inst✝² : Monoid M
inst✝¹ : MeasurableSpace M
inst✝ : MeasurableMul₂ M
x y : M
⊢ dirac x ∗ₘ dirac y = dirac (x * y)

Tactic:
by

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

Goal state before:
pp: M : Type u_1
inst✝³ : Monoid M
inst✝² : MeasurableSpace M
inst✝¹ : MeasurableMul₂ M
μ : Measure M
inst✝ : SFinite μ
⊢ dirac 1 ∗ₘ μ = μ

Tactic:
by

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

Goal state before:
pp: M : Type u_1
inst✝³ : Monoid M
inst✝² : MeasurableSpace M
inst✝¹ : MeasurableMul₂ M
μ : Measure M
inst✝ : SFinite μ
⊢ μ ∗ₘ dirac 1 = μ

Tactic:
by

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

Goal state before:
pp: M : Type u_1
inst✝¹ : Monoid M
inst✝ : MeasurableSpace M
μ : Measure M
⊢ 0 ∗ₘ μ = 0

Tactic:
by

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

Goal state before:
pp: M : Type u_1
inst✝¹ : Monoid M
inst✝ : MeasurableSpace M
μ : Measure M
⊢ μ ∗ₘ 0 = 0

Tactic:
by

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

Goal state before:
pp: M : Type u_1
inst✝² : Monoid M
inst✝¹ : MeasurableSpace M
μ ν : Measure M
inst✝ : SFinite ν
s : ℝ≥0∞
⊢ (s • μ) ∗ₘ ν = s • μ ∗ₘ ν

Tactic:
by

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

Goal state before:
pp: M : Type u_1
inst✝⁵ : Monoid M
inst✝⁴ : MeasurableSpace M
inst✝³ : MeasurableMul₂ M
μ ν ρ : Measure M
inst✝² : SFinite μ
inst✝¹ : SFinite ν
inst✝ : SFinite ρ
⊢ μ ∗ₘ (ν + ρ) = μ ∗ₘ ν + μ ∗ₘ ρ

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α →ₛ ℝ≥0
L : ℝ≥0∞
hL : L < ∫⁻ (x : α), ↑(f x) ∂μ
⊢ ∃ g, (∀ (x : α), g x ≤ f x) ∧ ∫⁻ (x : α), ↑(g x) ∂μ < ∞ ∧ L < ∫⁻ (x : α), ↑(g x) ∂μ

Tactic:
by

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

Goal state before:
pp: M : Type u_1
inst✝⁵ : Monoid M
inst✝⁴ : MeasurableSpace M
inst✝³ : MeasurableMul₂ M
μ ν ρ : Measure M
inst✝² : SFinite μ
inst✝¹ : SFinite ν
inst✝ : SFinite ρ
⊢ (μ + ν) ∗ₘ ρ = μ ∗ₘ ρ + ν ∗ₘ ρ

Tactic:
by

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

Goal state before:
pp: M : Type u_2
inst✝⁴ : CommMonoid M
inst✝³ : MeasurableSpace M
inst✝² : MeasurableMul₂ M
μ ν : Measure M
inst✝¹ : SFinite μ
inst✝ : SFinite ν
⊢ Measurable fun x ↦ x.1 * x.2

Tactic:
by

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

Goal state before:
pp: M : Type u_2
inst✝⁴ : CommMonoid M
inst✝³ : MeasurableSpace M
inst✝² : MeasurableMul₂ M
μ ν : Measure M
inst✝¹ : SFinite μ
inst✝ : SFinite ν
⊢ μ ∗ₘ ν = ν ∗ₘ μ

Tactic:
by

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

Goal state before:
pp: M : Type u_1
inst✝³ : Monoid M
inst✝² : MeasurableSpace M
μ ν : Measure M
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
⊢ (μ ∗ₘ ν) Set.univ < ∞

Tactic:
by

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

Goal state before:
pp: M : Type u_1
inst✝³ : Monoid M
inst✝² : MeasurableSpace M
μ ν : Measure M
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
⊢ IsFiniteMeasure (μ ∗ₘ ν)

Tactic:
by

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

Goal state before:
pp: M : Type u_1
inst✝⁴ : Monoid M
inst✝³ : MeasurableSpace M
inst✝² : MeasurableMul₂ M
μ ν ρ : Measure M
inst✝¹ : SFinite ν
inst✝ : SFinite ρ
f : M → ℝ≥0∞
hf : Measurable f
⊢ Measurable f

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α → ℝ≥0
L : ℝ≥0∞
g₀ : α →ₛ ℝ≥0
hg₀ : ∀ (x : α), ↑(g₀ x) ≤ ↑(f x)
g₀L : L < (SimpleFunc.map ofNNReal g₀).lintegral μ
⊢ ∫⁻ (x : α), ↑(g₀ x) ∂μ = (SimpleFunc.map ofNNReal g₀).lintegral μ

Tactic:
rw [← SimpleFunc.lintegral_eq_lintegral, SimpleFunc.coe_map]

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α → ℝ≥0
L : ℝ≥0∞
g₀ : α →ₛ ℝ≥0
hg₀ : ∀ (x : α), ↑(g₀ x) ≤ ↑(f x)
g₀L : L < (SimpleFunc.map ofNNReal g₀).lintegral μ
⊢ ∫⁻ (x : α), ↑(g₀ x) ∂μ = ∫⁻ (a : α), (ofNNReal ∘ ⇑g₀) a ∂μ
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α → ℝ≥0
L : ℝ≥0∞
g₀ : α →ₛ ℝ≥0
hg₀ : ∀ (x : α), ↑(g₀ x) ≤ ↑(f x)
g₀L : L < (SimpleFunc.map ofNNReal g₀).lintegral μ
⊢ L < ∫⁻ (x : α), ↑(g₀ x) ∂μ

Tactic:
by

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

Goal state before:
pp: M : Type u_1
inst✝⁴ : Monoid M
inst✝³ : MeasurableSpace M
inst✝² : MeasurableMul₂ M
μ ν ρ : Measure M
inst✝¹ : SFinite ν
inst✝ : SFinite ρ
f : M → ℝ≥0∞
hf : Measurable f
⊢ Measurable fun x ↦ ∫⁻ (y : M), f (x * y) ∂ρ

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α → ℝ≥0
L : ℝ≥0∞
hL : L < ∫⁻ (x : α), ↑(f x) ∂μ
⊢ ∃ g, (∀ (x : α), g x ≤ f x) ∧ ∫⁻ (x : α), ↑(g x) ∂μ < ∞ ∧ L < ∫⁻ (x : α), ↑(g x) ∂μ

Tactic:
by

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

Goal state before:
pp: M : Type u_1
inst✝⁴ : Monoid M
inst✝³ : MeasurableSpace M
inst✝² : MeasurableMul₂ M
μ ν ρ : Measure M
inst✝¹ : SFinite ν
inst✝ : SFinite ρ
f : M → ℝ≥0∞
hf : Measurable f
x : M
⊢ Measurable fun y ↦ f (x * y)

Tactic:
by

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

Goal state before:
pp: M : Type u_1
inst✝⁴ : Monoid M
inst✝³ : MeasurableSpace M
inst✝² : MeasurableMul₂ M
μ ν ρ : Measure M
inst✝¹ : SFinite ν
inst✝ : SFinite ρ
⊢ (μ ∗ₘ ν) ∗ₘ ρ = μ ∗ₘ ν ∗ₘ ρ

Tactic:
by

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

Goal state before:
pp: M : Type u_1
inst✝⁴ : Monoid M
inst✝³ : MeasurableSpace M
μ ν : Measure M
inst✝² : MeasurableMul₂ M
inst✝¹ : IsProbabilityMeasure μ
inst✝ : IsProbabilityMeasure ν
⊢ AEMeasurable (fun x ↦ x.1 * x.2) (μ.prod ν)

Tactic:
by

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

Goal state before:
pp: M : Type u_1
inst✝⁴ : Monoid M
inst✝³ : MeasurableSpace M
inst✝² : MeasurableMul₂ M
μ ν ρ : Measure M
inst✝¹ : ρ.IsMulLeftInvariant
inst✝ : SFinite ν
hν : ν ≪ ρ
s : Set M
hs : MeasurableSet s
h : ρ s = 0
⊢ Measurable (s.indicator 1)

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 ν
⊢ ∀ {f : α × β → ℝ≥0∞}, Measurable f → Measurable fun x ↦ ∫⁻ (y : β), f (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 β
s : Set (α × β)
hs : MeasurableSet s
⊢ (μ.prod ν) s ≤ ∫⁻ (x : α), ν (Prod.mk x ⁻¹' s) ∂μ

Tactic:
by

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

Goal state before:
pp: M : Type u_1
inst✝⁴ : Monoid M
inst✝³ : MeasurableSpace M
inst✝² : MeasurableMul₂ M
μ ν ρ : Measure M
inst✝¹ : ρ.IsMulLeftInvariant
inst✝ : SFinite ν
hν : ν ≪ ρ
s : Set M
hs : MeasurableSet s
h : ρ s = 0
x : M
⊢ Measurable (HMul.hMul x)

Tactic:
by

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

Goal state before:
pp: M : Type u_1
inst✝⁴ : Monoid M
inst✝³ : MeasurableSpace M
inst✝² : MeasurableMul₂ M
μ ν ρ : Measure M
inst✝¹ : ρ.IsMulLeftInvariant
inst✝ : SFinite ν
hν : ν ≪ ρ
s : Set M
hs : MeasurableSet s
h : ρ s = 0
x : M
⊢ MeasurableSet (HMul.hMul x ⁻¹' 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 β
s : Set α
t : Set β
S : Set α := toMeasurable μ s
T : Set β := toMeasurable ν t
⊢ (μ.prod ν) (s ×ˢ t) ≤ (μ.prod ν) (S ×ˢ T)

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 β
s : Set α
t : Set β
S : Set α := toMeasurable μ s
T : Set β := toMeasurable ν t
⊢ MeasurableSet (S ×ˢ T)

Tactic:
by

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

Goal state before:
pp: M : Type u_1
inst✝⁴ : Monoid M
inst✝³ : MeasurableSpace M
inst✝² : MeasurableMul₂ M
μ ν ρ : Measure M
inst✝¹ : ρ.IsMulLeftInvariant
inst✝ : SFinite ν
hν : ν ≪ ρ
s : Set M
hs : MeasurableSet s
h : ρ s = 0
x : M
⊢ ν (HMul.hMul x ⁻¹' s) = 0

Tactic:
by

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

Goal state before:
pp: M : Type u_1
inst✝⁴ : Monoid M
inst✝³ : MeasurableSpace M
inst✝² : MeasurableMul₂ M
μ ν ρ : Measure M
inst✝¹ : ρ.IsMulLeftInvariant
inst✝ : SFinite ν
hν : ν ≪ ρ
⊢ μ ∗ₘ ν ≪ ρ

Tactic:
by

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

Goal state before:
pp: M : Type u_2
M' : Type u_3
mM : MeasurableSpace M
inst✝⁵ : Monoid M
inst✝⁴ : MeasurableMul₂ M
mM' : MeasurableSpace M'
inst✝³ : Monoid M'
inst✝² : MeasurableMul₂ M'
μ ν : Measure M
inst✝¹ : SFinite μ
inst✝ : SFinite ν
L : M →* M'
hL : Measurable ⇑L
⊢ Measurable ⇑L

Tactic:
by

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

Goal state before:
pp: M : Type u_2
M' : Type u_3
mM : MeasurableSpace M
inst✝⁵ : Monoid M
inst✝⁴ : MeasurableMul₂ M
mM' : MeasurableSpace M'
inst✝³ : Monoid M'
inst✝² : MeasurableMul₂ M'
μ ν : Measure M
inst✝¹ : SFinite μ
inst✝ : SFinite ν
L : M →* M'
hL : Measurable ⇑L
⊢ Measurable fun x ↦ x.1 * x.2

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 β
s : Set α
t : Set β
S : Set α := toMeasurable μ s
T : Set β := toMeasurable ν t
⊢ ∫⁻ (x : α), ν (Prod.mk x ⁻¹' S ×ˢ T) ∂μ = μ S * ν T

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 β
s : Set α
t : Set β
S : Set α := toMeasurable μ s
T : Set β := toMeasurable ν t
⊢ μ S * ν T = μ s * ν t

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 β
s : Set α
t : Set β
⊢ (μ.prod ν) (s ×ˢ t) ≤ μ s * ν 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 γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝ : NullSingletonClass μ
x : α
y : β
⊢ (μ.prod ν) {(x, y)} = (μ.prod ν) ({x} ×ˢ {y})

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 γ
inst✝ : NullSingletonClass μ
x : α
y : β
⊢ μ {x} * ν {y} = 0

Tactic:
by

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

Goal state before:
pp: M : Type u_2
M' : Type u_3
mM : MeasurableSpace M
inst✝⁵ : Monoid M
inst✝⁴ : MeasurableMul₂ M
mM' : MeasurableSpace M'
inst✝³ : Monoid M'
inst✝² : MeasurableMul₂ M'
μ ν : Measure M
inst✝¹ : SFinite μ
inst✝ : SFinite ν
L : M →* M'
hL : Measurable ⇑L
⊢ (⇑L ∘ fun p ↦ p.1 * p.2) = (fun p ↦ p.1 * p.2) ∘ Prod.map ⇑L ⇑L

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 γ
inst✝ : NullSingletonClass ν
x : α
y : β
⊢ (μ.prod ν) {(x, y)} = (μ.prod ν) ({x} ×ˢ {y})

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 γ
inst✝ : NullSingletonClass ν
x : α
y : β
⊢ μ {x} * ν {y} = 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 α
ν : Measure β
inst✝ : SFinite ν
s : Set (α × β)
hs : MeasurableSet s
⊢ (μ.prod ν) s = ∫⁻ (x : α), ν (Prod.mk x ⁻¹' s) ∂μ

Tactic:
by

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

Goal state before:
pp: M : Type u_2
M' : Type u_3
mM : MeasurableSpace M
inst✝⁵ : Monoid M
inst✝⁴ : MeasurableMul₂ M
mM' : MeasurableSpace M'
inst✝³ : Monoid M'
inst✝² : MeasurableMul₂ M'
μ ν : Measure M
inst✝¹ : SFinite μ
inst✝ : SFinite ν
L : M →* M'
hL : Measurable ⇑L
this : (⇑L ∘ fun p ↦ p.1 * p.2) = (fun p ↦ p.1 * p.2) ∘ Prod.map ⇑L ⇑L
⊢ Measurable fun p ↦ p.1 * p.2

Tactic:
by

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

Goal state before:
pp: M : Type u_2
M' : Type u_3
mM : MeasurableSpace M
inst✝⁵ : Monoid M
inst✝⁴ : MeasurableMul₂ M
mM' : MeasurableSpace M'
inst✝³ : Monoid M'
inst✝² : MeasurableMul₂ M'
μ ν : Measure M
inst✝¹ : SFinite μ
inst✝ : SFinite ν
L : M →* M'
hL : Measurable ⇑L
this : (⇑L ∘ fun p ↦ p.1 * p.2) = (fun p ↦ p.1 * p.2) ∘ Prod.map ⇑L ⇑L
⊢ Measurable (Prod.map ⇑L ⇑L)

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 ν
s : Set α
t : Set β
ST : Set (α × β) := toMeasurable (μ.prod ν) (s ×ˢ t)
hSTm : MeasurableSet ST
hST : s ×ˢ t ⊆ ST
f : α → ℝ≥0∞ := fun x ↦ ν (Prod.mk x ⁻¹' ST)
hfm : Measurable f
s' : Set α := {x | ν t ≤ f x}
hss' : s ⊆ s'
⊢ μ s * ν t ≤ μ s' * ν t

Tactic:
by

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

Goal state before:
pp: M : Type u_2
M' : Type u_3
mM : MeasurableSpace M
inst✝⁵ : Monoid M
inst✝⁴ : MeasurableMul₂ M
mM' : MeasurableSpace M'
inst✝³ : Monoid M'
inst✝² : MeasurableMul₂ M'
μ ν : Measure M
inst✝¹ : SFinite μ
inst✝ : SFinite ν
L : M →* M'
hL : Measurable ⇑L
this : (⇑L ∘ fun p ↦ p.1 * p.2) = (fun p ↦ p.1 * p.2) ∘ Prod.map ⇑L ⇑L
⊢ Measurable ⇑L

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 ν
s : Set α
t : Set β
ST : Set (α × β) := toMeasurable (μ.prod ν) (s ×ˢ t)
hSTm : MeasurableSet ST
hST : s ×ˢ t ⊆ ST
f : α → ℝ≥0∞ := fun x ↦ ν (Prod.mk x ⁻¹' ST)
hfm : Measurable f
s' : Set α := {x | ν t ≤ f x}
hss' : s ⊆ s'
⊢ μ s' * ν t = ∫⁻ (x : α) in s', ν t ∂μ

Tactic:
by

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

Goal state before:
pp: M : Type u_2
M' : Type u_3
mM : MeasurableSpace M
inst✝⁵ : Monoid M
inst✝⁴ : MeasurableMul₂ M
mM' : MeasurableSpace M'
inst✝³ : Monoid M'
inst✝² : MeasurableMul₂ M'
μ ν : Measure M
inst✝¹ : SFinite μ
inst✝ : SFinite ν
L : M →* M'
hL : Measurable ⇑L
⊢ map (⇑L) (μ ∗ₘ ν) = map (⇑L) μ ∗ₘ map (⇑L) ν

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 ν
s : Set α
t : Set β
⊢ (μ.prod ν) (s ×ˢ t) = μ s * ν t

Tactic:
by

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

Goal state before:
pp: E : Type u_2
F : Type u_3
inst✝¹¹ : AddCommMonoid E
inst✝¹⁰ : AddCommMonoid F
inst✝⁹ : Module ℝ E
inst✝⁸ : Module ℝ F
inst✝⁷ : TopologicalSpace E
inst✝⁶ : TopologicalSpace F
mE : MeasurableSpace E
inst✝⁵ : MeasurableAdd₂ E
mF : MeasurableSpace F
inst✝⁴ : MeasurableAdd₂ F
inst✝³ : OpensMeasurableSpace E
inst✝² : BorelSpace F
μ ν : Measure E
inst✝¹ : SFinite μ
inst✝ : SFinite ν
L : E →L[ℝ] F
this : map (⇑↑L) (μ ∗ ν) = map (⇑↑L) μ ∗ map (⇑↑L) ν
⊢ map (⇑L) (μ ∗ ν) = map (⇑L) μ ∗ map (⇑L) ν

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 ν
s : Set α
t : Set β
⊢ (μ.prod ν).real (s ×ˢ t) = μ.real s * ν.real t

Tactic:
by

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

Goal state before:
pp: E : Type u_2
F : Type u_3
inst✝¹¹ : AddCommMonoid E
inst✝¹⁰ : AddCommMonoid F
inst✝⁹ : Module ℝ E
inst✝⁸ : Module ℝ F
inst✝⁷ : TopologicalSpace E
inst✝⁶ : TopologicalSpace F
mE : MeasurableSpace E
inst✝⁵ : MeasurableAdd₂ E
mF : MeasurableSpace F
inst✝⁴ : MeasurableAdd₂ F
inst✝³ : OpensMeasurableSpace E
inst✝² : BorelSpace F
μ ν : Measure E
inst✝¹ : SFinite μ
inst✝ : SFinite ν
L : E →L[ℝ] F
⊢ map (⇑L) (μ ∗ ν) = map (⇑L) μ ∗ map (⇑L) ν

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 ν
⊢ map Prod.fst (μ.prod ν) = ν univ • μ

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✝ : IsProbabilityMeasure ν
⊢ map Prod.fst (μ.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 β
inst✝ : SFinite ν
⊢ map Prod.snd (μ.prod ν) = μ univ • ν

Tactic:
by

Goal state after:
Module: Mathlib.Dynamics.Minimal

Goal state before:
pp: case mpr.refine_1
M : Type u_1
α : Type u_3
inst✝³ : Monoid M
inst✝² : TopologicalSpace α
inst✝¹ : MulAction M α
inst✝ : ContinuousConstSMul M α
H : ∀ (s : Set α), IsClosed s → (∀ (c : M), c • s ⊆ s) → s = ∅ ∨ s = univ
x✝ : α
⊢ IsClosed (closure (orbit M x✝))

pp: case mpr.refine_2
M : Type u_1
α : Type u_3
inst✝³ : Monoid M
inst✝² : TopologicalSpace α
inst✝¹ : MulAction M α
inst✝ : ContinuousConstSMul M α
H : ∀ (s : Set α), IsClosed s → (∀ (c : M), c • s ⊆ s) → s = ∅ ∨ s = univ
x✝ : α
⊢ ∀ (c : M), c • closure (orbit M x✝) ⊆ closure (orbit M x✝)

pp: case mpr.refine_3
M : Type u_1
α : Type u_3
inst✝³ : Monoid M
inst✝² : TopologicalSpace α
inst✝¹ : MulAction M α
inst✝ : ContinuousConstSMul M α
H : ∀ (s : Set α), IsClosed s → (∀ (c : M), c • s ⊆ s) → s = ∅ ∨ s = univ
x✝ : α
⊢ ¬closure (orbit M x✝) = ∅

Tactic:
exacts [isClosed_closure, fun _ ↦ smul_closure_orbit_subset _ _,
    (nonempty_orbit _).closure.ne_empty]

Goal state after:
Module: Mathlib.Dynamics.Minimal

Goal state before:
pp: M : Type u_1
α : Type u_3
inst✝³ : Monoid M
inst✝² : TopologicalSpace α
inst✝¹ : MulAction M α
inst✝ : ContinuousConstSMul M α
⊢ IsMinimal M α ↔ ∀ (s : Set α), IsClosed s → (∀ (c : M), c • s ⊆ s) → s = ∅ ∨ s = univ

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✝ : IsProbabilityMeasure μ
⊢ map Prod.snd (μ.prod ν) = ν

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 γ
inst✝⁵ : SFinite ν✝
X : Type u_4
Y : Type u_5
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
m : MeasurableSpace X
μ : Measure X
inst✝² : μ.IsOpenPosMeasure
m' : MeasurableSpace Y
ν : Measure Y
inst✝¹ : ν.IsOpenPosMeasure
inst✝ : SFinite ν
⊢ (μ.prod ν).IsOpenPosMeasure

Tactic:
constructor
  rintro U U_open ⟨⟨x, y⟩, hxy⟩
  rcases isOpen_prod_iff.1 U_open x y hxy with ⟨u, v, u_open, v_open, xu, yv, huv⟩
  refine ne_of_gt (lt_of_lt_of_le ?_ (measure_mono huv))
  simp only [prod_prod, CanonicallyOrderedAdd.mul_pos]
  constructor
  · exact u_open.measure_pos μ ⟨x, xu⟩
  · exact v_open.measure_pos ν ⟨y, yv⟩

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 γ
inst✝⁵ : SFinite ν✝
X : Type u_4
Y : Type u_5
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
m : MeasurableSpace X
μ : Measure X
inst✝² : μ.IsOpenPosMeasure
m' : MeasurableSpace Y
ν : Measure Y
inst✝¹ : ν.IsOpenPosMeasure
inst✝ : SFinite ν
⊢ (μ.prod ν).IsOpenPosMeasure

Tactic:
by

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

Goal state before:
pp: X : Type u_4
Y : Type u_5
m : MeasurableSpace X
μ : Measure X
m' : MeasurableSpace Y
ν : Measure Y
l : Filter X
l' : Filter Y
hμ : μ.FiniteAtFilter l
hν : ν.FiniteAtFilter l'
⊢ (μ.prod ν).FiniteAtFilter (l ×ˢ l')

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 γ
inst✝⁴ : SFinite ν✝
X : Type u_4
Y : Type u_5
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
m : MeasurableSpace X
μ : Measure X
inst✝¹ : IsLocallyFiniteMeasure μ
m' : MeasurableSpace Y
ν : Measure Y
inst✝ : IsLocallyFiniteMeasure ν
x : X × Y
⊢ (μ.prod ν).FiniteAtFilter (𝓝 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 β✝
τ : Measure γ
inst✝² : SFinite ν✝
α : Type u_4
β : Type u_5
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
⊢ IsFiniteMeasure (μ.prod ν)

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 γ
inst✝² : SFinite ν✝
α : Type u_4
β : Type u_5
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝¹ : IsProbabilityMeasure μ
inst✝ : IsProbabilityMeasure ν
⊢ (μ.prod ν) univ = 1

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 γ
inst✝⁷ : SFinite ν✝
X : Type u_4
Y : Type u_5
inst✝⁶ : PseudoMetricSpace X
inst✝⁵ : MeasurableSpace X
inst✝⁴ : PseudoMetricSpace Y
inst✝³ : MeasurableSpace Y
μ : Measure X
ν : Measure Y
inst✝² : SFinite ν
inst✝¹ : IsUnifLocDoublingMeasure μ
inst✝ : IsUnifLocDoublingMeasure ν
⊢ IsUnifLocDoublingMeasure (μ.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 β
inst✝ : SFinite ν
s : Set (α × β)
hs : MeasurableSet s
h2s : (μ.prod ν) s ≠ ∞
⊢ ∀ᵐ (x : α) ∂μ, ν (Prod.mk x ⁻¹' s) < ∞

Tactic:
by

Goal state after: