awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.Smeval
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
S : Type u_2
inst_1 : NonAssocSemiring S
inst_2 : Module R S
inst_3 : Pow S ℕ
x : S
inst_4 : NatPowAssoc S
inst_5 : IsScalarTower R S S
inst_6 : SMulCommClass R S S
r s : R[X]
hr : (r * q).smeval x = r.smeval x * q.smeval x
hs : (s * q).smeval x = s.smeval x * q.smeval x
⊢ ((r + s) * q).smeval x = (r + s).smeval x * q.smeval x

Tactic:
simp only [hr, hs, smeval_add, add_mul]

Premises used: add_mul, Polynomial.smeval_add
-- Module: Mathlib.Algebra.Polynomial.Smeval
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
S : Type u_2
inst_1 : NonAssocSemiring S
inst_2 : Module R S
inst_3 : Pow S ℕ
x : S
inst_4 : NatPowAssoc S
inst_5 : IsScalarTower R S S
inst_6 : SMulCommClass R S S
n : ℕ
a : R
⊢ (HMul.hMul (α := R[X]) ((monomial n : (a : R) → R[X]) a : R[X]) q).smeval x =
    smeval.{u_1, u_2} (R := R) ((monomial n : (a : R) → R[X]) a) x * q.smeval x

Tactic:
simp only [smeval_monomial, smeval_monomial_mul, smul_mul_assoc]

Premises used: Polynomial.smeval_monomial_mul, smul_mul_assoc, Polynomial.smeval_monomial
-- Module: Mathlib.Algebra.Polynomial.Smeval
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
S : Type u_2
inst_1 : NonAssocSemiring S
inst_2 : Module R S
inst_3 : Pow S ℕ
x : S
inst_4 : NatPowAssoc S
inst_5 : IsScalarTower R S S
inst_6 : SMulCommClass R S S
add :
  ∀ (r s : R[X]) (hr : (r * q).smeval x = r.smeval x * q.smeval x) (hs : (s * q).smeval x = s.smeval x * q.smeval x),
    ((r + s) * q).smeval x = (r + s).smeval x * q.smeval x
monomial :
  ∀ (n : ℕ) (a : R),
    (HMul.hMul (α := R[X]) ((Polynomial.monomial n : (a : R) → R[X]) a : R[X]) q).smeval x =
      smeval.{u_1, u_2} (R := R) ((Polynomial.monomial n : (a : R) → R[X]) a) x * q.smeval x
⊢ (p * q).smeval x = p.smeval x * q.smeval x

Tactic:
induction p using Polynomial.induction_on' with
  | add r s hr hs => simp only [hr, hs, smeval_add, add_mul]
  | monomial n a =>
    simp only [smeval_monomial, smeval_monomial_mul, smul_mul_assoc]

Premises used: Polynomial.smeval_monomial_mul, add_mul, Polynomial.monomial, smul_mul_assoc, Polynomial.smeval_monomial, Polynomial.smeval_add
-- Module: Mathlib.Algebra.Polynomial.Smeval
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
S : Type u_2
inst_1 : NonAssocSemiring S
inst_2 : Module R S
inst_3 : Pow S ℕ
x : S
inst_4 : NatPowAssoc S
inst_5 : IsScalarTower R S S
inst_6 : SMulCommClass R S S
⊢ (HPow.hPow (β := ℕ) p 0).smeval x = HPow.hPow (β := ℕ) (p.smeval x) 0

Tactic:
simp only [npow_zero, smeval_one, one_smul]

Premises used: npow_zero, one_smul, Polynomial.smeval_one
-- Module: Mathlib.Algebra.Polynomial.Smeval
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
S : Type u_2
inst_1 : NonAssocSemiring S
inst_2 : Module R S
inst_3 : Pow S ℕ
x : S
inst_4 : NatPowAssoc S
inst_5 : IsScalarTower R S S
inst_6 : SMulCommClass R S S
n : ℕ
rw : (p ^ n * HPow.hPow (β := ℕ) p 1).smeval x = p.smeval x ^ (n + 1)
rw₁ : (p ^ n).smeval x * (HPow.hPow (β := ℕ) p 1).smeval x = p.smeval x ^ (n + 1)
rw₂ : p.smeval x ^ n * (HPow.hPow (β := ℕ) p 1).smeval x = p.smeval x ^ (n + 1)
rw₃ : p.smeval x ^ n * p.smeval x = p.smeval x ^ (n + 1)
rw₄ : p.smeval x ^ n * p.smeval x = p.smeval x ^ n * HPow.hPow (β := ℕ) (p.smeval x) 1
rw₅ rw₆ : p.smeval x ^ n * p.smeval x = p.smeval x ^ n * p.smeval x
⊢ (p ^ (n + 1)).smeval x = p.smeval x ^ (n + 1)

