awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
hf : f.natDegree = 3
hi : 4 < 5
hj : 2 < 5
⊢ HAdd.hAdd (α := R) 2 1 = 3

Tactic:
norm_num
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
hf : f.natDegree = 3
hi : 4 < 5
hj : 3 < 5
⊢ HAdd.hAdd (α := R) 2 1 = 3

Tactic:
norm_num
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
hf : f.natDegree = 3
hi hj : 4 < 5
⊢ HAdd.hAdd (α := R) 2 1 = 3

Tactic:
norm_num
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
hf : f.degree = 3
⊢ f.natDegree = 3

Tactic:
apply natDegree_eq_of_degree_eq_some at hf

Premises used: Polynomial.natDegree_eq_of_degree_eq_some
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
hf : f.natDegree = 3
rw rw₁ : 3 - 1 + 3 = 5
⊢ f.natDegree - 1 + f.natDegree = 5

Tactic:
rw [hf]
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
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 ⋯
rw :
  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
⊢ f.discr =
    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:
rw [discr, ← Matrix.det_reindex_self e, sylvesterDeriv_of_natDegree_eq_three hf]

Premises used: Matrix.det_reindex_self, Polynomial.discr, _private.0.Polynomial.sylvesterDeriv_of_natDegree_eq_three
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
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 ⋯
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
⊢ 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

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]

Premises used: Fin.succAbove, Finset.sum_fin_eq_sum_range, Matrix.det_fin_three, Matrix.det_succ_row_zero, Finset.sum_range_succ
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
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 ⋯
⊢ (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:
ring_nf
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
s : R
i : ℕ
⊢ (p.scaleRoots s).coeff i = p.coeff i * s ^ (p.natDegree - i)

Tactic:
simp +contextual [scaleRoots, coeff_monomial]

Premises used: Polynomial.coeff_monomial, Polynomial.scaleRoots
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
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
rw₄ rw₅ : p.coeff p.natDegree = p.coeff p.natDegree
⊢ (p.scaleRoots s).coeff p.natDegree = p.leadingCoeff

Tactic:
rw [leadingCoeff, coeff_scaleRoots, tsub_self, pow_zero, mul_one]

Premises used: tsub_self, Polynomial.coeff_scaleRoots, Polynomial.leadingCoeff, pow_zero, mul_one
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
R : Type u_1
inst : Semiring R
s : R
a : ∀ (n : ℕ), coeff (scaleRoots 0 s) n = coeff 0 n
⊢ Eq (α := R[X]) (scaleRoots 0 s) 0

Tactic:
ext
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
R : Type u_1
inst : Semiring R
s : R
n : ℕ
⊢ coeff (scaleRoots 0 s) n = coeff 0 n

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
hp : p ≠ 0
s : R
h : p.scaleRoots s = 0
⊢ p.coeff p.natDegree ≠ 0

Tactic:
have : p.coeff p.natDegree ≠ 0 := mt leadingCoeff_eq_zero.mp hp
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
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
⊢ (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
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
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
⊢ p.leadingCoeff = 0

Tactic:
rw [coeff_scaleRoots_natDegree] at this

Premises used: Polynomial.coeff_scaleRoots_natDegree
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
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.leadingCoeff = 0
⊢ False

Tactic:
contradiction
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
s : R
x : ℕ
⊢ x ∈ (p.scaleRoots s).support → x ∈ p.support

Tactic:
simpa using left_ne_zero_of_mul

Premises used: left_ne_zero_of_mul
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
s : R
hs : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) s
i : ℕ
simp : p.coeff i ≠ 0 → p.coeff i * s ^ (p.natDegree - i) ≠ 0
⊢ i ∈ p.support → i ∈ (p.scaleRoots s).support

Tactic:
simp only [coeff_scaleRoots, Polynomial.mem_support_iff]

Premises used: Polynomial.mem_support_iff, Polynomial.coeff_scaleRoots
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
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
⊢ p.coeff i = 0

Tactic:
have := (pow_mem hs (p.natDegree - i)).2 _ ps_zero
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
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
this : p.coeff i = 0
⊢ False

Tactic:
contradiction
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
s : R
haveI : ∀ (this : (a : Prop) → Decidable a), (p.scaleRoots s).degree = p.degree
⊢ (p.scaleRoots s).degree = p.degree

Tactic:
haveI := Classical.propDecidable
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
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
neg : ∀ (hp : ¬p = 0), (p.scaleRoots s).degree = p.degree
⊢ (p.scaleRoots s).degree = p.degree

Tactic:
by_cases hp : p = 0
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
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
pos₁ pos₂ : degree.{u_1} (R := R) 0 = degree.{u_1} (R := R) 0
⊢ (p.scaleRoots s).degree = p.degree

Tactic:
rw [hp, zero_scaleRoots]

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

Tactic:
le_antisymm (Finset.sup_mono (support_scaleRoots_le p s)) (degree_le_degree ?_)

Premises used: Polynomial.degree_le_degree, le_antisymm, Finset.sup_mono, Polynomial.support_scaleRoots_le
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
s : R
this : (a : Prop) → Decidable a
hp : ¬p = 0
neg : (p.scaleRoots s).coeff p.natDegree ≠ 0
⊢ (p.scaleRoots s).degree = p.degree

Tactic:
refine le_antisymm (Finset.sup_mono (support_scaleRoots_le p s)) (degree_le_degree ?_)

Premises used: Polynomial.degree_le_degree, le_antisymm, Finset.sup_mono, Polynomial.support_scaleRoots_le
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
s : R
this : (a : Prop) → Decidable a
hp : ¬p = 0
neg : p.leadingCoeff ≠ 0
⊢ (p.scaleRoots s).coeff p.natDegree ≠ 0

Tactic:
rw [coeff_scaleRoots_natDegree]

Premises used: Polynomial.coeff_scaleRoots_natDegree
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
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
⊢ p = 0

Tactic:
have := leadingCoeff_eq_zero.mp h
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
s : R
this_1 : (a : Prop) → Decidable a
hp : ¬p = 0
h : p.leadingCoeff = 0
this : p = 0
⊢ False

Tactic:
contradiction
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
s : R
⊢ (p.scaleRoots s).natDegree = p.natDegree

Tactic:
simp only [natDegree, degree_scaleRoots]

Premises used: Polynomial.degree_scaleRoots, Polynomial.natDegree
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
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
rw₂ rw₃ : p.leadingCoeff = p.leadingCoeff
⊢ (p.scaleRoots r).leadingCoeff = p.leadingCoeff

Tactic:
rw [leadingCoeff, natDegree_scaleRoots, coeff_scaleRoots_natDegree]

Premises used: Polynomial.natDegree_scaleRoots, Polynomial.leadingCoeff, Polynomial.coeff_scaleRoots_natDegree
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
s : R
⊢ (p.scaleRoots s).Monic ↔ p.Monic

Tactic:
simp only [Monic, leadingCoeff_scaleRoots]

Premises used: Polynomial.Monic, Polynomial.leadingCoeff_scaleRoots
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
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)
a : ∀ (n : ℕ), (map f (p.scaleRoots x)).coeff n = ((map f p).scaleRoots ((f : (a : R) → S) x)).coeff n
⊢ map f (p.scaleRoots x) = (map f p).scaleRoots ((f : (a : R) → S) x)

