-- Mathlib/MeasureTheory/Measure/Prod.lean
theorem lintegral_prod_of_measurable :
    ∀ (f : α × β → ℝ≥0∞), Measurable f → ∫⁻ z, f z ∂μ.prod ν = ∫⁻ x, ∫⁻ y, f (x, y) ∂ν ∂μ

Proof state:
case refine_1
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝ : SFinite ν
m :
  ∀ {α : Type ?u.165217} {β : Type ?u.165216} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {x : α},
    Measurable (Prod.mk x)
c : ℝ≥0∞
s : Set (α × β)
hs : MeasurableSet s
⊢ ∫⁻ (z : α × β), s.indicator (fun x => c) z ∂μ.prod ν =
    ∫⁻ (x : α), lintegral ν ((Prod.mk x ⁻¹' s).indicator fun x => c) ∂μ

Tactic:
conv_rhs =>
  enter [2, x]
  rw [lintegral_indicator (m (x := x) hs), lintegral_const,
    Measure.restrict_apply MeasurableSet.univ, univ_inter]

Result:
case refine_1
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝ : SFinite ν
m : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {x : α}, Measurable (Prod.mk x)
c : ℝ≥0∞
s : Set (α × β)
hs : MeasurableSet s
⊢ ∫⁻ (z : α × β), s.indicator (fun x => c) z ∂μ.prod ν = ∫⁻ (x : α), c * ν (Prod.mk x ⁻¹' s) ∂μ

Proof state:
case refine_1
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝ : SFinite ν
m :
  ∀ {α : Type ?u.165217} {β : Type ?u.165216} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {x : α},
    Measurable (Prod.mk x)
c : ℝ≥0∞
s : Set (α × β)
hs : MeasurableSet s
⊢ ∫⁻ (z : α × β), s.indicator (fun x => c) z ∂μ.prod ν = ∫⁻ (x : α), ∫⁻ (y : β), s.indicator (fun x => c) (x, y) ∂ν ∂μ

Tactic:
conv_rhs =>
  enter [2, x, 2, y]
  rw [← indicator_comp_right, const_def, const_comp, ← const_def]

Result:
case refine_1
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝ : SFinite ν
m :
  ∀ {α : Type ?u.165217} {β : Type ?u.165216} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {x : α},
    Measurable (Prod.mk x)
c : ℝ≥0∞
s : Set (α × β)
hs : MeasurableSet s
⊢ ∫⁻ (z : α × β), s.indicator (fun x => c) z ∂μ.prod ν =
    ∫⁻ (x : α), lintegral ν ((Prod.mk x ⁻¹' s).indicator fun x => c) ∂μ

Proof state:
case refine_3
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝ : SFinite ν
m : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {x : α}, Measurable (Prod.mk x)
f : ℕ → α × β → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
h2f : Monotone f
h3f : ∀ (n : ℕ), (fun f => ∫⁻ (z : α × β), f z ∂μ.prod ν = ∫⁻ (x : α), ∫⁻ (y : β), f (x, y) ∂ν ∂μ) (f n)
kf : ∀ (x : α) (n : ℕ), Measurable fun y => f n (x, y)
k2f : ∀ (x : α), Monotone fun n y => f n (x, y)
lf : ∀ (n : ℕ), Measurable fun x => ∫⁻ (y : β), f n (x, y) ∂ν
⊢ ∫⁻ (z : α × β), (fun x => ⨆ n, f n x) z ∂μ.prod ν = ∫⁻ (x : α), ∫⁻ (y : β), (fun x => ⨆ n, f n x) (x, y) ∂ν ∂μ

Tactic:
have l2f : Monotone fun n x => ∫⁻ y, f n (x, y) ∂ν := fun i j hij x =>
  lintegral_mono (k2f x hij)

Result:
case refine_3
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝ : SFinite ν
m : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {x : α}, Measurable (Prod.mk x)
f : ℕ → α × β → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
h2f : Monotone f
h3f : ∀ (n : ℕ), (fun f => ∫⁻ (z : α × β), f z ∂μ.prod ν = ∫⁻ (x : α), ∫⁻ (y : β), f (x, y) ∂ν ∂μ) (f n)
kf : ∀ (x : α) (n : ℕ), Measurable fun y => f n (x, y)
k2f : ∀ (x : α), Monotone fun n y => f n (x, y)
lf : ∀ (n : ℕ), Measurable fun x => ∫⁻ (y : β), f n (x, y) ∂ν
l2f : Monotone fun n x => ∫⁻ (y : β), f n (x, y) ∂ν
⊢ ∫⁻ (z : α × β), (fun x => ⨆ n, f n x) z ∂μ.prod ν = ∫⁻ (x : α), ∫⁻ (y : β), (fun x => ⨆ n, f n x) (x, y) ∂ν ∂μ

Proof state:
case refine_3
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝ : SFinite ν
m : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {x : α}, Measurable (Prod.mk x)
f : ℕ → α × β → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
h2f : Monotone f
h3f : ∀ (n : ℕ), (fun f => ∫⁻ (z : α × β), f z ∂μ.prod ν = ∫⁻ (x : α), ∫⁻ (y : β), f (x, y) ∂ν ∂μ) (f n)
kf : ∀ (x : α) (n : ℕ), Measurable fun y => f n (x, y)
k2f : ∀ (x : α), Monotone fun n y => f n (x, y)
⊢ ∫⁻ (z : α × β), (fun x => ⨆ n, f n x) z ∂μ.prod ν = ∫⁻ (x : α), ∫⁻ (y : β), (fun x => ⨆ n, f n x) (x, y) ∂ν ∂μ

Tactic:
have lf : ∀ n, Measurable fun x => ∫⁻ y, f n (x, y) ∂ν := fun n => (hf n).lintegral_prod_right'

Result:
case refine_3
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝ : SFinite ν
m : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {x : α}, Measurable (Prod.mk x)
f : ℕ → α × β → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
h2f : Monotone f
h3f : ∀ (n : ℕ), (fun f => ∫⁻ (z : α × β), f z ∂μ.prod ν = ∫⁻ (x : α), ∫⁻ (y : β), f (x, y) ∂ν ∂μ) (f n)
kf : ∀ (x : α) (n : ℕ), Measurable fun y => f n (x, y)
k2f : ∀ (x : α), Monotone fun n y => f n (x, y)
lf : ∀ (n : ℕ), Measurable fun x => ∫⁻ (y : β), f n (x, y) ∂ν
⊢ ∫⁻ (z : α × β), (fun x => ⨆ n, f n x) z ∂μ.prod ν = ∫⁻ (x : α), ∫⁻ (y : β), (fun x => ⨆ n, f n x) (x, y) ∂ν ∂μ

Proof state:
case refine_3
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝ : SFinite ν
m : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {x : α}, Measurable (Prod.mk x)
f : ℕ → α × β → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
h2f : Monotone f
h3f : ∀ (n : ℕ), (fun f => ∫⁻ (z : α × β), f z ∂μ.prod ν = ∫⁻ (x : α), ∫⁻ (y : β), f (x, y) ∂ν ∂μ) (f n)
kf : ∀ (x : α) (n : ℕ), Measurable fun y => f n (x, y)
⊢ ∫⁻ (z : α × β), (fun x => ⨆ n, f n x) z ∂μ.prod ν = ∫⁻ (x : α), ∫⁻ (y : β), (fun x => ⨆ n, f n x) (x, y) ∂ν ∂μ

Tactic:
have k2f : ∀ x, Monotone fun n y => f n (x, y) := fun x i j hij y => h2f hij (x, y)

Result:
case refine_3
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝ : SFinite ν
m : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {x : α}, Measurable (Prod.mk x)
f : ℕ → α × β → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
h2f : Monotone f
h3f : ∀ (n : ℕ), (fun f => ∫⁻ (z : α × β), f z ∂μ.prod ν = ∫⁻ (x : α), ∫⁻ (y : β), f (x, y) ∂ν ∂μ) (f n)
kf : ∀ (x : α) (n : ℕ), Measurable fun y => f n (x, y)
k2f : ∀ (x : α), Monotone fun n y => f n (x, y)
⊢ ∫⁻ (z : α × β), (fun x => ⨆ n, f n x) z ∂μ.prod ν = ∫⁻ (x : α), ∫⁻ (y : β), (fun x => ⨆ n, f n x) (x, y) ∂ν ∂μ

Proof state:
case refine_1
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝ : SFinite ν
m : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {x : α}, Measurable (Prod.mk x)
c : ℝ≥0∞
s : Set (α × β)
hs : MeasurableSet s
⊢ ∫⁻ (z : α × β), s.indicator (fun x => c) z ∂μ.prod ν = ∫⁻ (x : α), c * ν (Prod.mk x ⁻¹' s) ∂μ

Tactic:
simp [hs, lintegral_const_mul, measurable_measure_prod_mk_left (ν := ν) hs, prod_apply]

Result:
no goals