Subset insert filter card zero inductive

lemma subset_insert_filter_card_zero_inductive    (T : Multiset (ChargeSpectrum 𝓩))    (S5 S10 : Finset 𝓩)    (p : ChargeSpectrum 𝓩 → Prop) [DecidablePred p]    (hnotSubset : ∀ (x y : ChargeSpectrum 𝓩), x ⊆ y → ¬ p x → ¬ p y)    (hComplet : ∀ x ∈ T, IsComplete x)    (x : ChargeSpectrum 𝓩)    (hx : x ∈ T) (y : ChargeSpectrum 𝓩) (hsubset : x ⊆ y)    (hy : y ∈ ofFinset S5 S10)    (h10 : ∀ q10 : S10, ((T.map fun x => ⟨x.qHd, x.qHu, x.Q5, insert q10.1 x.Q10⟩).filter      fun y => (y ∉ T ∧ p y)) = ∅)    (h5 : ∀ q5 : S5, ((T.map fun x => ⟨x.qHd, x.qHu, insert q5.1 x.Q5, x.Q10⟩).filter      fun y => (y ∉ T ∧ p y)) = ∅) :    (n : ℕ) → (hn : n = y.card - x.card) → y ∉ T → ¬ p y  | 0, hn, hnot_in_T => by    have hxy : x = y := by      refine eq_of_subset_card hsubset ?_      have hl : x.card ≤ y.card := card_mono hsubset      omega    subst hxy    simp_all  | Nat.succ n, hn, hnot_in_T => by    have hxy : x ≠ y := by      intro h      subst h      simp at hn    obtain ⟨z, hz, hsubsetz⟩ := exists_minimalSuperSet S5 S10 hy hsubset hxy    have hz' := insert_filter_card_zero T S5 S10 p hComplet h10 h5 x hx z hz    by_cases hz_not_in_T : z ∉ T    · apply hnotSubset      · exact hsubsetz      · exact hz' hz_not_in_T    apply subset_insert_filter_card_zero_inductive T S5 S10 p hnotSubset hComplet z (n := n)    · simpa using hz_not_in_T    · exact hsubsetz    · exact hy    · exact fun q10 => h10 q10    · exact fun q5 => h5 q5    · rw [card_of_mem_minimalSuperSet z hz]      omega    · exact hnot_in_T