simp only [Real.norm_eq_abs, Complex.abs_abs, one_div, mul_inv_rev, norm_mul,
  norm_inv, norm_pow, eventually_principal, mem_setOf_eq, and_imp] at hc
case calc_2.e_a.e_a.intro
ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 ψ
ψpos : ∀ (x : ℝ), 0 ≤ ψ x
suppΨ : support ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, ψ x / x = 1
X : ℝ
X_pos : 0 < X
ε : ℝ
εpos : 0 < ε
c : ℝ
hc : ∀ᶠ (x : ℂ) in 𝓟 {s | 2 ≤ s.re ∧ s.re ≤ 2}, ‖‖𝓜 (fun x => ↑(Smooth1 ψ ε x)) x‖‖ ≤ c * ‖1 / (ε * ‖x‖ ^ 2)‖
⊢ ∫ (t : ℝ), ∑' (n : ℕ), ↑(Λ n) / ↑n ^ (2 + ↑t * I) * 𝓜 (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * ↑X ^ (2 + ↑t * I) =
    ∑' (n : ℕ), ∫ (t : ℝ), ↑(Λ n) / ↑n ^ (2 + ↑t * I) * 𝓜 (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * ↑X ^ (2 + ↑t * I)
case calc_2.e_a.e_a.intro
ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 ψ
ψpos : ∀ (x : ℝ), 0 ≤ ψ x
suppΨ : support ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, ψ x / x = 1
X : ℝ
X_pos : 0 < X
ε : ℝ
εpos : 0 < ε
c : ℝ
hc : ∀ (x : ℂ), 2 ≤ x.re → x.re ≤ 2 → |‖𝓜 (fun x => ↑(Smooth1 ψ ε x)) x‖| ≤ c * ((|‖x‖| ^ 2)⁻¹ * |ε|⁻¹)
⊢ ∫ (t : ℝ), ∑' (n : ℕ), ↑(Λ n) / ↑n ^ (2 + ↑t * I) * 𝓜 (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * ↑X ^ (2 + ↑t * I) =
    ∑' (n : ℕ), ∫ (t : ℝ), ↑(Λ n) / ↑n ^ (2 + ↑t * I) * 𝓜 (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * ↑X ^ (2 + ↑t * I)