awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.Eval.Degree
Goal:
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst : Semiring R
p_1 q r : R[X]
inst_1 : Semiring S
f : R →+* S
p : R[X]
e : R ≃+* S
a₁ :
  ∀ (x : R[X]) (n : ℕ),
    Eq.{u + 1} (α := R)
      (coeff
        ((RingHom.comp (β := S[X]) (mapRingHom (↑e.symm : S →+* R)) (mapRingHom (↑e : R →+* S)) : (a : R[X]) → R[X]) x)
        n)
      (coeff ((RingHom.id R[X] : (a : R[X]) → R[X]) x) n)
⊢ Eq (α := R[X] →+* R[X]) (RingHom.comp (β := S[X]) (mapRingHom (↑e.symm : S →+* R)) (mapRingHom (↑e : R →+* S)))
    (RingHom.id R[X])

Tactic:
ext
-- Module: Mathlib.Algebra.Polynomial.Eval.Degree
Goal:
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst : Semiring R
p_1 q r : R[X]
inst_1 : Semiring S
f : R →+* S
p : R[X]
e : R ≃+* S
x : R[X]
n_1 : ℕ
⊢ Eq.{u + 1} (α := R)
    (coeff
      ((RingHom.comp (β := S[X]) (mapRingHom (↑e.symm : S →+* R)) (mapRingHom (↑e : R →+* S)) : (a : R[X]) → R[X]) x)
      n_1)
    (coeff ((RingHom.id R[X] : (a : R[X]) → R[X]) x) n_1)

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Eval.Degree
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
p : R[X]
hp : p.Monic
hfp : map f p = 0
x : R
⊢ (f : (a : R) → S) x = HMul.hMul (α := S) (β := S) ((f : (a : R) → S) x : S) ((f : (a : R) → S) p.leadingCoeff : S)

Tactic:
simp only [mul_one, hp.leadingCoeff, f.map_one]

Premises used: RingHom.map_one, Polynomial.Monic.leadingCoeff, mul_one
-- Module: Mathlib.Algebra.Polynomial.Eval.Degree
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
p : R[X]
hp : p.Monic
hfp : map f p = 0
x : R
⊢ HMul.hMul (α := S) ((f : (a : R) → S) x : S) ((map f p).coeff p.natDegree) = 0

Tactic:
simp only [hfp, mul_zero, coeff_zero]

Premises used: MulZeroClass.mul_zero, Polynomial.coeff_zero
-- Module: Mathlib.Algebra.Polynomial.Eval.Degree
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
p : R[X]
hp : p.Monic
h : ∀ (x : R), Eq.{v + 1} (α := S) ((f : (a : R) → S) x : S) (0 : S)
n : ℕ
⊢ (map f p).coeff n = coeff 0 n

Tactic:
simp only [h, coeff_map, coeff_zero]

Premises used: Polynomial.coeff_map, Polynomial.coeff_zero
-- Module: Mathlib.Algebra.Polynomial.Eval.Degree
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
p : R[X]
hp : p.Monic
inst_2 : Nontrivial S
⊢ map f p ≠ 0

Tactic:
fun h =>
  f.map_one_ne_zero ((map_monic_eq_zero_iff hp).mp h _)

Premises used: RingHom.map_one_ne_zero, Iff.mp, Polynomial.map_monic_eq_zero_iff, OfNat.ofNat, Not
-- Module: Mathlib.Algebra.Polynomial.Eval.Degree
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
p : R[X]
⊢ (map f p).degree ≤ p.degree

Tactic:
(degree_le_iff_coeff_zero _ _).2 fun m hm => ?_

Premises used: Iff.mpr, Polynomial.degree_le_iff_coeff_zero
-- Module: Mathlib.Algebra.Polynomial.Eval.Degree
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
p : R[X]
refine : ∀ (m : ℕ) (hm : p.degree < (↑m : WithBot ℕ)), (map f p).coeff m = 0
⊢ (map f p).degree ≤ p.degree

Tactic:
refine (degree_le_iff_coeff_zero _ _).2 fun m hm => ?_

