-- Mathlib/Topology/MetricSpace/PiNat.lean
theorem exists_nat_nat_continuous_surjective_of_completeSpace (α : Type*) [MetricSpace α]
    [CompleteSpace α] [SecondCountableTopology α] [Nonempty α] :
    ∃ f : (ℕ → ℕ) → α, Continuous f ∧ Surjective f

Proof state:
α : Type u_2
inst✝³ : MetricSpace α
inst✝² : CompleteSpace α
inst✝¹ : SecondCountableTopology α
inst✝ : Nonempty α
this : MetricSpace (ℕ → ℕ) := metricSpaceNatNat
I0 : 0 < 1 / 2
I1 : 1 / 2 < 1
u : ℕ → α
hu : DenseRange u
s : Set (ℕ → ℕ) := {x | (⋂ n, closedBall (u (x n)) ((1 / 2) ^ n)).Nonempty}
g : ↑s → α := fun x => Set.Nonempty.some ⋯
A : ∀ (x : ↑s) (n : ℕ), dist (g x) (u (↑x n)) ≤ (1 / 2) ^ n
g_cont : Continuous g
g_surj : Surjective g
x : ℕ → ℕ
hx : ClusterPt x (𝓟 s)
L : Tendsto (fun n => diam (closedBall (u (x n)) ((1 / 2) ^ n))) atTop (𝓝 0)
N : ℕ
⊢ (⋂ n, ⋂ (_ : n ≤ N), closedBall (u (x n)) ((1 / 2) ^ n)).Nonempty

Tactic:
obtain ⟨y, hxy, ys⟩ : ∃ y, y ∈ ball x ((1 / 2) ^ N) ∩ s :=
  clusterPt_principal_iff.1 hx _ (ball_mem_nhds x (pow_pos I0 N))

Result:
case intro.intro
α : Type u_2
inst✝³ : MetricSpace α
inst✝² : CompleteSpace α
inst✝¹ : SecondCountableTopology α
inst✝ : Nonempty α
this : MetricSpace (ℕ → ℕ) := metricSpaceNatNat
I0 : 0 < 1 / 2
I1 : 1 / 2 < 1
u : ℕ → α
hu : DenseRange u
s : Set (ℕ → ℕ) := {x | (⋂ n, closedBall (u (x n)) ((1 / 2) ^ n)).Nonempty}
g : ↑s → α := fun x => Set.Nonempty.some ⋯
A : ∀ (x : ↑s) (n : ℕ), dist (g x) (u (↑x n)) ≤ (1 / 2) ^ n
g_cont : Continuous g
g_surj : Surjective g
x : ℕ → ℕ
hx : ClusterPt x (𝓟 s)
L : Tendsto (fun n => diam (closedBall (u (x n)) ((1 / 2) ^ n))) atTop (𝓝 0)
N : ℕ
y : ℕ → ℕ
hxy : y ∈ ball x ((1 / 2) ^ N)
ys : y ∈ s
⊢ (⋂ n, ⋂ (_ : n ≤ N), closedBall (u (x n)) ((1 / 2) ^ n)).Nonempty

Proof state:
α : Type u_2
inst✝³ : MetricSpace α
inst✝² : CompleteSpace α
inst✝¹ : SecondCountableTopology α
inst✝ : Nonempty α
this : MetricSpace (ℕ → ℕ) := metricSpaceNatNat
I0 : 0 < 1 / 2
I1 : 1 / 2 < 1
u : ℕ → α
hu : DenseRange u
s : Set (ℕ → ℕ) := {x | (⋂ n, closedBall (u (x n)) ((1 / 2) ^ n)).Nonempty}
g : ↑s → α := fun x => Set.Nonempty.some ⋯
A : ∀ (x : ↑s) (n : ℕ), dist (g x) (u (↑x n)) ≤ (1 / 2) ^ n
y x : ↑s
hxy : dist x y < 1
hne : x ≠ y
hne' : ↑x ≠ ↑y
dist' : dist x y = dist ↑x ↑y
n : ℕ := firstDiff ↑x ↑y - 1
h : firstDiff ↑x ↑y ≤ 0
⊢ dist ↑x ↑y < 1

