-- Mathlib/RingTheory/Polynomial/ScaleRoots.lean
/-- Multiplication and `scaleRoots` commute up to a power of `r`. The factor disappears if we
assume that the product of the leading coeffs does not vanish. See `Polynomial.mul_scaleRoots'`. -/
lemma mul_scaleRoots (p q : R[X]) (r : R) :
    r ^ (natDegree p + natDegree q - natDegree (p * q)) • (p * q).scaleRoots r =
      p.scaleRoots r * q.scaleRoots r

Proof state:
case inl
R : Type u_1
inst✝ : CommSemiring R
p q : R[X]
r : R
n : ℕ
h : (p * q).natDegree < n
⊢ r ^ (p.natDegree + q.natDegree - (p * q).natDegree) * ((p * q).coeff n * r ^ ((p * q).natDegree - n)) =
    (p * q).coeff n * r ^ (p.natDegree + q.natDegree - n)

Tactic:
simp only [coeff_eq_zero_of_natDegree_lt h, zero_mul, mul_zero]

Result:
no goals

Proof state:
case a
R : Type u_1
inst✝ : CommSemiring R
p q : R[X]
r : R
n : ℕ
⊢ r ^ (p.natDegree + q.natDegree - (p * q).natDegree) * ((p * q).coeff n * r ^ ((p * q).natDegree - n)) =
    (p.scaleRoots r * q.scaleRoots r).coeff n

Tactic:
trans (∑ x ∈ Finset.antidiagonal n, coeff p x.1 * coeff q x.2) *
  r ^ (natDegree p + natDegree q - n)

Result:
R : Type u_1
inst✝ : CommSemiring R
p q : R[X]
r : R
n : ℕ
⊢ r ^ (p.natDegree + q.natDegree - (p * q).natDegree) * ((p * q).coeff n * r ^ ((p * q).natDegree - n)) =
    (∑ x ∈ Finset.antidiagonal n, p.coeff x.1 * q.coeff x.2) * r ^ (p.natDegree + q.natDegree - n)

R : Type u_1
inst✝ : CommSemiring R
p q : R[X]
r : R
n : ℕ
⊢ (∑ x ∈ Finset.antidiagonal n, p.coeff x.1 * q.coeff x.2) * r ^ (p.natDegree + q.natDegree - n) =
    (p.scaleRoots r * q.scaleRoots r).coeff n

Proof state:
case inr
R : Type u_1
inst✝ : CommSemiring R
p q : R[X]
r : R
n : ℕ
h : n ≤ (p * q).natDegree
⊢ r ^ (p.natDegree + q.natDegree - (p * q).natDegree) * ((p * q).coeff n * r ^ ((p * q).natDegree - n)) =
    (p * q).coeff n * r ^ (p.natDegree + q.natDegree - n)

Tactic:
rw [mul_comm, mul_assoc, ← pow_add, add_comm, tsub_add_tsub_cancel natDegree_mul_le h]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommSemiring R
p q : R[X]
r : R
n : ℕ
⊢ ∀ (a b : ℕ),
    a + b = n →
      p.coeff a * q.coeff b * r ^ (p.natDegree + q.natDegree - n) =
        p.coeff a * r ^ (p.natDegree - a) * (q.coeff b * r ^ (q.natDegree - b))

Tactic:
intros a b e

Result:
R : Type u_1
inst✝ : CommSemiring R
p q : R[X]
r : R
n a b : ℕ
e : a + b = n
⊢ p.coeff a * q.coeff b * r ^ (p.natDegree + q.natDegree - n) =
    p.coeff a * r ^ (p.natDegree - a) * (q.coeff b * r ^ (q.natDegree - b))

Proof state:
case a
R : Type u_1
inst✝ : CommSemiring R
p q : R[X]
r : R
n : ℕ
⊢ (r ^ (p.natDegree + q.natDegree - (p * q).natDegree) • (p * q).scaleRoots r).coeff n =
    (p.scaleRoots r * q.scaleRoots r).coeff n

