awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
S : Type u_2
A : Type u_3
inst : Semiring S
inst_1 : Semiring A
p : S[X]
f : S →+* A
a : A
s : S
hsa : Commute ((f : (a : S) → A) s) a
hf : ∀ (s₁ s₂ : S), Commute.{u_3} (S := A) ((f : (a : S) → A) s₁ : A) ((f : (a : S) → A) s₂ : A)
i : ℕ
_hi : i ∈ p.support
simp_rw :
  HMul.hMul (α := A) (β := A) ((f : (a : S) → A) (p.coeff i) : A) ((f : (a : S) → A) (s ^ (p.natDegree - i)) : A) *
      HMul.hMul (α := A) ((f : (a : S) → A) s : A) a ^ i =
    HMul.hMul (α := A) ((f : (a : S) → A) (p.coeff i) : A)
        (HPow.hPow (α := A) ((f : (a : S) → A) s : A) (p.natDegree - i + i)) *
      a ^ i
simp_rw₁ :
  HMul.hMul (α := A) ((f : (a : S) → A) (p.coeff i) : A)
        (HPow.hPow (α := A) ((f : (a : S) → A) s : A) (p.natDegree - i)) *
      HMul.hMul (α := A) ((f : (a : S) → A) s : A) a ^ i =
    HMul.hMul (α := A) ((f : (a : S) → A) (p.coeff i) : A)
        (HPow.hPow (α := A) ((f : (a : S) → A) s : A) (p.natDegree - i + i)) *
      a ^ i
simp_rw₂ :
  HMul.hMul (α := A) ((f : (a : S) → A) (p.coeff i) : A)
        (HPow.hPow (α := A) ((f : (a : S) → A) s : A) (p.natDegree - i)) *
      HMul.hMul (α := A) ((f : (a : S) → A) s : A) a ^ i =
    HMul.hMul (α := A) ((f : (a : S) → A) (p.coeff i) : A)
        (HPow.hPow (α := A) ((f : (a : S) → A) s : A) (p.natDegree - i) *
          HPow.hPow (α := A) ((f : (a : S) → A) s : A) i) *
      a ^ i
simp_rw₃ :
  HMul.hMul (α := A) ((f : (a : S) → A) (p.coeff i) : A)
        (HPow.hPow (α := A) ((f : (a : S) → A) s : A) (p.natDegree - i)) *
      (HPow.hPow (α := A) ((f : (a : S) → A) s : A) i * a ^ i) =
    HMul.hMul (α := A) ((f : (a : S) → A) (p.coeff i) : A)
        (HPow.hPow (α := A) ((f : (a : S) → A) s : A) (p.natDegree - i) *
          HPow.hPow (α := A) ((f : (a : S) → A) s : A) i) *
      a ^ i
⊢ HMul.hMul (α := A) ((f : (a : S) → A) (p.coeff i * s ^ (p.natDegree - i)) : A)
      (HMul.hMul (α := A) ((f : (a : S) → A) s : A) a ^ i) =
    HMul.hMul (α := A) ((f : (a : S) → A) (p.coeff i) : A)
        (HPow.hPow (α := A) ((f : (a : S) → A) s : A) (p.natDegree - i + i)) *
      a ^ i

Tactic:
simp_rw [f.map_mul, f.map_pow, pow_add, hsa.mul_pow, mul_assoc]

Premises used: mul_assoc, pow_add, Commute.mul_pow, RingHom.map_mul, RingHom.map_pow
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
S : Type u_2
A : Type u_3
inst : Semiring S
inst_1 : Semiring A
p : S[X]
f : S →+* A
a : A
s : S
hsa : Commute ((f : (a : S) → A) s) a
hf : ∀ (s₁ s₂ : S), Commute.{u_3} (S := A) ((f : (a : S) → A) s₁ : A) ((f : (a : S) → A) s₂ : A)
i : ℕ
hi : i ∈ p.support
rw : i ≤ p.natDegree
⊢ HMul.hMul (α := A) ((f : (a : S) → A) (p.coeff i) : A)
        (HPow.hPow (α := A) ((f : (a : S) → A) s : A) (p.natDegree - i + i)) *
      a ^ i =
    HPow.hPow (α := A) ((f : (a : S) → A) s : A) p.natDegree *
      HMul.hMul (α := A) ((f : (a : S) → A) (p.coeff i) : A) (a ^ i)

