awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.RingDivision
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
p q : R[X]
pos : ∀ (hp : p = 0), (p * q).trailingDegree = p.trailingDegree + q.trailingDegree
neg : ∀ (hp : ¬p = 0), (p * q).trailingDegree = p.trailingDegree + q.trailingDegree
⊢ (p * q).trailingDegree = p.trailingDegree + q.trailingDegree

Tactic:
by_cases hp : p = 0
-- Module: Mathlib.Algebra.Polynomial.RingDivision
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
p q : R[X]
hp : p = 0
pos : (0 * q).trailingDegree = trailingDegree.{u} (R := R) 0 + q.trailingDegree
pos₁ : trailingDegree.{u} (R := R) 0 = trailingDegree.{u} (R := R) 0 + q.trailingDegree
pos₂ : ⊤ = ⊤ + q.trailingDegree
pos₃ pos₄ : Eq (α := ℕ∞) ⊤ ⊤
⊢ (p * q).trailingDegree = p.trailingDegree + q.trailingDegree

Tactic:
rw [hp, zero_mul, trailingDegree_zero, top_add]

Premises used: MulZeroClass.zero_mul, Polynomial.trailingDegree_zero, top_add
-- Module: Mathlib.Algebra.Polynomial.RingDivision
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
p q : R[X]
hp : ¬p = 0
pos : ∀ (hq : q = 0), (p * q).trailingDegree = p.trailingDegree + q.trailingDegree
neg : ∀ (hq : ¬q = 0), (p * q).trailingDegree = p.trailingDegree + q.trailingDegree
⊢ (p * q).trailingDegree = p.trailingDegree + q.trailingDegree

Tactic:
by_cases hq : q = 0
-- Module: Mathlib.Algebra.Polynomial.RingDivision
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
p q : R[X]
hp : ¬p = 0
hq : q = 0
pos : (p * 0).trailingDegree = p.trailingDegree + trailingDegree.{u} (R := R) 0
pos₁ : trailingDegree.{u} (R := R) 0 = p.trailingDegree + trailingDegree.{u} (R := R) 0
pos₂ : ⊤ = p.trailingDegree + ⊤
pos₃ pos₄ : Eq (α := ℕ∞) ⊤ ⊤
⊢ (p * q).trailingDegree = p.trailingDegree + q.trailingDegree

Tactic:
rw [hq, mul_zero, trailingDegree_zero, add_top]

Premises used: add_top, Polynomial.trailingDegree_zero, MulZeroClass.mul_zero
-- Module: Mathlib.Algebra.Polynomial.RingDivision
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
p q : R[X]
hp : ¬p = 0
hq : ¬q = 0
neg :
  (↑(p.natTrailingDegree + q.natTrailingDegree) : ℕ∞) =
    HAdd.hAdd (α := ℕ∞) (↑p.natTrailingDegree : ℕ∞) (↑q.natTrailingDegree : ℕ∞)
⊢ (p * q).trailingDegree = p.trailingDegree + q.trailingDegree

Tactic:
rw [trailingDegree_eq_natTrailingDegree hp, trailingDegree_eq_natTrailingDegree hq,
    trailingDegree_eq_natTrailingDegree (mul_ne_zero hp hq), natTrailingDegree_mul hp hq]

Premises used: Polynomial.natTrailingDegree_mul, mul_ne_zero, Polynomial.trailingDegree_eq_natTrailingDegree
-- Module: Mathlib.Algebra.Polynomial.RingDivision
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
p q : R[X]
hp : ¬p = 0
hq : ¬q = 0
⊢ (↑(p.natTrailingDegree + q.natTrailingDegree) : ℕ∞) =
    HAdd.hAdd (α := ℕ∞) (↑p.natTrailingDegree : ℕ∞) (↑q.natTrailingDegree : ℕ∞)

Tactic:
apply WithTop.coe_add

Premises used: WithTop.coe_add
-- Module: Mathlib.Algebra.Polynomial.RingDivision
Goal:
R : Type u
inst : CommRing R
p : R[X]
t : R
simp_rw :
  (if p = 0 then 0 else multiplicity (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X])) p) =
    if p = 0 then 0
    else
      multiplicity (HSub.hSub (α := R[X]) X ((C : (a : R) → R[X]) 0))
        (p.comp (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X])))
⊢ rootMultiplicity t p =
    rootMultiplicity 0 (p.comp (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X])))

Tactic:
simp_rw [rootMultiplicity_eq_multiplicity, comp_X_add_C_eq_zero_iff]

