Reduce num Chiral D of mem elems No Exotics

lemma reduce_numChiralD_of_mem_elemsNoExotics {F : FiveQuanta 𝓩}    (hx : F.toFluxesFive ∈ FluxesFive.elemsNoExotics) :    F.reduce.toFluxesFive.numChiralD = 3 := by  have hE : F.toFluxesFive.NoExotics := ((FluxesFive.noExotics_iff_mem_elemsNoExotics _).mpr hx).1  have hnn : ∀ a ∈ F.reduce.toFluxesFive.map (fun f => f.M), 0 ≤ a := by    intro a ha    obtain ⟨f, hf, rfl⟩ := Multiset.mem_map.mp ha    replace hf := mem_powerset_sum_of_mem_reduce_toFluxesFive hf    clear ha hE    generalize F.toFluxesFive = G at *    revert f    revert G    decide  rw [FluxesFive.numChiralD, FluxesFive.chiralIndicesOfD, Multiset.filter_eq_self.mpr hnn,    ← FluxesFive.chiralIndicesOfD_sum_eq_three_of_noExotics _ hE, FluxesFive.chiralIndicesOfD,    toFluxesFive, toFluxesFive, Multiset.map_map, Multiset.map_map]  exact reduce_sum_eq_sum_toCharges F (fun _ => ⟨⟨fun f => f.M, by simp⟩, fun x y => by simp⟩)