Tactic:
rw [mul_assoc, ← map_pow, (hf _ _).left_comm, map_pow, tsub_add_cancel_of_le]

Premises used: Commute.left_comm, mul_assoc, tsub_add_cancel_of_le, map_pow
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
S : Type u_2
A : Type u_3
inst : Semiring S
inst_1 : Semiring A
p : S[X]
f : S →+* A
a : A
s : S
hsa : Commute ((f : (a : S) → A) s) a
hf : ∀ (s₁ s₂ : S), Commute.{u_3} (S := A) ((f : (a : S) → A) s₁ : A) ((f : (a : S) → A) s₂ : A)
i : ℕ
hi : i ∈ p.support
⊢ i ≤ p.natDegree

Tactic:
le_natDegree_of_ne_zero (Polynomial.mem_support_iff.mp hi)

Premises used: Polynomial.mem_support_iff, Iff.mp, Polynomial.le_natDegree_of_ne_zero
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
S : Type u_2
A : Type u_3
inst : Semiring S
inst_1 : Semiring A
p : S[X]
f : S →+* A
a : A
s : S
hsa : Commute ((f : (a : S) → A) s) a
hf : ∀ (s₁ s₂ : S), Commute.{u_3} (S := A) ((f : (a : S) → A) s₁ : A) ((f : (a : S) → A) s₂ : A)
i : ℕ
hi : i ∈ p.support
⊢ i ≤ p.natDegree

Tactic:
exact le_natDegree_of_ne_zero (Polynomial.mem_support_iff.mp hi)

Premises used: Polynomial.mem_support_iff, Iff.mp, Polynomial.le_natDegree_of_ne_zero
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
S : Type u_2
A : Type u_3
inst : Semiring S
inst_1 : Semiring A
p : S[X]
f : S →+* A
a : A
s : S
hsa : Commute ((f : (a : S) → A) s) a
hf : ∀ (s₁ s₂ : S), Commute.{u_3} (S := A) ((f : (a : S) → A) s₁ : A) ((f : (a : S) → A) s₂ : A)
⊢ ∑ i ∈ p.support,
      HPow.hPow (α := A) ((f : (a : S) → A) s : A) p.natDegree *
        HMul.hMul (α := A) ((f : (a : S) → A) (p.coeff i) : A) (a ^ i) =
    HPow.hPow (α := A) ((f : (a : S) → A) s : A) p.natDegree * eval₂ f a p

Tactic:
simp [← Finset.mul_sum, eval₂_eq_sum, sum_def]

Premises used: Finset.mul_sum, Polynomial.sum_def, Polynomial.eval₂_eq_sum
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
S : Type u_2
A : Type u_3
inst : Semiring S
inst_1 : Semiring A
p : S[X]
f : S →+* A
a : A
s : S
hsa : Commute ((f : (a : S) → A) s) a
hf : ∀ (s₁ s₂ : S), Commute.{u_3} (S := A) ((f : (a : S) → A) s₁ : A) ((f : (a : S) → A) s₂ : A)
_ :
  eval₂ f (HMul.hMul (α := A) ((f : (a : S) → A) s : A) a) (p.scaleRoots s) =
    ∑ i ∈ (p.scaleRoots s).support,
      HMul.hMul (α := A) ((f : (a : S) → A) (p.coeff i * s ^ (p.natDegree - i)) : A)
        (HMul.hMul (α := A) ((f : (a : S) → A) s : A) a ^ i)
_₁ :
  ∑ i ∈ p.support,
      HPow.hPow (α := A) ((f : (a : S) → A) s : A) p.natDegree *
        HMul.hMul (α := A) ((f : (a : S) → A) (p.coeff i) : A) (a ^ i) =
    HPow.hPow (α := A) ((f : (a : S) → A) s : A) p.natDegree * eval₂ f a p
