-- Mathlib/MeasureTheory/Integral/Marginal.lean
theorem lmarginal_union (f : (∀ i, π i) → ℝ≥0∞) (hf : Measurable f)
    (hst : Disjoint s t) : ∫⋯∫⁻_s ∪ t, f ∂μ = ∫⋯∫⁻_s, ∫⋯∫⁻_t, f ∂μ ∂μ

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

Tactic:
ext1 x

Result:
case h
δ : Type u_1
π : δ → Type u_3
inst✝² : (x : δ) → MeasurableSpace (π x)
μ : (i : δ) → Measure (π i)
inst✝¹ : DecidableEq δ
s t : Finset δ
inst✝ : ∀ (i : δ), SigmaFinite (μ i)
f : ((i : δ) → π i) → ℝ≥0∞
hf : Measurable f
hst : Disjoint s t
x : (i : δ) → π i
⊢ (∫⋯∫⁻_s ∪ t, f ∂μ) x = (∫⋯∫⁻_s, ∫⋯∫⁻_t, f ∂μ ∂μ) x

Proof state:
δ : Type u_1
π : δ → Type u_3
inst✝² : (x : δ) → MeasurableSpace (π x)
μ : (i : δ) → Measure (π i)
inst✝¹ : DecidableEq δ
s t : Finset δ
inst✝ : ∀ (i : δ), SigmaFinite (μ i)
f : ((i : δ) → π i) → ℝ≥0∞
hf : Measurable f
hst : Disjoint s t
x : (i : δ) → π i
e : ((i : { x // x ∈ s }) → π ↑i) × ((i : { x // x ∈ t }) → π ↑i) ≃ᵐ ((i : { x // x ∈ s ∪ t }) → π ↑i) :=
  MeasurableEquiv.piFinsetUnion π hst
⊢ ∫⁻ (y : ((i : { x // x ∈ s }) → π ↑i) × ((j : { x // x ∈ t }) → π ↑j)),
      f
        (updateFinset x (s ∪ t)
          ((MeasurableEquiv.piFinsetUnion π hst) y)) ∂(Measure.pi fun i => μ ↑i).prod (Measure.pi fun j => μ ↑j) =
    ∫⁻ (y : (i : { x // x ∈ s }) → π ↑i),
      ∫⁻ (z : (j : { x // x ∈ t }) → π ↑j),
        f (updateFinset x (s ∪ t) (e (y, z))) ∂Measure.pi fun j => μ ↑j ∂Measure.pi fun i => μ ↑i

Tactic:
apply lintegral_prod

Result:
case hf
δ : Type u_1
π : δ → Type u_3
inst✝² : (x : δ) → MeasurableSpace (π x)
μ : (i : δ) → Measure (π i)
inst✝¹ : DecidableEq δ
s t : Finset δ
inst✝ : ∀ (i : δ), SigmaFinite (μ i)
f : ((i : δ) → π i) → ℝ≥0∞
hf : Measurable f
hst : Disjoint s t
x : (i : δ) → π i
e : ((i : { x // x ∈ s }) → π ↑i) × ((i : { x // x ∈ t }) → π ↑i) ≃ᵐ ((i : { x // x ∈ s ∪ t }) → π ↑i) :=
  MeasurableEquiv.piFinsetUnion π hst
⊢ AEMeasurable (fun z => f (updateFinset x (s ∪ t) ((MeasurableEquiv.piFinsetUnion π hst) z)))
    ((Measure.pi fun i => μ ↑i).prod (Measure.pi fun j => μ ↑j))

Proof state:
δ : Type u_1
π : δ → Type u_3
inst✝² : (x : δ) → MeasurableSpace (π x)
μ : (i : δ) → Measure (π i)
inst✝¹ : DecidableEq δ
s t : Finset δ
inst✝ : ∀ (i : δ), SigmaFinite (μ i)
f : ((i : δ) → π i) → ℝ≥0∞
hf : Measurable f
hst : Disjoint s t
x : (i : δ) → π i
e : ((i : { x // x ∈ s }) → π ↑i) × ((i : { x // x ∈ t }) → π ↑i) ≃ᵐ ((i : { x // x ∈ s ∪ t }) → π ↑i) :=
  MeasurableEquiv.piFinsetUnion π hst
⊢ (∫⁻ (y : (i : { x // x ∈ s ∪ t }) → π ↑i), f (updateFinset x (s ∪ t) y) ∂Measure.pi fun i' => μ ↑i') =
    ∫⁻ (y : ((i : { x // x ∈ s }) → π ↑i) × ((j : { x // x ∈ t }) → π ↑j)),
      f (updateFinset x (s ∪ t) (?m.23462 y)) ∂(Measure.pi fun i => μ ↑i).prod (Measure.pi fun j => μ ↑j)

Tactic:
rw [measurePreserving_piFinsetUnion hst μ |>.lintegral_map_equiv]

Result:
no goals

Proof state:
case hf
δ : Type u_1
π : δ → Type u_3
inst✝² : (x : δ) → MeasurableSpace (π x)
μ : (i : δ) → Measure (π i)
inst✝¹ : DecidableEq δ
s t : Finset δ
inst✝ : ∀ (i : δ), SigmaFinite (μ i)
f : ((i : δ) → π i) → ℝ≥0∞
hf : Measurable f
hst : Disjoint s t
x : (i : δ) → π i
e : ((i : { x // x ∈ s }) → π ↑i) × ((i : { x // x ∈ t }) → π ↑i) ≃ᵐ ((i : { x // x ∈ s ∪ t }) → π ↑i) :=
  MeasurableEquiv.piFinsetUnion π hst
⊢ AEMeasurable (fun z => f (updateFinset x (s ∪ t) ((MeasurableEquiv.piFinsetUnion π hst) z)))
    ((Measure.pi fun i => μ ↑i).prod (Measure.pi fun j => μ ↑j))

Tactic:
apply Measurable.aemeasurable

Result:
case hf.h
δ : Type u_1
π : δ → Type u_3
inst✝² : (x : δ) → MeasurableSpace (π x)
μ : (i : δ) → Measure (π i)
inst✝¹ : DecidableEq δ
s t : Finset δ
inst✝ : ∀ (i : δ), SigmaFinite (μ i)
f : ((i : δ) → π i) → ℝ≥0∞
hf : Measurable f
hst : Disjoint s t
x : (i : δ) → π i
e : ((i : { x // x ∈ s }) → π ↑i) × ((i : { x // x ∈ t }) → π ↑i) ≃ᵐ ((i : { x // x ∈ s ∪ t }) → π ↑i) :=
  MeasurableEquiv.piFinsetUnion π hst
⊢ Measurable fun z => f (updateFinset x (s ∪ t) ((MeasurableEquiv.piFinsetUnion π hst) z))

Proof state:
δ : Type u_1
π : δ → Type u_3
inst✝² : (x : δ) → MeasurableSpace (π x)
μ : (i : δ) → Measure (π i)
inst✝¹ : DecidableEq δ
s t : Finset δ
inst✝ : ∀ (i : δ), SigmaFinite (μ i)
f : ((i : δ) → π i) → ℝ≥0∞
hf : Measurable f
hst : Disjoint s t
x : (i : δ) → π i
e : ((i : { x // x ∈ s }) → π ↑i) × ((i : { x // x ∈ t }) → π ↑i) ≃ᵐ ((i : { x // x ∈ s ∪ t }) → π ↑i) :=
  MeasurableEquiv.piFinsetUnion π hst
⊢ (∫⁻ (y : (i : { x // x ∈ s }) → π ↑i),
      ∫⁻ (z : (j : { x // x ∈ t }) → π ↑j),
        f (updateFinset x (s ∪ t) (e (y, z))) ∂Measure.pi fun j => μ ↑j ∂Measure.pi fun i => μ ↑i) =
    (∫⋯∫⁻_s, ∫⋯∫⁻_t, f ∂μ ∂μ) x

Tactic:
simp_rw [lmarginal, updateFinset_updateFinset hst]

Result:
δ : Type u_1
π : δ → Type u_3
inst✝² : (x : δ) → MeasurableSpace (π x)
μ : (i : δ) → Measure (π i)
inst✝¹ : DecidableEq δ
s t : Finset δ
inst✝ : ∀ (i : δ), SigmaFinite (μ i)
f : ((i : δ) → π i) → ℝ≥0∞
hf : Measurable f
hst : Disjoint s t
x : (i : δ) → π i
e : ((i : { x // x ∈ s }) → π ↑i) × ((i : { x // x ∈ t }) → π ↑i) ≃ᵐ ((i : { x // x ∈ s ∪ t }) → π ↑i) :=
  MeasurableEquiv.piFinsetUnion π hst
⊢ (∫⁻ (y : (i : { x // x ∈ s }) → π ↑i),
      ∫⁻ (z : (j : { x // x ∈ t }) → π ↑j),
        f (updateFinset x (s ∪ t) (e (y, z))) ∂Measure.pi fun j => μ ↑j ∂Measure.pi fun i => μ ↑i) =
    ∫⁻ (y : (i : { x // x ∈ s }) → π ↑i),
      ∫⁻ (y_1 : (i : { x // x ∈ t }) → π ↑i),
        f (updateFinset x (s ∪ t) ((piFinsetUnion π hst) (y, y_1))) ∂Measure.pi fun j => μ ↑j ∂Measure.pi fun i => μ ↑i

Proof state:
δ : Type u_1
π : δ → Type u_3
inst✝² : (x : δ) → MeasurableSpace (π x)
μ : (i : δ) → Measure (π i)
inst✝¹ : DecidableEq δ
s t : Finset δ
inst✝ : ∀ (i : δ), SigmaFinite (μ i)
f : ((i : δ) → π i) → ℝ≥0∞
hf : Measurable f
hst : Disjoint s t
x : (i : δ) → π i
e : ((i : { x // x ∈ s }) → π ↑i) × ((i : { x // x ∈ t }) → π ↑i) ≃ᵐ ((i : { x // x ∈ s ∪ t }) → π ↑i) :=
  MeasurableEquiv.piFinsetUnion π hst
⊢ (∫⁻ (y : (i : { x // x ∈ s }) → π ↑i),
      ∫⁻ (z : (j : { x // x ∈ t }) → π ↑j),
        f (updateFinset x (s ∪ t) (e (y, z))) ∂Measure.pi fun j => μ ↑j ∂Measure.pi fun i => μ ↑i) =
    ∫⁻ (y : (i : { x // x ∈ s }) → π ↑i),
      ∫⁻ (y_1 : (i : { x // x ∈ t }) → π ↑i),
        f (updateFinset x (s ∪ t) ((piFinsetUnion π hst) (y, y_1))) ∂Measure.pi fun j => μ ↑j ∂Measure.pi fun i => μ ↑i

Tactic:
rfl

Result:
no goals

Proof state:
case h
δ : Type u_1
π : δ → Type u_3
inst✝² : (x : δ) → MeasurableSpace (π x)
μ : (i : δ) → Measure (π i)
inst✝¹ : DecidableEq δ
s t : Finset δ
inst✝ : ∀ (i : δ), SigmaFinite (μ i)
f : ((i : δ) → π i) → ℝ≥0∞
hf : Measurable f
hst : Disjoint s t
x : (i : δ) → π i
e : ((i : { x // x ∈ s }) → π ↑i) × ((i : { x // x ∈ t }) → π ↑i) ≃ᵐ ((i : { x // x ∈ s ∪ t }) → π ↑i) :=
  MeasurableEquiv.piFinsetUnion π hst
⊢ (∫⋯∫⁻_s ∪ t, f ∂μ) x = (∫⋯∫⁻_s, ∫⋯∫⁻_t, f ∂μ ∂μ) x

Tactic:
calc (∫⋯∫⁻_s ∪ t, f ∂μ) x
    = ∫⁻ (y : (i : ↥(s ∪ t)) → π i), f (updateFinset x (s ∪ t) y)
        ∂.pi fun i' : ↥(s ∪ t) ↦ μ i' := rfl
  _ = ∫⁻ (y : ((i : s) → π i) × ((j : t) → π j)), f (updateFinset x (s ∪ t) _)
        ∂(Measure.pi fun i : s ↦ μ i).prod (.pi fun j : t ↦ μ j) := by
      rw [measurePreserving_piFinsetUnion hst μ |>.lintegral_map_equiv]
  _ = ∫⁻ (y : (i : s) → π i), ∫⁻ (z : (j : t) → π j), f (updateFinset x (s ∪ t) (e (y, z)))
        ∂.pi fun j : t ↦ μ j ∂.pi fun i : s ↦ μ i := by
      apply lintegral_prod
      apply Measurable.aemeasurable
      exact hf.comp <| measurable_updateFinset.comp e.measurable
  _ = (∫⋯∫⁻_s, ∫⋯∫⁻_t, f ∂μ ∂μ) x := by
      simp_rw [lmarginal, updateFinset_updateFinset hst]
      rfl

Result:
no goals