case intro.intro
α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : IsCountablyGenerated (𝓤 α)
U : ℕ → Set (α × α)
U_mem : ∀ (n : ℕ), U n ∈ 𝓤 α
HU : ∀ (u : ℕ → α), (∀ (N m n : ℕ), N ≤ m → N ≤ n → (u m, u n) ∈ U N) → ∃ a, Tendsto u atTop (𝓝 a)
U' : ℕ → Set (α × α)
hU' : ∀ {s : Set (α × α)}, s ∈ 𝓤 α ↔ ∃ i, U' i ⊆ s
⊢ CompleteSpace α
α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : IsCountablyGenerated (𝓤 α)
U : ℕ → Set (α × α)
U_mem : ∀ (n : ℕ), U n ∈ 𝓤 α
HU : ∀ (u : ℕ → α), (∀ (N m n : ℕ), N ≤ m → N ≤ n → (u m, u n) ∈ U N) → ∃ a, Tendsto u atTop (𝓝 a)
⊢ CompleteSpace α
obtain ⟨U', -, hU'⟩ := (𝓤 α).exists_antitone_seq
case intro.intro
α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : IsCountablyGenerated (𝓤 α)
U : ℕ → Set (α × α)
U_mem : ∀ (n : ℕ), U n ∈ 𝓤 α
HU : ∀ (u : ℕ → α), (∀ (N m n : ℕ), N ≤ m → N ≤ n → (u m, u n) ∈ U N) → ∃ a, Tendsto u atTop (𝓝 a)
U' : ℕ → Set (α × α)
hU' : ∀ {s : Set (α × α)}, s ∈ 𝓤 α ↔ ∃ i, U' i ⊆ s
Hmem : ∀ (n : ℕ), U n ∩ U' n ∈ 𝓤 α
⊢ CompleteSpace α
case intro.intro
α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : IsCountablyGenerated (𝓤 α)
U : ℕ → Set (α × α)
U_mem : ∀ (n : ℕ), U n ∈ 𝓤 α
HU : ∀ (u : ℕ → α), (∀ (N m n : ℕ), N ≤ m → N ≤ n → (u m, u n) ∈ U N) → ∃ a, Tendsto u atTop (𝓝 a)
U' : ℕ → Set (α × α)
hU' : ∀ {s : Set (α × α)}, s ∈ 𝓤 α ↔ ∃ i, U' i ⊆ s
⊢ CompleteSpace α
have Hmem : ∀ n, U n ∩ U' n ∈ 𝓤 α := fun n => inter_mem (U_mem n) (hU'.2 ⟨n, Subset.refl _⟩)
case intro.intro.refine_1
α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : IsCountablyGenerated (𝓤 α)
U : ℕ → Set (α × α)
U_mem : ∀ (n : ℕ), U n ∈ 𝓤 α
HU : ∀ (u : ℕ → α), (∀ (N m n : ℕ), N ≤ m → N ≤ n → (u m, u n) ∈ U N) → ∃ a, Tendsto u atTop (𝓝 a)
U' : ℕ → Set (α × α)
hU' : ∀ {s : Set (α × α)}, s ∈ 𝓤 α ↔ ∃ i, U' i ⊆ s
Hmem : ∀ (n : ℕ), U n ∩ U' n ∈ 𝓤 α
f✝ : Filter α
hf : Cauchy f✝
N m n : ℕ
hm : N ≤ m
hn : N ≤ n
⊢ (SequentiallyComplete.seq hf Hmem m, SequentiallyComplete.seq hf Hmem n) ∈ U N

case intro.intro.refine_2
α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : IsCountablyGenerated (𝓤 α)
U : ℕ → Set (α × α)
U_mem : ∀ (n : ℕ), U n ∈ 𝓤 α
HU : ∀ (u : ℕ → α), (∀ (N m n : ℕ), N ≤ m → N ≤ n → (u m, u n) ∈ U N) → ∃ a, Tendsto u atTop (𝓝 a)
U' : ℕ → Set (α × α)
hU' : ∀ {s : Set (α × α)}, s ∈ 𝓤 α ↔ ∃ i, U' i ⊆ s
Hmem : ∀ (n : ℕ), U n ∩ U' n ∈ 𝓤 α
f✝ : Filter α
hf : Cauchy f✝
s : Set (α × α)
hs : s ∈ 𝓤 α
⊢ ∃ n, U n ∩ U' n ⊆ s
case intro.intro
α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : IsCountablyGenerated (𝓤 α)
U : ℕ → Set (α × α)
U_mem : ∀ (n : ℕ), U n ∈ 𝓤 α
HU : ∀ (u : ℕ → α), (∀ (N m n : ℕ), N ≤ m → N ≤ n → (u m, u n) ∈ U N) → ∃ a, Tendsto u atTop (𝓝 a)
U' : ℕ → Set (α × α)
hU' : ∀ {s : Set (α × α)}, s ∈ 𝓤 α ↔ ∃ i, U' i ⊆ s
Hmem : ∀ (n : ℕ), U n ∩ U' n ∈ 𝓤 α
⊢ CompleteSpace α
refine ⟨fun hf => (HU (seq hf Hmem) fun N m n hm hn => ?_).imp <|
  le_nhds_of_seq_tendsto_nhds _ _ fun s hs => ?_⟩
