awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
hca : IsCoprime c a
hCu : Ne (α := k[X]) ((C : (a : k) → k[X]) u : k[X]) (0 : k[X])
hCv : Ne (α := k[X]) ((C : (a : k) → k[X]) v : k[X]) (0 : k[X])
hCw : Ne (α := k[X]) ((C : (a : k) → k[X]) w : k[X]) (0 : k[X])
hap : a ^ p ≠ 0
hbq : b ^ q ≠ 0
hcr : c ^ r ≠ 0
habp :
  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))
hbcp :
  IsCoprime (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))
⊢ IsCoprime (c ^ r) (a ^ p)

Tactic:
exact hca.pow

Premises used: IsCoprime.pow
-- 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
hca : IsCoprime c a
hCu : Ne (α := k[X]) ((C : (a : k) → k[X]) u : k[X]) (0 : k[X])
hCv : Ne (α := k[X]) ((C : (a : k) → k[X]) v : k[X]) (0 : k[X])
hCw : Ne (α := k[X]) ((C : (a : k) → k[X]) w : k[X]) (0 : k[X])
hap : a ^ p ≠ 0
hbq : b ^ q ≠ 0
hcr : c ^ r ≠ 0
habp :
  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))
hbcp :
  IsCoprime (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))
⊢ IsCoprime (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))

Tactic:
have hcap : IsCoprime (C w * c ^ r) (C u * a ^ p) := by
    rw [isCoprime_mul_units_left hw.isUnit_C hu.isUnit_C]; exact hca.pow
-- 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
hca : IsCoprime c a
hCu : Ne (α := k[X]) ((C : (a : k) → k[X]) u : k[X]) (0 : k[X])
hCv : Ne (α := k[X]) ((C : (a : k) → k[X]) v : k[X]) (0 : k[X])
hCw : Ne (α := k[X]) ((C : (a : k) → k[X]) w : k[X]) (0 : k[X])
hap : a ^ p ≠ 0
hbq : b ^ q ≠ 0
hcr : c ^ r ≠ 0
habp :
  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))
hbcp :
  IsCoprime (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))
hcap :
  IsCoprime (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))
⊢ 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))
    (HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) w : k[X]) (c ^ r))

Tactic:
have habcp := hcap.symm.mul_left hbcp
-- 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
hca : IsCoprime c a
hCu : Ne (α := k[X]) ((C : (a : k) → k[X]) u : k[X]) (0 : k[X])
hCv : Ne (α := k[X]) ((C : (a : k) → k[X]) v : k[X]) (0 : k[X])
hCw : Ne (α := k[X]) ((C : (a : k) → k[X]) w : k[X]) (0 : k[X])
hap : a ^ p ≠ 0
hbq : b ^ q ≠ 0
hcr : c ^ r ≠ 0
habp :
  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))
hbcp :
  IsCoprime (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))
hcap :
  IsCoprime (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))
habcp :
  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))
    (HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) w : k[X]) (c ^ r))
nd_lt :
  p * a.natDegree + 1 ≤ (radical (a * b * c)).natDegree ∧
    q * b.natDegree + 1 ≤ (radical (a * b * c)).natDegree ∧ r * c.natDegree + 1 ≤ (radical (a * b * c)).natDegree
⊢ p * a.natDegree + 1 ≤ (radical (a * b * c)).natDegree

Tactic:
obtain ⟨hpa', hqb', hrc'⟩ := nd_lt
-- 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
hca : IsCoprime c a
hCu : Ne (α := k[X]) ((C : (a : k) → k[X]) u : k[X]) (0 : k[X])
hCv : Ne (α := k[X]) ((C : (a : k) → k[X]) v : k[X]) (0 : k[X])
hCw : Ne (α := k[X]) ((C : (a : k) → k[X]) w : k[X]) (0 : k[X])
hap : a ^ p ≠ 0
hbq : b ^ q ≠ 0
hcr : c ^ r ≠ 0
habp :
  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))
hbcp :
  IsCoprime (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))
hcap :
  IsCoprime (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))
habcp :
  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))
    (HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) w : k[X]) (c ^ r))
nd_lt :
  p * a.natDegree + 1 ≤ (radical (a * b * c)).natDegree ∧
    q * b.natDegree + 1 ≤ (radical (a * b * c)).natDegree ∧ r * c.natDegree + 1 ≤ (radical (a * b * c)).natDegree
hpa' : p * a.natDegree + 1 ≤ (radical (a * b * c)).natDegree
⊢ q * b.natDegree + 1 ≤ (radical (a * b * c)).natDegree

