awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
inst : Semiring R
p : R[X]
a : R
inst_1 : NoZeroDivisors R
h₀ : ¬a = 0
⊢ (HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) a : R[X])).nextCoeff = p.nextCoeff * a

Tactic:
simp [h₀, nextCoeff, natDegree_mul_C]

Premises used: Polynomial.nextCoeff, Polynomial.natDegree_mul_C
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
inst : Ring R
p : R[X]
⊢ Nontrivial R

Tactic:
nontriviality R
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
inst : Ring R
p : R[X]
h : Nontrivial R
pos : ∀ (h : p = 0), (p.comp (-X)).leadingCoeff = HPow.hPow (α := R) (-1) p.natDegree * p.leadingCoeff
neg : ∀ (h : ¬p = 0), (p.comp (-X)).leadingCoeff = HPow.hPow (α := R) (-1) p.natDegree * p.leadingCoeff
⊢ (p.comp (-X)).leadingCoeff = HPow.hPow (α := R) (-1) p.natDegree * p.leadingCoeff

Tactic:
by_cases h : p = 0
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
inst : Ring R
p : R[X]
h_1 : Nontrivial R
h : p = 0
⊢ (p.comp (-X)).leadingCoeff = HPow.hPow (α := R) (-1) p.natDegree * p.leadingCoeff

Tactic:
simp [h]
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
inst : Ring R
p : R[X]
h_1 : Nontrivial R
h : ¬p = 0
neg :
  p.leadingCoeff * HPow.hPow (α := R) (leadingCoeff (-X)) p.natDegree =
    HPow.hPow (α := R) (-1) p.natDegree * p.leadingCoeff
neg₁ : natDegree.{u} (R := R) (-X) ≠ 0
neg₂ : p.leadingCoeff * HPow.hPow (α := R) (leadingCoeff (-X)) p.natDegree ≠ 0
⊢ (p.comp (-X)).leadingCoeff = HPow.hPow (α := R) (-1) p.natDegree * p.leadingCoeff

Tactic:
rw [Polynomial.leadingCoeff, natDegree_comp_eq_of_mul_ne_zero, coeff_comp_degree_mul_degree]

Premises used: Polynomial.natDegree_comp_eq_of_mul_ne_zero, Polynomial.leadingCoeff, Polynomial.coeff_comp_degree_mul_degree
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
inst : Ring R
p : R[X]
h_1 : Nontrivial R
h : ¬p = 0
⊢ p.leadingCoeff * HPow.hPow (α := R) (leadingCoeff (-X)) p.natDegree =
    HPow.hPow (α := R) (-1) p.natDegree * p.leadingCoeff

Tactic:
simp [((Commute.neg_one_left _).pow_left _).eq, h]

Premises used: Commute.pow_left, Commute.neg_one_left, Commute.eq
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
inst : Ring R
p : R[X]
h_1 : Nontrivial R
h : ¬p = 0
⊢ natDegree.{u} (R := R) (-X) ≠ 0

Tactic:
simp [((Commute.neg_one_left _).pow_left _).eq, h]

Premises used: Commute.pow_left, Commute.neg_one_left, Commute.eq
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
inst : Ring R
p : R[X]
h_1 : Nontrivial R
h : ¬p = 0
⊢ p.leadingCoeff * HPow.hPow (α := R) (leadingCoeff (-X)) p.natDegree ≠ 0

Tactic:
simp [((Commute.neg_one_left _).pow_left _).eq, h]

Premises used: Commute.pow_left, Commute.neg_one_left, Commute.eq
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
inst : Ring R
p : R[X]
⊢ p.comp (-X) = 0 ↔ p = 0

Tactic:
simp [← leadingCoeff_eq_zero]

Premises used: Polynomial.leadingCoeff_eq_zero
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
p q : R[X]
h : p = 0
⊢ p.comp q = 0

