case intro.intro
ι : Type ?u.5762
α : Type u_1
β : Type ?u.5768
γ : Type ?u.5771
m0 : MeasurableSpace α
μ : Measure α
s t✝ t : Set α
htm : MeasurableSet t
hst : s =ᵐ[μ] t
⊢ ∃ t x, MeasurableSet t ∧ t =ᵐ[μ] s
ι : Type ?u.5762
α : Type u_1
β : Type ?u.5768
γ : Type ?u.5771
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
h : NullMeasurableSet s
⊢ ∃ t x, MeasurableSet t ∧ t =ᵐ[μ] s
rcases h with ⟨t, htm, hst⟩
case intro.intro.refine'_1
ι : Type ?u.5762
α : Type u_1
β : Type ?u.5768
γ : Type ?u.5771
m0 : MeasurableSpace α
μ : Measure α
s t✝ t : Set α
htm : MeasurableSet t
hst : s =ᵐ[μ] t
⊢ t ∪ toMeasurable μ (s \ t) ⊇ s

case intro.intro.refine'_2
ι : Type ?u.5762
α : Type u_1
β : Type ?u.5768
γ : Type ?u.5771
m0 : MeasurableSpace α
μ : Measure α
s t✝ t : Set α
htm : MeasurableSet t
hst : s =ᵐ[μ] t
⊢ t ∪ toMeasurable μ (s \ t) =ᵐ[μ] s
case intro.intro
ι : Type ?u.5762
α : Type u_1
β : Type ?u.5768
γ : Type ?u.5771
m0 : MeasurableSpace α
μ : Measure α
s t✝ t : Set α
htm : MeasurableSet t
hst : s =ᵐ[μ] t
⊢ ∃ t x, MeasurableSet t ∧ t =ᵐ[μ] s
refine' ⟨t ∪ toMeasurable μ (s \ t), _, htm.union (measurableSet_toMeasurable _ _), _⟩
no goals
case intro.intro.refine'_1
ι : Type ?u.5762
α : Type u_1
β : Type ?u.5768
γ : Type ?u.5771
m0 : MeasurableSpace α
μ : Measure α
s t✝ t : Set α
htm : MeasurableSet t
hst : s =ᵐ[μ] t
⊢ t ∪ toMeasurable μ (s \ t) ⊇ s
exact diff_subset_iff.1 (subset_toMeasurable _ _)
case intro.intro.refine'_2
ι : Type ?u.5762
α : Type u_1
β : Type ?u.5768
γ : Type ?u.5771
m0 : MeasurableSpace α
μ : Measure α
s t✝ t : Set α
htm : MeasurableSet t
hst : s =ᵐ[μ] t
this : toMeasurable μ (s \ t) =ᵐ[μ] ∅
⊢ t ∪ toMeasurable μ (s \ t) =ᵐ[μ] s
case intro.intro.refine'_2
ι : Type ?u.5762
α : Type u_1
β : Type ?u.5768
γ : Type ?u.5771
m0 : MeasurableSpace α
μ : Measure α
s t✝ t : Set α
htm : MeasurableSet t
hst : s =ᵐ[μ] t
⊢ t ∪ toMeasurable μ (s \ t) =ᵐ[μ] s
have : toMeasurable μ (s \ t) =ᵐ[μ] (∅ : Set α) := by simp [ae_le_set.1 hst.le]
no goals
case intro.intro.refine'_2
ι : Type ?u.5762
α : Type u_1
β : Type ?u.5768
γ : Type ?u.5771
m0 : MeasurableSpace α
μ : Measure α
s t✝ t : Set α
htm : MeasurableSet t
hst : s =ᵐ[μ] t
this : toMeasurable μ (s \ t) =ᵐ[μ] ∅
⊢ t ∪ toMeasurable μ (s \ t) =ᵐ[μ] s
simpa only [union_empty] using hst.symm.union this
no goals
ι : Type ?u.5762
α : Type u_1
β : Type ?u.5768
γ : Type ?u.5771
m0 : MeasurableSpace α
μ : Measure α
s t✝ t : Set α
htm : MeasurableSet t
hst : s =ᵐ[μ] t
⊢ toMeasurable μ (s \ t) =ᵐ[μ] ∅
simp [ae_le_set.1 hst.le]