Tactic:
rw [npow_add, smeval_mul, smeval_pow n, pow_one, npow_add, npow_one]

Premises used: npow_one, Polynomial.smeval_mul, pow_one, npow_add
-- Module: Mathlib.Algebra.Polynomial.Smeval
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
S : Type u_2
inst_1 : NonAssocSemiring S
inst_2 : Module R S
inst_3 : Pow S ℕ
x : S
inst_4 : NatPowAssoc S
inst_5 : IsScalarTower R S S
inst_6 : SMulCommClass R S S
r s : R[X]
hr : (r.comp q).smeval x = r.smeval (q.smeval x)
hs : (s.comp q).smeval x = s.smeval (q.smeval x)
⊢ ((r + s).comp q).smeval x = (r + s).smeval (q.smeval x)

Tactic:
simp [add_comp, hr, hs, smeval_add]

Premises used: Polynomial.add_comp, Polynomial.smeval_add
-- Module: Mathlib.Algebra.Polynomial.Smeval
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
S : Type u_2
inst_1 : NonAssocSemiring S
inst_2 : Module R S
inst_3 : Pow S ℕ
x : S
inst_4 : NatPowAssoc S
inst_5 : IsScalarTower R S S
inst_6 : SMulCommClass R S S
n : ℕ
a : R
⊢ (comp ((monomial n : (a : R) → R[X]) a) q).smeval x =
    smeval.{u_1, u_2} (R := R) ((monomial n : (a : R) → R[X]) a) (q.smeval x)

Tactic:
simp [smeval_monomial, smeval_C_mul, smeval_pow]

Premises used: Polynomial.smeval_C_mul, Polynomial.smeval_pow, Polynomial.smeval_monomial
-- Module: Mathlib.Algebra.Polynomial.Smeval
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
S : Type u_2
inst_1 : NonAssocSemiring S
inst_2 : Module R S
inst_3 : Pow S ℕ
x : S
inst_4 : NatPowAssoc S
inst_5 : IsScalarTower R S S
inst_6 : SMulCommClass R S S
add :
  ∀ (r s : R[X]) (hr : (r.comp q).smeval x = r.smeval (q.smeval x)) (hs : (s.comp q).smeval x = s.smeval (q.smeval x)),
    ((r + s).comp q).smeval x = (r + s).smeval (q.smeval x)
monomial :
  ∀ (n : ℕ) (a : R),
    (comp ((Polynomial.monomial n : (a : R) → R[X]) a) q).smeval x =
      smeval.{u_1, u_2} (R := R) ((Polynomial.monomial n : (a : R) → R[X]) a) (q.smeval x)
⊢ (p.comp q).smeval x = p.smeval (q.smeval x)

Tactic:
induction p using Polynomial.induction_on' with
  | add r s hr hs => simp [add_comp, hr, hs, smeval_add]
  | monomial n a => simp [smeval_monomial, smeval_C_mul, smeval_pow]

Premises used: Polynomial.monomial, Polynomial.smeval_C_mul, Polynomial.add_comp, Polynomial.smeval_pow, Polynomial.smeval_monomial, Polynomial.smeval_add
-- Module: Mathlib.Algebra.Polynomial.Smeval
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
S : Type u_2
inst_1 : Semiring S
inst_2 : Module R S
inst_3 : IsScalarTower R S S
inst_4 : SMulCommClass R S S
x y : S
hc : Commute x y
r s : R[X]
hr : Commute (r.smeval x) y
hs : Commute (s.smeval x) y
⊢ Commute ((r + s).smeval x) y

