internlm/Lean-Github huggingface dataset:
Theorem: polynomial.pair_in_list₂
Proof state before:
case left
α : Type u_1
l✝ : List α
pairs✝ : List (α × α)
h✝ : pairs✝ = build_pairs l✝
l : List α
pairs : List (α × α)
p : α × α
x : α
xs : List α
h : pairs = build_pairs.pairs x xs ++ build_pairs xs
in_pairs : p ∈ build_pairs.pairs x xs ∨ p ∈ build_pairs xs
in_build_pairs : ∃ a, a ∈ xs ∧ (x, a) = p
y : α
t : y ∈ xs ∧ (x, y) = p
left : y ∈ xs
⊢ p.snd ∈ x :: xs

case right
α : Type u_1
l✝ : List α
pairs✝ : List (α × α)
h✝ : pairs✝ = build_pairs l✝
l : List α
pairs : List (α × α)
p : α × α
x : α
xs : List α
h : pairs = build_pairs.pairs x xs ++ build_pairs xs
in_pairs : p ∈ build_pairs.pairs x xs ∨ p ∈ build_pairs xs
⊢ p ∈ build_pairs xs → p.snd ∈ x :: xs
Tactic:
have right := t.right
Proof state after:
case left
α : Type u_1
l✝ : List α
pairs✝ : List (α × α)
h✝ : pairs✝ = build_pairs l✝
l : List α
pairs : List (α × α)
p : α × α
x : α
xs : List α
h : pairs = build_pairs.pairs x xs ++ build_pairs xs
in_pairs : p ∈ build_pairs.pairs x xs ∨ p ∈ build_pairs xs
in_build_pairs : ∃ a, a ∈ xs ∧ (x, a) = p
y : α
t : y ∈ xs ∧ (x, y) = p
left : y ∈ xs
right : (x, y) = p
⊢ p.snd ∈ x :: xs

case right
α : Type u_1
l✝ : List α
pairs✝ : List (α × α)
h✝ : pairs✝ = build_pairs l✝
l : List α
pairs : List (α × α)
p : α × α
x : α
xs : List α
h : pairs = build_pairs.pairs x xs ++ build_pairs xs
in_pairs : p ∈ build_pairs.pairs x xs ∨ p ∈ build_pairs xs
⊢ p ∈ build_pairs xs → p.snd ∈ x :: xs
Theorem: polynomial.pair_in_list₂
Proof state before:
case left
α : Type u_1
l✝ : List α
pairs✝ : List (α × α)
h✝ : pairs✝ = build_pairs l✝
l : List α
pairs : List (α × α)
p : α × α
x : α
xs : List α
h : pairs = build_pairs.pairs x xs ++ build_pairs xs
in_pairs : p ∈ build_pairs.pairs x xs ∨ p ∈ build_pairs xs
in_build_pairs : ∃ a, a ∈ xs ∧ (x, a) = p
y : α
t : y ∈ xs ∧ (x, y) = p
left : y ∈ xs
right : (x, y) = p
⊢ p.snd ∈ x :: xs

