no goals
F : Type ?u.1063529
α : Type u
β : Type v
γ : Type w
inst✝¹ : TopologicalSpace α
inst✝ : SeminormedAddCommGroup β
f g : α →ᵇ β
x : α
C : ℝ
⊢ (⨆ (x : α), ‖↑f x‖) = ↑(⨆ (x : α), ‖↑f x‖₊)
simp_rw [val_eq_coe, NNReal.coe_iSup, coe_nnnorm]