Exists to Charges to Fluxes Ten of mem lift Charge

lemma exists_toCharges_toFluxesTen_of_mem_liftCharge (c : Finset 𝓩)    {x : TenQuanta 𝓩} (h : x ∈ liftCharge c) :    ∃ a : TenQuanta 𝓩, a.reduce = x ∧ a.toCharges.toFinset = c ∧    (a.toFluxesTen = {⟨1, 0⟩, ⟨1, 0⟩, ⟨1, 0⟩}    ∨ a.toFluxesTen = {⟨1, 1⟩, ⟨1, -1⟩, ⟨1, 0⟩}) := by  have h' := h  rw [liftCharge, Multiset.mem_map] at h  obtain ⟨a, h, rfl⟩ := h  use a  simp only [Multiset.insert_eq_cons, Int.reduceNeg, true_and]  apply And.intro  · rw [← toCharge_toFinset_of_mem_liftCharge c h', reduce_toCharges]    simp  simp at h  rcases h with h | h  · obtain ⟨⟨s, h, rfl⟩, h'⟩ := h    left    simp [toFluxesTen]    rw [h.2]    decide  · obtain ⟨⟨q1, q2, q3, h, rfl⟩, h'⟩ := h    simp [toFluxesTen]