intro σ hσ t t_gt
case intro.intro.intro.intro.intro.intro
A : ℝ
ha : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
h : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log
c : ℝ
hc : 0 < c
h_inv : ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ c / (σ - 1)
⊢ ∀ {σ : ℝ},
    σ ∈ Ioc 1 2 →
      ∀ (t : ℝ),
        3 < |t| → 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ (2 * C) ^ (1 / 4) * c ^ (3 / 4) * (σ - 1) ^ (-3 / 4) * |t|.log ^ (1 / 4)
case intro.intro.intro.intro.intro.intro
A : ℝ
ha : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
h : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log
c : ℝ
hc : 0 < c
h_inv : ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ c / (σ - 1)
σ : ℝ
hσ : σ ∈ Ioc 1 2
t : ℝ
t_gt : 3 < |t|
⊢ 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ (2 * C) ^ (1 / 4) * c ^ (3 / 4) * (σ - 1) ^ (-3 / 4) * |t|.log ^ (1 / 4)