Eq allows Term Form of mem minimally Allows Term Of Finset

lemma eq_allowsTermForm_of_mem_minimallyAllowsTermOfFinset {S5 S10 : Finset 𝓩} {T : PotentialTerm}    {x : ChargeSpectrum 𝓩} (hx : x ∈ minimallyAllowsTermsOfFinset S5 S10 T) :    ∃ a b c, x = allowsTermForm a b c T := by  cases T  all_goals    simp [minimallyAllowsTermsOfFinset] at hx  case μ =>    obtain ⟨a, b, ⟨⟨ha, hb⟩, hsum⟩, rfl⟩ := hx    simp_all [allowsTermForm]    grind  case β =>    obtain ⟨a, b, ⟨⟨ha, ⟨hb, hbcard⟩⟩, hsum⟩, rfl⟩ := hx    obtain ⟨c, rfl⟩ := Multiset.card_eq_one.mp hbcard    simp_all [allowsTermForm]    grind  case K1 =>    obtain ⟨a, b, ⟨⟨⟨ha, hacard⟩, ⟨hb, hbcard⟩⟩, hsum⟩, rfl⟩ := hx    obtain ⟨c, rfl⟩ := Multiset.card_eq_one.mp hacard    obtain ⟨d, e, rfl⟩ := Multiset.card_eq_two.mp hbcard    simp_all [allowsTermForm]    refine ⟨-c, ?_, d, ?_⟩ <;> grind  case Λ =>    obtain ⟨a, b, ⟨⟨⟨ha, hacard⟩, ⟨hb, hbcard⟩⟩, hsum⟩, rfl⟩ := hx    obtain ⟨c, d, rfl⟩ := Multiset.card_eq_two.mp hacard    obtain ⟨e, rfl⟩ := Multiset.card_eq_one.mp hbcard    simp_all [allowsTermForm]    grind  case W1 =>    obtain ⟨⟨a, b, ⟨⟨⟨ha, hacard⟩, ⟨hb, hbcard⟩⟩, hsum⟩, rfl⟩, _⟩ := hx    obtain ⟨c, rfl⟩ := Multiset.card_eq_one.mp hacard    obtain ⟨e, d, f, rfl⟩ := Multiset.card_eq_three.mp hbcard    simp_all [allowsTermForm]    grind  case W2 =>    obtain ⟨⟨a, b, ⟨⟨ha, ⟨hb, hbcard⟩⟩, hsum⟩, rfl⟩, _⟩ := hx    obtain ⟨e, d, f, rfl⟩ := Multiset.card_eq_three.mp hbcard    simp_all [allowsTermForm]    grind  case W3 =>    obtain ⟨a, b, ⟨⟨ha, ⟨hb, hbcard⟩⟩, hsum⟩, rfl⟩ := hx    obtain ⟨c, d, rfl⟩ := Multiset.card_eq_two.mp hbcard    simp_all [allowsTermForm]    refine ⟨-a, ?_, c, ?_⟩ <;> grind  case W4 =>    obtain ⟨a, b, c, ⟨⟨ha, ⟨hb, hc, hcard⟩⟩, hsum⟩, rfl⟩ := hx    obtain ⟨d, rfl⟩ := Multiset.card_eq_one.mp hcard    simp_all [allowsTermForm]    exact ⟨-b, by grind⟩  case K2 =>    obtain ⟨a, b, c, ⟨⟨ha, ⟨hb, hc, hcard⟩⟩, hsum⟩, rfl⟩ := hx    obtain ⟨d, rfl⟩ := Multiset.card_eq_one.mp hcard    simp_all [allowsTermForm]    grind  case topYukawa =>    obtain ⟨a, b, ⟨⟨ha, ⟨hb, hbcard⟩⟩, hsum⟩, rfl⟩ := hx    obtain ⟨c, d, rfl⟩ := Multiset.card_eq_two.mp hbcard    simp_all [allowsTermForm]    refine ⟨-a, ?_, c, ?_⟩ <;> grind  case bottomYukawa =>    obtain ⟨a, b, c, ⟨⟨ha, ⟨⟨hb, hbcard⟩, hc, hcard⟩⟩, hsum⟩, rfl⟩ := hx    obtain ⟨e, rfl⟩ := Multiset.card_eq_one.mp hcard    obtain ⟨d, rfl⟩ := Multiset.card_eq_one.mp hbcard    simp_all [allowsTermForm]    grind