no goals
α : Type u_1
β : Type ?u.546970
γ : Type ?u.546973
δ : Type ?u.546976
ι : Type ?u.546979
R : Type ?u.546982
R' : Type ?u.546985
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
⊢ sᶜ ∈ cofinite μ ↔ ↑↑μ s < ⊤
rw [mem_cofinite, compl_compl]