awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Marginal (goal)
Goal:
δ : Type u_1
X : δ → Type u_3
inst : (i : δ) → MeasurableSpace (X i)
μ : (i : δ) → Measure (X i)
inst_1 : DecidableEq δ
f : ((i : δ) → X i) → ℝ≥0∞
i : δ
α : Type u_1 := ↥{i}
e : X (↑default : δ) ≃ᵐ ((i_1 : α) → X (↑i_1 : δ)) :=
  MeasurableEquiv.symm (MeasurableEquiv.piUnique fun (j : α) ↦ X (↑j : δ))
x : (i : δ) → X i
⊢ lmarginal (X := X) μ {i} f x =
    ∫⁻ (y : X (↑default : δ)),
      f (updateFinset (π := X) x {i} ((e : (a : X (↑default : δ)) → (i_1 : α) → X (↑i_1 : δ)) y)) ∂μ (↑default : δ)
have simp_rw : (∫⁻ (y : (i_1 : ↥{i}) → X (↑i_1 : δ)),
    f
      (updateFinset (π := X) x {i}
        y) ∂Measure.pi (α := fun (i_1 : ↥{i}) ↦ X (↑i_1 : δ)) fun (i_1 : ↥{i}) ↦ μ (↑i_1 : δ)) =
  ∫⁻ (y : X (↑default : δ)),
    f (updateFinset (π := X) x {i} ((e : (a : X (↑default : δ)) → (i_1 : α) → X (↑i_1 : δ)) y)) ∂μ (↑default : δ)
Tactic: simp_rw [lmarginal,
          measurePreserving_piUnique (fun j : ({i} : Finset δ) ↦ μ j) |>.symm _
            |>.lintegral_map_equiv, e, α]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Marginal (goal)
Goal:
δ : Type u_1
X : δ → Type u_3
inst : (i : δ) → MeasurableSpace (X i)
μ : (i : δ) → Measure (X i)
inst_1 : DecidableEq δ
f : ((i : δ) → X i) → ℝ≥0∞
i : δ
α : Type u_1 := ↥{i}
e : X (↑default : δ) ≃ᵐ ((i_1 : α) → X (↑i_1 : δ)) :=
  MeasurableEquiv.symm (MeasurableEquiv.piUnique fun (j : α) ↦ X (↑j : δ))
x : (i : δ) → X i
simp_rw :
  (∫⁻ (y : (i_1 : ↥{i}) → X (↑i_1 : δ)),
      f
        (updateFinset (π := X) x {i}
          y) ∂Measure.pi (α := fun (i_1 : ↥{i}) ↦ X (↑i_1 : δ)) fun (i_1 : ↥{i}) ↦ μ (↑i_1 : δ)) =
    ∫⁻ (y : X (↑default : δ)),
      f (updateFinset (π := X) x {i} ((e : (a : X (↑default : δ)) → (i_1 : α) → X (↑i_1 : δ)) y)) ∂μ (↑default : δ)
⊢ lmarginal (X := X) μ {i} f x =
    ∫⁻ (y : X (↑default : δ)),
      f (updateFinset (π := X) x {i} ((e : (a : X (↑default : δ)) → (i_1 : α) → X (↑i_1 : δ)) y)) ∂μ (↑default : δ)
have simp_rw₁ : ∫⁻ (a : X (↑default : δ)),
    f
      (updateFinset (π := X) x {i}
        (((MeasurableEquiv.symm (MeasurableEquiv.piUnique fun (j : ↥{i}) ↦ X (↑j : δ)) :
              X (↑default : δ) ≃ᵐ ((i_1 : ↥{i}) → X (↑i_1 : δ))) :
            (a : X (↑default : δ)) → (i_1 : ↥{i}) → X (↑i_1 : δ))
          a)) ∂μ (↑default : δ) =
  ∫⁻ (y : X (↑default : δ)),
    f (updateFinset (π := X) x {i} ((e : (a : X (↑default : δ)) → (i_1 : α) → X (↑i_1 : δ)) y)) ∂μ (↑default : δ)
Tactic: simp_rw [lmarginal,
          measurePreserving_piUnique (fun j : ({i} : Finset δ) ↦ μ j) |>.symm _
            |>.lintegral_map_equiv, e, α]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Marginal (goal)
Goal:
δ : Type u_1
X : δ → Type u_3
inst : (i : δ) → MeasurableSpace (X i)
μ : (i : δ) → Measure (X i)
inst_1 : DecidableEq δ
f : ((i : δ) → X i) → ℝ≥0∞
i : δ
α : Type u_1 := ↥{i}
e : X (↑default : δ) ≃ᵐ ((i_1 : α) → X (↑i_1 : δ)) :=
  MeasurableEquiv.symm (MeasurableEquiv.piUnique fun (j : α) ↦ X (↑j : δ))
