Of Potential Term subset of Potential Term

lemma ofPotentialTerm_subset_ofPotentialTerm' {x : ChargeSpectrum 𝓩} (T : PotentialTerm) :    x.ofPotentialTerm T ⊆ x.ofPotentialTerm' T := by  refine Multiset.subset_iff.mpr (fun n h => ?_)  simp [ofPotentialTerm] at h  cases T  all_goals    simp [PotentialTerm.toFieldLabel, -existsAndEq] at h    obtain ⟨f1, f2, ⟨⟨f3, f4, ⟨h3, f4_mem⟩, rfl⟩, f2_mem⟩, f1_add_f2_eq_zero⟩ := h  case' μ | β => obtain ⟨rfl⟩ := h3  case' Λ | W1 | W2 | W3 | W4 | K1 | K2 | topYukawa | bottomYukawa =>    obtain ⟨f5, f6, ⟨h4, f6_mem⟩, rfl⟩ := h3  case' Λ | K1 | K2 | topYukawa | bottomYukawa => obtain ⟨rfl⟩ := h4  case' W1 | W2 | W3 | W4 => obtain ⟨f7, f8, ⟨rfl, f8_mem⟩, rfl⟩ := h4  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]    try simp [ofPotentialTerm', -existsAndEq]    simp_all [ofFieldLabel, -existsAndEq]  case' W1 => use f2, f4, f6, f8  case' W2 => use f2, f4, f6, f8  case' W3 => use (-f2), f6, f8  case' W4 => use f6, (-f4), f8  case' K1 => use (-f2), f4, f6  case' K2 => use f4, f6, f2  case' Λ => use f4, f6, f2  case' topYukawa => use (-f2), f4, f6  case' bottomYukawa => use f2, f4, f6  case' β => use (-f4), f2  all_goals simp_all  all_goals    rw [← f1_add_f2_eq_zero]    abel