no goals
x y a b : ℝ
n : ℕ
ha : a ≠ 0
⊢ (fun x => x ^ n / (a * exp x + b)) ∘ log =ᶠ[atTop] fun x => log x ^ n / (a * x + b)
filter_upwards [eventually_gt_atTop (0 : ℝ)] with x hx using by simp [exp_log hx]
no goals
x✝ y a b : ℝ
n : ℕ
ha : a ≠ 0
x : ℝ
hx : 0 < x
⊢ ((fun x => x ^ n / (a * exp x + b)) ∘ log) x = log x ^ n / (a * x + b)
simp [exp_log hx]