-- Mathlib/RingTheory/Polynomial/Wronskian.lean
theorem _root_.IsCoprime.wronskian_eq_zero_iff
    [NoZeroDivisors R] {a b : R[X]} (hc : IsCoprime a b) :
    wronskian a b = 0 ↔ derivative a = 0 ∧ derivative b = 0 where
  mp hw

Proof state:
case left
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
a b : R[X]
hc : IsCoprime a b
hw : a * derivative b = derivative a * b
⊢ derivative a = 0

Tactic:
rw [← dvd_derivative_iff]

Result:
case left
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
a b : R[X]
hc : IsCoprime a b
hw : a * derivative b = derivative a * b
⊢ a ∣ derivative a

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
a b : R[X]
hc : IsCoprime a b
hw : a * derivative b = derivative a * b
⊢ derivative a = 0 ∧ derivative b = 0

Tactic:
constructor

Result:
case left
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
a b : R[X]
hc : IsCoprime a b
hw : a * derivative b = derivative a * b
⊢ derivative a = 0

case right
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
a b : R[X]
hc : IsCoprime a b
hw : a * derivative b = derivative a * b
⊢ derivative b = 0

Proof state:
case intro
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
a b : R[X]
hc : IsCoprime a b
hda : derivative a = 0
hdb : derivative b = 0
⊢ a * derivative b - derivative a * b = 0

Tactic:
rw [hda, hdb]

Result:
case intro
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
a b : R[X]
hc : IsCoprime a b
hda : derivative a = 0
hdb : derivative b = 0
⊢ a * 0 - 0 * b = 0

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
a b : R[X]
hc : IsCoprime a b
hdab : derivative a = 0 ∧ derivative b = 0
⊢ a.wronskian b = 0

Tactic:
obtain ⟨hda, hdb⟩ := hdab

Result:
case intro
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
a b : R[X]
hc : IsCoprime a b
hda : derivative a = 0
hdb : derivative b = 0
⊢ a.wronskian b = 0

Proof state:
case right
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
a b : R[X]
hc : IsCoprime a b
hw : a * derivative b = derivative a * b
⊢ b ∣ derivative b

Tactic:
apply hc.symm.dvd_of_dvd_mul_left

Result:
case right
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
a b : R[X]
hc : IsCoprime a b
hw : a * derivative b = derivative a * b
⊢ b ∣ a * derivative b

Proof state:
case intro
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
a b : R[X]
hc : IsCoprime a b
hda : derivative a = 0
hdb : derivative b = 0
⊢ a.wronskian b = 0

Tactic:
rw [wronskian]

Result:
case intro
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
a b : R[X]
hc : IsCoprime a b
hda : derivative a = 0
hdb : derivative b = 0
⊢ a * derivative b - derivative a * b = 0

Proof state:
case left
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
a b : R[X]
hc : IsCoprime a b
hw : a * derivative b = derivative a * b
⊢ a ∣ a * derivative b

Tactic:
exact dvd_mul_right _ _

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
a b : R[X]
hc : IsCoprime a b
hw : a.wronskian b = 0
⊢ derivative a = 0 ∧ derivative b = 0

Tactic:
rw [wronskian, sub_eq_iff_eq_add, zero_add] at hw

Result:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
a b : R[X]
hc : IsCoprime a b
hw : a * derivative b = derivative a * b
⊢ derivative a = 0 ∧ derivative b = 0

Proof state:
case right
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
a b : R[X]
hc : IsCoprime a b
hw : a * derivative b = derivative a * b
⊢ derivative b = 0

Tactic:
rw [← dvd_derivative_iff]

Result:
case right
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
a b : R[X]
hc : IsCoprime a b
hw : a * derivative b = derivative a * b
⊢ b ∣ derivative b

Proof state:
case right
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
a b : R[X]
hc : IsCoprime a b
hw : a * derivative b = derivative a * b
⊢ b ∣ derivative a * b

Tactic:
exact dvd_mul_left _ _

Result:
no goals

Proof state:
case right
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
a b : R[X]
hc : IsCoprime a b
hw : a * derivative b = derivative a * b
⊢ b ∣ a * derivative b

Tactic:
rw [hw]

Result:
case right
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
a b : R[X]
hc : IsCoprime a b
hw : a * derivative b = derivative a * b
⊢ b ∣ derivative a * b

Proof state:
case left
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
a b : R[X]
hc : IsCoprime a b
hw : a * derivative b = derivative a * b
⊢ a ∣ derivative a * b

Tactic:
rw [← hw]

Result:
case left
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
a b : R[X]
hc : IsCoprime a b
hw : a * derivative b = derivative a * b
⊢ a ∣ a * derivative b

Proof state:
case left
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
a b : R[X]
hc : IsCoprime a b
hw : a * derivative b = derivative a * b
⊢ a ∣ derivative a

Tactic:
apply hc.dvd_of_dvd_mul_right

Result:
case left
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
a b : R[X]
hc : IsCoprime a b
hw : a * derivative b = derivative a * b
⊢ a ∣ derivative a * b

Proof state:
case intro
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
a b : R[X]
hc : IsCoprime a b
hda : derivative a = 0
hdb : derivative b = 0
⊢ a * 0 - 0 * b = 0

Tactic:
simp only [MulZeroClass.mul_zero, MulZeroClass.zero_mul, sub_self]

Result:
no goals