awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
hf : Injective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
p : R[X]
⊢ p.Monic ↔ (map f p).Monic

Tactic:
⟨Monic.map _, Polynomial.monic_of_injective hf⟩

Premises used: Iff.intro, Polynomial.monic_of_injective, Polynomial.Monic.map
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Ring R
x : R
⊢ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).Monic

Tactic:
simpa only [sub_eq_add_neg, C_neg] using monic_X_add_C (-x)

Premises used: sub_eq_add_neg, Polynomial.monic_X_add_C, Polynomial.C_neg, Neg.neg
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Ring R
p : R[X]
n : ℕ
H : p.degree < (↑n : WithBot ℕ)
rwa rwa₁ rwa₂ rwa₃ : ∀ (H : (-p).degree < (↑n : WithBot ℕ)), (-p).degree < (↑n : WithBot ℕ)
⊢ (-p).degree < (↑n : WithBot ℕ)

Tactic:
rwa [← degree_neg p] at H

Premises used: Polynomial.degree_neg
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Ring R
p : R[X]
n : ℕ
H : p.degree < (↑n : WithBot ℕ)
⊢ (HPow.hPow (α := R[X]) X n - p).Monic

Tactic:
simpa [sub_eq_add_neg] using monic_X_pow_add (show degree (-p) < n by rwa [← degree_neg p] at H)

Premises used: Polynomial.monic_X_pow_add, sub_eq_add_neg
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Ring R
a : R
n : ℕ
h : n ≠ 0
⊢ (HSub.hSub (β := R[X]) (HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) a : R[X])).Monic

Tactic:
simpa only [map_neg, ← sub_eq_add_neg] using monic_X_pow_add_C (-a) h

Premises used: Polynomial.monic_X_pow_add_C, sub_eq_add_neg, map_neg, Neg.neg
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u_1
inst : Ring R
inst_1 : Nontrivial R
n : ℕ
h : IsUnit (HPow.hPow (α := R[X]) X n - 1)
inl : ∀ (h : IsUnit (HPow.hPow (α := R[X]) (β := ℕ) X 0 - 1)), False
inr : ∀ (hn : n ≠ 0), False
⊢ False

Tactic:
rcases eq_or_ne n 0 with (rfl | hn)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u_1
inst : Ring R
inst_1 : Nontrivial R
h : IsUnit (HPow.hPow (α := R[X]) (β := ℕ) X 0 - 1)
⊢ False

Tactic:
simp at h
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u_1
inst : Ring R
inst_1 : Nontrivial R
n : ℕ
h : IsUnit (HPow.hPow (α := R[X]) X n - 1)
hn : n ≠ 0
inr : n = 0
⊢ False

Tactic:
apply hn
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u_1
inst : Ring R
inst_1 : Nontrivial R
n : ℕ
h : IsUnit (HPow.hPow (α := R[X]) X n - 1)
hn : n ≠ 0
inr : n = natDegree.{u_1} (R := R) 1
inr₁ : n = (HPow.hPow (α := R[X]) X n - (C : (a : R) → R[X]) 1).natDegree
inr₂ inr₃ : n = n
⊢ n = 0

Tactic:
rw [← @natDegree_one R, ← (monic_X_pow_sub_C _ hn).eq_one_of_isUnit h, natDegree_X_pow_sub_C]

Premises used: Polynomial.natDegree_X_pow_sub_C, Polynomial.monic_X_pow_sub_C, Polynomial.natDegree_one, Polynomial.Monic.eq_one_of_isUnit
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Ring R
p : R[X]
hp : p.Monic
r : R
⊢ (p.comp (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X]))).Monic

Tactic:
simpa using hp.comp_X_add_C (-r)

Premises used: Polynomial.Monic.comp_X_add_C, Neg.neg
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Ring R
p q : R[X]
hp : p.Monic
hpq : q.degree < p.degree
apply : (-q).degree < p.degree
⊢ (p + -q).Monic

Tactic:
apply hp.add_of_left

Premises used: Polynomial.Monic.add_of_left
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Ring R
p q : R[X]
hp : p.Monic
hpq rwa rwa₁ rwa₂ rwa₃ : q.degree < p.degree
⊢ (-q).degree < p.degree

