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 ν
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'
⊢ ν t * μ s' = ν t * μ s'

Tactic:
]

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
⊢ map (fun p ↦ p.1 * p.2) ((map (⇑L) μ).prod (map (⇑L) ν)) = map (fun x ↦ x.1 * x.2) ((map (⇑L) μ).prod (map (⇑L) ν))

Tactic:
]

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) μ ∗ map (⇑↑L) ν

pp: case hL
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
⊢ Measurable ⇑↑L

Tactic:
]

Goal state after:
case hL
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
⊢ Measurable ⇑↑L
Module: Mathlib.MeasureTheory.Group.Convolution

Goal state before:
pp: case hL
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
⊢ Measurable ⇑L

Tactic:
]

Goal state after:
case hL
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
⊢ Measurable ⇑L
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 ν
⊢ μ = μ

Tactic:
]

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:
ext s hs
  simp [Measure.map_apply measurable_snd hs, ← univ_prod]

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 μ
⊢ ν = ν

Tactic:
]

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

Goal state before:
pp: case right
X : Type u_4
Y : Type u_5
m : MeasurableSpace X
μ : Measure X
m' : MeasurableSpace Y
ν : Measure Y
l : Filter X
l' : Filter Y
s : Set X
hs : s ∈ l
hμs : μ s < ∞
t : Set Y
ht : t ∈ l'
hνt : ν t < ∞
⊢ μ s * ν t < ∞

Tactic:
]

Goal state after:
case right
X : Type u_4
Y : Type u_5
m : MeasurableSpace X
μ : Measure X
m' : MeasurableSpace Y
ν : Measure Y
l : Filter X
l' : Filter Y
s : Set X
hs : s ∈ l
hμs : μ s < ∞
t : Set Y
ht : t ∈ l'
hνt : ν t < ∞
⊢ μ s * ν t < ∞
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.1 ×ˢ 𝓝 x.2)

Tactic:
]

Goal state after:
α : 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.1 ×ˢ 𝓝 x.2)
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 ν
⊢ μ univ * ν univ < ∞

Tactic:
]

Goal state after:
α✝ : 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 ν
⊢ μ univ * ν univ < ∞
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 ν
⊢ 1 = 1

Tactic:
]

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 ν
r : ℝ
hμr : ∀ (x : X), μ (Metric.closedBall x (2 * r)) ≤ ↑(doublingConstant μ) * μ (Metric.closedBall x r)
hνr : ∀ (x : Y), ν (Metric.closedBall x (2 * r)) ≤ ↑(doublingConstant ν) * ν (Metric.closedBall x r)
x : X × Y
⊢ μ (Metric.closedBall x.1 (2 * r)) * ν (Metric.closedBall x.2 (2 * r)) ≤
    ↑(doublingConstant μ * doublingConstant ν) * (μ (Metric.closedBall x.1 r) * ν (Metric.closedBall x.2 r))

Tactic:
]

Goal state after:
α : 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 ν
r : ℝ
hμr : ∀ (x : X), μ (Metric.closedBall x (2 * r)) ≤ ↑(doublingConstant μ) * μ (Metric.closedBall x r)
hνr : ∀ (x : Y), ν (Metric.closedBall x (2 * r)) ≤ ↑(doublingConstant ν) * ν (Metric.closedBall x r)
x : X × Y
⊢ μ (Metric.closedBall x.1 (2 * r)) * ν (Metric.closedBall x.2 (2 * r)) ≤
    ↑(doublingConstant μ * doublingConstant ν) * (μ (Metric.closedBall x.1 r) * ν (Metric.closedBall x.2 r))
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 ν
r : ℝ
hμr : ∀ (x : X), μ (Metric.closedBall x (2 * r)) ≤ ↑(doublingConstant μ) * μ (Metric.closedBall x r)
hνr : ∀ (x : Y), ν (Metric.closedBall x (2 * r)) ≤ ↑(doublingConstant ν) * ν (Metric.closedBall x r)
x : X × Y
⊢ ↑(doublingConstant μ) * ↑(doublingConstant ν) * (μ (Metric.closedBall x.1 r) * ν (Metric.closedBall x.2 r)) ≤
    ↑(doublingConstant μ) * ↑(doublingConstant ν) * (μ (Metric.closedBall x.1 r) * ν (Metric.closedBall x.2 r))

