Simplify dist def for sequence_tendsto

Stream: general

[ZHAO Jinxiang]

import data.real.basic
import topology.metric_space.basic

def sequence_tendsto (a : ℕ → ℝ) (t : ℝ) :=
∀ ε > 0, ∃ N , ∀ n, N ≤ n → |a n - t| < ε

def sequence_tendsto₁ (a : ℕ → ℝ) (t : ℝ) :=
∀ ε > 0, ∃ N , ∀ n, N ≤ n → dist t (a n) < ε
example : sequence_tendsto = sequence_tendsto₁ := begin
  ext a t,
  unfold sequence_tendsto sequence_tendsto₁ dist,
  -- Help me here: code below are too redundant
  split,
  {
    intros h a b,
    specialize h a b,
    cases h with N h,
    use N,
    intros n hn,
    specialize h n hn,
    rw <-abs_neg,
    simp,
    assumption,
  },
  {
    intros h a b,
    specialize h a b,
    cases h with N h,
    use N,
    intros n hn,
    specialize h n hn,
    rw <-abs_neg,
    simp,
    assumption,
  }
end

code are too redundant, can you simplify it?

[FR]

import data.real.basic
import topology.metric_space.basic

def sequence_tendsto (a : ℕ → ℝ) (t : ℝ) :=
∀ ε > 0, ∃ N, ∀ n, N ≤ n → |a n - t| < ε

def sequence_tendsto₁ (a : ℕ → ℝ) (t : ℝ) :=
∀ ε > 0, ∃ N, ∀ n, N ≤ n → dist t (a n) < ε

example : sequence_tendsto = sequence_tendsto₁ :=
begin
  ext a t,
  unfold sequence_tendsto sequence_tendsto₁ dist,
  simp_rw abs_sub_comm,
end