awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : CommRing R
p : R[X]
t : R
h : p ≠ 0
n : ℕ
ih :
  ∀ (hnzd : ∀ m ≤ n, m ≠ 0 → Membership.mem (γ := Submonoid R) (nonZeroDivisors R) (↑m : R)),
    Membership.mem (γ := Submonoid R) (nonZeroDivisors R) (↑n ! : R)
hnzd : ∀ m ≤ n + 1, m ≠ 0 → Membership.mem (γ := Submonoid R) (nonZeroDivisors R) (↑m : R)
⊢ Membership.mem (γ := Submonoid R) (nonZeroDivisors R) (↑(n + 1) : R) ∧
    Membership.mem (γ := Submonoid R) (nonZeroDivisors R) (↑n ! : R)

Tactic:
exact ⟨hnzd _ le_rfl n.succ_ne_zero, ih fun m h ↦ hnzd m (h.trans n.le_succ)⟩
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : CommRing R
p : R[X]
t : R
n : ℕ
h : p ≠ 0
hnzd : ∀ m ≤ n, m ≠ 0 → Membership.mem (γ := Submonoid R) (nonZeroDivisors R) (↑m : R)
zero :
  ∀ (hnzd : ∀ m ≤ 0, m ≠ 0 → Membership.mem (γ := Submonoid R) (nonZeroDivisors R) (↑m : R)),
    Membership.mem (γ := Submonoid R) (nonZeroDivisors R) (↑0! : R)
succ :
  ∀ (n : ℕ)
    (ih :
      ∀ (hnzd : ∀ m ≤ n, m ≠ 0 → Membership.mem (γ := Submonoid R) (nonZeroDivisors R) (↑m : R)),
        Membership.mem (γ := Submonoid R) (nonZeroDivisors R) (↑n ! : R))
    (hnzd : ∀ m ≤ n + 1, m ≠ 0 → Membership.mem (γ := Submonoid R) (nonZeroDivisors R) (↑m : R)),
    Membership.mem (γ := Submonoid R) (nonZeroDivisors R) (↑(n + 1)! : R)
⊢ Membership.mem (γ := Submonoid R) (nonZeroDivisors R) (↑n ! : R)

Tactic:
induction n with
  | zero =>
    simp only [Nat.factorial_zero, Nat.cast_one]
    exact Submonoid.one_mem _
  | succ n ih =>
    rw [Nat.factorial_succ, Nat.cast_mul, mul_mem_nonZeroDivisors]
    exact ⟨hnzd _ le_rfl n.succ_ne_zero, ih fun m h ↦ hnzd m (h.trans n.le_succ)⟩

Premises used: Nat.factorial_succ, Submonoid.one_mem, Nat.cast_mul, Nat.factorial_zero, Nat.cast_one, mul_mem_nonZeroDivisors
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : CommRing R
p : R[X]
t : R
n : ℕ
h : p ≠ 0
hnzd : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) (↑n ! : R)
⊢ n < rootMultiplicity t p ↔ ∀ m ≤ n, ((⇑derivative : (a : R[X]) → R[X])^[m] p).IsRoot t

Tactic:
⟨fun hn _ hm ↦ isRoot_iterate_derivative_of_lt_rootMultiplicity <| hm.trans_lt hn,
    fun hr ↦ lt_rootMultiplicity_of_isRoot_iterate_derivative_of_mem_nonZeroDivisors h hr hnzd⟩

Premises used: Polynomial.isRoot_iterate_derivative_of_lt_rootMultiplicity, Iff.intro, Polynomial.lt_rootMultiplicity_of_isRoot_iterate_derivative_of_mem_nonZeroDivisors, LE.le.trans_lt
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : CommRing R
p : R[X]
t : R
n : ℕ
h : p ≠ 0
hnzd : ∀ m ≤ n, m ≠ 0 → Membership.mem (γ := Submonoid R) (nonZeroDivisors R) (↑m : R)
⊢ n < rootMultiplicity t p ↔ ∀ m ≤ n, ((⇑derivative : (a : R[X]) → R[X])^[m] p).IsRoot t

Tactic:
⟨fun hn _ hm ↦ isRoot_iterate_derivative_of_lt_rootMultiplicity <| Nat.lt_of_le_of_lt hm hn,
    fun hr ↦ lt_rootMultiplicity_of_isRoot_iterate_derivative_of_mem_nonZeroDivisors' h hr hnzd⟩