case right
α : Type u_1
l✝ : List α
pairs✝ : List (α × α)
h✝ : pairs✝ = build_pairs l✝
l : List α
pairs : List (α × α)
p : α × α
x : α
xs : List α
h : pairs = build_pairs.pairs x xs ++ build_pairs xs
in_pairs : p ∈ build_pairs.pairs x xs ∨ p ∈ build_pairs xs
⊢ p ∈ build_pairs xs → p.snd ∈ x :: xs
Tactic:
simp [Eq.symm right, left]
Proof state after:
case right
α : Type u_1
l✝ : List α
pairs✝ : List (α × α)
h✝ : pairs✝ = build_pairs l✝
l : List α
pairs : List (α × α)
p : α × α
x : α
xs : List α
h : pairs = build_pairs.pairs x xs ++ build_pairs xs
in_pairs : p ∈ build_pairs.pairs x xs ∨ p ∈ build_pairs xs
⊢ p ∈ build_pairs xs → p.snd ∈ x :: xs
Theorem: polynomial.pair_in_list₂
Proof state before:
case right
α : Type u_1
l✝ : List α
pairs✝ : List (α × α)
h✝ : pairs✝ = build_pairs l✝
l : List α
pairs : List (α × α)
p : α × α
x : α
xs : List α
h : pairs = build_pairs.pairs x xs ++ build_pairs xs
in_pairs : p ∈ build_pairs.pairs x xs ∨ p ∈ build_pairs xs
⊢ p ∈ build_pairs xs → p.snd ∈ x :: xs
Tactic:
intros in_build_pairs
Proof state after:
case right
α : Type u_1
l✝ : List α
pairs✝ : List (α × α)
h✝ : pairs✝ = build_pairs l✝
l : List α
pairs : List (α × α)
p : α × α
x : α
xs : List α
h : pairs = build_pairs.pairs x xs ++ build_pairs xs
in_pairs : p ∈ build_pairs.pairs x xs ∨ p ∈ build_pairs xs
in_build_pairs : p ∈ build_pairs xs
⊢ p.snd ∈ x :: xs
Theorem: polynomial.pair_in_list₂
Proof state before:
case right
α : Type u_1
l✝ : List α
pairs✝ : List (α × α)
h✝ : pairs✝ = build_pairs l✝
l : List α
pairs : List (α × α)
p : α × α
x : α
xs : List α
h : pairs = build_pairs.pairs x xs ++ build_pairs xs
in_pairs : p ∈ build_pairs.pairs x xs ∨ p ∈ build_pairs xs
in_build_pairs : p ∈ build_pairs xs
⊢ p.snd ∈ x :: xs
Tactic:
simp
Proof state after:
case right
α : Type u_1
l✝ : List α
pairs✝ : List (α × α)
h✝ : pairs✝ = build_pairs l✝
l : List α
pairs : List (α × α)
p : α × α
x : α
xs : List α
h : pairs = build_pairs.pairs x xs ++ build_pairs xs
in_pairs : p ∈ build_pairs.pairs x xs ∨ p ∈ build_pairs xs
in_build_pairs : p ∈ build_pairs xs
⊢ p.snd = x ∨ p.snd ∈ xs
Theorem: polynomial.pair_in_list₂
Proof state before:
case right
α : Type u_1
l✝ : List α
pairs✝ : List (α × α)
h✝ : pairs✝ = build_pairs l✝
l : List α
pairs : List (α × α)
p : α × α
x : α
xs : List α
h : pairs = build_pairs.pairs x xs ++ build_pairs xs
in_pairs : p ∈ build_pairs.pairs x xs ∨ p ∈ build_pairs xs
in_build_pairs : p ∈ build_pairs xs
⊢ p.snd = x ∨ p.snd ∈ xs
Tactic:
have res := aux xs (build_pairs xs) (by simp) p
Proof state after:
case right
α : Type u_1
l✝ : List α
pairs✝ : List (α × α)
h✝ : pairs✝ = build_pairs l✝
l : List α
pairs : List (α × α)
p : α × α
x : α
xs : List α
h : pairs = build_pairs.pairs x xs ++ build_pairs xs
in_pairs : p ∈ build_pairs.pairs x xs ∨ p ∈ build_pairs xs
in_build_pairs : p ∈ build_pairs xs
res : p ∈ build_pairs xs → p.snd ∈ xs
⊢ p.snd = x ∨ p.snd ∈ xs
Theorem: polynomial.pair_in_list₂
Proof state before:
case right
α : Type u_1
l✝ : List α
pairs✝ : List (α × α)
h✝ : pairs✝ = build_pairs l✝
l : List α
pairs : List (α × α)
p : α × α
x : α
xs : List α
h : pairs = build_pairs.pairs x xs ++ build_pairs xs
in_pairs : p ∈ build_pairs.pairs x xs ∨ p ∈ build_pairs xs
in_build_pairs : p ∈ build_pairs xs
res : p ∈ build_pairs xs → p.snd ∈ xs
⊢ p.snd = x ∨ p.snd ∈ xs
Tactic:
simp [res in_build_pairs]
Proof state after:
no goals
Theorem: polynomial.pair_in_list₂
Proof state before:
α : Type u_1
l✝ : List α
pairs✝ : List (α × α)
h✝ : pairs✝ = build_pairs l✝
l : List α
pairs : List (α × α)
p : α × α
x : α
xs : List α
h : pairs = build_pairs.pairs x xs ++ build_pairs xs
in_pairs : p ∈ build_pairs.pairs x xs ∨ p ∈ build_pairs xs
in_build_pairs : p ∈ build_pairs xs
⊢ build_pairs xs = build_pairs xs
Tactic:
simp
Proof state after:
no goals
Theorem: polynomial.pair_in_list
Proof state before:
α : Type u_1
l : List α
pairs : List (α × α)
h : pairs = build_pairs l
⊢ ∀ (p : α × α), p ∈ pairs → p.fst ∈ l ∧ p.snd ∈ l
Tactic:
intros p in_pairs
Proof state after:
α : Type u_1
l : List α
pairs : List (α × α)
h : pairs = build_pairs l
p : α × α
in_pairs : p ∈ pairs
⊢ p.fst ∈ l ∧ p.snd ∈ l
Theorem: polynomial.pair_in_list
Proof state before:
α : Type u_1
l : List α
pairs : List (α × α)
h : pairs = build_pairs l
p : α × α
in_pairs : p ∈ pairs
⊢ p.fst ∈ l ∧ p.snd ∈ l
Tactic:
constructor
Proof state after:
case left
α : Type u_1
l : List α
pairs : List (α × α)
h : pairs = build_pairs l
p : α × α
in_pairs : p ∈ pairs
⊢ p.fst ∈ l

