mathlib-initiative/mathlib-tactics huggingface dataset:
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 ν
ρ : Measure (α × β)
inst✝ : IsZeroOrProbabilityMeasure ρ
⊢ IsZeroOrProbabilityMeasure ρ.snd

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : TopologicalSpace G
inst✝⁵ : BorelSpace G
μ : Measure G
inst✝⁴ : Group G
inst✝³ : IsTopologicalGroup G
inst✝² : LocallyCompactSpace G
inst✝¹ : IsFiniteMeasureOnCompacts μ
inst✝ : μ.InnerRegularCompactLTTop
k : Set G
hk : IsCompact k
h'k : IsClosed[inst✝⁶] k
ε : ℝ≥0∞
hε : ε ≠ 0
U : Set G
hUk : k ⊆ U
hU : IsOpen[inst✝⁶] U
hμUk : μ U < μ k + ε
V : Set G
hV1 : V ∈ 𝓝 1
hVkU : V * k ⊆ U
g : G
hg : g ∈ V
⊢ μ (g • k \ k) ≤ μ (U \ k)

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : TopologicalSpace G
inst✝⁵ : BorelSpace G
μ : Measure G
inst✝⁴ : Group G
inst✝³ : IsTopologicalGroup G
inst✝² : LocallyCompactSpace G
inst✝¹ : IsFiniteMeasureOnCompacts μ
inst✝ : μ.InnerRegularCompactLTTop
k : Set G
hk : IsCompact k
h'k : IsClosed[inst✝⁶] k
ε : ℝ≥0∞
hε : ε ≠ 0
⊢ ∀ᶠ (g : G) in 𝓝 1, μ (g • k \ k) < ε

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 μ
⊢ (μ.prod ν).snd = ν

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✝²]
⊢ μ.WeaklyRegular

Tactic:
by

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

