Fluxes Five chiral Indices Of D subset sum le three of no Exotics

lemma FluxesFive.chiralIndicesOfD_subset_sum_le_three_of_noExotics (F : FluxesFive)    (hF : NoExotics F) (S : Multiset Fluxes)    (hSle : S ≤ F) : (S.map (fun x => x.1)).sum ≤ 3 := by  have hs : S.map (fun x => x.1) ≤ F.chiralIndicesOfD := Multiset.map_le_map hSle  have hpos : 0 ≤ (F.chiralIndicesOfD - S.map (fun x => x.1)).sum :=    Multiset.sum_nonneg fun x hx =>      chiralIndicesOfD_noneg_of_noExotics F hF x (Multiset.mem_of_le tsub_le_self hx)  have sum_add_compl_eq_three : (S.map (fun x => x.1)).sum +      (F.chiralIndicesOfD - S.map (fun x => x.1)).sum = 3 := by    rw [← Multiset.sum_add, add_tsub_cancel_of_le hs,      F.chiralIndicesOfD_sum_eq_three_of_noExotics hF]  omega