Sum of suprema in ENat

theorem ENat.sum_iSup {α : Type u_1} {ι : Type u_2} {s : Finset α} {f : α → ι → ℕ∞} (hf : ∀ (i j : ι), ∃ (k : ι), ∀ (a : α), f a i ≤ f a k ∧ f a j ≤ f a k) : ∑ a ∈ s, ⨆ (i : ι), f a i = ⨆ (i : ι), ∑ a ∈ s, f a i

theorem ENat.sum_iSup_of_monotone {α : Type u_1} {ι : Type u_2} [Preorder ι] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] {s : Finset α} {f : α → ι → ℕ∞} (hf : ∀ (a : α), Monotone (f a)) : ∑ a ∈ s, iSup (f a) = ⨆ (n : ι), ∑ a ∈ s, f a n