Allows Term Form subset allows Term of allows Term

lemma allowsTermForm_subset_allowsTerm_of_allowsTerm {T : PotentialTerm} {x : ChargeSpectrum 𝓩}    (h : x.AllowsTerm T) :    ∃ a b c, allowsTermForm a b c T ⊆ x ∧ (allowsTermForm a b c T).AllowsTerm T := by  simp [AllowsTerm, 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  -- The cases which are present  case' μ => use f4, (f2), 0  case' β => use (- f4), f2, 0  case' Λ => use f4, f6, f2  case' W1 => use f4, f6, f8  case' W2 => use f4, f6, f8  case' W3 => use (f2), f6, f8  case' W4 => use f6, (f2), f8  case' K1 => use f2, f4, f6  case' K2 => use f4, f6, f2  case' topYukawa => use (f2), f4, f6  case' bottomYukawa => use f2, f4, f6  all_goals    rw [subset_def]    simp_all [ofFieldLabel, Finset.insert_subset_iff, allowsTermForm]  all_goals    simp [AllowsTerm, ofPotentialTerm, PotentialTerm.toFieldLabel, ofFieldLabel]  -- Replacements of equalities  case' W1 | W2 =>    obtain rfl : f2 = -f4 - f6 - f8 := by      rw [← sub_zero f2, ← f1_add_f2_eq_zero]      abel    simp_all  case β =>    obtain rfl : f4 = - f2 := eq_neg_of_add_eq_zero_left f1_add_f2_eq_zero    simp_all  case K2 =>    obtain rfl : f2 = - f4 - f6 := by      rw [← sub_zero f2, ← f1_add_f2_eq_zero]      abel    simp_all  case' Λ =>    obtain rfl : f2 = -f4 - f6 := by      rw [← sub_zero f2, ← f1_add_f2_eq_zero]      abel    simp_all  case' W3 =>    subst f4_mem    obtain rfl : f8 = - f6 - 2 • f4 := by      rw [← sub_zero f8, ← f1_add_f2_eq_zero]      abel    simp_all  case' bottomYukawa =>    obtain rfl : f6 = - f2 - f4 := by      rw [← sub_zero f2, ← f1_add_f2_eq_zero]      abel    simp_all  -- AllowsTerm  case W3 =>    use (- f6 - 2 • f4), f6    simpa using f1_add_f2_eq_zero  case W1 | W2 =>    use f4, f6, f8    simp only [true_or, or_true, and_self, true_and]    abel  case K1 =>    obtain rfl : f6 = - f2 - f4 := by      rw [← sub_zero f2, ← f1_add_f2_eq_zero]      abel    simp_all    use (-f2 - f4), f4    simp  case' topYukawa =>    obtain rfl : f2 = - f4 - f6 := by      rw [← sub_zero f2, ← f1_add_f2_eq_zero]      abel    simp_all  case topYukawa | Λ =>    use f6, f4    simp only [or_true, true_or, and_self, true_and]    abel  case W4 =>    apply And.intro    · rw [← sub_zero f8, ← f1_add_f2_eq_zero]      abel    · abel  case μ =>    rw [← sub_zero f2, ← f1_add_f2_eq_zero]    abel