internlm/Lean-Github huggingface dataset:
Theorem: IdealHelpers.list_union_as_set
Proof state before:
case cons
α : Type u_1
l₁ : List α
head✝ : α
tail✝ : List α
tail_ih✝ : asSet (l₁ ++ tail✝) = asSet l₁ ∪ asSet tail✝
⊢ asSet (l₁ ++ head✝ :: tail✝) = asSet l₁ ∪ asSet (head✝ :: tail✝)
Tactic:
simp [asSet]
Proof state after:
case cons
α : Type u_1
l₁ : List α
head✝ : α
tail✝ : List α
tail_ih✝ : asSet (l₁ ++ tail✝) = asSet l₁ ∪ asSet tail✝
⊢ { x | x ∈ l₁ ∨ x = head✝ ∨ x ∈ tail✝ } = { x | x ∈ l₁ } ∪ { x | x = head✝ ∨ x ∈ tail✝ }
Theorem: IdealHelpers.list_union_as_set
Proof state before:
case cons
α : Type u_1
l₁ : List α
head✝ : α
tail✝ : List α
tail_ih✝ : asSet (l₁ ++ tail✝) = asSet l₁ ∪ asSet tail✝
⊢ { x | x ∈ l₁ ∨ x = head✝ ∨ x ∈ tail✝ } = { x | x ∈ l₁ } ∪ { x | x = head✝ ∨ x ∈ tail✝ }
Tactic:
constructor
Proof state after:
no goals
Theorem: IdealHelpers.listInIdeal
Proof state before:
α : Type u_1
inst✝ : Semiring α
l : List α
⊢ ∀ (x : α), x ∈ l → x ∈ asIdeal l
Tactic:
intros y h
Proof state after:
α : Type u_1
inst✝ : Semiring α
l : List α
y : α
h : y ∈ l
⊢ y ∈ asIdeal l
Theorem: IdealHelpers.listInIdeal
Proof state before:
α : Type u_1
inst✝ : Semiring α
l : List α
y : α
h : y ∈ l
⊢ y ∈ asIdeal l
Tactic:
rw [asIdeal, asSet]
Proof state after:
α : Type u_1
inst✝ : Semiring α
l : List α
y : α
h : y ∈ l
⊢ y ∈ span { x | x ∈ l }
Theorem: IdealHelpers.listInIdeal
Proof state before:
α : Type u_1
inst✝ : Semiring α
l : List α
y : α
h : y ∈ l
⊢ y ∈ span { x | x ∈ l }
Tactic:
have in_set := listInSet l y h
Proof state after:
α : Type u_1
inst✝ : Semiring α
l : List α
y : α
h : y ∈ l
in_set : y ∈ asSet l
⊢ y ∈ span { x | x ∈ l }
Theorem: IdealHelpers.listInIdeal
Proof state before:
α : Type u_1
inst✝ : Semiring α
l : List α
y : α
h : y ∈ l
in_set : y ∈ asSet l
⊢ y ∈ span { x | x ∈ l }
Tactic:
rw [asSet] at in_set
Proof state after:
α : Type u_1
inst✝ : Semiring α
l : List α
y : α
h : y ∈ l
in_set : y ∈ { x | x ∈ l }
⊢ y ∈ span { x | x ∈ l }
Theorem: IdealHelpers.listInIdeal
Proof state before:
α : Type u_1
inst✝ : Semiring α
l : List α
y : α
h : y ∈ l
in_set : y ∈ { x | x ∈ l }
⊢ y ∈ span { x | x ∈ l }
Tactic:
apply Ideal.subset_span
Proof state after:
case a
α : Type u_1
inst✝ : Semiring α
l : List α
y : α
h : y ∈ l
in_set : y ∈ { x | x ∈ l }
⊢ y ∈ { x | x ∈ l }
Theorem: IdealHelpers.listInIdeal
Proof state before:
case a
α : Type u_1
inst✝ : Semiring α
l : List α
y : α
h : y ∈ l
in_set : y ∈ { x | x ∈ l }
⊢ y ∈ { x | x ∈ l }
Tactic:
exact in_set
Proof state after:
no goals
Theorem: IdealHelpers.elemInListElemInIdeal
Proof state before:
α : Type u_1
inst✝ : Semiring α
l : List α
x : α
h : x ∈ l
⊢ x ∈ asIdeal l
Tactic:
have list_in_ideal := listInIdeal l
Proof state after:
α : Type u_1
inst✝ : Semiring α
l : List α
x : α
h : x ∈ l
list_in_ideal : ∀ (x : α), x ∈ l → x ∈ asIdeal l
⊢ x ∈ asIdeal l
Theorem: IdealHelpers.elemInListElemInIdeal
Proof state before:
α : Type u_1
inst✝ : Semiring α
l : List α
x : α
h : x ∈ l
list_in_ideal : ∀ (x : α), x ∈ l → x ∈ asIdeal l
⊢ x ∈ asIdeal l
Tactic:
exact list_in_ideal x h
Proof state after:
no goals
Theorem: IdealHelpers.subsets_h
Proof state before:
α : Type u_1
l : List α
s : Set α
h : ∀ (e : α), e ∈ l → e ∈ s
⊢ asSet l ⊆ s
Tactic:
rw [asSet]
Proof state after:
α : Type u_1
l : List α
s : Set α
h : ∀ (e : α), e ∈ l → e ∈ s
⊢ { x | x ∈ l } ⊆ s
Theorem: IdealHelpers.subsets_h
Proof state before:
α : Type u_1
l : List α
s : Set α
h : ∀ (e : α), e ∈ l → e ∈ s
⊢ { x | x ∈ l } ⊆ s
Tactic:
exact h
Proof state after:
no goals
Theorem: IdealHelpers.generators_extension
Proof 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]
Proof 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)
Theorem: IdealHelpers.generators_extension
Proof 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
Proof 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)
Theorem: IdealHelpers.generators_extension
Proof 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]
Proof 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)
Theorem: IdealHelpers.generators_extension
Proof 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 *
Proof 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)
Theorem: IdealHelpers.generators_extension
Proof 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
Proof 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)
Theorem: IdealHelpers.generators_extension
Proof 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
Proof state after:
no goals
Theorem: polynomial.s_poly_in_ideal
Proof state before:
n : ℕ
ord : Type
inst✝ : MonomialOrder (Variables n ord)
ideal : Ideal (Polynomial n ord)
⊢ ∀ (p : Polynomial n ord), p ∈ ideal → ∀ (q : Polynomial n ord), q ∈ ideal → build_s_polynomial p q ∈ ideal
Tactic:
intros p h_in_p q h_in_q
Proof state after:
n : ℕ
ord : Type
inst✝ : MonomialOrder (Variables n ord)
ideal : Ideal (Polynomial n ord)
p : Polynomial n ord
h_in_p : p ∈ ideal
q : Polynomial n ord
h_in_q : q ∈ ideal
⊢ build_s_polynomial p q ∈ ideal
Theorem: polynomial.s_poly_in_ideal
Proof state before:
n : ℕ
ord : Type
inst✝ : MonomialOrder (Variables n ord)
ideal : Ideal (Polynomial n ord)
p : Polynomial n ord
h_in_p : p ∈ ideal
q : Polynomial n ord
h_in_q : q ∈ ideal
⊢ build_s_polynomial p q ∈ ideal
Tactic:
rw [build_s_polynomial]
Proof state after:
n : ℕ
ord : Type
inst✝ : MonomialOrder (Variables n ord)
ideal : Ideal (Polynomial n ord)
p : Polynomial n ord
h_in_p : p ∈ ideal
q : Polynomial n ord
h_in_q : q ∈ ideal
⊢ build_s_polynomial.div_lcm_lt (build_s_polynomial.lcm p q) (Polynomial.lt p) * p -
      build_s_polynomial.div_lcm_lt (build_s_polynomial.lcm p q) (Polynomial.lt q) * q ∈
    ideal
