awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
S : Type u_1
inst : Semiring R
inst_1 : Nontrivial R
p : R[X]
hp : p.Monic
a : HPow.hPow (α := R[X]) X p.natDegree + p.eraseLead = p
⊢ (↑((fun (p_1 : ↥(degreeLT R p.natDegree)) ↦
            (Subtype.mk (p := fun (p_2 : R[X]) ↦ p_2.Monic ∧ p_2.natDegree = p.natDegree)
                (HPow.hPow (α := R[X]) X p.natDegree + (↑p_1 : R[X])) ⋯ :
              { p_2 : R[X] // p_2.Monic ∧ p_2.natDegree = p.natDegree }))
          ((fun (p_1 : { p_1 : R[X] // p_1.Monic ∧ p_1.natDegree = p.natDegree }) ↦
              Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submodule R R[X]) (degreeLT R p.natDegree) x)
                (↑p_1 : R[X]).eraseLead ⋯)
            (Subtype.mk (p := fun (p_1 : R[X]) ↦ p_1.Monic ∧ p_1.natDegree = p.natDegree) p ⋯))) :
      R[X]) =
    (↑(Subtype.mk (p := fun (p_1 : R[X]) ↦ p_1.Monic ∧ p_1.natDegree = p.natDegree) p ⋯) : R[X])

Tactic:
simp only
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
S : Type u_1
inst : Semiring R
inst_1 : Nontrivial R
p : R[X]
hp : p.Monic
rw :
  p.eraseLead + HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X p.natDegree)
| p

Tactic:
rw [← eraseLead_add_C_mul_X_pow p]

Premises used: Polynomial.eraseLead_add_C_mul_X_pow
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
S : Type u_1
inst : Semiring R
inst_1 : Nontrivial R
p : R[X]
hp : p.Monic
a :
  HPow.hPow (α := R[X]) X p.natDegree + p.eraseLead =
    p.eraseLead +
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X p.natDegree)
⊢ HPow.hPow (α := R[X]) X p.natDegree + p.eraseLead = p

Tactic:
conv_rhs => rw [← eraseLead_add_C_mul_X_pow p]

Premises used: Polynomial.eraseLead_add_C_mul_X_pow
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
S : Type u_1
inst : Semiring R
inst_1 : Nontrivial R
p : R[X]
hp : p.Monic
⊢ HPow.hPow (α := R[X]) X p.natDegree + p.eraseLead =
    p.eraseLead +
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X p.natDegree)

Tactic:
simp [Monic.def.1 hp, add_comm]

Premises used: add_comm, Iff.mp, Polynomial.Monic.def
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
S : Type u_1
inst : Semiring R
inst_1 : Nontrivial R
n : ℕ
p : R[X]
hp : Membership.mem (γ := Submodule R R[X]) (degreeLT R n) p
a :
  (↑((fun (p : { p : R[X] // p.Monic ∧ p.natDegree = n }) ↦
            Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submodule R R[X]) (degreeLT R n) x)
              (↑p : R[X]).eraseLead ⋯)
          ((fun (p : ↥(degreeLT R n)) ↦
              (Subtype.mk (p := fun (p : R[X]) ↦ p.Monic ∧ p.natDegree = n) (HPow.hPow (α := R[X]) X n + (↑p : R[X]))
                  ⋯ :
                { p : R[X] // p.Monic ∧ p.natDegree = n }))
            (Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submodule R R[X]) (degreeLT R n) x) p hp))) :
      R[X]) =
    (↑(Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submodule R R[X]) (degreeLT R n) x) p hp) : R[X])
⊢ (fun (p : { p : R[X] // p.Monic ∧ p.natDegree = n }) ↦
        Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submodule R R[X]) (degreeLT R n) x) (↑p : R[X]).eraseLead
          ⋯)
      ((fun (p : ↥(degreeLT R n)) ↦
          (Subtype.mk (p := fun (p : R[X]) ↦ p.Monic ∧ p.natDegree = n) (HPow.hPow (α := R[X]) X n + (↑p : R[X])) ⋯ :
            { p : R[X] // p.Monic ∧ p.natDegree = n }))
        (Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submodule R R[X]) (degreeLT R n) x) p hp)) =
    Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submodule R R[X]) (degreeLT R n) x) p hp

