awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.FLT.Polynomial
Goal:
k : Type u_1
inst : Field k
p q r : ℕ
u v w : k
hp : p ≠ 0
hq : q ≠ 0
hr : r ≠ 0
hineq : q * r + r * p + p * q ≤ p * q * r
chp : Ne.{u_1 + 1} (α := k) (↑p : k) 0
chq : Ne.{u_1 + 1} (α := k) (↑q : k) 0
chr : Ne.{u_1 + 1} (α := k) (↑r : k) 0
hu : u ≠ 0
hv : v ≠ 0
hw : w ≠ 0
d : ℕ
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
eq_d : a.natDegree = d + 1
ad : Eq (α := k[X]) ((derivative : (a : k[X]) → k[X]) a : k[X]) (0 : k[X])
bd : Eq (α := k[X]) ((derivative : (a : k[X]) → k[X]) b : k[X]) (0 : k[X])
cd : Eq (α := k[X]) ((derivative : (a : k[X]) → k[X]) c : k[X]) (0 : k[X])
ca : k[X]
ca_nz : ca ≠ 0
cb : k[X]
cb_nz : cb ≠ 0
cc : k[X]
cc_nz : cc ≠ 0
ch : ℕ := ringChar k
chn0 : ch ≠ 0
eq_a : a = (expand k ch : (a : k[X]) → k[X]) ca
eq_deg_a : a.natDegree = ca.natDegree * ch
eq_b : b = (expand k ch : (a : k[X]) → k[X]) cb
eq_deg_b : b.natDegree = cb.natDegree * ch
eq_c : c = (expand k ch : (a : k[X]) → k[X]) cc
eq_deg_c : c.natDegree = cc.natDegree * ch
hnca : ¬ca.natDegree = 0
heq :
  Eq (α := k[X])
    ((expand k ch : (a : k[X]) → k[X])
        (HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) u : k[X]) (ca ^ p) +
            HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) v : k[X]) (cb ^ q) +
          HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) w : k[X]) (cc ^ r)) :
      k[X])
    (0 : k[X])
rwa rwa₁ rwa₂ rwa₃ :
  ∀
    (heq :
      HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) u : k[X]) (ca ^ p) +
            HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) v : k[X]) (cb ^ q) +
          HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) w : k[X]) (cc ^ r) =
        0),
    HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) u : k[X]) (ca ^ p) +
          HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) v : k[X]) (cb ^ q) +
        HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) w : k[X]) (cc ^ r) =
      0
⊢ HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) u : k[X]) (ca ^ p) +
        HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) v : k[X]) (cb ^ q) +
      HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) w : k[X]) (cc ^ r) =
    0

Tactic:
rwa [Polynomial.expand_eq_zero (zero_lt_iff.mpr chn0)] at heq

Premises used: Iff.mpr, Polynomial.expand_eq_zero, zero_lt_iff
-- Module: Mathlib.NumberTheory.FLT.Polynomial
Goal:
k : Type u_1
inst : Field k
p q r : ℕ
hp : p ≠ 0
hq : q ≠ 0
hr : r ≠ 0
hineq : q * r + r * p + p * q ≤ p * q * r
chp : Ne.{u_1 + 1} (α := k) (↑p : k) 0
chq : Ne.{u_1 + 1} (α := k) (↑q : k) 0
chr : Ne.{u_1 + 1} (α := k) (↑r : k) 0
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
u v w : k
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
apply : p ≠ 0
apply₁ : q ≠ 0
apply₂ : r ≠ 0
apply₃ : u ≠ 0
apply₄ : v ≠ 0
apply₅ : w ≠ 0
⊢ IsCoprime b c

Tactic:
apply rot_coprime heq hab

Premises used: _private.0.rot_coprime
-- Module: Mathlib.NumberTheory.FLT.Polynomial
Goal:
k : Type u_1
inst : Field k
p q r : ℕ
hp : p ≠ 0
hq : q ≠ 0
hr : r ≠ 0
hineq : q * r + r * p + p * q ≤ p * q * r
chp : Ne.{u_1 + 1} (α := k) (↑p : k) 0
chq : Ne.{u_1 + 1} (α := k) (↑q : k) 0
chr : Ne.{u_1 + 1} (α := k) (↑r : k) 0
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
u v w : k
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
⊢ IsCoprime b c

Tactic:
have hbc : IsCoprime b c := by
    apply rot_coprime heq hab <;> assumption
