Decompose to Fluxes Ten

lemma decompose_toFluxesTen (x : TenQuanta 𝓩)    (hx : x.toFluxesTen ∈ FluxesTen.elemsNoExotics) :    x.decompose.toFluxesTen = {⟨1, 0⟩, ⟨1, 0⟩, ⟨1, 0⟩} ∨    x.decompose.toFluxesTen = {⟨1, 1⟩, ⟨1, -1⟩, ⟨1, 0⟩} := by  rw [toFluxesTen, decompose]  rw [Multiset.map_bind]  simp only [Multiset.map_map, Function.comp_apply, Multiset.map_id', Multiset.insert_eq_cons,    Int.reduceNeg]  have hx : (Multiset.bind x fun a => decomposeFluxes a.2) =      (Multiset.bind x.toFluxesTen fun a => decomposeFluxes a) := by    rw [toFluxesTen, Multiset.bind_map]  rw [hx]  clear hx  generalize x.toFluxesTen = F at *  revert F  decide