Tactic:
exact hxy

Result:
no goals

Proof state:
α : Type u_2
inst✝³ : MetricSpace α
inst✝² : CompleteSpace α
inst✝¹ : SecondCountableTopology α
inst✝ : Nonempty α
this : MetricSpace (ℕ → ℕ) := metricSpaceNatNat
I0 : 0 < 1 / 2
I1 : 1 / 2 < 1
u : ℕ → α
hu : DenseRange u
s : Set (ℕ → ℕ) := {x | (⋂ n, closedBall (u (x n)) ((1 / 2) ^ n)).Nonempty}
g : ↑s → α := fun x => Set.Nonempty.some ⋯
A : ∀ (x : ↑s) (n : ℕ), dist (g x) (u (↑x n)) ≤ (1 / 2) ^ n
y x : ↑s
hxy : dist x y < 1
hne : x ≠ y
hne' : ↑x ≠ ↑y
dist' : dist x y = dist ↑x ↑y
n : ℕ := firstDiff ↑x ↑y - 1
diff_pos : 0 < firstDiff ↑x ↑y
hn : firstDiff ↑x ↑y = n + 1
B : ↑x n = ↑y n
⊢ (1 / 2) ^ n + (1 / 2) ^ n = 4 * (1 / 2) ^ (n + 1)

Tactic:
ring

Result:
no goals

Proof state:
α : Type u_2
inst✝³ : MetricSpace α
inst✝² : CompleteSpace α
inst✝¹ : SecondCountableTopology α
inst✝ : Nonempty α
this : MetricSpace (ℕ → ℕ) := metricSpaceNatNat
I0 : 0 < 1 / 2
I1 : 1 / 2 < 1
u : ℕ → α
hu : DenseRange u
s : Set (ℕ → ℕ) := {x | (⋂ n, closedBall (u (x n)) ((1 / 2) ^ n)).Nonempty}
g : ↑s → α := fun x => Set.Nonempty.some ⋯
A : ∀ (x : ↑s) (n : ℕ), dist (g x) (u (↑x n)) ≤ (1 / 2) ^ n
y x : ↑s
hxy : dist x y < 1
hne : x ≠ y
hne' : ↑x ≠ ↑y
dist' : dist x y = dist ↑x ↑y
n : ℕ := firstDiff ↑x ↑y - 1
diff_pos : 0 < firstDiff ↑x ↑y
hn : firstDiff ↑x ↑y = n + 1
B : ↑x n = ↑y n
⊢ dist (g x) (u (↑x n)) + dist (g y) (u (↑x n)) = dist (g x) (u (↑x n)) + dist (g y) (u (↑y n))

Tactic:
rw [← B]

Result:
no goals

Proof state:
α : Type u_2
inst✝³ : MetricSpace α
inst✝² : CompleteSpace α
inst✝¹ : SecondCountableTopology α
inst✝ : Nonempty α
this : MetricSpace (ℕ → ℕ) := metricSpaceNatNat
I0 : 0 < 1 / 2
I1 : 1 / 2 < 1
u : ℕ → α
hu : DenseRange u
s : Set (ℕ → ℕ) := {x | (⋂ n, closedBall (u (x n)) ((1 / 2) ^ n)).Nonempty}
g : ↑s → α := fun x => Set.Nonempty.some ⋯
A : ∀ (x : ↑s) (n : ℕ), dist (g x) (u (↑x n)) ≤ (1 / 2) ^ n
g_cont : Continuous g
y : α
n : ℕ
⊢ ∃ j, y ∈ closedBall (u j) ((1 / 2) ^ n)

Tactic:
rcases hu.exists_dist_lt y (by simp : (0 : ℝ) < (1 / 2) ^ n) with ⟨j, hj⟩

