diff --git a/PhysLean/Particles/SuperSymmetry/SU5/Charges/AllowsTerm.lean b/PhysLean/Particles/SuperSymmetry/SU5/Charges/AllowsTerm.lean
index e7507bd00..e77220c25 100644
--- a/PhysLean/Particles/SuperSymmetry/SU5/Charges/AllowsTerm.lean
+++ b/PhysLean/Particles/SuperSymmetry/SU5/Charges/AllowsTerm.lean
@@ -25,19 +25,22 @@ namespace SU5
 
 namespace Charges
 
+variable {𝓩 : Type} [AddCommGroup 𝓩]
+
 /-- The charges of representations `x : Charges` allow a potential term `T : PotentialTerm`
 if the zero charge is in the set of charges associated with that potential term. -/
-def AllowsTerm (x : Charges) (T : PotentialTerm) : Prop := 0 ∈ ofPotentialTerm x T
+def AllowsTerm (x : Charges 𝓩) (T : PotentialTerm) : Prop := 0 ∈ ofPotentialTerm x T
 
-lemma allowsTerm_iff_zero_mem_ofPotentialTerm' {x : Charges} {T : PotentialTerm} :
+lemma allowsTerm_iff_zero_mem_ofPotentialTerm' [DecidableEq 𝓩]
+    {x : Charges 𝓩} {T : PotentialTerm} :
     x.AllowsTerm T ↔ 0 ∈ x.ofPotentialTerm' T := by
   rw [AllowsTerm]
   exact mem_ofPotentialTerm_iff_mem_ofPotentialTerm
 
