[GOAL]
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : ι → α → β
μ : Measure α
p : α → (ι → β) → Prop
hf : ∀ (i : ι), AEMeasurable (f i)
x : α
hx : x ∈ aeSeqSet hf p
i : ι
⊢ aeSeqSet hf p ⊆ {x | ∀ (i : ι), f i x = AEMeasurable.mk (f i) (_ : AEMeasurable (f i)) x}
[PROOFSTEP]
rw [aeSeqSet, ← compl_compl {x | ∀ i, f i x = (hf i).mk (f i) x}, Set.compl_subset_compl]
[GOAL]
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : ι → α → β
μ : Measure α
p : α → (ι → β) → Prop
hf : ∀ (i : ι), AEMeasurable (f i)
x : α
hx : x ∈ aeSeqSet hf p
i : ι
⊢ {x | ∀ (i : ι), f i x = AEMeasurable.mk (f i) (_ : AEMeasurable (f i)) x}ᶜ ⊆
    toMeasurable μ {x | (∀ (i : ι), f i x = AEMeasurable.mk (f i) (_ : AEMeasurable (f i)) x) ∧ p x fun n => f n x}ᶜ
[PROOFSTEP]
refine' Set.Subset.trans (Set.compl_subset_compl.mpr fun x h => _) (subset_toMeasurable _ _)
[GOAL]
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : ι → α → β
μ : Measure α
p : α → (ι → β) → Prop
hf : ∀ (i : ι), AEMeasurable (f i)
x✝ : α
hx : x✝ ∈ aeSeqSet hf p
i : ι
x : α
h : x ∈ {x | (∀ (i : ι), f i x = AEMeasurable.mk (f i) (_ : AEMeasurable (f i)) x) ∧ p x fun n => f n x}
⊢ x ∈ {x | ∀ (i : ι), f i x = AEMeasurable.mk (f i) (_ : AEMeasurable (f i)) x}
[PROOFSTEP]
exact h.1
[GOAL]
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : ι → α → β
μ : Measure α
p : α → (ι → β) → Prop
hf : ∀ (i : ι), AEMeasurable (f i)
x : α
hx : x ∈ aeSeqSet hf p
i : ι
⊢ aeSeq hf p i x = AEMeasurable.mk (f i) (_ : AEMeasurable (f i)) x
[PROOFSTEP]
simp only [aeSeq, hx, if_true]
[GOAL]
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : ι → α → β
μ : Measure α
p : α → (ι → β) → Prop
hf : ∀ (i : ι), AEMeasurable (f i)
x : α
hx : x ∈ aeSeqSet hf p
i : ι
⊢ aeSeq hf p i x = f i x
[PROOFSTEP]
simp only [aeSeq_eq_mk_of_mem_aeSeqSet hf hx i, mk_eq_fun_of_mem_aeSeqSet hf hx i]
[GOAL]
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : ι → α → β
μ : Measure α
p : α → (ι → β) → Prop
hf : ∀ (i : ι), AEMeasurable (f i)
x : α
hx : x ∈ aeSeqSet hf p
⊢ p x fun n => aeSeq hf p n x
[PROOFSTEP]
simp only [aeSeq, hx, if_true]
[GOAL]
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : ι → α → β
μ : Measure α
p : α → (ι → β) → Prop
hf : ∀ (i : ι), AEMeasurable (f i)
x : α
hx : x ∈ aeSeqSet hf p
⊢ p x fun n => AEMeasurable.mk (f n) (_ : AEMeasurable (f n)) x
[PROOFSTEP]
rw [funext fun n => mk_eq_fun_of_mem_aeSeqSet hf hx n]
[GOAL]
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : ι → α → β
μ : Measure α
p : α → (ι → β) → Prop
hf : ∀ (i : ι), AEMeasurable (f i)
x : α
hx : x ∈ aeSeqSet hf p
⊢ p x fun n => f n x
[PROOFSTEP]
have h_ss : aeSeqSet hf p ⊆ {x | p x fun n => f n x} :=
  by
  rw [← compl_compl {x | p x fun n => f n x}, aeSeqSet, Set.compl_subset_compl]
  refine' Set.Subset.trans (Set.compl_subset_compl.mpr _) (subset_toMeasurable _ _)
  exact fun x hx => hx.2
[GOAL]
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : ι → α → β
μ : Measure α
p : α → (ι → β) → Prop
hf : ∀ (i : ι), AEMeasurable (f i)
x : α
hx : x ∈ aeSeqSet hf p
⊢ aeSeqSet hf p ⊆ {x | p x fun n => f n x}
[PROOFSTEP]
rw [← compl_compl {x | p x fun n => f n x}, aeSeqSet, Set.compl_subset_compl]
[GOAL]
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : ι → α → β
μ : Measure α
p : α → (ι → β) → Prop
hf : ∀ (i : ι), AEMeasurable (f i)
x : α
hx : x ∈ aeSeqSet hf p
⊢ {x | p x fun n => f n x}ᶜ ⊆
    toMeasurable μ {x | (∀ (i : ι), f i x = AEMeasurable.mk (f i) (_ : AEMeasurable (f i)) x) ∧ p x fun n => f n x}ᶜ
