simp only [hh', neg_mul, Left.neg_nonpos_iff, ge_iff_le]
n : ℕ
A a✝ b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a x : ℝ
ha : a ∈ Ioo (-1) 1
this : 0 < pp a x.log
⊢ hh' a x ≤ 0
n : ℕ
A a✝ b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a x : ℝ
ha : a ∈ Ioo (-1) 1
this : 0 < pp a x.log
⊢ 0 ≤ pp a x.log * hh a x ^ 2