awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
hf : f.natDegree = 3
e : Fin (f.natDegree - 1 + f.natDegree) ≃ Fin 5 := finCongr ⋯
⊢ Matrix.det (n := Fin 5)
        !![f.coeff 0, 0, 1 * f.coeff 1, 0, 0;
          f.coeff 1, f.coeff 0, 2 * f.coeff 2, 1 * f.coeff 1, 0;
          f.coeff 2, f.coeff 1, 3 * f.coeff 3, 2 * f.coeff 2, 1 * f.coeff 1;
          f.coeff 3, f.coeff 2, 0, 3 * f.coeff 3, 2 * f.coeff 2;
          0, 1, 0, 0, 3] *
      HPow.hPow (α := R) (-1) (f.natDegree * (f.natDegree - 1) / 2) =
    HPow.hPow (β := ℕ) (f.coeff 2) 2 * HPow.hPow (β := ℕ) (f.coeff 1) 2 -
            4 * f.coeff 3 * HPow.hPow (β := ℕ) (f.coeff 1) 3 -
          4 * HPow.hPow (β := ℕ) (f.coeff 2) 3 * f.coeff 0 -
        27 * HPow.hPow (β := ℕ) (f.coeff 3) 2 * HPow.hPow (β := ℕ) (f.coeff 0) 2 +
      18 * f.coeff 3 * f.coeff 2 * f.coeff 1 * f.coeff 0
have simp : (f.coeff 0 *
        (f.coeff 0 * (3 * f.coeff 3 * (3 * f.coeff 3) * 3) +
            -(2 * f.coeff 2 *
                (f.coeff 1 * (3 * f.coeff 3) * 3 - 2 * f.coeff 2 * f.coeff 2 * 3 + 2 * f.coeff 2 * (2 * f.coeff 2) -
                  f.coeff 1 * (3 * f.coeff 3))) +
          f.coeff 1 * (-(3 * f.coeff 3 * f.coeff 2 * 3) + 3 * f.coeff 3 * (2 * f.coeff 2))) +
      f.coeff 1 *
        (f.coeff 1 *
              (f.coeff 1 * (3 * f.coeff 3) * 3 - 2 * f.coeff 2 * f.coeff 2 * 3 + 2 * f.coeff 2 * (2 * f.coeff 2) -
                f.coeff 1 * (3 * f.coeff 3)) +
            -(f.coeff 0 * (f.coeff 2 * (3 * f.coeff 3) * 3 - 2 * f.coeff 2 * f.coeff 3 * 3)) +
          f.coeff 1 *
            (f.coeff 2 * f.coeff 2 * 3 - f.coeff 2 * (2 * f.coeff 2) - f.coeff 1 * f.coeff 3 * 3 +
              f.coeff 1 * f.coeff 3))) *
    HPow.hPow (α := R) (β := ℕ) (-1) 3 =
  HPow.hPow (β := ℕ) (f.coeff 2) 2 * HPow.hPow (β := ℕ) (f.coeff 1) 2 -
          4 * f.coeff 3 * HPow.hPow (β := ℕ) (f.coeff 1) 3 -
        4 * HPow.hPow (β := ℕ) (f.coeff 2) 3 * f.coeff 0 -
      27 * HPow.hPow (β := ℕ) (f.coeff 3) 2 * HPow.hPow (β := ℕ) (f.coeff 0) 2 +
    18 * f.coeff 3 * f.coeff 2 * f.coeff 1 * f.coeff 0
Tactic: simp [Matrix.det_succ_row_zero (n := 4), Matrix.det_succ_row_zero (n := 3), Fin.succAbove,
    Matrix.det_fin_three, Finset.sum_fin_eq_sum_range, Finset.sum_range_succ, hf]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