no goals
case intro.intro.refine_1
α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : IsCountablyGenerated (𝓤 α)
U : ℕ → Set (α × α)
U_mem : ∀ (n : ℕ), U n ∈ 𝓤 α
HU : ∀ (u : ℕ → α), (∀ (N m n : ℕ), N ≤ m → N ≤ n → (u m, u n) ∈ U N) → ∃ a, Tendsto u atTop (𝓝 a)
U' : ℕ → Set (α × α)
hU' : ∀ {s : Set (α × α)}, s ∈ 𝓤 α ↔ ∃ i, U' i ⊆ s
Hmem : ∀ (n : ℕ), U n ∩ U' n ∈ 𝓤 α
f✝ : Filter α
hf : Cauchy f✝
N m n : ℕ
hm : N ≤ m
hn : N ≤ n
⊢ (SequentiallyComplete.seq hf Hmem m, SequentiallyComplete.seq hf Hmem n) ∈ U N
exact inter_subset_left _ _ (seq_pair_mem hf Hmem hm hn)
case intro.intro.refine_2.intro
α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : IsCountablyGenerated (𝓤 α)
U : ℕ → Set (α × α)
U_mem : ∀ (n : ℕ), U n ∈ 𝓤 α
HU : ∀ (u : ℕ → α), (∀ (N m n : ℕ), N ≤ m → N ≤ n → (u m, u n) ∈ U N) → ∃ a, Tendsto u atTop (𝓝 a)
U' : ℕ → Set (α × α)
hU' : ∀ {s : Set (α × α)}, s ∈ 𝓤 α ↔ ∃ i, U' i ⊆ s
Hmem : ∀ (n : ℕ), U n ∩ U' n ∈ 𝓤 α
f✝ : Filter α
hf : Cauchy f✝
s : Set (α × α)
hs : s ∈ 𝓤 α
N : ℕ
hN : U' N ⊆ s
⊢ ∃ n, U n ∩ U' n ⊆ s
case intro.intro.refine_2
α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : IsCountablyGenerated (𝓤 α)
U : ℕ → Set (α × α)
U_mem : ∀ (n : ℕ), U n ∈ 𝓤 α
HU : ∀ (u : ℕ → α), (∀ (N m n : ℕ), N ≤ m → N ≤ n → (u m, u n) ∈ U N) → ∃ a, Tendsto u atTop (𝓝 a)
U' : ℕ → Set (α × α)
hU' : ∀ {s : Set (α × α)}, s ∈ 𝓤 α ↔ ∃ i, U' i ⊆ s
Hmem : ∀ (n : ℕ), U n ∩ U' n ∈ 𝓤 α
f✝ : Filter α
hf : Cauchy f✝
s : Set (α × α)
hs : s ∈ 𝓤 α
⊢ ∃ n, U n ∩ U' n ⊆ s
rcases hU'.1 hs with ⟨N, hN⟩
no goals
case intro.intro.refine_2.intro
α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : IsCountablyGenerated (𝓤 α)
U : ℕ → Set (α × α)
U_mem : ∀ (n : ℕ), U n ∈ 𝓤 α
HU : ∀ (u : ℕ → α), (∀ (N m n : ℕ), N ≤ m → N ≤ n → (u m, u n) ∈ U N) → ∃ a, Tendsto u atTop (𝓝 a)
U' : ℕ → Set (α × α)
hU' : ∀ {s : Set (α × α)}, s ∈ 𝓤 α ↔ ∃ i, U' i ⊆ s
Hmem : ∀ (n : ℕ), U n ∩ U' n ∈ 𝓤 α
f✝ : Filter α
hf : Cauchy f✝
s : Set (α × α)
hs : s ∈ 𝓤 α
N : ℕ
hN : U' N ⊆ s
⊢ ∃ n, U n ∩ U' n ⊆ s
exact ⟨N, Subset.trans (inter_subset_right _ _) hN⟩