Allows Term insert Q10 of allows Term Q10

lemma allowsTerm_insertQ10_of_allowsTermQ10 {qHd qHu : Option 𝓩}    {Q5 Q10: Finset 𝓩} {q10 : 𝓩} (T : PotentialTerm)    (h : AllowsTermQ10 ⟨qHd, qHu, Q5, Q10⟩ q10 T) :    AllowsTerm ⟨qHd, qHu, Q5, insert q10 Q10⟩ T := by  rcases T  all_goals    simp [AllowsTermQ10] at h  all_goals    simp [allowsTerm_iff_zero_mem_ofPotentialTerm', ofPotentialTerm']  · obtain ⟨a1, a2, ⟨h1, h2⟩, hsum⟩ := h    use a1, a2, q10    simp_all  · obtain ⟨a1, a2, a3, ⟨h1, h2, h3⟩, hsum⟩ := h    use a1, a2, a3, q10    simp_all  · match qHd with    | none => simp at h    | some qHd =>      simp at h ⊢      obtain ⟨a1, a2, ⟨h1, h2⟩, hsum⟩ := h      use a1, a2, q10      simp_all  · obtain ⟨a1, a2, ⟨h1, h2⟩, hsum⟩ := h    use a1, a2, q10    simp_all  · 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 ⊢      rcases h with h | h      · use q10, q10        rw [← h]        simp only [true_or, and_self, true_and]        abel      · obtain ⟨a1, h1, hsum⟩ := h        use a1, q10        simp_all        rw [← hsum]        abel  · match qHd with    | none => simp at h    | some qHd =>      simp at h ⊢      obtain ⟨a1, h1, hsum⟩ := h      use a1, q10      simp_all      rw [← hsum]      abel