Completeness of is Pheno Closed Q5 is Pheno Closed Q10

lemma completeness_of_isPhenoClosedQ5_isPhenoClosedQ10    {S5 S10 : Finset 𝓩} {charges : Multiset (ChargeSpectrum 𝓩)}    (charges_topYukawa : ∀ x ∈ charges, x.AllowsTerm .topYukawa)    (charges_not_isPhenoConstrained : ∀ x ∈ charges, ¬ x.IsPhenoConstrained)    (charges_yukawa : ∀ x ∈ charges, ¬ x.YukawaGeneratesDangerousAtLevel 1)    (charges_complete : ∀ x ∈ charges, x.IsComplete)    (charges_isPhenoClosedQ5 : IsPhenoClosedQ5 S5 charges)    (charges_isPhenoClosedQ10 : IsPhenoClosedQ10 S10 charges)    (charges_exist : ContainsPhenoCompletionsOfMinimallyAllows S5 S10 charges)    {x : ChargeSpectrum 𝓩} (hsub : x ∈ ofFinset S5 S10) :    x ∈ charges ↔ AllowsTerm x .topYukawa ∧    ¬ IsPhenoConstrained x ∧ ¬ YukawaGeneratesDangerousAtLevel x 1 ∧ IsComplete x := by  constructor  · /- Showing that if `x ∈ Charges` it satisfies the conditions. -/    intro h    exact ⟨charges_topYukawa x h, charges_not_isPhenoConstrained x h, charges_yukawa x h,      charges_complete x h⟩  · intro ⟨hTop, hPheno, hY, hComplete⟩    /- Showing that if `x ∉ charges` and `AllowsTerm x .topYukawa`,      `¬ IsPhenoConstrained x`, ``¬ YukawaGeneratesDangerousAtLevel x 1`, `IsComplete x`,      then `False`. -/    by_contra hn    suffices hnot : ¬ ((¬ IsPhenoConstrained x ∧ ¬ YukawaGeneratesDangerousAtLevel x 1) ∧        AllowsTerm x topYukawa) by      simp_all    revert hn    rw [not_and]    simp only [hTop, not_true_eq_false, imp_false]    suffices hmem : ∃ y ∈ charges, y ⊆ x by      obtain ⟨y, y_mem, hyx⟩ := hmem      refine subset_insert_filter_card_zero charges S5 S10 (fun x =>        (¬x.IsPhenoConstrained ∧ ¬x.YukawaGeneratesDangerousAtLevel 1))        ?_ ?_ y ?_ x hyx hsub ?_ ?_      · simpa using fun x y hxy h1 h2 => yukawaGeneratesDangerousAtLevel_of_subset hxy <| h1          fun hn => h2 <| isPhenoConstrained_mono hxy hn      · intro x        exact fun a => charges_complete x a      · exact y_mem      · intro q10        rw [Multiset.empty_eq_zero, Multiset.eq_zero_iff_forall_notMem]        simp only [Multiset.mem_filter, Multiset.mem_map, not_and, Decidable.not_not,          forall_exists_index, and_imp, forall_apply_eq_imp_iff₂]        intro z hz hzP h2        have h1 := charges_isPhenoClosedQ10 q10 q10.2 z hz        simp_all      · intro q5        rw [Multiset.empty_eq_zero, Multiset.eq_zero_iff_forall_notMem]        simp only [Multiset.mem_filter, Multiset.mem_map, not_and, Decidable.not_not,          forall_exists_index, and_imp, forall_apply_eq_imp_iff₂]        intro z hz hzP h2        have h1 := charges_isPhenoClosedQ5 q5 q5.2 z hz        simp_all    /- Getting the subset of `x` which minimally allows the top Yukawa. -/    obtain ⟨y, hyMem, hysubsetx⟩ : ∃ y ∈ (minimallyAllowsTermsOfFinset S5 S10 topYukawa),        y ⊆ x := by      rw [allowsTerm_iff_subset_minimallyAllowsTerm] at hTop      obtain ⟨y, hPower, hIrre⟩ := hTop      use y      constructor      · rw [← minimallyAllowsTerm_iff_mem_minimallyAllowsTermOfFinset]        · exact hIrre        · exact mem_ofFinset_antitone S5 S10 (by simpa using hPower) hsub      · simpa using hPower    obtain ⟨z, hz1, hz2⟩ := exist_completions_subset_of_complete S5 S10 y x hysubsetx hsub hComplete    use z    constructor    · refine charges_exist y hyMem ?_ z hz1 ?_      · by_contra hn        have := isPhenoConstrained_mono hysubsetx hn        simp_all      · apply And.intro        · by_contra hn          have := isPhenoConstrained_mono hz2 hn          simp_all        · by_contra hn          have := yukawaGeneratesDangerousAtLevel_of_subset hz2 hn          simp_all    · simp_all