Premises used: Iff.mpr, Polynomial.degree_le_iff_coeff_zero
-- Module: Mathlib.Algebra.Polynomial.Eval.Degree
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
p : R[X]
m : ℕ
hm : p.degree < (↑m : WithBot ℕ)
⊢ ∀ (m_1 : ℕ), m ≤ m_1 → p.coeff m_1 = 0

Tactic:
rw [degree_lt_iff_coeff_zero] at hm

Premises used: Polynomial.degree_lt_iff_coeff_zero
-- Module: Mathlib.Algebra.Polynomial.Eval.Degree
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
p : R[X]
m : ℕ
hm : ∀ (m_1 : ℕ), m ≤ m_1 → p.coeff m_1 = 0
⊢ (map f p).coeff m = 0

Tactic:
simp [hm m le_rfl]

Premises used: le_rfl
-- Module: Mathlib.Algebra.Polynomial.Eval.Degree
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
p : R[X]
⊢ (map f p).natDegree ≤ p.natDegree

Tactic:
natDegree_le_natDegree degree_map_le

Premises used: Polynomial.degree_map_le, Polynomial.natDegree_le_natDegree
-- Module: Mathlib.Algebra.Polynomial.Eval.Degree
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
p : R[X]
hp : Eq.{v + 1} (α := S) ((f : (a : R) → S) p.leadingCoeff : S) (0 : S)
hp₀ : p ≠ 0
⊢ (map f p).degree < p.degree

Tactic:
degree_map_le.lt_of_ne fun hpq ↦ hp₀ ?_

Premises used: Polynomial.degree_map_le, LE.le.lt_of_ne
-- Module: Mathlib.Algebra.Polynomial.Eval.Degree
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
p : R[X]
hp : Eq.{v + 1} (α := S) ((f : (a : R) → S) p.leadingCoeff : S) (0 : S)
hp₀ : p ≠ 0
refine : ∀ (hpq : (map f p).degree = p.degree), p = 0
⊢ (map f p).degree < p.degree

Tactic:
refine degree_map_le.lt_of_ne fun hpq ↦ hp₀ ?_

Premises used: Polynomial.degree_map_le, LE.le.lt_of_ne
-- Module: Mathlib.Algebra.Polynomial.Eval.Degree
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
p : R[X]
hp : Eq.{v + 1} (α := S) ((f : (a : R) → S) p.leadingCoeff : S) (0 : S)
hp₀ : p ≠ 0
hpq : (map f p).degree = p.degree
⊢ map f p = 0

Tactic:
rw [leadingCoeff, ← coeff_map, ← natDegree_eq_natDegree hpq, ← leadingCoeff, leadingCoeff_eq_zero]
    at hp

Premises used: Polynomial.coeff_map, Polynomial.leadingCoeff, Polynomial.natDegree_eq_natDegree, Polynomial.leadingCoeff_eq_zero
-- Module: Mathlib.Algebra.Polynomial.Eval.Degree
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
p : R[X]
hp : Eq.{v + 1} (α := S) ((f : (a : R) → S) p.leadingCoeff : S) (0 : S)
hp₀ : p ≠ 0
hpq : (map f p).degree = p.degree
hp₁ : map f p = 0
⊢ p ≠ 0

Tactic:
rw [leadingCoeff, ← coeff_map, ← natDegree_eq_natDegree hpq, ← leadingCoeff, leadingCoeff_eq_zero]
    at hp

Premises used: Polynomial.coeff_map, Polynomial.leadingCoeff, Polynomial.natDegree_eq_natDegree, Polynomial.leadingCoeff_eq_zero
-- Module: Mathlib.Algebra.Polynomial.Eval.Degree
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
p : R[X]
hp : Eq.{v + 1} (α := S) ((f : (a : R) → S) p.leadingCoeff : S) (0 : S)
hp₀ : p ≠ 0
hpq : (map f p).degree = p.degree
hp₁ : map f p = 0
hp₂ : p ≠ 0
⊢ (map f p).degree = p.degree

Tactic:
rw [leadingCoeff, ← coeff_map, ← natDegree_eq_natDegree hpq, ← leadingCoeff, leadingCoeff_eq_zero]
    at hp

