rw [asIdeal, asIdeal, list_union_as_set, span_union]
n : ℕ
ord : Type
inst✝ : MonomialOrder (Variables n ord)
generators extension : List (Polynomial n ord)
in_ideal : ∀ (e : Polynomial n ord), e ∈ extension → e ∈ asIdeal generators
⊢ asIdeal (generators ++ extension) = asIdeal generators
n : ℕ
ord : Type
inst✝ : MonomialOrder (Variables n ord)
generators extension : List (Polynomial n ord)
in_ideal : ∀ (e : Polynomial n ord), e ∈ extension → e ∈ asIdeal generators
⊢ span (asSet generators) ⊔ span (asSet extension) = span (asSet generators)