-- Mathlib/MeasureTheory/Measure/Prod.lean
theorem prod_prod (s : Set α) (t : Set β) : μ.prod ν (s ×ˢ t) = μ s * ν t

Proof state:
case a
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝ : SFinite ν
s : Set α
t : Set β
ST : Set (α × β) := toMeasurable (μ.prod ν) (s ×ˢ t)
⊢ μ s * ν t ≤ (μ.prod ν) (s ×ˢ t)

Tactic:
have hSTm : MeasurableSet ST := measurableSet_toMeasurable _ _

Result:
case a
α : 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
⊢ μ s * ν t ≤ (μ.prod ν) (s ×ˢ t)

Proof state:
case a
α : 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 * ν t ≤ (μ.prod ν) (s ×ˢ t)

Tactic:
set s' : Set α := { x | ν t ≤ f x }

Result:
case a
α : 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}
⊢ μ s * ν t ≤ (μ.prod ν) (s ×ˢ t)

Proof state:
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝ : SFinite ν
s : Set α
t : Set β
S : Set α := toMeasurable μ s
T : Set β := toMeasurable ν t
hSTm : MeasurableSet (S ×ˢ T)
⊢ (μ.prod ν) (s ×ˢ t) ≤ (μ.prod ν) (S ×ˢ T)

Tactic:
gcongr <;> apply subset_toMeasurable

Result:
no goals

Proof state:
case a
α : 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)
⊢ μ s * ν t ≤ (μ.prod ν) (s ×ˢ t)

Tactic:
have hfm : Measurable f := measurable_measure_prod_mk_left hSTm

Result:
case a
α : 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 * ν t ≤ (μ.prod ν) (s ×ˢ t)

Proof state:
case a
α : 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
⊢ μ s * ν t ≤ (μ.prod ν) (s ×ˢ t)

Tactic:
have hST : s ×ˢ t ⊆ ST := subset_toMeasurable _ _

Result:
case a
α : 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
⊢ μ s * ν t ≤ (μ.prod ν) (s ×ˢ t)

Proof state:
case a
α : 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
⊢ μ s * ν t ≤ (μ.prod ν) (s ×ˢ t)

Tactic:
set f : α → ℝ≥0∞ := fun x => ν (Prod.mk x ⁻¹' ST)

Result:
case a
α : 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)
⊢ μ s * ν t ≤ (μ.prod ν) (s ×ˢ t)

Proof state:
case a
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝ : SFinite ν
s : Set α
t : Set β
⊢ μ s * ν t ≤ (μ.prod ν) (s ×ˢ t)

Tactic:
set ST := toMeasurable (μ.prod ν) (s ×ˢ t)

Result:
case a
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝ : SFinite ν
s : Set α
t : Set β
ST : Set (α × β) := toMeasurable (μ.prod ν) (s ×ˢ t)
⊢ μ s * ν t ≤ (μ.prod ν) (s ×ˢ t)

Proof state:
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝ : SFinite ν
s : Set α
t : Set β
S : Set α := toMeasurable μ s
T : Set β := toMeasurable ν t
hSTm : MeasurableSet (S ×ˢ T)
⊢ (μ.prod ν) (S ×ˢ T) = μ S * ν T

Tactic:
rw [prod_apply hSTm]

Result:
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝ : SFinite ν
s : Set α
t : Set β
S : Set α := toMeasurable μ s
T : Set β := toMeasurable ν t
hSTm : MeasurableSet (S ×ˢ T)
⊢ ∫⁻ (x : α), ν (Prod.mk x ⁻¹' S ×ˢ T) ∂μ = μ S * ν T

Proof state:
α : 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:
gcongr

Result:
no goals

Proof state:
case a
α : 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}
⊢ μ s * ν t ≤ (μ.prod ν) (s ×ˢ t)

Tactic:
have hss' : s ⊆ s' := fun x hx => measure_mono fun y hy => hST <| mk_mem_prod hx hy

Result:
case a
α : 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 ≤ (μ.prod ν) (s ×ˢ t)

Proof state:
case a
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝ : SFinite ν
s : Set α
t : Set β
S : Set α := toMeasurable μ s
T : Set β := toMeasurable ν t
⊢ (μ.prod ν) (s ×ˢ t) ≤ μ s * ν t

Tactic:
have hSTm : MeasurableSet (S ×ˢ T) :=
  (measurableSet_toMeasurable _ _).prod (measurableSet_toMeasurable _ _)

Result:
case a
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝ : SFinite ν
s : Set α
t : Set β
S : Set α := toMeasurable μ s
T : Set β := toMeasurable ν t
hSTm : MeasurableSet (S ×ˢ T)
⊢ (μ.prod ν) (s ×ˢ t) ≤ μ s * ν t

Proof state:
α : 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:
rw [setLIntegral_const, mul_comm]

Result:
no goals