awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDense
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : PseudoEMetricSpace α
inst_2 : OpensMeasurableSpace α
e : ℕ → α
x : α
N : ℕ
ihN : ∀ {k : ℕ} (hk : k ≤ N), edist ((nearestPt e N : (a : α) → α) x) x ≤ edist (e k) x
k : ℕ
hk : k ≤ N + 1
l : ℕ
hlN : l ≤ N
hxl : edist (e l) x ≤ edist (e (N + 1)) x
neg : ∀ (hk : N + 1 ≤ N + 1), edist (e ((nearestPtInd e N : (a : α) → ℕ) x)) x ≤ edist (e (N + 1)) x
neg₁ : ∀ (hk : k < N + 1), edist (e ((nearestPtInd e N : (a : α) → ℕ) x)) x ≤ edist (e k) x
⊢ edist (e ((nearestPtInd e N : (a : α) → ℕ) x)) x ≤ edist (e k) x

Tactic:
rcases hk.eq_or_lt with (rfl | hk)

Premises used: LE.le.eq_or_lt, rfl
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDense
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : PseudoEMetricSpace α
inst_2 : OpensMeasurableSpace α
e : ℕ → α
x : α
N : ℕ
ihN : ∀ {k : ℕ} (hk : k ≤ N), edist ((nearestPt e N : (a : α) → α) x) x ≤ edist (e k) x
l : ℕ
hlN : l ≤ N
hxl : edist (e l) x ≤ edist (e (N + 1)) x
hk : N + 1 ≤ N + 1
⊢ edist (e ((nearestPtInd e N : (a : α) → ℕ) x)) x ≤ edist (e (N + 1)) x

Tactic:
(ihN hlN).trans hxl

Premises used: LE.le.trans
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDense
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : PseudoEMetricSpace α
inst_2 : OpensMeasurableSpace α
e : ℕ → α
x : α
N : ℕ
ihN : ∀ {k : ℕ} (hk : k ≤ N), edist ((nearestPt e N : (a : α) → α) x) x ≤ edist (e k) x
k : ℕ
hk_1 : k ≤ N + 1
l : ℕ
hlN : l ≤ N
hxl : edist (e l) x ≤ edist (e (N + 1)) x
hk : k < N + 1
⊢ edist (e ((nearestPtInd e N : (a : α) → ℕ) x)) x ≤ edist (e k) x

Tactic:
ihN (Nat.lt_succ_iff.1 hk)

Premises used: Nat.lt_succ_iff, Iff.mp
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDense
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : PseudoEMetricSpace α
inst_2 : OpensMeasurableSpace α
e : ℕ → α
x : α
N : ℕ
ihN : ∀ {k : ℕ} (hk : k ≤ N), edist ((nearestPt e N : (a : α) → α) x) x ≤ edist (e k) x
l : ℕ
hlN : l ≤ N
hxl : edist (e l) x ≤ edist (e (N + 1)) x
hk : N + 1 ≤ N + 1
⊢ edist (e ((nearestPtInd e N : (a : α) → ℕ) x)) x ≤ edist (e (N + 1)) x

Tactic:
exacts [(ihN hlN).trans hxl, ihN (Nat.lt_succ_iff.1 hk)]

Premises used: Nat.lt_succ_iff, Iff.mp, LE.le.trans
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDense
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : PseudoEMetricSpace α
inst_2 : OpensMeasurableSpace α
e : ℕ → α
x : α
k N : ℕ
hk : k ≤ N
zero : ∀ {k : ℕ} (hk : k ≤ 0), edist ((nearestPt e 0 : (a : α) → α) x) x ≤ edist (e k) x
succ :
  ∀ (N : ℕ) (ihN : ∀ {k : ℕ} (hk : k ≤ N), edist ((nearestPt e N : (a : α) → α) x) x ≤ edist (e k) x) {k : ℕ}
    (hk : k ≤ N + 1), edist ((nearestPt e (N + 1) : (a : α) → α) x) x ≤ edist (e k) x
