have ⟨h₁, h₂, h₃⟩ := UpperBnd_aux6 t_gt ⟨σ_gt, hσ.2⟩ neOne Npos N_le_t
case intro.intro.intro.intro.intro.calc_4
A σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
t_gt : 3 < |t|
hσ : σ ∈ Icc (1 - A / |t|.log) 2
C : ℝ := A.exp * (5 + 8 * 2)
N : ℕ := ⌊|t|⌋₊
s : ℂ := ↑σ + ↑t * I
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
logt_gt : 1 < |t|.log
σPos : 0 < σ
neOne : ↑σ + ↑t * I ≠ 1
σ_gt : 1 / 2 < σ
⊢ A.exp * 2 * |t|.log + ↑N ^ (1 - σ) / ‖1 - s‖ + ↑N ^ (-σ) / 2 + 2 * |t| * ↑N ^ (-σ) / σ ≤
    A.exp * 2 * |t|.log + |t| ^ (1 - σ) * 2 + |t| ^ (1 - σ) + 2 * |t| * (8 * |t| ^ (-σ))
case intro.intro.intro.intro.intro.calc_4
A σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
t_gt : 3 < |t|
hσ : σ ∈ Icc (1 - A / |t|.log) 2
C : ℝ := A.exp * (5 + 8 * 2)
N : ℕ := ⌊|t|⌋₊
s : ℂ := ↑σ + ↑t * I
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
logt_gt : 1 < |t|.log
σPos : 0 < σ
neOne : ↑σ + ↑t * I ≠ 1
σ_gt : 1 / 2 < σ
h₁ : ↑⌊|t|⌋₊ ^ (1 - σ) / ‖1 - (↑σ + ↑t * I)‖ ≤ |t| ^ (1 - σ) * 2
h₂ : ↑⌊|t|⌋₊ ^ (-σ) / 2 ≤ |t| ^ (1 - σ)
h₃ : ↑⌊|t|⌋₊ ^ (-σ) / σ ≤ 8 * |t| ^ (-σ)
⊢ A.exp * 2 * |t|.log + ↑N ^ (1 - σ) / ‖1 - s‖ + ↑N ^ (-σ) / 2 + 2 * |t| * ↑N ^ (-σ) / σ ≤
    A.exp * 2 * |t|.log + |t| ^ (1 - σ) * 2 + |t| ^ (1 - σ) + 2 * |t| * (8 * |t| ^ (-σ))