awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (goal)
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) =
    HPow.hPow (α := A) ((f : (a : S) → A) s : A) p.natDegree * eval₂ f a p
have _ : 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)
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]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (goal)
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)
⊢ 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
have _₁ : ∑ 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: 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]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (goal)
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
⊢ eval₂ f (HMul.hMul (α := R) ((f : (a : S) → R) s : R) r) (p.scaleRoots s) = 0
have rw : HPow.hPow (α := R) ((f : (a : S) → R) s : R) p.natDegree * eval₂ f r p = 0
Tactic: rw [scaleRoots_eval₂_mul, hr, mul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (goal)
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
⊢ eval₂ f (HMul.hMul (α := R) ((f : (a : S) → R) s : R) r) (p.scaleRoots s) = 0
have rw₁ : HPow.hPow (α := R) ((f : (a : S) → R) s : R) p.natDegree * 0 = 0
Tactic: rw [scaleRoots_eval₂_mul, hr, mul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (goal)
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
⊢ eval₂ f (HMul.hMul (α := R) ((f : (a : S) → R) s : R) r) (p.scaleRoots s) = 0
have rw₂ : Eq.{u_1 + 1} (α := R) 0 0
Tactic: rw [scaleRoots_eval₂_mul, hr, mul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (goal)
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)
⊢ 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)
have hsa : Commute ((algebraMap R A : (a : R) → A) r) a
Tactic: rw [aeval_def, scaleRoots_eval₂_mul_of_commute, ← aeval_def, ha, mul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (goal)
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
⊢ 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)
have 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)
Tactic: rw [aeval_def, scaleRoots_eval₂_mul_of_commute, ← aeval_def, ha, mul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (goal)
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
⊢ Commute.{u_3} (S := A) ((algebraMap R A : (a : R) → A) s₁ : A) ((algebraMap R A : (a : R) → A) s₂ : A)
have 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)
Tactic: rw [Commute, SemiconjBy, ← map_mul, ← map_mul, mul_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (goal)
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)
⊢ Commute.{u_3} (S := A) ((algebraMap R A : (a : R) → A) s₁ : A) ((algebraMap R A : (a : R) → A) s₂ : A)
have 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)
Tactic: rw [Commute, SemiconjBy, ← map_mul, ← map_mul, mul_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (goal)
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)
⊢ Commute.{u_3} (S := A) ((algebraMap R A : (a : R) → A) s₁ : A) ((algebraMap R A : (a : R) → A) s₂ : A)
have 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)
Tactic: rw [Commute, SemiconjBy, ← map_mul, ← map_mul, mul_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (goal)
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)
⊢ Commute.{u_3} (S := A) ((algebraMap R A : (a : R) → A) s₁ : A) ((algebraMap R A : (a : R) → A) s₂ : A)
have hf₃ : Eq.{u_3 + 1} (α := A) ((algebraMap R A : (a : R) → A) (s₁ * s₂) : A) ((algebraMap R A : (a : R) → A) (s₂ * s₁) : A)
Tactic: rw [Commute, SemiconjBy, ← map_mul, ← map_mul, mul_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (goal)
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)
⊢ Commute.{u_3} (S := A) ((algebraMap R A : (a : R) → A) s₁ : A) ((algebraMap R A : (a : R) → A) s₂ : A)
have hf₄ : Eq.{u_3 + 1} (α := A) ((algebraMap R A : (a : R) → A) (s₂ * s₁) : A) ((algebraMap R A : (a : R) → A) (s₂ * s₁) : A)
Tactic: rw [Commute, SemiconjBy, ← map_mul, ← map_mul, mul_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (hypothesis)
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
⊢ eval₂ f ((f : (a : S) → K) r) (p.scaleRoots s) = 0
have a : Nontrivial S
Tactic: nontriviality S using Subsingleton.eq_zero (_ : S)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (goal)
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 ((f : (a : S) → K) r) (p.scaleRoots s) = 0
have 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))
Tactic: convert! @scaleRoots_eval₂_eq_zero _ _ _ _ p f _ s hr
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (goal)
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
⊢ (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))
have h : Ne.{u_4 + 1} (α := K) ((f : (a : S) → K) s : K) (0 : K)
Tactic: rw [← mul_div_assoc, mul_comm, mul_div_cancel_right₀]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (goal)
Goal:
R : Type u_1
inst : CommSemiring R
p : R[X]
r s : R
⊢ p.scaleRoots (r * s) = (p.scaleRoots r).scaleRoots s
have a : ∀ (n : ℕ), (p.scaleRoots (r * s)).coeff n = ((p.scaleRoots r).scaleRoots s).coeff n
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (goal)
Goal:
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
have a : ∀ (n : ℕ),
  (r ^ (p.natDegree + q.natDegree - (p * q).natDegree) • (p * q).scaleRoots r).coeff n =
    (p.scaleRoots r * q.scaleRoots r).coeff n