⊢ edist ((nearestPt e N : (a : α) → α) x) x ≤ edist (e k) x

Tactic:
induction N generalizing k with
  | zero => simp [nonpos_iff_eq_zero.1 hk]
  | succ N ihN =>
    simp only [nearestPt, nearestPtInd_succ, map_apply]
    split_ifs with h
    · rcases hk.eq_or_lt with (rfl | hk)
      exacts [le_rfl, (h k (Nat.lt_succ_iff.1 hk)).le]
    · push Not at h
      rcases h with ⟨l, hlN, hxl⟩
      rcases hk.eq_or_lt with (rfl | hk)
      exacts [(ihN hlN).trans hxl, ihN (Nat.lt_succ_iff.1 hk)]

Premises used: LE.le.eq_or_lt, le_rfl, MeasureTheory.SimpleFunc.nearestPtInd_succ, MeasureTheory.SimpleFunc.nearestPt, Iff.mp, MeasureTheory.SimpleFunc.map_apply, Not, rfl, nonpos_iff_eq_zero
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDense
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : PseudoEMetricSpace α
inst_2 : OpensMeasurableSpace α
e : ℕ → α
x : α
hx : x ∈ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (range e)
⊢ Tendsto (fun (N : ℕ) ↦ (nearestPt e N : (a : α) → α) x) atTop (𝓝 x)

Tactic:
(atTop_basis.tendsto_iff nhds_basis_eball).2 fun ε hε => ?_

Premises used: Iff.mpr, Filter.atTop_basis, Filter.HasBasis.tendsto_iff, Metric.nhds_basis_eball
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDense
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : PseudoEMetricSpace α
inst_2 : OpensMeasurableSpace α
e : ℕ → α
x : α
hx : x ∈ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (range e)
refine :
  ∀ (ε : ℝ≥0∞) (hε : 0 < ε),
    ∃ (ia : ℕ), True ∧ ∀ x_1 ∈ Ici ia, Membership.mem (α := α) (eball x ε) ((nearestPt e x_1 : (a : α) → α) x : α)
⊢ Tendsto (fun (N : ℕ) ↦ (nearestPt e N : (a : α) → α) x) atTop (𝓝 x)

Tactic:
refine (atTop_basis.tendsto_iff nhds_basis_eball).2 fun ε hε => ?_

Premises used: Iff.mpr, Filter.atTop_basis, Filter.HasBasis.tendsto_iff, Metric.nhds_basis_eball
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDense
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : PseudoEMetricSpace α
inst_2 : OpensMeasurableSpace α
e : ℕ → α
x : α
hx : x ∈ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (range e)
ε : ℝ≥0∞
hε : 0 < ε
rcases :
  ∀ (N : ℕ) (hN : edist x (e N) < ε),
    ∃ (ia : ℕ), True ∧ ∀ x_1 ∈ Ici ia, Membership.mem (α := α) (eball x ε) ((nearestPt e x_1 : (a : α) → α) x : α)
⊢ ∃ (ia : ℕ), True ∧ ∀ x_1 ∈ Ici ia, Membership.mem (α := α) (eball x ε) ((nearestPt e x_1 : (a : α) → α) x : α)

Tactic:
rcases EMetric.mem_closure_iff.1 hx ε hε with ⟨_, ⟨N, rfl⟩, hN⟩

Premises used: Iff.mp, EMetric.mem_closure_iff, rfl
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDense
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : PseudoEMetricSpace α
inst_2 : OpensMeasurableSpace α
e : ℕ → α
x : α
hx : x ∈ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (range e)
ε : ℝ≥0∞
hε : 0 < ε
N : ℕ
hN : edist x (e N) < ε
⊢ edist (e N) x < ε

Tactic:
rw [edist_comm] at hN

