[GOAL]
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : FrechetUrysohnSpace X
s : Set X
a : X
⊢ a ∈ closure s ↔ ∃ x, (∀ (n : ℕ), x n ∈ s) ∧ Tendsto x atTop (𝓝 a)
[PROOFSTEP]
rw [← seqClosure_eq_closure]
[GOAL]
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : FrechetUrysohnSpace X
s : Set X
a : X
⊢ a ∈ seqClosure s ↔ ∃ x, (∀ (n : ℕ), x n ∈ s) ∧ Tendsto x atTop (𝓝 a)
[PROOFSTEP]
rfl
[GOAL]
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : FrechetUrysohnSpace X
f : X → Y
a : X
b : Y
⊢ Tendsto f (𝓝 a) (𝓝 b) ↔ ∀ (u : ℕ → X), Tendsto u atTop (𝓝 a) → Tendsto (f ∘ u) atTop (𝓝 b)
[PROOFSTEP]
refine' ⟨fun hf u hu => hf.comp hu, fun h => ((nhds_basis_closeds _).tendsto_iff (nhds_basis_closeds _)).2 _⟩
[GOAL]
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : FrechetUrysohnSpace X
f : X → Y
a : X
b : Y
h : ∀ (u : ℕ → X), Tendsto u atTop (𝓝 a) → Tendsto (f ∘ u) atTop (𝓝 b)
⊢ ∀ (ib : Set Y), ¬b ∈ ib ∧ IsClosed ib → ∃ ia, (¬a ∈ ia ∧ IsClosed ia) ∧ ∀ (x : X), x ∈ iaᶜ → f x ∈ ibᶜ
[PROOFSTEP]
rintro s ⟨hbs, hsc⟩
[GOAL]
case intro
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : FrechetUrysohnSpace X
f : X → Y
a : X
b : Y
h : ∀ (u : ℕ → X), Tendsto u atTop (𝓝 a) → Tendsto (f ∘ u) atTop (𝓝 b)
s : Set Y
hbs : ¬b ∈ s
hsc : IsClosed s
⊢ ∃ ia, (¬a ∈ ia ∧ IsClosed ia) ∧ ∀ (x : X), x ∈ iaᶜ → f x ∈ sᶜ
[PROOFSTEP]
refine' ⟨closure (f ⁻¹' s), ⟨mt _ hbs, isClosed_closure⟩, fun x => mt fun hx => subset_closure hx⟩
[GOAL]
case intro
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : FrechetUrysohnSpace X
f : X → Y
a : X
b : Y
h : ∀ (u : ℕ → X), Tendsto u atTop (𝓝 a) → Tendsto (f ∘ u) atTop (𝓝 b)
s : Set Y
hbs : ¬b ∈ s
hsc : IsClosed s
⊢ a ∈ closure (f ⁻¹' s) → b ∈ s
[PROOFSTEP]
rw [← seqClosure_eq_closure]
[GOAL]
case intro
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : FrechetUrysohnSpace X
f : X → Y
a : X
b : Y
h : ∀ (u : ℕ → X), Tendsto u atTop (𝓝 a) → Tendsto (f ∘ u) atTop (𝓝 b)
s : Set Y
hbs : ¬b ∈ s
hsc : IsClosed s
⊢ a ∈ seqClosure (f ⁻¹' s) → b ∈ s
[PROOFSTEP]
rintro ⟨u, hus, hu⟩
[GOAL]
case intro.intro.intro
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : FrechetUrysohnSpace X
f : X → Y
a : X
b : Y
h : ∀ (u : ℕ → X), Tendsto u atTop (𝓝 a) → Tendsto (f ∘ u) atTop (𝓝 b)
s : Set Y
hbs : ¬b ∈ s
hsc : IsClosed s
u : ℕ → X
hus : ∀ (n : ℕ), u n ∈ f ⁻¹' s
hu : Tendsto u atTop (𝓝 a)
⊢ b ∈ s
[PROOFSTEP]
exact hsc.mem_of_tendsto (h u hu) (eventually_of_forall hus)
[GOAL]
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h :
  ∀ (f : X → Prop) (a : X), (∀ (u : ℕ → X), Tendsto u atTop (𝓝 a) → Tendsto (f ∘ u) atTop (𝓝 (f a))) → ContinuousAt f a
⊢ FrechetUrysohnSpace X
[PROOFSTEP]
refine ⟨fun s x hcx => ?_⟩
[GOAL]
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h :
  ∀ (f : X → Prop) (a : X), (∀ (u : ℕ → X), Tendsto u atTop (𝓝 a) → Tendsto (f ∘ u) atTop (𝓝 (f a))) → ContinuousAt f a
s : Set X
x : X
hcx : x ∈ closure s
⊢ x ∈ seqClosure s
[PROOFSTEP]
by_cases hx : x ∈ s
[GOAL]
case pos
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h :
  ∀ (f : X → Prop) (a : X), (∀ (u : ℕ → X), Tendsto u atTop (𝓝 a) → Tendsto (f ∘ u) atTop (𝓝 (f a))) → ContinuousAt f a
s : Set X
x : X
hcx : x ∈ closure s
hx : x ∈ s
⊢ x ∈ seqClosure s
[PROOFSTEP]
exact subset_seqClosure hx
[GOAL]
case neg
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h :
  ∀ (f : X → Prop) (a : X), (∀ (u : ℕ → X), Tendsto u atTop (𝓝 a) → Tendsto (f ∘ u) atTop (𝓝 (f a))) → ContinuousAt f a
s : Set X
x : X
hcx : x ∈ closure s
hx : ¬x ∈ s
⊢ x ∈ seqClosure s
[PROOFSTEP]
obtain ⟨u, hux, hus⟩ : ∃ u : ℕ → X, Tendsto u atTop (𝓝 x) ∧ ∃ᶠ x in atTop, u x ∈ s
[GOAL]
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h :
  ∀ (f : X → Prop) (a : X), (∀ (u : ℕ → X), Tendsto u atTop (𝓝 a) → Tendsto (f ∘ u) atTop (𝓝 (f a))) → ContinuousAt f a
s : Set X
x : X
hcx : x ∈ closure s
hx : ¬x ∈ s
⊢ ∃ u, Tendsto u atTop (𝓝 x) ∧ ∃ᶠ (x : ℕ) in atTop, u x ∈ s
[PROOFSTEP]
simpa only [ContinuousAt, hx, tendsto_nhds_true, (· ∘ ·), ← not_frequently, exists_prop, ← mem_closure_iff_frequently,
  hcx, imp_false, not_forall, not_not] using h (· ∉ s) x
[GOAL]
case neg.intro.intro
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h :
  ∀ (f : X → Prop) (a : X), (∀ (u : ℕ → X), Tendsto u atTop (𝓝 a) → Tendsto (f ∘ u) atTop (𝓝 (f a))) → ContinuousAt f a
s : Set X
x : X
hcx : x ∈ closure s
hx : ¬x ∈ s
u : ℕ → X
hux : Tendsto u atTop (𝓝 x)
hus : ∃ᶠ (x : ℕ) in atTop, u x ∈ s
⊢ x ∈ seqClosure s
[PROOFSTEP]
rcases extraction_of_frequently_atTop hus with ⟨φ, φ_mono, hφ⟩
[GOAL]
case neg.intro.intro.intro.intro
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h :
  ∀ (f : X → Prop) (a : X), (∀ (u : ℕ → X), Tendsto u atTop (𝓝 a) → Tendsto (f ∘ u) atTop (𝓝 (f a))) → ContinuousAt f a
s : Set X
x : X
hcx : x ∈ closure s
hx : ¬x ∈ s
u : ℕ → X
hux : Tendsto u atTop (𝓝 x)
hus : ∃ᶠ (x : ℕ) in atTop, u x ∈ s
φ : ℕ → ℕ
φ_mono : StrictMono φ
hφ : ∀ (n : ℕ), u (φ n) ∈ s
⊢ x ∈ seqClosure s
[PROOFSTEP]
exact ⟨u ∘ φ, hφ, hux.comp φ_mono.tendsto_atTop⟩
[GOAL]
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : FrechetUrysohnSpace X
s : Set X
hs : IsSeqClosed s
⊢ IsClosed s
[PROOFSTEP]
rw [← closure_eq_iff_isClosed, ← seqClosure_eq_closure, hs.seqClosure_eq]
[GOAL]
X : Type u_1
Y : Type u_2
inst✝ : UniformSpace X
s : Set X
h : IsSeqCompact s
⊢ TotallyBounded s
[PROOFSTEP]
intro V V_in
[GOAL]
X : Type u_1
Y : Type u_2
inst✝ : UniformSpace X
s : Set X
h : IsSeqCompact s
V : Set (X × X)
V_in : V ∈ 𝓤 X
⊢ ∃ t, Set.Finite t ∧ s ⊆ ⋃ (y : X) (_ : y ∈ t), {x | (x, y) ∈ V}
[PROOFSTEP]
unfold IsSeqCompact at h 
[GOAL]
X : Type u_1
Y : Type u_2
inst✝ : UniformSpace X
s : Set X
h : ∀ ⦃x : ℕ → X⦄, (∀ (n : ℕ), x n ∈ s) → ∃ a, a ∈ s ∧ ∃ φ, StrictMono φ ∧ Tendsto (x ∘ φ) atTop (𝓝 a)
V : Set (X × X)
V_in : V ∈ 𝓤 X
⊢ ∃ t, Set.Finite t ∧ s ⊆ ⋃ (y : X) (_ : y ∈ t), {x | (x, y) ∈ V}
[PROOFSTEP]
contrapose! h
[GOAL]
X : Type u_1
Y : Type u_2
inst✝ : UniformSpace X
s : Set X
V : Set (X × X)
V_in : V ∈ 𝓤 X
h : ∀ (t : Set X), Set.Finite t → ¬s ⊆ ⋃ (y : X) (_ : y ∈ t), {x | (x, y) ∈ V}
⊢ Exists fun ⦃x⦄ => (∀ (n : ℕ), x n ∈ s) ∧ ∀ (a : X), a ∈ s → ∀ (φ : ℕ → ℕ), StrictMono φ → ¬Tendsto (x ∘ φ) atTop (𝓝 a)
[PROOFSTEP]
obtain ⟨u, u_in, hu⟩ : ∃ u : ℕ → X, (∀ n, u n ∈ s) ∧ ∀ n m, m < n → u m ∉ ball (u n) V :=
  by
  simp only [not_subset, mem_iUnion₂, not_exists, exists_prop] at h 
  simpa only [forall_and, ball_image_iff, not_and] using seq_of_forall_finite_exists h
[GOAL]
X : Type u_1
Y : Type u_2
inst✝ : UniformSpace X
s : Set X
V : Set (X × X)
V_in : V ∈ 𝓤 X
h : ∀ (t : Set X), Set.Finite t → ¬s ⊆ ⋃ (y : X) (_ : y ∈ t), {x | (x, y) ∈ V}
⊢ ∃ u, (∀ (n : ℕ), u n ∈ s) ∧ ∀ (n m : ℕ), m < n → ¬u m ∈ ball (u n) V
[PROOFSTEP]
simp only [not_subset, mem_iUnion₂, not_exists, exists_prop] at h 
[GOAL]
X : Type u_1
Y : Type u_2
inst✝ : UniformSpace X
s : Set X
V : Set (X × X)
V_in : V ∈ 𝓤 X
h : ∀ (t : Set X), Set.Finite t → ∃ a, a ∈ s ∧ ∀ (x : X), ¬(x ∈ t ∧ a ∈ {x_1 | (x_1, x) ∈ V})
⊢ ∃ u, (∀ (n : ℕ), u n ∈ s) ∧ ∀ (n m : ℕ), m < n → ¬u m ∈ ball (u n) V
[PROOFSTEP]
simpa only [forall_and, ball_image_iff, not_and] using seq_of_forall_finite_exists h
[GOAL]
case intro.intro
X : Type u_1
Y : Type u_2
inst✝ : UniformSpace X
s : Set X
V : Set (X × X)
V_in : V ∈ 𝓤 X
h : ∀ (t : Set X), Set.Finite t → ¬s ⊆ ⋃ (y : X) (_ : y ∈ t), {x | (x, y) ∈ V}
u : ℕ → X
u_in : ∀ (n : ℕ), u n ∈ s
hu : ∀ (n m : ℕ), m < n → ¬u m ∈ ball (u n) V
⊢ Exists fun ⦃x⦄ => (∀ (n : ℕ), x n ∈ s) ∧ ∀ (a : X), a ∈ s → ∀ (φ : ℕ → ℕ), StrictMono φ → ¬Tendsto (x ∘ φ) atTop (𝓝 a)
[PROOFSTEP]
refine' ⟨u, u_in, fun x _ φ hφ huφ => _⟩
[GOAL]
case intro.intro
X : Type u_1
Y : Type u_2
inst✝ : UniformSpace X
s : Set X
V : Set (X × X)
V_in : V ∈ 𝓤 X
h : ∀ (t : Set X), Set.Finite t → ¬s ⊆ ⋃ (y : X) (_ : y ∈ t), {x | (x, y) ∈ V}
u : ℕ → X
u_in : ∀ (n : ℕ), u n ∈ s
hu : ∀ (n m : ℕ), m < n → ¬u m ∈ ball (u n) V
x : X
x✝ : x ∈ s
φ : ℕ → ℕ
hφ : StrictMono φ
huφ : Tendsto (u ∘ φ) atTop (𝓝 x)
⊢ False
[PROOFSTEP]
obtain ⟨N, hN⟩ : ∃ N, ∀ p q, p ≥ N → q ≥ N → (u (φ p), u (φ q)) ∈ V
[GOAL]
X : Type u_1
Y : Type u_2
inst✝ : UniformSpace X
s : Set X
V : Set (X × X)
V_in : V ∈ 𝓤 X
h : ∀ (t : Set X), Set.Finite t → ¬s ⊆ ⋃ (y : X) (_ : y ∈ t), {x | (x, y) ∈ V}
u : ℕ → X
u_in : ∀ (n : ℕ), u n ∈ s
hu : ∀ (n m : ℕ), m < n → ¬u m ∈ ball (u n) V
x : X
x✝ : x ∈ s
φ : ℕ → ℕ
hφ : StrictMono φ
huφ : Tendsto (u ∘ φ) atTop (𝓝 x)
⊢ ∃ N, ∀ (p q : ℕ), p ≥ N → q ≥ N → (u (φ p), u (φ q)) ∈ V
case intro.intro.intro
X : Type u_1
Y : Type u_2
inst✝ : UniformSpace X
s : Set X
V : Set (X × X)
V_in : V ∈ 𝓤 X
h : ∀ (t : Set X), Set.Finite t → ¬s ⊆ ⋃ (y : X) (_ : y ∈ t), {x | (x, y) ∈ V}
u : ℕ → X
u_in : ∀ (n : ℕ), u n ∈ s
hu : ∀ (n m : ℕ), m < n → ¬u m ∈ ball (u n) V
x : X
x✝ : x ∈ s
φ : ℕ → ℕ
hφ : StrictMono φ
huφ : Tendsto (u ∘ φ) atTop (𝓝 x)
N : ℕ
hN : ∀ (p q : ℕ), p ≥ N → q ≥ N → (u (φ p), u (φ q)) ∈ V
⊢ False
[PROOFSTEP]
exact huφ.cauchySeq.mem_entourage V_in
[GOAL]
case intro.intro.intro
X : Type u_1
Y : Type u_2
inst✝ : UniformSpace X
s : Set X
V : Set (X × X)
V_in : V ∈ 𝓤 X
h : ∀ (t : Set X), Set.Finite t → ¬s ⊆ ⋃ (y : X) (_ : y ∈ t), {x | (x, y) ∈ V}
u : ℕ → X
u_in : ∀ (n : ℕ), u n ∈ s
hu : ∀ (n m : ℕ), m < n → ¬u m ∈ ball (u n) V
x : X
x✝ : x ∈ s
φ : ℕ → ℕ
hφ : StrictMono φ
huφ : Tendsto (u ∘ φ) atTop (𝓝 x)
N : ℕ
hN : ∀ (p q : ℕ), p ≥ N → q ≥ N → (u (φ p), u (φ q)) ∈ V
⊢ False
[PROOFSTEP]
exact hu (φ <| N + 1) (φ N) (hφ <| lt_add_one N) (hN (N + 1) N N.le_succ le_rfl)
[GOAL]
X : Type u_1
Y : Type u_2
inst✝¹ : UniformSpace X
s : Set X
inst✝ : IsCountablyGenerated (𝓤 X)
hs : IsSeqCompact s
l : Filter X
hl : Cauchy l
hls : l ≤ 𝓟 s
⊢ ∃ x, x ∈ s ∧ l ≤ 𝓝 x
[PROOFSTEP]
have := hl.1
[GOAL]
X : Type u_1
Y : Type u_2
inst✝¹ : UniformSpace X
s : Set X
inst✝ : IsCountablyGenerated (𝓤 X)
hs : IsSeqCompact s
l : Filter X
hl : Cauchy l
hls : l ≤ 𝓟 s
this : NeBot l
⊢ ∃ x, x ∈ s ∧ l ≤ 𝓝 x
[PROOFSTEP]
rcases exists_antitone_basis (𝓤 X) with ⟨V, hV⟩
[GOAL]
case intro
X : Type u_1
Y : Type u_2
inst✝¹ : UniformSpace X
s : Set X
inst✝ : IsCountablyGenerated (𝓤 X)
hs : IsSeqCompact s
l : Filter X
hl : Cauchy l
hls : l ≤ 𝓟 s
this : NeBot l
V : ℕ → Set (X × X)
hV : HasAntitoneBasis (𝓤 X) V
⊢ ∃ x, x ∈ s ∧ l ≤ 𝓝 x
[PROOFSTEP]
choose W hW hWV using fun n => comp_mem_uniformity_sets (hV.mem n)
[GOAL]
case intro
X : Type u_1
Y : Type u_2
inst✝¹ : UniformSpace X
s : Set X
inst✝ : IsCountablyGenerated (𝓤 X)
hs : IsSeqCompact s
l : Filter X
hl : Cauchy l
hls : l ≤ 𝓟 s
this : NeBot l
V : ℕ → Set (X × X)
hV : HasAntitoneBasis (𝓤 X) V
W : ℕ → Set (X × X)
hW : ∀ (n : ℕ), W n ∈ 𝓤 X
hWV : ∀ (n : ℕ), W n ○ W n ⊆ V n
⊢ ∃ x, x ∈ s ∧ l ≤ 𝓝 x
[PROOFSTEP]
have hWV' : ∀ n, W n ⊆ V n := fun n ⟨x, y⟩ hx => @hWV n (x, y) ⟨x, refl_mem_uniformity <| hW _, hx⟩
[GOAL]
case intro
X : Type u_1
Y : Type u_2
inst✝¹ : UniformSpace X
s : Set X
inst✝ : IsCountablyGenerated (𝓤 X)
hs : IsSeqCompact s
l : Filter X
hl : Cauchy l
hls : l ≤ 𝓟 s
this : NeBot l
V : ℕ → Set (X × X)
hV : HasAntitoneBasis (𝓤 X) V
W : ℕ → Set (X × X)
hW : ∀ (n : ℕ), W n ∈ 𝓤 X
hWV : ∀ (n : ℕ), W n ○ W n ⊆ V n
hWV' : ∀ (n : ℕ), W n ⊆ V n
⊢ ∃ x, x ∈ s ∧ l ≤ 𝓝 x
[PROOFSTEP]
obtain ⟨t, ht_anti, htl, htW, hts⟩ :
  ∃ t : ℕ → Set X, Antitone t ∧ (∀ n, t n ∈ l) ∧ (∀ n, t n ×ˢ t n ⊆ W n) ∧ ∀ n, t n ⊆ s :=
  by
  have : ∀ n, ∃ t ∈ l, t ×ˢ t ⊆ W n ∧ t ⊆ s :=
    by
    rw [le_principal_iff] at hls 
    have : ∀ n, W n ∩ s ×ˢ s ∈ l ×ˢ l := fun n => inter_mem (hl.2 (hW n)) (prod_mem_prod hls hls)
    simpa only [l.basis_sets.prod_self.mem_iff, true_imp_iff, subset_inter_iff, prod_self_subset_prod_self,
      and_assoc] using this
  choose t htl htW hts using this
  have : ∀ n : ℕ, ⋂ k ≤ n, t k ⊆ t n := fun n => by apply iInter₂_subset; rfl
  exact
    ⟨fun n => ⋂ k ≤ n, t k, fun m n h => biInter_subset_biInter_left fun k (hk : k ≤ m) => hk.trans h, fun n =>
      (biInter_mem (finite_le_nat n)).2 fun k _ => htl k, fun n => (prod_mono (this n) (this n)).trans (htW n), fun n =>
      (this n).trans (hts n)⟩
[GOAL]
X : Type u_1
Y : Type u_2
inst✝¹ : UniformSpace X
s : Set X
inst✝ : IsCountablyGenerated (𝓤 X)
hs : IsSeqCompact s
l : Filter X
hl : Cauchy l
hls : l ≤ 𝓟 s
this : NeBot l
V : ℕ → Set (X × X)
hV : HasAntitoneBasis (𝓤 X) V
W : ℕ → Set (X × X)
hW : ∀ (n : ℕ), W n ∈ 𝓤 X
hWV : ∀ (n : ℕ), W n ○ W n ⊆ V n
hWV' : ∀ (n : ℕ), W n ⊆ V n
⊢ ∃ t, Antitone t ∧ (∀ (n : ℕ), t n ∈ l) ∧ (∀ (n : ℕ), t n ×ˢ t n ⊆ W n) ∧ ∀ (n : ℕ), t n ⊆ s
[PROOFSTEP]
have : ∀ n, ∃ t ∈ l, t ×ˢ t ⊆ W n ∧ t ⊆ s := by
  rw [le_principal_iff] at hls 
  have : ∀ n, W n ∩ s ×ˢ s ∈ l ×ˢ l := fun n => inter_mem (hl.2 (hW n)) (prod_mem_prod hls hls)
  simpa only [l.basis_sets.prod_self.mem_iff, true_imp_iff, subset_inter_iff, prod_self_subset_prod_self,
    and_assoc] using this
[GOAL]
X : Type u_1
Y : Type u_2
inst✝¹ : UniformSpace X
s : Set X
inst✝ : IsCountablyGenerated (𝓤 X)
hs : IsSeqCompact s
l : Filter X
hl : Cauchy l
hls : l ≤ 𝓟 s
this : NeBot l
V : ℕ → Set (X × X)
hV : HasAntitoneBasis (𝓤 X) V
W : ℕ → Set (X × X)
hW : ∀ (n : ℕ), W n ∈ 𝓤 X
hWV : ∀ (n : ℕ), W n ○ W n ⊆ V n
hWV' : ∀ (n : ℕ), W n ⊆ V n
⊢ ∀ (n : ℕ), ∃ t, t ∈ l ∧ t ×ˢ t ⊆ W n ∧ t ⊆ s
[PROOFSTEP]
rw [le_principal_iff] at hls 
[GOAL]
X : Type u_1
Y : Type u_2
inst✝¹ : UniformSpace X
s : Set X
inst✝ : IsCountablyGenerated (𝓤 X)
hs : IsSeqCompact s
l : Filter X
hl : Cauchy l
hls : s ∈ l
this : NeBot l
V : ℕ → Set (X × X)
hV : HasAntitoneBasis (𝓤 X) V
W : ℕ → Set (X × X)
hW : ∀ (n : ℕ), W n ∈ 𝓤 X
hWV : ∀ (n : ℕ), W n ○ W n ⊆ V n
hWV' : ∀ (n : ℕ), W n ⊆ V n
⊢ ∀ (n : ℕ), ∃ t, t ∈ l ∧ t ×ˢ t ⊆ W n ∧ t ⊆ s
[PROOFSTEP]
have : ∀ n, W n ∩ s ×ˢ s ∈ l ×ˢ l := fun n => inter_mem (hl.2 (hW n)) (prod_mem_prod hls hls)
[GOAL]
X : Type u_1
Y : Type u_2
inst✝¹ : UniformSpace X
s : Set X
inst✝ : IsCountablyGenerated (𝓤 X)
hs : IsSeqCompact s
l : Filter X
hl : Cauchy l
hls : s ∈ l
this✝ : NeBot l
V : ℕ → Set (X × X)
hV : HasAntitoneBasis (𝓤 X) V
W : ℕ → Set (X × X)
hW : ∀ (n : ℕ), W n ∈ 𝓤 X
hWV : ∀ (n : ℕ), W n ○ W n ⊆ V n
hWV' : ∀ (n : ℕ), W n ⊆ V n
this : ∀ (n : ℕ), W n ∩ s ×ˢ s ∈ l ×ˢ l
⊢ ∀ (n : ℕ), ∃ t, t ∈ l ∧ t ×ˢ t ⊆ W n ∧ t ⊆ s
[PROOFSTEP]
simpa only [l.basis_sets.prod_self.mem_iff, true_imp_iff, subset_inter_iff, prod_self_subset_prod_self, and_assoc] using
  this
[GOAL]
X : Type u_1
Y : Type u_2
inst✝¹ : UniformSpace X
s : Set X
inst✝ : IsCountablyGenerated (𝓤 X)
hs : IsSeqCompact s
l : Filter X
hl : Cauchy l
hls : l ≤ 𝓟 s
this✝ : NeBot l
V : ℕ → Set (X × X)
hV : HasAntitoneBasis (𝓤 X) V
W : ℕ → Set (X × X)
hW : ∀ (n : ℕ), W n ∈ 𝓤 X
hWV : ∀ (n : ℕ), W n ○ W n ⊆ V n
hWV' : ∀ (n : ℕ), W n ⊆ V n
this : ∀ (n : ℕ), ∃ t, t ∈ l ∧ t ×ˢ t ⊆ W n ∧ t ⊆ s
⊢ ∃ t, Antitone t ∧ (∀ (n : ℕ), t n ∈ l) ∧ (∀ (n : ℕ), t n ×ˢ t n ⊆ W n) ∧ ∀ (n : ℕ), t n ⊆ s
[PROOFSTEP]
choose t htl htW hts using this
[GOAL]
X : Type u_1
Y : Type u_2
inst✝¹ : UniformSpace X
s : Set X
inst✝ : IsCountablyGenerated (𝓤 X)
hs : IsSeqCompact s
l : Filter X
hl : Cauchy l
hls : l ≤ 𝓟 s
this : NeBot l
V : ℕ → Set (X × X)
hV : HasAntitoneBasis (𝓤 X) V
W : ℕ → Set (X × X)
hW : ∀ (n : ℕ), W n ∈ 𝓤 X
hWV : ∀ (n : ℕ), W n ○ W n ⊆ V n
hWV' : ∀ (n : ℕ), W n ⊆ V n
t : ℕ → Set X
htl : ∀ (n : ℕ), t n ∈ l
htW : ∀ (n : ℕ), t n ×ˢ t n ⊆ W n
hts : ∀ (n : ℕ), t n ⊆ s
⊢ ∃ t, Antitone t ∧ (∀ (n : ℕ), t n ∈ l) ∧ (∀ (n : ℕ), t n ×ˢ t n ⊆ W n) ∧ ∀ (n : ℕ), t n ⊆ s
[PROOFSTEP]
have : ∀ n : ℕ, ⋂ k ≤ n, t k ⊆ t n := fun n => by apply iInter₂_subset; rfl
[GOAL]
X : Type u_1
Y : Type u_2
inst✝¹ : UniformSpace X
s : Set X
inst✝ : IsCountablyGenerated (𝓤 X)
hs : IsSeqCompact s
l : Filter X
hl : Cauchy l
hls : l ≤ 𝓟 s
this : NeBot l
V : ℕ → Set (X × X)
hV : HasAntitoneBasis (𝓤 X) V
W : ℕ → Set (X × X)
hW : ∀ (n : ℕ), W n ∈ 𝓤 X
hWV : ∀ (n : ℕ), W n ○ W n ⊆ V n
hWV' : ∀ (n : ℕ), W n ⊆ V n
t : ℕ → Set X
htl : ∀ (n : ℕ), t n ∈ l
htW : ∀ (n : ℕ), t n ×ˢ t n ⊆ W n
hts : ∀ (n : ℕ), t n ⊆ s
n : ℕ
⊢ ⋂ (k : ℕ) (_ : k ≤ n), t k ⊆ t n
[PROOFSTEP]
apply iInter₂_subset
[GOAL]
case j
X : Type u_1
Y : Type u_2
inst✝¹ : UniformSpace X
s : Set X
inst✝ : IsCountablyGenerated (𝓤 X)
hs : IsSeqCompact s
l : Filter X
hl : Cauchy l
hls : l ≤ 𝓟 s
this : NeBot l
V : ℕ → Set (X × X)
hV : HasAntitoneBasis (𝓤 X) V
W : ℕ → Set (X × X)
hW : ∀ (n : ℕ), W n ∈ 𝓤 X
hWV : ∀ (n : ℕ), W n ○ W n ⊆ V n
hWV' : ∀ (n : ℕ), W n ⊆ V n
t : ℕ → Set X
htl : ∀ (n : ℕ), t n ∈ l
htW : ∀ (n : ℕ), t n ×ˢ t n ⊆ W n
hts : ∀ (n : ℕ), t n ⊆ s
n : ℕ
⊢ n ≤ n
[PROOFSTEP]
rfl
[GOAL]
X : Type u_1
Y : Type u_2
inst✝¹ : UniformSpace X
s : Set X
inst✝ : IsCountablyGenerated (𝓤 X)
hs : IsSeqCompact s
l : Filter X
hl : Cauchy l
hls : l ≤ 𝓟 s
this✝ : NeBot l
V : ℕ → Set (X × X)
hV : HasAntitoneBasis (𝓤 X) V
W : ℕ → Set (X × X)
hW : ∀ (n : ℕ), W n ∈ 𝓤 X
hWV : ∀ (n : ℕ), W n ○ W n ⊆ V n
hWV' : ∀ (n : ℕ), W n ⊆ V n
t : ℕ → Set X
htl : ∀ (n : ℕ), t n ∈ l
htW : ∀ (n : ℕ), t n ×ˢ t n ⊆ W n
hts : ∀ (n : ℕ), t n ⊆ s
this : ∀ (n : ℕ), ⋂ (k : ℕ) (_ : k ≤ n), t k ⊆ t n
⊢ ∃ t, Antitone t ∧ (∀ (n : ℕ), t n ∈ l) ∧ (∀ (n : ℕ), t n ×ˢ t n ⊆ W n) ∧ ∀ (n : ℕ), t n ⊆ s
[PROOFSTEP]
exact
  ⟨fun n => ⋂ k ≤ n, t k, fun m n h => biInter_subset_biInter_left fun k (hk : k ≤ m) => hk.trans h, fun n =>
    (biInter_mem (finite_le_nat n)).2 fun k _ => htl k, fun n => (prod_mono (this n) (this n)).trans (htW n), fun n =>
    (this n).trans (hts n)⟩
[GOAL]
case intro.intro.intro.intro.intro
X : Type u_1
Y : Type u_2
inst✝¹ : UniformSpace X
s : Set X
inst✝ : IsCountablyGenerated (𝓤 X)
hs : IsSeqCompact s
l : Filter X
hl : Cauchy l
hls : l ≤ 𝓟 s
this : NeBot l
V : ℕ → Set (X × X)
hV : HasAntitoneBasis (𝓤 X) V
W : ℕ → Set (X × X)
hW : ∀ (n : ℕ), W n ∈ 𝓤 X
hWV : ∀ (n : ℕ), W n ○ W n ⊆ V n
hWV' : ∀ (n : ℕ), W n ⊆ V n
t : ℕ → Set X
ht_anti : Antitone t
htl : ∀ (n : ℕ), t n ∈ l
htW : ∀ (n : ℕ), t n ×ˢ t n ⊆ W n
hts : ∀ (n : ℕ), t n ⊆ s
⊢ ∃ x, x ∈ s ∧ l ≤ 𝓝 x
[PROOFSTEP]
choose u hu using fun n => Filter.nonempty_of_mem (htl n)
[GOAL]
case intro.intro.intro.intro.intro
X : Type u_1
Y : Type u_2
inst✝¹ : UniformSpace X
s : Set X
inst✝ : IsCountablyGenerated (𝓤 X)
hs : IsSeqCompact s
l : Filter X
hl : Cauchy l
hls : l ≤ 𝓟 s
this : NeBot l
V : ℕ → Set (X × X)
hV : HasAntitoneBasis (𝓤 X) V
W : ℕ → Set (X × X)
hW : ∀ (n : ℕ), W n ∈ 𝓤 X
hWV : ∀ (n : ℕ), W n ○ W n ⊆ V n
hWV' : ∀ (n : ℕ), W n ⊆ V n
t : ℕ → Set X
ht_anti : Antitone t
htl : ∀ (n : ℕ), t n ∈ l
htW : ∀ (n : ℕ), t n ×ˢ t n ⊆ W n
hts : ∀ (n : ℕ), t n ⊆ s
u : ℕ → X
hu : ∀ (n : ℕ), u n ∈ t n
⊢ ∃ x, x ∈ s ∧ l ≤ 𝓝 x
[PROOFSTEP]
have huc : CauchySeq u :=
  hV.toHasBasis.cauchySeq_iff.2 fun N _ =>
    ⟨N, fun m hm n hn => hWV' _ <| @htW N (_, _) ⟨ht_anti hm (hu _), ht_anti hn (hu _)⟩⟩
[GOAL]
case intro.intro.intro.intro.intro
X : Type u_1
Y : Type u_2
inst✝¹ : UniformSpace X
s : Set X
inst✝ : IsCountablyGenerated (𝓤 X)
hs : IsSeqCompact s
l : Filter X
hl : Cauchy l
hls : l ≤ 𝓟 s
this : NeBot l
V : ℕ → Set (X × X)
hV : HasAntitoneBasis (𝓤 X) V
W : ℕ → Set (X × X)
hW : ∀ (n : ℕ), W n ∈ 𝓤 X
hWV : ∀ (n : ℕ), W n ○ W n ⊆ V n
hWV' : ∀ (n : ℕ), W n ⊆ V n
t : ℕ → Set X
ht_anti : Antitone t
htl : ∀ (n : ℕ), t n ∈ l
htW : ∀ (n : ℕ), t n ×ˢ t n ⊆ W n
hts : ∀ (n : ℕ), t n ⊆ s
u : ℕ → X
hu : ∀ (n : ℕ), u n ∈ t n
huc : CauchySeq u
⊢ ∃ x, x ∈ s ∧ l ≤ 𝓝 x
[PROOFSTEP]
rcases hs.exists_tendsto (fun n => hts n (hu n)) huc with ⟨x, hxs, hx⟩
[GOAL]
case intro.intro.intro.intro.intro.intro.intro
X : Type u_1
Y : Type u_2
inst✝¹ : UniformSpace X
s : Set X
inst✝ : IsCountablyGenerated (𝓤 X)
hs : IsSeqCompact s
l : Filter X
hl : Cauchy l
hls : l ≤ 𝓟 s
this : NeBot l
V : ℕ → Set (X × X)
hV : HasAntitoneBasis (𝓤 X) V
W : ℕ → Set (X × X)
hW : ∀ (n : ℕ), W n ∈ 𝓤 X
hWV : ∀ (n : ℕ), W n ○ W n ⊆ V n
hWV' : ∀ (n : ℕ), W n ⊆ V n
t : ℕ → Set X
ht_anti : Antitone t
htl : ∀ (n : ℕ), t n ∈ l
htW : ∀ (n : ℕ), t n ×ˢ t n ⊆ W n
hts : ∀ (n : ℕ), t n ⊆ s
u : ℕ → X
hu : ∀ (n : ℕ), u n ∈ t n
huc : CauchySeq u
x : X
hxs : x ∈ s
hx : Tendsto (fun n => u n) atTop (𝓝 x)
⊢ ∃ x, x ∈ s ∧ l ≤ 𝓝 x
[PROOFSTEP]
refine ⟨x, hxs, (nhds_basis_uniformity' hV.toHasBasis).ge_iff.2 fun N _ => ?_⟩
[GOAL]
case intro.intro.intro.intro.intro.intro.intro
X : Type u_1
Y : Type u_2
inst✝¹ : UniformSpace X
s : Set X
inst✝ : IsCountablyGenerated (𝓤 X)
hs : IsSeqCompact s
l : Filter X
hl : Cauchy l
hls : l ≤ 𝓟 s
this : NeBot l
V : ℕ → Set (X × X)
hV : HasAntitoneBasis (𝓤 X) V
W : ℕ → Set (X × X)
hW : ∀ (n : ℕ), W n ∈ 𝓤 X
hWV : ∀ (n : ℕ), W n ○ W n ⊆ V n
hWV' : ∀ (n : ℕ), W n ⊆ V n
t : ℕ → Set X
ht_anti : Antitone t
htl : ∀ (n : ℕ), t n ∈ l
htW : ∀ (n : ℕ), t n ×ˢ t n ⊆ W n
hts : ∀ (n : ℕ), t n ⊆ s
u : ℕ → X
hu : ∀ (n : ℕ), u n ∈ t n
huc : CauchySeq u
x : X
hxs : x ∈ s
hx : Tendsto (fun n => u n) atTop (𝓝 x)
N : ℕ
x✝ : True
⊢ ball x (V N) ∈ l
[PROOFSTEP]
obtain ⟨n, hNn, hn⟩ : ∃ n, N ≤ n ∧ u n ∈ ball x (W N)
[GOAL]
X : Type u_1
Y : Type u_2
inst✝¹ : UniformSpace X
s : Set X
inst✝ : IsCountablyGenerated (𝓤 X)
hs : IsSeqCompact s
l : Filter X
hl : Cauchy l
hls : l ≤ 𝓟 s
this : NeBot l
V : ℕ → Set (X × X)
hV : HasAntitoneBasis (𝓤 X) V
W : ℕ → Set (X × X)
hW : ∀ (n : ℕ), W n ∈ 𝓤 X
hWV : ∀ (n : ℕ), W n ○ W n ⊆ V n
hWV' : ∀ (n : ℕ), W n ⊆ V n
t : ℕ → Set X
ht_anti : Antitone t
htl : ∀ (n : ℕ), t n ∈ l
htW : ∀ (n : ℕ), t n ×ˢ t n ⊆ W n
hts : ∀ (n : ℕ), t n ⊆ s
u : ℕ → X
hu : ∀ (n : ℕ), u n ∈ t n
huc : CauchySeq u
x : X
hxs : x ∈ s
hx : Tendsto (fun n => u n) atTop (𝓝 x)
N : ℕ
x✝ : True
⊢ ∃ n, N ≤ n ∧ u n ∈ ball x (W N)
[PROOFSTEP]
exact ((eventually_ge_atTop N).and (hx <| ball_mem_nhds x (hW N))).exists
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro
X : Type u_1
Y : Type u_2
inst✝¹ : UniformSpace X
s : Set X
inst✝ : IsCountablyGenerated (𝓤 X)
hs : IsSeqCompact s
l : Filter X
hl : Cauchy l
hls : l ≤ 𝓟 s
this : NeBot l
V : ℕ → Set (X × X)
hV : HasAntitoneBasis (𝓤 X) V
W : ℕ → Set (X × X)
hW : ∀ (n : ℕ), W n ∈ 𝓤 X
hWV : ∀ (n : ℕ), W n ○ W n ⊆ V n
hWV' : ∀ (n : ℕ), W n ⊆ V n
t : ℕ → Set X
ht_anti : Antitone t
htl : ∀ (n : ℕ), t n ∈ l
htW : ∀ (n : ℕ), t n ×ˢ t n ⊆ W n
hts : ∀ (n : ℕ), t n ⊆ s
u : ℕ → X
hu : ∀ (n : ℕ), u n ∈ t n
huc : CauchySeq u
x : X
hxs : x ∈ s
hx : Tendsto (fun n => u n) atTop (𝓝 x)
N : ℕ
x✝ : True
n : ℕ
hNn : N ≤ n
hn : u n ∈ ball x (W N)
⊢ ball x (V N) ∈ l
[PROOFSTEP]
refine mem_of_superset (htl n) fun y hy => hWV N ⟨u n, hn, htW N ?_⟩
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro
X : Type u_1
Y : Type u_2
inst✝¹ : UniformSpace X
s : Set X
inst✝ : IsCountablyGenerated (𝓤 X)
hs : IsSeqCompact s
l : Filter X
hl : Cauchy l
hls : l ≤ 𝓟 s
this : NeBot l
V : ℕ → Set (X × X)
hV : HasAntitoneBasis (𝓤 X) V
W : ℕ → Set (X × X)
hW : ∀ (n : ℕ), W n ∈ 𝓤 X
hWV : ∀ (n : ℕ), W n ○ W n ⊆ V n
hWV' : ∀ (n : ℕ), W n ⊆ V n
t : ℕ → Set X
ht_anti : Antitone t
htl : ∀ (n : ℕ), t n ∈ l
htW : ∀ (n : ℕ), t n ×ˢ t n ⊆ W n
hts : ∀ (n : ℕ), t n ⊆ s
u : ℕ → X
hu : ∀ (n : ℕ), u n ∈ t n
huc : CauchySeq u
x : X
hxs : x ∈ s
hx : Tendsto (fun n => u n) atTop (𝓝 x)
N : ℕ
x✝ : True
n : ℕ
hNn : N ≤ n
hn : u n ∈ ball x (W N)
y : X
hy : y ∈ t n
⊢ (u n, (x, y).snd) ∈ t N ×ˢ t N
[PROOFSTEP]
exact ⟨ht_anti hNn (hu n), ht_anti hNn hy⟩
[GOAL]
X : Type u_1
Y : Type u_2
inst✝¹ : UniformSpace X
s : Set X
inst✝ : IsCountablyGenerated (𝓤 X)
⊢ CompactSpace X ↔ SeqCompactSpace X
[PROOFSTEP]
simp only [← isCompact_univ_iff, seqCompactSpace_iff, UniformSpace.isCompact_iff_isSeqCompact]
