awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
α : Type u_2
inst : MetricSpace α
inst_1 : CompleteSpace α
inst_2 : SecondCountableTopology α
inst_3 : Nonempty α
this_1 : MetricSpace (ℕ → ℕ) := metricSpaceNatNat
I0 : 0 < 1 / 2
I1 : 1 / 2 < 1
u : ℕ → α
hu : DenseRange u
s : Set (ℕ → ℕ) := {x : ℕ → ℕ | Set.Nonempty.{u_2} (α := α) (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))}
g : (↑s : Type) → α :=
  fun (x : (↑s : Type)) ↦ Set.Nonempty.some (s := ⋂ (n : ℕ), closedBall (u ((↑x : ℕ → ℕ) n)) ((1 / 2) ^ n)) ⋯
A : ∀ (x : (↑s : Type)) (n : ℕ), dist (g x) (u ((↑x : ℕ → ℕ) n)) ≤ (1 / 2) ^ n
g_cont : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
g_surj : Surjective g
x : ℕ → ℕ
hx : ClusterPt x (𝓟 s)
this : Tendsto (β := ℝ) (fun (n : ℕ) ↦ 2 * (1 / 2) ^ n) atTop (𝓝 0)
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ diam (closedBall (u (x n)) ((1 / 2) ^ n))) atTop (𝓝 0)

Tactic:
exact
        squeeze_zero (fun n => diam_nonneg) (fun n => diam_closedBall (pow_nonneg I0.le _)) this

Premises used: squeeze_zero, pow_nonneg, LT.lt.le, Metric.diam_nonneg, Metric.diam_closedBall
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
α : Type u_2
inst : MetricSpace α
inst_1 : CompleteSpace α
inst_2 : SecondCountableTopology α
inst_3 : Nonempty α
this : MetricSpace (ℕ → ℕ) := metricSpaceNatNat
I0 : 0 < 1 / 2
I1 : 1 / 2 < 1
u : ℕ → α
hu : DenseRange u
s : Set (ℕ → ℕ) := {x : ℕ → ℕ | Set.Nonempty.{u_2} (α := α) (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))}
g : (↑s : Type) → α :=
  fun (x : (↑s : Type)) ↦ Set.Nonempty.some (s := ⋂ (n : ℕ), closedBall (u ((↑x : ℕ → ℕ) n)) ((1 / 2) ^ n)) ⋯
A : ∀ (x : (↑s : Type)) (n : ℕ), dist (g x) (u ((↑x : ℕ → ℕ) n)) ≤ (1 / 2) ^ n
g_cont : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
g_surj : Surjective g
x : ℕ → ℕ
hx : ClusterPt x (𝓟 s)
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ diam (closedBall (u (x n)) ((1 / 2) ^ n))) atTop (𝓝 0)

Tactic:
have L : Tendsto (fun n : ℕ => diam (closedBall (u (x n)) ((1 / 2) ^ n))) atTop (𝓝 0) := by
      have : Tendsto (fun n : ℕ => (2 : ℝ) * (1 / 2) ^ n) atTop (𝓝 (2 * 0)) :=
        (tendsto_pow_atTop_nhds_zero_of_lt_one I0.le I1).const_mul _
      rw [mul_zero] at this
      exact
        squeeze_zero (fun n => diam_nonneg) (fun n => diam_closedBall (pow_nonneg I0.le _)) this
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
α : Type u_2
inst : MetricSpace α
inst_1 : CompleteSpace α
inst_2 : SecondCountableTopology α
inst_3 : Nonempty α
this : MetricSpace (ℕ → ℕ) := metricSpaceNatNat
I0 : 0 < 1 / 2
I1 : 1 / 2 < 1
u : ℕ → α
hu : DenseRange u
s : Set (ℕ → ℕ) := {x : ℕ → ℕ | Set.Nonempty.{u_2} (α := α) (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))}
g : (↑s : Type) → α :=
  fun (x : (↑s : Type)) ↦ Set.Nonempty.some (s := ⋂ (n : ℕ), closedBall (u ((↑x : ℕ → ℕ) n)) ((1 / 2) ^ n)) ⋯
