E : ℕ → Type ?u.233694
α : Type u_1
inst✝³ : MetricSpace α
inst✝² : CompleteSpace α
inst✝¹ : SecondCountableTopology α
inst✝ : Nonempty α
this : MetricSpace (ℕ → ℕ) := metricSpaceNatNat
⊢ ∃ f, Continuous f ∧ Surjective f
E : ℕ → Type ?u.233694
α : Type u_1
inst✝³ : MetricSpace α
inst✝² : CompleteSpace α
inst✝¹ : SecondCountableTopology α
inst✝ : Nonempty α
⊢ ∃ f, Continuous f ∧ Surjective f
letI : MetricSpace (ℕ → ℕ) := PiNat.metricSpaceNatNat
E : ℕ → Type ?u.233694
α : Type u_1
inst✝³ : MetricSpace α
inst✝² : CompleteSpace α
inst✝¹ : SecondCountableTopology α
inst✝ : Nonempty α
this : MetricSpace (ℕ → ℕ) := metricSpaceNatNat
I0 : 0 < 1 / 2
⊢ ∃ f, Continuous f ∧ Surjective f
E : ℕ → Type ?u.233694
α : Type u_1
inst✝³ : MetricSpace α
inst✝² : CompleteSpace α
inst✝¹ : SecondCountableTopology α
inst✝ : Nonempty α
this : MetricSpace (ℕ → ℕ) := metricSpaceNatNat
⊢ ∃ f, Continuous f ∧ Surjective f
have I0 : (0 : ℝ) < 1 / 2 := by norm_num
E : ℕ → Type ?u.233694
α : Type u_1
inst✝³ : MetricSpace α
inst✝² : CompleteSpace α
inst✝¹ : SecondCountableTopology α
inst✝ : Nonempty α
this : MetricSpace (ℕ → ℕ) := metricSpaceNatNat
I0 : 0 < 1 / 2
I1 : 1 / 2 < 1
⊢ ∃ f, Continuous f ∧ Surjective f
E : ℕ → Type ?u.233694
α : Type u_1
inst✝³ : MetricSpace α
inst✝² : CompleteSpace α
inst✝¹ : SecondCountableTopology α
inst✝ : Nonempty α
this : MetricSpace (ℕ → ℕ) := metricSpaceNatNat
I0 : 0 < 1 / 2
⊢ ∃ f, Continuous f ∧ Surjective f
have I1 : (1 / 2 : ℝ) < 1 := by norm_num
case intro
E : ℕ → Type ?u.233694
α : Type u_1
inst✝³ : MetricSpace α
inst✝² : CompleteSpace α
inst✝¹ : SecondCountableTopology α
inst✝ : Nonempty α
this : MetricSpace (ℕ → ℕ) := metricSpaceNatNat
I0 : 0 < 1 / 2
I1 : 1 / 2 < 1
u : ℕ → α
hu : DenseRange u
⊢ ∃ f, Continuous f ∧ Surjective f
E : ℕ → Type ?u.233694
α : Type u_1
inst✝³ : MetricSpace α
inst✝² : CompleteSpace α
inst✝¹ : SecondCountableTopology α
inst✝ : Nonempty α
this : MetricSpace (ℕ → ℕ) := metricSpaceNatNat
I0 : 0 < 1 / 2
I1 : 1 / 2 < 1
⊢ ∃ f, Continuous f ∧ Surjective f
rcases exists_dense_seq α with ⟨u, hu⟩
case intro
E : ℕ → Type ?u.233694
α : Type u_1
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 | Set.Nonempty (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))}
⊢ ∃ f, Continuous f ∧ Surjective f
case intro
E : ℕ → Type ?u.233694
α : Type u_1
inst✝³ : MetricSpace α
inst✝² : CompleteSpace α
inst✝¹ : SecondCountableTopology α
inst✝ : Nonempty α
this : MetricSpace (ℕ → ℕ) := metricSpaceNatNat
I0 : 0 < 1 / 2
I1 : 1 / 2 < 1
u : ℕ → α
hu : DenseRange u
⊢ ∃ f, Continuous f ∧ Surjective f
let s : Set (ℕ → ℕ) := { x | (⋂ n : ℕ, closedBall (u (x n)) ((1 / 2) ^ n)).Nonempty }
case intro
E : ℕ → Type ?u.233694
α : Type u_1
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 | Set.Nonempty (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))}
g : ↑s → α := fun x => Set.Nonempty.some (_ : ↑x ∈ s)
⊢ ∃ f, Continuous f ∧ Surjective f
case intro
E : ℕ → Type ?u.233694
α : Type u_1
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 | Set.Nonempty (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))}
⊢ ∃ f, Continuous f ∧ Surjective f
let g : s → α := fun x => x.2.some
case intro
E : ℕ → Type ?u.233694
α : Type u_1
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 | Set.Nonempty (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))}
g : ↑s → α := fun x => Set.Nonempty.some (_ : ↑x ∈ s)
A : ∀ (x : ↑s) (n : ℕ), dist (g x) (u (↑x n)) ≤ (1 / 2) ^ n
⊢ ∃ f, Continuous f ∧ Surjective f
case intro
E : ℕ → Type ?u.233694
α : Type u_1
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 | Set.Nonempty (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))}
g : ↑s → α := fun x => Set.Nonempty.some (_ : ↑x ∈ s)
⊢ ∃ f, Continuous f ∧ Surjective f
have A : ∀ (x : s) (n : ℕ), dist (g x) (u ((x : ℕ → ℕ) n)) ≤ (1 / 2) ^ n := fun x n =>
  (mem_iInter.1 x.2.some_mem n : _)
