Theorem: polynomial.sufficiency_poly_in_ideal (Diploma/Polynomials/Groebner.lean)

State before:
n : ℕ
ord : Type
inst✝ : MonomialOrder (Variables n ord)
p : Polynomial n ord
dividers : List (Polynomial n ord)
dividers_non_empty : ¬(dividers == []) = true
not_div_by_zero : ¬(List.any dividers fun p => p == 0) = true
div_res : DivisionResult p dividers
h : div_res = divide_many p dividers dividers_non_empty not_div_by_zero
⊢ div_res.r = 0 → p ∈ asIdeal dividers
Tactic:
intros is_zero
State after:
n : ℕ
ord : Type
inst✝ : MonomialOrder (Variables n ord)
p : Polynomial n ord
dividers : List (Polynomial n ord)
dividers_non_empty : ¬(dividers == []) = true
not_div_by_zero : ¬(List.any dividers fun p => p == 0) = true
div_res : DivisionResult p dividers
h : div_res = divide_many p dividers dividers_non_empty not_div_by_zero
is_zero : div_res.r = 0
⊢ p ∈ asIdeal dividers

State before:
n : ℕ
ord : Type
inst✝ : MonomialOrder (Variables n ord)
p : Polynomial n ord
dividers : List (Polynomial n ord)
dividers_non_empty : ¬(dividers == []) = true
not_div_by_zero : ¬(List.any dividers fun p => p == 0) = true
div_res : DivisionResult p dividers
h : div_res = divide_many p dividers dividers_non_empty not_div_by_zero
is_zero : div_res.r = 0
⊢ p ∈ asIdeal dividers
Tactic:
cases div_res
State after:
case mk
n : ℕ
ord : Type
inst✝ : MonomialOrder (Variables n ord)
p : Polynomial n ord
dividers : List (Polynomial n ord)
dividers_non_empty : ¬(dividers == []) = true
not_div_by_zero : ¬(List.any dividers fun p => p == 0) = true
p✝ r✝ : Polynomial n ord
r_as_list✝ : List (Monomial n ord)
sum_eq✝ : p = p✝ + r✝
correct_r✝ :
  r_as_list✝ = [] ∨
    ∀ (m : Monomial n ord),
      m ∈ r_as_list✝ → ∀ (d : Polynomial n ord), d ∈ dividers → (Monomial.is_div m (Polynomial.lt d) == false) = true
p_in_ideal✝ : p✝ ∈ asIdeal dividers
r_in_ideal✝ : p ∈ asIdeal dividers → r✝ ∈ asIdeal dividers
h :
  { p := p✝, r := r✝, r_as_list := r_as_list✝, sum_eq := sum_eq✝, correct_r := correct_r✝, p_in_ideal := p_in_ideal✝,
      r_in_ideal := r_in_ideal✝ } =
    divide_many p dividers dividers_non_empty not_div_by_zero
is_zero :
  { p := p✝, r := r✝, r_as_list := r_as_list✝, sum_eq := sum_eq✝, correct_r := correct_r✝, p_in_ideal := p_in_ideal✝,
        r_in_ideal := r_in_ideal✝ }.r =
    0
⊢ p ∈ asIdeal dividers

State before:
case mk
n : ℕ
ord : Type
inst✝ : MonomialOrder (Variables n ord)
p : Polynomial n ord
dividers : List (Polynomial n ord)
dividers_non_empty : ¬(dividers == []) = true
not_div_by_zero : ¬(List.any dividers fun p => p == 0) = true
p✝ r✝ : Polynomial n ord
r_as_list✝ : List (Monomial n ord)
sum_eq✝ : p = p✝ + r✝
correct_r✝ :
  r_as_list✝ = [] ∨
    ∀ (m : Monomial n ord),
      m ∈ r_as_list✝ → ∀ (d : Polynomial n ord), d ∈ dividers → (Monomial.is_div m (Polynomial.lt d) == false) = true
p_in_ideal✝ : p✝ ∈ asIdeal dividers
r_in_ideal✝ : p ∈ asIdeal dividers → r✝ ∈ asIdeal dividers
h :
  { p := p✝, r := r✝, r_as_list := r_as_list✝, sum_eq := sum_eq✝, correct_r := correct_r✝, p_in_ideal := p_in_ideal✝,
      r_in_ideal := r_in_ideal✝ } =
    divide_many p dividers dividers_non_empty not_div_by_zero
is_zero :
  { p := p✝, r := r✝, r_as_list := r_as_list✝, sum_eq := sum_eq✝, correct_r := correct_r✝, p_in_ideal := p_in_ideal✝,
        r_in_ideal := r_in_ideal✝ }.r =
    0