Premises used: PseudoEMetricSpace.edist_comm
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDense
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : PseudoEMetricSpace α
inst_2 : OpensMeasurableSpace α
e : ℕ → α
x : α
hx : x ∈ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (range e)
ε : ℝ≥0∞
hε : 0 < ε
N : ℕ
hN : edist (e N) x < ε
⊢ ∃ (ia : ℕ), True ∧ ∀ x_1 ∈ Ici ia, Membership.mem (α := α) (eball x ε) ((nearestPt e x_1 : (a : α) → α) x : α)

Tactic:
⟨N, trivial, fun n hn => (edist_nearestPt_le e x hn).trans_lt hN⟩

Premises used: trivial, And.intro, Exists.intro, MeasureTheory.SimpleFunc.edist_nearestPt_le, LE.le.trans_lt
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDense
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : PseudoEMetricSpace α
inst_2 : OpensMeasurableSpace α
e : ℕ → α
x : α
hx : x ∈ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (range e)
ε : ℝ≥0∞
hε : 0 < ε
N : ℕ
hN : edist (e N) x < ε
⊢ ∃ (ia : ℕ), True ∧ ∀ x_1 ∈ Ici ia, Membership.mem (α := α) (eball x ε) ((nearestPt e x_1 : (a : α) → α) x : α)

Tactic:
exact ⟨N, trivial, fun n hn => (edist_nearestPt_le e x hn).trans_lt hN⟩
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDense
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : PseudoEMetricSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : MeasurableSpace β
f : β → α
hf : Measurable f
s : Set α
y₀ : α
h₀ : y₀ ∈ s
inst_4 : SeparableSpace.{u_1} (↑s : Type u_1)
x : β
⊢ (approxOn f hf s y₀ h₀ 0 : (a : β) → α) x = y₀

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDense
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : PseudoEMetricSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : MeasurableSpace β
f : β → α
hf : Measurable f
s : Set α
y₀ : α
h₀ : y₀ ∈ s
inst_4 : SeparableSpace.{u_1} (↑s : Type u_1)
n : ℕ
x : β
⊢ Nonempty.{u_1 + 1} (↑s : Type u_1)

