α : Type u_2
β✝ : Type ?u.902392
γ : Type ?u.902395
δ : Type ?u.902398
m : MeasurableSpace α
μ ν : Measure α
β : Type u_1
inst✝ : MeasurableSpace β
μ' : Measure β
f : α →ₛ ℝ≥0∞
g : β →ₛ ℝ≥0∞
m' : α → β
eq : ∀ (a : α), ↑f a = ↑g (m' a)
h : ∀ (s : Set β), MeasurableSet s → ↑↑μ' s = ↑↑μ (m' ⁻¹' s)
y : ℝ≥0∞
⊢ ↑↑μ {x | ↑g (m' x) ∈ {y}} = ↑↑μ' {x | ↑g x ∈ {y}}
α : Type u_2
β✝ : Type ?u.902392
γ : Type ?u.902395
δ : Type ?u.902398
m : MeasurableSpace α
μ ν : Measure α
β : Type u_1
inst✝ : MeasurableSpace β
μ' : Measure β
f : α →ₛ ℝ≥0∞
g : β →ₛ ℝ≥0∞
m' : α → β
eq : ∀ (a : α), ↑f a = ↑g (m' a)
h : ∀ (s : Set β), MeasurableSet s → ↑↑μ' s = ↑↑μ (m' ⁻¹' s)
y : ℝ≥0∞
⊢ ↑↑μ (↑f ⁻¹' {y}) = ↑↑μ' (↑g ⁻¹' {y})
simp only [preimage, eq]
no goals
α : Type u_2
β✝ : Type ?u.902392
γ : Type ?u.902395
δ : Type ?u.902398
m : MeasurableSpace α
μ ν : Measure α
β : Type u_1
inst✝ : MeasurableSpace β
μ' : Measure β
f : α →ₛ ℝ≥0∞
g : β →ₛ ℝ≥0∞
m' : α → β
eq : ∀ (a : α), ↑f a = ↑g (m' a)
h : ∀ (s : Set β), MeasurableSet s → ↑↑μ' s = ↑↑μ (m' ⁻¹' s)
y : ℝ≥0∞
⊢ ↑↑μ {x | ↑g (m' x) ∈ {y}} = ↑↑μ' {x | ↑g x ∈ {y}}
exact (h (g ⁻¹' {y}) (g.measurableSet_preimage _)).symm