awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
S : Type v
inst : Semiring R
f : S → R[X]
s : Finset S
h : Set.Pairwise {i : S | i ∈ s ∧ f i ≠ 0} (Ne on natDegree ∘ f)
x : S
hx : x ∈ s
hx' : f x ≠ 0
hs : s.Nonempty
pos : (s.sum f).degree = (↑(s.sup fun (i : S) ↦ (f i).natDegree) : WithBot ℕ)
⊢ (s.sum f).natDegree = s.sup fun (i : S) ↦ (f i).natDegree

Tactic:
refine natDegree_eq_of_degree_eq_some ?_

Premises used: Polynomial.natDegree_eq_of_degree_eq_some
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
S : Type v
inst : Semiring R
f : S → R[X]
s : Finset S
h : Set.Pairwise {i : S | i ∈ s ∧ f i ≠ 0} (Ne on natDegree ∘ f)
x : S
hx : x ∈ s
hx' : f x ≠ 0
hs : s.Nonempty
pos : Eq (α := WithBot ℕ) (s.sup fun (i : S) ↦ (f i).degree) (↑(s.sup fun (i : S) ↦ (f i).natDegree) : WithBot ℕ)
pos₁ : Set.Pairwise {i : S | i ∈ s ∧ f i ≠ 0} (Ne on degree ∘ f)
⊢ (s.sum f).degree = (↑(s.sup fun (i : S) ↦ (f i).natDegree) : WithBot ℕ)

Tactic:
rw [degree_sum_eq_of_disjoint]

Premises used: Polynomial.degree_sum_eq_of_disjoint
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
S : Type v
inst : Semiring R
f : S → R[X]
s : Finset S
h : Set.Pairwise {i : S | i ∈ s ∧ f i ≠ 0} (Ne on natDegree ∘ f)
x : S
hx : x ∈ s
hx' : f x ≠ 0
hs : s.Nonempty
pos :
  Eq (α := WithBot ℕ) (s.sup' hs fun (i : S) ↦ (f i).degree) (s.sup' hs (WithBot.some ∘ fun (i : S) ↦ (f i).natDegree))
⊢ Eq (α := WithBot ℕ) (s.sup fun (i : S) ↦ (f i).degree) (↑(s.sup fun (i : S) ↦ (f i).natDegree) : WithBot ℕ)