⊢ p ∈ asIdeal dividers
Tactic:
rename_i q r sum_eq _ p_in_ideal r_in_ideal
State after:
case mk
n : ℕ
ord : Type
inst✝ : MonomialOrder (Variables n ord)
p : Polynomial n ord
dividers : List (Polynomial n ord)
dividers_non_empty : ¬(dividers == []) = true
not_div_by_zero : ¬(List.any dividers fun p => p == 0) = true
p✝ q : Polynomial n ord
r : List (Monomial n ord)
sum_eq : p = p✝ + q
correct_r✝ :
  r = [] ∨
    ∀ (m : Monomial n ord),
      m ∈ r → ∀ (d : Polynomial n ord), d ∈ dividers → (Monomial.is_div m (Polynomial.lt d) == false) = true
p_in_ideal : p✝ ∈ asIdeal dividers
r_in_ideal : p ∈ asIdeal dividers → q ∈ asIdeal dividers
h :
  { p := p✝, r := q, r_as_list := r, sum_eq := sum_eq, correct_r := correct_r✝, p_in_ideal := p_in_ideal,
      r_in_ideal := r_in_ideal } =
    divide_many p dividers dividers_non_empty not_div_by_zero
is_zero :
  { p := p✝, r := q, r_as_list := r, sum_eq := sum_eq, correct_r := correct_r✝, p_in_ideal := p_in_ideal,
        r_in_ideal := r_in_ideal }.r =
    0
⊢ p ∈ asIdeal dividers

State before:
case mk
n : ℕ
ord : Type
inst✝ : MonomialOrder (Variables n ord)
p : Polynomial n ord
dividers : List (Polynomial n ord)
dividers_non_empty : ¬(dividers == []) = true
not_div_by_zero : ¬(List.any dividers fun p => p == 0) = true
p✝ q : Polynomial n ord
r : List (Monomial n ord)
sum_eq : p = p✝ + q
correct_r✝ :
  r = [] ∨
    ∀ (m : Monomial n ord),
      m ∈ r → ∀ (d : Polynomial n ord), d ∈ dividers → (Monomial.is_div m (Polynomial.lt d) == false) = true
p_in_ideal : p✝ ∈ asIdeal dividers
r_in_ideal : p ∈ asIdeal dividers → q ∈ asIdeal dividers
h :
  { p := p✝, r := q, r_as_list := r, sum_eq := sum_eq, correct_r := correct_r✝, p_in_ideal := p_in_ideal,
      r_in_ideal := r_in_ideal } =
    divide_many p dividers dividers_non_empty not_div_by_zero
is_zero :
  { p := p✝, r := q, r_as_list := r, sum_eq := sum_eq, correct_r := correct_r✝, p_in_ideal := p_in_ideal,
        r_in_ideal := r_in_ideal }.r =
    0
⊢ p ∈ asIdeal dividers
Tactic:
simp at *
State after:
case mk
n : ℕ
ord : Type
inst✝ : MonomialOrder (Variables n ord)
p : Polynomial n ord
dividers : List (Polynomial n ord)
dividers_non_empty : ¬(dividers == []) = true
not_div_by_zero : ¬(List.any dividers fun p => p == 0) = true
p✝ q : Polynomial n ord
r : List (Monomial n ord)
sum_eq : p = p✝ + q
correct_r✝ :
  r = [] ∨
    ∀ (m : Monomial n ord),
      m ∈ r → ∀ (d : Polynomial n ord), d ∈ dividers → (Monomial.is_div m (Polynomial.lt d) == false) = true
p_in_ideal : p✝ ∈ asIdeal dividers
r_in_ideal : p ∈ asIdeal dividers → q ∈ asIdeal dividers
h :
  { p := p✝, r := q, r_as_list := r, sum_eq := sum_eq, correct_r := correct_r✝, p_in_ideal := p_in_ideal,
      r_in_ideal := r_in_ideal } =
    divide_many p dividers dividers_non_empty not_div_by_zero
is_zero : q = 0
⊢ p ∈ asIdeal dividers

State before:
case mk
n : ℕ
ord : Type
inst✝ : MonomialOrder (Variables n ord)
p : Polynomial n ord
dividers : List (Polynomial n ord)
dividers_non_empty : ¬(dividers == []) = true
not_div_by_zero : ¬(List.any dividers fun p => p == 0) = true
p✝ q : Polynomial n ord
r : List (Monomial n ord)
sum_eq : p = p✝ + q
correct_r✝ :
  r = [] ∨
    ∀ (m : Monomial n ord),
      m ∈ r → ∀ (d : Polynomial n ord), d ∈ dividers → (Monomial.is_div m (Polynomial.lt d) == false) = true
p_in_ideal : p✝ ∈ asIdeal dividers
r_in_ideal : p ∈ asIdeal dividers → q ∈ asIdeal dividers
h :
  { p := p✝, r := q, r_as_list := r, sum_eq := sum_eq, correct_r := correct_r✝, p_in_ideal := p_in_ideal,
      r_in_ideal := r_in_ideal } =
    divide_many p dividers dividers_non_empty not_div_by_zero
