-- 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:
α : 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)
⊢ ∀ (f : α × β → ℝ≥0∞), Measurable f → ∫⁻ (z : α × β), f z ∂μ.prod ν = ∫⁻ (x : α), ∫⁻ (y : β), f (x, y) ∂ν ∂μ

Tactic:
refine Measurable.ennreal_induction
  (P := fun f => ∫⁻ z, f z ∂μ.prod ν = ∫⁻ x, ∫⁻ y, f (x, y) ∂ν ∂μ) ?_ ?_ ?_

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 (α × β)⦄,
    MeasurableSet s →
      (fun f => ∫⁻ (z : α × β), f z ∂μ.prod ν = ∫⁻ (x : α), ∫⁻ (y : β), f (x, y) ∂ν ∂μ) (s.indicator fun x => c)

case refine_2
α : 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)
⊢ ∀ ⦃f g : α × β → ℝ≥0∞⦄,
    Disjoint (support f) (support g) →
      Measurable f →
        Measurable g →
          (fun f => ∫⁻ (z : α × β), f z ∂μ.prod ν = ∫⁻ (x : α), ∫⁻ (y : β), f (x, y) ∂ν ∂μ) f →
            (fun f => ∫⁻ (z : α × β), f z ∂μ.prod ν = ∫⁻ (x : α), ∫⁻ (y : β), f (x, y) ∂ν ∂μ) g →
              (fun f => ∫⁻ (z : α × β), f z ∂μ.prod ν = ∫⁻ (x : α), ∫⁻ (y : β), f (x, y) ∂ν ∂μ) (f + g)

case refine_3
α : 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)
⊢ ∀ ⦃f : ℕ → α × β → ℝ≥0∞⦄,
    (∀ (n : ℕ), Measurable (f n)) →
      Monotone f →
        (∀ (n : ℕ), (fun f => ∫⁻ (z : α × β), f z ∂μ.prod ν = ∫⁻ (x : α), ∫⁻ (y : β), f (x, y) ∂ν ∂μ) (f n)) →
          (fun f => ∫⁻ (z : α × β), f z ∂μ.prod ν = ∫⁻ (x : α), ∫⁻ (y : β), f (x, y) ∂ν ∂μ) fun x => ⨆ n, f n x

Proof state:
case refine_2
α : 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 g : α × β → ℝ≥0∞
hf : Measurable f
a✝ : Measurable g
h2f : ∫⁻ (z : α × β), f z ∂μ.prod ν = ∫⁻ (x : α), ∫⁻ (y : β), f (x, y) ∂ν ∂μ
h2g : ∫⁻ (z : α × β), g z ∂μ.prod ν = ∫⁻ (x : α), ∫⁻ (y : β), g (x, y) ∂ν ∂μ
⊢ ∫⁻ (a : α × β), f a ∂μ.prod ν + ∫⁻ (a : α × β), g a ∂μ.prod ν = ∫⁻ (x : α), ∫⁻ (y : β), f (x, y) + g (x, y) ∂ν ∂μ

Tactic:
conv_rhs => enter [2, x]; erw [lintegral_add_left (hf.comp (m (x := x)))]

Result:
case refine_2
α : 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 g : α × β → ℝ≥0∞
hf : Measurable f
a✝ : Measurable g
h2f : ∫⁻ (z : α × β), f z ∂μ.prod ν = ∫⁻ (x : α), ∫⁻ (y : β), f (x, y) ∂ν ∂μ
h2g : ∫⁻ (z : α × β), g z ∂μ.prod ν = ∫⁻ (x : α), ∫⁻ (y : β), g (x, y) ∂ν ∂μ
⊢ ∫⁻ (a : α × β), f a ∂μ.prod ν + ∫⁻ (a : α × β), g a ∂μ.prod ν =
    ∫⁻ (x : α), ∫⁻ (a : β), (f ∘ Prod.mk x) a ∂ν + ∫⁻ (a : β), g (x, a) ∂ν ∂μ

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) ∂ν
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) ∂ν ∂μ

Tactic:
simp only [lintegral_iSup hf h2f, lintegral_iSup (kf _), k2f, lintegral_iSup lf l2f, h3f]

