cases hf (ε₀ / 2) (half_pos hε₀) with
| intro Nf hNf =>
  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
f f' g g' : CauchySeq
hf : f ≈ f'
hg : g ≈ g'
ε₀ : ℚ
hε₀ : ε₀ > 0
⊢ ∃ N, ∀ (m : ℕ), N ≤ m → |seqOf (f + g) m - seqOf (f' + g') m| < ε₀
no goals