Theorem: SmoothedChebyshevDirichlet
Proof state before:
ψ : ℝ → ℝ
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 < ε
⊢ 1 / (2 * ↑π * I) *
      (I *
        ∫ (t : ℝ),
          -deriv riemannZeta (2 + ↑t * I) / riemannZeta (2 + ↑t * I) * mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) *
            ↑X ^ (2 + ↑t * I)) =
    ↑(∑' (n : ℕ), Λ n * Smooth1 ψ ε (↑n / X))
Tactic:
calc
  _ = 1 / (2 * π * I) * (I * ∫ (t : ℝ), ∑' n, Λ n / (n : ℂ) ^ (2 + ↑t * I) *
    mellin (fun x ↦ ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * X ^ (2 + ↑t * I)) := ?_
  _ = 1 / (2 * π * I) * (I * ∑' n, ∫ (t : ℝ), Λ n / (n : ℂ) ^ (2 + ↑t * I) *
    mellin (fun x ↦ ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * X ^ (2 + ↑t * I)) := ?_
  _ = 1 / (2 * π * I) * (I * ∑' n, Λ n * ∫ (t : ℝ),
    mellin (fun x ↦ ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * (X / (n : ℂ)) ^ (2 + ↑t * I)) := ?_
  _ = 1 / (2 * π) * (∑' n, Λ n * ∫ (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) * (X / (n : ℂ)) ^ (2 + ↑t * I)) := ?_
  _ = ∑' n, Λ n * (1 / (2 * π) * ∫ (t : ℝ),
    mellin (fun x ↦ ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * ((n : ℂ) / X) ^ (-(2 + ↑t * I))) := ?_
  _ = _ := ?_
Proof state after:
case calc_1
ψ : ℝ → ℝ
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 < ε
⊢ 1 / (2 * ↑π * I) *
      (I *
        ∫ (t : ℝ),
          -deriv riemannZeta (2 + ↑t * I) / riemannZeta (2 + ↑t * I) * mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) *
            ↑X ^ (2 + ↑t * I)) =
    1 / (2 * ↑π * I) *
      (I *
        ∫ (t : ℝ),
          ∑' (n : ℕ), ↑(Λ n) / ↑n ^ (2 + ↑t * I) * mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * ↑X ^ (2 + ↑t * I))

case calc_2
ψ : ℝ → ℝ
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 < ε
⊢ 1 / (2 * ↑π * I) *
      (I *
        ∫ (t : ℝ),
          ∑' (n : ℕ),
            ↑(Λ n) / ↑n ^ (2 + ↑t * I) * mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * ↑X ^ (2 + ↑t * I)) =
    1 / (2 * ↑π * I) *
      (I *
        ∑' (n : ℕ),
          ∫ (t : ℝ), ↑(Λ n) / ↑n ^ (2 + ↑t * I) * mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * ↑X ^ (2 + ↑t * I))

case calc_3
ψ : ℝ → ℝ
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 < ε
⊢ 1 / (2 * ↑π * I) *
      (I *
        ∑' (n : ℕ),
          ∫ (t : ℝ), ↑(Λ n) / ↑n ^ (2 + ↑t * I) * mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * ↑X ^ (2 + ↑t * I)) =
    1 / (2 * ↑π * I) *
      (I * ∑' (n : ℕ), ↑(Λ n) * ∫ (t : ℝ), mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * (↑X / ↑n) ^ (2 + ↑t * I))

case calc_4
ψ : ℝ → ℝ
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 < ε
⊢ 1 / (2 * ↑π * I) *
      (I * ∑' (n : ℕ), ↑(Λ n) * ∫ (t : ℝ), mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * (↑X / ↑n) ^ (2 + ↑t * I)) =
    1 / (2 * ↑π) *
      ∑' (n : ℕ), ↑(Λ n) * ∫ (t : ℝ), mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * (↑X / ↑n) ^ (2 + ↑t * I)

case calc_5
ψ : ℝ → ℝ
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 < ε
⊢ 1 / (2 * ↑π) *
      ∑' (n : ℕ), ↑(Λ n) * ∫ (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) * (↑X / ↑n) ^ (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 < ε
⊢ ∑' (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_7
ψ : ℝ → ℝ
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 < ε
⊢ ∑' (n : ℕ),
      ↑(Λ n) *
        (1 / (2 * ↑π) * ∫ (t : ℝ), mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * (↑n / ↑X) ^ (-(2 + ↑t * I))) =
    ↑(∑' (n : ℕ), Λ n * Smooth1 ψ ε (↑n / X))