-instance (x : Charges) (T : PotentialTerm) : Decidable (x.AllowsTerm T) :=
+instance [DecidableEq 𝓩] (x : Charges 𝓩) (T : PotentialTerm) : Decidable (x.AllowsTerm T) :=
   decidable_of_iff (0 ∈ x.ofPotentialTerm' T) allowsTerm_iff_zero_mem_ofPotentialTerm'.symm
 
-lemma allowsTerm_mono {T : PotentialTerm} {y x : Charges}
+lemma allowsTerm_mono {T : PotentialTerm} {y x : Charges 𝓩}
     (h : y ⊆ x) (hy : y.AllowsTerm T) : x.AllowsTerm T := ofPotentialTerm_mono h T hy
 
 /-!
@@ -50,86 +53,86 @@ lemma allowsTerm_mono {T : PotentialTerm} {y x : Charges}
   Defined such that `allowsTermForm a b c T` always allows the potential term `T`,
   and if any over charge `x` allows `T` then it is due to a subset of the form
   `allowsTermForm a b c T`. -/
-def allowsTermForm (a b c : ℤ) : (T : PotentialTerm) → Charges
+def allowsTermForm [DecidableEq 𝓩] (a b c : 𝓩) : (T : PotentialTerm) → Charges 𝓩
   | .μ => (some a, some a, ∅, ∅)
   | .β => (none, some a, {a}, ∅)
   | .Λ => (none, none, {a, b}, {- a - b})
   | .W1 => (none, none, {- a - b - c}, {a, b, c})
   | .W2 => (some (- a - b - c), none, ∅, {a, b, c})
-  | .W3 => (none, some (- a), {b, - b - 2 * a}, ∅)
-  | .W4 => (some (- c - 2 * b), some (- b), {c}, ∅)
+  | .W3 => (none, some (- a), {b, - b - 2 • a}, ∅)
+  | .W4 => (some (- c - 2 • b), some (- b), {c}, ∅)
   | .K1 => (none, none, {-a}, {b, - a - b})
   | .K2 => (some a, some b, ∅, {- a - b})
   | .topYukawa => (none, some (-a), ∅, {b, - a - b})
   | .bottomYukawa => (some a, none, {b}, {- a - b})
 
-lemma allowsTermForm_allowsTerm {a b c : ℤ} {T : PotentialTerm} :
+lemma allowsTermForm_allowsTerm [DecidableEq 𝓩] {a b c : 𝓩} {T : PotentialTerm} :
     (allowsTermForm a b c T).AllowsTerm T := by
   simp [AllowsTerm, ofPotentialTerm, allowsTermForm]
   cases T
   all_goals
     simp [PotentialTerm.toFieldLabel, ofFieldLabel, ofPotentialTerm]
-  any_goals omega
-  case' Λ =>
+  case Λ =>
     use a + b
     simp only [add_add_sub_cancel, add_neg_cancel, and_true]
     use a, b
     simp only [or_true, and_true]
     use 0, a
     simp
-  case' W3 =>
-    use - 2 * a
-    apply And.intro ?_ (by omega)
-    use b, -b - 2 * a
-    apply And.intro ?_ (by omega)
+  case W3 =>
+    use - 2 • a
+    apply And.intro ?_ (by abel)
+    use b, -b - 2 • a
+    apply And.intro ?_ (by abel)
     simp only [or_true, and_true]
     use 0, b
     simp
-  case' K1 =>
+  case K1 =>
     use - a
-    apply And.intro ?_ (by omega)
+    apply And.intro ?_ (by abel)
     use b, - a - b
-    apply And.intro ?_ (by omega)
+    apply And.intro ?_ (by abel)
     simp only [or_true, and_true]
     use 0, b
     simp
-  case' topYukawa =>
+  case topYukawa =>
     use - a
-    apply And.intro ?_ (by omega)
+    apply And.intro ?_ (by abel)
     use b, - a - b
-    apply And.intro ?_ (by omega)
+    apply And.intro ?_ (by abel)
     simp only [or_true, and_true]
     use 0, b
     simp
-  case' W1 =>
+  case W1 =>
     use a + b + c
-    apply And.intro ?_ (by omega)
+    apply And.intro ?_ (by abel)
     use a + b, c
-    apply And.intro ?_ (by omega)
+    apply And.intro ?_ (by abel)
     simp only [or_true, and_true]
     use a, b
     simp only [true_or, or_true, and_true]
     use 0, a
     simp
-  case' W2 =>
+  case W2 =>
     use a + b + c
-    apply And.intro ?_ (by omega)
+    apply And.intro ?_ (by abel)
     use a + b, c
-    apply And.intro ?_ (by omega)
+    apply And.intro ?_ (by abel)
     simp only [or_true, and_true]
     use a, b
     simp only [true_or, or_true, and_true]
     use 0, a
     simp
+  all_goals abel
 
-lemma allowsTerm_of_eq_allowsTermForm {T : PotentialTerm}
-    (x : Charges) (h : ∃ a b c, x = allowsTermForm a b c T) :
+lemma allowsTerm_of_eq_allowsTermForm [DecidableEq 𝓩] {T : PotentialTerm}
+    (x : Charges 𝓩) (h : ∃ a b c, x = allowsTermForm a b c T) :
     x.AllowsTerm T := by
   obtain ⟨a, b, c, rfl⟩ := h
   exact allowsTermForm_allowsTerm
 open PotentialTerm in
 
-lemma allowsTermForm_eq_of_subset {a b c a' b' c' : ℤ} {T : PotentialTerm}
+lemma allowsTermForm_eq_of_subset [DecidableEq 𝓩] {a b c a' b' c' : 𝓩} {T : PotentialTerm}
     (h : allowsTermForm a b c T ⊆ allowsTermForm a' b' c' T) (hT : T ≠ W1 ∧ T ≠ W2) :
     allowsTermForm a b c T = allowsTermForm a' b' c' T := by
   cases T
@@ -162,7 +165,7 @@ lemma allowsTermForm_eq_of_subset {a b c a' b' c' : ℤ} {T : PotentialTerm}
     obtain ⟨rfl | rfl, h1 | h2⟩ := h2
     all_goals simp_all [Finset.pair_comm]
 
-lemma allowsTermForm_card_le_degree {a b c : ℤ} {T : PotentialTerm} :
+lemma allowsTermForm_card_le_degree [DecidableEq 𝓩] {a b c : 𝓩} {T : PotentialTerm} :
     (allowsTermForm a b c T).card ≤ T.degree := by
   cases T
   all_goals
@@ -172,7 +175,7 @@ lemma allowsTermForm_card_le_degree {a b c : ℤ} {T : PotentialTerm} :
     have h1 : Finset.card {a, b} ≤ 2 := Finset.card_le_two
     omega
   case' W3 =>
-    have h1 : Finset.card {b, -b - 2 * a} ≤ 2 := Finset.card_le_two
+    have h1 : Finset.card {b, -b - 2 • a} ≤ 2 := Finset.card_le_two
     omega
   case' K1 =>
     have h1 : Finset.card {b, -a - b} ≤ 2 := Finset.card_le_two
@@ -184,8 +187,8 @@ lemma allowsTermForm_card_le_degree {a b c : ℤ} {T : PotentialTerm} :
     have h1 : Finset.card {a, b, c} ≤ 3 := Finset.card_le_three
     omega
 
-lemma allowsTermForm_subset_allowsTerm_of_allowsTerm {T : PotentialTerm} {x : Charges}
-    (h : x.AllowsTerm T) :
+lemma allowsTermForm_subset_allowsTerm_of_allowsTerm [DecidableEq 𝓩]
+    {T : PotentialTerm} {x : Charges 𝓩} (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
@@ -216,77 +219,100 @@ lemma allowsTermForm_subset_allowsTerm_of_allowsTerm {T : PotentialTerm} {x : Ch
     simp [AllowsTerm, ofPotentialTerm, PotentialTerm.toFieldLabel, ofFieldLabel]
   -- Replacements of equalities
   case' W1 | W2 =>
-    have hf2 : f2 = -f4 - f6 - f8 := by omega
+    have hf2 : f2 = -f4 - f6 - f8 := by
+      rw [← sub_zero f2, ← f1_add_f2_eq_zero]
+      abel
     subst hf2
     simp_all
-  case' β =>
-    have hf2 : f4 = - f2 := by omega
+  case β =>
+    have hf2 : f4 = - f2 := by
+      rw [← sub_zero f2, ← f1_add_f2_eq_zero]
+      abel
     subst hf2
     simp_all
-  case' K2 =>
-    have hf2 : f2 = - f4 - f6 := by omega
+  case K2 =>
+    have hf2 : f2 = - f4 - f6 := by
+      rw [← sub_zero f2, ← f1_add_f2_eq_zero]
+      abel
     subst hf2
     simp_all
   case' Λ =>
-    have hf2 : f2 = -f4 - f6 := by omega
+    have hf2 : f2 = -f4 - f6 := by
+      rw [← sub_zero f2, ← f1_add_f2_eq_zero]
+      abel
     subst hf2
     simp_all
   case' W3 =>
     subst f4_mem
-    have hf8 : f8 = - f6 -2 * f4 := by omega
+    have hf8 : f8 = - f6 - 2 • f4 := by
+      rw [← sub_zero f8, ← f1_add_f2_eq_zero]
+      abel
     subst hf8
     simp_all
-  case' bottomYukawa =>
-    have hf6 : f6 = - f2 - f4 := by omega
+  case bottomYukawa =>
+    have hf6 : f6 = - f2 - f4 := by
+      rw [← sub_zero f2, ← f1_add_f2_eq_zero]
+      abel
     subst hf6
     simp_all
   -- AllowsTerm
-  any_goals omega
-  case' W3 =>
-    use (- f6 -2 * f4) + f6
-    apply And.intro ?_ (by omega)
+  case W3 =>
+    use (- f6 - 2 • f4) + f6
+    apply And.intro ?_ (by abel)
     try simp
-    use (- f6 -2 * f4), f6
+    use (- f6 - 2 • f4), f6
     simp only [true_or, and_true]
-    use 0, (- f6 -2 * f4)
+    use 0, (- f6 - 2 • f4)
     simp
-  case' W1 | W2 =>
+  case W1 | W2 =>
     use f8 + f6 + f4
-    apply And.intro ?_ (by omega)
+    apply And.intro ?_ (by abel)
     use f8 + f6, f4
-  case' W1 | W2 =>
-    apply And.intro ?_ (by omega)
+    apply And.intro ?_ (by abel)
     try simp
     use f8, f6
     simp only [true_or, or_true, and_true]
     use 0, f8
     simp
-  case' K1 =>
-    have hf6 : f6 = - f2 - f4 := by omega
+  case K1 =>
+    have hf6 : f6 = - f2 - f4 := by
+      rw [← sub_zero f2, ← f1_add_f2_eq_zero]
+      abel
     subst hf6
     simp_all
     use (-f2 - f4) + f4
-    apply And.intro ?_ (by omega)
+    apply And.intro ?_ (by abel)
     use (-f2 - f4), f4
-    apply And.intro ?_ (by omega)
+    apply And.intro ?_ (by abel)
     simp only [true_or, and_true]
     use 0, (-f2 - f4)
     simp
   case' topYukawa =>
-    have hf2 : f2 = - f4 - f6 := by omega
+    have hf2 : f2 = - f4 - f6 := by
+      rw [← sub_zero f2, ← f1_add_f2_eq_zero]
+      abel
     subst hf2
     simp_all
-  case' topYukawa | Λ =>
+  case topYukawa | Λ =>
     use f6 + f4
-    apply And.intro ?_ (by omega)
+    apply And.intro ?_ (by abel)
     use f6, f4
-    apply And.intro ?_ (by omega)
+    apply And.intro ?_ (by abel)
     simp only [true_or, and_true]
     use 0, f6
     simp
+  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
 
-lemma subset_card_le_degree_allowsTerm_of_allowsTerm {T : PotentialTerm} {x : Charges}
-    (h : x.AllowsTerm T) : ∃ y ∈ x.powerset, y.card ≤ T.degree ∧ y.AllowsTerm T := by
+lemma subset_card_le_degree_allowsTerm_of_allowsTerm [DecidableEq 𝓩] {T : PotentialTerm}
+    {x : Charges 𝓩} (h : x.AllowsTerm T) :
+    ∃ y ∈ x.powerset, y.card ≤ T.degree ∧ y.AllowsTerm T := by
   obtain ⟨a, b, c, h1, h2⟩ := allowsTermForm_subset_allowsTerm_of_allowsTerm h
   use allowsTermForm a b c T
   simp_all
diff --git a/PhysLean/Particles/SuperSymmetry/SU5/Charges/Basic.lean b/PhysLean/Particles/SuperSymmetry/SU5/Charges/Basic.lean
index 67888ba25..89bf9e94d 100644
--- a/PhysLean/Particles/SuperSymmetry/SU5/Charges/Basic.lean
+++ b/PhysLean/Particles/SuperSymmetry/SU5/Charges/Basic.lean
@@ -23,15 +23,22 @@ namespace SU5
   The order of charges is implicitly taken to be `qHd`, `qHu`, `Q5`, `Q10`.
 
   The `Q5` and `Q10` charges are represented by `Finset` rather than
-  `Multiset`, so multiplicity is not included. -/
-def Charges : Type := Option ℤ × Option ℤ × Finset ℤ × Finset ℤ
+  `Multiset`, so multiplicity is not included.
+
+  This is defined for a general type `𝓩`, which could be e.g.
+- `ℤ` in the case  of `U(1)`,
+- `ℤ × ℤ` in the case of `U(1) × U(1)`,
+- `Fin 2` in the case of `ℤ₂` etc -/
+def Charges (𝓩 : Type := ℤ) : Type := Option 𝓩 × Option 𝓩 × Finset 𝓩 × Finset 𝓩
 
 namespace Charges
 
-instance : DecidableEq Charges := inferInstanceAs
-  (DecidableEq (Option ℤ × Option ℤ × Finset ℤ × Finset ℤ))
+variable {𝓩 : Type}
+
+instance [DecidableEq 𝓩] : DecidableEq (Charges 𝓩):= inferInstanceAs
+  (DecidableEq (Option 𝓩 × Option 𝓩 × Finset 𝓩 × Finset 𝓩))
 
-unsafe instance : Repr Charges where
+unsafe instance [Repr 𝓩] : Repr (Charges 𝓩) where
   reprPrec x _ := match x with
     | (qHd, qHu, Q5, Q10) =>
       let s1 := reprStr qHd
@@ -40,11 +47,11 @@ unsafe instance : Repr Charges where
       let s10 := reprStr Q10
       s!"({s1}, {s2}, {s5}, {s10})"
 
-/-- The explicit casting of a term of `Charges` to a term of
-  `Option ℤ × Option ℤ × Finset ℤ × Finset ℤ`. -/
-def toProd (x : Charges) : Option ℤ × Option ℤ × Finset ℤ × Finset ℤ := x
+/-- The explicit casting of a term of `Charges 𝓩` to a term of
+  `Option 𝓩 × Option 𝓩 × Finset 𝓩 × Finset 𝓩`. -/
+def toProd (x : Charges 𝓩) : Option 𝓩 × Option 𝓩 × Finset 𝓩 × Finset 𝓩 := x
 
-lemma eq_of_parts {x y : Charges} (h1 : x.1 = y.1) (h2 : x.2.1 = y.2.1)
+lemma eq_of_parts {x y : Charges 𝓩} (h1 : x.1 = y.1) (h2 : x.2.1 = y.2.1)
     (h3 : x.2.2.1 = y.2.2.1) (h4 : x.2.2.2 = y.2.2.2) : x = y := by
   match x, y with
   | (x1, x2, x3, x4), (y1, y2, y3, y4) =>
@@ -56,23 +63,23 @@ lemma eq_of_parts {x y : Charges} (h1 : x.1 = y.1) (h2 : x.2.1 = y.2.1)
 
 -/
 
-instance hasSubset : HasSubset Charges where
+instance hasSubset : HasSubset (Charges 𝓩) where
   Subset x y := x.1.toFinset ⊆ y.1.toFinset ∧
     x.2.1.toFinset ⊆ y.2.1.toFinset ∧
     x.2.2.1 ⊆ y.2.2.1 ∧
     x.2.2.2 ⊆ y.2.2.2
 
-instance hasSSubset : HasSSubset Charges where
+instance hasSSubset : HasSSubset (Charges 𝓩) where
   SSubset x y := x ⊆ y ∧ x ≠ y
 
-instance subsetDecidable (x y : Charges) : Decidable (x ⊆ y) := instDecidableAnd
+instance subsetDecidable [DecidableEq 𝓩] (x y : Charges 𝓩) : Decidable (x ⊆ y) := instDecidableAnd
 
-lemma subset_def {x y : Charges} : x ⊆ y ↔ x.1.toFinset ⊆ y.1.toFinset ∧
+lemma subset_def {x y : Charges 𝓩} : x ⊆ y ↔ x.1.toFinset ⊆ y.1.toFinset ∧
     x.2.1.toFinset ⊆ y.2.1.toFinset ∧ x.2.2.1 ⊆ y.2.2.1 ∧ x.2.2.2 ⊆ y.2.2.2 := by
   rfl
 
 @[simp, refl]
-lemma subset_refl (x : Charges) : x ⊆ x := by
+lemma subset_refl (x : Charges 𝓩) : x ⊆ x := by
   constructor
   · rfl
   · constructor
@@ -81,7 +88,7 @@ lemma subset_refl (x : Charges) : x ⊆ x := by
       · rfl
       · rfl
 
-lemma _root_.Option.toFinset_inj {x y : Option ℤ} :
+lemma _root_.Option.toFinset_inj {x y : Option 𝓩} :
     x = y ↔ x.toFinset = y.toFinset := by
   match x, y with
   | none, none => simp [Option.toFinset]
@@ -93,10 +100,10 @@ lemma _root_.Option.toFinset_inj {x y : Option ℤ} :
   | some _, none => simp [Option.toFinset]
   | some _, some _ => simp [Option.toFinset]
 
-lemma subset_trans {x y z : Charges} (hxy : x ⊆ y) (hyz : y ⊆ z) : x ⊆ z := by
+lemma subset_trans {x y z : Charges 𝓩} (hxy : x ⊆ y) (hyz : y ⊆ z) : x ⊆ z := by
   simp_all [Subset]
 
-lemma subset_antisymm {x y : Charges} (hxy : x ⊆ y) (hyx : y ⊆ x) : x = y := by
+lemma subset_antisymm {x y : Charges 𝓩} (hxy : x ⊆ y) (hyx : y ⊆ x) : x = y := by
   rw [Subset] at hxy hyx
   dsimp [hasSubset] at hxy hyx
   rcases x with ⟨x1, x2, x3, x4⟩
@@ -114,15 +121,15 @@ lemma subset_antisymm {x y : Charges} (hxy : x ⊆ y) (hyx : y ⊆ x) : x = y :=
 
 -/
 
-instance emptyInst : EmptyCollection Charges where
+instance emptyInst : EmptyCollection (Charges 𝓩) where
   emptyCollection := (none, none, {}, {})
 
 @[simp]
-lemma empty_subset (x : Charges) : ∅ ⊆ x := by
+lemma empty_subset (x : Charges 𝓩) : ∅ ⊆ x := by
   simp [hasSubset, Subset, emptyInst]
 
 @[simp]
-lemma subset_of_empty_iff_empty {x : Charges} :
+lemma subset_of_empty_iff_empty {x : Charges 𝓩} :
     x ⊆ ∅ ↔ x = ∅ := by
   constructor
   · intro h
@@ -134,19 +141,19 @@ lemma subset_of_empty_iff_empty {x : Charges} :
     simp
 
 @[simp]
-lemma empty_qHd : (∅ : Charges).1 = none := by
+lemma empty_qHd : (∅ : Charges 𝓩).1 = none := by
   simp [emptyInst]
 
 @[simp]
-lemma empty_qHu : (∅ : Charges).2.1 = none := by
+lemma empty_qHu : (∅ : Charges 𝓩).2.1 = none := by
   simp [emptyInst]
 
 @[simp]
-lemma empty_Q5 : (∅ : Charges).2.2.1 = ∅ := by
+lemma empty_Q5 : (∅ : Charges 𝓩).2.2.1 = ∅ := by
   simp [emptyInst]
 
 @[simp]
-lemma empty_Q10 : (∅ : Charges).2.2.2 = ∅ := by
+lemma empty_Q10 : (∅ : Charges 𝓩).2.2.2 = ∅ := by
   simp [emptyInst]
 
 /-!
@@ -157,14 +164,14 @@ lemma empty_Q10 : (∅ : Charges).2.2.2 = ∅ := by
 
 /-- The cardinality of a `Charges` is defined to be the sum of the cardinalities
   of each of the underlying finite sets of charges, with `Option ℤ` turned to finsets. -/
-def card (x : Charges) : Nat :=
+def card (x : Charges 𝓩) : Nat :=
   x.1.toFinset.card + x.2.1.toFinset.card + x.2.2.1.card + x.2.2.2.card
 
 @[simp]
-lemma card_empty : card (∅ : Charges) = 0 := by
+lemma card_empty : card (∅ : Charges 𝓩) = 0 := by
   simp [card, emptyInst]
 
-lemma card_mono {x y : Charges} (h : x ⊆ y) : card x ≤ card y := by
+lemma card_mono {x y : Charges 𝓩} (h : x ⊆ y) : card x ≤ card y := by
   simp [card, hasSubset] at h
   have h1 := Finset.card_le_card h.1
   have h2 := Finset.card_le_card h.2.1
@@ -173,7 +180,7 @@ lemma card_mono {x y : Charges} (h : x ⊆ y) : card x ≤ card y := by
   simp [card]
   omega
 
-lemma eq_of_subset_card {x y : Charges} (h : x ⊆ y) (hcard : card x = card y) : x = y := by
+lemma eq_of_subset_card {x y : Charges 𝓩} (h : x ⊆ y) (hcard : card x = card y) : x = y := by
   simp [card] at hcard
   have h1 := Finset.card_le_card h.1
   have h2 := Finset.card_le_card h.2.1
@@ -196,21 +203,24 @@ lemma eq_of_subset_card {x y : Charges} (h : x ⊆ y) (hcard : card x = card y)
   rw [← Option.toFinset_inj] at h1 h2
   simp_all
 
+section powerset
 /-!
 
 ## Powerset
 
 -/
 
-/-- The powerset of `x : Option ℤ` defined as `{none}` if `x` is `none`
+variable [DecidableEq 𝓩]
+
+/-- The powerset of `x : Option 𝓩` defined as `{none}` if `x` is `none`
   and `{none, some y}` is `x` is `some y`. -/
-def _root_.Option.powerset (x : Option ℤ) : Finset (Option ℤ) :=
+def _root_.Option.powerset (x : Option 𝓩) : Finset (Option 𝓩) :=
   match x with
   | none => {none}
   | some x => {none, some x}
 
 @[simp]
-lemma _root_.Option.mem_powerset_iff {x : Option ℤ} (y : Option ℤ) :
+lemma _root_.Option.mem_powerset_iff {x : Option 𝓩} (y : Option 𝓩) :
     y ∈ x.powerset ↔ y.toFinset ⊆ x.toFinset :=
   match x, y with
   | none, none => by
@@ -224,11 +234,11 @@ lemma _root_.Option.mem_powerset_iff {x : Option ℤ} (y : Option ℤ) :
 
 /-- The powerset of a charge . Given a charge `x : Charges`
   it's powerset is the finite set of all `Charges` which are subsets of `x`. -/
-def powerset (x : Charges) : Finset Charges :=
+def powerset [DecidableEq 𝓩] (x : Charges 𝓩) : Finset (Charges 𝓩):=
   x.1.powerset.product <| x.2.1.powerset.product <| x.2.2.1.powerset.product <| x.2.2.2.powerset
 
 @[simp]
-lemma mem_powerset_iff_subset {x y : Charges} :
+lemma mem_powerset_iff_subset {x y : Charges 𝓩} :
     x ∈ powerset y ↔ x ⊆ y := by
   cases x
   cases y
@@ -236,19 +246,19 @@ lemma mem_powerset_iff_subset {x y : Charges} :
   rw [Finset.mem_product]
   simp_all [Subset]
 
-lemma self_mem_powerset (x : Charges) :
+lemma self_mem_powerset (x : Charges 𝓩) :
     x ∈ powerset x := by simp
 
-lemma empty_mem_powerset (x : Charges) :
+lemma empty_mem_powerset (x : Charges 𝓩) :
     ∅ ∈ powerset x := by simp
 
 @[simp]
 lemma powerset_of_empty :
-    powerset ∅ = {∅} := by
+    powerset (∅ : Charges 𝓩) = {∅} := by
   ext x
   simp
 
-lemma powerset_mono {x y : Charges} :
+lemma powerset_mono {x y : Charges 𝓩} :
     powerset x ⊆ powerset y ↔ x ⊆ y := by
   constructor
   · intro h
@@ -260,7 +270,7 @@ lemma powerset_mono {x y : Charges} :
     intro h1
     exact subset_trans h1 h
 
-lemma min_exists_inductive (S : Finset Charges) (hS : S ≠ ∅) :
+lemma min_exists_inductive (S : Finset (Charges 𝓩)) (hS : S ≠ ∅) :
     (n : ℕ) → (hn : S.card = n) →
     ∃ y ∈ S, powerset y ∩ S = {y}
   | 0, h => by simp_all
@@ -325,26 +335,31 @@ lemma min_exists_inductive (S : Finset Charges) (hS : S ≠ ∅) :
         subst hzy
         simp_all
 
-lemma min_exists (S : Finset Charges) (hS : S ≠ ∅) :
+lemma min_exists (S : Finset (Charges 𝓩)) (hS : S ≠ ∅) :
     ∃ y ∈ S, powerset y ∩ S = {y} := min_exists_inductive S hS S.card rfl
 
+end powerset
+
+section ofFinset
 /-!
 
 ## ofFinset
 
 -/
 
-/-- Given `S5 S10 : Finset ℤ` the finite set of charges associated with
+variable [DecidableEq 𝓩]
+
+/-- Given `S5 S10 : Finset 𝓩` the finite set of charges associated with
   for which the 5-bar representation charges sit in `S5` and
   the 10d representation charges sit in `S10`. -/
-def ofFinset (S5 S10 : Finset ℤ) : Finset Charges :=
-  let SqHd := {none} ∪ S5.map ⟨Option.some, Option.some_injective ℤ⟩
-  let SqHu := {none} ∪ S5.map ⟨Option.some, Option.some_injective ℤ⟩
+def ofFinset (S5 S10 : Finset 𝓩) : Finset (Charges 𝓩) :=
+  let SqHd := {none} ∪ S5.map ⟨Option.some, Option.some_injective 𝓩⟩
+  let SqHu := {none} ∪ S5.map ⟨Option.some, Option.some_injective 𝓩⟩
   let SQ5 := S5.powerset
   let SQ10 := S10.powerset
   SqHd.product (SqHu.product (SQ5.product SQ10))
 
-lemma qHd_mem_ofFinset (S5 S10 : Finset ℤ) (z : ℤ) (x2 : Option ℤ × Finset ℤ × Finset ℤ)
+lemma qHd_mem_ofFinset (S5 S10 : Finset 𝓩) (z : 𝓩) (x2 : Option 𝓩 × Finset 𝓩 × Finset 𝓩)
     (hsub : (some z, x2) ∈ ofFinset S5 S10) :
     z ∈ S5 := by
   have hoption (x : Option ℤ) (S : Finset ℤ) :
@@ -360,15 +375,9 @@ lemma qHd_mem_ofFinset (S5 S10 : Finset ℤ) (z : ℤ) (x2 : Option ℤ × Finse
   simp only [Finset.mem_powerset] at hsub
   simp_all
 
-lemma qHu_mem_ofFinset (S5 S10 : Finset ℤ) (z : ℤ) (x1 : Option ℤ) (x2 : Finset ℤ × Finset ℤ)
+lemma qHu_mem_ofFinset (S5 S10 : Finset 𝓩) (z : 𝓩) (x1 : Option 𝓩) (x2 : Finset 𝓩 × Finset 𝓩)
     (hsub : (x1, some z, x2) ∈ ofFinset S5 S10) :
     z ∈ S5 := by
-  have hoption (x : Option ℤ) (S : Finset ℤ) :
-      x ∈ ({none} : Finset (Option ℤ)) ∪ S.map ⟨Option.some, Option.some_injective ℤ⟩ ↔
-      x.toFinset ⊆ S := by
-    match x with
-    | none => simp
-    | some x => simp
   rw [ofFinset] at hsub
   cases x2
   repeat rw [Finset.product_eq_sprod, Finset.mem_product] at hsub
@@ -376,8 +385,8 @@ lemma qHu_mem_ofFinset (S5 S10 : Finset ℤ) (z : ℤ) (x1 : Option ℤ) (x2 : F
   simp only [Finset.mem_powerset] at hsub
   simp_all
 
-lemma mem_ofFinset_Q5_subset (S5 S10 : Finset ℤ)
-    {x : Charges} (hx : x ∈ ofFinset S5 S10) :
+lemma mem_ofFinset_Q5_subset (S5 S10 : Finset 𝓩)
+    {x : Charges 𝓩} (hx : x ∈ ofFinset S5 S10) :
     x.2.2.1 ⊆ S5 := by
   rw [ofFinset] at hx
   cases x
@@ -386,8 +395,8 @@ lemma mem_ofFinset_Q5_subset (S5 S10 : Finset ℤ)
   simp only [Finset.mem_powerset] at hx
   exact hx.2.2.1
 
-lemma mem_ofFinset_Q10_subset (S5 S10 : Finset ℤ)
-    {x : Charges} (hx : x ∈ ofFinset S5 S10) :
+lemma mem_ofFinset_Q10_subset (S5 S10 : Finset 𝓩)
+    {x : Charges 𝓩} (hx : x ∈ ofFinset S5 S10) :
     x.2.2.2 ⊆ S10 := by
   rw [ofFinset] at hx
   cases x
@@ -396,11 +405,11 @@ lemma mem_ofFinset_Q10_subset (S5 S10 : Finset ℤ)
   simp only [Finset.mem_powerset] at hx
   exact hx.2.2.2
 
-lemma mem_ofFinset_antitone (S5 S10 : Finset ℤ)
-    {x y : Charges} (h : x ⊆ y) (hy : y ∈ ofFinset S5 S10) :
+lemma mem_ofFinset_antitone (S5 S10 : Finset 𝓩)
+    {x y : Charges 𝓩} (h : x ⊆ y) (hy : y ∈ ofFinset S5 S10) :
     x ∈ ofFinset S5 S10 := by
-  have hoption (x : Option ℤ) (S : Finset ℤ) :
-      x ∈ ({none} : Finset (Option ℤ)) ∪ S.map ⟨Option.some, Option.some_injective ℤ⟩ ↔
+  have hoption (x : Option 𝓩) (S : Finset 𝓩) :
+      x ∈ ({none} : Finset (Option 𝓩)) ∪ S.map ⟨Option.some, Option.some_injective 𝓩⟩ ↔
       x.toFinset ⊆ S := by
     match x with
     | none => simp
@@ -416,13 +425,13 @@ lemma mem_ofFinset_antitone (S5 S10 : Finset ℤ)
   simp only [hoption, Finset.mem_powerset] at hy ⊢
   exact ⟨h.1.trans hy.1, h.2.1.trans hy.2.1, h.2.2.1.trans hy.2.2.1, h.2.2.2.trans hy.2.2.2⟩
 
-lemma mem_ofFinset_iff {S5 S10 : Finset ℤ} {x : Charges} :
+lemma mem_ofFinset_iff {S5 S10 : Finset 𝓩} {x : Charges 𝓩} :
     x ∈ ofFinset S5 S10 ↔ x.1.toFinset ⊆ S5 ∧ x.2.1.toFinset ⊆ S5 ∧
       x.2.2.1 ⊆ S5 ∧ x.2.2.2 ⊆ S10 := by
   match x with
   | (qHd, qHu, Q5, Q10) =>
-  have hoption (x : Option ℤ) (S : Finset ℤ) :
-      x ∈ ({none} : Finset (Option ℤ)) ∪ S.map ⟨Option.some, Option.some_injective ℤ⟩ ↔
+  have hoption (x : Option 𝓩) (S : Finset 𝓩) :
+      x ∈ ({none} : Finset (Option 𝓩)) ∪ S.map ⟨Option.some, Option.some_injective 𝓩⟩ ↔
       x.toFinset ⊆ S := by
     match x with
     | none => simp
@@ -432,13 +441,15 @@ lemma mem_ofFinset_iff {S5 S10 : Finset ℤ} {x : Charges} :
   rw [hoption, hoption]
   simp
 
-lemma ofFinset_subset_of_subset {S5 S5' S10 S10' : Finset ℤ}
+lemma ofFinset_subset_of_subset {S5 S5' S10 S10' : Finset 𝓩}
     (h5 : S5 ⊆ S5') (h10 : S10 ⊆ S10') :
     ofFinset S5 S10 ⊆ ofFinset S5' S10' := by
   intro x hx
   rw [mem_ofFinset_iff] at hx ⊢
   exact ⟨hx.1.trans h5, hx.2.1.trans h5, hx.2.2.1.trans h5, hx.2.2.2.trans h10⟩
 
+end ofFinset
+
 end Charges
 
 end SU5
diff --git a/PhysLean/Particles/SuperSymmetry/SU5/Charges/Completions.lean b/PhysLean/Particles/SuperSymmetry/SU5/Charges/Completions.lean
index 3480d1ca8..c8fd02872 100644
--- a/PhysLean/Particles/SuperSymmetry/SU5/Charges/Completions.lean
+++ b/PhysLean/Particles/SuperSymmetry/SU5/Charges/Completions.lean
@@ -25,6 +25,7 @@ namespace SU5
 
 namespace Charges
 
+variable {𝓩 : Type}
 /-!
 
 ## Completions
@@ -32,17 +33,17 @@ namespace Charges
 -/
 
 /-- A collection of charges is complete if it has all types of fields. -/
-def IsComplete (x : Charges) : Prop :=
+def IsComplete (x : Charges 𝓩) : Prop :=
   x.1.isSome ∧ x.2.1.isSome ∧ x.2.2.1 ≠ ∅ ∧ x.2.2.2 ≠ ∅
 
-instance (x : Charges) : Decidable (IsComplete x) :=
+instance [DecidableEq 𝓩] (x : Charges 𝓩) : Decidable (IsComplete x) :=
   inferInstanceAs (Decidable (x.1.isSome ∧ x.2.1.isSome ∧ x.2.2.1 ≠ ∅ ∧ x.2.2.2 ≠ ∅))
 
 @[simp]
-lemma not_isComplete_empty : ¬ IsComplete ∅ := by
+lemma not_isComplete_empty : ¬ IsComplete (∅ : Charges 𝓩) := by
   simp [IsComplete]
 
-lemma isComplete_mono {x y : Charges} (h : x ⊆ y) (hx : IsComplete x) :
+lemma isComplete_mono {x y : Charges 𝓩} (h : x ⊆ y) (hx : IsComplete x) :
     IsComplete y := by
   simp [IsComplete] at *
   rw [subset_def] at h
@@ -76,17 +77,19 @@ Note the completions are not monotonic with respect to the subset relation.
 
 -/
 
+variable [DecidableEq 𝓩]
+
 /-- Given a collection of charges `x` in `ofFinset S5 S10`,
   the minimimal charges `y` in `ofFinset S5 S10` which are a super sets of `x` and are
   complete. -/
-def completions (S5 S10 : Finset ℤ) (x : Charges) : Multiset Charges :=
+def completions [DecidableEq 𝓩] (S5 S10 : Finset 𝓩) (x : Charges 𝓩) : Multiset (Charges 𝓩) :=
   let SqHd := if x.1.isSome then {x.1} else S5.val.map fun y => some y
   let SqHu := if x.2.1.isSome then {x.2.1} else S5.val.map fun y => some y
   let SQ5 := if x.2.2.1 ≠ ∅ then {x.2.2.1} else S5.val.map fun y => {y}
   let SQ10 := if x.2.2.2 ≠ ∅ then {x.2.2.2} else S10.val.map fun y => {y}
   (SqHd.product (SqHu.product (SQ5.product SQ10)))
 
-lemma completions_eq_singleton_of_complete {S5 S10 : Finset ℤ} (x : Charges)
+lemma completions_eq_singleton_of_complete {S5 S10 : Finset 𝓩} (x : Charges 𝓩)
     (hcomplete : IsComplete x) :
     completions S5 S10 x = {x} := by
   simp [completions]
@@ -103,7 +106,7 @@ lemma completions_eq_singleton_of_complete {S5 S10 : Finset ℤ} (x : Charges)
   rfl
 
 @[simp]
-lemma self_mem_completions_iff_isComplete {S5 S10 : Finset ℤ} (x : Charges) :
+lemma self_mem_completions_iff_isComplete {S5 S10 : Finset 𝓩} (x : Charges 𝓩) :
     x ∈ completions S5 S10 x ↔ IsComplete x := by
   simp [completions, IsComplete]
   repeat rw [Multiset.mem_product]
@@ -117,7 +120,7 @@ lemma self_mem_completions_iff_isComplete {S5 S10 : Finset ℤ} (x : Charges) :
   case' neg => simp_all
   simp_all
 
-lemma mem_completions_isComplete {S5 S10 : Finset ℤ} {x y : Charges}
+lemma mem_completions_isComplete {S5 S10 : Finset 𝓩} {x y : Charges 𝓩}
     (hx : y ∈ completions S5 S10 x) : IsComplete y := by
   match y with
   | (qHd, qHu, Q5, Q10) =>
@@ -154,7 +157,7 @@ lemma mem_completions_isComplete {S5 S10 : Finset ℤ} {x y : Charges}
       obtain ⟨a, h, rfl⟩ := hx.2.2.2
       simp
 
-lemma self_subset_mem_completions (S5 S10 : Finset ℤ) (x y : Charges)
+lemma self_subset_mem_completions (S5 S10 : Finset 𝓩) (x y : Charges 𝓩)
     (hy : y ∈ completions S5 S10 x) : x ⊆ y := by
   simp [completions] at hy
   repeat rw [Multiset.mem_product] at hy
@@ -174,7 +177,7 @@ lemma self_subset_mem_completions (S5 S10 : Finset ℤ) (x y : Charges)
     · simp_all
     · simp_all
 
-lemma exist_completions_subset_of_complete (S5 S10 : Finset ℤ) (x y : Charges)
+lemma exist_completions_subset_of_complete (S5 S10 : Finset 𝓩) (x y : Charges 𝓩)
     (hsubset : x ⊆ y) (hy : y ∈ ofFinset S5 S10) (hycomplete : IsComplete y) :
     ∃ z ∈ completions S5 S10 x, z ⊆ y := by
   by_cases hx : IsComplete x
diff --git a/PhysLean/Particles/SuperSymmetry/SU5/Charges/MinimalSuperSet.lean b/PhysLean/Particles/SuperSymmetry/SU5/Charges/MinimalSuperSet.lean
index 453aeff27..5278c4d5c 100644
--- a/PhysLean/Particles/SuperSymmetry/SU5/Charges/MinimalSuperSet.lean
+++ b/PhysLean/Particles/SuperSymmetry/SU5/Charges/MinimalSuperSet.lean
@@ -20,16 +20,17 @@ namespace SU5
 
 namespace Charges
 
+variable {𝓩 : Type} [DecidableEq 𝓩]
 /-- Given a collection of charges `x` in `ofFinset S5 S10`,
   the minimimal charges `y` in `ofFinset S5 S10` which are a super sets of `x`. -/
-def minimalSuperSet (S5 S10 : Finset ℤ) (x : Charges) : Finset Charges :=
+def minimalSuperSet (S5 S10 : Finset 𝓩) (x : Charges 𝓩) : Finset (Charges 𝓩) :=
   let SqHd := if x.1.isSome then ∅ else S5.val.map fun y => (some y, x.2)
   let SqHu := if x.2.1.isSome then ∅ else S5.val.map fun y => (x.1, some y, x.2.2)
   let SQ5 := S5.val.map (fun y => (x.1, x.2.1, insert y x.2.2.1, x.2.2.2))
   let SQ10 := S10.val.map (fun y => (x.1, x.2.1, x.2.2.1, insert y x.2.2.2))
   (SqHd ∪ SqHu ∪ SQ5 ∪ SQ10).toFinset.erase x
 
-lemma self_subset_mem_minimalSuperSet (S5 S10 : Finset ℤ) (x y : Charges)
+lemma self_subset_mem_minimalSuperSet (S5 S10 : Finset 𝓩) (x y : Charges 𝓩)
     (hy : y ∈ minimalSuperSet S5 S10 x) : x ⊆ y := by
   simp [minimalSuperSet] at hy
   rcases hy with ⟨hy1, hr | hr | hr | hr⟩
@@ -63,18 +64,18 @@ lemma self_subset_mem_minimalSuperSet (S5 S10 : Finset ℤ) (x y : Charges)
       simp [hasSubset]
 
 @[simp]
-lemma self_not_mem_minimalSuperSet (S5 S10 : Finset ℤ) (x : Charges) :
+lemma self_not_mem_minimalSuperSet (S5 S10 : Finset 𝓩) (x : Charges 𝓩) :
     x ∉ minimalSuperSet S5 S10 x := by
   simp [minimalSuperSet]
 
-lemma self_neq_mem_minimalSuperSet (S5 S10 : Finset ℤ) (x y : Charges)
+lemma self_neq_mem_minimalSuperSet (S5 S10 : Finset 𝓩) (x y : Charges 𝓩)
     (hy : y ∈ minimalSuperSet S5 S10 x) : x ≠ y := by
   by_contra h
   subst h
   simp at hy
 
-lemma card_of_mem_minimalSuperSet {S5 S10 : Finset ℤ} {x : Charges}
-    (y : Charges) (hy : y ∈ minimalSuperSet S5 S10 x) :
+lemma card_of_mem_minimalSuperSet {S5 S10 : Finset 𝓩} {x : Charges 𝓩}
+    (y : Charges 𝓩) (hy : y ∈ minimalSuperSet S5 S10 x) :
     card y = card x + 1 := by
   simp [minimalSuperSet] at hy
   rcases hy with ⟨hy1, hr | hr | hr | hr⟩
@@ -115,8 +116,8 @@ lemma card_of_mem_minimalSuperSet {S5 S10 : Finset ℤ} {x : Charges}
       rw [Finset.insert_eq_of_mem h] at hy1
       simp at hy1
 
-lemma insert_Q5_mem_minimalSuperSet {S5 S10 : Finset ℤ} {x : Charges}
-    (z : ℤ) (hz : z ∈ S5) (hznot : z ∉ x.2.2.1) :
+lemma insert_Q5_mem_minimalSuperSet {S5 S10 : Finset 𝓩} {x : Charges 𝓩}
+    (z : 𝓩) (hz : z ∈ S5) (hznot : z ∉ x.2.2.1) :
     (x.1, x.2.1, insert z x.2.2.1, x.2.2.2) ∈ minimalSuperSet S5 S10 x := by
   simp [minimalSuperSet]
   match x with
@@ -128,8 +129,8 @@ lemma insert_Q5_mem_minimalSuperSet {S5 S10 : Finset ℤ} {x : Charges}
     left
     use z
 
-lemma insert_Q10_mem_minimalSuperSet {S5 S10 : Finset ℤ} {x : Charges}
-    (z : ℤ) (hz : z ∈ S10) (hznot : z ∉ x.2.2.2) :
+lemma insert_Q10_mem_minimalSuperSet {S5 S10 : Finset 𝓩} {x : Charges 𝓩}
+    (z : 𝓩) (hz : z ∈ S10) (hznot : z ∉ x.2.2.2) :
     (x.1, x.2.1, x.2.2.1, insert z x.2.2.2) ∈ minimalSuperSet S5 S10 x := by
   simp [minimalSuperSet]
   match x with
@@ -141,17 +142,17 @@ lemma insert_Q10_mem_minimalSuperSet {S5 S10 : Finset ℤ} {x : Charges}
     right
     use z
 
-lemma some_qHd_mem_minimalSuperSet_of_none {S5 S10 : Finset ℤ} {x2 : Option ℤ × Finset ℤ × Finset ℤ}
-    (z : ℤ) (hz : z ∈ S5) :
+lemma some_qHd_mem_minimalSuperSet_of_none {S5 S10 : Finset 𝓩}
+    {x2 : Option 𝓩 × Finset 𝓩 × Finset 𝓩} (z : 𝓩) (hz : z ∈ S5) :
     (some z, x2) ∈ minimalSuperSet S5 S10 (none, x2) := by
   simp_all [minimalSuperSet]
 
-lemma some_qHu_mem_minimalSuperSet_of_none {S5 S10 : Finset ℤ}
-    {x1 : Option ℤ} {x2 : Finset ℤ × Finset ℤ} (z : ℤ) (hz : z ∈ S5) :
+lemma some_qHu_mem_minimalSuperSet_of_none {S5 S10 : Finset 𝓩}
+    {x1 : Option 𝓩} {x2 : Finset 𝓩 × Finset 𝓩} (z : 𝓩) (hz : z ∈ S5) :
     (x1, some z, x2) ∈ minimalSuperSet S5 S10 (x1, none, x2) := by
   simp_all [minimalSuperSet]
 
-lemma exists_minimalSuperSet (S5 S10 : Finset ℤ) {x y : Charges}
+lemma exists_minimalSuperSet (S5 S10 : Finset 𝓩) {x y : Charges 𝓩}
     (hy : y ∈ ofFinset S5 S10) (hsubset : x ⊆ y)
     (hxneqy : x ≠ y) : ∃ z ∈ minimalSuperSet S5 S10 x, z ⊆ y := by
   rw [Subset] at hsubset
@@ -229,10 +230,10 @@ lemma exists_minimalSuperSet (S5 S10 : Finset ℤ) {x y : Charges}
   | some x1, some y1, some x2, some y2 =>
     simp_all
 
-lemma minimalSuperSet_induction_on_inductive {S5 S10 : Finset ℤ}
-    (p : Charges → Prop) (hp : (x : Charges) → p x → ∀ y ∈ minimalSuperSet S5 S10 x, p y)
-    (x : Charges) (hbase : p x)
-    (y : Charges) (hy : y ∈ ofFinset S5 S10) (hsubset : x ⊆ y) :
+lemma minimalSuperSet_induction_on_inductive {S5 S10 : Finset 𝓩}
+    (p : Charges 𝓩 → Prop) (hp : (x : Charges 𝓩) → p x → ∀ y ∈ minimalSuperSet S5 S10 x, p y)
+    (x : Charges 𝓩) (hbase : p x)
+    (y : Charges 𝓩) (hy : y ∈ ofFinset S5 S10) (hsubset : x ⊆ y) :
     (n : ℕ) → (hn : n = y.card - x.card) → p y
   | 0, hn => by
     have hxy : x = y := by
diff --git a/PhysLean/Particles/SuperSymmetry/SU5/Charges/MinimallyAllowsTerm/Basic.lean b/PhysLean/Particles/SuperSymmetry/SU5/Charges/MinimallyAllowsTerm/Basic.lean
index 3dd12e66b..401837551 100644
--- a/PhysLean/Particles/SuperSymmetry/SU5/Charges/MinimallyAllowsTerm/Basic.lean
+++ b/PhysLean/Particles/SuperSymmetry/SU5/Charges/MinimallyAllowsTerm/Basic.lean
@@ -21,15 +21,17 @@ namespace Charges
 
 open SuperSymmetry.SU5
 
+variable {𝓩 : Type} [AddCommGroup 𝓩] [DecidableEq 𝓩]
+
 /-- A collection of charges `x : Charges` is said to minimally allow
   the potential term `T` if it allows `T` and no strict subset of it allows `T`. -/
-def MinimallyAllowsTerm (x : Charges) (T : PotentialTerm) : Prop :=
+def MinimallyAllowsTerm (x : Charges 𝓩) (T : PotentialTerm) : Prop :=
   ∀ y ∈ x.powerset, y = x ↔ y.AllowsTerm T
 
-instance (x : Charges) (T : PotentialTerm) : Decidable (x.MinimallyAllowsTerm T) :=
+instance (x : Charges 𝓩) (T : PotentialTerm) : Decidable (x.MinimallyAllowsTerm T) :=
   inferInstanceAs (Decidable (∀ y ∈ powerset x, y = x ↔ y.AllowsTerm T))
 
-variable {T : PotentialTerm} {x : Charges}
+variable {T : PotentialTerm} {x : Charges 𝓩}
 
 lemma allowsTerm_of_minimallyAllowsTerm (h : x.MinimallyAllowsTerm T) : x.AllowsTerm T := by
   simp only [MinimallyAllowsTerm] at h
@@ -143,7 +145,7 @@ lemma eq_allowsTermForm_of_minimallyAllowsTerm (h1 : x.MinimallyAllowsTerm T) :
   exact hy.symm
 
 open PotentialTerm in
-lemma allowsTermForm_minimallyAllowsTerm {a b c : ℤ} {T : PotentialTerm}
+lemma allowsTermForm_minimallyAllowsTerm {a b c : 𝓩} {T : PotentialTerm}
     (hT : T ≠ W1 ∧ T ≠ W2) :
     MinimallyAllowsTerm (allowsTermForm a b c T) T := by
   simp [MinimallyAllowsTerm]
diff --git a/PhysLean/Particles/SuperSymmetry/SU5/Charges/MinimallyAllowsTerm/OfFinset.lean b/PhysLean/Particles/SuperSymmetry/SU5/Charges/MinimallyAllowsTerm/OfFinset.lean
index eda260ab3..006e01971 100644
--- a/PhysLean/Particles/SuperSymmetry/SU5/Charges/MinimallyAllowsTerm/OfFinset.lean
+++ b/PhysLean/Particles/SuperSymmetry/SU5/Charges/MinimallyAllowsTerm/OfFinset.lean
@@ -27,14 +27,15 @@ namespace Charges
 ## Auxillary results: Multisets from Finsets of given cardinality.
 
 -/
+variable {𝓩 : Type}
 
 /-- The multisets of cardinality `1` containing elements from a finite set `s`. -/
-def toMultisetsOne (s : Finset ℤ) : Multiset (Multiset ℤ) :=
+def toMultisetsOne (s : Finset 𝓩) : Multiset (Multiset 𝓩) :=
   let X1 := (s.powersetCard 1).val.map fun X => X.val
   X1
 
 @[simp]
-lemma mem_toMultisetsOne_iff {s : Finset ℤ} (X : Multiset ℤ) :
+lemma mem_toMultisetsOne_iff [DecidableEq 𝓩] {s : Finset 𝓩} (X : Multiset 𝓩) :
     X ∈ toMultisetsOne s ↔ X.toFinset ⊆ s ∧ X.card = 1 := by
   simp [toMultisetsOne]
   intro h
@@ -43,13 +44,13 @@ lemma mem_toMultisetsOne_iff {s : Finset ℤ} (X : Multiset ℤ) :
   simp
 
 /-- The multisets of cardinality `2` containing elements from a finite set `s`. -/
-def toMultisetsTwo (s : Finset ℤ) : Multiset (Multiset ℤ) :=
+def toMultisetsTwo (s : Finset 𝓩) : Multiset (Multiset 𝓩) :=
   let X1 := (s.powersetCard 1).val.map (fun X => X.val.bind (fun x => Multiset.replicate 2 x))
   let X2 := (s.powersetCard 2).val.map fun X => X.val
   X1 + X2
 
 @[simp]
-lemma mem_toMultisetsTwo_iff {s : Finset ℤ} (X : Multiset ℤ) :
+lemma mem_toMultisetsTwo_iff [DecidableEq 𝓩] {s : Finset 𝓩} (X : Multiset 𝓩) :
     X ∈ toMultisetsTwo s ↔ X.toFinset ⊆ s ∧ X.card = 2 := by
   simp [toMultisetsTwo]
   constructor
@@ -79,14 +80,14 @@ lemma mem_toMultisetsTwo_iff {s : Finset ℤ} (X : Multiset ℤ) :
       · exact Multiset.dedup_subset'.mp hsub
 
 /-- The multisets of cardinality `3` containing elements from a finite set `s`. -/
-def toMultisetsThree (s : Finset ℤ) : Multiset (Multiset ℤ) :=
+def toMultisetsThree [DecidableEq 𝓩] (s : Finset 𝓩) : Multiset (Multiset 𝓩) :=
   let X1 := (s.powersetCard 1).val.map (fun X => X.val.bind (fun x => Multiset.replicate 3 x))
   let X2 := s.val.bind (fun x => (s \ {x}).val.map (fun y => {x} + Multiset.replicate 2 y))
   let X3 := (s.powersetCard 3).val.map fun X => X.val
   X1 + X2 + X3
 
 @[simp]
-lemma mem_toMultisetsThree_iff {s : Finset ℤ} (X : Multiset ℤ) :
+lemma mem_toMultisetsThree_iff [DecidableEq 𝓩] {s : Finset 𝓩} (X : Multiset 𝓩) :
     X ∈ toMultisetsThree s ↔ X.toFinset ⊆ s ∧ X.card = 3 := by
   simp [toMultisetsThree]
   constructor
@@ -153,13 +154,12 @@ lemma mem_toMultisetsThree_iff {s : Finset ℤ} (X : Multiset ℤ) :
           simp_all
           use b
           apply And.intro
-          · refine (Multiset.mem_erase_of_ne (by omega)).mpr ?_
+          · refine (Multiset.mem_erase_of_ne (fun h => hac h.symm)).mpr ?_
             simp_all
           exact Multiset.cons_swap b a {b}
         · right
           refine (Multiset.le_iff_subset ?_).mpr ?_
-          · simp
-            omega
+          · simpa using ⟨⟨hab, hac⟩, hbc⟩
           · exact Multiset.dedup_subset'.mp hsub
 /-!
 
@@ -167,10 +167,10 @@ lemma mem_toMultisetsThree_iff {s : Finset ℤ} (X : Multiset ℤ) :
 -/
 
 open PotentialTerm
-
+variable {𝓩 : Type} [DecidableEq 𝓩] [AddCommGroup 𝓩]
 /-- The multiset of all charges within `ofFinset S5 S10` which minimally allow the
   potential term `T`. -/
-def minimallyAllowsTermsOfFinset (S5 S10 : Finset ℤ) : (T : PotentialTerm) → Multiset Charges
+def minimallyAllowsTermsOfFinset (S5 S10 : Finset 𝓩) : (T : PotentialTerm) → Multiset (Charges 𝓩)
   | μ =>
     let SqHd := S5.val
     let SqHu := S5.val
@@ -195,13 +195,13 @@ def minimallyAllowsTermsOfFinset (S5 S10 : Finset ℤ) : (T : PotentialTerm) →
     let SqHu := S5.val
     let Q5 := toMultisetsOne S5
     let prod := SqHd.product (SqHu.product Q5)
-    let Filt := prod.filter (fun x => x.1 - 2 * x.2.1 + x.2.2.sum = 0)
+    let Filt := prod.filter (fun x => x.1 - 2 • x.2.1 + x.2.2.sum = 0)
     (Filt.map (fun x => (x.1, x.2.1, x.2.2.toFinset, ∅)))
   | W3 =>
     let SqHu := S5.val
     let Q5 := toMultisetsTwo S5
     let prod := SqHu.product Q5
-    let Filt := prod.filter (fun x => - 2 * x.1 + x.2.sum = 0)
+    let Filt := prod.filter (fun x => - 2 • x.1 + x.2.sum = 0)
     (Filt.map (fun x => (none, x.1, x.2.toFinset, ∅)))
   | W2 =>
     let SqHd := S5.val
@@ -242,8 +242,8 @@ def minimallyAllowsTermsOfFinset (S5 S10 : Finset ℤ) : (T : PotentialTerm) →
     let Filt := prod.filter (fun x => x.1 + x.2.1.sum + x.2.2.sum = 0)
     (Filt.map (fun x => (x.1, none,x.2.1.toFinset, x.2.2.toFinset)))
 
-lemma eq_allowsTermForm_of_mem_minimallyAllowsTermOfFinset {S5 S10 : Finset ℤ} {T : PotentialTerm}
-    {x : Charges} (hx : x ∈ minimallyAllowsTermsOfFinset S5 S10 T) :
+lemma eq_allowsTermForm_of_mem_minimallyAllowsTermOfFinset {S5 S10 : Finset 𝓩} {T : PotentialTerm}
+    {x : Charges 𝓩} (hx : x ∈ minimallyAllowsTermsOfFinset S5 S10 T) :
     ∃ a b c, x = allowsTermForm a b c T := by
   cases T
   all_goals
@@ -298,69 +298,75 @@ lemma eq_allowsTermForm_of_mem_minimallyAllowsTermOfFinset {S5 S10 : Finset ℤ}
     any_goals rfl
   all_goals
     simp_all
-    try omega
   all_goals
     congr 2
-    omega
+  case μ | topYukawa | β =>
+    rw [← add_zero a, ← h.2]
+    abel
+  case Λ | W4 | W1 | W3 | bottomYukawa =>
+    rw [← sub_zero q51, ← h.2]
+    abel
+  case K1 | K2 | W2 =>
+    rw [← sub_zero q101, ← h.2]
+    abel
 
-lemma allowsTerm_of_mem_minimallyAllowsTermOfFinset {S5 S10 : Finset ℤ} {T : PotentialTerm}
-    {x : Charges} (hx : x ∈ minimallyAllowsTermsOfFinset S5 S10 T) :
+lemma allowsTerm_of_mem_minimallyAllowsTermOfFinset {S5 S10 : Finset 𝓩} {T : PotentialTerm}
+    {x : Charges 𝓩} (hx : x ∈ minimallyAllowsTermsOfFinset S5 S10 T) :
     x.AllowsTerm T := by
   obtain ⟨a, b, c, rfl⟩ := eq_allowsTermForm_of_mem_minimallyAllowsTermOfFinset hx
   exact allowsTermForm_allowsTerm
 
-lemma mem_minimallyAllowsTermOfFinset_of_minimallyAllowsTerm {S5 S10 : Finset ℤ }
-    {T : PotentialTerm} (x : Charges) (h : x.MinimallyAllowsTerm T) (hx : x ∈ ofFinset S5 S10) :
+lemma mem_minimallyAllowsTermOfFinset_of_minimallyAllowsTerm {S5 S10 : Finset 𝓩}
+    {T : PotentialTerm} (x : Charges 𝓩) (h : x.MinimallyAllowsTerm T) (hx : x ∈ ofFinset S5 S10) :
     x ∈ minimallyAllowsTermsOfFinset S5 S10 T := by
   obtain ⟨a, b, c, rfl⟩ := eq_allowsTermForm_of_minimallyAllowsTerm h
   cases T
   all_goals
     simp [allowsTermForm, minimallyAllowsTermsOfFinset]
     rw [mem_ofFinset_iff] at hx
-  case' μ =>
+  case μ =>
     use a, a
     simp_all [allowsTermForm]
-  case' β =>
+  case β =>
     use a, {a}
     simp_all [allowsTermForm]
-  case' Λ =>
+  case Λ =>
     use {a, b}, {- a - b}
     simp_all [allowsTermForm]
-  case' W1 =>
+  case W1 =>
     apply And.intro
     · use {- a - b - c}, {a, b, c}
       simp_all [allowsTermForm]
-      omega
+      abel
     · exact h
-  case' W2 =>
+  case W2 =>
     apply And.intro
     · use (- a - b - c), {a, b, c}
       simp_all [allowsTermForm]
-      omega
+      abel
     · exact h
-  case' W3 =>
-    use (-a), {b, - b - 2 * a}
+  case W3 =>
+    use (-a), {b, - b - 2 • a}
     simp_all [allowsTermForm]
-    omega
-  case' W4 =>
-    use (- c - 2 * b), (-b), {c}
+    abel
+  case W4 =>
+    use (- c - 2 • b), (-b), {c}
     simp_all [allowsTermForm]
-    omega
-  case' K1 =>
+  case K1 =>
     use {-a}, {b, - a - b}
     simp_all [allowsTermForm]
-  case' K2 =>
+  case K2 =>
     use a, b, {- a - b}
     simp_all [allowsTermForm]
-  case' topYukawa =>
+  case topYukawa =>
     use (-a), {b, - a - b}
     simp_all [allowsTermForm]
-  case' bottomYukawa =>
+  case bottomYukawa =>
     use a, {b}, {- a - b}
     simp_all [allowsTermForm]
 
-lemma minimallyAllowsTerm_of_mem_minimallyAllowsTermOfFinset {S5 S10 : Finset ℤ}
-    {T : PotentialTerm} {x : Charges}
+lemma minimallyAllowsTerm_of_mem_minimallyAllowsTermOfFinset {S5 S10 : Finset 𝓩}
+    {T : PotentialTerm} {x : Charges 𝓩}
     (hx : x ∈ minimallyAllowsTermsOfFinset S5 S10 T) :
     x.MinimallyAllowsTerm T := by
   by_cases hT : T ≠ W1 ∧ T ≠ W2
@@ -376,8 +382,8 @@ lemma minimallyAllowsTerm_of_mem_minimallyAllowsTermOfFinset {S5 S10 : Finset 
       simp [minimallyAllowsTermsOfFinset] at hx
       exact hx.2
 
-lemma mem_ofFinset_of_mem_minimallyAllowsTermOfFinset {S5 S10 : Finset ℤ} {T : PotentialTerm}
-    {x : Charges} (hx : x ∈ minimallyAllowsTermsOfFinset S5 S10 T) :
+lemma mem_ofFinset_of_mem_minimallyAllowsTermOfFinset {S5 S10 : Finset 𝓩} {T : PotentialTerm}
+    {x : Charges 𝓩} (hx : x ∈ minimallyAllowsTermsOfFinset S5 S10 T) :
     x ∈ ofFinset S5 S10 := by
   cases T
   all_goals
@@ -418,15 +424,15 @@ lemma mem_ofFinset_of_mem_minimallyAllowsTermOfFinset {S5 S10 : Finset ℤ} {T :
     rw [mem_ofFinset_iff]
     simp_all
 
-lemma minimallyAllowsTermOfFinset_subset_ofFinset {S5 S10 : Finset ℤ} {T : PotentialTerm} :
+lemma minimallyAllowsTermOfFinset_subset_ofFinset {S5 S10 : Finset 𝓩} {T : PotentialTerm} :
     minimallyAllowsTermsOfFinset S5 S10 T ⊆ (ofFinset S5 S10).val := by
   refine Multiset.subset_iff.mpr (fun x hx => ?_)
   rw [Finset.mem_val]
   exact mem_ofFinset_of_mem_minimallyAllowsTermOfFinset hx
 
 lemma minimallyAllowsTerm_iff_mem_minimallyAllowsTermOfFinset
-    {S5 S10 : Finset ℤ} {T : PotentialTerm}
-    {x : Charges} (hx : x ∈ ofFinset S5 S10) :
+    {S5 S10 : Finset 𝓩} {T : PotentialTerm}
+    {x : Charges 𝓩} (hx : x ∈ ofFinset S5 S10) :
     x.MinimallyAllowsTerm T ↔ x ∈ minimallyAllowsTermsOfFinset S5 S10 T := by
   constructor
   · intro h
@@ -434,7 +440,8 @@ lemma minimallyAllowsTerm_iff_mem_minimallyAllowsTermOfFinset
   · intro h
     exact minimallyAllowsTerm_of_mem_minimallyAllowsTermOfFinset h
 
-lemma minimallyAllowsTermOfFinset_subset_of_subset {S5 S5' S10 S10'} {T : PotentialTerm}
+lemma minimallyAllowsTermOfFinset_subset_of_subset {S5 S5' S10 S10' : Finset 𝓩}
+    {T : PotentialTerm}
     (h5 : S5' ⊆ S5) (h10 : S10' ⊆ S10) :
     minimallyAllowsTermsOfFinset S5' S10' T ⊆ minimallyAllowsTermsOfFinset S5 S10 T := by
   intro x hx
diff --git a/PhysLean/Particles/SuperSymmetry/SU5/Charges/OfFieldLabel.lean b/PhysLean/Particles/SuperSymmetry/SU5/Charges/OfFieldLabel.lean
index 085142b5c..0f7730640 100644
--- a/PhysLean/Particles/SuperSymmetry/SU5/Charges/OfFieldLabel.lean
+++ b/PhysLean/Particles/SuperSymmetry/SU5/Charges/OfFieldLabel.lean
@@ -18,10 +18,11 @@ namespace SuperSymmetry
 namespace SU5
 
 namespace Charges
-open SuperSymmetry.SU5
+
+variable {𝓩 : Type} [InvolutiveNeg 𝓩]
 
 /-- Given an `x : Charges`, the charges associated with a given `FieldLabel`. -/
-def ofFieldLabel (x : Charges) : FieldLabel → Finset ℤ
+def ofFieldLabel (x : Charges 𝓩) : FieldLabel → Finset 𝓩
   | .fiveBarHd => x.1.toFinset
   | .fiveBarHu => x.2.1.toFinset
   | .fiveBarMatter => x.2.2.1
@@ -32,12 +33,12 @@ def ofFieldLabel (x : Charges) : FieldLabel → Finset ℤ
 
 @[simp]
 lemma ofFieldLabel_empty (F : FieldLabel) :
-    ofFieldLabel ∅ F = ∅ := by
+    ofFieldLabel (∅ : Charges 𝓩) F = ∅ := by
   cases F
   all_goals
     rfl
 
-lemma ofFieldLabel_mono {x y : Charges} (h : x ⊆ y) (F : FieldLabel) :
+lemma ofFieldLabel_mono {x y : Charges 𝓩} (h : x ⊆ y) (F : FieldLabel) :
     x.ofFieldLabel F ⊆ y.ofFieldLabel F := by
   rw [subset_def] at h
   obtain ⟨h1, h2, h3, h4⟩ := h
@@ -45,25 +46,25 @@ lemma ofFieldLabel_mono {x y : Charges} (h : x ⊆ y) (F : FieldLabel) :
   all_goals simp_all [ofFieldLabel]
 
 @[simp]
-lemma mem_ofFieldLabel_fiveHd (x : ℤ) (y : Charges) :
+lemma mem_ofFieldLabel_fiveHd (x : 𝓩) (y : Charges 𝓩) :
     x ∈ y.ofFieldLabel FieldLabel.fiveHd ↔ -x ∈ y.ofFieldLabel .fiveBarHd := by
   simp [ofFieldLabel, FieldLabel.fiveHd]
   aesop
 
 @[simp]
-lemma mem_ofFieldLabel_fiveHu (x : ℤ) (y : Charges) :
+lemma mem_ofFieldLabel_fiveHu (x : 𝓩) (y : Charges 𝓩) :
     x ∈ y.ofFieldLabel FieldLabel.fiveHu ↔ -x ∈ y.ofFieldLabel .fiveBarHu := by
   simp [ofFieldLabel, FieldLabel.fiveHu]
   aesop
 
 @[simp]
-lemma mem_ofFieldLabel_fiveMatter (x : ℤ) (y : Charges) :
+lemma mem_ofFieldLabel_fiveMatter (x : 𝓩) (y : Charges 𝓩) :
     x ∈ y.ofFieldLabel FieldLabel.fiveMatter ↔ -x ∈ y.ofFieldLabel .fiveBarMatter := by
   simp [ofFieldLabel, FieldLabel.fiveBarHd]
   aesop
 
 /-- Two charges are equal if they are equal on all field labels. -/
-lemma ext_ofFieldLabel {x y : Charges} (h : ∀ F, x.ofFieldLabel F = y.ofFieldLabel F) :
+lemma ext_ofFieldLabel {x y : Charges 𝓩} (h : ∀ F, x.ofFieldLabel F = y.ofFieldLabel F) :
     x = y := by
   match x, y with
   | (x1, x2, x3, x4), (y1, y2, y3, y4) =>
diff --git a/PhysLean/Particles/SuperSymmetry/SU5/Charges/OfPotentialTerm.lean b/PhysLean/Particles/SuperSymmetry/SU5/Charges/OfPotentialTerm.lean
index dca6d477d..d2d9cb0c0 100644
--- a/PhysLean/Particles/SuperSymmetry/SU5/Charges/OfPotentialTerm.lean
+++ b/PhysLean/Particles/SuperSymmetry/SU5/Charges/OfPotentialTerm.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
 import PhysLean.Particles.SuperSymmetry.SU5.Charges.OfFieldLabel
+import Mathlib.Tactic.Abel
 /-!
 
 # Charges associated with a potential term
@@ -19,16 +20,25 @@ namespace SU5
 namespace Charges
 open PotentialTerm
 
+variable {𝓩 : Type} [AddCommGroup 𝓩]
+
 /-- Given a charges `x : Charges` associated to the representations, and a potential
   term `T`, the charges associated with instances of that potential term. -/
-def ofPotentialTerm (x : Charges) (T : PotentialTerm) : Multiset ℤ :=
-  let add : Multiset ℤ → Multiset ℤ → Multiset ℤ := fun a b => (a.product b).map
+def ofPotentialTerm (x : Charges 𝓩) (T : PotentialTerm) : Multiset 𝓩 :=
+  let add : Multiset 𝓩 → Multiset 𝓩 → Multiset 𝓩 := fun a b => (a.product b).map
       fun (x, y) => x + y
   (T.toFieldLabel.map fun F => (ofFieldLabel x F).val).foldl add {0}
 
-lemma ofPotentialTerm_mono {x y : Charges} (h : x ⊆ y) (T : PotentialTerm) :
+@[simp]
+lemma ofPotentialTerm_empty (T : PotentialTerm) :
+    ofPotentialTerm (∅ : Charges 𝓩) T = ∅ := by
+  cases T
+  all_goals
+    rfl
+
+lemma ofPotentialTerm_mono {x y : Charges 𝓩} (h : x ⊆ y) (T : PotentialTerm) :
     x.ofPotentialTerm T ⊆ y.ofPotentialTerm T := by
-  have h1 {S1 S2 T1 T2 : Multiset ℤ} (h1 : S1 ⊆ S2) (h2 : T1 ⊆ T2) :
+  have h1 {S1 S2 T1 T2 : Multiset 𝓩} (h1 : S1 ⊆ S2) (h2 : T1 ⊆ T2) :
       (S1.product T1) ⊆ S2.product T2 :=
     Multiset.subset_iff.mpr (fun x => by simpa using fun h1' h2' => ⟨h1 h1', h2 h2'⟩)
   rw [subset_def] at h
@@ -40,20 +50,13 @@ lemma ofPotentialTerm_mono {x y : Charges} (h : x ⊆ y) (T : PotentialTerm) :
         h1 _ (Finset.subset_def.mp (ofFieldLabel_mono h _))
     simp
 
-@[simp]
-lemma ofPotentialTerm_empty (T : PotentialTerm) :
-    ofPotentialTerm ∅ T = ∅ := by
-  cases T
-  all_goals
-    rfl
-
 /-- Given a charges `x : Charges` associated to the representations, and a potential
   term `T`, the charges associated with instances of that potential term.
 
   This is a more explicit form of `PotentialTerm`, which has the benifit that
   it is quick with `decide`, but it is not defined based on more fundamental
   concepts, like `ofPotentialTerm` is. -/
-def ofPotentialTerm' (y : Charges) (T : PotentialTerm) : Multiset ℤ :=
+def ofPotentialTerm' (y : Charges 𝓩) (T : PotentialTerm) : Multiset 𝓩 :=
   let qHd := y.1
   let qHu := y.2.1
   let Q5 := y.2.2.1
@@ -79,7 +82,7 @@ def ofPotentialTerm' (y : Charges) (T : PotentialTerm) : Multiset ℤ :=
   | bottomYukawa => (qHd.toFinset.product <| Q5.product <| Q10).val.map
     (fun x => x.1 + x.2.1 + x.2.2)
 
-lemma ofPotentialTerm_subset_ofPotentialTerm' {x : Charges} (T : PotentialTerm) :
+lemma ofPotentialTerm_subset_ofPotentialTerm' {x : Charges 𝓩} (T : PotentialTerm) :
     x.ofPotentialTerm T ⊆ x.ofPotentialTerm' T := by
   refine Multiset.subset_iff.mpr (fun n h => ?_)
   simp [ofPotentialTerm] at h
@@ -107,9 +110,11 @@ lemma ofPotentialTerm_subset_ofPotentialTerm' {x : Charges} (T : PotentialTerm)
   case' bottomYukawa => use f2, f4, f6
   case' β => use (-f4), f2
   all_goals simp_all
-  all_goals omega
+  all_goals
+    rw [← f1_add_f2_eq_zero]
+    abel
 
-lemma ofPotentialTerm'_subset_ofPotentialTerm {x : Charges} (T : PotentialTerm) :
+lemma ofPotentialTerm'_subset_ofPotentialTerm [DecidableEq 𝓩] {x : Charges 𝓩} (T : PotentialTerm) :
     x.ofPotentialTerm' T ⊆ x.ofPotentialTerm T := by
   refine Multiset.subset_iff.mpr (fun n h => ?_)
   cases T
@@ -148,57 +153,65 @@ lemma ofPotentialTerm'_subset_ofPotentialTerm {x : Charges} (T : PotentialTerm)
     simp_all [Finset.insert_subset]
   all_goals
     simp [ofPotentialTerm, PotentialTerm.toFieldLabel, ofFieldLabel]
-  any_goals omega
   case' ΛP =>
     use - q3 + n
     simp only [neg_add_cancel_comm, and_true]
     use - q1 - q3 + n, q1
-    apply And.intro ?_ (by omega)
+    apply And.intro ?_ (by abel)
     simp only [true_or, and_true]
     use 0
     simp only [true_and, zero_add, exists_eq_right]
-    omega
+    right
+    rw [← q_sum]
+    abel
   case' W3P =>
-    use 2 * q1 + n
-    apply And.intro ?_ (by omega)
-    use - q2 + 2 * q1 + n, q2
-    apply And.intro ?_ (by omega)
+    use 2 • q1 + n
+    apply And.intro ?_ (by abel)
+    use - q2 + 2 • q1 + n, q2
+    apply And.intro ?_ (by abel)
     simp only [true_or, and_true]
     use 0, q3
     simp only [or_true, and_self, zero_add, true_and]
-    omega
+    rw [← q_sum]
+    abel
   case' K1P =>
     use q1 + n
-    apply And.intro ?_ (by omega)
+    apply And.intro ?_ (by abel)
     use q1 - q2 + n, q2
-    apply And.intro ?_ (by omega)
+    apply And.intro ?_ (by abel)
     simp only [true_or, and_true]
     use 0, q3
     simp only [or_true, and_self, zero_add, true_and]
-    omega
+    rw [← q_sum]
+    abel
   case' topYukawaP =>
     use q1 + n
-    apply And.intro ?_ (by omega)
+    apply And.intro ?_ (by abel)
     use q1 - q2 + n, q2
-    apply And.intro ?_ (by omega)
+    apply And.intro ?_ (by abel)
     simp only [true_or, and_true]
     use 0, q3
     simp only [or_true, and_self, zero_add, true_and]
-    omega
+    rw [← q_sum]
+    abel
   case' W1P | W2P =>
     use - q1 + n
-    apply And.intro ?_ (by omega)
+    apply And.intro ?_ (by abel)
     use - q1 - q2 + n, q2
-    apply And.intro ?_ (by omega)
+    apply And.intro ?_ (by abel)
     simp only [true_or, and_true]
     use -q1 - q2 - q3 + n, q3
-    apply And.intro ?_ (by omega)
+    apply And.intro ?_ (by abel)
     simp only [true_or, or_true, and_true]
     use 0, q4
     simp only [or_true, and_self, zero_add, true_and]
-    omega
+    rw [← q_sum]
+    abel
+  all_goals rw [← q_sum]
+  any_goals abel
 
-lemma mem_ofPotentialTerm_iff_mem_ofPotentialTerm {T : PotentialTerm} {n : ℤ} {y : Charges} :
+lemma mem_ofPotentialTerm_iff_mem_ofPotentialTerm [DecidableEq 𝓩] {T : PotentialTerm} {n : 𝓩}
+    {y : Charges 𝓩} :
     n ∈ y.ofPotentialTerm T ↔ n ∈ y.ofPotentialTerm' T := by
   constructor
   · exact fun h => ofPotentialTerm_subset_ofPotentialTerm' T h
diff --git a/PhysLean/Particles/SuperSymmetry/SU5/Charges/PhenoConstrained.lean b/PhysLean/Particles/SuperSymmetry/SU5/Charges/PhenoConstrained.lean
index 693fef384..7d49130df 100644
--- a/PhysLean/Particles/SuperSymmetry/SU5/Charges/PhenoConstrained.lean
+++ b/PhysLean/Particles/SuperSymmetry/SU5/Charges/PhenoConstrained.lean
@@ -22,23 +22,24 @@ namespace SU5
 namespace Charges
 open SuperSymmetry.SU5
 open PotentialTerm
-
+variable {𝓩 : Type} [AddCommGroup 𝓩]
 /-- A charge is pheno-constrained if it leads to the presence of any term causing proton decay
   ` {W1, Λ, W2, K1}` or R-parity violation `{β, Λ, W2, W4, K1, K2}`. -/
-def IsPhenoConstrained (x : Charges) : Prop :=
+def IsPhenoConstrained (x : Charges 𝓩) : Prop :=
   x.AllowsTerm μ ∨ x.AllowsTerm β ∨ x.AllowsTerm Λ ∨ x.AllowsTerm W2 ∨ x.AllowsTerm W4 ∨
   x.AllowsTerm K1 ∨ x.AllowsTerm K2 ∨ x.AllowsTerm W1
 
-instance decidableIsPhenoConstrained (x : Charges) : Decidable x.IsPhenoConstrained :=
+instance decidableIsPhenoConstrained [DecidableEq 𝓩] (x : Charges 𝓩) :
+    Decidable x.IsPhenoConstrained :=
   inferInstanceAs (Decidable (x.AllowsTerm μ ∨ x.AllowsTerm β ∨ x.AllowsTerm Λ ∨ x.AllowsTerm W2
     ∨ x.AllowsTerm W4 ∨ x.AllowsTerm K1 ∨ x.AllowsTerm K2 ∨ x.AllowsTerm W1))
 
 @[simp]
 lemma not_isPhenoConstrained_empty :
-    ¬ IsPhenoConstrained ∅ := by
+    ¬ IsPhenoConstrained (∅ : Charges 𝓩) := by
   simp [IsPhenoConstrained, AllowsTerm, ofPotentialTerm_empty]
 
-lemma isPhenoConstrained_mono {x y : Charges} (h : x ⊆ y)
+lemma isPhenoConstrained_mono {x y : Charges 𝓩} (h : x ⊆ y)
     (hx : x.IsPhenoConstrained) : y.IsPhenoConstrained := by
   simp [IsPhenoConstrained] at *
   rcases hx with hr | hr | hr | hr | hr | hr | hr | hr
@@ -47,16 +48,16 @@ lemma isPhenoConstrained_mono {x y : Charges} (h : x ⊆ y)
     simp_all
 
 /-- The collection of charges of super-potential terms leading to a pheno-constrained model. -/
-def phenoConstrainingChargesSP (x : Charges) : Multiset ℤ :=
+def phenoConstrainingChargesSP (x : Charges 𝓩) : Multiset 𝓩 :=
   x.ofPotentialTerm μ + x.ofPotentialTerm β + x.ofPotentialTerm Λ +
   x.ofPotentialTerm W2 + x.ofPotentialTerm W4 + x.ofPotentialTerm W1
 
 @[simp]
 lemma phenoConstrainingChargesSP_empty :
-    phenoConstrainingChargesSP ∅ = ∅ := by
+    phenoConstrainingChargesSP (∅ : Charges 𝓩) = ∅ := by
   simp [phenoConstrainingChargesSP]
 
-lemma phenoConstrainingChargesSP_mono {x y : Charges} (h : x ⊆ y) :
+lemma phenoConstrainingChargesSP_mono {x y : Charges 𝓩} (h : x ⊆ y) :
     x.phenoConstrainingChargesSP ⊆ y.phenoConstrainingChargesSP := by
   simp only [phenoConstrainingChargesSP]
   refine Multiset.subset_iff.mpr ?_
@@ -88,19 +89,21 @@ open PhysLean FourTree
 ### Inserting `q10` charges into trees
 
 -/
+variable [DecidableEq 𝓩]
 
 /-- The twig obtained by taking the new, not pheno-constrained, charges obtained by inserting
   `q10` into all leafs of a twig. This assumes that all existing charges in the twig are
   already not pheno constrained. -/
-def Twig.phenoInsertQ10 (t : Twig (Finset ℤ) (Finset ℤ)) (qHd : Option ℤ) (x : ℤ) :
-    Twig (Finset ℤ) (Finset ℤ) :=
+def Twig.phenoInsertQ10 (t : Twig (Finset 𝓩) (Finset 𝓩))
+    (qHd : Option 𝓩) (x : 𝓩) :
+    Twig (Finset 𝓩) (Finset 𝓩) :=
   match t with
   | .twig Q5 leafs =>
     if AllowsTerm (none, none, Q5, {x}) Λ then
       .twig Q5 {}
     else
       let leafFinst := leafs.map (fun (.leaf ys) => ys)
-      let sub : Multiset (Finset ℤ) := leafFinst.filterMap (fun ys =>
+      let sub : Multiset (Finset 𝓩) := leafFinst.filterMap (fun ys =>
         if ¬ insert x ys ∈ leafFinst then
           some (insert x ys)
         else
@@ -113,8 +116,8 @@ def Twig.phenoInsertQ10 (t : Twig (Finset ℤ) (Finset ℤ)) (qHd : Option ℤ)
 /-- The branch obtained by taking the new, not pheno-constrained, charges obtained by inserting
   `q10` into all leafs of a branch. This assumes that all existing charges in the branch are
   already not pheno constrained. -/
-def Branch.phenoInsertQ10 (b : Branch (Option ℤ) (Finset ℤ) (Finset ℤ)) (qHd : Option ℤ) (x : ℤ) :
-    Branch (Option ℤ) (Finset ℤ) (Finset ℤ) :=
+def Branch.phenoInsertQ10 (b : Branch (Option 𝓩) (Finset 𝓩) (Finset 𝓩)) (qHd : Option 𝓩) (x : 𝓩) :
+    Branch (Option 𝓩) (Finset 𝓩) (Finset 𝓩) :=
   match b with
   | .branch qHu twigs =>
       if AllowsTerm (qHd, qHu, ∅, {x}) K2 then
@@ -125,8 +128,9 @@ def Branch.phenoInsertQ10 (b : Branch (Option ℤ) (Finset ℤ) (Finset ℤ)) (q
 /-- The trunk obtained by taking the new, not pheno-constrained, charges obtained by inserting
   `q10` into all leafs of a trunk. This assumes that all existing charges in the trunk are
   already not pheno constrained. -/
-def Trunk.phenoInsertQ10 (T : Trunk (Option ℤ) (Option ℤ) (Finset ℤ) (Finset ℤ)) (x : ℤ) :
-    Trunk (Option ℤ) (Option ℤ) (Finset ℤ) (Finset ℤ) :=
+def Trunk.phenoInsertQ10 (T : Trunk (Option 𝓩) (Option 𝓩) (Finset 𝓩) (Finset 𝓩))
+    (x : 𝓩) :
+    Trunk (Option 𝓩) (Option 𝓩) (Finset 𝓩) (Finset 𝓩) :=
   match T with
   | .trunk qHd branches =>
     .trunk qHd (branches.map fun b => Branch.phenoInsertQ10 b qHd x)
@@ -134,14 +138,14 @@ def Trunk.phenoInsertQ10 (T : Trunk (Option ℤ) (Option ℤ) (Finset ℤ) (Fins
 /-- The tree obtained by taking the new, not pheno-constrained, charges obtained by inserting
   `q10` into all leafs of a tree. This assumes that all existing charges in the tree are
   already not pheno constrained. -/
-def phenoInsertQ10 (T : FourTree (Option ℤ) (Option ℤ) (Finset ℤ) (Finset ℤ)) (x : ℤ) :
-    FourTree (Option ℤ) (Option ℤ) (Finset ℤ) (Finset ℤ) :=
+def phenoInsertQ10 (T : FourTree (Option 𝓩) (Option 𝓩) (Finset 𝓩) (Finset 𝓩)) (x : 𝓩) :
+    FourTree (Option 𝓩) (Option 𝓩) (Finset 𝓩) (Finset 𝓩) :=
   match T with
   | .root trunks =>
     .root (trunks.map fun ts => (Trunk.phenoInsertQ10 ts x))
 
 lemma mem_phenoInsertQ10_of_mem_allowsTerm
-    (T : FourTree (Option ℤ) (Option ℤ) (Finset ℤ) (Finset ℤ)) (q10 : ℤ) (C : Charges)
+    (T : FourTree (Option 𝓩) (Option 𝓩) (Finset 𝓩) (Finset 𝓩)) (q10 : 𝓩) (C : Charges 𝓩)
     (h : C ∈ (T.uniqueMap4 (insert q10))) (hC : ¬ AllowsTerm (C.1, C.2.1, ∅, {q10}) K2
       ∧ ¬ AllowsTerm (none, none, C.2.2.1, {q10}) Λ
       ∧ ¬ AllowsTerm (none, none, C.2.2.1, C.2.2.2) W1 ∧
@@ -225,8 +229,8 @@ lemma mem_phenoInsertQ10_of_mem_allowsTerm
 /-- The branch obtained by taking the new, not pheno-constrained, charges obtained by inserting
   `q5` into all leafs of a branch. This assumes that all existing charges in the branch are
   already not pheno constrained. -/
-def Branch.phenoInsertQ5 (b : Branch (Option ℤ) (Finset ℤ) (Finset ℤ)) (qHd : Option ℤ) (x : ℤ) :
-    Branch (Option ℤ) (Finset ℤ) (Finset ℤ) :=
+def Branch.phenoInsertQ5 (b : Branch (Option 𝓩) (Finset 𝓩) (Finset 𝓩)) (qHd : Option 𝓩) (x : 𝓩) :
+    Branch (Option 𝓩) (Finset 𝓩) (Finset 𝓩) :=
   match b with
   | .branch qHu twigs =>
     if AllowsTerm (none, qHu, {x}, ∅) β ∨ AllowsTerm (qHd, qHu, {x}, ∅) W4 then
@@ -242,8 +246,8 @@ def Branch.phenoInsertQ5 (b : Branch (Option ℤ) (Finset ℤ) (Finset ℤ)) (qH
 /-- The trunk obtained by taking the new, not pheno-constrained, charges obtained by inserting
   `q5` into all leafs of a trunk. This assumes that all existing charges in the trunk are
   already not pheno constrained. -/
-def Trunk.phenoInsertQ5 (T : Trunk (Option ℤ) (Option ℤ) (Finset ℤ) (Finset ℤ)) (x : ℤ) :
-    Trunk (Option ℤ) (Option ℤ) (Finset ℤ) (Finset ℤ) :=
+def Trunk.phenoInsertQ5 (T : Trunk (Option 𝓩) (Option 𝓩) (Finset 𝓩) (Finset 𝓩)) (x : 𝓩) :
+    Trunk (Option 𝓩) (Option 𝓩) (Finset 𝓩) (Finset 𝓩) :=
   match T with
   | .trunk qHd branches =>
     .trunk qHd (branches.map fun b => Branch.phenoInsertQ5 b qHd x)
@@ -251,14 +255,14 @@ def Trunk.phenoInsertQ5 (T : Trunk (Option ℤ) (Option ℤ) (Finset ℤ) (Finse
 /-- The tree obtained by taking the new, not pheno-constrained, charges obtained by inserting
   `q5` into all leafs of a tree. This assumes that all existing charges in the tree are
   already not pheno constrained. -/
-def phenoInsertQ5 (T : FourTree (Option ℤ) (Option ℤ) (Finset ℤ) (Finset ℤ)) (x : ℤ) :
-    FourTree (Option ℤ) (Option ℤ) (Finset ℤ) (Finset ℤ) :=
+def phenoInsertQ5 (T : FourTree (Option 𝓩) (Option 𝓩) (Finset 𝓩) (Finset 𝓩)) (x : 𝓩) :
+    FourTree (Option 𝓩) (Option 𝓩) (Finset 𝓩) (Finset 𝓩) :=
   match T with
   | .root trunks =>
     .root (trunks.map fun ts => (Trunk.phenoInsertQ5 ts x))
 
-lemma mem_phenoInsertQ5_of_mem_allowsTerm (T : FourTree (Option ℤ) (Option ℤ) (Finset ℤ) (Finset ℤ))
-    (q5 : ℤ) (C : Charges)
+lemma mem_phenoInsertQ5_of_mem_allowsTerm (T : FourTree (Option 𝓩) (Option 𝓩) (Finset 𝓩) (Finset 𝓩))
+    (q5 : 𝓩) (C : Charges 𝓩)
     (h : C ∈ (T.uniqueMap3 (insert q5))) (hC : ¬ AllowsTerm (none, C.2.1, {q5}, ∅) β
       ∧ ¬ AllowsTerm (C.1, C.2.1, {q5}, ∅) W4 ∧
       ¬ AllowsTerm (none, none, {q5}, C.2.2.2) W1 ∧ ¬ AllowsTerm (none, none, {q5}, C.2.2.2) K1
diff --git a/PhysLean/Particles/SuperSymmetry/SU5/Charges/Tree.lean b/PhysLean/Particles/SuperSymmetry/SU5/Charges/Tree.lean
index 4dc494da1..fdede0d77 100644
--- a/PhysLean/Particles/SuperSymmetry/SU5/Charges/Tree.lean
+++ b/PhysLean/Particles/SuperSymmetry/SU5/Charges/Tree.lean
@@ -59,10 +59,11 @@ def leaf : Finset ℤ → Leaf (Finset ℤ) := fun q10 => .leaf q10
 ## Inserting charges and minimal super sets
 
 -/
+variable {𝓩 : Type} [DecidableEq 𝓩]
 
 lemma insert_filter_card_zero
-    (T : FourTree (Option ℤ) (Option ℤ) (Finset ℤ) (Finset ℤ)) (S5 S10 : Finset ℤ)
-    (p : Charges → Prop) [DecidablePred p]
+    (T : FourTree (Option 𝓩) (Option 𝓩) (Finset 𝓩) (Finset 𝓩)) (S5 S10 : Finset 𝓩)
+    (p : Charges 𝓩 → Prop) [DecidablePred p]
     (hComplet : ∀ x ∈ T, IsComplete x)
     (h10 : ∀ q10 : S10, (T.uniqueMap4 (insert q10.1)).toMultiset.filter p = ∅)
     (h5 : ∀ q5 : S5, (T.uniqueMap3 (insert q5.1)).toMultiset.filter p = ∅) :
@@ -96,13 +97,13 @@ lemma insert_filter_card_zero
     simp_all
 
 lemma subset_insert_filter_card_zero_inductive
-    (T : FourTree (Option ℤ) (Option ℤ) (Finset ℤ) (Finset ℤ))
-    (S5 S10 : Finset ℤ)
-    (p : Charges → Prop) [DecidablePred p]
-    (hnotSubset : ∀ (x y : Charges), x ⊆ y → ¬ p x → ¬ p y)
+    (T : FourTree (Option 𝓩) (Option 𝓩) (Finset 𝓩) (Finset 𝓩))
+    (S5 S10 : Finset 𝓩)
+    (p : Charges 𝓩 → Prop) [DecidablePred p]
+    (hnotSubset : ∀ (x y : Charges 𝓩), x ⊆ y → ¬ p x → ¬ p y)
     (hComplet : ∀ x ∈ T, IsComplete x)
-    (x : Charges)
-    (hx : x ∈ T) (y : Charges) (hsubset : x ⊆ y)
+    (x : Charges 𝓩)
+    (hx : x ∈ T) (y : Charges 𝓩) (hsubset : x ⊆ y)
     (hy : y ∈ ofFinset S5 S10)
     (h10 : ∀ q10 : S10, (T.uniqueMap4 (insert q10.1)).toMultiset.filter p = ∅)
     (h5 : ∀ q5 : S5, (T.uniqueMap3 (insert q5.1)).toMultiset.filter p = ∅) :
@@ -141,13 +142,13 @@ lemma subset_insert_filter_card_zero_inductive
   This assumes that all charges in `T` are complete, and that `p` satisfies
   `x ⊆ y → ¬ p x → ¬ p y`. -/
 lemma subset_insert_filter_card_zero
-    (T : FourTree (Option ℤ) (Option ℤ) (Finset ℤ) (Finset ℤ))
-    (S5 S10 : Finset ℤ)
-    (p : Charges → Prop) [DecidablePred p]
-    (hnotSubset : ∀ (x y : Charges), x ⊆ y → ¬ p x → ¬ p y)
+    (T : FourTree (Option 𝓩) (Option 𝓩) (Finset 𝓩) (Finset 𝓩))
+    (S5 S10 : Finset 𝓩)
+    (p : Charges 𝓩 → Prop) [DecidablePred p]
+    (hnotSubset : ∀ (x y : Charges 𝓩), x ⊆ y → ¬ p x → ¬ p y)
     (hComplet : ∀ x ∈ T, IsComplete x)
-    (x : Charges)
-    (hx : x ∈ T) (y : Charges) (hsubset : x ⊆ y)
+    (x : Charges 𝓩)
+    (hx : x ∈ T) (y : Charges 𝓩) (hsubset : x ⊆ y)
     (hy : y ∈ ofFinset S5 S10)
     (h10 : ∀ q10 : S10, (T.uniqueMap4 (insert q10.1)).toMultiset.filter p = ∅)
     (h5 : ∀ q5 : S5, (T.uniqueMap3 (insert q5.1)).toMultiset.filter p = ∅) :
diff --git a/PhysLean/Particles/SuperSymmetry/SU5/Charges/Yukawa.lean b/PhysLean/Particles/SuperSymmetry/SU5/Charges/Yukawa.lean
index 07c9ed7c3..c79f776eb 100644
--- a/PhysLean/Particles/SuperSymmetry/SU5/Charges/Yukawa.lean
+++ b/PhysLean/Particles/SuperSymmetry/SU5/Charges/Yukawa.lean
@@ -22,13 +22,14 @@ namespace SU5
 namespace Charges
 open PotentialTerm
 
+variable {𝓩 : Type} [AddCommGroup 𝓩]
 /-- The collection of charges associated with Yukawa terms.
   Correspondingly, the (negative) of the charges of the singlets needed to regenerate all
   Yukawa terms in the potential. -/
-def ofYukawaTerms (x : Charges) : Multiset ℤ :=
+def ofYukawaTerms (x : Charges 𝓩) : Multiset 𝓩 :=
   x.ofPotentialTerm topYukawa + x.ofPotentialTerm bottomYukawa
 
-lemma ofYukawaTerms_subset_of_subset {x y : Charges} (h : x ⊆ y) :
+lemma ofYukawaTerms_subset_of_subset {x y : Charges 𝓩} (h : x ⊆ y) :
     x.ofYukawaTerms ⊆ y.ofYukawaTerms := by
   simp only [ofYukawaTerms]
   refine Multiset.subset_iff.mpr ?_
@@ -47,12 +48,12 @@ lemma ofYukawaTerms_subset_of_subset {x y : Charges} (h : x ⊆ y) :
   insertions of singlets needed to regenerate the Yukawa terms.
   Equivalently, the sum of up-to `n` integers each corresponding to a charge of the
   Yukawa terms.  -/
-def ofYukawaTermsNSum (x : Charges) : ℕ → Multiset ℤ
+def ofYukawaTermsNSum (x : Charges 𝓩) : ℕ → Multiset 𝓩
   | 0 => {0}
   | n + 1 => x.ofYukawaTermsNSum n + (x.ofYukawaTermsNSum n).bind fun sSum =>
     (x.ofYukawaTerms.map fun s => sSum + s)
 
-lemma ofYukawaTermsNSum_subset_of_subset {x y : Charges} (h : x ⊆ y) (n : ℕ) :
+lemma ofYukawaTermsNSum_subset_of_subset {x y : Charges 𝓩} (h : x ⊆ y) (n : ℕ) :
     x.ofYukawaTermsNSum n ⊆ y.ofYukawaTermsNSum n := by
   induction n with
   | zero => simp [ofYukawaTermsNSum]
@@ -74,22 +75,23 @@ lemma ofYukawaTermsNSum_subset_of_subset {x y : Charges} (h : x ⊆ y) (n : ℕ)
     apply ofYukawaTerms_subset_of_subset h
     exact hz2
 
+variable [DecidableEq 𝓩]
 /-- For charges `x : Charges`, the proposition which states that the singlets
   needed to regenerate the Yukawa couplings regnerate a dangerous coupling
   (in the superpotential) with up-to `n` insertions of the scalars. -/
-def YukawaGeneratesDangerousAtLevel (x : Charges) (n : ℕ) : Prop :=
+def YukawaGeneratesDangerousAtLevel (x : Charges 𝓩) (n : ℕ) : Prop :=
   (x.ofYukawaTermsNSum n).toFinset ∩ x.phenoConstrainingChargesSP.toFinset ≠ ∅
 
 @[simp]
 lemma not_yukawaGeneratesDangerousAtLevel_of_empty (n : ℕ) :
-    ¬ YukawaGeneratesDangerousAtLevel ∅ n := by
+    ¬ YukawaGeneratesDangerousAtLevel (∅ : Charges 𝓩) n := by
   simp [YukawaGeneratesDangerousAtLevel]
 
-instance (x : Charges) (n : ℕ) : Decidable (YukawaGeneratesDangerousAtLevel x n) :=
+instance (x : Charges 𝓩) (n : ℕ) : Decidable (YukawaGeneratesDangerousAtLevel x n) :=
   inferInstanceAs (Decidable ((x.ofYukawaTermsNSum n).toFinset
     ∩ x.phenoConstrainingChargesSP.toFinset ≠ ∅))
 
-lemma yukawaGeneratesDangerousAtLevel_of_subset {x y : Charges} {n : ℕ} (h : x ⊆ y)
+lemma yukawaGeneratesDangerousAtLevel_of_subset {x y : Charges 𝓩} {n : ℕ} (h : x ⊆ y)
     (hx : x.YukawaGeneratesDangerousAtLevel n) :
     y.YukawaGeneratesDangerousAtLevel n := by
   simp [YukawaGeneratesDangerousAtLevel] at *
@@ -108,7 +110,7 @@ lemma yukawaGeneratesDangerousAtLevel_of_subset {x y : Charges} {n : ℕ} (h : x
   rw [h1] at hx
   simp at hx
 
-lemma yukawaGeneratesDangerousAtLevel_succ {x : Charges} {n : ℕ}
+lemma yukawaGeneratesDangerousAtLevel_succ {x : Charges 𝓩} {n : ℕ}
     (hx : x.YukawaGeneratesDangerousAtLevel n) :
     x.YukawaGeneratesDangerousAtLevel (n + 1) := by
   simp [YukawaGeneratesDangerousAtLevel] at *
@@ -119,14 +121,14 @@ lemma yukawaGeneratesDangerousAtLevel_succ {x : Charges} {n : ℕ}
   left
   exact hx
 
-lemma yukawaGeneratesDangerousAtLevel_add_of_left {x : Charges} {n k : ℕ}
+lemma yukawaGeneratesDangerousAtLevel_add_of_left {x : Charges 𝓩} {n k : ℕ}
     (hx : x.YukawaGeneratesDangerousAtLevel n) :
     x.YukawaGeneratesDangerousAtLevel (n + k) := by
   induction k with
   | zero => exact hx
   | succ k ih => exact yukawaGeneratesDangerousAtLevel_succ ih
 
-lemma yukawaGeneratesDangerousAtLevel_of_le {x : Charges} {n m : ℕ}
+lemma yukawaGeneratesDangerousAtLevel_of_le {x : Charges 𝓩} {n m : ℕ}
     (h : n ≤ m) (hx : x.YukawaGeneratesDangerousAtLevel n) :
     x.YukawaGeneratesDangerousAtLevel m := by
   generalize hk : m - n = k at *