α : Type u_1
β : Type ?u.86486
γ : Type ?u.86489
δ : Type ?u.86492
ι : Type ?u.86495
R : Type ?u.86498
R' : Type ?u.86501
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ s t u : Set α
hs : MeasurableSet s
h : ↑↑μ t = ↑↑μ u
htu : t ⊆ u
ht_ne_top : ↑↑μ u ≠ ⊤
⊢ ↑↑μ (t ∩ s) = ↑↑μ (u ∩ s)
α : Type u_1
β : Type ?u.86486
γ : Type ?u.86489
δ : Type ?u.86492
ι : Type ?u.86495
R : Type ?u.86498
R' : Type ?u.86501
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ s t u : Set α
hs : MeasurableSet s
h : ↑↑μ t = ↑↑μ u
htu : t ⊆ u
ht_ne_top : ↑↑μ t ≠ ⊤
⊢ ↑↑μ (t ∩ s) = ↑↑μ (u ∩ s)
rw [h] at ht_ne_top
α : Type u_1
β : Type ?u.86486
γ : Type ?u.86489
δ : Type ?u.86492
ι : Type ?u.86495
R : Type ?u.86498
R' : Type ?u.86501
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ s t u : Set α
hs : MeasurableSet s
h : ↑↑μ t = ↑↑μ u
htu : t ⊆ u
ht_ne_top : ↑↑μ u ≠ ⊤
⊢ ↑↑μ (u ∩ s) ≤ ↑↑μ (t ∩ s)
α : Type u_1
β : Type ?u.86486
γ : Type ?u.86489
δ : Type ?u.86492
ι : Type ?u.86495
R : Type ?u.86498
R' : Type ?u.86501
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ s t u : Set α
hs : MeasurableSet s
h : ↑↑μ t = ↑↑μ u
htu : t ⊆ u
ht_ne_top : ↑↑μ u ≠ ⊤
⊢ ↑↑μ (t ∩ s) = ↑↑μ (u ∩ s)
refine' le_antisymm (measure_mono (inter_subset_inter_left _ htu)) _
α : Type u_1
β : Type ?u.86486
γ : Type ?u.86489
δ : Type ?u.86492
ι : Type ?u.86495
R : Type ?u.86498
R' : Type ?u.86501
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ s t u : Set α
hs : MeasurableSet s
h : ↑↑μ t = ↑↑μ u
htu : t ⊆ u
ht_ne_top : ↑↑μ u ≠ ⊤
A : ↑↑μ (u ∩ s) + ↑↑μ (u \ s) ≤ ↑↑μ (t ∩ s) + ↑↑μ (u \ s)
⊢ ↑↑μ (u ∩ s) ≤ ↑↑μ (t ∩ s)
α : Type u_1
β : Type ?u.86486
γ : Type ?u.86489
δ : Type ?u.86492
ι : Type ?u.86495
R : Type ?u.86498
R' : Type ?u.86501
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ s t u : Set α
hs : MeasurableSet s
h : ↑↑μ t = ↑↑μ u
htu : t ⊆ u
ht_ne_top : ↑↑μ u ≠ ⊤
⊢ ↑↑μ (u ∩ s) ≤ ↑↑μ (t ∩ s)
have A : μ (u ∩ s) + μ (u \ s) ≤ μ (t ∩ s) + μ (u \ s) :=
  calc
    μ (u ∩ s) + μ (u \ s) = μ u := measure_inter_add_diff _ hs
    _ = μ t := h.symm
    _ = μ (t ∩ s) + μ (t \ s) := (measure_inter_add_diff _ hs).symm
    _ ≤ μ (t ∩ s) + μ (u \ s) :=
      add_le_add le_rfl (measure_mono (diff_subset_diff htu Subset.rfl))
α : Type u_1
β : Type ?u.86486
γ : Type ?u.86489
δ : Type ?u.86492
ι : Type ?u.86495
R : Type ?u.86498
R' : Type ?u.86501
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ s t u : Set α
hs : MeasurableSet s
h : ↑↑μ t = ↑↑μ u
htu : t ⊆ u
ht_ne_top : ↑↑μ u ≠ ⊤
A : ↑↑μ (u ∩ s) + ↑↑μ (u \ s) ≤ ↑↑μ (t ∩ s) + ↑↑μ (u \ s)
B : ↑↑μ (u \ s) ≠ ⊤
⊢ ↑↑μ (u ∩ s) ≤ ↑↑μ (t ∩ s)
α : Type u_1
β : Type ?u.86486
γ : Type ?u.86489
δ : Type ?u.86492
ι : Type ?u.86495
R : Type ?u.86498
R' : Type ?u.86501
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ s t u : Set α
hs : MeasurableSet s
h : ↑↑μ t = ↑↑μ u
htu : t ⊆ u
ht_ne_top : ↑↑μ u ≠ ⊤
A : ↑↑μ (u ∩ s) + ↑↑μ (u \ s) ≤ ↑↑μ (t ∩ s) + ↑↑μ (u \ s)
⊢ ↑↑μ (u ∩ s) ≤ ↑↑μ (t ∩ s)
have B : μ (u \ s) ≠ ∞ := (lt_of_le_of_lt (measure_mono (diff_subset _ _)) ht_ne_top.lt_top).ne
no goals
α : Type u_1
β : Type ?u.86486
γ : Type ?u.86489
δ : Type ?u.86492
ι : Type ?u.86495
R : Type ?u.86498
R' : Type ?u.86501
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ s t u : Set α
hs : MeasurableSet s
h : ↑↑μ t = ↑↑μ u
htu : t ⊆ u
ht_ne_top : ↑↑μ u ≠ ⊤
A : ↑↑μ (u ∩ s) + ↑↑μ (u \ s) ≤ ↑↑μ (t ∩ s) + ↑↑μ (u \ s)
B : ↑↑μ (u \ s) ≠ ⊤
⊢ ↑↑μ (u ∩ s) ≤ ↑↑μ (t ∩ s)
exact ENNReal.le_of_add_le_add_right B A