Tactic:
obtain ⟨hpa', hqb', hrc'⟩ := nd_lt
-- 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
hca : IsCoprime c a
hCu : Ne (α := k[X]) ((C : (a : k) → k[X]) u : k[X]) (0 : k[X])
hCv : Ne (α := k[X]) ((C : (a : k) → k[X]) v : k[X]) (0 : k[X])
hCw : Ne (α := k[X]) ((C : (a : k) → k[X]) w : k[X]) (0 : k[X])
hap : a ^ p ≠ 0
hbq : b ^ q ≠ 0
hcr : c ^ r ≠ 0
habp :
  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))
hbcp :
  IsCoprime (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))
hcap :
  IsCoprime (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))
habcp :
  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))
    (HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) w : k[X]) (c ^ r))
nd_lt :
  p * a.natDegree + 1 ≤ (radical (a * b * c)).natDegree ∧
    q * b.natDegree + 1 ≤ (radical (a * b * c)).natDegree ∧ r * c.natDegree + 1 ≤ (radical (a * b * c)).natDegree
hpa' : p * a.natDegree + 1 ≤ (radical (a * b * c)).natDegree
hqb' : q * b.natDegree + 1 ≤ (radical (a * b * c)).natDegree
⊢ r * c.natDegree + 1 ≤ (radical (a * b * c)).natDegree

Tactic:
obtain ⟨hpa', hqb', hrc'⟩ := nd_lt
-- 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
hca : IsCoprime c a
hCu : Ne (α := k[X]) ((C : (a : k) → k[X]) u : k[X]) (0 : k[X])
hCv : Ne (α := k[X]) ((C : (a : k) → k[X]) v : k[X]) (0 : k[X])
hCw : Ne (α := k[X]) ((C : (a : k) → k[X]) w : k[X]) (0 : k[X])
hap : a ^ p ≠ 0
hbq : b ^ q ≠ 0
hcr : c ^ r ≠ 0
habp :
  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))
hbcp :
  IsCoprime (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))
hcap :
  IsCoprime (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))
habcp :
  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))
    (HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) w : k[X]) (c ^ r))
hpa' : p * a.natDegree + 1 ≤ (radical (a * b * c)).natDegree
hqb' : q * b.natDegree + 1 ≤ (radical (a * b * c)).natDegree
hrc' : r * c.natDegree + 1 ≤ (radical (a * b * c)).natDegree
⊢ p * a.natDegree + 1 ≤ (a * b * c).natDegree

Tactic:
have hpa := hpa'.trans natDegree_radical_le
-- 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
hca : IsCoprime c a
hCu : Ne (α := k[X]) ((C : (a : k) → k[X]) u : k[X]) (0 : k[X])
hCv : Ne (α := k[X]) ((C : (a : k) → k[X]) v : k[X]) (0 : k[X])
hCw : Ne (α := k[X]) ((C : (a : k) → k[X]) w : k[X]) (0 : k[X])
hap : a ^ p ≠ 0
hbq : b ^ q ≠ 0
hcr : c ^ r ≠ 0
habp :
  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))
hbcp :
  IsCoprime (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))
hcap :
  IsCoprime (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))
habcp :
  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))
    (HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) w : k[X]) (c ^ r))
hpa' : p * a.natDegree + 1 ≤ (radical (a * b * c)).natDegree
hqb' : q * b.natDegree + 1 ≤ (radical (a * b * c)).natDegree
hrc' : r * c.natDegree + 1 ≤ (radical (a * b * c)).natDegree
hpa : p * a.natDegree + 1 ≤ (a * b * c).natDegree
⊢ q * b.natDegree + 1 ≤ (a * b * c).natDegree

Tactic:
have hqb := hqb'.trans natDegree_radical_le
-- 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
hca : IsCoprime c a
hCu : Ne (α := k[X]) ((C : (a : k) → k[X]) u : k[X]) (0 : k[X])
hCv : Ne (α := k[X]) ((C : (a : k) → k[X]) v : k[X]) (0 : k[X])
hCw : Ne (α := k[X]) ((C : (a : k) → k[X]) w : k[X]) (0 : k[X])
hap : a ^ p ≠ 0
hbq : b ^ q ≠ 0
hcr : c ^ r ≠ 0
habp :
  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))
hbcp :
  IsCoprime (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))
hcap :
  IsCoprime (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))
habcp :
  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))
    (HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) w : k[X]) (c ^ r))
hpa' : p * a.natDegree + 1 ≤ (radical (a * b * c)).natDegree
hqb' : q * b.natDegree + 1 ≤ (radical (a * b * c)).natDegree
hrc' : r * c.natDegree + 1 ≤ (radical (a * b * c)).natDegree
hpa : p * a.natDegree + 1 ≤ (a * b * c).natDegree
hqb : q * b.natDegree + 1 ≤ (a * b * c).natDegree
⊢ r * c.natDegree + 1 ≤ (a * b * c).natDegree

