-- Mathlib/MeasureTheory/Integral/Marginal.lean
theorem _root_.Measurable.lmarginal [∀ i, SigmaFinite (μ i)] (hf : Measurable f) :
    Measurable (∫⋯∫⁻_s, f ∂μ)

Proof state:
δ : Type u_1
π : δ → Type u_3
inst✝² : (x : δ) → MeasurableSpace (π x)
μ : (i : δ) → Measure (π i)
inst✝¹ : DecidableEq δ
s : Finset δ
f : ((i : δ) → π i) → ℝ≥0∞
inst✝ : ∀ (i : δ), SigmaFinite (μ i)
hf : Measurable f
⊢ Measurable (uncurry fun x y => f (updateFinset x s y))

Tactic:
refine hf.comp ?_

Result:
δ : Type u_1
π : δ → Type u_3
inst✝² : (x : δ) → MeasurableSpace (π x)
μ : (i : δ) → Measure (π i)
inst✝¹ : DecidableEq δ
s : Finset δ
f : ((i : δ) → π i) → ℝ≥0∞
inst✝ : ∀ (i : δ), SigmaFinite (μ i)
hf : Measurable f
⊢ Measurable fun a => updateFinset a.1 s a.2

Proof state:
δ : Type u_1
π : δ → Type u_3
inst✝² : (x : δ) → MeasurableSpace (π x)
μ : (i : δ) → Measure (π i)
inst✝¹ : DecidableEq δ
s : Finset δ
f : ((i : δ) → π i) → ℝ≥0∞
inst✝ : ∀ (i : δ), SigmaFinite (μ i)
hf : Measurable f
⊢ ∀ (a : δ), Measurable fun x => updateFinset x.1 s x.2 a

Tactic:
intro i

Result:
δ : Type u_1
π : δ → Type u_3
inst✝² : (x : δ) → MeasurableSpace (π x)
μ : (i : δ) → Measure (π i)
inst✝¹ : DecidableEq δ
s : Finset δ
f : ((i : δ) → π i) → ℝ≥0∞
inst✝ : ∀ (i : δ), SigmaFinite (μ i)
hf : Measurable f
i : δ
⊢ Measurable fun x => updateFinset x.1 s x.2 i

Proof state:
case neg
δ : Type u_1
π : δ → Type u_3
inst✝² : (x : δ) → MeasurableSpace (π x)
μ : (i : δ) → Measure (π i)
inst✝¹ : DecidableEq δ
s : Finset δ
f : ((i : δ) → π i) → ℝ≥0∞
inst✝ : ∀ (i : δ), SigmaFinite (μ i)
hf : Measurable f
i : δ
hi : i ∉ s
⊢ Measurable fun x => updateFinset x.1 s x.2 i

Tactic:
simpa [hi, updateFinset] using measurable_pi_iff.1 measurable_fst _

Result:
no goals

Proof state:
case pos
δ : Type u_1
π : δ → Type u_3
inst✝² : (x : δ) → MeasurableSpace (π x)
μ : (i : δ) → Measure (π i)
inst✝¹ : DecidableEq δ
s : Finset δ
f : ((i : δ) → π i) → ℝ≥0∞
inst✝ : ∀ (i : δ), SigmaFinite (μ i)
hf : Measurable f
i : δ
hi : i ∈ s
⊢ Measurable fun x => updateFinset x.1 s x.2 i

Tactic:
simpa [hi, updateFinset] using measurable_pi_iff.1 measurable_snd _

Result:
no goals

Proof state:
δ : Type u_1
π : δ → Type u_3
inst✝² : (x : δ) → MeasurableSpace (π x)
μ : (i : δ) → Measure (π i)
inst✝¹ : DecidableEq δ
s : Finset δ
f : ((i : δ) → π i) → ℝ≥0∞
inst✝ : ∀ (i : δ), SigmaFinite (μ i)
hf : Measurable f
⊢ Measurable fun a => updateFinset a.1 s a.2

Tactic:
rw [measurable_pi_iff]

Result:
δ : Type u_1
π : δ → Type u_3
inst✝² : (x : δ) → MeasurableSpace (π x)
μ : (i : δ) → Measure (π i)
inst✝¹ : DecidableEq δ
s : Finset δ
f : ((i : δ) → π i) → ℝ≥0∞
inst✝ : ∀ (i : δ), SigmaFinite (μ i)
hf : Measurable f
⊢ ∀ (a : δ), Measurable fun x => updateFinset x.1 s x.2 a

Proof state:
δ : Type u_1
π : δ → Type u_3
inst✝² : (x : δ) → MeasurableSpace (π x)
μ : (i : δ) → Measure (π i)
inst✝¹ : DecidableEq δ
s : Finset δ
f : ((i : δ) → π i) → ℝ≥0∞
inst✝ : ∀ (i : δ), SigmaFinite (μ i)
hf : Measurable f
i : δ
⊢ Measurable fun x => updateFinset x.1 s x.2 i

Tactic:
by_cases hi : i ∈ s

Result:
case pos
δ : Type u_1
π : δ → Type u_3
inst✝² : (x : δ) → MeasurableSpace (π x)
μ : (i : δ) → Measure (π i)
inst✝¹ : DecidableEq δ
s : Finset δ
f : ((i : δ) → π i) → ℝ≥0∞
inst✝ : ∀ (i : δ), SigmaFinite (μ i)
hf : Measurable f
i : δ
hi : i ∈ s
⊢ Measurable fun x => updateFinset x.1 s x.2 i

case neg
δ : Type u_1
π : δ → Type u_3
inst✝² : (x : δ) → MeasurableSpace (π x)
μ : (i : δ) → Measure (π i)
inst✝¹ : DecidableEq δ
s : Finset δ
f : ((i : δ) → π i) → ℝ≥0∞
inst✝ : ∀ (i : δ), SigmaFinite (μ i)
hf : Measurable f
i : δ
hi : i ∉ s
⊢ Measurable fun x => updateFinset x.1 s x.2 i

Proof state:
δ : Type u_1
π : δ → Type u_3
inst✝² : (x : δ) → MeasurableSpace (π x)
μ : (i : δ) → Measure (π i)
inst✝¹ : DecidableEq δ
s : Finset δ
f : ((i : δ) → π i) → ℝ≥0∞
inst✝ : ∀ (i : δ), SigmaFinite (μ i)
hf : Measurable f
⊢ Measurable (∫⋯∫⁻_s, f ∂μ)

Tactic:
refine Measurable.lintegral_prod_right ?_

Result:
δ : Type u_1
π : δ → Type u_3
inst✝² : (x : δ) → MeasurableSpace (π x)
μ : (i : δ) → Measure (π i)
inst✝¹ : DecidableEq δ
s : Finset δ
f : ((i : δ) → π i) → ℝ≥0∞
inst✝ : ∀ (i : δ), SigmaFinite (μ i)
hf : Measurable f
⊢ Measurable (uncurry fun x y => f (updateFinset x s y))