Allows Term insert Q5 of allows Term Q5

lemma allowsTerm_insertQ5_of_allowsTermQ5 {qHd qHu : Option 𝓩}    {Q5 Q10: Finset 𝓩} {q5 : 𝓩} (T : PotentialTerm)    (h : AllowsTermQ5 ⟨qHd, qHu, Q5, Q10⟩ q5 T) :    AllowsTerm ⟨qHd, qHu, insert q5 Q5, Q10⟩ T := by  rcases T  all_goals    simp [AllowsTermQ5] at h  all_goals    simp [allowsTerm_iff_zero_mem_ofPotentialTerm', ofPotentialTerm']  · match qHu with    | some qHu =>      simp at h      subst h      simp    | none => simp at h  · obtain ⟨q1, q2, ⟨h1, h2⟩, hsum⟩ := h    use q1, q5, q2    simp_all  · obtain ⟨q1, q2, q3, h3, hsum⟩ := h    use q5, q1, q2, q3    simp_all  · match qHu with    | some qHu =>      simp at h      simp only [Multiset.mem_map, Multiset.mem_product, Multiset.mem_ndinsert, Finset.mem_val,        Prod.exists]      by_cases h' : q5 + q5 - qHu - qHu = 0      · use q5, q5        simp only [true_or, and_self, true_and]        rw [← h']        abel      · simp_all        obtain ⟨q1, hsum⟩ := h        use q1, q5        simp_all        rw [← hsum.2]        abel    | none => simp at h  · match qHd, qHu with    | some qHd, some qHu =>      simp_all      left      rw [← h]      abel    | none, _ => simp at h    | some x, none => simp at h  · obtain ⟨q1, q2, ⟨h1, h2⟩, hsum⟩ := h    use q5, q1, q2    simp_all  · match qHd with    | none => simp at h    | some qHd =>      simp at h      obtain ⟨q1, h1, hsum⟩ := h      simp only [Multiset.mem_map, Multiset.mem_product, Multiset.mem_ndinsert, Finset.mem_val,        Prod.exists]      use q5, q1      simp_all      rw [← hsum]      abel