Map lift Charge

lemma map_liftCharge {𝓩 𝓩1 : Type}[DecidableEq 𝓩] [DecidableEq 𝓩1] [CommRing 𝓩] [CommRing 𝓩1]    (f : 𝓩 →+* 𝓩1) (c : Finset 𝓩) (F : TenQuanta 𝓩) (h : F ∈ liftCharge c) :    TenQuanta.reduce (F.map fun y => (f y.1, y.2)) ∈ liftCharge (c.image f) := by  rw [mem_liftCharge_iff] at h ⊢  refine ⟨?_, ?_, ?_⟩  · apply reduce_mem_elemsNoExotics    simpa [toFluxesTen, Multiset.map_map] using h.1  · rw [reduce_toCharges]    simp [← h.2.1, ← Multiset.toFinset_map, toCharges]  · rw [reduce_toCharges]    exact Multiset.nodup_dedup (toCharges (Multiset.map (fun y => (f y.1, y.2)) F))