Theorem: IdealHelpers.generators_extension (Diploma/Algebra/IdealHelpers.lean)

State before:
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
Tactic:
rw [asIdeal, asIdeal, list_union_as_set, span_union]
State after:
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)

State before:
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)
Tactic:
have subset := subsets_h extension (asIdeal generators) in_ideal
State after:
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 generators) ⊔ span (asSet extension) = span (asSet generators)

State before:
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 generators) ⊔ span (asSet extension) = span (asSet generators)
Tactic:
simp [span_mono]
State after:
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)

State before:
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)
Tactic:
simp [←span_le] at *
State after:
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)

State before:
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)
Tactic:
rw [asIdeal] at subset
State after:
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) ≤ span (asSet generators)
⊢ span (asSet extension) ≤ span (asSet generators)

State before:
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) ≤ span (asSet generators)
⊢ span (asSet extension) ≤ span (asSet generators)
Tactic:
exact subset
State after:
no goals