Mem completions is Complete

lemma mem_completions_isComplete {S5 S10 : Finset 𝓩} {x y : ChargeSpectrum 𝓩}    (hx : y ∈ completions S5 S10 x) : IsComplete y := by  match y with  | ⟨qHd, qHu, Q5, Q10⟩ =>  simp [mem_completions_iff] at hx  match x with  | ⟨x1, x2, x3, x4⟩ =>  simp_all  rw [IsComplete]  refine ⟨?_, ?_, ?_, ?_⟩  · simp    by_cases hs : x1.isSome    · simp_all    · simp_all      obtain ⟨a, h, rfl⟩ := hx.1      simp  · simp    by_cases hs : x2.isSome    · simp_all    · simp_all      obtain ⟨a, h, rfl⟩ := hx.2.1      simp  · simp    by_cases hs : x3 ≠ ∅    · simp_all    · simp_all      obtain ⟨a, h, rfl⟩ := hx.2.2.1      simp  · simp    by_cases hs : x4 ≠ ∅    · simp_all    · simp_all      obtain ⟨a, h, rfl⟩ := hx.2.2.2      simp