-- Mathlib/RingTheory/Polynomial/Radical.lean
theorem divRadical_dvd_derivative (a : k[X]) : divRadical a ∣ derivative a

Proof state:
k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
a : k[X]
⊢ divRadical a ∣ derivative a

Tactic:
induction a using induction_on_coprime

Result:
case h0
k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
⊢ divRadical 0 ∣ derivative 0

case h1
k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
x✝ : k[X]
a✝ : IsUnit x✝
⊢ divRadical x✝ ∣ derivative x✝

case hpr
k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
p✝ : k[X]
i✝ : ℕ
a✝ : Prime p✝
⊢ divRadical (p✝ ^ i✝) ∣ derivative (p✝ ^ i✝)

case hcp
k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
x✝ y✝ : k[X]
a✝² : IsRelPrime x✝ y✝
a✝¹ : divRadical x✝ ∣ derivative x✝
a✝ : divRadical y✝ ∣ derivative y✝
⊢ divRadical (x✝ * y✝) ∣ derivative (x✝ * y✝)

Proof state:
k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
p : k[X]
hp : Prime p
i : ℕ
⊢ divRadical (p ^ (i + 1)) ∣ derivative (p ^ (i + 1))

Tactic:
rw [← mul_dvd_mul_iff_left (radical_ne_zero (p ^ i.succ)), radical_mul_divRadical,
  radical_pow_of_prime hp i.succ_pos, derivative_pow_succ, ← mul_assoc]

Result:
k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
p : k[X]
hp : Prime p
i : ℕ
⊢ p ^ i.succ ∣ normalize p * (C (↑i + 1) * p ^ i) * derivative p

Proof state:
case succ
k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
p : k[X]
hp : Prime p
n✝ : ℕ
⊢ divRadical (p ^ (n✝ + 1)) ∣ derivative (p ^ (n✝ + 1))

Tactic:
case succ i =>
rw [← mul_dvd_mul_iff_left (radical_ne_zero (p ^ i.succ)), radical_mul_divRadical,
  radical_pow_of_prime hp i.succ_pos, derivative_pow_succ, ← mul_assoc]
apply dvd_mul_of_dvd_left
rw [mul_comm, mul_assoc]
apply dvd_mul_of_dvd_right
rw [pow_succ, mul_dvd_mul_iff_left (pow_ne_zero i hp.ne_zero), dvd_normalize_iff]

Result:
no goals

Proof state:
k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
x y : k[X]
hpxy : IsRelPrime x y
hx : divRadical x ∣ derivative x
hy : divRadical y ∣ derivative y
hc : IsCoprime x y
⊢ divRadical x * divRadical y ∣ derivative x * y + x * derivative y

Tactic:
exact dvd_add (mul_dvd_mul hx (divRadical_dvd_self y)) (mul_dvd_mul (divRadical_dvd_self x) hy)

Result:
no goals

Proof state:
k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
⊢ divRadical 0 ∣ 0

Tactic:
apply dvd_zero

Result:
no goals

Proof state:
case h
k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
p : k[X]
hp : Prime p
i : ℕ
⊢ p ^ i.succ ∣ normalize p * (C (↑i + 1) * p ^ i)

Tactic:
rw [mul_comm, mul_assoc]

Result:
case h
k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
p : k[X]
hp : Prime p
i : ℕ
⊢ p ^ i.succ ∣ C (↑i + 1) * (p ^ i * normalize p)

Proof state:
case h.h
k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
p : k[X]
hp : Prime p
i : ℕ
⊢ p ^ i.succ ∣ p ^ i * normalize p

Tactic:
rw [pow_succ, mul_dvd_mul_iff_left (pow_ne_zero i hp.ne_zero), dvd_normalize_iff]

Result:
no goals

Proof state:
k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
⊢ divRadical 0 ∣ derivative 0

Tactic:
rw [derivative_zero]

Result:
k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
⊢ divRadical 0 ∣ 0

Proof state:
case h1
k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
x✝ : k[X]
a✝ : IsUnit x✝
⊢ divRadical x✝ ∣ derivative x✝

Tactic:
case h1 a ha =>
exact (divRadical_isUnit ha).dvd

Result:
no goals

Proof state:
k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
a : k[X]
ha : IsUnit a
⊢ divRadical a ∣ derivative a

Tactic:
exact (divRadical_isUnit ha).dvd

Result:
no goals