⊢ eval₂ f (HMul.hMul (α := A) ((f : (a : S) → A) s : A) a) (p.scaleRoots s) =
    HPow.hPow (α := A) ((f : (a : S) → A) s : A) p.natDegree * eval₂ f a p

Tactic:
calc
    _ = (scaleRoots p s).support.sum fun i =>
          f (coeff p i * s ^ (p.natDegree - i)) * (f s * a) ^ i := by
      simp [eval₂_eq_sum, sum_def]
    _ = p.support.sum fun i => f (coeff p i * s ^ (p.natDegree - i)) * (f s * a) ^ i :=
      (Finset.sum_subset (support_scaleRoots_le p s) fun i _hi hi' => by
        let this : coeff p i * s ^ (p.natDegree - i) = 0 := by simpa using hi'
        simp [this])
    _ = p.support.sum fun i : ℕ => f (p.coeff i) * f s ^ (p.natDegree - i + i) * a ^ i :=
      (Finset.sum_congr rfl fun i _hi => by
        simp_rw [f.map_mul, f.map_pow, pow_add, hsa.mul_pow, mul_assoc])
    _ = p.support.sum fun i : ℕ => f s ^ p.natDegree * (f (p.coeff i) * a ^ i) :=
      Finset.sum_congr rfl fun i hi => by
        rw [mul_assoc, ← map_pow, (hf _ _).left_comm, map_pow, tsub_add_cancel_of_le]
        exact le_natDegree_of_ne_zero (Polynomial.mem_support_iff.mp hi)
    _ = f s ^ p.natDegree * eval₂ f a p := by simp [← Finset.mul_sum, eval₂_eq_sum, sum_def]

Premises used: HMul.hMul, HSub.hSub, Polynomial.eval₂, Polynomial.coeff, HPow.hPow, HAdd.hAdd, Finset.sum_subset, Polynomial.scaleRoots, Polynomial.natDegree, Polynomial.support_scaleRoots_le, DFunLike.coe, Polynomial.support, Finset.sum_congr, Finset.sum, rfl
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
R : Type u_1
S : Type u_2
inst : Semiring S
inst_1 : CommSemiring R
p : S[X]
f : S →+* R
r : R
s : S
⊢ eval₂ f (HMul.hMul (α := R) ((f : (a : S) → R) s : R) r) (p.scaleRoots s) =
    HPow.hPow (α := R) ((f : (a : S) → R) s : R) p.natDegree * eval₂ f r p

Tactic:
scaleRoots_eval₂_mul_of_commute f r s (mul_comm _ _) fun _ _ ↦ mul_comm _ _

Premises used: Polynomial.scaleRoots_eval₂_mul_of_commute, mul_comm, DFunLike.coe
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
R : Type u_1
S : Type u_2
inst : Semiring S
inst_1 : CommSemiring R
p : S[X]
f : S →+* R
r : R
s : S
hr : eval₂ f r p = 0
rw : HPow.hPow (α := R) ((f : (a : S) → R) s : R) p.natDegree * eval₂ f r p = 0
rw₁ : HPow.hPow (α := R) ((f : (a : S) → R) s : R) p.natDegree * 0 = 0
rw₂ rw₃ : Eq.{u_1 + 1} (α := R) 0 0
⊢ eval₂ f (HMul.hMul (α := R) ((f : (a : S) → R) s : R) r) (p.scaleRoots s) = 0

Tactic:
rw [scaleRoots_eval₂_mul, hr, mul_zero]

Premises used: Polynomial.scaleRoots_eval₂_mul, MulZeroClass.mul_zero
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
R : Type u_1
inst : CommSemiring R
p : R[X]
r s : R
⊢ eval (s * r) (p.scaleRoots s) = s ^ p.natDegree * eval r p

Tactic:
scaleRoots_eval₂_mul _ _ _

Premises used: Polynomial.eval, Polynomial.scaleRoots_eval₂_mul
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
R : Type u_1
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
p : R[X]
a : A
r : R
ha : Eq.{u_3 + 1} (α := A) ((aeval a : (a : R[X]) → A) p : A) (0 : A)
hsa : Commute ((algebraMap R A : (a : R) → A) r) a
hf :
  ∀ (s₁ s₂ : R), Commute.{u_3} (S := A) ((algebraMap R A : (a : R) → A) s₁ : A) ((algebraMap R A : (a : R) → A) s₂ : A)
