-- Mathlib/MeasureTheory/Measure/Sub.lean
theorem sub_apply [IsFiniteMeasure ν] (h₁ : MeasurableSet s) (h₂ : ν ≤ μ) :
    (μ - ν) s = μ s - ν s

Proof state:
case a.a
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
inst✝ : IsFiniteMeasure ν
h₁ : MeasurableSet s
h₂ : ν ≤ μ
measure_sub : Measure α := ofMeasurable (fun t x => μ t - ν t) ⋯ ⋯
h_measure_sub_add : ν + measure_sub = μ
⊢ ∀ b ∈ {d | μ ≤ d + ν}, measure_sub ≤ b

Tactic:
intro d h_d

Result:
case a.a
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
inst✝ : IsFiniteMeasure ν
h₁ : MeasurableSet s
h₂ : ν ≤ μ
measure_sub : Measure α := ofMeasurable (fun t x => μ t - ν t) ⋯ ⋯
h_measure_sub_add : ν + measure_sub = μ
d : Measure α
h_d : d ∈ {d | μ ≤ d + ν}
⊢ measure_sub ≤ d

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
inst✝ : IsFiniteMeasure ν
h₁ : MeasurableSet s
h₂ : ν ≤ μ
g : ℕ → Set α
h_meas : ∀ (i : ℕ), MeasurableSet (g i)
h_disj : Pairwise (Function.onFun Disjoint g)
⊢ ν (⋃ i, g i) ≠ ⊤

Tactic:
apply measure_ne_top

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
inst✝ : IsFiniteMeasure ν
h₁ : MeasurableSet s
h₂ : ν ≤ μ
⊢ (fun t x => μ t - ν t) ∅ ⋯ = 0

Tactic:
simp

Result:
no goals

Proof state:
case a.a
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
inst✝ : IsFiniteMeasure ν
h₁ : MeasurableSet s
h₂ : ν ≤ μ
measure_sub : Measure α := ofMeasurable (fun t x => μ t - ν t) ⋯ ⋯
h_measure_sub_add : ν + measure_sub = μ
⊢ measure_sub ∈ {d | μ ≤ d + ν}

Tactic:
simp [le_refl, add_comm, h_measure_sub_add]

Result:
no goals

Proof state:
case h
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
inst✝ : IsFiniteMeasure ν
h₁ : MeasurableSet s
h₂ : ν ≤ μ
measure_sub : Measure α := ofMeasurable (fun t x => μ t - ν t) ⋯ ⋯
t : Set α
h_t_measurable_set : MeasurableSet t
⊢ (ν + measure_sub) t = μ t

Tactic:
simp only [Pi.add_apply, coe_add]

Result:
case h
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
inst✝ : IsFiniteMeasure ν
h₁ : MeasurableSet s
h₂ : ν ≤ μ
measure_sub : Measure α := ofMeasurable (fun t x => μ t - ν t) ⋯ ⋯
t : Set α
h_t_measurable_set : MeasurableSet t
⊢ ν t + measure_sub t = μ t

Proof state:
case a.a
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
inst✝ : IsFiniteMeasure ν
h₁ : MeasurableSet s
h₂ : ν ≤ μ
measure_sub : Measure α := ofMeasurable (fun t x => μ t - ν t) ⋯ ⋯
h_measure_sub_add : ν + measure_sub = μ
d : Measure α
h_d : ν + measure_sub ≤ ν + d
⊢ measure_sub ≤ d

Tactic:
apply Measure.le_of_add_le_add_left h_d

Result:
no goals

Proof state:
case a
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
inst✝ : IsFiniteMeasure ν
h₁ : MeasurableSet s
h₂ : ν ≤ μ
measure_sub : Measure α := ofMeasurable (fun t x => μ t - ν t) ⋯ ⋯
h_measure_sub_add : ν + measure_sub = μ
⊢ sInf {d | μ ≤ d + ν} ≤ measure_sub

Tactic:
apply sInf_le

Result:
case a.a
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
inst✝ : IsFiniteMeasure ν
h₁ : MeasurableSet s
h₂ : ν ≤ μ
measure_sub : Measure α := ofMeasurable (fun t x => μ t - ν t) ⋯ ⋯
h_measure_sub_add : ν + measure_sub = μ
⊢ measure_sub ∈ {d | μ ≤ d + ν}

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
inst✝ : IsFiniteMeasure ν
h₁ : MeasurableSet s
h₂ : ν ≤ μ
g : ℕ → Set α
h_meas : ∀ (i : ℕ), MeasurableSet (g i)
h_disj : Pairwise (Function.onFun Disjoint g)
⊢ (fun t x => μ t - ν t) (⋃ i, g i) ⋯ = ∑' (i : ℕ), (fun t x => μ t - ν t) (g i) ⋯

Tactic:
simp only [measure_iUnion h_disj h_meas]

Result:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
inst✝ : IsFiniteMeasure ν
h₁ : MeasurableSet s
h₂ : ν ≤ μ
g : ℕ → Set α
h_meas : ∀ (i : ℕ), MeasurableSet (g i)
h_disj : Pairwise (Function.onFun Disjoint g)
⊢ ∑' (i : ℕ), μ (g i) - ∑' (i : ℕ), ν (g i) = ∑' (i : ℕ), (μ (g i) - ν (g i))

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
inst✝ : IsFiniteMeasure ν
h₁ : MeasurableSet s
h₂ : ν ≤ μ
measure_sub : Measure α := ofMeasurable (fun t x => μ t - ν t) ⋯ ⋯
h_measure_sub_add : ν + measure_sub = μ
⊢ μ - ν = measure_sub

