ι : Type ?u.6547
α : Type u_1
β : Type ?u.6553
γ : Type ?u.6556
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
h : NullMeasurableSet s
⊢ Exists.choose ?hc =ᵐ[μ] s

case hc
ι : Type ?u.6547
α : Type u_1
β : Type ?u.6553
γ : Type ?u.6556
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
h : NullMeasurableSet s
⊢ ∃ t x, MeasurableSet t ∧ t =ᵐ[μ] s
ι : Type ?u.6547
α : Type u_1
β : Type ?u.6553
γ : Type ?u.6556
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
h : NullMeasurableSet s
⊢ toMeasurable μ s =ᵐ[μ] s
rw [toMeasurable_def, dif_pos]
no goals
ι : Type ?u.6547
α : Type u_1
β : Type ?u.6553
γ : Type ?u.6556
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
h : NullMeasurableSet s
⊢ Exists.choose ?hc =ᵐ[μ] s

case hc
ι : Type ?u.6547
α : Type u_1
β : Type ?u.6553
γ : Type ?u.6556
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
h : NullMeasurableSet s
⊢ ∃ t x, MeasurableSet t ∧ t =ᵐ[μ] s
exact (exists_measurable_superset_ae_eq h).choose_spec.snd.2