Tactic:
haveI : Nonempty s := ⟨⟨y₀, h₀⟩⟩
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDense
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : PseudoEMetricSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : MeasurableSpace β
f : β → α
hf : Measurable f
s : Set α
y₀ : α
h₀ : y₀ ∈ s
inst_4 : SeparableSpace.{u_1} (↑s : Type u_1)
n : ℕ
x : β
this_1 : Nonempty.{u_1 + 1} (↑s : Type u_1)
this :
  ∀ (n : ℕ),
    Membership.mem (α := α) s
      (Nat.casesOn (motive := fun (x : ℕ) ↦ α) n y₀
          (Function.comp (β := (↑s : Type u_1)) (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (denseSeq (↑s : Type u_1))) :
        α)
⊢ Membership.mem (α := α) s ((approxOn f hf s y₀ h₀ n : (a : β) → α) x : α)

Tactic:
apply this
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDense
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : PseudoEMetricSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : MeasurableSpace β
f : β → α
hf : Measurable f
s : Set α
y₀ : α
h₀ : y₀ ∈ s
inst_4 : SeparableSpace.{u_1} (↑s : Type u_1)
n : ℕ
x : β
this : Nonempty.{u_1 + 1} (↑s : Type u_1)
suffices :
  ∀ (n : ℕ),
    Membership.mem (α := α) s
      (Nat.casesOn (motive := fun (x : ℕ) ↦ α) n y₀
          (Function.comp (β := (↑s : Type u_1)) (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (denseSeq (↑s : Type u_1))) :
        α)
⊢ Membership.mem (α := α) s ((approxOn f hf s y₀ h₀ n : (a : β) → α) x : α)

Tactic:
suffices ∀ n, (Nat.casesOn n y₀ ((↑) ∘ denseSeq s) : α) ∈ s by apply this
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDense
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : PseudoEMetricSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : MeasurableSpace β
f : β → α
hf : Measurable f
s : Set α
y₀ : α
h₀ : y₀ ∈ s
inst_4 : SeparableSpace.{u_1} (↑s : Type u_1)
n : ℕ
x : β
this : Nonempty.{u_1 + 1} (↑s : Type u_1)
⊢ Membership.mem (α := α) s
    (Nat.casesOn (motive := fun (x : ℕ) ↦ α) 0 y₀
        (Function.comp (β := (↑s : Type u_1)) (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (denseSeq (↑s : Type u_1))) :
      α)

Tactic:
h₀

Premises used: Set.Mem
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDense
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : PseudoEMetricSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : MeasurableSpace β
f : β → α
hf : Measurable f
s : Set α
y₀ : α
h₀ : y₀ ∈ s
inst_4 : SeparableSpace.{u_1} (↑s : Type u_1)
n_1 : ℕ
x : β
this : Nonempty.{u_1 + 1} (↑s : Type u_1)
n : ℕ
⊢ Membership.mem (α := α) s
    (Nat.casesOn (motive := fun (x : ℕ) ↦ α) (n + 1) y₀
        (Function.comp (β := (↑s : Type u_1)) (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (denseSeq (↑s : Type u_1))) :
      α)

Tactic:
Subtype.mem _

Premises used: Set.Mem, Subtype.mem
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDense
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : PseudoEMetricSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : MeasurableSpace β
f : β → α
hf : Measurable f
s : Set α
y₀ : α
h₀ : y₀ ∈ s
inst_4 : SeparableSpace.{u_1} (↑s : Type u_1)
n : ℕ
x : β
this : Nonempty.{u_1 + 1} (↑s : Type u_1)
⊢ Membership.mem (α := α) s
    (Nat.casesOn (motive := fun (x : ℕ) ↦ α) 0 y₀
        (Function.comp (β := (↑s : Type u_1)) (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (denseSeq (↑s : Type u_1))) :
      α)

Tactic:
exacts [h₀, Subtype.mem _]

Premises used: Subtype.mem
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDense
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : PseudoEMetricSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : MeasurableSpace β
f_1 : β → α
inst_4 : Zero α
inst_5 : Preorder α
f : β → α
hf : 0 ≤ f
hfm : Measurable f
inst_6 : SeparableSpace.{u_1} (↑(range f ∪ {0}) : Type u_1)
n : ℕ
⊢ 0 ∈ range f ∪ {0}

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDense
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : PseudoEMetricSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : MeasurableSpace β
inst_4 : Zero α
inst_5 : Preorder α
f : β → α
hf : 0 ≤ f
hfm : Measurable f
inst_6 : SeparableSpace.{u_1} (↑(range f ∪ {0}) : Type u_1)
n : ℕ
simp : range f ⊆ Ici 0
⊢ range f ∪ {0} ⊆ Ici 0

Tactic:
simp only [Set.union_singleton, Set.insert_subset_iff, Set.mem_Ici, le_refl, true_and]

Premises used: le_refl, Set.insert_subset_iff, Set.mem_Ici, Set.union_singleton, true_and
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDense
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : PseudoEMetricSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : MeasurableSpace β
inst_4 : Zero α
inst_5 : Preorder α
f : β → α
hf : 0 ≤ f
hfm : Measurable f
inst_6 : SeparableSpace.{u_1} (↑(range f ∪ {0}) : Type u_1)
n : ℕ
x : β
⊢ Membership.mem (γ := Set α) (Ici 0) (f x)

Tactic:
hf x

Premises used: Set.Ici, Set.Mem, setOf
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDense
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : PseudoEMetricSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : MeasurableSpace β
inst_4 : Zero α
inst_5 : Preorder α
f : β → α
hf : 0 ≤ f
hfm : Measurable f
inst_6 : SeparableSpace.{u_1} (↑(range f ∪ {0}) : Type u_1)
n : ℕ
x : β
⊢ Membership.mem (γ := Set α) (Ici 0) (f x)

Tactic:
exact hf x
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDense
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : PseudoEMetricSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : MeasurableSpace β
inst_4 : Zero α
inst_5 : Preorder α
f : β → α
hf : 0 ≤ f
hfm : Measurable f
inst_6 : SeparableSpace.{u_1} (↑(range f ∪ {0}) : Type u_1)
n : ℕ
⊢ range f ∪ {0} ⊆ Ici 0

Tactic:
have : range f ∪ {0} ⊆ Set.Ici 0 := by
    simp only [Set.union_singleton, Set.insert_subset_iff, Set.mem_Ici, le_refl, true_and]
    rintro - ⟨x, rfl⟩
    exact hf x
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDense
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : PseudoEMetricSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : MeasurableSpace β
inst_4 : Zero α
inst_5 : Preorder α
f : β → α
hf : 0 ≤ f
hfm : Measurable f
inst_6 : SeparableSpace.{u_1} (↑(range f ∪ {0}) : Type u_1)
n : ℕ
this : range f ∪ {0} ⊆ Ici 0
⊢ 0 ≤ approxOn f hfm (range f ∪ {0}) 0 ⋯ n

Tactic:
fun _ ↦ this <| approxOn_mem ..

Premises used: Set.Ici, Set.Mem, setOf, MeasureTheory.SimpleFunc.approxOn_mem, MeasureTheory.SimpleFunc.approxOn_range_nonneg._proof_1
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDense
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : PseudoEMetricSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : MeasurableSpace β
inst_4 : Zero α
inst_5 : Preorder α
f : β → α
hf : 0 ≤ f
hfm : Measurable f
inst_6 : SeparableSpace.{u_1} (↑(range f ∪ {0}) : Type u_1)
n : ℕ
this : range f ∪ {0} ⊆ Ici 0
⊢ 0 ≤ approxOn f hfm (range f ∪ {0}) 0 ⋯ n

Tactic:
exact fun _ ↦ this <| approxOn_mem ..

Premises used: MeasureTheory.SimpleFunc.approxOn_mem
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDense
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : PseudoEMetricSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : MeasurableSpace β
γ : Type u_3
inst_4 : MeasurableSpace γ
f : β → α
hf : Measurable f
g : γ → β
hg : Measurable g
s : Set α
y₀ : α
h₀ : y₀ ∈ s
inst_5 : SeparableSpace.{u_1} (↑s : Type u_1)
n : ℕ
⊢ approxOn (f ∘ g) ⋯ s y₀ h₀ n = (approxOn f hf s y₀ h₀ n).comp g hg

Tactic:
rfl

Premises used: MeasureTheory.SimpleFunc.nearestPt, MeasureTheory.SimpleFunc.approxOn, MeasureTheory.SimpleFunc.bind, MeasureTheory.SimpleFunc.comp, rfl, MeasureTheory.SimpleFunc.map
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDense
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : PseudoEMetricSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : MeasurableSpace β
f : β → α
hf : Measurable f
s : Set α
y₀ : α
h₀ : y₀ ∈ s
inst_4 : SeparableSpace.{u_1} (↑s : Type u_1)
x : β
hx : f x ∈ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ Nonempty.{u_1 + 1} (↑s : Type u_1)

Tactic:
haveI : Nonempty s := ⟨⟨y₀, h₀⟩⟩
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDense
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : PseudoEMetricSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : MeasurableSpace β
f : β → α
hf : Measurable f
s : Set α
y₀ : α
h₀ : y₀ ∈ s
inst_4 : SeparableSpace.{u_1} (↑s : Type u_1)
x : β
hx : f x ∈ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s
this : Nonempty.{u_1 + 1} (↑s : Type u_1)
⊢ Nonempty.{u_1 + 1} (↑s : Type u_1)

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

Premises used: Set.image_univ, TopologicalSpace.denseRange_denseSeq, Set.Elem, Dense.closure_eq, Subtype.range_coe
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDense
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : PseudoEMetricSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : MeasurableSpace β
f : β → α
hf : Measurable f
s : Set α
y₀ : α
h₀ : y₀ ∈ s
inst_4 : SeparableSpace.{u_1} (↑s : Type u_1)
x : β
hx : f x ∈ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s
this this₁ : Nonempty.{u_1 + 1} (↑s : Type u_1)
⊢ Membership.mem (γ := Set α)
    (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace]
      (image (α := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s))
        (closure[instTopologicalSpaceSubtype] (range (denseSeq (↑s : Type u_1))))))
    (f x)

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

Premises used: Set.image_univ, TopologicalSpace.denseRange_denseSeq, Set.Elem, Dense.closure_eq, Subtype.range_coe
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDense
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : PseudoEMetricSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : MeasurableSpace β
f : β → α
hf : Measurable f
s : Set α
y₀ : α
h₀ : y₀ ∈ s
inst_4 : SeparableSpace.{u_1} (↑s : Type u_1)
x : β
this : Nonempty.{u_1 + 1} (↑s : Type u_1)
hx :
  Membership.mem (γ := Set α)
    (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace]
      (image (α := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s))
        (closure[instTopologicalSpaceSubtype] (range (denseSeq (↑s : Type u_1))))))
    (f x)
simp :
  Tendsto
    (fun (n : ℕ) ↦
      ((⇑(nearestPt
                (fun (k : ℕ) ↦
                  Nat.casesOn (motive := fun (x : ℕ) ↦ α) k y₀
                    (Function.comp (β := (↑s : Type u_1)) (Subtype.val (p := fun (x : α) ↦ x ∈ s))
                      (denseSeq (↑s : Type u_1))))
                n) :
            (a : α) → α) ∘
          f)
        x)
    atTop (𝓝 (f x))
⊢ Tendsto (fun (n : ℕ) ↦ (approxOn f hf s y₀ h₀ n : (a : β) → α) x) atTop (𝓝 (f x))

Tactic:
simp -iota only [approxOn, coe_comp]

Premises used: MeasureTheory.SimpleFunc.coe_comp, MeasureTheory.SimpleFunc.approxOn
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDense
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : PseudoEMetricSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : MeasurableSpace β
f : β → α
hf : Measurable f
s : Set α
y₀ : α
h₀ : y₀ ∈ s
inst_4 : SeparableSpace.{u_1} (↑s : Type u_1)
x : β
this : Nonempty.{u_1 + 1} (↑s : Type u_1)
hx :
  Membership.mem (γ := Set α)
    (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace]
      (image (α := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s))
        (closure[instTopologicalSpaceSubtype] (range (denseSeq (↑s : Type u_1))))))
    (f x)
