rename_i q r sum_eq _ p_in_ideal r_in_ideal
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
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