no goals
E : Type ?u.258402
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
⊢ Tendsto (↑normSq) (cocompact ℂ) atTop
simpa [mul_self_abs]
using tendsto_abs_cocompact_atTop.atTop_mul_atTop tendsto_abs_cocompact_atTop