Exist completions subset of complete

lemma exist_completions_subset_of_complete (S5 S10 : Finset 𝓩) (x y : ChargeSpectrum 𝓩)    (hsubset : x ⊆ y) (hy : y ∈ ofFinset S5 S10) (hycomplete : IsComplete y) :    ∃ z ∈ completions S5 S10 x, z ⊆ y := by  by_cases hx : IsComplete x  · use x    simp_all  rw [Subset] at hsubset  dsimp [hasSubset] at hsubset  match x, y with  | ⟨x1, x2, x3, x4⟩, ⟨y1, y2, y3, y4⟩ =>  simp [IsComplete] at hycomplete  rw [Option.isSome_iff_exists, Option.isSome_iff_exists] at hycomplete  obtain ⟨y1, rfl⟩ := hycomplete.1  obtain ⟨y2, rfl⟩ := hycomplete.2.1  rw [Finset.eq_empty_iff_forall_notMem, Finset.eq_empty_iff_forall_notMem] at hycomplete  simp at hycomplete  obtain ⟨z3, hz3⟩ := hycomplete.1  obtain ⟨z4, hz4⟩ := hycomplete.2  simp [mem_ofFinset_iff] at hy  have hz3Mem : z3 ∈ S5 := by    apply hy.2.2.1    simp_all  have hz4Mem : z4 ∈ S10 := by    apply hy.2.2.2    simp_all  have hy1' : some y1 ∈ if x1.isSome = true then {x1} else      Multiset.map (fun y => some y) S5.val := by    match x1 with    | none => simpa using hy.1    | some a => simp_all  have hy2' : some y2 ∈ if x2.isSome = true then {x2} else      Multiset.map (fun y => some y) S5.val := by    match x2 with    | none => simpa using hy.2.1    | some a => simp_all  simp_all  refine ⟨⟨y1, y2, if x3 = ∅ then {z3} else x3, if x4 = ∅ then {z4} else x4⟩, ?_, ?_⟩  · rw [mem_completions_iff]    refine ⟨by simp_all, by simp_all, ?_, ?_⟩    · split_ifs with h3 <;> simp_all    · split_ifs with h4 <;> simp_all  · rw [Subset]    dsimp [hasSubset]    refine ⟨by simp_all, by simp_all, ?_, ?_⟩    · split_ifs with h3 <;> simp_all [Finset.singleton_subset_iff]    · split_ifs with h4 <;> simp_all [Finset.singleton_subset_iff]