-- Mathlib/MeasureTheory/Measure/Prod.lean
theorem Measurable.lintegral_prod_right' [SFinite ν] :
    ∀ {f : α × β → ℝ≥0∞}, Measurable f → Measurable fun x => ∫⁻ y, f (x, y) ∂ν

Proof state:
case refine_2
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
m :
  ∀ {α : Type ?u.7641} {β : Type ?u.7640} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {x : α},
    Measurable (Prod.mk x)
f g : α × β → ℝ≥0∞
hf : Measurable f
h2f : Measurable fun x => ∫⁻ (y : β), f (x, y) ∂ν
h2g : Measurable fun x => ∫⁻ (y : β), g (x, y) ∂ν
⊢ Measurable fun x => ∫⁻ (y : β), f (x, y) + g (x, y) ∂ν

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

Result:
case refine_2
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
ν : 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
h2f : Measurable fun x => ∫⁻ (y : β), f (x, y) ∂ν
h2g : Measurable fun x => ∫⁻ (y : β), g (x, y) ∂ν
⊢ Measurable fun x => ∫⁻ (a : β), (f ∘ Prod.mk x) a ∂ν + ∫⁻ (a : β), g (x, a) ∂ν

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

Tactic:
simpa [lintegral_indicator (m hs)]

Result:
no goals

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

Tactic:
simp only [← indicator_comp_right]

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

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

Tactic:
suffices Measurable fun x => c * ν (Prod.mk x ⁻¹' s) by simpa [lintegral_indicator (m hs)]

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

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

Tactic:
exact (measurable_measure_prod_mk_left hs).const_mul _

Result:
no goals

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

Tactic:
intro f hf h2f h3f

Result:
case refine_3
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
ν : 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 => Measurable fun x => ∫⁻ (y : β), f (x, y) ∂ν) (f n)
⊢ Measurable fun x => ∫⁻ (y : β), (fun x => ⨆ n, f n x) (x, y) ∂ν

Proof state:
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
⊢ ∀ {f : α × β → ℝ≥0∞}, Measurable f → Measurable fun x => ∫⁻ (y : β), f (x, y) ∂ν

Tactic:
have m := @measurable_prod_mk_left

Result:
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
m :
  ∀ {α : Type ?u.7641} {β : Type ?u.7640} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {x : α},
    Measurable (Prod.mk x)
⊢ ∀ {f : α × β → ℝ≥0∞}, Measurable f → Measurable fun x => ∫⁻ (y : β), f (x, y) ∂ν

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

Tactic:
intro c s hs

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