awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.FLT.MasonStothers
Goal:
k : Type u_1
inst : Field k
inst_1 : DecidableEq k
a b c w : k[X]
hw : w ≠ 0
wab : w = a.wronskian b
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
ab_nz : a * b ≠ 0
abc_nz : a * b * c ≠ 0
abc_dr : k[X] := divRadical (a * b * c)
abc_dr_dvd_w : abc_dr ∣ w
abc_dr_ndeg_lt : abc_dr.natDegree < a.natDegree + b.natDegree
abc_r : k[X] := radical (a * b * c)
a₁ : a.natDegree + b.natDegree + c.natDegree < a.natDegree + b.natDegree + abc_r.natDegree
n : ℕ
⊢ c.natDegree + 1 ≤ abc_r.natDegree

Tactic:
apply Nat.lt_of_add_lt_add_left

Premises used: Nat.lt_of_add_lt_add_left
-- Module: Mathlib.NumberTheory.FLT.MasonStothers
Goal:
k : Type u_1
inst : Field k
inst_1 : DecidableEq k
a b c w : k[X]
hw : w ≠ 0
wab : w = a.wronskian b
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
ab_nz : a * b ≠ 0
abc_nz : a * b * c ≠ 0
abc_dr : k[X] := divRadical (a * b * c)
abc_dr_dvd_w : abc_dr ∣ w
abc_dr_ndeg_lt : abc_dr.natDegree < a.natDegree + b.natDegree
abc_r : k[X] := radical (a * b * c)
rw : a.natDegree + b.natDegree + c.natDegree = (a * b).natDegree + c.natDegree
rw₁ rw₂ : a.natDegree + b.natDegree + c.natDegree = a.natDegree + b.natDegree + c.natDegree
⊢ a.natDegree + b.natDegree + c.natDegree = (a * b * c).natDegree

Tactic:
rw [Polynomial.natDegree_mul ab_nz hc, Polynomial.natDegree_mul ha hb]

Premises used: Polynomial.natDegree_mul
-- Module: Mathlib.NumberTheory.FLT.MasonStothers
Goal:
k : Type u_1
inst : Field k
inst_1 : DecidableEq k
a b c w : k[X]
hw : w ≠ 0
wab : w = a.wronskian b
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
ab_nz : a * b ≠ 0
abc_nz : a * b * c ≠ 0
abc_dr : k[X] := divRadical (a * b * c)
abc_dr_dvd_w : abc_dr ∣ w
abc_dr_ndeg_lt : abc_dr.natDegree < a.natDegree + b.natDegree
abc_r : k[X] := radical (a * b * c)
rw : (a * b * c).natDegree = (radical (a * b * c) * divRadical (a * b * c)).natDegree
rw₁ rw₂ : (a * b * c).natDegree = (a * b * c).natDegree
⊢ (a * b * c).natDegree = (divRadical (a * b * c) * radical (a * b * c)).natDegree

Tactic:
rw [mul_comm _ (radical _), radical_mul_divRadical]

Premises used: EuclideanDomain.radical_mul_divRadical, UniqueFactorizationMonoid.radical, mul_comm
-- Module: Mathlib.NumberTheory.FLT.MasonStothers
Goal:
k : Type u_1
inst : Field k
inst_1 : DecidableEq k
a b c w : k[X]
hw : w ≠ 0
wab : w = a.wronskian b
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
ab_nz : a * b ≠ 0
abc_nz : a * b * c ≠ 0
abc_dr : k[X] := divRadical (a * b * c)
abc_dr_dvd_w : abc_dr ∣ w
abc_dr_ndeg_lt : abc_dr.natDegree < a.natDegree + b.natDegree
abc_r : k[X] := radical (a * b * c)
rw rw₁ :
  (divRadical (a * b * c) * radical (a * b * c)).natDegree = (divRadical (a * b * c) * radical (a * b * c)).natDegree
⊢ (divRadical (a * b * c) * radical (a * b * c)).natDegree = abc_dr.natDegree + abc_r.natDegree