Tactic:
ext1
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
S : Type u_1
inst : Semiring R
inst_1 : Nontrivial R
n : ℕ
p : R[X]
hp : Membership.mem (γ := Submodule R R[X]) (degreeLT R n) p
a : (HPow.hPow (α := R[X]) X n + p).eraseLead = p
⊢ (↑((fun (p : { p : R[X] // p.Monic ∧ p.natDegree = n }) ↦
            Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submodule R R[X]) (degreeLT R n) x)
              (↑p : R[X]).eraseLead ⋯)
          ((fun (p : ↥(degreeLT R n)) ↦
              (Subtype.mk (p := fun (p : R[X]) ↦ p.Monic ∧ p.natDegree = n) (HPow.hPow (α := R[X]) X n + (↑p : R[X]))
                  ⋯ :
                { p : R[X] // p.Monic ∧ p.natDegree = n }))
            (Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submodule R R[X]) (degreeLT R n) x) p hp))) :
      R[X]) =
    (↑(Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submodule R R[X]) (degreeLT R n) x) p hp) : R[X])

Tactic:
simp only
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
S : Type u_1
inst : Semiring R
inst_1 : Nontrivial R
n : ℕ
p : R[X]
hp : Membership.mem (γ := Submodule R R[X]) (degreeLT R n) p
a : (HPow.hPow (α := R[X]) X n).eraseLead + p = p
a₁ : p.degree < (HPow.hPow (α := R[X]) X n).degree
⊢ (HPow.hPow (α := R[X]) X n + p).eraseLead = p

Tactic:
rw [eraseLead_add_of_degree_lt_left]

Premises used: Polynomial.eraseLead_add_of_degree_lt_left
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
S : Type u_1
inst : Semiring R
inst_1 : Nontrivial R
n : ℕ
p : R[X]
hp : Membership.mem (γ := Submodule R R[X]) (degreeLT R n) p
⊢ (HPow.hPow (α := R[X]) X n).eraseLead + p = p

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
S : Type u_1
inst : Semiring R
inst_1 : Nontrivial R
n : ℕ
p : R[X]
hp : Membership.mem (γ := Submodule R R[X]) (degreeLT R n) p
⊢ p.degree < (HPow.hPow (α := R[X]) X n).degree

Tactic:
simp [mem_degreeLT.1 hp]

