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 : 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
⊢ 0 = a.wronskian b

Tactic:
rw [hw] at wab wbc
-- 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
wab₁ : 0 = a.wronskian b
⊢ IsCoprime b c

Tactic:
rw [hw] at wab wbc
-- 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
wab₁ : 0 = a.wronskian b
hbc₁ : IsCoprime b c
⊢ b + c + a = 0

Tactic:
rw [hw] at wab wbc
-- 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
wab₁ : 0 = a.wronskian b
hbc₁ : IsCoprime b c
hsum'₁ : b + c + a = 0
⊢ IsCoprime c a

Tactic:
rw [hw] at wab wbc
-- 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
wab₁ : 0 = a.wronskian b
hbc₁ : IsCoprime b c
hsum'₁ : b + c + a = 0
hca₁ : IsCoprime c a
⊢ 0 = b.wronskian c

Tactic:
rw [hw] at wab wbc
-- 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
wab₁ : 0 = a.wronskian b
hbc₁ : IsCoprime b c
hsum'₁ : b + c + a = 0
hca₁ : IsCoprime c a
wbc₁ : 0 = b.wronskian c
⊢ w = c.wronskian a

Tactic:
rw [hw] at wab wbc
-- 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
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
⊢ divRadical (a * b * c) ∣ w

Tactic:
rw [hw] at wab wbc
-- 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
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
⊢ w = 0

Tactic:
rw [hw] at wab wbc
-- 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 : 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
⊢ Eq (α := k[X]) ((derivative : (a : k[X]) → k[X]) a : k[X]) (0 : k[X])

Tactic:
obtain ⟨ga, gb⟩ := hab.wronskian_eq_zero_iff.mp wab.symm

Premises used: IsCoprime.wronskian_eq_zero_iff, Iff.mp, Eq.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 : 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 : 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])

Tactic:
obtain ⟨ga, gb⟩ := hab.wronskian_eq_zero_iff.mp wab.symm

Premises used: IsCoprime.wronskian_eq_zero_iff, Iff.mp, Eq.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 : 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 : Eq (α := k[X]) ((derivative : (a : k[X]) → k[X]) a : k[X]) (0 : k[X])
gb : Eq (α := k[X]) ((derivative : (a : k[X]) → k[X]) b : k[X]) (0 : k[X])
⊢ Eq (α := k[X]) ((derivative : (a : k[X]) → k[X]) b : k[X]) (0 : k[X])

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

Premises used: IsCoprime.wronskian_eq_zero_iff, Iff.mp, Eq.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 : 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 : Eq (α := k[X]) ((derivative : (a : k[X]) → k[X]) a : k[X]) (0 : k[X])
gb left : 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:
obtain ⟨_, gc⟩ := hbc.wronskian_eq_zero_iff.mp wbc.symm

Premises used: IsCoprime.wronskian_eq_zero_iff, Iff.mp, Eq.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 : 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 : Eq (α := k[X]) ((derivative : (a : k[X]) → k[X]) a : k[X]) (0 : k[X])
gb left : Eq (α := k[X]) ((derivative : (a : k[X]) → k[X]) b : k[X]) (0 : k[X])
gc : Eq (α := k[X]) ((derivative : (a : k[X]) → k[X]) c : k[X]) (0 : k[X])
⊢ 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:
⟨ga, gb, gc⟩

Premises used: And.intro
-- 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 : 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 : Eq (α := k[X]) ((derivative : (a : k[X]) → k[X]) a : k[X]) (0 : k[X])
gb left : Eq (α := k[X]) ((derivative : (a : k[X]) → k[X]) b : k[X]) (0 : k[X])
gc : Eq (α := k[X]) ((derivative : (a : k[X]) → k[X]) c : k[X]) (0 : k[X])
⊢ 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:
exact ⟨ga, gb, gc⟩
-- 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
neg :
  a.natDegree + 1 ≤ (radical (a * b * c)).natDegree ∧
    b.natDegree + 1 ≤ (radical (a * b * c)).natDegree ∧ c.natDegree + 1 ≤ (radical (a * b * c)).natDegree
⊢ 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:
left
-- 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
⊢ a.natDegree + 1 ≤ (radical (a * b * c)).natDegree ∧
    b.natDegree + 1 ≤ (radical (a * b * c)).natDegree ∧ c.natDegree + 1 ≤ (radical (a * b * c)).natDegree

Tactic:
⟨?_, ?_, ?_⟩