A : ∀ (x : (↑s : Type)) (n : ℕ), dist (g x) (u ((↑x : ℕ → ℕ) n)) ≤ (1 / 2) ^ n
g_cont : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
g_surj : Surjective g
x : ℕ → ℕ
hx : ClusterPt x (𝓟 s)
L : Tendsto (β := ℝ) (fun (n : ℕ) ↦ diam (closedBall (u (x n)) ((1 / 2) ^ n))) atTop (𝓝 0)
⊢ x ∈ s

Tactic:
nonempty_iInter_of_nonempty_biInter (fun n => isClosed_closedBall)
      (fun n => isBounded_closedBall) (fun N ↦ ?_) L

Premises used: Metric.isBounded_closedBall, Set.Mem, Metric.isClosed_closedBall, setOf, Set.Nonempty, Metric.nonempty_iInter_of_nonempty_biInter
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
α : Type u_2
inst : MetricSpace α
inst_1 : CompleteSpace α
inst_2 : SecondCountableTopology α
inst_3 : Nonempty α
this : MetricSpace (ℕ → ℕ) := metricSpaceNatNat
I0 : 0 < 1 / 2
I1 : 1 / 2 < 1
u : ℕ → α
hu : DenseRange u
s : Set (ℕ → ℕ) := {x : ℕ → ℕ | Set.Nonempty.{u_2} (α := α) (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))}
g : (↑s : Type) → α :=
  fun (x : (↑s : Type)) ↦ Set.Nonempty.some (s := ⋂ (n : ℕ), closedBall (u ((↑x : ℕ → ℕ) n)) ((1 / 2) ^ n)) ⋯
A : ∀ (x : (↑s : Type)) (n : ℕ), dist (g x) (u ((↑x : ℕ → ℕ) n)) ≤ (1 / 2) ^ n
g_cont : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
g_surj : Surjective g
x : ℕ → ℕ
hx : ClusterPt x (𝓟 s)
L : Tendsto (β := ℝ) (fun (n : ℕ) ↦ diam (closedBall (u (x n)) ((1 / 2) ^ n))) atTop (𝓝 0)
refine : ∀ (N : ℕ), Set.Nonempty.{u_2} (α := α) (⋂ (n : ℕ), ⋂ (_ : n ≤ N), closedBall (u (x n)) ((1 / 2) ^ n))
⊢ x ∈ s

Tactic:
refine nonempty_iInter_of_nonempty_biInter (fun n => isClosed_closedBall)
      (fun n => isBounded_closedBall) (fun N ↦ ?_) L

Premises used: Metric.isBounded_closedBall, Metric.isClosed_closedBall, Metric.nonempty_iInter_of_nonempty_biInter
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
α : Type u_2
inst : MetricSpace α
inst_1 : CompleteSpace α
inst_2 : SecondCountableTopology α
inst_3 : Nonempty α
this : MetricSpace (ℕ → ℕ) := metricSpaceNatNat
I0 : 0 < 1 / 2
I1 : 1 / 2 < 1
u : ℕ → α
hu : DenseRange u
s : Set (ℕ → ℕ) := {x : ℕ → ℕ | Set.Nonempty.{u_2} (α := α) (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))}
g : (↑s : Type) → α :=
  fun (x : (↑s : Type)) ↦ Set.Nonempty.some (s := ⋂ (n : ℕ), closedBall (u ((↑x : ℕ → ℕ) n)) ((1 / 2) ^ n)) ⋯
A : ∀ (x : (↑s : Type)) (n : ℕ), dist (g x) (u ((↑x : ℕ → ℕ) n)) ≤ (1 / 2) ^ n
g_cont : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] 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 : ℕ → ℕ), y ∈ ball x ((1 / 2) ^ N) ∩ s

Tactic:
clusterPt_principal_iff.1 hx _ (ball_mem_nhds x (pow_pos I0 N))