Tactic: ext n
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (goal)
Goal:
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
have 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
Tactic: simp only [coeff_scaleRoots, coeff_smul, smul_eq_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (goal)
Goal:
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
have 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)
Tactic: trans (∑ x ∈ Finset.antidiagonal n, coeff p x.1 * coeff q x.2) *
    r ^ (natDegree p + natDegree q - n)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (goal)
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)
⊢ 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
have 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
Tactic: trans (∑ x ∈ Finset.antidiagonal n, coeff p x.1 * coeff q x.2) *
    r ^ (natDegree p + natDegree q - n)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (goal)
Goal:
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 _ Nat.instAddMonoid _ n, p.coeff x.1 * q.coeff x.2) *
      r ^ (p.natDegree + q.natDegree - n)
have 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)
Tactic: rw [← coeff_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (goal)
Goal:
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)
have 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)
Tactic: rw [mul_comm, mul_assoc, ← pow_add, add_comm, tsub_add_tsub_cancel natDegree_mul_le h]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (goal)
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)
⊢ 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)
have 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)
Tactic: rw [mul_comm, mul_assoc, ← pow_add, add_comm, tsub_add_tsub_cancel natDegree_mul_le h]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (goal)
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)
⊢ 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)
have 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)
Tactic: rw [mul_comm, mul_assoc, ← pow_add, add_comm, tsub_add_tsub_cancel natDegree_mul_le h]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (goal)
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)
⊢ 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)
have 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)
Tactic: rw [mul_comm, mul_assoc, ← pow_add, add_comm, tsub_add_tsub_cancel natDegree_mul_le h]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (goal)
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)
⊢ 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)
have inr₄ : (p * q).coeff n * r ^ (p.natDegree + 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]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (hypothesis)
Goal:
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)
have x : (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]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (goal)
Goal:
R : Type u_1
inst : CommSemiring R
p q : R[X]
r : R
n : ℕ
⊢ (∑ 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
have 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)
Tactic: rw [coeff_mul, Finset.sum_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (goal)
Goal:
R : Type u_1
inst : CommSemiring R
p q : R[X]
r : R
n : ℕ
⊢ 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)
have 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
Tactic: apply Finset.sum_congr rfl
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (goal)
Goal:
R : Type u_1
inst : CommSemiring R
p q : R[X]
r : R
n : ℕ
⊢ ∀ 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
have 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))
Tactic: simp only [Finset.mem_antidiagonal, coeff_scaleRoots, Prod.forall]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (goal)
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
⊢ 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))
have 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)))
Tactic: simp only [← e, mul_assoc, mul_comm (r ^ (_ - a)), ← pow_add]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (goal)
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
⊢ 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)))
have inr : p.coeff a * (q.coeff b * r ^ (p.natDegree + q.natDegree - (a + b))) =
  p.coeff a * (q.coeff b * r ^ (p.natDegree - a + (q.natDegree - b)))
Tactic: rw [add_comm (_ - _), tsub_add_tsub_comm ha hb]