awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 δ
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 :
  ∫⁻ (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
⊢ ∫⁻ (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:
simp [update_eq_updateFinset]

Premises used: Function.update_eq_updateFinset
-- 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 δ
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 (updateFinset (π := X) x {i} (uniqueElim (α := fun (i_1 : ↥{i}) ↦ X (↑i_1 : δ)) xᵢ)) ∂μ i

Tactic:
rfl
-- 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 δ
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 : δ)
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
⊢ lmarginal (X := X) μ {i} f x = ∫⁻ (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

Premises used: Inhabited.default, MeasureTheory.lmarginal, Singleton.singleton, Subtype.val
-- 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 : Finset δ
f g : ((i : δ) → X i) → ℝ≥0∞
hfg : f ≤ g
⊢ lmarginal (X := X) μ s f ≤ lmarginal (X := X) μ s g

Tactic:
fun _ => lintegral_mono fun _ => hfg _

Premises used: Function.updateFinset, MeasureTheory.lintegral_mono, MeasureTheory.lmarginal
-- 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
h : ∀ (x : (i : δ) → X i), lmarginal (X := X) μ (s ∪ t) f x = lmarginal (X := X) μ s (lmarginal (X := X) μ t f) x
⊢ lmarginal (X := X) μ (s ∪ t) f = lmarginal (X := X) μ s (lmarginal (X := X) μ t f)

Tactic:
ext1 x
-- 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
⊢ lmarginal (X := X) μ (s ∪ t) f x =
    ∫⁻ (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' : δ)

Tactic:
rfl

Premises used: MeasureTheory.lmarginal, rfl
-- 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
rw 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 : δ))
⊢ (∫⁻ (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:
rw [measurePreserving_piFinsetUnion hst μ |>.lintegral_map_equiv]

Premises used: MeasurableEquiv.piFinsetUnion, MeasureTheory.measurePreserving_piFinsetUnion, MeasureTheory.MeasurePreserving.lintegral_map_equiv
-- 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
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 : δ)))
⊢ ∫⁻ (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:
apply lintegral_prod

Premises used: MeasureTheory.lintegral_prod
-- 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
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))
⊢ 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 Measurable.aemeasurable

Premises used: Measurable.aemeasurable
-- 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
⊢ 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:
hf.comp <| measurable_updateFinset.comp e.measurable

Premises used: Measurable.comp, measurable_updateFinset, MeasurableEquiv.measurable
-- 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
⊢ 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:
exact hf.comp <| measurable_updateFinset.comp e.measurable

