case refine'_1
α : Type u_1
inst✝ : MeasurableSpace α
m μ : OuterMeasure α
s : Set α
hs : MeasurableSet s
t : Set α
⊢ ↑(trim (↑(restrict s) μ)) t ≤ ↑(↑(restrict s) (trim μ)) t

case refine'_2
α : Type u_1
inst✝ : MeasurableSpace α
m μ : OuterMeasure α
s : Set α
hs : MeasurableSet s
t : Set α
ht : MeasurableSet t
⊢ ↑(↑(restrict s) (trim μ)) t ≤ ↑(↑(restrict s) μ) t
α : Type u_1
inst✝ : MeasurableSpace α
m μ : OuterMeasure α
s : Set α
hs : MeasurableSet s
⊢ trim (↑(restrict s) μ) = ↑(restrict s) (trim μ)
refine' le_antisymm (fun t => _) (le_trim_iff.2 fun t ht => _)
case refine'_1
α : Type u_1
inst✝ : MeasurableSpace α
m μ : OuterMeasure α
s : Set α
hs : MeasurableSet s
t : Set α
⊢ ↑(trim (↑(restrict s) μ)) t ≤ ↑(trim μ) (t ∩ s)
case refine'_1
α : Type u_1
inst✝ : MeasurableSpace α
m μ : OuterMeasure α
s : Set α
hs : MeasurableSet s
t : Set α
⊢ ↑(trim (↑(restrict s) μ)) t ≤ ↑(↑(restrict s) (trim μ)) t
rw [restrict_apply]
case refine'_1.intro.intro.intro
α : Type u_1
inst✝ : MeasurableSpace α
m μ : OuterMeasure α
s : Set α
hs : MeasurableSet s
t t' : Set α
htt' : t ∩ s ⊆ t'
ht' : MeasurableSet t'
hμt' : ↑μ t' = ↑(trim μ) (t ∩ s)
⊢ ↑(trim (↑(restrict s) μ)) t ≤ ↑(trim μ) (t ∩ s)
case refine'_1
α : Type u_1
inst✝ : MeasurableSpace α
m μ : OuterMeasure α
s : Set α
hs : MeasurableSet s
t : Set α
⊢ ↑(trim (↑(restrict s) μ)) t ≤ ↑(trim μ) (t ∩ s)
rcases μ.exists_measurable_superset_eq_trim (t ∩ s) with ⟨t', htt', ht', hμt'⟩
case refine'_1.intro.intro.intro
α : Type u_1
inst✝ : MeasurableSpace α
m μ : OuterMeasure α
s : Set α
hs : MeasurableSet s
t t' : Set α
htt' : t ∩ s ⊆ t'
ht' : MeasurableSet t'
hμt' : ↑μ t' = ↑(trim μ) (t ∩ s)
⊢ ↑(trim (↑(restrict s) μ)) t ≤ ↑μ t'
case refine'_1.intro.intro.intro
α : Type u_1
inst✝ : MeasurableSpace α
m μ : OuterMeasure α
s : Set α
hs : MeasurableSet s
t t' : Set α
htt' : t ∩ s ⊆ t'
ht' : MeasurableSet t'
hμt' : ↑μ t' = ↑(trim μ) (t ∩ s)
⊢ ↑(trim (↑(restrict s) μ)) t ≤ ↑(trim μ) (t ∩ s)
rw [← hμt']
case refine'_1.intro.intro.intro
α : Type u_1
inst✝ : MeasurableSpace α
m μ : OuterMeasure α
s : Set α
hs : MeasurableSet s
t t' : Set α
htt' : t ⊆ sᶜ ∪ t'
ht' : MeasurableSet t'
hμt' : ↑μ t' = ↑(trim μ) (t ∩ s)
⊢ ↑(trim (↑(restrict s) μ)) t ≤ ↑μ t'
case refine'_1.intro.intro.intro
α : Type u_1
inst✝ : MeasurableSpace α
m μ : OuterMeasure α
s : Set α
hs : MeasurableSet s
t t' : Set α
htt' : t ∩ s ⊆ t'
ht' : MeasurableSet t'
hμt' : ↑μ t' = ↑(trim μ) (t ∩ s)
⊢ ↑(trim (↑(restrict s) μ)) t ≤ ↑μ t'
rw [inter_subset] at htt'
case refine'_1.intro.intro.intro
α : Type u_1
inst✝ : MeasurableSpace α
m μ : OuterMeasure α
s : Set α
hs : MeasurableSet s
t t' : Set α
htt' : t ⊆ sᶜ ∪ t'
ht' : MeasurableSet t'
hμt' : ↑μ t' = ↑(trim μ) (t ∩ s)
⊢ ↑(trim (↑(restrict s) μ)) (sᶜ ∪ t') ≤ ↑μ t'
case refine'_1.intro.intro.intro
α : Type u_1
inst✝ : MeasurableSpace α
m μ : OuterMeasure α
s : Set α
hs : MeasurableSet s
t t' : Set α
htt' : t ⊆ sᶜ ∪ t'
ht' : MeasurableSet t'
hμt' : ↑μ t' = ↑(trim μ) (t ∩ s)
⊢ ↑(trim (↑(restrict s) μ)) t ≤ ↑μ t'
refine' (mono' _ htt').trans _
case refine'_1.intro.intro.intro
α : Type u_1
inst✝ : MeasurableSpace α
m μ : OuterMeasure α
s : Set α
hs : MeasurableSet s
t t' : Set α
htt' : t ⊆ sᶜ ∪ t'
ht' : MeasurableSet t'
hμt' : ↑μ t' = ↑(trim μ) (t ∩ s)
⊢ ↑μ (t' ∩ s) ≤ ↑μ t'
case refine'_1.intro.intro.intro
α : Type u_1
inst✝ : MeasurableSpace α
m μ : OuterMeasure α
s : Set α
hs : MeasurableSet s
t t' : Set α
htt' : t ⊆ sᶜ ∪ t'
ht' : MeasurableSet t'
hμt' : ↑μ t' = ↑(trim μ) (t ∩ s)
⊢ ↑(trim (↑(restrict s) μ)) (sᶜ ∪ t') ≤ ↑μ t'
rw [trim_eq _ (hs.compl.union ht'), restrict_apply, union_inter_distrib_right, compl_inter_self,
  Set.empty_union]
no goals
case refine'_1.intro.intro.intro
α : Type u_1
inst✝ : MeasurableSpace α
m μ : OuterMeasure α
s : Set α
hs : MeasurableSet s
t t' : Set α
htt' : t ⊆ sᶜ ∪ t'
ht' : MeasurableSet t'
hμt' : ↑μ t' = ↑(trim μ) (t ∩ s)
⊢ ↑μ (t' ∩ s) ≤ ↑μ t'
exact μ.mono' (inter_subset_left _ _)
no goals
case refine'_2
α : Type u_1
inst✝ : MeasurableSpace α
m μ : OuterMeasure α
s : Set α
hs : MeasurableSet s
t : Set α
ht : MeasurableSet t
⊢ ↑(↑(restrict s) (trim μ)) t ≤ ↑(↑(restrict s) μ) t
rw [restrict_apply, trim_eq _ (ht.inter hs), restrict_apply]