case right
α : Type u_1
l : List α
pairs : List (α × α)
h : pairs = build_pairs l
p : α × α
in_pairs : p ∈ pairs
⊢ p.snd ∈ l
Theorem: polynomial.pair_in_list
Proof state before:
case left
α : Type u_1
l : List α
pairs : List (α × α)
h : pairs = build_pairs l
p : α × α
in_pairs : p ∈ pairs
⊢ p.fst ∈ l

case right
α : Type u_1
l : List α
pairs : List (α × α)
h : pairs = build_pairs l
p : α × α
in_pairs : p ∈ pairs
⊢ p.snd ∈ l
Tactic:
exact pair_in_list₁ l pairs h p in_pairs
Proof state after:
case right
α : Type u_1
l : List α
pairs : List (α × α)
h : pairs = build_pairs l
p : α × α
in_pairs : p ∈ pairs
⊢ p.snd ∈ l
Theorem: polynomial.pair_in_list
Proof state before:
case right
α : Type u_1
l : List α
pairs : List (α × α)
h : pairs = build_pairs l
p : α × α
in_pairs : p ∈ pairs
⊢ p.snd ∈ l
Tactic:
exact pair_in_list₂ l pairs h p in_pairs
Proof state after:
no goals
Theorem: polynomial.cons_non_empty
Proof state before:
α : Type u_1
inst✝ : BEq α
a b : List α
h : ¬(b == []) = true
⊢ ¬(a ++ b == []) = true
Tactic:
simp at *
Proof state after:
α : Type u_1
inst✝ : BEq α
a b : List α
h : (b == []) = false
⊢ (a ++ b == []) = false
Theorem: polynomial.cons_non_empty
Proof state before:
α : Type u_1
inst✝ : BEq α
a b : List α
h : (b == []) = false
⊢ (a ++ b == []) = false
Tactic:
cases a
Proof state after:
case nil
α : Type u_1
inst✝ : BEq α
b : List α
h : (b == []) = false
⊢ ([] ++ b == []) = false

case cons
α : Type u_1
inst✝ : BEq α
b : List α
h : (b == []) = false
head✝ : α
tail✝ : List α
⊢ (head✝ :: tail✝ ++ b == []) = false
Theorem: polynomial.cons_non_empty
Proof state before:
case nil
α : Type u_1
inst✝ : BEq α
b : List α
h : (b == []) = false
⊢ ([] ++ b == []) = false

