convert ZetaUpperBnd' ⟨by norm_num, le_rfl⟩ t_gt ⟨σ_ge, σ_le⟩ using 1
A : ℝ := 1 / 2
C : ℝ := A.exp * (5 + 8 * 2)
σ t : ℝ
t_gt : 3 < |t|
σ_ge : 1 - A / |t|.log ≤ σ
σ_le : σ ≤ 2
Npos : 0 < ⌊|t|⌋₊
left✝² : ↑⌊|t|⌋₊ ≤ |t|
left✝¹ : 1 < |t|.log
left✝ : 1 - A < σ
σPos : 0 < σ
neOne : ↑σ + ↑t * I ≠ 1
⊢ ‖∑ n ∈ Finset.range (⌊|t|⌋₊ + 1), 1 / ↑n ^ (↑σ + ↑t * I)‖ + ‖-↑⌊|t|⌋₊ ^ (1 - (↑σ + ↑t * I)) / (1 - (↑σ + ↑t * I))‖ +
        ‖-↑⌊|t|⌋₊ ^ (-(↑σ + ↑t * I)) / 2‖ +
      ‖(↑σ + ↑t * I) * ∫ (x : ℝ) in Ioi ↑⌊|t|⌋₊, (↑⌊x⌋ + 1 / 2 - ↑x) / ↑x ^ (↑σ + ↑t * I + 1)‖ ≤
    C * |t|.log
case h.e'_3
A : ℝ := 1 / 2
C : ℝ := A.exp * (5 + 8 * 2)
σ t : ℝ
t_gt : 3 < |t|
σ_ge : 1 - A / |t|.log ≤ σ
σ_le : σ ≤ 2
Npos : 0 < ⌊|t|⌋₊
left✝² : ↑⌊|t|⌋₊ ≤ |t|
left✝¹ : 1 < |t|.log
left✝ : 1 - A < σ
σPos : 0 < σ
neOne : ↑σ + ↑t * I ≠ 1
⊢ ‖∑ n ∈ Finset.range (⌊|t|⌋₊ + 1), 1 / ↑n ^ (↑σ + ↑t * I)‖ + ‖-↑⌊|t|⌋₊ ^ (1 - (↑σ + ↑t * I)) / (1 - (↑σ + ↑t * I))‖ +
        ‖-↑⌊|t|⌋₊ ^ (-(↑σ + ↑t * I)) / 2‖ +
      ‖(↑σ + ↑t * I) * ∫ (x : ℝ) in Ioi ↑⌊|t|⌋₊, (↑⌊x⌋ + 1 / 2 - ↑x) / ↑x ^ (↑σ + ↑t * I + 1)‖ =
    ‖∑ n ∈ Finset.range (⌊|t|⌋₊ + 1), 1 / ↑n ^ (↑σ + ↑t * I)‖ + ‖↑⌊|t|⌋₊ ^ (1 - (↑σ + ↑t * I)) / (1 - (↑σ + ↑t * I))‖ +
        ‖↑⌊|t|⌋₊ ^ (-(↑σ + ↑t * I)) / 2‖ +
      ‖(↑σ + ↑t * I) * ∫ (x : ℝ) in Ioi ↑⌊|t|⌋₊, (↑⌊x⌋ + 1 / 2 - ↑x) / ↑x ^ (↑σ + ↑t * I + 1)‖