x : (i : δ) → X i
⊢ ∫⁻ (y : X (↑default : δ)),
      f (updateFinset (π := X) x {i} ((e : (a : X (↑default : δ)) → (i_1 : α) → X (↑i_1 : δ)) y)) ∂μ (↑default : δ) =
    ∫⁻ (xᵢ : X i), f (update (β := X) x i xᵢ) ∂μ i
have simp : ∫⁻ (y : X (↑default : δ)),
    f (updateFinset (π := X) x {i} ((e : (a : X (↑default : δ)) → (i_1 : α) → X (↑i_1 : δ)) y)) ∂μ (↑default : δ) =
  ∫⁻ (xᵢ : X i), f (updateFinset (π := X) x {i} (uniqueElim (α := fun (i_1 : ↥{i}) ↦ X (↑i_1 : δ)) xᵢ)) ∂μ i
Tactic: simp [update_eq_updateFinset]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Marginal (goal)
Goal:
δ : Type u_1
X : δ → Type u_3
inst : (i : δ) → MeasurableSpace (X i)
μ : (i : δ) → Measure (X i)
inst_1 : DecidableEq δ
f : ((i : δ) → X i) → ℝ≥0∞
i : δ
α : Type u_1 := ↥{i}
e : X (↑default : δ) ≃ᵐ ((i_1 : α) → X (↑i_1 : δ)) :=
  MeasurableEquiv.symm (MeasurableEquiv.piUnique fun (j : α) ↦ X (↑j : δ))
x : (i : δ) → X i
⊢ lmarginal (X := X) μ {i} f x = ∫⁻ (xᵢ : X i), f (update (β := X) x i xᵢ) ∂μ i
have calc : lmarginal (X := X) μ {i} f x =
  ∫⁻ (y : X (↑default : δ)),
    f (updateFinset (π := X) x {i} ((e : (a : X (↑default : δ)) → (i_1 : α) → X (↑i_1 : δ)) y)) ∂μ (↑default : δ)
Tactic: calc (∫⋯∫⁻_{i}, f ∂μ) x
      = ∫⁻ (y : X (default : α)), f (updateFinset x {i} (e y)) ∂μ (default : α) := by
        simp_rw [lmarginal,
          measurePreserving_piUnique (fun j : ({i} : Finset δ) ↦ μ j) |>.symm _
            |>.lintegral_map_equiv, e, α]
    _ = ∫⁻ xᵢ, f (Function.update x i xᵢ) ∂μ i := by simp [update_eq_updateFinset]; rfl
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Marginal (goal)
Goal:
δ : Type u_1
X : δ → Type u_3
inst : (i : δ) → MeasurableSpace (X i)
μ : (i : δ) → Measure (X i)
inst_1 : DecidableEq δ
f : ((i : δ) → X i) → ℝ≥0∞
i : δ
α : Type u_1 := ↥{i}
e : X (↑default : δ) ≃ᵐ ((i_1 : α) → X (↑i_1 : δ)) :=
  MeasurableEquiv.symm (MeasurableEquiv.piUnique fun (j : α) ↦ X (↑j : δ))
x : (i : δ) → X i
calc :
  lmarginal (X := X) μ {i} f x =
    ∫⁻ (y : X (↑default : δ)),
      f (updateFinset (π := X) x {i} ((e : (a : X (↑default : δ)) → (i_1 : α) → X (↑i_1 : δ)) y)) ∂μ (↑default : δ)
⊢ lmarginal (X := X) μ {i} f x = ∫⁻ (xᵢ : X i), f (update (β := X) x i xᵢ) ∂μ i
have calc₁ : ∫⁻ (y : X (↑default : δ)),
    f (updateFinset (π := X) x {i} ((e : (a : X (↑default : δ)) → (i_1 : α) → X (↑i_1 : δ)) y)) ∂μ (↑default : δ) =
  ∫⁻ (xᵢ : X i), f (update (β := X) x i xᵢ) ∂μ i
