case h
α : Type u_1
β : Type ?u.1765436
γ : Type ?u.1765439
δ : Type ?u.1765442
m : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
⊢ ↑↑(withDensity μ 1) s = ↑↑μ s
α : Type u_1
β : Type ?u.1765436
γ : Type ?u.1765439
δ : Type ?u.1765442
m : MeasurableSpace α
μ ν : Measure α
⊢ withDensity μ 1 = μ
ext1 s hs
no goals
case h
α : Type u_1
β : Type ?u.1765436
γ : Type ?u.1765439
δ : Type ?u.1765442
m : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
⊢ ↑↑(withDensity μ 1) s = ↑↑μ s
simp [withDensity_apply _ hs]