Of Potential Term' subset of Potential Term

lemma ofPotentialTerm'_subset_ofPotentialTerm [DecidableEq 𝓩]    {x : ChargeSpectrum 𝓩} (T : PotentialTerm) :    x.ofPotentialTerm' T ⊆ x.ofPotentialTerm T := by  refine Multiset.subset_iff.mpr (fun n h => ?_)  cases T  all_goals    try simp [ofPotentialTerm'_W2_finset, ofPotentialTerm'_W3_finset,      ofPotentialTerm'_β_finset, ofPotentialTerm'_μ_finset,      ofPotentialTerm'_W4_finset, ofPotentialTerm'_K2_finset,      ofPotentialTerm'_topYukawa_finset, ofPotentialTerm'_bottomYukawa_finset] at h    try simp [ofPotentialTerm', -existsAndEq] at h  case' μ | β =>    obtain ⟨q1, q2, ⟨q1_mem, q2_mem⟩, q_sum⟩ := h  case' Λ | W3 | W4 | K1 | K2 | topYukawa | bottomYukawa =>    obtain ⟨q1, q2, q3, ⟨q1_mem, q2_mem, q3_mem⟩, q_sum⟩ := h  case' W1 | W2 =>    obtain ⟨q1, q2, q3, q4, ⟨q1_mem, q2_mem, q3_mem, q4_mem⟩, q_sum⟩ := h  case' μ => refine ofPotentialTerm_mono (x := ⟨q1, q2, ∅, ∅⟩) ?μSub _ ?μP  case' β => refine ofPotentialTerm_mono (x := ⟨none, q1, {q2}, ∅⟩) ?βSub _ ?βP  case' Λ =>    refine ofPotentialTerm_mono (x := ⟨none, none, {q1, q2}, {q3}⟩) ?ΛSub _ ?ΛP  case' W1 =>    refine ofPotentialTerm_mono (x := ⟨none, none, {q1}, {q2, q3, q4}⟩) ?W1Sub _ ?W1P  case' W2 =>    refine ofPotentialTerm_mono (x := ⟨q1, none, ∅, {q2, q3, q4}⟩) ?W2Sub _ ?W2P  case' W3 => refine ofPotentialTerm_mono (x := ⟨none, q1, {q2, q3}, ∅⟩) ?W3Sub _ ?W3P  case' W4 => refine ofPotentialTerm_mono (x := ⟨q1, q2, {q3}, ∅⟩) ?W4Sub _ ?W4P  case' K1 =>    refine ofPotentialTerm_mono (x := ⟨none, none, {q1}, {q2, q3}⟩)      ?K1Sub _ ?K1P  case' K2 => refine ofPotentialTerm_mono (x := ⟨q1, q2, ∅, {q3}⟩) ?K2Sub _ ?K2P  case' topYukawa =>    refine ofPotentialTerm_mono (x := ⟨none, q1, ∅, {q2, q3}⟩)      ?topYukawaSub _ ?topYukawaP  case' bottomYukawa =>    refine ofPotentialTerm_mono (x := ⟨q1, none, {q2}, {q3}⟩)      ?bottomYukawaSub _ ?bottomYukawaP  case' μSub | βSub | ΛSub | W1Sub | W2Sub | W3Sub | W4Sub | K1Sub | K2Sub |      topYukawaSub | bottomYukawaSub =>    rw [subset_def]    simp_all [Finset.insert_subset, -existsAndEq]  all_goals    simp [ofPotentialTerm, PotentialTerm.toFieldLabel, ofFieldLabel]  case ΛP =>    use q1, q2    simp [← q_sum]  case W3P | K1P | topYukawaP =>    use q2, q3    simp [← q_sum]    abel  case W1P | W2P =>    use q2, q3, q4    simp [← q_sum]    abel  all_goals    rw [← q_sum]    try abel