-- Mathlib/Topology/MetricSpace/CauSeqFilter.lean
theorem CauSeq.cauchySeq (f : CauSeq β norm) : CauchySeq f

Proof state:
β : Type v
inst✝ : NormedField β
f : CauSeq β norm
⊢ (map (↑f) atTop).NeBot

Tactic:
infer_instance

Result:
no goals

Proof state:
case intro.intro.intro.right.mk.intro.intro.intro.intro.intro
β : Type v
inst✝ : NormedField β
f : CauSeq β norm
s : Set (β × β)
hs : s ∈ uniformity β
ε : ℝ
hε : ε > 0
hεs : ∀ ⦃a b : β⦄, dist a b < ε → (a, b) ∈ s
N : ℕ
hN : ∀ j ≥ N, ∀ k ≥ N, ‖↑f j - ↑f k‖ < ε
a b : β
a' : ℕ
ha'1 : a' ≥ N
ha'2 : ↑f a' = a
b' : ℕ
hb'1 : b' ≥ N
hb'2 : ↑f b' = b
⊢ (↑f a', ↑f b') ∈ s

Tactic:
apply hεs

Result:
case intro.intro.intro.right.mk.intro.intro.intro.intro.intro.a
β : Type v
inst✝ : NormedField β
f : CauSeq β norm
s : Set (β × β)
hs : s ∈ uniformity β
ε : ℝ
hε : ε > 0
hεs : ∀ ⦃a b : β⦄, dist a b < ε → (a, b) ∈ s
N : ℕ
hN : ∀ j ≥ N, ∀ k ≥ N, ‖↑f j - ↑f k‖ < ε
a b : β
a' : ℕ
ha'1 : a' ≥ N
ha'2 : ↑f a' = a
b' : ℕ
hb'1 : b' ≥ N
hb'2 : ↑f b' = b
⊢ dist (↑f a') (↑f b') < ε

Proof state:
case intro.intro.intro.left
β : Type v
inst✝ : NormedField β
f : CauSeq β norm
s : Set (β × β)
hs : s ∈ uniformity β
ε : ℝ
hε : ε > 0
hεs : ∀ ⦃a b : β⦄, dist a b < ε → (a, b) ∈ s
N : ℕ
hN : ∀ j ≥ N, ∀ k ≥ N, ‖↑f j - ↑f k‖ < ε
⊢ ∃ a, ∀ b ≥ a, b ∈ ↑f ⁻¹' (↑f '' {n | n ≥ N})

Tactic:
exists N

Result:
case intro.intro.intro.left
β : Type v
inst✝ : NormedField β
f : CauSeq β norm
s : Set (β × β)
hs : s ∈ uniformity β
ε : ℝ
hε : ε > 0
hεs : ∀ ⦃a b : β⦄, dist a b < ε → (a, b) ∈ s
N : ℕ
hN : ∀ j ≥ N, ∀ k ≥ N, ‖↑f j - ↑f k‖ < ε
⊢ ∀ b ≥ N, b ∈ ↑f ⁻¹' (↑f '' {n | n ≥ N})

Proof state:
case intro.intro.intro.right.mk.intro.intro.intro.intro.intro.a
β : Type v
inst✝ : NormedField β
f : CauSeq β norm
s : Set (β × β)
hs : s ∈ uniformity β
ε : ℝ
hε : ε > 0
hεs : ∀ ⦃a b : β⦄, dist a b < ε → (a, b) ∈ s
N : ℕ
hN : ∀ j ≥ N, ∀ k ≥ N, ‖↑f j - ↑f k‖ < ε
a b : β
a' : ℕ
ha'1 : a' ≥ N
ha'2 : ↑f a' = a
b' : ℕ
hb'1 : b' ≥ N
hb'2 : ↑f b' = b
⊢ dist (↑f a') (↑f b') < ε

Tactic:
rw [dist_eq_norm]

Result:
case intro.intro.intro.right.mk.intro.intro.intro.intro.intro.a
β : Type v
inst✝ : NormedField β
f : CauSeq β norm
s : Set (β × β)
hs : s ∈ uniformity β
ε : ℝ
hε : ε > 0
hεs : ∀ ⦃a b : β⦄, dist a b < ε → (a, b) ∈ s
N : ℕ
hN : ∀ j ≥ N, ∀ k ≥ N, ‖↑f j - ↑f k‖ < ε
a b : β
a' : ℕ
ha'1 : a' ≥ N
ha'2 : ↑f a' = a
b' : ℕ
hb'1 : b' ≥ N
hb'2 : ↑f b' = b
⊢ ‖↑f a' - ↑f b'‖ < ε