is_zero : q = 0
⊢ p ∈ asIdeal dividers
Tactic:
simp [is_zero] at sum_eq
State after:
case mk
n : ℕ
ord : Type
inst✝ : MonomialOrder (Variables n ord)
p : Polynomial n ord
dividers : List (Polynomial n ord)
dividers_non_empty : ¬(dividers == []) = true
not_div_by_zero : ¬(List.any dividers fun p => p == 0) = true
p✝ q : Polynomial n ord
r : List (Monomial n ord)
sum_eq✝ : p = p✝ + q
correct_r✝ :
  r = [] ∨
    ∀ (m : Monomial n ord),
      m ∈ r → ∀ (d : Polynomial n ord), d ∈ dividers → (Monomial.is_div m (Polynomial.lt d) == false) = true
p_in_ideal : p✝ ∈ asIdeal dividers
r_in_ideal : p ∈ asIdeal dividers → q ∈ asIdeal dividers
h :
  { p := p✝, r := q, r_as_list := r, sum_eq := sum_eq✝, correct_r := correct_r✝, p_in_ideal := p_in_ideal,
      r_in_ideal := r_in_ideal } =
    divide_many p dividers dividers_non_empty not_div_by_zero
is_zero : q = 0
sum_eq : p = p✝
⊢ p ∈ asIdeal dividers

State before:
case mk
n : ℕ
ord : Type
inst✝ : MonomialOrder (Variables n ord)
p : Polynomial n ord
dividers : List (Polynomial n ord)
dividers_non_empty : ¬(dividers == []) = true
not_div_by_zero : ¬(List.any dividers fun p => p == 0) = true
p✝ q : Polynomial n ord
r : List (Monomial n ord)
sum_eq✝ : p = p✝ + q
correct_r✝ :
  r = [] ∨
    ∀ (m : Monomial n ord),
      m ∈ r → ∀ (d : Polynomial n ord), d ∈ dividers → (Monomial.is_div m (Polynomial.lt d) == false) = true
p_in_ideal : p✝ ∈ asIdeal dividers
r_in_ideal : p ∈ asIdeal dividers → q ∈ asIdeal dividers
h :
  { p := p✝, r := q, r_as_list := r, sum_eq := sum_eq✝, correct_r := correct_r✝, p_in_ideal := p_in_ideal,
      r_in_ideal := r_in_ideal } =
    divide_many p dividers dividers_non_empty not_div_by_zero
is_zero : q = 0
sum_eq : p = p✝
⊢ p ∈ asIdeal dividers
Tactic:
rw [sum_eq]
State after:
case mk
n : ℕ
ord : Type
inst✝ : MonomialOrder (Variables n ord)
p : Polynomial n ord
dividers : List (Polynomial n ord)
dividers_non_empty : ¬(dividers == []) = true
not_div_by_zero : ¬(List.any dividers fun p => p == 0) = true
p✝ q : Polynomial n ord
r : List (Monomial n ord)
sum_eq✝ : p = p✝ + q
correct_r✝ :
  r = [] ∨
    ∀ (m : Monomial n ord),
      m ∈ r → ∀ (d : Polynomial n ord), d ∈ dividers → (Monomial.is_div m (Polynomial.lt d) == false) = true
p_in_ideal : p✝ ∈ asIdeal dividers
r_in_ideal : p ∈ asIdeal dividers → q ∈ asIdeal dividers
h :
  { p := p✝, r := q, r_as_list := r, sum_eq := sum_eq✝, correct_r := correct_r✝, p_in_ideal := p_in_ideal,
      r_in_ideal := r_in_ideal } =
    divide_many p dividers dividers_non_empty not_div_by_zero
is_zero : q = 0
sum_eq : p = p✝
⊢ p✝ ∈ asIdeal dividers

State before:
case mk
n : ℕ
ord : Type
inst✝ : MonomialOrder (Variables n ord)
p : Polynomial n ord
dividers : List (Polynomial n ord)
dividers_non_empty : ¬(dividers == []) = true
not_div_by_zero : ¬(List.any dividers fun p => p == 0) = true
p✝ q : Polynomial n ord
r : List (Monomial n ord)
sum_eq✝ : p = p✝ + q
correct_r✝ :
  r = [] ∨
    ∀ (m : Monomial n ord),
      m ∈ r → ∀ (d : Polynomial n ord), d ∈ dividers → (Monomial.is_div m (Polynomial.lt d) == false) = true
p_in_ideal : p✝ ∈ asIdeal dividers
r_in_ideal : p ∈ asIdeal dividers → q ∈ asIdeal dividers
h :
  { p := p✝, r := q, r_as_list := r, sum_eq := sum_eq✝, correct_r := correct_r✝, p_in_ideal := p_in_ideal,
      r_in_ideal := r_in_ideal } =
    divide_many p dividers dividers_non_empty not_div_by_zero
is_zero : q = 0
sum_eq : p = p✝
⊢ p✝ ∈ asIdeal dividers
Tactic:
exact p_in_ideal
State after:
no goals