apply Exists.intro (max Nf Ng)
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
⊢ ∃ N, ∀ (m : ℕ), N ≤ m → |seqOf (f + g) m - seqOf (f' + g') m| < ε₀
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 : ℕ), max Nf Ng ≤ m → |seqOf (f + g) m - seqOf (f' + g') m| < ε₀