α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
⊢ restrict (sInf {d | μ ≤ d + ν}) s = sInf {d | restrict μ s ≤ d + restrict ν s}
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
⊢ restrict (μ - ν) s = restrict μ s - restrict ν s
repeat' rw [sub_def]
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
h_nonempty : Set.Nonempty {d | μ ≤ d + ν}
⊢ restrict (sInf {d | μ ≤ d + ν}) s = sInf {d | restrict μ s ≤ d + restrict ν s}
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
⊢ restrict (sInf {d | μ ≤ d + ν}) s = sInf {d | restrict μ s ≤ d + restrict ν s}
have h_nonempty : { d | μ ≤ d + ν }.Nonempty := ⟨μ, Measure.le_add_right le_rfl⟩
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
h_nonempty : Set.Nonempty {d | μ ≤ d + ν}
⊢ sInf ((fun μ => restrict μ s) '' {d | μ ≤ d + ν}) = sInf {d | restrict μ s ≤ d + restrict ν s}
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
h_nonempty : Set.Nonempty {d | μ ≤ d + ν}
⊢ restrict (sInf {d | μ ≤ d + ν}) s = sInf {d | restrict μ s ≤ d + restrict ν s}
rw [restrict_sInf_eq_sInf_restrict h_nonempty h_meas_s]
case a
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
h_nonempty : Set.Nonempty {d | μ ≤ d + ν}
⊢ sInf ((fun μ => restrict μ s) '' {d | μ ≤ d + ν}) ≤ sInf {d | restrict μ s ≤ d + restrict ν s}

case a
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
h_nonempty : Set.Nonempty {d | μ ≤ d + ν}
⊢ sInf {d | restrict μ s ≤ d + restrict ν s} ≤ sInf ((fun μ => restrict μ s) '' {d | μ ≤ d + ν})
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
h_nonempty : Set.Nonempty {d | μ ≤ d + ν}
⊢ sInf ((fun μ => restrict μ s) '' {d | μ ≤ d + ν}) = sInf {d | restrict μ s ≤ d + restrict ν s}
apply le_antisymm
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
⊢ restrict (sInf {d | μ ≤ d + ν}) s = sInf {d | restrict μ s ≤ d + restrict ν s}
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
⊢ restrict (sInf {d | μ ≤ d + ν}) s = sInf {d | restrict μ s ≤ d + restrict ν s}
rw [sub_def]
case a
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
h_nonempty : Set.Nonempty {d | μ ≤ d + ν}
⊢ ∀ (x : Measure α),
    x ∈ {d | restrict μ s ≤ d + restrict ν s} → ∃ y, y ∈ (fun μ => restrict μ s) '' {d | μ ≤ d + ν} ∧ y ≤ x
case a
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
h_nonempty : Set.Nonempty {d | μ ≤ d + ν}
⊢ sInf ((fun μ => restrict μ s) '' {d | μ ≤ d + ν}) ≤ sInf {d | restrict μ s ≤ d + restrict ν s}
refine' sInf_le_sInf_of_forall_exists_le _
case a
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
h_nonempty : Set.Nonempty {d | μ ≤ d + ν}
ν' : Measure α
h_ν'_in : ν' ∈ {d | restrict μ s ≤ d + restrict ν s}
⊢ ∃ y, y ∈ (fun μ => restrict μ s) '' {d | μ ≤ d + ν} ∧ y ≤ ν'
case a
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
h_nonempty : Set.Nonempty {d | μ ≤ d + ν}
⊢ ∀ (x : Measure α),
    x ∈ {d | restrict μ s ≤ d + restrict ν s} → ∃ y, y ∈ (fun μ => restrict μ s) '' {d | μ ≤ d + ν} ∧ y ≤ x
