no goals
α : Type u_1
β : Type ?u.15260
γ : Type ?u.15263
δ : Type ?u.15266
ι : Type ?u.15269
inst✝ : MeasurableSpace α
μ✝ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t : Set α
μ ν : Measure α
s : Set α
⊢ ∃ t, s ⊆ t ∧ MeasurableSet t ∧ ↑↑μ t = ↑↑μ s ∧ ↑↑ν t = ↑↑ν s
simpa only [Bool.forall_bool.trans and_comm] using
  exists_measurable_superset_forall_eq (fun b => cond b μ ν) s