Premises used: Measurable.comp, measurable_updateFinset, MeasurableEquiv.measurable
-- 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
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 : δ)
⊢ (∫⁻ (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

Tactic:
simp_rw [lmarginal, updateFinset_updateFinset hst]

Premises used: Function.updateFinset_updateFinset, MeasureTheory.lmarginal
-- 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
⊢ (∫⁻ (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:
rfl
-- 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 δ
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)
rw₁ rw₂ : lmarginal (X := X) μ t (lmarginal (X := X) μ 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)

Tactic:
rw [Finset.union_comm, lmarginal_union μ f hf hst.symm]

Premises used: Finset.union_comm, MeasureTheory.lmarginal_union, Disjoint.symm
-- 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 : 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
rw₂ 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
⊢ lmarginal (X := X) μ (insert 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]

Premises used: Iff.mpr, Finset.insert_eq, MeasureTheory.lmarginal_union, MeasureTheory.lmarginal_singleton, Finset.disjoint_singleton_left
-- 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 : 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) μ s f x = ∫⁻ (xᵢ : X i), lmarginal (X := X) μ (s.erase i) f (update (β := X) x i xᵢ) ∂μ i

Tactic:
simpa [insert_erase hi] using lmarginal_insert _ hf (notMem_erase i s) x

Premises used: MeasureTheory.lmarginal_insert, Finset.notMem_erase, Finset.insert_erase
-- 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 : 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
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
rw₂ :
  lmarginal (X := X) μ s (lmarginal (X := X) μ {i} f) =
    lmarginal (X := X) μ s fun (x : (i : δ) → X i) ↦ ∫⁻ (xᵢ : X i), f (update (β := X) x i xᵢ) ∂μ i
rw₃ rw₄ :
  (lmarginal (X := X) μ s fun (x : (a : δ) → X a) ↦ ∫⁻ (xᵢ : X i), f (update (β := X) x i xᵢ) ∂μ i) =
    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

Tactic:
rw [Finset.insert_eq, Finset.union_comm,
    lmarginal_union (s := s) μ f hf (Finset.disjoint_singleton_right.mpr hi), lmarginal_singleton]

Premises used: Iff.mpr, Finset.insert_eq, Finset.union_comm, MeasureTheory.lmarginal_union, MeasureTheory.lmarginal_singleton, Finset.disjoint_singleton_right
-- 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 : Finset δ
inst_2 : ∀ (i : δ), SigmaFinite (μ i)
f : ((i : δ) → X i) → ℝ≥0∞
hf : Measurable f
i : δ
hi : i ∈ s
⊢ lmarginal (X := X) μ s f =
    lmarginal (X := X) μ (s.erase i) fun (x : (i : δ) → X i) ↦ ∫⁻ (xᵢ : X i), f (update (β := X) x i xᵢ) ∂μ i

Tactic:
simpa [insert_erase hi] using lmarginal_insert' _ hf (notMem_erase i s)

Premises used: Finset.notMem_erase, Finset.insert_erase, MeasureTheory.lmarginal_insert'
-- 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 δ
inst_2 : ∀ (i : δ), SigmaFinite (μ i)
inst_3 : Fintype δ
f : ((i : δ) → X i) → ℝ≥0∞
e : ↥Finset.univ ≃ δ := subtypeUnivEquiv (p := fun (j : δ) ↦ Membership.mem (γ := Finset δ) Finset.univ j) ⋯
h : ∀ (x : (i : δ) → X i), lmarginal (X := X) μ Finset.univ f x = ∫⁻ (x : (i : δ) → X i), f x ∂Measure.pi (α := X) μ
⊢ lmarginal (X := X) μ Finset.univ f = fun (x : (i : δ) → X i) ↦ ∫⁻ (x : (i : δ) → X i), f x ∂Measure.pi (α := X) μ

Tactic:
ext1 x
-- 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 δ
inst_2 : ∀ (i : δ), SigmaFinite (μ i)
inst_3 : Fintype δ
f : ((i : δ) → X i) → ℝ≥0∞
e : ↥Finset.univ ≃ δ := subtypeUnivEquiv (p := fun (j : δ) ↦ Membership.mem (γ := Finset δ) Finset.univ j) ⋯
x : (i : δ) → X i
h :
  (∫⁻ (y : (i : ↥Finset.univ) → X (↑i : δ)),
      f fun (i : δ) ↦
        if hi : Membership.mem (γ := Finset δ) Finset.univ i then
          y (Subtype.mk (p := fun (x : δ) ↦ Membership.mem (γ := Finset δ) Finset.univ x) i hi)
        else x i ∂Measure.pi (α := fun (i : ↥Finset.univ) ↦ X (↑i : δ)) fun (i : ↥Finset.univ) ↦ μ (↑i : δ)) =
    ∫⁻ (a : (b : ↥Finset.univ) → X ((e : (a : ↥Finset.univ) → δ) b)),
      f
        ((MeasurableEquiv.piCongrLeft X e :
            (a : (b : ↥Finset.univ) → X ((e : (a : ↥Finset.univ) → δ) b)) → (a : δ) → X a)
          a) ∂Measure.pi (α := fun (b : ↥Finset.univ) ↦ X ((e : (a : ↥Finset.univ) → δ) b)) fun (i' : ↥Finset.univ) ↦
        μ ((e : (a : ↥Finset.univ) → δ) i')
⊢ lmarginal (X := X) μ Finset.univ f x = ∫⁻ (x : (i : δ) → X i), f x ∂Measure.pi (α := X) μ

Tactic:
simp_rw [lmarginal, measurePreserving_piCongrLeft μ e |>.lintegral_map_equiv, updateFinset_def]

Premises used: MeasureTheory.measurePreserving_piCongrLeft, MeasurableEquiv.piCongrLeft, MeasureTheory.lmarginal, Function.updateFinset_def, MeasureTheory.MeasurePreserving.lintegral_map_equiv
-- 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 δ
inst_2 : ∀ (i : δ), SigmaFinite (μ i)
inst_3 : Fintype δ
f : ((i : δ) → X i) → ℝ≥0∞
e : ↥Finset.univ ≃ δ := subtypeUnivEquiv (p := fun (j : δ) ↦ Membership.mem (γ := Finset δ) Finset.univ j) ⋯
x : (i : δ) → X i
h :
  (∫⁻ (y : (i : ↥Finset.univ) → X (↑i : δ)),
      f fun (i : δ) ↦
        y
          (Subtype.mk (p := fun (x : δ) ↦ Membership.mem (γ := Finset δ) Finset.univ x) i
            ⋯) ∂Measure.pi (α := fun (i : ↥Finset.univ) ↦ X (↑i : δ)) fun (i : ↥Finset.univ) ↦ μ (↑i : δ)) =
    ∫⁻ (a : (b : ↥Finset.univ) → X ((e : (a : ↥Finset.univ) → δ) b)),
      f
        ((MeasurableEquiv.piCongrLeft X e :
            (a : (b : ↥Finset.univ) → X ((e : (a : ↥Finset.univ) → δ) b)) → (a : δ) → X a)
          a) ∂Measure.pi (α := fun (b : ↥Finset.univ) ↦ X ((e : (a : ↥Finset.univ) → δ) b)) fun (i' : ↥Finset.univ) ↦
        μ ((e : (a : ↥Finset.univ) → δ) i')
⊢ (∫⁻ (y : (i : ↥Finset.univ) → X (↑i : δ)),
      f fun (i : δ) ↦
        if hi : Membership.mem (γ := Finset δ) Finset.univ i then
          y (Subtype.mk (p := fun (x : δ) ↦ Membership.mem (γ := Finset δ) Finset.univ x) i hi)
        else x i ∂Measure.pi (α := fun (i : ↥Finset.univ) ↦ X (↑i : δ)) fun (i : ↥Finset.univ) ↦ μ (↑i : δ)) =
    ∫⁻ (a : (b : ↥Finset.univ) → X ((e : (a : ↥Finset.univ) → δ) b)),
      f
        ((MeasurableEquiv.piCongrLeft X e :
            (a : (b : ↥Finset.univ) → X ((e : (a : ↥Finset.univ) → δ) b)) → (a : δ) → X a)
          a) ∂Measure.pi (α := fun (b : ↥Finset.univ) ↦ X ((e : (a : ↥Finset.univ) → δ) b)) fun (i' : ↥Finset.univ) ↦
        μ ((e : (a : ↥Finset.univ) → δ) i')

Tactic:
simp
-- 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 δ
inst_2 : ∀ (i : δ), SigmaFinite (μ i)
inst_3 : Fintype δ
f : ((i : δ) → X i) → ℝ≥0∞
e : ↥Finset.univ ≃ δ := subtypeUnivEquiv (p := fun (j : δ) ↦ Membership.mem (γ := Finset δ) Finset.univ j) ⋯
x : (i : δ) → X i
⊢ (∫⁻ (y : (i : ↥Finset.univ) → X (↑i : δ)),
      f fun (i : δ) ↦
        y
          (Subtype.mk (p := fun (x : δ) ↦ Membership.mem (γ := Finset δ) Finset.univ x) i
            ⋯) ∂Measure.pi (α := fun (i : ↥Finset.univ) ↦ X (↑i : δ)) fun (i : ↥Finset.univ) ↦ μ (↑i : δ)) =
    ∫⁻ (a : (b : ↥Finset.univ) → X ((e : (a : ↥Finset.univ) → δ) b)),
      f
        ((MeasurableEquiv.piCongrLeft X e :
            (a : (b : ↥Finset.univ) → X ((e : (a : ↥Finset.univ) → δ) b)) → (a : δ) → X a)
          a) ∂Measure.pi (α := fun (b : ↥Finset.univ) ↦ X ((e : (a : ↥Finset.univ) → δ) b)) fun (i' : ↥Finset.univ) ↦
        μ ((e : (a : ↥Finset.univ) → δ) i')

Tactic:
rfl