-- Mathlib/Data/Complex/Norm.lean
theorem equiv_limAux (f : CauSeq ℂ (‖·‖)) :
    f ≈ CauSeq.const (‖·‖) (limAux f) := fun ε ε0 ↦
  (exists_forall_ge_and
  (CauSeq.equiv_lim ⟨_, isCauSeq_re f⟩ _ (half_pos ε0))
        (CauSeq.equiv_lim ⟨_, isCauSeq_im f⟩ _ (half_pos ε0))).imp
    fun _ H j ij ↦ by
    obtain ⟨H₁, H₂⟩ := H _ ij
    apply lt_of_le_of_lt (norm_le_abs_re_add_abs_im _)
    dsimp [limAux] at *
    have := add_lt_add H₁ H₂
    rwa [add_halves] at this

Proof state:
case intro
f : CauSeq ℂ fun x => ‖x‖
ε : ℝ
ε0 : ε > 0
x✝ : ℕ
H :
  ∀ j ≥ x✝,
    |↑(⟨fun n => (↑f n).re, ⋯⟩ - CauSeq.const abs (CauSeq.lim ⟨fun n => (↑f n).re, ⋯⟩)) j| < ε / 2 ∧
      |↑(⟨fun n => (↑f n).im, ⋯⟩ - CauSeq.const abs (CauSeq.lim ⟨fun n => (↑f n).im, ⋯⟩)) j| < ε / 2
j : ℕ
ij : j ≥ x✝
H₁ : |↑(⟨fun n => (↑f n).re, ⋯⟩ - CauSeq.const abs (CauSeq.lim ⟨fun n => (↑f n).re, ⋯⟩)) j| < ε / 2
H₂ : |↑(⟨fun n => (↑f n).im, ⋯⟩ - CauSeq.const abs (CauSeq.lim ⟨fun n => (↑f n).im, ⋯⟩)) j| < ε / 2
⊢ (fun x => ‖x‖) (↑(f - CauSeq.const (fun x => ‖x‖) (limAux f)) j) < ε

Tactic:
apply lt_of_le_of_lt (norm_le_abs_re_add_abs_im _)

Result:
case intro
f : CauSeq ℂ fun x => ‖x‖
ε : ℝ
ε0 : ε > 0
x✝ : ℕ
H :
  ∀ j ≥ x✝,
    |↑(⟨fun n => (↑f n).re, ⋯⟩ - CauSeq.const abs (CauSeq.lim ⟨fun n => (↑f n).re, ⋯⟩)) j| < ε / 2 ∧
      |↑(⟨fun n => (↑f n).im, ⋯⟩ - CauSeq.const abs (CauSeq.lim ⟨fun n => (↑f n).im, ⋯⟩)) j| < ε / 2
j : ℕ
ij : j ≥ x✝
H₁ : |↑(⟨fun n => (↑f n).re, ⋯⟩ - CauSeq.const abs (CauSeq.lim ⟨fun n => (↑f n).re, ⋯⟩)) j| < ε / 2
H₂ : |↑(⟨fun n => (↑f n).im, ⋯⟩ - CauSeq.const abs (CauSeq.lim ⟨fun n => (↑f n).im, ⋯⟩)) j| < ε / 2
⊢ |(↑(f - CauSeq.const (fun x => ‖x‖) (limAux f)) j).re| + |(↑(f - CauSeq.const (fun x => ‖x‖) (limAux f)) j).im| < ε

Proof state:
case intro
f : CauSeq ℂ fun x => ‖x‖
ε : ℝ
ε0 : ε > 0
x✝ : ℕ
H :
  ∀ j ≥ x✝,
    |(↑f j).re - CauSeq.lim ⟨fun n => (↑f n).re, ⋯⟩| < ε / 2 ∧ |(↑f j).im - CauSeq.lim ⟨fun n => (↑f n).im, ⋯⟩| < ε / 2
j : ℕ
ij : j ≥ x✝
H₁ : |(↑f j).re - CauSeq.lim ⟨fun n => (↑f n).re, ⋯⟩| < ε / 2
H₂ : |(↑f j).im - CauSeq.lim ⟨fun n => (↑f n).im, ⋯⟩| < ε / 2
⊢ |(↑f j).re - (cauSeqRe f).lim| + |(↑f j).im - (cauSeqIm f).lim| < ε

Tactic:
have := add_lt_add H₁ H₂

Result:
case intro
f : CauSeq ℂ fun x => ‖x‖
ε : ℝ
ε0 : ε > 0
x✝ : ℕ
H :
  ∀ j ≥ x✝,
    |(↑f j).re - CauSeq.lim ⟨fun n => (↑f n).re, ⋯⟩| < ε / 2 ∧ |(↑f j).im - CauSeq.lim ⟨fun n => (↑f n).im, ⋯⟩| < ε / 2
j : ℕ
ij : j ≥ x✝
H₁ : |(↑f j).re - CauSeq.lim ⟨fun n => (↑f n).re, ⋯⟩| < ε / 2
H₂ : |(↑f j).im - CauSeq.lim ⟨fun n => (↑f n).im, ⋯⟩| < ε / 2
this :
  |(↑f j).re - CauSeq.lim ⟨fun n => (↑f n).re, ⋯⟩| + |(↑f j).im - CauSeq.lim ⟨fun n => (↑f n).im, ⋯⟩| < ε / 2 + ε / 2
⊢ |(↑f j).re - (cauSeqRe f).lim| + |(↑f j).im - (cauSeqIm f).lim| < ε

