α : Type u_1
β : Type ?u.136128
γ : Type ?u.136131
δ : Type ?u.136134
ι : Type ?u.136137
R : Type ?u.136140
R' : Type ?u.136143
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ s t : Set α
h : ↑↑(μ + ν) t ≠ ⊤
h' : s ⊆ t
h'' : ↑↑(μ + ν) s = ↑↑(μ + ν) t
⊢ ↑↑μ t ≤ ↑↑μ s
α : Type u_1
β : Type ?u.136128
γ : Type ?u.136131
δ : Type ?u.136134
ι : Type ?u.136137
R : Type ?u.136140
R' : Type ?u.136143
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ s t : Set α
h : ↑↑(μ + ν) t ≠ ⊤
h' : s ⊆ t
h'' : ↑↑(μ + ν) s = ↑↑(μ + ν) t
⊢ ↑↑μ s = ↑↑μ t
refine' le_antisymm (measure_mono h') _
α : Type u_1
β : Type ?u.136128
γ : Type ?u.136131
δ : Type ?u.136134
ι : Type ?u.136137
R : Type ?u.136140
R' : Type ?u.136143
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ s t : Set α
h : ↑↑(μ + ν) t ≠ ⊤
h' : s ⊆ t
h'' : ↑↑(μ + ν) s = ↑↑(μ + ν) t
this : ↑↑μ t + ↑↑ν t ≤ ↑↑μ s + ↑↑ν t
⊢ ↑↑μ t ≤ ↑↑μ s
α : Type u_1
β : Type ?u.136128
γ : Type ?u.136131
δ : Type ?u.136134
ι : Type ?u.136137
R : Type ?u.136140
R' : Type ?u.136143
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ s t : Set α
h : ↑↑(μ + ν) t ≠ ⊤
h' : s ⊆ t
h'' : ↑↑(μ + ν) s = ↑↑(μ + ν) t
⊢ ↑↑μ t ≤ ↑↑μ s
have : μ t + ν t ≤ μ s + ν t :=
  calc
    μ t + ν t = μ s + ν s := h''.symm
    _ ≤ μ s + ν t := add_le_add le_rfl (measure_mono h')
α : Type u_1
β : Type ?u.136128
γ : Type ?u.136131
δ : Type ?u.136134
ι : Type ?u.136137
R : Type ?u.136140
R' : Type ?u.136143
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ s t : Set α
h : ↑↑(μ + ν) t ≠ ⊤
h' : s ⊆ t
h'' : ↑↑(μ + ν) s = ↑↑(μ + ν) t
this : ↑↑μ t + ↑↑ν t ≤ ↑↑μ s + ↑↑ν t
⊢ ↑↑ν t ≠ ⊤
α : Type u_1
β : Type ?u.136128
γ : Type ?u.136131
δ : Type ?u.136134
ι : Type ?u.136137
R : Type ?u.136140
R' : Type ?u.136143
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ s t : Set α
h : ↑↑(μ + ν) t ≠ ⊤
h' : s ⊆ t
h'' : ↑↑(μ + ν) s = ↑↑(μ + ν) t
this : ↑↑μ t + ↑↑ν t ≤ ↑↑μ s + ↑↑ν t
⊢ ↑↑μ t ≤ ↑↑μ s
apply ENNReal.le_of_add_le_add_right _ this
α : Type u_1
β : Type ?u.136128
γ : Type ?u.136131
δ : Type ?u.136134
ι : Type ?u.136137
R : Type ?u.136140
R' : Type ?u.136143
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ s t : Set α
h' : s ⊆ t
h'' : ↑↑(μ + ν) s = ↑↑(μ + ν) t
this : ↑↑μ t + ↑↑ν t ≤ ↑↑μ s + ↑↑ν t
h : ¬↑↑μ t = ⊤ ∧ ¬↑↑ν t = ⊤
⊢ ↑↑ν t ≠ ⊤
α : Type u_1
β : Type ?u.136128
γ : Type ?u.136131
δ : Type ?u.136134
ι : Type ?u.136137
R : Type ?u.136140
R' : Type ?u.136143
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ s t : Set α
h : ↑↑(μ + ν) t ≠ ⊤
h' : s ⊆ t
h'' : ↑↑(μ + ν) s = ↑↑(μ + ν) t
this : ↑↑μ t + ↑↑ν t ≤ ↑↑μ s + ↑↑ν t
⊢ ↑↑ν t ≠ ⊤
simp only [not_or, ENNReal.add_eq_top, Pi.add_apply, Ne.def, coe_add] at h
no goals
α : Type u_1
β : Type ?u.136128
γ : Type ?u.136131
δ : Type ?u.136134
ι : Type ?u.136137
R : Type ?u.136140
R' : Type ?u.136143
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ s t : Set α
h' : s ⊆ t
h'' : ↑↑(μ + ν) s = ↑↑(μ + ν) t
this : ↑↑μ t + ↑↑ν t ≤ ↑↑μ s + ↑↑ν t
h : ¬↑↑μ t = ⊤ ∧ ¬↑↑ν t = ⊤
⊢ ↑↑ν t ≠ ⊤
exact h.2