Premises used: Polynomial.coeff_map, Polynomial.leadingCoeff, Polynomial.natDegree_eq_natDegree, Polynomial.leadingCoeff_eq_zero
-- Module: Mathlib.Algebra.Polynomial.Eval.Degree
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
p : R[X]
hp : map f p = 0
hp₀ : p ≠ 0
hpq : (map f p).degree = p.degree
rw : p.degree = ⊥
rw₁ : (map f p).degree = ⊥
rw₂ : degree.{v} (R := S) 0 = ⊥
rw₃ rw₄ : Eq (α := WithBot ℕ) ⊥ ⊥
⊢ p = 0

Tactic:
rw [← degree_eq_bot, ← hpq, hp, degree_zero]

Premises used: Polynomial.degree_zero, Polynomial.degree_eq_bot
-- Module: Mathlib.Algebra.Polynomial.Eval.Degree
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
hp : Eq.{v + 1} (α := S) ((f : (a : R) → S) (leadingCoeff 0) : S) (0 : S)
hp₀ : map f 0 ≠ 0
⊢ False

Tactic:
simp at hp₀
-- Module: Mathlib.Algebra.Polynomial.Eval.Degree
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
p : R[X]
hp : Eq.{v + 1} (α := S) ((f : (a : R) → S) p.leadingCoeff : S) (0 : S)
hp₀ : 0 < p.natDegree
pos : ∀ (H : map f p = 0), (map f p).natDegree < p.natDegree
neg : ∀ (H : ¬map f p = 0), (map f p).natDegree < p.natDegree
⊢ (map f p).natDegree < p.natDegree

Tactic:
by_cases H : map f p = 0

Premises used: Polynomial.map
-- Module: Mathlib.Algebra.Polynomial.Eval.Degree
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
p : R[X]
hp : Eq.{v + 1} (α := S) ((f : (a : R) → S) p.leadingCoeff : S) (0 : S)
hp₀ : 0 < p.natDegree
H : map f p = 0
pos : natDegree.{v} (R := S) 0 < p.natDegree
pos₁ pos₂ pos₃ pos₄ : 0 < p.natDegree
⊢ (map f p).natDegree < p.natDegree

Tactic:
rwa [H, natDegree_zero]

Premises used: Polynomial.natDegree_zero
-- Module: Mathlib.Algebra.Polynomial.Eval.Degree
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
p : R[X]
hp : Eq.{v + 1} (α := S) ((f : (a : R) → S) p.leadingCoeff : S) (0 : S)
hp₀ : 0 < p.natDegree
H : ¬map f p = 0
⊢ (map f p).natDegree < p.natDegree

Tactic:
natDegree_map_lt hp H

Premises used: Polynomial.natDegree_map_lt
-- Module: Mathlib.Algebra.Polynomial.Eval.Degree
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
p : R[X]
hp : Eq.{v + 1} (α := S) ((f : (a : R) → S) p.leadingCoeff : S) (0 : S)
hp₀ : 0 < p.natDegree
H : ¬map f p = 0
⊢ (map f p).natDegree < p.natDegree

Tactic:
exact natDegree_map_lt hp H

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

Tactic:
degree_map_le.antisymm ?_

Premises used: Polynomial.degree_map_le, LE.le.antisymm
-- Module: Mathlib.Algebra.Polynomial.Eval.Degree
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
p : R[X]
f : R →+* S
hf : Ne.{v + 1} (α := S) ((f : (a : R) → S) p.leadingCoeff : S) (0 : S)
refine : p.degree ≤ (map f p).degree
⊢ (map f p).degree = p.degree

Tactic:
refine degree_map_le.antisymm ?_

Premises used: Polynomial.degree_map_le, LE.le.antisymm
-- Module: Mathlib.Algebra.Polynomial.Eval.Degree
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
p : R[X]
f : R →+* S
hf : Ne.{v + 1} (α := S) ((f : (a : R) → S) p.leadingCoeff : S) (0 : S)
⊢ p ≠ 0

