α : Type u
β : Type v
inst✝ : UniformSpace α
V : ℕ → Set (α × α)
hV : ∀ (n : ℕ), V n ∈ 𝓤 α
u : ℕ → α
hu : CauchySeq u
this : ∀ (n : ℕ), ∃ N, ∀ (k : ℕ), k ≥ N → ∀ (l : ℕ), l ≥ k → (u l, u k) ∈ V n
⊢ ∃ φ, StrictMono φ ∧ ∀ (n : ℕ), (u (φ (n + 1)), u (φ n)) ∈ V n
α : Type u
β : Type v
inst✝ : UniformSpace α
V : ℕ → Set (α × α)
hV : ∀ (n : ℕ), V n ∈ 𝓤 α
u : ℕ → α
hu : CauchySeq u
⊢ ∃ φ, StrictMono φ ∧ ∀ (n : ℕ), (u (φ (n + 1)), u (φ n)) ∈ V n
have : ∀ n, ∃ N, ∀ k ≥ N, ∀ l ≥ k, (u l, u k) ∈ V n := fun n => by
  rw [cauchySeq_iff] at hu
  rcases hu _ (hV n) with ⟨N, H⟩
  exact ⟨N, fun k hk l hl => H _ (le_trans hk hl) _ hk⟩
case intro.intro
α : Type u
β : Type v
inst✝ : UniformSpace α
V : ℕ → Set (α × α)
hV : ∀ (n : ℕ), V n ∈ 𝓤 α
u : ℕ → α
hu : CauchySeq u
this : ∀ (n : ℕ), ∃ N, ∀ (k : ℕ), k ≥ N → ∀ (l : ℕ), l ≥ k → (u l, u k) ∈ V n
φ : ℕ → ℕ
φ_extr : StrictMono φ
hφ : ∀ (n l : ℕ), l ≥ φ n → (u l, u (φ n)) ∈ V n
⊢ ∃ φ, StrictMono φ ∧ ∀ (n : ℕ), (u (φ (n + 1)), u (φ n)) ∈ V n
α : Type u
β : Type v
inst✝ : UniformSpace α
V : ℕ → Set (α × α)
hV : ∀ (n : ℕ), V n ∈ 𝓤 α
u : ℕ → α
hu : CauchySeq u
this : ∀ (n : ℕ), ∃ N, ∀ (k : ℕ), k ≥ N → ∀ (l : ℕ), l ≥ k → (u l, u k) ∈ V n
⊢ ∃ φ, StrictMono φ ∧ ∀ (n : ℕ), (u (φ (n + 1)), u (φ n)) ∈ V n
obtain ⟨φ : ℕ → ℕ, φ_extr : StrictMono φ, hφ : ∀ n, ∀ l ≥ φ n, (u l, u <| φ n) ∈ V n⟩ :=
  extraction_forall_of_eventually' this
no goals
case intro.intro
α : Type u
β : Type v
inst✝ : UniformSpace α
V : ℕ → Set (α × α)
hV : ∀ (n : ℕ), V n ∈ 𝓤 α
u : ℕ → α
hu : CauchySeq u
this : ∀ (n : ℕ), ∃ N, ∀ (k : ℕ), k ≥ N → ∀ (l : ℕ), l ≥ k → (u l, u k) ∈ V n
φ : ℕ → ℕ
φ_extr : StrictMono φ
hφ : ∀ (n l : ℕ), l ≥ φ n → (u l, u (φ n)) ∈ V n
⊢ ∃ φ, StrictMono φ ∧ ∀ (n : ℕ), (u (φ (n + 1)), u (φ n)) ∈ V n
exact ⟨φ, φ_extr, fun n => hφ _ _ (φ_extr <| lt_add_one n).le⟩
α : Type u
β : Type v
inst✝ : UniformSpace α
V : ℕ → Set (α × α)
hV : ∀ (n : ℕ), V n ∈ 𝓤 α
u : ℕ → α
hu : ∀ (V : Set (α × α)), V ∈ 𝓤 α → ∃ N, ∀ (k : ℕ), k ≥ N → ∀ (l : ℕ), l ≥ N → (u k, u l) ∈ V
n : ℕ
⊢ ∃ N, ∀ (k : ℕ), k ≥ N → ∀ (l : ℕ), l ≥ k → (u l, u k) ∈ V n
α : Type u
β : Type v
inst✝ : UniformSpace α
V : ℕ → Set (α × α)
hV : ∀ (n : ℕ), V n ∈ 𝓤 α
u : ℕ → α
hu : CauchySeq u
n : ℕ
⊢ ∃ N, ∀ (k : ℕ), k ≥ N → ∀ (l : ℕ), l ≥ k → (u l, u k) ∈ V n
rw [cauchySeq_iff] at hu
case intro
α : Type u
β : Type v
inst✝ : UniformSpace α
V : ℕ → Set (α × α)
hV : ∀ (n : ℕ), V n ∈ 𝓤 α
u : ℕ → α
hu : ∀ (V : Set (α × α)), V ∈ 𝓤 α → ∃ N, ∀ (k : ℕ), k ≥ N → ∀ (l : ℕ), l ≥ N → (u k, u l) ∈ V
n N : ℕ
H : ∀ (k : ℕ), k ≥ N → ∀ (l : ℕ), l ≥ N → (u k, u l) ∈ V n
⊢ ∃ N, ∀ (k : ℕ), k ≥ N → ∀ (l : ℕ), l ≥ k → (u l, u k) ∈ V n
α : Type u
β : Type v
inst✝ : UniformSpace α
V : ℕ → Set (α × α)
hV : ∀ (n : ℕ), V n ∈ 𝓤 α
u : ℕ → α
hu : ∀ (V : Set (α × α)), V ∈ 𝓤 α → ∃ N, ∀ (k : ℕ), k ≥ N → ∀ (l : ℕ), l ≥ N → (u k, u l) ∈ V
n : ℕ
⊢ ∃ N, ∀ (k : ℕ), k ≥ N → ∀ (l : ℕ), l ≥ k → (u l, u k) ∈ V n
rcases hu _ (hV n) with ⟨N, H⟩
no goals
case intro
α : Type u
β : Type v
inst✝ : UniformSpace α
V : ℕ → Set (α × α)
hV : ∀ (n : ℕ), V n ∈ 𝓤 α
u : ℕ → α
hu : ∀ (V : Set (α × α)), V ∈ 𝓤 α → ∃ N, ∀ (k : ℕ), k ≥ N → ∀ (l : ℕ), l ≥ N → (u k, u l) ∈ V
n N : ℕ
H : ∀ (k : ℕ), k ≥ N → ∀ (l : ℕ), l ≥ N → (u k, u l) ∈ V n
⊢ ∃ N, ∀ (k : ℕ), k ≥ N → ∀ (l : ℕ), l ≥ k → (u l, u k) ∈ V n
exact ⟨N, fun k hk l hl => H _ (le_trans hk hl) _ hk⟩