Subset le mem of card eq succ

lemma subset_le_mem_of_card_eq_succ {n : ℕ} {F : FluxesTen} (hF : F.NoExotics) (hnZ : F.HasNoZero)    (S : Multiset Fluxes) (hcard : S.card = n.succ) (hS : S ≤ F) {Y X : Finset (Multiset Fluxes)}    (hY : ∀ (S : Multiset Fluxes), S.card = n → S ≤ F → S ∈ Y)    (hX : ∀ a ∈ ({⟨1, -1⟩, ⟨1, 0⟩, ⟨1, 1⟩, ⟨2, -1⟩, ⟨2, 0⟩, ⟨2, 1⟩, ⟨3, 0⟩} : Finset Fluxes),      ∀ y ∈ Y,      (Multiset.map (fun x => x.M) (a ::ₘ y)).sum ≤ 3 →      (Multiset.map (fun x => x.M - x.N) (a ::ₘ y)).sum ≤ 3 →      (Multiset.map (fun x => x.M + x.N) (a ::ₘ y)).sum ≤ 3 →      a ::ₘ y ∈ X) :    S ∈ X := by  have hSum1 := chiralIndicesOfQ_subset_sum_le_three_of_noExotics F hF S hS  have hSum2 := chiralIndicesOfU_subset_sum_le_three_of_noExotics F hF S hS  have hsum3 := chiralIndicesOfE_subset_sum_le_three_of_noExotics F hF S hS  revert S  apply Multiset.induction  · simp  intro a S ih hcard hle hsum1 hsum2 hsum3  have hsub : S ≤ F := (S.le_cons_self a).trans hle  have ha : a ∈ F := Multiset.mem_of_le hle (S.mem_cons_self a)  rw [Multiset.card_cons] at hcard  simp at hcard  exact hX a (mem_mem_finset_of_noExotics F hF hnZ a ha) S (hY S hcard hsub) hsum1 hsum2 hsum3