Premises used: Iff.mp, Polynomial.mem_degreeLT
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
s : Set R[X]
p : R[X]
hs : s.Nonempty
hp : Membership.mem (γ := Submodule R R[X]) (Submodule.span R s) p
by_contra! : ∀ (h : ∀ (p' : R[X]) (_ : p' ∈ s), p'.degree < p.degree), False
⊢ ∃ p' ∈ s, p.degree ≤ p'.degree

Tactic:
by_contra! h
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
s : Set R[X]
p : R[X]
hs : s.Nonempty
hp : Membership.mem (γ := Submodule R R[X]) (Submodule.span R s) p
h : ∀ (p' : R[X]) (_ : p' ∈ s), p'.degree < p.degree
pos : ∀ (hp_zero : p = 0), False
neg : ∀ (hp_zero : ¬p = 0), False
⊢ False

Tactic:
by_cases hp_zero : p = 0
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
s : Set R[X]
p : R[X]
hs : s.Nonempty
hp : Membership.mem (γ := Submodule R R[X]) (Submodule.span R s) p
h : ∀ (p' : R[X]) (_ : p' ∈ s), p'.degree < p.degree
hp_zero : p = 0
⊢ ∀ (p' : R[X]) (_ : p' ∈ s), p'.degree < ⊥

Tactic:
rw [hp_zero, degree_zero] at h

Premises used: Polynomial.degree_zero
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
s : Set R[X]
p : R[X]
hs : s.Nonempty
hp : Membership.mem (γ := Submodule R R[X]) (Submodule.span R s) p
h : ∀ (p' : R[X]) (_ : p' ∈ s), p'.degree < p.degree
hp_zero : p = 0
h₁ : ∀ (p' : R[X]) (_ : p' ∈ s), p'.degree < ⊥
⊢ p = 0

Tactic:
rw [hp_zero, degree_zero] at h

Premises used: Polynomial.degree_zero
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
s : Set R[X]
p : R[X]
hs : s.Nonempty
hp : Membership.mem (γ := Submodule R R[X]) (Submodule.span R s) p
h : ∀ (p' : R[X]) (_ : p' ∈ s), p'.degree < ⊥
hp_zero : p = 0
pos : ∀ (x : R[X]) (hx : x ∈ s), False
⊢ False

Tactic:
rcases hs with ⟨x, hx⟩
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
s : Set R[X]
p : R[X]
hp : Membership.mem (γ := Submodule R R[X]) (Submodule.span R s) p
h : ∀ (p' : R[X]) (_ : p' ∈ s), p'.degree < ⊥
hp_zero : p = 0
x : R[X]
hx : x ∈ s
⊢ False

Tactic:
not_lt_bot (h x hx)

Premises used: not_lt_bot
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
s : Set R[X]
p : R[X]
hp : Membership.mem (γ := Submodule R R[X]) (Submodule.span R s) p
h : ∀ (p' : R[X]) (_ : p' ∈ s), p'.degree < ⊥
hp_zero : p = 0
x : R[X]
hx : x ∈ s
⊢ False

Tactic:
exact not_lt_bot (h x hx)

Premises used: not_lt_bot
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
s : Set R[X]
p : R[X]
hs : s.Nonempty
hp : Membership.mem (γ := Submodule R R[X]) (Submodule.span R s) p
h : ∀ (p' : R[X]) (_ : p' ∈ s), p'.degree < p.degree
hp_zero : ¬p = 0
⊢ Membership.mem (γ := Submodule R R[X]) (degreeLT R p.natDegree) p

Tactic:
(Submodule.span_le.mpr fun p' p'_mem => ?_) hp

Premises used: Iff.mpr, Submodule.span_le
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
s : Set R[X]
p : R[X]
hs : s.Nonempty
hp : Membership.mem (γ := Submodule R R[X]) (Submodule.span R s) p
h : ∀ (p' : R[X]) (_ : p' ∈ s), p'.degree < p.degree
hp_zero : ¬p = 0
refine : ∀ (p' : R[X]) (p'_mem : p' ∈ s), p' ∈ (↑(degreeLT R p.natDegree) : Set R[X])
⊢ Membership.mem (γ := Submodule R R[X]) (degreeLT R p.natDegree) p

Tactic:
refine (Submodule.span_le.mpr fun p' p'_mem => ?_) hp

Premises used: Iff.mpr, Submodule.span_le
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
s : Set R[X]
p : R[X]
hs : s.Nonempty
hp : Membership.mem (γ := Submodule R R[X]) (Submodule.span R s) p
h : ∀ (p' : R[X]) (_ : p' ∈ s), p'.degree < p.degree
hp_zero : ¬p = 0
p' : R[X]
p'_mem : p' ∈ s
rw : p'.degree < (↑p.natDegree : WithBot ℕ)
⊢ p' ∈ (↑(degreeLT R p.natDegree) : Set R[X])

Tactic:
rw [SetLike.mem_coe, mem_degreeLT, Nat.cast_withBot]

Premises used: SetLike.mem_coe, Nat.cast_withBot, Polynomial.mem_degreeLT
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
s : Set R[X]
p : R[X]
hs : s.Nonempty
hp : Membership.mem (γ := Submodule R R[X]) (Submodule.span R s) p
h : ∀ (p' : R[X]) (_ : p' ∈ s), p'.degree < p.degree
hp_zero : ¬p = 0
p' : R[X]
p'_mem : p' ∈ s
⊢ p'.degree < (↑p.natDegree : WithBot ℕ)

Tactic:
lt_of_lt_of_le (h p' p'_mem) degree_le_natDegree

Premises used: Polynomial.degree_le_natDegree, lt_of_lt_of_le
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
s : Set R[X]
p : R[X]
hs : s.Nonempty
hp : Membership.mem (γ := Submodule R R[X]) (Submodule.span R s) p
h : ∀ (p' : R[X]) (_ : p' ∈ s), p'.degree < p.degree
hp_zero : ¬p = 0
p' : R[X]
p'_mem : p' ∈ s
⊢ p'.degree < (↑p.natDegree : WithBot ℕ)

Tactic:
exact lt_of_lt_of_le (h p' p'_mem) degree_le_natDegree

Premises used: Polynomial.degree_le_natDegree, lt_of_lt_of_le
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
s : Set R[X]
p : R[X]
hs : s.Nonempty
hp : Membership.mem (γ := Submodule R R[X]) (Submodule.span R s) p
h : ∀ (p' : R[X]) (_ : p' ∈ s), p'.degree < p.degree
hp_zero : ¬p = 0
⊢ Membership.mem (γ := Submodule R R[X]) (degreeLT R p.natDegree) p

Tactic:
have : p ∈ degreeLT R (natDegree p) := by
      refine (Submodule.span_le.mpr fun p' p'_mem => ?_) hp
      rw [SetLike.mem_coe, mem_degreeLT, Nat.cast_withBot]
      exact lt_of_lt_of_le (h p' p'_mem) degree_le_natDegree
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
s : Set R[X]
p : R[X]
hs : s.Nonempty
hp : Membership.mem (γ := Submodule R R[X]) (Submodule.span R s) p
h : ∀ (p' : R[X]) (_ : p' ∈ s), p'.degree < p.degree
hp_zero : ¬p = 0
this : Membership.mem (γ := Submodule R R[X]) (degreeLT R p.natDegree) p
neg : ∀ (this : p.degree < (↑p.natDegree : WithBot ℕ)), False
neg₁ : ∀ (this : p.degree < (↑p.natDegree : WithBot ℕ)), False
neg₂ : ∀ (this : (↑p.natDegree : WithBot ℕ) < (↑p.natDegree : WithBot ℕ)), False
neg₃ : ∀ (this : (↑p.natDegree : WithBot ℕ) < (↑p.natDegree : WithBot ℕ)), False
neg₄ neg₅ neg₆ neg₇ : ∀ (this : False), False
⊢ False

Tactic:
rwa [mem_degreeLT, Nat.cast_withBot, degree_eq_natDegree hp_zero,
      Nat.cast_withBot, lt_self_iff_false] at this

Premises used: Polynomial.degree_eq_natDegree, lt_self_iff_false, Nat.cast_withBot, Polynomial.mem_degreeLT
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
s : Set R[X]
s_fin : s.Finite
hs : s.Nonempty
obtain :
  ∀ (a : R[X]) (has : a ∈ s)
    (hmax : ∀ ⦃j : R[X]⦄, (fun (x : R[X]) ↦ x ∈ s) j → a.degree ≤ j.degree → j.degree ≤ a.degree),
    ∃ p' ∈ s, ∀ (p : R[X]), Membership.mem (γ := Submodule R R[X]) (Submodule.span R s) p → p.degree ≤ p'.degree
⊢ ∃ p' ∈ s, ∀ (p : R[X]), Membership.mem (γ := Submodule R R[X]) (Submodule.span R s) p → p.degree ≤ p'.degree

Tactic:
obtain ⟨a, has, hmax⟩ := s_fin.exists_maximalFor degree s hs

Premises used: Set.Finite.exists_maximalFor, Polynomial.degree
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
s : Set R[X]
s_fin : s.Finite
hs : s.Nonempty
a : R[X]
has : a ∈ s
hmax : ∀ ⦃j : R[X]⦄, (fun (x : R[X]) ↦ x ∈ s) j → a.degree ≤ j.degree → j.degree ≤ a.degree
⊢ ∃ p' ∈ s, ∀ (p : R[X]), Membership.mem (γ := Submodule R R[X]) (Submodule.span R s) p → p.degree ≤ p'.degree

Tactic:
⟨a, has, fun p hp => ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
s : Set R[X]
s_fin : s.Finite
hs : s.Nonempty
a : R[X]
has : a ∈ s
hmax : ∀ ⦃j : R[X]⦄, (fun (x : R[X]) ↦ x ∈ s) j → a.degree ≤ j.degree → j.degree ≤ a.degree
refine : ∀ (p : R[X]) (hp : Membership.mem (γ := Submodule R R[X]) (Submodule.span R s) p), p.degree ≤ a.degree
⊢ ∃ p' ∈ s, ∀ (p : R[X]), Membership.mem (γ := Submodule R R[X]) (Submodule.span R s) p → p.degree ≤ p'.degree

Tactic:
refine ⟨a, has, fun p hp => ?_⟩
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
s : Set R[X]
s_fin : s.Finite
hs : s.Nonempty
a : R[X]
has : a ∈ s
hmax : ∀ ⦃j : R[X]⦄, (fun (x : R[X]) ↦ x ∈ s) j → a.degree ≤ j.degree → j.degree ≤ a.degree
p : R[X]
hp : Membership.mem (γ := Submodule R R[X]) (Submodule.span R s) p
obtain : ∀ (p' : R[X]) (hp' : p' ∈ s) (hpp' : p.degree ≤ p'.degree), p.degree ≤ a.degree
⊢ p.degree ≤ a.degree

Tactic:
obtain ⟨p', hp', hpp'⟩ := exists_degree_le_of_mem_span hs hp

Premises used: Polynomial.exists_degree_le_of_mem_span
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
s : Set R[X]
s_fin : s.Finite
hs : s.Nonempty
a : R[X]
has : a ∈ s
hmax : ∀ ⦃j : R[X]⦄, (fun (x : R[X]) ↦ x ∈ s) j → a.degree ≤ j.degree → j.degree ≤ a.degree
p : R[X]
hp : Membership.mem (γ := Submodule R R[X]) (Submodule.span R s) p
p' : R[X]
hp' : p' ∈ s
hpp' : p.degree ≤ p'.degree
⊢ p.degree ≤ a.degree

Tactic:
hpp'.trans <| not_lt.1 <| not_lt_iff_le_imp_ge.2 <| hmax hp'

Premises used: Iff.mpr, not_lt, Iff.mp, LE.le.trans, not_lt_iff_le_imp_ge
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
s : Set R[X]
s_fin : s.Finite
hs : s.Nonempty
a : R[X]
has : a ∈ s
hmax : ∀ ⦃j : R[X]⦄, (fun (x : R[X]) ↦ x ∈ s) j → a.degree ≤ j.degree → j.degree ≤ a.degree
p : R[X]
hp : Membership.mem (γ := Submodule R R[X]) (Submodule.span R s) p
p' : R[X]
hp' : p' ∈ s
hpp' : p.degree ≤ p'.degree
⊢ p.degree ≤ a.degree

Tactic:
exact hpp'.trans <| not_lt.1 <| not_lt_iff_le_imp_ge.2 <| hmax hp'

Premises used: Iff.mpr, not_lt, Iff.mp, LE.le.trans, not_lt_iff_le_imp_ge
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
s : Set R[X]
s_fin : s.Finite
pos : ∀ (s_emp : s.Nonempty), ∃ (n : ℕ), Submodule.span R s ≤ degreeLE R (↑n : WithBot ℕ)
neg : ∀ (s_emp : ¬s.Nonempty), ∃ (n : ℕ), Submodule.span R s ≤ degreeLE R (↑n : WithBot ℕ)
⊢ ∃ (n : ℕ), Submodule.span R s ≤ degreeLE R (↑n : WithBot ℕ)

Tactic:
by_cases s_emp : s.Nonempty

Premises used: Set.Nonempty
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
s : Set R[X]
s_fin : s.Finite
s_emp : s.Nonempty
pos :
  ∀ p' ∈ s,
    ∀ (hp'max : ∀ (p : R[X]), Membership.mem (γ := Submodule R R[X]) (Submodule.span R s) p → p.degree ≤ p'.degree),
      ∃ (n : ℕ), Submodule.span R s ≤ degreeLE R (↑n : WithBot ℕ)
⊢ ∃ (n : ℕ), Submodule.span R s ≤ degreeLE R (↑n : WithBot ℕ)

Tactic:
rcases exists_degree_le_of_mem_span_of_finite s_fin s_emp with ⟨p', _, hp'max⟩

Premises used: Polynomial.exists_degree_le_of_mem_span_of_finite
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
s : Set R[X]
s_fin : s.Finite
s_emp : s.Nonempty
p' : R[X]
left : p' ∈ s
hp'max : ∀ (p : R[X]), Membership.mem (γ := Submodule R R[X]) (Submodule.span R s) p → p.degree ≤ p'.degree
⊢ ∃ (n : ℕ), Submodule.span R s ≤ degreeLE R (↑n : WithBot ℕ)

Tactic:
⟨natDegree p', fun p hp => mem_degreeLE.mpr ((hp'max _ hp).trans degree_le_natDegree)⟩

Premises used: Iff.mpr, Polynomial.degree_le_natDegree, Exists.intro, LE.le.trans, Polynomial.natDegree, Polynomial.mem_degreeLE
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
s : Set R[X]
s_fin : s.Finite
s_emp : s.Nonempty
p' : R[X]
left : p' ∈ s
hp'max : ∀ (p : R[X]), Membership.mem (γ := Submodule R R[X]) (Submodule.span R s) p → p.degree ≤ p'.degree
⊢ ∃ (n : ℕ), Submodule.span R s ≤ degreeLE R (↑n : WithBot ℕ)

Tactic:
exact ⟨natDegree p', fun p hp => mem_degreeLE.mpr ((hp'max _ hp).trans degree_le_natDegree)⟩
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
s : Set R[X]
s_fin : s.Finite
s_emp : ¬s.Nonempty
⊢ s = ∅