case cons
α : Type u_1
inst✝ : BEq α
b : List α
h : (b == []) = false
head✝ : α
tail✝ : List α
⊢ (head✝ :: tail✝ ++ b == []) = false
Tactic:
simp [h]
Proof state after:
case cons
α : Type u_1
inst✝ : BEq α
b : List α
h : (b == []) = false
head✝ : α
tail✝ : List α
⊢ (head✝ :: tail✝ ++ b == []) = false
Theorem: polynomial.cons_non_empty
Proof state before:
case cons
α : Type u_1
inst✝ : BEq α
b : List α
h : (b == []) = false
head✝ : α
tail✝ : List α
⊢ (head✝ :: tail✝ ++ b == []) = false
Tactic:
rfl
Proof state after:
no goals
Theorem: polynomial.list_empty
Proof state before:
α : Type u_1
inst✝ : BEq α
⊢ ∀ (l : List α), (l == []) = true → l = []
Tactic:
intros l h
Proof state after:
α : Type u_1
inst✝ : BEq α
l : List α
h : (l == []) = true
⊢ l = []
Theorem: polynomial.list_empty
Proof state before:
α : Type u_1
inst✝ : BEq α
l : List α
h : (l == []) = true
⊢ l = []
Tactic:
cases l
Proof state after:
case nil
α : Type u_1
inst✝ : BEq α
h : ([] == []) = true
⊢ [] = []

case cons
α : Type u_1
inst✝ : BEq α
head✝ : α
tail✝ : List α
h : (head✝ :: tail✝ == []) = true
⊢ head✝ :: tail✝ = []
Theorem: polynomial.list_empty
Proof state before:
case nil
α : Type u_1
inst✝ : BEq α
h : ([] == []) = true
⊢ [] = []

