-- Mathlib/MeasureTheory/Function/SimpleFuncDense.lean
theorem edist_nearestPt_le (e : ℕ → α) (x : α) {k N : ℕ} (hk : k ≤ N) :
    edist (nearestPt e N x) x ≤ edist (e k) x

Proof state:
case pos
α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : PseudoEMetricSpace α
inst✝ : OpensMeasurableSpace α
e : ℕ → α
x : α
N : ℕ
ihN : ∀ {k : ℕ}, k ≤ N → edist ((nearestPt e N) x) x ≤ edist (e k) x
k : ℕ
hk : k ≤ N + 1
h : ∀ k ≤ N, edist (e (N + 1)) x < edist (e k) x
⊢ edist (e (N + 1)) x ≤ edist (e k) x

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

Result:
case pos.inl
α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : PseudoEMetricSpace α
inst✝ : OpensMeasurableSpace α
e : ℕ → α
x : α
N : ℕ
ihN : ∀ {k : ℕ}, k ≤ N → edist ((nearestPt e N) x) x ≤ edist (e k) x
h : ∀ k ≤ N, edist (e (N + 1)) x < edist (e k) x
hk : N + 1 ≤ N + 1
⊢ edist (e (N + 1)) x ≤ edist (e (N + 1)) x

case pos.inr
α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : PseudoEMetricSpace α
inst✝ : OpensMeasurableSpace α
e : ℕ → α
x : α
N : ℕ
ihN : ∀ {k : ℕ}, k ≤ N → edist ((nearestPt e N) x) x ≤ edist (e k) x
k : ℕ
hk✝ : k ≤ N + 1
h : ∀ k ≤ N, edist (e (N + 1)) x < edist (e k) x
hk : k < N + 1
⊢ edist (e (N + 1)) x ≤ edist (e k) x

Proof state:
case neg.intro.intro.inl
α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : PseudoEMetricSpace α
inst✝ : OpensMeasurableSpace α
e : ℕ → α
x : α
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 : N + 1 ≤ N + 1
⊢ edist (e ((nearestPtInd e N) x)) x ≤ edist (e (N + 1)) x