Premises used: Nat.lt_of_le_of_lt, Polynomial.isRoot_iterate_derivative_of_lt_rootMultiplicity, Iff.intro, Polynomial.lt_rootMultiplicity_of_isRoot_iterate_derivative_of_mem_nonZeroDivisors'
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : CommRing R
p : R[X]
t : R
h : p ≠ 0
rw : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) 1
⊢ Membership.mem (γ := Submonoid R) (nonZeroDivisors R) (↑1! : R)

Tactic:
rw [Nat.factorial_one, Nat.cast_one]

Premises used: Nat.cast_one, Nat.factorial_one
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : CommRing R
p : R[X]
t : R
h : p ≠ 0
⊢ Membership.mem (γ := Submonoid R) (nonZeroDivisors R) 1

Tactic:
Submonoid.one_mem _

Premises used: Set.Mem, Submonoid.one_mem
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : CommRing R
p : R[X]
t : R
h : p ≠ 0
⊢ Membership.mem (γ := Submonoid R) (nonZeroDivisors R) 1

Tactic:
exact Submonoid.one_mem _

Premises used: Submonoid.one_mem
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : CommRing R
p : R[X]
t : R
h : p ≠ 0
rw :
  (∀ m ≤ 1, ((⇑derivative : (a : R[X]) → R[X])^[m] p).IsRoot t) ↔
    p.IsRoot t ∧ IsRoot ((derivative : (a : R[X]) → R[X]) p) t
⊢ 1 < rootMultiplicity t p ↔ p.IsRoot t ∧ IsRoot ((derivative : (a : R[X]) → R[X]) p) t

Tactic:
rw [one_lt_rootMultiplicity_iff_isRoot_iterate_derivative h]

Premises used: Polynomial.one_lt_rootMultiplicity_iff_isRoot_iterate_derivative
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : CommRing R
p : R[X]
t : R
h_1 : p ≠ 0
h : ∀ m ≤ 1, ((⇑derivative : (a : R[X]) → R[X])^[m] p).IsRoot t
⊢ LE.le (α := ℕ) 0 1

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : CommRing R
p : R[X]
t : R
h_1 : p ≠ 0
h : ∀ m ≤ 1, ((⇑derivative : (a : R[X]) → R[X])^[m] p).IsRoot t
⊢ LE.le (α := ℕ) 1 1

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : CommRing R
p : R[X]
t : R
h : p ≠ 0
refine :
  p.IsRoot t ∧ IsRoot ((derivative : (a : R[X]) → R[X]) p) t →
    ∀ (m : ℕ) (hm : m ≤ 1) (h0 : p.IsRoot t) (h1 : IsRoot ((derivative : (a : R[X]) → R[X]) p) t),
      ((⇑derivative : (a : R[X]) → R[X])^[m] p).IsRoot t
⊢ (∀ m ≤ 1, ((⇑derivative : (a : R[X]) → R[X])^[m] p).IsRoot t) ↔
    p.IsRoot t ∧ IsRoot ((derivative : (a : R[X]) → R[X]) p) t

Tactic:
refine ⟨fun h ↦ ⟨h 0 (by simp), h 1 (by simp)⟩, fun ⟨h0, h1⟩ m hm ↦ ?_⟩
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : CommRing R
p : R[X]
t : R
h : p ≠ 0
h_1 : p.IsRoot t ∧ IsRoot ((derivative : (a : R[X]) → R[X]) p) t
m : ℕ
hm : m ≤ 1
h0 : p.IsRoot t
h1 : IsRoot ((derivative : (a : R[X]) → R[X]) p) t
zero : ∀ (hm : LE.le (α := ℕ) 0 1), ((⇑derivative : (a : R[X]) → R[X])^[0] p).IsRoot t
succ : ∀ (hm : HAdd.hAdd (α := ℕ) 0 1 ≤ 1), ((⇑derivative : (a : R[X]) → R[X])^[HAdd.hAdd (α := ℕ) 0 1] p).IsRoot t
succ₁ : ∀ (m : ℕ) (hm : m + 1 + 1 ≤ 1), ((⇑derivative : (a : R[X]) → R[X])^[m + 1 + 1] p).IsRoot t
⊢ ((⇑derivative : (a : R[X]) → R[X])^[m] p).IsRoot t

