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 δ
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
⊢ 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 (lmarginal (X := X) μ {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]
-- 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
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
⊢ 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 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
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 δ
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) ⋯
⊢ lmarginal (X := X) μ Finset.univ f = fun (x : (i : δ) → X i) ↦ ∫⁻ (x : (i : δ) → X i), f x ∂Measure.pi (α := X) μ
have h : ∀ (x : (i : δ) → X i), lmarginal (X := X) μ Finset.univ f x = ∫⁻ (x : (i : δ) → X i), f x ∂Measure.pi (α := 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 δ
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
⊢ lmarginal (X := X) μ Finset.univ f x = ∫⁻ (x : (i : δ) → X i), f x ∂Measure.pi (α := X) μ
have 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')
Tactic: simp_rw [lmarginal, measurePreserving_piCongrLeft μ e |>.lintegral_map_equiv, updateFinset_def]
-- 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)
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 : δ) ↦
        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')
have h : (∫⁻ (y : (i : ↥Finset.univ) → X (↑i : δ)),
    f fun (i : δ) ↦
      y
        (Subtype.mk (p := fun (x : δ) ↦ Membership.mem (γ := Finset δ) Finset.univ x) i
          sorry) ∂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
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Marginal (hypothesis)
Goal:
δ : Type u_1
δ' : Type u_2
X : δ → Type u_3
inst : (i : δ) → MeasurableSpace (X i)
μ : (i : δ) → Measure (X i)
inst_1 : DecidableEq δ
inst_2 : ∀ (i : δ), SigmaFinite (μ i)
inst_3 : DecidableEq δ'
e : δ' → δ
he : Injective e
s : Finset δ'
f : ((i : δ') → X (e i)) → ℝ≥0∞
hf : Measurable f
x : (i : δ) → X i
⊢ lmarginal (X := X) μ (Finset.image e s)
      (f ∘ fun (x : (i : δ) → X i) ↦ dcomp (β := fun {x : δ'} ↦ δ) (φ := fun {x : δ'} ↦ X) (fun {x_1 : δ'} ↦ x) e) x =
    lmarginal (X := fun (i : δ') ↦ X (e i))
      (dcomp (β := fun {x : δ'} ↦ δ) (φ := fun {x : δ'} (y : δ) ↦ Measure (X y)) (fun {x : δ'} ↦ μ) e) s f
      (dcomp (β := fun {x : δ'} ↦ δ) (φ := fun {x : δ'} ↦ X) (fun {x_1 : δ'} ↦ x) e)
have h : Measurable (β := (x : δ') → X (e x)) fun (x : (i : δ) → X i) ↦
  dcomp (β := fun {x : δ'} ↦ δ) (φ := fun {x : δ'} ↦ X) (fun {x_1 : δ'} ↦ x) e
Tactic: have h : Measurable ((· ∘' e) : (∀ i, X i) → _) :=
    measurable_pi_iff.mpr <| fun i ↦ measurable_pi_apply (e i)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Marginal (goal)
Goal:
δ : Type u_1
δ' : Type u_2
X : δ → Type u_3
inst : (i : δ) → MeasurableSpace (X i)
μ : (i : δ) → Measure (X i)
inst_1 : DecidableEq δ
inst_2 : ∀ (i : δ), SigmaFinite (μ i)
inst_3 : DecidableEq δ'
e : δ' → δ
he : Injective e
f : ((i : δ') → X (e i)) → ℝ≥0∞
hf : Measurable f
h :
  Measurable (β := (x : δ') → X (e x)) fun (x : (i : δ) → X i) ↦
    dcomp (β := fun {x : δ'} ↦ δ) (φ := fun {x : δ'} ↦ X) (fun {x_1 : δ'} ↦ x) e
a : δ'
s : Finset δ'
hi : a ∉ s
ih :
  ∀ (x : (i : δ) → X i),
    lmarginal (X := X) μ (Finset.image e s)
        (f ∘ fun (x : (i : δ) → X i) ↦ dcomp (β := fun {x : δ'} ↦ δ) (φ := fun {x : δ'} ↦ X) (fun {x_1 : δ'} ↦ x) e) x =
      lmarginal (X := fun (i : δ') ↦ X (e i))
        (dcomp (β := fun {x : δ'} ↦ δ) (φ := fun {x : δ'} (y : δ) ↦ Measure (X y)) (fun {x : δ'} ↦ μ) e) s f
        (dcomp (β := fun {x : δ'} ↦ δ) (φ := fun {x : δ'} ↦ X) (fun {x_1 : δ'} ↦ x) e)
x : (i : δ) → X i
⊢ lmarginal (X := X) μ (Finset.image e (insert a s))
      (f ∘ fun (x : (i : δ) → X i) ↦ dcomp (β := fun {x : δ'} ↦ δ) (φ := fun {x : δ'} ↦ X) (fun {x_1 : δ'} ↦ x) e) x =
    lmarginal (X := fun (i : δ') ↦ X (e i))
      (dcomp (β := fun {x : δ'} ↦ δ) (φ := fun {x : δ'} (y : δ) ↦ Measure (X y)) (fun {x : δ'} ↦ μ) e) (insert a s) f
      (dcomp (β := fun {x : δ'} ↦ δ) (φ := fun {x : δ'} ↦ X) (fun {x_1 : δ'} ↦ x) e)
have insert : ∫⁻ (xᵢ : X (e a)),
    lmarginal (X := X) μ (Finset.image e s)
      (f ∘ fun (x : (i : δ) → X i) ↦ dcomp (β := fun {x : δ'} ↦ δ) (φ := fun {x : δ'} ↦ X) (fun {x_1 : δ'} ↦ x) e)
      (update (β := X) x (e a) xᵢ) ∂μ (e a) =
  ∫⁻ (xᵢ : X (e a)),
    lmarginal (X := fun (i : δ') ↦ X (e i))
      (dcomp (β := fun {x : δ'} ↦ δ) (φ := fun {x : δ'} (y : δ) ↦ Measure (X y)) (fun {x : δ'} ↦ μ) e) s f
      (update (β := fun (i : δ') ↦ X (e i))
        (dcomp (β := fun {x : δ'} ↦ δ) (φ := fun {x : δ'} ↦ X) (fun {x_1 : δ'} ↦ x) e) a
        xᵢ) ∂dcomp (β := fun {x : δ'} ↦ δ) (φ := fun {x : δ'} (y : δ) ↦ Measure (X y)) (fun {x : δ'} ↦ μ) e a
Tactic: rw [image_insert, lmarginal_insert _ (hf.comp h) (he.mem_finset_image.not.mpr hi),
      lmarginal_insert _ hf hi]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Marginal (goal)
Goal:
δ : Type u_1
δ' : Type u_2
X : δ → Type u_3
inst : (i : δ) → MeasurableSpace (X i)
μ : (i : δ) → Measure (X i)
inst_1 : DecidableEq δ
inst_2 : ∀ (i : δ), SigmaFinite (μ i)
inst_3 : DecidableEq δ'
e : δ' → δ
he : Injective e
f : ((i : δ') → X (e i)) → ℝ≥0∞
hf : Measurable f
h :
  Measurable (β := (x : δ') → X (e x)) fun (x : (i : δ) → X i) ↦
    dcomp (β := fun {x : δ'} ↦ δ) (φ := fun {x : δ'} ↦ X) (fun {x_1 : δ'} ↦ x) e
a : δ'
s : Finset δ'
hi : a ∉ s
ih :
  ∀ (x : (i : δ) → X i),
    lmarginal (X := X) μ (Finset.image e s)
        (f ∘ fun (x : (i : δ) → X i) ↦ dcomp (β := fun {x : δ'} ↦ δ) (φ := fun {x : δ'} ↦ X) (fun {x_1 : δ'} ↦ x) e) x =
      lmarginal (X := fun (i : δ') ↦ X (e i))
        (dcomp (β := fun {x : δ'} ↦ δ) (φ := fun {x : δ'} (y : δ) ↦ Measure (X y)) (fun {x : δ'} ↦ μ) e) s f
        (dcomp (β := fun {x : δ'} ↦ δ) (φ := fun {x : δ'} ↦ X) (fun {x_1 : δ'} ↦ x) e)
x : (i : δ) → X i
⊢ ∫⁻ (xᵢ : X (e a)),
      lmarginal (X := X) μ (Finset.image e s)
        (f ∘ fun (x : (i : δ) → X i) ↦ dcomp (β := fun {x : δ'} ↦ δ) (φ := fun {x : δ'} ↦ X) (fun {x_1 : δ'} ↦ x) e)
        (update (β := X) x (e a) xᵢ) ∂μ (e a) =
    ∫⁻ (xᵢ : X (e a)),
      lmarginal (X := fun (i : δ') ↦ X (e i))
        (dcomp (β := fun {x : δ'} ↦ δ) (φ := fun {x : δ'} (y : δ) ↦ Measure (X y)) (fun {x : δ'} ↦ μ) e) s f
        (update (β := fun (i : δ') ↦ X (e i))
          (dcomp (β := fun {x : δ'} ↦ δ) (φ := fun {x : δ'} ↦ X) (fun {x_1 : δ'} ↦ x) e) a
          xᵢ) ∂dcomp (β := fun {x : δ'} ↦ δ) (φ := fun {x : δ'} (y : δ) ↦ Measure (X y)) (fun {x : δ'} ↦ μ) e a
have insert : ∫⁻ (xᵢ : X (e a)),
    lmarginal (X := fun (i : δ') ↦ X (e i))
      (dcomp (β := fun {x : δ'} ↦ δ) (φ := fun {x : δ'} (y : δ) ↦ Measure (X y)) (fun {x : δ'} ↦ μ) e) s f
      (dcomp (β := fun {x : δ'} ↦ δ) (φ := fun {x : δ'} ↦ X) (fun {x_1 : δ'} ↦ update (β := X) x (e a) xᵢ) e) ∂μ (e a) =
  ∫⁻ (xᵢ : X (e a)),
    lmarginal (X := fun (i : δ') ↦ X (e i))
      (dcomp (β := fun {x : δ'} ↦ δ) (φ := fun {x : δ'} (y : δ) ↦ Measure (X y)) (fun {x : δ'} ↦ μ) e) s f
      (update (β := fun (i : δ') ↦ X (e i))
        (dcomp (β := fun {x : δ'} ↦ δ) (φ := fun {x : δ'} ↦ X) (fun {x_1 : δ'} ↦ x) e) a
        xᵢ) ∂dcomp (β := fun {x : δ'} ↦ δ) (φ := fun {x : δ'} (y : δ) ↦ Measure (X y)) (fun {x : δ'} ↦ μ) e a
Tactic: simp_rw [ih, ← update_comp_eq_of_injective' x he]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Marginal (goal)
Goal:
δ : Type u_1
δ' : Type u_2
X : δ → Type u_3
inst : (i : δ) → MeasurableSpace (X i)
μ : (i : δ) → Measure (X i)
inst_1 : DecidableEq δ
inst_2 : ∀ (i : δ), SigmaFinite (μ i)
inst_3 : DecidableEq δ'
e : δ' → δ
he : Injective e
s : Finset δ'
f : ((i : δ') → X (e i)) → ℝ≥0∞
hf : Measurable f
x : (i : δ) → X i
h :
  Measurable (β := (x : δ') → X (e x)) fun (x : (i : δ) → X i) ↦
    dcomp (β := fun {x : δ'} ↦ δ) (φ := fun {x : δ'} ↦ X) (fun {x_1 : δ'} ↦ x) e
⊢ lmarginal (X := X) μ (Finset.image e s)
      (f ∘ fun (x : (i : δ) → X i) ↦ dcomp (β := fun {x : δ'} ↦ δ) (φ := fun {x : δ'} ↦ X) (fun {x_1 : δ'} ↦ x) e) x =
    lmarginal (X := fun (i : δ') ↦ X (e i))
      (dcomp (β := fun {x : δ'} ↦ δ) (φ := fun {x : δ'} (y : δ) ↦ Measure (X y)) (fun {x : δ'} ↦ μ) e) s f
      (dcomp (β := fun {x : δ'} ↦ δ) (φ := fun {x : δ'} ↦ X) (fun {x_1 : δ'} ↦ x) e)
have empty : ∀ (x : (i : δ) → X i),
  lmarginal (X := X) μ (Finset.image e ∅)
      (f ∘ fun (x : (i : δ) → X i) ↦ dcomp (β := fun {x : δ'} ↦ δ) (φ := fun {x : δ'} ↦ X) (fun {x_1 : δ'} ↦ x) e) x =
    lmarginal (X := fun (i : δ') ↦ X (e i))
      (dcomp (β := fun {x : δ'} ↦ δ) (φ := fun {x : δ'} (y : δ) ↦ Measure (X y)) (fun {x : δ'} ↦ μ) e) ∅ f
      (dcomp (β := fun {x : δ'} ↦ δ) (φ := fun {x : δ'} ↦ X) (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]
Cleared hypotheses: s, x
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Marginal (goal)
Goal:
δ : Type u_1
δ' : Type u_2
X : δ → Type u_3
inst : (i : δ) → MeasurableSpace (X i)
μ : (i : δ) → Measure (X i)
inst_1 : DecidableEq δ
inst_2 : ∀ (i : δ), SigmaFinite (μ i)
inst_3 : DecidableEq δ'
e : δ' → δ
he : Injective e
s : Finset δ'
f : ((i : δ') → X (e i)) → ℝ≥0∞
hf : Measurable f
x : (i : δ) → X i
h :
  Measurable (β := (x : δ') → X (e x)) fun (x : (i : δ) → X i) ↦
    dcomp (β := fun {x : δ'} ↦ δ) (φ := fun {x : δ'} ↦ X) (fun {x_1 : δ'} ↦ x) e
empty :
  ∀ (x : (i : δ) → X i),
    lmarginal (X := X) μ (Finset.image e ∅)
        (f ∘ fun (x : (i : δ) → X i) ↦ dcomp (β := fun {x : δ'} ↦ δ) (φ := fun {x : δ'} ↦ X) (fun {x_1 : δ'} ↦ x) e) x =
      lmarginal (X := fun (i : δ') ↦ X (e i))
        (dcomp (β := fun {x : δ'} ↦ δ) (φ := fun {x : δ'} (y : δ) ↦ Measure (X y)) (fun {x : δ'} ↦ μ) e) ∅ f
        (dcomp (β := fun {x : δ'} ↦ δ) (φ := fun {x : δ'} ↦ X) (fun {x_1 : δ'} ↦ x) e)
⊢ lmarginal (X := X) μ (Finset.image e s)
      (f ∘ fun (x : (i : δ) → X i) ↦ dcomp (β := fun {x : δ'} ↦ δ) (φ := fun {x : δ'} ↦ X) (fun {x_1 : δ'} ↦ x) e) x =
    lmarginal (X := fun (i : δ') ↦ X (e i))
      (dcomp (β := fun {x : δ'} ↦ δ) (φ := fun {x : δ'} (y : δ) ↦ Measure (X y)) (fun {x : δ'} ↦ μ) e) s f
      (dcomp (β := fun {x : δ'} ↦ δ) (φ := fun {x : δ'} ↦ X) (fun {x_1 : δ'} ↦ x) e)
have insert : ∀ (a : δ') (s : Finset δ') (hi : a ∉ s)
  (ih :
    ∀ (x : (i : δ) → X i),
      lmarginal (X := X) μ (Finset.image e s)
          (f ∘ fun (x : (i : δ) → X i) ↦ dcomp (β := fun {x : δ'} ↦ δ) (φ := fun {x : δ'} ↦ X) (fun {x_1 : δ'} ↦ x) e)
          x =
        lmarginal (X := fun (i : δ') ↦ X (e i))
          (dcomp (β := fun {x : δ'} ↦ δ) (φ := fun {x : δ'} (y : δ) ↦ Measure (X y)) (fun {x : δ'} ↦ μ) e) s f
          (dcomp (β := fun {x : δ'} ↦ δ) (φ := fun {x : δ'} ↦ X) (fun {x_1 : δ'} ↦ x) e))
  (x : (i : δ) → X i),
  lmarginal (X := X) μ (Finset.image e (insert a s))
      (f ∘ fun (x : (i : δ) → X i) ↦ dcomp (β := fun {x : δ'} ↦ δ) (φ := fun {x : δ'} ↦ X) (fun {x_1 : δ'} ↦ x) e) x =
    lmarginal (X := fun (i : δ') ↦ X (e i))
      (dcomp (β := fun {x : δ'} ↦ δ) (φ := fun {x : δ'} (y : δ) ↦ Measure (X y)) (fun {x : δ'} ↦ μ) e) (insert a s) f
      (dcomp (β := fun {x : δ'} ↦ δ) (φ := fun {x : δ'} ↦ X) (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]
Cleared hypotheses: s, 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_1 : Finset δ
inst_2 : ∀ (i : δ), SigmaFinite (μ i)
i : δ
f : ((i : δ) → X i) → ℝ≥0∞
hf : Measurable f
y : X i
i' : δ
s : Finset δ
hi' : i' ∉ s
ih :
  ∀ (hi : i ∉ s) (x : (i : δ) → X i),
    lmarginal (X := X) μ s f (update (β := X) x i y) =
      lmarginal (X := X) μ s (f ∘ fun (x : (i : δ) → X i) ↦ update (β := X) x i y) x
hi : i ∉ insert i' s
x : (i : δ) → X i
⊢ lmarginal (X := X) μ (insert i' s) f (update (β := X) x i y) =
    lmarginal (X := X) μ (insert i' s) (f ∘ fun (x : (i : δ) → X i) ↦ update (β := X) x i y) x
have insert : ∫⁻ (xᵢ : X i'), lmarginal (X := X) μ s f (update (β := X) (update (β := X) x i y) i' xᵢ) ∂μ i' =
  ∫⁻ (xᵢ : X i'),
    lmarginal (X := X) μ s (f ∘ fun (x : (a : δ) → X a) ↦ update (β := X) x i y) (update (β := X) x i' xᵢ) ∂μ i'
Tactic: rw [lmarginal_insert _ hf hi', lmarginal_insert _ (hf.comp measurable_update_left) hi']
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Marginal (hypothesis)
Goal:
δ : Type u_1
X : δ → Type u_3
inst : (i : δ) → MeasurableSpace (X i)
μ : (i : δ) → Measure (X i)
inst_1 : DecidableEq δ
s_1 : Finset δ
inst_2 : ∀ (i : δ), SigmaFinite (μ i)
i : δ
f : ((i : δ) → X i) → ℝ≥0∞
hf : Measurable f
y : X i
i' : δ
s : Finset δ
hi' : i' ∉ s
ih :
  ∀ (hi : i ∉ s) (x : (i : δ) → X i),
    lmarginal (X := X) μ s f (update (β := X) x i y) =
      lmarginal (X := X) μ s (f ∘ fun (x : (i : δ) → X i) ↦ update (β := X) x i y) x
hi : i ∉ insert i' s
x : (i : δ) → X i
⊢ ∫⁻ (xᵢ : X i'), lmarginal (X := X) μ s f (update (β := X) (update (β := X) x i y) i' xᵢ) ∂μ i' =
    ∫⁻ (xᵢ : X i'),
      lmarginal (X := X) μ s (f ∘ fun (x : (a : δ) → X a) ↦ update (β := X) x i y) (update (β := X) x i' xᵢ) ∂μ i'
have hii' : i ≠ i'
Tactic: have hii' : i ≠ i' := mt (by rintro rfl; exact mem_insert_self i s) hi
-- 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_1 : Finset δ
inst_2 : ∀ (i : δ), SigmaFinite (μ i)
i : δ
f : ((i : δ) → X i) → ℝ≥0∞
hf : Measurable f
y : X i
i' : δ
s : Finset δ
hi' : i' ∉ s
ih :
  ∀ (hi : i ∉ s) (x : (i : δ) → X i),
    lmarginal (X := X) μ s f (update (β := X) x i y) =
      lmarginal (X := X) μ s (f ∘ fun (x : (i : δ) → X i) ↦ update (β := X) x i y) x
hi : i ∉ insert i' s
x : (i : δ) → X i
hii' : i ≠ i'
⊢ ∫⁻ (xᵢ : X i'), lmarginal (X := X) μ s f (update (β := X) (update (β := X) x i y) i' xᵢ) ∂μ i' =
    ∫⁻ (xᵢ : X i'),
      lmarginal (X := X) μ s (f ∘ fun (x : (a : δ) → X a) ↦ update (β := X) x i y) (update (β := X) x i' xᵢ) ∂μ i'
have insert : ∫⁻ (xᵢ : X i'), lmarginal (X := X) μ s f (update (β := X) (update (β := X) x i' xᵢ) i y) ∂μ i' =
  ∫⁻ (xᵢ : X i'),
    lmarginal (X := X) μ s (f ∘ fun (x : (a : δ) → X a) ↦ update (β := X) x i y) (update (β := X) x i' xᵢ) ∂μ i'
Tactic: simp_rw [update_comm hii', ih (mt Finset.mem_insert_of_mem hi)]
-- 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)
i : δ
f : ((i : δ) → X i) → ℝ≥0∞
hf : Measurable f
hi : i ∉ s
x : (i : δ) → X i
y : X i
⊢ lmarginal (X := X) μ s f (update (β := X) x i y) =
    lmarginal (X := X) μ s (f ∘ fun (x : (i : δ) → X i) ↦ update (β := X) x i y) x
have empty : ∀ (hi : i ∉ ∅) (x : (i : δ) → X i),
  lmarginal (X := X) μ ∅ f (update (β := X) x i y) =
    lmarginal (X := X) μ ∅ (f ∘ fun (x : (i : δ) → X i) ↦ update (β := X) x i y) x
Tactic: induction s using Finset.induction generalizing x with
  | empty => simp
  | insert i' s hi' ih =>
    rw [lmarginal_insert _ hf hi', lmarginal_insert _ (hf.comp measurable_update_left) hi']
    have hii' : i ≠ i' := mt (by rintro rfl; exact mem_insert_self i s) hi
    simp_rw [update_comm hii', ih (mt Finset.mem_insert_of_mem hi)]
Cleared hypotheses: hi, 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 : Finset δ
inst_2 : ∀ (i : δ), SigmaFinite (μ i)
i : δ
f : ((i : δ) → X i) → ℝ≥0∞
hf : Measurable f
hi : i ∉ s
x : (i : δ) → X i
y : X i
empty :
  ∀ (hi : i ∉ ∅) (x : (i : δ) → X i),
    lmarginal (X := X) μ ∅ f (update (β := X) x i y) =
      lmarginal (X := X) μ ∅ (f ∘ fun (x : (i : δ) → X i) ↦ update (β := X) x i y) x
⊢ lmarginal (X := X) μ s f (update (β := X) x i y) =
    lmarginal (X := X) μ s (f ∘ fun (x : (i : δ) → X i) ↦ update (β := X) x i y) x
have insert : ∀ (i' : δ) (s : Finset δ) (hi' : i' ∉ s)
  (ih :
    ∀ (hi : i ∉ s) (x : (i : δ) → X i),
      lmarginal (X := X) μ s f (update (β := X) x i y) =
        lmarginal (X := X) μ s (f ∘ fun (x : (i : δ) → X i) ↦ update (β := X) x i y) x)
  (hi : i ∉ insert i' s) (x : (i : δ) → X i),
  lmarginal (X := X) μ (insert i' s) f (update (β := X) x i y) =
    lmarginal (X := X) μ (insert i' s) (f ∘ fun (x : (i : δ) → X i) ↦ update (β := X) x i y) x
Tactic: induction s using Finset.induction generalizing x with
  | empty => simp
  | insert i' s hi' ih =>
    rw [lmarginal_insert _ hf hi', lmarginal_insert _ (hf.comp measurable_update_left) hi']
    have hii' : i ≠ i' := mt (by rintro rfl; exact mem_insert_self i s) hi
    simp_rw [update_comm hii', ih (mt Finset.mem_insert_of_mem hi)]
Cleared hypotheses: hi, 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 g : ((i : δ) → X i) → ℝ≥0∞
hst : s ⊆ t
hf : Measurable f
hg : Measurable g
hfg : lmarginal (X := X) μ s f = lmarginal (X := X) μ s g
⊢ lmarginal (X := X) μ t f = lmarginal (X := X) μ t g
have rw : lmarginal (X := X) μ (s ∪ t \ s) f = lmarginal (X := X) μ (s ∪ t \ s) g
Tactic: rw [← union_sdiff_of_subset hst, lmarginal_union' μ f hf disjoint_sdiff,
    lmarginal_union' μ g hg disjoint_sdiff, hfg]
-- 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 g : ((i : δ) → X i) → ℝ≥0∞
hst : s ⊆ t
hf : Measurable f
hg : Measurable g
hfg : lmarginal (X := X) μ s f = lmarginal (X := X) μ s g
rw : lmarginal (X := X) μ (s ∪ t \ s) f = lmarginal (X := X) μ (s ∪ t \ s) g
⊢ lmarginal (X := X) μ t f = lmarginal (X := X) μ t g
have rw₁ : lmarginal (X := X) μ (t \ s) (lmarginal (X := X) μ s f) = lmarginal (X := X) μ (s ∪ t \ s) g
Tactic: rw [← union_sdiff_of_subset hst, lmarginal_union' μ f hf disjoint_sdiff,
    lmarginal_union' μ g hg disjoint_sdiff, hfg]
-- 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 g : ((i : δ) → X i) → ℝ≥0∞
hst : s ⊆ t
hf : Measurable f
hg : Measurable g
hfg : lmarginal (X := X) μ s f = lmarginal (X := X) μ s g
rw : lmarginal (X := X) μ (s ∪ t \ s) f = lmarginal (X := X) μ (s ∪ t \ s) g
rw₁ : lmarginal (X := X) μ (t \ s) (lmarginal (X := X) μ s f) = lmarginal (X := X) μ (s ∪ t \ s) g
⊢ lmarginal (X := X) μ t f = lmarginal (X := X) μ t g
have rw₂ : lmarginal (X := X) μ (t \ s) (lmarginal (X := X) μ s f) = lmarginal (X := X) μ (t \ s) (lmarginal (X := X) μ s g)
Tactic: rw [← union_sdiff_of_subset hst, lmarginal_union' μ f hf disjoint_sdiff,
    lmarginal_union' μ g hg disjoint_sdiff, hfg]