-- Mathlib/MeasureTheory/Measure/Sub.lean
theorem restrict_sub_eq_restrict_sub_restrict (h_meas_s : MeasurableSet s) :
    (μ - ν).restrict s = μ.restrict s - ν.restrict s

Proof state:
case a
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
h_nonempty : {d | μ ≤ d + ν}.Nonempty
ν' : Measure α
h_ν'_in : μ.restrict s ≤ ν' + ν.restrict s
⊢ ν'.restrict s ∈ (fun μ => μ.restrict s) '' {d | μ ≤ d + ν}

Tactic:
refine ⟨ν' + (⊤ : Measure α).restrict sᶜ, ?_, ?_⟩

Result:
case a.refine_1
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
h_nonempty : {d | μ ≤ d + ν}.Nonempty
ν' : 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 : {d | μ ≤ d + ν}.Nonempty
ν' : Measure α
h_ν'_in : μ.restrict s ≤ ν' + ν.restrict s
⊢ (fun μ => μ.restrict s) (ν' + ⊤.restrict sᶜ) = ν'.restrict s

Proof state:
case a.refine_2.h
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
h_nonempty : {d | μ ≤ d + ν}.Nonempty
ν' : Measure α
h_ν'_in : μ.restrict s ≤ ν' + ν.restrict s
t : Set α
h_meas_t : MeasurableSet t
⊢ ((fun μ => μ.restrict s) (ν' + ⊤.restrict sᶜ)) t = (ν'.restrict s) t

Tactic:
simp [restrict_apply h_meas_t, restrict_apply (h_meas_t.inter h_meas_s), inter_assoc]

Result:
no goals

Proof state:
case a.refine_1
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
h_nonempty : {d | μ ≤ d + ν}.Nonempty
ν' : Measure α
h_ν'_in : μ.restrict s ≤ ν' + ν.restrict s
t : Set α
h_meas_t : MeasurableSet t
⊢ μ (t ∩ s) + μ (t \ s) ≤ (ν' + ν + ⊤.restrict sᶜ) t

Tactic:
rw [← measure_inter_add_diff t h_meas_s]

Result:
case a.refine_1
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
h_nonempty : {d | μ ≤ d + ν}.Nonempty
ν' : 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)

Proof state:
case a
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
h_nonempty : {d | μ ≤ d + ν}.Nonempty
ν' : Measure α
h_ν'_in : μ.restrict s ≤ ν' + ν.restrict s
⊢ ∃ y ∈ (fun μ => μ.restrict s) '' {d | μ ≤ d + ν}, y ≤ ν'

Tactic:
refine ⟨ν'.restrict s, ?_, restrict_le_self⟩

Result:
case a
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
h_nonempty : {d | μ ≤ d + ν}.Nonempty
ν' : Measure α
h_ν'_in : μ.restrict s ≤ ν' + ν.restrict s
⊢ ν'.restrict s ∈ (fun μ => μ.restrict s) '' {d | μ ≤ d + ν}

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
⊢ (sInf {d | μ ≤ d + ν}).restrict s = sInf {d | μ.restrict s ≤ d + ν.restrict s}

Tactic:
have h_nonempty : { d | μ ≤ d + ν }.Nonempty := ⟨μ, Measure.le_add_right le_rfl⟩

Result:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
h_nonempty : {d | μ ≤ d + ν}.Nonempty
⊢ (sInf {d | μ ≤ d + ν}).restrict s = sInf {d | μ.restrict s ≤ d + ν.restrict s}

Proof state:
case a
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
h_nonempty : {d | μ ≤ d + ν}.Nonempty
⊢ sInf ((fun μ => μ.restrict s) '' {d | μ ≤ d + ν}) ≤ sInf {d | μ.restrict s ≤ d + ν.restrict s}

Tactic:
refine sInf_le_sInf_of_forall_exists_le ?_

Result:
case a
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
h_nonempty : {d | μ ≤ d + ν}.Nonempty
⊢ ∀ x ∈ {d | μ.restrict s ≤ d + ν.restrict s}, ∃ y ∈ (fun μ => μ.restrict s) '' {d | μ ≤ d + ν}, y ≤ x

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
h_nonempty : {d | μ ≤ d + ν}.Nonempty
⊢ sInf ((fun μ => μ.restrict s) '' {d | μ ≤ d + ν}) = sInf {d | μ.restrict s ≤ d + ν.restrict s}

Tactic:
apply le_antisymm

Result:
case a
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
h_nonempty : {d | μ ≤ d + ν}.Nonempty
⊢ 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 : {d | μ ≤ d + ν}.Nonempty
⊢ sInf {d | μ.restrict s ≤ d + ν.restrict s} ≤ sInf ((fun μ => μ.restrict s) '' {d | μ ≤ d + ν})

Proof state:
case a
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
h_nonempty : {d | μ ≤ d + ν}.Nonempty
⊢ ∀ x ∈ (fun μ => μ.restrict s) '' {d | μ ≤ d + ν}, ∃ y ∈ {d | μ.restrict s ≤ d + ν.restrict s}, y ≤ x

Tactic:
refine forall_mem_image.2 fun t h_t_in => ⟨t.restrict s, ?_, le_rfl⟩

Result:
case a
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
h_nonempty : {d | μ ≤ d + ν}.Nonempty
t : Measure α
h_t_in : t ∈ {d | μ ≤ d + ν}
⊢ t.restrict s ∈ {d | μ.restrict s ≤ d + ν.restrict s}

Proof state:
case a.refine_1
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
h_nonempty : {d | μ ≤ d + ν}.Nonempty
ν' : Measure α
h_ν'_in : μ.restrict s ≤ ν' + ν.restrict s
t : Set α
h_meas_t : MeasurableSet t
⊢ μ t ≤ (ν' + ν + ⊤.restrict sᶜ) t

Tactic:
repeat rw [← measure_inter_add_diff t h_meas_s]

Result:
case a.refine_1
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
h_nonempty : {d | μ ≤ d + ν}.Nonempty
ν' : 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)

Proof state:
case a
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
h_nonempty : {d | μ ≤ d + ν}.Nonempty
t : Measure α
h_t_in : t ∈ {d | μ ≤ d + ν}
⊢ t.restrict s ∈ {d | μ.restrict s ≤ d + ν.restrict s}

Tactic:
rw [Set.mem_setOf_eq, ← restrict_add]

Result:
case a
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
h_nonempty : {d | μ ≤ d + ν}.Nonempty
t : Measure α
h_t_in : t ∈ {d | μ ≤ d + ν}
⊢ μ.restrict s ≤ (t + ν).restrict s

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
h_nonempty : {d | μ ≤ d + ν}.Nonempty
⊢ (sInf {d | μ ≤ d + ν}).restrict s = sInf {d | μ.restrict s ≤ d + ν.restrict s}

Tactic:
rw [restrict_sInf_eq_sInf_restrict h_nonempty h_meas_s]

Result:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
h_nonempty : {d | μ ≤ d + ν}.Nonempty
⊢ sInf ((fun μ => μ.restrict s) '' {d | μ ≤ d + ν}) = sInf {d | μ.restrict s ≤ d + ν.restrict s}

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
⊢ (sInf {d | μ ≤ d + ν}).restrict s = μ.restrict s - ν.restrict s

Tactic:
rw [sub_def]

Result:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
⊢ (sInf {d | μ ≤ d + ν}).restrict s = sInf {d | μ.restrict s ≤ d + ν.restrict s}

Proof state:
case a.refine_2
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
h_nonempty : {d | μ ≤ d + ν}.Nonempty
ν' : Measure α
h_ν'_in : μ.restrict s ≤ ν' + ν.restrict s
⊢ (fun μ => μ.restrict s) (ν' + ⊤.restrict sᶜ) = ν'.restrict s

Tactic:
ext1 t h_meas_t

Result:
case a.refine_2.h
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
h_nonempty : {d | μ ≤ d + ν}.Nonempty
ν' : Measure α
h_ν'_in : μ.restrict s ≤ ν' + ν.restrict s
t : Set α
h_meas_t : MeasurableSet t
⊢ ((fun μ => μ.restrict s) (ν' + ⊤.restrict sᶜ)) t = (ν'.restrict s) t