Premises used: And.intro
-- 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
neg : a.natDegree + 1 ≤ (radical (a * b * c)).natDegree
neg₁ : b.natDegree + 1 ≤ (radical (a * b * c)).natDegree
neg₂ : c.natDegree + 1 ≤ (radical (a * b * c)).natDegree
⊢ a.natDegree + 1 ≤ (radical (a * b * c)).natDegree ∧
    b.natDegree + 1 ≤ (radical (a * b * c)).natDegree ∧ c.natDegree + 1 ≤ (radical (a * b * c)).natDegree

Tactic:
refine ⟨?_, ?_, ?_⟩
-- 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
neg : ∀ (abc_dr_dvd_w : divRadical (b * c * a) ∣ w) (hw : ¬w = 0), a.natDegree + 1 ≤ (radical (b * c * a)).natDegree
⊢ a.natDegree + 1 ≤ (radical (a * b * c)).natDegree

Tactic:
rw [mul_rotate] at abc_dr_dvd_w ⊢

Premises used: mul_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
hsum' : b + c + a = 0
hca : IsCoprime c a
wbc : w = b.wronskian c
wca : w = c.wronskian a
abc_dr_dvd_w : divRadical (b * c * a) ∣ w
hw : ¬w = 0
neg : b ≠ 0
neg₁ : c ≠ 0
neg₂ : a ≠ 0
neg₃ : divRadical (b * c * a) ∣ w
apply : w ≠ 0
⊢ a.natDegree + 1 ≤ (radical (b * c * a)).natDegree

Tactic:
apply abc_subcall wbc

Premises used: _private.0.abc_subcall
-- 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 (b * c * a) ∣ w
hw : ¬w = 0
⊢ b ≠ 0

Tactic:
assumption
-- 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 (b * c * a) ∣ w
hw : ¬w = 0
⊢ c ≠ 0

Tactic:
assumption
-- 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 (b * c * a) ∣ w
hw : ¬w = 0
⊢ a ≠ 0

Tactic:
assumption
-- 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 (b * c * a) ∣ w
hw : ¬w = 0
⊢ divRadical (b * c * a) ∣ w

Tactic:
assumption
-- 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 (b * c * a) ∣ w
hw : ¬w = 0
⊢ w ≠ 0

Tactic:
assumption
-- 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
neg : ∀ (abc_dr_dvd_w : divRadical (c * a * b) ∣ w) (hw : ¬w = 0), b.natDegree + 1 ≤ (radical (c * a * b)).natDegree
⊢ b.natDegree + 1 ≤ (radical (a * b * c)).natDegree

Tactic:
rw [← mul_rotate] at abc_dr_dvd_w ⊢

Premises used: mul_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
hsum' : b + c + a = 0
hca : IsCoprime c a
wbc : w = b.wronskian c
wca : w = c.wronskian a
abc_dr_dvd_w : divRadical (c * a * b) ∣ w
hw : ¬w = 0
neg : c ≠ 0
neg₁ : a ≠ 0
neg₂ : b ≠ 0
neg₃ : divRadical (c * a * b) ∣ w
apply : w ≠ 0
⊢ b.natDegree + 1 ≤ (radical (c * a * b)).natDegree

Tactic:
apply abc_subcall wca

Premises used: _private.0.abc_subcall
-- 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 (c * a * b) ∣ w
hw : ¬w = 0
⊢ c ≠ 0

Tactic:
assumption
-- 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 (c * a * b) ∣ w
hw : ¬w = 0
⊢ a ≠ 0

Tactic:
assumption
-- 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 (c * a * b) ∣ w
hw : ¬w = 0
⊢ b ≠ 0

Tactic:
assumption
-- 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 (c * a * b) ∣ w
hw : ¬w = 0
⊢ divRadical (c * a * b) ∣ w

Tactic:
assumption
-- 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 (c * a * b) ∣ w
hw : ¬w = 0
⊢ w ≠ 0

Tactic:
assumption
-- 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
neg : a ≠ 0
neg₁ : b ≠ 0
neg₂ : c ≠ 0
neg₃ : divRadical (a * b * c) ∣ w
apply : w ≠ 0
⊢ c.natDegree + 1 ≤ (radical (a * b * c)).natDegree

Tactic:
apply abc_subcall wab

Premises used: _private.0.abc_subcall
-- 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
⊢ a ≠ 0

