case refine'_1
α : Type u
β : Type v
inst✝² : UniformSpace α
γ : Sort u_1
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
u : β → α
p : γ → Prop
s : γ → Set (α × α)
H : HasBasis (𝓤 α) p s
h : ∀ (i : γ), p i → ∃ N, ∀ (m : β), N ≤ m → ∀ (n : β), N ≤ n → (u m, u n) ∈ s i
i : γ
hi : p i
⊢ ∃ N, ∀ (n : β), n ≥ N → (u n, u N) ∈ s i

case refine'_2
α : Type u
β : Type v
inst✝² : UniformSpace α
γ : Sort u_1
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
u : β → α
p : γ → Prop
s : γ → Set (α × α)
H : HasBasis (𝓤 α) p s
h : ∀ (i : γ), p i → ∃ N, ∀ (n : β), n ≥ N → (u n, u N) ∈ s i
i : γ
hi : p i
⊢ ∃ N, ∀ (m : β), N ≤ m → ∀ (n : β), N ≤ n → (u m, u n) ∈ s i
α : Type u
β : Type v
inst✝² : UniformSpace α
γ : Sort u_1
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
u : β → α
p : γ → Prop
s : γ → Set (α × α)
H : HasBasis (𝓤 α) p s
⊢ CauchySeq u ↔ ∀ (i : γ), p i → ∃ N, ∀ (n : β), n ≥ N → (u n, u N) ∈ s i
refine' H.cauchySeq_iff.trans ⟨fun h i hi => _, fun h i hi => _⟩
no goals
case refine'_1
α : Type u
β : Type v
inst✝² : UniformSpace α
γ : Sort u_1
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
u : β → α
p : γ → Prop
s : γ → Set (α × α)
H : HasBasis (𝓤 α) p s
h : ∀ (i : γ), p i → ∃ N, ∀ (m : β), N ≤ m → ∀ (n : β), N ≤ n → (u m, u n) ∈ s i
i : γ
hi : p i
⊢ ∃ N, ∀ (n : β), n ≥ N → (u n, u N) ∈ s i
exact (h i hi).imp fun N hN n hn => hN n hn N le_rfl
case refine'_2.intro.intro.intro
α : Type u
β : Type v
inst✝² : UniformSpace α
γ : Sort u_1
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
u : β → α
p : γ → Prop
s : γ → Set (α × α)
H : HasBasis (𝓤 α) p s
h : ∀ (i : γ), p i → ∃ N, ∀ (n : β), n ≥ N → (u n, u N) ∈ s i
i : γ
hi : p i
t : Set (α × α)
ht : t ∈ 𝓤 α
ht' : ∀ {a b : α}, (a, b) ∈ t → (b, a) ∈ t
hts : t ○ t ⊆ s i
⊢ ∃ N, ∀ (m : β), N ≤ m → ∀ (n : β), N ≤ n → (u m, u n) ∈ s i
case refine'_2
α : Type u
β : Type v
inst✝² : UniformSpace α
γ : Sort u_1
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
u : β → α
p : γ → Prop
s : γ → Set (α × α)
H : HasBasis (𝓤 α) p s
h : ∀ (i : γ), p i → ∃ N, ∀ (n : β), n ≥ N → (u n, u N) ∈ s i
i : γ
hi : p i
⊢ ∃ N, ∀ (m : β), N ≤ m → ∀ (n : β), N ≤ n → (u m, u n) ∈ s i
rcases comp_symm_of_uniformity (H.mem_of_mem hi) with ⟨t, ht, ht', hts⟩
case refine'_2.intro.intro.intro.intro.intro
α : Type u
β : Type v
inst✝² : UniformSpace α
γ : Sort u_1
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
u : β → α
p : γ → Prop
s : γ → Set (α × α)
H : HasBasis (𝓤 α) p s
h : ∀ (i : γ), p i → ∃ N, ∀ (n : β), n ≥ N → (u n, u N) ∈ s i
i : γ
hi : p i
t : Set (α × α)
ht : t ∈ 𝓤 α
ht' : ∀ {a b : α}, (a, b) ∈ t → (b, a) ∈ t
hts : t ○ t ⊆ s i
j : γ
hj : p j
hjt : s j ⊆ t
⊢ ∃ N, ∀ (m : β), N ≤ m → ∀ (n : β), N ≤ n → (u m, u n) ∈ s i
case refine'_2.intro.intro.intro
α : Type u
β : Type v
inst✝² : UniformSpace α
γ : Sort u_1
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
u : β → α
p : γ → Prop
s : γ → Set (α × α)
H : HasBasis (𝓤 α) p s
h : ∀ (i : γ), p i → ∃ N, ∀ (n : β), n ≥ N → (u n, u N) ∈ s i
i : γ
hi : p i
t : Set (α × α)
ht : t ∈ 𝓤 α
ht' : ∀ {a b : α}, (a, b) ∈ t → (b, a) ∈ t
hts : t ○ t ⊆ s i
⊢ ∃ N, ∀ (m : β), N ≤ m → ∀ (n : β), N ≤ n → (u m, u n) ∈ s i
rcases H.mem_iff.1 ht with ⟨j, hj, hjt⟩
case refine'_2.intro.intro.intro.intro.intro.refine'_1
α : Type u
β : Type v
inst✝² : UniformSpace α
γ : Sort u_1
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
u : β → α
p : γ → Prop
s : γ → Set (α × α)
H : HasBasis (𝓤 α) p s
h : ∀ (i : γ), p i → ∃ N, ∀ (n : β), n ≥ N → (u n, u N) ∈ s i
i : γ
hi : p i
t : Set (α × α)
ht : t ∈ 𝓤 α
ht' : ∀ {a b : α}, (a, b) ∈ t → (b, a) ∈ t
hts : t ○ t ⊆ s i
j : γ
hj : p j
hjt : s j ⊆ t
N : β
hN : ∀ (n : β), n ≥ N → (u n, u N) ∈ s j
m : β
hm : N ≤ m
n : β
hn : N ≤ n
⊢ ((u m, u n).fst, u N) ∈ s j