Tactic:
]

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 : ∫⁻ (x : α), ν (Prod.mk x ⁻¹' s) ∂μ ≠ ∞
⊢ ∀ᵐ (x : α) ∂μ, ν (Prod.mk x ⁻¹' s) < ∞

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝ : SFinite ν
s : Set (α × β)
hs : MeasurableSet s
h2s : ∫⁻ (x : α), ν (Prod.mk x ⁻¹' s) ∂μ ≠ ∞
⊢ ∀ᵐ (x : α) ∂μ, ν (Prod.mk x ⁻¹' s) < ∞
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
ν : Measure β
s : Set (α × β)
hsm : MeasurableSet s
hs : (fun x ↦ ν (Prod.mk x ⁻¹' s)) =ᵐ[μ] 0
⊢ (μ.prod ν) s ≤ 0

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
ν : Measure β
s : Set (α × β)
hsm : MeasurableSet s
hs : (fun x ↦ ν (Prod.mk x ⁻¹' s)) =ᵐ[μ] 0
⊢ (μ.prod ν) s ≤ 0
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
⊢ (fun x ↦ ν (Prod.mk x ⁻¹' s)) =ᵐ[μ] 0 ↔ (fun x ↦ ν (Prod.mk x ⁻¹' s)) =ᵐ[μ] 0

Tactic:
]

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 (α × β)
h : (μ.prod ν) s = 0
t : Set (α × β)
hst : s ⊆ t
mt : MeasurableSet t
ht : (fun x ↦ ν (Prod.mk x ⁻¹' t)) =ᵐ[μ] 0
⊢ (fun x ↦ ν (Prod.mk x ⁻¹' s)) =ᵐ[μ] 0

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝ : SFinite ν
s : Set (α × β)
h : (μ.prod ν) s = 0
t : Set (α × β)
hst : s ⊆ t
mt : MeasurableSet t
ht : (fun x ↦ ν (Prod.mk x ⁻¹' t)) =ᵐ[μ] 0
⊢ (fun x ↦ ν (Prod.mk x ⁻¹' s)) =ᵐ[μ] 0
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 (α × β)
h : (μ.prod ν) s = 0
t : Set (α × β)
hst : s ⊆ t
mt : MeasurableSet t
ht : (fun x ↦ ν (Prod.mk x ⁻¹' t)) =ᵐ[μ] 0
⊢ (fun x ↦ ν (Prod.mk x ⁻¹' s)) =ᵐ[μ] 0

Tactic:
eventuallyLE_antisymm_iff

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝ : SFinite ν
s : Set (α × β)
h : (μ.prod ν) s = 0
t : Set (α × β)
hst : s ⊆ t
mt : MeasurableSet t
ht : (fun x ↦ ν (Prod.mk x ⁻¹' t)) =ᵐ[μ] 0
⊢ (fun x ↦ ν (Prod.mk x ⁻¹' s)) ≤ᵐ[μ] 0 ∧ 0 ≤ᵐ[μ] fun x ↦ ν (Prod.mk x ⁻¹' s)
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 (α × β)
h : (μ.prod ν) s = 0
t : Set (α × β)
hst : s ⊆ t
mt : MeasurableSet t
ht : (fun x ↦ ν (Prod.mk x ⁻¹' t)) =ᵐ[μ] 0
⊢ (fun x ↦ ν (Prod.mk x ⁻¹' s)) ≤ᵐ[μ] 0 ∧ 0 ≤ᵐ[μ] fun x ↦ ν (Prod.mk x ⁻¹' s)

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝ : SFinite ν
s : Set (α × β)
h : (μ.prod ν) s = 0
t : Set (α × β)
hst : s ⊆ t
mt : MeasurableSet t
ht : (fun x ↦ ν (Prod.mk x ⁻¹' t)) =ᵐ[μ] 0
⊢ (fun x ↦ ν (Prod.mk x ⁻¹' s)) ≤ᵐ[μ] 0 ∧ 0 ≤ᵐ[μ] fun x ↦ ν (Prod.mk x ⁻¹' s)
Module: Mathlib.MeasureTheory.Group.MeasurableEquiv

Goal state before:
pp: G : Type u_1
A : Type u_2
inst✝³ : Group G
inst✝² : MulAction G A
inst✝¹ : MeasurableSpace A
inst✝ : MeasurableConstSMul G A
μ✝ ν : Measure A
g✝ : G
g g' : Gᵈᵐᵃ
μ : Measure A
⊢ map (fun x ↦ DomMulAct.mk.symm (g * g')⁻¹ • x) μ =
    map ((fun x ↦ DomMulAct.mk.symm g⁻¹ • x) ∘ fun x ↦ DomMulAct.mk.symm g'⁻¹ • x) μ

pp: case hg
G : Type u_1
A : Type u_2
inst✝³ : Group G
inst✝² : MulAction G A
inst✝¹ : MeasurableSpace A
inst✝ : MeasurableConstSMul G A
μ✝ ν : Measure A
g✝ : G
g g' : Gᵈᵐᵃ
μ : Measure A
⊢ Measurable fun x ↦ DomMulAct.mk.symm g⁻¹ • x

pp: case hf
G : Type u_1
A : Type u_2
inst✝³ : Group G
inst✝² : MulAction G A
inst✝¹ : MeasurableSpace A
inst✝ : MeasurableConstSMul G A
μ✝ ν : Measure A
g✝ : G
g g' : Gᵈᵐᵃ
μ : Measure A
⊢ Measurable fun x ↦ DomMulAct.mk.symm g'⁻¹ • x

Tactic:
]

Goal state after:
G : Type u_1
A : Type u_2
inst✝³ : Group G
inst✝² : MulAction G A
inst✝¹ : MeasurableSpace A
inst✝ : MeasurableConstSMul G A
μ✝ ν : Measure A
g✝ : G
g g' : Gᵈᵐᵃ
μ : Measure A
⊢ map (fun x ↦ DomMulAct.mk.symm (g * g')⁻¹ • x) μ =
    map ((fun x ↦ DomMulAct.mk.symm g⁻¹ • x) ∘ fun x ↦ DomMulAct.mk.symm g'⁻¹ • x) μ

case hg
G : Type u_1
A : Type u_2
inst✝³ : Group G
inst✝² : MulAction G A
inst✝¹ : MeasurableSpace A
inst✝ : MeasurableConstSMul G A
μ✝ ν : Measure A
g✝ : G
g g' : Gᵈᵐᵃ
μ : Measure A
⊢ Measurable fun x ↦ DomMulAct.mk.symm g⁻¹ • x

case hf
G : Type u_1
A : Type u_2
inst✝³ : Group G
inst✝² : MulAction G A
inst✝¹ : MeasurableSpace A
inst✝ : MeasurableConstSMul G A
μ✝ ν : Measure A
g✝ : G
g g' : Gᵈᵐᵃ
μ : Measure A
⊢ Measurable fun x ↦ DomMulAct.mk.symm g'⁻¹ • x
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ μ' : Measure α
ν ν' : Measure β
inst✝ : SFinite ν'
h1 : μ ≪ μ'
h2 : ν ≪ ν'
s : Set (α × β)
hs : MeasurableSet s
h2s : (fun x ↦ ν' (Prod.mk x ⁻¹' s)) =ᵐ[μ'] 0
⊢ (fun x ↦ ν (Prod.mk x ⁻¹' s)) =ᵐ[μ] 0

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ μ' : Measure α
ν ν' : Measure β
inst✝ : SFinite ν'
h1 : μ ≪ μ'
h2 : ν ≪ ν'
s : Set (α × β)
hs : MeasurableSet s
h2s : (fun x ↦ ν' (Prod.mk x ⁻¹' s)) =ᵐ[μ'] 0
⊢ (fun x ↦ ν (Prod.mk x ⁻¹' s)) =ᵐ[μ] 0
Module: Mathlib.MeasureTheory.Group.MeasurableEquiv

Goal state before:
pp: G : Type u_1
A : Type u_2
inst✝³ : Group G
inst✝² : MulAction G A
inst✝¹ : MeasurableSpace A
inst✝ : MeasurableConstSMul G A
μ✝ ν✝ : Measure A
g✝ : G
g : Gᵈᵐᵃ
μ ν : Measure A
⊢ map (fun x ↦ DomMulAct.mk.symm g⁻¹ • x) μ + map (fun x ↦ DomMulAct.mk.symm g⁻¹ • x) ν =
    map (fun x ↦ DomMulAct.mk.symm g⁻¹ • x) μ + map (fun x ↦ DomMulAct.mk.symm g⁻¹ • x) ν

pp: case hf
G : Type u_1
A : Type u_2
inst✝³ : Group G
inst✝² : MulAction G A
inst✝¹ : MeasurableSpace A
inst✝ : MeasurableConstSMul G A
μ✝ ν✝ : Measure A
g✝ : G
g : Gᵈᵐᵃ
μ ν : Measure A
⊢ Measurable fun x ↦ DomMulAct.mk.symm g⁻¹ • x

Tactic:
]

Goal state after:
case hf
G : Type u_1
A : Type u_2
inst✝³ : Group G
inst✝² : MulAction G A
inst✝¹ : MeasurableSpace A
inst✝ : MeasurableConstSMul G A
μ✝ ν✝ : Measure A
g✝ : G
g : Gᵈᵐᵃ
μ ν : Measure A
⊢ Measurable fun x ↦ DomMulAct.mk.symm g⁻¹ • x
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
h2s : μ s = 0
⊢ (μ.prod ν) (s ×ˢ univ) ≤ 0

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
ν : Measure β
s : Set α
hs : MeasurableSet s
h2s : μ s = 0
⊢ (μ.prod ν) (s ×ˢ univ) ≤ 0
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
h2s : μ s = 0
⊢ 0 = 0

Tactic:
]

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
h2s : ν s = 0
⊢ (μ.prod ν) (univ ×ˢ s) ≤ 0

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
ν : Measure β
s : Set β
hs : MeasurableSet s
h2s : ν s = 0
⊢ (μ.prod ν) (univ ×ˢ s) ≤ 0
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
inst✝¹ : MeasurableSpace α
inst✝ : OpensMeasurableSpace α
s t : Set α
hs : s = ∅ ∨ ∃ f, Continuous[_, inst✝³] f ∧ range f = s
ht : t = ∅ ∨ ∃ f, Continuous[_, inst✝³] f ∧ range f = t
h : Disjoint s t
⊢ MeasurablySeparable s t

Tactic:
]

Goal state after:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
inst✝¹ : MeasurableSpace α
inst✝ : OpensMeasurableSpace α
s t : Set α
hs : s = ∅ ∨ ∃ f, Continuous[_, inst✝³] f ∧ range f = s
ht : t = ∅ ∨ ∃ f, Continuous[_, inst✝³] f ∧ range f = t
h : Disjoint s t
⊢ MeasurablySeparable s t
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
h2s : ν s = 0
⊢ 0 = 0

Tactic:
]

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 β
s_ae_univ : μ sᶜ = 0
t_ae_univ : ν tᶜ = 0
⊢ (μ.prod ν) (sᶜ ×ˢ univ) = 0 ∧ (μ.prod ν) (univ ×ˢ tᶜ) = 0

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝ : SFinite ν
s : Set α
t : Set β
s_ae_univ : μ sᶜ = 0
t_ae_univ : ν tᶜ = 0
⊢ (μ.prod ν) (sᶜ ×ˢ univ) = 0 ∧ (μ.prod ν) (univ ×ˢ tᶜ) = 0
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 β
hs : μ s ≠ 0
u : Set (α × β)
hum : MeasurableSet u
hu : s ×ˢ t =ᵐ[μ.prod ν] u
x : α
hxs : x ∈ s
hx : t =ᵐ[ν] Prod.mk x ⁻¹' u
⊢ t =ᵐ[ν] Prod.mk x ⁻¹' u

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝ : SFinite ν
s : Set α
t : Set β
hs : μ s ≠ 0
u : Set (α × β)
hum : MeasurableSet u
hu : s ×ˢ t =ᵐ[μ.prod ν] u
x : α
hxs : x ∈ s
hx : t =ᵐ[ν] Prod.mk x ⁻¹' u
⊢ t =ᵐ[ν] Prod.mk x ⁻¹' u
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝¹ : SFinite ν
inst✝ : NeZero μ
t : Set β
h : NullMeasurableSet (Prod.snd ⁻¹' t) (μ.prod ν)
⊢ NullMeasurableSet (Prod.snd ⁻¹' t) (μ.prod ν)

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝¹ : SFinite ν
inst✝ : NeZero μ
t : Set β
h : NullMeasurableSet (Prod.snd ⁻¹' t) (μ.prod ν)
⊢ NullMeasurableSet (Prod.snd ⁻¹' t) (μ.prod ν)
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ μ' : Measure α
ν✝ ν' : Measure β
τ : Measure γ
inst✝ : SFinite ν✝
ν : Measure β
C : Set (Set α)
D : Set (Set β)
hμ : μ.FiniteSpanningSetsIn C
hν : ν.FiniteSpanningSetsIn D
this : SigmaFinite ν
n : ℕ
⊢ μ (hμ.set (Nat.unpair n).1) * ν (hν.set (Nat.unpair n).2) < ∞

Tactic:
]

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ μ' : Measure α
ν✝ ν' : Measure β
τ : Measure γ
inst✝ : SFinite ν✝
ν : Measure β
C : Set (Set α)
D : Set (Set β)
hμ : μ.FiniteSpanningSetsIn C
hν : ν.FiniteSpanningSetsIn D
this : SigmaFinite ν
n : ℕ
⊢ μ (hμ.set (Nat.unpair n).1) * ν (hν.set (Nat.unpair n).2) < ∞
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: case hs
X : Type u_3
Z : Type u_5
inst✝³ : MeasurableSpace X
inst✝² : StandardBorelSpace X
inst✝¹ : MeasurableSpace Z
inst✝ : CountablySeparated Z
f : X → Z
hf : Measurable f
hsurj : Surjective f
s : Set Z
h : MeasurableSet (f ⁻¹' s)
τ : TopologicalSpace Z
left✝¹ : SecondCountableTopology Z
left✝ : T4Space Z
right✝ : OpensMeasurableSpace Z
⊢ AnalyticSet (f '' f ⁻¹' s)

Tactic:
]

Goal state after:
case hs
X : Type u_3
Z : Type u_5
inst✝³ : MeasurableSpace X
inst✝² : StandardBorelSpace X
inst✝¹ : MeasurableSpace Z
inst✝ : CountablySeparated Z
f : X → Z
hf : Measurable f
hsurj : Surjective f
s : Set Z
h : MeasurableSet (f ⁻¹' s)
τ : TopologicalSpace Z
left✝¹ : SecondCountableTopology Z
left✝ : T4Space Z
right✝ : OpensMeasurableSpace Z
⊢ AnalyticSet (f '' f ⁻¹' s)
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: case hsc
X : Type u_3
Z : Type u_5
inst✝³ : MeasurableSpace X
inst✝² : StandardBorelSpace X
inst✝¹ : MeasurableSpace Z
inst✝ : CountablySeparated Z
f : X → Z
hf : Measurable f
hsurj : Surjective f
s : Set Z
h : MeasurableSet (f ⁻¹' s)
τ : TopologicalSpace Z
left✝¹ : SecondCountableTopology Z
left✝ : T4Space Z
right✝ : OpensMeasurableSpace Z
⊢ AnalyticSet (f '' f ⁻¹' sᶜ)

Tactic:
]

Goal state after:
case hsc
X : Type u_3
Z : Type u_5
inst✝³ : MeasurableSpace X
inst✝² : StandardBorelSpace X
inst✝¹ : MeasurableSpace Z
inst✝ : CountablySeparated Z
f : X → Z
hf : Measurable f
hsurj : Surjective f
s : Set Z
h : MeasurableSet (f ⁻¹' s)
τ : TopologicalSpace Z
left✝¹ : SecondCountableTopology Z
left✝ : T4Space Z
right✝ : OpensMeasurableSpace Z
⊢ AnalyticSet (f '' f ⁻¹' sᶜ)
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: X : Type u_3
Z : Type u_5
inst✝³ : MeasurableSpace X
inst✝² : StandardBorelSpace X
inst✝¹ : MeasurableSpace Z
f : X → Z
inst✝ : CountablySeparated ↑(range f)
hf : Measurable f
hr : MeasurableSet (range f)
s : Set Z
⊢ MeasurableSet (range f ∩ s) ↔ MeasurableSet (range f ∩ s)

Tactic:
]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
ι' : Type u_4
inst✝¹ : Countable ι'
m : Measure α
m' : ι' → Measure β
inst✝ : ∀ (n : ι'), SFinite (m' n)
s : Set (α × β)
hs : MeasurableSet s
M : ∀ (x : α), MeasurableSet (Prod.mk x ⁻¹' s)
⊢ ∑' (i : ι'), ∫⁻ (a : α), (m' i) (Prod.mk a ⁻¹' s) ∂m = ∑' (i : ι'), ∫⁻ (x : α), (m' i) (Prod.mk x ⁻¹' s) ∂m

Tactic:
]

Goal state after: