-- Mathlib/MeasureTheory/Decomposition/RadonNikodym.lean
lemma setIntegral_toReal_rnDeriv_le [SigmaFinite μ] {s : Set α} (hμs : μ s ≠ ∞) :
    ∫ x in s, (μ.rnDeriv ν x).toReal ∂ν ≤ (μ s).toReal

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : SigmaFinite μ
s : Set α
hμs : μ s ≠ ⊤
t : Set α := toMeasurable μ s
ht : t = toMeasurable μ s
ht_m : MeasurableSet t
hμt : μ t ≠ ⊤
⊢ ((ν.withDensity (μ.rnDeriv ν)) t).toReal ≤ (μ t).toReal

Tactic:
gcongr

Result:
case hb
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : SigmaFinite μ
s : Set α
hμs : μ s ≠ ⊤
t : Set α := toMeasurable μ s
ht : t = toMeasurable μ s
ht_m : MeasurableSet t
hμt : μ t ≠ ⊤
⊢ μ t ≠ ⊤

case h
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : SigmaFinite μ
s : Set α
hμs : μ s ≠ ⊤
t : Set α := toMeasurable μ s
ht : t = toMeasurable μ s
ht_m : MeasurableSet t
hμt : μ t ≠ ⊤
⊢ (ν.withDensity (μ.rnDeriv ν)) t ≤ μ t

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : SigmaFinite μ
s : Set α
hμs : μ s ≠ ⊤
t : Set α := toMeasurable μ s
ht : t = toMeasurable μ s
⊢ ∫ (x : α) in s, (μ.rnDeriv ν x).toReal ∂ν ≤ (μ s).toReal

Tactic:
have ht_m : MeasurableSet t := measurableSet_toMeasurable μ s

Result:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : SigmaFinite μ
s : Set α
hμs : μ s ≠ ⊤
t : Set α := toMeasurable μ s
ht : t = toMeasurable μ s
ht_m : MeasurableSet t
⊢ ∫ (x : α) in s, (μ.rnDeriv ν x).toReal ∂ν ≤ (μ s).toReal

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : SigmaFinite μ
s : Set α
hμs : μ s ≠ ⊤
t : Set α := toMeasurable μ s
ht : t = toMeasurable μ s
ht_m : MeasurableSet t
hμt : μ t ≠ ⊤
⊢ ∫ (x : α) in s, (μ.rnDeriv ν x).toReal ∂ν ≤ ∫ (x : α) in t, (μ.rnDeriv ν x).toReal ∂ν

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

Result:
case refine_1
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : SigmaFinite μ
s : Set α
hμs : μ s ≠ ⊤
t : Set α := toMeasurable μ s
ht : t = toMeasurable μ s
ht_m : MeasurableSet t
hμt : μ t ≠ ⊤
⊢ IntegrableOn (fun x => (μ.rnDeriv ν x).toReal) t ν

case refine_2
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : SigmaFinite μ
s : Set α
hμs : μ s ≠ ⊤
t : Set α := toMeasurable μ s
ht : t = toMeasurable μ s
ht_m : MeasurableSet t
hμt : μ t ≠ ⊤
⊢ 0 ≤ᶠ[ae (ν.restrict t)] fun x => (μ.rnDeriv ν x).toReal

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : SigmaFinite μ
s : Set α
hμs : μ s ≠ ⊤
t : Set α := toMeasurable μ s
ht : t = toMeasurable μ s
ht_m : MeasurableSet t
hμt : μ t ≠ ⊤
⊢ (μ t).toReal = (μ s).toReal

Tactic:
rw [measure_toMeasurable s]

Result:
no goals

Proof state:
case refine_1
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : SigmaFinite μ
s : Set α
hμs : μ s ≠ ⊤
t : Set α := toMeasurable μ s
ht : t = toMeasurable μ s
ht_m : MeasurableSet t
hμt : μ t ≠ ⊤
⊢ IntegrableOn (fun x => (μ.rnDeriv ν x).toReal) t ν

Tactic:
exact integrableOn_toReal_rnDeriv hμt

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : SigmaFinite μ
s : Set α
hμs : μ s ≠ ⊤
t : Set α := toMeasurable μ s
ht : t = toMeasurable μ s
ht_m : MeasurableSet t
hμt : μ t ≠ ⊤
⊢ ∀ (a : α), 0 a ≤ (fun x => (μ.rnDeriv ν x).toReal) a

Tactic:
simp

Result:
no goals

Proof state:
case hb
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : SigmaFinite μ
s : Set α
hμs : μ s ≠ ⊤
t : Set α := toMeasurable μ s
ht : t = toMeasurable μ s
ht_m : MeasurableSet t
hμt : μ t ≠ ⊤
⊢ μ t ≠ ⊤

Tactic:
exact hμt

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : SigmaFinite μ
s : Set α
hμs : μ s ≠ ⊤
t : Set α := toMeasurable μ s
ht : t = toMeasurable μ s
ht_m : MeasurableSet t
⊢ ∫ (x : α) in s, (μ.rnDeriv ν x).toReal ∂ν ≤ (μ s).toReal

Tactic:
have hμt : μ t ≠ ∞ := by rwa [ht, measure_toMeasurable s]

Result:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : SigmaFinite μ
s : Set α
hμs : μ s ≠ ⊤
t : Set α := toMeasurable μ s
ht : t = toMeasurable μ s
ht_m : MeasurableSet t
hμt : μ t ≠ ⊤
⊢ ∫ (x : α) in s, (μ.rnDeriv ν x).toReal ∂ν ≤ (μ s).toReal

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : SigmaFinite μ
s : Set α
hμs : μ s ≠ ⊤
⊢ ∫ (x : α) in s, (μ.rnDeriv ν x).toReal ∂ν ≤ (μ s).toReal

Tactic:
set t := toMeasurable μ s with ht

Result:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : SigmaFinite μ
s : Set α
hμs : μ s ≠ ⊤
t : Set α := toMeasurable μ s
ht : t = toMeasurable μ s
⊢ ∫ (x : α) in s, (μ.rnDeriv ν x).toReal ∂ν ≤ (μ s).toReal

Proof state:
case refine_2
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : SigmaFinite μ
s : Set α
hμs : μ s ≠ ⊤
t : Set α := toMeasurable μ s
ht : t = toMeasurable μ s
ht_m : MeasurableSet t
hμt : μ t ≠ ⊤
⊢ 0 ≤ᶠ[ae (ν.restrict t)] fun x => (μ.rnDeriv ν x).toReal

Tactic:
exact ae_of_all _ (by simp)

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : SigmaFinite μ
s : Set α
hμs : μ s ≠ ⊤
t : Set α := toMeasurable μ s
ht : t = toMeasurable μ s
ht_m : MeasurableSet t
⊢ μ t ≠ ⊤

Tactic:
rwa [ht, measure_toMeasurable s]

Result:
no goals

Proof state:
case h
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : SigmaFinite μ
s : Set α
hμs : μ s ≠ ⊤
t : Set α := toMeasurable μ s
ht : t = toMeasurable μ s
ht_m : MeasurableSet t
hμt : μ t ≠ ⊤
⊢ (ν.withDensity (μ.rnDeriv ν)) t ≤ μ t

Tactic:
apply withDensity_rnDeriv_le

Result:
no goals