-- Mathlib/RingTheory/Polynomial/ScaleRoots.lean
lemma isCoprime_scaleRoots (p q : R[X]) (r : R) (hr : IsUnit r) (h : IsCoprime p q) :
    IsCoprime (p.scaleRoots r) (q.scaleRoots r)

Proof state:
case h
R : Type u_1
inst✝ : CommSemiring R
p q : R[X]
r : R
hr : IsUnit r
a b : R[X]
e : a * p + b * q = 1
s : R := ↑hr.unit⁻¹
this : (a * p).natDegree = (b * q).natDegree
⊢ s ^ (a * p).natDegree • s ^ (a.natDegree + p.natDegree - (a * p).natDegree) • a.scaleRoots r * p.scaleRoots r +
      s ^ (a * p).natDegree • s ^ (b.natDegree + q.natDegree - (b * q).natDegree) • b.scaleRoots r * q.scaleRoots r =
    1

Tactic:
simp only [s, smul_mul_assoc, ← mul_scaleRoots, smul_smul, Units.smul_def, mul_assoc,
  ← mul_pow, IsUnit.val_inv_mul, one_pow, mul_one, ← smul_add, one_smul, e, natDegree_one,
  one_scaleRoots, ← add_scaleRoots_of_natDegree_eq _ _ _ this, tsub_zero]

Result:
no goals

Proof state:
case intro.intro
R : Type u_1
inst✝ : CommSemiring R
p q : R[X]
r : R
hr : IsUnit r
a b : R[X]
e : a * p + b * q = 1
⊢ IsCoprime (p.scaleRoots r) (q.scaleRoots r)

Tactic:
let s : R := ↑hr.unit⁻¹

Result:
case intro.intro
R : Type u_1
inst✝ : CommSemiring R
p q : R[X]
r : R
hr : IsUnit r
a b : R[X]
e : a * p + b * q = 1
s : R := ↑hr.unit⁻¹
⊢ IsCoprime (p.scaleRoots r) (q.scaleRoots r)

Proof state:
case H
R : Type u_1
inst✝ : CommSemiring R
p q : R[X]
r : R
hr : IsUnit r
a b : R[X]
e : a * p + b * q = 1
s : R := ↑hr.unit⁻¹
⊢ (a * p + b * q).natDegree = 0

Tactic:
rw [e, natDegree_one]

Result:
no goals

Proof state:
case intro.intro
R : Type u_1
inst✝ : CommSemiring R
p q : R[X]
r : R
hr : IsUnit r
a b : R[X]
e : a * p + b * q = 1
s : R := ↑hr.unit⁻¹
⊢ IsCoprime (p.scaleRoots r) (q.scaleRoots r)

Tactic:
have : natDegree (a * p) = natDegree (b * q) := by
  apply natDegree_eq_of_natDegree_add_eq_zero
  rw [e, natDegree_one]

Result:
case intro.intro
R : Type u_1
inst✝ : CommSemiring R
p q : R[X]
r : R
hr : IsUnit r
a b : R[X]
e : a * p + b * q = 1
s : R := ↑hr.unit⁻¹
this : (a * p).natDegree = (b * q).natDegree
⊢ IsCoprime (p.scaleRoots r) (q.scaleRoots r)

Proof state:
R : Type u_1
inst✝ : CommSemiring R
p q : R[X]
r : R
hr : IsUnit r
h : IsCoprime p q
⊢ IsCoprime (p.scaleRoots r) (q.scaleRoots r)

Tactic:
obtain ⟨a, b, e⟩ := h

Result:
case intro.intro
R : Type u_1
inst✝ : CommSemiring R
p q : R[X]
r : R
hr : IsUnit r
a b : R[X]
e : a * p + b * q = 1
⊢ IsCoprime (p.scaleRoots r) (q.scaleRoots r)

Proof state:
R : Type u_1
inst✝ : CommSemiring R
p q : R[X]
r : R
hr : IsUnit r
a b : R[X]
e : a * p + b * q = 1
s : R := ↑hr.unit⁻¹
⊢ (a * p).natDegree = (b * q).natDegree

Tactic:
apply natDegree_eq_of_natDegree_add_eq_zero

Result:
case H
R : Type u_1
inst✝ : CommSemiring R
p q : R[X]
r : R
hr : IsUnit r
a b : R[X]
e : a * p + b * q = 1
s : R := ↑hr.unit⁻¹
⊢ (a * p + b * q).natDegree = 0

Proof state:
case h
R : Type u_1
inst✝ : CommSemiring R
p q : R[X]
r : R
hr : IsUnit r
a b : R[X]
e : a * p + b * q = 1
s : R := ↑hr.unit⁻¹
this : (a * p).natDegree = (b * q).natDegree
⊢ ∃ b,
    s ^ (a * p).natDegree • s ^ (a.natDegree + p.natDegree - (a * p).natDegree) • a.scaleRoots r * p.scaleRoots r +
        b * q.scaleRoots r =
      1

Tactic:
use s ^ natDegree (a * p) • s ^ (natDegree b + natDegree q - natDegree (b * q)) • b.scaleRoots r

Result:
case h
R : Type u_1
inst✝ : CommSemiring R
p q : R[X]
r : R
hr : IsUnit r
a b : R[X]
e : a * p + b * q = 1
s : R := ↑hr.unit⁻¹
this : (a * p).natDegree = (b * q).natDegree
⊢ s ^ (a * p).natDegree • s ^ (a.natDegree + p.natDegree - (a * p).natDegree) • a.scaleRoots r * p.scaleRoots r +
      s ^ (a * p).natDegree • s ^ (b.natDegree + q.natDegree - (b * q).natDegree) • b.scaleRoots r * q.scaleRoots r =
    1

Proof state:
case intro.intro
R : Type u_1
inst✝ : CommSemiring R
p q : R[X]
r : R
hr : IsUnit r
a b : R[X]
e : a * p + b * q = 1
s : R := ↑hr.unit⁻¹
this : (a * p).natDegree = (b * q).natDegree
⊢ IsCoprime (p.scaleRoots r) (q.scaleRoots r)

Tactic:
use s ^ natDegree (a * p) • s ^ (natDegree a + natDegree p - natDegree (a * p)) • a.scaleRoots r

Result:
case h
R : Type u_1
inst✝ : CommSemiring R
p q : R[X]
r : R
hr : IsUnit r
a b : R[X]
e : a * p + b * q = 1
s : R := ↑hr.unit⁻¹
this : (a * p).natDegree = (b * q).natDegree
⊢ ∃ b,
    s ^ (a * p).natDegree • s ^ (a.natDegree + p.natDegree - (a * p).natDegree) • a.scaleRoots r * p.scaleRoots r +
        b * q.scaleRoots r =
      1