rw [ENNReal.coe_sSup (absNthDeriv_bddAbove_image hK)]
n : ℕ
f : Bump ℝ
K : Set ℝ
hK : IsCompact K
⊢ ⨆ x ∈ K, ↑(absNthDeriv n f x) = ↑(sSup (absNthDeriv n f '' K))
n : ℕ
f : Bump ℝ
K : Set ℝ
hK : IsCompact K
⊢ ⨆ x ∈ K, ↑(absNthDeriv n f x) = ⨆ a ∈ absNthDeriv n f '' K, ↑a