Tactic:
rw [Set.not_nonempty_iff_eq_empty] at s_emp

Premises used: Set.not_nonempty_iff_eq_empty
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
s : Set R[X]
s_fin : s.Finite
s_emp : s = ∅
neg : ∃ (n : ℕ), LE.le (α := Submodule R R[X]) ⊥ (degreeLE R (↑n : WithBot ℕ))
⊢ ∃ (n : ℕ), Submodule.span R s ≤ degreeLE R (↑n : WithBot ℕ)

Tactic:
rw [s_emp, Submodule.span_empty]

Premises used: Submodule.span_empty
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
s : Set R[X]
s_fin : s.Finite
s_emp : s = ∅
⊢ ∃ (n : ℕ), LE.le (α := Submodule R R[X]) ⊥ (degreeLE R (↑n : WithBot ℕ))

Tactic:
⟨0, bot_le⟩

Premises used: Exists.intro, OfNat.ofNat, bot_le
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
s : Set R[X]
s_fin : s.Finite
s_emp : s = ∅
⊢ ∃ (n : ℕ), LE.le (α := Submodule R R[X]) ⊥ (degreeLE R (↑n : WithBot ℕ))

Tactic:
exact ⟨0, bot_le⟩
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
s : Set R[X]
s_fin : s.Finite
rcases : ∀ (n : ℕ), Submodule.span R s ≤ degreeLE R (↑n : WithBot ℕ) → ∃ (n : ℕ), Submodule.span R s ≤ degreeLT R n
⊢ ∃ (n : ℕ), Submodule.span R s ≤ degreeLT R n

