-- Module: Mathlib.MeasureTheory.Integral.Marginal
Goal:
δ : Type u_1
X : δ → Type u_3
inst : (i : δ) → MeasurableSpace (X i)
μ : (i : δ) → Measure (X i)
inst_1 : DecidableEq δ
s t : Finset δ
inst_2 : ∀ (i : δ), SigmaFinite (μ i)
f : ((i : δ) → X i) → ℝ≥0∞
hf : Measurable f
hst : Disjoint s t
x : (i : δ) → X i
e : ((i : ↥s) → X (↑i : δ)) × ((i : ↥t) → X (↑i : δ)) ≃ᵐ ((i : ↥(s ∪ t)) → X (↑i : δ)) :=
  MeasurableEquiv.piFinsetUnion X hst
calc :
  (∫⁻ (y : (i : ↥(s ∪ t)) → X (↑i : δ)),
      f
        (updateFinset (π := X) x (s ∪ t)
          y) ∂Measure.pi (α := fun (i' : ↥(s ∪ t)) ↦ X (↑i' : δ)) fun (i' : ↥(s ∪ t)) ↦ μ (↑i' : δ)) =
    ∫⁻ (y : ((i : ↥s) → X (↑i : δ)) × ((j : ↥t) → X (↑j : δ))),
      f
        (updateFinset (π := X) x (s ∪ t)
          ((MeasurableEquiv.piFinsetUnion X hst :
              (a : ((i : ↥s) → X (↑i : δ)) × ((i : ↥t) → X (↑i : δ))) → (i : ↥(s ∪ t)) → X (↑i : δ))
            y)) ∂Measure.prod (Measure.pi (α := fun (i : ↥s) ↦ X (↑i : δ)) fun (i : ↥s) ↦ μ (↑i : δ))
        (Measure.pi (α := fun (j : ↥t) ↦ X (↑j : δ)) fun (j : ↥t) ↦ μ (↑j : δ))
calc₁ :
  ∫⁻ (y : ((i : ↥s) → X (↑i : δ)) × ((j : ↥t) → X (↑j : δ))),
      f
        (updateFinset (π := X) x (s ∪ t)
          ((MeasurableEquiv.piFinsetUnion X hst :
              (a : ((i : ↥s) → X (↑i : δ)) × ((i : ↥t) → X (↑i : δ))) → (i : ↥(s ∪ t)) → X (↑i : δ))
            y)) ∂Measure.prod (Measure.pi (α := fun (i : ↥s) ↦ X (↑i : δ)) fun (i : ↥s) ↦ μ (↑i : δ))
        (Measure.pi (α := fun (j : ↥t) ↦ X (↑j : δ)) fun (j : ↥t) ↦ μ (↑j : δ)) =
    ∫⁻ (y : (i : ↥s) → X (↑i : δ)),
      ∫⁻ (z : (j : ↥t) → X (↑j : δ)),
        f
          (updateFinset (π := X) x (s ∪ t)
            ((e : (a : ((i : ↥s) → X (↑i : δ)) × ((i : ↥t) → X (↑i : δ))) → (i : ↥(s ∪ t)) → X (↑i : δ))
              (y,
                z))) ∂Measure.pi (α := fun (j : ↥t) ↦ X (↑j : δ)) fun (j : ↥t) ↦
          μ (↑j : δ) ∂Measure.pi (α := fun (i : ↥s) ↦ X (↑i : δ)) fun (i : ↥s) ↦ μ (↑i : δ)
calc₂ :
  (∫⁻ (y : (i : ↥s) → X (↑i : δ)),
      ∫⁻ (z : (j : ↥t) → X (↑j : δ)),
        f
          (updateFinset (π := X) x (s ∪ t)
            ((e : (a : ((i : ↥s) → X (↑i : δ)) × ((i : ↥t) → X (↑i : δ))) → (i : ↥(s ∪ t)) → X (↑i : δ))
              (y,
                z))) ∂Measure.pi (α := fun (j : ↥t) ↦ X (↑j : δ)) fun (j : ↥t) ↦
          μ (↑j : δ) ∂Measure.pi (α := fun (i : ↥s) ↦ X (↑i : δ)) fun (i : ↥s) ↦ μ (↑i : δ)) =
    lmarginal (X := X) μ s (lmarginal (X := X) μ t f) x
⊢ lmarginal (X := X) μ (s ∪ t) f x = lmarginal (X := X) μ s (lmarginal (X := X) μ t f) x

Tactic:
calc (∫⋯∫⁻_s ∪ t, f ∂μ) x
      = ∫⁻ (y : (i : ↥(s ∪ t)) → X i), f (updateFinset x (s ∪ t) y)
          ∂.pi fun i' : ↥(s ∪ t) ↦ μ i' := rfl
    _ = ∫⁻ (y : ((i : s) → X i) × ((j : t) → X 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) → X i), ∫⁻ (z : (j : t) → X 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

Premises used: Function.updateFinset, MeasureTheory.Measure.prod, MeasureTheory.lmarginal, MeasureTheory.Measure.pi, Union.union, Subtype.val, rfl