Some lemmas on extended non-negative reals

These are some lemmas split off from ENNReal.Basic because they need a lot more imports. They are probably good targets for further cleanup or moves.

@[simp]

theorem ENNReal.coe_indicator {α : Type u_2} (s : Set α) (f : α → NNReal) (a : α) : ↑(s.indicator f a) = s.indicator (fun (x : α) => ↑(f x)) a

@[simp]

theorem ENNReal.coe_finset_sup {α : Type u_1} {s : Finset α} {f : α → NNReal} : ↑(s.sup f) = s.sup fun (x : α) => ↑(f x)