ENNReal.enorm_sum_eq_sum_enorm

lemma enorm_sum_eq_sum_enorm {f : α → ℝ} (hf : ∀ i ∈ t, 0 ≤ f i) :    ‖∑ i ∈ t, f i‖ₑ = ∑ i ∈ t, ‖f i‖ₑ := by  induction t using Finset.cons_induction with  | empty => simp  | cons a t ha ihs =>    simp only [Finset.sum_cons]    simp only [Finset.mem_cons, forall_eq_or_imp] at hf    have n₁ := hf.1    have n₂ := Finset.sum_nonneg hf.2    rw [Real.enorm_of_nonneg (add_nonneg n₁ n₂), ENNReal.ofReal_add n₁ n₂,      ← Real.enorm_of_nonneg n₁, ← Real.enorm_of_nonneg n₂, ihs hf.2]