Tactic:
ext
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
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)
n : ℕ
⊢ (map f (p.scaleRoots x)).coeff n = ((map f p).scaleRoots ((f : (a : R) → S) x)).coeff n

Tactic:
simp [Polynomial.natDegree_map_of_leadingCoeff_ne_zero _ h]

Premises used: Polynomial.natDegree_map_of_leadingCoeff_ne_zero
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
R : Type u_1
inst : Semiring R
r c : R
a : ∀ (n : ℕ), coeff (scaleRoots ((C : (a : R) → R[X]) c) r) n = coeff ((C : (a : R) → R[X]) c) n
⊢ Eq (α := R[X]) (scaleRoots ((C : (a : R) → R[X]) c) r) ((C : (a : R) → R[X]) c)

Tactic:
ext
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
R : Type u_1
inst : Semiring R
r c : R
n : ℕ
⊢ coeff (scaleRoots ((C : (a : R) → R[X]) c) r) n = coeff ((C : (a : R) → R[X]) c) n

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
a : ∀ (n : ℕ), (p.scaleRoots 1).coeff n = p.coeff n
⊢ p.scaleRoots 1 = p

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

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
a : ∀ (n : ℕ), (p.scaleRoots 0).coeff n = (p.leadingCoeff • HPow.hPow (α := R[X]) X p.natDegree).coeff n
⊢ p.scaleRoots 0 = p.leadingCoeff • HPow.hPow (α := R[X]) X p.natDegree