Goal state before:
pp: X : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : PseudoMetrizableSpace X
inst✝ : MeasurableSpace X
μ : Measure X
⊢ μ.InnerRegularWRT IsClosed[inst✝²] IsOpen[inst✝²]

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : TopologicalSpace G
inst✝³ : BorelSpace G
μ : Measure G
inst✝² : Group G
inst✝¹ : IsTopologicalGroup G
inst✝ : μ.IsMulLeftInvariant
K : Set G
hK : IsCompact K
U : Set G
hU : IsOpen[inst✝⁴] U
hne : (interior U).Nonempty
h : μ U = 0
t : Finset G
hKt : K ⊆ ⋃ g ∈ t, (fun h ↦ g * h) ⁻¹' U
⊢ ∑ g ∈ t, μ ((fun h ↦ g * h) ⁻¹' U) = 0

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 γ
X : α → β
Y : α → γ
μ : Measure α
hX : AEMeasurable X μ
hY : ¬AEMeasurable Y μ
⊢ ¬AEMeasurable (fun x ↦ (X x, Y x)) μ

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : TopologicalSpace G
inst✝³ : BorelSpace G
μ : Measure G
inst✝² : Group G
inst✝¹ : IsTopologicalGroup G
inst✝ : μ.IsMulLeftInvariant
K : Set G
hK : IsCompact K
h : μ K ≠ 0
⊢ μ.IsOpenPosMeasure

Tactic:
by

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

Goal state before:
pp: X : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : SigmaCompactSpace X
inst✝ : MeasurableSpace X
μ : Measure X
F : Set X
hF : IsClosed[inst✝²] F
r : ℝ≥0∞
hr : r < μ F
B : ℕ → Set X := compactCovering X
hBc : ∀ (n : ℕ), IsCompact (F ∩ B n)
⊢ ⋃ n, F ∩ B n = F

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 γ
X : α → β
Y : α → γ
μ : Measure α
hX : AEMeasurable X μ
⊢ (map (fun a ↦ (X a, Y a)) μ).snd = map Y μ

Tactic:
by

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

Goal state before:
pp: X : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : SigmaCompactSpace X
inst✝ : MeasurableSpace X
μ : Measure X
F : Set X
hF : IsClosed[inst✝²] F
r : ℝ≥0∞
hr : r < μ F
B : ℕ → Set X := compactCovering X
hBc : ∀ (n : ℕ), IsCompact (F ∩ B n)
hBU : ⋃ n, F ∩ B n = F
⊢ μ F = ⨆ n, μ (F ∩ B n)

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 (α × β)
⊢ (map Prod.swap ρ).fst = ρ.snd

Tactic:
by

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

Goal state before:
pp: X : Type u_6
E : Type u_7
ι : Type u_8
inst✝⁸ : MeasurableSpace X
inst✝⁷ : CommMonoid E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : PseudoMetrizableSpace E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
inst✝² : MeasurableMul₂ E
L : SummationFilter ι
inst✝¹ : L.NeBot
inst✝ : L.filter.IsCountablyGenerated
μ : Measure X
f : ι → X → E
h : ∀ (i : ι), AEMeasurable (f i) μ
⊢ AEMeasurable (∏'[L] (i : ι), f i) μ

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝⁶ : MeasurableSpace G
inst✝⁵ : TopologicalSpace G
inst✝⁴ : BorelSpace G
μ : Measure G
inst✝³ : Group G
inst✝² : IsTopologicalGroup G
inst✝¹ : μ.IsMulLeftInvariant
inst✝ : μ.Regular
s : Set G
hs : IsOpen[inst✝⁵] s
⊢ μ s = 0 ↔ s = ∅ ∨ μ = 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 (α × β)
⊢ (map Prod.swap ρ).snd = ρ.fst

Tactic:
by

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

Goal state before:
pp: X : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : SigmaCompactSpace X
inst✝ : MeasurableSpace X
μ : Measure X
⊢ μ.InnerRegularWRT IsCompact IsClosed[inst✝²]

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝⁶ : MeasurableSpace G
inst✝⁵ : TopologicalSpace G
inst✝⁴ : BorelSpace G
μ : Measure G
inst✝³ : Group G
inst✝² : IsTopologicalGroup G
inst✝¹ : μ.IsMulLeftInvariant
inst✝ : μ.Regular
hμ : μ ≠ 0
s : Set G
hs : IsOpen[inst✝⁵] s
⊢ μ s ≠ 0 ↔ s.Nonempty

Tactic:
by

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

Goal state before:
pp: α : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : StandardBorelSpace α
s : Set α
hs : MeasurableSet s
⊢ ∃ x, BorelSpace α ∧ PolishSpace α ∧ IsClosed s ∧ IsOpen s

Tactic:
by

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

Goal state before:
pp: α : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : StandardBorelSpace α
s : Set α
hs : MeasurableSet s
⊢ StandardBorelSpace ↑s

Tactic:
by

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

Goal state before:
pp: α✝ : Type u_1
ι : Type u_2
γ : Type u_3
α : Type u_4
β✝ : Type u_5
inst✝⁴ : MeasurableSpace β✝
β : Type u_6
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : StandardBorelSpace α
inst✝ : StandardBorelSpace β
h : ¬Countable α
this : UpgradedStandardBorel α := upgradeStandardBorel α
⊢ ¬univ.Countable

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace α
inst✝¹ : R1Space α
inst✝ : OpensMeasurableSpace α
h : μ.InnerRegular
⊢ μ.InnerRegularWRT IsClosed[inst✝²] IsOpen[inst✝²]

Tactic:
by

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

Goal state before:
pp: α✝ : Type u_1
ι : Type u_2
γ : Type u_3
α : Type u_4
β✝ : Type u_5
inst✝⁴ : MeasurableSpace β✝
β : Type u_6
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : StandardBorelSpace α
inst✝ : StandardBorelSpace β
h : ¬Countable α
⊢ α ≃ᵐ (ℕ → Bool)

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : TopologicalSpace G
inst✝³ : BorelSpace G
μ : Measure G
inst✝² : Group G
inst✝¹ : IsTopologicalGroup G
inst✝ : μ.IsMulLeftInvariant
U : Set G
hU : IsOpen[inst✝⁴] U
h'U : (interior U).Nonempty
h : μ U ≠ ∞
K : Set G
hK : IsCompact K
t : Finset G
hKt : K ⊆ ⋃ g ∈ t, (fun h ↦ g * h) ⁻¹' U
⊢ ∀ i ∈ ↑t, μ ((fun h ↦ i * h) ⁻¹' U) < ∞

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace α
inst✝ : μ.InnerRegular
⊢ (∃ K, IsCompact K ∧ μ K ≠ 0) ↔ μ ≠ 0

Tactic:
by

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

Goal state before:
pp: α✝ : Type u_1
ι : Type u_2
γ : Type u_3
α : Type u_4
β✝ : Type u_5
inst✝⁴ : MeasurableSpace β✝
β : Type u_6
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : StandardBorelSpace α
inst✝ : StandardBorelSpace β
e : α ≃ β
⊢ α ≃ᵐ β

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : TopologicalSpace G
inst✝³ : BorelSpace G
μ : Measure G
inst✝² : Group G
inst✝¹ : IsTopologicalGroup G
inst✝ : μ.IsMulLeftInvariant
U : Set G
hU : IsOpen[inst✝⁴] U
h'U : U.Nonempty
h : μ U ≠ ∞
K : Set G
hK : IsCompact K
⊢ μ K < ∞

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : MeasurableSpace β
inst✝¹ : TopologicalSpace β
inst✝ : BorelSpace β
f : α ≃ₜ β
⊢ (map (⇑f) μ).InnerRegular ↔ μ.InnerRegular

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 γ
μa : Measure α
μb : Measure β
μc : Measure γ
inst✝¹ : SFinite μb
inst✝ : SFinite μc
⊢ map (⇑MeasurableEquiv.prodAssoc) ((μa.prod μb).prod μc) = μa.prod (μb.prod μc)

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝³ : MeasurableSpace G
inst✝² : Group G
inst✝¹ : MeasurableMul₂ G
μ : Measure G
inst✝ : SFinite μ
s : Set G
hs : MeasurableSet s
this : Measurable fun y ↦ μ ((fun x ↦ (x, y)) ⁻¹' (fun z ↦ (1, z.1 * z.2)) ⁻¹' univ ×ˢ s)
⊢ Measurable fun x ↦ μ ((fun y ↦ y * x) ⁻¹' s)

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝³ : MeasurableSpace G
inst✝² : Group G
inst✝¹ : MeasurableMul₂ G
μ : Measure G
inst✝ : SFinite μ
s : Set G
hs : MeasurableSet s
⊢ Measurable fun x ↦ μ ((fun y ↦ y * x) ⁻¹' s)

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
μ ν : Measure G
inst✝⁴ : SFinite ν
inst✝³ : SFinite μ
inst✝² : MeasurableInv G
inst✝¹ : μ.IsMulLeftInvariant
inst✝ : ν.IsMulLeftInvariant
⊢ MeasurePreserving (fun z ↦ (z.2 * z.1, z.1⁻¹)) (μ.prod ν) (μ.prod ν)

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul₂ G
μ : Measure G
inst✝² : SFinite μ
inst✝¹ : MeasurableInv G
inst✝ : μ.IsMulLeftInvariant
s : Set G
hsm : MeasurableSet s
hμs : μ s = 0
hf : Measurable fun z ↦ (z.2 * z.1, z.1⁻¹)
this : (map (fun z ↦ (z.2 * z.1, z.1⁻¹)) (μ.prod μ)) (s⁻¹ ×ˢ s⁻¹) = 0
⊢ μ s⁻¹ = 0

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝³ : MeasurableSpace G
μ : Measure G
inst✝² : InvolutiveInv G
inst✝¹ : MeasurableInv G
inst✝ : μ.IsInvInvariant
f : G → ℝ≥0∞
⊢ ∫⁻ (x : G), f x⁻¹ ∂μ = ∫⁻ (x : G), f x ∂μ

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝³ : MeasurableSpace G
μ : Measure G
inst✝² : Group G
inst✝¹ : MeasurableMul G
inst✝ : μ.IsMulLeftInvariant
f : G → ℝ≥0∞
g : G
⊢ ∫⁻ (x : G), f (g * x) ∂μ = ∫⁻ (x : G), f x ∂μ

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝³ : MeasurableSpace G
μ : Measure G
inst✝² : Group G
inst✝¹ : MeasurableMul G
inst✝ : μ.IsMulRightInvariant
f : G → ℝ≥0∞
g : G
⊢ ∫⁻ (x : G), f (x * g) ∂μ = ∫⁻ (x : G), f x ∂μ

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝³ : MeasurableSpace G
μ : Measure G
inst✝² : Group G
inst✝¹ : MeasurableMul G
inst✝ : μ.IsMulRightInvariant
f : G → ℝ≥0∞
g : G
⊢ ∫⁻ (x : G), f (x / g) ∂μ = ∫⁻ (x : G), f x ∂μ

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝⁵ : MeasurableSpace G
μ : Measure G
inst✝⁴ : Group G
inst✝³ : MeasurableMul G
inst✝² : μ.IsMulLeftInvariant
inst✝¹ : MeasurableInv G
inst✝ : μ.IsInvInvariant
f : G → ℝ≥0∞
g : G
⊢ ∫⁻ (x : G), f (g / x) ∂μ = ∫⁻ (x : G), f x ∂μ

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝⁷ : MeasurableSpace G
μ : Measure G
inst✝⁶ : TopologicalSpace G
inst✝⁵ : Group G
inst✝⁴ : IsTopologicalGroup G
inst✝³ : BorelSpace G
inst✝² : μ.IsMulLeftInvariant
inst✝¹ : μ.Regular
inst✝ : NeZero μ
f : G → ℝ≥0∞
hf : Continuous f
⊢ ∫⁻ (x : G), f x ∂μ = 0 ↔ f = 0

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
μ✝ : Measure α
inst✝² : TopologicalSpace α
μ ν : Measure α
inst✝¹ : μ.InnerRegular
inst✝ : ν.InnerRegular
s : Set α
hs : MeasurableSet s
r : ℝ≥0∞
h : μ s = 0
hr : r < ν s
K : Set α
Ks : K ⊆ s
hK : IsCompact K
h'K : r < ν K
⊢ ν K ≤ (μ + ν) K

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝⁸ : MeasurableSpace G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : BorelSpace G
inst✝⁵ : Group G
inst✝⁴ : IsTopologicalGroup G
inst✝³ : WeaklyLocallyCompactSpace G
inst✝² : NoncompactSpace G
μ : Measure G
inst✝¹ : μ.IsOpenPosMeasure
inst✝ : μ.IsMulLeftInvariant
K : Set G
K1 : K ∈ 𝓝 1
hK : IsCompact K
Kclosed : IsClosed[inst✝⁷] K
K_pos : 0 < μ K
g : Set G → G
hg : ∀ (L : Set G), IsCompact L → Disjoint L (g L • K)
L : ℕ → Set G := fun n ↦ (fun T ↦ T ∪ g T • K)^[n] K
n : ℕ
⊢ IsCompact (L n)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.LConvolution

Goal state before:
pp: G : Type u_1
mG : MeasurableSpace G
inst✝¹ : Mul G
inst✝ : Inv G
f : G → ℝ≥0∞
μ : Measure G
⊢ 0 ⋆ₘₗ[μ] f = 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.LConvolution

Goal state before:
pp: G : Type u_1
mG : MeasurableSpace G
inst✝¹ : Mul G
inst✝ : Inv G
f : G → ℝ≥0∞
μ : Measure G
⊢ f ⋆ₘₗ[μ] 0 = 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.LConvolution

Goal state before:
pp: G : Type u_1
mG : MeasurableSpace G
inst✝⁴ : Mul G
inst✝³ : Inv G
inst✝² : MeasurableMul₂ G
inst✝¹ : MeasurableInv G
f g : G → ℝ≥0∞
μ : Measure G
inst✝ : SFinite μ
hf : Measurable f
hg : Measurable g
⊢ Measurable (f ⋆ₘₗ[μ] g)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.LConvolution

Goal state before:
pp: G : Type u_1
mG : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul₂ G
inst✝² : MeasurableInv G
μ : Measure G
inst✝¹ : μ.IsMulLeftInvariant
inst✝ : SFinite μ
f g : G → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
⊢ AEMeasurable (f ⋆ₘₗ[μ] g) μ

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.LConvolution

Goal state before:
pp: G : Type u_1
mG : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul₂ G
inst✝² : MeasurableInv G
μ : Measure G
inst✝¹ : μ.IsMulLeftInvariant
inst✝ : SFinite μ
f g k : G → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hk : AEMeasurable k μ
x y : G
⊢ AEMeasurable (fun y_1 ↦ g y_1 * k (y_1⁻¹ * (y⁻¹ * x))) μ

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.LConvolution

Goal state before:
pp: G : Type u_1
mG : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul₂ G
inst✝² : MeasurableInv G
μ : Measure G
inst✝¹ : μ.IsMulLeftInvariant
inst✝ : SFinite μ
f g k : G → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hk : AEMeasurable k μ
x y : G
⊢ AEMeasurable (fun y_1 ↦ f y_1 * g (y_1⁻¹ * y)) μ

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul₂ G
μ : Measure G
inst✝² : SFinite μ
inst✝¹ : MeasurableInv G
inst✝ : μ.IsMulLeftInvariant
⊢ QuasiMeasurePreserving Inv.inv μ μ

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul₂ G
μ : Measure G
inst✝² : SFinite μ
s : Set G
inst✝¹ : MeasurableInv G
inst✝ : μ.IsMulLeftInvariant
⊢ μ s⁻¹ = 0 ↔ μ s = 0

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul₂ G
μ : Measure G
inst✝² : SFinite μ
inst✝¹ : MeasurableInv G
inst✝ : μ.IsMulLeftInvariant
⊢ (ae μ)⁻¹ = ae μ

Tactic:
refine le_antisymm (quasiMeasurePreserving_inv μ).tendsto_ae ?_

Goal state after:
G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul₂ G
μ : Measure G
inst✝² : SFinite μ
inst✝¹ : MeasurableInv G
inst✝ : μ.IsMulLeftInvariant
⊢ ae μ ≤ (ae μ)⁻¹
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
μ✝ : Measure α
inst✝² : TopologicalSpace α
μ ν : Measure α
inst✝¹ : μ.InnerRegular
inst✝ : ν.InnerRegular
s : Set α
hs : MeasurableSet s
r : ℝ≥0∞
h : μ s ≠ 0
h' : ν s = 0
hr : r < μ s
K : Set α
Ks : K ⊆ s
hK : IsCompact K
h'K : r < μ K
⊢ μ K ≤ (μ + ν) K

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul₂ G
μ : Measure G
inst✝² : SFinite μ
inst✝¹ : MeasurableInv G
inst✝ : μ.IsMulLeftInvariant
⊢ (ae μ)⁻¹ = ae μ

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul₂ G
μ : Measure G
inst✝² : SFinite μ
s : Set G
inst✝¹ : MeasurableInv G
inst✝ : μ.IsMulLeftInvariant
⊢ EventuallyConst s⁻¹ (ae μ) ↔ EventuallyConst s (ae μ)

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul₂ G
μ : Measure G
inst✝² : SFinite μ
inst✝¹ : MeasurableInv G
inst✝ : μ.IsMulLeftInvariant
⊢ μ ≪ μ.inv

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝⁸ : MeasurableSpace G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : BorelSpace G
inst✝⁵ : Group G
inst✝⁴ : IsTopologicalGroup G
inst✝³ : WeaklyLocallyCompactSpace G
inst✝² : NoncompactSpace G
μ : Measure G
inst✝¹ : μ.IsOpenPosMeasure
inst✝ : μ.IsMulLeftInvariant
K : Set G
K1 : K ∈ 𝓝 1
hK : IsCompact K
Kclosed : IsClosed[inst✝⁷] K
K_pos : 0 < μ K
g : Set G → G
hg : ∀ (L : Set G), IsCompact L → Disjoint L (g L • K)
L : ℕ → Set G := fun n ↦ (fun T ↦ T ∪ g T • K)^[n] K
Lcompact : ∀ (n : ℕ), IsCompact (L n)
n : ℕ
⊢ IsClosed[inst✝⁷] (L n)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.LConvolution

Goal state before:
pp: G : Type u_1
mG : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul₂ G
inst✝² : MeasurableInv G
μ : Measure G
inst✝¹ : μ.IsMulLeftInvariant
inst✝ : SFinite μ
f g k : G → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hk : AEMeasurable k μ
x : G
⊢ AEMeasurable (Function.uncurry fun y x_1 ↦ f y * (g (y⁻¹ * x_1) * k (x_1⁻¹ * x))) (μ.prod μ)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.LConvolution

Goal state before:
pp: G : Type u_1
mG : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul₂ G
inst✝² : MeasurableInv G
μ : Measure G
inst✝¹ : μ.IsMulLeftInvariant
inst✝ : SFinite μ
f g k : G → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hk : AEMeasurable k μ
⊢ f ⋆ₘₗ[μ] g ⋆ₘₗ[μ] k = (f ⋆ₘₗ[μ] g) ⋆ₘₗ[μ] k

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.LConvolution

Goal state before:
pp: G : Type u_1
mG : MeasurableSpace G
inst✝⁴ : CommGroup G
inst✝³ : MeasurableMul₂ G
inst✝² : MeasurableInv G
μ : Measure G
inst✝¹ : μ.IsMulLeftInvariant
inst✝ : μ.IsInvInvariant
f g : G → ℝ≥0∞
⊢ f ⋆ₘₗ[μ] g = g ⋆ₘₗ[μ] f

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
μ ν : Measure G
inst✝⁴ : SFinite ν
inst✝³ : SFinite μ
inst✝² : MeasurableInv G
inst✝¹ : μ.IsMulLeftInvariant
inst✝ : ν.IsMulLeftInvariant
f : G → G → ℝ≥0∞
hf : AEMeasurable (uncurry f) (μ.prod ν)
⊢ ∫⁻ (x : G), ∫⁻ (y : G), f (y * x) x⁻¹ ∂ν ∂μ = ∫⁻ (x : G), ∫⁻ (y : G), f x y ∂ν ∂μ

Tactic:
by

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ✝ : Measure α
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
⊢ ∫⁻ (a : α) in ∅, f a ∂μ = 0

Tactic:
by

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
⊢ ∫⁻ (a : α) in s, f a ∂μ ≤ (μ.withDensity f) s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
f : α → ℝ≥0∞
s : Set α
t : Set α := toMeasurable μ s
⊢ ∫⁻ (a : α) in t, f a ∂μ = ∫⁻ (a : α) in s, f a ∂μ

Tactic:
by

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
f : α → ℝ≥0∞
s : Set α
⊢ (μ.withDensity f) s = ∫⁻ (a : α) in s, f a ∂μ

Tactic:
by

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
f : α → ℝ≥0∞
⊢ withDensity 0 f = 0

Tactic:
by

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
h : f =ᵐ[μ] g
⊢ μ.withDensity f = μ.withDensity g

Tactic:
by

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hfg : f ≤ᵐ[μ] g
⊢ μ.withDensity f ≤ μ.withDensity g

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul₂ G
μ : Measure G
inst✝² : SFinite μ
s : Set G
inst✝¹ : MeasurableInv G
inst✝ : μ.IsMulLeftInvariant
y : G
⊢ μ ((fun x ↦ x * y) ⁻¹' s) = 0 ↔ μ ((fun x ↦ y⁻¹ * x) ⁻¹' s⁻¹)⁻¹ = 0

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝⁸ : MeasurableSpace G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : BorelSpace G
inst✝⁵ : Group G
inst✝⁴ : IsTopologicalGroup G
inst✝³ : WeaklyLocallyCompactSpace G
inst✝² : NoncompactSpace G
μ : Measure G
inst✝¹ : μ.IsOpenPosMeasure
inst✝ : μ.IsMulLeftInvariant
K : Set G
K1 : K ∈ 𝓝 1
hK : IsCompact K
Kclosed : IsClosed[inst✝⁷] K
K_pos : 0 < μ K
g : Set G → G
hg : ∀ (L : Set G), IsCompact L → Disjoint L (g L • K)
L : ℕ → Set G := fun n ↦ (fun T ↦ T ∪ g T • K)^[n] K
Lcompact : ∀ (n : ℕ), IsCompact (L n)
Lclosed : ∀ (n : ℕ), IsClosed[inst✝⁷] (L n)
n : ℕ
IH : μ (L n) = ↑(n + 1) * μ K
⊢ μ (L (n + 1)) = μ (L n) + μ (g (L n) • K)

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul₂ G
μ : Measure G
inst✝² : SFinite μ
s : Set G
inst✝¹ : MeasurableInv G
inst✝ : μ.IsMulLeftInvariant
y : G
⊢ μ ((fun x ↦ y⁻¹ * x) ⁻¹' s⁻¹)⁻¹ = 0 ↔ μ s = 0

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
μ✝ : Measure α
inst✝² : TopologicalSpace α
μ ν : Measure α
inst✝¹ : μ.InnerRegular
inst✝ : ν.InnerRegular
⊢ (μ + ν).InnerRegular

Tactic:
by

Goal state after: