-- Mathlib/NumberTheory/FLT/Polynomial.lean
private lemma rot_coprime
    {p q r : ℕ} {a b c : k[X]} {u v w : k}
    {hp : 0 < p} {hq : 0 < q} {hr : 0 < r}
    {hu : u ≠ 0} {hv : v ≠ 0} {hw : w ≠ 0}
    (heq : C u * a ^ p + C v * b ^ q + C w * c ^ r = 0) (hab : IsCoprime a b) : IsCoprime b c

Proof state:
k : Type u_1
inst✝ : Field k
p q r : ℕ
a b c : k[X]
u v w : k
hp : 0 < p
hq : 0 < q
hr : 0 < r
hu : u ≠ 0
hv : v ≠ 0
hw : w ≠ 0
heq : C u * a ^ p + C v * b ^ q + C w * c ^ r = 0
hab : IsCoprime a b
hCu : IsUnit (C u)
hCv : IsUnit (C v)
hCw : IsUnit (C w)
⊢ IsCoprime b c

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

Result:
k : Type u_1
inst✝ : Field k
p q r : ℕ
a b c : k[X]
u v w : k
hp : 0 < p
hq : 0 < q
hr : 0 < r
hu : u ≠ 0
hv : v ≠ 0
hw : w ≠ 0
heq : C u * a ^ p + C v * b ^ q + C w * c ^ r = 0
hab : IsCoprime (C u * a ^ p) (C v * b ^ q)
hCu : IsUnit (C u)
hCv : IsUnit (C v)
hCw : IsUnit (C w)
⊢ IsCoprime b c

Proof state:
k : Type u_1
inst✝ : Field k
p q r : ℕ
a b c : k[X]
u v w : k
hp : 0 < p
hq : 0 < q
hr : 0 < r
hu : u ≠ 0
hv : v ≠ 0
hw : w ≠ 0
heq : C u * a ^ p + C v * b ^ q + C w * c ^ r = 0
hab : IsCoprime a b
hCu : IsUnit (C u)
hCv : IsUnit (C v)
⊢ IsCoprime b c

Tactic:
have hCw : IsUnit (C w) := hw.isUnit_C

Result:
k : Type u_1
inst✝ : Field k
p q r : ℕ
a b c : k[X]
u v w : k
hp : 0 < p
hq : 0 < q
hr : 0 < r
hu : u ≠ 0
hv : v ≠ 0
hw : w ≠ 0
heq : C u * a ^ p + C v * b ^ q + C w * c ^ r = 0
hab : IsCoprime a b
hCu : IsUnit (C u)
hCv : IsUnit (C v)
hCw : IsUnit (C w)
⊢ IsCoprime b c

Proof state:
k : Type u_1
inst✝ : Field k
p q r : ℕ
a b c : k[X]
u v w : k
hp : 0 < p
hq : 0 < q
hr : 0 < r
hu : u ≠ 0
hv : v ≠ 0
hw : w ≠ 0
heq : -(C u * a ^ p + C v * b ^ q) = C w * c ^ r
hab : IsCoprime (C u * a ^ p) (C v * b ^ q)
hCu : IsUnit (C u)
hCv : IsUnit (C v)
hCw : IsUnit (C w)
⊢ IsCoprime b c

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

Result:
k : Type u_1
inst✝ : Field k
p q r : ℕ
a b c : k[X]
u v w : k
hp : 0 < p
hq : 0 < q
hr : 0 < r
hu : u ≠ 0
hv : v ≠ 0
hw : w ≠ 0
heq : -(C u * a ^ p + C v * b ^ q) = C w * c ^ r
hab : IsCoprime (C u * a ^ p) (C v * b ^ q)
hCu : IsUnit (C u)
hCv : IsUnit (C v)
hCw : IsUnit (C w)
⊢ IsCoprime (C v * b ^ q) (C u * a ^ p + C v * b ^ q)

Proof state:
k : Type u_1
inst✝ : Field k
p q r : ℕ
a b c : k[X]
u v w : k
hp : 0 < p
hq : 0 < q
hr : 0 < r
hu : u ≠ 0
hv : v ≠ 0
hw : w ≠ 0
heq : -(C u * a ^ p + C v * b ^ q) = C w * c ^ r
hab : IsCoprime (C u * a ^ p) (C v * b ^ q)
hCu : IsUnit (C u)
hCv : IsUnit (C v)
hCw : IsUnit (C w)
⊢ IsCoprime (C v * b ^ q) (C u * a ^ p + C v * b ^ q)

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

Result:
case h.e'_4.h.e'_6
k : Type u_1
inst✝ : Field k
p q r : ℕ
a b c : k[X]
u v w : k
hp : 0 < p
hq : 0 < q
hr : 0 < r
hu : u ≠ 0
hv : v ≠ 0
hw : w ≠ 0
heq : -(C u * a ^ p + C v * b ^ q) = C w * c ^ r
hab : IsCoprime (C u * a ^ p) (C v * b ^ q)
hCu : IsUnit (C u)
hCv : IsUnit (C v)
hCw : IsUnit (C w)
⊢ C v * b ^ q = C v * b ^ q * 1

Proof state:
k : Type u_1
inst✝ : Field k
p q r : ℕ
a b c : k[X]
u v w : k
hp : 0 < p
hq : 0 < q
hr : 0 < r
hu : u ≠ 0
hv : v ≠ 0
hw : w ≠ 0
heq : C u * a ^ p + C v * b ^ q + C w * c ^ r = 0
hab : IsCoprime (C u * a ^ p) (C v * b ^ q)
hCu : IsUnit (C u)
hCv : IsUnit (C v)
hCw : IsUnit (C w)
⊢ IsCoprime b c

Tactic:
rw [add_eq_zero_iff_neg_eq] at heq

Result:
k : Type u_1
inst✝ : Field k
p q r : ℕ
a b c : k[X]
u v w : k
hp : 0 < p
hq : 0 < q
hr : 0 < r
hu : u ≠ 0
hv : v ≠ 0
hw : w ≠ 0
heq : -(C u * a ^ p + C v * b ^ q) = C w * c ^ r
hab : IsCoprime (C u * a ^ p) (C v * b ^ q)
hCu : IsUnit (C u)
hCv : IsUnit (C v)
hCw : IsUnit (C w)
⊢ IsCoprime b c

Proof state:
k : Type u_1
inst✝ : Field k
p q r : ℕ
a b c : k[X]
u v w : k
hp : 0 < p
hq : 0 < q
hr : 0 < r
hu : u ≠ 0
hv : v ≠ 0
hw : w ≠ 0
heq : C u * a ^ p + C v * b ^ q + C w * c ^ r = 0
hab : IsCoprime a b
hCu : IsUnit (C u)
⊢ IsCoprime b c

Tactic:
have hCv : IsUnit (C v) := hv.isUnit_C

Result:
k : Type u_1
inst✝ : Field k
p q r : ℕ
a b c : k[X]
u v w : k
hp : 0 < p
hq : 0 < q
hr : 0 < r
hu : u ≠ 0
hv : v ≠ 0
hw : w ≠ 0
heq : C u * a ^ p + C v * b ^ q + C w * c ^ r = 0
hab : IsCoprime a b
hCu : IsUnit (C u)
hCv : IsUnit (C v)
⊢ IsCoprime b c

Proof state:
k : Type u_1
inst✝ : Field k
p q r : ℕ
a b c : k[X]
u v w : k
hp : 0 < p
hq : 0 < q
hr : 0 < r
hu : u ≠ 0
hv : v ≠ 0
hw : w ≠ 0
heq : C u * a ^ p + C v * b ^ q + C w * c ^ r = 0
hab : IsCoprime a b
⊢ IsCoprime b c

Tactic:
have hCu : IsUnit (C u) := hu.isUnit_C

Result:
k : Type u_1
inst✝ : Field k
p q r : ℕ
a b c : k[X]
u v w : k
hp : 0 < p
hq : 0 < q
hr : 0 < r
hu : u ≠ 0
hv : v ≠ 0
hw : w ≠ 0
heq : C u * a ^ p + C v * b ^ q + C w * c ^ r = 0
hab : IsCoprime a b
hCu : IsUnit (C u)
⊢ IsCoprime b c

Proof state:
case h.e'_4.h.e'_6
k : Type u_1
inst✝ : Field k
p q r : ℕ
a b c : k[X]
u v w : k
hp : 0 < p
hq : 0 < q
hr : 0 < r
hu : u ≠ 0
hv : v ≠ 0
hw : w ≠ 0
heq : -(C u * a ^ p + C v * b ^ q) = C w * c ^ r
hab : IsCoprime (C u * a ^ p) (C v * b ^ q)
hCu : IsUnit (C u)
hCv : IsUnit (C v)
hCw : IsUnit (C w)
⊢ C v * b ^ q = C v * b ^ q * 1

Tactic:
rw [mul_one]

Result:
no goals