case intro.intro.intro
α : Type u_1
β : Type ?u.575568
γ : Type ?u.575571
δ : Type ?u.575574
ι : Type ?u.575577
R : Type ?u.575580
R' : Type ?u.575583
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t✝ : Set α
hs : NullMeasurableSet s
t : Set α
hts : t ⊆ s
htm : MeasurableSet t
ht_eq : t =ᶠ[ae μ] s
⊢ ∀ᵐ (x : α) ∂Measure.restrict μ s, x ∈ s
α : Type u_1
β : Type ?u.575568
γ : Type ?u.575571
δ : Type ?u.575574
ι : Type ?u.575577
R : Type ?u.575580
R' : Type ?u.575583
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
hs : NullMeasurableSet s
⊢ ∀ᵐ (x : α) ∂Measure.restrict μ s, x ∈ s
rcases hs.exists_measurable_subset_ae_eq with ⟨t, hts, htm, ht_eq⟩
case intro.intro.intro
α : Type u_1
β : Type ?u.575568
γ : Type ?u.575571
δ : Type ?u.575574
ι : Type ?u.575577
R : Type ?u.575580
R' : Type ?u.575583
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t✝ : Set α
hs : NullMeasurableSet s
t : Set α
hts : t ⊆ s
htm : MeasurableSet t
ht_eq : t =ᶠ[ae μ] s
⊢ ∀ᵐ (x : α) ∂Measure.restrict μ t, x ∈ s
case intro.intro.intro
α : Type u_1
β : Type ?u.575568
γ : Type ?u.575571
δ : Type ?u.575574
ι : Type ?u.575577
R : Type ?u.575580
R' : Type ?u.575583
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t✝ : Set α
hs : NullMeasurableSet s
t : Set α
hts : t ⊆ s
htm : MeasurableSet t
ht_eq : t =ᶠ[ae μ] s
⊢ ∀ᵐ (x : α) ∂Measure.restrict μ s, x ∈ s
rw [← restrict_congr_set ht_eq]
no goals
case intro.intro.intro
α : Type u_1
β : Type ?u.575568
γ : Type ?u.575571
δ : Type ?u.575574
ι : Type ?u.575577
R : Type ?u.575580
R' : Type ?u.575583
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t✝ : Set α
hs : NullMeasurableSet s
t : Set α
hts : t ⊆ s
htm : MeasurableSet t
ht_eq : t =ᶠ[ae μ] s
⊢ ∀ᵐ (x : α) ∂Measure.restrict μ t, x ∈ s
exact (ae_restrict_mem htm).mono hts