Allows Term Q5 or allows Term of allows Term insert Q5

lemma allowsTermQ5_or_allowsTerm_of_allowsTerm_insertQ5 {qHd qHu : Option 𝓩}    {Q5 Q10: Finset 𝓩} {q5 : 𝓩} (T : PotentialTerm)    (h : AllowsTerm ⟨qHd, qHu, insert q5 Q5, Q10⟩ T) :    AllowsTermQ5 ⟨qHd, qHu, Q5, Q10⟩ q5 T ∨    AllowsTerm ⟨qHd, qHu, Q5, Q10⟩ T := by  rcases T  all_goals    simp [allowsTerm_iff_zero_mem_ofPotentialTerm', ofPotentialTerm', AllowsTermQ5] at h ⊢  · exact h  · match qHu with    | some qHu =>      simp at h      simp only [Multiset.mem_map, Finset.mem_val]      convert h using 1      rw [neg_add_eq_zero, eq_comm]    | none => simp at h  · obtain ⟨a1, a2, a3, ⟨h1, h2, h3⟩, hsum⟩ := h    rcases h1 with h1 | h1    · subst h1      refine .inl ⟨a2, a3, ⟨h2, h3⟩, ?_⟩      rw [← hsum]      abel    · rcases h2 with h2 | h2      · subst h2        exact .inl ⟨a1, a3, ⟨.inr h1, h3⟩, hsum⟩      · exact .inr ⟨a1, a2, a3, ⟨h1, h2, h3⟩, hsum⟩  · obtain ⟨a1, a2, a3, a4, ⟨h1, h2, h3, h4⟩, hsum⟩ := h    rcases h1 with h1 | h1    · left      use a2, a3, a4      simp_all    · right      use a1, a2, a3, a4  · simp_all  · match qHu with    | some qHu =>      simp at h      obtain ⟨a1, a2, ⟨h1, h2⟩, hsum⟩ := h      rcases h1 with h1 | h1      · subst h1        left        rcases h2 with h2 | h2        · left          subst h2          rw [← hsum]          abel        · right          use a2          simp_all          rw [← hsum]          abel      · rcases h2 with h2 | h2        · left          right          use a1          simp_all          rw [← hsum]          abel        · right          rw [@Multiset.mem_map]          simp only [Multiset.mem_product, Finset.mem_val, Prod.exists]          use a1, a2    | none => simp at h  · match qHd, qHu with    | some qHd, some qHu =>      simp_all      convert h using 1      constructor      all_goals      · intro h        rw [← h]        abel    | none, _ => simp at h    | some x, none => simp at h  · obtain ⟨a1, a2, a3, ⟨h1, h2, h3⟩, hsum⟩ := h    rcases h1 with h1 | h1    · left      use a2, a3      simp_all    · right      use a1, a2, a3  · simp_all  · simp_all  · match qHd with    | none => simp at h    | some qHd =>      simp_all      obtain ⟨a1, a2, ⟨h1, h2⟩, hsum⟩ := h      rcases h1 with h1 | h1      · subst h1        left        use a2        simp_all        rw [← hsum]        abel      · right        use a1, a2