Tactic:
have hp0 : p ≠ 0 :=
    leadingCoeff_ne_zero.mp fun hp0 => hf (_root_.trans (congr_arg _ hp0) f.map_zero)
-- Module: Mathlib.Algebra.Polynomial.Eval.Degree
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
p : R[X]
f : R →+* S
hf : Ne.{v + 1} (α := S) ((f : (a : R) → S) p.leadingCoeff : S) (0 : S)
hp0 : p ≠ 0
rw : (↑p.natDegree : WithBot ℕ) ≤ (map f p).degree
⊢ p.degree ≤ (map f p).degree

Tactic:
rw [degree_eq_natDegree hp0]

Premises used: Polynomial.degree_eq_natDegree
-- Module: Mathlib.Algebra.Polynomial.Eval.Degree
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
p : R[X]
f : R →+* S
hf : Ne.{v + 1} (α := S) ((f : (a : R) → S) p.leadingCoeff : S) (0 : S)
hp0 : p ≠ 0
⊢ (↑p.natDegree : WithBot ℕ) ≤ (map f p).degree

Tactic:
le_degree_of_ne_zero ?_

Premises used: Polynomial.le_degree_of_ne_zero
-- Module: Mathlib.Algebra.Polynomial.Eval.Degree
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
p : R[X]
f : R →+* S
hf : Ne.{v + 1} (α := S) ((f : (a : R) → S) p.leadingCoeff : S) (0 : S)
hp0 : p ≠ 0
refine : (map f p).coeff p.natDegree ≠ 0
⊢ (↑p.natDegree : WithBot ℕ) ≤ (map f p).degree

Tactic:
refine le_degree_of_ne_zero ?_

Premises used: Polynomial.le_degree_of_ne_zero
-- Module: Mathlib.Algebra.Polynomial.Eval.Degree
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
p : R[X]
f : R →+* S
hf : Ne.{v + 1} (α := S) ((f : (a : R) → S) p.leadingCoeff : S) (0 : S)
hp0 : p ≠ 0
rw : Ne.{v + 1} (α := S) ((f : (a : R) → S) (p.coeff p.natDegree) : S) (0 : S)
⊢ (map f p).coeff p.natDegree ≠ 0

Tactic:
rw [coeff_map]

Premises used: Polynomial.coeff_map
-- Module: Mathlib.Algebra.Polynomial.Eval.Degree
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
p : R[X]
f : R →+* S
hf : Ne.{v + 1} (α := S) ((f : (a : R) → S) p.leadingCoeff : S) (0 : S)
hp0 : p ≠ 0
⊢ Ne.{v + 1} (α := S) ((f : (a : R) → S) (p.coeff p.natDegree) : S) (0 : S)

Tactic:
hf

Premises used: Polynomial.leadingCoeff
-- Module: Mathlib.Algebra.Polynomial.Eval.Degree
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
p : R[X]
f : R →+* S
hf : Ne.{v + 1} (α := S) ((f : (a : R) → S) p.leadingCoeff : S) (0 : S)
hp0 : p ≠ 0
⊢ Ne.{v + 1} (α := S) ((f : (a : R) → S) (p.coeff p.natDegree) : S) (0 : S)

Tactic:
exact hf
-- Module: Mathlib.Algebra.Polynomial.Eval.Degree
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
p : R[X]
f : R →+* S
hf : Ne.{v + 1} (α := S) ((f : (a : R) → S) p.leadingCoeff : S) (0 : S)
⊢ (map f p).natDegree = p.natDegree

Tactic:
natDegree_eq_of_degree_eq (degree_map_eq_of_leadingCoeff_ne_zero f hf)

Premises used: Polynomial.degree_map_eq_of_leadingCoeff_ne_zero, Polynomial.natDegree_eq_of_degree_eq
-- Module: Mathlib.Algebra.Polynomial.Eval.Degree
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
p : R[X]
f : R →+* S
hf : Ne.{v + 1} (α := S) ((f : (a : R) → S) p.leadingCoeff : S) (0 : S)
unfold : (map f p).coeff (map f p).natDegree = (f : (a : R) → S) (p.coeff p.natDegree)
⊢ (map f p).leadingCoeff = (f : (a : R) → S) p.leadingCoeff