Proof state:
case intro
f : CauSeq ℂ fun x => ‖x‖
ε : ℝ
ε0 : ε > 0
x✝ : ℕ
H :
  ∀ j ≥ x✝,
    |(↑f j).re - CauSeq.lim ⟨fun n => (↑f n).re, ⋯⟩| < ε / 2 ∧ |(↑f j).im - CauSeq.lim ⟨fun n => (↑f n).im, ⋯⟩| < ε / 2
j : ℕ
ij : j ≥ x✝
H₁ : |(↑f j).re - CauSeq.lim ⟨fun n => (↑f n).re, ⋯⟩| < ε / 2
H₂ : |(↑f j).im - CauSeq.lim ⟨fun n => (↑f n).im, ⋯⟩| < ε / 2
this :
  |(↑f j).re - CauSeq.lim ⟨fun n => (↑f n).re, ⋯⟩| + |(↑f j).im - CauSeq.lim ⟨fun n => (↑f n).im, ⋯⟩| < ε / 2 + ε / 2
⊢ |(↑f j).re - (cauSeqRe f).lim| + |(↑f j).im - (cauSeqIm f).lim| < ε

Tactic:
rwa [add_halves] at this

Result:
no goals

Proof state:
case intro
f : CauSeq ℂ fun x => ‖x‖
ε : ℝ
ε0 : ε > 0
x✝ : ℕ
H :
  ∀ j ≥ x✝,
    |↑(⟨fun n => (↑f n).re, ⋯⟩ - CauSeq.const abs (CauSeq.lim ⟨fun n => (↑f n).re, ⋯⟩)) j| < ε / 2 ∧
      |↑(⟨fun n => (↑f n).im, ⋯⟩ - CauSeq.const abs (CauSeq.lim ⟨fun n => (↑f n).im, ⋯⟩)) j| < ε / 2
j : ℕ
ij : j ≥ x✝
H₁ : |↑(⟨fun n => (↑f n).re, ⋯⟩ - CauSeq.const abs (CauSeq.lim ⟨fun n => (↑f n).re, ⋯⟩)) j| < ε / 2
H₂ : |↑(⟨fun n => (↑f n).im, ⋯⟩ - CauSeq.const abs (CauSeq.lim ⟨fun n => (↑f n).im, ⋯⟩)) j| < ε / 2
⊢ |(↑(f - CauSeq.const (fun x => ‖x‖) (limAux f)) j).re| + |(↑(f - CauSeq.const (fun x => ‖x‖) (limAux f)) j).im| < ε

Tactic:
dsimp [limAux] at *

Result:
case intro
f : CauSeq ℂ fun x => ‖x‖
ε : ℝ
ε0 : ε > 0
x✝ : ℕ
H :
  ∀ j ≥ x✝,
    |(↑f j).re - CauSeq.lim ⟨fun n => (↑f n).re, ⋯⟩| < ε / 2 ∧ |(↑f j).im - CauSeq.lim ⟨fun n => (↑f n).im, ⋯⟩| < ε / 2
j : ℕ
ij : j ≥ x✝
H₁ : |(↑f j).re - CauSeq.lim ⟨fun n => (↑f n).re, ⋯⟩| < ε / 2
H₂ : |(↑f j).im - CauSeq.lim ⟨fun n => (↑f n).im, ⋯⟩| < ε / 2
⊢ |(↑f j).re - (cauSeqRe f).lim| + |(↑f j).im - (cauSeqIm f).lim| < ε

Proof state:
f : CauSeq ℂ fun x => ‖x‖
ε : ℝ
ε0 : ε > 0
x✝ : ℕ
H :
  ∀ j ≥ x✝,
    |↑(⟨fun n => (↑f n).re, ⋯⟩ - CauSeq.const abs (CauSeq.lim ⟨fun n => (↑f n).re, ⋯⟩)) j| < ε / 2 ∧
      |↑(⟨fun n => (↑f n).im, ⋯⟩ - CauSeq.const abs (CauSeq.lim ⟨fun n => (↑f n).im, ⋯⟩)) j| < ε / 2
j : ℕ
ij : j ≥ x✝
⊢ (fun x => ‖x‖) (↑(f - CauSeq.const (fun x => ‖x‖) (limAux f)) j) < ε

Tactic:
obtain ⟨H₁, H₂⟩ := H _ ij

Result:
case intro
f : CauSeq ℂ fun x => ‖x‖
ε : ℝ
ε0 : ε > 0
x✝ : ℕ
H :
  ∀ j ≥ x✝,
    |↑(⟨fun n => (↑f n).re, ⋯⟩ - CauSeq.const abs (CauSeq.lim ⟨fun n => (↑f n).re, ⋯⟩)) j| < ε / 2 ∧
      |↑(⟨fun n => (↑f n).im, ⋯⟩ - CauSeq.const abs (CauSeq.lim ⟨fun n => (↑f n).im, ⋯⟩)) j| < ε / 2
j : ℕ
ij : j ≥ x✝
H₁ : |↑(⟨fun n => (↑f n).re, ⋯⟩ - CauSeq.const abs (CauSeq.lim ⟨fun n => (↑f n).re, ⋯⟩)) j| < ε / 2
H₂ : |↑(⟨fun n => (↑f n).im, ⋯⟩ - CauSeq.const abs (CauSeq.lim ⟨fun n => (↑f n).im, ⋯⟩)) j| < ε / 2
⊢ (fun x => ‖x‖) (↑(f - CauSeq.const (fun x => ‖x‖) (limAux f)) j) < ε