Reduce eq self of of Charges nodup

lemma reduce_eq_self_of_ofCharges_nodup (x : FiveQuanta 𝓩) (h : x.toCharges.Nodup) :    x.reduce = x := by  rw [reduce, Multiset.Nodup.dedup h]  simp [toCharges]  conv_rhs => rw [← Multiset.map_id x]  apply Multiset.map_congr rfl  intro p hp  simp only [id_eq]  have x_noDup : x.Nodup := Multiset.Nodup.of_map Prod.fst h  suffices (Multiset.filter (fun f => f.1 = p.1) x) = {p} by simp [this]  refine (Multiset.Nodup.ext (Multiset.Nodup.filter (fun f => f.1 = p.1) x_noDup)    (Multiset.nodup_singleton p)).mpr ?_  intro p'  simp only [Multiset.mem_filter, Multiset.mem_singleton]  constructor  · rintro ⟨h1, h2⟩    simp [toCharges] at h    rw [propext (Multiset.nodup_map_iff_inj_on x_noDup)] at h    apply h    · exact h1    · exact hp    · exact h2  · rintro ⟨rfl⟩    simp_all