Tactic:
unfold leadingCoeff

Premises used: Polynomial.leadingCoeff
-- Module: Mathlib.Algebra.Polynomial.Eval.Degree
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
p : R[X]
f : R →+* S
hf : Ne.{v + 1} (α := S) ((f : (a : R) → S) p.leadingCoeff : S) (0 : S)
rw :
  Eq.{v + 1} (α := S) ((f : (a : R) → S) (p.coeff (map f p).natDegree) : S)
    ((f : (a : R) → S) (p.coeff p.natDegree) : S)
rw₁ rw₂ :
  Eq.{v + 1} (α := S) ((f : (a : R) → S) (p.coeff p.natDegree) : S) ((f : (a : R) → S) (p.coeff p.natDegree) : S)
⊢ (map f p).coeff (map f p).natDegree = (f : (a : R) → S) (p.coeff p.natDegree)

Tactic:
rw [coeff_map, natDegree_map_of_leadingCoeff_ne_zero f hf]

Premises used: Polynomial.coeff_map, Polynomial.natDegree_map_of_leadingCoeff_ne_zero
-- Module: Mathlib.Algebra.Polynomial.Eval.Degree
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
p : R[X]
f : R →+* S
hf : Ne.{v + 1} (α := S) ((f : (a : R) → S) p.leadingCoeff : S) (0 : S)
⊢ (map f p).nextCoeff = (f : (a : R) → S) p.nextCoeff

Tactic:
grind [nextCoeff, natDegree_map_of_leadingCoeff_ne_zero, coeff_map]

Premises used: Polynomial.coeff_map, Polynomial.nextCoeff, Polynomial.natDegree_map_of_leadingCoeff_ne_zero
-- Module: Mathlib.Algebra.Polynomial.Eval.Degree
Goal:
R : Type u
S : Type v
inst : Semiring R
p q : R[X]
inst_1 : CommSemiring S
f : R →+* S
x : S
rw :
  eval₂ f x (eval₂ C q (∑ i ∈ range (p.natDegree + 1), (monomial i : (a : R) → R[X]) (p.coeff i))) =
    eval₂ f (eval₂ f x q) (∑ i ∈ range (p.natDegree + 1), (monomial i : (a : R) → R[X]) (p.coeff i))
⊢ eval₂ f x (p.comp q) = eval₂ f (eval₂ f x q) p

Tactic:
rw [comp, p.as_sum_range]

Premises used: Polynomial.as_sum_range, Polynomial.comp
-- Module: Mathlib.Algebra.Polynomial.Eval.Degree
Goal:
R : Type u
S : Type v
inst : Semiring R
p q : R[X]
inst_1 : CommSemiring S
f : R →+* S
x : S
⊢ eval₂ f x (eval₂ C q (∑ i ∈ range (p.natDegree + 1), (monomial i : (a : R) → R[X]) (p.coeff i))) =
    eval₂ f (eval₂ f x q) (∑ i ∈ range (p.natDegree + 1), (monomial i : (a : R) → R[X]) (p.coeff i))

Tactic:
simp [eval₂_finsetSum, eval₂_pow]

Premises used: Polynomial.eval₂_pow, Polynomial.eval₂_finsetSum
-- Module: Mathlib.Algebra.Polynomial.Eval.Degree
Goal:
R : Type u
S : Type v
inst : Semiring R
p q : R[X]
inst_1 : CommSemiring S
f : R →+* S
t : S
⊢ eval₂ f t (p.comp^[0] q) = (fun (x : S) ↦ eval₂ f x p)^[0] (eval₂ f t q)

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Eval.Degree
Goal:
R : Type u
S : Type v
inst : Semiring R
p q : R[X]
inst_1 : CommSemiring S
f : R →+* S
t : S
k : ℕ
IH : eval₂ f t (p.comp^[k] q) = (fun (x : S) ↦ eval₂ f x p)^[k] (eval₂ f t q)
succ : eval₂ f t (p.comp (p.comp^[k] q)) = (fun (x : S) ↦ eval₂ f x p)^[k + 1] (eval₂ f t q)
succ₁ : eval₂ f t (p.comp (p.comp^[k] q)) = eval₂ f ((fun (x : S) ↦ eval₂ f x p)^[k] (eval₂ f t q)) p
succ₂ : eval₂ f (eval₂ f t (p.comp^[k] q)) p = eval₂ f ((fun (x : S) ↦ eval₂ f x p)^[k] (eval₂ f t q)) p
succ₃ succ₄ :
  eval₂ f ((fun (x : S) ↦ eval₂ f x p)^[k] (eval₂ f t q)) p = eval₂ f ((fun (x : S) ↦ eval₂ f x p)^[k] (eval₂ f t q)) p
