-- Mathlib/FieldTheory/Separable.lean
theorem isUnit_of_self_mul_dvd_separable {p q : R[X]} (hp : p.Separable) (hq : q * q ∣ p) :
    IsUnit q

Proof state:
R : Type u
inst✝ : CommSemiring R
q p : R[X]
hp : IsCoprime (q * q * p) (derivative (q * q * p))
⊢ IsCoprime (q * q * p) (q * derivative q * p + q * derivative q * p + q * q * derivative p)

Tactic:
convert hp using 1

Result:
case h.e'_4
R : Type u
inst✝ : CommSemiring R
q p : R[X]
hp : IsCoprime (q * q * p) (derivative (q * q * p))
⊢ q * derivative q * p + q * derivative q * p + q * q * derivative p = derivative (q * q * p)

Proof state:
case intro
R : Type u
inst✝ : CommSemiring R
q p : R[X]
hp : (q * q * p).Separable
this : IsCoprime (q * (q * p)) (q * (derivative q * p + derivative q * p + q * derivative p))
⊢ IsCoprime q q

Tactic:
exact IsCoprime.of_mul_right_left (IsCoprime.of_mul_left_left this)

Result:
no goals

Proof state:
R : Type u
inst✝ : CommSemiring R
q p : R[X]
hp : (q * q * p).Separable
⊢ IsCoprime (q * q * p) (q * derivative q * p + q * derivative q * p + q * q * derivative p)

Tactic:
dsimp only [Separable] at hp

Result:
R : Type u
inst✝ : CommSemiring R
q p : R[X]
hp : IsCoprime (q * q * p) (derivative (q * q * p))
⊢ IsCoprime (q * q * p) (q * derivative q * p + q * derivative q * p + q * q * derivative p)

Proof state:
case intro
R : Type u
inst✝ : CommSemiring R
q p : R[X]
hp : (q * q * p).Separable
⊢ IsUnit q

Tactic:
apply isCoprime_self.mp

Result:
case intro
R : Type u
inst✝ : CommSemiring R
q p : R[X]
hp : (q * q * p).Separable
⊢ IsCoprime q q

Proof state:
case h.e'_4
R : Type u
inst✝ : CommSemiring R
q p : R[X]
hp : IsCoprime (q * q * p) (derivative (q * q * p))
⊢ q * derivative q * p + q * derivative q * p + q * q * derivative p = derivative (q * q * p)

Tactic:
rw [derivative_mul, derivative_mul]

Result:
case h.e'_4
R : Type u
inst✝ : CommSemiring R
q p : R[X]
hp : IsCoprime (q * q * p) (derivative (q * q * p))
⊢ q * derivative q * p + q * derivative q * p + q * q * derivative p =
    (derivative q * q + q * derivative q) * p + q * q * derivative p

Proof state:
case intro
R : Type u
inst✝ : CommSemiring R
q p : R[X]
hp : (q * q * p).Separable
⊢ IsCoprime q q

Tactic:
have : IsCoprime (q * (q * p))
    (q * (derivative q * p + derivative q * p + q * derivative p)) := by
  simp only [← mul_assoc, mul_add]
  dsimp only [Separable] at hp
  convert hp using 1
  rw [derivative_mul, derivative_mul]
  ring

Result:
case intro
R : Type u
inst✝ : CommSemiring R
q p : R[X]
hp : (q * q * p).Separable
this : IsCoprime (q * (q * p)) (q * (derivative q * p + derivative q * p + q * derivative p))
⊢ IsCoprime q q

Proof state:
case h.e'_4
R : Type u
inst✝ : CommSemiring R
q p : R[X]
hp : IsCoprime (q * q * p) (derivative (q * q * p))
⊢ q * derivative q * p + q * derivative q * p + q * q * derivative p =
    (derivative q * q + q * derivative q) * p + q * q * derivative p

Tactic:
ring

Result:
no goals

Proof state:
R : Type u
inst✝ : CommSemiring R
q p : R[X]
hp : (q * q * p).Separable
⊢ IsCoprime (q * (q * p)) (q * (derivative q * p + derivative q * p + q * derivative p))

Tactic:
simp only [← mul_assoc, mul_add]

Result:
R : Type u
inst✝ : CommSemiring R
q p : R[X]
hp : (q * q * p).Separable
⊢ IsCoprime (q * q * p) (q * derivative q * p + q * derivative q * p + q * q * derivative p)

Proof state:
R : Type u
inst✝ : CommSemiring R
p q : R[X]
hp : p.Separable
hq : q * q ∣ p
⊢ IsUnit q

Tactic:
obtain ⟨p, rfl⟩ := hq

Result:
case intro
R : Type u
inst✝ : CommSemiring R
q p : R[X]
hp : (q * q * p).Separable
⊢ IsUnit q