intro ν' h_ν'_in
case a
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
h_nonempty : Set.Nonempty {d | μ ≤ d + ν}
ν' : Measure α
h_ν'_in : restrict μ s ≤ ν' + restrict ν s
⊢ ∃ y, y ∈ (fun μ => restrict μ s) '' {d | μ ≤ d + ν} ∧ y ≤ ν'
case a
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
h_nonempty : Set.Nonempty {d | μ ≤ d + ν}
ν' : Measure α
h_ν'_in : ν' ∈ {d | restrict μ s ≤ d + restrict ν s}
⊢ ∃ y, y ∈ (fun μ => restrict μ s) '' {d | μ ≤ d + ν} ∧ y ≤ ν'
rw [mem_setOf_eq] at h_ν'_in
case a
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
h_nonempty : Set.Nonempty {d | μ ≤ d + ν}
ν' : Measure α
h_ν'_in : restrict μ s ≤ ν' + restrict ν s
⊢ restrict ν' s ∈ (fun μ => restrict μ s) '' {d | μ ≤ d + ν}
case a
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
h_nonempty : Set.Nonempty {d | μ ≤ d + ν}
ν' : Measure α
h_ν'_in : restrict μ s ≤ ν' + restrict ν s
⊢ ∃ y, y ∈ (fun μ => restrict μ s) '' {d | μ ≤ d + ν} ∧ y ≤ ν'
refine' ⟨ν'.restrict s, _, restrict_le_self⟩
case a.refine'_1
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
h_nonempty : Set.Nonempty {d | μ ≤ d + ν}
ν' : Measure α
h_ν'_in : restrict μ s ≤ ν' + restrict ν s
⊢ ν' + restrict ⊤ (sᶜ) ∈ {d | μ ≤ d + ν}