⊢ eval₂ f t (p.comp^[k + 1] q) = (fun (x : S) ↦ eval₂ f x p)^[k + 1] (eval₂ f t q)

Tactic:
rw [Function.iterate_succ_apply', Function.iterate_succ_apply', eval₂_comp, IH]

Premises used: Function.iterate_succ_apply', Polynomial.eval₂_comp
-- Module: Mathlib.Algebra.Polynomial.Eval.Degree
Goal:
R : Type u
S : Type v
inst : Semiring R
p q : R[X]
inst_1 : CommSemiring S
f : R →+* S
k : ℕ
t : S
zero : eval₂ f t (p.comp^[0] q) = (fun (x : S) ↦ eval₂ f x p)^[0] (eval₂ f t q)
succ :
  ∀ (k : ℕ) (IH : eval₂ f t (p.comp^[k] q) = (fun (x : S) ↦ eval₂ f x p)^[k] (eval₂ f t q)),
    eval₂ f t (p.comp^[k + 1] q) = (fun (x : S) ↦ eval₂ f x p)^[k + 1] (eval₂ f t q)
⊢ eval₂ f t (p.comp^[k] q) = (fun (x : S) ↦ eval₂ f x p)^[k] (eval₂ f t q)

Tactic:
induction k with
  | zero => simp
  | succ k IH => rw [Function.iterate_succ_apply', Function.iterate_succ_apply', eval₂_comp, IH]

Premises used: Function.iterate_succ_apply', AddMonoidAlgebra.zero, Polynomial.eval₂_comp
-- Module: Mathlib.Algebra.Polynomial.Eval.Degree
Goal:
R : Type u
inst : CommSemiring R
p q : R[X]
⊢ ∀ (k : ℕ) (t : R), eval t (p.comp^[k] q) = (fun (x : R) ↦ eval x p)^[k] (eval t q)

Tactic:
iterate_comp_eval₂ _

Premises used: Polynomial.eval, Polynomial.iterate_comp_eval₂
-- Module: Mathlib.Algebra.Polynomial.Eval.Degree
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : CommRing S
inst_2 : IsDomain S
φ : R →+* S
f : R[X]
hf : IsUnit f.leadingCoeff
H : IsUnit (map φ f)
⊢ (map φ f).degree = 0

Tactic:
have dz := degree_eq_zero_of_isUnit H
-- Module: Mathlib.Algebra.Polynomial.Eval.Degree
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : CommRing S
inst_2 : IsDomain S
φ : R →+* S
f : R[X]
hf : IsUnit f.leadingCoeff
H : IsUnit (map φ f)
dz : (map φ f).degree = 0
rw : ∀ (dz : f.degree = 0), IsUnit f
hf₁ : Ne.{v + 1} (α := S) ((φ : (a : R) → S) f.leadingCoeff : S) (0 : S)
⊢ IsUnit f

Tactic:
rw [degree_map_eq_of_leadingCoeff_ne_zero] at dz

Premises used: Polynomial.degree_map_eq_of_leadingCoeff_ne_zero
-- Module: Mathlib.Algebra.Polynomial.Eval.Degree
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : CommRing S
inst_2 : IsDomain S
φ : R →+* S
f : R[X]
hf : IsUnit f.leadingCoeff
H : IsUnit (map φ f)
dz : f.degree = 0
rw : IsUnit (M := R[X]) ((C : (a : R) → R[X]) (f.coeff 0) : R[X])
⊢ IsUnit f