Tactic:
rcases span_le_degreeLE_of_finite s_fin with ⟨n, _⟩

Premises used: Polynomial.span_le_degreeLE_of_finite
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
s : Set R[X]
s_fin : s.Finite
n : ℕ
h rwa rwa₁ rwa₂ rwa₃ : Submodule.span R s ≤ degreeLE R (↑n : WithBot ℕ)
⊢ Submodule.span R s ≤ degreeLT R (n + 1)

Tactic:
rwa [degreeLT_succ_eq_degreeLE]

Premises used: Polynomial.degreeLT_succ_eq_degreeLE
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
s : Set R[X]
s_fin : s.Finite
n : ℕ
h : Submodule.span R s ≤ degreeLE R (↑n : WithBot ℕ)
⊢ ∃ (n : ℕ), Submodule.span R s ≤ degreeLT R n

Tactic:
exact ⟨n + 1, by rwa [degreeLT_succ_eq_degreeLE]⟩
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : Nontrivial R
rw : ¬∃ (S : Set R[X]), S.Finite ∧ Eq (α := Submodule R R[X]) (Submodule.span R S) ⊤
⊢ ¬Module.Finite R R[X]

Tactic:
rw [Module.finite_def, Submodule.fg_def]

Premises used: Submodule.fg_def, Module.finite_def
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : Nontrivial R
push : ∀ (S : Set R[X]) (_ : S.Finite), Ne (α := Submodule R R[X]) (Submodule.span R S) ⊤
⊢ ¬∃ (S : Set R[X]), S.Finite ∧ Eq (α := Submodule R R[X]) (Submodule.span R S) ⊤

