cases hg (ε₀ / 2) (half_pos hε₀) with
| intro Ng hNg =>
  apply Exists.intro (max Nf Ng)
  intro m hm
  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
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
⊢ ∃ N, ∀ (m : ℕ), N ≤ m → |seqOf (f + g) m - seqOf (f' + g') m| < ε₀
no goals