convert intervalIntegral.norm_integral_le_of_norm_le_const ?_ using 1
case intro.intro.intro.intro
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
C : ℝ
Cpos : 0 < C
hC : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 2
σ₁ σ₂ t : ℝ
t_gt : 3 < |t|
σ₁_ge : 1 - A / |t|.log ≤ σ₁
σ₂_le : σ₂ ≤ 2
σ₁_lt_σ₂ : σ₁ < σ₂
t_ne_zero : t ≠ 0
⊢ ‖∫ (σ : ℝ) in σ₁..σ₂, deriv ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 2 * (σ₂ - σ₁)
case h.e'_4
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
C : ℝ
Cpos : 0 < C
hC : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 2
σ₁ σ₂ t : ℝ
t_gt : 3 < |t|
σ₁_ge : 1 - A / |t|.log ≤ σ₁
σ₂_le : σ₂ ≤ 2
σ₁_lt_σ₂ : σ₁ < σ₂
t_ne_zero : t ≠ 0
⊢ C * |t|.log ^ 2 * (σ₂ - σ₁) = ?intro.intro.intro.intro.convert_6 * |σ₂ - σ₁|

case intro.intro.intro.intro.convert_6
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
C : ℝ
Cpos : 0 < C
hC : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 2
σ₁ σ₂ t : ℝ
t_gt : 3 < |t|
σ₁_ge : 1 - A / |t|.log ≤ σ₁
σ₂_le : σ₂ ≤ 2
σ₁_lt_σ₂ : σ₁ < σ₂
t_ne_zero : t ≠ 0
⊢ ℝ

case intro.intro.intro.intro.convert_8
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
C : ℝ
Cpos : 0 < C
hC : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 2
σ₁ σ₂ t : ℝ
t_gt : 3 < |t|
σ₁_ge : 1 - A / |t|.log ≤ σ₁
σ₂_le : σ₂ ≤ 2
σ₁_lt_σ₂ : σ₁ < σ₂
t_ne_zero : t ≠ 0
⊢ ∀ x ∈ Ι σ₁ σ₂, ‖deriv ζ (↑x + ↑t * I)‖ ≤ ?intro.intro.intro.intro.convert_6