Tactic:
push Not

Premises used: Not
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : Nontrivial R
s : Set R[X]
hs : s.Finite
contra : Eq (α := Submodule R R[X]) (Submodule.span R s) ⊤
rcases : ∀ (n : ℕ) (hn : Submodule.span R s ≤ degreeLE R (↑n : WithBot ℕ)), False
⊢ False

Tactic:
rcases span_le_degreeLE_of_finite hs with ⟨n, hn⟩

Premises used: Polynomial.span_le_degreeLE_of_finite
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : Nontrivial R
s : Set R[X]
hs : s.Finite
contra : Eq (α := Submodule R R[X]) (Submodule.span R s) ⊤
n : ℕ
hn : Submodule.span R s ≤ degreeLE R (↑n : WithBot ℕ)
⊢ LE.le (α := Submodule R R[X]) ⊤ (degreeLE R (↑n : WithBot ℕ))

Tactic:
rw [contra] at hn
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : Nontrivial R
s : Set R[X]
hs : s.Finite
contra : Eq (α := Submodule R R[X]) (Submodule.span R s) ⊤
n : ℕ
hn : LE.le (α := Submodule R R[X]) ⊤ (degreeLE R (↑n : WithBot ℕ))
⊢ Membership.mem (γ := Submodule R R[X]) (degreeLE R (↑n : WithBot ℕ)) (HPow.hPow (α := R[X]) X (n + 1))

