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
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
⊢ b ≠ 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
⊢ c ≠ 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
⊢ IsCoprime a b

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
⊢ 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
hca : IsCoprime c a
⊢ 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
hca : IsCoprime c a
⊢ 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
hca : IsCoprime c a
refine_2 :
  ∀ (hineq : r * p + p * q + q * r ≤ 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]) 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)
    (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), b.natDegree = 0
⊢ b.natDegree = 0

Tactic:
rw [add_rotate] at heq hineq

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 : r * p + p * q + q * r ≤ 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]) 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
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_2 :
  ∀ (hineq : r * p + p * q + q * r ≤ q * r * p) (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]) 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)
    (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), b.natDegree = 0
⊢ b.natDegree = 0

Tactic:
rw [mul_rotate] at hineq

Premises used: mul_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 : r * p + p * q + q * r ≤ q * r * p
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]) 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
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_2 : q ≠ 0
refine_2₁ : r ≠ 0
refine_2₂ : p ≠ 0
refine_2₃ : r * p + p * q + q * r ≤ q * r * p
refine_2₄ : Ne.{u_1 + 1} (α := k) (↑q : k) 0
refine_2₅ : Ne.{u_1 + 1} (α := k) (↑r : k) 0
refine_2₆ : Ne.{u_1 + 1} (α := k) (↑p : k) 0
refine_2₇ : b ≠ 0
refine_2₈ : c ≠ 0
refine_2₉ : a ≠ 0
refine_2₁₀ : IsCoprime b c
refine_2₁₁ : v ≠ 0
refine_2₁₂ : w ≠ 0
refine_2₁₃ : u ≠ 0
⊢ b.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 : r * p + p * q + q * r ≤ q * r * p
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]) 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
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 : r * p + p * q + q * r ≤ q * r * p
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]) 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
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 : r * p + p * q + q * r ≤ q * r * p
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]) 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
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 : r * p + p * q + q * r ≤ q * r * p
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]) 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
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 * p + p * q + q * r ≤ q * r * p

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 : r * p + p * q + q * r ≤ q * r * p
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]) 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
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 : r * p + p * q + q * r ≤ q * r * p
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]) 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
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 : r * p + p * q + q * r ≤ q * r * p
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]) 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
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 : r * p + p * q + q * r ≤ q * r * p
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]) 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
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
⊢ b ≠ 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 : r * p + p * q + q * r ≤ q * r * p
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]) 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
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
⊢ c ≠ 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 : r * p + p * q + q * r ≤ q * r * p
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]) 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
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
-- 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 : r * p + p * q + q * r ≤ q * r * p
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]) 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
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
⊢ IsCoprime b c

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 : r * p + p * q + q * r ≤ q * r * p
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]) 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
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
⊢ 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 : r * p + p * q + q * r ≤ q * r * p
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]) 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
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
⊢ 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 : r * p + p * q + q * r ≤ q * r * p
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]) 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
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
⊢ u ≠ 0

Tactic:
assumption