α : Type u_2
β : Type ?u.337219
γ : Type ?u.337222
δ : Type ?u.337225
ι : Type u_1
R : Type ?u.337231
R' : Type ?u.337234
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
inst✝ : Countable ι
μ : ι → Measure α
s : Set α
h : ∀ (i : ι), ↑↑(μ i) s = 0
⊢ ↑↑(sum μ) s ≤ 0
α : Type u_2
β : Type ?u.337219
γ : Type ?u.337222
δ : Type ?u.337225
ι : Type u_1
R : Type ?u.337231
R' : Type ?u.337234
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
inst✝ : Countable ι
μ : ι → Measure α
s : Set α
⊢ ↑↑(sum μ) s = 0 ↔ ∀ (i : ι), ↑↑(μ i) s = 0
refine'
  ⟨fun h i => nonpos_iff_eq_zero.1 <| h ▸ le_iff'.1 (le_sum μ i) _, fun h =>
    nonpos_iff_eq_zero.1 _⟩
case intro.intro.intro
α : Type u_2
β : Type ?u.337219
γ : Type ?u.337222
δ : Type ?u.337225
ι : Type u_1
R : Type ?u.337231
R' : Type ?u.337234
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ : Set α
inst✝ : Countable ι
μ : ι → Measure α
s : Set α
h : ∀ (i : ι), ↑↑(μ i) s = 0
t : Set α
hst : s ⊆ t
htm : MeasurableSet t
ht : ∀ (i : ι), ↑↑(μ i) t = ↑↑(μ i) s
⊢ ↑↑(sum μ) s ≤ 0
α : Type u_2
β : Type ?u.337219
γ : Type ?u.337222
δ : Type ?u.337225
ι : Type u_1
R : Type ?u.337231
R' : Type ?u.337234
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
inst✝ : Countable ι
μ : ι → Measure α
s : Set α
h : ∀ (i : ι), ↑↑(μ i) s = 0
⊢ ↑↑(sum μ) s ≤ 0
rcases exists_measurable_superset_forall_eq μ s with ⟨t, hst, htm, ht⟩
no goals
case intro.intro.intro
α : Type u_2
β : Type ?u.337219
γ : Type ?u.337222
δ : Type ?u.337225
ι : Type u_1
R : Type ?u.337231
R' : Type ?u.337234
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ : Set α
inst✝ : Countable ι
μ : ι → Measure α
s : Set α
h : ∀ (i : ι), ↑↑(μ i) s = 0
t : Set α
hst : s ⊆ t
htm : MeasurableSet t
ht : ∀ (i : ι), ↑↑(μ i) t = ↑↑(μ i) s
⊢ ↑↑(sum μ) s ≤ 0
calc
  sum μ s ≤ sum μ t := measure_mono hst
  _ = 0 := by simp [*]
no goals
α : Type u_2
β : Type ?u.337219
γ : Type ?u.337222
δ : Type ?u.337225
ι : Type u_1
R : Type ?u.337231
R' : Type ?u.337234
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ : Set α
inst✝ : Countable ι
μ : ι → Measure α
s : Set α
h : ∀ (i : ι), ↑↑(μ i) s = 0
t : Set α
hst : s ⊆ t
htm : MeasurableSet t
ht : ∀ (i : ι), ↑↑(μ i) t = ↑↑(μ i) s
⊢ ↑↑(sum μ) t = 0
simp [*]