Tactic:
hn Submodule.mem_top

Premises used: Submodule.mem_top
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : Nontrivial R
s : Set R[X]
hs : s.Finite
contra : Eq (α := Submodule R R[X]) (Submodule.span R s) ⊤
n : ℕ
hn : LE.le (α := Submodule R R[X]) ⊤ (degreeLE R (↑n : WithBot ℕ))
⊢ Membership.mem (γ := Submodule R R[X]) (degreeLE R (↑n : WithBot ℕ)) (HPow.hPow (α := R[X]) X (n + 1))

Tactic:
exact hn Submodule.mem_top

Premises used: Submodule.mem_top
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : Nontrivial R
s : Set R[X]
hs : s.Finite
contra : Eq (α := Submodule R R[X]) (Submodule.span R s) ⊤
n : ℕ
hn : Submodule.span R s ≤ degreeLE R (↑n : WithBot ℕ)
⊢ Membership.mem (γ := Submodule R R[X]) (degreeLE R (↑n : WithBot ℕ)) (HPow.hPow (α := R[X]) X (n + 1))

Tactic:
have : ((X : R[X]) ^ (n + 1)) ∈ Polynomial.degreeLE R ↑n := by
    rw [contra] at hn
    exact hn Submodule.mem_top
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : Nontrivial R
s : Set R[X]
hs : s.Finite
contra : Eq (α := Submodule R R[X]) (Submodule.span R s) ⊤
n : ℕ
hn : Submodule.span R s ≤ degreeLE R (↑n : WithBot ℕ)
this : Membership.mem (γ := Submodule R R[X]) (degreeLE R (↑n : WithBot ℕ)) (HPow.hPow (α := R[X]) X (n + 1))
⊢ Eq (α := ℕ) 1 0

