Extensions to ENNReal

The intention is to upstream these to mathlib.

theorem ENNReal.tsum_biUnion'' {α : Type u_2} {ι : Type u_1} {t : ι → Set α} {f : ↑(⋃ (i : ι), t i) → ENNReal} (h : Set.univ.PairwiseDisjoint t) : ∑' (x : ↑(⋃ (i : ι), t i)), f x = ∑' (i : ι) (x : ↑(t i)), f ⟨↑x, ⋯⟩

@[simp]

theorem NNRat.ennreal_cast {n : ℕ} : ↑↑n = ↑n

@[simp]

theorem NNRat.ennreal_cast_zero : ↑0 = 0

@[simp]

theorem NNRat.ennreal_cast_one : ↑1 = 1

@[simp]

theorem NNRat.toENNReal_sub (a b : ℚ≥0) : ↑(a - b) = ↑a - ↑b