case intro
E : ℕ → Type ?u.233694
α : Type u_1
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 | Set.Nonempty (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))}
g : ↑s → α := fun x => Set.Nonempty.some (_ : ↑x ∈ s)
A : ∀ (x : ↑s) (n : ℕ), dist (g x) (u (↑x n)) ≤ (1 / 2) ^ n
g_cont : Continuous g
g_surj : Surjective g
⊢ ∃ f, Continuous f ∧ Surjective f
case intro
E : ℕ → Type ?u.233694
α : Type u_1
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 | Set.Nonempty (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))}
g : ↑s → α := fun x => Set.Nonempty.some (_ : ↑x ∈ s)
A : ∀ (x : ↑s) (n : ℕ), dist (g x) (u (↑x n)) ≤ (1 / 2) ^ n
g_cont : Continuous g
⊢ ∃ f, Continuous f ∧ Surjective f
have g_surj : Surjective g := fun y ↦ by
  have : ∀ n : ℕ, ∃ j, y ∈ closedBall (u j) ((1 / 2) ^ n) := fun n ↦ by
    rcases hu.exists_dist_lt y (by simp : (0 : ℝ) < (1 / 2) ^ n) with ⟨j, hj⟩
    exact ⟨j, hj.le⟩
  choose x hx using this
  have I : (⋂ n : ℕ, closedBall (u (x n)) ((1 / 2) ^ n)).Nonempty := ⟨y, mem_iInter.2 hx⟩
  refine' ⟨⟨x, I⟩, _⟩
  refine' dist_le_zero.1 _
  have J : ∀ n : ℕ, dist (g ⟨x, I⟩) y ≤ (1 / 2) ^ n + (1 / 2) ^ n := fun n =>
    calc
      dist (g ⟨x, I⟩) y ≤ dist (g ⟨x, I⟩) (u (x n)) + dist y (u (x n)) :=
        dist_triangle_right _ _ _
      _ ≤ (1 / 2) ^ n + (1 / 2) ^ n := add_le_add (A ⟨x, I⟩ n) (hx n)
  have L : Tendsto (fun n : ℕ => (1 / 2 : ℝ) ^ n + (1 / 2) ^ n) atTop (𝓝 (0 + 0)) :=
    (tendsto_pow_atTop_nhds_0_of_lt_1 I0.le I1).add (tendsto_pow_atTop_nhds_0_of_lt_1 I0.le I1)
  rw [add_zero] at L
  exact ge_of_tendsto' L J
case intro
E : ℕ → Type ?u.233694
α : Type u_1
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 | Set.Nonempty (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))}
g : ↑s → α := fun x => Set.Nonempty.some (_ : ↑x ∈ s)
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
⊢ ∃ f, Continuous f ∧ Surjective f
case intro
E : ℕ → Type ?u.233694
α : Type u_1
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 | Set.Nonempty (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))}
g : ↑s → α := fun x => Set.Nonempty.some (_ : ↑x ∈ s)
A : ∀ (x : ↑s) (n : ℕ), dist (g x) (u (↑x n)) ≤ (1 / 2) ^ n
g_cont : Continuous g
g_surj : Surjective g
⊢ ∃ f, Continuous f ∧ Surjective f
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_0_of_lt_1 I0.le I1).const_mul _
    rw [MulZeroClass.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_ball)
    (fun n => bounded_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₂
case intro.intro.intro.intro
E : ℕ → Type ?u.233694
α : Type u_1
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 | Set.Nonempty (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))}
g : ↑s → α := fun x => Set.Nonempty.some (_ : ↑x ∈ s)
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
f : (ℕ → ℕ) → ↑s
f_surj : Surjective f
f_cont : Continuous f
⊢ ∃ f, Continuous f ∧ Surjective f
case intro
E : ℕ → Type ?u.233694
α : Type u_1
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 | Set.Nonempty (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))}
g : ↑s → α := fun x => Set.Nonempty.some (_ : ↑x ∈ s)
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
⊢ ∃ f, Continuous f ∧ Surjective f
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
no goals
case intro.intro.intro.intro
E : ℕ → Type ?u.233694
α : Type u_1
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 | Set.Nonempty (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))}
g : ↑s → α := fun x => Set.Nonempty.some (_ : ↑x ∈ s)
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
f : (ℕ → ℕ) → ↑s
f_surj : Surjective f
f_cont : Continuous f
⊢ ∃ f, Continuous f ∧ Surjective f
exact ⟨g ∘ f, g_cont.comp f_cont, g_surj.comp f_surj⟩
no goals
E : ℕ → Type ?u.233694
α : Type u_1
inst✝³ : MetricSpace α
inst✝² : CompleteSpace α
inst✝¹ : SecondCountableTopology α
inst✝ : Nonempty α
this : MetricSpace (ℕ → ℕ) := metricSpaceNatNat
⊢ 0 < 1 / 2
norm_num
no goals
E : ℕ → Type ?u.233694
α : Type u_1
inst✝³ : MetricSpace α
inst✝² : CompleteSpace α
inst✝¹ : SecondCountableTopology α
inst✝ : Nonempty α
this : MetricSpace (ℕ → ℕ) := metricSpaceNatNat
I0 : 0 < 1 / 2
⊢ 1 / 2 < 1
norm_num
E : ℕ → Type ?u.233694
α : Type u_1
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 | Set.Nonempty (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))}
g : ↑s → α := fun x => Set.Nonempty.some (_ : ↑x ∈ s)
A : ∀ (x : ↑s) (n : ℕ), dist (g x) (u (↑x n)) ≤ (1 / 2) ^ n
y : ↑s
⊢ ContinuousAt g y
E : ℕ → Type ?u.233694
α : Type u_1
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 | Set.Nonempty (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))}
g : ↑s → α := fun x => Set.Nonempty.some (_ : ↑x ∈ s)
A : ∀ (x : ↑s) (n : ℕ), dist (g x) (u (↑x n)) ≤ (1 / 2) ^ n
⊢ Continuous g
refine continuous_iff_continuousAt.2 fun y => ?_
E : ℕ → Type ?u.233694
α : Type u_1
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 | Set.Nonempty (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))}
g : ↑s → α := fun x => Set.Nonempty.some (_ : ↑x ∈ s)
A : ∀ (x : ↑s) (n : ℕ), dist (g x) (u (↑x n)) ≤ (1 / 2) ^ n
y x : ↑s
hxy : dist x y < 1
⊢ dist (g x) (g y) ≤ 4 * dist x y
E : ℕ → Type ?u.233694
α : Type u_1
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 | Set.Nonempty (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))}
g : ↑s → α := fun x => Set.Nonempty.some (_ : ↑x ∈ s)
A : ∀ (x : ↑s) (n : ℕ), dist (g x) (u (↑x n)) ≤ (1 / 2) ^ n
y : ↑s
⊢ ContinuousAt g y
refine continuousAt_of_locally_lipschitz zero_lt_one 4 fun x hxy => ?_
case inl
E : ℕ → Type ?u.233694
α : Type u_1
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 | Set.Nonempty (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))}
g : ↑s → α := fun x => Set.Nonempty.some (_ : ↑x ∈ s)
A : ∀ (x : ↑s) (n : ℕ), dist (g x) (u (↑x n)) ≤ (1 / 2) ^ n
x : ↑s
hxy : dist x x < 1
⊢ dist (g x) (g x) ≤ 4 * dist x x