s : R
⊢ (p.scaleRoots s).coeff p.natDegree = p.leadingCoeff
have rw : (p.scaleRoots s).coeff p.natDegree = p.coeff p.natDegree
Tactic: rw [leadingCoeff, coeff_scaleRoots, tsub_self, pow_zero, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
s : R
rw : (p.scaleRoots s).coeff p.natDegree = p.coeff p.natDegree
⊢ (p.scaleRoots s).coeff p.natDegree = p.leadingCoeff
have rw₁ : p.coeff p.natDegree * s ^ (p.natDegree - p.natDegree) = p.coeff p.natDegree
Tactic: rw [leadingCoeff, coeff_scaleRoots, tsub_self, pow_zero, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
s : R
rw : (p.scaleRoots s).coeff p.natDegree = p.coeff p.natDegree
rw₁ : p.coeff p.natDegree * s ^ (p.natDegree - p.natDegree) = p.coeff p.natDegree
⊢ (p.scaleRoots s).coeff p.natDegree = p.leadingCoeff
have rw₂ : p.coeff p.natDegree * HPow.hPow (β := ℕ) s 0 = p.coeff p.natDegree
Tactic: rw [leadingCoeff, coeff_scaleRoots, tsub_self, pow_zero, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
s : R
rw : (p.scaleRoots s).coeff p.natDegree = p.coeff p.natDegree
rw₁ : p.coeff p.natDegree * s ^ (p.natDegree - p.natDegree) = p.coeff p.natDegree
rw₂ : p.coeff p.natDegree * HPow.hPow (β := ℕ) s 0 = p.coeff p.natDegree
⊢ (p.scaleRoots s).coeff p.natDegree = p.leadingCoeff
have rw₃ : p.coeff p.natDegree * 1 = p.coeff p.natDegree
Tactic: rw [leadingCoeff, coeff_scaleRoots, tsub_self, pow_zero, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
s : R
rw : (p.scaleRoots s).coeff p.natDegree = p.coeff p.natDegree
rw₁ : p.coeff p.natDegree * s ^ (p.natDegree - p.natDegree) = p.coeff p.natDegree
rw₂ : p.coeff p.natDegree * HPow.hPow (β := ℕ) s 0 = p.coeff p.natDegree
rw₃ : p.coeff p.natDegree * 1 = p.coeff p.natDegree
⊢ (p.scaleRoots s).coeff p.natDegree = p.leadingCoeff
have rw₄ : p.coeff p.natDegree = p.coeff p.natDegree
Tactic: rw [leadingCoeff, coeff_scaleRoots, tsub_self, pow_zero, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (goal)
Goal:
R : Type u_1
inst : Semiring R
s : R
⊢ Eq (α := R[X]) (scaleRoots 0 s) 0
have a : ∀ (n : ℕ), coeff (scaleRoots 0 s) n = coeff 0 n
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (hypothesis)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
hp : p ≠ 0
s : R
h : p.scaleRoots s = 0
⊢ False
have this : p.coeff p.natDegree ≠ 0
Tactic: have : p.coeff p.natDegree ≠ 0 := mt leadingCoeff_eq_zero.mp hp
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (hypothesis)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
hp : p ≠ 0
s : R
h : p.scaleRoots s = 0
this : p.coeff p.natDegree ≠ 0
⊢ False
have this₁ : (p.scaleRoots s).coeff p.natDegree = 0
Tactic: have : (scaleRoots p s).coeff p.natDegree = 0 :=
    congr_fun (congr_arg (coeff : R[X] → ℕ → R) h) p.natDegree
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (hypothesis)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
hp : p ≠ 0
s : R
h : p.scaleRoots s = 0
this_1 : p.coeff p.natDegree ≠ 0
this : (p.scaleRoots s).coeff p.natDegree = 0
⊢ False
have this₁ : p.leadingCoeff = 0
Tactic: rw [coeff_scaleRoots_natDegree] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
s : R
hs : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) s
i : ℕ
⊢ i ∈ p.support → i ∈ (p.scaleRoots s).support
have simp : p.coeff i ≠ 0 → p.coeff i * s ^ (p.natDegree - i) ≠ 0
Tactic: simp only [coeff_scaleRoots, Polynomial.mem_support_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (hypothesis)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
s : R
hs : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) s
i : ℕ
p_ne_zero : p.coeff i ≠ 0
ps_zero : p.coeff i * s ^ (p.natDegree - i) = 0
⊢ False
have this : p.coeff i = 0
Tactic: have := (pow_mem hs (p.natDegree - i)).2 _ ps_zero
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
s : R
⊢ (p.scaleRoots s).degree = p.degree
have haveI : ∀ (this : (a : Prop) → Decidable a), (p.scaleRoots s).degree = p.degree
Tactic: haveI := Classical.propDecidable
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
s : R
this : (a : Prop) → Decidable a
⊢ (p.scaleRoots s).degree = p.degree
have pos : ∀ (hp : p = 0), (p.scaleRoots s).degree = p.degree
Tactic: by_cases hp : p = 0
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
s : R
this : (a : Prop) → Decidable a
pos : ∀ (hp : p = 0), (p.scaleRoots s).degree = p.degree
⊢ (p.scaleRoots s).degree = p.degree
have neg : ∀ (hp : ¬p = 0), (p.scaleRoots s).degree = p.degree
Tactic: by_cases hp : p = 0
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
s : R
this : (a : Prop) → Decidable a
hp : p = 0
⊢ (p.scaleRoots s).degree = p.degree
have pos : degree (scaleRoots 0 s) = degree.{u_1} (R := R) 0
Tactic: rw [hp, zero_scaleRoots]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
s : R
this : (a : Prop) → Decidable a
hp : p = 0
pos : degree (scaleRoots 0 s) = degree.{u_1} (R := R) 0
⊢ (p.scaleRoots s).degree = p.degree
have pos₁ : degree.{u_1} (R := R) 0 = degree.{u_1} (R := R) 0
Tactic: rw [hp, zero_scaleRoots]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
s : R
this : (a : Prop) → Decidable a
hp : ¬p = 0
⊢ (p.scaleRoots s).degree = p.degree
have neg : (p.scaleRoots s).coeff p.natDegree ≠ 0
Tactic: refine le_antisymm (Finset.sup_mono (support_scaleRoots_le p s)) (degree_le_degree ?_)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
s : R
this : (a : Prop) → Decidable a
hp : ¬p = 0
⊢ (p.scaleRoots s).coeff p.natDegree ≠ 0
have neg : p.leadingCoeff ≠ 0
Tactic: rw [coeff_scaleRoots_natDegree]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (hypothesis)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
s : R
this : (a : Prop) → Decidable a
hp : ¬p = 0
h : p.leadingCoeff = 0
⊢ False
have this₁ : p = 0
Tactic: have := leadingCoeff_eq_zero.mp h
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
r : R
⊢ (p.scaleRoots r).leadingCoeff = p.leadingCoeff
have rw : (p.scaleRoots r).coeff (p.scaleRoots r).natDegree = p.leadingCoeff
Tactic: rw [leadingCoeff, natDegree_scaleRoots, coeff_scaleRoots_natDegree]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
r : R
rw : (p.scaleRoots r).coeff (p.scaleRoots r).natDegree = p.leadingCoeff
⊢ (p.scaleRoots r).leadingCoeff = p.leadingCoeff
have rw₁ : (p.scaleRoots r).coeff p.natDegree = p.leadingCoeff
Tactic: rw [leadingCoeff, natDegree_scaleRoots, coeff_scaleRoots_natDegree]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
r : R
rw : (p.scaleRoots r).coeff (p.scaleRoots r).natDegree = p.leadingCoeff
rw₁ : (p.scaleRoots r).coeff p.natDegree = p.leadingCoeff
⊢ (p.scaleRoots r).leadingCoeff = p.leadingCoeff
have rw₂ : p.leadingCoeff = p.leadingCoeff
Tactic: rw [leadingCoeff, natDegree_scaleRoots, coeff_scaleRoots_natDegree]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (goal)
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
inst_1 : Semiring S
p : R[X]
x : R
f : R →+* S
h : Ne.{u_2 + 1} (α := S) ((f : (a : R) → S) p.leadingCoeff : S) (0 : S)
⊢ map f (p.scaleRoots x) = (map f p).scaleRoots ((f : (a : R) → S) x)
have a : ∀ (n : ℕ), (map f (p.scaleRoots x)).coeff n = ((map f p).scaleRoots ((f : (a : R) → S) x)).coeff n
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (goal)
Goal:
R : Type u_1
inst : Semiring R
r c : R
⊢ Eq (α := R[X]) (scaleRoots ((C : (a : R) → R[X]) c) r) ((C : (a : R) → R[X]) c)
have a : ∀ (n : ℕ), coeff (scaleRoots ((C : (a : R) → R[X]) c) r) n = coeff ((C : (a : R) → R[X]) c) n
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
⊢ p.scaleRoots 1 = p
have a : ∀ (n : ℕ), (p.scaleRoots 1).coeff n = p.coeff n
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
⊢ p.scaleRoots 0 = p.leadingCoeff • HPow.hPow (α := R[X]) X p.natDegree
have a : ∀ (n : ℕ), (p.scaleRoots 0).coeff n = (p.leadingCoeff • HPow.hPow (α := R[X]) X p.natDegree).coeff n
Tactic: ext n
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
n : ℕ
⊢ (p.scaleRoots 0).coeff n = (p.leadingCoeff • HPow.hPow (α := R[X]) X p.natDegree).coeff n
have a : (if p.natDegree ≤ n then p.coeff n else 0) = if n = p.natDegree then p.leadingCoeff else 0
Tactic: simp only [coeff_scaleRoots, tsub_eq_zero_iff_le, zero_pow_eq, mul_ite,
    mul_one, mul_zero, coeff_smul, coeff_X_pow, smul_eq_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
n : ℕ
⊢ (if p.natDegree ≤ n then p.coeff n else 0) = if n = p.natDegree then p.leadingCoeff else 0
have pos : ∀ (h₁ : p.natDegree ≤ n) (h₂ : n = p.natDegree), p.coeff n = p.leadingCoeff
Tactic: split_ifs with h₁ h₂ h₂
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
n : ℕ
pos : ∀ (h₁ : p.natDegree ≤ n) (h₂ : n = p.natDegree), p.coeff n = p.leadingCoeff
⊢ (if p.natDegree ≤ n then p.coeff n else 0) = if n = p.natDegree then p.leadingCoeff else 0
have neg : ∀ (h₁ : p.natDegree ≤ n) (h₂ : ¬n = p.natDegree), p.coeff n = 0
Tactic: split_ifs with h₁ h₂ h₂
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
n : ℕ
pos : ∀ (h₁ : p.natDegree ≤ n) (h₂ : n = p.natDegree), p.coeff n = p.leadingCoeff
neg : ∀ (h₁ : p.natDegree ≤ n) (h₂ : ¬n = p.natDegree), p.coeff n = 0
⊢ (if p.natDegree ≤ n then p.coeff n else 0) = if n = p.natDegree then p.leadingCoeff else 0
have pos₁ : ∀ (h₁ : ¬p.natDegree ≤ n) (h₂ : n = p.natDegree), 0 = p.leadingCoeff
Tactic: split_ifs with h₁ h₂ h₂
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
n : ℕ
pos : ∀ (h₁ : p.natDegree ≤ n) (h₂ : n = p.natDegree), p.coeff n = p.leadingCoeff
neg : ∀ (h₁ : p.natDegree ≤ n) (h₂ : ¬n = p.natDegree), p.coeff n = 0
pos₁ : ∀ (h₁ : ¬p.natDegree ≤ n) (h₂ : n = p.natDegree), 0 = p.leadingCoeff
⊢ (if p.natDegree ≤ n then p.coeff n else 0) = if n = p.natDegree then p.leadingCoeff else 0
have neg₁ : ∀ (h₁ : ¬p.natDegree ≤ n) (h₂ : ¬n = p.natDegree), Eq.{u_1 + 1} (α := R) 0 0
Tactic: split_ifs with h₁ h₂ h₂
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
n : ℕ
h₁ : p.natDegree ≤ n
h₂ : n = p.natDegree
⊢ p.coeff n = p.leadingCoeff
have pos : ∀ (h₁ : p.natDegree ≤ p.natDegree), p.coeff p.natDegree = p.leadingCoeff
Tactic: subst h₂
Cleared hypotheses: n, h₁, h₂
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (goal)
Goal:
R : Type u_1
inst : Semiring R
r : R
⊢ Eq (α := R[X]) (scaleRoots 1 r) 1
have a : ∀ (n : ℕ), coeff (scaleRoots 1 r) n = coeff 1 n
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (hypothesis)
Goal:
R : Type u_1
inst : Semiring R
r s : R
⊢ (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X])).scaleRoots s =
    HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (r * s) : R[X])
have a : Nontrivial R
Tactic: nontriviality R
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (goal)
Goal:
R : Type u_1
inst : Semiring R
r s : R
h : Nontrivial R
⊢ (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X])).scaleRoots s =
    HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (r * s) : R[X])