case cons
α : Type u_1
inst✝ : BEq α
head✝ : α
tail✝ : List α
h : (head✝ :: tail✝ == []) = true
⊢ head✝ :: tail✝ = []
Tactic:
simp
Proof state after:
case cons
α : Type u_1
inst✝ : BEq α
head✝ : α
tail✝ : List α
h : (head✝ :: tail✝ == []) = true
⊢ head✝ :: tail✝ = []
Theorem: polynomial.list_empty
Proof state before:
case cons
α : Type u_1
inst✝ : BEq α
head✝ : α
tail✝ : List α
h : (head✝ :: tail✝ == []) = true
⊢ head✝ :: tail✝ = []
Tactic:
contradiction
Proof state after:
no goals
Theorem: polynomial.sufficiency_poly_in_ideal
Proof 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
Proof 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
Theorem: polynomial.sufficiency_poly_in_ideal
Proof 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
Proof 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
Theorem: polynomial.sufficiency_poly_in_ideal
Proof 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
Proof 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
Theorem: polynomial.sufficiency_poly_in_ideal
Proof 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 *
Proof 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
Theorem: polynomial.sufficiency_poly_in_ideal
Proof 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
Proof 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
Theorem: polynomial.sufficiency_poly_in_ideal
Proof 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]
Proof 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
Theorem: polynomial.sufficiency_poly_in_ideal
Proof 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
Proof state after:
no goals
Theorem: t_add_zero
Proof state before:
n : ℕ
ord : Type
inst✝ : MonomialOrder (Variables n ord)
⊢ ∀ (a : Polynomial n ord), a + 0 = a
Tactic:
intros p
Proof state after:
n : ℕ
ord : Type
inst✝ : MonomialOrder (Variables n ord)
p : Polynomial n ord
⊢ p + 0 = p
Theorem: t_add_zero
Proof state before:
n : ℕ
ord : Type
inst✝ : MonomialOrder (Variables n ord)
p : Polynomial n ord
⊢ p + 0 = p
Tactic:
simp [t_add_comm p, t_zero_add]
Proof state after:
no goals
Theorem: t_mul_zero
Proof state before:
n : ℕ
ord : Type
inst✝ : MonomialOrder (Variables n ord)
⊢ ∀ (a : Polynomial n ord), a * 0 = 0
Tactic:
intros p
Proof state after:
n : ℕ
ord : Type
inst✝ : MonomialOrder (Variables n ord)
p : Polynomial n ord
⊢ p * 0 = 0
Theorem: t_mul_zero
Proof state before:
n : ℕ
ord : Type
inst✝ : MonomialOrder (Variables n ord)
p : Polynomial n ord
⊢ p * 0 = 0
Tactic:
simp [t_mul_comm p, t_zero_mul]
Proof state after:
no goals
Theorem: t_right_distrib
Proof state before:
n : ℕ
ord : Type
inst✝ : MonomialOrder (Variables n ord)
⊢ ∀ (a b c : Polynomial n ord), (a + b) * c = a * c + b * c
Tactic:
intros a b c
Proof state after:
n : ℕ
ord : Type
inst✝ : MonomialOrder (Variables n ord)
a b c : Polynomial n ord
⊢ (a + b) * c = a * c + b * c
Theorem: t_right_distrib
Proof state before:
n : ℕ
ord : Type
inst✝ : MonomialOrder (Variables n ord)
a b c : Polynomial n ord
⊢ (a + b) * c = a * c + b * c
Tactic:
have rl_mul := t_mul_comm (a + b) c
Proof state after:
n : ℕ
ord : Type
inst✝ : MonomialOrder (Variables n ord)
a b c : Polynomial n ord
rl_mul : (a + b) * c = c * (a + b)
⊢ (a + b) * c = a * c + b * c
Theorem: t_right_distrib
Proof state before:
n : ℕ
ord : Type
inst✝ : MonomialOrder (Variables n ord)
a b c : Polynomial n ord
rl_mul : (a + b) * c = c * (a + b)
⊢ (a + b) * c = a * c + b * c
Tactic:
simp [rl_mul, t_left_distrib, t_mul_comm]
Proof state after:
no goals
Theorem: t_mul_one
Proof state before:
n : ℕ
ord : Type
inst✝ : MonomialOrder (Variables n ord)
⊢ ∀ (a : Polynomial n ord), a * 1 = a
Tactic:
intros p
Proof state after:
n : ℕ
ord : Type
inst✝ : MonomialOrder (Variables n ord)
p : Polynomial n ord
⊢ p * 1 = p
Theorem: t_mul_one
Proof state before:
n : ℕ
ord : Type
inst✝ : MonomialOrder (Variables n ord)
p : Polynomial n ord
⊢ p * 1 = p
Tactic:
simp [t_mul_comm p, t_one_mul]
Proof state after:
no goals
Theorem: IdealHelpers.listInSet
Proof state before:
α : Type u_1
l : List α
⊢ ∀ (x : α), x ∈ l → x ∈ asSet l
Tactic:
intros y h
Proof state after:
α : Type u_1
l : List α
y : α
h : y ∈ l
⊢ y ∈ asSet l
Theorem: IdealHelpers.listInSet
Proof state before:
α : Type u_1
l : List α
y : α
h : y ∈ l
⊢ y ∈ asSet l
Tactic:
simp [asSet]
Proof state after:
α : Type u_1
l : List α
y : α
h : y ∈ l
⊢ y ∈ l
Theorem: IdealHelpers.listInSet
Proof state before:
α : Type u_1
l : List α
y : α
h : y ∈ l
⊢ y ∈ l
Tactic:
exact h
Proof state after:
no goals
Theorem: IdealHelpers.list_union_as_set
Proof state before:
α : Type u_1
l₁ l₂ : List α
⊢ asSet (l₁ ++ l₂) = asSet l₁ ∪ asSet l₂
Tactic:
induction l₂
Proof state after:
case nil
α : Type u_1
l₁ : List α
⊢ asSet (l₁ ++ []) = asSet l₁ ∪ asSet []

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✝)
Theorem: IdealHelpers.list_union_as_set
Proof state before:
case nil
α : Type u_1
l₁ : List α
⊢ asSet (l₁ ++ []) = asSet l₁ ∪ asSet []

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✝
⊢ asSet (l₁ ++ head✝ :: tail✝) = asSet l₁ ∪ asSet (head✝ :: tail✝)