l : Filter ℂ
hre : Tendsto re l atTop
n : ℕ
hr : im =O[l] fun z => z.re ^ n
⊢ im =O[l] fun z => z.re ^ ↑n
l : Filter ℂ
hre : Tendsto re l atTop
n : ℕ
hr : im =O[l] fun z => z.re ^ ↑n
⊢ im =O[l] fun z => z.re ^ ↑n
norm_cast at hr
no goals
l : Filter ℂ
hre : Tendsto re l atTop
n : ℕ
hr : im =O[l] fun z => z.re ^ n
⊢ im =O[l] fun z => z.re ^ ↑n
simpa only [Real.rpow_nat_cast]