Tactic: calc (∫⋯∫⁻_{i}, f ∂μ) x
      = ∫⁻ (y : X (default : α)), f (updateFinset x {i} (e y)) ∂μ (default : α) := by
        simp_rw [lmarginal,
          measurePreserving_piUnique (fun j : ({i} : Finset δ) ↦ μ j) |>.symm _
            |>.lintegral_map_equiv, e, α]
    _ = ∫⁻ xᵢ, f (Function.update x i xᵢ) ∂μ i := by simp [update_eq_updateFinset]; rfl
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Marginal (goal)
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
⊢ lmarginal (X := X) μ (s ∪ t) f = lmarginal (X := X) μ s (lmarginal (X := X) μ t f)
have h : ∀ (x : (i : δ) → X i), lmarginal (X := X) μ (s ∪ t) f x = lmarginal (X := X) μ s (lmarginal (X := X) μ t f) x
Tactic: ext1 x
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Marginal (goal)
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
⊢ (∫⁻ (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 : δ))
have rw : ∫⁻ (a : ((i : ↥s) → X (↑i : δ)) × ((i : ↥t) → X (↑i : δ))),
    f
      (updateFinset (π := X) x (s ∪ t)
        ((MeasurableEquiv.piFinsetUnion X hst :
            (a : ((i : ↥s) → X (↑i : δ)) × ((i : ↥t) → X (↑i : δ))) → (i : ↥(s ∪ t)) → X (↑i : δ))
          a)) ∂Measure.prod (Measure.pi (α := fun (i : ↥s) ↦ X (↑i : δ)) fun (i : ↥s) ↦ μ (↑i : δ))
      (Measure.pi (α := fun (i : ↥t) ↦ X (↑i : δ)) fun (i : ↥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 : δ))
Tactic: rw [measurePreserving_piFinsetUnion hst μ |>.lintegral_map_equiv]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Marginal (goal)
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
⊢ ∫⁻ (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 : δ)
have hf₁ : AEMeasurable (β := ℝ≥0∞) (_m := Prod.instMeasurableSpace)
  (fun (z : ((i : ↥s) → X (↑i : δ)) × ((i : ↥t) → X (↑i : δ))) ↦
    f
      (updateFinset (π := X) x (s ∪ t)
        ((MeasurableEquiv.piFinsetUnion X hst :
            (a : ((i : ↥s) → X (↑i : δ)) × ((i : ↥t) → X (↑i : δ))) → (i : ↥(s ∪ t)) → X (↑i : δ))
          z)))
  (Measure.prod (Measure.pi (α := fun (i : ↥s) ↦ X (↑i : δ)) fun (i : ↥s) ↦ μ (↑i : δ))
    (Measure.pi (α := fun (j : ↥t) ↦ X (↑j : δ)) fun (j : ↥t) ↦ μ (↑j : δ)))
Tactic: apply lintegral_prod
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Marginal (goal)
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
⊢ AEMeasurable (β := ℝ≥0∞) (_m := Prod.instMeasurableSpace)
    (fun (z : ((i : ↥s) → X (↑i : δ)) × ((i : ↥t) → X (↑i : δ))) ↦
      f
        (updateFinset (π := X) x (s ∪ t)
          ((MeasurableEquiv.piFinsetUnion X hst :
              (a : ((i : ↥s) → X (↑i : δ)) × ((i : ↥t) → X (↑i : δ))) → (i : ↥(s ∪ t)) → X (↑i : δ))
            z)))
    (Measure.prod (Measure.pi (α := fun (i : ↥s) ↦ X (↑i : δ)) fun (i : ↥s) ↦ μ (↑i : δ))
      (Measure.pi (α := fun (j : ↥t) ↦ X (↑j : δ)) fun (j : ↥t) ↦ μ (↑j : δ)))
have hf₁ : Measurable (β := ℝ≥0∞) fun (z : ((i : ↥s) → X (↑i : δ)) × ((i : ↥t) → X (↑i : δ))) ↦
  f
    (updateFinset (π := X) x (s ∪ t)
      ((MeasurableEquiv.piFinsetUnion X hst :
          (a : ((i : ↥s) → X (↑i : δ)) × ((i : ↥t) → X (↑i : δ))) → (i : ↥(s ∪ t)) → X (↑i : δ))
        z))