case inr
E : ℕ → Type ?u.233694
α : Type u_1
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 | Set.Nonempty (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))}
g : ↑s → α := fun x => Set.Nonempty.some (_ : ↑x ∈ s)
A : ∀ (x : ↑s) (n : ℕ), dist (g x) (u (↑x n)) ≤ (1 / 2) ^ n
y x : ↑s
hxy : dist x y < 1
hne : x ≠ y
⊢ dist (g x) (g y) ≤ 4 * dist x y
E : ℕ → Type ?u.233694
α : Type u_1
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 | Set.Nonempty (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))}
g : ↑s → α := fun x => Set.Nonempty.some (_ : ↑x ∈ s)
A : ∀ (x : ↑s) (n : ℕ), dist (g x) (u (↑x n)) ≤ (1 / 2) ^ n
y x : ↑s
hxy : dist x y < 1
⊢ dist (g x) (g y) ≤ 4 * dist x y
rcases eq_or_ne x y with (rfl | hne)
case inr
E : ℕ → Type ?u.233694
α : Type u_1
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 | Set.Nonempty (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))}
g : ↑s → α := fun x => Set.Nonempty.some (_ : ↑x ∈ s)
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 (g x) (g y) ≤ 4 * dist x y
case inr
E : ℕ → Type ?u.233694
α : Type u_1
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 | Set.Nonempty (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))}
g : ↑s → α := fun x => Set.Nonempty.some (_ : ↑x ∈ s)
A : ∀ (x : ↑s) (n : ℕ), dist (g x) (u (↑x n)) ≤ (1 / 2) ^ n
y x : ↑s
hxy : dist x y < 1
hne : x ≠ y
⊢ dist (g x) (g y) ≤ 4 * dist x y
have hne' : x.1 ≠ y.1 := Subtype.coe_injective.ne hne
case inr
E : ℕ → Type ?u.233694
α : Type u_1
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 | Set.Nonempty (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))}
g : ↑s → α := fun x => Set.Nonempty.some (_ : ↑x ∈ s)
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
⊢ dist (g x) (g y) ≤ 4 * dist x y
case inr
E : ℕ → Type ?u.233694
α : Type u_1
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 | Set.Nonempty (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))}
g : ↑s → α := fun x => Set.Nonempty.some (_ : ↑x ∈ s)
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 (g x) (g y) ≤ 4 * dist x y
have dist' : dist x y = dist x.1 y.1 := rfl
case inr
E : ℕ → Type ?u.233694
α : Type u_1
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 | Set.Nonempty (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))}
g : ↑s → α := fun x => Set.Nonempty.some (_ : ↑x ∈ s)
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
case inr
E : ℕ → Type ?u.233694
α : Type u_1
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 | Set.Nonempty (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))}
g : ↑s → α := fun x => Set.Nonempty.some (_ : ↑x ∈ s)
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
⊢ dist (g x) (g y) ≤ 4 * dist x y
let n := firstDiff x.1 y.1 - 1
case inr
E : ℕ → Type ?u.233694
α : Type u_1
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 | Set.Nonempty (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))}
g : ↑s → α := fun x => Set.Nonempty.some (_ : ↑x ∈ s)
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
case inr
E : ℕ → Type ?u.233694
α : Type u_1
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 | Set.Nonempty (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))}
g : ↑s → α := fun x => Set.Nonempty.some (_ : ↑x ∈ s)
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
have diff_pos : 0 < firstDiff x.1 y.1 := by
  by_contra' h
  apply apply_firstDiff_ne hne'
  rw [le_zero_iff.1 h]
  apply apply_eq_of_dist_lt _ le_rfl
  rw [pow_zero]
  exact hxy
case inr
E : ℕ → Type ?u.233694
α : Type u_1
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 | Set.Nonempty (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))}
g : ↑s → α := fun x => Set.Nonempty.some (_ : ↑x ∈ s)
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
⊢ dist (g x) (g y) ≤ 4 * dist x y
case inr
E : ℕ → Type ?u.233694
α : Type u_1
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 | Set.Nonempty (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))}
g : ↑s → α := fun x => Set.Nonempty.some (_ : ↑x ∈ s)
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
have hn : firstDiff x.1 y.1 = n + 1 := (Nat.succ_pred_eq_of_pos diff_pos).symm
case inr
E : ℕ → Type ?u.233694
α : Type u_1
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 | Set.Nonempty (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))}
g : ↑s → α := fun x => Set.Nonempty.some (_ : ↑x ∈ s)
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
⊢ dist (g x) (g y) ≤ 4 * (1 / 2) ^ (n + 1)
case inr
E : ℕ → Type ?u.233694
α : Type u_1
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 | Set.Nonempty (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))}
g : ↑s → α := fun x => Set.Nonempty.some (_ : ↑x ∈ s)
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
⊢ dist (g x) (g y) ≤ 4 * dist x y
rw [dist', dist_eq_of_ne hne', hn]
case inr
E : ℕ → Type ?u.233694
α : Type u_1
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 | Set.Nonempty (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))}
g : ↑s → α := fun x => Set.Nonempty.some (_ : ↑x ∈ s)
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) (g y) ≤ 4 * (1 / 2) ^ (n + 1)
case inr
E : ℕ → Type ?u.233694
α : Type u_1
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 | Set.Nonempty (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))}
g : ↑s → α := fun x => Set.Nonempty.some (_ : ↑x ∈ s)
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
⊢ dist (g x) (g y) ≤ 4 * (1 / 2) ^ (n + 1)
have B : x.1 n = y.1 n := mem_cylinder_firstDiff x.1 y.1 n (Nat.pred_lt diff_pos.ne')
no goals
case inr
E : ℕ → Type ?u.233694
α : Type u_1
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 | Set.Nonempty (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))}
g : ↑s → α := fun x => Set.Nonempty.some (_ : ↑x ∈ s)
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) (g y) ≤ 4 * (1 / 2) ^ (n + 1)
calc
  dist (g x) (g y) ≤ dist (g x) (u (x.1 n)) + dist (g y) (u (x.1 n)) :=
    dist_triangle_right _ _ _
  _ = dist (g x) (u (x.1 n)) + dist (g y) (u (y.1 n)) := by rw [← B]
  _ ≤ (1 / 2) ^ n + (1 / 2) ^ n := (add_le_add (A x n) (A y n))
  _ = 4 * (1 / 2) ^ (n + 1) := by ring