Tactic:
(smeval_add R r s x) ▸ Commute.add_left hr hs

Premises used: Eq.rec, Commute.add_left, Polynomial.smeval_add, Eq.symm
-- Module: Mathlib.Algebra.Polynomial.Smeval
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
S : Type u_2
inst_1 : Semiring S
inst_2 : Module R S
inst_3 : IsScalarTower R S S
inst_4 : SMulCommClass R S S
x y : S
hc : Commute x y
r s : R[X]
hr : Commute (r.smeval x) y
hs : Commute (s.smeval x) y
⊢ Commute ((r + s).smeval x) y

Tactic:
exact (smeval_add R r s x) ▸ Commute.add_left hr hs
-- Module: Mathlib.Algebra.Polynomial.Smeval
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
S : Type u_2
inst_1 : Semiring S
inst_2 : Module R S
inst_3 : IsScalarTower R S S
inst_4 : SMulCommClass R S S
x y : S
hc : Commute x y
n : ℕ
a : R
⊢ Commute (smeval.{u_1, u_2} (R := R) ((monomial n : (a : R) → R[X]) a) x) y

Tactic:
simpa [smeval_monomial] using Commute.smul_left (Commute.pow_left hc _) _

Premises used: Commute.smul_left, Commute.pow_left, Polynomial.smeval_monomial
-- Module: Mathlib.Algebra.Polynomial.Smeval
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
S : Type u_2
inst_1 : Semiring S
inst_2 : Module R S
inst_3 : IsScalarTower R S S
inst_4 : SMulCommClass R S S
x y : S
hc : Commute x y
add : ∀ (r s : R[X]) (hr : Commute (r.smeval x) y) (hs : Commute (s.smeval x) y), Commute ((r + s).smeval x) y
monomial : ∀ (n : ℕ) (a : R), Commute (smeval.{u_1, u_2} (R := R) ((Polynomial.monomial n : (a : R) → R[X]) a) x) y
⊢ Commute (p.smeval x) y

Tactic:
induction p using Polynomial.induction_on' with
  | add r s hr hs => exact (smeval_add R r s x) ▸ Commute.add_left hr hs
  | monomial n a => simpa [smeval_monomial] using Commute.smul_left (Commute.pow_left hc _) _

Premises used: Commute.smul_left, Polynomial.monomial, Commute.pow_left, Polynomial.smeval_monomial
-- Module: Mathlib.Algebra.Polynomial.Smeval
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
S : Type u_2
inst_1 : Semiring S
inst_2 : Module R S
inst_3 : IsScalarTower R S S
inst_4 : SMulCommClass R S S
x y : S
hc : Commute x y
r s : R[X]
hr : Commute (r.smeval x) (q.smeval y)
hs : Commute (s.smeval x) (q.smeval y)
⊢ Commute ((r + s).smeval x) (q.smeval y)

Tactic:
(smeval_add R r s x) ▸ Commute.add_left hr hs

Premises used: Eq.rec, Commute.add_left, Polynomial.smeval_add, Eq.symm
-- Module: Mathlib.Algebra.Polynomial.Smeval
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
S : Type u_2
inst_1 : Semiring S
inst_2 : Module R S
inst_3 : IsScalarTower R S S
inst_4 : SMulCommClass R S S
x y : S
hc : Commute x y
r s : R[X]
hr : Commute (r.smeval x) (q.smeval y)
hs : Commute (s.smeval x) (q.smeval y)
⊢ Commute ((r + s).smeval x) (q.smeval y)

Tactic:
exact (smeval_add R r s x) ▸ Commute.add_left hr hs
-- Module: Mathlib.Algebra.Polynomial.Smeval
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
S : Type u_2
inst_1 : Semiring S
inst_2 : Module R S
inst_3 : IsScalarTower R S S
inst_4 : SMulCommClass R S S
x y : S
hc : Commute x y
n : ℕ
a : R
monomial : Commute (a • x ^ n) (q.smeval y)
⊢ Commute (smeval.{u_1, u_2} (R := R) ((Polynomial.monomial n : (a : R) → R[X]) a) x) (q.smeval y)

Tactic:
simp only [smeval_monomial]