Tactic:
rwa [degree_neg]

Premises used: Polynomial.degree_neg
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Ring R
p q : R[X]
hq : q.leadingCoeff = -1
hpq : p.degree < q.degree
rw : (-q).coeff q.natDegree = 1
rw₁ : -q.coeff q.natDegree = 1
rw₂ : Eq.{u + 1} (α := R) (- -1) 1
rw₃ rw₄ : Eq.{u + 1} (α := R) 1 1
⊢ (-q).coeff (-q).natDegree = 1

Tactic:
rw [natDegree_neg, coeff_neg, show q.coeff q.natDegree = -1 from hq, neg_neg]

Premises used: neg_neg, Polynomial.coeff_neg, Polynomial.natDegree_neg
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Ring R
p q : R[X]
hq : q.leadingCoeff = -1
hpq : p.degree < q.degree
⊢ (-q).coeff (-q).natDegree = 1

Tactic:
have : (-q).coeff (-q).natDegree = 1 := by
    rw [natDegree_neg, coeff_neg, show q.coeff q.natDegree = -1 from hq, neg_neg]
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Ring R
p q : R[X]
hq : q.leadingCoeff = -1
hpq : p.degree < q.degree
this : (-q).coeff (-q).natDegree = 1
apply : p.degree < (-q).degree
⊢ (p + -q).Monic

Tactic:
apply Monic.add_of_right this

Premises used: Polynomial.Monic.add_of_right
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Ring R
p q : R[X]
hq : q.leadingCoeff = -1
hpq : p.degree < q.degree
this : (-q).coeff (-q).natDegree = 1
rwa rwa₁ rwa₂ rwa₃ : p.degree < q.degree
⊢ p.degree < (-q).degree

Tactic:
rwa [degree_neg]

Premises used: Polynomial.degree_neg
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
inst_1 : Nontrivial R
⊢ ¬Monic.{u} (R := R) 0

Tactic:
not_monic_zero_iff.mp zero_ne_one

Premises used: zero_ne_one, Polynomial.leadingCoeff, Polynomial.coeff, Polynomial.Monic, Iff.mp, Polynomial.not_monic_zero_iff
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p.Monic
q : R[X]
hq : q ≠ 0
pos : ∀ (h : p = 1), q * p ≠ 0
neg : ∀ (h : ¬p = 1), q * p ≠ 0
⊢ q * p ≠ 0

Tactic:
by_cases h : p = 1
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p.Monic
q : R[X]
hq : q ≠ 0
h : p = 1
⊢ q * p ≠ 0

Tactic:
simpa [h]
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p.Monic
q : R[X]
hq : q ≠ 0
h : ¬p = 1
neg : ¬q = 0 ∧ ¬p.degree = ⊥
⊢ q * p ≠ 0

Tactic:
rw [Ne, ← degree_eq_bot, hp.degree_mul, WithBot.add_eq_bot, not_or, degree_eq_bot]

Premises used: Ne, not_or, Polynomial.Monic.degree_mul, Polynomial.degree_eq_bot, WithBot.add_eq_bot
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p.Monic
q : R[X]
hq : q ≠ 0
h : ¬p = 1
⊢ ¬q = 0 ∧ ¬p.degree = ⊥

Tactic:
⟨hq, ?_⟩

Premises used: And.intro
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p.Monic
q : R[X]
hq : q ≠ 0
h : ¬p = 1
neg : ¬p.degree = ⊥
⊢ ¬q = 0 ∧ ¬p.degree = ⊥

Tactic:
refine ⟨hq, ?_⟩
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p.Monic
q : R[X]
hq : q ≠ 0
h : ¬p = 1
⊢ 0 < p.degree

Tactic:
rw [← hp.degree_le_zero_iff_eq_one, not_le] at h

Premises used: not_le, Polynomial.Monic.degree_le_zero_iff_eq_one
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p.Monic
q : R[X]
hq : q ≠ 0
h : 0 < p.degree
⊢ ¬p.degree = ⊥

Tactic:
(lt_trans ?_ h).ne'