Tactic:
assumption
-- 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
⊢ b ≠ 0

Tactic:
assumption
-- 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
⊢ c ≠ 0

Tactic:
assumption
-- 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
⊢ divRadical (a * b * c) ∣ w

Tactic:
assumption
-- 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
⊢ w ≠ 0

Tactic:
assumption
-- Module: Mathlib.NumberTheory.FLT.Polynomial
Goal:
k : Type u_1
inst : Field k
u : k
hu : u ≠ 0
⊢ IsUnit (M := k[X]) ((C : (a : k) → k[X]) u : k[X])

Tactic:
Polynomial.isUnit_C.mpr hu.isUnit

Premises used: Iff.mpr, Ne.isUnit, Polynomial.isUnit_C
-- Module: Mathlib.NumberTheory.FLT.Polynomial
Goal:
k : Type u_1
inst : Field k
p q r : ℕ
a b c : k[X]
u v w : k
hp : p ≠ 0
hq : q ≠ 0
hr : r ≠ 0
hu : u ≠ 0
hv : v ≠ 0
hw : w ≠ 0
heq :
  HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) u : k[X]) (a ^ p) +
        HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) v : k[X]) (b ^ q) +
      HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) w : k[X]) (c ^ r) =
    0
hab : IsCoprime a b
⊢ IsUnit (M := k[X]) ((C : (a : k) → k[X]) u : k[X])

Tactic:
have hCu : IsUnit (C u) := hu.isUnit_C
-- Module: Mathlib.NumberTheory.FLT.Polynomial
Goal:
k : Type u_1
inst : Field k
p q r : ℕ
a b c : k[X]
u v w : k
hp : p ≠ 0
hq : q ≠ 0
hr : r ≠ 0
hu : u ≠ 0
hv : v ≠ 0
hw : w ≠ 0
heq :
  HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) u : k[X]) (a ^ p) +
        HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) v : k[X]) (b ^ q) +
      HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) w : k[X]) (c ^ r) =
    0
hab : IsCoprime a b
hCu : IsUnit (M := k[X]) ((C : (a : k) → k[X]) u : k[X])
⊢ IsUnit (M := k[X]) ((C : (a : k) → k[X]) v : k[X])

Tactic:
have hCv : IsUnit (C v) := hv.isUnit_C
-- Module: Mathlib.NumberTheory.FLT.Polynomial
Goal:
k : Type u_1
inst : Field k
p q r : ℕ
a b c : k[X]
u v w : k
hp : p ≠ 0
hq : q ≠ 0
hr : r ≠ 0
hu : u ≠ 0
hv : v ≠ 0
hw : w ≠ 0
heq :
  HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) u : k[X]) (a ^ p) +
        HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) v : k[X]) (b ^ q) +
      HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) w : k[X]) (c ^ r) =
    0
hab : IsCoprime a b
hCu : IsUnit (M := k[X]) ((C : (a : k) → k[X]) u : k[X])
hCv : IsUnit (M := k[X]) ((C : (a : k) → k[X]) v : k[X])
⊢ IsUnit (M := k[X]) ((C : (a : k) → k[X]) w : k[X])

Tactic:
have hCw : IsUnit (C w) := hw.isUnit_C
-- Module: Mathlib.NumberTheory.FLT.Polynomial
Goal:
k : Type u_1
inst : Field k
p q r : ℕ
a b c : k[X]
u v w : k
hp : p ≠ 0
hq : q ≠ 0
hr : r ≠ 0
hu : u ≠ 0
hv : v ≠ 0
hw : w ≠ 0
heq :
  HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) u : k[X]) (a ^ p) +
        HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) v : k[X]) (b ^ q) +
      HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) w : k[X]) (c ^ r) =
    0
hab : IsCoprime a b
hCu : IsUnit (M := k[X]) ((C : (a : k) → k[X]) u : k[X])
hCv : IsUnit (M := k[X]) ((C : (a : k) → k[X]) v : k[X])
hCw : IsUnit (M := k[X]) ((C : (a : k) → k[X]) w : k[X])
⊢ IsCoprime (HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) u : k[X]) (a ^ p))
    (HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) v : k[X]) (b ^ q))

Tactic:
rw [← IsCoprime.pow_iff hp.bot_lt hq.bot_lt, ← isCoprime_mul_units_left hCu hCv] at hab

Premises used: isCoprime_mul_units_left, IsCoprime.pow_iff, Ne.bot_lt