Complete Min Subset subset iff contains Pheno Completions Of Minimally Allows

lemma completeMinSubset_subset_iff_containsPhenoCompletionsOfMinimallyAllows    (S5 S10 : Finset 𝓩) (charges : Multiset (ChargeSpectrum 𝓩)) :    completeMinSubset S5 S10 ⊆ charges ↔    ContainsPhenoCompletionsOfMinimallyAllows S5 S10 charges := by  constructor  · intro h    rw [containsPhenoCompletionsOfMinimallyAllows_iff_completionsTopYukawa]    rw [Multiset.subset_iff] at h    intro x hx y hy1 hy2    apply h    simp [completeMinSubset]    simp_all    use x  · intro h y hy    simp [completeMinSubset] at hy    obtain ⟨⟨x, hx, hyx⟩, hy2⟩ := hy    rw [containsPhenoCompletionsOfMinimallyAllows_iff_completionsTopYukawa] at h    exact h x hx y hyx hy2