α : Type u_1
β : Type ?u.607532
γ : Type ?u.607535
δ : Type ?u.607538
ι : Type ?u.607541
R : Type ?u.607544
R' : Type ?u.607547
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
inst✝ : IsFiniteMeasure μ
hs : MeasurableSet s
ht : MeasurableSet t
ε : ℝ≥0∞
h : ↑↑μ s ≤ ↑↑μ t + ε
⊢ ↑↑μ univ ≤ ↑↑μ univ - ↑↑μ s + ε + ↑↑μ t
α : Type u_1
β : Type ?u.607532
γ : Type ?u.607535
δ : Type ?u.607538
ι : Type ?u.607541
R : Type ?u.607544
R' : Type ?u.607547
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
inst✝ : IsFiniteMeasure μ
hs : MeasurableSet s
ht : MeasurableSet t
ε : ℝ≥0∞
h : ↑↑μ s ≤ ↑↑μ t + ε
⊢ ↑↑μ (tᶜ) ≤ ↑↑μ (sᶜ) + ε
rw [measure_compl ht (measure_ne_top μ _), measure_compl hs (measure_ne_top μ _),
  tsub_le_iff_right]
no goals
α : Type u_1
β : Type ?u.607532
γ : Type ?u.607535
δ : Type ?u.607538
ι : Type ?u.607541
R : Type ?u.607544
R' : Type ?u.607547
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
inst✝ : IsFiniteMeasure μ
hs : MeasurableSet s
ht : MeasurableSet t
ε : ℝ≥0∞
h : ↑↑μ s ≤ ↑↑μ t + ε
⊢ ↑↑μ univ ≤ ↑↑μ univ - ↑↑μ s + ε + ↑↑μ t
calc
  μ univ = μ univ - μ s + μ s := (tsub_add_cancel_of_le <| measure_mono s.subset_univ).symm
  _ ≤ μ univ - μ s + (μ t + ε) := (add_le_add_left h _)
  _ = _ := by rw [add_right_comm, add_assoc]
no goals
α : Type u_1
β : Type ?u.607532
γ : Type ?u.607535
δ : Type ?u.607538
ι : Type ?u.607541
R : Type ?u.607544
R' : Type ?u.607547
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
inst✝ : IsFiniteMeasure μ
hs : MeasurableSet s
ht : MeasurableSet t
ε : ℝ≥0∞
h : ↑↑μ s ≤ ↑↑μ t + ε
⊢ ↑↑μ univ - ↑↑μ s + (↑↑μ t + ε) = ↑↑μ univ - ↑↑μ s + ε + ↑↑μ t
rw [add_right_comm, add_assoc]