Premises used: clusterPt_principal_iff, pow_pos, Metric.ball_mem_nhds, Set.Nonempty, Iff.mp
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
α : Type u_2
inst : MetricSpace α
inst_1 : CompleteSpace α
inst_2 : SecondCountableTopology α
inst_3 : Nonempty α
this : MetricSpace (ℕ → ℕ) := metricSpaceNatNat
I0 : 0 < 1 / 2
I1 : 1 / 2 < 1
u : ℕ → α
hu : DenseRange u
s : Set (ℕ → ℕ) := {x : ℕ → ℕ | Set.Nonempty.{u_2} (α := α) (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))}
g : (↑s : Type) → α :=
  fun (x : (↑s : Type)) ↦ Set.Nonempty.some (s := ⋂ (n : ℕ), closedBall (u ((↑x : ℕ → ℕ) n)) ((1 / 2) ^ n)) ⋯
A : ∀ (x : (↑s : Type)) (n : ℕ), dist (g x) (u ((↑x : ℕ → ℕ) n)) ≤ (1 / 2) ^ n
g_cont : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] 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 : ℕ
obtain :
  ∀ (y : ℕ → ℕ) (hxy : y ∈ ball x ((1 / 2) ^ N)) (ys : y ∈ s),
    Set.Nonempty.{u_2} (α := α) (⋂ (n : ℕ), ⋂ (_ : n ≤ N), closedBall (u (x n)) ((1 / 2) ^ n))
⊢ Set.Nonempty.{u_2} (α := α) (⋂ (n : ℕ), ⋂ (_ : n ≤ N), closedBall (u (x n)) ((1 / 2) ^ n))

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))

Premises used: clusterPt_principal_iff, pow_pos, HDiv.hDiv, Metric.ball, Metric.ball_mem_nhds, HPow.hPow, Iff.mp, OfNat.ofNat
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
α : Type u_2
inst : MetricSpace α
inst_1 : CompleteSpace α
inst_2 : SecondCountableTopology α
inst_3 : Nonempty α
this : MetricSpace (ℕ → ℕ) := metricSpaceNatNat
I0 : 0 < 1 / 2
I1 : 1 / 2 < 1
u : ℕ → α
hu : DenseRange u
s : Set (ℕ → ℕ) := {x : ℕ → ℕ | Set.Nonempty.{u_2} (α := α) (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))}
g : (↑s : Type) → α :=
  fun (x : (↑s : Type)) ↦ Set.Nonempty.some (s := ⋂ (n : ℕ), closedBall (u ((↑x : ℕ → ℕ) n)) ((1 / 2) ^ n)) ⋯
A : ∀ (x : (↑s : Type)) (n : ℕ), dist (g x) (u ((↑x : ℕ → ℕ) n)) ≤ (1 / 2) ^ n
g_cont : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] 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
⊢ Eq.{u_2 + 1} (α := Set α) (⋂ (n : ℕ), ⋂ (_ : n ≤ N), closedBall (u (x n)) ((1 / 2) ^ n))
    (⋂ (n : ℕ), ⋂ (_ : n ≤ N), closedBall (u (y n)) ((1 / 2) ^ n))

Tactic:
iInter_congr fun n ↦ iInter_congr fun hn ↦ ?_

Premises used: Set.iInter_congr
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
α : Type u_2
inst : MetricSpace α
inst_1 : CompleteSpace α
inst_2 : SecondCountableTopology α
inst_3 : Nonempty α
this : MetricSpace (ℕ → ℕ) := metricSpaceNatNat
I0 : 0 < 1 / 2
I1 : 1 / 2 < 1
u : ℕ → α
hu : DenseRange u
s : Set (ℕ → ℕ) := {x : ℕ → ℕ | Set.Nonempty.{u_2} (α := α) (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))}
g : (↑s : Type) → α :=
  fun (x : (↑s : Type)) ↦ Set.Nonempty.some (s := ⋂ (n : ℕ), closedBall (u ((↑x : ℕ → ℕ) n)) ((1 / 2) ^ n)) ⋯
A : ∀ (x : (↑s : Type)) (n : ℕ), dist (g x) (u ((↑x : ℕ → ℕ) n)) ≤ (1 / 2) ^ n
g_cont : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] 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
refine : ∀ (n : ℕ) (hn : n ≤ N), closedBall (u (x n)) ((1 / 2) ^ n) = closedBall (u (y n)) ((1 / 2) ^ n)
⊢ Eq.{u_2 + 1} (α := Set α) (⋂ (n : ℕ), ⋂ (_ : n ≤ N), closedBall (u (x n)) ((1 / 2) ^ n))
    (⋂ (n : ℕ), ⋂ (_ : n ≤ N), closedBall (u (y n)) ((1 / 2) ^ n))

