Exists to Charges to Fluxes Five of mem lift Charge

lemma exists_toCharges_toFluxesFive_of_mem_liftCharge (c : Finset 𝓩) {x : FiveQuanta 𝓩}    (h : x ∈ liftCharge c) :    ∃ a : FiveQuanta 𝓩, a.reduce = x ∧ a.toCharges.toFinset = c ∧ a.toFluxesFive =      {⟨1, -1⟩, ⟨1, -1⟩, ⟨1, -1⟩, ⟨0, 1⟩, ⟨0, 1⟩, ⟨0, 1⟩} := by  have h' := h  rw [liftCharge, Multiset.mem_map] at h  obtain ⟨a, h, rfl⟩ := h  use a  simp only [Int.reduceNeg, Multiset.insert_eq_cons, true_and]  apply And.intro  · simpa [reduce_toCharges] using toCharges_toFinset_of_mem_liftCharge c h'  · simp at h    obtain ⟨s1, s2, ⟨⟨⟨s1_subset, s1_card⟩, ⟨s2_subset, s2_card⟩⟩, hsum⟩, rfl⟩ := h    simp [toFluxesFive, s1_card, s2_card]    decide