Tactic:
rw [eq_C_of_degree_eq_zero dz]

Premises used: Polynomial.eq_C_of_degree_eq_zero
-- Module: Mathlib.Algebra.Polynomial.Eval.Degree
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : CommRing S
inst_2 : IsDomain S
φ : R →+* S
f : R[X]
hf : IsUnit f.leadingCoeff
H : IsUnit (map φ f)
dz : f.degree = 0
⊢ IsUnit (M := R[X]) ((C : (a : R) → R[X]) (f.coeff 0) : R[X])

Tactic:
IsUnit.map C ?_

Premises used: Polynomial.C, IsUnit.map
-- Module: Mathlib.Algebra.Polynomial.Eval.Degree
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : CommRing S
inst_2 : IsDomain S
φ : R →+* S
f : R[X]
hf : IsUnit f.leadingCoeff
H : IsUnit (map φ f)
dz : f.degree = 0
refine : IsUnit (f.coeff 0)
⊢ IsUnit (M := R[X]) ((C : (a : R) → R[X]) (f.coeff 0) : R[X])

Tactic:
refine IsUnit.map C ?_

Premises used: Polynomial.C, IsUnit.map
-- Module: Mathlib.Algebra.Polynomial.Eval.Degree
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : CommRing S
inst_2 : IsDomain S
φ : R →+* S
f : R[X]
hf : IsUnit f.leadingCoeff
H : IsUnit (map φ f)
dz : f.degree = 0
⊢ IsUnit f.leadingCoeff

Tactic:
hf
-- Module: Mathlib.Algebra.Polynomial.Eval.Degree
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : CommRing S
inst_2 : IsDomain S
φ : R →+* S
f : R[X]
hf : IsUnit f.leadingCoeff
H : IsUnit (map φ f)
dz : f.degree = 0
h : f.coeff 0 = f.leadingCoeff
⊢ IsUnit (f.coeff 0)

Tactic:
convert! hf
-- Module: Mathlib.Algebra.Polynomial.Eval.Degree
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : CommRing S
inst_2 : IsDomain S
φ : R →+* S
f : R[X]
hf : IsUnit f.leadingCoeff
H : IsUnit (map φ f)
dz : f.degree = 0
h : f.coeff 0 = f.coeff Zero.zero
rw : f ≠ 0
⊢ f.coeff 0 = f.coeff f.natDegree

Tactic:
rw [(degree_eq_iff_natDegree_eq _).1 dz]

Premises used: Iff.mp, Polynomial.degree_eq_iff_natDegree_eq
-- Module: Mathlib.Algebra.Polynomial.Eval.Degree
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : CommRing S
inst_2 : IsDomain S
φ : R →+* S
f : R[X]
hf : IsUnit f.leadingCoeff
H : IsUnit (map φ f)
dz : f.degree = 0
⊢ f.coeff 0 = f.coeff Zero.zero

Tactic:
rfl
-- Module: Mathlib.Algebra.Polynomial.Eval.Degree
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : CommRing S
inst_2 : IsDomain S
φ : R →+* S
hf : IsUnit.{u} (M := R) (leadingCoeff 0)
H : IsUnit (map φ 0)
dz : degree.{u} (R := R) 0 = 0
⊢ False

Tactic:
simp at H
-- Module: Mathlib.Algebra.Polynomial.Eval.Degree
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : CommRing S
inst_2 : IsDomain S
φ : R →+* S
f : R[X]
hf : IsUnit f.leadingCoeff
H : IsUnit (map φ f)
dz : (map φ f).degree = 0
h : Eq.{v + 1} (α := S) ((φ : (a : R) → S) f.leadingCoeff : S) (0 : S)
⊢ IsUnit.{v} (M := S) ((φ : (a : R) → S) f.leadingCoeff : S)