Tactic:
refine iInter_congr fun n ↦ iInter_congr fun hn ↦ ?_

Premises used: Set.iInter_congr
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
α : Type u_2
inst : MetricSpace α
inst_1 : CompleteSpace α
inst_2 : SecondCountableTopology α
inst_3 : Nonempty α
this : MetricSpace (ℕ → ℕ) := metricSpaceNatNat
I0 : 0 < 1 / 2
I1 : 1 / 2 < 1
u : ℕ → α
hu : DenseRange u
s : Set (ℕ → ℕ) := {x : ℕ → ℕ | Set.Nonempty.{u_2} (α := α) (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))}
g : (↑s : Type) → α :=
  fun (x : (↑s : Type)) ↦ Set.Nonempty.some (s := ⋂ (n : ℕ), closedBall (u ((↑x : ℕ → ℕ) n)) ((1 / 2) ^ n)) ⋯
A : ∀ (x : (↑s : Type)) (n : ℕ), dist (g x) (u ((↑x : ℕ → ℕ) n)) ≤ (1 / 2) ^ n
g_cont : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] 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 : ℕ
hn : n ≤ N
⊢ x n = y n

Tactic:
have : x n = y n := apply_eq_of_dist_lt (mem_ball'.1 hxy) hn
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
α : Type u_2
inst : MetricSpace α
inst_1 : CompleteSpace α
inst_2 : SecondCountableTopology α
inst_3 : Nonempty α
this_1 : MetricSpace (ℕ → ℕ) := metricSpaceNatNat
I0 : 0 < 1 / 2
I1 : 1 / 2 < 1
u : ℕ → α
hu : DenseRange u
s : Set (ℕ → ℕ) := {x : ℕ → ℕ | Set.Nonempty.{u_2} (α := α) (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))}
g : (↑s : Type) → α :=
  fun (x : (↑s : Type)) ↦ Set.Nonempty.some (s := ⋂ (n : ℕ), closedBall (u ((↑x : ℕ → ℕ) n)) ((1 / 2) ^ n)) ⋯
A : ∀ (x : (↑s : Type)) (n : ℕ), dist (g x) (u ((↑x : ℕ → ℕ) n)) ≤ (1 / 2) ^ n
g_cont : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] 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 : ℕ
hn : n ≤ N
this : x n = y n
rw rw₁ : closedBall (u (y n)) ((1 / 2) ^ n) = closedBall (u (y n)) ((1 / 2) ^ n)
⊢ closedBall (u (x n)) ((1 / 2) ^ n) = closedBall (u (y n)) ((1 / 2) ^ n)

Tactic:
rw [this]
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
α : Type u_2
inst : MetricSpace α
inst_1 : CompleteSpace α
inst_2 : SecondCountableTopology α
inst_3 : Nonempty α
this : MetricSpace (ℕ → ℕ) := metricSpaceNatNat
I0 : 0 < 1 / 2
I1 : 1 / 2 < 1
u : ℕ → α
hu : DenseRange u
s : Set (ℕ → ℕ) := {x : ℕ → ℕ | Set.Nonempty.{u_2} (α := α) (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))}
g : (↑s : Type) → α :=
  fun (x : (↑s : Type)) ↦ Set.Nonempty.some (s := ⋂ (n : ℕ), closedBall (u ((↑x : ℕ → ℕ) n)) ((1 / 2) ^ n)) ⋯
A : ∀ (x : (↑s : Type)) (n : ℕ), dist (g x) (u ((↑x : ℕ → ℕ) n)) ≤ (1 / 2) ^ n
g_cont : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] 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
⊢ Eq.{u_2 + 1} (α := Set α) (⋂ (n : ℕ), ⋂ (_ : n ≤ N), closedBall (u (x n)) ((1 / 2) ^ n))
    (⋂ (n : ℕ), ⋂ (_ : n ≤ N), closedBall (u (y n)) ((1 / 2) ^ n))

