ι : Type ?u.4585
α : Type u_1
β : Type ?u.4591
l : Filter α
⊢ (∃ i, Set.Finite i ∧ ∃ i', i' ∈ l ∧ i' ⊆ i) ↔ ∃ s, s ∈ l ∧ Set.Finite s
ι : Type ?u.4585
α : Type u_1
β : Type ?u.4591
l : Filter α
⊢ Disjoint cofinite l ↔ ∃ s, s ∈ l ∧ Set.Finite s
simp only [hasBasis_cofinite.disjoint_iff l.basis_sets, id, disjoint_compl_left_iff_subset]
no goals
ι : Type ?u.4585
α : Type u_1
β : Type ?u.4591
l : Filter α
⊢ (∃ i, Set.Finite i ∧ ∃ i', i' ∈ l ∧ i' ⊆ i) ↔ ∃ s, s ∈ l ∧ Set.Finite s
exact ⟨fun ⟨s, hs, t, ht, hts⟩ => ⟨t, ht, hs.subset hts⟩,
  fun ⟨s, hs, hsf⟩ => ⟨s, hsf, s, hs, Subset.rfl⟩⟩