no goals
case inl
E : ℕ → Type ?u.233694
α : Type u_1
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 | Set.Nonempty (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))}
g : ↑s → α := fun x => Set.Nonempty.some (_ : ↑x ∈ s)
A : ∀ (x : ↑s) (n : ℕ), dist (g x) (u (↑x n)) ≤ (1 / 2) ^ n
x : ↑s
hxy : dist x x < 1
⊢ dist (g x) (g x) ≤ 4 * dist x x
simp
E : ℕ → Type ?u.233694
α : Type u_1
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 | Set.Nonempty (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))}
g : ↑s → α := fun x => Set.Nonempty.some (_ : ↑x ∈ s)
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
⊢ False
E : ℕ → Type ?u.233694
α : Type u_1
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 | Set.Nonempty (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))}
g : ↑s → α := fun x => Set.Nonempty.some (_ : ↑x ∈ s)
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
⊢ 0 < firstDiff ↑x ↑y
by_contra' h
E : ℕ → Type ?u.233694
α : Type u_1
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 | Set.Nonempty (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))}
g : ↑s → α := fun x => Set.Nonempty.some (_ : ↑x ∈ s)
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
⊢ ↑x (firstDiff ↑x ↑y) = ↑y (firstDiff ↑x ↑y)
E : ℕ → Type ?u.233694
α : Type u_1
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 | Set.Nonempty (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))}
g : ↑s → α := fun x => Set.Nonempty.some (_ : ↑x ∈ s)
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
⊢ False
apply apply_firstDiff_ne hne'
E : ℕ → Type ?u.233694
α : Type u_1
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 | Set.Nonempty (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))}
g : ↑s → α := fun x => Set.Nonempty.some (_ : ↑x ∈ s)
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
⊢ ↑x 0 = ↑y 0
E : ℕ → Type ?u.233694
α : Type u_1
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 | Set.Nonempty (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))}
g : ↑s → α := fun x => Set.Nonempty.some (_ : ↑x ∈ s)
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
⊢ ↑x (firstDiff ↑x ↑y) = ↑y (firstDiff ↑x ↑y)
rw [le_zero_iff.1 h]
E : ℕ → Type ?u.233694
α : Type u_1
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 | Set.Nonempty (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))}
g : ↑s → α := fun x => Set.Nonempty.some (_ : ↑x ∈ s)
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 / 2) ^ 0
E : ℕ → Type ?u.233694
α : Type u_1
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 | Set.Nonempty (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))}
g : ↑s → α := fun x => Set.Nonempty.some (_ : ↑x ∈ s)
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
⊢ ↑x 0 = ↑y 0
apply apply_eq_of_dist_lt _ le_rfl
E : ℕ → Type ?u.233694
α : Type u_1
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 | Set.Nonempty (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))}
g : ↑s → α := fun x => Set.Nonempty.some (_ : ↑x ∈ s)
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
E : ℕ → Type ?u.233694
α : Type u_1
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 | Set.Nonempty (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))}
g : ↑s → α := fun x => Set.Nonempty.some (_ : ↑x ∈ s)
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 / 2) ^ 0
rw [pow_zero]
no goals
E : ℕ → Type ?u.233694
α : Type u_1
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 | Set.Nonempty (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))}
g : ↑s → α := fun x => Set.Nonempty.some (_ : ↑x ∈ s)
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
exact hxy
no goals
E : ℕ → Type ?u.233694
α : Type u_1
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 | Set.Nonempty (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))}
g : ↑s → α := fun x => Set.Nonempty.some (_ : ↑x ∈ s)
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))
rw [← B]
no goals
E : ℕ → Type ?u.233694
α : Type u_1
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 | Set.Nonempty (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))}
g : ↑s → α := fun x => Set.Nonempty.some (_ : ↑x ∈ s)
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)
ring
E : ℕ → Type ?u.233694
α : Type u_1
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 | Set.Nonempty (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))}
g : ↑s → α := fun x => Set.Nonempty.some (_ : ↑x ∈ s)
A : ∀ (x : ↑s) (n : ℕ), dist (g x) (u (↑x n)) ≤ (1 / 2) ^ n
g_cont : Continuous g
y : α
this : ∀ (n : ℕ), ∃ j, y ∈ closedBall (u j) ((1 / 2) ^ n)
⊢ ∃ a, g a = y
E : ℕ → Type ?u.233694
α : Type u_1
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 | Set.Nonempty (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))}
g : ↑s → α := fun x => Set.Nonempty.some (_ : ↑x ∈ s)
A : ∀ (x : ↑s) (n : ℕ), dist (g x) (u (↑x n)) ≤ (1 / 2) ^ n
g_cont : Continuous g
y : α
⊢ ∃ a, g a = y
have : ∀ n : ℕ, ∃ j, y ∈ closedBall (u j) ((1 / 2) ^ n) := fun n ↦ by
  rcases hu.exists_dist_lt y (by simp : (0 : ℝ) < (1 / 2) ^ n) with ⟨j, hj⟩
  exact ⟨j, hj.le⟩