Premises used: Polynomial.smeval_monomial
-- Module: Mathlib.Algebra.Polynomial.Smeval
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
S : Type u_2
inst_1 : Semiring S
inst_2 : Module R S
inst_3 : IsScalarTower R S S
inst_4 : SMulCommClass R S S
x y : S
hc : Commute x y
n : ℕ
a : R
⊢ Commute (a • x ^ n) (q.smeval y)

Tactic:
Commute.smul_left ?_ a

Premises used: Commute.smul_left
-- Module: Mathlib.Algebra.Polynomial.Smeval
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
S : Type u_2
inst_1 : Semiring S
inst_2 : Module R S
inst_3 : IsScalarTower R S S
inst_4 : SMulCommClass R S S
x y : S
hc : Commute x y
n : ℕ
a : R
monomial : Commute (x ^ n) (q.smeval y)
⊢ Commute (a • x ^ n) (q.smeval y)

Tactic:
refine Commute.smul_left ?_ a

Premises used: Commute.smul_left
-- Module: Mathlib.Algebra.Polynomial.Smeval
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
S : Type u_2
inst_1 : Semiring S
inst_2 : Module R S
inst_3 : IsScalarTower R S S
inst_4 : SMulCommClass R S S
x y : S
hc : Commute x y
a : R
⊢ Commute (HPow.hPow (β := ℕ) x 0) (q.smeval y)

Tactic:
simp only [npow_zero, Commute.one_left]

Premises used: npow_zero, Commute.one_left
-- Module: Mathlib.Algebra.Polynomial.Smeval
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
S : Type u_2
inst_1 : Semiring S
inst_2 : Module R S
inst_3 : IsScalarTower R S S
inst_4 : SMulCommClass R S S
x y : S
hc : Commute x y
a : R
n : ℕ
ih : Commute (x ^ n) (q.smeval y)
⊢ Commute (x ^ (n + 1)) (q.smeval y)

Tactic:
(commute_iff_eq (x ^ (n + 1)) (q.smeval y)).mpr ?_

Premises used: Iff.mpr, commute_iff_eq, HPow.hPow, HAdd.hAdd, OfNat.ofNat, Polynomial.smeval
-- Module: Mathlib.Algebra.Polynomial.Smeval
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
S : Type u_2
inst_1 : Semiring S
inst_2 : Module R S
inst_3 : IsScalarTower R S S
inst_4 : SMulCommClass R S S
x y : S
hc : Commute x y
a : R
n : ℕ
ih : Commute (x ^ n) (q.smeval y)
⊢ x ^ n * q.smeval y = q.smeval y * x ^ n

Tactic:
rw [commute_iff_eq (x ^ n) (q.smeval y)] at ih

Premises used: commute_iff_eq, HPow.hPow, Polynomial.smeval
-- Module: Mathlib.Algebra.Polynomial.Smeval
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
S : Type u_2
inst_1 : Semiring S
inst_2 : Module R S
inst_3 : IsScalarTower R S S
inst_4 : SMulCommClass R S S
x y : S
hc : Commute x y
a : R
n : ℕ
ih : x ^ n * q.smeval y = q.smeval y * x ^ n
⊢ x * q.smeval y = q.smeval y * x

Tactic:
(commute_iff_eq x (q.smeval y)).mp ?_

Premises used: commute_iff_eq, Iff.mp, Polynomial.smeval
-- Module: Mathlib.Algebra.Polynomial.Smeval
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
S : Type u_2
inst_1 : Semiring S
inst_2 : Module R S
inst_3 : IsScalarTower R S S
inst_4 : SMulCommClass R S S
x y : S
hc : Commute x y
a : R
n : ℕ
ih : x ^ n * q.smeval y = q.smeval y * x ^ n
⊢ Commute x (q.smeval y)

Tactic:
Commute.symm (smeval_commute_left R q (Commute.symm hc))

Premises used: Commute.symm, Polynomial.smeval_commute_left
-- Module: Mathlib.Algebra.Polynomial.Smeval
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
S : Type u_2
inst_1 : Semiring S
inst_2 : Module R S
inst_3 : IsScalarTower R S S
inst_4 : SMulCommClass R S S
x y : S
hc : Commute x y
a : R
n : ℕ
ih : x ^ n * q.smeval y = q.smeval y * x ^ n
⊢ Commute x (q.smeval y)

