Mem min Top Bottom of minimally Allows Finset Terms

lemma mem_minTopBottom_of_minimallyAllowsFinsetTerms    {x : ChargeSpectrum 𝓩} {S5 S10 : Finset 𝓩}    (h : x.MinimallyAllowsFinsetTerms {topYukawa, bottomYukawa})    (hx : x ∈ ofFinset S5 S10) :    x ∈ minTopBottom S5 S10 := by  simp [minTopBottom]  have hTop : x.AllowsTerm topYukawa := allowsTerm_of_minimallyAllowsFinsetTerms h (by simp)  have hBottom : x.AllowsTerm bottomYukawa := allowsTerm_of_minimallyAllowsFinsetTerms h (by simp)  match x with  | ⟨none, qHu, Q5, Q10⟩ =>    simp [allowsTerm_iff_subset_allowsTermForm, allowsTermForm, subset_def] at hBottom  | ⟨qHd, none, Q5, Q10⟩ =>    simp [allowsTerm_iff_subset_allowsTermForm, allowsTermForm, subset_def] at hTop  | ⟨some qHd, some qHu, Q5, Q10⟩ =>  simp [allowsTerm_iff_subset_allowsTermForm, allowsTermForm, subset_def] at hTop hBottom  obtain ⟨n, hn, q10, h10⟩ := hTop  obtain ⟨q5, h5⟩ := hBottom  use qHd, qHu, q5, q10  simp [mem_ofFinset_iff] at hx  refine ⟨⟨hx.1, hx.2.1, hx.2.2.1 h5.1, hx.2.2.2 (h10 (Finset.mem_insert_self _ _))⟩, ?_⟩  refine (h _ ?_).mpr ?_  · simp [subset_def]    exact ⟨h5.1, Finset.insert_subset h5.2 (hn ▸ h10)⟩  · intro T hT    fin_cases hT    · simp [allowsTerm_iff_subset_allowsTermForm, allowsTermForm, subset_def]      exact ⟨-qHu, by simp, q10, by simp⟩    · simp [allowsTerm_iff_subset_allowsTermForm, allowsTermForm, subset_def]