E : ℕ → Type ?u.233694
α : Type u_1
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 | Set.Nonempty (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))}
g : ↑s → α := fun x => Set.Nonempty.some (_ : ↑x ∈ s)
A : ∀ (x : ↑s) (n : ℕ), dist (g x) (u (↑x n)) ≤ (1 / 2) ^ n
g_cont : Continuous g
y : α
x : ℕ → ℕ
hx : ∀ (n : ℕ), y ∈ closedBall (u (x n)) ((1 / 2) ^ n)
⊢ ∃ a, g a = y
E : ℕ → Type ?u.233694
α : Type u_1
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 | Set.Nonempty (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))}
g : ↑s → α := fun x => Set.Nonempty.some (_ : ↑x ∈ s)
A : ∀ (x : ↑s) (n : ℕ), dist (g x) (u (↑x n)) ≤ (1 / 2) ^ n
g_cont : Continuous g
y : α
this : ∀ (n : ℕ), ∃ j, y ∈ closedBall (u j) ((1 / 2) ^ n)
⊢ ∃ a, g a = y
choose x hx using this
E : ℕ → Type ?u.233694
α : Type u_1
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 | Set.Nonempty (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))}
g : ↑s → α := fun x => Set.Nonempty.some (_ : ↑x ∈ s)
A : ∀ (x : ↑s) (n : ℕ), dist (g x) (u (↑x n)) ≤ (1 / 2) ^ n
g_cont : Continuous g
y : α
x : ℕ → ℕ
hx : ∀ (n : ℕ), y ∈ closedBall (u (x n)) ((1 / 2) ^ n)
I : Set.Nonempty (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))
⊢ ∃ a, g a = y
E : ℕ → Type ?u.233694
α : Type u_1
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 | Set.Nonempty (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))}
g : ↑s → α := fun x => Set.Nonempty.some (_ : ↑x ∈ s)
A : ∀ (x : ↑s) (n : ℕ), dist (g x) (u (↑x n)) ≤ (1 / 2) ^ n
g_cont : Continuous g
y : α
x : ℕ → ℕ
hx : ∀ (n : ℕ), y ∈ closedBall (u (x n)) ((1 / 2) ^ n)
⊢ ∃ a, g a = y
have I : (⋂ n : ℕ, closedBall (u (x n)) ((1 / 2) ^ n)).Nonempty := ⟨y, mem_iInter.2 hx⟩
E : ℕ → Type ?u.233694
α : Type u_1
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 | Set.Nonempty (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))}
g : ↑s → α := fun x => Set.Nonempty.some (_ : ↑x ∈ s)
A : ∀ (x : ↑s) (n : ℕ), dist (g x) (u (↑x n)) ≤ (1 / 2) ^ n
g_cont : Continuous g
y : α
x : ℕ → ℕ
hx : ∀ (n : ℕ), y ∈ closedBall (u (x n)) ((1 / 2) ^ n)
I : Set.Nonempty (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))
⊢ g { val := x, property := I } = y
E : ℕ → Type ?u.233694
α : Type u_1
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 | Set.Nonempty (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))}
g : ↑s → α := fun x => Set.Nonempty.some (_ : ↑x ∈ s)
A : ∀ (x : ↑s) (n : ℕ), dist (g x) (u (↑x n)) ≤ (1 / 2) ^ n
g_cont : Continuous g
y : α
x : ℕ → ℕ
hx : ∀ (n : ℕ), y ∈ closedBall (u (x n)) ((1 / 2) ^ n)
I : Set.Nonempty (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))
⊢ ∃ a, g a = y
refine' ⟨⟨x, I⟩, _⟩
E : ℕ → Type ?u.233694
α : Type u_1
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 | Set.Nonempty (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))}
g : ↑s → α := fun x => Set.Nonempty.some (_ : ↑x ∈ s)
A : ∀ (x : ↑s) (n : ℕ), dist (g x) (u (↑x n)) ≤ (1 / 2) ^ n
g_cont : Continuous g
y : α
x : ℕ → ℕ
hx : ∀ (n : ℕ), y ∈ closedBall (u (x n)) ((1 / 2) ^ n)
I : Set.Nonempty (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))
⊢ dist (g { val := x, property := I }) y ≤ 0
E : ℕ → Type ?u.233694
α : Type u_1
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 | Set.Nonempty (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))}
g : ↑s → α := fun x => Set.Nonempty.some (_ : ↑x ∈ s)
A : ∀ (x : ↑s) (n : ℕ), dist (g x) (u (↑x n)) ≤ (1 / 2) ^ n
g_cont : Continuous g
y : α
x : ℕ → ℕ
hx : ∀ (n : ℕ), y ∈ closedBall (u (x n)) ((1 / 2) ^ n)
I : Set.Nonempty (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))
⊢ g { val := x, property := I } = y
refine' dist_le_zero.1 _
E : ℕ → Type ?u.233694
α : Type u_1
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 | Set.Nonempty (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))}
g : ↑s → α := fun x => Set.Nonempty.some (_ : ↑x ∈ s)
A : ∀ (x : ↑s) (n : ℕ), dist (g x) (u (↑x n)) ≤ (1 / 2) ^ n
g_cont : Continuous g
y : α
x : ℕ → ℕ
hx : ∀ (n : ℕ), y ∈ closedBall (u (x n)) ((1 / 2) ^ n)
I : Set.Nonempty (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))
J : ∀ (n : ℕ), dist (g { val := x, property := I }) y ≤ (1 / 2) ^ n + (1 / 2) ^ n
⊢ dist (g { val := x, property := I }) y ≤ 0
E : ℕ → Type ?u.233694
α : Type u_1
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 | Set.Nonempty (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))}
g : ↑s → α := fun x => Set.Nonempty.some (_ : ↑x ∈ s)
A : ∀ (x : ↑s) (n : ℕ), dist (g x) (u (↑x n)) ≤ (1 / 2) ^ n
g_cont : Continuous g
y : α
x : ℕ → ℕ
hx : ∀ (n : ℕ), y ∈ closedBall (u (x n)) ((1 / 2) ^ n)
I : Set.Nonempty (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))
⊢ dist (g { val := x, property := I }) y ≤ 0
have J : ∀ n : ℕ, dist (g ⟨x, I⟩) y ≤ (1 / 2) ^ n + (1 / 2) ^ n := fun n =>
  calc
    dist (g ⟨x, I⟩) y ≤ dist (g ⟨x, I⟩) (u (x n)) + dist y (u (x n)) :=
      dist_triangle_right _ _ _
    _ ≤ (1 / 2) ^ n + (1 / 2) ^ n := add_le_add (A ⟨x, I⟩ n) (hx n)