Result:
case intro
α : Type u_2
inst✝³ : MetricSpace α
inst✝² : CompleteSpace α
inst✝¹ : SecondCountableTopology α
inst✝ : Nonempty α
this : MetricSpace (ℕ → ℕ) := metricSpaceNatNat
I0 : 0 < 1 / 2
I1 : 1 / 2 < 1
u : ℕ → α
hu : DenseRange u
s : Set (ℕ → ℕ) := {x | (⋂ n, closedBall (u (x n)) ((1 / 2) ^ n)).Nonempty}
g : ↑s → α := fun x => Set.Nonempty.some ⋯
A : ∀ (x : ↑s) (n : ℕ), dist (g x) (u (↑x n)) ≤ (1 / 2) ^ n
g_cont : Continuous g
y : α
n j : ℕ
hj : dist y (u j) < (1 / 2) ^ n
⊢ ∃ j, y ∈ closedBall (u j) ((1 / 2) ^ n)

Proof state:
α : Type u_2
inst✝³ : MetricSpace α
inst✝² : CompleteSpace α
inst✝¹ : SecondCountableTopology α
inst✝ : Nonempty α
this : MetricSpace (ℕ → ℕ) := metricSpaceNatNat
I0 : 0 < 1 / 2
I1 : 1 / 2 < 1
u : ℕ → α
hu : DenseRange u
s : Set (ℕ → ℕ) := {x | (⋂ n, closedBall (u (x n)) ((1 / 2) ^ n)).Nonempty}
g : ↑s → α := fun x => Set.Nonempty.some ⋯
A : ∀ (x : ↑s) (n : ℕ), dist (g x) (u (↑x n)) ≤ (1 / 2) ^ n
g_cont : Continuous g
g_surj : Surjective g
s_closed : IsClosed s
⊢ s.Nonempty

Tactic:
simpa only [nonempty_coe_sort] using g_surj.nonempty

Result:
no goals

Proof state:
case inr
α : Type u_2
inst✝³ : MetricSpace α
inst✝² : CompleteSpace α
inst✝¹ : SecondCountableTopology α
inst✝ : Nonempty α
this : MetricSpace (ℕ → ℕ) := metricSpaceNatNat
I0 : 0 < 1 / 2
I1 : 1 / 2 < 1
u : ℕ → α
hu : DenseRange u
s : Set (ℕ → ℕ) := {x | (⋂ n, closedBall (u (x n)) ((1 / 2) ^ n)).Nonempty}
g : ↑s → α := fun x => Set.Nonempty.some ⋯
A : ∀ (x : ↑s) (n : ℕ), dist (g x) (u (↑x n)) ≤ (1 / 2) ^ n
y x : ↑s
hxy : dist x y < 1
hne : x ≠ y
hne' : ↑x ≠ ↑y
dist' : dist x y = dist ↑x ↑y
n : ℕ := firstDiff ↑x ↑y - 1
⊢ dist (g x) (g y) ≤ 4 * dist x y

Tactic:
have diff_pos : 0 < firstDiff x.1 y.1 := by
  by_contra! h
  apply apply_firstDiff_ne hne'
  rw [Nat.le_zero.1 h]
  apply apply_eq_of_dist_lt _ le_rfl
  rw [pow_zero]
  exact hxy

Result:
case inr
α : Type u_2
inst✝³ : MetricSpace α
inst✝² : CompleteSpace α
inst✝¹ : SecondCountableTopology α
inst✝ : Nonempty α
this : MetricSpace (ℕ → ℕ) := metricSpaceNatNat
I0 : 0 < 1 / 2
I1 : 1 / 2 < 1
u : ℕ → α
hu : DenseRange u
s : Set (ℕ → ℕ) := {x | (⋂ n, closedBall (u (x n)) ((1 / 2) ^ n)).Nonempty}
g : ↑s → α := fun x => Set.Nonempty.some ⋯
A : ∀ (x : ↑s) (n : ℕ), dist (g x) (u (↑x n)) ≤ (1 / 2) ^ n
y x : ↑s
hxy : dist x y < 1
hne : x ≠ y
hne' : ↑x ≠ ↑y
dist' : dist x y = dist ↑x ↑y
n : ℕ := firstDiff ↑x ↑y - 1
diff_pos : 0 < firstDiff ↑x ↑y
⊢ dist (g x) (g y) ≤ 4 * dist x y