simp only [integrableOn_Ici_iff_integrableOn_Ioi, hh]
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ha : 0 < a
hb : 0 < b
hc : 0 < c
⊢ IntegrableOn (fun t => a * hh b (t / c)) (Ici 0) volume ∧ ∫ (t : ℝ) in Ioi 0, a * hh b (t / c) = a * c / b * π
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ha : 0 < a
hb : 0 < b
hc : 0 < c
⊢ IntegrableOn (fun t => a * (t / c * (1 + (b * (t / c).log) ^ 2))⁻¹) (Ioi 0) volume ∧
    ∫ (t : ℝ) in Ioi 0, a * (t / c * (1 + (b * (t / c).log) ^ 2))⁻¹ = a * c / b * π