awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.FLT.Polynomial
Goal:
k : Type u_1
inst : Field k
p q r : ℕ
a b c : k[X]
u v w : k
hp : p ≠ 0
hq : q ≠ 0
hr : r ≠ 0
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
hab : IsCoprime a b
hCu : IsUnit (M := k[X]) ((C : (a : k) → k[X]) u : k[X])
hCv : IsUnit (M := k[X]) ((C : (a : k) → k[X]) v : k[X])
hCw : IsUnit (M := k[X]) ((C : (a : k) → k[X]) w : k[X])
hab₁ :
  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))
⊢ IsUnit (M := k[X]) ((C : (a : k) → k[X]) u : k[X])

Tactic:
rw [← IsCoprime.pow_iff hp.bot_lt hq.bot_lt, ← isCoprime_mul_units_left hCu hCv] at hab

Premises used: isCoprime_mul_units_left, IsCoprime.pow_iff, Ne.bot_lt
-- Module: Mathlib.NumberTheory.FLT.Polynomial
Goal:
k : Type u_1
inst : Field k
p q r : ℕ
a b c : k[X]
u v w : k
hp : p ≠ 0
hq : q ≠ 0
hr : r ≠ 0
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
hab : IsCoprime a b
hCu : IsUnit (M := k[X]) ((C : (a : k) → k[X]) u : k[X])
hCv : IsUnit (M := k[X]) ((C : (a : k) → k[X]) v : k[X])
hCw : IsUnit (M := k[X]) ((C : (a : k) → k[X]) w : k[X])
hab₁ :
  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))
hCu₁ : IsUnit (M := k[X]) ((C : (a : k) → k[X]) u : k[X])
⊢ IsUnit (M := k[X]) ((C : (a : k) → k[X]) v : k[X])

Tactic:
rw [← IsCoprime.pow_iff hp.bot_lt hq.bot_lt, ← isCoprime_mul_units_left hCu hCv] at hab

Premises used: isCoprime_mul_units_left, IsCoprime.pow_iff, Ne.bot_lt
-- Module: Mathlib.NumberTheory.FLT.Polynomial
Goal:
k : Type u_1
inst : Field k
p q r : ℕ
a b c : k[X]
u v w : k
hp : p ≠ 0
hq : q ≠ 0
hr : r ≠ 0
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
hab : IsCoprime a b
hCu : IsUnit (M := k[X]) ((C : (a : k) → k[X]) u : k[X])
hCv : IsUnit (M := k[X]) ((C : (a : k) → k[X]) v : k[X])
hCw : IsUnit (M := k[X]) ((C : (a : k) → k[X]) w : k[X])
hab₁ :
  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))
hCu₁ : IsUnit (M := k[X]) ((C : (a : k) → k[X]) u : k[X])
hCv₁ : IsUnit (M := k[X]) ((C : (a : k) → k[X]) v : k[X])
⊢ IsUnit (M := k[X]) ((C : (a : k) → k[X]) w : k[X])

Tactic:
rw [← IsCoprime.pow_iff hp.bot_lt hq.bot_lt, ← isCoprime_mul_units_left hCu hCv] at hab

Premises used: isCoprime_mul_units_left, IsCoprime.pow_iff, Ne.bot_lt
-- Module: Mathlib.NumberTheory.FLT.Polynomial
Goal:
k : Type u_1
inst : Field k
p q r : ℕ
a b c : k[X]
u v w : k
hp : p ≠ 0
hq : q ≠ 0
hr : r ≠ 0
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
hab :
  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))
hCu : IsUnit (M := k[X]) ((C : (a : k) → k[X]) u : k[X])
hCv : IsUnit (M := k[X]) ((C : (a : k) → k[X]) v : k[X])
hCw : IsUnit (M := k[X]) ((C : (a : k) → k[X]) w : k[X])
⊢ -(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:
rw [add_eq_zero_iff_neg_eq] at heq

Premises used: add_eq_zero_iff_neg_eq
-- Module: Mathlib.NumberTheory.FLT.Polynomial
Goal:
k : Type u_1
inst : Field k
p q r : ℕ
a b c : k[X]
u v w : k
hp : p ≠ 0
hq : q ≠ 0
hr : r ≠ 0
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
hab :
  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))