have a : ((HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X])).scaleRoots s).coeff 0 =
  (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (r * s) : R[X])).coeff 0
Tactic: ext (_ | _ | i)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (goal)
Goal:
R : Type u_1
inst : Semiring R
r s : R
h : Nontrivial R
a :
  ((HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X])).scaleRoots s).coeff 0 =
    (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (r * s) : R[X])).coeff 0
⊢ (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X])).scaleRoots s =
    HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (r * s) : R[X])
have a₁ : ((HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X])).scaleRoots s).coeff (HAdd.hAdd (α := ℕ) 0 1) =
  (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (r * s) : R[X])).coeff (HAdd.hAdd (α := ℕ) 0 1)
Tactic: ext (_ | _ | i)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ScaleRoots (goal)
Goal:
R : Type u_1
inst : Semiring R
r s : R
h : Nontrivial R
a :
  ((HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X])).scaleRoots s).coeff 0 =
    (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (r * s) : R[X])).coeff 0
a₁ :
  ((HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X])).scaleRoots s).coeff (HAdd.hAdd (α := ℕ) 0 1) =
    (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (r * s) : R[X])).coeff (HAdd.hAdd (α := ℕ) 0 1)
⊢ (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X])).scaleRoots s =
    HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (r * s) : R[X])
have a₂ : ∀ (i : ℕ),
  ((HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X])).scaleRoots s).coeff (i + 1 + 1) =
    (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (r * s) : R[X])).coeff (i + 1 + 1)
Tactic: ext (_ | _ | i)
-- 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)
i : ℕ
_hi : i ∈ p.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) =
    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
have 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
Tactic: simp_rw [f.map_mul, f.map_pow, pow_add, hsa.mul_pow, mul_assoc]
-- 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)
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
⊢ 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
have 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
Tactic: simp_rw [f.map_mul, f.map_pow, pow_add, hsa.mul_pow, mul_assoc]
-- 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)
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
⊢ 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
have 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
Tactic: simp_rw [f.map_mul, f.map_pow, pow_add, hsa.mul_pow, mul_assoc]
-- 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)
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
⊢ 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
have 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
Tactic: simp_rw [f.map_mul, f.map_pow, pow_add, hsa.mul_pow, mul_assoc]
-- 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)
i : ℕ
hi : i ∈ p.support
⊢ 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)
have rw : i ≤ p.natDegree
Tactic: rw [mul_assoc, ← map_pow, (hf _ _).left_comm, map_pow, tsub_add_cancel_of_le]