-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Polynomial (goal)
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))
inl :
  ∀
    (nd_lt :
      (HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) u : k[X]) (a ^ p)).natDegree + 1 ≤
          (radical
              (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))).natDegree ∧
        (HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) v : k[X]) (b ^ q)).natDegree + 1 ≤
            (radical
                (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))).natDegree ∧
          (HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) w : k[X]) (c ^ r)).natDegree + 1 ≤
            (radical
                (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))).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])
⊢ 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 inr : ∀
  (dr0 :
    Eq (α := k[X])
        ((derivative : (a : k[X]) → k[X]) (HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) u : k[X]) (a ^ p)) : k[X])
        (0 : k[X]) ∧
      Eq (α := k[X])
          ((derivative : (a : k[X]) → k[X]) (HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) v : k[X]) (b ^ q)) : k[X])
          (0 : k[X]) ∧
        Eq (α := k[X])
          ((derivative : (a : k[X]) → k[X]) (HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) w : k[X]) (c ^ r)) : 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: classical
  rcases Polynomial.abc
      (mul_ne_zero hCu hap) (mul_ne_zero hCv hbq) (mul_ne_zero hCw hcr)
      habp heq with nd_lt | dr0
  · simp_rw [radical_mul habcp.isRelPrime, radical_mul habp.isRelPrime,
      radical_mul_of_isUnit_left hu.isUnit_C,
      radical_mul_of_isUnit_left hv.isUnit_C,
      radical_mul_of_isUnit_left hw.isUnit_C,
      radical_pow a hp, radical_pow b hq, radical_pow c hr,
      natDegree_mul hCu hap,
      natDegree_mul hCv hbq,
      natDegree_mul hCw hcr,
      natDegree_C, natDegree_pow, zero_add,
      ← radical_mul hab.isRelPrime,
      ← radical_mul (hca.symm.mul_left hbc).isRelPrime] at nd_lt
    obtain ⟨hpa', hqb', hrc'⟩ := nd_lt
    have hpa := hpa'.trans natDegree_radical_le
    have hqb := hqb'.trans natDegree_radical_le
    have hrc := hrc'.trans natDegree_radical_le
    rw [natDegree_mul (mul_ne_zero ha hb) hc,
      natDegree_mul ha hb, Nat.add_one_le_iff] at hpa hqb hrc
    exfalso
    exact (ineq_pqr_contradiction hp hq hr hineq hpa hqb hrc)
  · rw [derivative_C_mul, derivative_C_mul, derivative_C_mul,
      mul_eq_zero_iff_left (C_ne_zero.mpr hu),
      mul_eq_zero_iff_left (C_ne_zero.mpr hv),
      mul_eq_zero_iff_left (C_ne_zero.mpr hw),
      derivative_pow_eq_zero chp,
      derivative_pow_eq_zero chq,
      derivative_pow_eq_zero chr] at dr0
    exact dr0