-- Module: Mathlib.NumberTheory.FLT.Polynomial
Goal:
k : Type u_1
inst : Field k
p q r : ℕ
hp : p ≠ 0
hq : q ≠ 0
hr : r ≠ 0
hineq : q * r + r * p + p * q ≤ p * q * r
chp : Ne.{u_1 + 1} (α := k) (↑p : k) 0
chq : Ne.{u_1 + 1} (α := k) (↑q : k) 0
chr : Ne.{u_1 + 1} (α := k) (↑r : k) 0
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
u v w : k
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
hbc : IsCoprime b c
rwa rwa₁ rwa₂ rwa₃ :
  ∀
    (heq :
      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) +
          HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) u : k[X]) (a ^ p) =
        0)
    (hbc : IsCoprime b c),
    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) +
        HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) u : k[X]) (a ^ p) =
      0
⊢ 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) +
      HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) u : k[X]) (a ^ p) =
    0

Tactic:
rwa [add_rotate] at heq

Premises used: add_rotate
-- Module: Mathlib.NumberTheory.FLT.Polynomial
Goal:
k : Type u_1
inst : Field k
p q r : ℕ
hp : p ≠ 0
hq : q ≠ 0
hr : r ≠ 0
hineq : q * r + r * p + p * q ≤ p * q * r
chp : Ne.{u_1 + 1} (α := k) (↑p : k) 0
chq : Ne.{u_1 + 1} (α := k) (↑q : k) 0
chr : Ne.{u_1 + 1} (α := k) (↑r : k) 0
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
u v w : k
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
hbc : IsCoprime b c
⊢ 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) +
      HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) u : k[X]) (a ^ p) =
    0

Tactic:
have heq' : C v * b ^ q + C w * c ^ r + C u * a ^ p = 0 := by
    rwa [add_rotate] at heq
-- Module: Mathlib.NumberTheory.FLT.Polynomial
Goal:
k : Type u_1
inst : Field k
p q r : ℕ
hp : p ≠ 0
hq : q ≠ 0
hr : r ≠ 0
hineq : q * r + r * p + p * q ≤ p * q * r
chp : Ne.{u_1 + 1} (α := k) (↑p : k) 0
chq : Ne.{u_1 + 1} (α := k) (↑q : k) 0
chr : Ne.{u_1 + 1} (α := k) (↑r : k) 0
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
u v w : k
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
hbc : IsCoprime b c
heq' :
  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) +
      HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) u : k[X]) (a ^ p) =
    0
apply : q ≠ 0
apply₁ : r ≠ 0
apply₂ : p ≠ 0
apply₃ : v ≠ 0
apply₄ : w ≠ 0
apply₅ : u ≠ 0
⊢ IsCoprime c a

Tactic:
apply rot_coprime heq' hbc

Premises used: _private.0.rot_coprime
-- Module: Mathlib.NumberTheory.FLT.Polynomial
Goal:
k : Type u_1
inst : Field k
p q r : ℕ
hp : p ≠ 0
hq : q ≠ 0
hr : r ≠ 0
hineq : q * r + r * p + p * q ≤ p * q * r
chp : Ne.{u_1 + 1} (α := k) (↑p : k) 0
chq : Ne.{u_1 + 1} (α := k) (↑q : k) 0
chr : Ne.{u_1 + 1} (α := k) (↑r : k) 0
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
u v w : k
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
hbc : IsCoprime b c
heq' :
  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) +
      HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) u : k[X]) (a ^ p) =
    0
⊢ q ≠ 0

Tactic:
assumption
-- Module: Mathlib.NumberTheory.FLT.Polynomial
Goal:
k : Type u_1
inst : Field k
p q r : ℕ
hp : p ≠ 0
hq : q ≠ 0
hr : r ≠ 0
hineq : q * r + r * p + p * q ≤ p * q * r
chp : Ne.{u_1 + 1} (α := k) (↑p : k) 0
chq : Ne.{u_1 + 1} (α := k) (↑q : k) 0
chr : Ne.{u_1 + 1} (α := k) (↑r : k) 0
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
u v w : k
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
hbc : IsCoprime b c
heq' :
  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) +
      HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) u : k[X]) (a ^ p) =
    0
⊢ r ≠ 0

