Mem minimally Allows Term Of Finset of minimally Allows Term

lemma mem_minimallyAllowsTermOfFinset_of_minimallyAllowsTerm {S5 S10 : Finset 𝓩}    {T : PotentialTerm} (x : ChargeSpectrum 𝓩) (h : x.MinimallyAllowsTerm T)    (hx : x ∈ ofFinset S5 S10) :    x ∈ minimallyAllowsTermsOfFinset S5 S10 T := by  obtain ⟨a, b, c, rfl⟩ := eq_allowsTermForm_of_minimallyAllowsTerm h  cases T  all_goals    simp [allowsTermForm, minimallyAllowsTermsOfFinset]    rw [mem_ofFinset_iff] at hx  case μ =>    simp_all [allowsTermForm]  case β =>    exact ⟨{a}, by simp_all [allowsTermForm]⟩  case Λ =>    exact ⟨{a, b}, {- a - b}, by simp_all [allowsTermForm]⟩  case W1 =>    refine ⟨⟨{- a - b - c}, {a, b, c}, ?_⟩, h⟩    simp_all [allowsTermForm]    abel  case W2 =>    refine ⟨⟨{a, b, c}, ?_⟩, h⟩    simp_all [allowsTermForm]    abel  case W3 =>    use {b, - b - 2 • a}    simp_all [allowsTermForm]    abel  case W4 =>    exact ⟨{c}, by simp_all [allowsTermForm]⟩  case K1 =>    exact ⟨{-a}, {b, - a - b}, by simp_all [allowsTermForm]⟩  case K2 =>    exact ⟨{- a - b}, by simp_all [allowsTermForm]⟩  case topYukawa =>    exact ⟨{b, - a - b}, by simp_all [allowsTermForm]⟩  case bottomYukawa =>    exact ⟨{b}, {- a - b}, by simp_all [allowsTermForm]⟩