Tactic: apply Measurable.aemeasurable
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Marginal (goal)
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
⊢ (∫⁻ (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
have simp_rw : (∫⁻ (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 : δ)) =
  ∫⁻ (y : (i : ↥s) → X (↑i : δ)),
    ∫⁻ (y_1 : (i : ↥t) → X (↑i : δ)),
      f
        (updateFinset (π := X) x (s ∪ t)
          ((piFinsetUnion X hst : (a : ((i : ↥s) → X (↑i : δ)) × ((i : ↥t) → X (↑i : δ))) → (i : ↥(s ∪ t)) → X (↑i : δ))
            (y,
              y_1))) ∂Measure.pi (α := fun (j : ↥t) ↦ X (↑j : δ)) fun (j : ↥t) ↦
        μ (↑j : δ) ∂Measure.pi (α := fun (i : ↥s) ↦ X (↑i : δ)) fun (i : ↥s) ↦ μ (↑i : δ)
Tactic: simp_rw [lmarginal, updateFinset_updateFinset hst]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Marginal (goal)
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
⊢ lmarginal (X := X) μ (s ∪ t) f x = lmarginal (X := X) μ s (lmarginal (X := X) μ t f) x
have 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 : δ))
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
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Marginal (goal)
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 : δ))
⊢ lmarginal (X := X) μ (s ∪ t) f x = lmarginal (X := X) μ s (lmarginal (X := X) μ t f) x
have 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 : δ)
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
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Marginal (goal)
Goal:
δ : Type u_1
X : δ → Type u_3
inst : (i : δ) → MeasurableSpace (X i)
μ : (i : δ) → Measure (X i)
inst_1 : DecidableEq δ
inst_2 : ∀ (i : δ), SigmaFinite (μ i)
f : ((i : δ) → X i) → ℝ≥0∞
hf : Measurable f
s t : Finset δ
hst : Disjoint s t
⊢ lmarginal (X := X) μ (s ∪ t) f = lmarginal (X := X) μ t (lmarginal (X := X) μ s f)
have rw : lmarginal (X := X) μ (t ∪ s) f = lmarginal (X := X) μ t (lmarginal (X := X) μ s f)
Tactic: rw [Finset.union_comm, lmarginal_union μ f hf hst.symm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Marginal (goal)
Goal:
δ : Type u_1
X : δ → Type u_3
inst : (i : δ) → MeasurableSpace (X i)
μ : (i : δ) → Measure (X i)
inst_1 : DecidableEq δ
inst_2 : ∀ (i : δ), SigmaFinite (μ i)
f : ((i : δ) → X i) → ℝ≥0∞
hf : Measurable f
s t : Finset δ
hst : Disjoint s t
rw : lmarginal (X := X) μ (t ∪ s) f = lmarginal (X := X) μ t (lmarginal (X := X) μ s f)
⊢ lmarginal (X := X) μ (s ∪ t) f = lmarginal (X := X) μ t (lmarginal (X := X) μ s f)
have rw₁ : lmarginal (X := X) μ t (lmarginal (X := X) μ s f) = lmarginal (X := X) μ t (lmarginal (X := X) μ s f)
Tactic: rw [Finset.union_comm, lmarginal_union μ f hf hst.symm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Marginal (goal)
Goal:
δ : Type u_1
X : δ → Type u_3
inst : (i : δ) → MeasurableSpace (X i)
μ : (i : δ) → Measure (X i)
inst_1 : DecidableEq δ
s : Finset δ
inst_2 : ∀ (i : δ), SigmaFinite (μ i)
f : ((i : δ) → X i) → ℝ≥0∞
hf : Measurable f
i : δ
hi : i ∉ s
x : (i : δ) → X i
⊢ lmarginal (X := X) μ (insert i s) f x = ∫⁻ (xᵢ : X i), lmarginal (X := X) μ s f (update (β := X) x i xᵢ) ∂μ i
have rw : lmarginal (X := X) μ ({i} ∪ s) f x = ∫⁻ (xᵢ : X i), lmarginal (X := X) μ s f (update (β := X) x i xᵢ) ∂μ i
Tactic: rw [Finset.insert_eq, lmarginal_union μ f hf (Finset.disjoint_singleton_left.mpr hi),
    lmarginal_singleton]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Marginal (goal)
Goal:
δ : Type u_1
X : δ → Type u_3
inst : (i : δ) → MeasurableSpace (X i)
μ : (i : δ) → Measure (X i)
inst_1 : DecidableEq δ
s : Finset δ
inst_2 : ∀ (i : δ), SigmaFinite (μ i)
f : ((i : δ) → X i) → ℝ≥0∞
hf : Measurable f
i : δ
hi : i ∉ s
x : (i : δ) → X i
rw : lmarginal (X := X) μ ({i} ∪ s) f x = ∫⁻ (xᵢ : X i), lmarginal (X := X) μ s f (update (β := X) x i xᵢ) ∂μ i
⊢ lmarginal (X := X) μ (insert i s) f x = ∫⁻ (xᵢ : X i), lmarginal (X := X) μ s f (update (β := X) x i xᵢ) ∂μ i
have rw₁ : lmarginal (X := X) μ {i} (lmarginal (X := X) μ s f) x =
  ∫⁻ (xᵢ : X i), lmarginal (X := X) μ s f (update (β := X) x i xᵢ) ∂μ i
Tactic: rw [Finset.insert_eq, lmarginal_union μ f hf (Finset.disjoint_singleton_left.mpr hi),
    lmarginal_singleton]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Marginal (goal)
Goal:
δ : Type u_1
X : δ → Type u_3
inst : (i : δ) → MeasurableSpace (X i)
μ : (i : δ) → Measure (X i)
inst_1 : DecidableEq δ
s : Finset δ
inst_2 : ∀ (i : δ), SigmaFinite (μ i)
f : ((i : δ) → X i) → ℝ≥0∞
hf : Measurable f
i : δ
hi : i ∉ s
x : (i : δ) → X i
rw : lmarginal (X := X) μ ({i} ∪ s) f x = ∫⁻ (xᵢ : X i), lmarginal (X := X) μ s f (update (β := X) x i xᵢ) ∂μ i
rw₁ :
  lmarginal (X := X) μ {i} (lmarginal (X := X) μ s f) x =
    ∫⁻ (xᵢ : X i), lmarginal (X := X) μ s f (update (β := X) x i xᵢ) ∂μ i
⊢ lmarginal (X := X) μ (insert i s) f x = ∫⁻ (xᵢ : X i), lmarginal (X := X) μ s f (update (β := X) x i xᵢ) ∂μ i
have rw₂ : (fun (x : (a : δ) → X a) ↦ ∫⁻ (xᵢ : X i), lmarginal (X := X) μ s f (update (β := X) x i xᵢ) ∂μ i) x =
  ∫⁻ (xᵢ : X i), lmarginal (X := X) μ s f (update (β := X) x i xᵢ) ∂μ i
Tactic: rw [Finset.insert_eq, lmarginal_union μ f hf (Finset.disjoint_singleton_left.mpr hi),
    lmarginal_singleton]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Marginal (goal)
Goal:
δ : Type u_1
X : δ → Type u_3
inst : (i : δ) → MeasurableSpace (X i)
μ : (i : δ) → Measure (X i)
inst_1 : DecidableEq δ
s : Finset δ
inst_2 : ∀ (i : δ), SigmaFinite (μ i)
f : ((i : δ) → X i) → ℝ≥0∞
hf : Measurable f
i : δ
hi : i ∉ s
⊢ lmarginal (X := X) μ (insert i s) f =
    lmarginal (X := X) μ s fun (x : (i : δ) → X i) ↦ ∫⁻ (xᵢ : X i), f (update (β := X) x i xᵢ) ∂μ i
have rw : lmarginal (X := X) μ ({i} ∪ s) f =
  lmarginal (X := X) μ s fun (x : (i : δ) → X i) ↦ ∫⁻ (xᵢ : X i), f (update (β := X) x i xᵢ) ∂μ i
Tactic: rw [Finset.insert_eq, Finset.union_comm,
    lmarginal_union (s := s) μ f hf (Finset.disjoint_singleton_right.mpr hi), lmarginal_singleton]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Marginal (goal)
Goal:
δ : Type u_1
X : δ → Type u_3
inst : (i : δ) → MeasurableSpace (X i)
μ : (i : δ) → Measure (X i)
inst_1 : DecidableEq δ
s : Finset δ
inst_2 : ∀ (i : δ), SigmaFinite (μ i)
f : ((i : δ) → X i) → ℝ≥0∞
hf : Measurable f
i : δ
hi : i ∉ s
rw :
  lmarginal (X := X) μ ({i} ∪ s) f =
    lmarginal (X := X) μ s fun (x : (i : δ) → X i) ↦ ∫⁻ (xᵢ : X i), f (update (β := X) x i xᵢ) ∂μ i
⊢ lmarginal (X := X) μ (insert i s) f =
    lmarginal (X := X) μ s fun (x : (i : δ) → X i) ↦ ∫⁻ (xᵢ : X i), f (update (β := X) x i xᵢ) ∂μ i
have rw₁ : lmarginal (X := X) μ (s ∪ {i}) f =
  lmarginal (X := X) μ s fun (x : (i : δ) → X i) ↦ ∫⁻ (xᵢ : X i), f (update (β := X) x i xᵢ) ∂μ i
Tactic: rw [Finset.insert_eq, Finset.union_comm,
    lmarginal_union (s := s) μ f hf (Finset.disjoint_singleton_right.mpr hi), lmarginal_singleton]