α : Type u_1
β : Type ?u.11058
ι : Type ?u.11061
E : Type ?u.11064
F : Type ?u.11067
𝕜 : Type ?u.11070
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
α : Type u_1
β : Type ?u.11058
ι : Type ?u.11061
E : Type ?u.11064
F : Type ?u.11067
𝕜 : Type ?u.11070
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
simp only [nearestPtInd, coe_piecewise, Set.piecewise]
case e_c
α : Type u_1
β : Type ?u.11058
ι : Type ?u.11061
E : Type ?u.11064
F : Type ?u.11067
𝕜 : Type ?u.11070
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
α : Type u_1
β : Type ?u.11058
ι : Type ?u.11061
E : Type ?u.11064
F : Type ?u.11067
𝕜 : Type ?u.11070
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
congr
no goals
case e_c
α : Type u_1
β : Type ?u.11058
ι : Type ?u.11061
E : Type ?u.11064
F : Type ?u.11067
𝕜 : Type ?u.11070
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
simp