⊢ Eq.{u_3 + 1} (α := A)
    ((aeval (HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) r : A) a) : (a : R[X]) → A) (p.scaleRoots r) : A)
    (0 : A)

Tactic:
rw [aeval_def, scaleRoots_eval₂_mul_of_commute, ← aeval_def, ha, mul_zero]

Premises used: Polynomial.scaleRoots_eval₂_mul_of_commute, Polynomial.aeval_def, MulZeroClass.mul_zero
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
R : Type u_1
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
p : R[X]
a : A
r : R
ha : Eq.{u_3 + 1} (α := A) ((aeval a : (a : R[X]) → A) p : A) (0 : A)
⊢ Commute ((algebraMap R A : (a : R) → A) r) a

Tactic:
apply Algebra.commutes

Premises used: Algebra.commutes
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
R : Type u_1
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
p : R[X]
a : A
r : R
ha : Eq.{u_3 + 1} (α := A) ((aeval a : (a : R[X]) → A) p : A) (0 : A)
s₁ s₂ : R
hf :
  SemiconjBy.{u_3} (M := A) ((algebraMap R A : (a : R) → A) s₁ : A) ((algebraMap R A : (a : R) → A) s₂ : A)
    ((algebraMap R A : (a : R) → A) s₂ : A)
hf₁ :
  HMul.hMul (α := A) (β := A) ((algebraMap R A : (a : R) → A) s₁ : A) ((algebraMap R A : (a : R) → A) s₂ : A) =
    HMul.hMul (α := A) (β := A) ((algebraMap R A : (a : R) → A) s₂ : A) ((algebraMap R A : (a : R) → A) s₁ : A)
hf₂ :
  (algebraMap R A : (a : R) → A) (s₁ * s₂) =
    HMul.hMul (α := A) (β := A) ((algebraMap R A : (a : R) → A) s₂ : A) ((algebraMap R A : (a : R) → A) s₁ : A)
hf₃ :
  Eq.{u_3 + 1} (α := A) ((algebraMap R A : (a : R) → A) (s₁ * s₂) : A) ((algebraMap R A : (a : R) → A) (s₂ * s₁) : A)
hf₄ hf₅ :
  Eq.{u_3 + 1} (α := A) ((algebraMap R A : (a : R) → A) (s₂ * s₁) : A) ((algebraMap R A : (a : R) → A) (s₂ * s₁) : A)
⊢ Commute.{u_3} (S := A) ((algebraMap R A : (a : R) → A) s₁ : A) ((algebraMap R A : (a : R) → A) s₂ : A)

Tactic:
rw [Commute, SemiconjBy, ← map_mul, ← map_mul, mul_comm]

Premises used: SemiconjBy, Commute, map_mul, mul_comm
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
S : Type u_2
K : Type u_4
inst : Semiring S
inst_1 : Field K
p : S[X]
f : S →+* K
hf : Function.Injective.{u_2 + 1, u_4 + 1} (α := S) (β := K) (⇑f : (a : S) → K)
r s : S
hr : eval₂ f (HDiv.hDiv (α := K) (β := K) ((f : (a : S) → K) r : K) ((f : (a : S) → K) s : K)) p = 0
hs : Membership.mem (γ := Submonoid S) (nonZeroDivisors S) s
⊢ Nontrivial S

Tactic:
nontriviality S using Subsingleton.eq_zero (_ : S)
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
S : Type u_2
K : Type u_4
inst : Semiring S
inst_1 : Field K
p : S[X]
f : S →+* K
hf : Function.Injective.{u_2 + 1, u_4 + 1} (α := S) (β := K) (⇑f : (a : S) → K)
r s : S
hr : eval₂ f (HDiv.hDiv (α := K) (β := K) ((f : (a : S) → K) r : K) ((f : (a : S) → K) s : K)) p = 0
hs : Membership.mem (γ := Submonoid S) (nonZeroDivisors S) s
h : Nontrivial S
⊢ eval₂ f
      (HMul.hMul (α := K) ((f : (a : S) → K) s : K)
        (HDiv.hDiv (α := K) (β := K) ((f : (a : S) → K) r : K) ((f : (a : S) → K) s : K)))
      (p.scaleRoots s) =
    0

