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

Tactic:
simp_rw [S, mk_preimage_prod_right_eq_if, measure_if,
  lintegral_indicator (measurableSet_toMeasurable _ _), lintegral_const,
  restrict_apply_univ, mul_comm]

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

Tactic:
set S := toMeasurable μ s

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

Tactic:
set T := toMeasurable ν t

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
⊢ (μ.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)
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)

Tactic:
calc
  μ s * ν t ≤ μ s' * ν t := by gcongr
  _ = ∫⁻ _ in s', ν t ∂μ := by rw [setLIntegral_const, mul_comm]
  _ ≤ ∫⁻ x in s', f x ∂μ := setLIntegral_mono hfm fun x => id
  _ ≤ ∫⁻ x, f x ∂μ := lintegral_mono' restrict_le_self le_rfl
  _ = μ.prod ν ST := (prod_apply hSTm).symm
  _ = μ.prod ν (s ×ˢ t) := measure_toMeasurable _

Result:
no goals

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

Tactic:
apply le_antisymm

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

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)

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)
⊢ μ S * ν T = μ s * ν t

Tactic:
rw [measure_toMeasurable, measure_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 β
S : Set α := toMeasurable μ s
T : Set β := toMeasurable ν t
hSTm : MeasurableSet (S ×ˢ T)
⊢ (μ.prod ν) (s ×ˢ t) ≤ μ s * ν t

Tactic:
calc
  μ.prod ν (s ×ˢ t) ≤ μ.prod ν (S ×ˢ T) := by gcongr <;> apply subset_toMeasurable
  _ = μ S * ν T := by
    rw [prod_apply hSTm]
    simp_rw [S, mk_preimage_prod_right_eq_if, measure_if,
      lintegral_indicator (measurableSet_toMeasurable _ _), lintegral_const,
      restrict_apply_univ, mul_comm]
  _ = μ s * ν t := by rw [measure_toMeasurable, measure_toMeasurable]

Result:
no goals