case intro
α : Type u
β : Type v
inst✝ : UniformSpace α
f : Filter α
hf : Cauchy f
U : ℕ → Set (α × α)
U_mem : ∀ (n : ℕ), U n ∈ 𝓤 α
U_le : ∀ (s : Set (α × α)), s ∈ 𝓤 α → ∃ n, U n ⊆ s
a : α
ha : Tendsto (seq hf U_mem) atTop (𝓝 a)
s : Set (α × α)
hs : s ∈ 𝓤 α
m : ℕ
hm : U m ⊆ s
⊢ ∃ t, t ∈ f ∧ t ×ˢ t ⊆ s ∧ ∃ y, (a, y) ∈ s ∧ y ∈ t
α : Type u
β : Type v
inst✝ : UniformSpace α
f : Filter α
hf : Cauchy f
U : ℕ → Set (α × α)
U_mem : ∀ (n : ℕ), U n ∈ 𝓤 α
U_le : ∀ (s : Set (α × α)), s ∈ 𝓤 α → ∃ n, U n ⊆ s
a : α
ha : Tendsto (seq hf U_mem) atTop (𝓝 a)
s : Set (α × α)
hs : s ∈ 𝓤 α
⊢ ∃ t, t ∈ f ∧ t ×ˢ t ⊆ s ∧ ∃ y, (a, y) ∈ s ∧ y ∈ t
rcases U_le s hs with ⟨m, hm⟩
case intro.intro
α : Type u
β : Type v
inst✝ : UniformSpace α
f : Filter α
hf : Cauchy f
U : ℕ → Set (α × α)
U_mem : ∀ (n : ℕ), U n ∈ 𝓤 α
U_le : ∀ (s : Set (α × α)), s ∈ 𝓤 α → ∃ n, U n ⊆ s
a : α
ha : Tendsto (seq hf U_mem) atTop (𝓝 a)
s : Set (α × α)
hs : s ∈ 𝓤 α
m : ℕ
hm : U m ⊆ s
n : ℕ
hn : ∀ (b : ℕ), b ≥ n → seq hf U_mem b ∈ {y | (a, y) ∈ U m}
⊢ ∃ t, t ∈ f ∧ t ×ˢ t ⊆ s ∧ ∃ y, (a, y) ∈ s ∧ y ∈ t
case intro
α : Type u
β : Type v
inst✝ : UniformSpace α
f : Filter α
hf : Cauchy f
U : ℕ → Set (α × α)
U_mem : ∀ (n : ℕ), U n ∈ 𝓤 α
U_le : ∀ (s : Set (α × α)), s ∈ 𝓤 α → ∃ n, U n ⊆ s
a : α
ha : Tendsto (seq hf U_mem) atTop (𝓝 a)
s : Set (α × α)
hs : s ∈ 𝓤 α
m : ℕ
hm : U m ⊆ s
⊢ ∃ t, t ∈ f ∧ t ×ˢ t ⊆ s ∧ ∃ y, (a, y) ∈ s ∧ y ∈ t
rcases tendsto_atTop'.1 ha _ (mem_nhds_left a (U_mem m)) with ⟨n, hn⟩
case intro.intro.refine'_1
α : Type u
β : Type v
inst✝ : UniformSpace α
f : Filter α
hf : Cauchy f
U : ℕ → Set (α × α)
U_mem : ∀ (n : ℕ), U n ∈ 𝓤 α
U_le : ∀ (s : Set (α × α)), s ∈ 𝓤 α → ∃ n, U n ⊆ s
a : α
ha : Tendsto (seq hf U_mem) atTop (𝓝 a)
s : Set (α × α)
hs : s ∈ 𝓤 α
m : ℕ
hm : U m ⊆ s
n : ℕ
hn : ∀ (b : ℕ), b ≥ n → seq hf U_mem b ∈ {y | (a, y) ∈ U m}
⊢ setSeq hf U_mem (max m n) ×ˢ setSeq hf U_mem (max m n) ⊆ s