Tactic:
@scaleRoots_eval₂_eq_zero _ _ _ _ p f _ s hr

Premises used: Polynomial.scaleRoots_eval₂_eq_zero
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
S : Type u_2
K : Type u_4
inst : Semiring S
inst_1 : Field K
p : S[X]
f : S →+* K
hf : Function.Injective.{u_2 + 1, u_4 + 1} (α := S) (β := K) (⇑f : (a : S) → K)
r s : S
hr : eval₂ f (HDiv.hDiv (α := K) (β := K) ((f : (a : S) → K) r : K) ((f : (a : S) → K) s : K)) p = 0
hs : Membership.mem (γ := Submonoid S) (nonZeroDivisors S) s
h_1 : Nontrivial S
h :
  (f : (a : S) → K) r =
    HMul.hMul (α := K) ((f : (a : S) → K) s : K)
      (HDiv.hDiv (α := K) (β := K) ((f : (a : S) → K) r : K) ((f : (a : S) → K) s : K))
⊢ eval₂ f ((f : (a : S) → K) r) (p.scaleRoots s) = 0

Tactic:
convert! @scaleRoots_eval₂_eq_zero _ _ _ _ p f _ s hr

Premises used: Polynomial.scaleRoots_eval₂_eq_zero
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
S : Type u_2
K : Type u_4
inst : Semiring S
inst_1 : Field K
p : S[X]
f : S →+* K
hf : Function.Injective.{u_2 + 1, u_4 + 1} (α := S) (β := K) (⇑f : (a : S) → K)
r s : S
hr : eval₂ f (HDiv.hDiv (α := K) (β := K) ((f : (a : S) → K) r : K) ((f : (a : S) → K) s : K)) p = 0
hs : Membership.mem (γ := Submonoid S) (nonZeroDivisors S) s
h_1 : Nontrivial S
h : Ne.{u_4 + 1} (α := K) ((f : (a : S) → K) s : K) (0 : K)
⊢ (f : (a : S) → K) r =
    HMul.hMul (α := K) ((f : (a : S) → K) s : K)
      (HDiv.hDiv (α := K) (β := K) ((f : (a : S) → K) r : K) ((f : (a : S) → K) s : K))

Tactic:
rw [← mul_div_assoc, mul_comm, mul_div_cancel_right₀]

Premises used: mul_div_assoc, mul_div_cancel_right₀, mul_comm
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
S : Type u_2
K : Type u_4
inst : Semiring S
inst_1 : Field K
p : S[X]
f : S →+* K
hf : Function.Injective.{u_2 + 1, u_4 + 1} (α := S) (β := K) (⇑f : (a : S) → K)
r s : S
hr : eval₂ f (HDiv.hDiv (α := K) (β := K) ((f : (a : S) → K) r : K) ((f : (a : S) → K) s : K)) p = 0
hs : Membership.mem (γ := Submonoid S) (nonZeroDivisors S) s
h : Nontrivial S
⊢ Ne.{u_4 + 1} (α := K) ((f : (a : S) → K) s : K) (0 : K)

Tactic:
map_ne_zero_of_mem_nonZeroDivisors _ hf hs

Premises used: map_ne_zero_of_mem_nonZeroDivisors
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
S : Type u_2
K : Type u_4
inst : Semiring S
inst_1 : Field K
p : S[X]
f : S →+* K
hf : Function.Injective.{u_2 + 1, u_4 + 1} (α := S) (β := K) (⇑f : (a : S) → K)
r s : S
hr : eval₂ f (HDiv.hDiv (α := K) (β := K) ((f : (a : S) → K) r : K) ((f : (a : S) → K) s : K)) p = 0
hs : Membership.mem (γ := Submonoid S) (nonZeroDivisors S) s
h : Nontrivial S
⊢ Ne.{u_4 + 1} (α := K) ((f : (a : S) → K) s : K) (0 : K)