Proof state:
k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
p : k[X]
i : ℕ
hp : Prime p
⊢ divRadical (p ^ i) ∣ derivative (p ^ i)

Tactic:
cases i

Result:
case zero
k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
p : k[X]
hp : Prime p
⊢ divRadical (p ^ 0) ∣ derivative (p ^ 0)

case succ
k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
p : k[X]
hp : Prime p
n✝ : ℕ
⊢ divRadical (p ^ (n✝ + 1)) ∣ derivative (p ^ (n✝ + 1))

Proof state:
case hcp
k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
x✝ y✝ : k[X]
a✝² : IsRelPrime x✝ y✝
a✝¹ : divRadical x✝ ∣ derivative x✝
a✝ : divRadical y✝ ∣ derivative y✝
⊢ divRadical (x✝ * y✝) ∣ derivative (x✝ * y✝)

Tactic:
case hcp x y hpxy hx hy =>
have hc : IsCoprime x y :=
  EuclideanDomain.isCoprime_of_dvd
    (fun ⟨hx, hy⟩ => not_isUnit_zero (hpxy (zero_dvd_iff.mpr hx) (zero_dvd_iff.mpr hy)))
    fun p hp _ hpx hpy => hp (hpxy hpx hpy)
rw [divRadical_mul hc, derivative_mul]
exact dvd_add (mul_dvd_mul hx (divRadical_dvd_self y)) (mul_dvd_mul (divRadical_dvd_self x) hy)

Result:
no goals

Proof state:
k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
x y : k[X]
hpxy : IsRelPrime x y
hx : divRadical x ∣ derivative x
hy : divRadical y ∣ derivative y
⊢ divRadical (x * y) ∣ derivative (x * y)

Tactic:
have hc : IsCoprime x y :=
  EuclideanDomain.isCoprime_of_dvd
    (fun ⟨hx, hy⟩ => not_isUnit_zero (hpxy (zero_dvd_iff.mpr hx) (zero_dvd_iff.mpr hy)))
    fun p hp _ hpx hpy => hp (hpxy hpx hpy)

Result:
k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
x y : k[X]
hpxy : IsRelPrime x y
hx : divRadical x ∣ derivative x
hy : divRadical y ∣ derivative y
hc : IsCoprime x y
⊢ divRadical (x * y) ∣ derivative (x * y)

Proof state:
case zero
k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
p : k[X]
hp : Prime p
⊢ divRadical 1 ∣ 0

Tactic:
apply dvd_zero

Result:
no goals

Proof state:
k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
x y : k[X]
hpxy : IsRelPrime x y
hx : divRadical x ∣ derivative x
hy : divRadical y ∣ derivative y
hc : IsCoprime x y
⊢ divRadical (x * y) ∣ derivative (x * y)

Tactic:
rw [divRadical_mul hc, derivative_mul]

Result:
k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
x y : k[X]
hpxy : IsRelPrime x y
hx : divRadical x ∣ derivative x
hy : divRadical y ∣ derivative y
hc : IsCoprime x y
⊢ divRadical x * divRadical y ∣ derivative x * y + x * derivative y

Proof state:
case h
k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
p : k[X]
hp : Prime p
i : ℕ
⊢ p ^ i.succ ∣ C (↑i + 1) * (p ^ i * normalize p)

Tactic:
apply dvd_mul_of_dvd_right

Result:
case h.h
k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
p : k[X]
hp : Prime p
i : ℕ
⊢ p ^ i.succ ∣ p ^ i * normalize p

Proof state:
case h0
k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
⊢ divRadical 0 ∣ derivative 0

Tactic:
case h0 =>
rw [derivative_zero]
apply dvd_zero

Result:
no goals

Proof state:
k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
p : k[X]
hp : Prime p
i : ℕ
⊢ p ^ i.succ ∣ normalize p * (C (↑i + 1) * p ^ i) * derivative p

Tactic:
apply dvd_mul_of_dvd_left

Result:
case h
k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
p : k[X]
hp : Prime p
i : ℕ
⊢ p ^ i.succ ∣ normalize p * (C (↑i + 1) * p ^ i)

Proof state:
case zero
k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
p : k[X]
hp : Prime p
⊢ divRadical (p ^ 0) ∣ derivative (p ^ 0)

Tactic:
rw [pow_zero, derivative_one]

Result:
case zero
k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
p : k[X]
hp : Prime p
⊢ divRadical 1 ∣ 0