E : ℕ → Type ?u.233694
α : Type u_1
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 | Set.Nonempty (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))}
g : ↑s → α := fun x => Set.Nonempty.some (_ : ↑x ∈ s)
A : ∀ (x : ↑s) (n : ℕ), dist (g x) (u (↑x n)) ≤ (1 / 2) ^ n
g_cont : Continuous g
y : α
x : ℕ → ℕ
hx : ∀ (n : ℕ), y ∈ closedBall (u (x n)) ((1 / 2) ^ n)
I : Set.Nonempty (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))
J : ∀ (n : ℕ), dist (g { val := x, property := I }) y ≤ (1 / 2) ^ n + (1 / 2) ^ n
L : Tendsto (fun n => (1 / 2) ^ n + (1 / 2) ^ n) atTop (𝓝 (0 + 0))
⊢ dist (g { val := x, property := I }) y ≤ 0
E : ℕ → Type ?u.233694
α : Type u_1
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 | Set.Nonempty (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))}
g : ↑s → α := fun x => Set.Nonempty.some (_ : ↑x ∈ s)
A : ∀ (x : ↑s) (n : ℕ), dist (g x) (u (↑x n)) ≤ (1 / 2) ^ n
g_cont : Continuous g
y : α
x : ℕ → ℕ
hx : ∀ (n : ℕ), y ∈ closedBall (u (x n)) ((1 / 2) ^ n)
I : Set.Nonempty (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))
J : ∀ (n : ℕ), dist (g { val := x, property := I }) y ≤ (1 / 2) ^ n + (1 / 2) ^ n
⊢ dist (g { val := x, property := I }) y ≤ 0
have L : Tendsto (fun n : ℕ => (1 / 2 : ℝ) ^ n + (1 / 2) ^ n) atTop (𝓝 (0 + 0)) :=
  (tendsto_pow_atTop_nhds_0_of_lt_1 I0.le I1).add (tendsto_pow_atTop_nhds_0_of_lt_1 I0.le I1)
E : ℕ → Type ?u.233694
α : Type u_1
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 | Set.Nonempty (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))}
g : ↑s → α := fun x => Set.Nonempty.some (_ : ↑x ∈ s)
A : ∀ (x : ↑s) (n : ℕ), dist (g x) (u (↑x n)) ≤ (1 / 2) ^ n
g_cont : Continuous g
y : α
x : ℕ → ℕ
hx : ∀ (n : ℕ), y ∈ closedBall (u (x n)) ((1 / 2) ^ n)
I : Set.Nonempty (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))
J : ∀ (n : ℕ), dist (g { val := x, property := I }) y ≤ (1 / 2) ^ n + (1 / 2) ^ n
L : Tendsto (fun n => (1 / 2) ^ n + (1 / 2) ^ n) atTop (𝓝 0)
⊢ dist (g { val := x, property := I }) y ≤ 0
E : ℕ → Type ?u.233694
α : Type u_1
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 | Set.Nonempty (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))}
g : ↑s → α := fun x => Set.Nonempty.some (_ : ↑x ∈ s)
A : ∀ (x : ↑s) (n : ℕ), dist (g x) (u (↑x n)) ≤ (1 / 2) ^ n
g_cont : Continuous g
y : α
x : ℕ → ℕ
hx : ∀ (n : ℕ), y ∈ closedBall (u (x n)) ((1 / 2) ^ n)
I : Set.Nonempty (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))
J : ∀ (n : ℕ), dist (g { val := x, property := I }) y ≤ (1 / 2) ^ n + (1 / 2) ^ n
L : Tendsto (fun n => (1 / 2) ^ n + (1 / 2) ^ n) atTop (𝓝 (0 + 0))
⊢ dist (g { val := x, property := I }) y ≤ 0
rw [add_zero] at L
no goals
E : ℕ → Type ?u.233694
α : Type u_1
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 | Set.Nonempty (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))}
g : ↑s → α := fun x => Set.Nonempty.some (_ : ↑x ∈ s)
A : ∀ (x : ↑s) (n : ℕ), dist (g x) (u (↑x n)) ≤ (1 / 2) ^ n
g_cont : Continuous g
y : α
x : ℕ → ℕ
hx : ∀ (n : ℕ), y ∈ closedBall (u (x n)) ((1 / 2) ^ n)
I : Set.Nonempty (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))
J : ∀ (n : ℕ), dist (g { val := x, property := I }) y ≤ (1 / 2) ^ n + (1 / 2) ^ n
L : Tendsto (fun n => (1 / 2) ^ n + (1 / 2) ^ n) atTop (𝓝 0)
⊢ dist (g { val := x, property := I }) y ≤ 0
exact ge_of_tendsto' L J
case intro
E : ℕ → Type ?u.233694
α : Type u_1
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 | Set.Nonempty (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))}
g : ↑s → α := fun x => Set.Nonempty.some (_ : ↑x ∈ s)
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)
E : ℕ → Type ?u.233694
α : Type u_1
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 | Set.Nonempty (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))}
g : ↑s → α := fun x => Set.Nonempty.some (_ : ↑x ∈ s)
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)
rcases hu.exists_dist_lt y (by simp : (0 : ℝ) < (1 / 2) ^ n) with ⟨j, hj⟩
no goals
case intro
E : ℕ → Type ?u.233694
α : Type u_1
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 | Set.Nonempty (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))}
g : ↑s → α := fun x => Set.Nonempty.some (_ : ↑x ∈ s)
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)
exact ⟨j, hj.le⟩
no goals
E : ℕ → Type ?u.233694
α : Type u_1
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 | Set.Nonempty (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))}
g : ↑s → α := fun x => Set.Nonempty.some (_ : ↑x ∈ s)
A : ∀ (x : ↑s) (n : ℕ), dist (g x) (u (↑x n)) ≤ (1 / 2) ^ n
g_cont : Continuous g
y : α
n : ℕ
⊢ 0 < (1 / 2) ^ n
simp
E : ℕ → Type ?u.233694
α : Type u_1
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 | Set.Nonempty (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))}
g : ↑s → α := fun x => Set.Nonempty.some (_ : ↑x ∈ s)
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)
⊢ x ∈ s
E : ℕ → Type ?u.233694
α : Type u_1
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 | Set.Nonempty (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))}
g : ↑s → α := fun x => Set.Nonempty.some (_ : ↑x ∈ s)
A : ∀ (x : ↑s) (n : ℕ), dist (g x) (u (↑x n)) ≤ (1 / 2) ^ n
g_cont : Continuous g
g_surj : Surjective g
⊢ IsClosed s
refine isClosed_iff_clusterPt.mpr fun x hx ↦ ?_
E : ℕ → Type ?u.233694
α : Type u_1
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 | Set.Nonempty (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))}
g : ↑s → α := fun x => Set.Nonempty.some (_ : ↑x ∈ s)
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)
⊢ x ∈ s
E : ℕ → Type ?u.233694
α : Type u_1
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 | Set.Nonempty (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))}
g : ↑s → α := fun x => Set.Nonempty.some (_ : ↑x ∈ s)
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)
⊢ x ∈ s
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_0_of_lt_1 I0.le I1).const_mul _
  rw [MulZeroClass.mul_zero] at this
  exact
    squeeze_zero (fun n => diam_nonneg) (fun n => diam_closedBall (pow_nonneg I0.le _)) this