Theorem: polynomial.s_poly_in_ideal
Proof state before:
n : ℕ
ord : Type
inst✝ : MonomialOrder (Variables n ord)
ideal : Ideal (Polynomial n ord)
p : Polynomial n ord
h_in_p : p ∈ ideal
q : Polynomial n ord
h_in_q : q ∈ ideal
⊢ build_s_polynomial.div_lcm_lt (build_s_polynomial.lcm p q) (Polynomial.lt p) * p -
      build_s_polynomial.div_lcm_lt (build_s_polynomial.lcm p q) (Polynomial.lt q) * q ∈
    ideal
Tactic:
have left_mem
  : build_s_polynomial.div_lcm_lt (build_s_polynomial.lcm p q) (Polynomial.lt p) * p ∈ ideal
Proof state after:
case left_mem
n : ℕ
ord : Type
inst✝ : MonomialOrder (Variables n ord)
ideal : Ideal (Polynomial n ord)
p : Polynomial n ord
h_in_p : p ∈ ideal
q : Polynomial n ord
h_in_q : q ∈ ideal
⊢ build_s_polynomial.div_lcm_lt (build_s_polynomial.lcm p q) (Polynomial.lt p) * p ∈ ideal

n : ℕ
ord : Type
inst✝ : MonomialOrder (Variables n ord)
ideal : Ideal (Polynomial n ord)
p : Polynomial n ord
h_in_p : p ∈ ideal
q : Polynomial n ord
h_in_q : q ∈ ideal
left_mem : build_s_polynomial.div_lcm_lt (build_s_polynomial.lcm p q) (Polynomial.lt p) * p ∈ ideal
⊢ build_s_polynomial.div_lcm_lt (build_s_polynomial.lcm p q) (Polynomial.lt p) * p -
      build_s_polynomial.div_lcm_lt (build_s_polynomial.lcm p q) (Polynomial.lt q) * q ∈
    ideal
