-- Mathlib/MeasureTheory/Integral/Marginal.lean
theorem lmarginal_image [DecidableEq δ'] {e : δ' → δ} (he : Injective e) (s : Finset δ')
    {f : (∀ i, π (e i)) → ℝ≥0∞} (hf : Measurable f) (x : ∀ i, π i) :
      (∫⋯∫⁻_s.image e, f ∘ (· ∘' e) ∂μ) x = (∫⋯∫⁻_s, f ∂μ ∘' e) (x ∘' e)

Proof state:
case insert
δ : Type u_1
δ' : Type u_2
π : δ → Type u_3
inst✝³ : (x : δ) → MeasurableSpace (π x)
μ : (i : δ) → Measure (π i)
inst✝² : DecidableEq δ
inst✝¹ : ∀ (i : δ), SigmaFinite (μ i)
inst✝ : DecidableEq δ'
e : δ' → δ
he : Injective e
f : ((i : δ') → π (e i)) → ℝ≥0∞
hf : Measurable f
h : Measurable fun x => (fun {x_1} => x) ∘' e
a✝ : δ'
s✝ : Finset δ'
hi : a✝ ∉ s✝
ih :
  ∀ (x : (i : δ) → π i),
    (∫⋯∫⁻_Finset.image e s✝, f ∘ fun x => (fun {x_1} => x) ∘' e ∂μ) x =
      (∫⋯∫⁻_s✝, f ∂(fun {x} => μ) ∘' e) ((fun {x_1} => x) ∘' e)
x : (i : δ) → π i
⊢ (∫⋯∫⁻_Finset.image e (insert a✝ s✝), f ∘ fun x => (fun {x_1} => x) ∘' e ∂μ) x =
    (∫⋯∫⁻_insert a✝ s✝, f ∂(fun {x} => μ) ∘' e) ((fun {x_1} => x) ∘' e)

Tactic:
rw [image_insert, lmarginal_insert _ (hf.comp h) (he.mem_finset_image.not.mpr hi),
  lmarginal_insert _ hf hi]

Result:
case insert
δ : Type u_1
δ' : Type u_2
π : δ → Type u_3
inst✝³ : (x : δ) → MeasurableSpace (π x)
μ : (i : δ) → Measure (π i)
inst✝² : DecidableEq δ
inst✝¹ : ∀ (i : δ), SigmaFinite (μ i)
inst✝ : DecidableEq δ'
e : δ' → δ
he : Injective e
f : ((i : δ') → π (e i)) → ℝ≥0∞
hf : Measurable f
h : Measurable fun x => (fun {x_1} => x) ∘' e
a✝ : δ'
s✝ : Finset δ'
hi : a✝ ∉ s✝
ih :
  ∀ (x : (i : δ) → π i),
    (∫⋯∫⁻_Finset.image e s✝, f ∘ fun x => (fun {x_1} => x) ∘' e ∂μ) x =
      (∫⋯∫⁻_s✝, f ∂(fun {x} => μ) ∘' e) ((fun {x_1} => x) ∘' e)
x : (i : δ) → π i
⊢ ∫⁻ (xᵢ : π (e a✝)), (∫⋯∫⁻_Finset.image e s✝, f ∘ fun x => (fun {x_1} => x) ∘' e ∂μ) (update x (e a✝) xᵢ) ∂μ (e a✝) =
    ∫⁻ (xᵢ : π (e a✝)),
      (∫⋯∫⁻_s✝, f ∂(fun {x} => μ) ∘' e) (update ((fun {x_1} => x) ∘' e) a✝ xᵢ) ∂((fun {x} => μ) ∘' e) a✝

Proof state:
case empty
δ : Type u_1
δ' : Type u_2
π : δ → Type u_3
inst✝³ : (x : δ) → MeasurableSpace (π x)
μ : (i : δ) → Measure (π i)
inst✝² : DecidableEq δ
inst✝¹ : ∀ (i : δ), SigmaFinite (μ i)
inst✝ : DecidableEq δ'
e : δ' → δ
he : Injective e
f : ((i : δ') → π (e i)) → ℝ≥0∞
hf : Measurable f
h : Measurable fun x => (fun {x_1} => x) ∘' e
x : (i : δ) → π i
⊢ (∫⋯∫⁻_Finset.image e ∅, f ∘ fun x => (fun {x_1} => x) ∘' e ∂μ) x =
    (∫⋯∫⁻_∅, f ∂(fun {x} => μ) ∘' e) ((fun {x_1} => x) ∘' e)

Tactic:
simp

Result:
no goals

Proof state:
case insert
δ : Type u_1
δ' : Type u_2
π : δ → Type u_3
inst✝³ : (x : δ) → MeasurableSpace (π x)
μ : (i : δ) → Measure (π i)
inst✝² : DecidableEq δ
inst✝¹ : ∀ (i : δ), SigmaFinite (μ i)
inst✝ : DecidableEq δ'
e : δ' → δ
he : Injective e
f : ((i : δ') → π (e i)) → ℝ≥0∞
hf : Measurable f
h : Measurable fun x => (fun {x_1} => x) ∘' e
a✝ : δ'
s✝ : Finset δ'
hi : a✝ ∉ s✝
ih :
  ∀ (x : (i : δ) → π i),
    (∫⋯∫⁻_Finset.image e s✝, f ∘ fun x => (fun {x_1} => x) ∘' e ∂μ) x =
      (∫⋯∫⁻_s✝, f ∂(fun {x} => μ) ∘' e) ((fun {x_1} => x) ∘' e)
x : (i : δ) → π i
⊢ ∫⁻ (xᵢ : π (e a✝)), (∫⋯∫⁻_Finset.image e s✝, f ∘ fun x => (fun {x_1} => x) ∘' e ∂μ) (update x (e a✝) xᵢ) ∂μ (e a✝) =
    ∫⁻ (xᵢ : π (e a✝)),
      (∫⋯∫⁻_s✝, f ∂(fun {x} => μ) ∘' e) (update ((fun {x_1} => x) ∘' e) a✝ xᵢ) ∂((fun {x} => μ) ∘' e) a✝

Tactic:
simp_rw [ih, ← update_comp_eq_of_injective' x he]

Result:
no goals

Proof state:
δ : Type u_1
δ' : Type u_2
π : δ → Type u_3
inst✝³ : (x : δ) → MeasurableSpace (π x)
μ : (i : δ) → Measure (π i)
inst✝² : DecidableEq δ
inst✝¹ : ∀ (i : δ), SigmaFinite (μ i)
inst✝ : DecidableEq δ'
e : δ' → δ
he : Injective e
s : Finset δ'
f : ((i : δ') → π (e i)) → ℝ≥0∞
hf : Measurable f
x : (i : δ) → π i
h : Measurable fun x => (fun {x_1} => x) ∘' e
⊢ (∫⋯∫⁻_Finset.image e s, f ∘ fun x => (fun {x_1} => x) ∘' e ∂μ) x =
    (∫⋯∫⁻_s, f ∂(fun {x} => μ) ∘' e) ((fun {x_1} => x) ∘' e)

Tactic:
induction s using Finset.induction generalizing x with
| empty => simp
| insert hi ih =>
  rw [image_insert, lmarginal_insert _ (hf.comp h) (he.mem_finset_image.not.mpr hi),
    lmarginal_insert _ hf hi]
  simp_rw [ih, ← update_comp_eq_of_injective' x he]

Result:
no goals