awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
n : ℕ
x : R[X]
x_zero : ¬x = 0
neg : x.degree < (↑(n + 1) : WithBot ℕ) ↔ Membership.mem (γ := Submodule R R[X]) (degreeLE R (↑n : WithBot ℕ)) x
neg₁ : x.degree < (↑(n + 1) : WithBot ℕ) ↔ x.degree ≤ (↑n : WithBot ℕ)
⊢ Membership.mem (γ := Submodule R R[X]) (degreeLT R (n + 1)) x ↔
    Membership.mem (γ := Submodule R R[X]) (degreeLE R (↑n : WithBot ℕ)) x
have neg₂ : x.natDegree < n + 1 ↔ x.degree ≤ (↑n : WithBot ℕ)
Tactic: rw [mem_degreeLT, mem_degreeLE, ← natDegree_lt_iff_degree_lt (by rwa [ne_eq]),
      ← natDegree_le_iff_degree_le, Nat.lt_succ_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
n : ℕ
x : R[X]
x_zero : ¬x = 0
neg : x.degree < (↑(n + 1) : WithBot ℕ) ↔ Membership.mem (γ := Submodule R R[X]) (degreeLE R (↑n : WithBot ℕ)) x
neg₁ : x.degree < (↑(n + 1) : WithBot ℕ) ↔ x.degree ≤ (↑n : WithBot ℕ)
neg₂ : x.natDegree < n + 1 ↔ x.degree ≤ (↑n : WithBot ℕ)
⊢ Membership.mem (γ := Submodule R R[X]) (degreeLT R (n + 1)) x ↔
    Membership.mem (γ := Submodule R R[X]) (degreeLE R (↑n : WithBot ℕ)) x
have neg₃ : x.natDegree < n + 1 ↔ x.natDegree ≤ n
Tactic: rw [mem_degreeLT, mem_degreeLE, ← natDegree_lt_iff_degree_lt (by rwa [ne_eq]),
      ← natDegree_le_iff_degree_le, Nat.lt_succ_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
n : ℕ
x : R[X]
x_zero : ¬x = 0
neg : x.degree < (↑(n + 1) : WithBot ℕ) ↔ Membership.mem (γ := Submodule R R[X]) (degreeLE R (↑n : WithBot ℕ)) x
neg₁ : x.degree < (↑(n + 1) : WithBot ℕ) ↔ x.degree ≤ (↑n : WithBot ℕ)
neg₂ : x.natDegree < n + 1 ↔ x.degree ≤ (↑n : WithBot ℕ)
neg₃ : x.natDegree < n + 1 ↔ x.natDegree ≤ n
⊢ Membership.mem (γ := Submodule R R[X]) (degreeLT R (n + 1)) x ↔
    Membership.mem (γ := Submodule R R[X]) (degreeLE R (↑n : WithBot ℕ)) x
have neg₄ : x.natDegree ≤ n ↔ x.natDegree ≤ n
Tactic: rw [mem_degreeLT, mem_degreeLE, ← natDegree_lt_iff_degree_lt (by rwa [ne_eq]),
      ← natDegree_le_iff_degree_le, Nat.lt_succ_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
S : Type u_1
inst : Semiring R
inst_1 : Nontrivial R
n : ℕ
p : { p : R[X] // p.Monic ∧ p.natDegree = n }
⊢ Membership.mem (γ := Submodule R R[X]) (degreeLT R n) (↑p : R[X]).eraseLead
have rcases : ∀ (p : R[X]) (hp : p.Monic),
  Membership.mem (γ := Submodule R R[X]) (degreeLT R p.natDegree)
    (↑(Subtype.mk (p := fun (p_1 : R[X]) ↦ p_1.Monic ∧ p_1.natDegree = p.natDegree) p sorry) : R[X]).eraseLead
Tactic: rcases p with ⟨p, hp, rfl⟩
Cleared hypotheses: n, p
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
S : Type u_1
inst : Semiring R
inst_1 : Nontrivial R
p : R[X]
hp : p.Monic
⊢ Membership.mem (γ := Submodule R R[X]) (degreeLT R p.natDegree)
    (↑(Subtype.mk (p := fun (p_1 : R[X]) ↦ p_1.Monic ∧ p_1.natDegree = p.natDegree) p ⋯) : R[X]).eraseLead
have simp : p.eraseLead.degree < (↑p.natDegree : WithBot ℕ)
Tactic: simp only [mem_degreeLT]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
S : Type u_1
inst : Semiring R
inst_1 : Nontrivial R
p : R[X]
hp : p.Monic
⊢ p.eraseLead.degree < (↑p.natDegree : WithBot ℕ)
have refine : p.eraseLead.degree < p.degree
Tactic: refine lt_of_lt_of_le ?_ degree_le_natDegree
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
S : Type u_1
inst : Semiring R
inst_1 : Nontrivial R
n : ℕ
p : ↥(degreeLT R n)
⊢ (HPow.hPow (α := R[X]) X n + (↑p : R[X])).natDegree = n
have rw : (HPow.hPow (α := R[X]) X n).natDegree = n
Tactic: rw [natDegree_add_eq_left_of_degree_lt]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
S : Type u_1
inst : Semiring R
inst_1 : Nontrivial R
n : ℕ
p : ↥(degreeLT R n)
rw : (HPow.hPow (α := R[X]) X n).natDegree = n
⊢ (HPow.hPow (α := R[X]) X n + (↑p : R[X])).natDegree = n
have rw₁ : (↑p : R[X]).degree < (HPow.hPow (α := R[X]) X n).degree
Tactic: rw [natDegree_add_eq_left_of_degree_lt]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
S : Type u_1
inst : Semiring R
inst_1 : Nontrivial R
p : R[X]
hp : p.Monic
⊢ Eq (α := { p_1 : R[X] // p_1.Monic ∧ p_1.natDegree = p.natDegree })
    ((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 ⋯)))
    (Subtype.mk (p := fun (p_1 : R[X]) ↦ p_1.Monic ∧ p_1.natDegree = p.natDegree) p ⋯)
have a : (↑((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])) sorry :
            { 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 sorry)
          (Subtype.mk (p := fun (p_1 : R[X]) ↦ p_1.Monic ∧ p_1.natDegree = p.natDegree) p sorry))) :
    R[X]) =
  (↑(Subtype.mk (p := fun (p_1 : R[X]) ↦ p_1.Monic ∧ p_1.natDegree = p.natDegree) p sorry) : R[X])
Tactic: ext1
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
S : Type u_1
inst : Semiring R
inst_1 : Nontrivial R
p : R[X]
hp : p.Monic
⊢ (↑((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])
have a : HPow.hPow (α := R[X]) X p.natDegree + p.eraseLead = p
Tactic: simp only
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
S : Type u_1
inst : Semiring R
inst_1 : Nontrivial R
p : R[X]
hp : p.Monic
| p
have rw : p.eraseLead + HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X p.natDegree)
Tactic: rw [← eraseLead_add_C_mul_X_pow p]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
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
have 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)
Tactic: conv_rhs => rw [← eraseLead_add_C_mul_X_pow p]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
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
⊢ (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
have 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 sorry)
        ((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])) sorry :
              { 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: ext1
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
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
⊢ (↑((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])
have a : (HPow.hPow (α := R[X]) X n + p).eraseLead = p
Tactic: simp only
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
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 + p).eraseLead = p
have a : (HPow.hPow (α := R[X]) X n).eraseLead + p = p
Tactic: rw [eraseLead_add_of_degree_lt_left]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
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
⊢ (HPow.hPow (α := R[X]) X n + p).eraseLead = p
have a₁ : p.degree < (HPow.hPow (α := R[X]) X n).degree
Tactic: rw [eraseLead_add_of_degree_lt_left]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
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
⊢ ∃ p' ∈ s, p.degree ≤ p'.degree
have by_contra! : ∀ (h : ∀ (p' : R[X]) (_ : p' ∈ s), p'.degree < p.degree), False
Tactic: by_contra! h
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
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
⊢ False
have pos : ∀ (hp_zero : p = 0), False
Tactic: by_cases hp_zero : p = 0
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
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
⊢ False
have neg : ∀ (hp_zero : ¬p = 0), False
Tactic: by_cases hp_zero : p = 0
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (hypothesis)
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
⊢ False
have h₁ : ∀ (p' : R[X]) (_ : p' ∈ s), p'.degree < ⊥
Tactic: rw [hp_zero, degree_zero] at h
Cleared hypotheses: h, hp_zero
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
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
⊢ False
have pos : ∀ (x : R[X]) (hx : x ∈ s), False
Tactic: rcases hs with ⟨x, hx⟩
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
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
have refine : ∀ (p' : R[X]) (p'_mem : p' ∈ s), p' ∈ (↑(degreeLT R p.natDegree) : Set R[X])
Tactic: refine (Submodule.span_le.mpr fun p' p'_mem => ?_) hp
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
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' ∈ (↑(degreeLT R p.natDegree) : Set R[X])
have rw : p'.degree < (↑p.natDegree : WithBot ℕ)
Tactic: rw [SetLike.mem_coe, mem_degreeLT, Nat.cast_withBot]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (hypothesis)
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
⊢ False
have this : 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
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
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
⊢ False
have neg : ∀ (this : p.degree < (↑p.natDegree : WithBot ℕ)), False
Tactic: rwa [mem_degreeLT, Nat.cast_withBot, degree_eq_natDegree hp_zero,
      Nat.cast_withBot, lt_self_iff_false] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
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
⊢ False
have neg₁ : ∀ (this : p.degree < (↑p.natDegree : WithBot ℕ)), False
Tactic: rwa [mem_degreeLT, Nat.cast_withBot, degree_eq_natDegree hp_zero,
      Nat.cast_withBot, lt_self_iff_false] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
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
⊢ False
have neg₂ : ∀ (this : (↑p.natDegree : WithBot ℕ) < (↑p.natDegree : WithBot ℕ)), False
Tactic: rwa [mem_degreeLT, Nat.cast_withBot, degree_eq_natDegree hp_zero,
      Nat.cast_withBot, lt_self_iff_false] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
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
⊢ False
have neg₃ : ∀ (this : (↑p.natDegree : WithBot ℕ) < (↑p.natDegree : WithBot ℕ)), False
Tactic: rwa [mem_degreeLT, Nat.cast_withBot, degree_eq_natDegree hp_zero,
      Nat.cast_withBot, lt_self_iff_false] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
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
⊢ False
have neg₄ : ∀ (this : False), False
Tactic: rwa [mem_degreeLT, Nat.cast_withBot, degree_eq_natDegree hp_zero,
      Nat.cast_withBot, lt_self_iff_false] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
s : Set R[X]
s_fin : s.Finite
hs : s.Nonempty
⊢ ∃ p' ∈ s, ∀ (p : R[X]), Membership.mem (γ := Submodule R R[X]) (Submodule.span R s) p → p.degree ≤ p'.degree
have 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
Tactic: obtain ⟨a, has, hmax⟩ := s_fin.exists_maximalFor degree s hs
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
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
have refine : ∀ (p : R[X]) (hp : Membership.mem (γ := Submodule R R[X]) (Submodule.span R s) p), p.degree ≤ a.degree
Tactic: refine ⟨a, has, fun p hp => ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
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.degree ≤ a.degree
have obtain : ∀ (p' : R[X]) (hp' : p' ∈ s) (hpp' : p.degree ≤ p'.degree), p.degree ≤ a.degree
Tactic: obtain ⟨p', hp', hpp'⟩ := exists_degree_le_of_mem_span hs hp
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
s : Set R[X]
s_fin : s.Finite
⊢ ∃ (n : ℕ), Submodule.span R s ≤ degreeLE R (↑n : WithBot ℕ)
have pos : ∀ (s_emp : s.Nonempty), ∃ (n : ℕ), Submodule.span R s ≤ degreeLE R (↑n : WithBot ℕ)
Tactic: by_cases s_emp : s.Nonempty
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
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 ℕ)
⊢ ∃ (n : ℕ), Submodule.span R s ≤ degreeLE R (↑n : WithBot ℕ)
have neg : ∀ (s_emp : ¬s.Nonempty), ∃ (n : ℕ), Submodule.span R s ≤ degreeLE R (↑n : WithBot ℕ)
Tactic: by_cases s_emp : s.Nonempty
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
s : Set R[X]
s_fin : s.Finite
s_emp : s.Nonempty
⊢ ∃ (n : ℕ), Submodule.span R s ≤ degreeLE R (↑n : WithBot ℕ)
have 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 ℕ)
Tactic: rcases exists_degree_le_of_mem_span_of_finite s_fin s_emp with ⟨p', _, hp'max⟩
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (hypothesis)
Goal:
R : Type u
inst : Semiring R
s : Set R[X]
s_fin : s.Finite
s_emp : ¬s.Nonempty
⊢ ∃ (n : ℕ), Submodule.span R s ≤ degreeLE R (↑n : WithBot ℕ)
have s_emp₁ : s = ∅
Tactic: rw [Set.not_nonempty_iff_eq_empty] at s_emp
Cleared hypotheses: s_emp
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
s : Set R[X]
s_fin : s.Finite
s_emp : s = ∅
⊢ ∃ (n : ℕ), Submodule.span R s ≤ degreeLE R (↑n : WithBot ℕ)
have neg : ∃ (n : ℕ), LE.le (α := Submodule R R[X]) ⊥ (degreeLE R (↑n : WithBot ℕ))
Tactic: rw [s_emp, Submodule.span_empty]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
s : Set R[X]
s_fin : s.Finite
⊢ ∃ (n : ℕ), Submodule.span R s ≤ degreeLT R n
have rcases : ∀ (n : ℕ), Submodule.span R s ≤ degreeLE R (↑n : WithBot ℕ) → ∃ (n : ℕ), Submodule.span R s ≤ degreeLT R n
Tactic: rcases span_le_degreeLE_of_finite s_fin with ⟨n, _⟩
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : Nontrivial R
⊢ ¬Module.Finite R R[X]
have rw : ¬∃ (S : Set R[X]), S.Finite ∧ Eq (α := Submodule R R[X]) (Submodule.span R S) ⊤
Tactic: rw [Module.finite_def, Submodule.fg_def]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : Nontrivial R
⊢ ¬∃ (S : Set R[X]), S.Finite ∧ Eq (α := Submodule R R[X]) (Submodule.span R S) ⊤
have push : ∀ (S : Set R[X]) (_ : S.Finite), Ne (α := Submodule R R[X]) (Submodule.span R S) ⊤
Tactic: push Not
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
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) ⊤
⊢ False
have rcases : ∀ (n : ℕ) (hn : Submodule.span R s ≤ degreeLE R (↑n : WithBot ℕ)), False
Tactic: rcases span_le_degreeLE_of_finite hs with ⟨n, hn⟩
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (hypothesis)
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))
have hn₁ : LE.le (α := Submodule R R[X]) ⊤ (degreeLE R (↑n : WithBot ℕ))
Tactic: rw [contra] at hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (hypothesis)
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 ℕ)
⊢ False
have this : 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
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (hypothesis)
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))
⊢ False
have this₁ : Eq (α := ℕ) 1 0
Tactic: rw [mem_degreeLE, degree_X_pow, Nat.cast_le, add_le_iff_nonpos_right, nonpos_iff_eq_zero] at this
Cleared hypotheses: this