awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.LebesgueNormedSpace
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : SecondCountableTopology E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
f : α → ℝ≥0
hf : Measurable f
g : α → E
mp :
  AEMeasurable g (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)) →
    AEMeasurable.{u_1, u_2} (β := E) (fun (x : α) ↦ (↑(f x) : ℝ) • g x) μ
mpr :
  AEMeasurable.{u_1, u_2} (β := E) (fun (x : α) ↦ (↑(f x) : ℝ) • g x) μ →
    AEMeasurable g (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞))
⊢ AEMeasurable g (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)) ↔
    AEMeasurable.{u_1, u_2} (β := E) (fun (x : α) ↦ (↑(f x) : ℝ) • g x) μ

Tactic:
constructor
-- Module: Mathlib.MeasureTheory.Integral.LebesgueNormedSpace
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : SecondCountableTopology E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : Measurable g'
hg' : g =ᶠ[ae (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞))] g'
⊢ MeasurableSet.{u_1} (α := α) {x : α | f x ≠ 0}

Tactic:
have A : MeasurableSet { x : α | f x ≠ 0 } := (hf (measurableSet_singleton 0)).compl
-- Module: Mathlib.MeasureTheory.Integral.LebesgueNormedSpace
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : SecondCountableTopology E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : Measurable g'
hg' : g =ᶠ[ae (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞))] g'
A : MeasurableSet.{u_1} (α := α) {x : α | f x ≠ 0}
⊢ AEMeasurable.{u_1, u_2} (β := E) (fun (x : α) ↦ (↑(f x) : ℝ) • g x) μ

Tactic:
⟨fun x => (f x : ℝ) • g' x, hf.coe_nnreal_real.smul g'meas, ?_⟩

Premises used: AEMeasurable, Measurable.coe_nnreal_real, And.intro, Measurable.smul, Exists.intro, HSMul.hSMul, NNReal.toReal
-- Module: Mathlib.MeasureTheory.Integral.LebesgueNormedSpace
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : SecondCountableTopology E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : Measurable g'
hg' : g =ᶠ[ae (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞))] g'
A : MeasurableSet.{u_1} (α := α) {x : α | f x ≠ 0}
mp : EventuallyEq.{u_1, u_2} (β := E) (ae μ) (fun (x : α) ↦ (↑(f x) : ℝ) • g x) fun (x : α) ↦ (↑(f x) : ℝ) • g' x
⊢ AEMeasurable.{u_1, u_2} (β := E) (fun (x : α) ↦ (↑(f x) : ℝ) • g x) μ