Tactic:
simp [h]
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
p q : R[X]
h : eval (q.coeff 0) p = 0 ∧ q = (C : (a : R) → R[X]) (q.coeff 0)
rw : p.comp ((C : (a : R) → R[X]) (q.coeff 0)) = 0
rw₁ : Eq (α := R[X]) ((C : (a : R) → R[X]) (eval (q.coeff 0) p) : R[X]) (0 : R[X])
rw₂ : Eq.{u + 1} (α := R[X]) ((C : (a : R) → R[X]) 0) 0
rw₃ rw₄ : Eq.{u + 1} (α := R[X]) 0 0
⊢ p.comp q = 0

Tactic:
rw [h.2, comp_C, h.1, C_0]

Premises used: Polynomial.C_0, Polynomial.comp_C, And.right, And.left
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
p q : R[X]
refine : ∀ (h : p.comp q = 0), p = 0 ∨ eval (q.coeff 0) p = 0 ∧ q = (C : (a : R) → R[X]) (q.coeff 0)
⊢ p.comp q = 0 ↔ p = 0 ∨ eval (q.coeff 0) p = 0 ∧ q = (C : (a : R) → R[X]) (q.coeff 0)

Tactic:
refine ⟨fun h ↦ ?_, Or.rec (fun h ↦ by simp [h]) fun h ↦ by rw [h.2, comp_C, h.1, C_0]⟩
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
p q : R[X]
h : p.comp q = 0
rw : p.natDegree * q.natDegree = 0
rw₁ : (p.comp q).natDegree = 0
rw₂ : natDegree.{u} (R := R) 0 = 0
rw₃ rw₄ : Eq (α := ℕ) 0 0
⊢ p.natDegree = 0 ∨ q.natDegree = 0

Tactic:
rw [← mul_eq_zero, ← natDegree_comp, h, natDegree_zero]

Premises used: Polynomial.natDegree_comp, Polynomial.natDegree_zero, mul_eq_zero
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
p q : R[X]
h : p.comp q = 0
⊢ p.natDegree = 0 ∨ q.natDegree = 0

Tactic:
have key : p.natDegree = 0 ∨ q.natDegree = 0 := by
    rw [← mul_eq_zero, ← natDegree_comp, h, natDegree_zero]
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
p q : R[X]
h : p.comp q = 0
key : p.natDegree = 0 ∨ q.natDegree = 0
inl :
  ∀ (key : p = (C : (a : R) → R[X]) (p.coeff 0)), p = 0 ∨ eval (q.coeff 0) p = 0 ∧ q = (C : (a : R) → R[X]) (q.coeff 0)
inr :
  ∀ (key : q = (C : (a : R) → R[X]) (q.coeff 0)), p = 0 ∨ eval (q.coeff 0) p = 0 ∧ q = (C : (a : R) → R[X]) (q.coeff 0)
⊢ p = 0 ∨ eval (q.coeff 0) p = 0 ∧ q = (C : (a : R) → R[X]) (q.coeff 0)

Tactic:
obtain key | key := Or.imp eq_C_of_natDegree_eq_zero eq_C_of_natDegree_eq_zero key

Premises used: Polynomial.eq_C_of_natDegree_eq_zero, Or.imp
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
p q : R[X]
h : p.comp q = 0
key_1 : p.natDegree = 0 ∨ q.natDegree = 0
key : p = (C : (a : R) → R[X]) (p.coeff 0)
⊢ Eq (α := R[X]) ((C : (a : R) → R[X]) (p.coeff 0) : R[X]) (0 : R[X])

Tactic:
rw [key, C_comp] at h

Premises used: Polynomial.C_comp
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
p q : R[X]
h : p.comp q = 0
key_1 : p.natDegree = 0 ∨ q.natDegree = 0
key : p = (C : (a : R) → R[X]) (p.coeff 0)
h₁ : Eq (α := R[X]) ((C : (a : R) → R[X]) (p.coeff 0) : R[X]) (0 : R[X])
⊢ p.natDegree = 0 ∨ q.natDegree = 0

Tactic:
rw [key, C_comp] at h

