calc
  abs (seqOf (f + g) m - seqOf (f' + g') m)
  = abs ((seqOf f m + seqOf g m)
    - (seqOf f' m + seqOf g' m)) :=
    by rfl
  _ = abs ((seqOf f m - seqOf f' m)
      + (seqOf g m - seqOf g' m)) :=
    by
      have arg_eq :
        seqOf f m + seqOf g m
          - (seqOf f' m + seqOf g' m) =
        seqOf f m - seqOf f' m
          + (seqOf g m - seqOf g' m) :=
        by linarith
      rw [arg_eq]
  _ ≤ abs (seqOf f m - seqOf f' m)
      + abs (seqOf g m - seqOf g' m) :=
    by apply abs_add
  _ < ε₀ / 2 + ε₀ / 2 :=
    add_lt_add (hNf m (le_of_max_le_left hm))
      (hNg m (le_of_max_le_right hm))
  _ = ε₀ :=
    by simp
case intro.intro
f f' g g' : CauchySeq
hf : f ≈ f'
hg : g ≈ g'
ε₀ : ℚ
hε₀ : ε₀ > 0
Nf : ℕ
hNf : ∀ (m : ℕ), m ≥ Nf → |seqOf f m - seqOf f' m| < ε₀ / 2
Ng : ℕ
hNg : ∀ (m : ℕ), m ≥ Ng → |seqOf g m - seqOf g' m| < ε₀ / 2
m : ℕ
hm : max Nf Ng ≤ m
⊢ |seqOf (f + g) m - seqOf (f' + g') m| < ε₀
no goals