Tactic:
exact Commute.symm (smeval_commute_left R q (Commute.symm hc))

Premises used: Commute.symm, Polynomial.smeval_commute_left
-- Module: Mathlib.Algebra.Polynomial.Smeval
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
S : Type u_2
inst_1 : Semiring S
inst_2 : Module R S
inst_3 : IsScalarTower R S S
inst_4 : SMulCommClass R S S
x y : S
hc : Commute x y
a : R
n : ℕ
ih : x ^ n * q.smeval y = q.smeval y * x ^ n
⊢ x * q.smeval y = q.smeval y * x

Tactic:
have hxq : x * q.smeval y = q.smeval y * x := by
        refine (commute_iff_eq x (q.smeval y)).mp ?_
        exact Commute.symm (smeval_commute_left R q (Commute.symm hc))
-- Module: Mathlib.Algebra.Polynomial.Smeval
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
S : Type u_2
inst_1 : Semiring S
inst_2 : Module R S
inst_3 : IsScalarTower R S S
inst_4 : SMulCommClass R S S
x y : S
hc : Commute x y
a : R
n : ℕ
ih : x ^ n * q.smeval y = q.smeval y * x ^ n
hxq : x * q.smeval y = q.smeval y * x
monomial : x ^ n * x * q.smeval y = q.smeval y * (x ^ n * x)
monomial₁ : x ^ n * x * q.smeval y = q.smeval y * x ^ n * x
monomial₂ : x ^ n * x * q.smeval y = x ^ n * q.smeval y * x
monomial₃ : x ^ n * (x * q.smeval y) = x ^ n * q.smeval y * x
monomial₄ : x ^ n * (q.smeval y * x) = x ^ n * q.smeval y * x
monomial₅ monomial₆ : x ^ n * (q.smeval y * x) = x ^ n * (q.smeval y * x)
⊢ x ^ (n + 1) * q.smeval y = q.smeval y * x ^ (n + 1)

Tactic:
rw [pow_succ, ← mul_assoc, ← ih, mul_assoc, hxq, mul_assoc]

Premises used: pow_succ, mul_assoc
-- Module: Mathlib.Algebra.Polynomial.Smeval
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
S : Type u_2
inst_1 : Semiring S
inst_2 : Module R S
inst_3 : IsScalarTower R S S
inst_4 : SMulCommClass R S S
x y : S
hc : Commute x y
n : ℕ
a : R
monomial : Commute (HPow.hPow (β := ℕ) x 0) (q.smeval y)
monomial₁ : ∀ (n : ℕ) (ih : Commute (x ^ n) (q.smeval y)), Commute (x ^ (n + 1)) (q.smeval y)
⊢ Commute (x ^ n) (q.smeval y)

Tactic:
induction n with
    | zero => simp only [npow_zero, Commute.one_left]
    | succ n ih =>
      refine (commute_iff_eq (x ^ (n + 1)) (q.smeval y)).mpr ?_
      rw [commute_iff_eq (x ^ n) (q.smeval y)] at ih
      have hxq : x * q.smeval y = q.smeval y * x := by
        refine (commute_iff_eq x (q.smeval y)).mp ?_
        exact Commute.symm (smeval_commute_left R q (Commute.symm hc))
      rw [pow_succ, ← mul_assoc, ← ih, mul_assoc, hxq, mul_assoc]

Premises used: Iff.mpr, pow_succ, mul_assoc, commute_iff_eq, npow_zero, HPow.hPow, HAdd.hAdd, OfNat.ofNat, Polynomial.smeval, Commute.one_left
-- Module: Mathlib.Algebra.Polynomial.Smeval
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
S : Type u_2
inst_1 : Semiring S
inst_2 : Module R S
inst_3 : IsScalarTower R S S
inst_4 : SMulCommClass R S S
x y : S
hc : Commute x y
add :
  ∀ (r s : R[X]) (hr : Commute (r.smeval x) (q.smeval y)) (hs : Commute (s.smeval x) (q.smeval y)),
    Commute ((r + s).smeval x) (q.smeval y)