Premises used: Polynomial.rootMultiplicity_eq_multiplicity, Polynomial.comp_X_add_C_eq_zero_iff
-- Module: Mathlib.Algebra.Polynomial.RingDivision
Goal:
R : Type u
inst : CommRing R
p : R[X]
t : R
e_e :
  multiplicity (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X])) p =
    multiplicity (HSub.hSub (α := R[X]) X ((C : (a : R) → R[X]) 0))
      (p.comp (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X])))
⊢ (if p = 0 then 0 else multiplicity (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X])) p) =
    if p = 0 then 0
    else
      multiplicity (HSub.hSub (α := R[X]) X ((C : (a : R) → R[X]) 0))
        (p.comp (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X])))

Tactic:
congr 1
-- Module: Mathlib.Algebra.Polynomial.RingDivision
Goal:
R : Type u
inst : CommRing R
p : R[X]
t : R
e_e :
  multiplicity (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X])) p =
    multiplicity X (p.comp (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X])))
⊢ multiplicity (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X])) p =
    multiplicity (HSub.hSub (α := R[X]) X ((C : (a : R) → R[X]) 0))
      (p.comp (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X])))

Tactic:
rw [C_0, sub_zero]

Premises used: sub_zero, Polynomial.C_0
-- Module: Mathlib.Algebra.Polynomial.RingDivision
Goal:
R : Type u
inst : CommRing R
p : R[X]
t : R
⊢ multiplicity (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X])) p =
    multiplicity (α := R[X])
      ((algEquivAevalXAddC t : (a : R[X]) → R[X])
          (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X])) :
        R[X])
      ((algEquivAevalXAddC t : (a : R[X]) → R[X]) p : R[X])

Tactic:
(multiplicity_map_eq <| algEquivAevalXAddC t).symm

Premises used: multiplicity_map_eq, Polynomial.algEquivAevalXAddC, Eq.symm
-- Module: Mathlib.Algebra.Polynomial.RingDivision
Goal:
R : Type u
inst : CommRing R
p : R[X]
t : R
h :
  Eq.{u + 1} (α := R[X]) X
    ((algEquivAevalXAddC t : (a : R[X]) → R[X]) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X])))
⊢ multiplicity (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X])) p =
    multiplicity X (p.comp (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X])))

Tactic:
convert! (multiplicity_map_eq <| algEquivAevalXAddC t).symm using 2

Premises used: multiplicity_map_eq, Polynomial.algEquivAevalXAddC, Eq.symm
-- Module: Mathlib.Algebra.Polynomial.RingDivision
Goal:
R : Type u
inst : CommRing R
p : R[X]
t : R
⊢ Eq.{u + 1} (α := R[X]) X
    ((algEquivAevalXAddC t : (a : R[X]) → R[X]) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X])))

Tactic:
simp [C_eq_algebraMap]

Premises used: Polynomial.C_eq_algebraMap
-- Module: Mathlib.Algebra.Polynomial.RingDivision
Goal:
R : Type u
inst : CommRing R
p : R[X]
t : R
simp_rw :
  (if p = 0 then 0 else multiplicity (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X])) p) =
    if p.comp (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X])) = 0 then 0
    else
      multiplicity (HSub.hSub (α := R[X]) X ((C : (a : R) → R[X]) 0))
        (p.comp (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X])))
simp_rw₁ :
  (if p = 0 then 0 else multiplicity (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X])) p) =
    if p = 0 then 0
    else
      multiplicity (HSub.hSub (α := R[X]) X ((C : (a : R) → R[X]) 0))
        (p.comp (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X])))
e_e :
  multiplicity (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X])) p =
    multiplicity (HSub.hSub (α := R[X]) X ((C : (a : R) → R[X]) 0))
      (p.comp (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X])))
e_e₁ :
  multiplicity (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X])) p =
    multiplicity X (p.comp (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X])))
h :
  Eq.{u + 1} (α := R[X]) X
    ((algEquivAevalXAddC t : (a : R[X]) → R[X]) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X])))
⊢ rootMultiplicity t p =
    rootMultiplicity 0 (p.comp (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X])))

Tactic:
classical
  simp_rw [rootMultiplicity_eq_multiplicity, comp_X_add_C_eq_zero_iff]
  congr 1
  rw [C_0, sub_zero]
  convert! (multiplicity_map_eq <| algEquivAevalXAddC t).symm using 2
  simp [C_eq_algebraMap]