Tactic:
assumption
-- Module: Mathlib.NumberTheory.FLT.Polynomial
Goal:
k : Type u_1
inst : Field k
p q r : ℕ
hp : p ≠ 0
hq : q ≠ 0
hr : r ≠ 0
hineq : q * r + r * p + p * q ≤ p * q * r
chp : Ne.{u_1 + 1} (α := k) (↑p : k) 0
chq : Ne.{u_1 + 1} (α := k) (↑q : k) 0
chr : Ne.{u_1 + 1} (α := k) (↑r : k) 0
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
u v w : k
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
hbc : IsCoprime b c
heq' :
  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) +
      HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) u : k[X]) (a ^ p) =
    0
⊢ p ≠ 0

Tactic:
assumption
-- Module: Mathlib.NumberTheory.FLT.Polynomial
Goal:
k : Type u_1
inst : Field k
p q r : ℕ
hp : p ≠ 0
hq : q ≠ 0
hr : r ≠ 0
hineq : q * r + r * p + p * q ≤ p * q * r
chp : Ne.{u_1 + 1} (α := k) (↑p : k) 0
chq : Ne.{u_1 + 1} (α := k) (↑q : k) 0
chr : Ne.{u_1 + 1} (α := k) (↑r : k) 0
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
u v w : k
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
hbc : IsCoprime b c
heq' :
  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) +
      HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) u : k[X]) (a ^ p) =
    0
⊢ v ≠ 0

Tactic:
assumption
-- Module: Mathlib.NumberTheory.FLT.Polynomial
Goal:
k : Type u_1
inst : Field k
p q r : ℕ
hp : p ≠ 0
hq : q ≠ 0
hr : r ≠ 0
hineq : q * r + r * p + p * q ≤ p * q * r
chp : Ne.{u_1 + 1} (α := k) (↑p : k) 0
chq : Ne.{u_1 + 1} (α := k) (↑q : k) 0
chr : Ne.{u_1 + 1} (α := k) (↑r : k) 0
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
u v w : k
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
hbc : IsCoprime b c
heq' :
  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) +
      HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) u : k[X]) (a ^ p) =
    0
⊢ w ≠ 0

Tactic:
assumption
-- Module: Mathlib.NumberTheory.FLT.Polynomial
Goal:
k : Type u_1
inst : Field k
p q r : ℕ
hp : p ≠ 0
hq : q ≠ 0
hr : r ≠ 0
hineq : q * r + r * p + p * q ≤ p * q * r
chp : Ne.{u_1 + 1} (α := k) (↑p : k) 0
chq : Ne.{u_1 + 1} (α := k) (↑q : k) 0
chr : Ne.{u_1 + 1} (α := k) (↑r : k) 0
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
u v w : k
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
hbc : IsCoprime b c
heq' :
  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) +
      HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) u : k[X]) (a ^ p) =
    0
⊢ u ≠ 0

Tactic:
assumption
-- Module: Mathlib.NumberTheory.FLT.Polynomial
Goal:
k : Type u_1
inst : Field k
p q r : ℕ
hp : p ≠ 0
hq : q ≠ 0
hr : r ≠ 0
hineq : q * r + r * p + p * q ≤ p * q * r
chp : Ne.{u_1 + 1} (α := k) (↑p : k) 0
chq : Ne.{u_1 + 1} (α := k) (↑q : k) 0
chr : Ne.{u_1 + 1} (α := k) (↑r : k) 0
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
u v w : k
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
hbc : IsCoprime b c
heq' :
  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) +
      HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) u : k[X]) (a ^ p) =
    0
⊢ IsCoprime c a

Tactic:
have hca : IsCoprime c a := by
    apply rot_coprime heq' hbc <;> assumption
-- Module: Mathlib.NumberTheory.FLT.Polynomial
Goal:
k : Type u_1
inst : Field k
p q r : ℕ
hp : p ≠ 0
hq : q ≠ 0
hr : r ≠ 0
hineq : q * r + r * p + p * q ≤ p * q * r
chp : Ne.{u_1 + 1} (α := k) (↑p : k) 0
chq : Ne.{u_1 + 1} (α := k) (↑q : k) 0
chr : Ne.{u_1 + 1} (α := k) (↑r : k) 0
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
u v w : k
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
hbc : IsCoprime b c
heq' :
  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) +
      HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) u : k[X]) (a ^ p) =
    0
hca : IsCoprime c a
⊢ a.natDegree = 0 ∧ b.natDegree = 0 ∧ c.natDegree = 0

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