Tactic:
refine ⟨fun x => (f x : ℝ) • g' x, hf.coe_nnreal_real.smul g'meas, ?_⟩
-- Module: Mathlib.MeasureTheory.Integral.LebesgueNormedSpace
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : SecondCountableTopology E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : Measurable g'
hg' : g =ᶠ[ae (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞))] g'
A : MeasurableSet.{u_1} (α := α) {x : α | f x ≠ 0}
mp :
  ∀ᵐ (x : α) ∂μ.restrict {x : α | f x ≠ 0},
    Eq.{u_2 + 1} (α := E) ((fun (x : α) ↦ (↑(f x) : ℝ) • g x) x) ((fun (x : α) ↦ (↑(f x) : ℝ) • g' x) x)
mp₁ :
  ∀ᵐ (x : α) ∂μ.restrict {x : α | f x ≠ 0}ᶜ,
    Eq.{u_2 + 1} (α := E) ((fun (x : α) ↦ (↑(f x) : ℝ) • g x) x) ((fun (x : α) ↦ (↑(f x) : ℝ) • g' x) x)
⊢ EventuallyEq.{u_1, u_2} (β := E) (ae μ) (fun (x : α) ↦ (↑(f x) : ℝ) • g x) fun (x : α) ↦ (↑(f x) : ℝ) • g' x

Tactic:
apply @ae_of_ae_restrict_of_ae_restrict_compl _ _ _ { x | f x ≠ 0 }

Premises used: MeasureTheory.ae_of_ae_restrict_of_ae_restrict_compl, setOf, Ne, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Integral.LebesgueNormedSpace
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : SecondCountableTopology E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : Measurable g'
hg' : g =ᶠ[ae (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞))] g'
A : MeasurableSet.{u_1} (α := α) {x : α | f x ≠ 0}
⊢ ∀ᵐ (x : α) ∂μ, (↑(f x) : ℝ≥0∞) ≠ 0 → g x = g' x

Tactic:
rw [EventuallyEq, ae_withDensity_iff hf.coe_nnreal_ennreal] at hg'

Premises used: Measurable.coe_nnreal_ennreal, MeasureTheory.ae_withDensity_iff, Filter.EventuallyEq
-- Module: Mathlib.MeasureTheory.Integral.LebesgueNormedSpace
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : SecondCountableTopology E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : Measurable g'
hg' : g =ᶠ[ae (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞))] g'
A : MeasurableSet.{u_1} (α := α) {x : α | f x ≠ 0}
hg'₁ : ∀ᵐ (x : α) ∂μ, (↑(f x) : ℝ≥0∞) ≠ 0 → g x = g' x
⊢ MeasurableSet.{u_1} (α := α) {x : α | f x ≠ 0}

Tactic:
rw [EventuallyEq, ae_withDensity_iff hf.coe_nnreal_ennreal] at hg'

Premises used: Measurable.coe_nnreal_ennreal, MeasureTheory.ae_withDensity_iff, Filter.EventuallyEq
-- Module: Mathlib.MeasureTheory.Integral.LebesgueNormedSpace
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : SecondCountableTopology E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : Measurable g'
hg' : ∀ᵐ (x : α) ∂μ, (↑(f x) : ℝ≥0∞) ≠ 0 → g x = g' x
A : MeasurableSet.{u_1} (α := α) {x : α | f x ≠ 0}
mp :
  ∀ᵐ (x : α) ∂μ,
    Membership.mem (γ := Set α) {x : α | f x ≠ 0} x →
      Eq.{u_2 + 1} (α := E) ((fun (x : α) ↦ (↑(f x) : ℝ) • g x) x) ((fun (x : α) ↦ (↑(f x) : ℝ) • g' x) x)
⊢ ∀ᵐ (x : α) ∂μ.restrict {x : α | f x ≠ 0},
    Eq.{u_2 + 1} (α := E) ((fun (x : α) ↦ (↑(f x) : ℝ) • g x) x) ((fun (x : α) ↦ (↑(f x) : ℝ) • g' x) x)

Tactic:
rw [ae_restrict_iff' A]

Premises used: MeasureTheory.ae_restrict_iff'
-- Module: Mathlib.MeasureTheory.Integral.LebesgueNormedSpace
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : SecondCountableTopology E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : Measurable g'
hg' : ∀ᵐ (x : α) ∂μ, (↑(f x) : ℝ≥0∞) ≠ 0 → g x = g' x
A : MeasurableSet.{u_1} (α := α) {x : α | f x ≠ 0}
h : ∀ (a : α), ((↑(f a) : ℝ≥0∞) ≠ 0 → g a = g' a) → f a ≠ 0 → (↑(f a) : ℝ) • g a = (↑(f a) : ℝ) • g' a
⊢ ∀ᵐ (x : α) ∂μ,
    Membership.mem (γ := Set α) {x : α | f x ≠ 0} x →
      Eq.{u_2 + 1} (α := E) ((fun (x : α) ↦ (↑(f x) : ℝ) • g x) x) ((fun (x : α) ↦ (↑(f x) : ℝ) • g' x) x)

Tactic:
filter_upwards [hg']
-- Module: Mathlib.MeasureTheory.Integral.LebesgueNormedSpace
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : SecondCountableTopology E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : Measurable g'
hg' : ∀ᵐ (x : α) ∂μ, (↑(f x) : ℝ≥0∞) ≠ 0 → g x = g' x
A : MeasurableSet.{u_1} (α := α) {x : α | f x ≠ 0}
a : α
ha : (↑(f a) : ℝ≥0∞) ≠ 0 → g a = g' a
h'a : f a ≠ 0
⊢ (↑(f a) : ℝ≥0∞) ≠ 0

Tactic:
simpa only [Ne, ENNReal.coe_eq_zero] using h'a

Premises used: Ne, ENNReal.coe_eq_zero
-- Module: Mathlib.MeasureTheory.Integral.LebesgueNormedSpace
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : SecondCountableTopology E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : Measurable g'
hg' : ∀ᵐ (x : α) ∂μ, (↑(f x) : ℝ≥0∞) ≠ 0 → g x = g' x
A : MeasurableSet.{u_1} (α := α) {x : α | f x ≠ 0}
a : α
ha : (↑(f a) : ℝ≥0∞) ≠ 0 → g a = g' a
h'a : f a ≠ 0
⊢ (↑(f a) : ℝ≥0∞) ≠ 0

Tactic:
have : (f a : ℝ≥0∞) ≠ 0 := by simpa only [Ne, ENNReal.coe_eq_zero] using h'a
-- Module: Mathlib.MeasureTheory.Integral.LebesgueNormedSpace
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : SecondCountableTopology E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : Measurable g'
hg' : ∀ᵐ (x : α) ∂μ, (↑(f x) : ℝ≥0∞) ≠ 0 → g x = g' x
A : MeasurableSet.{u_1} (α := α) {x : α | f x ≠ 0}
a : α
ha : (↑(f a) : ℝ≥0∞) ≠ 0 → g a = g' a
h'a : f a ≠ 0
this : (↑(f a) : ℝ≥0∞) ≠ 0
h h₁ : (↑(f a) : ℝ) • g' a = (↑(f a) : ℝ) • g' a
⊢ (↑(f a) : ℝ) • g a = (↑(f a) : ℝ) • g' a

Tactic:
rw [ha this]
-- Module: Mathlib.MeasureTheory.Integral.LebesgueNormedSpace
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : SecondCountableTopology E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : Measurable g'
hg' : g =ᶠ[ae (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞))] g'
A : MeasurableSet.{u_1} (α := α) {x : α | f x ≠ 0}
h : ∀ (a : α), Membership.mem (γ := Set α) {x : α | f x ≠ 0}ᶜ a → (↑(f a) : ℝ) • g a = (↑(f a) : ℝ) • g' a
⊢ ∀ᵐ (x : α) ∂μ.restrict {x : α | f x ≠ 0}ᶜ,
    Eq.{u_2 + 1} (α := E) ((fun (x : α) ↦ (↑(f x) : ℝ) • g x) x) ((fun (x : α) ↦ (↑(f x) : ℝ) • g' x) x)

Tactic:
filter_upwards [ae_restrict_mem A.compl]

Premises used: MeasureTheory.ae_restrict_mem, MeasurableSet.compl
-- Module: Mathlib.MeasureTheory.Integral.LebesgueNormedSpace
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : SecondCountableTopology E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : Measurable g'
hg' : g =ᶠ[ae (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞))] g'
A : MeasurableSet.{u_1} (α := α) {x : α | f x ≠ 0}
x : α
hx : Membership.mem (γ := Set α) {x : α | f x ≠ 0}ᶜ x
⊢ f x = 0

Tactic:
simp only [Classical.not_not, mem_setOf_eq, mem_compl_iff] at hx

Premises used: Classical.not_not, Set.mem_setOf_eq, Set.mem_compl_iff
-- Module: Mathlib.MeasureTheory.Integral.LebesgueNormedSpace
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : SecondCountableTopology E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : Measurable g'
hg' : g =ᶠ[ae (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞))] g'
A : MeasurableSet.{u_1} (α := α) {x : α | f x ≠ 0}
x : α
hx : f x = 0
⊢ (↑(f x) : ℝ) • g x = (↑(f x) : ℝ) • g' x

Tactic:
simp [hx]
-- Module: Mathlib.MeasureTheory.Integral.LebesgueNormedSpace
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : SecondCountableTopology E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : Measurable g'
hg' : (fun (x : α) ↦ (↑(f x) : ℝ) • g x) =ᶠ[ae μ] g'
⊢ AEMeasurable g (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞))

Tactic:
⟨fun x => (f x : ℝ)⁻¹ • g' x, hf.coe_nnreal_real.inv.smul g'meas, ?_⟩

Premises used: AEMeasurable, Measurable.coe_nnreal_real, Inv.inv, Measurable.inv, And.intro, Measurable.smul, Exists.intro, HSMul.hSMul, NNReal.toReal
-- Module: Mathlib.MeasureTheory.Integral.LebesgueNormedSpace
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : SecondCountableTopology E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : Measurable g'
hg' : (fun (x : α) ↦ (↑(f x) : ℝ) • g x) =ᶠ[ae μ] g'
mpr : g =ᶠ[ae (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞))] fun (x : α) ↦ (↑(f x) : ℝ)⁻¹ • g' x
⊢ AEMeasurable g (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞))

Tactic:
refine ⟨fun x => (f x : ℝ)⁻¹ • g' x, hf.coe_nnreal_real.inv.smul g'meas, ?_⟩
-- Module: Mathlib.MeasureTheory.Integral.LebesgueNormedSpace
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : SecondCountableTopology E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : Measurable g'
hg' : (fun (x : α) ↦ (↑(f x) : ℝ) • g x) =ᶠ[ae μ] g'
mpr : ∀ᵐ (x : α) ∂μ, (↑(f x) : ℝ≥0∞) ≠ 0 → g x = (↑(f x) : ℝ)⁻¹ • g' x
⊢ g =ᶠ[ae (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞))] fun (x : α) ↦ (↑(f x) : ℝ)⁻¹ • g' x

Tactic:
rw [EventuallyEq, ae_withDensity_iff hf.coe_nnreal_ennreal]

Premises used: Measurable.coe_nnreal_ennreal, MeasureTheory.ae_withDensity_iff, Filter.EventuallyEq
-- Module: Mathlib.MeasureTheory.Integral.LebesgueNormedSpace
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : SecondCountableTopology E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : Measurable g'
hg' : (fun (x : α) ↦ (↑(f x) : ℝ) • g x) =ᶠ[ae μ] g'
h : ∀ (a : α), (↑(f a) : ℝ) • g a = g' a → (↑(f a) : ℝ≥0∞) ≠ 0 → g a = (↑(f a) : ℝ)⁻¹ • g' a
⊢ ∀ᵐ (x : α) ∂μ, (↑(f x) : ℝ≥0∞) ≠ 0 → g x = (↑(f x) : ℝ)⁻¹ • g' x

Tactic:
filter_upwards [hg']
-- Module: Mathlib.MeasureTheory.Integral.LebesgueNormedSpace
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : SecondCountableTopology E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : Measurable g'
hg' : (fun (x : α) ↦ (↑(f x) : ℝ) • g x) =ᶠ[ae μ] g'
x : α
hx : (↑(f x) : ℝ) • g x = g' x
h'x : (↑(f x) : ℝ≥0∞) ≠ 0
h : (↑(f x) : ℝ) ≠ 0
⊢ g x = (↑(f x) : ℝ)⁻¹ • g' x

Tactic:
rw [← hx, smul_smul, inv_mul_cancel₀, one_smul]

Premises used: smul_smul, one_smul, inv_mul_cancel₀
-- Module: Mathlib.MeasureTheory.Integral.LebesgueNormedSpace
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : SecondCountableTopology E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : Measurable g'
hg' : (fun (x : α) ↦ (↑(f x) : ℝ) • g x) =ᶠ[ae μ] g'
x : α
hx : (↑(f x) : ℝ) • g x = g' x
h'x : (↑(f x) : ℝ≥0∞) ≠ 0
⊢ ¬f x = 0

Tactic:
simp only [Ne, ENNReal.coe_eq_zero] at h'x

Premises used: Ne, ENNReal.coe_eq_zero
-- Module: Mathlib.MeasureTheory.Integral.LebesgueNormedSpace
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : SecondCountableTopology E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : Measurable g'
hg' : (fun (x : α) ↦ (↑(f x) : ℝ) • g x) =ᶠ[ae μ] g'
x : α
hx : (↑(f x) : ℝ) • g x = g' x
h'x : ¬f x = 0
⊢ (↑(f x) : ℝ) ≠ 0

Tactic:
simpa only [NNReal.coe_eq_zero, Ne] using h'x

Premises used: NNReal.coe_eq_zero, Ne
-- 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 : ((i : δ) → X i) → ℝ≥0∞
inst_2 : ∀ (i : δ), SigmaFinite (μ i)
hf : Measurable f
⊢ Measurable (lmarginal (X := X) μ s f)

Tactic:
Measurable.lintegral_prod_right (hf.comp measurable_updateFinset')

Premises used: Measurable.comp, measurable_updateFinset', MeasureTheory.lmarginal, Measurable.lintegral_prod_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 δ
f : ((i : δ) → X i) → ℝ≥0∞
h : ∀ (x : (i : δ) → X i), lmarginal (X := X) μ ∅ f x = f x
⊢ lmarginal (X := X) μ ∅ f = 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 δ
f : ((i : δ) → X i) → ℝ≥0∞
x : (i : δ) → X i
h :
  (∫⁻ (y : (i : ↥∅) → X (↑i : δ)),
      f (updateFinset (π := X) x ∅ y) ∂Measure.dirac fun (a : ↥∅) ↦ isEmptyElim (p := fun (x : ↥∅) ↦ X (↑x : δ)) a) =
    f x
⊢ lmarginal (X := X) μ ∅ f x = f x

Tactic:
simp_rw [lmarginal, Measure.pi_of_empty fun i : (∅ : Finset δ) => μ i]

Premises used: MeasureTheory.Measure.pi_of_empty, isEmptyElim, MeasureTheory.lmarginal, 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 δ
f : ((i : δ) → X i) → ℝ≥0∞
x : (i : δ) → X i
h : Measurable (β := ℝ≥0∞) fun (a : (i : ↥∅) → X (↑i : δ)) ↦ f (updateFinset (π := X) x ∅ a)
⊢ (∫⁻ (y : (i : ↥∅) → X (↑i : δ)),
      f (updateFinset (π := X) x ∅ y) ∂Measure.dirac fun (a : ↥∅) ↦ isEmptyElim (p := fun (x : ↥∅) ↦ X (↑x : δ)) a) =
    f x

Tactic:
apply lintegral_dirac'

Premises used: MeasureTheory.lintegral_dirac'
-- 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∞
x : (i : δ) → X i
⊢ Measurable (β := ℝ≥0∞) fun (a : (i : ↥∅) → X (↑i : δ)) ↦ f (updateFinset (π := X) x ∅ a)

Tactic:
Subsingleton.measurable

Premises used: Subsingleton.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 δ
f : ((i : δ) → X i) → ℝ≥0∞
x : (i : δ) → X i
⊢ Measurable (β := ℝ≥0∞) fun (a : (i : ↥∅) → X (↑i : δ)) ↦ f (updateFinset (π := X) x ∅ a)

Tactic:
exact Subsingleton.measurable

Premises used: Subsingleton.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 : Finset δ
x y : (i : δ) → X i
f : ((i : δ) → X i) → ℝ≥0∞
h : ∀ i ∉ s, x i = y i
dsimp :
  (∫⁻ (y : (i : ↥s) → X (↑i : δ)),
      f fun (i : δ) ↦
        if hi : i ∈ s then y (Subtype.mk (p := fun (x : δ) ↦ x ∈ s) i hi)
        else x i ∂Measure.pi (α := fun (i : ↥s) ↦ X (↑i : δ)) fun (i : ↥s) ↦ μ (↑i : δ)) =
    ∫⁻ (y_1 : (i : ↥s) → X (↑i : δ)),
      f fun (i : δ) ↦
        if hi : i ∈ s then y_1 (Subtype.mk (p := fun (x : δ) ↦ x ∈ s) i hi)
        else y i ∂Measure.pi (α := fun (i : ↥s) ↦ X (↑i : δ)) fun (i : ↥s) ↦ μ (↑i : δ)
⊢ lmarginal (X := X) μ s f x = lmarginal (X := X) μ s f y

Tactic:
dsimp [lmarginal, updateFinset_def]

Premises used: MeasureTheory.lmarginal, Function.updateFinset_def
-- 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 δ
x y : (i : δ) → X i
f : ((i : δ) → X i) → ℝ≥0∞
h : ∀ i ∉ s, x i = y i
e_f : ∀ (x_1 : (i : ↥s) → X (↑i : δ)), ∀ x_2 ∉ s, x x_2 = y x_2
⊢ (∫⁻ (y : (i : ↥s) → X (↑i : δ)),
      f fun (i : δ) ↦
        if hi : i ∈ s then y (Subtype.mk (p := fun (x : δ) ↦ x ∈ s) i hi)
        else x i ∂Measure.pi (α := fun (i : ↥s) ↦ X (↑i : δ)) fun (i : ↥s) ↦ μ (↑i : δ)) =
    ∫⁻ (y_1 : (i : ↥s) → X (↑i : δ)),
      f fun (i : δ) ↦
        if hi : i ∈ s then y_1 (Subtype.mk (p := fun (x : δ) ↦ x ∈ s) i hi)
        else y i ∂Measure.pi (α := fun (i : ↥s) ↦ X (↑i : δ)) fun (i : ↥s) ↦ μ (↑i : δ)

Tactic:
rcongr
-- 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 δ
x y : (i : δ) → X i
f : ((i : δ) → X i) → ℝ≥0∞
h : ∀ i ∉ s, x i = y i
x_1 : (i : ↥s) → X (↑i : δ)
x_2 : δ
h_1 : x_2 ∉ s
⊢ x x_2 = y x_2

Tactic:
h _ ‹_›
-- 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 δ
x y : (i : δ) → X i
f : ((i : δ) → X i) → ℝ≥0∞
h : ∀ i ∉ s, x i = y i
x_1 : (i : ↥s) → X (↑i : δ)
x_2 : δ
h_1 : x_2 ∉ s
⊢ x x_2 = y x_2

Tactic:
exact h _ ‹_›
-- 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 δ
i : δ
hi : i ∈ s
f : ((i : δ) → X i) → ℝ≥0∞
x : (i : δ) → X i
y : X i
⊢ lmarginal (X := X) μ s f (update (β := X) x i y) = lmarginal (X := X) μ s f x

Tactic:
grind [MeasureTheory.lmarginal_congr]

Premises used: MeasureTheory.lmarginal_congr
-- 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 : δ))
h : ∀ (x : (i : δ) → X i), lmarginal (X := X) μ {i} f x = ∫⁻ (xᵢ : X i), f (update (β := X) x i xᵢ) ∂μ i
⊢ lmarginal (X := X) μ {i} f = fun (x : (a : δ) → X a) ↦ ∫⁻ (xᵢ : X i), f (update (β := X) x i xᵢ) ∂μ i

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 δ
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 : δ)
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 : δ)
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}
          (((MeasurableEquiv.symm (MeasurableEquiv.piUnique fun (j : α) ↦ X (↑j : δ)) :
                X (↑default : δ) ≃ᵐ ((i_1 : α) → X (↑i_1 : δ))) :
              (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 : δ)

Tactic:
simp_rw [lmarginal,
          measurePreserving_piUnique (fun j : ({i} : Finset δ) ↦ μ j) |>.symm _
            |>.lintegral_map_equiv, e, α]

Premises used: MeasureTheory.MeasurePreserving.symm, MeasurableEquiv.piUnique, MeasurableEquiv.symm, MeasureTheory.measurePreserving_piUnique, MeasureTheory.lmarginal, Subtype.val, MeasureTheory.MeasurePreserving.lintegral_map_equiv