case refine'_2.intro.intro.intro.intro.intro.refine'_2
α : Type u
β : Type v
inst✝² : UniformSpace α
γ : Sort u_1
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
u : β → α
p : γ → Prop
s : γ → Set (α × α)
H : HasBasis (𝓤 α) p s
h : ∀ (i : γ), p i → ∃ N, ∀ (n : β), n ≥ N → (u n, u N) ∈ s i
i : γ
hi : p i
t : Set (α × α)
ht : t ∈ 𝓤 α
ht' : ∀ {a b : α}, (a, b) ∈ t → (b, a) ∈ t
hts : t ○ t ⊆ s i
j : γ
hj : p j
hjt : s j ⊆ t
N : β
hN : ∀ (n : β), n ≥ N → (u n, u N) ∈ s j
m : β
hm : N ≤ m
n : β
hn : N ≤ n
⊢ ((u m, u n).snd, u N) ∈ s j
case refine'_2.intro.intro.intro.intro.intro
α : Type u
β : Type v
inst✝² : UniformSpace α
γ : Sort u_1
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
u : β → α
p : γ → Prop
s : γ → Set (α × α)
H : HasBasis (𝓤 α) p s
h : ∀ (i : γ), p i → ∃ N, ∀ (n : β), n ≥ N → (u n, u N) ∈ s i
i : γ
hi : p i
t : Set (α × α)
ht : t ∈ 𝓤 α
ht' : ∀ {a b : α}, (a, b) ∈ t → (b, a) ∈ t
hts : t ○ t ⊆ s i
j : γ
hj : p j
hjt : s j ⊆ t
⊢ ∃ N, ∀ (m : β), N ≤ m → ∀ (n : β), N ≤ n → (u m, u n) ∈ s i
refine' (h j hj).imp fun N hN m hm n hn => hts ⟨u N, hjt _, ht' <| hjt _⟩
no goals
case refine'_2.intro.intro.intro.intro.intro.refine'_1
α : Type u
β : Type v
inst✝² : UniformSpace α
γ : Sort u_1
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
u : β → α
p : γ → Prop
s : γ → Set (α × α)
H : HasBasis (𝓤 α) p s
h : ∀ (i : γ), p i → ∃ N, ∀ (n : β), n ≥ N → (u n, u N) ∈ s i
i : γ
hi : p i
t : Set (α × α)
ht : t ∈ 𝓤 α
ht' : ∀ {a b : α}, (a, b) ∈ t → (b, a) ∈ t
hts : t ○ t ⊆ s i
j : γ
hj : p j
hjt : s j ⊆ t
N : β
hN : ∀ (n : β), n ≥ N → (u n, u N) ∈ s j
m : β
hm : N ≤ m
n : β
hn : N ≤ n
⊢ ((u m, u n).fst, u N) ∈ s j

case refine'_2.intro.intro.intro.intro.intro.refine'_2
α : Type u
β : Type v
inst✝² : UniformSpace α
γ : Sort u_1
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
u : β → α
p : γ → Prop
s : γ → Set (α × α)
H : HasBasis (𝓤 α) p s
h : ∀ (i : γ), p i → ∃ N, ∀ (n : β), n ≥ N → (u n, u N) ∈ s i
i : γ
hi : p i
t : Set (α × α)
ht : t ∈ 𝓤 α
ht' : ∀ {a b : α}, (a, b) ∈ t → (b, a) ∈ t
hts : t ○ t ⊆ s i
j : γ
hj : p j
hjt : s j ⊆ t
N : β
hN : ∀ (n : β), n ≥ N → (u n, u N) ∈ s j
m : β
hm : N ≤ m
n : β
hn : N ≤ n
⊢ ((u m, u n).snd, u N) ∈ s j
exacts [hN m hm, hN n hn]