case intro.intro.refine'_2
α : Type u
β : Type v
inst✝ : UniformSpace α
f : Filter α
hf : Cauchy f
U : ℕ → Set (α × α)
U_mem : ∀ (n : ℕ), U n ∈ 𝓤 α
U_le : ∀ (s : Set (α × α)), s ∈ 𝓤 α → ∃ n, U n ⊆ s
a : α
ha : Tendsto (seq hf U_mem) atTop (𝓝 a)
s : Set (α × α)
hs : s ∈ 𝓤 α
m : ℕ
hm : U m ⊆ s
n : ℕ
hn : ∀ (b : ℕ), b ≥ n → seq hf U_mem b ∈ {y | (a, y) ∈ U m}
⊢ (a, seq hf U_mem (max m n)) ∈ s
case intro.intro
α : Type u
β : Type v
inst✝ : UniformSpace α
f : Filter α
hf : Cauchy f
U : ℕ → Set (α × α)
U_mem : ∀ (n : ℕ), U n ∈ 𝓤 α
U_le : ∀ (s : Set (α × α)), s ∈ 𝓤 α → ∃ n, U n ⊆ s
a : α
ha : Tendsto (seq hf U_mem) atTop (𝓝 a)
s : Set (α × α)
hs : s ∈ 𝓤 α
m : ℕ
hm : U m ⊆ s
n : ℕ
hn : ∀ (b : ℕ), b ≥ n → seq hf U_mem b ∈ {y | (a, y) ∈ U m}
⊢ ∃ t, t ∈ f ∧ t ×ˢ t ⊆ s ∧ ∃ y, (a, y) ∈ s ∧ y ∈ t
refine'
  ⟨setSeq hf U_mem (max m n), setSeq_mem hf U_mem _, _, seq hf U_mem (max m n), _,
    seq_mem hf U_mem _⟩
case intro.intro.refine'_1
α : Type u
β : Type v
inst✝ : UniformSpace α
f : Filter α
hf : Cauchy f
U : ℕ → Set (α × α)
U_mem : ∀ (n : ℕ), U n ∈ 𝓤 α
U_le : ∀ (s : Set (α × α)), s ∈ 𝓤 α → ∃ n, U n ⊆ s
a : α
ha : Tendsto (seq hf U_mem) atTop (𝓝 a)
s : Set (α × α)
hs : s ∈ 𝓤 α
m : ℕ
hm : U m ⊆ s
n : ℕ
hn : ∀ (b : ℕ), b ≥ n → seq hf U_mem b ∈ {y | (a, y) ∈ U m}
this : m ≤ max m n
⊢ setSeq hf U_mem (max m n) ×ˢ setSeq hf U_mem (max m n) ⊆ s
case intro.intro.refine'_1
α : Type u
β : Type v
inst✝ : UniformSpace α
f : Filter α
hf : Cauchy f
U : ℕ → Set (α × α)
U_mem : ∀ (n : ℕ), U n ∈ 𝓤 α
U_le : ∀ (s : Set (α × α)), s ∈ 𝓤 α → ∃ n, U n ⊆ s
a : α
ha : Tendsto (seq hf U_mem) atTop (𝓝 a)
s : Set (α × α)
hs : s ∈ 𝓤 α
m : ℕ
hm : U m ⊆ s
n : ℕ
hn : ∀ (b : ℕ), b ≥ n → seq hf U_mem b ∈ {y | (a, y) ∈ U m}
⊢ setSeq hf U_mem (max m n) ×ˢ setSeq hf U_mem (max m n) ⊆ s
have := le_max_left m n
no goals
case intro.intro.refine'_1
α : Type u
β : Type v
inst✝ : UniformSpace α
f : Filter α
hf : Cauchy f
U : ℕ → Set (α × α)
U_mem : ∀ (n : ℕ), U n ∈ 𝓤 α
U_le : ∀ (s : Set (α × α)), s ∈ 𝓤 α → ∃ n, U n ⊆ s
a : α
ha : Tendsto (seq hf U_mem) atTop (𝓝 a)
s : Set (α × α)
hs : s ∈ 𝓤 α
m : ℕ
hm : U m ⊆ s
n : ℕ
hn : ∀ (b : ℕ), b ≥ n → seq hf U_mem b ∈ {y | (a, y) ∈ U m}
this : m ≤ max m n
⊢ setSeq hf U_mem (max m n) ×ˢ setSeq hf U_mem (max m n) ⊆ s
exact Set.Subset.trans (setSeq_prod_subset hf U_mem this this) hm
no goals
case intro.intro.refine'_2
α : Type u
β : Type v
inst✝ : UniformSpace α
f : Filter α
hf : Cauchy f
U : ℕ → Set (α × α)
U_mem : ∀ (n : ℕ), U n ∈ 𝓤 α
U_le : ∀ (s : Set (α × α)), s ∈ 𝓤 α → ∃ n, U n ⊆ s
a : α
ha : Tendsto (seq hf U_mem) atTop (𝓝 a)
s : Set (α × α)
hs : s ∈ 𝓤 α
m : ℕ
hm : U m ⊆ s
n : ℕ
hn : ∀ (b : ℕ), b ≥ n → seq hf U_mem b ∈ {y | (a, y) ∈ U m}
⊢ (a, seq hf U_mem (max m n)) ∈ s
exact hm (hn _ <| le_max_right m n)