Reduce num Chiral E of mem elems No Exotics

lemma reduce_numChiralE_of_mem_elemsNoExotics {F : TenQuanta 𝓩}    (hx : F.toFluxesTen ∈ FluxesTen.elemsNoExotics) :    F.reduce.toFluxesTen.numChiralE = 3 := by  have hE : F.toFluxesTen.NoExotics := ((FluxesTen.noExotics_iff_mem_elemsNoExotics _).mpr hx).1  have numChiralE_eq_sum := F.toFluxesTen.numChiralE_eq_sum_sub_numAntiChiralE  rw [hE.2.2.2.2.1, hE.2.2.2.2.2, sub_zero, FluxesTen.chiralIndicesOfE] at numChiralE_eq_sum  have hmap : (F.reduce.toFluxesTen.map (fun f => f.M + f.N)).sum =      (F.toFluxesTen.map (fun f => f.M + f.N)).sum := by    have h := reduce_sum_eq_sum_toCharges F      (fun _ => (⟨⟨fun f => f.M + f.N, by simp⟩, fun a b => by simp; ring⟩ : Fluxes →+ ℤ))    simpa [toFluxesTen, Multiset.map_map, Function.comp] using h  rw [FluxesTen.numChiralE, FluxesTen.chiralIndicesOfE, Multiset.filter_eq_self.mpr, hmap]  · exact numChiralE_eq_sum.symm  intro a ha  obtain ⟨f, hf, rfl⟩ := Multiset.mem_map.mp ha  replace hf := mem_powerset_sum_of_mem_reduce_toFluxesTen hf  clear ha hmap numChiralE_eq_sum hE  generalize F.toFluxesTen = G at *  revert f  revert G  decide