⊢ Tendsto
    (fun (n : ℕ) ↦
      ((⇑(nearestPt
                (fun (k : ℕ) ↦
                  Nat.casesOn (motive := fun (x : ℕ) ↦ α) k y₀
                    (Function.comp (β := (↑s : Type u_1)) (Subtype.val (p := fun (x : α) ↦ x ∈ s))
                      (denseSeq (↑s : Type u_1))))
                n) :
            (a : α) → α) ∘
          f)
        x)
    atTop (𝓝 (f x))

Tactic:
tendsto_nearestPt (closure_minimal ?_ isClosed_closure hx)

Premises used: closure_minimal, MeasureTheory.SimpleFunc.tendsto_nearestPt, isClosed_closure
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDense
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : PseudoEMetricSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : MeasurableSpace β
f : β → α
hf : Measurable f
s : Set α
y₀ : α
h₀ : y₀ ∈ s
inst_4 : SeparableSpace.{u_1} (↑s : Type u_1)
x : β
this : Nonempty.{u_1 + 1} (↑s : Type u_1)
hx :
  Membership.mem (γ := Set α)
    (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace]
      (image (α := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s))
        (closure[instTopologicalSpaceSubtype] (range (denseSeq (↑s : Type u_1))))))
    (f x)
refine :
  Subset.{u_1} (α := Set α)
    (image (α := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s))
      (closure[instTopologicalSpaceSubtype] (range (denseSeq (↑s : Type u_1)))))
    (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace]
      (range fun (k : ℕ) ↦
        Nat.casesOn (motive := fun (x : ℕ) ↦ α) k y₀
          (Function.comp (β := (↑s : Type u_1)) (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (denseSeq (↑s : Type u_1)))))
