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

Proof state:
case intro.intro
R : Type u
inst✝ : Semiring R
s : Set R[X]
s_fin : s.Finite
hs : s.Nonempty
a : R[X]
has : a ∈ s
hmax : ∀ a' ∈ s, a.degree ≤ a'.degree → a.degree = a'.degree
p : R[X]
hp : p ∈ Submodule.span R s
⊢ p.degree ≤ a.degree

Tactic:
rcases exists_degree_le_of_mem_span hs hp with ⟨p', hp'⟩

Result:
case intro.intro.intro
R : Type u
inst✝ : Semiring R
s : Set R[X]
s_fin : s.Finite
hs : s.Nonempty
a : R[X]
has : a ∈ s
hmax : ∀ a' ∈ s, a.degree ≤ a'.degree → a.degree = a'.degree
p : R[X]
hp : p ∈ Submodule.span R s
p' : R[X]
hp' : p' ∈ s ∧ p.degree ≤ p'.degree
⊢ p.degree ≤ a.degree

Proof state:
case intro.intro
R : Type u
inst✝ : Semiring R
s : Set R[X]
s_fin : s.Finite
hs : s.Nonempty
a : R[X]
has : a ∈ s
hmax : ∀ a' ∈ s, a.degree ≤ a'.degree → a.degree = a'.degree
⊢ ∃ p' ∈ s, ∀ p ∈ Submodule.span R s, p.degree ≤ p'.degree

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

Result:
case intro.intro
R : Type u
inst✝ : Semiring R
s : Set R[X]
s_fin : s.Finite
hs : s.Nonempty
a : R[X]
has : a ∈ s
hmax : ∀ a' ∈ s, a.degree ≤ a'.degree → a.degree = a'.degree
p : R[X]
hp : p ∈ Submodule.span R s
⊢ p.degree ≤ a.degree

Proof state:
case neg
R : Type u
inst✝ : Semiring R
s : Set R[X]
s_fin : s.Finite
hs : s.Nonempty
a : R[X]
has : a ∈ s
hmax : ∀ a' ∈ s, a.degree ≤ a'.degree → a.degree = a'.degree
p : R[X]
hp : p ∈ Submodule.span R s
p' : R[X]
hp' : p' ∈ s ∧ p.degree ≤ p'.degree
h : ¬a.degree ≤ p'.degree
⊢ p.degree ≤ a.degree

Tactic:
exact le_trans hp'.right (not_le.mp h).le

Result:
no goals

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

Tactic:
rcases Set.Finite.exists_maximal_wrt degree s s_fin hs with ⟨a, has, hmax⟩

Result:
case intro.intro
R : Type u
inst✝ : Semiring R
s : Set R[X]
s_fin : s.Finite
hs : s.Nonempty
a : R[X]
has : a ∈ s
hmax : ∀ a' ∈ s, a.degree ≤ a'.degree → a.degree = a'.degree
⊢ ∃ p' ∈ s, ∀ p ∈ Submodule.span R s, p.degree ≤ p'.degree

Proof state:
case pos
R : Type u
inst✝ : Semiring R
s : Set R[X]
s_fin : s.Finite
hs : s.Nonempty
a : R[X]
has : a ∈ s
hmax : ∀ a' ∈ s, a.degree ≤ a'.degree → a.degree = a'.degree
p : R[X]
hp : p ∈ Submodule.span R s
p' : R[X]
hp' : p' ∈ s ∧ p.degree ≤ p'.degree
h : a.degree ≤ p'.degree
⊢ p.degree ≤ a.degree

Tactic:
rw [← hmax p' hp'.left h] at hp'

Result:
case pos
R : Type u
inst✝ : Semiring R
s : Set R[X]
s_fin : s.Finite
hs : s.Nonempty
a : R[X]
has : a ∈ s
hmax : ∀ a' ∈ s, a.degree ≤ a'.degree → a.degree = a'.degree
p : R[X]
hp : p ∈ Submodule.span R s
p' : R[X]
hp' : p' ∈ s ∧ p.degree ≤ a.degree
h : a.degree ≤ p'.degree
⊢ p.degree ≤ a.degree

Proof state:
case pos
R : Type u
inst✝ : Semiring R
s : Set R[X]
s_fin : s.Finite
hs : s.Nonempty
a : R[X]
has : a ∈ s
hmax : ∀ a' ∈ s, a.degree ≤ a'.degree → a.degree = a'.degree
p : R[X]
hp : p ∈ Submodule.span R s
p' : R[X]
hp' : p' ∈ s ∧ p.degree ≤ a.degree
h : a.degree ≤ p'.degree
⊢ p.degree ≤ a.degree

Tactic:
exact hp'.right

Result:
no goals

Proof state:
case intro.intro.intro
R : Type u
inst✝ : Semiring R
s : Set R[X]
s_fin : s.Finite
hs : s.Nonempty
a : R[X]
has : a ∈ s
hmax : ∀ a' ∈ s, a.degree ≤ a'.degree → a.degree = a'.degree
p : R[X]
hp : p ∈ Submodule.span R s
p' : R[X]
hp' : p' ∈ s ∧ p.degree ≤ p'.degree
⊢ p.degree ≤ a.degree

Tactic:
by_cases h : degree a ≤ degree p'

Result:
case pos
R : Type u
inst✝ : Semiring R
s : Set R[X]
s_fin : s.Finite
hs : s.Nonempty
a : R[X]
has : a ∈ s
hmax : ∀ a' ∈ s, a.degree ≤ a'.degree → a.degree = a'.degree
p : R[X]
hp : p ∈ Submodule.span R s
p' : R[X]
hp' : p' ∈ s ∧ p.degree ≤ p'.degree
h : a.degree ≤ p'.degree
⊢ p.degree ≤ a.degree

case neg
R : Type u
inst✝ : Semiring R
s : Set R[X]
s_fin : s.Finite
hs : s.Nonempty
a : R[X]
has : a ∈ s
hmax : ∀ a' ∈ s, a.degree ≤ a'.degree → a.degree = a'.degree
p : R[X]
hp : p ∈ Submodule.span R s
p' : R[X]
hp' : p' ∈ s ∧ p.degree ≤ p'.degree
h : ¬a.degree ≤ p'.degree
⊢ p.degree ≤ a.degree