hCu : IsUnit (M := k[X]) ((C : (a : k) → k[X]) u : k[X])
hCv : IsUnit (M := k[X]) ((C : (a : k) → k[X]) v : k[X])
hCw : IsUnit (M := k[X]) ((C : (a : k) → k[X]) w : k[X])
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)
⊢ 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))

Tactic:
rw [add_eq_zero_iff_neg_eq] at heq

Premises used: add_eq_zero_iff_neg_eq
-- Module: Mathlib.NumberTheory.FLT.Polynomial
Goal:
k : Type u_1
inst : Field k
p q r : ℕ
a b c : k[X]
u v w : k
hp : p ≠ 0
hq : q ≠ 0
hr : r ≠ 0
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
hab :
  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))
hCu : IsUnit (M := k[X]) ((C : (a : k) → k[X]) u : k[X])
hCv : IsUnit (M := k[X]) ((C : (a : k) → k[X]) v : k[X])
hCw : IsUnit (M := k[X]) ((C : (a : k) → k[X]) w : k[X])
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)
hab₁ :
  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))
⊢ IsUnit (M := k[X]) ((C : (a : k) → k[X]) u : k[X])

Tactic:
rw [add_eq_zero_iff_neg_eq] at heq

Premises used: add_eq_zero_iff_neg_eq
-- Module: Mathlib.NumberTheory.FLT.Polynomial
Goal:
k : Type u_1
inst : Field k
p q r : ℕ
a b c : k[X]
u v w : k
hp : p ≠ 0
hq : q ≠ 0
hr : r ≠ 0
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
hab :
  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))
hCu : IsUnit (M := k[X]) ((C : (a : k) → k[X]) u : k[X])
hCv : IsUnit (M := k[X]) ((C : (a : k) → k[X]) v : k[X])
hCw : IsUnit (M := k[X]) ((C : (a : k) → k[X]) w : k[X])
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)
hab₁ :
  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))
hCu₁ : IsUnit (M := k[X]) ((C : (a : k) → k[X]) u : k[X])
⊢ IsUnit (M := k[X]) ((C : (a : k) → k[X]) v : k[X])

Tactic:
rw [add_eq_zero_iff_neg_eq] at heq

Premises used: add_eq_zero_iff_neg_eq
-- Module: Mathlib.NumberTheory.FLT.Polynomial
Goal:
k : Type u_1
inst : Field k
p q r : ℕ
a b c : k[X]
u v w : k
hp : p ≠ 0
hq : q ≠ 0
hr : r ≠ 0
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
hab :
  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))
hCu : IsUnit (M := k[X]) ((C : (a : k) → k[X]) u : k[X])
hCv : IsUnit (M := k[X]) ((C : (a : k) → k[X]) v : k[X])
hCw : IsUnit (M := k[X]) ((C : (a : k) → k[X]) w : k[X])
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)
hab₁ :
  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))
hCu₁ : IsUnit (M := k[X]) ((C : (a : k) → k[X]) u : k[X])
hCv₁ : IsUnit (M := k[X]) ((C : (a : k) → k[X]) v : k[X])
⊢ IsUnit (M := k[X]) ((C : (a : k) → k[X]) w : k[X])

Tactic:
rw [add_eq_zero_iff_neg_eq] at heq

Premises used: add_eq_zero_iff_neg_eq
-- Module: Mathlib.NumberTheory.FLT.Polynomial
Goal:
k : Type u_1
inst : Field k
p q r : ℕ
a b c : k[X]
u v w : k
hp : p ≠ 0
hq : q ≠ 0
hr : r ≠ 0
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)
hab :
  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))
hCu : IsUnit (M := k[X]) ((C : (a : k) → k[X]) u : k[X])
hCv : IsUnit (M := k[X]) ((C : (a : k) → k[X]) v : k[X])
hCw : IsUnit (M := k[X]) ((C : (a : k) → k[X]) w : k[X])
rw :
  IsCoprime (HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) v : k[X]) (b ^ q))
    (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))
⊢ IsCoprime b c