Premises used: And.intro
-- Module: Mathlib.NumberTheory.FLT.Polynomial
Goal:
k : Type u_1
inst : Field k
p q r : ℕ
hp : p ≠ 0
hq : q ≠ 0
hr : r ≠ 0
hineq : q * r + r * p + p * q ≤ p * q * r
chp : Ne.{u_1 + 1} (α := k) (↑p : k) 0
chq : Ne.{u_1 + 1} (α := k) (↑q : k) 0
chr : Ne.{u_1 + 1} (α := k) (↑r : k) 0
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
u v w : k
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
hbc : IsCoprime b c
heq' :
  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) +
      HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) u : k[X]) (a ^ p) =
    0
hca : IsCoprime c a
refine_1 : a.natDegree = 0
refine_2 : b.natDegree = 0
refine_3 : c.natDegree = 0
⊢ a.natDegree = 0 ∧ b.natDegree = 0 ∧ c.natDegree = 0

Tactic:
refine ⟨?_, ?_, ?_⟩
-- Module: Mathlib.NumberTheory.FLT.Polynomial
Goal:
k : Type u_1
inst : Field k
p q r : ℕ
hp : p ≠ 0
hq : q ≠ 0
hr : r ≠ 0
hineq : q * r + r * p + p * q ≤ p * q * r
chp : Ne.{u_1 + 1} (α := k) (↑p : k) 0
chq : Ne.{u_1 + 1} (α := k) (↑q : k) 0
chr : Ne.{u_1 + 1} (α := k) (↑r : k) 0
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
u v w : k
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
hbc : IsCoprime b c
heq' :
  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) +
      HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) u : k[X]) (a ^ p) =
    0
hca : IsCoprime c a
refine_1 : p ≠ 0
refine_1₁ : q ≠ 0
refine_1₂ : r ≠ 0
refine_1₃ : q * r + r * p + p * q ≤ p * q * r
refine_1₄ : Ne.{u_1 + 1} (α := k) (↑p : k) 0
refine_1₅ : Ne.{u_1 + 1} (α := k) (↑q : k) 0
refine_1₆ : Ne.{u_1 + 1} (α := k) (↑r : k) 0
refine_1₇ : a ≠ 0
refine_1₈ : b ≠ 0
refine_1₉ : c ≠ 0
refine_1₁₀ : IsCoprime a b
refine_1₁₁ : u ≠ 0
refine_1₁₂ : v ≠ 0
refine_1₁₃ : w ≠ 0
⊢ a.natDegree = 0

Tactic:
apply flt_catalan_aux heq

Premises used: _private.0.Polynomial.flt_catalan_aux
-- Module: Mathlib.NumberTheory.FLT.Polynomial
Goal:
k : Type u_1
inst : Field k
p q r : ℕ
hp : p ≠ 0
hq : q ≠ 0
hr : r ≠ 0
hineq : q * r + r * p + p * q ≤ p * q * r
chp : Ne.{u_1 + 1} (α := k) (↑p : k) 0
chq : Ne.{u_1 + 1} (α := k) (↑q : k) 0
chr : Ne.{u_1 + 1} (α := k) (↑r : k) 0
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
u v w : k
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
hbc : IsCoprime b c
heq' :
  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) +
      HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) u : k[X]) (a ^ p) =
    0
hca : IsCoprime c a
⊢ p ≠ 0

Tactic:
assumption
-- Module: Mathlib.NumberTheory.FLT.Polynomial
Goal:
k : Type u_1
inst : Field k
p q r : ℕ
hp : p ≠ 0
hq : q ≠ 0
hr : r ≠ 0
hineq : q * r + r * p + p * q ≤ p * q * r
chp : Ne.{u_1 + 1} (α := k) (↑p : k) 0
chq : Ne.{u_1 + 1} (α := k) (↑q : k) 0
chr : Ne.{u_1 + 1} (α := k) (↑r : k) 0
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
u v w : k
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
hbc : IsCoprime b c
heq' :
  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) +
      HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) u : k[X]) (a ^ p) =
    0
hca : IsCoprime c a
⊢ q ≠ 0

