[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
E : Type u_4
F : Type u_5
𝕜 : Type u_6
inst✝² : MeasurableSpace α
inst✝¹ : PseudoEMetricSpace α
inst✝ : OpensMeasurableSpace α
e : ℕ → α
N : ℕ
x : α
⊢ ↑(nearestPtInd e (N + 1)) x =
    if ∀ (k : ℕ), k ≤ N → edist (e (N + 1)) x < edist (e k) x then N + 1 else ↑(nearestPtInd e N) x
[PROOFSTEP]
simp only [nearestPtInd, coe_piecewise, Set.piecewise]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
E : Type u_4
F : Type u_5
𝕜 : Type u_6
inst✝² : MeasurableSpace α
inst✝¹ : PseudoEMetricSpace α
inst✝ : OpensMeasurableSpace α
e : ℕ → α
N : ℕ
x : α
⊢ (if x ∈ ⋂ (k : ℕ) (_ : k ≤ Nat.add N 0), {x | edist (e (Nat.add N 0 + 1)) x < edist (e k) x} then
      ↑(const α (Nat.add N 0 + 1)) x
    else ↑(nearestPtInd e (Nat.add N 0)) x) =
    if ∀ (k : ℕ), k ≤ N → edist (e (N + 1)) x < edist (e k) x then N + 1 else ↑(nearestPtInd e N) x
[PROOFSTEP]
congr
[GOAL]
case e_c
α : Type u_1
β : Type u_2
ι : Type u_3
E : Type u_4
F : Type u_5
𝕜 : Type u_6
inst✝² : MeasurableSpace α
inst✝¹ : PseudoEMetricSpace α
inst✝ : OpensMeasurableSpace α
e : ℕ → α
N : ℕ
x : α
⊢ (x ∈ ⋂ (k : ℕ) (_ : k ≤ Nat.add N 0), {x | edist (e (Nat.add N 0 + 1)) x < edist (e k) x}) =
    ∀ (k : ℕ), k ≤ N → edist (e (N + 1)) x < edist (e k) x
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
E : Type u_4
F : Type u_5
𝕜 : Type u_6
inst✝² : MeasurableSpace α
inst✝¹ : PseudoEMetricSpace α
inst✝ : OpensMeasurableSpace α
e : ℕ → α
N : ℕ
x : α
⊢ ↑(nearestPtInd e N) x ≤ N
[PROOFSTEP]
induction' N with N ihN
[GOAL]
case zero
α : Type u_1
β : Type u_2
ι : Type u_3
E : Type u_4
F : Type u_5
𝕜 : Type u_6
inst✝² : MeasurableSpace α
inst✝¹ : PseudoEMetricSpace α
inst✝ : OpensMeasurableSpace α
e : ℕ → α
x : α
⊢ ↑(nearestPtInd e Nat.zero) x ≤ Nat.zero
[PROOFSTEP]
simp
[GOAL]
case succ
α : Type u_1
β : Type u_2
ι : Type u_3
E : Type u_4
F : Type u_5
𝕜 : Type u_6
inst✝² : MeasurableSpace α
inst✝¹ : PseudoEMetricSpace α
inst✝ : OpensMeasurableSpace α
e : ℕ → α
x : α
N : ℕ
ihN : ↑(nearestPtInd e N) x ≤ N
⊢ ↑(nearestPtInd e (Nat.succ N)) x ≤ Nat.succ N
[PROOFSTEP]
simp only [nearestPtInd_succ]
[GOAL]
case succ
α : Type u_1
β : Type u_2
ι : Type u_3
E : Type u_4
F : Type u_5
𝕜 : Type u_6
inst✝² : MeasurableSpace α
inst✝¹ : PseudoEMetricSpace α
inst✝ : OpensMeasurableSpace α
e : ℕ → α
x : α
N : ℕ
ihN : ↑(nearestPtInd e N) x ≤ N
⊢ (if ∀ (k : ℕ), k ≤ N → edist (e (N + 1)) x < edist (e k) x then N + 1 else ↑(nearestPtInd e N) x) ≤ Nat.succ N
[PROOFSTEP]
split_ifs
[GOAL]
case pos
α : Type u_1
β : Type u_2
ι : Type u_3
E : Type u_4
F : Type u_5
𝕜 : Type u_6
inst✝² : MeasurableSpace α
inst✝¹ : PseudoEMetricSpace α
inst✝ : OpensMeasurableSpace α
e : ℕ → α
x : α
N : ℕ
ihN : ↑(nearestPtInd e N) x ≤ N
h✝ : ∀ (k : ℕ), k ≤ N → edist (e (N + 1)) x < edist (e k) x
⊢ N + 1 ≤ Nat.succ N
case neg
α : Type u_1
β : Type u_2
ι : Type u_3
E : Type u_4
F : Type u_5
𝕜 : Type u_6
inst✝² : MeasurableSpace α
inst✝¹ : PseudoEMetricSpace α
inst✝ : OpensMeasurableSpace α
e : ℕ → α
x : α
N : ℕ
ihN : ↑(nearestPtInd e N) x ≤ N
h✝ : ¬∀ (k : ℕ), k ≤ N → edist (e (N + 1)) x < edist (e k) x
⊢ ↑(nearestPtInd e N) x ≤ Nat.succ N
[PROOFSTEP]
exacts [le_rfl, ihN.trans N.le_succ]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
E : Type u_4
F : Type u_5
𝕜 : Type u_6
inst✝² : MeasurableSpace α
inst✝¹ : PseudoEMetricSpace α
inst✝ : OpensMeasurableSpace α
e : ℕ → α
x : α
k N : ℕ
hk : k ≤ N
⊢ edist (↑(nearestPt e N) x) x ≤ edist (e k) x
[PROOFSTEP]
induction' N with N ihN generalizing k
[GOAL]
case zero
α : Type u_1
β : Type u_2
ι : Type u_3
E : Type u_4
F : Type u_5
𝕜 : Type u_6
inst✝² : MeasurableSpace α
inst✝¹ : PseudoEMetricSpace α
inst✝ : OpensMeasurableSpace α
e : ℕ → α
x : α
k✝ N : ℕ
hk✝ : k✝ ≤ N
k : ℕ
hk : k ≤ Nat.zero
⊢ edist (↑(nearestPt e Nat.zero) x) x ≤ edist (e k) x
[PROOFSTEP]
simp [nonpos_iff_eq_zero.1 hk, le_refl]
[GOAL]
case succ
α : Type u_1
β : Type u_2
ι : Type u_3
E : Type u_4
F : Type u_5
𝕜 : Type u_6
inst✝² : MeasurableSpace α
inst✝¹ : PseudoEMetricSpace α
inst✝ : OpensMeasurableSpace α
e : ℕ → α
x : α
k✝ N✝ : ℕ
hk✝ : k✝ ≤ N✝
N : ℕ
ihN : ∀ {k : ℕ}, k ≤ N → edist (↑(nearestPt e N) x) x ≤ edist (e k) x
k : ℕ
hk : k ≤ Nat.succ N
⊢ edist (↑(nearestPt e (Nat.succ N)) x) x ≤ edist (e k) x
[PROOFSTEP]
simp only [nearestPt, nearestPtInd_succ, map_apply]
[GOAL]
case succ
α : Type u_1
β : Type u_2
ι : Type u_3
E : Type u_4
F : Type u_5
𝕜 : Type u_6
inst✝² : MeasurableSpace α
inst✝¹ : PseudoEMetricSpace α
inst✝ : OpensMeasurableSpace α
e : ℕ → α
x : α
k✝ N✝ : ℕ
hk✝ : k✝ ≤ N✝
N : ℕ
ihN : ∀ {k : ℕ}, k ≤ N → edist (↑(nearestPt e N) x) x ≤ edist (e k) x
k : ℕ
hk : k ≤ Nat.succ N
⊢ edist (e (if ∀ (k : ℕ), k ≤ N → edist (e (N + 1)) x < edist (e k) x then N + 1 else ↑(nearestPtInd e N) x)) x ≤
    edist (e k) x
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
α : Type u_1
β : Type u_2
ι : Type u_3
E : Type u_4
F : Type u_5
𝕜 : Type u_6
inst✝² : MeasurableSpace α
inst✝¹ : PseudoEMetricSpace α
inst✝ : OpensMeasurableSpace α
e : ℕ → α
x : α
k✝ N✝ : ℕ
hk✝ : k✝ ≤ N✝
N : ℕ
ihN : ∀ {k : ℕ}, k ≤ N → edist (↑(nearestPt e N) x) x ≤ edist (e k) x
k : ℕ
hk : k ≤ Nat.succ N
h : ∀ (k : ℕ), k ≤ N → edist (e (N + 1)) x < edist (e k) x
⊢ edist (e (N + 1)) x ≤ edist (e k) x
[PROOFSTEP]
rcases hk.eq_or_lt with (rfl | hk)
[GOAL]
case pos.inl
α : Type u_1
β : Type u_2
ι : Type u_3
E : Type u_4
F : Type u_5
𝕜 : Type u_6
inst✝² : MeasurableSpace α
inst✝¹ : PseudoEMetricSpace α
inst✝ : OpensMeasurableSpace α
e : ℕ → α
x : α
k N✝ : ℕ
hk✝ : k ≤ N✝
N : ℕ
ihN : ∀ {k : ℕ}, k ≤ N → edist (↑(nearestPt e N) x) x ≤ edist (e k) x
h : ∀ (k : ℕ), k ≤ N → edist (e (N + 1)) x < edist (e k) x
hk : Nat.succ N ≤ Nat.succ N
⊢ edist (e (N + 1)) x ≤ edist (e (Nat.succ N)) x
case pos.inr
α : Type u_1
β : Type u_2
ι : Type u_3
E : Type u_4
F : Type u_5
𝕜 : Type u_6
inst✝² : MeasurableSpace α
inst✝¹ : PseudoEMetricSpace α
inst✝ : OpensMeasurableSpace α
e : ℕ → α
x : α
k✝ N✝ : ℕ
hk✝¹ : k✝ ≤ N✝
N : ℕ
ihN : ∀ {k : ℕ}, k ≤ N → edist (↑(nearestPt e N) x) x ≤ edist (e k) x
k : ℕ
hk✝ : k ≤ Nat.succ N
h : ∀ (k : ℕ), k ≤ N → edist (e (N + 1)) x < edist (e k) x
hk : k < Nat.succ N
⊢ edist (e (N + 1)) x ≤ edist (e k) x
[PROOFSTEP]
exacts [le_rfl, (h k (Nat.lt_succ_iff.1 hk)).le]
[GOAL]
case neg
α : Type u_1
β : Type u_2
ι : Type u_3
E : Type u_4
F : Type u_5
𝕜 : Type u_6
inst✝² : MeasurableSpace α
inst✝¹ : PseudoEMetricSpace α
inst✝ : OpensMeasurableSpace α
e : ℕ → α
x : α
k✝ N✝ : ℕ
hk✝ : k✝ ≤ N✝
N : ℕ
ihN : ∀ {k : ℕ}, k ≤ N → edist (↑(nearestPt e N) x) x ≤ edist (e k) x
k : ℕ
hk : k ≤ Nat.succ N
h : ¬∀ (k : ℕ), k ≤ N → edist (e (N + 1)) x < edist (e k) x
⊢ edist (e (↑(nearestPtInd e N) x)) x ≤ edist (e k) x
[PROOFSTEP]
push_neg at h 
[GOAL]
case neg
α : Type u_1
β : Type u_2
ι : Type u_3
E : Type u_4
F : Type u_5
𝕜 : Type u_6
inst✝² : MeasurableSpace α
inst✝¹ : PseudoEMetricSpace α
inst✝ : OpensMeasurableSpace α
e : ℕ → α
x : α
k✝ N✝ : ℕ
hk✝ : k✝ ≤ N✝
N : ℕ
ihN : ∀ {k : ℕ}, k ≤ N → edist (↑(nearestPt e N) x) x ≤ edist (e k) x
k : ℕ
hk : k ≤ Nat.succ N
h : ∃ k, k ≤ N ∧ edist (e k) x ≤ edist (e (N + 1)) x
⊢ edist (e (↑(nearestPtInd e N) x)) x ≤ edist (e k) x
[PROOFSTEP]
rcases h with ⟨l, hlN, hxl⟩
[GOAL]
case neg.intro.intro
α : Type u_1
β : Type u_2
ι : Type u_3
E : Type u_4
F : Type u_5
𝕜 : Type u_6
inst✝² : MeasurableSpace α
inst✝¹ : PseudoEMetricSpace α
inst✝ : OpensMeasurableSpace α
e : ℕ → α
x : α
k✝ N✝ : ℕ
hk✝ : k✝ ≤ N✝
N : ℕ
ihN : ∀ {k : ℕ}, k ≤ N → edist (↑(nearestPt e N) x) x ≤ edist (e k) x
k : ℕ
hk : k ≤ Nat.succ N
l : ℕ
hlN : l ≤ N
hxl : edist (e l) x ≤ edist (e (N + 1)) x
⊢ edist (e (↑(nearestPtInd e N) x)) x ≤ edist (e k) x
[PROOFSTEP]
rcases hk.eq_or_lt with (rfl | hk)
[GOAL]
case neg.intro.intro.inl
α : Type u_1
β : Type u_2
ι : Type u_3
E : Type u_4
F : Type u_5
𝕜 : Type u_6
inst✝² : MeasurableSpace α
inst✝¹ : PseudoEMetricSpace α
inst✝ : OpensMeasurableSpace α
e : ℕ → α
x : α
k N✝ : ℕ
hk✝ : k ≤ N✝
N : ℕ
ihN : ∀ {k : ℕ}, k ≤ N → edist (↑(nearestPt e N) x) x ≤ edist (e k) x
l : ℕ
hlN : l ≤ N
hxl : edist (e l) x ≤ edist (e (N + 1)) x
hk : Nat.succ N ≤ Nat.succ N
⊢ edist (e (↑(nearestPtInd e N) x)) x ≤ edist (e (Nat.succ N)) x
case neg.intro.intro.inr
α : Type u_1
β : Type u_2
ι : Type u_3
E : Type u_4
F : Type u_5
𝕜 : Type u_6
inst✝² : MeasurableSpace α
inst✝¹ : PseudoEMetricSpace α
inst✝ : OpensMeasurableSpace α
e : ℕ → α
x : α
k✝ N✝ : ℕ
hk✝¹ : k✝ ≤ N✝
N : ℕ
ihN : ∀ {k : ℕ}, k ≤ N → edist (↑(nearestPt e N) x) x ≤ edist (e k) x
k : ℕ
hk✝ : k ≤ Nat.succ N
l : ℕ
hlN : l ≤ N
hxl : edist (e l) x ≤ edist (e (N + 1)) x
hk : k < Nat.succ N
⊢ edist (e (↑(nearestPtInd e N) x)) x ≤ edist (e k) x
[PROOFSTEP]
exacts [(ihN hlN).trans hxl, ihN (Nat.lt_succ_iff.1 hk)]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
E : Type u_4
F : Type u_5
𝕜 : Type u_6
inst✝² : MeasurableSpace α
inst✝¹ : PseudoEMetricSpace α
inst✝ : OpensMeasurableSpace α
e : ℕ → α
x : α
hx : x ∈ closure (Set.range e)
⊢ Tendsto (fun N => ↑(nearestPt e N) x) atTop (𝓝 x)
[PROOFSTEP]
refine' (atTop_basis.tendsto_iff nhds_basis_eball).2 fun ε hε => _
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
E : Type u_4
F : Type u_5
𝕜 : Type u_6
inst✝² : MeasurableSpace α
inst✝¹ : PseudoEMetricSpace α
inst✝ : OpensMeasurableSpace α
e : ℕ → α
x : α
hx : x ∈ closure (Set.range e)
ε : ℝ≥0∞
hε : 0 < ε
⊢ ∃ ia, True ∧ ∀ (x_1 : ℕ), x_1 ∈ Set.Ici ia → ↑(nearestPt e x_1) x ∈ ball x ε
[PROOFSTEP]
rcases EMetric.mem_closure_iff.1 hx ε hε with ⟨_, ⟨N, rfl⟩, hN⟩
[GOAL]
case intro.intro.intro
α : Type u_1
β : Type u_2
ι : Type u_3
E : Type u_4
F : Type u_5
𝕜 : Type u_6
inst✝² : MeasurableSpace α
inst✝¹ : PseudoEMetricSpace α
inst✝ : OpensMeasurableSpace α
e : ℕ → α
x : α
hx : x ∈ closure (Set.range e)
ε : ℝ≥0∞
hε : 0 < ε
N : ℕ
hN : edist x (e N) < ε
⊢ ∃ ia, True ∧ ∀ (x_1 : ℕ), x_1 ∈ Set.Ici ia → ↑(nearestPt e x_1) x ∈ ball x ε
[PROOFSTEP]
rw [edist_comm] at hN 
[GOAL]
case intro.intro.intro
α : Type u_1
β : Type u_2
ι : Type u_3
E : Type u_4
F : Type u_5
𝕜 : Type u_6
inst✝² : MeasurableSpace α
inst✝¹ : PseudoEMetricSpace α
inst✝ : OpensMeasurableSpace α
e : ℕ → α
x : α
hx : x ∈ closure (Set.range e)
ε : ℝ≥0∞
hε : 0 < ε
N : ℕ
hN : edist (e N) x < ε
⊢ ∃ ia, True ∧ ∀ (x_1 : ℕ), x_1 ∈ Set.Ici ia → ↑(nearestPt e x_1) x ∈ ball x ε
[PROOFSTEP]
exact ⟨N, trivial, fun n hn => (edist_nearestPt_le e x hn).trans_lt hN⟩
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
E : Type u_4
F : Type u_5
𝕜 : Type u_6
inst✝⁴ : MeasurableSpace α
inst✝³ : PseudoEMetricSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : MeasurableSpace β
f✝ f : β → α
hf : Measurable f
s : Set α
y₀ : α
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
n : ℕ
x : β
⊢ ↑(approxOn f hf s y₀ h₀ n) x ∈ s
[PROOFSTEP]
haveI : Nonempty s := ⟨⟨y₀, h₀⟩⟩
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
E : Type u_4
F : Type u_5
𝕜 : Type u_6
inst✝⁴ : MeasurableSpace α
inst✝³ : PseudoEMetricSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : MeasurableSpace β
f✝ f : β → α
hf : Measurable f
s : Set α
y₀ : α
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
n : ℕ
x : β
this : Nonempty ↑s
⊢ ↑(approxOn f hf s y₀ h₀ n) x ∈ s
[PROOFSTEP]
suffices ∀ n, (Nat.casesOn n y₀ ((↑) ∘ denseSeq s) : α) ∈ s by apply this
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
E : Type u_4
F : Type u_5
𝕜 : Type u_6
inst✝⁴ : MeasurableSpace α
inst✝³ : PseudoEMetricSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : MeasurableSpace β
f✝ f : β → α
hf : Measurable f
s : Set α
y₀ : α
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
n : ℕ
x : β
this✝ : Nonempty ↑s
this : ∀ (n : ℕ), Nat.casesOn n y₀ (Subtype.val ∘ denseSeq ↑s) ∈ s
⊢ ↑(approxOn f hf s y₀ h₀ n) x ∈ s
[PROOFSTEP]
apply this
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
E : Type u_4
F : Type u_5
𝕜 : Type u_6
inst✝⁴ : MeasurableSpace α
inst✝³ : PseudoEMetricSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : MeasurableSpace β
f✝ f : β → α
hf : Measurable f
s : Set α
y₀ : α
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
n : ℕ
x : β
this : Nonempty ↑s
⊢ ∀ (n : ℕ), Nat.casesOn n y₀ (Subtype.val ∘ denseSeq ↑s) ∈ s
[PROOFSTEP]
rintro (_ | n)
[GOAL]
case zero
α : Type u_1
β : Type u_2
ι : Type u_3
E : Type u_4
F : Type u_5
𝕜 : Type u_6
inst✝⁴ : MeasurableSpace α
inst✝³ : PseudoEMetricSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : MeasurableSpace β
f✝ f : β → α
hf : Measurable f
s : Set α
y₀ : α
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
n : ℕ
x : β
this : Nonempty ↑s
⊢ Nat.casesOn Nat.zero y₀ (Subtype.val ∘ denseSeq ↑s) ∈ s
case succ
α : Type u_1
β : Type u_2
ι : Type u_3
E : Type u_4
F : Type u_5
𝕜 : Type u_6
inst✝⁴ : MeasurableSpace α
inst✝³ : PseudoEMetricSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : MeasurableSpace β
f✝ f : β → α
hf : Measurable f
s : Set α
y₀ : α
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
n✝ : ℕ
x : β
this : Nonempty ↑s
n : ℕ
⊢ Nat.casesOn (Nat.succ n) y₀ (Subtype.val ∘ denseSeq ↑s) ∈ s
[PROOFSTEP]
exacts [h₀, Subtype.mem _]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
E : Type u_4
F : Type u_5
𝕜 : Type u_6
inst✝⁴ : MeasurableSpace α
inst✝³ : PseudoEMetricSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : MeasurableSpace β
f✝ f : β → α
hf : Measurable f
s : Set α
y₀ : α
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
x : β
hx : f x ∈ closure s
⊢ Tendsto (fun n => ↑(approxOn f hf s y₀ h₀ n) x) atTop (𝓝 (f x))
[PROOFSTEP]
haveI : Nonempty s := ⟨⟨y₀, h₀⟩⟩
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
E : Type u_4
F : Type u_5
𝕜 : Type u_6
inst✝⁴ : MeasurableSpace α
inst✝³ : PseudoEMetricSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : MeasurableSpace β
f✝ f : β → α
hf : Measurable f
s : Set α
y₀ : α
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
x : β
hx : f x ∈ closure s
this : Nonempty ↑s
⊢ Tendsto (fun n => ↑(approxOn f hf s y₀ h₀ n) x) atTop (𝓝 (f x))
[PROOFSTEP]
rw [← @Subtype.range_coe _ s, ← image_univ, ← (denseRange_denseSeq s).closure_eq] at hx 
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
E : Type u_4
F : Type u_5
𝕜 : Type u_6
inst✝⁴ : MeasurableSpace α
inst✝³ : PseudoEMetricSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : MeasurableSpace β
f✝ f : β → α
hf : Measurable f
s : Set α
y₀ : α
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
x : β
this : Nonempty ↑s
hx : f x ∈ closure (Subtype.val '' closure (Set.range (denseSeq ↑s)))
⊢ Tendsto (fun n => ↑(approxOn f hf s y₀ h₀ n) x) atTop (𝓝 (f x))
[PROOFSTEP]
simp (config := { iota := false }) only [approxOn, coe_comp]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
E : Type u_4
F : Type u_5
𝕜 : Type u_6
inst✝⁴ : MeasurableSpace α
inst✝³ : PseudoEMetricSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : MeasurableSpace β
f✝ f : β → α
hf : Measurable f
s : Set α
y₀ : α
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
x : β
this : Nonempty ↑s
hx : f x ∈ closure (Subtype.val '' closure (Set.range (denseSeq ↑s)))
⊢ Tendsto (fun n => (↑(nearestPt (fun k => Nat.casesOn k y₀ (Subtype.val ∘ denseSeq ↑s)) n) ∘ f) x) atTop (𝓝 (f x))
[PROOFSTEP]
refine' tendsto_nearestPt (closure_minimal _ isClosed_closure hx)
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
E : Type u_4
F : Type u_5
𝕜 : Type u_6
inst✝⁴ : MeasurableSpace α
inst✝³ : PseudoEMetricSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : MeasurableSpace β
f✝ f : β → α
hf : Measurable f
s : Set α
y₀ : α
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
x : β
this : Nonempty ↑s
hx : f x ∈ closure (Subtype.val '' closure (Set.range (denseSeq ↑s)))
⊢ Subtype.val '' closure (Set.range (denseSeq ↑s)) ⊆
    closure (Set.range fun k => Nat.casesOn k y₀ (Subtype.val ∘ denseSeq ↑s))
[PROOFSTEP]
simp (config := { iota := false }) only [Nat.range_casesOn, closure_union, range_comp]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
E : Type u_4
F : Type u_5
𝕜 : Type u_6
inst✝⁴ : MeasurableSpace α
inst✝³ : PseudoEMetricSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : MeasurableSpace β
f✝ f : β → α
hf : Measurable f
s : Set α
y₀ : α
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
x : β
this : Nonempty ↑s
hx : f x ∈ closure (Subtype.val '' closure (Set.range (denseSeq ↑s)))
⊢ Subtype.val '' closure (Set.range (denseSeq ↑s)) ⊆ closure {y₀} ∪ closure (Subtype.val '' Set.range (denseSeq ↑s))
[PROOFSTEP]
exact Subset.trans (image_closure_subset_closure_image continuous_subtype_val) (subset_union_right _ _)
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
E : Type u_4
F : Type u_5
𝕜 : Type u_6
inst✝⁴ : MeasurableSpace α
inst✝³ : PseudoEMetricSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : MeasurableSpace β
f✝ f : β → α
hf : Measurable f
s : Set α
y₀ : α
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
x : β
m n : ℕ
h : m ≤ n
⊢ edist (↑(approxOn f hf s y₀ h₀ n) x) (f x) ≤ edist (↑(approxOn f hf s y₀ h₀ m) x) (f x)
[PROOFSTEP]
dsimp only [approxOn, coe_comp, Function.comp]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
E : Type u_4
F : Type u_5
𝕜 : Type u_6
inst✝⁴ : MeasurableSpace α
inst✝³ : PseudoEMetricSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : MeasurableSpace β
f✝ f : β → α
hf : Measurable f
s : Set α
y₀ : α
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
x : β
m n : ℕ
h : m ≤ n
⊢ edist (↑(nearestPt (fun k => Nat.rec y₀ (fun n n_ih => ↑(denseSeq (↑s) n)) k) n) (f x)) (f x) ≤
    edist (↑(nearestPt (fun k => Nat.rec y₀ (fun n n_ih => ↑(denseSeq (↑s) n)) k) m) (f x)) (f x)
[PROOFSTEP]
exact edist_nearestPt_le _ _ ((nearestPtInd_le _ _ _).trans h)