Theorem: polynomial.s_poly_in_ideal
Proof state before:
case left_mem
n : ℕ
ord : Type
inst✝ : MonomialOrder (Variables n ord)
ideal : Ideal (Polynomial n ord)
p : Polynomial n ord
h_in_p : p ∈ ideal
q : Polynomial n ord
h_in_q : q ∈ ideal
⊢ build_s_polynomial.div_lcm_lt (build_s_polynomial.lcm p q) (Polynomial.lt p) * p ∈ ideal

n : ℕ
ord : Type
inst✝ : MonomialOrder (Variables n ord)
ideal : Ideal (Polynomial n ord)
p : Polynomial n ord
h_in_p : p ∈ ideal
q : Polynomial n ord
h_in_q : q ∈ ideal
left_mem : build_s_polynomial.div_lcm_lt (build_s_polynomial.lcm p q) (Polynomial.lt p) * p ∈ ideal
⊢ build_s_polynomial.div_lcm_lt (build_s_polynomial.lcm p q) (Polynomial.lt p) * p -
      build_s_polynomial.div_lcm_lt (build_s_polynomial.lcm p q) (Polynomial.lt q) * q ∈
    ideal
Tactic:
exact mul_mem_left ideal 
                   (build_s_polynomial.div_lcm_lt (build_s_polynomial.lcm p q) (Polynomial.lt p)) 
                   h_in_p
Proof state after:
n : ℕ
ord : Type
inst✝ : MonomialOrder (Variables n ord)
ideal : Ideal (Polynomial n ord)
p : Polynomial n ord
h_in_p : p ∈ ideal
q : Polynomial n ord
h_in_q : q ∈ ideal
left_mem : build_s_polynomial.div_lcm_lt (build_s_polynomial.lcm p q) (Polynomial.lt p) * p ∈ ideal
⊢ build_s_polynomial.div_lcm_lt (build_s_polynomial.lcm p q) (Polynomial.lt p) * p -
      build_s_polynomial.div_lcm_lt (build_s_polynomial.lcm p q) (Polynomial.lt q) * q ∈
    ideal
Theorem: polynomial.s_poly_in_ideal
Proof state before:
n : ℕ
ord : Type
inst✝ : MonomialOrder (Variables n ord)
ideal : Ideal (Polynomial n ord)
p : Polynomial n ord
h_in_p : p ∈ ideal
q : Polynomial n ord
h_in_q : q ∈ ideal
left_mem : build_s_polynomial.div_lcm_lt (build_s_polynomial.lcm p q) (Polynomial.lt p) * p ∈ ideal
⊢ build_s_polynomial.div_lcm_lt (build_s_polynomial.lcm p q) (Polynomial.lt p) * p -
      build_s_polynomial.div_lcm_lt (build_s_polynomial.lcm p q) (Polynomial.lt q) * q ∈
    ideal