Proof state:
case intro.intro.intro.right.mk.intro.intro.intro.intro.intro
β : Type v
inst✝ : NormedField β
f : CauSeq β norm
s : Set (β × β)
hs : s ∈ uniformity β
ε : ℝ
hε : ε > 0
hεs : ∀ ⦃a b : β⦄, dist a b < ε → (a, b) ∈ s
N : ℕ
hN : ∀ j ≥ N, ∀ k ≥ N, ‖↑f j - ↑f k‖ < ε
a b : β
a' : ℕ
ha'1 : a' ∈ {n | n ≥ N}
ha'2 : ↑f a' = (a, b).1
b' : ℕ
hb'1 : b' ∈ {n | n ≥ N}
hb'2 : ↑f b' = (a, b).2
⊢ (a, b) ∈ s

Tactic:
dsimp at ha'1 ha'2 hb'1 hb'2

Result:
case intro.intro.intro.right.mk.intro.intro.intro.intro.intro
β : Type v
inst✝ : NormedField β
f : CauSeq β norm
s : Set (β × β)
hs : s ∈ uniformity β
ε : ℝ
hε : ε > 0
hεs : ∀ ⦃a b : β⦄, dist a b < ε → (a, b) ∈ s
N : ℕ
hN : ∀ j ≥ N, ∀ k ≥ N, ‖↑f j - ↑f k‖ < ε
a b : β
a' : ℕ
ha'1 : a' ≥ N
ha'2 : ↑f a' = a
b' : ℕ
hb'1 : b' ≥ N
hb'2 : ↑f b' = b
⊢ (a, b) ∈ s

