have := hA'.1
C' : ℝ
C'pos : C' > 0
hC₁ : ∀ {σ : ℝ}, σ ∈ Ioc 1 2 → ∀ (t : ℝ), 3 < |t| → 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C' * (σ - 1) ^ (-3 / 4) * |t|.log ^ (1 / 4)
A' : ℝ
hA' : A' ∈ Ioc 0 (1 / 2)
C₂ : ℝ
C₂pos : 0 < C₂
hC₂ :
  ∀ (σ₁ σ₂ t : ℝ),
    3 < |t| →
      1 - A' / |t|.log ≤ σ₁ → σ₂ ≤ 2 → σ₁ < σ₂ → ‖ζ (↑σ₂ + ↑t * I) - ζ (↑σ₁ + ↑t * I)‖ ≤ C₂ * |t|.log ^ 2 * (σ₂ - σ₁)
C₁ : ℝ := 1 / C'
A : ℝ := min A' (1 / 2 * (C₁ / (C₂ * 2)) ^ 4)
⊢ 0 < A
C' : ℝ
C'pos : C' > 0
hC₁ : ∀ {σ : ℝ}, σ ∈ Ioc 1 2 → ∀ (t : ℝ), 3 < |t| → 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C' * (σ - 1) ^ (-3 / 4) * |t|.log ^ (1 / 4)
A' : ℝ
hA' : A' ∈ Ioc 0 (1 / 2)
C₂ : ℝ
C₂pos : 0 < C₂
hC₂ :
  ∀ (σ₁ σ₂ t : ℝ),
    3 < |t| →
      1 - A' / |t|.log ≤ σ₁ → σ₂ ≤ 2 → σ₁ < σ₂ → ‖ζ (↑σ₂ + ↑t * I) - ζ (↑σ₁ + ↑t * I)‖ ≤ C₂ * |t|.log ^ 2 * (σ₂ - σ₁)
C₁ : ℝ := 1 / C'
A : ℝ := min A' (1 / 2 * (C₁ / (C₂ * 2)) ^ 4)
this : 0 < A'
⊢ 0 < A