[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
l : Filter α
⊢ univ ∈ {s | Set.Finite sᶜ}
[PROOFSTEP]
simp only [compl_univ, finite_empty, mem_setOf_eq]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
l : Filter α
x✝ y✝ : Set α
hs : x✝ ∈ {s | Set.Finite sᶜ}
ht : y✝ ∈ {s | Set.Finite sᶜ}
⊢ x✝ ∩ y✝ ∈ {s | Set.Finite sᶜ}
[PROOFSTEP]
simpa only [compl_inter, mem_setOf_eq] using hs.union ht
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
l : Filter α
⊢ cofinite = ⊥ ↔ Finite α
[PROOFSTEP]
simp [← empty_mem_iff_bot, finite_univ_iff]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
l : Filter α
p : α → Prop
⊢ (∃ᶠ (x : α) in cofinite, p x) ↔ Set.Infinite {x | p x}
[PROOFSTEP]
simp only [Filter.Frequently, Filter.Eventually, mem_cofinite, compl_setOf, not_not, Set.Infinite]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
l : Filter α
⊢ l ≤ cofinite ↔ ∀ (x : α), {x}ᶜ ∈ l
[PROOFSTEP]
refine' ⟨fun h x => h (finite_singleton x).compl_mem_cofinite, fun h s (hs : sᶜ.Finite) => _⟩
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
l : Filter α
h : ∀ (x : α), {x}ᶜ ∈ l
s : Set α
hs : Set.Finite sᶜ
⊢ s ∈ l
[PROOFSTEP]
rw [← compl_compl s, ← biUnion_of_singleton sᶜ, compl_iUnion₂, Filter.biInter_mem hs]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
l : Filter α
h : ∀ (x : α), {x}ᶜ ∈ l
s : Set α
hs : Set.Finite sᶜ
⊢ ∀ (i : α), i ∈ sᶜ → {i}ᶜ ∈ l
[PROOFSTEP]
exact fun x _ => h x
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
l : Filter α
s : Set (α × β)
⊢ sᶜ ∈ Filter.coprod cofinite cofinite ↔ sᶜ ∈ cofinite
[PROOFSTEP]
simp only [compl_mem_coprod, mem_cofinite, compl_compl, finite_image_fst_and_snd_iff]
[GOAL]
ι : Type u_1
α✝ : Type u_2
β : Type u_3
l : Filter α✝
α : ι → Type u_4
inst✝ : Finite ι
s : Set ((i : ι) → α i)
⊢ (sᶜ ∈ Filter.coprodᵢ fun i => cofinite) ↔ sᶜ ∈ cofinite
[PROOFSTEP]
simp only [compl_mem_coprodᵢ, mem_cofinite, compl_compl, forall_finite_image_eval_iff]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
l : Filter α
⊢ Disjoint cofinite l ↔ ∃ s, s ∈ l ∧ Set.Finite s
[PROOFSTEP]
simp only [hasBasis_cofinite.disjoint_iff l.basis_sets, id, disjoint_compl_left_iff_subset]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
l : Filter α
⊢ (∃ i, Set.Finite i ∧ ∃ i', i' ∈ l ∧ i' ⊆ i) ↔ ∃ s, s ∈ l ∧ Set.Finite s
[PROOFSTEP]
exact ⟨fun ⟨s, hs, t, ht, hts⟩ => ⟨t, ht, hs.subset hts⟩, fun ⟨s, hs, hsf⟩ => ⟨s, hsf, s, hs, Subset.rfl⟩⟩
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
l : Filter α
inst✝ : IsCountablyGenerated l
h : cofinite ≤ l
⊢ Set.Countable (⋂₀ l.sets)ᶜ
[PROOFSTEP]
rcases exists_antitone_basis l with ⟨s, hs⟩
[GOAL]
case intro
ι : Type u_1
α : Type u_2
β : Type u_3
l : Filter α
inst✝ : IsCountablyGenerated l
h : cofinite ≤ l
s : ℕ → Set α
hs : HasAntitoneBasis l s
⊢ Set.Countable (⋂₀ l.sets)ᶜ
[PROOFSTEP]
simp only [hs.sInter_sets, iInter_true, compl_iInter]
[GOAL]
case intro
ι : Type u_1
α : Type u_2
β : Type u_3
l : Filter α
inst✝ : IsCountablyGenerated l
h : cofinite ≤ l
s : ℕ → Set α
hs : HasAntitoneBasis l s
⊢ Set.Countable (⋃ (i : ℕ), (s i)ᶜ)
[PROOFSTEP]
exact countable_iUnion fun n ↦ Set.Finite.countable <| h <| hs.mem _
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
l✝ : Filter α
f : α → β
l : Filter β
inst✝ : IsCountablyGenerated l
h : Tendsto f cofinite l
⊢ Set.Countable (f ⁻¹' ⋂₀ l.sets)ᶜ
[PROOFSTEP]
erw [preimage_sInter, ← sInter_comap_sets]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
l✝ : Filter α
f : α → β
l : Filter β
inst✝ : IsCountablyGenerated l
h : Tendsto f cofinite l
⊢ Set.Countable (⋂₀ (comap f l).sets)ᶜ
[PROOFSTEP]
exact countable_compl_sInter_sets h.le_comap
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
l : Filter α
⊢ cofinite = atTop
[PROOFSTEP]
refine' le_antisymm _ atTop_le_cofinite
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
l : Filter α
⊢ cofinite ≤ atTop
[PROOFSTEP]
refine' atTop_basis.ge_iff.2 fun N _ => _
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
l : Filter α
N : ℕ
x✝ : True
⊢ Ici N ∈ cofinite
[PROOFSTEP]
simpa only [mem_cofinite, compl_Ici] using finite_lt_nat N
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
l : Filter α
p : ℕ → Prop
⊢ (∃ᶠ (n : ℕ) in atTop, p n) ↔ Set.Infinite {n | p n}
[PROOFSTEP]
rw [← Nat.cofinite_eq_atTop, frequently_cofinite_iff_infinite]
[GOAL]
ι : Type u_1
α✝ : Type u_2
β✝ : Type u_3
l : Filter α✝
α : Type u_4
β : Type u_5
inst✝ : LinearOrder β
s : Set α
hs : Set.Nonempty s
f : α → β
hf : Tendsto f cofinite atTop
⊢ ∃ a₀, a₀ ∈ s ∧ ∀ (a : α), a ∈ s → f a₀ ≤ f a
[PROOFSTEP]
rcases em (∃ y ∈ s, ∃ x, f y < x) with (⟨y, hys, x, hx⟩ | not_all_top)
[GOAL]
case inl.intro.intro.intro
ι : Type u_1
α✝ : Type u_2
β✝ : Type u_3
l : Filter α✝
α : Type u_4
β : Type u_5
inst✝ : LinearOrder β
s : Set α
hs : Set.Nonempty s
f : α → β
hf : Tendsto f cofinite atTop
y : α
hys : y ∈ s
x : β
hx : f y < x
⊢ ∃ a₀, a₀ ∈ s ∧ ∀ (a : α), a ∈ s → f a₀ ≤ f a
[PROOFSTEP]
have : {y | ¬x ≤ f y}.Finite := Filter.eventually_cofinite.mp (tendsto_atTop.1 hf x)
[GOAL]
case inl.intro.intro.intro
ι : Type u_1
α✝ : Type u_2
β✝ : Type u_3
l : Filter α✝
α : Type u_4
β : Type u_5
inst✝ : LinearOrder β
s : Set α
hs : Set.Nonempty s
f : α → β
hf : Tendsto f cofinite atTop
y : α
hys : y ∈ s
x : β
hx : f y < x
this : Set.Finite {y | ¬x ≤ f y}
⊢ ∃ a₀, a₀ ∈ s ∧ ∀ (a : α), a ∈ s → f a₀ ≤ f a
[PROOFSTEP]
simp only [not_le] at this 
[GOAL]
case inl.intro.intro.intro
ι : Type u_1
α✝ : Type u_2
β✝ : Type u_3
l : Filter α✝
α : Type u_4
β : Type u_5
inst✝ : LinearOrder β
s : Set α
hs : Set.Nonempty s
f : α → β
hf : Tendsto f cofinite atTop
y : α
hys : y ∈ s
x : β
hx : f y < x
this : Set.Finite {y | f y < x}
⊢ ∃ a₀, a₀ ∈ s ∧ ∀ (a : α), a ∈ s → f a₀ ≤ f a
[PROOFSTEP]
obtain ⟨a₀, ⟨ha₀ : f a₀ < x, ha₀s⟩, others_bigger⟩ := exists_min_image _ f (this.inter_of_left s) ⟨y, hx, hys⟩
[GOAL]
case inl.intro.intro.intro.intro.intro.intro
ι : Type u_1
α✝ : Type u_2
β✝ : Type u_3
l : Filter α✝
α : Type u_4
β : Type u_5
inst✝ : LinearOrder β
s : Set α
hs : Set.Nonempty s
f : α → β
hf : Tendsto f cofinite atTop
y : α
hys : y ∈ s
x : β
hx : f y < x
this : Set.Finite {y | f y < x}
a₀ : α
others_bigger : ∀ (b : α), b ∈ {y | f y < x} ∩ s → f a₀ ≤ f b
ha₀ : f a₀ < x
ha₀s : a₀ ∈ s
⊢ ∃ a₀, a₀ ∈ s ∧ ∀ (a : α), a ∈ s → f a₀ ≤ f a
[PROOFSTEP]
refine' ⟨a₀, ha₀s, fun a has => (lt_or_le (f a) x).elim _ (le_trans ha₀.le)⟩
[GOAL]
case inl.intro.intro.intro.intro.intro.intro
ι : Type u_1
α✝ : Type u_2
β✝ : Type u_3
l : Filter α✝
α : Type u_4
β : Type u_5
inst✝ : LinearOrder β
s : Set α
hs : Set.Nonempty s
f : α → β
hf : Tendsto f cofinite atTop
y : α
hys : y ∈ s
x : β
hx : f y < x
this : Set.Finite {y | f y < x}
a₀ : α
others_bigger : ∀ (b : α), b ∈ {y | f y < x} ∩ s → f a₀ ≤ f b
ha₀ : f a₀ < x
ha₀s : a₀ ∈ s
a : α
has : a ∈ s
⊢ f a < x → f a₀ ≤ f a
[PROOFSTEP]
exact fun h => others_bigger a ⟨h, has⟩
[GOAL]
case inr
ι : Type u_1
α✝ : Type u_2
β✝ : Type u_3
l : Filter α✝
α : Type u_4
β : Type u_5
inst✝ : LinearOrder β
s : Set α
hs : Set.Nonempty s
f : α → β
hf : Tendsto f cofinite atTop
not_all_top : ¬∃ y, y ∈ s ∧ ∃ x, f y < x
⊢ ∃ a₀, a₀ ∈ s ∧ ∀ (a : α), a ∈ s → f a₀ ≤ f a
[PROOFSTEP]
push_neg at not_all_top 
[GOAL]
case inr
ι : Type u_1
α✝ : Type u_2
β✝ : Type u_3
l : Filter α✝
α : Type u_4
β : Type u_5
inst✝ : LinearOrder β
s : Set α
hs : Set.Nonempty s
f : α → β
hf : Tendsto f cofinite atTop
not_all_top : ∀ (y : α), y ∈ s → ∀ (x : β), x ≤ f y
⊢ ∃ a₀, a₀ ∈ s ∧ ∀ (a : α), a ∈ s → f a₀ ≤ f a
[PROOFSTEP]
obtain ⟨a₀, ha₀s⟩ := hs
[GOAL]
case inr.intro
ι : Type u_1
α✝ : Type u_2
β✝ : Type u_3
l : Filter α✝
α : Type u_4
β : Type u_5
inst✝ : LinearOrder β
s : Set α
f : α → β
hf : Tendsto f cofinite atTop
not_all_top : ∀ (y : α), y ∈ s → ∀ (x : β), x ≤ f y
a₀ : α
ha₀s : a₀ ∈ s
⊢ ∃ a₀, a₀ ∈ s ∧ ∀ (a : α), a ∈ s → f a₀ ≤ f a
[PROOFSTEP]
exact ⟨a₀, ha₀s, fun a ha => not_all_top a ha (f a₀)⟩