Premises used: lt_trans, LT.lt.ne'
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p.Monic
q : R[X]
hq : q ≠ 0
h : 0 < p.degree
neg : LT.lt (α := WithBot ℕ) ⊥ 0
⊢ ¬p.degree = ⊥

Tactic:
refine (lt_trans ?_ h).ne'

Premises used: lt_trans, LT.lt.ne'
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p.Monic
q : R[X]
hq : q ≠ 0
h : 0 < p.degree
⊢ LT.lt (α := WithBot ℕ) ⊥ 0

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p.Monic
q : R[X]
hq : q ≠ 0
pos : ∀ (h : p = 1), p * q ≠ 0
neg : ∀ (h : ¬p = 1), p * q ≠ 0
⊢ p * q ≠ 0

Tactic:
by_cases h : p = 1
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p.Monic
q : R[X]
hq : q ≠ 0
h : p = 1
⊢ p * q ≠ 0

Tactic:
simpa [h]
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p.Monic
q : R[X]
hq : q ≠ 0
h : ¬p = 1
neg : ¬q = 0 ∧ ¬p.degree = ⊥
⊢ p * q ≠ 0

Tactic:
rw [Ne, ← degree_eq_bot, hp.degree_mul_comm, hp.degree_mul, WithBot.add_eq_bot, not_or,
    degree_eq_bot]

Premises used: Ne, not_or, Polynomial.Monic.degree_mul, Polynomial.Monic.degree_mul_comm, Polynomial.degree_eq_bot, WithBot.add_eq_bot
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : p.Monic
q : R[X]
pos : ∀ (hq : q = 0), (p * q).natDegree < p.natDegree ↔ p ≠ 1 ∧ q = 0
neg : ∀ (hq : ¬q = 0), (p * q).natDegree < p.natDegree ↔ p ≠ 1 ∧ q = 0
⊢ (p * q).natDegree < p.natDegree ↔ p ≠ 1 ∧ q = 0

Tactic:
by_cases hq : q = 0
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : p.Monic
q : R[X]
hq : q = 0
this : 0 < p.natDegree ↔ p.natDegree ≠ 0
⊢ (p * q).natDegree < p.natDegree ↔ p ≠ 1 ∧ q = 0

Tactic:
simp [hq, ← h.natDegree_eq_zero, iffComm]

Premises used: Polynomial.Monic.natDegree_eq_zero, iffComm
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : p.Monic
q : R[X]
hq : q = 0
pos : 0 < p.natDegree ↔ p.natDegree ≠ 0
⊢ (p * q).natDegree < p.natDegree ↔ p ≠ 1 ∧ q = 0

Tactic:
suffices 0 < p.natDegree ↔ p.natDegree ≠ 0 by simp [hq, ← h.natDegree_eq_zero, iffComm]
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : p.Monic
q : R[X]
hq : q = 0
⊢ 0 < p.natDegree ↔ p.natDegree ≠ 0

Tactic:
⟨fun h => h.ne', fun h => lt_of_le_of_ne (Nat.zero_le _) h.symm⟩

Premises used: Nat.zero_le, Ne.symm, LT.lt.ne', Iff.intro, Polynomial.natDegree, lt_of_le_of_ne
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : p.Monic
q : R[X]
hq : q = 0
⊢ 0 < p.natDegree ↔ p.natDegree ≠ 0

Tactic:
exact ⟨fun h => h.ne', fun h => lt_of_le_of_ne (Nat.zero_le _) h.symm⟩
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : p.Monic
q : R[X]
hq : ¬q = 0
⊢ (p * q).natDegree < p.natDegree ↔ p ≠ 1 ∧ q = 0