case a.refine'_2
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
h_nonempty : Set.Nonempty {d | μ ≤ d + ν}
ν' : Measure α
h_ν'_in : restrict μ s ≤ ν' + restrict ν s
⊢ (fun μ => restrict μ s) (ν' + restrict ⊤ (sᶜ)) = restrict ν' s
case a
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
h_nonempty : Set.Nonempty {d | μ ≤ d + ν}
ν' : Measure α
h_ν'_in : restrict μ s ≤ ν' + restrict ν s
⊢ restrict ν' s ∈ (fun μ => restrict μ s) '' {d | μ ≤ d + ν}
refine' ⟨ν' + (⊤ : Measure α).restrict (sᶜ), _, _⟩
case a.refine'_1
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
h_nonempty : Set.Nonempty {d | μ ≤ d + ν}
ν' : Measure α
h_ν'_in : restrict μ s ≤ ν' + restrict ν s
⊢ ∀ (s_1 : Set α), MeasurableSet s_1 → ↑↑μ s_1 ≤ ↑↑(ν' + ν + restrict ⊤ (sᶜ)) s_1
case a.refine'_1
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
h_nonempty : Set.Nonempty {d | μ ≤ d + ν}
ν' : Measure α
h_ν'_in : restrict μ s ≤ ν' + restrict ν s
⊢ ν' + restrict ⊤ (sᶜ) ∈ {d | μ ≤ d + ν}
rw [mem_setOf_eq, add_right_comm, Measure.le_iff]
case a.refine'_1
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
h_nonempty : Set.Nonempty {d | μ ≤ d + ν}
ν' : Measure α
h_ν'_in : restrict μ s ≤ ν' + restrict ν s
t : Set α
h_meas_t : MeasurableSet t
⊢ ↑↑μ t ≤ ↑↑(ν' + ν + restrict ⊤ (sᶜ)) t
case a.refine'_1
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
h_nonempty : Set.Nonempty {d | μ ≤ d + ν}
ν' : Measure α
h_ν'_in : restrict μ s ≤ ν' + restrict ν s
⊢ ∀ (s_1 : Set α), MeasurableSet s_1 → ↑↑μ s_1 ≤ ↑↑(ν' + ν + restrict ⊤ (sᶜ)) s_1
intro t h_meas_t
case a.refine'_1
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
h_nonempty : Set.Nonempty {d | μ ≤ d + ν}
ν' : Measure α
h_ν'_in : restrict μ s ≤ ν' + restrict ν s
t : Set α
h_meas_t : MeasurableSet t
⊢ ↑↑μ (t ∩ s) + ↑↑μ (t \ s) ≤ ↑↑(ν' + ν + restrict ⊤ (sᶜ)) (t ∩ s) + ↑↑(ν' + ν + restrict ⊤ (sᶜ)) (t \ s)
case a.refine'_1
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
h_nonempty : Set.Nonempty {d | μ ≤ d + ν}
ν' : Measure α
h_ν'_in : restrict μ s ≤ ν' + restrict ν s
t : Set α
h_meas_t : MeasurableSet t
⊢ ↑↑μ t ≤ ↑↑(ν' + ν + restrict ⊤ (sᶜ)) t
repeat' rw [← measure_inter_add_diff t h_meas_s]
case a.refine'_1.refine'_1
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
h_nonempty : Set.Nonempty {d | μ ≤ d + ν}
ν' : Measure α
h_ν'_in : restrict μ s ≤ ν' + restrict ν s
t : Set α
h_meas_t : MeasurableSet t
⊢ ↑↑μ (t ∩ s) ≤ ↑↑(ν' + ν + restrict ⊤ (sᶜ)) (t ∩ s)

case a.refine'_1.refine'_2
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
h_nonempty : Set.Nonempty {d | μ ≤ d + ν}
ν' : Measure α
h_ν'_in : restrict μ s ≤ ν' + restrict ν s
t : Set α
h_meas_t : MeasurableSet t
⊢ ↑↑μ (t \ s) ≤ ↑↑(ν' + ν + restrict ⊤ (sᶜ)) (t \ s)
case a.refine'_1
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
h_nonempty : Set.Nonempty {d | μ ≤ d + ν}
ν' : Measure α
h_ν'_in : restrict μ s ≤ ν' + restrict ν s
t : Set α
h_meas_t : MeasurableSet t
⊢ ↑↑μ (t ∩ s) + ↑↑μ (t \ s) ≤ ↑↑(ν' + ν + restrict ⊤ (sᶜ)) (t ∩ s) + ↑↑(ν' + ν + restrict ⊤ (sᶜ)) (t \ s)
refine' add_le_add _ _
case a.refine'_1
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
h_nonempty : Set.Nonempty {d | μ ≤ d + ν}
ν' : Measure α
h_ν'_in : restrict μ s ≤ ν' + restrict ν s
t : Set α
h_meas_t : MeasurableSet t
⊢ ↑↑μ (t ∩ s) + ↑↑μ (t \ s) ≤ ↑↑(ν' + ν + restrict ⊤ (sᶜ)) (t ∩ s) + ↑↑(ν' + ν + restrict ⊤ (sᶜ)) (t \ s)
case a.refine'_1
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
h_nonempty : Set.Nonempty {d | μ ≤ d + ν}
ν' : Measure α
h_ν'_in : restrict μ s ≤ ν' + restrict ν s
t : Set α
h_meas_t : MeasurableSet t
⊢ ↑↑μ (t ∩ s) + ↑↑μ (t \ s) ≤ ↑↑(ν' + ν + restrict ⊤ (sᶜ)) (t ∩ s) + ↑↑(ν' + ν + restrict ⊤ (sᶜ)) (t \ s)
rw [← measure_inter_add_diff t h_meas_s]
case a.refine'_1.refine'_1
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
h_nonempty : Set.Nonempty {d | μ ≤ d + ν}
ν' : Measure α
h_ν'_in : restrict μ s ≤ ν' + restrict ν s
t : Set α
h_meas_t : MeasurableSet t
⊢ ↑↑μ (t ∩ s) ≤ ↑↑ν' (t ∩ s) + ↑↑ν (t ∩ s) + ↑↑(restrict ⊤ (sᶜ)) (t ∩ s)
case a.refine'_1.refine'_1
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
h_nonempty : Set.Nonempty {d | μ ≤ d + ν}
ν' : Measure α
h_ν'_in : restrict μ s ≤ ν' + restrict ν s
t : Set α
h_meas_t : MeasurableSet t
⊢ ↑↑μ (t ∩ s) ≤ ↑↑(ν' + ν + restrict ⊤ (sᶜ)) (t ∩ s)
rw [add_apply, add_apply]
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
h_nonempty : Set.Nonempty {d | μ ≤ d + ν}
ν' : Measure α
h_ν'_in : restrict μ s ≤ ν' + restrict ν s
t : Set α
h_meas_t : MeasurableSet t
⊢ ↑↑μ (t ∩ s) ≤ ↑↑ν' (t ∩ s) + ↑↑ν (t ∩ s)
case a.refine'_1.refine'_1
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
h_nonempty : Set.Nonempty {d | μ ≤ d + ν}
ν' : Measure α
h_ν'_in : restrict μ s ≤ ν' + restrict ν s
t : Set α
h_meas_t : MeasurableSet t
⊢ ↑↑μ (t ∩ s) ≤ ↑↑ν' (t ∩ s) + ↑↑ν (t ∩ s) + ↑↑(restrict ⊤ (sᶜ)) (t ∩ s)
apply le_add_right _
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
h_nonempty : Set.Nonempty {d | μ ≤ d + ν}
ν' : Measure α
h_ν'_in : restrict μ s ≤ ν' + restrict ν s
t : Set α
h_meas_t : MeasurableSet t
⊢ ↑↑(restrict μ s) (t ∩ s) ≤ ↑↑ν' (t ∩ s) + ↑↑(restrict ν s) (t ∩ s)
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
h_nonempty : Set.Nonempty {d | μ ≤ d + ν}
ν' : Measure α
h_ν'_in : restrict μ s ≤ ν' + restrict ν s
t : Set α
h_meas_t : MeasurableSet t
⊢ ↑↑μ (t ∩ s) ≤ ↑↑ν' (t ∩ s) + ↑↑ν (t ∩ s)
rw [← restrict_eq_self μ (inter_subset_right _ _),
  ← restrict_eq_self ν (inter_subset_right _ _)]
no goals
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
h_nonempty : Set.Nonempty {d | μ ≤ d + ν}
ν' : Measure α
h_ν'_in : restrict μ s ≤ ν' + restrict ν s
t : Set α
h_meas_t : MeasurableSet t
⊢ ↑↑(restrict μ s) (t ∩ s) ≤ ↑↑ν' (t ∩ s) + ↑↑(restrict ν s) (t ∩ s)
apply h_ν'_in _ (h_meas_t.inter h_meas_s)
case a.refine'_1.refine'_2
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
h_nonempty : Set.Nonempty {d | μ ≤ d + ν}
ν' : Measure α
h_ν'_in : restrict μ s ≤ ν' + restrict ν s
t : Set α
h_meas_t : MeasurableSet t
⊢ ↑↑μ (t ∩ sᶜ) ≤ ↑↑(ν' + ν + ⊤) (t ∩ sᶜ)
case a.refine'_1.refine'_2
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
h_nonempty : Set.Nonempty {d | μ ≤ d + ν}
ν' : Measure α
h_ν'_in : restrict μ s ≤ ν' + restrict ν s
t : Set α
h_meas_t : MeasurableSet t
⊢ ↑↑μ (t \ s) ≤ ↑↑(ν' + ν + restrict ⊤ (sᶜ)) (t \ s)
rw [add_apply, restrict_apply (h_meas_t.diff h_meas_s), diff_eq, inter_assoc, inter_self,
  ← add_apply]
case a.refine'_1.refine'_2
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
h_nonempty : Set.Nonempty {d | μ ≤ d + ν}
ν' : Measure α
h_ν'_in : restrict μ s ≤ ν' + restrict ν s
t : Set α
h_meas_t : MeasurableSet t
h_mu_le_add_top : μ ≤ ν' + ν + ⊤
⊢ ↑↑μ (t ∩ sᶜ) ≤ ↑↑(ν' + ν + ⊤) (t ∩ sᶜ)
case a.refine'_1.refine'_2
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
h_nonempty : Set.Nonempty {d | μ ≤ d + ν}
ν' : Measure α
h_ν'_in : restrict μ s ≤ ν' + restrict ν s
t : Set α
h_meas_t : MeasurableSet t
⊢ ↑↑μ (t ∩ sᶜ) ≤ ↑↑(ν' + ν + ⊤) (t ∩ sᶜ)
have h_mu_le_add_top : μ ≤ ν' + ν + ⊤ := by simp only [add_top, le_top]
no goals
case a.refine'_1.refine'_2
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
h_nonempty : Set.Nonempty {d | μ ≤ d + ν}
ν' : Measure α
h_ν'_in : restrict μ s ≤ ν' + restrict ν s
t : Set α
h_meas_t : MeasurableSet t
h_mu_le_add_top : μ ≤ ν' + ν + ⊤
⊢ ↑↑μ (t ∩ sᶜ) ≤ ↑↑(ν' + ν + ⊤) (t ∩ sᶜ)
exact Measure.le_iff'.1 h_mu_le_add_top _
no goals
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
h_nonempty : Set.Nonempty {d | μ ≤ d + ν}
ν' : Measure α
h_ν'_in : restrict μ s ≤ ν' + restrict ν s
t : Set α
h_meas_t : MeasurableSet t
⊢ μ ≤ ν' + ν + ⊤
simp only [add_top, le_top]
case a.refine'_2.h
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
h_nonempty : Set.Nonempty {d | μ ≤ d + ν}
ν' : Measure α
h_ν'_in : restrict μ s ≤ ν' + restrict ν s
t : Set α
h_meas_t : MeasurableSet t
⊢ ↑↑((fun μ => restrict μ s) (ν' + restrict ⊤ (sᶜ))) t = ↑↑(restrict ν' s) t
case a.refine'_2
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
h_nonempty : Set.Nonempty {d | μ ≤ d + ν}
ν' : Measure α
h_ν'_in : restrict μ s ≤ ν' + restrict ν s
⊢ (fun μ => restrict μ s) (ν' + restrict ⊤ (sᶜ)) = restrict ν' s
ext1 t h_meas_t
no goals
case a.refine'_2.h
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
h_nonempty : Set.Nonempty {d | μ ≤ d + ν}
ν' : Measure α
h_ν'_in : restrict μ s ≤ ν' + restrict ν s
t : Set α
h_meas_t : MeasurableSet t
⊢ ↑↑((fun μ => restrict μ s) (ν' + restrict ⊤ (sᶜ))) t = ↑↑(restrict ν' s) t
simp [restrict_apply h_meas_t, restrict_apply (h_meas_t.inter h_meas_s), inter_assoc]
case a
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
h_nonempty : Set.Nonempty {d | μ ≤ d + ν}
⊢ ∀ (x : Measure α),
    x ∈ (fun μ => restrict μ s) '' {d | μ ≤ d + ν} → ∃ y, y ∈ {d | restrict μ s ≤ d + restrict ν s} ∧ y ≤ x
case a
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
h_nonempty : Set.Nonempty {d | μ ≤ d + ν}
⊢ sInf {d | restrict μ s ≤ d + restrict ν s} ≤ sInf ((fun μ => restrict μ s) '' {d | μ ≤ d + ν})
refine' sInf_le_sInf_of_forall_exists_le _
case a
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
h_nonempty : Set.Nonempty {d | μ ≤ d + ν}
t : Measure α
h_t_in : t ∈ {d | μ ≤ d + ν}
⊢ restrict t s ∈ {d | restrict μ s ≤ d + restrict ν s}
case a
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
h_nonempty : Set.Nonempty {d | μ ≤ d + ν}
⊢ ∀ (x : Measure α),
    x ∈ (fun μ => restrict μ s) '' {d | μ ≤ d + ν} → ∃ y, y ∈ {d | restrict μ s ≤ d + restrict ν s} ∧ y ≤ x
refine' ball_image_iff.2 fun t h_t_in => ⟨t.restrict s, _, le_rfl⟩
case a
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
h_nonempty : Set.Nonempty {d | μ ≤ d + ν}
t : Measure α
h_t_in : t ∈ {d | μ ≤ d + ν}
⊢ restrict μ s ≤ restrict (t + ν) s
case a
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
h_nonempty : Set.Nonempty {d | μ ≤ d + ν}
t : Measure α
h_t_in : t ∈ {d | μ ≤ d + ν}
⊢ restrict t s ∈ {d | restrict μ s ≤ d + restrict ν s}
rw [Set.mem_setOf_eq, ← restrict_add]
no goals
case a
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
h_nonempty : Set.Nonempty {d | μ ≤ d + ν}
t : Measure α
h_t_in : t ∈ {d | μ ≤ d + ν}
⊢ restrict μ s ≤ restrict (t + ν) s
exact restrict_mono Subset.rfl h_t_in