Completions eq completions Top Yukawa of mem minimally Allows Terms Of Finset

lemma completions_eq_completionsTopYukawa_of_mem_minimallyAllowsTermsOfFinset [AddCommGroup 𝓩]    {S5 S10 : Finset 𝓩} (x : ChargeSpectrum 𝓩)    (hx : x ∈ minimallyAllowsTermsOfFinset S5 S10 .topYukawa) :    completions S5 S10 x = completionsTopYukawa S5 x := by  refine (Multiset.Nodup.ext ?_ ?_).mpr ?_  · exact completions_nodup S5 S10 x  · exact completionsTopYukawa_nodup x  intro a  simp [minimallyAllowsTermsOfFinset] at hx  obtain ⟨qHu, Q10, ⟨⟨h1, ⟨h2, hcard⟩⟩, h3⟩, rfl⟩ := hx  simp [completions, completionsTopYukawa]  have Q10_ne_zero : Q10 ≠ 0 := by    by_contra hn    subst hn    simp at hcard  simp [Q10_ne_zero]  match a with  | ⟨xqHd, xqHu, xQ5, xQ10⟩ =>  simp [eq_iff]  aesop