Tactic:
obtain (_ | _ | m) := m
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : CommRing R
p : R[X]
t : R
h : p ≠ 0
h_1 : p.IsRoot t ∧ IsRoot ((derivative : (a : R[X]) → R[X]) p) t
h0 : p.IsRoot t
h1 : IsRoot ((derivative : (a : R[X]) → R[X]) p) t
hm : LE.le (α := ℕ) 0 1
⊢ ((⇑derivative : (a : R[X]) → R[X])^[0] p).IsRoot t

Tactic:
h0

Premises used: Nat.iterate
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : CommRing R
p : R[X]
t : R
h : p ≠ 0
h_1 : p.IsRoot t ∧ IsRoot ((derivative : (a : R[X]) → R[X]) p) t
h0 : p.IsRoot t
h1 : IsRoot ((derivative : (a : R[X]) → R[X]) p) t
hm : HAdd.hAdd (α := ℕ) 0 1 ≤ 1
⊢ ((⇑derivative : (a : R[X]) → R[X])^[HAdd.hAdd (α := ℕ) 0 1] p).IsRoot t

Tactic:
h1

Premises used: Nat.iterate
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : CommRing R
p : R[X]
t : R
h : p ≠ 0
h_1 : p.IsRoot t ∧ IsRoot ((derivative : (a : R[X]) → R[X]) p) t
h0 : p.IsRoot t
h1 : IsRoot ((derivative : (a : R[X]) → R[X]) p) t
m : ℕ
hm : m + 1 + 1 ≤ 1
⊢ ((⇑derivative : (a : R[X]) → R[X])^[m + 1 + 1] p).IsRoot t

Tactic:
lia
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : CommRing R
p : R[X]
t : R
h : p ≠ 0
h_1 : p.IsRoot t ∧ IsRoot ((derivative : (a : R[X]) → R[X]) p) t
h0 : p.IsRoot t
h1 : IsRoot ((derivative : (a : R[X]) → R[X]) p) t
hm : LE.le (α := ℕ) 0 1
⊢ ((⇑derivative : (a : R[X]) → R[X])^[0] p).IsRoot t

Tactic:
exacts [h0, h1, by lia]
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : CommRing R
inst_1 : GCDMonoid R[X]
p : R[X]
t : R
h : p ≠ 0
simp_rw :
  p.IsRoot t ∧ IsRoot ((derivative : (a : R[X]) → R[X]) p) t ↔
    (@gcd _ CommSemiring.toCommMonoidWithZero _ p ((derivative : (a : R[X]) → R[X]) p)).IsRoot t
simp_rw₁ :
  HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ∣ p ∧
      HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ∣ (derivative : (a : R[X]) → R[X]) p ↔
    HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ∣
      @gcd _ CommSemiring.toCommMonoidWithZero _ p ((derivative : (a : R[X]) → R[X]) p)
⊢ 1 < rootMultiplicity t p ↔
    (@gcd _ CommSemiring.toCommMonoidWithZero _ p ((derivative : (a : R[X]) → R[X]) p)).IsRoot t

Tactic:
simp_rw [one_lt_rootMultiplicity_iff_isRoot h, ← dvd_iff_isRoot, dvd_gcd_iff]

Premises used: Polynomial.dvd_iff_isRoot, Polynomial.one_lt_rootMultiplicity_iff_isRoot, dvd_gcd_iff
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : CommRing R
inst_1 : NoZeroDivisors R
inst_2 : CharZero R
p : R[X]
t : R
hpt : p.IsRoot t
pos : ∀ (h : p = 0), rootMultiplicity t ((derivative : (a : R[X]) → R[X]) p) = rootMultiplicity t p - 1
neg : ∀ (h : ¬p = 0), rootMultiplicity t ((derivative : (a : R[X]) → R[X]) p) = rootMultiplicity t p - 1
⊢ rootMultiplicity t ((derivative : (a : R[X]) → R[X]) p) = rootMultiplicity t p - 1

Tactic:
by_cases h : p = 0
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : CommRing R
inst_1 : NoZeroDivisors R
inst_2 : CharZero R
p : R[X]
t : R
hpt : p.IsRoot t
h : p = 0
pos : rootMultiplicity t ((derivative : (a : R[X]) → R[X]) 0) = rootMultiplicity t 0 - 1
pos₁ : rootMultiplicity t 0 = rootMultiplicity t 0 - 1
pos₂ pos₃ : 0 = HSub.hSub (α := ℕ) 0 1
⊢ rootMultiplicity t ((derivative : (a : R[X]) → R[X]) p) = rootMultiplicity t p - 1

