-- Mathlib/Topology/UniformSpace/Cauchy.lean
theorem Filter.HasBasis.cauchySeq_iff' {γ} [Nonempty β] [SemilatticeSup β] {u : β → α}
    {p : γ → Prop} {s : γ → Set (α × α)} (H : (𝓤 α).HasBasis p s) :
    CauchySeq u ↔ ∀ i, p i → ∃ N, ∀ n ≥ N, (u n, u N) ∈ s i

Proof state:
case refine_2.intro.intro.intro
α : Type u
β : Type v
uniformSpace : UniformSpace α
γ : Sort u_1
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
u : β → α
p : γ → Prop
s : γ → Set (α × α)
H : (𝓤 α).HasBasis p s
h : ∀ (i : γ), p i → ∃ 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

Tactic:
rcases H.mem_iff.1 ht with ⟨j, hj, hjt⟩

Result:
case refine_2.intro.intro.intro.intro.intro
α : Type u
β : Type v
uniformSpace : UniformSpace α
γ : Sort u_1
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
u : β → α
p : γ → Prop
s : γ → Set (α × α)
H : (𝓤 α).HasBasis p s
h : ∀ (i : γ), p i → ∃ 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

Proof state:
case refine_1
α : Type u
β : Type v
uniformSpace : 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, (u n, u N) ∈ s i

Tactic:
exact (h i hi).imp fun N hN n hn => hN n hn N le_rfl

Result:
no goals

Proof state:
case refine_2.intro.intro.intro.intro.intro.refine_1
α : Type u
β : Type v
uniformSpace : UniformSpace α
γ : Sort u_1
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
u : β → α
p : γ → Prop
s : γ → Set (α × α)
H : (𝓤 α).HasBasis p s
h : ∀ (i : γ), p i → ∃ 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, (u n, u N) ∈ s j
m : β
hm : N ≤ m
n : β
hn : N ≤ n
⊢ ((u m, u n).1, u N) ∈ s j

case refine_2.intro.intro.intro.intro.intro.refine_2
α : Type u
β : Type v
uniformSpace : UniformSpace α
γ : Sort u_1
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
u : β → α
p : γ → Prop
s : γ → Set (α × α)
H : (𝓤 α).HasBasis p s
h : ∀ (i : γ), p i → ∃ 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, (u n, u N) ∈ s j
m : β
hm : N ≤ m
n : β
hn : N ≤ n
⊢ ((u m, u n).2, u N) ∈ s j

Tactic:
exacts [hN m hm, hN n hn]

Result:
no goals

Proof state:
case refine_2.intro.intro.intro.intro.intro
α : Type u
β : Type v
uniformSpace : UniformSpace α
γ : Sort u_1
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
u : β → α
p : γ → Prop
s : γ → Set (α × α)
H : (𝓤 α).HasBasis p s
h : ∀ (i : γ), p i → ∃ 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

Tactic:
refine (h j hj).imp fun N hN m hm n hn => hts ⟨u N, hjt ?_, ht' <| hjt ?_⟩

Result:
case refine_2.intro.intro.intro.intro.intro.refine_1
α : Type u
β : Type v
uniformSpace : UniformSpace α
γ : Sort u_1
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
u : β → α
p : γ → Prop
s : γ → Set (α × α)
H : (𝓤 α).HasBasis p s
h : ∀ (i : γ), p i → ∃ 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, (u n, u N) ∈ s j
m : β
hm : N ≤ m
n : β
hn : N ≤ n
⊢ ((u m, u n).1, u N) ∈ s j

case refine_2.intro.intro.intro.intro.intro.refine_2
α : Type u
β : Type v
uniformSpace : UniformSpace α
γ : Sort u_1
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
u : β → α
p : γ → Prop
s : γ → Set (α × α)
H : (𝓤 α).HasBasis p s
h : ∀ (i : γ), p i → ∃ 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, (u n, u N) ∈ s j
m : β
hm : N ≤ m
n : β
hn : N ≤ n
⊢ ((u m, u n).2, u N) ∈ s j

Proof state:
case refine_2
α : Type u
β : Type v
uniformSpace : UniformSpace α
γ : Sort u_1
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
u : β → α
p : γ → Prop
s : γ → Set (α × α)
H : (𝓤 α).HasBasis p s
h : ∀ (i : γ), p i → ∃ 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

Tactic:
rcases comp_symm_of_uniformity (H.mem_of_mem hi) with ⟨t, ht, ht', hts⟩

Result:
case refine_2.intro.intro.intro
α : Type u
β : Type v
uniformSpace : UniformSpace α
γ : Sort u_1
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
u : β → α
p : γ → Prop
s : γ → Set (α × α)
H : (𝓤 α).HasBasis p s
h : ∀ (i : γ), p i → ∃ 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

Proof state:
α : Type u
β : Type v
uniformSpace : 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, (u n, u N) ∈ s i

Tactic:
refine H.cauchySeq_iff.trans ⟨fun h i hi => ?_, fun h i hi => ?_⟩

Result:
case refine_1
α : Type u
β : Type v
uniformSpace : 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, (u n, u N) ∈ s i

case refine_2
α : Type u
β : Type v
uniformSpace : UniformSpace α
γ : Sort u_1
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
u : β → α
p : γ → Prop
s : γ → Set (α × α)
H : (𝓤 α).HasBasis p s
h : ∀ (i : γ), p i → ∃ 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