no goals
α : Type u_1
β : Type ?u.35027
γ : Type ?u.35030
δ : Type ?u.35033
ι : Type ?u.35036
inst✝ : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s s₁ s₂ t : Set α
⊢ ¬↑↑μ (s ∪ t) = ⊤ ↔ ¬(↑↑μ s = ⊤ ∨ ↑↑μ t = ⊤)
simp only [← lt_top_iff_ne_top, ← Ne.def, not_or, measure_union_lt_top_iff]