-- Mathlib/NumberTheory/FLT/MasonStothers.lean
theorem Polynomial.abc
    {a b c : k[X]} (ha : a ≠ 0) (hb : b ≠ 0) (hc : c ≠ 0)
    (hab : IsCoprime a b) (hsum : a + b + c = 0) :
    ( natDegree a + 1 ≤ (radical (a * b * c)).natDegree ∧
      natDegree b + 1 ≤ (radical (a * b * c)).natDegree ∧
      natDegree c + 1 ≤ (radical (a * b * c)).natDegree ) ∨
      derivative a = 0 ∧ derivative b = 0 ∧ derivative c = 0

Proof state:
k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
hsum : a + b + c = 0
w : k[X] := a.wronskian b
wab : w = a.wronskian b
hbc : IsCoprime b c
hsum' : b + c + a = 0
hca : IsCoprime c a
wbc : w = b.wronskian c
wca : w = c.wronskian a
adr_dvd_w : divRadical a ∣ w
bdr_dvd_w : divRadical b ∣ w
cdr_dvd_w : divRadical c ∣ w
⊢ divRadical a * divRadical b * divRadical c ∣ w

Tactic:
exact (hca.divRadical.symm.mul_left hbc.divRadical).mul_dvd
  (hab.divRadical.mul_dvd adr_dvd_w bdr_dvd_w) cdr_dvd_w

Result:
no goals

Proof state:
k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
hsum : a + b + c = 0
w : k[X] := a.wronskian b
wab : w = a.wronskian b
hbc : IsCoprime b c
hsum' : b + c + a = 0
hca : IsCoprime c a
wbc : w = b.wronskian c
wca : w = c.wronskian a
adr_dvd_w : divRadical a ∣ w
bdr_dvd_w : divRadical b ∣ w
cdr_dvd_w : divRadical c ∣ b.wronskian c
⊢ divRadical (a * b * c) ∣ w

Tactic:
rw [← wbc] at cdr_dvd_w

Result:
k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
hsum : a + b + c = 0
w : k[X] := a.wronskian b
wab : w = a.wronskian b
hbc : IsCoprime b c
hsum' : b + c + a = 0
hca : IsCoprime c a
wbc : w = b.wronskian c
wca : w = c.wronskian a
adr_dvd_w : divRadical a ∣ w
bdr_dvd_w : divRadical b ∣ w
cdr_dvd_w : divRadical c ∣ w
⊢ divRadical (a * b * c) ∣ w

Proof state:
k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
hsum : a + b + c = 0
w : k[X] := a.wronskian b
wab : w = a.wronskian b
hbc : IsCoprime b c
⊢ b + c + a = 0

Tactic:
rwa [add_rotate] at hsum

Result:
no goals

Proof state:
case pos.h
k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
hsum : a + b + c = 0
w : k[X] := a.wronskian b
wab : w = a.wronskian b
hbc : IsCoprime b c
hsum' : b + c + a = 0
hca : IsCoprime c a
wbc : w = b.wronskian c
wca : w = c.wronskian a
abc_dr_dvd_w : divRadical (a * b * c) ∣ w
hw : w = 0
⊢ derivative a = 0 ∧ derivative b = 0 ∧ derivative c = 0

Tactic:
rw [hw] at wab wbc

Result:
case pos.h
k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
hsum : a + b + c = 0
w : k[X] := a.wronskian b
wab : 0 = a.wronskian b
hbc : IsCoprime b c
hsum' : b + c + a = 0
hca : IsCoprime c a
wbc : 0 = b.wronskian c
wca : w = c.wronskian a
abc_dr_dvd_w : divRadical (a * b * c) ∣ w
hw : w = 0
⊢ derivative a = 0 ∧ derivative b = 0 ∧ derivative c = 0

Proof state:
case pos.h.intro
k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
hsum : a + b + c = 0
w : k[X] := a.wronskian b
wab : 0 = a.wronskian b
hbc : IsCoprime b c
hsum' : b + c + a = 0
hca : IsCoprime c a
wbc : 0 = b.wronskian c
wca : w = c.wronskian a
abc_dr_dvd_w : divRadical (a * b * c) ∣ w
hw : w = 0
ga : derivative a = 0
gb : derivative b = 0
⊢ derivative a = 0 ∧ derivative b = 0 ∧ derivative c = 0

Tactic:
obtain ⟨_, gc⟩ := hbc.wronskian_eq_zero_iff.mp wbc.symm

