Theorem: polynomial.s_poly_in_ideal (Diploma/Polynomials/Division.lean)

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
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

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]
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

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
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

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
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

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
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

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
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

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
State after:
no goals