rw [abs_inv, inv_le_inv (by positivity) ht, abs_mul, abs_eq_self.mpr ht.le]
case neg
n : ℕ
A a✝ b c d u x y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a t : ℝ
h0 : ¬t = 0
ht : 0 < t
⊢ |(t * (1 + (a * t.log) ^ 2))⁻¹| ≤ t⁻¹
case neg
n : ℕ
A a✝ b c d u x y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a t : ℝ
h0 : ¬t = 0
ht : 0 < t
⊢ t ≤ t * |1 + (a * t.log) ^ 2|