awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.MasonStothers (goal)
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
⊢ c.natDegree + 1 ≤ abc_r.natDegree
have n : ℕ
Tactic: apply Nat.lt_of_add_lt_add_left
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.MasonStothers (goal)
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 * b * c).natDegree
have rw : a.natDegree + b.natDegree + c.natDegree = (a * b).natDegree + c.natDegree
Tactic: rw [Polynomial.natDegree_mul ab_nz hc, Polynomial.natDegree_mul ha hb]
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.MasonStothers (goal)
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
⊢ a.natDegree + b.natDegree + c.natDegree = (a * b * c).natDegree
have rw₁ : a.natDegree + b.natDegree + c.natDegree = a.natDegree + b.natDegree + c.natDegree
Tactic: rw [Polynomial.natDegree_mul ab_nz hc, Polynomial.natDegree_mul ha hb]
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.MasonStothers (goal)
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 * b * c).natDegree = (divRadical (a * b * c) * radical (a * b * c)).natDegree
have rw : (a * b * c).natDegree = (radical (a * b * c) * divRadical (a * b * c)).natDegree
Tactic: rw [mul_comm _ (radical _), radical_mul_divRadical]
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.MasonStothers (goal)
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
⊢ (a * b * c).natDegree = (divRadical (a * b * c) * radical (a * b * c)).natDegree
have rw₁ : (a * b * c).natDegree = (a * b * c).natDegree
Tactic: rw [mul_comm _ (radical _), radical_mul_divRadical]
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.MasonStothers (goal)
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)
⊢ (divRadical (a * b * c) * radical (a * b * c)).natDegree = abc_dr.natDegree + abc_r.natDegree
have rw : (divRadical (a * b * c) * radical (a * b * c)).natDegree = (divRadical (a * b * c) * radical (a * b * c)).natDegree
Tactic: rw [← Polynomial.natDegree_mul (divRadical_ne_zero abc_nz) radical_ne_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.MasonStothers (goal)
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)
⊢ ℕ
have b₁ : a.natDegree + b.natDegree + c.natDegree = (a * b * c).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 _
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.MasonStothers (goal)
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
⊢ ℕ
have b₂ : (a * b * c).natDegree = (divRadical (a * b * c) * radical (a * b * c)).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 _
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.MasonStothers (goal)
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
⊢ ℕ
have b₃ : (divRadical (a * b * c) * radical (a * b * c)).natDegree = abc_dr.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 _
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.MasonStothers (goal)
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
⊢ ℕ
have 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 _
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.MasonStothers (hypothesis)
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
⊢ 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])
have wab : let w := a.wronskian b;
w = a.wronskian b
Tactic: set w := wronskian a b with wab
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.MasonStothers (hypothesis)
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
have hsum₁ : -(a + b) = c
Tactic: rw [add_eq_zero_iff_neg_eq] at hsum
Cleared hypotheses: hsum, w, wab
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.MasonStothers (goal)
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 c
have rw : IsCoprime b (a + b)
Tactic: rw [← hsum, IsCoprime.neg_right_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.MasonStothers (goal)
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)
have h : b = b * 1
Tactic: convert! IsCoprime.add_mul_left_right hab.symm 1
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.MasonStothers (goal)
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
⊢ b = b * 1
have h : b = b
Tactic: rw [mul_one]
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.MasonStothers (hypothesis)
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.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])
have hbc : 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]
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.MasonStothers (goal)
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
have rwa : ∀ (hsum : b + c + a = 0),
  let w := a.wronskian b;
  ∀ (wab : w = a.wronskian b) (hbc : IsCoprime b c), b + c + a = 0
Tactic: rwa [add_rotate] at hsum
Cleared hypotheses: hsum, w, wab, hbc
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.MasonStothers (hypothesis)
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
⊢ 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])
have hsum' : b + c + a = 0
Tactic: have hsum' : b + c + a = 0 := by rwa [add_rotate] at hsum
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.MasonStothers (hypothesis)
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
have hsum'₁ : -(b + c) = a
Tactic: rw [add_eq_zero_iff_neg_eq] at hsum'
Cleared hypotheses: hsum'
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.MasonStothers (goal)
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 a
have rw : IsCoprime c (b + c)
Tactic: rw [← hsum', IsCoprime.neg_right_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.MasonStothers (goal)
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)
have h : c = c * 1
Tactic: convert! IsCoprime.add_mul_left_right hbc.symm 1
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.MasonStothers (goal)
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
⊢ c = c * 1
have h : c = c
Tactic: rw [mul_one]
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.MasonStothers (hypothesis)
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
⊢ 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])
have hca : 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]
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.MasonStothers (hypothesis)
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
⊢ 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])
have wbc : w = b.wronskian c
Tactic: have wbc : w = wronskian b c := wronskian_eq_of_sum_zero hsum
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.MasonStothers (goal)
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
have 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
Tactic: rw [add_rotate] at hsum
Cleared hypotheses: hsum, w, wab, hbc, hsum', hca, wbc
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.MasonStothers (hypothesis)
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
⊢ 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])
have wca : 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
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.MasonStothers (hypothesis)
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
have adr_dvd_w : divRadical a ∣ a.wronskian b
Tactic: have adr_dvd_w := divRadical_dvd_wronskian_left a b
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.MasonStothers (hypothesis)
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 (a * b * c) ∣ w
have bdr_dvd_w : divRadical b ∣ a.wronskian b
Tactic: have bdr_dvd_w := divRadical_dvd_wronskian_right a b
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.MasonStothers (hypothesis)
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 (a * b * c) ∣ w
have cdr_dvd_w : divRadical c ∣ b.wronskian c
Tactic: have cdr_dvd_w := divRadical_dvd_wronskian_right b c
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.MasonStothers (hypothesis)
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 (a * b * c) ∣ w
have cdr_dvd_w₁ : divRadical c ∣ w
Tactic: rw [← wbc] at cdr_dvd_w
Cleared hypotheses: cdr_dvd_w
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.MasonStothers (goal)
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 * b * c) ∣ w
have rw : divRadical a * divRadical b * divRadical c ∣ w
Tactic: rw [divRadical_mul (hca.symm.mul_left hbc), divRadical_mul hab]
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.MasonStothers (hypothesis)
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
⊢ 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])
have abc_dr_dvd_w : 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
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.MasonStothers (goal)
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
⊢ 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])
have 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])
Tactic: by_cases hw : w = 0