monomial :
  ∀ (n : ℕ) (a : R), Commute (smeval.{u_1, u_2} (R := R) ((Polynomial.monomial n : (a : R) → R[X]) a) x) (q.smeval y)
⊢ Commute (p.smeval x) (q.smeval y)

Tactic:
induction p using Polynomial.induction_on' with
  | add r s hr hs => exact (smeval_add R r s x) ▸ Commute.add_left hr hs
  | monomial n a =>
    simp only [smeval_monomial]
    refine Commute.smul_left ?_ a
    induction n with
    | zero => simp only [npow_zero, Commute.one_left]
    | succ n ih =>
      refine (commute_iff_eq (x ^ (n + 1)) (q.smeval y)).mpr ?_
      rw [commute_iff_eq (x ^ n) (q.smeval y)] at ih
      have hxq : x * q.smeval y = q.smeval y * x := by
        refine (commute_iff_eq x (q.smeval y)).mp ?_
        exact Commute.symm (smeval_commute_left R q (Commute.symm hc))
      rw [pow_succ, ← mul_assoc, ← ih, mul_assoc, hxq, mul_assoc]

Premises used: pow_succ, mul_assoc, Polynomial.monomial, npow_zero, Polynomial.smeval_monomial, Commute.one_left
-- Module: Mathlib.Algebra.Polynomial.Smeval
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : Semiring S
inst_2 : Algebra R S
x : S
p : R[X]
simp : (p.sum fun (e : ℕ) (a : R) ↦ a • x ^ e) = p.sum (smul_pow x)
⊢ (p.sum fun (e : ℕ) (a : R) ↦ (fun (r : R) ↦ HSMul.hSMul (β := S) r 1) a * x ^ e) = p.sum (smul_pow x)

Tactic:
simp only [Algebra.smul_mul_assoc, one_mul]

Premises used: Algebra.smul_mul_assoc, one_mul
-- Module: Mathlib.Algebra.Polynomial.Smeval
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : Semiring S
inst_2 : Algebra R S
x : S
p : R[X]
⊢ (p.sum fun (e : ℕ) (a : R) ↦ a • x ^ e) = p.sum (smul_pow x)

Tactic:
rfl

Premises used: Polynomial.smul_pow, rfl
-- Module: Mathlib.Algebra.Polynomial.Smeval
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : Semiring S
inst_2 : Algebra R S
x : S
p : R[X]
⊢ (p.sum fun (e : ℕ) (a : R) ↦ a • x ^ e) = p.sum (smul_pow x)

Tactic:
exact rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Polynomial.Smeval
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : Semiring S
inst_2 : Algebra R S
x : S
⊢ Eq (α := (a : R[X]) → S) (⇑(aeval x) : (a : R[X]) → S) fun (p : R[X]) ↦ p.smeval x

Tactic:
funext fun p => aeval_eq_smeval x p

Premises used: Polynomial.aeval_eq_smeval, funext
-- Module: Mathlib.Algebra.Polynomial.SpecificDegree
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
hp : p.Monic
hp2 : 2 ≤ p.natDegree
hp3 : p.natDegree ≤ 3
⊢ p ≠ 0

Tactic:
have hp0 : p ≠ 0 := hp.ne_zero
-- Module: Mathlib.Algebra.Polynomial.SpecificDegree
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
hp : Monic.{u_1} (R := R) 1
hp2 : 2 ≤ natDegree.{u_1} (R := R) 1
hp3 : natDegree.{u_1} (R := R) 1 ≤ 3
hp0 : Ne.{u_1 + 1} (α := R[X]) 1 0
⊢ LE.le (α := ℕ) 2 0

Tactic:
rw [natDegree_one] at hp2

Premises used: Polynomial.natDegree_one
-- Module: Mathlib.Algebra.Polynomial.SpecificDegree
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
hp : Monic.{u_1} (R := R) 1
hp2 : 2 ≤ natDegree.{u_1} (R := R) 1
hp3 : natDegree.{u_1} (R := R) 1 ≤ 3
hp0 : Ne.{u_1 + 1} (α := R[X]) 1 0
hp2₁ : LE.le (α := ℕ) 2 0
⊢ natDegree.{u_1} (R := R) 1 ≤ 3

