-- Mathlib/MeasureTheory/Integral/Marginal.lean
theorem lmarginal_update_of_not_mem {i : δ}
    {f : (∀ i, π i) → ℝ≥0∞} (hf : Measurable f) (hi : i ∉ s) (x : ∀ i, π i) (y : π i) :
    (∫⋯∫⁻_s, f ∂μ) (Function.update x i y) = (∫⋯∫⁻_s, f ∘ (Function.update · i y) ∂μ) x

Proof state:
case empty
δ : Type u_1
π : δ → Type u_3
inst✝² : (x : δ) → MeasurableSpace (π x)
μ : (i : δ) → Measure (π i)
inst✝¹ : DecidableEq δ
s : Finset δ
inst✝ : ∀ (i : δ), SigmaFinite (μ i)
i : δ
f : ((i : δ) → π i) → ℝ≥0∞
hf : Measurable f
y : π i
hi : i ∉ ∅
x : (i : δ) → π i
⊢ (∫⋯∫⁻_∅, f ∂μ) (update x i y) = (∫⋯∫⁻_∅, f ∘ fun x => update x i y ∂μ) x

Tactic:
simp

Result:
no goals

Proof state:
case insert
δ : Type u_1
π : δ → Type u_3
inst✝² : (x : δ) → MeasurableSpace (π x)
μ : (i : δ) → Measure (π i)
inst✝¹ : DecidableEq δ
s✝ : Finset δ
inst✝ : ∀ (i : δ), SigmaFinite (μ i)
i : δ
f : ((i : δ) → π i) → ℝ≥0∞
hf : Measurable f
y : π i
i' : δ
s : Finset δ
hi' : i' ∉ s
ih : i ∉ s → ∀ (x : (i : δ) → π i), (∫⋯∫⁻_s, f ∂μ) (update x i y) = (∫⋯∫⁻_s, f ∘ fun x => update x i y ∂μ) x
hi : i ∉ insert i' s
x : (i : δ) → π i
⊢ ∫⁻ (xᵢ : π i'), (∫⋯∫⁻_s, f ∂μ) (update (update x i y) i' xᵢ) ∂μ i' =
    ∫⁻ (xᵢ : π i'), (∫⋯∫⁻_s, f ∘ fun x => update x i y ∂μ) (update x i' xᵢ) ∂μ i'

Tactic:
have hii' : i ≠ i' := mt (by rintro rfl; exact mem_insert_self i s) hi

Result:
case insert
δ : Type u_1
π : δ → Type u_3
inst✝² : (x : δ) → MeasurableSpace (π x)
μ : (i : δ) → Measure (π i)
inst✝¹ : DecidableEq δ
s✝ : Finset δ
inst✝ : ∀ (i : δ), SigmaFinite (μ i)
i : δ
f : ((i : δ) → π i) → ℝ≥0∞
hf : Measurable f
y : π i
i' : δ
s : Finset δ
hi' : i' ∉ s
ih : i ∉ s → ∀ (x : (i : δ) → π i), (∫⋯∫⁻_s, f ∂μ) (update x i y) = (∫⋯∫⁻_s, f ∘ fun x => update x i y ∂μ) x
hi : i ∉ insert i' s
x : (i : δ) → π i
hii' : i ≠ i'
⊢ ∫⁻ (xᵢ : π i'), (∫⋯∫⁻_s, f ∂μ) (update (update x i y) i' xᵢ) ∂μ i' =
    ∫⁻ (xᵢ : π i'), (∫⋯∫⁻_s, f ∘ fun x => update x i y ∂μ) (update x i' xᵢ) ∂μ i'

Proof state:
case insert
δ : Type u_1
π : δ → Type u_3
inst✝² : (x : δ) → MeasurableSpace (π x)
μ : (i : δ) → Measure (π i)
inst✝¹ : DecidableEq δ
s✝ : Finset δ
inst✝ : ∀ (i : δ), SigmaFinite (μ i)
i : δ
f : ((i : δ) → π i) → ℝ≥0∞
hf : Measurable f
y : π i
i' : δ
s : Finset δ
hi' : i' ∉ s
ih : i ∉ s → ∀ (x : (i : δ) → π i), (∫⋯∫⁻_s, f ∂μ) (update x i y) = (∫⋯∫⁻_s, f ∘ fun x => update x i y ∂μ) x
hi : i ∉ insert i' s
x : (i : δ) → π i
⊢ (∫⋯∫⁻_insert i' s, f ∂μ) (update x i y) = (∫⋯∫⁻_insert i' s, f ∘ fun x => update x i y ∂μ) x

Tactic:
rw [lmarginal_insert _ hf hi', lmarginal_insert _ (hf.comp measurable_update_left) hi']