E : ℕ → Type ?u.233694
α : Type u_1
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 | Set.Nonempty (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))}
g : ↑s → α := fun x => Set.Nonempty.some (_ : ↑x ∈ s)
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 : ℕ
⊢ Set.Nonempty (⋂ (n : ℕ) (_ : n ≤ N), closedBall (u (x n)) ((1 / 2) ^ n))
E : ℕ → Type ?u.233694
α : Type u_1
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 | Set.Nonempty (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))}
g : ↑s → α := fun x => Set.Nonempty.some (_ : ↑x ∈ s)
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)
⊢ x ∈ s
refine nonempty_iInter_of_nonempty_biInter (fun n => isClosed_ball)
  (fun n => bounded_closedBall) (fun N ↦ ?_) L
case intro.intro
E : ℕ → Type ?u.233694
α : Type u_1
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 | Set.Nonempty (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))}
g : ↑s → α := fun x => Set.Nonempty.some (_ : ↑x ∈ s)
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
⊢ Set.Nonempty (⋂ (n : ℕ) (_ : n ≤ N), closedBall (u (x n)) ((1 / 2) ^ n))
E : ℕ → Type ?u.233694
α : Type u_1
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 | Set.Nonempty (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))}
g : ↑s → α := fun x => Set.Nonempty.some (_ : ↑x ∈ s)
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 : ℕ
⊢ Set.Nonempty (⋂ (n : ℕ) (_ : n ≤ N), closedBall (u (x n)) ((1 / 2) ^ n))
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))
case intro.intro
E✝ : ℕ → Type ?u.233694
α : Type u_1
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 | Set.Nonempty (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))}
g : ↑s → α := fun x => Set.Nonempty.some (_ : ↑x ∈ s)
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
E :
  (⋂ (n : ℕ) (_ : n ≤ N), closedBall (u (x n)) ((1 / 2) ^ n)) =
    ⋂ (n : ℕ) (_ : n ≤ N), closedBall (u (y n)) ((1 / 2) ^ n)
⊢ Set.Nonempty (⋂ (n : ℕ) (_ : n ≤ N), closedBall (u (x n)) ((1 / 2) ^ n))
case intro.intro
E : ℕ → Type ?u.233694
α : Type u_1
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 | Set.Nonempty (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))}
g : ↑s → α := fun x => Set.Nonempty.some (_ : ↑x ∈ s)
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
⊢ Set.Nonempty (⋂ (n : ℕ) (_ : n ≤ N), closedBall (u (x n)) ((1 / 2) ^ 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]
case intro.intro
E✝ : ℕ → Type ?u.233694
α : Type u_1
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 | Set.Nonempty (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))}
g : ↑s → α := fun x => Set.Nonempty.some (_ : ↑x ∈ s)
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
E :
  (⋂ (n : ℕ) (_ : n ≤ N), closedBall (u (x n)) ((1 / 2) ^ n)) =
    ⋂ (n : ℕ) (_ : n ≤ N), closedBall (u (y n)) ((1 / 2) ^ n)
⊢ Set.Nonempty (⋂ (n : ℕ) (_ : n ≤ N), closedBall (u (y n)) ((1 / 2) ^ n))
case intro.intro
E✝ : ℕ → Type ?u.233694
α : Type u_1
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 | Set.Nonempty (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))}
g : ↑s → α := fun x => Set.Nonempty.some (_ : ↑x ∈ s)
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
E :
  (⋂ (n : ℕ) (_ : n ≤ N), closedBall (u (x n)) ((1 / 2) ^ n)) =
    ⋂ (n : ℕ) (_ : n ≤ N), closedBall (u (y n)) ((1 / 2) ^ n)
⊢ Set.Nonempty (⋂ (n : ℕ) (_ : n ≤ N), closedBall (u (x n)) ((1 / 2) ^ n))
rw [E]
E✝ : ℕ → Type ?u.233694
α : Type u_1
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 | Set.Nonempty (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))}
g : ↑s → α := fun x => Set.Nonempty.some (_ : ↑x ∈ s)
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
E :
  (⋂ (n : ℕ) (_ : n ≤ N), closedBall (u (x n)) ((1 / 2) ^ n)) =
    ⋂ (n : ℕ) (_ : n ≤ N), closedBall (u (y n)) ((1 / 2) ^ n)
⊢ (⋂ (n : ℕ), closedBall (u (y n)) ((1 / 2) ^ n)) ⊆ ⋂ (n : ℕ) (_ : n ≤ N), closedBall (u (y n)) ((1 / 2) ^ n)
case intro.intro
E✝ : ℕ → Type ?u.233694
α : Type u_1
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 | Set.Nonempty (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))}
g : ↑s → α := fun x => Set.Nonempty.some (_ : ↑x ∈ s)
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
E :
  (⋂ (n : ℕ) (_ : n ≤ N), closedBall (u (x n)) ((1 / 2) ^ n)) =
    ⋂ (n : ℕ) (_ : n ≤ N), closedBall (u (y n)) ((1 / 2) ^ n)
