Mem powerset sum of mem reduce to Fluxes Ten

lemma mem_powerset_sum_of_mem_reduce_toFluxesTen {F : TenQuanta 𝓩}    {f : Fluxes} (hf : f ∈ F.reduce.toFluxesTen) :    f ∈ (Multiset.powerset F.toFluxesTen).map fun s => s.sum := by  rw [toFluxesTen, 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))  simp only [and_true]  rw [toFluxesTen]  refine Multiset.map_le_map ?_  exact Multiset.filter_le (fun x => x.1 = q) F