Tactic:
rw [h, map_zero, rootMultiplicity_zero]

Premises used: map_zero, Polynomial.rootMultiplicity_zero
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : CommRing R
inst_1 : NoZeroDivisors R
inst_2 : CharZero R
p : R[X]
t : R
hpt : p.IsRoot t
h : ¬p = 0
⊢ rootMultiplicity t ((derivative : (a : R[X]) → R[X]) p) = rootMultiplicity t p - 1

Tactic:
derivative_rootMultiplicity_of_root_of_mem_nonZeroDivisors hpt <|
    mem_nonZeroDivisors_of_ne_zero <| Nat.cast_ne_zero.2 ((rootMultiplicity_pos h).2 hpt).ne'

Premises used: Iff.mpr, Polynomial.rootMultiplicity_pos, Polynomial.derivative_rootMultiplicity_of_root_of_mem_nonZeroDivisors, LT.lt.ne', mem_nonZeroDivisors_of_ne_zero, Nat.cast_ne_zero
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : CommRing R
inst_1 : NoZeroDivisors R
inst_2 : CharZero R
p : R[X]
t : R
hpt : p.IsRoot t
h : ¬p = 0
⊢ rootMultiplicity t ((derivative : (a : R[X]) → R[X]) p) = rootMultiplicity t p - 1

Tactic:
exact derivative_rootMultiplicity_of_root_of_mem_nonZeroDivisors hpt <|
    mem_nonZeroDivisors_of_ne_zero <| Nat.cast_ne_zero.2 ((rootMultiplicity_pos h).2 hpt).ne'

Premises used: Iff.mpr, Polynomial.rootMultiplicity_pos, Polynomial.derivative_rootMultiplicity_of_root_of_mem_nonZeroDivisors, LT.lt.ne', mem_nonZeroDivisors_of_ne_zero, Nat.cast_ne_zero
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : CommRing R
inst_1 : NoZeroDivisors R
inst_2 : CharZero R
p : R[X]
t : R
pos : ∀ (h : p.IsRoot t), rootMultiplicity t p - 1 ≤ rootMultiplicity t ((derivative : (a : R[X]) → R[X]) p)
neg : ∀ (h : ¬p.IsRoot t), rootMultiplicity t p - 1 ≤ rootMultiplicity t ((derivative : (a : R[X]) → R[X]) p)
⊢ rootMultiplicity t p - 1 ≤ rootMultiplicity t ((derivative : (a : R[X]) → R[X]) p)

Tactic:
by_cases h : p.IsRoot t

Premises used: Polynomial.IsRoot
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : CommRing R
inst_1 : NoZeroDivisors R
inst_2 : CharZero R
p : R[X]
t : R
h : p.IsRoot t
⊢ rootMultiplicity t p - 1 ≤ rootMultiplicity t ((derivative : (a : R[X]) → R[X]) p)

Tactic:
(derivative_rootMultiplicity_of_root h).symm.le

Premises used: Polynomial.derivative_rootMultiplicity_of_root, Eq.le, Eq.symm
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : CommRing R
inst_1 : NoZeroDivisors R
inst_2 : CharZero R
p : R[X]
t : R
h : p.IsRoot t
⊢ rootMultiplicity t p - 1 ≤ rootMultiplicity t ((derivative : (a : R[X]) → R[X]) p)

Tactic:
exact (derivative_rootMultiplicity_of_root h).symm.le

Premises used: Polynomial.derivative_rootMultiplicity_of_root, Eq.le, Eq.symm
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : CommRing R
inst_1 : NoZeroDivisors R
inst_2 : CharZero R
p : R[X]
t : R
h : ¬p.IsRoot t
⊢ rootMultiplicity t p - 1 ≤ rootMultiplicity t ((derivative : (a : R[X]) → R[X]) p)

Tactic:
simp [rootMultiplicity_eq_zero h]

Premises used: Polynomial.rootMultiplicity_eq_zero
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : CommRing R
inst_1 : NoZeroDivisors R
inst_2 : CharZero R
p : R[X]
t : R
n : ℕ
h : p ≠ 0
hroot : ∀ m ≤ n, ((⇑derivative : (a : R[X]) → R[X])^[m] p).IsRoot t
⊢ n ! ≠ 0