case neg.intro.intro.inr
α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : PseudoEMetricSpace α
inst✝ : OpensMeasurableSpace α
e : ℕ → α
x : α
N : ℕ
ihN : ∀ {k : ℕ}, k ≤ N → edist ((nearestPt e N) 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
hk : k < N + 1
⊢ edist (e ((nearestPtInd e N) x)) x ≤ edist (e k) x

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

Result:
no goals

Proof state:
case zero
α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : PseudoEMetricSpace α
inst✝ : OpensMeasurableSpace α
e : ℕ → α
x : α
k : ℕ
hk : k ≤ 0
⊢ edist ((nearestPt e 0) x) x ≤ edist (e k) x

Tactic:
simp [nonpos_iff_eq_zero.1 hk, le_refl]

Result:
no goals

Proof state:
case succ
α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : PseudoEMetricSpace α
inst✝ : OpensMeasurableSpace α
e : ℕ → α
x : α
N : ℕ
ihN : ∀ {k : ℕ}, k ≤ N → edist ((nearestPt e N) x) x ≤ edist (e k) x
k : ℕ
hk : k ≤ N + 1
⊢ edist ((nearestPt e (N + 1)) x) x ≤ edist (e k) x

Tactic:
simp only [nearestPt, nearestPtInd_succ, map_apply]

Result:
case succ
α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : PseudoEMetricSpace α
inst✝ : OpensMeasurableSpace α
e : ℕ → α
x : α
N : ℕ
ihN : ∀ {k : ℕ}, k ≤ N → edist ((nearestPt e N) x) x ≤ edist (e k) x
k : ℕ
hk : k ≤ N + 1
⊢ edist (e (if ∀ k ≤ N, edist (e (N + 1)) x < edist (e k) x then N + 1 else (nearestPtInd e N) x)) x ≤ edist (e k) x

Proof state:
α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : PseudoEMetricSpace α
inst✝ : OpensMeasurableSpace α
e : ℕ → α
x : α
k N : ℕ
hk : k ≤ N
⊢ edist ((nearestPt e N) x) x ≤ edist (e k) x

Tactic:
induction' N with N ihN generalizing k

Result:
case zero
α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : PseudoEMetricSpace α
inst✝ : OpensMeasurableSpace α
e : ℕ → α
x : α
k : ℕ
hk : k ≤ 0
⊢ edist ((nearestPt e 0) x) x ≤ edist (e k) x

case succ
α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : PseudoEMetricSpace α
inst✝ : OpensMeasurableSpace α
e : ℕ → α
x : α
N : ℕ
ihN : ∀ {k : ℕ}, k ≤ N → edist ((nearestPt e N) x) x ≤ edist (e k) x
k : ℕ
hk : k ≤ N + 1
⊢ edist ((nearestPt e (N + 1)) x) x ≤ edist (e k) x

Proof state:
case neg
α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : PseudoEMetricSpace α
inst✝ : OpensMeasurableSpace α
e : ℕ → α
x : α
N : ℕ
ihN : ∀ {k : ℕ}, k ≤ N → edist ((nearestPt e N) x) x ≤ edist (e k) x
k : ℕ
hk : k ≤ N + 1
h : ∃ k ≤ N, edist (e k) x ≤ edist (e (N + 1)) x
⊢ edist (e ((nearestPtInd e N) x)) x ≤ edist (e k) x

Tactic:
rcases h with ⟨l, hlN, hxl⟩

Result:
case neg.intro.intro
α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : PseudoEMetricSpace α
inst✝ : OpensMeasurableSpace α
e : ℕ → α
x : α
N : ℕ
ihN : ∀ {k : ℕ}, k ≤ N → edist ((nearestPt e N) 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
⊢ edist (e ((nearestPtInd e N) x)) x ≤ edist (e k) x

Proof state:
case neg
α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : PseudoEMetricSpace α
inst✝ : OpensMeasurableSpace α
e : ℕ → α
x : α
N : ℕ
ihN : ∀ {k : ℕ}, k ≤ N → edist ((nearestPt e N) x) x ≤ edist (e k) x
k : ℕ
hk : k ≤ N + 1
h : ¬∀ k ≤ N, edist (e (N + 1)) x < edist (e k) x
⊢ edist (e ((nearestPtInd e N) x)) x ≤ edist (e k) x

Tactic:
push_neg at h

Result:
case neg
α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : PseudoEMetricSpace α
inst✝ : OpensMeasurableSpace α
e : ℕ → α
x : α
N : ℕ
ihN : ∀ {k : ℕ}, k ≤ N → edist ((nearestPt e N) x) x ≤ edist (e k) x
k : ℕ
hk : k ≤ N + 1
h : ∃ k ≤ N, edist (e k) x ≤ edist (e (N + 1)) x
⊢ edist (e ((nearestPtInd e N) x)) x ≤ edist (e k) x

Proof state:
case succ
α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : PseudoEMetricSpace α
inst✝ : OpensMeasurableSpace α
e : ℕ → α
x : α
N : ℕ
ihN : ∀ {k : ℕ}, k ≤ N → edist ((nearestPt e N) x) x ≤ edist (e k) x
k : ℕ
hk : k ≤ N + 1
⊢ edist (e (if ∀ k ≤ N, edist (e (N + 1)) x < edist (e k) x then N + 1 else (nearestPtInd e N) x)) x ≤ edist (e k) x

Tactic:
split_ifs with h

Result:
case pos
α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : PseudoEMetricSpace α
inst✝ : OpensMeasurableSpace α
e : ℕ → α
x : α
N : ℕ
ihN : ∀ {k : ℕ}, k ≤ N → edist ((nearestPt e N) x) x ≤ edist (e k) x
k : ℕ
hk : k ≤ N + 1
h : ∀ k ≤ N, edist (e (N + 1)) x < edist (e k) x
⊢ edist (e (N + 1)) x ≤ edist (e k) x

case neg
α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : PseudoEMetricSpace α
inst✝ : OpensMeasurableSpace α
e : ℕ → α
x : α
N : ℕ
ihN : ∀ {k : ℕ}, k ≤ N → edist ((nearestPt e N) x) x ≤ edist (e k) x
k : ℕ
hk : k ≤ N + 1
h : ¬∀ k ≤ N, edist (e (N + 1)) x < edist (e k) x
⊢ edist (e ((nearestPtInd e N) x)) x ≤ edist (e k) x

Proof state:
case neg.intro.intro
α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : PseudoEMetricSpace α
inst✝ : OpensMeasurableSpace α
e : ℕ → α
x : α
N : ℕ
ihN : ∀ {k : ℕ}, k ≤ N → edist ((nearestPt e N) 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
⊢ edist (e ((nearestPtInd e N) x)) x ≤ edist (e k) x

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

Result:
case neg.intro.intro.inl
α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : PseudoEMetricSpace α
inst✝ : OpensMeasurableSpace α
e : ℕ → α
x : α
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 : N + 1 ≤ N + 1
⊢ edist (e ((nearestPtInd e N) x)) x ≤ edist (e (N + 1)) x

case neg.intro.intro.inr
α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : PseudoEMetricSpace α
inst✝ : OpensMeasurableSpace α
e : ℕ → α
x : α
N : ℕ
ihN : ∀ {k : ℕ}, k ≤ N → edist ((nearestPt e N) 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
hk : k < N + 1
⊢ edist (e ((nearestPtInd e N) x)) x ≤ edist (e k) x