case refine'_1.a
α : 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
N m n : ℕ
hm : N ≤ m
hn : N ≤ n
p : α × α
hp : p ∈ setSeq hf U_mem m ×ˢ setSeq hf U_mem n
⊢ p.fst ∈ setSeq hf U_mem N

case refine'_2.a
α : 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
N m n : ℕ
hm : N ≤ m
hn : N ≤ n
p : α × α
hp : p ∈ setSeq hf U_mem m ×ˢ setSeq hf U_mem n
⊢ p.snd ∈ setSeq hf U_mem N
α : 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
N m n : ℕ
hm : N ≤ m
hn : N ≤ n
p : α × α
hp : p ∈ setSeq hf U_mem m ×ˢ setSeq hf U_mem n
⊢ p ∈ U N
refine' (setSeqAux hf U_mem N).2.2 ⟨_, _⟩ <;> apply setSeq_sub_aux
case refine'_2.a
α : 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
N m n : ℕ
hm : N ≤ m
hn : N ≤ n
p : α × α
hp : p ∈ setSeq hf U_mem m ×ˢ setSeq hf U_mem n
⊢ p.snd ∈ setSeq hf U_mem N
case refine'_1.a
α : 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
N m n : ℕ
hm : N ≤ m
hn : N ≤ n
p : α × α
hp : p ∈ setSeq hf U_mem m ×ˢ setSeq hf U_mem n
⊢ p.fst ∈ setSeq hf U_mem N

case refine'_2.a
α : 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
N m n : ℕ
hm : N ≤ m
hn : N ≤ n
p : α × α
hp : p ∈ setSeq hf U_mem m ×ˢ setSeq hf U_mem n
⊢ p.snd ∈ setSeq hf U_mem N
exact setSeq_mono hf U_mem hm hp.1
no goals
case refine'_2.a
α : 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
N m n : ℕ
hm : N ≤ m
hn : N ≤ n
p : α × α
hp : p ∈ setSeq hf U_mem m ×ˢ setSeq hf U_mem n
⊢ p.snd ∈ setSeq hf U_mem N
exact setSeq_mono hf U_mem hn hp.2