[PROOFSTEP]
refine' Set.Subset.trans (Set.compl_subset_compl.mpr _) (subset_toMeasurable _ _)
[GOAL]
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : ι → α → β
μ : Measure α
p : α → (ι → β) → Prop
hf : ∀ (i : ι), AEMeasurable (f i)
x : α
hx : x ∈ aeSeqSet hf p
⊢ {x | (∀ (i : ι), f i x = AEMeasurable.mk (f i) (_ : AEMeasurable (f i)) x) ∧ p x fun n => f n x} ⊆
    {x | p x fun n => f n x}
[PROOFSTEP]
exact fun x hx => hx.2
[GOAL]
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : ι → α → β
μ : Measure α
p : α → (ι → β) → Prop
hf : ∀ (i : ι), AEMeasurable (f i)
x : α
hx : x ∈ aeSeqSet hf p
h_ss : aeSeqSet hf p ⊆ {x | p x fun n => f n x}
⊢ p x fun n => f n x
[PROOFSTEP]
have hx' := Set.mem_of_subset_of_mem h_ss hx
[GOAL]
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : ι → α → β
μ : Measure α
p : α → (ι → β) → Prop
hf : ∀ (i : ι), AEMeasurable (f i)
x : α
hx : x ∈ aeSeqSet hf p
h_ss : aeSeqSet hf p ⊆ {x | p x fun n => f n x}
hx' : x ∈ {x | p x fun n => f n x}
⊢ p x fun n => f n x
[PROOFSTEP]
exact hx'
[GOAL]
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : ι → α → β
μ : Measure α
p : α → (ι → β) → Prop
hf : ∀ (i : ι), AEMeasurable (f i)
x : α
hx : x ∈ aeSeqSet hf p
⊢ p x fun n => f n x
[PROOFSTEP]
have h_eq : (fun n => f n x) = fun n => aeSeq hf p n x := funext fun n => (aeSeq_eq_fun_of_mem_aeSeqSet hf hx n).symm
[GOAL]
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : ι → α → β
μ : Measure α
p : α → (ι → β) → Prop
hf : ∀ (i : ι), AEMeasurable (f i)
x : α
hx : x ∈ aeSeqSet hf p
h_eq : (fun n => f n x) = fun n => aeSeq hf p n x
⊢ p x fun n => f n x
[PROOFSTEP]
rw [h_eq]
[GOAL]
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : ι → α → β
μ : Measure α
p : α → (ι → β) → Prop
hf : ∀ (i : ι), AEMeasurable (f i)
x : α
hx : x ∈ aeSeqSet hf p
h_eq : (fun n => f n x) = fun n => aeSeq hf p n x
⊢ p x fun n => aeSeq hf p n x
[PROOFSTEP]
exact prop_of_mem_aeSeqSet hf hx
[GOAL]
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
f : ι → α → β
μ : Measure α
p : α → (ι → β) → Prop
inst✝ : Countable ι
hf : ∀ (i : ι), AEMeasurable (f i)
hp : ∀ᵐ (x : α) ∂μ, p x fun n => f n x
⊢ ↑↑μ (aeSeqSet hf p)ᶜ = 0
[PROOFSTEP]
rw [aeSeqSet, compl_compl, measure_toMeasurable]
[GOAL]
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
f : ι → α → β
μ : Measure α
p : α → (ι → β) → Prop
inst✝ : Countable ι
hf : ∀ (i : ι), AEMeasurable (f i)
hp : ∀ᵐ (x : α) ∂μ, p x fun n => f n x
⊢ ↑↑μ {x | (∀ (i : ι), f i x = AEMeasurable.mk (f i) (_ : AEMeasurable (f i)) x) ∧ p x fun n => f n x}ᶜ = 0
[PROOFSTEP]
have hf_eq := fun i => (hf i).ae_eq_mk
[GOAL]
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
f : ι → α → β
μ : Measure α
p : α → (ι → β) → Prop
inst✝ : Countable ι
hf : ∀ (i : ι), AEMeasurable (f i)
hp : ∀ᵐ (x : α) ∂μ, p x fun n => f n x
hf_eq : ∀ (i : ι), f i =ᵐ[μ] AEMeasurable.mk (f i) (_ : AEMeasurable (f i))
⊢ ↑↑μ {x | (∀ (i : ι), f i x = AEMeasurable.mk (f i) (_ : AEMeasurable (f i)) x) ∧ p x fun n => f n x}ᶜ = 0
[PROOFSTEP]
simp_rw [Filter.EventuallyEq, ← ae_all_iff] at hf_eq
[GOAL]
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
f : ι → α → β
μ : Measure α
p : α → (ι → β) → Prop
inst✝ : Countable ι
hf : ∀ (i : ι), AEMeasurable (f i)
hp : ∀ᵐ (x : α) ∂μ, p x fun n => f n x
hf_eq : ∀ᵐ (a : α) ∂μ, ∀ (i : ι), f i a = AEMeasurable.mk (f i) (_ : AEMeasurable (f i)) a
⊢ ↑↑μ {x | (∀ (i : ι), f i x = AEMeasurable.mk (f i) (_ : AEMeasurable (f i)) x) ∧ p x fun n => f n x}ᶜ = 0
[PROOFSTEP]
exact Filter.Eventually.and hf_eq hp
[GOAL]
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
f : ι → α → β
μ : Measure α
p : α → (ι → β) → Prop
inst✝ : Countable ι
hf : ∀ (i : ι), AEMeasurable (f i)
hp : ∀ᵐ (x : α) ∂μ, p x fun n => f n x
x : α
hx : x ∈ aeSeqSet hf p
i : ι
⊢ aeSeq hf p i x = AEMeasurable.mk (f i) (_ : AEMeasurable (f i)) x
[PROOFSTEP]
simp only [aeSeq, hx, if_true]
[GOAL]
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
f : ι → α → β
μ : Measure α
p : α → (ι → β) → Prop
inst✝¹ : CompleteLattice β
inst✝ : Countable ι
hf : ∀ (i : ι), AEMeasurable (f i)
hp : ∀ᵐ (x : α) ∂μ, p x fun n => f n x
⊢ ⨆ (n : ι), aeSeq hf p n =ᵐ[μ] ⨆ (n : ι), f n
[PROOFSTEP]
simp_rw [Filter.EventuallyEq, ae_iff, iSup_apply]
[GOAL]
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
f : ι → α → β
μ : Measure α
p : α → (ι → β) → Prop
inst✝¹ : CompleteLattice β
inst✝ : Countable ι
hf : ∀ (i : ι), AEMeasurable (f i)
hp : ∀ᵐ (x : α) ∂μ, p x fun n => f n x
⊢ ↑↑μ {a | ¬⨆ (i : ι), aeSeq hf p i a = ⨆ (i : ι), f i a} = 0
[PROOFSTEP]
have h_ss : aeSeqSet hf p ⊆ {a : α | ⨆ i : ι, aeSeq hf p i a = ⨆ i : ι, f i a} :=
  by
  intro x hx
  congr
  exact funext fun i => aeSeq_eq_fun_of_mem_aeSeqSet hf hx i