Premises used: Polynomial.C_comp
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
p q : R[X]
h : p.comp q = 0
key_1 : p.natDegree = 0 ∨ q.natDegree = 0
key : p = (C : (a : R) → R[X]) (p.coeff 0)
h₁ : Eq (α := R[X]) ((C : (a : R) → R[X]) (p.coeff 0) : R[X]) (0 : R[X])
key₁ : p.natDegree = 0 ∨ q.natDegree = 0
⊢ p = (C : (a : R) → R[X]) (p.coeff 0)

Tactic:
rw [key, C_comp] at h

Premises used: Polynomial.C_comp
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
p q : R[X]
h : Eq (α := R[X]) ((C : (a : R) → R[X]) (p.coeff 0) : R[X]) (0 : R[X])
key_1 : p.natDegree = 0 ∨ q.natDegree = 0
key : p = (C : (a : R) → R[X]) (p.coeff 0)
⊢ p = 0 ∨ eval (q.coeff 0) p = 0 ∧ q = (C : (a : R) → R[X]) (q.coeff 0)

Tactic:
Or.inl (key.trans h)

Premises used: Or.inl, Eq.trans
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
p q : R[X]
h : Eq (α := R[X]) ((C : (a : R) → R[X]) (p.coeff 0) : R[X]) (0 : R[X])
key_1 : p.natDegree = 0 ∨ q.natDegree = 0
key : p = (C : (a : R) → R[X]) (p.coeff 0)
⊢ p = 0 ∨ eval (q.coeff 0) p = 0 ∧ q = (C : (a : R) → R[X]) (q.coeff 0)

Tactic:
exact Or.inl (key.trans h)

Premises used: Or.inl, Eq.trans
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
p q : R[X]
h : p.comp q = 0
key_1 : p.natDegree = 0 ∨ q.natDegree = 0
key : q = (C : (a : R) → R[X]) (q.coeff 0)
⊢ eval (q.coeff 0) p = 0

Tactic:
rw [key, comp_C, C_eq_zero] at h

Premises used: Polynomial.C_eq_zero, Polynomial.comp_C
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
p q : R[X]
h : p.comp q = 0
key_1 : p.natDegree = 0 ∨ q.natDegree = 0
key : q = (C : (a : R) → R[X]) (q.coeff 0)
h₁ : eval (q.coeff 0) p = 0
⊢ p.natDegree = 0 ∨ q.natDegree = 0

Tactic:
rw [key, comp_C, C_eq_zero] at h

Premises used: Polynomial.C_eq_zero, Polynomial.comp_C
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
p q : R[X]
h : p.comp q = 0
key_1 : p.natDegree = 0 ∨ q.natDegree = 0
key : q = (C : (a : R) → R[X]) (q.coeff 0)
h₁ : eval (q.coeff 0) p = 0
key₁ : p.natDegree = 0 ∨ q.natDegree = 0
⊢ q = (C : (a : R) → R[X]) (q.coeff 0)

Tactic:
rw [key, comp_C, C_eq_zero] at h

Premises used: Polynomial.C_eq_zero, Polynomial.comp_C
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
p q : R[X]
h : eval (q.coeff 0) p = 0
key_1 : p.natDegree = 0 ∨ q.natDegree = 0
key : q = (C : (a : R) → R[X]) (q.coeff 0)
⊢ p = 0 ∨ eval (q.coeff 0) p = 0 ∧ q = (C : (a : R) → R[X]) (q.coeff 0)

Tactic:
Or.inr ⟨h, key⟩

Premises used: And.intro, Or.inr
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
p q : R[X]
h : eval (q.coeff 0) p = 0
key_1 : p.natDegree = 0 ∨ q.natDegree = 0
key : q = (C : (a : R) → R[X]) (q.coeff 0)
⊢ p = 0 ∨ eval (q.coeff 0) p = 0 ∧ q = (C : (a : R) → R[X]) (q.coeff 0)

Tactic:
exact Or.inr ⟨h, key⟩