Tactic:
rw [← Polynomial.natDegree_mul (divRadical_ne_zero abc_nz) radical_ne_zero]

Premises used: Polynomial.natDegree_mul, UniqueFactorizationMonoid.radical_ne_zero, EuclideanDomain.divRadical_ne_zero
-- Module: Mathlib.NumberTheory.FLT.MasonStothers
Goal:
k : Type u_1
inst : Field k
inst_1 : DecidableEq k
a b c w : k[X]
hw : w ≠ 0
wab : w = a.wronskian b
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
ab_nz : a * b ≠ 0
abc_nz : a * b * c ≠ 0
abc_dr : k[X] := divRadical (a * b * c)
abc_dr_dvd_w : abc_dr ∣ w
abc_dr_ndeg_lt : abc_dr.natDegree < a.natDegree + b.natDegree
abc_r : k[X] := radical (a * b * c)
⊢ abc_dr.natDegree + abc_r.natDegree < a.natDegree + b.natDegree + abc_r.natDegree

Tactic:
Nat.add_lt_add_right abc_dr_ndeg_lt _

Premises used: Nat.add_lt_add_right
-- Module: Mathlib.NumberTheory.FLT.MasonStothers
Goal:
k : Type u_1
inst : Field k
inst_1 : DecidableEq k
a b c w : k[X]
hw : w ≠ 0
wab : w = a.wronskian b
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
ab_nz : a * b ≠ 0
abc_nz : a * b * c ≠ 0
abc_dr : k[X] := divRadical (a * b * c)
abc_dr_dvd_w : abc_dr ∣ w
abc_dr_ndeg_lt : abc_dr.natDegree < a.natDegree + b.natDegree
abc_r : k[X] := radical (a * b * c)
⊢ abc_dr.natDegree + abc_r.natDegree < a.natDegree + b.natDegree + abc_r.natDegree

Tactic:
exact Nat.add_lt_add_right abc_dr_ndeg_lt _

Premises used: Nat.add_lt_add_right
-- Module: Mathlib.NumberTheory.FLT.MasonStothers
Goal:
k : Type u_1
inst : Field k
inst_1 : DecidableEq k
a b c w : k[X]
hw : w ≠ 0
wab : w = a.wronskian b
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
ab_nz : a * b ≠ 0
abc_nz : a * b * c ≠ 0
abc_dr : k[X] := divRadical (a * b * c)
abc_dr_dvd_w : abc_dr ∣ w
abc_dr_ndeg_lt : abc_dr.natDegree < a.natDegree + b.natDegree
abc_r : k[X] := radical (a * b * c)
b₁ : a.natDegree + b.natDegree + c.natDegree = (a * b * c).natDegree
b₂ : (a * b * c).natDegree = (divRadical (a * b * c) * radical (a * b * c)).natDegree
b₃ : (divRadical (a * b * c) * radical (a * b * c)).natDegree = abc_dr.natDegree + abc_r.natDegree
b₄ : abc_dr.natDegree + abc_r.natDegree < a.natDegree + b.natDegree + abc_r.natDegree
⊢ ℕ

Tactic:
a.natDegree + b.natDegree + c.natDegree = (a * b * c).natDegree := by
      rw [Polynomial.natDegree_mul ab_nz hc, Polynomial.natDegree_mul ha hb]
    _ = ((divRadical (a * b * c)) * (radical (a * b * c))).natDegree := by
      rw [mul_comm _ (radical _), radical_mul_divRadical]
    _ = abc_dr.natDegree + abc_r.natDegree := by
      rw [← Polynomial.natDegree_mul (divRadical_ne_zero abc_nz) radical_ne_zero]
    _ < a.natDegree + b.natDegree + abc_r.natDegree := by
      exact Nat.add_lt_add_right abc_dr_ndeg_lt _

