case refine'_1
ι : Type ?u.14279
α : Type u_1
β : Type ?u.14285
γ : Type ?u.14288
m0 : MeasurableSpace α
μ : Measure α
s✝ t s : Set α
ht : NullMeasurableSet t
⊢ ↑↑μ (s ∩ t) + ↑↑μ (s \ t) ≤ ↑↑μ s

case refine'_2
ι : Type ?u.14279
α : Type u_1
β : Type ?u.14285
γ : Type ?u.14288
m0 : MeasurableSpace α
μ : Measure α
s✝ t s : Set α
ht : NullMeasurableSet t
⊢ ↑↑μ s ≤ ↑↑μ (s ∩ t) + ↑↑μ (s \ t)
ι : Type ?u.14279
α : Type u_1
β : Type ?u.14285
γ : Type ?u.14288
m0 : MeasurableSpace α
μ : Measure α
s✝ t s : Set α
ht : NullMeasurableSet t
⊢ ↑↑μ (s ∩ t) + ↑↑μ (s \ t) = ↑↑μ s
refine' le_antisymm _ _
case refine'_1.intro.intro.intro
ι : Type ?u.14279
α : Type u_1
β : Type ?u.14285
γ : Type ?u.14288
m0 : MeasurableSpace α
μ : Measure α
s✝ t s : Set α
ht : NullMeasurableSet t
s' : Set α
hsub : s ⊆ s'
hs'm : MeasurableSet s'
hs' : ↑↑μ s' = ↑↑μ s
⊢ ↑↑μ (s ∩ t) + ↑↑μ (s \ t) ≤ ↑↑μ s
case refine'_1
ι : Type ?u.14279
α : Type u_1
β : Type ?u.14285
γ : Type ?u.14288
m0 : MeasurableSpace α
μ : Measure α
s✝ t s : Set α
ht : NullMeasurableSet t
⊢ ↑↑μ (s ∩ t) + ↑↑μ (s \ t) ≤ ↑↑μ s
rcases exists_measurable_superset μ s with ⟨s', hsub, hs'm, hs'⟩
case refine'_1.intro.intro.intro
ι : Type ?u.14279
α : Type u_1
β : Type ?u.14285
γ : Type ?u.14288
m0 : MeasurableSpace α
μ : Measure α
s✝ t s : Set α
ht : NullMeasurableSet t
s' : Set α
hsub : s ⊆ s'
hs' : ↑↑μ s' = ↑↑μ s
hs'm : NullMeasurableSet s'
⊢ ↑↑μ (s ∩ t) + ↑↑μ (s \ t) ≤ ↑↑μ s
case refine'_1.intro.intro.intro
ι : Type ?u.14279
α : Type u_1
β : Type ?u.14285
γ : Type ?u.14288
m0 : MeasurableSpace α
μ : Measure α
s✝ t s : Set α
ht : NullMeasurableSet t
s' : Set α
hsub : s ⊆ s'
hs'm : MeasurableSet s'
hs' : ↑↑μ s' = ↑↑μ s
⊢ ↑↑μ (s ∩ t) + ↑↑μ (s \ t) ≤ ↑↑μ s
replace hs'm : NullMeasurableSet s' μ := hs'm.nullMeasurableSet
no goals
case refine'_1.intro.intro.intro
ι : Type ?u.14279
α : Type u_1
β : Type ?u.14285
γ : Type ?u.14288
m0 : MeasurableSpace α
μ : Measure α
s✝ t s : Set α
ht : NullMeasurableSet t
s' : Set α
hsub : s ⊆ s'
hs' : ↑↑μ s' = ↑↑μ s
hs'm : NullMeasurableSet s'
⊢ ↑↑μ (s ∩ t) + ↑↑μ (s \ t) ≤ ↑↑μ s
calc
  μ (s ∩ t) + μ (s \ t) ≤ μ (s' ∩ t) + μ (s' \ t) :=
    add_le_add (measure_mono <| inter_subset_inter_left _ hsub)
      (measure_mono <| diff_subset_diff_left hsub)
  _ = μ (s' ∩ t ∪ s' \ t) :=
    (measure_union₀_aux (hs'm.inter ht) (hs'm.diff ht) <|
        (@disjoint_inf_sdiff _ s' t _).aedisjoint).symm
  _ = μ s' := (congr_arg μ (inter_union_diff _ _))
  _ = μ s := hs'
no goals
case refine'_2
ι : Type ?u.14279
α : Type u_1
β : Type ?u.14285
γ : Type ?u.14288
m0 : MeasurableSpace α
μ : Measure α
s✝ t s : Set α
ht : NullMeasurableSet t
⊢ ↑↑μ s ≤ ↑↑μ (s ∩ t) + ↑↑μ (s \ t)
calc
  μ s = μ (s ∩ t ∪ s \ t) := by rw [inter_union_diff]
  _ ≤ μ (s ∩ t) + μ (s \ t) := measure_union_le _ _
no goals
ι : Type ?u.14279
α : Type u_1
β : Type ?u.14285
γ : Type ?u.14288
m0 : MeasurableSpace α
μ : Measure α
s✝ t s : Set α
ht : NullMeasurableSet t
⊢ ↑↑μ s = ↑↑μ (s ∩ t ∪ s \ t)
rw [inter_union_diff]