Premises used: sub_zero, Polynomial.C_0, Polynomial.C_eq_algebraMap, multiplicity_map_eq, Polynomial.rootMultiplicity_eq_multiplicity, Polynomial.algEquivAevalXAddC, Polynomial.comp_X_add_C_eq_zero_iff, Eq.symm
-- Module: Mathlib.Algebra.Polynomial.RingDivision
Goal:
R : Type u
inst : CommRing R
p : R[X]
t : R
⊢ rootMultiplicity t p =
    (p.comp (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]))).natTrailingDegree

Tactic:
rootMultiplicity_eq_rootMultiplicity.trans rootMultiplicity_eq_natTrailingDegree'

Premises used: Polynomial.rootMultiplicity_eq_rootMultiplicity, Polynomial.rootMultiplicity_eq_natTrailingDegree', Eq.trans
-- Module: Mathlib.Algebra.Polynomial.RingDivision
Goal:
R : Type u
inst : CommRing R
p : R[X]
h : p.Monic
⊢ Membership.mem (γ := Submonoid R[X]) R[X]⁰ p

Tactic:
mem_nonzeroDivisors_of_coeff_mem _ (h.coeff_natDegree ▸ one_mem R⁰)

Premises used: Polynomial.mem_nonzeroDivisors_of_coeff_mem
-- Module: Mathlib.Algebra.Polynomial.RingDivision
Goal:
R : Type u
inst : CommRing R
p : R[X]
h : Membership.mem (γ := Submonoid R) R⁰ p.leadingCoeff
⊢ Membership.mem (γ := Submonoid R[X]) R[X]⁰ p

Tactic:
mem_nonzeroDivisors_of_coeff_mem _ h

Premises used: Polynomial.mem_nonzeroDivisors_of_coeff_mem
-- Module: Mathlib.Algebra.Polynomial.RingDivision
Goal:
R : Type u
inst : CommRing R
p : R[X]
h : Membership.mem (γ := Submonoid R) R⁰ p.trailingCoeff
⊢ Membership.mem (γ := Submonoid R[X]) R[X]⁰ p

Tactic:
mem_nonzeroDivisors_of_coeff_mem _ h

Premises used: Polynomial.mem_nonzeroDivisors_of_coeff_mem
-- Module: Mathlib.Algebra.Polynomial.RingDivision
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Ring S
inst_3 : Algebra R S
inst_4 : FaithfulSMul R S
p : R[X]
hp : Irreducible p
hdeg : p.natDegree ≠ 1
x : S
hx : Membership.mem (γ := Subring S) (RingHom.range.{u, v} (R := R) (algebraMap R S)) x
obtain :
  ∀ (w : R),
    Ne.{v + 1} (α := S) (((aeval (((algebraMap R S : R →+* S) : (a : R) → S) w) : R[X] →ₐ[R] S) : (a : R[X]) → S) p : S)
      (0 : S)
⊢ Ne.{v + 1} (α := S) ((aeval x : (a : R[X]) → S) p : S) (0 : S)

Tactic:
obtain ⟨_, rfl⟩ := hx

Premises used: rfl
-- Module: Mathlib.Algebra.Polynomial.RingDivision
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Ring S
inst_3 : Algebra R S
inst_4 : FaithfulSMul R S
p : R[X]
hp : Irreducible p
hdeg : p.natDegree ≠ 1
w : R
rw : Ne.{v + 1} (α := S) ((algebraMap R S : (a : R) → S) (eval w p) : S) (0 : S)
⊢ Ne.{v + 1} (α := S) (((aeval (((algebraMap R S : R →+* S) : (a : R) → S) w) : R[X] →ₐ[R] S) : (a : R[X]) → S) p : S)
    (0 : S)

Tactic:
rw [aeval_algebraMap_apply_eq_algebraMap_eval]

Premises used: Polynomial.aeval_algebraMap_apply_eq_algebraMap_eval
-- Module: Mathlib.Algebra.Polynomial.RingDivision
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Ring S
inst_3 : Algebra R S
inst_4 : FaithfulSMul R S
p : R[X]
hp : Irreducible p
hdeg : p.natDegree ≠ 1
w : R
⊢ Ne.{v + 1} (α := S) ((algebraMap R S : (a : R) → S) (eval w p) : S) (0 : S)

Tactic:
fun heq ↦ hp.not_isRoot_of_natDegree_ne_one hdeg <|
    FaithfulSMul.algebraMap_injective _ _ <| map_zero (algebraMap R S) ▸ heq

