Mem powerset sum of mem reduce to Fluxes Five

lemma mem_powerset_sum_of_mem_reduce_toFluxesFive {F : FiveQuanta 𝓩}    {f : Fluxes} (hf : f ∈ F.reduce.toFluxesFive) :    f ∈ (Multiset.powerset F.toFluxesFive).map fun s => s.sum := by  rw [toFluxesFive, Multiset.mem_map] at hf  obtain ⟨⟨q, f⟩, hp, rfl⟩ := hf  rw [mem_reduce_iff] at hp  simp at hp  obtain ⟨hq, rfl⟩ := hp  simp only [Multiset.mem_map, Multiset.mem_powerset]  use (Multiset.map (fun x => x.2) (Multiset.filter (fun x => x.1 = q) F))  exact ⟨Multiset.map_le_map (Multiset.filter_le _ F), rfl⟩