awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0∞ := AEMeasurable.mk f hf
hg : AEMeasurable g (μ.withDensity f')
this : μ.withDensity f = μ.withDensity f'
g' : α → ℝ≥0∞ := AEMeasurable.mk g hg
Z : g =ᶠ[ae (μ.withDensity f')] AEMeasurable.mk g hg
⊢ ∀ᵐ (x : α) ∂μ.restrict {x : α | AEMeasurable.mk f hf x ≠ 0}, g x = AEMeasurable.mk g hg x

Tactic:
rw [EventuallyEq, ae_withDensity_iff_ae_restrict hf.measurable_mk] at Z

Premises used: MeasureTheory.ae_withDensity_iff_ae_restrict, Filter.EventuallyEq, AEMeasurable.measurable_mk
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0∞ := AEMeasurable.mk f hf
hg : AEMeasurable g (μ.withDensity f')
this : μ.withDensity f = μ.withDensity f'
g' : α → ℝ≥0∞ := AEMeasurable.mk g hg
Z : ∀ᵐ (x : α) ∂μ.restrict {x : α | AEMeasurable.mk f hf x ≠ 0}, g x = AEMeasurable.mk g hg x
h : ∀ (a : α), g a = AEMeasurable.mk g hg a → (f' * g') a = (f' * g) a
⊢ ∀ᵐ (x : α) ∂μ.restrict {x : α | f' x ≠ 0}, (f' * g') x = (f' * g) x

Tactic:
filter_upwards [Z]
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0∞ := AEMeasurable.mk f hf
hg : AEMeasurable g (μ.withDensity f')
this : μ.withDensity f = μ.withDensity f'
g' : α → ℝ≥0∞ := AEMeasurable.mk g hg
Z : ∀ᵐ (x : α) ∂μ.restrict {x : α | AEMeasurable.mk f hf x ≠ 0}, g x = AEMeasurable.mk g hg x
x : α
hx : g x = AEMeasurable.mk g hg x
⊢ (f' * g') x = (f' * g) x

Tactic:
simp only [g', hx, Pi.mul_apply]

Premises used: Pi.mul_apply
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0∞ := AEMeasurable.mk f hf
hg : AEMeasurable g (μ.withDensity f')
this : μ.withDensity f = μ.withDensity f'
g' : α → ℝ≥0∞ := AEMeasurable.mk g hg
⊢ MeasurableSet.{u_1} (α := α) {x : α | f' x ≠ 0}ᶜ

Tactic:
have M : MeasurableSet { x : α | f' x ≠ 0 }ᶜ :=
          (hf.measurable_mk (measurableSet_singleton 0).compl).compl
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0∞ := AEMeasurable.mk f hf
hg : AEMeasurable g (μ.withDensity f')
this : μ.withDensity f = μ.withDensity f'
g' : α → ℝ≥0∞ := AEMeasurable.mk g hg
M : MeasurableSet.{u_1} (α := α) {x : α | f' x ≠ 0}ᶜ
h : ∀ (a : α), Membership.mem (γ := Set α) {x : α | f' x ≠ 0}ᶜ a → (f' * g') a = (f' * g) a
⊢ ∀ᵐ (x : α) ∂μ.restrict {x : α | f' x ≠ 0}ᶜ, (f' * g') x = (f' * g) x

Tactic:
filter_upwards [ae_restrict_mem M]

Premises used: MeasureTheory.ae_restrict_mem
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0∞ := AEMeasurable.mk f hf
hg : AEMeasurable g (μ.withDensity f')
this : μ.withDensity f = μ.withDensity f'
g' : α → ℝ≥0∞ := AEMeasurable.mk g hg
M : 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.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0∞ := AEMeasurable.mk f hf
hg : AEMeasurable g (μ.withDensity f')
this : μ.withDensity f = μ.withDensity f'
g' : α → ℝ≥0∞ := AEMeasurable.mk g hg
M : MeasurableSet.{u_1} (α := α) {x : α | f' x ≠ 0}ᶜ
x : α
hx : f' x = 0
⊢ (f' * g') x = (f' * g) x

Tactic:
simp only [hx, zero_mul, Pi.mul_apply]

Premises used: Pi.mul_apply, MulZeroClass.zero_mul
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0∞ := AEMeasurable.mk f hf
hg : AEMeasurable g (μ.withDensity f')
this : μ.withDensity f = μ.withDensity f'
g' : α → ℝ≥0∞ := AEMeasurable.mk g hg
h : f' * g =ᶠ[ae μ] f * g
⊢ ∫⁻ (a : α), (f' * g) a ∂μ = ∫⁻ (a : α), (f * g) a ∂μ

Tactic:
apply lintegral_congr_ae

Premises used: MeasureTheory.lintegral_congr_ae
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0∞ := AEMeasurable.mk f hf
hg : AEMeasurable g (μ.withDensity f')
this : μ.withDensity f = μ.withDensity f'
g' : α → ℝ≥0∞ := AEMeasurable.mk g hg
h : ∀ (a : α), f a = AEMeasurable.mk f hf a → (f' * g) a = (f * g) a
⊢ f' * g =ᶠ[ae μ] f * g

Tactic:
filter_upwards [hf.ae_eq_mk]

Premises used: AEMeasurable.ae_eq_mk
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0∞ := AEMeasurable.mk f hf
hg : AEMeasurable g (μ.withDensity f')
this : μ.withDensity f = μ.withDensity f'
g' : α → ℝ≥0∞ := AEMeasurable.mk g hg
x : α
hx : f x = AEMeasurable.mk f hf x
⊢ (f' * g) x = (f * g) x

Tactic:
simp only [f', hx, Pi.mul_apply]

Premises used: Pi.mul_apply
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0∞ := AEMeasurable.mk f hf
hg : AEMeasurable g (μ.withDensity f')
this : μ.withDensity f = μ.withDensity f'
g' : α → ℝ≥0∞ := AEMeasurable.mk g hg
g₁ : ∫⁻ (a : α), (f' * g') a ∂μ = ∫⁻ (a : α), (f' * g) a ∂μ
g₂ : ∫⁻ (a : α), (f' * g) a ∂μ = ∫⁻ (a : α), (f * g) a ∂μ
⊢ ∫⁻ (a : α), g a ∂μ.withDensity f' = ∫⁻ (a : α), (f * g) a ∂μ

Tactic:
calc
    ∫⁻ a, g a ∂μ.withDensity f' = ∫⁻ a, g' a ∂μ.withDensity f' := lintegral_congr_ae hg.ae_eq_mk
    _ = ∫⁻ a, (f' * g') a ∂μ :=
      (lintegral_withDensity_eq_lintegral_mul _ hf.measurable_mk hg.measurable_mk)
    _ = ∫⁻ a, (f' * g) a ∂μ := by
      apply lintegral_congr_ae
      apply ae_of_ae_restrict_of_ae_restrict_compl { x | f' x ≠ 0 }
      · have Z := hg.ae_eq_mk
        rw [EventuallyEq, ae_withDensity_iff_ae_restrict hf.measurable_mk] at Z
        filter_upwards [Z]
        intro x hx
        simp only [g', hx, Pi.mul_apply]
      · have M : MeasurableSet { x : α | f' x ≠ 0 }ᶜ :=
          (hf.measurable_mk (measurableSet_singleton 0).compl).compl
        filter_upwards [ae_restrict_mem M]
        intro x hx
        simp only [Classical.not_not, mem_setOf_eq, mem_compl_iff] at hx
        simp only [hx, zero_mul, Pi.mul_apply]
    _ = ∫⁻ a : α, (f * g) a ∂μ := by
      apply lintegral_congr_ae
      filter_upwards [hf.ae_eq_mk]
      intro x hx
      simp only [f', hx, Pi.mul_apply]

Premises used: MeasureTheory.Measure.withDensity, MeasureTheory.lintegral_withDensity_eq_lintegral_mul, MeasureTheory.lintegral_congr_ae, AEMeasurable.ae_eq_mk, AEMeasurable.measurable_mk
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
g : α → ℝ≥0∞
hg : AEMeasurable g (μ.withDensity f)
s : Set α
hs : MeasurableSet s
rw : AEMeasurable g ((μ.restrict s).withDensity f)
⊢ ∫⁻ (a : α) in s, g a ∂μ.withDensity f = ∫⁻ (a : α) in s, (f * g) a ∂μ

Tactic:
rw [restrict_withDensity hs, lintegral_withDensity_eq_lintegral_mul₀' hf.restrict]

Premises used: MeasureTheory.restrict_withDensity, AEMeasurable.restrict, MeasureTheory.lintegral_withDensity_eq_lintegral_mul₀'
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
g : α → ℝ≥0∞
hg : AEMeasurable g (μ.withDensity f)
s : Set α
hs : MeasurableSet s
rw : AEMeasurable g ((μ.withDensity f).restrict s)
⊢ AEMeasurable g ((μ.restrict s).withDensity f)

Tactic:
rw [← restrict_withDensity hs]

Premises used: MeasureTheory.restrict_withDensity
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
g : α → ℝ≥0∞
hg : AEMeasurable g (μ.withDensity f)
s : Set α
hs : MeasurableSet s
⊢ AEMeasurable g ((μ.withDensity f).restrict s)

Tactic:
hg.restrict

Premises used: AEMeasurable.restrict
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
g : α → ℝ≥0∞
hg : AEMeasurable g (μ.withDensity f)
s : Set α
hs : MeasurableSet s
⊢ AEMeasurable g ((μ.withDensity f).restrict s)

Tactic:
exact hg.restrict

Premises used: AEMeasurable.restrict
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
g : α → ℝ≥0∞
hg : AEMeasurable g μ
⊢ ∫⁻ (a : α), g a ∂μ.withDensity f = ∫⁻ (a : α), (f * g) a ∂μ

Tactic:
lintegral_withDensity_eq_lintegral_mul₀' hf (hg.mono' (withDensity_absolutelyContinuous μ f))

Premises used: MeasureTheory.lintegral_withDensity_eq_lintegral_mul₀', MeasureTheory.withDensity_absolutelyContinuous, AEMeasurable.mono'
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
g : α → ℝ≥0∞
hg : AEMeasurable g μ
s : Set α
hs : MeasurableSet s
⊢ ∫⁻ (a : α) in s, g a ∂μ.withDensity f = ∫⁻ (a : α) in s, (f * g) a ∂μ

Tactic:
setLIntegral_withDensity_eq_lintegral_mul₀' hf
    (hg.mono' (MeasureTheory.withDensity_absolutelyContinuous μ f)) hs

Premises used: MeasureTheory.setLIntegral_withDensity_eq_lintegral_mul₀', MeasureTheory.withDensity_absolutelyContinuous, AEMeasurable.mono'
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
g : α → ℝ≥0∞
rw :
  LE.le (α := ℝ≥0∞) (⨆ (g_1 : α → ℝ≥0∞), ⨆ (_ : Measurable g_1), ⨆ (_ : g_1 ≤ g), ∫⁻ (a : α), g_1 a ∂μ.withDensity f)
    (⨆ (g_1 : α → ℝ≥0∞), ⨆ (_ : Measurable g_1), ⨆ (_ : g_1 ≤ f * g), ∫⁻ (a : α), g_1 a ∂μ)
⊢ ∫⁻ (a : α), g a ∂μ.withDensity f ≤ ∫⁻ (a : α), (f * g) a ∂μ

Tactic:
rw [← iSup_lintegral_measurable_le_eq_lintegral, ← iSup_lintegral_measurable_le_eq_lintegral]

Premises used: MeasureTheory.iSup_lintegral_measurable_le_eq_lintegral
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
g : α → ℝ≥0∞
⊢ LE.le (α := ℝ≥0∞) (⨆ (g_1 : α → ℝ≥0∞), ⨆ (_ : Measurable g_1), ⨆ (_ : g_1 ≤ g), ∫⁻ (a : α), g_1 a ∂μ.withDensity f)
    (⨆ (g_1 : α → ℝ≥0∞), ⨆ (_ : Measurable g_1), ⨆ (_ : g_1 ≤ f * g), ∫⁻ (a : α), g_1 a ∂μ)

Tactic:
iSup₂_le fun i i_meas => iSup_le fun hi => ?_

Premises used: iSup₂_le, iSup_le
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
g : α → ℝ≥0∞
refine :
  ∀ (i : α → ℝ≥0∞) (i_meas : Measurable i) (hi : i ≤ g),
    ∫⁻ (a : α), i a ∂μ.withDensity f ≤
      ⨆ (g_1 : α → ℝ≥0∞), ⨆ (_ : Measurable g_1), ⨆ (_ : g_1 ≤ f * g), ∫⁻ (a : α), g_1 a ∂μ
⊢ LE.le (α := ℝ≥0∞) (⨆ (g_1 : α → ℝ≥0∞), ⨆ (_ : Measurable g_1), ⨆ (_ : g_1 ≤ g), ∫⁻ (a : α), g_1 a ∂μ.withDensity f)
    (⨆ (g_1 : α → ℝ≥0∞), ⨆ (_ : Measurable g_1), ⨆ (_ : g_1 ≤ f * g), ∫⁻ (a : α), g_1 a ∂μ)

Tactic:
refine iSup₂_le fun i i_meas => iSup_le fun hi => ?_

Premises used: iSup₂_le, iSup_le
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
g i : α → ℝ≥0∞
i_meas : Measurable i
hi : i ≤ g
rw : ∫⁻ (a : α), (f * i) a ∂μ ≤ ⨆ (g_1 : α → ℝ≥0∞), ⨆ (_ : Measurable g_1), ⨆ (_ : g_1 ≤ f * g), ∫⁻ (a : α), g_1 a ∂μ
⊢ ∫⁻ (a : α), i a ∂μ.withDensity f ≤
    ⨆ (g_1 : α → ℝ≥0∞), ⨆ (_ : Measurable g_1), ⨆ (_ : g_1 ≤ f * g), ∫⁻ (a : α), g_1 a ∂μ

Tactic:
rw [lintegral_withDensity_eq_lintegral_mul _ f_meas i_meas]

Premises used: MeasureTheory.lintegral_withDensity_eq_lintegral_mul
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
g i : α → ℝ≥0∞
i_meas : Measurable i
hi : i ≤ g
grw grw₁ : f * g ≤ f * g
⊢ f * i ≤ f * g

Tactic:
grw [hi]
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
g i : α → ℝ≥0∞
i_meas : Measurable i
hi : i ≤ g
⊢ ∫⁻ (a : α), (f * i) a ∂μ ≤ ⨆ (g_1 : α → ℝ≥0∞), ⨆ (_ : Measurable g_1), ⨆ (_ : g_1 ≤ f * g), ∫⁻ (a : α), g_1 a ∂μ

Tactic:
exact le_iSup₂_of_le (f * i) (f_meas.mul i_meas) <| le_iSup_of_le (by grw [hi]) le_rfl

Premises used: Measurable.mul, le_rfl, HMul.hMul, le_iSup_of_le, le_iSup₂_of_le
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
hf : ∀ᵐ (x : α) ∂μ, f x < ∞
g : α → ℝ≥0∞
⊢ ∫⁻ (a : α), g a ∂μ.withDensity f = ∫⁻ (a : α), (f * g) a ∂μ

Tactic:
le_antisymm (lintegral_withDensity_le_lintegral_mul μ f_meas g) ?_

Premises used: le_antisymm, MeasureTheory.lintegral_withDensity_le_lintegral_mul
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
hf : ∀ᵐ (x : α) ∂μ, f x < ∞
g : α → ℝ≥0∞
refine : ∫⁻ (a : α), (f * g) a ∂μ ≤ ∫⁻ (a : α), g a ∂μ.withDensity f
⊢ ∫⁻ (a : α), g a ∂μ.withDensity f = ∫⁻ (a : α), (f * g) a ∂μ

Tactic:
refine le_antisymm (lintegral_withDensity_le_lintegral_mul μ f_meas g) ?_

Premises used: le_antisymm, MeasureTheory.lintegral_withDensity_le_lintegral_mul
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
hf : ∀ᵐ (x : α) ∂μ, f x < ∞
g : α → ℝ≥0∞
rw :
  LE.le (α := ℝ≥0∞) (⨆ (g_1 : α → ℝ≥0∞), ⨆ (_ : Measurable g_1), ⨆ (_ : g_1 ≤ f * g), ∫⁻ (a : α), g_1 a ∂μ)
    (⨆ (g_1 : α → ℝ≥0∞), ⨆ (_ : Measurable g_1), ⨆ (_ : g_1 ≤ g), ∫⁻ (a : α), g_1 a ∂μ.withDensity f)
⊢ ∫⁻ (a : α), (f * g) a ∂μ ≤ ∫⁻ (a : α), g a ∂μ.withDensity f

Tactic:
rw [← iSup_lintegral_measurable_le_eq_lintegral, ← iSup_lintegral_measurable_le_eq_lintegral]

Premises used: MeasureTheory.iSup_lintegral_measurable_le_eq_lintegral
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
hf : ∀ᵐ (x : α) ∂μ, f x < ∞
g : α → ℝ≥0∞
⊢ LE.le (α := ℝ≥0∞) (⨆ (g_1 : α → ℝ≥0∞), ⨆ (_ : Measurable g_1), ⨆ (_ : g_1 ≤ f * g), ∫⁻ (a : α), g_1 a ∂μ)
    (⨆ (g_1 : α → ℝ≥0∞), ⨆ (_ : Measurable g_1), ⨆ (_ : g_1 ≤ g), ∫⁻ (a : α), g_1 a ∂μ.withDensity f)

Tactic:
iSup₂_le fun i i_meas => iSup_le fun hi => ?_

Premises used: iSup₂_le, iSup_le
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
hf : ∀ᵐ (x : α) ∂μ, f x < ∞
g : α → ℝ≥0∞
refine :
  ∀ (i : α → ℝ≥0∞) (i_meas : Measurable i) (hi : i ≤ f * g),
    ∫⁻ (a : α), i a ∂μ ≤ ⨆ (g_1 : α → ℝ≥0∞), ⨆ (_ : Measurable g_1), ⨆ (_ : g_1 ≤ g), ∫⁻ (a : α), g_1 a ∂μ.withDensity f
⊢ LE.le (α := ℝ≥0∞) (⨆ (g_1 : α → ℝ≥0∞), ⨆ (_ : Measurable g_1), ⨆ (_ : g_1 ≤ f * g), ∫⁻ (a : α), g_1 a ∂μ)
    (⨆ (g_1 : α → ℝ≥0∞), ⨆ (_ : Measurable g_1), ⨆ (_ : g_1 ≤ g), ∫⁻ (a : α), g_1 a ∂μ.withDensity f)

Tactic:
refine iSup₂_le fun i i_meas => iSup_le fun hi => ?_

Premises used: iSup₂_le, iSup_le
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
hf : ∀ᵐ (x : α) ∂μ, f x < ∞
g i : α → ℝ≥0∞
i_meas : Measurable i
hi : i ≤ f * g
x : α
rw : i x / f x ≤ g x
⊢ (f x)⁻¹ * i x ≤ g x

Tactic:
rw [mul_comm, ← div_eq_mul_inv]

Premises used: div_eq_mul_inv, mul_comm
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
hf : ∀ᵐ (x : α) ∂μ, f x < ∞
g i : α → ℝ≥0∞
i_meas : Measurable i
hi : i ≤ f * g
x : α
⊢ i x / f x ≤ g x

Tactic:
div_le_of_le_mul' (hi x)

Premises used: ENNReal.div_le_of_le_mul'
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
hf : ∀ᵐ (x : α) ∂μ, f x < ∞
g i : α → ℝ≥0∞
i_meas : Measurable i
hi : i ≤ f * g
x : α
⊢ i x / f x ≤ g x

Tactic:
exact div_le_of_le_mul' (hi x)

Premises used: ENNReal.div_le_of_le_mul'
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
hf : ∀ᵐ (x : α) ∂μ, f x < ∞
g i : α → ℝ≥0∞
i_meas : Measurable i
hi : i ≤ f * g
⊢ (fun (x : α) ↦ (f x)⁻¹ * i x) ≤ g

Tactic:
have A : (fun x => (f x)⁻¹ * i x) ≤ g := by
    intro x
    dsimp
    rw [mul_comm, ← div_eq_mul_inv]
    exact div_le_of_le_mul' (hi x)
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
hf : ∀ᵐ (x : α) ∂μ, f x < ∞
g i : α → ℝ≥0∞
i_meas : Measurable i
hi : i ≤ f * g
A : (fun (x : α) ↦ (f x)⁻¹ * i x) ≤ g
⊢ ∫⁻ (a : α), i a ∂μ ≤ ⨆ (g_1 : α → ℝ≥0∞), ⨆ (_ : Measurable g_1), ⨆ (_ : g_1 ≤ g), ∫⁻ (a : α), g_1 a ∂μ.withDensity f

Tactic:
le_iSup_of_le (fun x => (f x)⁻¹ * i x) (le_iSup_of_le (f_meas.inv.mul i_meas) ?_)

Premises used: Measurable.mul, HMul.hMul, Inv.inv, Measurable.inv, le_iSup_of_le
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
hf : ∀ᵐ (x : α) ∂μ, f x < ∞
g i : α → ℝ≥0∞
i_meas : Measurable i
hi : i ≤ f * g
A : (fun (x : α) ↦ (f x)⁻¹ * i x) ≤ g
refine :
  ∫⁻ (a : α), i a ∂μ ≤
    ⨆ (_ : (fun (x : α) ↦ (f x)⁻¹ * i x) ≤ g), ∫⁻ (a : α), (fun (x : α) ↦ (f x)⁻¹ * i x) a ∂μ.withDensity f
⊢ ∫⁻ (a : α), i a ∂μ ≤ ⨆ (g_1 : α → ℝ≥0∞), ⨆ (_ : Measurable g_1), ⨆ (_ : g_1 ≤ g), ∫⁻ (a : α), g_1 a ∂μ.withDensity f

Tactic:
refine le_iSup_of_le (fun x => (f x)⁻¹ * i x) (le_iSup_of_le (f_meas.inv.mul i_meas) ?_)
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
hf : ∀ᵐ (x : α) ∂μ, f x < ∞
g i : α → ℝ≥0∞
i_meas : Measurable i
hi : i ≤ f * g
A : (fun (x : α) ↦ (f x)⁻¹ * i x) ≤ g
⊢ ∫⁻ (a : α), i a ∂μ ≤
    ⨆ (_ : (fun (x : α) ↦ (f x)⁻¹ * i x) ≤ g), ∫⁻ (a : α), (fun (x : α) ↦ (f x)⁻¹ * i x) a ∂μ.withDensity f

Tactic:
le_iSup_of_le A ?_

Premises used: le_iSup_of_le
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
hf : ∀ᵐ (x : α) ∂μ, f x < ∞
g i : α → ℝ≥0∞
i_meas : Measurable i
hi : i ≤ f * g
A : (fun (x : α) ↦ (f x)⁻¹ * i x) ≤ g
refine : ∫⁻ (a : α), i a ∂μ ≤ ∫⁻ (a : α), (fun (x : α) ↦ (f x)⁻¹ * i x) a ∂μ.withDensity f
⊢ ∫⁻ (a : α), i a ∂μ ≤
    ⨆ (_ : (fun (x : α) ↦ (f x)⁻¹ * i x) ≤ g), ∫⁻ (a : α), (fun (x : α) ↦ (f x)⁻¹ * i x) a ∂μ.withDensity f

Tactic:
refine le_iSup_of_le A ?_

Premises used: le_iSup_of_le
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
hf : ∀ᵐ (x : α) ∂μ, f x < ∞
g i : α → ℝ≥0∞
i_meas : Measurable i
hi : i ≤ f * g
A : (fun (x : α) ↦ (f x)⁻¹ * i x) ≤ g
rw : ∫⁻ (a : α), i a ∂μ ≤ ∫⁻ (a : α), HMul.hMul (β := α → ℝ≥0∞) f (fun (a : α) ↦ (f a)⁻¹ * i a) a ∂μ
⊢ ∫⁻ (a : α), i a ∂μ ≤ ∫⁻ (a : α), (fun (x : α) ↦ (f x)⁻¹ * i x) a ∂μ.withDensity f

Tactic:
rw [lintegral_withDensity_eq_lintegral_mul _ f_meas (f_meas.inv.mul i_meas)]

Premises used: Measurable.mul, MeasureTheory.lintegral_withDensity_eq_lintegral_mul, Measurable.inv
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
hf : ∀ᵐ (x : α) ∂μ, f x < ∞
g i : α → ℝ≥0∞
i_meas : Measurable i
hi : i ≤ f * g
A : (fun (x : α) ↦ (f x)⁻¹ * i x) ≤ g
h : ∀ᵐ (a : α) ∂μ, i a ≤ HMul.hMul (β := α → ℝ≥0∞) f (fun (a : α) ↦ (f a)⁻¹ * i a) a
⊢ ∫⁻ (a : α), i a ∂μ ≤ ∫⁻ (a : α), HMul.hMul (β := α → ℝ≥0∞) f (fun (a : α) ↦ (f a)⁻¹ * i a) a ∂μ

Tactic:
apply lintegral_mono_ae

Premises used: MeasureTheory.lintegral_mono_ae
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
hf : ∀ᵐ (x : α) ∂μ, f x < ∞
g i : α → ℝ≥0∞
i_meas : Measurable i
hi : i ≤ f * g
A : (fun (x : α) ↦ (f x)⁻¹ * i x) ≤ g
h : ∀ (a : α), f a < ∞ → i a ≤ HMul.hMul (β := α → ℝ≥0∞) f (fun (a : α) ↦ (f a)⁻¹ * i a) a
⊢ ∀ᵐ (a : α) ∂μ, i a ≤ HMul.hMul (β := α → ℝ≥0∞) f (fun (a : α) ↦ (f a)⁻¹ * i a) a

Tactic:
filter_upwards [hf]
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
hf : ∀ᵐ (x : α) ∂μ, f x < ∞
g i : α → ℝ≥0∞
i_meas : Measurable i
hi : i ≤ f * g
A : (fun (x : α) ↦ (f x)⁻¹ * i x) ≤ g
x : α
h'x : f x < ∞
h : ∀ (hx : f x = 0), i x ≤ HMul.hMul (β := α → ℝ≥0∞) f (fun (a : α) ↦ (f a)⁻¹ * i a) x
h₁ : ∀ (hx : f x ≠ 0), i x ≤ HMul.hMul (β := α → ℝ≥0∞) f (fun (a : α) ↦ (f a)⁻¹ * i a) x
⊢ i x ≤ HMul.hMul (β := α → ℝ≥0∞) f (fun (a : α) ↦ (f a)⁻¹ * i a) x

Tactic:
rcases eq_or_ne (f x) 0 with (hx | hx)

Premises used: eq_or_ne, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
hf : ∀ᵐ (x : α) ∂μ, f x < ∞
g i : α → ℝ≥0∞
i_meas : Measurable i
hi : i ≤ f * g
A : (fun (x : α) ↦ (f x)⁻¹ * i x) ≤ g
x : α
h'x : f x < ∞
hx : f x = 0
⊢ i x ≤ (f * g) x

Tactic:
have := hi x
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
hf : ∀ᵐ (x : α) ∂μ, f x < ∞
g i : α → ℝ≥0∞
i_meas : Measurable i
hi : i ≤ f * g
A : (fun (x : α) ↦ (f x)⁻¹ * i x) ≤ g
x : α
h'x : f x < ∞
hx : f x = 0
this : i x ≤ (f * g) x
⊢ i x = 0

Tactic:
simp only [hx, zero_mul, Pi.mul_apply, nonpos_iff_eq_zero] at this

Premises used: Pi.mul_apply, MulZeroClass.zero_mul, nonpos_iff_eq_zero
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
hf : ∀ᵐ (x : α) ∂μ, f x < ∞
g i : α → ℝ≥0∞
i_meas : Measurable i
hi : i ≤ f * g
A : (fun (x : α) ↦ (f x)⁻¹ * i x) ≤ g
x : α
h'x : f x < ∞
hx : f x = 0
this : i x = 0
⊢ i x ≤ HMul.hMul (β := α → ℝ≥0∞) f (fun (a : α) ↦ (f a)⁻¹ * i a) x

Tactic:
simp [this]
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
hf : ∀ᵐ (x : α) ∂μ, f x < ∞
g i : α → ℝ≥0∞
i_meas : Measurable i
hi : i ≤ f * g
A : (fun (x : α) ↦ (f x)⁻¹ * i x) ≤ g
x : α
h'x : f x < ∞
hx : f x ≠ 0
apply : i x = HMul.hMul (β := α → ℝ≥0∞) f (fun (a : α) ↦ (f a)⁻¹ * i a) x
⊢ i x ≤ HMul.hMul (β := α → ℝ≥0∞) f (fun (a : α) ↦ (f a)⁻¹ * i a) x

Tactic:
apply le_of_eq _

Premises used: le_of_eq
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
hf : ∀ᵐ (x : α) ∂μ, f x < ∞
g i : α → ℝ≥0∞
i_meas : Measurable i
hi : i ≤ f * g
A : (fun (x : α) ↦ (f x)⁻¹ * i x) ≤ g
x : α
h'x : f x < ∞
hx : f x ≠ 0
rw : i x = f x * (f x)⁻¹ * i x
rw₁ : i x = 1 * i x
rw₂ rw₃ : i x = i x
⊢ i x = f x * ((f x)⁻¹ * i x)

Tactic:
rw [← mul_assoc, ENNReal.mul_inv_cancel hx h'x.ne, one_mul]

Premises used: mul_assoc, ENNReal.mul_inv_cancel, one_mul, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
g : α → ℝ≥0∞
s : Set α
hs : MeasurableSet s
hf : ∀ᵐ (x : α) ∂μ.restrict s, f x < ∞
rw : ∫⁻ (a : α), g a ∂(μ.restrict s).withDensity f = ∫⁻ (a : α) in s, (f * g) a ∂μ
rw₁ rw₂ : ∫⁻ (a : α) in s, (f * g) a ∂μ = ∫⁻ (a : α) in s, (f * g) a ∂μ
⊢ ∫⁻ (a : α) in s, g a ∂μ.withDensity f = ∫⁻ (a : α) in s, (f * g) a ∂μ

Tactic:
rw [restrict_withDensity hs, lintegral_withDensity_eq_lintegral_mul_non_measurable _ f_meas hf]

Premises used: MeasureTheory.lintegral_withDensity_eq_lintegral_mul_non_measurable, MeasureTheory.restrict_withDensity