Tactic:
rw [← Finset.sup'_eq_sup hs, ← Finset.sup'_eq_sup hs,
        Nat.cast_withBot, Finset.coe_sup' hs, ←
        Finset.sup'_eq_sup hs]

Premises used: Finset.coe_sup', Nat.cast_withBot, Finset.sup'_eq_sup
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
S : Type v
inst : Semiring R
f : S → R[X]
s : Finset S
h : Set.Pairwise {i : S | i ∈ s ∧ f i ≠ 0} (Ne on natDegree ∘ f)
x : S
hx : x ∈ s
hx' : f x ≠ 0
hs : s.Nonempty
⊢ Eq (α := WithBot ℕ) (s.sup' hs fun (i : S) ↦ (f i).degree) (s.sup' hs (WithBot.some ∘ fun (i : S) ↦ (f i).natDegree))

Tactic:
le_antisymm ?_ ?_

Premises used: le_antisymm
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
S : Type v
inst : Semiring R
f : S → R[X]
s : Finset S
h : Set.Pairwise {i : S | i ∈ s ∧ f i ≠ 0} (Ne on natDegree ∘ f)
x : S
hx : x ∈ s
hx' : f x ≠ 0
hs : s.Nonempty
pos :
  LE.le (α := WithBot ℕ) (s.sup' hs fun (i : S) ↦ (f i).degree)
    (s.sup' hs (WithBot.some ∘ fun (i : S) ↦ (f i).natDegree))
pos₁ :
  LE.le (α := WithBot ℕ) (s.sup' hs (WithBot.some ∘ fun (i : S) ↦ (f i).natDegree))
    (s.sup' hs fun (i : S) ↦ (f i).degree)
⊢ Eq (α := WithBot ℕ) (s.sup' hs fun (i : S) ↦ (f i).degree) (s.sup' hs (WithBot.some ∘ fun (i : S) ↦ (f i).natDegree))

Tactic:
refine le_antisymm ?_ ?_

Premises used: le_antisymm
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
S : Type v
inst : Semiring R
f : S → R[X]
s : Finset S
h : Set.Pairwise {i : S | i ∈ s ∧ f i ≠ 0} (Ne on natDegree ∘ f)
x : S
hx : x ∈ s
hx' : f x ≠ 0
hs : s.Nonempty
pos : ∀ b ∈ s, (f b).degree ≤ s.sup' hs (WithBot.some ∘ fun (i : S) ↦ (f i).natDegree)
⊢ LE.le (α := WithBot ℕ) (s.sup' hs fun (i : S) ↦ (f i).degree)
    (s.sup' hs (WithBot.some ∘ fun (i : S) ↦ (f i).natDegree))

Tactic:
rw [Finset.sup'_le_iff]

Premises used: Finset.sup'_le_iff
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
S : Type v
inst : Semiring R
f : S → R[X]
s : Finset S
h : Set.Pairwise {i : S | i ∈ s ∧ f i ≠ 0} (Ne on natDegree ∘ f)
x : S
hx : x ∈ s
hx' : f x ≠ 0
hs : s.Nonempty
b : S
hb : b ∈ s
pos : ∀ (hb' : f b = 0), (f b).degree ≤ s.sup' hs (WithBot.some ∘ fun (i : S) ↦ (f i).natDegree)
neg : ∀ (hb' : ¬f b = 0), (f b).degree ≤ s.sup' hs (WithBot.some ∘ fun (i : S) ↦ (f i).natDegree)
⊢ (f b).degree ≤ s.sup' hs (WithBot.some ∘ fun (i : S) ↦ (f i).natDegree)

Tactic:
by_cases hb' : f b = 0
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
S : Type v
inst : Semiring R
f : S → R[X]
s : Finset S
h : Set.Pairwise {i : S | i ∈ s ∧ f i ≠ 0} (Ne on natDegree ∘ f)
x : S
hx : x ∈ s
hx' : f x ≠ 0
hs : s.Nonempty
b : S
hb : b ∈ s
hb' : f b = 0
⊢ (f b).degree ≤ s.sup' hs (WithBot.some ∘ fun (i : S) ↦ (f i).natDegree)

Tactic:
simpa [hb'] using hs
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
S : Type v
inst : Semiring R
f : S → R[X]
s : Finset S
h : Set.Pairwise {i : S | i ∈ s ∧ f i ≠ 0} (Ne on natDegree ∘ f)
x : S
hx : x ∈ s
hx' : f x ≠ 0
hs : s.Nonempty
b : S
hb : b ∈ s
hb' : ¬f b = 0
neg : (↑(f b).natDegree : WithBot ℕ) ≤ s.sup' hs (WithBot.some ∘ fun (i : S) ↦ (f i).natDegree)
⊢ (f b).degree ≤ s.sup' hs (WithBot.some ∘ fun (i : S) ↦ (f i).natDegree)

Tactic:
rw [degree_eq_natDegree hb', Nat.cast_withBot]

Premises used: Polynomial.degree_eq_natDegree, Nat.cast_withBot
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
S : Type v
inst : Semiring R
f : S → R[X]
s : Finset S
h : Set.Pairwise {i : S | i ∈ s ∧ f i ≠ 0} (Ne on natDegree ∘ f)
x : S
hx : x ∈ s
hx' : f x ≠ 0
hs : s.Nonempty
b : S
hb : b ∈ s
hb' : ¬f b = 0
⊢ (↑(f b).natDegree : WithBot ℕ) ≤ s.sup' hs (WithBot.some ∘ fun (i : S) ↦ (f i).natDegree)

Tactic:
Finset.le_sup' (fun i : S => (natDegree (f i) : WithBot ℕ)) hb

Premises used: Nat.cast, Polynomial.natDegree, Finset.le_sup'
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
S : Type v
inst : Semiring R
f : S → R[X]
s : Finset S
h : Set.Pairwise {i : S | i ∈ s ∧ f i ≠ 0} (Ne on natDegree ∘ f)
x : S
hx : x ∈ s
hx' : f x ≠ 0
hs : s.Nonempty
b : S
hb : b ∈ s
hb' : ¬f b = 0
⊢ (↑(f b).natDegree : WithBot ℕ) ≤ s.sup' hs (WithBot.some ∘ fun (i : S) ↦ (f i).natDegree)

Tactic:
exact Finset.le_sup' (fun i : S => (natDegree (f i) : WithBot ℕ)) hb

Premises used: Nat.cast, Polynomial.natDegree, Finset.le_sup'
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
S : Type v
inst : Semiring R
f : S → R[X]
s : Finset S
h : Set.Pairwise {i : S | i ∈ s ∧ f i ≠ 0} (Ne on natDegree ∘ f)
x : S
hx : x ∈ s
hx' : f x ≠ 0
hs : s.Nonempty
pos :
  ∀ b ∈ s,
    LE.le (α := WithBot ℕ) ((WithBot.some ∘ fun (i : S) ↦ (f i).natDegree) b) (s.sup' hs fun (i : S) ↦ (f i).degree)
⊢ LE.le (α := WithBot ℕ) (s.sup' hs (WithBot.some ∘ fun (i : S) ↦ (f i).natDegree))
    (s.sup' hs fun (i : S) ↦ (f i).degree)

Tactic:
rw [Finset.sup'_le_iff]

Premises used: Finset.sup'_le_iff
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
S : Type v
inst : Semiring R
f : S → R[X]
s : Finset S
h : Set.Pairwise {i : S | i ∈ s ∧ f i ≠ 0} (Ne on natDegree ∘ f)
x : S
hx : x ∈ s
hx' : f x ≠ 0
hs : s.Nonempty
b : S
hb : b ∈ s
pos : ∃ b_1 ∈ s, (↑(f b).natDegree : WithBot ℕ) ≤ (f b_1).degree
⊢ LE.le (α := WithBot ℕ) ((WithBot.some ∘ fun (i : S) ↦ (f i).natDegree) b) (s.sup' hs fun (i : S) ↦ (f i).degree)

Tactic:
simp only [Finset.le_sup'_iff, Function.comp_apply]

Premises used: Finset.le_sup'_iff, Function.comp_apply
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
S : Type v
inst : Semiring R
f : S → R[X]
s : Finset S
h : Set.Pairwise {i : S | i ∈ s ∧ f i ≠ 0} (Ne on natDegree ∘ f)
x : S
hx : x ∈ s
hx' : f x ≠ 0
hs : s.Nonempty
b : S
hb : b ∈ s
pos : ∀ (hb' : f b = 0), ∃ b_1 ∈ s, (↑(f b).natDegree : WithBot ℕ) ≤ (f b_1).degree
neg : ∀ (hb' : ¬f b = 0), ∃ b_1 ∈ s, (↑(f b).natDegree : WithBot ℕ) ≤ (f b_1).degree
⊢ ∃ b_1 ∈ s, (↑(f b).natDegree : WithBot ℕ) ≤ (f b_1).degree

Tactic:
by_cases hb' : f b = 0
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
S : Type v
inst : Semiring R
f : S → R[X]
s : Finset S
h : Set.Pairwise {i : S | i ∈ s ∧ f i ≠ 0} (Ne on natDegree ∘ f)
x : S
hx : x ∈ s
hx' : f x ≠ 0
hs : s.Nonempty
b : S
hb : b ∈ s
hb' : f b = 0
⊢ ∃ b_1 ∈ s, (↑(f b).natDegree : WithBot ℕ) ≤ (f b_1).degree

Tactic:
⟨x, hx, ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
S : Type v
inst : Semiring R
f : S → R[X]
s : Finset S
h : Set.Pairwise {i : S | i ∈ s ∧ f i ≠ 0} (Ne on natDegree ∘ f)
x : S
hx : x ∈ s
hx' : f x ≠ 0
hs : s.Nonempty
b : S
hb : b ∈ s
hb' : f b = 0
pos : (↑(f b).natDegree : WithBot ℕ) ≤ (f x).degree
⊢ ∃ b_1 ∈ s, (↑(f b).natDegree : WithBot ℕ) ≤ (f b_1).degree

Tactic:
refine ⟨x, hx, ?_⟩
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
S : Type v
inst : Semiring R
f : S → R[X]
s : Finset S
h : Set.Pairwise {i : S | i ∈ s ∧ f i ≠ 0} (Ne on natDegree ∘ f)
x : S
hx : x ∈ s
hx' : f x ≠ 0
hs : s.Nonempty
b : S
hb : b ∈ s
hb' : f b = 0
pos : ∀ (hx' : (f x).degree < (↑(f b).natDegree : WithBot ℕ)), f x = 0
⊢ (↑(f b).natDegree : WithBot ℕ) ≤ (f x).degree

Tactic:
contrapose! hx'
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
S : Type v
inst : Semiring R
f : S → R[X]
s : Finset S
h : Set.Pairwise {i : S | i ∈ s ∧ f i ≠ 0} (Ne on natDegree ∘ f)
x : S
hx : x ∈ s
hs : s.Nonempty
b : S
hb : b ∈ s
hb' : f b = 0
hx' : (f x).degree < (↑(f b).natDegree : WithBot ℕ)
⊢ f x = 0

Tactic:
simpa [← Nat.cast_withBot, hb', degree_eq_bot] using hx'

Premises used: Nat.cast_withBot, Polynomial.degree_eq_bot
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
S : Type v
inst : Semiring R
f : S → R[X]
s : Finset S
h : Set.Pairwise {i : S | i ∈ s ∧ f i ≠ 0} (Ne on natDegree ∘ f)
x : S
hx : x ∈ s
hx' : f x ≠ 0
hs : s.Nonempty
b : S
hb : b ∈ s
hb' : ¬f b = 0
⊢ ∃ b_1 ∈ s, (↑(f b).natDegree : WithBot ℕ) ≤ (f b_1).degree

Tactic:
⟨b, hb, (degree_eq_natDegree hb').ge⟩

Premises used: Eq.ge, Polynomial.degree_eq_natDegree, And.intro, Exists.intro
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
S : Type v
inst : Semiring R
f : S → R[X]
s : Finset S
h : Set.Pairwise {i : S | i ∈ s ∧ f i ≠ 0} (Ne on natDegree ∘ f)
x : S
hx : x ∈ s
hx' : f x ≠ 0
hs : s.Nonempty
b : S
hb : b ∈ s
hb' : ¬f b = 0
⊢ ∃ b_1 ∈ s, (↑(f b).natDegree : WithBot ℕ) ≤ (f b_1).degree

Tactic:
exact ⟨b, hb, (degree_eq_natDegree hb').ge⟩
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
S : Type v
inst : Semiring R
f : S → R[X]
s : Finset S
h : Set.Pairwise {i : S | i ∈ s ∧ f i ≠ 0} (Ne on natDegree ∘ f)
x : S
hx : x ∈ s
hx' : f x ≠ 0
hs : s.Nonempty
⊢ Set.Pairwise {i : S | i ∈ s ∧ f i ≠ 0} (Ne on degree ∘ f)

Tactic:
h.imp fun x y hxy hxy' => hxy (natDegree_eq_of_degree_eq hxy')

Premises used: Polynomial.natDegree_eq_of_degree_eq, Set.Pairwise.imp
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
S : Type v
inst : Semiring R
f : S → R[X]
s : Finset S
h : Set.Pairwise {i : S | i ∈ s ∧ f i ≠ 0} (Ne on natDegree ∘ f)
x : S
hx : x ∈ s
hx' : f x ≠ 0
hs : s.Nonempty
⊢ Set.Pairwise {i : S | i ∈ s ∧ f i ≠ 0} (Ne on degree ∘ f)

Tactic:
exact h.imp fun x y hxy hxy' => hxy (natDegree_eq_of_degree_eq hxy')

Premises used: Polynomial.natDegree_eq_of_degree_eq, Set.Pairwise.imp
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
S : Type v
inst : Semiring R
f : S → R[X]
s : Finset S
h : Set.Pairwise {i : S | i ∈ s ∧ f i ≠ 0} (Ne on natDegree ∘ f)
H : ∀ (x : S) (_ : x ∈ s), f x = 0
neg : ∀ s_1 ∈ s, (f s_1).natDegree = ⊥
⊢ (s.sum f).natDegree = s.sup fun (i : S) ↦ (f i).natDegree

Tactic:
rw [Finset.sum_eq_zero H, natDegree_zero, eq_comm, show 0 = ⊥ from rfl, Finset.sup_eq_bot_iff]

Premises used: Finset.sum_eq_zero, Polynomial.natDegree_zero, eq_comm, Finset.sup_eq_bot_iff, rfl
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
S : Type v
inst : Semiring R
f : S → R[X]
s : Finset S
h : Set.Pairwise {i : S | i ∈ s ∧ f i ≠ 0} (Ne on natDegree ∘ f)
H : ∀ (x : S) (_ : x ∈ s), f x = 0
x : S
hx : x ∈ s
⊢ (f x).natDegree = ⊥

Tactic:
simp [H x hx]
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
p : R[X]
hp : p ≠ 0
f : R →+* S
z : S
hz : eval₂ f z p = 0
inj : ∀ (x : R), Eq.{v + 1} (α := S) ((f : (a : R) → S) x : S) (0 : S) → x = 0
hlt : p.natDegree ≤ 0
⊢ p = (C : (a : R) → R[X]) (p.coeff 0)

Tactic:
have A : p = C (p.coeff 0) := eq_C_of_natDegree_le_zero hlt
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
p : R[X]
hp : p ≠ 0
f : R →+* S
z : S
hz : eval₂ f z p = 0
inj : ∀ (x : R), Eq.{v + 1} (α := S) ((f : (a : R) → S) x : S) (0 : S) → x = 0
hlt : p.natDegree ≤ 0
A : p = (C : (a : R) → R[X]) (p.coeff 0)
⊢ Eq.{v + 1} (α := S) ((f : (a : R) → S) (p.coeff 0) : S) (0 : S)

Tactic:
rw [A, eval₂_C] at hz

Premises used: Polynomial.eval₂_C
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
p : R[X]
hp : p ≠ 0
f : R →+* S
z : S
hz : eval₂ f z p = 0
inj : ∀ (x : R), Eq.{v + 1} (α := S) ((f : (a : R) → S) x : S) (0 : S) → x = 0
hlt : p.natDegree ≤ 0
A : p = (C : (a : R) → R[X]) (p.coeff 0)
hz₁ : Eq.{v + 1} (α := S) ((f : (a : R) → S) (p.coeff 0) : S) (0 : S)
⊢ ∀ (x : R), Eq.{v + 1} (α := S) ((f : (a : R) → S) x : S) (0 : S) → x = 0

Tactic:
rw [A, eval₂_C] at hz

Premises used: Polynomial.eval₂_C
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
p : R[X]
hp : p ≠ 0
f : R →+* S
z : S
hz : eval₂ f z p = 0
inj : ∀ (x : R), Eq.{v + 1} (α := S) ((f : (a : R) → S) x : S) (0 : S) → x = 0
hlt : p.natDegree ≤ 0
A : p = (C : (a : R) → R[X]) (p.coeff 0)
hz₁ : Eq.{v + 1} (α := S) ((f : (a : R) → S) (p.coeff 0) : S) (0 : S)
inj₁ : ∀ (x : R), Eq.{v + 1} (α := S) ((f : (a : R) → S) x : S) (0 : S) → x = 0
⊢ p.natDegree ≤ 0

Tactic:
rw [A, eval₂_C] at hz

Premises used: Polynomial.eval₂_C
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
p : R[X]
hp : p ≠ 0
f : R →+* S
z : S
hz : eval₂ f z p = 0
inj : ∀ (x : R), Eq.{v + 1} (α := S) ((f : (a : R) → S) x : S) (0 : S) → x = 0
hlt : p.natDegree ≤ 0
A : p = (C : (a : R) → R[X]) (p.coeff 0)
hz₁ : Eq.{v + 1} (α := S) ((f : (a : R) → S) (p.coeff 0) : S) (0 : S)
inj₁ : ∀ (x : R), Eq.{v + 1} (α := S) ((f : (a : R) → S) x : S) (0 : S) → x = 0
hlt₁ : p.natDegree ≤ 0
⊢ p = (C : (a : R) → R[X]) (p.coeff 0)

Tactic:
rw [A, eval₂_C] at hz

Premises used: Polynomial.eval₂_C
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
p : R[X]
hp : p ≠ 0
f : R →+* S
z : S
hz : Eq.{v + 1} (α := S) ((f : (a : R) → S) (p.coeff 0) : S) (0 : S)
inj : ∀ (x : R), Eq.{v + 1} (α := S) ((f : (a : R) → S) x : S) (0 : S) → x = 0
hlt : p.natDegree ≤ 0
A : p = (C : (a : R) → R[X]) (p.coeff 0)
⊢ p = 0

Tactic:
simp only [inj (p.coeff 0) hz, map_zero] at A

Premises used: map_zero, Polynomial.coeff, OfNat.ofNat
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
p : R[X]
hp : p ≠ 0
f : R →+* S
z : S
hz : Eq.{v + 1} (α := S) ((f : (a : R) → S) (p.coeff 0) : S) (0 : S)
inj : ∀ (x : R), Eq.{v + 1} (α := S) ((f : (a : R) → S) x : S) (0 : S) → x = 0
hlt : p.natDegree ≤ 0
A : p = 0
⊢ False

Tactic:
hp A
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
p : R[X]
hp : p ≠ 0
f : R →+* S
z : S
hz : Eq.{v + 1} (α := S) ((f : (a : R) → S) (p.coeff 0) : S) (0 : S)
inj : ∀ (x : R), Eq.{v + 1} (α := S) ((f : (a : R) → S) x : S) (0 : S) → x = 0
hlt : p.natDegree ≤ 0
A : p = 0
⊢ False

Tactic:
exact hp A
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
p : R[X]
hp : p ≠ 0
f : R →+* S
z : S
hz : eval₂ f z p = 0
inj : ∀ (x : R), Eq.{v + 1} (α := S) ((f : (a : R) → S) x : S) (0 : S) → x = 0
⊢ 0 < p.degree

Tactic:
natDegree_pos_iff_degree_pos.mp (natDegree_pos_of_eval₂_root hp f hz inj)

Premises used: Polynomial.natDegree_pos_of_eval₂_root, Iff.mp, Polynomial.natDegree_pos_iff_degree_pos
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
pos : ∀ (h : p = 0), (↑n : WithBot ℕ) < p.degree ↔ n < p.natDegree
neg : ∀ (h : ¬p = 0), (↑n : WithBot ℕ) < p.degree ↔ n < p.natDegree
⊢ (↑n : WithBot ℕ) < p.degree ↔ n < p.natDegree

Tactic:
by_cases h : p = 0
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
h : p = 0
⊢ (↑n : WithBot ℕ) < p.degree ↔ n < p.natDegree

Tactic:
simp [h]
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
h : ¬p = 0
⊢ (↑n : WithBot ℕ) < p.degree ↔ n < p.natDegree

Tactic:
simp [degree_eq_natDegree h, Nat.cast_lt]

Premises used: Polynomial.degree_eq_natDegree, Nat.cast_lt
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
p : R[X]
inl :
  ∀ (h : p = 0),
    (map f p).degree = p.degree ↔ Ne.{v + 1} (α := S) ((f : (a : R) → S) p.leadingCoeff : S) (0 : S) ∨ p = 0
inr :
  ∀ (h : p ≠ 0),
    (map f p).degree = p.degree ↔ Ne.{v + 1} (α := S) ((f : (a : R) → S) p.leadingCoeff : S) (0 : S) ∨ p = 0
⊢ (map f p).degree = p.degree ↔ Ne.{v + 1} (α := S) ((f : (a : R) → S) p.leadingCoeff : S) (0 : S) ∨ p = 0

Tactic:
rcases eq_or_ne p 0 with h | h

Premises used: eq_or_ne, OfNat.ofNat
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
p : R[X]
h : p = 0
⊢ (map f p).degree = p.degree ↔ Ne.{v + 1} (α := S) ((f : (a : R) → S) p.leadingCoeff : S) (0 : S) ∨ p = 0

Tactic:
simp [h]
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
p : R[X]
h : p ≠ 0
inr : (map f p).degree = p.degree ↔ Ne.{v + 1} (α := S) ((f : (a : R) → S) p.leadingCoeff : S) (0 : S)
⊢ (map f p).degree = p.degree ↔ Ne.{v + 1} (α := S) ((f : (a : R) → S) p.leadingCoeff : S) (0 : S) ∨ p = 0

Tactic:
simp only [h, or_false]

Premises used: or_false
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
p : R[X]
h : p ≠ 0
⊢ (map f p).degree = p.degree ↔ Ne.{v + 1} (α := S) ((f : (a : R) → S) p.leadingCoeff : S) (0 : S)

Tactic:
⟨fun h2 ↦ ?_, degree_map_eq_of_leadingCoeff_ne_zero f⟩

Premises used: Polynomial.degree_map_eq_of_leadingCoeff_ne_zero, Iff.intro
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
p : R[X]
h : p ≠ 0
inr : ∀ (h2 : (map f p).degree = p.degree), Ne.{v + 1} (α := S) ((f : (a : R) → S) p.leadingCoeff : S) (0 : S)
⊢ (map f p).degree = p.degree ↔ Ne.{v + 1} (α := S) ((f : (a : R) → S) p.leadingCoeff : S) (0 : S)

Tactic:
refine ⟨fun h2 ↦ ?_, degree_map_eq_of_leadingCoeff_ne_zero f⟩
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
p : R[X]
h : p ≠ 0
h2 : (map f p).degree = p.degree
⊢ (map f p).natDegree = p.natDegree

Tactic:
have h3 : natDegree (map f p) = natDegree p := by simp_rw [natDegree, h2]
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
p : R[X]
h : p ≠ 0
h2 : (map f p).degree = p.degree
h3 : (map f p).natDegree = p.natDegree
rwa : ¬map f p = 0
rwa₁ : ¬(map f p).degree = ⊥
rwa₂ : ¬p.degree = ⊥
rwa₃ rwa₄ rwa₅ rwa₆ : ¬p = 0
⊢ map f p ≠ 0

Tactic:
rwa [ne_eq, ← degree_eq_bot, h2, degree_eq_bot]

Premises used: ne_eq, Polynomial.degree_eq_bot
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
p : R[X]
h : p ≠ 0
h2 : (map f p).degree = p.degree
h3 : (map f p).natDegree = p.natDegree
⊢ map f p ≠ 0

Tactic:
have h4 : map f p ≠ 0 := by
    rwa [ne_eq, ← degree_eq_bot, h2, degree_eq_bot]
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
p : R[X]
h : p ≠ 0
h2 : (map f p).degree = p.degree
h3 : (map f p).natDegree = p.natDegree
h4 : map f p ≠ 0
inr : Ne.{v + 1} (α := S) ((f : (a : R) → S) (p.coeff p.natDegree) : S) (0 : S)
inr₁ : (map f p).coeff p.natDegree ≠ 0
inr₂ : (map f p).coeff (map f p).natDegree ≠ 0
inr₃ : (map f p).leadingCoeff ≠ 0
inr₄ : ¬(map f p).leadingCoeff = 0
inr₅ inr₆ inr₇ inr₈ : ¬map f p = 0
⊢ Ne.{v + 1} (α := S) ((f : (a : R) → S) p.leadingCoeff : S) (0 : S)

Tactic:
rwa [← coeff_natDegree, ← coeff_map, ← h3, coeff_natDegree, ne_eq, leadingCoeff_eq_zero]

Premises used: Polynomial.coeff_map, Polynomial.coeff_natDegree, ne_eq, Polynomial.leadingCoeff_eq_zero
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
p : R[X]
inl :
  ∀ (h : p.natDegree = 0),
    (map f p).natDegree = p.natDegree ↔
      Ne.{v + 1} (α := S) ((f : (a : R) → S) p.leadingCoeff : S) (0 : S) ∨ p.natDegree = 0
inr :
  ∀ (h : p.natDegree ≠ 0),
    (map f p).natDegree = p.natDegree ↔
      Ne.{v + 1} (α := S) ((f : (a : R) → S) p.leadingCoeff : S) (0 : S) ∨ p.natDegree = 0
⊢ (map f p).natDegree = p.natDegree ↔
    Ne.{v + 1} (α := S) ((f : (a : R) → S) p.leadingCoeff : S) (0 : S) ∨ p.natDegree = 0

Tactic:
rcases eq_or_ne (natDegree p) 0 with h | h

Premises used: eq_or_ne, Polynomial.natDegree, OfNat.ofNat
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
p : R[X]
h : p.natDegree = 0
inl : (map f p).natDegree = 0 ↔ Ne.{v + 1} (α := S) ((f : (a : R) → S) p.leadingCoeff : S) (0 : S) ∨ True
inl₁ : (map f p).natDegree = 0 ↔ ¬Eq.{v + 1} (α := S) ((f : (a : R) → S) p.leadingCoeff : S) (0 : S) ∨ True
inl₂ : (map f p).natDegree = 0 ↔ True
inl₃ : (map f p).natDegree = 0
inl₄ : (map f p).natDegree ≤ 0
inl₅ : (map f p).natDegree ≤ p.natDegree
⊢ (map f p).natDegree = p.natDegree ↔
    Ne.{v + 1} (α := S) ((f : (a : R) → S) p.leadingCoeff : S) (0 : S) ∨ p.natDegree = 0

Tactic:
simp_rw [h, ne_eq, or_true, iff_true, ← Nat.le_zero, ← h, natDegree_map_le]

Premises used: iff_true, Nat.le_zero, ne_eq, Polynomial.natDegree_map_le, or_true
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
p : R[X]
h : p.natDegree ≠ 0
⊢ (map f p).natDegree = p.natDegree ↔
    Ne.{v + 1} (α := S) ((f : (a : R) → S) p.leadingCoeff : S) (0 : S) ∨ p.natDegree = 0

Tactic:
simp_all [natDegree, WithBot.unbotD_eq_unbotD_iff]

Premises used: Polynomial.natDegree, WithBot.unbotD_eq_unbotD_iff
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
S : Type v
inst : Semiring R
p : R[X]
inst_1 : Semiring S
inst_2 : Nontrivial S
f : R →+* S
hp : IsUnit p.leadingCoeff
⊢ (map f p).degree = p.degree

Tactic:
degree_map_eq_of_leadingCoeff_ne_zero _ <| f.isUnit_map hp |>.ne_zero

Premises used: Polynomial.degree_map_eq_of_leadingCoeff_ne_zero, IsUnit.ne_zero, RingHom.isUnit_map
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
S : Type v
inst : Semiring R
p : R[X]
inst_1 : Semiring S
inst_2 : Nontrivial S
f : R →+* S
hp : IsUnit p.leadingCoeff
⊢ (map f p).natDegree = p.natDegree

Tactic:
natDegree_eq_natDegree <| degree_map_eq_of_isUnit_leadingCoeff _ hp

Premises used: Polynomial.degree_map_eq_of_isUnit_leadingCoeff, Polynomial.natDegree_eq_natDegree
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
S : Type v
inst : Semiring R
p : R[X]
inst_1 : Semiring S
inst_2 : Nontrivial S
f : R →+* S
hp : IsUnit p.leadingCoeff
⊢ (map f p).leadingCoeff = (f : (a : R) → S) p.leadingCoeff

Tactic:
leadingCoeff_map_of_leadingCoeff_ne_zero _ <| f.isUnit_map hp |>.ne_zero

Premises used: Polynomial.leadingCoeff_map_of_leadingCoeff_ne_zero, IsUnit.ne_zero, RingHom.isUnit_map
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
S : Type v
inst : Semiring R
p : R[X]
inst_1 : Semiring S
inst_2 : Nontrivial S
f : R →+* S
hp : IsUnit p.leadingCoeff
⊢ (map f p).nextCoeff = (f : (a : R) → S) p.nextCoeff

Tactic:
nextCoeff_map_of_leadingCoeff_ne_zero _ <| f.isUnit_map hp |>.ne_zero

Premises used: Polynomial.nextCoeff_map_of_leadingCoeff_ne_zero, IsUnit.ne_zero, RingHom.isUnit_map
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
hf : Function.Injective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
p : R[X]
⊢ (map f p).degree = p.degree

Tactic:
simp [hf, map_ne_zero_iff, ne_or_eq]

Premises used: ne_or_eq, map_ne_zero_iff