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]) 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 apply : IsCoprime b c
apply₁ : q ≠ 0
apply₂ : r ≠ 0
apply₃ : p ≠ 0
apply₄ : v ≠ 0
apply₅ : w ≠ 0
apply₆ : u ≠ 0
⊢ IsCoprime c a

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]) 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
⊢ 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 : 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]) 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
⊢ 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]) 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
⊢ 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]) 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
⊢ 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]) 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
⊢ 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]) 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
⊢ 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]) 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
⊢ 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
⊢ IsCoprime c a

Tactic:
have hca : IsCoprime c a := by
    rw [add_rotate] at heq; 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
hca : IsCoprime c a
⊢ Ne (α := k[X]) ((C : (a : k) → k[X]) u : k[X]) (0 : k[X])

Tactic:
have hCu := C_ne_zero.mpr hu
-- 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])
⊢ Ne (α := k[X]) ((C : (a : k) → k[X]) v : k[X]) (0 : k[X])

Tactic:
have hCv := C_ne_zero.mpr hv
-- 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])
⊢ Ne (α := k[X]) ((C : (a : k) → k[X]) w : k[X]) (0 : k[X])

Tactic:
have hCw := C_ne_zero.mpr hw
-- 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])
⊢ a ^ p ≠ 0

Tactic:
have hap := pow_ne_zero p ha
-- 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
⊢ b ^ q ≠ 0

Tactic:
have hbq := pow_ne_zero q hb
-- 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
⊢ c ^ r ≠ 0

Tactic:
have hcr := pow_ne_zero r hc
-- 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
rw : IsCoprime (a ^ p) (b ^ q)
⊢ 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 [isCoprime_mul_units_left hu.isUnit_C hv.isUnit_C]

Premises used: _private.0.Ne.isUnit_C, isCoprime_mul_units_left
-- 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
⊢ IsCoprime (a ^ p) (b ^ q)

Tactic:
hab.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
⊢ IsCoprime (a ^ p) (b ^ q)

Tactic:
exact hab.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
⊢ 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:
have habp : IsCoprime (C u * a ^ p) (C v * b ^ q) := by
    rw [isCoprime_mul_units_left hu.isUnit_C hv.isUnit_C]; exact hab.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))
rw : IsCoprime (b ^ q) (c ^ r)
⊢ 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))

Tactic:
rw [isCoprime_mul_units_left hv.isUnit_C hw.isUnit_C]

Premises used: _private.0.Ne.isUnit_C, isCoprime_mul_units_left
-- 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))
⊢ IsCoprime (b ^ q) (c ^ r)

Tactic:
hbc.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))
⊢ IsCoprime (b ^ q) (c ^ r)

Tactic:
exact hbc.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))
⊢ 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))

Tactic:
have hbcp : IsCoprime (C v * b ^ q) (C w * c ^ r) := by
    rw [isCoprime_mul_units_left hv.isUnit_C hw.isUnit_C]; exact hbc.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))
rw : IsCoprime (c ^ r) (a ^ p)
⊢ 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:
rw [isCoprime_mul_units_left hw.isUnit_C hu.isUnit_C]

Premises used: _private.0.Ne.isUnit_C, isCoprime_mul_units_left
-- 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:
hca.pow

Premises used: IsCoprime.pow