Tactic:
simp [h.natDegree_mul', hq]

Premises used: Polynomial.Monic.natDegree_mul'
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : p.Monic
q : R[X]
pos : ∀ (hq : q = 0), p * q = 0 ↔ q = 0
neg : ∀ (hq : ¬q = 0), p * q = 0 ↔ q = 0
⊢ p * q = 0 ↔ q = 0

Tactic:
by_cases hq : q = 0
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : p.Monic
q : R[X]
hq : q = 0
⊢ p * q = 0 ↔ q = 0

Tactic:
simp [h.mul_right_ne_zero, hq]

Premises used: Polynomial.Monic.mul_right_ne_zero
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : p.Monic
q : R[X]
hq : ¬q = 0
⊢ p * q = 0 ↔ q = 0

Tactic:
simp [h.mul_right_ne_zero, hq]

Premises used: Polynomial.Monic.mul_right_ne_zero
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : p.Monic
q : R[X]
pos : ∀ (hq : q = 0), q * p = 0 ↔ q = 0
neg : ∀ (hq : ¬q = 0), q * p = 0 ↔ q = 0
⊢ q * p = 0 ↔ q = 0

Tactic:
by_cases hq : q = 0
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : p.Monic
q : R[X]
hq : q = 0
⊢ q * p = 0 ↔ q = 0

Tactic:
simp [h.mul_left_ne_zero, hq]

Premises used: Polynomial.Monic.mul_left_ne_zero
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : p.Monic
q : R[X]
hq : ¬q = 0
⊢ q * p = 0 ↔ q = 0

Tactic:
simp [h.mul_left_ne_zero, hq]

Premises used: Polynomial.Monic.mul_left_ne_zero
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u_1
inst : Ring R
p : R[X]
hp : p.Monic
left : IsLeftRegular p
right : IsRightRegular p
⊢ IsRegular p

Tactic:
constructor
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u_1
inst : Ring R
p : R[X]
hp : p.Monic
q r : R[X]
h : p * q = p * r
left : q - r = 0
left₁ : p * (q - r) = 0
left₂ : p * q - p * r = 0
left₃ : p * r - p * r = 0
left₄ left₅ : Eq.{u_1 + 1} (α := R[X]) 0 0
⊢ q = r

Tactic:
rw [← sub_eq_zero, ← hp.mul_right_eq_zero_iff, mul_sub, h, sub_self]

Premises used: mul_sub, sub_self, sub_eq_zero, Polynomial.Monic.mul_right_eq_zero_iff
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u_1
inst : Ring R
p : R[X]
hp : p.Monic
q r : R[X]
h : q * p = r * p
right : q - r = 0
right₁ : (q - r) * p = 0
right₂ : q * p - r * p = 0
right₃ : r * p - r * p = 0
right₄ right₅ : Eq.{u_1 + 1} (α := R[X]) 0 0
⊢ q = r

Tactic:
rw [← sub_eq_zero, ← hp.mul_left_eq_zero_iff, sub_mul, h, sub_self]

Premises used: sub_self, sub_eq_zero, sub_mul, Polynomial.Monic.mul_left_eq_zero_iff
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
S : Type u_1
inst_1 : SMulZeroClass S R
k : S
p : R[X]
h : IsSMulRegular R k
⊢ (k • p).degree = p.degree

Tactic:
le_antisymm ?_ ?_

Premises used: le_antisymm
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
S : Type u_1
inst_1 : SMulZeroClass S R
k : S
p : R[X]
h : IsSMulRegular R k
refine_1 : (k • p).degree ≤ p.degree
refine_2 : p.degree ≤ (k • p).degree
⊢ (k • p).degree = p.degree

Tactic:
refine le_antisymm ?_ ?_

Premises used: le_antisymm
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
S : Type u_1
inst_1 : SMulZeroClass S R
k : S
p : R[X]
h : IsSMulRegular R k
refine_1 : ∀ (m : ℕ), p.degree < (↑m : WithBot ℕ) → (k • p).coeff m = 0
⊢ (k • p).degree ≤ p.degree

Tactic:
rw [degree_le_iff_coeff_zero]

Premises used: Polynomial.degree_le_iff_coeff_zero
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
S : Type u_1
inst_1 : SMulZeroClass S R
k : S
p : R[X]
h : IsSMulRegular R k
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.Monic
Goal:
R : Type u
inst : Semiring R
S : Type u_1
inst_1 : SMulZeroClass S R
k : S
p : R[X]
h : IsSMulRegular R k
m : ℕ
hm : ∀ (m_1 : ℕ), m ≤ m_1 → p.coeff m_1 = 0
⊢ (k • p).coeff m = 0

Tactic:
simp [hm m le_rfl]

Premises used: le_rfl
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
S : Type u_1
inst_1 : SMulZeroClass S R
k : S
p : R[X]
h : IsSMulRegular R k
refine_2 : ∀ (m : ℕ), (k • p).degree < (↑m : WithBot ℕ) → p.coeff m = 0
⊢ p.degree ≤ (k • p).degree

Tactic:
rw [degree_le_iff_coeff_zero]

Premises used: Polynomial.degree_le_iff_coeff_zero
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
S : Type u_1
inst_1 : SMulZeroClass S R
k : S
p : R[X]
h : IsSMulRegular R k
m : ℕ
hm : (k • p).degree < (↑m : WithBot ℕ)
⊢ ∀ (m_1 : ℕ), m ≤ m_1 → (k • 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.Monic
Goal:
R : Type u
inst : Semiring R
S : Type u_1
inst_1 : SMulZeroClass S R
k : S
p : R[X]
h : IsSMulRegular R k
m : ℕ
hm : ∀ (m_1 : ℕ), m ≤ m_1 → (k • p).coeff m_1 = 0
⊢ p.coeff m = 0

Tactic:
h ?_
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
S : Type u_1
inst_1 : SMulZeroClass S R
k : S
p : R[X]
h : IsSMulRegular R k
m : ℕ
hm : ∀ (m_1 : ℕ), m ≤ m_1 → (k • p).coeff m_1 = 0
refine_2 : Eq.{u + 1} (α := R) ((fun (x : R) ↦ k • x) (p.coeff m)) ((fun (x : R) ↦ k • x) 0)
⊢ p.coeff m = 0

Tactic:
refine h ?_
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
S : Type u_1
inst_1 : SMulZeroClass S R
k : S
p : R[X]
h : IsSMulRegular R k
m : ℕ
hm : ∀ (m_1 : ℕ), m ≤ m_1 → (k • p).coeff m_1 = 0
⊢ Eq.{u + 1} (α := R) ((fun (x : R) ↦ k • x) (p.coeff m)) ((fun (x : R) ↦ k • x) 0)

Tactic:
simpa using hm m le_rfl

Premises used: le_rfl
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
S : Type u_1
inst_1 : SMulZeroClass S R
k : S
p : R[X]
h : IsSMulRegular R k
pos : ∀ (hp : p = 0), (k • p).natDegree = p.natDegree
neg : ∀ (hp : ¬p = 0), (k • p).natDegree = p.natDegree
⊢ (k • p).natDegree = p.natDegree

Tactic:
by_cases hp : p = 0
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
S : Type u_1
inst_1 : SMulZeroClass S R
k : S
p : R[X]
h : IsSMulRegular R k
hp : p = 0
⊢ (k • p).natDegree = p.natDegree

Tactic:
simp [hp]
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
S : Type u_1
inst_1 : SMulZeroClass S R
k : S
p : R[X]
h : IsSMulRegular R k
hp : ¬p = 0
neg : k • p ≠ 0
⊢ (k • p).natDegree = p.natDegree

Tactic:
rw [← Nat.cast_inj (R := WithBot ℕ), ← degree_eq_natDegree hp, ← degree_eq_natDegree,
    degree_smul_of_smul_regular p h]

Premises used: Polynomial.degree_smul_of_smul_regular, Polynomial.degree_eq_natDegree, Nat.cast_inj
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
S : Type u_1
inst_1 : SMulZeroClass S R
k : S
p : R[X]
h : IsSMulRegular R k
hp : ¬p = 0
neg : ∀ (hp : k • p = 0), p = 0
⊢ k • p ≠ 0

Tactic:
contrapose hp
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
S : Type u_1
inst_1 : SMulZeroClass S R
k : S
p : R[X]
h : IsSMulRegular R k
hp : k • p = 0
⊢ k • p = HSMul.hSMul (β := R[X]) k 0

Tactic:
rw [← smul_zero k] at hp

Premises used: smul_zero
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
S : Type u_1
inst_1 : SMulZeroClass S R
k : S
p : R[X]
h : IsSMulRegular R k
hp : k • p = HSMul.hSMul (β := R[X]) k 0
⊢ p = 0

Tactic:
h.polynomial hp

Premises used: IsSMulRegular.polynomial
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
S : Type u_1
inst_1 : SMulZeroClass S R
k : S
p : R[X]
h : IsSMulRegular R k
hp : k • p = HSMul.hSMul (β := R[X]) k 0
⊢ p = 0

Tactic:
exact h.polynomial hp

Premises used: IsSMulRegular.polynomial
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
S : Type u_1
inst_1 : SMulZeroClass S R
k : S
p : R[X]
h : IsSMulRegular R k
rw : (k • p).coeff (k • p).natDegree = k • p.leadingCoeff
rw₁ : (k • p).coeff (k • p).natDegree = k • p.coeff p.natDegree
rw₂ : k • p.coeff (k • p).natDegree = k • p.coeff p.natDegree
rw₃ rw₄ : k • p.coeff p.natDegree = k • p.coeff p.natDegree
⊢ (k • p).leadingCoeff = k • p.leadingCoeff

Tactic:
rw [Polynomial.leadingCoeff, Polynomial.leadingCoeff, coeff_smul,
    natDegree_smul_of_smul_regular p h]

Premises used: Polynomial.natDegree_smul_of_smul_regular, Polynomial.leadingCoeff, Polynomial.coeff_smul
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : IsUnit p.leadingCoeff
rw : (↑h.unit⁻¹ : R) • p.leadingCoeff = 1
⊢ (h.unit⁻¹ • p).Monic

Tactic:
rw [Monic.def, leadingCoeff_smul_of_smul_regular _ (isSMulRegular_of_group _), Units.smul_def]

Premises used: Polynomial.leadingCoeff_smul_of_smul_regular, Units.smul_def, Polynomial.Monic.def
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : IsUnit p.leadingCoeff
⊢ (↑h.unit⁻¹ : R) • p.leadingCoeff = 1

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : IsUnit p.leadingCoeff
q : R[X]
mp : p * q = 0 → q = 0
mpr : q = 0 → p * q = 0
⊢ p * q = 0 ↔ q = 0

Tactic:
constructor
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : IsUnit p.leadingCoeff
q : R[X]
hp : p * q = 0
⊢ h.unit⁻¹ • (p * q) = 0

Tactic:
rw [← smul_eq_zero_iff_eq h.unit⁻¹] at hp

Premises used: smul_eq_zero_iff_eq, Inv.inv, IsUnit.unit
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : IsUnit p.leadingCoeff
q : R[X]
hp : h.unit⁻¹ • (p * q) = 0
a : ∀ (n : ℕ), (h.unit⁻¹ • (p * q)).coeff n = (h.unit⁻¹ • p * q).coeff n
⊢ h.unit⁻¹ • (p * q) = h.unit⁻¹ • p * q

Tactic:
ext
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : IsUnit p.leadingCoeff
q : R[X]
hp : h.unit⁻¹ • (p * q) = 0
n : ℕ
a :
  Eq.{u + 1} (α := R) (∑ i ∈ @antidiagonal _ Nat.instAddMonoid _ n, (↑h.unit⁻¹ : R) * (p.coeff i.1 * q.coeff i.2))
    (∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ n, (↑h.unit⁻¹ : R) * p.coeff x.1 * q.coeff x.2)
⊢ (h.unit⁻¹ • (p * q)).coeff n = (h.unit⁻¹ • p * q).coeff n

Tactic:
simp only [Units.smul_def, coeff_smul, coeff_mul, smul_eq_mul, mul_sum]

Premises used: Finset.mul_sum, Polynomial.coeff_mul, Polynomial.coeff_smul, Units.smul_def, smul_eq_mul
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : IsUnit p.leadingCoeff
q : R[X]
hp : h.unit⁻¹ • (p * q) = 0
n : ℕ
⊢ Eq.{u + 1} (α := R) (∑ i ∈ @antidiagonal _ Nat.instAddMonoid _ n, (↑h.unit⁻¹ : R) * (p.coeff i.1 * q.coeff i.2))
    (∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ n, (↑h.unit⁻¹ : R) * p.coeff x.1 * q.coeff x.2)

Tactic:
sum_congr rfl fun x _ => ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : IsUnit p.leadingCoeff
q : R[X]
hp : h.unit⁻¹ • (p * q) = 0
n : ℕ
a :
  ∀ x ∈ @antidiagonal _ Nat.instAddMonoid _ n,
    (↑h.unit⁻¹ : R) * (p.coeff x.1 * q.coeff x.2) = (↑h.unit⁻¹ : R) * p.coeff x.1 * q.coeff x.2
⊢ Eq.{u + 1} (α := R) (∑ i ∈ @antidiagonal _ Nat.instAddMonoid _ n, (↑h.unit⁻¹ : R) * (p.coeff i.1 * q.coeff i.2))
    (∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ n, (↑h.unit⁻¹ : R) * p.coeff x.1 * q.coeff x.2)

Tactic:
refine sum_congr rfl fun x _ => ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : IsUnit p.leadingCoeff
q : R[X]
hp : h.unit⁻¹ • (p * q) = 0
n : ℕ
x : ℕ × ℕ
h_1 : x ∈ @antidiagonal _ Nat.instAddMonoid _ n
a a₁ : (↑h.unit⁻¹ : R) * p.coeff x.1 * q.coeff x.2 = (↑h.unit⁻¹ : R) * p.coeff x.1 * q.coeff x.2
⊢ (↑h.unit⁻¹ : R) * (p.coeff x.1 * q.coeff x.2) = (↑h.unit⁻¹ : R) * p.coeff x.1 * q.coeff x.2

Tactic:
rw [← mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : IsUnit p.leadingCoeff
q : R[X]
hp : h.unit⁻¹ • (p * q) = 0
⊢ h.unit⁻¹ • (p * q) = h.unit⁻¹ • p * q

Tactic:
have : h.unit⁻¹ • (p * q) = h.unit⁻¹ • p * q := by
      ext
      simp only [Units.smul_def, coeff_smul, coeff_mul, smul_eq_mul, mul_sum]
      refine sum_congr rfl fun x _ => ?_
      rw [← mul_assoc]
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : IsUnit p.leadingCoeff
q : R[X]
hp : h.unit⁻¹ • (p * q) = 0
this : h.unit⁻¹ • (p * q) = h.unit⁻¹ • p * q
mp : ∀ (hp : h.unit⁻¹ • p * q = 0) (this : h.unit⁻¹ • (p * q) = h.unit⁻¹ • p * q), (h.unit⁻¹ • p).Monic
⊢ q = 0

Tactic:
rwa [this, Monic.mul_right_eq_zero_iff] at hp

Premises used: Polynomial.Monic.mul_right_eq_zero_iff
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : IsUnit p.leadingCoeff
q : R[X]
hp : h.unit⁻¹ • p * q = 0
this : h.unit⁻¹ • (p * q) = h.unit⁻¹ • p * q
⊢ (h.unit⁻¹ • p).Monic

Tactic:
monic_of_isUnit_leadingCoeff_inv_smul _

Premises used: Polynomial.monic_of_isUnit_leadingCoeff_inv_smul
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : IsUnit p.leadingCoeff
q : R[X]
hp : h.unit⁻¹ • p * q = 0
this : h.unit⁻¹ • (p * q) = h.unit⁻¹ • p * q
⊢ (h.unit⁻¹ • p).Monic

Tactic:
exact monic_of_isUnit_leadingCoeff_inv_smul _

Premises used: Polynomial.monic_of_isUnit_leadingCoeff_inv_smul
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : IsUnit p.leadingCoeff
⊢ p * 0 = 0

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : IsUnit p.leadingCoeff
q : R[X]
mp : q * p = 0 → q = 0
mpr : q = 0 → q * p = 0
⊢ q * p = 0 ↔ q = 0

Tactic:
constructor
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : IsUnit p.leadingCoeff
q : R[X]
hp : q * p = 0
⊢ Eq.{u + 1} (α := R[X])
    ((fun (x : R[X]) ↦ HMul.hMul (β := R[X]) x ((C : (a : R) → R[X]) (↑h.unit⁻¹ : R) : R[X])) (q * p))
    ((fun (x : R[X]) ↦ HMul.hMul (β := R[X]) x ((C : (a : R) → R[X]) (↑h.unit⁻¹ : R) : R[X])) 0)

Tactic:
replace hp := congr_arg (· * C ↑h.unit⁻¹) hp