-- Mathlib/NumberTheory/FLT/Polynomial.lean
theorem Polynomial.flt_catalan_aux
    {p q r : ℕ} {a b c : k[X]} {u v w : k}
    (heq : C u * a ^ p + C v * b ^ q + C w * c ^ r = 0)
    (hp : 0 < p) (hq : 0 < q) (hr : 0 < r)
    (hineq : q * r + r * p + p * q ≤ p * q * r)
    (chp : (p : k) ≠ 0) (chq : (q : k) ≠ 0) (chr : (r : k) ≠ 0)
    (ha : a ≠ 0) (hb : b ≠ 0) (hc : c ≠ 0) (hab : IsCoprime a b)
    (hu : u ≠ 0) (hv : v ≠ 0) (hw : w ≠ 0) :
    a.natDegree = 0

Proof state:
k : Type u_1
inst✝ : Field k
p q r : ℕ
u v w : k
hp : 0 < p
hq : 0 < q
hr : 0 < r
hineq : q * r + r * p + p * q ≤ p * q * r
chp : ↑p ≠ 0
chq : ↑q ≠ 0
chr : ↑r ≠ 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 : derivative a = 0
bd : derivative b = 0
cd : derivative c = 0
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) ca
eq_deg_a : a.natDegree = ca.natDegree * ch
eq_b : b = (expand k ch) cb
eq_deg_b : b.natDegree = cb.natDegree * ch
eq_c : c = (expand k ch) cc
eq_deg_c : c.natDegree = cc.natDegree * ch
hnca : ¬ca.natDegree = 0
heq : (expand k ch) (C u * ca ^ p + C v * cb ^ q + C w * cc ^ r) = 0
⊢ C u * ca ^ p + C v * cb ^ q + C w * cc ^ r = 0

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

Result:
no goals

Proof state:
k : Type u_1
inst✝ : Field k
p q r : ℕ
u v w : k
hp : 0 < p
hq : 0 < q
hr : 0 < r
hineq : q * r + r * p + p * q ≤ p * q * r
chp : ↑p ≠ 0
chq : ↑q ≠ 0
chr : ↑r ≠ 0
hu : u ≠ 0
hv : v ≠ 0
hw : w ≠ 0
d : ℕ
a b c : k[X]
heq : C u * a ^ p + C v * b ^ q + C w * c ^ r = 0
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
eq_d : a.natDegree = d + 1
ad : derivative a = 0
bd : derivative b = 0
cd : derivative c = 0
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) ca
eq_deg_a : a.natDegree = ca.natDegree * ch
eq_b : b = (expand k ch) cb
eq_deg_b : b.natDegree = cb.natDegree * ch
eq_c : c = (expand k ch) cc
eq_deg_c : c.natDegree = cc.natDegree * ch
hnca : ¬ca.natDegree = 0
x✝ : ch ≠ 1
hch2 : 2 ≤ ch
⊢ ca.natDegree + 1 ≤ ca.natDegree * ch

Tactic:
refine le_trans ?_ (Nat.mul_le_mul_left _ hch2)

Result:
k : Type u_1
inst✝ : Field k
p q r : ℕ
u v w : k
hp : 0 < p
hq : 0 < q
hr : 0 < r
hineq : q * r + r * p + p * q ≤ p * q * r
chp : ↑p ≠ 0
chq : ↑q ≠ 0
chr : ↑r ≠ 0
hu : u ≠ 0
hv : v ≠ 0
hw : w ≠ 0
d : ℕ
a b c : k[X]
heq : C u * a ^ p + C v * b ^ q + C w * c ^ r = 0
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
eq_d : a.natDegree = d + 1
ad : derivative a = 0
bd : derivative b = 0
cd : derivative c = 0
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) ca
eq_deg_a : a.natDegree = ca.natDegree * ch
eq_b : b = (expand k ch) cb
eq_deg_b : b.natDegree = cb.natDegree * ch
eq_c : c = (expand k ch) cc
eq_deg_c : c.natDegree = cc.natDegree * ch
hnca : ¬ca.natDegree = 0
x✝ : ch ≠ 1
hch2 : 2 ≤ ch
⊢ ca.natDegree + 1 ≤ ca.natDegree * 2

Proof state:
k : Type u_1
inst✝ : Field k
p q r : ℕ
u v w : k
hp : 0 < p
hq : 0 < q
hr : 0 < r
hineq : q * r + r * p + p * q ≤ p * q * r
chp : ↑p ≠ 0
chq : ↑q ≠ 0
chr : ↑r ≠ 0
hu : u ≠ 0
hv : v ≠ 0
hw : w ≠ 0
d : ℕ
ih_d :
  ∀ m ≤ d,
    ∀ {a b c : k[X]},
      C u * a ^ p + C v * b ^ q + C w * c ^ r = 0 → a ≠ 0 → b ≠ 0 → c ≠ 0 → IsCoprime a b → a.natDegree = m → m = 0
a b c : k[X]
heq : C u * a ^ p + C v * b ^ q + C w * c ^ r = 0
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
eq_d : a.natDegree = d + 1
ad : derivative a = 0
bd : derivative b = 0
cd : derivative c = 0
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) ca
eq_deg_a : a.natDegree = ca.natDegree * ch
eq_b : b = (expand k ch) cb
eq_deg_b : b.natDegree = cb.natDegree * ch
eq_c : c = (expand k ch) cc
eq_deg_c : c.natDegree = cc.natDegree * ch
hca : ca.natDegree = 0
⊢ d + 1 = 0

Tactic:
rw [← eq_d, eq_deg_a, hca, zero_mul]

Result:
no goals