Proof state:
case intro.intro.intro
β : Type v
inst✝ : NormedField β
f : CauSeq β norm
s : Set (β × β)
hs : s ∈ uniformity β
ε : ℝ
hε : ε > 0
hεs : ∀ ⦃a b : β⦄, dist a b < ε → (a, b) ∈ s
N : ℕ
hN : ∀ j ≥ N, ∀ k ≥ N, ‖↑f j - ↑f k‖ < ε
⊢ (∃ a, ∀ b ≥ a, b ∈ ↑f ⁻¹' (↑f '' {n | n ≥ N})) ∧ (↑f '' {n | n ≥ N}) ×ˢ (↑f '' {n | n ≥ N}) ⊆ s

Tactic:
constructor

Result:
case intro.intro.intro.left
β : Type v
inst✝ : NormedField β
f : CauSeq β norm
s : Set (β × β)
hs : s ∈ uniformity β
ε : ℝ
hε : ε > 0
hεs : ∀ ⦃a b : β⦄, dist a b < ε → (a, b) ∈ s
N : ℕ
hN : ∀ j ≥ N, ∀ k ≥ N, ‖↑f j - ↑f k‖ < ε
⊢ ∃ a, ∀ b ≥ a, b ∈ ↑f ⁻¹' (↑f '' {n | n ≥ N})

case intro.intro.intro.right
β : Type v
inst✝ : NormedField β
f : CauSeq β norm
s : Set (β × β)
hs : s ∈ uniformity β
ε : ℝ
hε : ε > 0
hεs : ∀ ⦃a b : β⦄, dist a b < ε → (a, b) ∈ s
N : ℕ
hN : ∀ j ≥ N, ∀ k ≥ N, ‖↑f j - ↑f k‖ < ε
⊢ (↑f '' {n | n ≥ N}) ×ˢ (↑f '' {n | n ≥ N}) ⊆ s

Proof state:
case intro.intro.intro.right.mk.intro.intro.intro.intro.intro.a
β : Type v
inst✝ : NormedField β
f : CauSeq β norm
s : Set (β × β)
hs : s ∈ uniformity β
ε : ℝ
hε : ε > 0
hεs : ∀ ⦃a b : β⦄, dist a b < ε → (a, b) ∈ s
N : ℕ
hN : ∀ j ≥ N, ∀ k ≥ N, ‖↑f j - ↑f k‖ < ε
a b : β
a' : ℕ
ha'1 : a' ≥ N
ha'2 : ↑f a' = a
b' : ℕ
hb'1 : b' ≥ N
hb'2 : ↑f b' = b
⊢ ‖↑f a' - ↑f b'‖ < ε

Tactic:
apply hN <;> assumption

Result:
no goals

Proof state:
case intro.intro.intro.left
β : Type v
inst✝ : NormedField β
f : CauSeq β norm
s : Set (β × β)
hs : s ∈ uniformity β
ε : ℝ
hε : ε > 0
hεs : ∀ ⦃a b : β⦄, dist a b < ε → (a, b) ∈ s
N : ℕ
hN : ∀ j ≥ N, ∀ k ≥ N, ‖↑f j - ↑f k‖ < ε
⊢ ∀ b ≥ N, b ∈ ↑f ⁻¹' (↑f '' {n | n ≥ N})

Tactic:
intro b hb

Result:
case intro.intro.intro.left
β : Type v
inst✝ : NormedField β
f : CauSeq β norm
s : Set (β × β)
hs : s ∈ uniformity β
ε : ℝ
hε : ε > 0
hεs : ∀ ⦃a b : β⦄, dist a b < ε → (a, b) ∈ s
N : ℕ
hN : ∀ j ≥ N, ∀ k ≥ N, ‖↑f j - ↑f k‖ < ε
b : ℕ
hb : b ≥ N
⊢ b ∈ ↑f ⁻¹' (↑f '' {n | n ≥ N})

Proof state:
case intro.intro.intro.left
β : Type v
inst✝ : NormedField β
f : CauSeq β norm
s : Set (β × β)
hs : s ∈ uniformity β
ε : ℝ
hε : ε > 0
hεs : ∀ ⦃a b : β⦄, dist a b < ε → (a, b) ∈ s
N : ℕ
hN : ∀ j ≥ N, ∀ k ≥ N, ‖↑f j - ↑f k‖ < ε
b : ℕ
hb : b ≥ N
⊢ b ∈ ↑f ⁻¹' (↑f '' {n | n ≥ N})

Tactic:
exists b

Result:
no goals

Proof state:
case intro.intro.intro
β : Type v
inst✝ : NormedField β
f : CauSeq β norm
s : Set (β × β)
hs : s ∈ uniformity β
ε : ℝ
hε : ε > 0
hεs : ∀ ⦃a b : β⦄, dist a b < ε → (a, b) ∈ s
N : ℕ
hN : ∀ j ≥ N, ∀ k ≥ N, ‖↑f j - ↑f k‖ < ε
⊢ ↑f '' {n | n ≥ N} ∈ map (↑f) atTop ∧ (↑f '' {n | n ≥ N}) ×ˢ (↑f '' {n | n ≥ N}) ⊆ s

Tactic:
simp only [exists_prop, mem_atTop_sets, mem_map, mem_image, mem_setOf_eq]

Result:
case intro.intro.intro
β : Type v
inst✝ : NormedField β
f : CauSeq β norm
s : Set (β × β)
hs : s ∈ uniformity β
ε : ℝ
hε : ε > 0
hεs : ∀ ⦃a b : β⦄, dist a b < ε → (a, b) ∈ s
N : ℕ
hN : ∀ j ≥ N, ∀ k ≥ N, ‖↑f j - ↑f k‖ < ε
⊢ (∃ a, ∀ b ≥ a, b ∈ ↑f ⁻¹' (↑f '' {n | n ≥ N})) ∧ (↑f '' {n | n ≥ N}) ×ˢ (↑f '' {n | n ≥ N}) ⊆ s

Proof state:
case intro.intro.intro.right
β : Type v
inst✝ : NormedField β
f : CauSeq β norm
s : Set (β × β)
hs : s ∈ uniformity β
ε : ℝ
hε : ε > 0
hεs : ∀ ⦃a b : β⦄, dist a b < ε → (a, b) ∈ s
N : ℕ
hN : ∀ j ≥ N, ∀ k ≥ N, ‖↑f j - ↑f k‖ < ε
⊢ (↑f '' {n | n ≥ N}) ×ˢ (↑f '' {n | n ≥ N}) ⊆ s

Tactic:
rintro ⟨a, b⟩ ⟨⟨a', ⟨ha'1, ha'2⟩⟩, ⟨b', ⟨hb'1, hb'2⟩⟩⟩

Result:
case intro.intro.intro.right.mk.intro.intro.intro.intro.intro
β : Type v
inst✝ : NormedField β
f : CauSeq β norm
s : Set (β × β)
hs : s ∈ uniformity β
ε : ℝ
hε : ε > 0
hεs : ∀ ⦃a b : β⦄, dist a b < ε → (a, b) ∈ s
N : ℕ
hN : ∀ j ≥ N, ∀ k ≥ N, ‖↑f j - ↑f k‖ < ε
a b : β
a' : ℕ
ha'1 : a' ∈ {n | n ≥ N}
ha'2 : ↑f a' = (a, b).1
b' : ℕ
hb'1 : b' ∈ {n | n ≥ N}
hb'2 : ↑f b' = (a, b).2
⊢ (a, b) ∈ s

Proof state:
case intro.intro.intro
β : Type v
inst✝ : NormedField β
f : CauSeq β norm
s : Set (β × β)
hs : s ∈ uniformity β
ε : ℝ
hε : ε > 0
hεs : ∀ ⦃a b : β⦄, dist a b < ε → (a, b) ∈ s
N : ℕ
hN : ∀ j ≥ N, ∀ k ≥ N, ‖↑f j - ↑f k‖ < ε
⊢ ∃ t ∈ map (↑f) atTop, t ×ˢ t ⊆ s

Tactic:
exists { n | n ≥ N }.image f

Result:
case intro.intro.intro
β : Type v
inst✝ : NormedField β
f : CauSeq β norm
s : Set (β × β)
hs : s ∈ uniformity β
ε : ℝ
hε : ε > 0
hεs : ∀ ⦃a b : β⦄, dist a b < ε → (a, b) ∈ s
N : ℕ
hN : ∀ j ≥ N, ∀ k ≥ N, ‖↑f j - ↑f k‖ < ε
⊢ ↑f '' {n | n ≥ N} ∈ map (↑f) atTop ∧ (↑f '' {n | n ≥ N}) ×ˢ (↑f '' {n | n ≥ N}) ⊆ s