Tactic:
have E :
      ⋂ (n : ℕ) (H : n ≤ N), closedBall (u (x n)) ((1 / 2) ^ n) =
        ⋂ (n : ℕ) (H : n ≤ N), closedBall (u (y n)) ((1 / 2) ^ n) := by
      refine iInter_congr fun n ↦ iInter_congr fun hn ↦ ?_
      have : x n = y n := apply_eq_of_dist_lt (mem_ball'.1 hxy) hn
      rw [this]
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
α : Type u_2
inst : MetricSpace α
inst_1 : CompleteSpace α
inst_2 : SecondCountableTopology α
inst_3 : Nonempty α
this : MetricSpace (ℕ → ℕ) := metricSpaceNatNat
I0 : 0 < 1 / 2
I1 : 1 / 2 < 1
u : ℕ → α
hu : DenseRange u
s : Set (ℕ → ℕ) := {x : ℕ → ℕ | Set.Nonempty.{u_2} (α := α) (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))}
g : (↑s : Type) → α :=
  fun (x : (↑s : Type)) ↦ Set.Nonempty.some (s := ⋂ (n : ℕ), closedBall (u ((↑x : ℕ → ℕ) n)) ((1 / 2) ^ n)) ⋯
A : ∀ (x : (↑s : Type)) (n : ℕ), dist (g x) (u ((↑x : ℕ → ℕ) n)) ≤ (1 / 2) ^ n
g_cont : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] 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
E :
  Eq.{u_2 + 1} (α := Set α) (⋂ (n : ℕ), ⋂ (_ : n ≤ N), closedBall (u (x n)) ((1 / 2) ^ n))
    (⋂ (n : ℕ), ⋂ (_ : n ≤ N), closedBall (u (y n)) ((1 / 2) ^ n))
rw : Set.Nonempty.{u_2} (α := α) (⋂ (n : ℕ), ⋂ (_ : n ≤ N), closedBall (u (y n)) ((1 / 2) ^ n))
⊢ Set.Nonempty.{u_2} (α := α) (⋂ (n : ℕ), ⋂ (_ : n ≤ N), closedBall (u (x n)) ((1 / 2) ^ n))

Tactic:
rw [E]
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
α : Type u_2
inst : MetricSpace α
inst_1 : CompleteSpace α
inst_2 : SecondCountableTopology α
inst_3 : Nonempty α
this : MetricSpace (ℕ → ℕ) := metricSpaceNatNat
I0 : 0 < 1 / 2
I1 : 1 / 2 < 1
u : ℕ → α
hu : DenseRange u
s : Set (ℕ → ℕ) := {x : ℕ → ℕ | Set.Nonempty.{u_2} (α := α) (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))}
g : (↑s : Type) → α :=
  fun (x : (↑s : Type)) ↦ Set.Nonempty.some (s := ⋂ (n : ℕ), closedBall (u ((↑x : ℕ → ℕ) n)) ((1 / 2) ^ n)) ⋯
A : ∀ (x : (↑s : Type)) (n : ℕ), dist (g x) (u ((↑x : ℕ → ℕ) n)) ≤ (1 / 2) ^ n
g_cont : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] 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
E :
  Eq.{u_2 + 1} (α := Set α) (⋂ (n : ℕ), ⋂ (_ : n ≤ N), closedBall (u (x n)) ((1 / 2) ^ n))
    (⋂ (n : ℕ), ⋂ (_ : n ≤ N), closedBall (u (y n)) ((1 / 2) ^ n))
apply :
  Subset.{u_2} (α := Set α) (⋂ (n : ℕ), closedBall (u (y n)) ((1 / 2) ^ n))
    (⋂ (n : ℕ), ⋂ (_ : n ≤ N), closedBall (u (y n)) ((1 / 2) ^ n))
⊢ Set.Nonempty.{u_2} (α := α) (⋂ (n : ℕ), ⋂ (_ : n ≤ N), closedBall (u (y n)) ((1 / 2) ^ n))

Tactic:
apply Nonempty.mono _ ys