⊢ Tendsto
    (fun (n : ℕ) ↦
      ((⇑(nearestPt
                (fun (k : ℕ) ↦
                  Nat.casesOn (motive := fun (x : ℕ) ↦ α) k y₀
                    (Function.comp (β := (↑s : Type u_1)) (Subtype.val (p := fun (x : α) ↦ x ∈ s))
                      (denseSeq (↑s : Type u_1))))
                n) :
            (a : α) → α) ∘
          f)
        x)
    atTop (𝓝 (f x))

Tactic:
refine tendsto_nearestPt (closure_minimal ?_ isClosed_closure hx)

Premises used: closure_minimal, MeasureTheory.SimpleFunc.tendsto_nearestPt, isClosed_closure
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDense
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : PseudoEMetricSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : MeasurableSpace β
f : β → α
hf : Measurable f
s : Set α
y₀ : α
h₀ : y₀ ∈ s
inst_4 : SeparableSpace.{u_1} (↑s : Type u_1)
x : β
this : Nonempty.{u_1 + 1} (↑s : Type u_1)
hx :
  Membership.mem (γ := Set α)
    (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace]
      (image (α := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s))
        (closure[instTopologicalSpaceSubtype] (range (denseSeq (↑s : Type u_1))))))
    (f x)