Result:
case insert
δ : Type u_1
π : δ → Type u_3
inst✝² : (x : δ) → MeasurableSpace (π x)
μ : (i : δ) → Measure (π i)
inst✝¹ : DecidableEq δ
s✝ : Finset δ
inst✝ : ∀ (i : δ), SigmaFinite (μ i)
i : δ
f : ((i : δ) → π i) → ℝ≥0∞
hf : Measurable f
y : π i
i' : δ
s : Finset δ
hi' : i' ∉ s
ih : i ∉ s → ∀ (x : (i : δ) → π i), (∫⋯∫⁻_s, f ∂μ) (update x i y) = (∫⋯∫⁻_s, f ∘ fun x => update x i y ∂μ) x
hi : i ∉ insert i' s
x : (i : δ) → π i
⊢ ∫⁻ (xᵢ : π i'), (∫⋯∫⁻_s, f ∂μ) (update (update x i y) i' xᵢ) ∂μ i' =
    ∫⁻ (xᵢ : π i'), (∫⋯∫⁻_s, f ∘ fun x => update x i y ∂μ) (update x i' xᵢ) ∂μ i'

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

Tactic:
induction s using Finset.induction generalizing x with
| empty => simp
| @insert i' s hi' ih =>
  rw [lmarginal_insert _ hf hi', lmarginal_insert _ (hf.comp measurable_update_left) hi']
  have hii' : i ≠ i' := mt (by rintro rfl; exact mem_insert_self i s) hi
  simp_rw [update_comm hii', ih (mt Finset.mem_insert_of_mem hi)]

Result:
no goals

Proof state:
δ : Type u_1
π : δ → Type u_3
inst✝² : (x : δ) → MeasurableSpace (π x)
μ : (i : δ) → Measure (π i)
inst✝¹ : DecidableEq δ
s✝ : Finset δ
inst✝ : ∀ (i : δ), SigmaFinite (μ i)
i : δ
f : ((i : δ) → π i) → ℝ≥0∞
hf : Measurable f
y : π i
s : Finset δ
ih : i ∉ s → ∀ (x : (i : δ) → π i), (∫⋯∫⁻_s, f ∂μ) (update x i y) = (∫⋯∫⁻_s, f ∘ fun x => update x i y ∂μ) x
x : (i : δ) → π i
hi' : i ∉ s
hi : i ∉ insert i s
⊢ i ∈ insert i s

Tactic:
exact mem_insert_self i s

Result:
no goals

Proof state:
case insert
δ : Type u_1
π : δ → Type u_3
inst✝² : (x : δ) → MeasurableSpace (π x)
μ : (i : δ) → Measure (π i)
inst✝¹ : DecidableEq δ
s✝ : Finset δ
inst✝ : ∀ (i : δ), SigmaFinite (μ i)
i : δ
f : ((i : δ) → π i) → ℝ≥0∞
hf : Measurable f
y : π i
i' : δ
s : Finset δ
hi' : i' ∉ s
ih : i ∉ s → ∀ (x : (i : δ) → π i), (∫⋯∫⁻_s, f ∂μ) (update x i y) = (∫⋯∫⁻_s, f ∘ fun x => update x i y ∂μ) x
hi : i ∉ insert i' s
x : (i : δ) → π i
hii' : i ≠ i'
⊢ ∫⁻ (xᵢ : π i'), (∫⋯∫⁻_s, f ∂μ) (update (update x i y) i' xᵢ) ∂μ i' =
    ∫⁻ (xᵢ : π i'), (∫⋯∫⁻_s, f ∘ fun x => update x i y ∂μ) (update x i' xᵢ) ∂μ i'

Tactic:
simp_rw [update_comm hii', ih (mt Finset.mem_insert_of_mem hi)]

Result:
no goals

Proof state:
δ : Type u_1
π : δ → Type u_3
inst✝² : (x : δ) → MeasurableSpace (π x)
μ : (i : δ) → Measure (π i)
inst✝¹ : DecidableEq δ
s✝ : Finset δ
inst✝ : ∀ (i : δ), SigmaFinite (μ i)
i : δ
f : ((i : δ) → π i) → ℝ≥0∞
hf : Measurable f
y : π i
i' : δ
s : Finset δ
hi' : i' ∉ s
ih : i ∉ s → ∀ (x : (i : δ) → π i), (∫⋯∫⁻_s, f ∂μ) (update x i y) = (∫⋯∫⁻_s, f ∘ fun x => update x i y ∂μ) x
hi : i ∉ insert i' s
x : (i : δ) → π i
⊢ i = i' → i ∈ insert i' s

Tactic:
rintro rfl

Result:
δ : Type u_1
π : δ → Type u_3
inst✝² : (x : δ) → MeasurableSpace (π x)
μ : (i : δ) → Measure (π i)
inst✝¹ : DecidableEq δ
s✝ : Finset δ
inst✝ : ∀ (i : δ), SigmaFinite (μ i)
i : δ
f : ((i : δ) → π i) → ℝ≥0∞
hf : Measurable f
y : π i
s : Finset δ
ih : i ∉ s → ∀ (x : (i : δ) → π i), (∫⋯∫⁻_s, f ∂μ) (update x i y) = (∫⋯∫⁻_s, f ∘ fun x => update x i y ∂μ) x
x : (i : δ) → π i
hi' : i ∉ s
hi : i ∉ insert i s
⊢ i ∈ insert i s