Result:
no goals

Proof state:
case refine_2
α : 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 g : α × β → ℝ≥0∞
hf : Measurable f
a✝ : Measurable g
h2f : ∫⁻ (z : α × β), f z ∂μ.prod ν = ∫⁻ (x : α), ∫⁻ (y : β), f (x, y) ∂ν ∂μ
h2g : ∫⁻ (z : α × β), g z ∂μ.prod ν = ∫⁻ (x : α), ∫⁻ (y : β), g (x, y) ∂ν ∂μ
⊢ ∫⁻ (z : α × β), f z + g z ∂μ.prod ν = ∫⁻ (x : α), ∫⁻ (y : β), f (x, y) + g (x, y) ∂ν ∂μ

Tactic:
conv_lhs => rw [lintegral_add_left hf]

Result:
case refine_2
α : 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 g : α × β → ℝ≥0∞
hf : Measurable f
a✝ : Measurable g
h2f : ∫⁻ (z : α × β), f z ∂μ.prod ν = ∫⁻ (x : α), ∫⁻ (y : β), f (x, y) ∂ν ∂μ
h2g : ∫⁻ (z : α × β), g z ∂μ.prod ν = ∫⁻ (x : α), ∫⁻ (y : β), g (x, y) ∂ν ∂μ
⊢ ∫⁻ (a : α × β), f a ∂μ.prod ν + ∫⁻ (a : α × β), g a ∂μ.prod ν = ∫⁻ (x : α), ∫⁻ (y : β), f (x, y) + g (x, y) ∂ν ∂μ

Proof state:
case refine_2
α : 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 g : α × β → ℝ≥0∞⦄,
    Disjoint (support f) (support g) →
      Measurable f →
        Measurable g →
          (fun f => ∫⁻ (z : α × β), f z ∂μ.prod ν = ∫⁻ (x : α), ∫⁻ (y : β), f (x, y) ∂ν ∂μ) f →
            (fun f => ∫⁻ (z : α × β), f z ∂μ.prod ν = ∫⁻ (x : α), ∫⁻ (y : β), f (x, y) ∂ν ∂μ) g →
              (fun f => ∫⁻ (z : α × β), f z ∂μ.prod ν = ∫⁻ (x : α), ∫⁻ (y : β), f (x, y) ∂ν ∂μ) (f + g)

Tactic:
rintro f g - hf _ h2f h2g

Result:
case refine_2
α : 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 g : α × β → ℝ≥0∞
hf : Measurable f
a✝ : Measurable g
h2f : ∫⁻ (z : α × β), f z ∂μ.prod ν = ∫⁻ (x : α), ∫⁻ (y : β), f (x, y) ∂ν ∂μ
h2g : ∫⁻ (z : α × β), g z ∂μ.prod ν = ∫⁻ (x : α), ∫⁻ (y : β), g (x, y) ∂ν ∂μ
⊢ ∫⁻ (z : α × β), (f + g) z ∂μ.prod ν = ∫⁻ (x : α), ∫⁻ (y : β), (f + g) (x, y) ∂ν ∂μ

Proof state:
case refine_2
α : 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 g : α × β → ℝ≥0∞
hf : Measurable f
a✝ : Measurable g
h2f : ∫⁻ (z : α × β), f z ∂μ.prod ν = ∫⁻ (x : α), ∫⁻ (y : β), f (x, y) ∂ν ∂μ
h2g : ∫⁻ (z : α × β), g z ∂μ.prod ν = ∫⁻ (x : α), ∫⁻ (y : β), g (x, y) ∂ν ∂μ
⊢ ∫⁻ (a : α × β), f a ∂μ.prod ν + ∫⁻ (a : α × β), g a ∂μ.prod ν =
    ∫⁻ (x : α), ∫⁻ (a : β), (f ∘ Prod.mk x) a ∂ν + ∫⁻ (a : β), g (x, a) ∂ν ∂μ

Tactic:
simp [lintegral_add_left, Measurable.lintegral_prod_right', hf, h2f, h2g]

Result:
no goals