have h (n : ℕ) (t : ℝ) : ((n : ℂ) / X) ^ ((-1 : ℂ) * (2 + t * I)) =
    ((n / X) ^ (-1 : ℂ)) ^ (2 + ↑t * I) := by
  rw [cpow_mul] <;> {rw [this n]; simp [Real.pi_pos, Real.pi_nonneg]}
case calc_6
ψ : ℝ → ℝ
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 < ε
ht : ∀ (t : ℝ), -(2 + ↑t * I) = -1 * (2 + ↑t * I)
hn : ∀ (n : ℂ), (n / ↑X) ^ (-1) = ↑X / n
this : ∀ (n : ℕ), ((↑n / ↑X).log * -1).im = 0
⊢ ∑' (n : ℕ),
      ↑(Λ n) * (1 / (2 * ↑π) * ∫ (t : ℝ), mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * (↑X / ↑n) ^ (2 + ↑t * I)) =
    ∑' (n : ℕ),
      ↑(Λ n) * (1 / (2 * ↑π) * ∫ (t : ℝ), mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * (↑n / ↑X) ^ (-(2 + ↑t * I)))
case calc_6
ψ : ℝ → ℝ
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 < ε
ht : ∀ (t : ℝ), -(2 + ↑t * I) = -1 * (2 + ↑t * I)
hn : ∀ (n : ℂ), (n / ↑X) ^ (-1) = ↑X / n
this : ∀ (n : ℕ), ((↑n / ↑X).log * -1).im = 0
h : ∀ (n : ℕ) (t : ℝ), (↑n / ↑X) ^ (-1 * (2 + ↑t * I)) = ((↑n / ↑X) ^ (-1)) ^ (2 + ↑t * I)
⊢ ∑' (n : ℕ),
      ↑(Λ n) * (1 / (2 * ↑π) * ∫ (t : ℝ), mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * (↑X / ↑n) ^ (2 + ↑t * I)) =
    ∑' (n : ℕ),
      ↑(Λ n) * (1 / (2 * ↑π) * ∫ (t : ℝ), mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * (↑n / ↑X) ^ (-(2 + ↑t * I)))