Tactic:
have hrc := hrc'.trans natDegree_radical_le
-- 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
hca : IsCoprime c a
hCu : Ne (α := k[X]) ((C : (a : k) → k[X]) u : k[X]) (0 : k[X])
hCv : Ne (α := k[X]) ((C : (a : k) → k[X]) v : k[X]) (0 : k[X])
hCw : Ne (α := k[X]) ((C : (a : k) → k[X]) w : k[X]) (0 : k[X])
hap : a ^ p ≠ 0
hbq : b ^ q ≠ 0
hcr : c ^ r ≠ 0
habp :
  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))
hbcp :
  IsCoprime (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))
hcap :
  IsCoprime (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))
habcp :
  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))
    (HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) w : k[X]) (c ^ r))
hpa' : p * a.natDegree + 1 ≤ (radical (a * b * c)).natDegree
hqb' : q * b.natDegree + 1 ≤ (radical (a * b * c)).natDegree
hrc' : r * c.natDegree + 1 ≤ (radical (a * b * c)).natDegree
hpa : p * a.natDegree + 1 ≤ (a * b * c).natDegree
hqb : q * b.natDegree + 1 ≤ (a * b * c).natDegree
hrc : r * c.natDegree + 1 ≤ (a * b * c).natDegree
⊢ p * a.natDegree < a.natDegree + b.natDegree + c.natDegree

Tactic:
rw [natDegree_mul (mul_ne_zero ha hb) hc,
      natDegree_mul ha hb, Nat.add_one_le_iff] at hpa hqb hrc

Premises used: Polynomial.natDegree_mul, Nat.add_one_le_iff, mul_ne_zero
-- 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
hca : IsCoprime c a
hCu : Ne (α := k[X]) ((C : (a : k) → k[X]) u : k[X]) (0 : k[X])
hCv : Ne (α := k[X]) ((C : (a : k) → k[X]) v : k[X]) (0 : k[X])
hCw : Ne (α := k[X]) ((C : (a : k) → k[X]) w : k[X]) (0 : k[X])
hap : a ^ p ≠ 0
hbq : b ^ q ≠ 0
hcr : c ^ r ≠ 0
habp :
  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))
hbcp :
  IsCoprime (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))
hcap :
  IsCoprime (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))
habcp :
  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))
    (HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) w : k[X]) (c ^ r))
hpa' : p * a.natDegree + 1 ≤ (radical (a * b * c)).natDegree
hqb' : q * b.natDegree + 1 ≤ (radical (a * b * c)).natDegree
hrc' : r * c.natDegree + 1 ≤ (radical (a * b * c)).natDegree
hpa : p * a.natDegree + 1 ≤ (a * b * c).natDegree
hqb : q * b.natDegree + 1 ≤ (a * b * c).natDegree
hrc : r * c.natDegree + 1 ≤ (a * b * c).natDegree
hpa₁ : p * a.natDegree < a.natDegree + b.natDegree + c.natDegree
⊢ q * b.natDegree < a.natDegree + b.natDegree + c.natDegree

Tactic:
rw [natDegree_mul (mul_ne_zero ha hb) hc,
      natDegree_mul ha hb, Nat.add_one_le_iff] at hpa hqb hrc

Premises used: Polynomial.natDegree_mul, Nat.add_one_le_iff, mul_ne_zero
-- 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
hca : IsCoprime c a
hCu : Ne (α := k[X]) ((C : (a : k) → k[X]) u : k[X]) (0 : k[X])
hCv : Ne (α := k[X]) ((C : (a : k) → k[X]) v : k[X]) (0 : k[X])
hCw : Ne (α := k[X]) ((C : (a : k) → k[X]) w : k[X]) (0 : k[X])
hap : a ^ p ≠ 0
hbq : b ^ q ≠ 0
hcr : c ^ r ≠ 0
habp :
  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))
hbcp :
  IsCoprime (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))
hcap :
  IsCoprime (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))
habcp :
  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))
    (HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) w : k[X]) (c ^ r))
hpa' : p * a.natDegree + 1 ≤ (radical (a * b * c)).natDegree
hqb' : q * b.natDegree + 1 ≤ (radical (a * b * c)).natDegree
hrc' : r * c.natDegree + 1 ≤ (radical (a * b * c)).natDegree
hpa : p * a.natDegree + 1 ≤ (a * b * c).natDegree
hqb : q * b.natDegree + 1 ≤ (a * b * c).natDegree
hrc : r * c.natDegree + 1 ≤ (a * b * c).natDegree
hpa₁ : p * a.natDegree < a.natDegree + b.natDegree + c.natDegree
hqb₁ : q * b.natDegree < a.natDegree + b.natDegree + c.natDegree
⊢ r * c.natDegree < a.natDegree + b.natDegree + c.natDegree

Tactic:
rw [natDegree_mul (mul_ne_zero ha hb) hc,
      natDegree_mul ha hb, Nat.add_one_le_iff] at hpa hqb hrc

Premises used: Polynomial.natDegree_mul, Nat.add_one_le_iff, mul_ne_zero