Tactic:
positivity
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : CommRing R
inst_1 : NoZeroDivisors R
inst_2 : CharZero R
p : R[X]
t : R
n : ℕ
h : p ≠ 0
⊢ n < rootMultiplicity t p ↔ ∀ m ≤ n, ((⇑derivative : (a : R[X]) → R[X])^[m] p).IsRoot t

Tactic:
⟨fun hn _ hm ↦ isRoot_iterate_derivative_of_lt_rootMultiplicity <| Nat.lt_of_le_of_lt hm hn,
    fun hr ↦ lt_rootMultiplicity_of_isRoot_iterate_derivative h hr⟩

Premises used: Nat.lt_of_le_of_lt, Polynomial.isRoot_iterate_derivative_of_lt_rootMultiplicity, Iff.intro, Polynomial.lt_rootMultiplicity_of_isRoot_iterate_derivative
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : CommRing R
inst_1 : NoZeroDivisors R
inst_2 : CharZero R
f g : R[X]
hf0 : f ≠ 0
hfd : f ∣ HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X]) g
a : R
haf : f.IsRoot a
rcases : ∀ (r : R[X]) (hr : HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X]) g = f * r), g.IsRoot a
⊢ g.IsRoot a

Tactic:
rcases hfd with ⟨r, hr⟩
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : CommRing R
inst_1 : NoZeroDivisors R
inst_2 : CharZero R
f g : R[X]
hf0 : f ≠ 0
a : R
haf : f.IsRoot a
r : R[X]
hr : HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X]) g = f * r
contrapose : ∀ (haf : Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X]) (0 : R[X])), ¬f.IsRoot a
⊢ Ne (α := R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X]) (0 : R[X])

Tactic:
contrapose haf
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : CommRing R
inst_1 : NoZeroDivisors R
inst_2 : CharZero R
f g : R[X]
hf0 : f ≠ 0
a : R
r : R[X]
hr : HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X]) g = f * r
haf : Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X]) (0 : R[X])
rw :
  ∀ (hf0 : Ne (α := R[X]) ((C : (a : R) → R[X]) (f.coeff 0) : R[X]) (0 : R[X])) {a : R} (r : R[X])
    (hr : HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X]) g = f * r)
    (haf : Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X]) (0 : R[X])),
    ¬IsRoot ((C : (a : R) → R[X]) (f.coeff 0)) a
⊢ ¬f.IsRoot a

Tactic:
rw [eq_C_of_derivative_eq_zero haf] at hf0 ⊢

Premises used: Polynomial.eq_C_of_derivative_eq_zero
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : CommRing R
inst_1 : NoZeroDivisors R
inst_2 : CharZero R
f g : R[X]
hf0 : Ne (α := R[X]) ((C : (a : R) → R[X]) (f.coeff 0) : R[X]) (0 : R[X])
a : R
r : R[X]
hr : HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X]) g = f * r
haf : Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X]) (0 : R[X])
⊢ ¬IsRoot ((C : (a : R) → R[X]) (f.coeff 0)) a

Tactic:
not_isRoot_C _ _ <| C_ne_zero.mp hf0

Premises used: Polynomial.not_isRoot_C, Iff.mp, Polynomial.C_ne_zero
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : CommRing R
inst_1 : NoZeroDivisors R
inst_2 : CharZero R
f g : R[X]
hf0 : Ne (α := R[X]) ((C : (a : R) → R[X]) (f.coeff 0) : R[X]) (0 : R[X])
a : R
r : R[X]
hr : HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X]) g = f * r
haf : Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X]) (0 : R[X])
⊢ ¬IsRoot ((C : (a : R) → R[X]) (f.coeff 0)) a

Tactic:
exact not_isRoot_C _ _ <| C_ne_zero.mp hf0

Premises used: Polynomial.not_isRoot_C, Iff.mp, Polynomial.C_ne_zero
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : CommRing R
inst_1 : NoZeroDivisors R
inst_2 : CharZero R
f g : R[X]
hf0 : f ≠ 0
a : R
haf : f.IsRoot a
r : R[X]
hr : HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X]) g = f * r
⊢ Ne (α := R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X]) (0 : R[X])

