no goals
α : Type ?u.32561
x✝ y z : ℝ
l : Filter α
n : ℕ
x : ℝ
⊢ ((fun r => r⁻¹) ∘ fun x => exp x / x ^ n) x = x ^ n * exp (-x)
rw [comp_apply, inv_eq_one_div, div_div_eq_mul_div, one_mul, div_eq_mul_inv, exp_neg]