case zero
α : Type u_1
β : Type ?u.23173
ι : Type ?u.23176
E : Type ?u.23179
F : Type ?u.23182
𝕜 : Type ?u.23185
inst✝² : MeasurableSpace α
inst✝¹ : PseudoEMetricSpace α
inst✝ : OpensMeasurableSpace α
e : ℕ → α
x : α
⊢ ↑(nearestPtInd e Nat.zero) x ≤ Nat.zero

case succ
α : Type u_1
β : Type ?u.23173
ι : Type ?u.23176
E : Type ?u.23179
F : Type ?u.23182
𝕜 : Type ?u.23185
inst✝² : MeasurableSpace α
inst✝¹ : PseudoEMetricSpace α
inst✝ : OpensMeasurableSpace α
e : ℕ → α
x : α
N : ℕ
ihN : ↑(nearestPtInd e N) x ≤ N
⊢ ↑(nearestPtInd e (Nat.succ N)) x ≤ Nat.succ N
α : Type u_1
β : Type ?u.23173
ι : Type ?u.23176
E : Type ?u.23179
F : Type ?u.23182
𝕜 : Type ?u.23185
inst✝² : MeasurableSpace α
inst✝¹ : PseudoEMetricSpace α
inst✝ : OpensMeasurableSpace α
e : ℕ → α
N : ℕ
x : α
⊢ ↑(nearestPtInd e N) x ≤ N
induction' N with N ihN
case succ
α : Type u_1
β : Type ?u.23173
ι : Type ?u.23176
E : Type ?u.23179
F : Type ?u.23182
𝕜 : Type ?u.23185
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
case succ
α : Type u_1
β : Type ?u.23173
ι : Type ?u.23176
E : Type ?u.23179
F : Type ?u.23182
𝕜 : Type ?u.23185
inst✝² : MeasurableSpace α
inst✝¹ : PseudoEMetricSpace α
inst✝ : OpensMeasurableSpace α
e : ℕ → α
x : α
N : ℕ
ihN : ↑(nearestPtInd e N) x ≤ N
⊢ ↑(nearestPtInd e (Nat.succ N)) x ≤ Nat.succ N
simp only [nearestPtInd_succ]
case succ.inl
α : Type u_1
β : Type ?u.23173
ι : Type ?u.23176
E : Type ?u.23179
F : Type ?u.23182
𝕜 : Type ?u.23185
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 succ.inr
α : Type u_1
β : Type ?u.23173
ι : Type ?u.23176
E : Type ?u.23179
F : Type ?u.23182
𝕜 : Type ?u.23185
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
case succ
α : Type u_1
β : Type ?u.23173
ι : Type ?u.23176
E : Type ?u.23179
F : Type ?u.23182
𝕜 : Type ?u.23185
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
split_ifs
no goals
case succ.inl
α : Type u_1
β : Type ?u.23173
ι : Type ?u.23176
E : Type ?u.23179
F : Type ?u.23182
𝕜 : Type ?u.23185
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 succ.inr
α : Type u_1
β : Type ?u.23173
ι : Type ?u.23176
E : Type ?u.23179
F : Type ?u.23182
𝕜 : Type ?u.23185
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
exacts [le_rfl, ihN.trans N.le_succ]
no goals
case zero
α : Type u_1
β : Type ?u.23173
ι : Type ?u.23176
E : Type ?u.23179
F : Type ?u.23182
𝕜 : Type ?u.23185
inst✝² : MeasurableSpace α
inst✝¹ : PseudoEMetricSpace α
inst✝ : OpensMeasurableSpace α
e : ℕ → α
x : α
⊢ ↑(nearestPtInd e Nat.zero) x ≤ Nat.zero
simp