⊢ Set.Nonempty (⋂ (n : ℕ) (_ : n ≤ N), closedBall (u (y n)) ((1 / 2) ^ n))
apply Nonempty.mono _ ys
no goals
E✝ : ℕ → Type ?u.233694
α : Type u_1
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 | Set.Nonempty (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))}
g : ↑s → α := fun x => Set.Nonempty.some (_ : ↑x ∈ s)
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
E :
  (⋂ (n : ℕ) (_ : n ≤ N), closedBall (u (x n)) ((1 / 2) ^ n)) =
    ⋂ (n : ℕ) (_ : n ≤ N), closedBall (u (y n)) ((1 / 2) ^ n)
⊢ (⋂ (n : ℕ), closedBall (u (y n)) ((1 / 2) ^ n)) ⊆ ⋂ (n : ℕ) (_ : n ≤ N), closedBall (u (y n)) ((1 / 2) ^ n)
apply iInter_subset_iInter₂
E : ℕ → Type ?u.233694
α : Type u_1
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 | Set.Nonempty (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))}
g : ↑s → α := fun x => Set.Nonempty.some (_ : ↑x ∈ s)
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)
this : Tendsto (fun n => 2 * (1 / 2) ^ n) atTop (𝓝 (2 * 0))
⊢ Tendsto (fun n => diam (closedBall (u (x n)) ((1 / 2) ^ n))) atTop (𝓝 0)
E : ℕ → Type ?u.233694
α : Type u_1
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 | Set.Nonempty (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))}
g : ↑s → α := fun x => Set.Nonempty.some (_ : ↑x ∈ s)
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)
⊢ Tendsto (fun n => diam (closedBall (u (x n)) ((1 / 2) ^ n))) atTop (𝓝 0)
have : Tendsto (fun n : ℕ => (2 : ℝ) * (1 / 2) ^ n) atTop (𝓝 (2 * 0)) :=
  (tendsto_pow_atTop_nhds_0_of_lt_1 I0.le I1).const_mul _
E : ℕ → Type ?u.233694
α : Type u_1
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 | Set.Nonempty (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))}
g : ↑s → α := fun x => Set.Nonempty.some (_ : ↑x ∈ s)
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)
this : Tendsto (fun n => 2 * (1 / 2) ^ n) atTop (𝓝 0)
⊢ Tendsto (fun n => diam (closedBall (u (x n)) ((1 / 2) ^ n))) atTop (𝓝 0)
E : ℕ → Type ?u.233694
α : Type u_1
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 | Set.Nonempty (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))}
g : ↑s → α := fun x => Set.Nonempty.some (_ : ↑x ∈ s)
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)
this : Tendsto (fun n => 2 * (1 / 2) ^ n) atTop (𝓝 (2 * 0))
⊢ Tendsto (fun n => diam (closedBall (u (x n)) ((1 / 2) ^ n))) atTop (𝓝 0)
rw [MulZeroClass.mul_zero] at this
no goals
E : ℕ → Type ?u.233694
α : Type u_1
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 | Set.Nonempty (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))}
g : ↑s → α := fun x => Set.Nonempty.some (_ : ↑x ∈ s)
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)
this : Tendsto (fun n => 2 * (1 / 2) ^ n) atTop (𝓝 0)
⊢ Tendsto (fun n => diam (closedBall (u (x n)) ((1 / 2) ^ n))) atTop (𝓝 0)
exact
  squeeze_zero (fun n => diam_nonneg) (fun n => diam_closedBall (pow_nonneg I0.le _)) this
E : ℕ → Type ?u.233694
α : Type u_1
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 | Set.Nonempty (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))}
g : ↑s → α := fun x => Set.Nonempty.some (_ : ↑x ∈ s)
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 : ℕ
hn : n ≤ N
⊢ closedBall (u (x n)) ((1 / 2) ^ n) = closedBall (u (y n)) ((1 / 2) ^ n)
E : ℕ → Type ?u.233694
α : Type u_1
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 | Set.Nonempty (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))}
g : ↑s → α := fun x => Set.Nonempty.some (_ : ↑x ∈ s)
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)) =
    ⋂ (n : ℕ) (_ : n ≤ N), closedBall (u (y n)) ((1 / 2) ^ n)
refine iInter_congr fun n ↦ iInter_congr fun hn ↦ ?_
E : ℕ → Type ?u.233694
α : Type u_1
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 | Set.Nonempty (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))}
g : ↑s → α := fun x => Set.Nonempty.some (_ : ↑x ∈ s)
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 : ℕ
hn : n ≤ N
this : x n = y n
⊢ closedBall (u (x n)) ((1 / 2) ^ n) = closedBall (u (y n)) ((1 / 2) ^ n)
E : ℕ → Type ?u.233694
α : Type u_1
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 | Set.Nonempty (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))}
g : ↑s → α := fun x => Set.Nonempty.some (_ : ↑x ∈ s)
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 : ℕ
hn : n ≤ N
⊢ closedBall (u (x n)) ((1 / 2) ^ n) = closedBall (u (y n)) ((1 / 2) ^ n)
have : x n = y n := apply_eq_of_dist_lt (mem_ball'.1 hxy) hn
no goals
E : ℕ → Type ?u.233694
α : Type u_1
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 | Set.Nonempty (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))}
g : ↑s → α := fun x => Set.Nonempty.some (_ : ↑x ∈ s)
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 : ℕ
hn : n ≤ N
this : x n = y n
⊢ closedBall (u (x n)) ((1 / 2) ^ n) = closedBall (u (y n)) ((1 / 2) ^ n)
rw [this]
E : ℕ → Type ?u.233694
α : Type u_1
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 | Set.Nonempty (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))}
g : ↑s → α := fun x => Set.Nonempty.some (_ : ↑x ∈ s)
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
⊢ Set.Nonempty s
E : ℕ → Type ?u.233694
α : Type u_1
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 | Set.Nonempty (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))}
g : ↑s → α := fun x => Set.Nonempty.some (_ : ↑x ∈ s)
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
⊢ ∃ f, (∀ (x : ↑s), f ↑x = x) ∧ Surjective f ∧ Continuous f
apply exists_retraction_subtype_of_isClosed s_closed
no goals
E : ℕ → Type ?u.233694
α : Type u_1
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 | Set.Nonempty (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))}
g : ↑s → α := fun x => Set.Nonempty.some (_ : ↑x ∈ s)
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
⊢ Set.Nonempty s
simpa only [nonempty_coe_sort] using g_surj.nonempty