Tactic:
have hdf0 : derivative f ≠ 0 := by
    contrapose haf
    rw [eq_C_of_derivative_eq_zero haf] at hf0 ⊢
    exact not_isRoot_C _ _ <| C_ne_zero.mp hf0
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : CommRing R
inst_1 : NoZeroDivisors R
inst_2 : CharZero R
f g : R[X]
hf0 : f ≠ 0
a : R
haf : f.IsRoot a
r : R[X]
hr : HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X]) g = f * r
hdf0 : Ne (α := R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X]) (0 : R[X])
by_contra : ∀ (hg : ¬g.IsRoot a), False
⊢ g.IsRoot a

Tactic:
by_contra hg
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : CommRing R
inst_1 : NoZeroDivisors R
inst_2 : CharZero R
f : R[X]
hf0 : f ≠ 0
a : R
haf : f.IsRoot a
r : R[X]
hdf0 : Ne (α := R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X]) (0 : R[X])
hr : HMul.hMul (α := R[X]) (β := R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X]) (0 : R[X]) = f * r
hg : ¬IsRoot 0 a
⊢ False

Tactic:
simp at hg
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : CommRing R
inst_1 : NoZeroDivisors R
inst_2 : CharZero R
f g : R[X]
hf0 : f ≠ 0
a : R
haf : f.IsRoot a
r : R[X]
hr : HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X]) g = f * r
hdf0 : Ne (α := R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X]) (0 : R[X])
hg : ¬g.IsRoot a
⊢ HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X]) g ≠ 0

Tactic:
have hdfg0 : f.derivative * g ≠ 0 := mul_ne_zero hdf0 (by rintro rfl; simp at hg)
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : CommRing R
inst_1 : NoZeroDivisors R
inst_2 : CharZero R
f g : R[X]
hf0 : f ≠ 0
a : R
haf : f.IsRoot a
r : R[X]
hr : HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X]) g = f * r
hdf0 : Ne (α := R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X]) (0 : R[X])
hg : ¬g.IsRoot a
hdfg0 : HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X]) g ≠ 0
⊢ rootMultiplicity a (HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X]) g) = rootMultiplicity a (f * r)

Tactic:
have hr' := congr_arg (rootMultiplicity a) hr
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : CommRing R
inst_1 : NoZeroDivisors R
inst_2 : CharZero R
f g : R[X]
hf0 : f ≠ 0
a : R
haf : f.IsRoot a
r : R[X]
hr : HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X]) g = f * r
hdf0 : Ne (α := R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X]) (0 : R[X])
hg : ¬g.IsRoot a
hdfg0 : HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X]) g ≠ 0
hr' :
  rootMultiplicity a (HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X]) g) = rootMultiplicity a (f * r)
⊢ IsDomain R

Tactic:
have : IsDomain R := {}
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : CommRing R
inst_1 : NoZeroDivisors R
inst_2 : CharZero R
f g : R[X]
hf0 : f ≠ 0
a : R
haf : f.IsRoot a
r : R[X]
hr : HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X]) g = f * r
hdf0 : Ne (α := R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X]) (0 : R[X])
hg : ¬g.IsRoot a
hdfg0 : HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X]) g ≠ 0
hr' :
  rootMultiplicity a (HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X]) g) = rootMultiplicity a (f * r)
this : IsDomain R
⊢ rootMultiplicity a f = rootMultiplicity a r + rootMultiplicity a f + Nat.succ 0

Tactic:
rw [rootMultiplicity_mul hdfg0, derivative_rootMultiplicity_of_root haf,
    rootMultiplicity_eq_zero hg, add_zero, rootMultiplicity_mul (hr ▸ hdfg0), add_comm,
    Nat.sub_eq_iff_eq_add (Nat.succ_le_iff.2 ((rootMultiplicity_pos hf0).2 haf))] at hr'

Premises used: Iff.mpr, Polynomial.derivative_rootMultiplicity_of_root, Polynomial.rootMultiplicity_mul, Nat.sub_eq_iff_eq_add, Polynomial.rootMultiplicity_pos, add_comm, Polynomial.rootMultiplicity_eq_zero, add_zero, Nat.succ_le_iff
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : CommRing R
inst_1 : NoZeroDivisors R
inst_2 : CharZero R
f g : R[X]
hf0 : f ≠ 0
a : R
haf : f.IsRoot a
r : R[X]
hr : HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X]) g = f * r
hdf0 : Ne (α := R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X]) (0 : R[X])
hg : ¬g.IsRoot a
hdfg0 : HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X]) g ≠ 0
hr' :
  rootMultiplicity a (HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X]) g) = rootMultiplicity a (f * r)
