Theorem: Bump₁.iSup₂_coe_eq_coe_sSup (ForML/BumpTopology.lean)

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

State before:
n : ℕ
f : Bump ℝ
K : Set ℝ
hK : IsCompact K
⊢ ⨆ x ∈ K, ↑(absNthDeriv n f x) = ⨆ a ∈ absNthDeriv n f '' K, ↑a
Tactic:
repeat rw [← sSup_image]
State after:
n : ℕ
f : Bump ℝ
K : Set ℝ
hK : IsCompact K
⊢ sSup ((fun x => ↑(absNthDeriv n f x)) '' K) = sSup ((fun a => ↑a) '' (absNthDeriv n f '' K))

State before:
n : ℕ
f : Bump ℝ
K : Set ℝ
hK : IsCompact K
⊢ sSup ((fun x => ↑(absNthDeriv n f x)) '' K) = sSup ((fun a => ↑a) '' (absNthDeriv n f '' K))
Tactic:
congr
State after:
case e_a
n : ℕ
f : Bump ℝ
K : Set ℝ
hK : IsCompact K
⊢ (fun x => ↑(absNthDeriv n f x)) '' K = (fun a => ↑a) '' (absNthDeriv n f '' K)

State before:
case e_a
n : ℕ
f : Bump ℝ
K : Set ℝ
hK : IsCompact K
⊢ (fun x => ↑(absNthDeriv n f x)) '' K = (fun a => ↑a) '' (absNthDeriv n f '' K)
Tactic:
ext x
State after:
case e_a.h
n : ℕ
f : Bump ℝ
K : Set ℝ
hK : IsCompact K
x : ENNReal
⊢ x ∈ (fun x => ↑(absNthDeriv n f x)) '' K ↔ x ∈ (fun a => ↑a) '' (absNthDeriv n f '' K)

State before:
case e_a.h
n : ℕ
f : Bump ℝ
K : Set ℝ
hK : IsCompact K
x : ENNReal
⊢ x ∈ (fun x => ↑(absNthDeriv n f x)) '' K ↔ x ∈ (fun a => ↑a) '' (absNthDeriv n f '' K)
Tactic:
simp
State after:
no goals

State before:
n : ℕ
f : Bump ℝ
K : Set ℝ
hK : IsCompact K
⊢ sSup ((fun x => ↑(absNthDeriv n f x)) '' K) = ⨆ a ∈ absNthDeriv n f '' K, ↑a
Tactic:
rw [← sSup_image]
State after:
n : ℕ
f : Bump ℝ
K : Set ℝ
hK : IsCompact K
⊢ sSup ((fun x => ↑(absNthDeriv n f x)) '' K) = sSup ((fun a => ↑a) '' (absNthDeriv n f '' K))