Tactic:
rw [MeasureTheory.Measure.sub_def]

Result:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
inst✝ : IsFiniteMeasure ν
h₁ : MeasurableSet s
h₂ : ν ≤ μ
measure_sub : Measure α := ofMeasurable (fun t x => μ t - ν t) ⋯ ⋯
h_measure_sub_add : ν + measure_sub = μ
⊢ sInf {d | μ ≤ d + ν} = measure_sub

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
inst✝ : IsFiniteMeasure ν
h₁ : MeasurableSet s
h₂ : ν ≤ μ
measure_sub : Measure α := ofMeasurable (fun t x => μ t - ν t) ⋯ ⋯
h_measure_sub_add : ν + measure_sub = μ
⊢ sInf {d | μ ≤ d + ν} = measure_sub

Tactic:
apply le_antisymm

Result:
case a
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
inst✝ : IsFiniteMeasure ν
h₁ : MeasurableSet s
h₂ : ν ≤ μ
measure_sub : Measure α := ofMeasurable (fun t x => μ t - ν t) ⋯ ⋯
h_measure_sub_add : ν + measure_sub = μ
⊢ sInf {d | μ ≤ d + ν} ≤ measure_sub

case a
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
inst✝ : IsFiniteMeasure ν
h₁ : MeasurableSet s
h₂ : ν ≤ μ
measure_sub : Measure α := ofMeasurable (fun t x => μ t - ν t) ⋯ ⋯
h_measure_sub_add : ν + measure_sub = μ
⊢ measure_sub ≤ sInf {d | μ ≤ d + ν}

Proof state:
case a
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
inst✝ : IsFiniteMeasure ν
h₁ : MeasurableSet s
h₂ : ν ≤ μ
measure_sub : Measure α := ofMeasurable (fun t x => μ t - ν t) ⋯ ⋯
h_measure_sub_add : ν + measure_sub = μ
⊢ measure_sub ≤ sInf {d | μ ≤ d + ν}

Tactic:
apply le_sInf

Result:
case a.a
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
inst✝ : IsFiniteMeasure ν
h₁ : MeasurableSet s
h₂ : ν ≤ μ
measure_sub : Measure α := ofMeasurable (fun t x => μ t - ν t) ⋯ ⋯
h_measure_sub_add : ν + measure_sub = μ
⊢ ∀ b ∈ {d | μ ≤ d + ν}, measure_sub ≤ b

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
inst✝ : IsFiniteMeasure ν
h₁ : MeasurableSet s
h₂ : ν ≤ μ
measure_sub : Measure α := ofMeasurable (fun t x => μ t - ν t) ⋯ ⋯
⊢ (μ - ν) s = μ s - ν s

Tactic:
have h_measure_sub_add : ν + measure_sub = μ := by
  ext1 t h_t_measurable_set
  simp only [Pi.add_apply, coe_add]
  rw [MeasureTheory.Measure.ofMeasurable_apply _ h_t_measurable_set, add_comm,
    tsub_add_cancel_of_le (h₂ t)]

Result:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
inst✝ : IsFiniteMeasure ν
h₁ : MeasurableSet s
h₂ : ν ≤ μ
measure_sub : Measure α := ofMeasurable (fun t x => μ t - ν t) ⋯ ⋯
h_measure_sub_add : ν + measure_sub = μ
⊢ (μ - ν) s = μ s - ν s

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
inst✝ : IsFiniteMeasure ν
h₁ : MeasurableSet s
h₂ : ν ≤ μ
g : ℕ → Set α
h_meas : ∀ (i : ℕ), MeasurableSet (g i)
h_disj : Pairwise (Function.onFun Disjoint g)
⊢ ∑' (i : ℕ), ν (g i) ≠ ⊤

Tactic:
rw [← measure_iUnion h_disj h_meas]

Result:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
inst✝ : IsFiniteMeasure ν
h₁ : MeasurableSet s
h₂ : ν ≤ μ
g : ℕ → Set α
h_meas : ∀ (i : ℕ), MeasurableSet (g i)
h_disj : Pairwise (Function.onFun Disjoint g)
⊢ ν (⋃ i, g i) ≠ ⊤

Proof state:
case a.a
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
inst✝ : IsFiniteMeasure ν
h₁ : MeasurableSet s
h₂ : ν ≤ μ
measure_sub : Measure α := ofMeasurable (fun t x => μ t - ν t) ⋯ ⋯
h_measure_sub_add : ν + measure_sub = μ
d : Measure α
h_d : d ∈ {d | μ ≤ d + ν}
⊢ measure_sub ≤ d

Tactic:
rw [← h_measure_sub_add, mem_setOf_eq, add_comm d] at h_d

Result:
case a.a
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
inst✝ : IsFiniteMeasure ν
h₁ : MeasurableSet s
h₂ : ν ≤ μ
measure_sub : Measure α := ofMeasurable (fun t x => μ t - ν t) ⋯ ⋯
h_measure_sub_add : ν + measure_sub = μ
d : Measure α
h_d : ν + measure_sub ≤ ν + d
⊢ measure_sub ≤ d