Tactic:
rw [natDegree_one] at hp2

Premises used: Polynomial.natDegree_one
-- Module: Mathlib.Algebra.Polynomial.SpecificDegree
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
hp : Monic.{u_1} (R := R) 1
hp2 : 2 ≤ natDegree.{u_1} (R := R) 1
hp3 : natDegree.{u_1} (R := R) 1 ≤ 3
hp0 : Ne.{u_1 + 1} (α := R[X]) 1 0
hp2₁ : LE.le (α := ℕ) 2 0
hp3₁ : natDegree.{u_1} (R := R) 1 ≤ 3
⊢ Ne.{u_1 + 1} (α := R[X]) 1 0

Tactic:
rw [natDegree_one] at hp2

Premises used: Polynomial.natDegree_one
-- Module: Mathlib.Algebra.Polynomial.SpecificDegree
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
hp : Monic.{u_1} (R := R) 1
hp2 : LE.le (α := ℕ) 2 0
hp3 : natDegree.{u_1} (R := R) 1 ≤ 3
hp0 : Ne.{u_1 + 1} (α := R[X]) 1 0
⊢ False

Tactic:
cases hp2
-- Module: Mathlib.Algebra.Polynomial.SpecificDegree
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
hp : p.Monic
hp2 : 2 ≤ p.natDegree
hp3 : p.natDegree ≤ 3
hp0 : p ≠ 0
⊢ p ≠ 1

Tactic:
have hp1 : p ≠ 1 := by rintro rfl; rw [natDegree_one] at hp2; cases hp2
-- Module: Mathlib.Algebra.Polynomial.SpecificDegree
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
hp : p.Monic
hp2 : 2 ≤ p.natDegree
hp3 : p.natDegree ≤ 3
hp0 : p ≠ 0
hp1 : p ≠ 1
rw : (∀ (q : R[X]), q.Monic → q.natDegree ∈ Finset.Ioc 0 (p.natDegree / 2) → ¬q ∣ p) ↔ p.roots = 0
⊢ Irreducible p ↔ p.roots = 0

Tactic:
rw [hp.irreducible_iff_lt_natDegree_lt hp1]

Premises used: Polynomial.Monic.irreducible_iff_lt_natDegree_lt
-- Module: Mathlib.Algebra.Polynomial.SpecificDegree
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
hp : p.Monic
hp2 : 2 ≤ p.natDegree
hp3 : p.natDegree ≤ 3
hp0 : p ≠ 0
hp1 : p ≠ 1
⊢ 3 / 2 ≤ p.natDegree / 2

Tactic:
apply Nat.div_le_div_right (c := 2) hp2

Premises used: Nat.div_le_div_right
-- Module: Mathlib.Algebra.Polynomial.SpecificDegree
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
hp : p.Monic
hp2 : 2 ≤ p.natDegree
hp3 : p.natDegree ≤ 3
hp0 : p ≠ 0
hp1 : p ≠ 1
simp_rw :
  (∀ (q : R[X]), q.Monic → q.natDegree = 1 → ¬q ∣ p) ↔
    ∀ (a : R), ¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ∣ p
⊢ (∀ (q : R[X]), q.Monic → q.natDegree ∈ Finset.Ioc 0 (p.natDegree / 2) → ¬q ∣ p) ↔ p.roots = 0

Tactic:
simp_rw [show p.natDegree / 2 = 1 from
      (Nat.div_le_div_right hp3).antisymm
        (by apply Nat.div_le_div_right (c := 2) hp2),
    show Finset.Ioc 0 1 = {1} from rfl,
    Finset.mem_singleton, Multiset.eq_zero_iff_forall_notMem, mem_roots hp0, ← dvd_iff_isRoot]

Premises used: Finset.mem_singleton, Nat.div_le_div_right, Multiset.eq_zero_iff_forall_notMem, LE.le.antisymm, Polynomial.mem_roots, Polynomial.dvd_iff_isRoot, rfl
-- Module: Mathlib.Algebra.Polynomial.SpecificDegree
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
hp : p.Monic
hp2 : 2 ≤ p.natDegree
hp3 : p.natDegree ≤ 3
hp0 : p ≠ 0
hp1 : p ≠ 1
⊢ (∀ (q : R[X]), q.Monic → q.natDegree = 1 → ¬q ∣ p) ↔
    ∀ (a : R), ¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ∣ p