Tactic:
have right_mem
  : build_s_polynomial.div_lcm_lt (build_s_polynomial.lcm p q) (Polynomial.lt q) * q ∈ ideal
Proof state after:
case right_mem
n : ℕ
ord : Type
inst✝ : MonomialOrder (Variables n ord)
ideal : Ideal (Polynomial n ord)
p : Polynomial n ord
h_in_p : p ∈ ideal
q : Polynomial n ord
h_in_q : q ∈ ideal
left_mem : build_s_polynomial.div_lcm_lt (build_s_polynomial.lcm p q) (Polynomial.lt p) * p ∈ ideal
⊢ build_s_polynomial.div_lcm_lt (build_s_polynomial.lcm p q) (Polynomial.lt q) * q ∈ ideal

n : ℕ
ord : Type
inst✝ : MonomialOrder (Variables n ord)
ideal : Ideal (Polynomial n ord)
p : Polynomial n ord
h_in_p : p ∈ ideal
q : Polynomial n ord
h_in_q : q ∈ ideal
left_mem : build_s_polynomial.div_lcm_lt (build_s_polynomial.lcm p q) (Polynomial.lt p) * p ∈ ideal
right_mem : build_s_polynomial.div_lcm_lt (build_s_polynomial.lcm p q) (Polynomial.lt q) * q ∈ ideal
⊢ build_s_polynomial.div_lcm_lt (build_s_polynomial.lcm p q) (Polynomial.lt p) * p -
      build_s_polynomial.div_lcm_lt (build_s_polynomial.lcm p q) (Polynomial.lt q) * q ∈
    ideal
Theorem: polynomial.s_poly_in_ideal
Proof state before:
case right_mem
n : ℕ
ord : Type
inst✝ : MonomialOrder (Variables n ord)
ideal : Ideal (Polynomial n ord)
p : Polynomial n ord
h_in_p : p ∈ ideal
q : Polynomial n ord
h_in_q : q ∈ ideal
left_mem : build_s_polynomial.div_lcm_lt (build_s_polynomial.lcm p q) (Polynomial.lt p) * p ∈ ideal
⊢ build_s_polynomial.div_lcm_lt (build_s_polynomial.lcm p q) (Polynomial.lt q) * q ∈ ideal

n : ℕ
ord : Type
inst✝ : MonomialOrder (Variables n ord)
ideal : Ideal (Polynomial n ord)
p : Polynomial n ord
h_in_p : p ∈ ideal
q : Polynomial n ord
h_in_q : q ∈ ideal
left_mem : build_s_polynomial.div_lcm_lt (build_s_polynomial.lcm p q) (Polynomial.lt p) * p ∈ ideal
right_mem : build_s_polynomial.div_lcm_lt (build_s_polynomial.lcm p q) (Polynomial.lt q) * q ∈ ideal
⊢ build_s_polynomial.div_lcm_lt (build_s_polynomial.lcm p q) (Polynomial.lt p) * p -
      build_s_polynomial.div_lcm_lt (build_s_polynomial.lcm p q) (Polynomial.lt q) * q ∈
    ideal
Tactic:
exact mul_mem_left ideal 
                   (build_s_polynomial.div_lcm_lt (build_s_polynomial.lcm p q) (Polynomial.lt q)) 
                   h_in_q
Proof state after:
n : ℕ
ord : Type
inst✝ : MonomialOrder (Variables n ord)
ideal : Ideal (Polynomial n ord)
p : Polynomial n ord
h_in_p : p ∈ ideal
q : Polynomial n ord
h_in_q : q ∈ ideal
left_mem : build_s_polynomial.div_lcm_lt (build_s_polynomial.lcm p q) (Polynomial.lt p) * p ∈ ideal
right_mem : build_s_polynomial.div_lcm_lt (build_s_polynomial.lcm p q) (Polynomial.lt q) * q ∈ ideal
⊢ build_s_polynomial.div_lcm_lt (build_s_polynomial.lcm p q) (Polynomial.lt p) * p -
      build_s_polynomial.div_lcm_lt (build_s_polynomial.lcm p q) (Polynomial.lt q) * q ∈
    ideal
