no goals
α : Type ?u.91489
Γ₀ : Type u_1
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
s : Set Γ₀
⊢ IsClosed s ↔ 0 ∈ s ∨ ∃ γ, γ ≠ 0 ∧ s ⊆ Ici γ
simp only [← isOpen_compl_iff, isOpen_iff, mem_compl_iff, not_not, ← compl_Ici,
  compl_subset_compl]