Allows Term Q10 or allows Term of allows Term insert Q10

lemma allowsTermQ10_or_allowsTerm_of_allowsTerm_insertQ10 {qHd qHu : Option 𝓩}    {Q5 Q10: Finset 𝓩} {q10 : 𝓩} (T : PotentialTerm)    (h : AllowsTerm ⟨qHd, qHu, Q5, insert q10 Q10⟩ T) :    AllowsTermQ10 ⟨qHd, qHu, Q5, Q10⟩ q10 T ∨    AllowsTerm ⟨qHd, qHu, Q5, Q10⟩ T := by  rcases T  all_goals    simp [allowsTerm_iff_zero_mem_ofPotentialTerm', ofPotentialTerm', AllowsTermQ10] at h ⊢  · simp_all  · simp_all  · obtain ⟨a1, a2, a3, ⟨h1, h2, h3⟩, hsum⟩ := h    rcases h3 with h3 | h3    · subst h3      left      use a1, a2    · right      use a1, a2, a3  · obtain ⟨a1, a2, a3, a4, ⟨h1, h2, h3, h4⟩, hsum⟩ := h    rcases h2 with h2 | h2    · subst h2      left      use a1, a3, a4      simp_all      rw [← hsum]      abel    rcases h3 with h3 | h3    · subst h3      left      use a1, a2, a4      simp_all      rw [← hsum]      abel    rcases h4 with h4 | h4    · subst h4      left      use a1, a2, a3      simp_all    right    use a1, a2, a3, a4  · match qHd with    | none => simp at h    | some qHd =>    simp_all    obtain ⟨a1, a2, a3, ⟨h1, h2, h3⟩, hsum⟩ := h    rcases h1 with h1 | h1    · subst h1      left      use a2, a3      simp_all      rw [← hsum]      abel    rcases h2 with h2 | h2    · subst h2      left      use a1, a3      simp_all      rw [← hsum]      abel    rcases h3 with h3 | h3    · subst h3      left      use a1, a2      simp_all    right    use a1, a2, a3  · match qHu with    | none => simp at h    | some qHu => simp_all  · match qHd, qHu with    | none, _ => simp at h    | some x, none => simp at h    | some qHd, some qHu => simp_all  · obtain ⟨a1, a2, a3, ⟨h1, h2, h3⟩, hsum⟩ := h    rcases h2 with h2 | h2    · left      use a1, a3      simp_all      rw [← hsum]      abel    rcases h3 with h3 | h3    · left      use a1, a2      simp_all    right    use a1, a2, a3  · match qHd, qHu with    | none, _ => simp at h    | some x, none => simp at h    | some qHd, some qHu => simp_all  · match qHu with    | none => simp at h    | 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      · subst h2        left        rw [← hsum]        abel      · right        use a2        simp_all        rw [← hsum]        abel    rcases h2 with h2 | h2    · subst h2      left; right      use a1      simp_all      rw [← hsum]      abel    · right      simp only [Multiset.mem_map, Multiset.mem_product, Finset.mem_val, Prod.exists]      use a1, a2  · match qHd with    | none => simp at h    | some qHd =>    simp_all    obtain ⟨a1, a2, ⟨h1, h2⟩, hsum⟩ := h    rcases h2 with h2 | h2    · subst h2      left      use a1      simp_all      rw [← hsum]      abel    right    use a1, a2