Card of mem minimal Super Set

lemma card_of_mem_minimalSuperSet {S5 S10 : Finset 𝓩} {x : ChargeSpectrum 𝓩}    (y : ChargeSpectrum 𝓩) (hy : y ∈ minimalSuperSet S5 S10 x) :    card y = card x + 1 := by  simp [minimalSuperSet] at hy  rcases hy with ⟨hy1, hr | hr | hr | hr⟩  · match x with    | ⟨none, _, _, _⟩ =>      simp at hr      obtain ⟨a, ha, rfl⟩ := hr      simp [card]      omega    | ⟨some x1, _, _, _⟩ =>      simp at hr  · match x with    | ⟨_, none, _, _⟩ =>      simp at hr      obtain ⟨a, ha, rfl⟩ := hr      simp [card]      omega    | ⟨_, some x2, _, _⟩ =>      simp at hr  · match x with    | ⟨_, _, Q5, _⟩ =>      simp at hr      obtain ⟨a, ha, rfl⟩ := hr      simp [card]      rw [Finset.card_insert_of_notMem]      omega      by_contra h      rw [Finset.insert_eq_of_mem h] at hy1      simp at hy1  · match x with    | ⟨_, _, _, Q10⟩ =>      simp at hr      obtain ⟨a, ha, rfl⟩ := hr      simp [card]      rw [Finset.card_insert_of_notMem]      omega      by_contra h      rw [Finset.insert_eq_of_mem h] at hy1      simp at hy1