simp [←span_le] at *
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
subset : asSet extension ⊆ ↑(asIdeal generators)
⊢ span (asSet extension) ≤ span (asSet 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
subset : span (asSet extension) ≤ asIdeal generators
⊢ span (asSet extension) ≤ span (asSet generators)