Premises used: Irreducible.not_isRoot_of_natDegree_ne_one, FaithfulSMul.algebraMap_injective, Not
-- Module: Mathlib.Algebra.Polynomial.RingDivision
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Ring S
inst_3 : Algebra R S
inst_4 : FaithfulSMul R S
p : R[X]
hp : Irreducible p
hdeg : p.natDegree ≠ 1
w : R
⊢ Ne.{v + 1} (α := S) ((algebraMap R S : (a : R) → S) (eval w p) : S) (0 : S)

Tactic:
exact fun heq ↦ hp.not_isRoot_of_natDegree_ne_one hdeg <|
    FaithfulSMul.algebraMap_injective _ _ <| map_zero (algebraMap R S) ▸ heq

Premises used: Irreducible.not_isRoot_of_natDegree_ne_one, FaithfulSMul.algebraMap_injective
-- Module: Mathlib.Algebra.Polynomial.RingDivision
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Nontrivial R
inst_2 : Semiring S
inst_3 : Algebra R S
inst_4 : FaithfulSMul R S
p : R[X]
hp : p.Monic
x : S
hx : Eq.{v + 1} (α := S) ((aeval x : (a : R[X]) → S) p : S) (0 : S)
⊢ 0 < p.natDegree

Tactic:
natDegree_pos_of_aeval_root (Monic.ne_zero hp) hx
    ((injective_iff_map_eq_zero (algebraMap R S)).mp (FaithfulSMul.algebraMap_injective R S))

Premises used: Algebra.algebraMap, injective_iff_map_eq_zero, FaithfulSMul.algebraMap_injective, Iff.mp, Polynomial.natDegree_pos_of_aeval_root, Polynomial.Monic.ne_zero
-- Module: Mathlib.Algebra.Polynomial.RingDivision
Goal:
R : Type u
inst : CommRing R
p : R[X]
a : R
n : ℕ
h : p ≠ 0
⊢ p * HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ n ≠ 0

Tactic:
have h2 := monic_X_sub_C a |>.pow n |>.mul_left_ne_zero h
-- Module: Mathlib.Algebra.Polynomial.RingDivision
Goal:
R : Type u
inst : CommRing R
p : R[X]
a : R
n : ℕ
h : p ≠ 0
h2 : p * HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ n ≠ 0
⊢ rootMultiplicity a (p * HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ n) =
    rootMultiplicity a p + n

Tactic:
le_antisymm ?_ ?_

Premises used: le_antisymm
-- Module: Mathlib.Algebra.Polynomial.RingDivision
Goal:
R : Type u
inst : CommRing R
p : R[X]
a : R
n : ℕ
h : p ≠ 0
h2 : p * HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ n ≠ 0
refine_1 :
  rootMultiplicity a (p * HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ n) ≤
    rootMultiplicity a p + n
refine_2 :
  rootMultiplicity a p + n ≤
    rootMultiplicity a (p * HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ n)
⊢ rootMultiplicity a (p * HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ n) =
    rootMultiplicity a p + n

Tactic:
refine le_antisymm ?_ ?_

Premises used: le_antisymm
-- Module: Mathlib.Algebra.Polynomial.RingDivision
Goal:
R : Type u
inst : CommRing R
p : R[X]
a : R
n : ℕ
h : p ≠ 0
h2 : p * HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ n ≠ 0
refine_1 : ¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ (rootMultiplicity a p + 1) ∣ p
⊢ rootMultiplicity a (p * HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ n) ≤
    rootMultiplicity a p + n

Tactic:
rw [rootMultiplicity_le_iff h2, add_assoc, add_comm n, ← add_assoc, pow_add,
      dvd_cancel_right_mem_nonZeroDivisors (monic_X_sub_C a |>.pow n |>.mem_nonZeroDivisors)]

Premises used: Polynomial.monic_X_sub_C, add_assoc, dvd_cancel_right_mem_nonZeroDivisors, pow_add, add_comm, Polynomial.Monic.mem_nonZeroDivisors, Polynomial.Monic.pow, Polynomial.rootMultiplicity_le_iff
-- Module: Mathlib.Algebra.Polynomial.RingDivision
Goal:
R : Type u
inst : CommRing R
p : R[X]
a : R
n : ℕ
h : p ≠ 0
h2 : p * HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ n ≠ 0
⊢ ¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ (rootMultiplicity a p + 1) ∣ p

Tactic:
pow_rootMultiplicity_not_dvd h a

