awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
p : α → Prop
h : ∀ᵐ (a : α) ∂μ, p a
h_ac : μ.withDensity (ν.rnDeriv μ) ≪ μ
h₁ :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α) {x : α | (fun (a : α) ↦ p a) x} x →
          Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ μ.rnDeriv ν x ≠ 0 → p x) x} x}
      a
h₂ h₃ : ∀ (a : α) (h : p a), μ.rnDeriv ν a ≠ 0 → p a
⊢ ∀ᵐ (x : α) ∂μ, μ.rnDeriv ν x ≠ 0 → p x

Tactic:
filter_upwards [h] with _ h _ using h
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
⊢ ∫⁻ (x : α) in s, μ.rnDeriv ν x ∂ν ≤ (μ : (a : Set α) → ℝ≥0∞) s

Tactic:
(withDensity_apply_le _ _).trans (Measure.le_iff'.1 (withDensity_rnDeriv_le μ ν) s)

Premises used: MeasureTheory.withDensity_apply_le, MeasureTheory.Measure.withDensity_rnDeriv_le, MeasureTheory.Measure.le_iff', Iff.mp, LE.le.trans
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
⊢ ∫⁻ (x : α), μ.rnDeriv ν x ∂ν ≤ (μ : (a : Set α) → ℝ≥0∞) Set.univ

Tactic:
(setLIntegral_univ _).symm ▸ Measure.setLIntegral_rnDeriv_le Set.univ

Premises used: Set.univ, Eq.rec, Eq.symm, MeasureTheory.Measure.setLIntegral_rnDeriv_le, MeasureTheory.setLIntegral_univ
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
s : Set α
hs : MeasurableSet s
rw : Eq (α := ℝ≥0∞) ((ν.withDensity (μ.rnDeriv ν) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
rw₁ rw₂ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ ∫⁻ (x : α) in s, μ.rnDeriv ν x ∂ν = (μ : (a : Set α) → ℝ≥0∞) s

Tactic:
rw [← withDensity_apply _ hs, Measure.withDensity_rnDeriv_eq _ _ hμν]

Premises used: MeasureTheory.withDensity_apply, MeasureTheory.Measure.withDensity_rnDeriv_eq
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
inst_1 : SFinite ν
hμν : μ ≪ ν
s : Set α
rw : Eq (α := ℝ≥0∞) ((ν.withDensity (μ.rnDeriv ν) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
rw₁ rw₂ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ ∫⁻ (x : α) in s, μ.rnDeriv ν x ∂ν = (μ : (a : Set α) → ℝ≥0∞) s

Tactic:
rw [← withDensity_apply' _ s, Measure.withDensity_rnDeriv_eq _ _ hμν]

Premises used: MeasureTheory.withDensity_apply', MeasureTheory.Measure.withDensity_rnDeriv_eq
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
rw : ∫⁻ (x : α) in Set.univ, μ.rnDeriv ν x ∂ν = (μ : (a : Set α) → ℝ≥0∞) Set.univ
rw₁ rw₂ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞)
⊢ ∫⁻ (x : α), μ.rnDeriv ν x ∂ν = (μ : (a : Set α) → ℝ≥0∞) Set.univ

Tactic:
rw [← setLIntegral_univ, setLIntegral_rnDeriv' hμν MeasurableSet.univ]

Premises used: MeasureTheory.Measure.setLIntegral_rnDeriv', MeasurableSet.univ, MeasureTheory.setLIntegral_univ
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ IntegrableOn (ε := ℝ) (fun (x : α) ↦ (μ.rnDeriv ν x).toReal) s ν

Tactic:
integrable_toReal_of_lintegral_ne_top (Measure.measurable_rnDeriv _ _).aemeasurable ?_

Premises used: Measurable.aemeasurable, MeasureTheory.IntegrableOn, MeasureTheory.integrable_toReal_of_lintegral_ne_top, MeasureTheory.Measure.measurable_rnDeriv
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
refine : ∫⁻ (x : α) in s, μ.rnDeriv ν x ∂ν ≠ ∞
⊢ IntegrableOn (ε := ℝ) (fun (x : α) ↦ (μ.rnDeriv ν x).toReal) s ν

Tactic:
refine integrable_toReal_of_lintegral_ne_top (Measure.measurable_rnDeriv _ _).aemeasurable ?_

Premises used: Measurable.aemeasurable, MeasureTheory.integrable_toReal_of_lintegral_ne_top, MeasureTheory.Measure.measurable_rnDeriv
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∫⁻ (x : α) in s, μ.rnDeriv ν x ∂ν ≠ ∞

Tactic:
((setLIntegral_rnDeriv_le _).trans_lt hμs.lt_top).ne

Premises used: Ne.lt_top, LE.le.trans_lt, MeasureTheory.Measure.setLIntegral_rnDeriv_le, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∫⁻ (x : α) in s, μ.rnDeriv ν x ∂ν ≠ ∞

Tactic:
exact ((setLIntegral_rnDeriv_le _).trans_lt hμs.lt_top).ne

Premises used: Ne.lt_top, LE.le.trans_lt, MeasureTheory.Measure.setLIntegral_rnDeriv_le, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
s : Set α
hs : MeasurableSet s
rw : (∫⁻ (a : α) in s, μ.rnDeriv ν a ∂ν).toReal = ENNReal.toReal ((ν.withDensity (μ.rnDeriv ν) : (a : Set α) → ℝ≥0∞) s)
rw₁ : ∀ᵐ (x : α) ∂ν.restrict s, μ.rnDeriv ν x < ∞
⊢ ∫ (x : α) in s, (μ.rnDeriv ν x).toReal ∂ν = (ν.withDensity (μ.rnDeriv ν)).real s

Tactic:
rw [integral_toReal (Measure.measurable_rnDeriv _ _).aemeasurable, measureReal_def]

Premises used: Measurable.aemeasurable, MeasureTheory.measureReal_def, MeasureTheory.Measure.measurable_rnDeriv, MeasureTheory.integral_toReal
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
s : Set α
hs : MeasurableSet s
rw :
  Eq (α := ℝ≥0∞) ((ν.withDensity (μ.rnDeriv ν) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
      ((ν.withDensity (μ.rnDeriv ν) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ∨
    Eq (α := ℝ≥0∞) ((ν.withDensity (μ.rnDeriv ν) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∧
        Eq (α := ℝ≥0∞) ((ν.withDensity (μ.rnDeriv ν) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∨
      Eq (α := ℝ≥0∞) ((ν.withDensity (μ.rnDeriv ν) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∧
        Eq (α := ℝ≥0∞) ((ν.withDensity (μ.rnDeriv ν) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ (∫⁻ (a : α) in s, μ.rnDeriv ν a ∂ν).toReal = ENNReal.toReal ((ν.withDensity (μ.rnDeriv ν) : (a : Set α) → ℝ≥0∞) s)

Tactic:
rw [ENNReal.toReal_eq_toReal_iff, ← withDensity_apply _ hs]

Premises used: ENNReal.toReal_eq_toReal_iff, MeasureTheory.withDensity_apply
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
s : Set α
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((ν.withDensity (μ.rnDeriv ν) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
      ((ν.withDensity (μ.rnDeriv ν) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ∨
    Eq (α := ℝ≥0∞) ((ν.withDensity (μ.rnDeriv ν) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∧
        Eq (α := ℝ≥0∞) ((ν.withDensity (μ.rnDeriv ν) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∨
      Eq (α := ℝ≥0∞) ((ν.withDensity (μ.rnDeriv ν) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∧
        Eq (α := ℝ≥0∞) ((ν.withDensity (μ.rnDeriv ν) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
s : Set α
hs : MeasurableSet s
⊢ ∀ᵐ (x : α) ∂ν.restrict s, μ.rnDeriv ν x < ∞

Tactic:
ae_restrict_of_ae (Measure.rnDeriv_lt_top _ _)

Premises used: MeasureTheory.Measure.rnDeriv_lt_top, MeasureTheory.ae_restrict_of_ae
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
s : Set α
hs : MeasurableSet s
⊢ ∀ᵐ (x : α) ∂ν.restrict s, μ.rnDeriv ν x < ∞

Tactic:
exact ae_restrict_of_ae (Measure.rnDeriv_lt_top _ _)

Premises used: MeasureTheory.Measure.rnDeriv_lt_top, MeasureTheory.ae_restrict_of_ae
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SFinite ν
s : Set α
rw : (∫⁻ (a : α) in s, μ.rnDeriv ν a ∂ν).toReal = ENNReal.toReal ((ν.withDensity (μ.rnDeriv ν) : (a : Set α) → ℝ≥0∞) s)
rw₁ : ∀ᵐ (x : α) ∂ν.restrict s, μ.rnDeriv ν x < ∞
⊢ ∫ (x : α) in s, (μ.rnDeriv ν x).toReal ∂ν = (ν.withDensity (μ.rnDeriv ν)).real s

Tactic:
rw [integral_toReal (Measure.measurable_rnDeriv _ _).aemeasurable, measureReal_def]

Premises used: Measurable.aemeasurable, MeasureTheory.measureReal_def, MeasureTheory.Measure.measurable_rnDeriv, MeasureTheory.integral_toReal
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SFinite ν
s : Set α
rw :
  Eq (α := ℝ≥0∞) ((ν.withDensity (μ.rnDeriv ν) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
      ((ν.withDensity (μ.rnDeriv ν) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ∨
    Eq (α := ℝ≥0∞) ((ν.withDensity (μ.rnDeriv ν) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∧
        Eq (α := ℝ≥0∞) ((ν.withDensity (μ.rnDeriv ν) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∨
      Eq (α := ℝ≥0∞) ((ν.withDensity (μ.rnDeriv ν) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∧
        Eq (α := ℝ≥0∞) ((ν.withDensity (μ.rnDeriv ν) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ (∫⁻ (a : α) in s, μ.rnDeriv ν a ∂ν).toReal = ENNReal.toReal ((ν.withDensity (μ.rnDeriv ν) : (a : Set α) → ℝ≥0∞) s)

Tactic:
rw [ENNReal.toReal_eq_toReal_iff, ← withDensity_apply' _ s]

Premises used: ENNReal.toReal_eq_toReal_iff, MeasureTheory.withDensity_apply'
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SFinite ν
s : Set α
⊢ Eq (α := ℝ≥0∞) ((ν.withDensity (μ.rnDeriv ν) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
      ((ν.withDensity (μ.rnDeriv ν) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ∨
    Eq (α := ℝ≥0∞) ((ν.withDensity (μ.rnDeriv ν) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∧
        Eq (α := ℝ≥0∞) ((ν.withDensity (μ.rnDeriv ν) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∨
      Eq (α := ℝ≥0∞) ((ν.withDensity (μ.rnDeriv ν) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∧
        Eq (α := ℝ≥0∞) ((ν.withDensity (μ.rnDeriv ν) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SFinite ν
s : Set α
⊢ ∀ᵐ (x : α) ∂ν.restrict s, μ.rnDeriv ν x < ∞

Tactic:
ae_restrict_of_ae (Measure.rnDeriv_lt_top _ _)

Premises used: MeasureTheory.Measure.rnDeriv_lt_top, MeasureTheory.ae_restrict_of_ae
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SFinite ν
s : Set α
⊢ ∀ᵐ (x : α) ∂ν.restrict s, μ.rnDeriv ν x < ∞

Tactic:
exact ae_restrict_of_ae (Measure.rnDeriv_lt_top _ _)

Premises used: MeasureTheory.Measure.rnDeriv_lt_top, MeasureTheory.ae_restrict_of_ae
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
s : Set α
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ let t := toMeasurable μ s;
  t = toMeasurable μ s

Tactic:
set t := toMeasurable μ s with ht

Premises used: MeasureTheory.toMeasurable
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
s : Set α
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
t : Set α := toMeasurable μ s
ht : t = toMeasurable μ s
⊢ MeasurableSet t

Tactic:
have ht_m : MeasurableSet t := measurableSet_toMeasurable μ s
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
s : Set α
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
t : Set α := toMeasurable μ s
ht : t = toMeasurable μ s
ht_m : MeasurableSet t
rwa : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ s) : ℝ≥0∞) (∞ : ℝ≥0∞)
rwa₁ rwa₂ rwa₃ rwa₄ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
rwa [ht, measure_toMeasurable s]

Premises used: MeasureTheory.measure_toMeasurable
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
s : Set α
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
t : Set α := toMeasurable μ s
ht : t = toMeasurable μ s
ht_m : MeasurableSet t
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
have hμt : μ t ≠ ∞ := by rwa [ht, measure_toMeasurable s]
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
s : Set α
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
t : Set α := toMeasurable μ s
ht : t = toMeasurable μ s
ht_m : MeasurableSet t
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ LE.le (α := ℝ) (∫ (x : α) in s, (μ.rnDeriv ν x).toReal ∂ν) (∫ (x : α) in t, (μ.rnDeriv ν x).toReal ∂ν)

Tactic:
setIntegral_mono_set ?_ ?_ (HasSubset.Subset.eventuallyLE (subset_toMeasurable _ _))

Premises used: MeasureTheory.setIntegral_mono_set, HasSubset.Subset.eventuallyLE, MeasureTheory.subset_toMeasurable
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
s : Set α
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
t : Set α := toMeasurable μ s
ht : t = toMeasurable μ s
ht_m : MeasurableSet t
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
refine_1 : IntegrableOn (ε := ℝ) (fun (x : α) ↦ (μ.rnDeriv ν x).toReal) t ν
refine_2 : (ae (ν.restrict t)).EventuallyLE (β := ℝ) 0 fun (x : α) ↦ (μ.rnDeriv ν x).toReal
⊢ LE.le (α := ℝ) (∫ (x : α) in s, (μ.rnDeriv ν x).toReal ∂ν) (∫ (x : α) in t, (μ.rnDeriv ν x).toReal ∂ν)

Tactic:
refine setIntegral_mono_set ?_ ?_ (HasSubset.Subset.eventuallyLE (subset_toMeasurable _ _))

Premises used: MeasureTheory.setIntegral_mono_set, HasSubset.Subset.eventuallyLE, MeasureTheory.subset_toMeasurable
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
s : Set α
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
t : Set α := toMeasurable μ s
ht : t = toMeasurable μ s
ht_m : MeasurableSet t
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ IntegrableOn (ε := ℝ) (fun (x : α) ↦ (μ.rnDeriv ν x).toReal) t ν

Tactic:
integrableOn_toReal_rnDeriv hμt

Premises used: MeasureTheory.Measure.integrableOn_toReal_rnDeriv
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
s : Set α
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
t : Set α := toMeasurable μ s
ht : t = toMeasurable μ s
ht_m : MeasurableSet t
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ IntegrableOn (ε := ℝ) (fun (x : α) ↦ (μ.rnDeriv ν x).toReal) t ν

Tactic:
exact integrableOn_toReal_rnDeriv hμt

Premises used: MeasureTheory.Measure.integrableOn_toReal_rnDeriv
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
s : Set α
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
t : Set α := toMeasurable μ s
ht : t = toMeasurable μ s
ht_m : MeasurableSet t
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∀ (a : α), LE.le (α := ℝ) (0 a) ((fun (x : α) ↦ (μ.rnDeriv ν x).toReal) a)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
s : Set α
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
t : Set α := toMeasurable μ s
ht : t = toMeasurable μ s
ht_m : MeasurableSet t
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ (ae (ν.restrict t)).EventuallyLE (β := ℝ) 0 fun (x : α) ↦ (μ.rnDeriv ν x).toReal

Tactic:
exact ae_of_all _ (by simp)

Premises used: MeasureTheory.ae_of_all
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
s : Set α
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
t : Set α := toMeasurable μ s
ht : t = toMeasurable μ s
ht_m : MeasurableSet t
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∫ (x : α) in t, (μ.rnDeriv ν x).toReal ∂ν = (ν.withDensity (μ.rnDeriv ν)).real t

Tactic:
setIntegral_toReal_rnDeriv_eq_withDensity' ht_m

Premises used: MeasureTheory.Measure.setIntegral_toReal_rnDeriv_eq_withDensity'
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
s : Set α
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
t : Set α := toMeasurable μ s
ht : t = toMeasurable μ s
ht_m : MeasurableSet t
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
h : ν.withDensity (μ.rnDeriv ν) ≤ μ
⊢ ENNReal.toReal ((ν.withDensity (μ.rnDeriv ν) : (a : Set α) → ℝ≥0∞) t) ≤ ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) t)

Tactic:
gcongr
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
s : Set α
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
t : Set α := toMeasurable μ s
ht : t = toMeasurable μ s
ht_m : MeasurableSet t
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ν.withDensity (μ.rnDeriv ν) ≤ μ

Tactic:
apply withDensity_rnDeriv_le

Premises used: MeasureTheory.Measure.withDensity_rnDeriv_le
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
s : Set α
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
t : Set α := toMeasurable μ s
ht : t = toMeasurable μ s
ht_m : MeasurableSet t
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
rw : ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) t) = μ.real s
rw₁ : ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) t) = ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) s)
rw₂ rw₃ : ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) s) = ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) s)
⊢ μ.real t = μ.real s

Tactic:
rw [measureReal_def, measureReal_def, measure_toMeasurable s]

Premises used: MeasureTheory.measure_toMeasurable, MeasureTheory.measureReal_def
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
s : Set α
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
t : Set α := toMeasurable μ s
ht : t = toMeasurable μ s
ht_m : MeasurableSet t
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
calc : LE.le (α := ℝ) (∫ (x : α) in s, (μ.rnDeriv ν x).toReal ∂ν) (∫ (x : α) in t, (μ.rnDeriv ν x).toReal ∂ν)
calc₁ : (ν.withDensity (μ.rnDeriv ν)).real t ≤ μ.real t
calc₂ : μ.real t = μ.real s
⊢ ∫ (x : α) in s, (μ.rnDeriv ν x).toReal ∂ν ≤ μ.real s

Tactic:
calc ∫ x in s, (μ.rnDeriv ν x).toReal ∂ν
    ≤ ∫ x in t, (μ.rnDeriv ν x).toReal ∂ν := by
        refine setIntegral_mono_set ?_ ?_ (HasSubset.Subset.eventuallyLE (subset_toMeasurable _ _))
        · exact integrableOn_toReal_rnDeriv hμt
        · exact ae_of_all _ (by simp)
  _ = (withDensity ν (rnDeriv μ ν)).real t := setIntegral_toReal_rnDeriv_eq_withDensity' ht_m
  _ ≤ μ.real t := by
        simp only [measureReal_def]
        gcongr
        apply withDensity_rnDeriv_le
  _ = μ.real s := by rw [measureReal_def, measureReal_def, measure_toMeasurable s]

Premises used: MeasureTheory.Measure.withDensity, MeasureTheory.Measure.real, MeasureTheory.Measure.rnDeriv, MeasureTheory.Measure.setIntegral_toReal_rnDeriv_eq_withDensity'
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
s : Set α
hs : MeasurableSet s
rw : (ν.withDensity (μ.rnDeriv ν)).real s = μ.real s
rw₁ : μ.real s = μ.real s
rw₂ rw₃ : ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) s) = ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) s)
⊢ ∫ (x : α) in s, (μ.rnDeriv ν x).toReal ∂ν = μ.real s

Tactic:
rw [setIntegral_toReal_rnDeriv_eq_withDensity' hs, Measure.withDensity_rnDeriv_eq _ _ hμν,
    measureReal_def]

Premises used: MeasureTheory.Measure.setIntegral_toReal_rnDeriv_eq_withDensity', MeasureTheory.measureReal_def, MeasureTheory.Measure.withDensity_rnDeriv_eq
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
s : Set α
rw : (ν.withDensity (μ.rnDeriv ν)).real s = μ.real s
rw₁ rw₂ : μ.real s = μ.real s
⊢ ∫ (x : α) in s, (μ.rnDeriv ν x).toReal ∂ν = μ.real s

Tactic:
rw [setIntegral_toReal_rnDeriv_eq_withDensity s, Measure.withDensity_rnDeriv_eq _ _ hμν]

Premises used: MeasureTheory.Measure.setIntegral_toReal_rnDeriv_eq_withDensity, MeasureTheory.Measure.withDensity_rnDeriv_eq
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
rw : ∫ (x : α) in Set.univ, (μ.rnDeriv ν x).toReal ∂ν = μ.real Set.univ
rw₁ rw₂ : μ.real Set.univ = μ.real Set.univ
⊢ ∫ (x : α), (μ.rnDeriv ν x).toReal ∂ν = μ.real Set.univ

Tactic:
rw [← setIntegral_univ, setIntegral_toReal_rnDeriv hμν Set.univ]

Premises used: Set.univ, MeasureTheory.Measure.setIntegral_toReal_rnDeriv, MeasureTheory.setIntegral_univ