-- Mathlib/MeasureTheory/Function/SimpleFuncDense.lean
theorem tendsto_approxOn {f : β → α} (hf : Measurable f) {s : Set α} {y₀ : α} (h₀ : y₀ ∈ s)
    [SeparableSpace s] {x : β} (hx : f x ∈ closure s) :
    Tendsto (fun n => approxOn f hf s y₀ h₀ n x) atTop (𝓝 <| f x)

Proof state:
α : Type u_1
β : Type u_2
inst✝⁴ : MeasurableSpace α
inst✝³ : PseudoEMetricSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : MeasurableSpace β
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))

Tactic:
simp (config := { iota := false }) only [approxOn, coe_comp]

Result:
α : Type u_1
β : Type u_2
inst✝⁴ : MeasurableSpace α
inst✝³ : PseudoEMetricSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : MeasurableSpace β
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))

Proof state:
α : Type u_1
β : Type u_2
inst✝⁴ : MeasurableSpace α
inst✝³ : PseudoEMetricSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : MeasurableSpace β
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))

Tactic:
haveI : Nonempty s := ⟨⟨y₀, h₀⟩⟩

Result:
α : Type u_1
β : Type u_2
inst✝⁴ : MeasurableSpace α
inst✝³ : PseudoEMetricSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : MeasurableSpace β
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))

Proof state:
α : Type u_1
β : Type u_2
inst✝⁴ : MeasurableSpace α
inst✝³ : PseudoEMetricSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : MeasurableSpace β
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))

Tactic:
refine tendsto_nearestPt (closure_minimal ?_ isClosed_closure hx)

Result:
α : Type u_1
β : Type u_2
inst✝⁴ : MeasurableSpace α
inst✝³ : PseudoEMetricSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : MeasurableSpace β
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))

Proof state:
α : Type u_1
β : Type u_2
inst✝⁴ : MeasurableSpace α
inst✝³ : PseudoEMetricSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : MeasurableSpace β
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))

Tactic:
simp (config := { iota := false }) only [Nat.range_casesOn, closure_union, range_comp]

Result:
α : Type u_1
β : Type u_2
inst✝⁴ : MeasurableSpace α
inst✝³ : PseudoEMetricSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : MeasurableSpace β
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))

Proof state:
α : Type u_1
β : Type u_2
inst✝⁴ : MeasurableSpace α
inst✝³ : PseudoEMetricSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : MeasurableSpace β
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))

Tactic:
exact
  Subset.trans (image_closure_subset_closure_image continuous_subtype_val)
    subset_union_right

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝⁴ : MeasurableSpace α
inst✝³ : PseudoEMetricSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : MeasurableSpace β
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))

Tactic:
rw [← @Subtype.range_coe _ s, ← image_univ, ← (denseRange_denseSeq s).closure_eq] at hx

Result:
α : Type u_1
β : Type u_2
inst✝⁴ : MeasurableSpace α
inst✝³ : PseudoEMetricSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : MeasurableSpace β
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))