Theorem: polynomial.s_poly_in_ideal
Proof state before:
n : ℕ
ord : Type
inst✝ : MonomialOrder (Variables n ord)
ideal : Ideal (Polynomial n ord)
p : Polynomial n ord
h_in_p : p ∈ ideal
q : Polynomial n ord
h_in_q : q ∈ ideal
left_mem : build_s_polynomial.div_lcm_lt (build_s_polynomial.lcm p q) (Polynomial.lt p) * p ∈ ideal
right_mem : build_s_polynomial.div_lcm_lt (build_s_polynomial.lcm p q) (Polynomial.lt q) * q ∈ ideal
⊢ build_s_polynomial.div_lcm_lt (build_s_polynomial.lcm p q) (Polynomial.lt p) * p -
      build_s_polynomial.div_lcm_lt (build_s_polynomial.lcm p q) (Polynomial.lt q) * q ∈
    ideal
Tactic:
exact sub_mem left_mem right_mem
Proof state after:
no goals
Theorem: polynomial.div_sum_r_eq_p
Proof state before:
n : ℕ
ord : Type
inst✝ : MonomialOrder (Variables n ord)
divisible p quotient remainder : Polynomial n ord
sum_eq : divisible = p + quotient + remainder
h : (p == 0) = true
⊢ divisible = quotient + remainder
Tactic:
have eq_zero := beq_eq p h
Proof state after:
n : ℕ
ord : Type
inst✝ : MonomialOrder (Variables n ord)
divisible p quotient remainder : Polynomial n ord
sum_eq : divisible = p + quotient + remainder
h : (p == 0) = true
eq_zero : p = 0
⊢ divisible = quotient + remainder
Theorem: polynomial.div_sum_r_eq_p
Proof state before:
n : ℕ
ord : Type
inst✝ : MonomialOrder (Variables n ord)
divisible p quotient remainder : Polynomial n ord
sum_eq : divisible = p + quotient + remainder
h : (p == 0) = true
eq_zero : p = 0
⊢ divisible = quotient + remainder
Tactic:
rw [eq_zero, zero_add] at sum_eq
Proof state after:
n : ℕ
ord : Type
inst✝ : MonomialOrder (Variables n ord)
divisible p quotient remainder : Polynomial n ord
sum_eq : divisible = quotient + remainder
h : (p == 0) = true
eq_zero : p = 0
⊢ divisible = quotient + remainder
Theorem: polynomial.div_sum_r_eq_p
Proof state before:
n : ℕ
ord : Type
inst✝ : MonomialOrder (Variables n ord)
divisible p quotient remainder : Polynomial n ord
sum_eq : divisible = quotient + remainder
h : (p == 0) = true
eq_zero : p = 0
⊢ divisible = quotient + remainder
Tactic:
exact sum_eq
Proof state after:
no goals
Theorem: polynomial.erase_lt
Proof state before:
n : ℕ
ord : Type
inst✝ : MonomialOrder (Variables n ord)
divisible p quotient remainder : Polynomial n ord
sum_eq : divisible = p + quotient + remainder
⊢ divisible = p - Polynomial.Lt p + quotient + (remainder + Polynomial.Lt p)
Tactic:
have h: remainder + Polynomial.Lt p = Polynomial.Lt p + remainder := 
  add_comm remainder (Polynomial.Lt p)
Proof state after:
n : ℕ
ord : Type
inst✝ : MonomialOrder (Variables n ord)
divisible p quotient remainder : Polynomial n ord
sum_eq : divisible = p + quotient + remainder
h : remainder + Polynomial.Lt p = Polynomial.Lt p + remainder
⊢ divisible = p - Polynomial.Lt p + quotient + (remainder + Polynomial.Lt p)
Theorem: polynomial.erase_lt
Proof state before:
n : ℕ
ord : Type
inst✝ : MonomialOrder (Variables n ord)
divisible p quotient remainder : Polynomial n ord
sum_eq : divisible = p + quotient + remainder
h : remainder + Polynomial.Lt p = Polynomial.Lt p + remainder
⊢ divisible = p - Polynomial.Lt p + quotient + (remainder + Polynomial.Lt p)
Tactic:
have h₂: -Polynomial.Lt p + quotient = quotient + -Polynomial.Lt p :=
  add_comm (-Polynomial.Lt p) quotient
