-- Mathlib/Algebra/Polynomial/FieldDivision.lean
theorem isRoot_of_isRoot_of_dvd_derivative_mul [CharZero R] {f g : R[X]} (hf0 : f ≠ 0)
    (hfd : f ∣ f.derivative * g) {a : R} (haf : f.IsRoot a) : g.IsRoot a

Proof state:
case intro
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : CharZero R
f g : R[X]
hf0 : f ≠ 0
a : R
haf : f.IsRoot a
r : R[X]
hr : derivative f * g = f * r
⊢ g.IsRoot a

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

Result:
case intro
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : CharZero R
f g : R[X]
hf0 : f ≠ 0
a : R
haf : f.IsRoot a
r : R[X]
hr : derivative f * g = f * r
hdf0 : derivative f ≠ 0
⊢ g.IsRoot a

Proof state:
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : CharZero R
f g : R[X]
hf0 : f ≠ 0
hfd : f ∣ derivative f * g
a : R
haf : f.IsRoot a
⊢ g.IsRoot a

Tactic:
rcases hfd with ⟨r, hr⟩

Result:
case intro
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : CharZero R
f g : R[X]
hf0 : f ≠ 0
a : R
haf : f.IsRoot a
r : R[X]
hr : derivative f * g = f * r
⊢ g.IsRoot a

Proof state:
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : CharZero R
f g : R[X]
hf0 : f ≠ 0
a : R
haf : f.IsRoot a
r : R[X]
hr : derivative f * g = f * r
hdf0 : derivative f ≠ 0
hg : ¬g.IsRoot a
⊢ g ≠ 0

Tactic:
rintro rfl

Result:
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : CharZero R
f : R[X]
hf0 : f ≠ 0
a : R
haf : f.IsRoot a
r : R[X]
hdf0 : derivative f ≠ 0
hr : derivative f * 0 = f * r
hg : ¬IsRoot 0 a
⊢ False

Proof state:
case intro
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : CharZero R
f g : R[X]
hf0 : f ≠ 0
a : R
haf : f.IsRoot a
r : R[X]
hr : derivative f * g = f * r
hdf0 : derivative f ≠ 0
hg : ¬g.IsRoot a
hdfg0 : derivative f * g ≠ 0
hr' : rootMultiplicity a (derivative f * g) = rootMultiplicity a (f * r)
⊢ False

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'

Result:
case intro
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : CharZero R
f g : R[X]
hf0 : f ≠ 0
a : R
haf : f.IsRoot a
r : R[X]
hr : derivative f * g = f * r
hdf0 : derivative f ≠ 0
hg : ¬g.IsRoot a
hdfg0 : derivative f * g ≠ 0
hr' : rootMultiplicity a f = rootMultiplicity a r + rootMultiplicity a f + Nat.succ 0
⊢ False

Proof state:
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : CharZero R
f g : R[X]
hf0 : f ≠ 0
a : R
r : R[X]
hr : derivative f * g = f * r
haf : derivative f = 0
⊢ ¬f.IsRoot a

Tactic:
rw [eq_C_of_derivative_eq_zero haf] at hf0 ⊢

Result:
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : CharZero R
f g : R[X]
hf0 : C (f.coeff 0) ≠ 0
a : R
r : R[X]
hr : derivative f * g = f * r
haf : derivative f = 0
⊢ ¬(C (f.coeff 0)).IsRoot a

Proof state:
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : CharZero R
f g : R[X]
hf0 : f ≠ 0
a : R
haf : f.IsRoot a
r : R[X]
hr : derivative f * g = f * r
⊢ derivative f ≠ 0

Tactic:
contrapose! haf

Result:
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : CharZero R
f g : R[X]
hf0 : f ≠ 0
a : R
r : R[X]
hr : derivative f * g = f * r
haf : derivative f = 0
⊢ ¬f.IsRoot a

Proof state:
case intro
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : CharZero R
f g : R[X]
hf0 : f ≠ 0
a : R
haf : f.IsRoot a
r : R[X]
hr : derivative f * g = f * r
hdf0 : derivative f ≠ 0
⊢ g.IsRoot a

Tactic:
by_contra hg

Result:
case intro
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : CharZero R
f g : R[X]
hf0 : f ≠ 0
a : R
haf : f.IsRoot a
r : R[X]
hr : derivative f * g = f * r
hdf0 : derivative f ≠ 0
hg : ¬g.IsRoot a
⊢ False

Proof state:
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : CharZero R
f g : R[X]
hf0 : C (f.coeff 0) ≠ 0
a : R
r : R[X]
hr : derivative f * g = f * r
haf : derivative f = 0
⊢ ¬(C (f.coeff 0)).IsRoot a

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

Result:
no goals

Proof state:
case intro
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : CharZero R
f g : R[X]
hf0 : f ≠ 0
a : R
haf : f.IsRoot a
r : R[X]
hr : derivative f * g = f * r
hdf0 : derivative f ≠ 0
hg : ¬g.IsRoot a
hdfg0 : derivative f * g ≠ 0
hr' : rootMultiplicity a f = rootMultiplicity a r + rootMultiplicity a f + Nat.succ 0
⊢ False

Tactic:
omega

Result:
no goals

Proof state:
case intro
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : CharZero R
f g : R[X]
hf0 : f ≠ 0
a : R
haf : f.IsRoot a
r : R[X]
hr : derivative f * g = f * r
hdf0 : derivative f ≠ 0
hg : ¬g.IsRoot a
hdfg0 : derivative f * g ≠ 0
⊢ False

Tactic:
have hr' := congr_arg (rootMultiplicity a) hr

Result:
case intro
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : CharZero R
f g : R[X]
hf0 : f ≠ 0
a : R
haf : f.IsRoot a
r : R[X]
hr : derivative f * g = f * r
hdf0 : derivative f ≠ 0
hg : ¬g.IsRoot a
hdfg0 : derivative f * g ≠ 0
hr' : rootMultiplicity a (derivative f * g) = rootMultiplicity a (f * r)
⊢ False

Proof state:
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : CharZero R
f : R[X]
hf0 : f ≠ 0
a : R
haf : f.IsRoot a
r : R[X]
hdf0 : derivative f ≠ 0
hr : derivative f * 0 = f * r
hg : ¬IsRoot 0 a
⊢ False

Tactic:
simp at hg

Result:
no goals

Proof state:
case intro
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : CharZero R
f g : R[X]
hf0 : f ≠ 0
a : R
haf : f.IsRoot a
r : R[X]
hr : derivative f * g = f * r
hdf0 : derivative f ≠ 0
hg : ¬g.IsRoot a
⊢ False

Tactic:
have hdfg0 : f.derivative * g ≠ 0 := mul_ne_zero hdf0 (by rintro rfl; simp at hg)

Result:
case intro
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : CharZero R
f g : R[X]
hf0 : f ≠ 0
a : R
haf : f.IsRoot a
r : R[X]
hr : derivative f * g = f * r
hdf0 : derivative f ≠ 0
hg : ¬g.IsRoot a
hdfg0 : derivative f * g ≠ 0
⊢ False