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 δ
inst_2 : ∀ (i : δ), SigmaFinite (μ i)
inst_3 : Fintype δ
f : ((i : δ) → X i) → ℝ≥0∞
x : (i : δ) → X i
⊢ ∫⁻ (x : (i : δ) → X i), f x ∂Measure.pi (α := X) μ = lmarginal (X := X) μ Finset.univ f x

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Integral.Marginal
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
⊢ 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)
-- Module: Mathlib.MeasureTheory.Integral.Marginal
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
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:
simp
-- Module: Mathlib.MeasureTheory.Integral.Marginal
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
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
⊢ lmarginal (X := X) μ (Finset.image e (Insert.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.insert a s) f (dcomp (β := fun {x : δ'} ↦ δ) (φ := fun {x : δ'} ↦ X) (fun {x_1 : δ'} ↦ x) e)

Tactic:
rw [image_insert, lmarginal_insert _ (hf.comp h) (he.mem_finset_image.not.mpr hi),
      lmarginal_insert _ hf hi]

Premises used: Iff.mpr, Measurable.comp, MeasureTheory.lmarginal_insert, Iff.not, Function.Injective.mem_finset_image, Finset.image_insert
-- Module: Mathlib.MeasureTheory.Integral.Marginal
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
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
⊢ ∫⁻ (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:
simp_rw [ih, ← update_comp_eq_of_injective' x he]

Premises used: Function.update_comp_eq_of_injective'
-- Module: Mathlib.MeasureTheory.Integral.Marginal
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)
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.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.insert a s) 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)

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]

Premises used: Insert.insert, Function.update_comp_eq_of_injective', Finset.image_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 δ
s : Finset δ
inst_2 : ∀ (i : δ), SigmaFinite (μ i)
i : δ
f : ((i : δ) → X i) → ℝ≥0∞
hf : Measurable f
y : X i
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:
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 δ
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.insert i' s
x : (i : δ) → X i
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'
⊢ lmarginal (X := X) μ (Insert.insert i' s) f (update (β := X) x i y) =
    lmarginal (X := X) μ (Insert.insert i' s) (f ∘ fun (x : (i : δ) → X i) ↦ update (β := X) x i y) x

Tactic:
rw [lmarginal_insert _ hf hi', lmarginal_insert _ (hf.comp measurable_update_left) hi']

Premises used: Measurable.comp, MeasureTheory.lmarginal_insert, measurable_update_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_1 : Finset δ
inst_2 : ∀ (i : δ), SigmaFinite (μ i)
i : δ
f : ((i : δ) → X i) → ℝ≥0∞
hf : Measurable f
y : X i
s : Finset δ
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
x : (i : δ) → X i
hi' : i ∉ s
hi : i ∉ insert i s
⊢ i ∈ insert i s

Tactic:
mem_insert_self i s

Premises used: Finset.mem_insert_self
-- 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_1 : Finset δ
inst_2 : ∀ (i : δ), SigmaFinite (μ i)
i : δ
f : ((i : δ) → X i) → ℝ≥0∞
hf : Measurable f
y : X i
s : Finset δ
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
x : (i : δ) → X i
hi' : i ∉ s
hi : i ∉ insert i s
⊢ i ∈ insert i s

Tactic:
exact mem_insert_self i s

Premises used: Finset.mem_insert_self
-- 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_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
⊢ i ≠ i'

Tactic:
have hii' : i ≠ i' := mt (by rintro rfl; exact mem_insert_self i s) hi
-- 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_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.insert i' s
x : (i : δ) → X i
hii' : i ≠ i'
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'
⊢ ∫⁻ (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:
simp_rw [update_comm hii', ih (mt Finset.mem_insert_of_mem hi)]

Premises used: mt, Function.update_comm, Finset.mem_insert_of_mem
-- 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)
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
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.insert i' s) (x : (i : δ) → X i),
    lmarginal (X := X) μ (Insert.insert i' s) f (update (β := X) x i y) =
      lmarginal (X := X) μ (Insert.insert i' s) (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

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)]

Premises used: Insert.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 δ
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
rw₂ : lmarginal (X := X) μ (t \ s) (lmarginal (X := X) μ s f) = lmarginal (X := X) μ (t \ s) (lmarginal (X := X) μ s g)
rw₃ rw₄ :
  lmarginal (X := X) μ (t \ s) (lmarginal (X := X) μ s g) = lmarginal (X := X) μ (t \ s) (lmarginal (X := X) μ s g)
⊢ lmarginal (X := X) μ t f = lmarginal (X := X) μ t g

Tactic:
rw [← union_sdiff_of_subset hst, lmarginal_union' μ f hf disjoint_sdiff,
    lmarginal_union' μ g hg disjoint_sdiff, hfg]

Premises used: Finset.disjoint_sdiff, Finset.union_sdiff_of_subset, MeasureTheory.lmarginal_union'
-- 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 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) μ (t \ s) (lmarginal (X := X) μ s f) ≤ lmarginal (X := X) μ (t \ s) (lmarginal (X := X) μ s g)
⊢ lmarginal (X := X) μ t f ≤ lmarginal (X := X) μ t g

Tactic:
rw [← union_sdiff_of_subset hst, lmarginal_union' μ f hf disjoint_sdiff,
    lmarginal_union' μ g hg disjoint_sdiff]

Premises used: Finset.disjoint_sdiff, Finset.union_sdiff_of_subset, MeasureTheory.lmarginal_union'
-- 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 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 \ s) (lmarginal (X := X) μ s f) ≤ lmarginal (X := X) μ (t \ s) (lmarginal (X := X) μ s g)

Tactic:
lmarginal_mono hfg

Premises used: MeasureTheory.lmarginal_mono
-- 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 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 \ s) (lmarginal (X := X) μ s f) ≤ lmarginal (X := X) μ (t \ s) (lmarginal (X := X) μ s g)

Tactic:
exact lmarginal_mono hfg

Premises used: MeasureTheory.lmarginal_mono
-- 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 δ
s : Finset δ
f g : ((i : δ) → X i) → ℝ≥0∞
hf : Measurable f
hg : Measurable g
hfg : lmarginal (X := X) μ s f = lmarginal (X := X) μ s g
inl :
  ∀ (h : IsEmpty ((i : δ) → X i)),
    ∫⁻ (x : (i : δ) → X i), f x ∂Measure.pi (α := X) μ = ∫⁻ (x : (i : δ) → X i), g x ∂Measure.pi (α := X) μ
inr :
  ∀ (x : (i : δ) → X i),
    ∫⁻ (x : (i : δ) → X i), f x ∂Measure.pi (α := X) μ = ∫⁻ (x : (i : δ) → X i), g x ∂Measure.pi (α := X) μ
⊢ ∫⁻ (x : (i : δ) → X i), f x ∂Measure.pi (α := X) μ = ∫⁻ (x : (i : δ) → X i), g x ∂Measure.pi (α := X) μ

Tactic:
rcases isEmpty_or_nonempty (∀ i, X i) with h | ⟨⟨x⟩⟩

Premises used: isEmpty_or_nonempty
-- 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 δ
s : Finset δ
f g : ((i : δ) → X i) → ℝ≥0∞
hf : Measurable f
hg : Measurable g
hfg : lmarginal (X := X) μ s f = lmarginal (X := X) μ s g
h : IsEmpty ((i : δ) → X i)
⊢ ∫⁻ (x : (i : δ) → X i), f x ∂Measure.pi (α := X) μ = ∫⁻ (x : (i : δ) → X i), g x ∂Measure.pi (α := X) μ

Tactic:
simp_rw [lintegral_of_isEmpty]

Premises used: MeasureTheory.lintegral_of_isEmpty
-- 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 δ
s : Finset δ
f g : ((i : δ) → X i) → ℝ≥0∞
hf : Measurable f
hg : Measurable g
hfg : lmarginal (X := X) μ s f = lmarginal (X := X) μ s g
x : (i : δ) → X i
inr : lmarginal (X := X) μ Finset.univ f x = lmarginal (X := X) μ Finset.univ g x
⊢ ∫⁻ (x : (i : δ) → X i), f x ∂Measure.pi (α := X) μ = ∫⁻ (x : (i : δ) → X i), g x ∂Measure.pi (α := X) μ

Tactic:
simp_rw [lintegral_eq_lmarginal_univ x, lmarginal_eq_of_subset (Finset.subset_univ s) hf hg hfg]

Premises used: MeasureTheory.lintegral_eq_lmarginal_univ, MeasureTheory.lmarginal_eq_of_subset, Finset.subset_univ
-- 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 δ
s : Finset δ
f g : ((i : δ) → X i) → ℝ≥0∞
hf : Measurable f
hg : Measurable g
hfg : lmarginal (X := X) μ s f ≤ lmarginal (X := X) μ s g
inl :
  ∀ (h : IsEmpty ((i : δ) → X i)),
    ∫⁻ (x : (i : δ) → X i), f x ∂Measure.pi (α := X) μ ≤ ∫⁻ (x : (i : δ) → X i), g x ∂Measure.pi (α := X) μ
inr :
  ∀ (x : (i : δ) → X i),
    ∫⁻ (x : (i : δ) → X i), f x ∂Measure.pi (α := X) μ ≤ ∫⁻ (x : (i : δ) → X i), g x ∂Measure.pi (α := X) μ
⊢ ∫⁻ (x : (i : δ) → X i), f x ∂Measure.pi (α := X) μ ≤ ∫⁻ (x : (i : δ) → X i), g x ∂Measure.pi (α := X) μ

Tactic:
rcases isEmpty_or_nonempty (∀ i, X i) with h | ⟨⟨x⟩⟩

Premises used: isEmpty_or_nonempty
-- 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 δ
s : Finset δ
f g : ((i : δ) → X i) → ℝ≥0∞
hf : Measurable f
hg : Measurable g
hfg : lmarginal (X := X) μ s f ≤ lmarginal (X := X) μ s g
h : IsEmpty ((i : δ) → X i)
inl : LE.le (α := ℝ≥0∞) 0 0
⊢ ∫⁻ (x : (i : δ) → X i), f x ∂Measure.pi (α := X) μ ≤ ∫⁻ (x : (i : δ) → X i), g x ∂Measure.pi (α := X) μ

Tactic:
simp_rw [lintegral_of_isEmpty, le_rfl]

Premises used: le_rfl, MeasureTheory.lintegral_of_isEmpty
-- 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 δ
s : Finset δ
f g : ((i : δ) → X i) → ℝ≥0∞
hf : Measurable f
hg : Measurable g
hfg : lmarginal (X := X) μ s f ≤ lmarginal (X := X) μ s g
x : (i : δ) → X i
inr : lmarginal (X := X) μ Finset.univ f x ≤ lmarginal (X := X) μ Finset.univ g x
⊢ ∫⁻ (x : (i : δ) → X i), f x ∂Measure.pi (α := X) μ ≤ ∫⁻ (x : (i : δ) → X i), g x ∂Measure.pi (α := X) μ

Tactic:
simp_rw [lintegral_eq_lmarginal_univ x, lmarginal_le_of_subset (Finset.subset_univ s) hf hg hfg x]

Premises used: MeasureTheory.lintegral_eq_lmarginal_univ, MeasureTheory.lmarginal_le_of_subset, Finset.subset_univ
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.HolderConjugate q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_norm : ∫⁻ (a : α), f a ^ p ∂μ = 1
hg_norm : ∫⁻ (a : α), g a ^ q ∂μ = 1
⊢ ∫⁻ (a : α), (f * g) a ∂μ ≤ ∫⁻ (a : α), f a ^ p / ENNReal.ofReal p + g a ^ q / ENNReal.ofReal q ∂μ

Tactic:
lintegral_mono fun a => young_inequality (f a) (g a) hpq

Premises used: MeasureTheory.lintegral_mono, ENNReal.young_inequality
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.HolderConjugate q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_norm : ∫⁻ (a : α), f a ^ p ∂μ = 1
hg_norm : ∫⁻ (a : α), g a ^ q ∂μ = 1
simp : ∫⁻ (a : α), f a ^ p * (ENNReal.ofReal p)⁻¹ + g a ^ q * (ENNReal.ofReal q)⁻¹ ∂μ = 1
⊢ ∫⁻ (a : α), f a ^ p / ENNReal.ofReal p + g a ^ q / ENNReal.ofReal q ∂μ = 1

Tactic:
simp only [div_eq_mul_inv]

Premises used: div_eq_mul_inv