Tactic:
rw [mem_degreeLE, degree_X_pow, Nat.cast_le, add_le_iff_nonpos_right, nonpos_iff_eq_zero] at this

Premises used: add_le_iff_nonpos_right, Polynomial.degree_X_pow, Nat.cast_le, Polynomial.mem_degreeLE, nonpos_iff_eq_zero
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : Nontrivial R
s : Set R[X]
hs : s.Finite
contra : Eq (α := Submodule R R[X]) (Submodule.span R s) ⊤
n : ℕ
hn : Submodule.span R s ≤ degreeLE R (↑n : WithBot ℕ)
this : Eq (α := ℕ) 1 0
⊢ False

Tactic:
one_ne_zero this

Premises used: one_ne_zero
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : Nontrivial R
s : Set R[X]
hs : s.Finite
contra : Eq (α := Submodule R R[X]) (Submodule.span R s) ⊤
n : ℕ
hn : Submodule.span R s ≤ degreeLE R (↑n : WithBot ℕ)
this : Eq (α := ℕ) 1 0
⊢ False

Tactic:
exact one_ne_zero this

Premises used: one_ne_zero
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
n : ℕ
a :
  ∀ (i : ℕ),
    (comp (∑ i ∈ range n, HPow.hPow (α := R[X]) X i) (HAdd.hAdd (α := R[X]) X 1)).coeff i =
      coeff (∑ i ∈ range n, (↑(n.choose (i + 1)) : R[X]) * HPow.hPow (α := R[X]) X i) i
⊢ comp (∑ i ∈ range n, HPow.hPow (α := R[X]) X i) (HAdd.hAdd (α := R[X]) X 1) =
    ∑ i ∈ range n, (↑(n.choose (i + 1)) : R[X]) * HPow.hPow (α := R[X]) X i

Tactic:
ext i
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
n i : ℕ
trans :
  (comp (∑ i ∈ range n, HPow.hPow (α := R[X]) X i) (HAdd.hAdd (α := R[X]) X 1)).coeff i = (↑(n.choose (i + 1)) : R)
trans₁ :
  Eq.{u + 1} (α := R) (↑(n.choose (i + 1)) : R)
    (coeff (∑ i ∈ range n, (↑(n.choose (i + 1)) : R[X]) * HPow.hPow (α := R[X]) X i) i)
⊢ (comp (∑ i ∈ range n, HPow.hPow (α := R[X]) X i) (HAdd.hAdd (α := R[X]) X 1)).coeff i =
    coeff (∑ i ∈ range n, (↑(n.choose (i + 1)) : R[X]) * HPow.hPow (α := R[X]) X i) i

Tactic:
trans (n.choose (i + 1) : R)

Premises used: Nat.choose, Nat.cast, HAdd.hAdd, OfNat.ofNat