Tactic:
⟨fun h r ↦ h _ (monic_X_sub_C r) (natDegree_X_sub_C r), fun h q hq hq1 ↦ ?_⟩

Premises used: Polynomial.monic_X_sub_C, Polynomial.C, HSub.hSub, Polynomial.natDegree_X_sub_C, Iff.intro, Polynomial.X, DFunLike.coe
-- Module: Mathlib.Algebra.Polynomial.SpecificDegree
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
hp : p.Monic
hp2 : 2 ≤ p.natDegree
hp3 : p.natDegree ≤ 3
hp0 : p ≠ 0
hp1 : p ≠ 1
refine :
  ∀ (h : ∀ (a : R), ¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ∣ p) (q : R[X]) (hq : q.Monic)
    (hq1 : q.natDegree = 1), ¬q ∣ p
⊢ (∀ (q : R[X]), q.Monic → q.natDegree = 1 → ¬q ∣ p) ↔
    ∀ (a : R), ¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ∣ p

Tactic:
refine ⟨fun h r ↦ h _ (monic_X_sub_C r) (natDegree_X_sub_C r), fun h q hq hq1 ↦ ?_⟩
-- Module: Mathlib.Algebra.Polynomial.SpecificDegree
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
hp : p.Monic
hp2 : 2 ≤ p.natDegree
hp3 : p.natDegree ≤ 3
hp0 : p ≠ 0
hp1 : p ≠ 1
h : ∀ (a : R), ¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ∣ p
q : R[X]
hq : q.Monic
hq1 : q.natDegree = 1
rw : ¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (-q.coeff 0) : R[X]) ∣ p
⊢ ¬q ∣ p

Tactic:
rw [hq.eq_X_add_C hq1, ← sub_neg_eq_add, ← C_neg]

Premises used: Polynomial.Monic.eq_X_add_C, Polynomial.C_neg, sub_neg_eq_add
-- Module: Mathlib.Algebra.Polynomial.SpecificDegree
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
hp : p.Monic
hp2 : 2 ≤ p.natDegree
hp3 : p.natDegree ≤ 3
hp0 : p ≠ 0
hp1 : p ≠ 1
h : ∀ (a : R), ¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ∣ p
q : R[X]
hq : q.Monic
hq1 : q.natDegree = 1
⊢ ¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (-q.coeff 0) : R[X]) ∣ p

Tactic:
apply h
-- Module: Mathlib.Algebra.Polynomial.SpecificDegree
Goal:
K : Type u_1
inst : Field K
hp2 : 2 ≤ natDegree.{u_1} (R := K) 0
hp3 : natDegree.{u_1} (R := K) 0 ≤ 3
⊢ LE.le (α := ℕ) 2 0

Tactic:
rw [natDegree_zero] at hp2

Premises used: Polynomial.natDegree_zero
-- Module: Mathlib.Algebra.Polynomial.SpecificDegree
Goal:
K : Type u_1
inst : Field K
hp2 : 2 ≤ natDegree.{u_1} (R := K) 0
hp3 : natDegree.{u_1} (R := K) 0 ≤ 3
hp2₁ : LE.le (α := ℕ) 2 0
⊢ natDegree.{u_1} (R := K) 0 ≤ 3

Tactic:
rw [natDegree_zero] at hp2

Premises used: Polynomial.natDegree_zero
-- Module: Mathlib.Algebra.Polynomial.SpecificDegree
Goal:
K : Type u_1
inst : Field K
hp2 : LE.le (α := ℕ) 2 0
hp3 : natDegree.{u_1} (R := K) 0 ≤ 3
⊢ False

Tactic:
cases hp2
-- Module: Mathlib.Algebra.Polynomial.SpecificDegree
Goal:
K : Type u_1
inst : Field K
p : K[X]
hp2 : 2 ≤ p.natDegree
hp3 : p.natDegree ≤ 3
⊢ p ≠ 0

Tactic:
have hp0 : p ≠ 0 := by rintro rfl; rw [natDegree_zero] at hp2; cases hp2