case refine'_1
α : Type u
β : Type v
ι : Type ?u.10996
π : ι → Type ?u.11001
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
⊢ Monotone fun f => ∃ a, a ∈ s ∧ ClusterPt a f

case refine'_2
α : Type u
β : Type v
ι : Type ?u.10996
π : ι → Type ?u.11001
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
⊢ (∀ (f : Ultrafilter α), ↑f ≤ 𝓟 s → ∃ a, a ∈ s ∧ ClusterPt a ↑f) ↔
    ∀ (f : Ultrafilter α), ↑f ≤ 𝓟 s → ∃ a, a ∈ s ∧ ↑f ≤ 𝓝 a
α : Type u
β : Type v
ι : Type ?u.10996
π : ι → Type ?u.11001
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
⊢ IsCompact s ↔ ∀ (f : Ultrafilter α), ↑f ≤ 𝓟 s → ∃ a, a ∈ s ∧ ↑f ≤ 𝓝 a
refine' (forall_neBot_le_iff _).trans _
case refine'_1.intro.intro
α : Type u
β : Type v
ι : Type ?u.10996
π : ι → Type ?u.11001
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
f g : Filter α
hle : f ≤ g
a : α
has : a ∈ s
haf : ClusterPt a f
⊢ ∃ a, a ∈ s ∧ ClusterPt a g
case refine'_1
α : Type u
β : Type v
ι : Type ?u.10996
π : ι → Type ?u.11001
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
⊢ Monotone fun f => ∃ a, a ∈ s ∧ ClusterPt a f
rintro f g hle ⟨a, has, haf⟩
no goals
case refine'_1.intro.intro
α : Type u
β : Type v
ι : Type ?u.10996
π : ι → Type ?u.11001
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
f g : Filter α
hle : f ≤ g
a : α
has : a ∈ s
haf : ClusterPt a f
⊢ ∃ a, a ∈ s ∧ ClusterPt a g
exact ⟨a, has, haf.mono hle⟩
no goals
case refine'_2
α : Type u
β : Type v
ι : Type ?u.10996
π : ι → Type ?u.11001
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
⊢ (∀ (f : Ultrafilter α), ↑f ≤ 𝓟 s → ∃ a, a ∈ s ∧ ClusterPt a ↑f) ↔
    ∀ (f : Ultrafilter α), ↑f ≤ 𝓟 s → ∃ a, a ∈ s ∧ ↑f ≤ 𝓝 a
simp only [Ultrafilter.clusterPt_iff]