Proof state after:
n : ℕ
ord : Type
inst✝ : MonomialOrder (Variables n ord)
divisible p quotient remainder : Polynomial n ord
sum_eq : divisible = p + quotient + remainder
h : remainder + Polynomial.Lt p = Polynomial.Lt p + remainder
h₂ : -Polynomial.Lt p + quotient = quotient + -Polynomial.Lt p
⊢ divisible = p - Polynomial.Lt p + quotient + (remainder + Polynomial.Lt p)
Theorem: polynomial.erase_lt
Proof state before:
n : ℕ
ord : Type
inst✝ : MonomialOrder (Variables n ord)
divisible p quotient remainder : Polynomial n ord
sum_eq : divisible = p + quotient + remainder
h : remainder + Polynomial.Lt p = Polynomial.Lt p + remainder
h₂ : -Polynomial.Lt p + quotient = quotient + -Polynomial.Lt p
⊢ divisible = p - Polynomial.Lt p + quotient + (remainder + Polynomial.Lt p)
Tactic:
rw [h, sub_eq_add_neg, add_assoc,
    add_assoc, add_comm, ←add_assoc,
    ←add_assoc, add_comm, h₂, add_comm, add_assoc, add_comm, 
    add_assoc, add_assoc, add_left_neg, add_zero, add_comm]
Proof state after:
n : ℕ
ord : Type
inst✝ : MonomialOrder (Variables n ord)
divisible p quotient remainder : Polynomial n ord
sum_eq : divisible = p + quotient + remainder
h : remainder + Polynomial.Lt p = Polynomial.Lt p + remainder
h₂ : -Polynomial.Lt p + quotient = quotient + -Polynomial.Lt p
⊢ divisible = p + quotient + remainder
Theorem: polynomial.erase_lt
Proof state before:
n : ℕ
ord : Type
inst✝ : MonomialOrder (Variables n ord)
divisible p quotient remainder : Polynomial n ord
sum_eq : divisible = p + quotient + remainder
h : remainder + Polynomial.Lt p = Polynomial.Lt p + remainder
h₂ : -Polynomial.Lt p + quotient = quotient + -Polynomial.Lt p
⊢ divisible = p + quotient + remainder
Tactic:
exact sum_eq
Proof state after:
no goals
Theorem: polynomial.erase_reducer
Proof state before:
n : ℕ
ord : Type
inst✝ : MonomialOrder (Variables n ord)
divisible p quotient remainder reducer : Polynomial n ord
sum_eq : divisible = p + quotient + remainder
⊢ divisible = p - reducer + (quotient + reducer) + remainder
Tactic:
have h: -reducer + (quotient + reducer) = (quotient + reducer) + -reducer := 
  add_comm (-reducer) (quotient + reducer)
Proof state after:
n : ℕ
ord : Type
inst✝ : MonomialOrder (Variables n ord)
divisible p quotient remainder reducer : Polynomial n ord
sum_eq : divisible = p + quotient + remainder
h : -reducer + (quotient + reducer) = quotient + reducer + -reducer
⊢ divisible = p - reducer + (quotient + reducer) + remainder
Theorem: polynomial.erase_reducer
Proof state before:
n : ℕ
ord : Type
inst✝ : MonomialOrder (Variables n ord)
divisible p quotient remainder reducer : Polynomial n ord
sum_eq : divisible = p + quotient + remainder
h : -reducer + (quotient + reducer) = quotient + reducer + -reducer
⊢ divisible = p - reducer + (quotient + reducer) + remainder
Tactic:
rw [sub_eq_add_neg, ←add_assoc, add_comm, add_assoc,
    add_assoc, h, add_assoc, add_right_neg, add_zero, add_comm]