Tactic:
ext n
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
n : ℕ
a : (if p.natDegree ≤ n then p.coeff n else 0) = if n = p.natDegree then p.leadingCoeff else 0
⊢ (p.scaleRoots 0).coeff n = (p.leadingCoeff • HPow.hPow (α := R[X]) X p.natDegree).coeff n

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]

Premises used: Polynomial.coeff_X_pow, mul_ite, Polynomial.coeff_scaleRoots, tsub_eq_zero_iff_le, MulZeroClass.mul_zero, Polynomial.coeff_smul, zero_pow_eq, smul_eq_mul, mul_one
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
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
neg₁ : ∀ (h₁ : ¬p.natDegree ≤ n) (h₂ : ¬n = p.natDegree), Eq.{u_1 + 1} (α := R) 0 0
⊢ (if p.natDegree ≤ n then p.coeff n else 0) = if n = p.natDegree then p.leadingCoeff else 0

Tactic:
split_ifs with h₁ h₂ h₂
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
n : ℕ
h₁ : p.natDegree ≤ n
h₂ : n = p.natDegree
pos : ∀ (h₁ : p.natDegree ≤ p.natDegree), p.coeff p.natDegree = p.leadingCoeff
⊢ p.coeff n = p.leadingCoeff

Tactic:
subst h₂
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
h₁ : p.natDegree ≤ p.natDegree
⊢ p.coeff p.natDegree = p.leadingCoeff

Tactic:
rfl
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
n : ℕ
h₁ : p.natDegree ≤ n
h₂ : ¬n = p.natDegree
⊢ p.coeff n = 0

Tactic:
coeff_eq_zero_of_natDegree_lt (lt_of_le_of_ne h₁ (Ne.symm h₂))

Premises used: Ne.symm, Polynomial.coeff_eq_zero_of_natDegree_lt, lt_of_le_of_ne
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
n : ℕ
h₁ : p.natDegree ≤ n
h₂ : ¬n = p.natDegree
⊢ p.coeff n = 0

Tactic:
exact coeff_eq_zero_of_natDegree_lt (lt_of_le_of_ne h₁ (Ne.symm h₂))

Premises used: Ne.symm, Polynomial.coeff_eq_zero_of_natDegree_lt, lt_of_le_of_ne
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
n : ℕ
h₁ : ¬p.natDegree ≤ n
h₂ : n = p.natDegree
⊢ 0 = p.leadingCoeff

Tactic:
(h₁ h₂.ge).elim

Premises used: Eq.ge, False.elim
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
n : ℕ
h₁ : ¬p.natDegree ≤ n
h₂ : n = p.natDegree
⊢ 0 = p.leadingCoeff

Tactic:
exact (h₁ h₂.ge).elim

Premises used: Eq.ge, False.elim
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
n : ℕ
h₁ : ¬p.natDegree ≤ n
h₂ : ¬n = p.natDegree
⊢ Eq.{u_1 + 1} (α := R) 0 0

Tactic:
rfl
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
R : Type u_1
inst : Semiring R
r : R
a : ∀ (n : ℕ), coeff (scaleRoots 1 r) n = coeff 1 n
⊢ Eq (α := R[X]) (scaleRoots 1 r) 1

Tactic:
ext
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
R : Type u_1
inst : Semiring R
r : R
n : ℕ
⊢ coeff (scaleRoots 1 r) n = coeff 1 n

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
R : Type u_1
inst : Semiring R
r s : R
⊢ Nontrivial R

Tactic:
nontriviality R
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
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)
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)
⊢ (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])

Tactic:
ext (_ | _ | i)
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
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).coeff 0 =
    (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (r * s) : R[X])).coeff 0

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
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).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:
simp
-- Module: Mathlib.RingTheory.Polynomial.ScaleRoots
Goal:
R : Type u_1
inst : Semiring R
r s : R
h : Nontrivial R
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:
simp
-- 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)

Tactic:
simp [eval₂_eq_sum, sum_def]

Premises used: 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)
i : ℕ
_hi : i ∈ p.support
hi' : i ∉ (p.scaleRoots s).support
⊢ p.coeff i * s ^ (p.natDegree - i) = 0

Tactic:
simpa using hi'
-- 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
hi' : i ∉ (p.scaleRoots s).support
this : p.coeff i * s ^ (p.natDegree - i) = 0 := ⋯
⊢ 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) =
    0

Tactic:
simp [this]