Tactic:
rw [← IsCoprime.pow_iff hq.bot_lt hr.bot_lt, ← isCoprime_mul_units_left hCv hCw,
    ← heq, IsCoprime.neg_right_iff]

Premises used: IsCoprime.neg_right_iff, isCoprime_mul_units_left, IsCoprime.pow_iff, Ne.bot_lt
-- Module: Mathlib.NumberTheory.FLT.Polynomial
Goal:
k : Type u_1
inst : Field k
p q r : ℕ
a b c : k[X]
u v w : k
hp : p ≠ 0
hq : q ≠ 0
hr : r ≠ 0
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)
hab :
  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))
hCu : IsUnit (M := k[X]) ((C : (a : k) → k[X]) u : k[X])
hCv : IsUnit (M := k[X]) ((C : (a : k) → k[X]) v : k[X])
hCw : IsUnit (M := k[X]) ((C : (a : k) → k[X]) w : k[X])
⊢ IsCoprime (HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) v : k[X]) (b ^ q))
    (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) * 1)

Tactic:
IsCoprime.add_mul_left_right hab.symm 1

Premises used: IsCoprime.symm, OfNat.ofNat, IsCoprime.add_mul_left_right
-- Module: Mathlib.NumberTheory.FLT.Polynomial
Goal:
k : Type u_1
inst : Field k
p q r : ℕ
a b c : k[X]
u v w : k
hp : p ≠ 0
hq : q ≠ 0
hr : r ≠ 0
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)
hab :
  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))
hCu : IsUnit (M := k[X]) ((C : (a : k) → k[X]) u : k[X])
hCv : IsUnit (M := k[X]) ((C : (a : k) → k[X]) v : k[X])
hCw : IsUnit (M := k[X]) ((C : (a : k) → k[X]) w : k[X])
h :
  HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) v : k[X]) (b ^ q) =
    HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) v : k[X]) (b ^ q) * 1
⊢ IsCoprime (HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) v : k[X]) (b ^ q))
    (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))

Tactic:
convert! IsCoprime.add_mul_left_right hab.symm 1 using 2

Premises used: IsCoprime.symm, OfNat.ofNat, IsCoprime.add_mul_left_right
-- Module: Mathlib.NumberTheory.FLT.Polynomial
Goal:
k : Type u_1
inst : Field k
p q r : ℕ
a b c : k[X]
u v w : k
hp : p ≠ 0
hq : q ≠ 0
hr : r ≠ 0
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)
hab :
  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))
hCu : IsUnit (M := k[X]) ((C : (a : k) → k[X]) u : k[X])
hCv : IsUnit (M := k[X]) ((C : (a : k) → k[X]) v : k[X])
hCw : IsUnit (M := k[X]) ((C : (a : k) → k[X]) w : k[X])
h h₁ :
  HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) v : k[X]) (b ^ q) =
    HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) v : k[X]) (b ^ q)
⊢ HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) v : k[X]) (b ^ q) =
    HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) v : k[X]) (b ^ q) * 1

Tactic:
rw [mul_one]

Premises used: mul_one
-- Module: Mathlib.NumberTheory.FLT.Polynomial
Goal:
p q r a b c : ℕ
hp : p ≠ 0
hq : q ≠ 0
hr : r ≠ 0
hineq : q * r + r * p + p * q ≤ p * q * r
hpa : p * a < a + b + c
hqb : q * b < a + b + c
hrc : r * c < a + b + c
h : p * q * r * (a + b + c) + 1 ≤ p * q * r * (a + b + c)
⊢ False

Tactic:
simp at h
-- Module: Mathlib.NumberTheory.FLT.Polynomial
Goal:
p q r a b c : ℕ
hp : p ≠ 0
hq : q ≠ 0
hr : r ≠ 0
hineq : q * r + r * p + p * q ≤ p * q * r
hpa : p * a < a + b + c
hqb : q * b < a + b + c
hrc : r * c < a + b + c
suffices : p * q * r * (a + b + c) + 1 ≤ p * q * r * (a + b + c)
⊢ False

