case intro
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q✝ : ℕ
q p : R[X]
hp : Separable (q * q * p)
⊢ IsUnit q
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q✝ : ℕ
p q : R[X]
hp : Separable p
hq : q * q ∣ p
⊢ IsUnit q
obtain ⟨p, rfl⟩ := hq
case intro
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q✝ : ℕ
q p : R[X]
hp : Separable (q * q * p)
⊢ IsCoprime q q
case intro
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q✝ : ℕ
q p : R[X]
hp : Separable (q * q * p)
⊢ IsUnit q
apply isCoprime_self.mp
case intro
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q✝ : ℕ
q p : R[X]
hp : Separable (q * q * p)
this : IsCoprime (q * (q * p)) (q * (↑derivative q * p + ↑derivative q * p + q * ↑derivative p))
⊢ IsCoprime q q
case intro
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q✝ : ℕ
q p : R[X]
hp : Separable (q * q * p)
⊢ IsCoprime q q
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
no goals
case intro
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q✝ : ℕ
q p : R[X]
hp : Separable (q * q * p)
this : IsCoprime (q * (q * p)) (q * (↑derivative q * p + ↑derivative q * p + q * ↑derivative p))
⊢ IsCoprime q q
exact IsCoprime.of_mul_right_left (IsCoprime.of_mul_left_left this)
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q✝ : ℕ
q p : R[X]
hp : Separable (q * q * p)
⊢ IsCoprime (q * q * p) (q * ↑derivative q * p + q * ↑derivative q * p + q * q * ↑derivative p)
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q✝ : ℕ
q p : R[X]
hp : Separable (q * q * p)
⊢ IsCoprime (q * (q * p)) (q * (↑derivative q * p + ↑derivative q * p + q * ↑derivative p))
simp only [← mul_assoc, mul_add]
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q✝ : ℕ
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)
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q✝ : ℕ
q p : R[X]
hp : Separable (q * q * p)
⊢ IsCoprime (q * q * p) (q * ↑derivative q * p + q * ↑derivative q * p + q * q * ↑derivative p)
dsimp only [Separable] at hp
case h.e'_4
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q✝ : ℕ
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)
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q✝ : ℕ
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)
convert hp using 1
case h.e'_4
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q✝ : ℕ
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
case h.e'_4
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q✝ : ℕ
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)
rw [derivative_mul, derivative_mul]
no goals
case h.e'_4
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q✝ : ℕ
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
ring