Tactic:
simp only [coeff_scaleRoots, coeff_smul, smul_eq_mul]

Result:
case a
R : Type u_1
inst✝ : CommSemiring R
p q : R[X]
r : R
n : ℕ
⊢ r ^ (p.natDegree + q.natDegree - (p * q).natDegree) * ((p * q).coeff n * r ^ ((p * q).natDegree - n)) =
    (p.scaleRoots r * q.scaleRoots r).coeff n

Proof state:
R : Type u_1
inst✝ : CommSemiring R
p q : R[X]
r : R
n a b : ℕ
e : a + b = n
⊢ p.coeff a * q.coeff b * r ^ (p.natDegree + q.natDegree - n) =
    p.coeff a * r ^ (p.natDegree - a) * (q.coeff b * r ^ (q.natDegree - b))

Tactic:
cases lt_or_le (natDegree p) a with
| inl h => simp only [coeff_eq_zero_of_natDegree_lt h, zero_mul, mul_zero]
| inr ha =>
  cases lt_or_le (natDegree q) b with
  | inl h => simp only [coeff_eq_zero_of_natDegree_lt h, zero_mul, mul_zero]
  | inr hb =>
    simp only [← e, mul_assoc, mul_comm (r ^ (_ - a)), ← pow_add]
    rw [add_comm (_ - _), tsub_add_tsub_comm ha hb]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommSemiring R
p q : R[X]
r : R
n : ℕ
⊢ (∑ x ∈ Finset.antidiagonal n, p.coeff x.1 * q.coeff x.2) * r ^ (p.natDegree + q.natDegree - n) =
    (p.scaleRoots r * q.scaleRoots r).coeff n

Tactic:
rw [coeff_mul, Finset.sum_mul]

Result:
R : Type u_1
inst✝ : CommSemiring R
p q : R[X]
r : R
n : ℕ
⊢ ∑ i ∈ Finset.antidiagonal n, p.coeff i.1 * q.coeff i.2 * r ^ (p.natDegree + q.natDegree - n) =
    ∑ x ∈ Finset.antidiagonal n, (p.scaleRoots r).coeff x.1 * (q.scaleRoots r).coeff x.2

Proof state:
R : Type u_1
inst✝ : CommSemiring R
p q : R[X]
r : R
n : ℕ
⊢ ∑ i ∈ Finset.antidiagonal n, p.coeff i.1 * q.coeff i.2 * r ^ (p.natDegree + q.natDegree - n) =
    ∑ x ∈ Finset.antidiagonal n, (p.scaleRoots r).coeff x.1 * (q.scaleRoots r).coeff x.2

Tactic:
apply Finset.sum_congr rfl

Result:
R : Type u_1
inst✝ : CommSemiring R
p q : R[X]
r : R
n : ℕ
⊢ ∀ x ∈ Finset.antidiagonal n,
    p.coeff x.1 * q.coeff x.2 * r ^ (p.natDegree + q.natDegree - n) =
      (p.scaleRoots r).coeff x.1 * (q.scaleRoots r).coeff x.2

Proof state:
R : Type u_1
inst✝ : CommSemiring R
p q : R[X]
r : R
n : ℕ
⊢ r ^ (p.natDegree + q.natDegree - (p * q).natDegree) * ((p * q).coeff n * r ^ ((p * q).natDegree - n)) =
    (∑ x ∈ Finset.antidiagonal n, p.coeff x.1 * q.coeff x.2) * r ^ (p.natDegree + q.natDegree - n)

Tactic:
rw [← coeff_mul]

Result:
R : Type u_1
inst✝ : CommSemiring R
p q : R[X]
r : R
n : ℕ
⊢ r ^ (p.natDegree + q.natDegree - (p * q).natDegree) * ((p * q).coeff n * r ^ ((p * q).natDegree - n)) =
    (p * q).coeff n * r ^ (p.natDegree + q.natDegree - n)

