Self subset mem minimal Super Set

lemma self_subset_mem_minimalSuperSet (S5 S10 : Finset 𝓩) (x y : ChargeSpectrum 𝓩)    (hy : y ∈ minimalSuperSet S5 S10 x) : x ⊆ y := 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      rw [Subset]      simp [hasSubset]    | ⟨some x1, _, _, _⟩ =>      simp at hr  · match x with    | ⟨_, none, _, _⟩ =>      simp at hr      obtain ⟨a, ha, rfl⟩ := hr      rw [Subset]      simp [hasSubset]    | ⟨_, some x2, _, _⟩ =>      simp at hr  · match x with    | ⟨_, _, Q5, _⟩ =>      simp at hr      obtain ⟨a, ha, rfl⟩ := hr      rw [Subset]      simp [hasSubset]  · match x with    | ⟨_, _, _, Q10⟩ =>      simp at hr      obtain ⟨a, ha, rfl⟩ := hr      rw [Subset]      simp [hasSubset]