Premises used: Set.Nonempty.mono
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
α : Type u_2
inst : MetricSpace α
inst_1 : CompleteSpace α
inst_2 : SecondCountableTopology α
inst_3 : Nonempty α
this : MetricSpace (ℕ → ℕ) := metricSpaceNatNat
I0 : 0 < 1 / 2
I1 : 1 / 2 < 1
u : ℕ → α
hu : DenseRange u
s : Set (ℕ → ℕ) := {x : ℕ → ℕ | Set.Nonempty.{u_2} (α := α) (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))}
g : (↑s : Type) → α :=
  fun (x : (↑s : Type)) ↦ Set.Nonempty.some (s := ⋂ (n : ℕ), closedBall (u ((↑x : ℕ → ℕ) n)) ((1 / 2) ^ n)) ⋯
A : ∀ (x : (↑s : Type)) (n : ℕ), dist (g x) (u ((↑x : ℕ → ℕ) n)) ≤ (1 / 2) ^ n
g_cont : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] 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
E :
  Eq.{u_2 + 1} (α := Set α) (⋂ (n : ℕ), ⋂ (_ : n ≤ N), closedBall (u (x n)) ((1 / 2) ^ n))
    (⋂ (n : ℕ), ⋂ (_ : n ≤ N), closedBall (u (y n)) ((1 / 2) ^ n))
⊢ Subset.{u_2} (α := Set α) (⋂ (n : ℕ), closedBall (u (y n)) ((1 / 2) ^ n))
    (⋂ (n : ℕ), ⋂ (_ : n ≤ N), closedBall (u (y n)) ((1 / 2) ^ n))

Tactic:
apply iInter_subset_iInter₂

Premises used: Set.iInter_subset_iInter₂
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
α : Type u_2
inst : MetricSpace α
inst_1 : CompleteSpace α
inst_2 : SecondCountableTopology α
inst_3 : Nonempty α
this : MetricSpace (ℕ → ℕ) := metricSpaceNatNat
I0 : 0 < 1 / 2
I1 : 1 / 2 < 1
u : ℕ → α
hu : DenseRange u
s : Set (ℕ → ℕ) := {x : ℕ → ℕ | Set.Nonempty.{u_2} (α := α) (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))}
g : (↑s : Type) → α :=
  fun (x : (↑s : Type)) ↦ Set.Nonempty.some (s := ⋂ (n : ℕ), closedBall (u ((↑x : ℕ → ℕ) n)) ((1 / 2) ^ n)) ⋯
A : ∀ (x : (↑s : Type)) (n : ℕ), dist (g x) (u ((↑x : ℕ → ℕ) n)) ≤ (1 / 2) ^ n
g_cont : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
g_surj : Surjective g
⊢ IsClosed s

Tactic:
have s_closed : IsClosed s := by
    refine isClosed_iff_clusterPt.mpr fun x hx ↦ ?_
    have L : Tendsto (fun n : ℕ => diam (closedBall (u (x n)) ((1 / 2) ^ n))) atTop (𝓝 0) := by
      have : Tendsto (fun n : ℕ => (2 : ℝ) * (1 / 2) ^ n) atTop (𝓝 (2 * 0)) :=
        (tendsto_pow_atTop_nhds_zero_of_lt_one I0.le I1).const_mul _
      rw [mul_zero] at this
      exact
        squeeze_zero (fun n => diam_nonneg) (fun n => diam_closedBall (pow_nonneg I0.le _)) this
    refine nonempty_iInter_of_nonempty_biInter (fun n => isClosed_closedBall)
      (fun n => isBounded_closedBall) (fun N ↦ ?_) L
    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))
    have E :
      ⋂ (n : ℕ) (H : n ≤ N), closedBall (u (x n)) ((1 / 2) ^ n) =
        ⋂ (n : ℕ) (H : n ≤ N), closedBall (u (y n)) ((1 / 2) ^ n) := by
      refine iInter_congr fun n ↦ iInter_congr fun hn ↦ ?_
      have : x n = y n := apply_eq_of_dist_lt (mem_ball'.1 hxy) hn
      rw [this]
    rw [E]
    apply Nonempty.mono _ ys
    apply iInter_subset_iInter₂
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
α : Type u_2
inst : MetricSpace α
inst_1 : CompleteSpace α
inst_2 : SecondCountableTopology α
inst_3 : Nonempty α
this : MetricSpace (ℕ → ℕ) := metricSpaceNatNat
I0 : 0 < 1 / 2
I1 : 1 / 2 < 1
u : ℕ → α
hu : DenseRange u
s : Set (ℕ → ℕ) := {x : ℕ → ℕ | Set.Nonempty.{u_2} (α := α) (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))}
g : (↑s : Type) → α :=
  fun (x : (↑s : Type)) ↦ Set.Nonempty.some (s := ⋂ (n : ℕ), closedBall (u ((↑x : ℕ → ℕ) n)) ((1 / 2) ^ n)) ⋯
