Reduce sum eq sum to Charges

lemma reduce_sum_eq_sum_toCharges {M} [AddCommMonoid M] (x : FiveQuanta 𝓩) (f : 𝓩 → Fluxes →+ M) :    (x.reduce.map fun (q5, x) => f q5 x).sum = (x.map fun (q5, x) => f q5 x).sum := by  calc _      _ = ∑ q5 ∈ x.toCharges.toFinset,          f q5 ((x.filter (fun f => f.1 = q5)).map (fun y => y.2)).sum := by        rw [reduce]        simp [Finset.sum]      _ = ∑ q5 ∈ x.toCharges.toFinset,          (((x.filter (fun f => f.1 = q5)).map (fun y => f q5 y.2))).sum := by        congr        funext q5        rw [AddMonoidHom.map_multiset_sum, Multiset.map_map]        rfl      _ = (x.toCharges.dedup.bind fun q5 =>          ((x.filter (fun f => f.1 = q5)).map (fun y => f q5 y.2))).sum := by        rw [Multiset.sum_bind]        simp [Finset.sum]      _ = (((x.toCharges.dedup.bind fun q5 =>          ((x.filter (fun f => f.1 = q5)))).map (fun y => f y.1 y.2))).sum := by        congr        rw [Multiset.map_bind]        congr        funext q5        refine Multiset.map_congr rfl ?_        intro y hy        simp at hy        rw [hy.2]      _ = ((x.map (fun y => f y.1 y.2))).sum := by        congr        apply Multiset.ext.mpr        intro p        trans ((x.map Prod.fst).dedup.map (fun y => if p.1 = y then x.count p else 0)).sum        · rw [@Multiset.count_bind]          congr          funext q5          rw [Multiset.count_filter]        by_cases h_mem : p.1 ∈ x.map Prod.fst        · have h_mem_dedup : p.1 ∈ (x.map Prod.fst).dedup := by rwa [Multiset.mem_dedup]          rw [Multiset.sum_map_eq_nsmul_single p.1]          simp only [↓reduceIte, smul_eq_mul]          have h_count_one : Multiset.count p.1 (Multiset.map Prod.fst x).dedup = 1 := by            refine Multiset.count_eq_one_of_mem ?_ h_mem_dedup            exact Multiset.nodup_dedup (Multiset.map Prod.fst x)          simp [h_count_one]          intro q5' h h2          simp_all [eq_comm]        · rw [Multiset.sum_eq_zero]          refine Eq.symm (Multiset.count_eq_zero_of_notMem ?_)          intro h          have h_mem : p.1 ∈ Multiset.map Prod.fst x := by            simp_all          (expose_names; exact h_mem_1 h_mem)          intro p' hp          simp at hp          obtain ⟨q5', ⟨f1, hf⟩, hp'⟩ := hp          by_cases h_eq : p.1 = q5'          · simp_all          · simp_all