this : IsDomain R
hr'₁ : rootMultiplicity a f = rootMultiplicity a r + rootMultiplicity a f + Nat.succ 0
⊢ IsDomain R

Tactic:
rw [rootMultiplicity_mul hdfg0, derivative_rootMultiplicity_of_root haf,
    rootMultiplicity_eq_zero hg, add_zero, rootMultiplicity_mul (hr ▸ hdfg0), add_comm,
    Nat.sub_eq_iff_eq_add (Nat.succ_le_iff.2 ((rootMultiplicity_pos hf0).2 haf))] at hr'

Premises used: Iff.mpr, Polynomial.derivative_rootMultiplicity_of_root, Polynomial.rootMultiplicity_mul, Nat.sub_eq_iff_eq_add, Polynomial.rootMultiplicity_pos, add_comm, Polynomial.rootMultiplicity_eq_zero, add_zero, Nat.succ_le_iff
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : CommRing R
inst_1 : NoZeroDivisors R
inst_2 : CharZero R
f g : R[X]
hf0 : f ≠ 0
a : R
haf : f.IsRoot a
r : R[X]
hr : HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X]) g = f * r
hdf0 : Ne (α := R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X]) (0 : R[X])
hg : ¬g.IsRoot a
hdfg0 : HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X]) g ≠ 0
hr' : rootMultiplicity a f = rootMultiplicity a r + rootMultiplicity a f + Nat.succ 0
this : IsDomain R
⊢ False

Tactic:
lia
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst : CommRing R
inst_1 : NoZeroDivisors R
inst_2 : NormalizationMonoid R
p : R[X]
rw :
  Eq (α := R[X]) ((C : (a : R) → R[X]) ((↑(normUnit p.leadingCoeff) : R) * (↑(normUnit p.leadingCoeff)⁻¹ : R)) : R[X])
    (1 : R[X])
rw₁ : Eq.{u + 1} (α := R[X]) ((C : (a : R) → R[X]) 1) 1
rw₂ rw₃ : Eq.{u + 1} (α := R[X]) 1 1
⊢ HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (↑(normUnit p.leadingCoeff) : R) : R[X])
      ((C : (a : R) → R[X]) (↑(normUnit p.leadingCoeff)⁻¹ : R) : R[X]) =
    1

Tactic:
rw [← map_mul, Units.mul_inv, C_1]

Premises used: Polynomial.C_1, Units.mul_inv, map_mul
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst : CommRing R
inst_1 : NoZeroDivisors R
inst_2 : NormalizationMonoid R
p : R[X]
rw :
  Eq (α := R[X]) ((C : (a : R) → R[X]) ((↑(normUnit p.leadingCoeff)⁻¹ : R) * (↑(normUnit p.leadingCoeff) : R)) : R[X])
    (1 : R[X])
rw₁ : Eq.{u + 1} (α := R[X]) ((C : (a : R) → R[X]) 1) 1
rw₂ rw₃ : Eq.{u + 1} (α := R[X]) 1 1
⊢ HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (↑(normUnit p.leadingCoeff)⁻¹ : R) : R[X])
      ((C : (a : R) → R[X]) (↑(normUnit p.leadingCoeff) : R) : R[X]) =
    1

Tactic:
rw [← map_mul, Units.inv_mul, C_1]

Premises used: Polynomial.C_1, Units.inv_mul, map_mul
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst : CommRing R
inst_1 : NoZeroDivisors R
inst_2 : NormalizationMonoid R
⊢ Eq.{u + 1} (α := R[X])
    (↑{ val := (C : (a : R) → R[X]) (↑(normUnit (leadingCoeff 0)) : R),
          inv := (C : (a : R) → R[X]) (↑(normUnit (leadingCoeff 0))⁻¹ : R), val_inv := ⋯, inv_val := ⋯ : R[X]ˣ } :
      R[X])
    (↑1 : R[X])

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst : CommRing R
inst_1 : NoZeroDivisors R
inst_2 : NormalizationMonoid R
a_1 b_1 : R[X]
hp0 : a_1 ≠ 0
hq0 : b_1 ≠ 0
⊢ ¬a_1.leadingCoeff = 0

Tactic:
rw [Ne, ← leadingCoeff_eq_zero] at *

Premises used: Ne, Polynomial.leadingCoeff_eq_zero