A : ∀ (x : (↑s : Type)) (n : ℕ), dist (g x) (u ((↑x : ℕ → ℕ) n)) ≤ (1 / 2) ^ n
g_cont : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
g_surj : Surjective g
s_closed : IsClosed s
apply : s.Nonempty
⊢ ∃ (f : (ℕ → ℕ) → (↑s : Type)), (∀ (x : (↑s : Type)), f (↑x : ℕ → ℕ) = x) ∧ Surjective f ∧ Continuous f

Tactic:
apply exists_retraction_subtype_of_isClosed s_closed

Premises used: PiNat.exists_retraction_subtype_of_isClosed
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
α : Type u_2
inst : MetricSpace α
inst_1 : CompleteSpace α
inst_2 : SecondCountableTopology α
inst_3 : Nonempty α
this : MetricSpace (ℕ → ℕ) := metricSpaceNatNat
I0 : 0 < 1 / 2
I1 : 1 / 2 < 1
u : ℕ → α
hu : DenseRange u
s : Set (ℕ → ℕ) := {x : ℕ → ℕ | Set.Nonempty.{u_2} (α := α) (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))}
g : (↑s : Type) → α :=
  fun (x : (↑s : Type)) ↦ Set.Nonempty.some (s := ⋂ (n : ℕ), closedBall (u ((↑x : ℕ → ℕ) n)) ((1 / 2) ^ n)) ⋯
A : ∀ (x : (↑s : Type)) (n : ℕ), dist (g x) (u ((↑x : ℕ → ℕ) n)) ≤ (1 / 2) ^ n
g_cont : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
g_surj : Surjective g
s_closed : IsClosed s
⊢ s.Nonempty

Tactic:
simpa only [nonempty_coe_sort] using g_surj.nonempty

Premises used: Set.nonempty_coe_sort, Function.Surjective.nonempty
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
α : Type u_2
inst : MetricSpace α
inst_1 : CompleteSpace α
inst_2 : SecondCountableTopology α
inst_3 : Nonempty α
this : MetricSpace (ℕ → ℕ) := metricSpaceNatNat
I0 : 0 < 1 / 2
I1 : 1 / 2 < 1
u : ℕ → α
hu : DenseRange u
s : Set (ℕ → ℕ) := {x : ℕ → ℕ | Set.Nonempty.{u_2} (α := α) (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))}
g : (↑s : Type) → α :=
  fun (x : (↑s : Type)) ↦ Set.Nonempty.some (s := ⋂ (n : ℕ), closedBall (u ((↑x : ℕ → ℕ) n)) ((1 / 2) ^ n)) ⋯
A : ∀ (x : (↑s : Type)) (n : ℕ), dist (g x) (u ((↑x : ℕ → ℕ) n)) ≤ (1 / 2) ^ n
g_cont : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
g_surj : Surjective g
s_closed : IsClosed s
obtain :
  ∀ (f : (ℕ → ℕ) → (↑s : Type)) (f_surj : Surjective f) (f_cont : Continuous f),
    ∃ (f : (ℕ → ℕ) → α), Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f ∧ Surjective f
⊢ ∃ (f : (ℕ → ℕ) → α), Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f ∧ Surjective f