Premises used: HMul.hMul, UniqueFactorizationMonoid.radical, Polynomial.natDegree, EuclideanDomain.divRadical
-- Module: Mathlib.NumberTheory.FLT.MasonStothers
Goal:
k : Type u_1
inst : Field k
inst_1 : DecidableEq k
a b c w : k[X]
hw : w ≠ 0
wab : w = a.wronskian b
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
ab_nz : a * b ≠ 0
abc_nz : a * b * c ≠ 0
abc_dr : k[X] := divRadical (a * b * c)
abc_dr_dvd_w : abc_dr ∣ w
abc_dr_ndeg_lt : abc_dr.natDegree < a.natDegree + b.natDegree
abc_r : k[X] := radical (a * b * c)
⊢ a.natDegree + b.natDegree + c.natDegree < a.natDegree + b.natDegree + abc_r.natDegree

Tactic:
calc
    a.natDegree + b.natDegree + c.natDegree = (a * b * c).natDegree := by
      rw [Polynomial.natDegree_mul ab_nz hc, Polynomial.natDegree_mul ha hb]
    _ = ((divRadical (a * b * c)) * (radical (a * b * c))).natDegree := by
      rw [mul_comm _ (radical _), radical_mul_divRadical]
    _ = abc_dr.natDegree + abc_r.natDegree := by
      rw [← Polynomial.natDegree_mul (divRadical_ne_zero abc_nz) radical_ne_zero]
    _ < a.natDegree + b.natDegree + abc_r.natDegree := by
      exact Nat.add_lt_add_right abc_dr_ndeg_lt _

Premises used: HMul.hMul, UniqueFactorizationMonoid.radical, Polynomial.natDegree, EuclideanDomain.divRadical
-- Module: Mathlib.NumberTheory.FLT.MasonStothers
Goal:
k : Type u_1
inst : Field k
inst_1 : 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
⊢ let w := a.wronskian b;
  w = a.wronskian b

Tactic:
set w := wronskian a b with wab

Premises used: Polynomial.wronskian
-- Module: Mathlib.NumberTheory.FLT.MasonStothers
Goal:
k : Type u_1
inst : Field k
inst_1 : 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
⊢ -(a + b) = c

Tactic:
rw [add_eq_zero_iff_neg_eq] at hsum

Premises used: add_eq_zero_iff_neg_eq
-- Module: Mathlib.NumberTheory.FLT.MasonStothers
Goal:
k : Type u_1
inst : Field k
inst_1 : 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
hsum₁ : -(a + b) = c
⊢ let w := a.wronskian b;
  w = a.wronskian b

Tactic:
rw [add_eq_zero_iff_neg_eq] at hsum

Premises used: add_eq_zero_iff_neg_eq
-- Module: Mathlib.NumberTheory.FLT.MasonStothers
Goal:
k : Type u_1
inst : Field k
inst_1 : 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
rw : IsCoprime b (a + b)
⊢ IsCoprime b c

Tactic:
rw [← hsum, IsCoprime.neg_right_iff]

Premises used: IsCoprime.neg_right_iff
-- Module: Mathlib.NumberTheory.FLT.MasonStothers
Goal:
k : Type u_1
inst : Field k
inst_1 : 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 * 1)

Tactic:
IsCoprime.add_mul_left_right hab.symm 1

Premises used: IsCoprime.symm, OfNat.ofNat, IsCoprime.add_mul_left_right
-- Module: Mathlib.NumberTheory.FLT.MasonStothers
Goal:
k : Type u_1
inst : Field k
inst_1 : 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
h : b = b * 1
⊢ IsCoprime b (a + b)

Tactic:
convert! IsCoprime.add_mul_left_right hab.symm 1

Premises used: IsCoprime.symm, OfNat.ofNat, IsCoprime.add_mul_left_right
-- Module: Mathlib.NumberTheory.FLT.MasonStothers
Goal:
k : Type u_1
inst : Field k
inst_1 : 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
h h₁ : b = b
⊢ b = b * 1

Tactic:
rw [mul_one]

Premises used: mul_one
-- Module: Mathlib.NumberTheory.FLT.MasonStothers
Goal:
k : Type u_1
inst : Field k
inst_1 : 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
⊢ IsCoprime b c