Tactic:
exact map_ne_zero_of_mem_nonZeroDivisors _ hf hs

Premises used: map_ne_zero_of_mem_nonZeroDivisors
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
R : Type u_1
K : Type u_4
inst : CommSemiring R
inst_1 : Field K
inst_2 : Algebra R K
inj : Function.Injective.{u_1 + 1, u_4 + 1} (α := R) (β := K) (⇑(algebraMap R K) : (a : R) → K)
p : R[X]
r s : R
hr :
  Eq.{u_4 + 1} (α := K)
    ((aeval
            (HDiv.hDiv (α := K) (β := K) ((algebraMap R K : (a : R) → K) r : K)
              ((algebraMap R K : (a : R) → K) s : K)) :
          (a : R[X]) → K)
        p :
      K)
    (0 : K)
hs : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) s
⊢ Eq.{u_4 + 1} (α := K)
    (((aeval ((algebraMap R K : (a : R) → K) r) : R[X] →ₐ[R] K) : (a : R[X]) → K) (p.scaleRoots s) : K) (0 : K)

Tactic:
scaleRoots_eval₂_eq_zero_of_eval₂_div_eq_zero inj hr hs

Premises used: Polynomial.scaleRoots_eval₂_eq_zero_of_eval₂_div_eq_zero, MonoidHomClass.toMonoidHom, RingHomClass.toRingHom
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
R : Type u_1
inst : CommSemiring R
p : R[X]
r s : R
a : ∀ (n : ℕ), (p.scaleRoots (r * s)).coeff n = ((p.scaleRoots r).scaleRoots s).coeff n
⊢ p.scaleRoots (r * s) = (p.scaleRoots r).scaleRoots s

Tactic:
ext
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
R : Type u_1
inst : CommSemiring R
p : R[X]
r s : R
n : ℕ
⊢ (p.scaleRoots (r * s)).coeff n = ((p.scaleRoots r).scaleRoots s).coeff n

Tactic:
simp [mul_pow, mul_assoc]

Premises used: mul_assoc, mul_pow
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
R : Type u_1
inst : CommSemiring R
p q : R[X]
r : R
a :
  ∀ (n : ℕ),
    (r ^ (p.natDegree + q.natDegree - (p * q).natDegree) • (p * q).scaleRoots r).coeff n =
      (p.scaleRoots r * q.scaleRoots r).coeff n
⊢ r ^ (p.natDegree + q.natDegree - (p * q).natDegree) • (p * q).scaleRoots r = p.scaleRoots r * q.scaleRoots r

Tactic:
ext n
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
R : Type u_1
inst : CommSemiring R
p q : R[X]
r : R
n : ℕ
a :
  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
⊢ (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]

Premises used: Polynomial.coeff_scaleRoots, Polynomial.coeff_smul, smul_eq_mul
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
R : Type u_1
inst : CommSemiring R
p q : R[X]
r : R
n : ℕ
trans :
  r ^ (p.natDegree + q.natDegree - (p * q).natDegree) * ((p * q).coeff n * r ^ ((p * q).natDegree - n)) =
    (∑ x ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ n, p.coeff x.1 * q.coeff x.2) *
      r ^ (p.natDegree + q.natDegree - n)
trans₁ :
  (∑ x ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ n, p.coeff x.1 * q.coeff x.2) *
      r ^ (p.natDegree + q.natDegree - n) =
    (p.scaleRoots r * q.scaleRoots r).coeff 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)

Premises used: HMul.hMul, HSub.hSub, Prod.fst, Polynomial.coeff, HAdd.hAdd, Polynomial.natDegree, Prod.snd, Finset.HasAntidiagonal.antidiagonal, Finset.sum
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
R : Type u_1
inst : CommSemiring R
p q : R[X]
r : R
n : ℕ
rw :
  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)
⊢ r ^ (p.natDegree + q.natDegree - (p * q).natDegree) * ((p * q).coeff n * r ^ ((p * q).natDegree - n)) =
    (∑ x ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ n, p.coeff x.1 * q.coeff x.2) *
      r ^ (p.natDegree + q.natDegree - n)

