-- Mathlib/RingTheory/Polynomial/Basic.lean
theorem exists_degree_le_of_mem_span {s : Set R[X]} {p : R[X]}
    (hs : s.Nonempty) (hp : p ∈ Submodule.span R s) :
    ∃ p' ∈ s, degree p ≤ degree p'

Proof state:
R : Type u
inst✝ : Semiring R
s : Set R[X]
p : R[X]
hs : s.Nonempty
hp : p ∈ Submodule.span R s
h : ∀ p' ∈ s, p'.degree < p.degree
hp_zero : ¬p = 0
⊢ p ∈ degreeLT R p.natDegree

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

Result:
R : Type u
inst✝ : Semiring R
s : Set R[X]
p : R[X]
hs : s.Nonempty
hp : p ∈ Submodule.span R s
h : ∀ p' ∈ s, p'.degree < p.degree
hp_zero : ¬p = 0
p' : R[X]
p'_mem : p' ∈ s
⊢ p' ∈ ↑(degreeLT R p.natDegree)

Proof state:
R : Type u
inst✝ : Semiring R
s : Set R[X]
p : R[X]
hs : s.Nonempty
hp : p ∈ Submodule.span R s
⊢ ∃ p' ∈ s, p.degree ≤ p'.degree

Tactic:
by_contra! h

Result:
R : Type u
inst✝ : Semiring R
s : Set R[X]
p : R[X]
hs : s.Nonempty
hp : p ∈ Submodule.span R s
h : ∀ p' ∈ s, p'.degree < p.degree
⊢ False

Proof state:
case neg
R : Type u
inst✝ : Semiring R
s : Set R[X]
p : R[X]
hs : s.Nonempty
hp : p ∈ Submodule.span R s
h : ∀ p' ∈ s, p'.degree < p.degree
hp_zero : ¬p = 0
this : p ∈ degreeLT R p.natDegree
⊢ False

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

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
s : Set R[X]
p : R[X]
hs : s.Nonempty
hp : p ∈ Submodule.span R s
h : ∀ p' ∈ s, p'.degree < p.degree
hp_zero : ¬p = 0
p' : R[X]
p'_mem : p' ∈ s
⊢ p'.degree < ↑p.natDegree

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

Result:
no goals

Proof state:
case pos.intro
R : Type u
inst✝ : Semiring R
s : Set R[X]
p : R[X]
hp : p ∈ Submodule.span R s
h : ∀ p' ∈ s, p'.degree < ⊥
hp_zero : p = 0
x : R[X]
hx : x ∈ s
⊢ False

Tactic:
exact not_lt_bot (h x hx)

Result:
no goals

Proof state:
case pos
R : Type u
inst✝ : Semiring R
s : Set R[X]
p : R[X]
hs : s.Nonempty
hp : p ∈ Submodule.span R s
h : ∀ p' ∈ s, p'.degree < p.degree
hp_zero : p = 0
⊢ False

Tactic:
rw [hp_zero, degree_zero] at h

Result:
case pos
R : Type u
inst✝ : Semiring R
s : Set R[X]
p : R[X]
hs : s.Nonempty
hp : p ∈ Submodule.span R s
h : ∀ p' ∈ s, p'.degree < ⊥
hp_zero : p = 0
⊢ False

Proof state:
case pos
R : Type u
inst✝ : Semiring R
s : Set R[X]
p : R[X]
hs : s.Nonempty
hp : p ∈ Submodule.span R s
h : ∀ p' ∈ s, p'.degree < ⊥
hp_zero : p = 0
⊢ False

Tactic:
rcases hs with ⟨x, hx⟩

Result:
case pos.intro
R : Type u
inst✝ : Semiring R
s : Set R[X]
p : R[X]
hp : p ∈ Submodule.span R s
h : ∀ p' ∈ s, p'.degree < ⊥
hp_zero : p = 0
x : R[X]
hx : x ∈ s
⊢ False

Proof state:
R : Type u
inst✝ : Semiring R
s : Set R[X]
p : R[X]
hs : s.Nonempty
hp : p ∈ Submodule.span R s
h : ∀ p' ∈ s, p'.degree < p.degree
hp_zero : ¬p = 0
p' : R[X]
p'_mem : p' ∈ s
⊢ p' ∈ ↑(degreeLT R p.natDegree)

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

Result:
R : Type u
inst✝ : Semiring R
s : Set R[X]
p : R[X]
hs : s.Nonempty
hp : p ∈ Submodule.span R s
h : ∀ p' ∈ s, p'.degree < p.degree
hp_zero : ¬p = 0
p' : R[X]
p'_mem : p' ∈ s
⊢ p'.degree < ↑p.natDegree

Proof state:
case neg
R : Type u
inst✝ : Semiring R
s : Set R[X]
p : R[X]
hs : s.Nonempty
hp : p ∈ Submodule.span R s
h : ∀ p' ∈ s, p'.degree < p.degree
hp_zero : ¬p = 0
⊢ False

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

Result:
case neg
R : Type u
inst✝ : Semiring R
s : Set R[X]
p : R[X]
hs : s.Nonempty
hp : p ∈ Submodule.span R s
h : ∀ p' ∈ s, p'.degree < p.degree
hp_zero : ¬p = 0
this : p ∈ degreeLT R p.natDegree
⊢ False

Proof state:
R : Type u
inst✝ : Semiring R
s : Set R[X]
p : R[X]
hs : s.Nonempty
hp : p ∈ Submodule.span R s
h : ∀ p' ∈ s, p'.degree < p.degree
⊢ False

Tactic:
by_cases hp_zero : p = 0

Result:
case pos
R : Type u
inst✝ : Semiring R
s : Set R[X]
p : R[X]
hs : s.Nonempty
hp : p ∈ Submodule.span R s
h : ∀ p' ∈ s, p'.degree < p.degree
hp_zero : p = 0
⊢ False

case neg
R : Type u
inst✝ : Semiring R
s : Set R[X]
p : R[X]
hs : s.Nonempty
hp : p ∈ Submodule.span R s
h : ∀ p' ∈ s, p'.degree < p.degree
hp_zero : ¬p = 0
⊢ False