Tactic:
have hbc : IsCoprime b c := by
    rw [add_eq_zero_iff_neg_eq] at hsum
    rw [← hsum, IsCoprime.neg_right_iff]
    convert! IsCoprime.add_mul_left_right hab.symm 1
    rw [mul_one]
-- Module: Mathlib.NumberTheory.FLT.MasonStothers
Goal:
k : Type u_1
inst : Field k
inst_1 : 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
rwa rwa₁ rwa₂ rwa₃ :
  ∀ (hsum : b + c + a = 0),
    let w := a.wronskian b;
    ∀ (wab : w = a.wronskian b) (hbc : IsCoprime b c), b + c + a = 0
⊢ b + c + a = 0

Tactic:
rwa [add_rotate] at hsum

Premises used: add_rotate
-- Module: Mathlib.NumberTheory.FLT.MasonStothers
Goal:
k : Type u_1
inst : Field k
inst_1 : 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:
have hsum' : b + c + a = 0 := by rwa [add_rotate] at hsum
-- Module: Mathlib.NumberTheory.FLT.MasonStothers
Goal:
k : Type u_1
inst : Field k
inst_1 : 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
⊢ -(b + c) = a

Tactic:
rw [add_eq_zero_iff_neg_eq] at hsum'

Premises used: add_eq_zero_iff_neg_eq
-- Module: Mathlib.NumberTheory.FLT.MasonStothers
Goal:
k : Type u_1
inst : Field k
inst_1 : 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
rw : IsCoprime c (b + c)
⊢ IsCoprime c a