Tactic:
rw [← coeff_mul]

Premises used: Polynomial.coeff_mul
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
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]

Premises used: MulZeroClass.zero_mul, MulZeroClass.mul_zero, Polynomial.coeff_eq_zero_of_natDegree_lt
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
R : Type u_1
inst : CommSemiring R
p q : R[X]
r : R
n : ℕ
h : n ≤ (p * q).natDegree
inr :
  (p * q).coeff n * r ^ ((p * q).natDegree - n) * r ^ (p.natDegree + q.natDegree - (p * q).natDegree) =
    (p * q).coeff n * r ^ (p.natDegree + q.natDegree - n)
inr₁ :
  (p * q).coeff n * (r ^ ((p * q).natDegree - n) * r ^ (p.natDegree + q.natDegree - (p * q).natDegree)) =
    (p * q).coeff n * r ^ (p.natDegree + q.natDegree - n)
inr₂ :
  (p * q).coeff n * r ^ ((p * q).natDegree - n + (p.natDegree + q.natDegree - (p * q).natDegree)) =
    (p * q).coeff n * r ^ (p.natDegree + q.natDegree - n)
inr₃ :
  (p * q).coeff n * r ^ (p.natDegree + q.natDegree - (p * q).natDegree + ((p * q).natDegree - n)) =
    (p * q).coeff n * r ^ (p.natDegree + q.natDegree - n)
inr₄ inr₅ :
  (p * q).coeff n * r ^ (p.natDegree + q.natDegree - n) = (p * q).coeff n * r ^ (p.natDegree + 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:
rw [mul_comm, mul_assoc, ← pow_add, add_comm, tsub_add_tsub_cancel natDegree_mul_le h]

Premises used: mul_assoc, pow_add, add_comm, mul_comm, Polynomial.natDegree_mul_le, tsub_add_tsub_cancel
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
R : Type u_1
inst : CommSemiring R
p q : R[X]
r : R
n : ℕ
⊢ (p * q).natDegree < n ∨ n ≤ (p * q).natDegree

Tactic:
cases lt_or_ge (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]

Premises used: HMul.hMul, MulZeroClass.zero_mul, mul_assoc, pow_add, add_comm, MulZeroClass.mul_zero, mul_comm, lt_or_ge, Polynomial.natDegree
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
R : Type u_1
inst : CommSemiring R
p q : R[X]
r : R
n : ℕ
rw :
  Eq.{u_1 + 1} (α := R)
    (∑ i ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ n,
      p.coeff i.1 * q.coeff i.2 * r ^ (p.natDegree + q.natDegree - n))
    (∑ x ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ n, (p.scaleRoots r).coeff x.1 * (q.scaleRoots r).coeff x.2)
⊢ (∑ x ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ 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]

Premises used: Polynomial.coeff_mul, Finset.sum_mul
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
R : Type u_1
inst : CommSemiring R
p q : R[X]
r : R
n : ℕ
apply :
  ∀ x ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ 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
⊢ Eq.{u_1 + 1} (α := R)
    (∑ i ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ n,
      p.coeff i.1 * q.coeff i.2 * r ^ (p.natDegree + q.natDegree - n))
    (∑ x ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ n, (p.scaleRoots r).coeff x.1 * (q.scaleRoots r).coeff x.2)

Tactic:
apply Finset.sum_congr rfl

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
R : Type u_1
inst : CommSemiring R
p q : R[X]
r : R
n : ℕ
simp :
  ∀ (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))
⊢ ∀ x ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ 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]

Premises used: Polynomial.coeff_scaleRoots, Finset.HasAntidiagonal.mem_antidiagonal, Prod.forall
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
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]

Premises used: MulZeroClass.zero_mul, Polynomial.coeff_eq_zero_of_natDegree_lt
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
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]

Premises used: MulZeroClass.zero_mul, MulZeroClass.mul_zero, Polynomial.coeff_eq_zero_of_natDegree_lt
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
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
inr :
  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)))
⊢ 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 [← e, mul_assoc, mul_comm (r ^ (_ - a)), ← pow_add]

Premises used: mul_assoc, HSub.hSub, pow_add, HPow.hPow, mul_comm