Proof state:
case inr.inr
R : Type u_1
inst✝ : CommSemiring R
p q : R[X]
r : R
n a b : ℕ
e : a + b = n
ha : a ≤ p.natDegree
hb : b ≤ q.natDegree
⊢ p.coeff a * (q.coeff b * r ^ (p.natDegree + q.natDegree - (a + b))) =
    p.coeff a * (q.coeff b * r ^ (q.natDegree - b + (p.natDegree - a)))

Tactic:
rw [add_comm (_ - _), tsub_add_tsub_comm ha hb]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommSemiring R
p q : R[X]
r : R
n : ℕ
⊢ r ^ (p.natDegree + q.natDegree - (p * q).natDegree) * ((p * q).coeff n * r ^ ((p * q).natDegree - n)) =
    (p * q).coeff n * r ^ (p.natDegree + q.natDegree - n)

Tactic:
cases lt_or_le (natDegree (p * q)) n with
| inl h => simp only [coeff_eq_zero_of_natDegree_lt h, zero_mul, mul_zero]
| inr h =>
  rw [mul_comm, mul_assoc, ← pow_add, add_comm, tsub_add_tsub_cancel natDegree_mul_le h]

Result:
no goals

Proof state:
case inr.inl
R : Type u_1
inst✝ : CommSemiring R
p q : R[X]
r : R
n a b : ℕ
e : a + b = n
ha : a ≤ p.natDegree
h : q.natDegree < b
⊢ p.coeff a * q.coeff b * r ^ (p.natDegree + q.natDegree - n) =
    p.coeff a * r ^ (p.natDegree - a) * (q.coeff b * r ^ (q.natDegree - b))

Tactic:
simp only [coeff_eq_zero_of_natDegree_lt h, zero_mul, mul_zero]

Result:
no goals

Proof state:
case inl
R : Type u_1
inst✝ : CommSemiring R
p q : R[X]
r : R
n a b : ℕ
e : a + b = n
h : p.natDegree < a
⊢ p.coeff a * q.coeff b * r ^ (p.natDegree + q.natDegree - n) =
    p.coeff a * r ^ (p.natDegree - a) * (q.coeff b * r ^ (q.natDegree - b))

Tactic:
simp only [coeff_eq_zero_of_natDegree_lt h, zero_mul, mul_zero]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommSemiring R
p q : R[X]
r : R
⊢ r ^ (p.natDegree + q.natDegree - (p * q).natDegree) • (p * q).scaleRoots r = p.scaleRoots r * q.scaleRoots r

Tactic:
ext n

Result:
case a
R : Type u_1
inst✝ : CommSemiring R
p q : R[X]
r : R
n : ℕ
⊢ (r ^ (p.natDegree + q.natDegree - (p * q).natDegree) • (p * q).scaleRoots r).coeff n =
    (p.scaleRoots r * q.scaleRoots r).coeff n

Proof state:
R : Type u_1
inst✝ : CommSemiring R
p q : R[X]
r : R
n : ℕ
⊢ ∀ x ∈ Finset.antidiagonal n,
    p.coeff x.1 * q.coeff x.2 * r ^ (p.natDegree + q.natDegree - n) =
      (p.scaleRoots r).coeff x.1 * (q.scaleRoots r).coeff x.2

Tactic:
simp only [Finset.mem_antidiagonal, coeff_scaleRoots, Prod.forall]

Result:
R : Type u_1
inst✝ : CommSemiring R
p q : R[X]
r : R
n : ℕ
⊢ ∀ (a b : ℕ),
    a + b = n →
      p.coeff a * q.coeff b * r ^ (p.natDegree + q.natDegree - n) =
        p.coeff a * r ^ (p.natDegree - a) * (q.coeff b * r ^ (q.natDegree - b))