[GOAL]
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
f : ι → α → β
μ : Measure α
p : α → (ι → β) → Prop
inst✝¹ : CompleteLattice β
inst✝ : Countable ι
hf : ∀ (i : ι), AEMeasurable (f i)
hp : ∀ᵐ (x : α) ∂μ, p x fun n => f n x
⊢ aeSeqSet hf p ⊆ {a | ⨆ (i : ι), aeSeq hf p i a = ⨆ (i : ι), f i a}
[PROOFSTEP]
intro x hx
[GOAL]
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
f : ι → α → β
μ : Measure α
p : α → (ι → β) → Prop
inst✝¹ : CompleteLattice β
inst✝ : Countable ι
hf : ∀ (i : ι), AEMeasurable (f i)
hp : ∀ᵐ (x : α) ∂μ, p x fun n => f n x
x : α
hx : x ∈ aeSeqSet hf p
⊢ x ∈ {a | ⨆ (i : ι), aeSeq hf p i a = ⨆ (i : ι), f i a}
[PROOFSTEP]
congr
[GOAL]
case e_s
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
f : ι → α → β
μ : Measure α
p : α → (ι → β) → Prop
inst✝¹ : CompleteLattice β
inst✝ : Countable ι
hf : ∀ (i : ι), AEMeasurable (f i)
hp : ∀ᵐ (x : α) ∂μ, p x fun n => f n x
x : α
hx : x ∈ aeSeqSet hf p
⊢ (fun i => aeSeq hf p i x) = fun i => f i x
[PROOFSTEP]
exact funext fun i => aeSeq_eq_fun_of_mem_aeSeqSet hf hx i
[GOAL]
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
f : ι → α → β
μ : Measure α
p : α → (ι → β) → Prop
inst✝¹ : CompleteLattice β
inst✝ : Countable ι
hf : ∀ (i : ι), AEMeasurable (f i)
hp : ∀ᵐ (x : α) ∂μ, p x fun n => f n x
h_ss : aeSeqSet hf p ⊆ {a | ⨆ (i : ι), aeSeq hf p i a = ⨆ (i : ι), f i a}
⊢ ↑↑μ {a | ¬⨆ (i : ι), aeSeq hf p i a = ⨆ (i : ι), f i a} = 0
[PROOFSTEP]
exact measure_mono_null (Set.compl_subset_compl.mpr h_ss) (measure_compl_aeSeqSet_eq_zero hf hp)


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