Premises used: Polynomial.pow_rootMultiplicity_not_dvd
-- Module: Mathlib.Algebra.Polynomial.RingDivision
Goal:
R : Type u
inst : CommRing R
p : R[X]
a : R
n : ℕ
h : p ≠ 0
h2 : p * HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ n ≠ 0
⊢ ¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ (rootMultiplicity a p + 1) ∣ p

Tactic:
exact pow_rootMultiplicity_not_dvd h a

Premises used: Polynomial.pow_rootMultiplicity_not_dvd
-- Module: Mathlib.Algebra.Polynomial.RingDivision
Goal:
R : Type u
inst : CommRing R
p : R[X]
a : R
n : ℕ
h : p ≠ 0
h2 : p * HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ n ≠ 0
refine_2 :
  HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ rootMultiplicity a p *
      HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ n ∣
    p * HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ n
⊢ rootMultiplicity a p + n ≤
    rootMultiplicity a (p * HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ n)

Tactic:
rw [le_rootMultiplicity_iff h2, pow_add]

Premises used: pow_add, Polynomial.le_rootMultiplicity_iff
-- Module: Mathlib.Algebra.Polynomial.RingDivision
Goal:
R : Type u
inst : CommRing R
p : R[X]
a : R
n : ℕ
h : p ≠ 0
h2 : p * HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ n ≠ 0
⊢ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ rootMultiplicity a p *
      HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ n ∣
    p * HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ n

Tactic:
mul_dvd_mul_right (pow_rootMultiplicity_dvd p a) _

Premises used: Polynomial.pow_rootMultiplicity_dvd, mul_dvd_mul_right
-- Module: Mathlib.Algebra.Polynomial.RingDivision
Goal:
R : Type u
inst : CommRing R
p : R[X]
a : R
n : ℕ
h : p ≠ 0
h2 : p * HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ n ≠ 0
⊢ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ rootMultiplicity a p *
      HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ n ∣
    p * HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ n

Tactic:
exact mul_dvd_mul_right (pow_rootMultiplicity_dvd p a) _

Premises used: Polynomial.pow_rootMultiplicity_dvd, mul_dvd_mul_right
-- Module: Mathlib.Algebra.Polynomial.RingDivision
Goal:
R : Type u
inst : CommRing R
inst_1 : Nontrivial R
a : R
n : ℕ
⊢ rootMultiplicity a
      ((C : (a : R) → R[X]) 1 * HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ n) =
    rootMultiplicity a ((C : (a : R) → R[X]) 1) + n

Tactic:
have := rootMultiplicity_mul_X_sub_C_pow (a := a) (n := n) C.map_one_ne_zero
-- Module: Mathlib.Algebra.Polynomial.RingDivision
Goal:
R : Type u
inst : CommRing R
inst_1 : Nontrivial R
a : R
n : ℕ
this :
  rootMultiplicity a
      ((C : (a : R) → R[X]) 1 * HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ n) =
    rootMultiplicity a ((C : (a : R) → R[X]) 1) + n
rwa :
  ∀
    (this :
      rootMultiplicity a
          ((C : (a : R) → R[X]) 1 * HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ n) =
        0 + n),
    rootMultiplicity a (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ n) = n
rwa₁ :
  ∀ (this : rootMultiplicity a (1 * HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ n) = 0 + n),
    rootMultiplicity a (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ n) = n
rwa₂ :
  ∀ (this : rootMultiplicity a (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ n) = 0 + n),
    rootMultiplicity a (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ n) = n
rwa₃ rwa₄ rwa₅ rwa₆ :
  ∀ (this : rootMultiplicity a (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ n) = n),
    rootMultiplicity a (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ n) = n
⊢ rootMultiplicity a (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ n) = n

Tactic:
rwa [rootMultiplicity_C, map_one, one_mul, zero_add] at this

Premises used: Polynomial.rootMultiplicity_C, zero_add, map_one, one_mul
-- Module: Mathlib.Algebra.Polynomial.RingDivision
Goal:
R : Type u
inst : CommRing R
inst_1 : Nontrivial R
x : R
⊢ rootMultiplicity x (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) = 1

Tactic:
pow_one (X - C x) ▸ rootMultiplicity_X_sub_C_pow x 1