Tactic:
obtain ⟨f, -, f_surj, f_cont⟩ :
    ∃ f : (ℕ → ℕ) → s, (∀ x : s, f x = x) ∧ Surjective f ∧ Continuous f := by
    apply exists_retraction_subtype_of_isClosed s_closed
    simpa only [nonempty_coe_sort] using g_surj.nonempty
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
α : Type u_2
inst : MetricSpace α
inst_1 : CompleteSpace α
inst_2 : SecondCountableTopology α
inst_3 : Nonempty α
this : MetricSpace (ℕ → ℕ) := metricSpaceNatNat
I0 : 0 < 1 / 2
I1 : 1 / 2 < 1
u : ℕ → α
hu : DenseRange u
s : Set (ℕ → ℕ) := {x : ℕ → ℕ | Set.Nonempty.{u_2} (α := α) (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))}
g : (↑s : Type) → α :=
  fun (x : (↑s : Type)) ↦ Set.Nonempty.some (s := ⋂ (n : ℕ), closedBall (u ((↑x : ℕ → ℕ) n)) ((1 / 2) ^ n)) ⋯
A : ∀ (x : (↑s : Type)) (n : ℕ), dist (g x) (u ((↑x : ℕ → ℕ) n)) ≤ (1 / 2) ^ n
g_cont : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
g_surj : Surjective g
s_closed : IsClosed s
f : (ℕ → ℕ) → (↑s : Type)
f_surj : Surjective f
f_cont : Continuous f
⊢ ∃ (f : (ℕ → ℕ) → α), Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f ∧ Surjective f

Tactic:
⟨g ∘ f, g_cont.comp f_cont, g_surj.comp f_surj⟩

Premises used: Continuous.comp, Function.comp, And.intro, Exists.intro, Function.Surjective.comp
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
α : Type u_2
inst : MetricSpace α
inst_1 : CompleteSpace α
inst_2 : SecondCountableTopology α
inst_3 : Nonempty α
this : MetricSpace (ℕ → ℕ) := metricSpaceNatNat
I0 : 0 < 1 / 2
I1 : 1 / 2 < 1
u : ℕ → α
hu : DenseRange u
s : Set (ℕ → ℕ) := {x : ℕ → ℕ | Set.Nonempty.{u_2} (α := α) (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))}
g : (↑s : Type) → α :=
  fun (x : (↑s : Type)) ↦ Set.Nonempty.some (s := ⋂ (n : ℕ), closedBall (u ((↑x : ℕ → ℕ) n)) ((1 / 2) ^ n)) ⋯
A : ∀ (x : (↑s : Type)) (n : ℕ), dist (g x) (u ((↑x : ℕ → ℕ) n)) ≤ (1 / 2) ^ n
g_cont : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
g_surj : Surjective g
s_closed : IsClosed s
f : (ℕ → ℕ) → (↑s : Type)
f_surj : Surjective f
f_cont : Continuous f
⊢ ∃ (f : (ℕ → ℕ) → α), Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f ∧ Surjective f

Tactic:
exact ⟨g ∘ f, g_cont.comp f_cont, g_surj.comp f_surj⟩
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
ι : Type u_2
inst : Encodable ι
F : ι → Type u_3
inst_1 : (i : ι) → EDist (F i)
x y : (i : ι) → F i
⊢ edist x y = ∑' (i : ι), min (HPow.hPow (α := ℝ≥0∞) 2⁻¹ (encode i)) (edist (x i) (y i))

Tactic:
rfl

Premises used: setOf, rfl
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
ι : Type u_2
inst : Encodable ι
F : ι → Type u_3
inst_1 : (i : ι) → EDist (F i)
x y : (i : ι) → F i
i : ι
⊢ min (HPow.hPow (α := ℝ≥0∞) 2⁻¹ (encode i)) (edist (x i) (y i)) ≤ edist x y

Tactic:
ENNReal.le_tsum _

Premises used: setOf, ENNReal.le_tsum
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
ι : Type u_2
inst : Encodable ι
F : ι → Type u_3
inst_1 : (i : ι) → EDist (F i)
x y : (i : ι) → F i
h : ∀ (i : ι), min (HPow.hPow (α := ℝ≥0∞) 2⁻¹ (encode i)) (edist (x i) (y i)) ≤ HPow.hPow (α := ℝ≥0∞) 2⁻¹ (encode i)
⊢ LE.le (α := ℝ≥0∞) (∑' (i : ι), min (HPow.hPow (α := ℝ≥0∞) 2⁻¹ (encode i)) (edist (x i) (y i)))
    (∑' (i : ι), HPow.hPow (α := ℝ≥0∞) 2⁻¹ (encode i))

Tactic:
gcongr