rw [norm_mul, norm_mul]
case intro.intro.intro.intro.intro.intro.intro.calc_3.refine_2
A : ℝ
ha : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
c : ℝ
hc : 0 < c
h_inv : ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ c / (σ - 1)
σ t : ℝ
t_gt : 3 < |t|
σ_gt : 1 < σ
σ_le : σ ≤ 2
ht' : 3 < |2 * t|
hnezero : ((σ - 1) / c) ^ (-3 / 4) ≠ 0
h : ‖ζ (↑σ + ↑(2 * t) * I)‖ ≤ C * |2 * t|.log
this : 0 ≤ |2 * t|.log
⊢ ‖((σ - 1) / c) ^ (-3 / 4) * ‖ζ (↑σ + 2 * ↑t * I)‖ ^ (1 / 4)‖ ≤
    ‖((σ - 1) / c) ^ (-3 / 4) * (C * |2 * t|.log) ^ (1 / 4)‖
case intro.intro.intro.intro.intro.intro.intro.calc_3.refine_2
A : ℝ
ha : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
c : ℝ
hc : 0 < c
h_inv : ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ c / (σ - 1)
σ t : ℝ
t_gt : 3 < |t|
σ_gt : 1 < σ
σ_le : σ ≤ 2
ht' : 3 < |2 * t|
hnezero : ((σ - 1) / c) ^ (-3 / 4) ≠ 0
h : ‖ζ (↑σ + ↑(2 * t) * I)‖ ≤ C * |2 * t|.log
this : 0 ≤ |2 * t|.log
⊢ ‖((σ - 1) / c) ^ (-3 / 4)‖ * ‖‖ζ (↑σ + 2 * ↑t * I)‖ ^ (1 / 4)‖ ≤
    ‖((σ - 1) / c) ^ (-3 / 4)‖ * ‖(C * |2 * t|.log) ^ (1 / 4)‖