simp :
  Subset (α := Set α)
    (image (α := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s))
      (closure[instTopologicalSpaceSubtype] (range (denseSeq (↑s : Type u_1)))))
    (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] {y₀} ∪
      closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace]
        (image (α := (↑s : Type u_1)) (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (range (denseSeq (↑s : Type u_1)))))
⊢ Subset.{u_1} (α := Set α)
    (image (α := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s))
      (closure[instTopologicalSpaceSubtype] (range (denseSeq (↑s : Type u_1)))))
    (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace]
      (range fun (k : ℕ) ↦
        Nat.casesOn (motive := fun (x : ℕ) ↦ α) k y₀
          (Function.comp (β := (↑s : Type u_1)) (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (denseSeq (↑s : Type u_1)))))

Tactic:
simp -iota only [Nat.range_casesOn, closure_union, range_comp]

Premises used: Set.range_comp, closure_union, Nat.range_casesOn
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDense
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : PseudoEMetricSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : MeasurableSpace β
f : β → α
hf : Measurable f
s : Set α
y₀ : α
h₀ : y₀ ∈ s
inst_4 : SeparableSpace.{u_1} (↑s : Type u_1)
x : β
this : Nonempty.{u_1 + 1} (↑s : Type u_1)
hx :
  Membership.mem (γ := Set α)
    (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace]
      (image (α := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s))
        (closure[instTopologicalSpaceSubtype] (range (denseSeq (↑s : Type u_1))))))
    (f x)
⊢ Subset (α := Set α)
    (image (α := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s))
      (closure[instTopologicalSpaceSubtype] (range (denseSeq (↑s : Type u_1)))))
    (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] {y₀} ∪
      closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace]
        (image (α := (↑s : Type u_1)) (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (range (denseSeq (↑s : Type u_1)))))

Tactic:
Subset.trans (image_closure_subset_closure_image continuous_subtype_val)
      subset_union_right

Premises used: continuous_subtype_val, Set.Subset.trans, Set.subset_union_right, image_closure_subset_closure_image