Proof state after:
n : ℕ
ord : Type
inst✝ : MonomialOrder (Variables n ord)
divisible p quotient remainder reducer : Polynomial n ord
sum_eq : divisible = p + quotient + remainder
h : -reducer + (quotient + reducer) = quotient + reducer + -reducer
⊢ divisible = p + quotient + remainder
Theorem: polynomial.erase_reducer
Proof state before:
n : ℕ
ord : Type
inst✝ : MonomialOrder (Variables n ord)
divisible p quotient remainder reducer : Polynomial n ord
sum_eq : divisible = p + quotient + remainder
h : -reducer + (quotient + reducer) = quotient + reducer + -reducer
⊢ divisible = p + quotient + remainder
Tactic:
exact sum_eq
Proof state after:
no goals
Theorem: polynomial.zero_r_in_ideal
Proof state before:
n : ℕ
ord : Type
inst✝ : MonomialOrder (Variables n ord)
divisible : Polynomial n ord
dividers : List (Polynomial n ord)
⊢ divisible ∈ asIdeal dividers → 0 ∈ asIdeal dividers
Tactic:
intros
Proof state after:
n : ℕ
ord : Type
inst✝ : MonomialOrder (Variables n ord)
divisible : Polynomial n ord
dividers : List (Polynomial n ord)
a✝ : divisible ∈ asIdeal dividers
⊢ 0 ∈ asIdeal dividers
Theorem: polynomial.zero_r_in_ideal
Proof state before:
n : ℕ
ord : Type
inst✝ : MonomialOrder (Variables n ord)
divisible : Polynomial n ord
dividers : List (Polynomial n ord)
a✝ : divisible ∈ asIdeal dividers
⊢ 0 ∈ asIdeal dividers
Tactic:
simp
Proof state after:
no goals
Theorem: polynomial.remainder_in_ideal
Proof state before:
n : ℕ
ord : Type
inst✝ : MonomialOrder (Variables n ord)
divisible quotient remainder : Polynomial n ord
dividers : List (Polynomial n ord)
div_sum_r_eq_p : divisible = quotient + remainder
quotient_in_ideal : quotient ∈ asIdeal dividers
⊢ divisible ∈ asIdeal dividers → remainder ∈ asIdeal dividers
Tactic:
intros divisible_in_ideal
Proof state after:
n : ℕ
ord : Type
inst✝ : MonomialOrder (Variables n ord)
divisible quotient remainder : Polynomial n ord
dividers : List (Polynomial n ord)
div_sum_r_eq_p : divisible = quotient + remainder
quotient_in_ideal : quotient ∈ asIdeal dividers
divisible_in_ideal : divisible ∈ asIdeal dividers
⊢ remainder ∈ asIdeal dividers
Theorem: polynomial.remainder_in_ideal
Proof state before:
n : ℕ
ord : Type
inst✝ : MonomialOrder (Variables n ord)
divisible quotient remainder : Polynomial n ord
dividers : List (Polynomial n ord)
div_sum_r_eq_p : divisible = quotient + remainder
quotient_in_ideal : quotient ∈ asIdeal dividers
divisible_in_ideal : divisible ∈ asIdeal dividers
⊢ remainder ∈ asIdeal dividers
Tactic:
have r_eq: remainder = divisible - quotient
Proof state after:
case r_eq
n : ℕ
ord : Type
inst✝ : MonomialOrder (Variables n ord)
divisible quotient remainder : Polynomial n ord
dividers : List (Polynomial n ord)
div_sum_r_eq_p : divisible = quotient + remainder
quotient_in_ideal : quotient ∈ asIdeal dividers
divisible_in_ideal : divisible ∈ asIdeal dividers
⊢ remainder = divisible - quotient

n : ℕ
ord : Type
inst✝ : MonomialOrder (Variables n ord)
divisible quotient remainder : Polynomial n ord
dividers : List (Polynomial n ord)
div_sum_r_eq_p : divisible = quotient + remainder
quotient_in_ideal : quotient ∈ asIdeal dividers
divisible_in_ideal : divisible ∈ asIdeal dividers
r_eq : remainder = divisible - quotient
⊢ remainder ∈ asIdeal dividers