Result:
case pos.h.intro.intro
k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
hsum : a + b + c = 0
w : k[X] := a.wronskian b
wab : 0 = a.wronskian b
hbc : IsCoprime b c
hsum' : b + c + a = 0
hca : IsCoprime c a
wbc : 0 = b.wronskian c
wca : w = c.wronskian a
abc_dr_dvd_w : divRadical (a * b * c) ∣ w
hw : w = 0
ga : derivative a = 0
gb left✝ : derivative b = 0
gc : derivative c = 0
⊢ derivative a = 0 ∧ derivative b = 0 ∧ derivative c = 0

Proof state:
k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
hsum : -(a + b) = c
w : k[X] := a.wronskian b
wab : w = a.wronskian b
⊢ IsCoprime b (a + b)

Tactic:
convert IsCoprime.add_mul_left_right hab.symm 1

Result:
case h.e'_4.h.e'_6
k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
hsum : -(a + b) = c
w : k[X] := a.wronskian b
wab : w = a.wronskian b
⊢ b = b * 1

Proof state:
k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
hsum : a + b + c = 0
w : k[X] := a.wronskian b
wab : w = a.wronskian b
hbc : IsCoprime b c
hsum' : b + c + a = 0
hca : IsCoprime c a
wbc : w = b.wronskian c
wca : w = c.wronskian a
abc_dr_dvd_w : divRadical (a * b * c) ∣ w
⊢ a.natDegree + 1 ≤ (radical (a * b * c)).natDegree ∧
      b.natDegree + 1 ≤ (radical (a * b * c)).natDegree ∧ c.natDegree + 1 ≤ (radical (a * b * c)).natDegree ∨
    derivative a = 0 ∧ derivative b = 0 ∧ derivative c = 0

Tactic:
by_cases hw : w = 0

Result:
case pos
k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
hsum : a + b + c = 0
w : k[X] := a.wronskian b
wab : w = a.wronskian b
hbc : IsCoprime b c
hsum' : b + c + a = 0
hca : IsCoprime c a
wbc : w = b.wronskian c
wca : w = c.wronskian a
abc_dr_dvd_w : divRadical (a * b * c) ∣ w
hw : w = 0
⊢ a.natDegree + 1 ≤ (radical (a * b * c)).natDegree ∧
      b.natDegree + 1 ≤ (radical (a * b * c)).natDegree ∧ c.natDegree + 1 ≤ (radical (a * b * c)).natDegree ∨
    derivative a = 0 ∧ derivative b = 0 ∧ derivative c = 0

case neg
k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
hsum : a + b + c = 0
w : k[X] := a.wronskian b
wab : w = a.wronskian b
hbc : IsCoprime b c
hsum' : b + c + a = 0
hca : IsCoprime c a
wbc : w = b.wronskian c
wca : w = c.wronskian a
abc_dr_dvd_w : divRadical (a * b * c) ∣ w
hw : ¬w = 0
⊢ a.natDegree + 1 ≤ (radical (a * b * c)).natDegree ∧
      b.natDegree + 1 ≤ (radical (a * b * c)).natDegree ∧ c.natDegree + 1 ≤ (radical (a * b * c)).natDegree ∨
    derivative a = 0 ∧ derivative b = 0 ∧ derivative c = 0

Proof state:
k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
hsum : a + b + c = 0
w : k[X] := a.wronskian b
wab : w = a.wronskian b
hbc : IsCoprime b c
hsum' : b + c + a = 0
hca : IsCoprime c a
wbc : w = b.wronskian c
⊢ a.natDegree + 1 ≤ (radical (a * b * c)).natDegree ∧
      b.natDegree + 1 ≤ (radical (a * b * c)).natDegree ∧ c.natDegree + 1 ≤ (radical (a * b * c)).natDegree ∨
    derivative a = 0 ∧ derivative b = 0 ∧ derivative c = 0

Tactic:
have wca : w = wronskian c a := by
  rw [add_rotate] at hsum
  simpa only [← wbc] using wronskian_eq_of_sum_zero hsum

Result:
k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
hsum : a + b + c = 0
w : k[X] := a.wronskian b
wab : w = a.wronskian b
hbc : IsCoprime b c
hsum' : b + c + a = 0
hca : IsCoprime c a
wbc : w = b.wronskian c
wca : w = c.wronskian a
⊢ a.natDegree + 1 ≤ (radical (a * b * c)).natDegree ∧
      b.natDegree + 1 ≤ (radical (a * b * c)).natDegree ∧ c.natDegree + 1 ≤ (radical (a * b * c)).natDegree ∨
    derivative a = 0 ∧ derivative b = 0 ∧ derivative c = 0