Premises used: Or.inr
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
p q : R[X]
hq : 0 < q.degree
inl : (comp 0 q).degree = degree.{u} (R := R) 0 * q.degree
inr : ∀ (hp : p ≠ 0), (p.comp q).degree = p.degree * q.degree
⊢ (p.comp q).degree = p.degree * q.degree

Tactic:
rcases eq_or_ne p 0 with rfl | hp

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
q : R[X]
hq : 0 < q.degree
inl : Eq (α := WithBot ℕ) ⊥ (if q.degree = 0 then 0 else ⊥)
⊢ (comp 0 q).degree = degree.{u} (R := R) 0 * q.degree

Tactic:
rw [zero_comp, degree_zero, WithBot.bot_mul']

Premises used: Polynomial.zero_comp, Polynomial.degree_zero, WithBot.bot_mul'
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
q : R[X]
hq : 0 < q.degree
⊢ Eq (α := WithBot ℕ) ⊥ (if q.degree = 0 then 0 else ⊥)

Tactic:
simp [hq.ne']

Premises used: LT.lt.ne'
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
p q : R[X]
hq : 0 < q.degree
hp : p ≠ 0
inr : (p.comp q).degree = (↑(p.comp q).natDegree : WithBot ℕ)
⊢ (p.comp q).degree = p.degree * q.degree

Tactic:
rw [degree_eq_natDegree hp, degree_eq_natDegree (ne_zero_of_degree_gt hq), ← Nat.cast_mul,
    ← natDegree_comp]

Premises used: Polynomial.degree_eq_natDegree, Polynomial.ne_zero_of_degree_gt, Polynomial.natDegree_comp, Nat.cast_mul
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
p q : R[X]
hq : 0 < q.degree
hp : p ≠ 0
inr : p.comp q ≠ 0
⊢ (p.comp q).degree = (↑(p.comp q).natDegree : WithBot ℕ)

Tactic:
apply degree_eq_natDegree

Premises used: Polynomial.degree_eq_natDegree
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
p q : R[X]
hq : 0 < q.degree
hp : p ≠ 0
inr : ¬eval (q.coeff 0) p = 0 ∨ ¬q.degree ≤ 0
⊢ p.comp q ≠ 0

Tactic:
simp_rw [Ne, comp_eq_zero_iff, hp, false_or, not_and_or, ← degree_le_zero_iff]

Premises used: Ne, false_or, Polynomial.comp_eq_zero_iff, not_and_or, Polynomial.degree_le_zero_iff
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
p q : R[X]
hq : 0 < q.degree
hp : p ≠ 0
⊢ ¬eval (q.coeff 0) p = 0 ∨ ¬q.degree ≤ 0

Tactic:
simp [hq]
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
inst : Ring R
p : R[X]
h : Nontrivial R
inl : degree.{u} (R := R) (comp 0 (-X)) = degree.{u} (R := R) 0
inr : ∀ (hp : p ≠ 0), (p.comp (-X)).degree = p.degree
⊢ (p.comp (-X)).degree = p.degree

Tactic:
rcases eq_or_ne p 0 with rfl | hp

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
inst : Ring R
h : Nontrivial R
inl inl₁ : degree.{u} (R := R) 0 = degree.{u} (R := R) 0
⊢ degree.{u} (R := R) (comp 0 (-X)) = degree.{u} (R := R) 0

Tactic:
rw [zero_comp]

Premises used: Polynomial.zero_comp
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
inst : Ring R
p : R[X]
h : Nontrivial R
hp : p ≠ 0
⊢ p.comp (-X) ≠ 0

Tactic:
simp [hp]
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
inst : Ring R
p : R[X]
h : Nontrivial R
hp : p ≠ 0
⊢ p.leadingCoeff * HPow.hPow (α := R) (leadingCoeff (-X)) p.natDegree ≠ 0

Tactic:
simp [hp]
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
inst : Ring R
p : R[X]
h : Nontrivial R
hp : p ≠ 0
inr : (↑(p.comp (-X)).natDegree : WithBot ℕ) = p.degree
inr₁ : Eq (α := WithBot ℕ) (↑(p.comp (-X)).natDegree : WithBot ℕ) (↑p.natDegree : WithBot ℕ)
inr₂ : (p.comp (-X)).natDegree = p.natDegree
inr₃ : p.natDegree * natDegree.{u} (R := R) (-X) = p.natDegree
inr₄ : p.natDegree * natDegree.{u} (R := R) X = p.natDegree
inr₅ : p.natDegree * 1 = p.natDegree
inr₆ inr₇ : p.natDegree = p.natDegree
⊢ (p.comp (-X)).degree = p.degree

Tactic:
rw [degree_eq_natDegree (by simp [hp]), degree_eq_natDegree hp, Nat.cast_inj,
    natDegree_comp_eq_of_mul_ne_zero (by simp [hp]), natDegree_neg, natDegree_X, mul_one]

Premises used: Polynomial.natDegree_X, Polynomial.degree_eq_natDegree, Polynomial.natDegree_comp_eq_of_mul_ne_zero, Nat.cast_inj, Polynomial.natDegree_neg, mul_one
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
K : Type u_1
inst : DivisionRing K
p : K[X]
pos :
  ∀ (hp0 : p = 0), Irreducible (HMul.hMul (β := K[X]) p ((C : (a : K) → K[X]) p.leadingCoeff⁻¹ : K[X])) ↔ Irreducible p
neg :
  ∀ (hp0 : ¬p = 0), Irreducible (HMul.hMul (β := K[X]) p ((C : (a : K) → K[X]) p.leadingCoeff⁻¹ : K[X])) ↔ Irreducible p
⊢ Irreducible (HMul.hMul (β := K[X]) p ((C : (a : K) → K[X]) p.leadingCoeff⁻¹ : K[X])) ↔ Irreducible p

Tactic:
by_cases hp0 : p = 0
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
K : Type u_1
inst : DivisionRing K
p : K[X]
hp0 : p = 0
⊢ Irreducible (HMul.hMul (β := K[X]) p ((C : (a : K) → K[X]) p.leadingCoeff⁻¹ : K[X])) ↔ Irreducible p

Tactic:
simp [hp0]
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
K : Type u_1
inst : DivisionRing K
p : K[X]
hp0 : ¬p = 0
⊢ Irreducible (HMul.hMul (β := K[X]) p ((C : (a : K) → K[X]) p.leadingCoeff⁻¹ : K[X])) ↔ Irreducible p

Tactic:
irreducible_mul_isUnit
    (isUnit_C.mpr (IsUnit.mk0 _ (inv_ne_zero (leadingCoeff_ne_zero.mpr hp0))))

Premises used: Iff.mpr, Polynomial.isUnit_C, Polynomial.leadingCoeff_ne_zero, IsUnit.mk0, inv_ne_zero, irreducible_mul_isUnit
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
K : Type u_1
inst : DivisionRing K
p : K[X]
hp0 : ¬p = 0
⊢ Irreducible (HMul.hMul (β := K[X]) p ((C : (a : K) → K[X]) p.leadingCoeff⁻¹ : K[X])) ↔ Irreducible p

Tactic:
exact irreducible_mul_isUnit
    (isUnit_C.mpr (IsUnit.mk0 _ (inv_ne_zero (leadingCoeff_ne_zero.mpr hp0))))

Premises used: Iff.mpr, Polynomial.isUnit_C, Polynomial.leadingCoeff_ne_zero, IsUnit.mk0, inv_ne_zero, irreducible_mul_isUnit
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
K : Type u_1
inst : DivisionRing K
p q : K[X]
hp0 : p ≠ 0
⊢ q ∣ HMul.hMul (β := K[X]) p ((C : (a : K) → K[X]) p.leadingCoeff⁻¹ : K[X]) ↔ q ∣ p

Tactic:
simp [hp0]
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
K : Type u_1
inst : DivisionRing K
p : K[X]
h : p ≠ 0
rw : (HMul.hMul (β := K[X]) p ((C : (a : K) → K[X]) p.leadingCoeff⁻¹ : K[X])).leadingCoeff = 1
rw₁ : p.leadingCoeff * leadingCoeff ((C : (a : K) → K[X]) p.leadingCoeff⁻¹) = 1
rw₂ : p.leadingCoeff * p.leadingCoeff⁻¹ = 1
rw₃ rw₄ : Eq.{u_1 + 1} (α := K) 1 1
⊢ (HMul.hMul (β := K[X]) p ((C : (a : K) → K[X]) p.leadingCoeff⁻¹ : K[X])).Monic

Tactic:
rw [Monic, leadingCoeff_mul, leadingCoeff_C,
    mul_inv_cancel₀ (show leadingCoeff p ≠ 0 from mt leadingCoeff_eq_zero.1 h)]

Premises used: mul_inv_cancel₀, Polynomial.leadingCoeff_mul, mt, Polynomial.Monic, Iff.mp, Polynomial.leadingCoeff_C, Polynomial.leadingCoeff_eq_zero
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
K : Type u_1
inst : DivisionRing K
p : K[X]
hp0 : p ≠ 0
⊢ degree.{u_1} (R := K) ((C : (a : K) → K[X]) p.leadingCoeff⁻¹) = 0

Tactic:
simp [hp0]
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
K : Type u_1
inst : DivisionRing K
p q : K[X]
h : q ≠ 0
⊢ q.leadingCoeff⁻¹ ≠ 0

Tactic:
have h₁ : (leadingCoeff q)⁻¹ ≠ 0 := inv_ne_zero (mt leadingCoeff_eq_zero.1 h)
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
K : Type u_1
inst : DivisionRing K
p q : K[X]
h : q ≠ 0
h₁ : q.leadingCoeff⁻¹ ≠ 0
rw rw₁ : p.degree = p.degree
⊢ (HMul.hMul (β := K[X]) p ((C : (a : K) → K[X]) q.leadingCoeff⁻¹ : K[X])).degree = p.degree

Tactic:
rw [degree_mul_C h₁]

Premises used: Polynomial.degree_mul_C
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
K : Type u_1
inst : DivisionRing K
p q : K[X]
h : q ≠ 0
⊢ (HMul.hMul (β := K[X]) p ((C : (a : K) → K[X]) q.leadingCoeff⁻¹ : K[X])).natDegree = p.natDegree

Tactic:
natDegree_eq_of_degree_eq (degree_mul_leadingCoeff_inv _ h)

Premises used: Polynomial.degree_mul_leadingCoeff_inv, Polynomial.natDegree_eq_of_degree_eq
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
K : Type u_1
inst : DivisionRing K
p : K[X]
pos : ∀ (hp : p = 0), (HMul.hMul (β := K[X]) p ((C : (a : K) → K[X]) p.leadingCoeff⁻¹ : K[X])).degree = p.degree
neg : ∀ (hp : ¬p = 0), (HMul.hMul (β := K[X]) p ((C : (a : K) → K[X]) p.leadingCoeff⁻¹ : K[X])).degree = p.degree
⊢ (HMul.hMul (β := K[X]) p ((C : (a : K) → K[X]) p.leadingCoeff⁻¹ : K[X])).degree = p.degree

Tactic:
by_cases hp : p = 0
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
K : Type u_1
inst : DivisionRing K
p : K[X]
hp : p = 0
⊢ (HMul.hMul (β := K[X]) p ((C : (a : K) → K[X]) p.leadingCoeff⁻¹ : K[X])).degree = p.degree

Tactic:
simp [hp]
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
K : Type u_1
inst : DivisionRing K
p : K[X]
hp : ¬p = 0
⊢ (HMul.hMul (β := K[X]) p ((C : (a : K) → K[X]) p.leadingCoeff⁻¹ : K[X])).degree = p.degree

Tactic:
degree_mul_leadingCoeff_inv _ hp

Premises used: Polynomial.degree_mul_leadingCoeff_inv
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
K : Type u_1
inst : DivisionRing K
p : K[X]
hp : ¬p = 0
⊢ (HMul.hMul (β := K[X]) p ((C : (a : K) → K[X]) p.leadingCoeff⁻¹ : K[X])).degree = p.degree

Tactic:
exact degree_mul_leadingCoeff_inv _ hp

Premises used: Polynomial.degree_mul_leadingCoeff_inv
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
K : Type u_1
inst : DivisionRing K
p : K[X]
⊢ (HMul.hMul (β := K[X]) p ((C : (a : K) → K[X]) p.leadingCoeff⁻¹ : K[X])).natDegree = p.natDegree

Tactic:
natDegree_eq_of_degree_eq (degree_mul_leadingCoeff_self_inv _)

Premises used: Polynomial.degree_mul_leadingCoeff_self_inv, Polynomial.natDegree_eq_of_degree_eq
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
K : Type u_1
inst : DivisionRing K
p : K[X]
rw : (HMul.hMul (β := K[X]) p ((C : (a : K) → K[X]) p.leadingCoeff⁻¹ : K[X])).degree = p.degree
rw₁ rw₂ : p.degree = p.degree
⊢ p.degree + degree.{u_1} (R := K) ((C : (a : K) → K[X]) p.leadingCoeff⁻¹) = p.degree

Tactic:
rw [← degree_mul, degree_mul_leadingCoeff_self_inv]

Premises used: Polynomial.degree_mul_leadingCoeff_self_inv, Polynomial.degree_mul
-- Module: Mathlib.Algebra.Polynomial.Degree.Monomial
Goal:
R : Type u
n : ℕ
inst : Semiring R
p : R[X]
hf : p.natDegree ≤ n
hn : p.coeff n = 0
zero : ∀ (hf : p.natDegree ≤ 0) (hn : p.coeff 0 = 0), p.natDegree ≤ HSub.hSub (α := ℕ) 0 1
succ : ∀ (n : ℕ) (hf : p.natDegree ≤ n + 1) (hn : p.coeff (n + 1) = 0), p.natDegree ≤ n + 1 - 1
⊢ p.natDegree ≤ n - 1

Tactic:
obtain _ | n := n
-- Module: Mathlib.Algebra.Polynomial.Degree.Monomial
Goal:
R : Type u
inst : Semiring R
p : R[X]
hf : p.natDegree ≤ 0
hn : p.coeff 0 = 0
⊢ p.natDegree ≤ HSub.hSub (α := ℕ) 0 1

Tactic:
hf
-- Module: Mathlib.Algebra.Polynomial.Degree.Monomial
Goal:
R : Type u
inst : Semiring R
p : R[X]
hf : p.natDegree ≤ 0
hn : p.coeff 0 = 0
⊢ p.natDegree ≤ HSub.hSub (α := ℕ) 0 1

Tactic:
exact hf
-- Module: Mathlib.Algebra.Polynomial.Degree.Monomial
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
hf : p.natDegree ≤ n + 1
hn : p.coeff (n + 1) = 0
⊢ p.natDegree ≤ n + 1 - 1

Tactic:
(Nat.le_succ_iff_eq_or_le.1 hf).resolve_left fun h ↦ ?_

Premises used: Or.resolve_left, Nat.le_succ_iff_eq_or_le, Iff.mp, Nat.pred
-- Module: Mathlib.Algebra.Polynomial.Degree.Monomial
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
hf : p.natDegree ≤ n + 1
hn : p.coeff (n + 1) = 0
succ : ∀ (h : p.natDegree = n.succ), False
⊢ p.natDegree ≤ n + 1 - 1

Tactic:
refine (Nat.le_succ_iff_eq_or_le.1 hf).resolve_left fun h ↦ ?_

Premises used: Or.resolve_left, Nat.le_succ_iff_eq_or_le, Iff.mp
-- Module: Mathlib.Algebra.Polynomial.Degree.Monomial
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
hf : p.natDegree ≤ n + 1
hn : p.coeff (n + 1) = 0
h : p.natDegree = n.succ
⊢ p = 0

Tactic:
rw [← Nat.succ_eq_add_one, ← h, coeff_natDegree, leadingCoeff_eq_zero] at hn

Premises used: Nat.succ_eq_add_one, Polynomial.coeff_natDegree, Polynomial.leadingCoeff_eq_zero
-- Module: Mathlib.Algebra.Polynomial.Degree.Monomial
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
hf : p.natDegree ≤ n + 1
hn : p.coeff (n + 1) = 0
h : p.natDegree = n.succ
hn₁ : p = 0
⊢ p.natDegree = n.succ

Tactic:
rw [← Nat.succ_eq_add_one, ← h, coeff_natDegree, leadingCoeff_eq_zero] at hn

Premises used: Nat.succ_eq_add_one, Polynomial.coeff_natDegree, Polynomial.leadingCoeff_eq_zero
-- Module: Mathlib.Algebra.Polynomial.Degree.Monomial
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
hf : p.natDegree ≤ n + 1
hn : p = 0
h : p.natDegree = n.succ
⊢ False

Tactic:
simp_all
-- Module: Mathlib.Algebra.Polynomial.Degree.Monomial
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : #p.support ≤ 1
rcases :
  ∀ (n : ℕ) (a : R) (h : #(support.{u} (R := R) ((monomial n : (a : R) → R[X]) a)) ≤ 1),
    Eq (α := R[X])
      ((monomial (natDegree.{u} (R := R) ((monomial n : (a : R) → R[X]) a)) : (a : R) → R[X])
          (leadingCoeff ((monomial n : (a : R) → R[X]) a)) :
        R[X])
      ((monomial n : (a : R) → R[X]) a : R[X])
⊢ (monomial p.natDegree : (a : R) → R[X]) p.leadingCoeff = p

Tactic:
rcases card_support_le_one_iff_monomial.1 h with ⟨n, a, rfl⟩

Premises used: Iff.mp, Polynomial.card_support_le_one_iff_monomial, rfl
-- Module: Mathlib.Algebra.Polynomial.Degree.Monomial
Goal:
R : Type u
inst : Semiring R
n : ℕ
a : R
h : #(support.{u} (R := R) ((monomial n : (a : R) → R[X]) a)) ≤ 1
pos :
  ∀ (ha : a = 0),
    Eq (α := R[X])
      ((monomial (natDegree.{u} (R := R) ((monomial n : (a : R) → R[X]) a)) : (a : R) → R[X])
          (leadingCoeff ((monomial n : (a : R) → R[X]) a)) :
        R[X])
      ((monomial n : (a : R) → R[X]) a : R[X])
neg :
  ∀ (ha : ¬a = 0),
    Eq (α := R[X])
      ((monomial (natDegree.{u} (R := R) ((monomial n : (a : R) → R[X]) a)) : (a : R) → R[X])
          (leadingCoeff ((monomial n : (a : R) → R[X]) a)) :
        R[X])
      ((monomial n : (a : R) → R[X]) a : R[X])
⊢ Eq (α := R[X])
    ((monomial (natDegree.{u} (R := R) ((monomial n : (a : R) → R[X]) a)) : (a : R) → R[X])
        (leadingCoeff ((monomial n : (a : R) → R[X]) a)) :
      R[X])
    ((monomial n : (a : R) → R[X]) a : R[X])

Tactic:
by_cases ha : a = 0
-- Module: Mathlib.Algebra.Polynomial.Degree.Monomial
Goal:
R : Type u
inst : Semiring R
n : ℕ
a : R
h : #(support.{u} (R := R) ((monomial n : (a : R) → R[X]) a)) ≤ 1
ha : a = 0
⊢ Eq (α := R[X])
    ((monomial (natDegree.{u} (R := R) ((monomial n : (a : R) → R[X]) a)) : (a : R) → R[X])
        (leadingCoeff ((monomial n : (a : R) → R[X]) a)) :
      R[X])
    ((monomial n : (a : R) → R[X]) a : R[X])

Tactic:
simp [ha]