Premises used: Polynomial.C, Polynomial.rootMultiplicity_X_sub_C_pow, HSub.hSub, Eq.rec, pow_one, OfNat.ofNat, Polynomial.X, DFunLike.coe
-- Module: Mathlib.Algebra.Polynomial.RingDivision
Goal:
R : Type u
inst : CommRing R
inst_1 : Nontrivial R
inst_2 : DecidableEq R
x y : R
pos : ∀ (hxy : x = y), rootMultiplicity x (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) y : R[X])) = 1
neg : ∀ (hxy : ¬x = y), rootMultiplicity x (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) y : R[X])) = 0
⊢ rootMultiplicity x (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) y : R[X])) = if x = y then 1 else 0

Tactic:
split_ifs with hxy
-- Module: Mathlib.Algebra.Polynomial.RingDivision
Goal:
R : Type u
inst : CommRing R
inst_1 : Nontrivial R
inst_2 : DecidableEq R
x y : R
hxy : x = y
pos : rootMultiplicity y (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) y : R[X])) = 1
⊢ rootMultiplicity x (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) y : R[X])) = 1

Tactic:
rw [hxy]
-- Module: Mathlib.Algebra.Polynomial.RingDivision
Goal:
R : Type u
inst : CommRing R
inst_1 : Nontrivial R
inst_2 : DecidableEq R
x y : R
hxy : x = y
⊢ rootMultiplicity y (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) y : R[X])) = 1

Tactic:
rootMultiplicity_X_sub_C_self

Premises used: Polynomial.rootMultiplicity_X_sub_C_self
-- Module: Mathlib.Algebra.Polynomial.RingDivision
Goal:
R : Type u
inst : CommRing R
inst_1 : Nontrivial R
inst_2 : DecidableEq R
x y : R
hxy : x = y
⊢ rootMultiplicity y (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) y : R[X])) = 1

Tactic:
exact rootMultiplicity_X_sub_C_self

Premises used: Polynomial.rootMultiplicity_X_sub_C_self
-- Module: Mathlib.Algebra.Polynomial.RingDivision
Goal:
R : Type u
inst : CommRing R
inst_1 : Nontrivial R
inst_2 : DecidableEq R
x y : R
hxy : ¬x = y
⊢ rootMultiplicity x (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) y : R[X])) = 0

Tactic:
rootMultiplicity_eq_zero (mt root_X_sub_C.mp (Ne.symm hxy))

Premises used: Polynomial.root_X_sub_C, mt, Ne.symm, Iff.mp, Polynomial.rootMultiplicity_eq_zero
-- Module: Mathlib.Algebra.Polynomial.RingDivision
Goal:
R : Type u
inst : CommRing R
inst_1 : Nontrivial R
inst_2 : DecidableEq R
x y : R
hxy : ¬x = y
⊢ rootMultiplicity x (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) y : R[X])) = 0

Tactic:
exact rootMultiplicity_eq_zero (mt root_X_sub_C.mp (Ne.symm hxy))

Premises used: Polynomial.root_X_sub_C, mt, Ne.symm, Iff.mp, Polynomial.rootMultiplicity_eq_zero
-- Module: Mathlib.Algebra.Polynomial.RingDivision
Goal:
R : Type u
inst : CommRing R
p q : R[X]
x : R
hpq :
  eval x (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) ^ rootMultiplicity x p) *
      eval x (q /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) ^ rootMultiplicity x q) ≠
    0
⊢ (p.comp (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]))).trailingCoeff *
      (q.comp (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]))).trailingCoeff ≠
    0

Tactic:
simp_rw [eval_divByMonic_eq_trailingCoeff_comp] at hpq

Premises used: Polynomial.eval_divByMonic_eq_trailingCoeff_comp
-- Module: Mathlib.Algebra.Polynomial.RingDivision
Goal:
R : Type u
inst : CommRing R
p q : R[X]
x : R
hpq :
  (p.comp (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]))).trailingCoeff *
      (q.comp (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]))).trailingCoeff ≠
    0
simp_rw :
  ((p * q).comp (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]))).natTrailingDegree =
    (p.comp (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]))).natTrailingDegree +
      (q.comp (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]))).natTrailingDegree
simp_rw₁ :
  (p.comp (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) *
        q.comp (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]))).natTrailingDegree =
    (p.comp (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]))).natTrailingDegree +
      (q.comp (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]))).natTrailingDegree
⊢ rootMultiplicity x (p * q) = rootMultiplicity x p + rootMultiplicity x q

Tactic:
simp_rw [rootMultiplicity_eq_natTrailingDegree, mul_comp, natTrailingDegree_mul' hpq]

Premises used: Polynomial.rootMultiplicity_eq_natTrailingDegree, Polynomial.mul_comp, Polynomial.natTrailingDegree_mul'