Tactic:
rw [← hsum', IsCoprime.neg_right_iff]

Premises used: IsCoprime.neg_right_iff
-- Module: Mathlib.NumberTheory.FLT.MasonStothers
Goal:
k : Type u_1
inst : Field k
inst_1 : 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
⊢ IsCoprime c (b + c * 1)

Tactic:
IsCoprime.add_mul_left_right hbc.symm 1

Premises used: IsCoprime.symm, OfNat.ofNat, IsCoprime.add_mul_left_right
-- Module: Mathlib.NumberTheory.FLT.MasonStothers
Goal:
k : Type u_1
inst : Field k
inst_1 : 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
h : c = c * 1
⊢ IsCoprime c (b + c)

Tactic:
convert! IsCoprime.add_mul_left_right hbc.symm 1

Premises used: IsCoprime.symm, OfNat.ofNat, IsCoprime.add_mul_left_right
-- Module: Mathlib.NumberTheory.FLT.MasonStothers
Goal:
k : Type u_1
inst : Field k
inst_1 : 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
h h₁ : c = c
⊢ c = c * 1

Tactic:
rw [mul_one]

Premises used: mul_one
-- Module: Mathlib.NumberTheory.FLT.MasonStothers
Goal:
k : Type u_1
inst : Field k
inst_1 : 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
⊢ IsCoprime c a

Tactic:
have hca : IsCoprime c a := by
    rw [add_eq_zero_iff_neg_eq] at hsum'
    rw [← hsum', IsCoprime.neg_right_iff]
    convert! IsCoprime.add_mul_left_right hbc.symm 1
    rw [mul_one]
-- Module: Mathlib.NumberTheory.FLT.MasonStothers
Goal:
k : Type u_1
inst : Field k
inst_1 : 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
⊢ w = b.wronskian c

Tactic:
have wbc : w = wronskian b c := wronskian_eq_of_sum_zero hsum
-- Module: Mathlib.NumberTheory.FLT.MasonStothers
Goal:
k : Type u_1
inst : Field k
inst_1 : 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
rw :
  ∀ (hsum : b + c + a = 0),
    let w := 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), w = c.wronskian a
⊢ w = c.wronskian a

Tactic:
rw [add_rotate] at hsum

Premises used: add_rotate
-- Module: Mathlib.NumberTheory.FLT.MasonStothers
Goal:
k : Type u_1
inst : Field k
inst_1 : DecidableEq k
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
hsum : b + c + a = 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
⊢ w = c.wronskian a

Tactic:
simpa only [← wbc] using wronskian_eq_of_sum_zero hsum

Premises used: Polynomial.wronskian_eq_of_sum_zero
-- Module: Mathlib.NumberTheory.FLT.MasonStothers
Goal:
k : Type u_1
inst : Field k
inst_1 : 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
⊢ w = c.wronskian a

Tactic:
have wca : w = wronskian c a := by
    rw [add_rotate] at hsum
    simpa only [← wbc] using wronskian_eq_of_sum_zero hsum
-- Module: Mathlib.NumberTheory.FLT.MasonStothers
Goal:
k : Type u_1
inst : Field k
inst_1 : 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
⊢ divRadical a ∣ a.wronskian b

Tactic:
have adr_dvd_w := divRadical_dvd_wronskian_left a b
-- Module: Mathlib.NumberTheory.FLT.MasonStothers
Goal:
k : Type u_1
inst : Field k
inst_1 : 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 ∣ a.wronskian b
⊢ divRadical b ∣ a.wronskian b

Tactic:
have bdr_dvd_w := divRadical_dvd_wronskian_right a b
-- Module: Mathlib.NumberTheory.FLT.MasonStothers
Goal:
k : Type u_1
inst : Field k
inst_1 : 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 ∣ a.wronskian b
bdr_dvd_w : divRadical b ∣ a.wronskian b
⊢ divRadical c ∣ b.wronskian c

Tactic:
have cdr_dvd_w := divRadical_dvd_wronskian_right b c
-- Module: Mathlib.NumberTheory.FLT.MasonStothers
Goal:
k : Type u_1
inst : Field k
inst_1 : 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 ∣ a.wronskian b
bdr_dvd_w : divRadical b ∣ a.wronskian b
cdr_dvd_w : divRadical c ∣ b.wronskian c
⊢ divRadical a ∣ w

Tactic:
rw [← wab] at adr_dvd_w bdr_dvd_w
-- Module: Mathlib.NumberTheory.FLT.MasonStothers
Goal:
k : Type u_1
inst : Field k
inst_1 : 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 ∣ a.wronskian b
bdr_dvd_w : divRadical b ∣ a.wronskian b
cdr_dvd_w : divRadical c ∣ b.wronskian c
adr_dvd_w₁ : divRadical a ∣ w
⊢ divRadical b ∣ w

Tactic:
rw [← wab] at adr_dvd_w bdr_dvd_w
-- Module: Mathlib.NumberTheory.FLT.MasonStothers
Goal:
k : Type u_1
inst : Field k
inst_1 : 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 ∣ a.wronskian b
bdr_dvd_w : divRadical b ∣ a.wronskian b
cdr_dvd_w : divRadical c ∣ b.wronskian c
adr_dvd_w₁ : divRadical a ∣ w
bdr_dvd_w₁ : divRadical b ∣ w
⊢ divRadical c ∣ b.wronskian c

Tactic:
rw [← wab] at adr_dvd_w bdr_dvd_w
-- Module: Mathlib.NumberTheory.FLT.MasonStothers
Goal:
k : Type u_1
inst : Field k
inst_1 : 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 c ∣ w

Tactic:
rw [← wbc] at cdr_dvd_w
-- Module: Mathlib.NumberTheory.FLT.MasonStothers
Goal:
k : Type u_1
inst : Field k
inst_1 : 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
rw : divRadical a * divRadical b * divRadical c ∣ w
⊢ divRadical (a * b * c) ∣ w

Tactic:
rw [divRadical_mul (hca.symm.mul_left hbc), divRadical_mul hab]

Premises used: IsCoprime.mul_left, EuclideanDomain.divRadical_mul, IsCoprime.symm
-- Module: Mathlib.NumberTheory.FLT.MasonStothers
Goal:
k : Type u_1
inst : Field k
inst_1 : 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:
(hca.divRadical.symm.mul_left hbc.divRadical).mul_dvd
      (hab.divRadical.mul_dvd adr_dvd_w bdr_dvd_w) cdr_dvd_w

Premises used: IsCoprime.mul_left, IsCoprime.mul_dvd, IsCoprime.symm, IsCoprime.divRadical
-- Module: Mathlib.NumberTheory.FLT.MasonStothers
Goal:
k : Type u_1
inst : Field k
inst_1 : 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

Premises used: IsCoprime.mul_left, IsCoprime.mul_dvd, IsCoprime.symm, IsCoprime.divRadical
-- Module: Mathlib.NumberTheory.FLT.MasonStothers
Goal:
k : Type u_1
inst : Field k
inst_1 : 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
⊢ divRadical (a * b * c) ∣ w

Tactic:
have abc_dr_dvd_w : divRadical (a * b * c) ∣ w := by
    have adr_dvd_w := divRadical_dvd_wronskian_left a b
    have bdr_dvd_w := divRadical_dvd_wronskian_right a b
    have cdr_dvd_w := divRadical_dvd_wronskian_right b c
    rw [← wab] at adr_dvd_w bdr_dvd_w
    rw [← wbc] at cdr_dvd_w
    rw [divRadical_mul (hca.symm.mul_left hbc), divRadical_mul hab]
    exact (hca.divRadical.symm.mul_left hbc.divRadical).mul_dvd
      (hab.divRadical.mul_dvd adr_dvd_w bdr_dvd_w) cdr_dvd_w
-- Module: Mathlib.NumberTheory.FLT.MasonStothers
Goal:
k : Type u_1
inst : Field k
inst_1 : 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
pos :
  ∀ (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 ∨
      Eq (α := k[X]) ((derivative : (a : k[X]) → k[X]) a : k[X]) (0 : k[X]) ∧
        Eq (α := k[X]) ((derivative : (a : k[X]) → k[X]) b : k[X]) (0 : k[X]) ∧
          Eq (α := k[X]) ((derivative : (a : k[X]) → k[X]) c : k[X]) (0 : k[X])
neg :
  ∀ (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 ∨
      Eq (α := k[X]) ((derivative : (a : k[X]) → k[X]) a : k[X]) (0 : k[X]) ∧
        Eq (α := k[X]) ((derivative : (a : k[X]) → k[X]) b : k[X]) (0 : k[X]) ∧
          Eq (α := k[X]) ((derivative : (a : k[X]) → k[X]) c : k[X]) (0 : k[X])
⊢ a.natDegree + 1 ≤ (radical (a * b * c)).natDegree ∧
      b.natDegree + 1 ≤ (radical (a * b * c)).natDegree ∧ c.natDegree + 1 ≤ (radical (a * b * c)).natDegree ∨
    Eq (α := k[X]) ((derivative : (a : k[X]) → k[X]) a : k[X]) (0 : k[X]) ∧
      Eq (α := k[X]) ((derivative : (a : k[X]) → k[X]) b : k[X]) (0 : k[X]) ∧
        Eq (α := k[X]) ((derivative : (a : k[X]) → k[X]) c : k[X]) (0 : k[X])

Tactic:
by_cases hw : w = 0
-- Module: Mathlib.NumberTheory.FLT.MasonStothers
Goal:
k : Type u_1
inst : Field k
inst_1 : 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
pos :
  Eq (α := k[X]) ((derivative : (a : k[X]) → k[X]) a : k[X]) (0 : k[X]) ∧
    Eq (α := k[X]) ((derivative : (a : k[X]) → k[X]) b : k[X]) (0 : k[X]) ∧
      Eq (α := k[X]) ((derivative : (a : k[X]) → k[X]) c : k[X]) (0 : k[X])
⊢ a.natDegree + 1 ≤ (radical (a * b * c)).natDegree ∧
      b.natDegree + 1 ≤ (radical (a * b * c)).natDegree ∧ c.natDegree + 1 ≤ (radical (a * b * c)).natDegree ∨
    Eq (α := k[X]) ((derivative : (a : k[X]) → k[X]) a : k[X]) (0 : k[X]) ∧
      Eq (α := k[X]) ((derivative : (a : k[X]) → k[X]) b : k[X]) (0 : k[X]) ∧
        Eq (α := k[X]) ((derivative : (a : k[X]) → k[X]) c : k[X]) (0 : k[X])

Tactic:
right