Tactic:
suffices h : p * q * r * (a + b + c) + 1 ≤ p * q * r * (a + b + c) by simp at h
-- Module: Mathlib.NumberTheory.FLT.Polynomial
Goal:
p q r a b c : ℕ
hp : p ≠ 0
hq : q ≠ 0
hr : r ≠ 0
hineq : q * r + r * p + p * q ≤ p * q * r
hpa : p * a < a + b + c
hqb : q * b < a + b + c
hrc : r * c < a + b + c
⊢ p * q * r * (a + b + c) + 1 = p * a * (q * r) + q * b * (r * p) + r * c * (p * q) + 1

Tactic:
ring
-- Module: Mathlib.NumberTheory.FLT.Polynomial
Goal:
p q r a b c : ℕ
hp : p ≠ 0
hq : q ≠ 0
hr : r ≠ 0
hineq : q * r + r * p + p * q ≤ p * q * r
hpa : p * a < a + b + c
hqb : q * b < a + b + c
hrc : r * c < a + b + c
h₁ : 0 < q * r
h₂ : 0 < r * p
h₃ : 0 < p * q
⊢ p * a * (q * r) + q * b * (r * p) + r * c * (p * q) <
    (a + b + c) * (q * r) + (a + b + c) * (r * p) + (a + b + c) * (p * q)

Tactic:
gcongr
-- Module: Mathlib.NumberTheory.FLT.Polynomial
Goal:
p q r a b c : ℕ
hp : p ≠ 0
hq : q ≠ 0
hr : r ≠ 0
hineq : q * r + r * p + p * q ≤ p * q * r
hpa : p * a < a + b + c
hqb : q * b < a + b + c
hrc : r * c < a + b + c
⊢ (a + b + c) * (q * r) + (a + b + c) * (r * p) + (a + b + c) * (p * q) = (q * r + r * p + p * q) * (a + b + c)

Tactic:
ring
-- Module: Mathlib.NumberTheory.FLT.Polynomial
Goal:
p q r a b c : ℕ
hp : p ≠ 0
hq : q ≠ 0
hr : r ≠ 0
hineq : q * r + r * p + p * q ≤ p * q * r
hpa : p * a < a + b + c
hqb : q * b < a + b + c
hrc : r * c < a + b + c
⊢ (q * r + r * p + p * q) * (a + b + c) ≤ p * q * r * (a + b + c)

Tactic:
gcongr
-- Module: Mathlib.NumberTheory.FLT.Polynomial
Goal:
p q r a b c : ℕ
hp : p ≠ 0
hq : q ≠ 0
hr : r ≠ 0
hineq : q * r + r * p + p * q ≤ p * q * r
hpa : p * a < a + b + c
hqb : q * b < a + b + c
hrc : r * c < a + b + c
_ : p * q * r * (a + b + c) + 1 = p * a * (q * r) + q * b * (r * p) + r * c * (p * q) + 1
_₁ :
  p * a * (q * r) + q * b * (r * p) + r * c * (p * q) + 1 ≤
    (a + b + c) * (q * r) + (a + b + c) * (r * p) + (a + b + c) * (p * q)
_₂ : (a + b + c) * (q * r) + (a + b + c) * (r * p) + (a + b + c) * (p * q) = (q * r + r * p + p * q) * (a + b + c)
_₃ : (q * r + r * p + p * q) * (a + b + c) ≤ p * q * r * (a + b + c)
⊢ p * q * r * (a + b + c) + 1 ≤ p * q * r * (a + b + c)

Tactic:
calc
    _ = (p * a) * (q * r) + (q * b) * (r * p) + (r * c) * (p * q) + 1 := by ring
    _ ≤ (a + b + c) * (q * r) + (a + b + c) * (r * p) + (a + b + c) * (p * q) := by
      rw [Nat.succ_le_iff]
      gcongr
    _ = (q * r + r * p + p * q) * (a + b + c) := by ring
    _ ≤ _ := by gcongr

Premises used: HMul.hMul, HAdd.hAdd
-- 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 : IsCoprime a b
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

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

Tactic:
have hbc : IsCoprime b c := by apply rot_coprime heq <;> 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
⊢ 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:
rw [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
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 b c

Tactic:
rw [add_rotate] at heq

Premises used: add_rotate