Tactic:
assumption
-- Module: Mathlib.NumberTheory.FLT.Polynomial
Goal:
k : Type u_1
inst : Field k
p q r : ℕ
hp : p ≠ 0
hq : q ≠ 0
hr : r ≠ 0
hineq : q * r + r * p + p * q ≤ p * q * r
chp : Ne.{u_1 + 1} (α := k) (↑p : k) 0
chq : Ne.{u_1 + 1} (α := k) (↑q : k) 0
chr : Ne.{u_1 + 1} (α := k) (↑r : k) 0
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
u v w : k
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
hbc : IsCoprime b c
heq' :
  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) +
      HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) u : k[X]) (a ^ p) =
    0
hca : IsCoprime c a
⊢ r ≠ 0

Tactic:
assumption
-- Module: Mathlib.NumberTheory.FLT.Polynomial
Goal:
k : Type u_1
inst : Field k
p q r : ℕ
hp : p ≠ 0
hq : q ≠ 0
hr : r ≠ 0
hineq : q * r + r * p + p * q ≤ p * q * r
chp : Ne.{u_1 + 1} (α := k) (↑p : k) 0
chq : Ne.{u_1 + 1} (α := k) (↑q : k) 0
chr : Ne.{u_1 + 1} (α := k) (↑r : k) 0
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
u v w : k
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
hbc : IsCoprime b c
heq' :
  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) +
      HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) u : k[X]) (a ^ p) =
    0
hca : IsCoprime c a
⊢ q * r + r * p + p * q ≤ p * q * r

Tactic:
assumption
-- Module: Mathlib.NumberTheory.FLT.Polynomial
Goal:
k : Type u_1
inst : Field k
p q r : ℕ
hp : p ≠ 0
hq : q ≠ 0
hr : r ≠ 0
hineq : q * r + r * p + p * q ≤ p * q * r
chp : Ne.{u_1 + 1} (α := k) (↑p : k) 0
chq : Ne.{u_1 + 1} (α := k) (↑q : k) 0
chr : Ne.{u_1 + 1} (α := k) (↑r : k) 0
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
u v w : k
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
hbc : IsCoprime b c
heq' :
  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) +
      HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) u : k[X]) (a ^ p) =
    0
hca : IsCoprime c a
⊢ Ne.{u_1 + 1} (α := k) (↑p : k) 0

Tactic:
assumption
-- Module: Mathlib.NumberTheory.FLT.Polynomial
Goal:
k : Type u_1
inst : Field k
p q r : ℕ
hp : p ≠ 0
hq : q ≠ 0
hr : r ≠ 0
hineq : q * r + r * p + p * q ≤ p * q * r
chp : Ne.{u_1 + 1} (α := k) (↑p : k) 0
chq : Ne.{u_1 + 1} (α := k) (↑q : k) 0
chr : Ne.{u_1 + 1} (α := k) (↑r : k) 0
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
u v w : k
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
hbc : IsCoprime b c
heq' :
  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) +
      HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) u : k[X]) (a ^ p) =
    0
hca : IsCoprime c a
⊢ Ne.{u_1 + 1} (α := k) (↑q : k) 0

Tactic:
assumption
-- Module: Mathlib.NumberTheory.FLT.Polynomial
Goal:
k : Type u_1
inst : Field k
p q r : ℕ
hp : p ≠ 0
hq : q ≠ 0
hr : r ≠ 0
hineq : q * r + r * p + p * q ≤ p * q * r
chp : Ne.{u_1 + 1} (α := k) (↑p : k) 0
chq : Ne.{u_1 + 1} (α := k) (↑q : k) 0
chr : Ne.{u_1 + 1} (α := k) (↑r : k) 0
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
u v w : k
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
hbc : IsCoprime b c
heq' :
  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) +
      HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) u : k[X]) (a ^ p) =
    0
hca : IsCoprime c a
⊢ Ne.{u_1 + 1} (α := k) (↑r : k) 0

Tactic:
assumption
-- Module: Mathlib.NumberTheory.FLT.Polynomial
Goal:
k : Type u_1
inst : Field k
p q r : ℕ
hp : p ≠ 0
hq : q ≠ 0
hr : r ≠ 0
hineq : q * r + r * p + p * q ≤ p * q * r
chp : Ne.{u_1 + 1} (α := k) (↑p : k) 0
chq : Ne.{u_1 + 1} (α := k) (↑q : k) 0
chr : Ne.{u_1 + 1} (α := k) (↑r : k) 0
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
u v w : k
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
hbc : IsCoprime b c
heq' :
  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) +
      HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) u : k[X]) (a ^ p) =
    0
hca : IsCoprime c a
⊢ a ≠ 0

Tactic:
assumption