case h
α : Type u_1
β : Type ?u.12666
γ : Type ?u.12669
δ : Type ?u.12672
ι : Type ?u.12675
inst✝ : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s s₁ s₂ t : Set α
hs : MeasurableSet s
⊢ MeasurableSet s
α : Type u_1
β : Type ?u.12666
γ : Type ?u.12669
δ : Type ?u.12672
ι : Type ?u.12675
inst✝ : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s s₁ s₂ t : Set α
hs : MeasurableSet s
⊢ ↑↑μ s = extend (fun t _ht => ↑↑μ t) s
rw [extend_eq]
no goals
case h
α : Type u_1
β : Type ?u.12666
γ : Type ?u.12669
δ : Type ?u.12672
ι : Type ?u.12675
inst✝ : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s s₁ s₂ t : Set α
hs : MeasurableSet s
⊢ MeasurableSet s
exact hs