Tactic:
have u : IsUnit (φ f.leadingCoeff) := IsUnit.map φ hf
-- Module: Mathlib.Algebra.Polynomial.Eval.Degree
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : CommRing S
inst_2 : IsDomain S
φ : R →+* S
f : R[X]
hf : IsUnit f.leadingCoeff
H : IsUnit (map φ f)
dz : (map φ f).degree = 0
h : Eq.{v + 1} (α := S) ((φ : (a : R) → S) f.leadingCoeff : S) (0 : S)
u : IsUnit.{v} (M := S) ((φ : (a : R) → S) f.leadingCoeff : S)
⊢ IsUnit.{v} (M := S) 0

Tactic:
rw [h] at u
-- Module: Mathlib.Algebra.Polynomial.Eval.Degree
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : CommRing S
inst_2 : IsDomain S
φ : R →+* S
f : R[X]
hf : IsUnit f.leadingCoeff
H : IsUnit (map φ f)
dz : (map φ f).degree = 0
h : Eq.{v + 1} (α := S) ((φ : (a : R) → S) f.leadingCoeff : S) (0 : S)
u : IsUnit.{v} (M := S) 0
⊢ False

Tactic:
simp at u
-- Module: Mathlib.Algebra.Polynomial.Eval.SMul
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
g : R →+* S
p : R[X]
x : S
s : R
⊢ p.natDegree < p.natDegree.succ

Tactic:
have A : p.natDegree < p.natDegree.succ := Nat.lt_succ_self _
-- Module: Mathlib.Algebra.Polynomial.Eval.SMul
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
g : R →+* S
p : R[X]
x : S
s : R
A : p.natDegree < p.natDegree.succ
⊢ (s • p).natDegree < p.natDegree.succ

Tactic:
have B : (s • p).natDegree < p.natDegree.succ := (natDegree_smul_le _ _).trans_lt A
-- Module: Mathlib.Algebra.Polynomial.Eval.SMul
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
g : R →+* S
p : R[X]
x : S
s : R
A : p.natDegree < p.natDegree.succ
B : (s • p).natDegree < p.natDegree.succ
rw :
  ∑ a ∈ range p.natDegree.succ, HMul.hMul (α := S) ((g : (a : R) → S) ((s • p).coeff a) : S) (x ^ a) =
    HMul.hMul (α := S) (β := S) ((g : (a : R) → S) s : S)
      (∑ a ∈ range p.natDegree.succ, HMul.hMul (α := S) ((g : (a : R) → S) (p.coeff a) : S) (x ^ a) : S)
rw₁ rw₂ : ∀ (n : ℕ), HMul.hMul (α := S) ((g : (a : R) → S) 0 : S) (x ^ n) = 0
⊢ eval₂ g x (s • p) = HMul.hMul (α := S) ((g : (a : R) → S) s : S) (eval₂ g x p)

Tactic:
rw [eval₂_eq_sum, eval₂_eq_sum, sum_over_range' _ _ _ A, sum_over_range' _ _ _ B]

Premises used: Polynomial.sum_over_range', Polynomial.eval₂_eq_sum
-- Module: Mathlib.Algebra.Polynomial.Eval.SMul
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
g : R →+* S
p : R[X]
x : S
s : R
A : p.natDegree < p.natDegree.succ
B : (s • p).natDegree < p.natDegree.succ
⊢ ∑ a ∈ range p.natDegree.succ, HMul.hMul (α := S) ((g : (a : R) → S) ((s • p).coeff a) : S) (x ^ a) =
    HMul.hMul (α := S) (β := S) ((g : (a : R) → S) s : S)
      (∑ a ∈ range p.natDegree.succ, HMul.hMul (α := S) ((g : (a : R) → S) (p.coeff a) : S) (x ^ a) : S)

Tactic:
simp [mul_sum, mul_assoc]

Premises used: Finset.mul_sum, mul_assoc
-- Module: Mathlib.Algebra.Polynomial.Eval.SMul
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
g : R →+* S
p : R[X]
x : S
s : R
A : p.natDegree < p.natDegree.succ
B : (s • p).natDegree < p.natDegree.succ
⊢ ∀ (n : ℕ), HMul.hMul (α := S) ((g : (a : R) → S) 0 : S) (x ^ n) = 0

Tactic:
simp [mul_sum, mul_assoc]

Premises used: Finset.mul_sum, mul_assoc