mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Polynomial.Dickson

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ ∃ K x, ∃ (_ : CharP K p), Infinite K

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.HilbertPoly

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
d k : ℕ
⊢ ↑d ! ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Hermite.Basic

Goal state before:
pp: n✝ k✝ : ℕ
hermite_explicit : ℕ → ℕ → ℤ := fun n k ↦ (-1) ^ n * ↑(2 * n - 1)‼ * ↑((2 * n + k).choose k)
n k : ℕ
⊢ 2 * (n + 1) - 1 = 2 * n + 1

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Dickson

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H✝ : Set.univ.Infinite
h : {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}.Finite
x : K
x✝ : x ∈ {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
φ : K[X] := X ^ 2 - C x * X + 1
H : φ = 0
⊢ eval 0 φ = 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.HilbertPoly

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
d k : ℕ
⊢ (preHilbertPoly F d k).natDegree = d

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Dickson

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Set.univ.Infinite
h : {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}.Finite
x : K
x✝ : x ∈ {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
φ : K[X] := X ^ 2 - C x * X + 1
⊢ φ ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Hermite.Basic

Goal state before:
pp: n✝ k✝ : ℕ
hermite_explicit : ℕ → ℕ → ℤ := fun n k ↦ (-1) ^ n * ↑(2 * n - 1)‼ * ↑((2 * n + k).choose k)
n k : ℕ
⊢ 2 * (n + 1) + (k + 1) = 2 * n + 1 + (k + 1) + 1

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.HilbertPoly

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
d k : ℕ
hne : ↑d ! ≠ 0
heq : d = ((ascPochhammer F d).comp (X - C ↑k + 1)).natDegree
⊢ ((↑d !)⁻¹ • (ascPochhammer F d).comp (X - C ↑k + 1)).coeff ((ascPochhammer F d).comp (X - C ↑k + 1)).natDegree =
    (↑d !)⁻¹ • ((ascPochhammer F d).comp (X - C (↑k - 1))).leadingCoeff

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Hermite.Basic

Goal state before:
pp: n✝ k✝ : ℕ
hermite_explicit : ℕ → ℕ → ℤ := fun n k ↦ (-1) ^ n * ↑(2 * n - 1)‼ * ↑((2 * n + k).choose k)
n k : ℕ
⊢ 2 * (n + 1) + k = 2 * n + 1 + (k + 1)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.HilbertPoly

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
d k : ℕ
hne : ↑d ! ≠ 0
heq : d = ((ascPochhammer F d).comp (X - C ↑k + 1)).natDegree
⊢ (↑d !)⁻¹ • ((ascPochhammer F d).comp (X - C (↑k - 1))).leadingCoeff = (↑d !)⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.HilbertPoly

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
d k : ℕ
⊢ (preHilbertPoly F d k).coeff d = (↑d !)⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Hermite.Basic

Goal state before:
pp: n✝ k✝ : ℕ
hermite_explicit : ℕ → ℕ → ℤ := fun n k ↦ (-1) ^ n * ↑(2 * n - 1)‼ * ↑((2 * n + k).choose k)
n k : ℕ
⊢ 2 * n + (k + 2) = 2 * n + 1 + (k + 1)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.HilbertPoly

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
d k : ℕ
⊢ (preHilbertPoly F d k).leadingCoeff = (↑d !)⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.HilbertPoly

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
d k n : ℕ
hkn : k ≤ n
⊢ ↑d ! ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.HilbertPoly

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
d k n : ℕ
hkn : k ≤ n
this : ↑d ! ≠ 0
⊢ eval (↑n) (preHilbertPoly F d k) = (↑d !)⁻¹ * eval (↑(n - k + 1)) (ascPochhammer F d)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.HilbertPoly

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
d k n : ℕ
hkn : k ≤ n
this : ↑d ! ≠ 0
⊢ (↑d !)⁻¹ * eval (↑(n - k + 1)) (ascPochhammer F d) = ↑((n - k + d).choose d)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.HilbertPoly

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
d k n : ℕ
hkn : k ≤ n
⊢ eval (↑n) (preHilbertPoly F d k) = ↑((n - k + d).choose d)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.HilbertPoly

Goal state before:
pp: case zero
F : Type u_1
inst✝ : Field F
⊢ (match 0 with
    | 0 => 0
    | d.succ => ∑ i ∈ support 0, coeff 0 i • preHilbertPoly F d i) =
    0

Tactic:
simp only

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Hermite.Basic

Goal state before:
pp: n k : ℕ
hermite_explicit : ℕ → ℕ → ℤ := fun n k ↦ (-1) ^ n * ↑(2 * n - 1)‼ * ↑((2 * n + k).choose k)
⊢ ∀ (n k : ℕ), hermite_explicit (n + 1) (k + 1) = hermite_explicit (n + 1) k - (↑k + 2) * hermite_explicit n (k + 2)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.HilbertPoly

Goal state before:
pp: F : Type u_1
inst✝ : Field F
d : ℕ
⊢ hilbertPoly 0 d = 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.HilbertPoly

Goal state before:
pp: F : Type u_1
inst✝ : Field F
d k : ℕ
⊢ (X ^ k).hilbertPoly (d + 1) = preHilbertPoly F d k

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Hermite.Gaussian

Goal state before:
pp: n : ℕ
x : ℝ
⊢ deriv^[n] (fun y ↦ Real.exp (-(y ^ 2 / 2))) x = (-1) ^ n * (aeval x) (hermite n) * Real.exp (-(x ^ 2 / 2))

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.HilbertPoly

Goal state before:
pp: case succ
F : Type u_1
inst✝ : Field F
p q : F[X]
d : ℕ
a✝ :
  (match d with
    | 0 => 0
    | d.succ => ∑ i ∈ (p + q).support, (p + q).coeff i • preHilbertPoly F d i) =
    (match d with
      | 0 => 0
      | d.succ => ∑ i ∈ p.support, p.coeff i • preHilbertPoly F d i) +
      match d with
      | 0 => 0
      | d.succ => ∑ i ∈ q.support, q.coeff i • preHilbertPoly F d i
⊢ (match d + 1 with
    | 0 => 0
    | d.succ => ∑ i ∈ (p + q).support, (p + q).coeff i • preHilbertPoly F d i) =
    (match d + 1 with
      | 0 => 0
      | d.succ => ∑ i ∈ p.support, p.coeff i • preHilbertPoly F d i) +
      match d + 1 with
      | 0 => 0
      | d.succ => ∑ i ∈ q.support, q.coeff i • preHilbertPoly F d i

Tactic:
simp only

Goal state after:
case succ
F : Type u_1
inst✝ : Field F
p q : F[X]
d : ℕ
a✝ :
  (match d with
    | 0 => 0
    | d.succ => ∑ i ∈ (p + q).support, (p + q).coeff i • preHilbertPoly F d i) =
    (match d with
      | 0 => 0
      | d.succ => ∑ i ∈ p.support, p.coeff i • preHilbertPoly F d i) +
      match d with
      | 0 => 0
      | d.succ => ∑ i ∈ q.support, q.coeff i • preHilbertPoly F d i
⊢ ∑ i ∈ (p + q).support, (p + q).coeff i • preHilbertPoly F d i =
    ∑ i ∈ p.support, p.coeff i • preHilbertPoly F d i + ∑ i ∈ q.support, q.coeff i • preHilbertPoly F d i
Module: Mathlib.RingTheory.Polynomial.Hermite.Gaussian

Goal state before:
pp: n : ℕ
x : ℝ
⊢ (aeval x) (hermite n) = (-1) ^ n * deriv^[n] (fun y ↦ Real.exp (-(y ^ 2 / 2))) x / Real.exp (-(x ^ 2 / 2))

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Dickson

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Set.univ.Infinite
h : {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}.Finite
this : Set.univ = ⋃ x ∈ {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}, {y | x = y + y⁻¹ ∨ y = 0}
⊢ Set.univ.Finite

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.HilbertPoly

Goal state before:
pp: F : Type u_1
inst✝ : Field F
p q : F[X]
d : ℕ
⊢ (p + q).hilbertPoly d = p.hilbertPoly d + q.hilbertPoly d

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Hermite.Gaussian

Goal state before:
pp: n : ℕ
x : ℝ
⊢ (aeval x) (hermite n) = (-1) ^ n * deriv^[n] (fun y ↦ Real.exp (-(y ^ 2 / 2))) x * Real.exp (x ^ 2 / 2)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.HilbertPoly

Goal state before:
pp: case succ
F : Type u_1
inst✝ : Field F
a : F
p : F[X]
d : ℕ
a✝ :
  (match d with
    | 0 => 0
    | d.succ => ∑ i ∈ (a • p).support, (a • p).coeff i • preHilbertPoly F d i) =
    a •
      match d with
      | 0 => 0
      | d.succ => ∑ i ∈ p.support, p.coeff i • preHilbertPoly F d i
⊢ (match d + 1 with
    | 0 => 0
    | d.succ => ∑ i ∈ (a • p).support, (a • p).coeff i • preHilbertPoly F d i) =
    a •
      match d + 1 with
      | 0 => 0
      | d.succ => ∑ i ∈ p.support, p.coeff i • preHilbertPoly F d i

Tactic:
simp only

Goal state after:
case succ
F : Type u_1
inst✝ : Field F
a : F
p : F[X]
d : ℕ
a✝ :
  (match d with
    | 0 => 0
    | d.succ => ∑ i ∈ (a • p).support, (a • p).coeff i • preHilbertPoly F d i) =
    a •
      match d with
      | 0 => 0
      | d.succ => ∑ i ∈ p.support, p.coeff i • preHilbertPoly F d i
⊢ ∑ i ∈ (a • p).support, (a • p).coeff i • preHilbertPoly F d i = a • ∑ i ∈ p.support, p.coeff i • preHilbertPoly F d i
Module: Mathlib.RingTheory.Polynomial.Hermite.Basic

Goal state before:
pp: n k : ℕ
hermite_explicit : ℕ → ℕ → ℤ := fun n k ↦ (-1) ^ n * ↑(2 * n - 1)‼ * ↑((2 * n + k).choose k)
hermite_explicit_recur :
  ∀ (n k : ℕ), hermite_explicit (n + 1) (k + 1) = hermite_explicit (n + 1) k - (↑k + 2) * hermite_explicit n (k + 2)
⊢ 2 * (n + 1) + k = 2 * n + (k + 2)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.IrreducibleRing

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : (nilradical R).IsPrime
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
f : R[X]
hm : f.Monic
R' : Type u_1 := R ⧸ nilradical R
ψ : R' →+* S := Ideal.Quotient.lift (nilradical R) φ ⋯
ι : R →+* R' := algebraMap R R'
hi : Irreducible (Polynomial.map ι f)
a b : R[X]
h : f = a * b
this : ∀ (a b : R[X]), f = a * b → IsUnit (Polynomial.map ι b) → IsUnit a ∨ IsUnit b
hb : ¬IsUnit (Polynomial.map ι b)
⊢ Polynomial.map ι f = Polynomial.map ι a * Polynomial.map ι b

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.HilbertPoly

Goal state before:
pp: F : Type u_1
inst✝ : Field F
a : F
p : F[X]
d : ℕ
⊢ (a • p).hilbertPoly d = a • p.hilbertPoly d

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Hermite.Basic

Goal state before:
pp: n k : ℕ
⊢ (hermite (2 * (n + 1) + (k + 1))).coeff (k + 1) =
    (-1) ^ (n + 1) * ↑(2 * (n + 1) - 1)‼ * ↑((2 * (n + 1) + (k + 1)).choose (k + 1))

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.IrreducibleRing

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : (nilradical R).IsPrime
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
f : R[X]
hm : f.Monic
R' : Type u_1 := R ⧸ nilradical R
ψ : R' →+* S := Ideal.Quotient.lift (nilradical R) φ ⋯
ι : R →+* R' := algebraMap R R'
hi✝ : Irreducible (Polynomial.map ι f)
a b : R[X]
h : f = a * b
hb : IsUnit (Polynomial.map ι b)
i : ℕ
hi : i ≠ 0
⊢ IsNilpotent (b.coeff i)

Tactic:
obtain ⟨_, _, h⟩ := Polynomial.isUnit_iff.1 hb

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : (nilradical R).IsPrime
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
f : R[X]
hm : f.Monic
R' : Type u_1 := R ⧸ nilradical R
ψ : R' →+* S := Ideal.Quotient.lift (nilradical R) φ ⋯
ι : R →+* R' := algebraMap R R'
hi✝ : Irreducible (Polynomial.map ι f)
a b : R[X]
h✝ : f = a * b
hb : IsUnit (Polynomial.map ι b)
i : ℕ
hi : i ≠ 0
w✝ : R'
left✝ : IsUnit w✝
h : C w✝ = Polynomial.map ι b
⊢ IsNilpotent (b.coeff i)
Module: Mathlib.RingTheory.Polynomial.IrreducibleRing

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : (nilradical R).IsPrime
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
f : R[X]
hm : f.Monic
R' : Type u_1 := R ⧸ nilradical R
ψ : R' →+* S := Ideal.Quotient.lift (nilradical R) φ ⋯
ι : R →+* R' := algebraMap R R'
hi✝ : Irreducible (Polynomial.map ι f)
a b : R[X]
h : f = a * b
hb : IsUnit (Polynomial.map ι b)
i : ℕ
hi : i ≠ 0
⊢ IsNilpotent (b.coeff i)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Dickson

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ dickson 1 1 p = X ^ p

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Dickson

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP R p
⊢ 1 = (ZMod.castHom ⋯ R) 1

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Hermite.Basic

Goal state before:
pp: n k : ℕ
h_le : k ≤ n
m : ℕ
hm : n - k = m + m
⊢ n = 2 * m + k

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Dickson

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP R p
⊢ dickson 1 1 p = X ^ p

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.HilbertPoly

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
n : ℕ
hn : p.natDegree < n
d : ℕ
hd :
  (PowerSeries.coeff n) (↑p * ↑(invOneSubPow F d)) =
    eval (↑n)
      (match d with
      | 0 => 0
      | d.succ => ∑ i ∈ p.support, p.coeff i • preHilbertPoly F d i)
h_le : ∀ (i : ↥p.support), ↑i ≤ n
i : ↥p.support
⊢ eval (↑n) (preHilbertPoly F d ↑i) = ↑((n + d - ↑i).choose d)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Hermite.Basic

Goal state before:
pp: n k : ℕ
hnk : Even (n + k)
⊢ (hermite n).coeff k = (-1) ^ ((n - k) / 2) * ↑(n - k - 1)‼ * ↑(n.choose k)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Hermite.Basic

Goal state before:
pp: n k : ℕ
⊢ (hermite n).coeff k = if Even (n + k) then (-1) ^ ((n - k) / 2) * ↑(n - k - 1)‼ * ↑(n.choose k) else 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.IrreducibleRing

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : (nilradical R).IsPrime
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
f : R[X]
hm : f.Monic
hi : Irreducible (Polynomial.map φ f)
⊢ Irreducible f

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Opposites

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
n : ℕ
r : R
⊢ (opRingEquiv R) (op ((monomial n) r)) = (monomial n) (op r)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Opposites

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
r : R
n : ℕ
⊢ (opRingEquiv R) (op (C r * X ^ n)) = C (op r) * X ^ n

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Opposites

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
n : ℕ
r : Rᵐᵒᵖ
⊢ (opRingEquiv R) ((opRingEquiv R).symm ((monomial n) r)) = (opRingEquiv R) (op ((monomial n) (unop r)))

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Opposites

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
r : Rᵐᵒᵖ
n : ℕ
⊢ (opRingEquiv R).symm (C r * X ^ n) = op (C (unop r) * X ^ n)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Opposites

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : R[X]ᵐᵒᵖ
n : ℕ
⊢ ((opRingEquiv R) p).coeff n = op ((unop p).coeff n)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Opposites

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : R[X]ᵐᵒᵖ
⊢ ((opRingEquiv R) p).support = (unop p).support

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Opposites

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : R[X]ᵐᵒᵖ
⊢ ((opRingEquiv R) p).natDegree = (unop p).natDegree

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Opposites

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : R[X]ᵐᵒᵖ
⊢ ((opRingEquiv R) p).leadingCoeff = op (unop p).leadingCoeff

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.HilbertPoly

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
d n : ℕ
hn : p.natDegree < n
⊢ (PowerSeries.coeff n) (↑p * ↑(invOneSubPow F d)) = eval (↑n) (p.hilbertPoly d)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Opposites

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
h : IsLeftCancelMulZero R[X]
a b c : R
eq : (fun x ↦ a + x) b = (fun x ↦ a + x) c
a✝ : Nontrivial R
trinomial : R → R[X] := fun r ↦ a • X ^ 2 + r • X + C a
r : R
⊢ (X + C 1) * trinomial r = a • X ^ 3 + (a + r) • X ^ 2 + (a + r) • X + C a

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Opposites

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
h : IsLeftCancelMulZero R[X]
a b c : R
eq : (fun x ↦ a + x) b = (fun x ↦ a + x) c
a✝ : Nontrivial R
trinomial : R → R[X] := fun r ↦ a • X ^ 2 + r • X + C a
ht : ∀ (r : R), (X + C 1) * trinomial r = a • X ^ 3 + (a + r) • X ^ 2 + (a + r) • X + C a
⊢ (fun x ↦ (X + C 1) * x) (trinomial b) = (fun x ↦ (X + C 1) * x) (trinomial c)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Opposites

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
h : IsLeftCancelMulZero R[X]
a b c : R
eq : (fun x ↦ a + x) b = (fun x ↦ a + x) c
⊢ b = c

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Opposites

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
⊢ IsRightCancelMulZero R[X] ↔ IsRightCancelMulZero R ∧ IsCancelAdd R

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Opposites

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
⊢ IsCancelMulZero R[X] ↔ IsCancelMulZero R ∧ IsCancelAdd R

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.HilbertPoly

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
d : ℕ
⊢ ∃! h, ∃ N, ∀ n > N, (PowerSeries.coeff n) (↑p * ↑(invOneSubPow F d)) = eval (↑n) h

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Opposites

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
⊢ IsDomain R[X] ↔ IsDomain R ∧ IsCancelAdd R

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.HilbertPoly

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
d n : ℕ
hn : n > (p * (1 - X)).natDegree
⊢ 1 - PowerSeries.X = ↑(1 - X)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.HilbertPoly

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
d : ℕ
⊢ (p * (1 - X)).hilbertPoly (d + 1) = p.hilbertPoly d

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.HilbertPoly

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
d e : ℕ
⊢ (p * (1 - X) ^ e).hilbertPoly (d + e) = p.hilbertPoly d

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.HilbertPoly

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
d : ℕ
hdp : d ≤ rootMultiplicity 1 p
hp : ¬p = 0
q : F[X]
hq1 : p = (X - C 1) ^ rootMultiplicity 1 p * q
hq2 : ¬X - C 1 ∣ q
⊢ p = q * (-1) ^ rootMultiplicity 1 p * (1 - X) ^ rootMultiplicity 1 p

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.HilbertPoly

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
d : ℕ
hdp : d ≤ rootMultiplicity 1 p
⊢ p.hilbertPoly d = 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.HilbertPoly

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
d : ℕ
hp : p ≠ 0
hpd : rootMultiplicity 1 p < d
q : F[X]
hq1 : p = (X - C 1) ^ rootMultiplicity 1 p * q
hq2 : ¬X - C 1 ∣ q
⊢ p = q * (-1) ^ rootMultiplicity 1 p * (1 - X) ^ rootMultiplicity 1 p

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.HilbertPoly

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
d : ℕ
hp : p ≠ 0
hpd : rootMultiplicity 1 p < d
q : F[X]
hq1 : p = (X - C 1) ^ rootMultiplicity 1 p * q
hq2 : ¬X - C 1 ∣ q
heq : p = q * (-1) ^ rootMultiplicity 1 p * (1 - X) ^ rootMultiplicity 1 p
⊢ (fun x a ↦ a) = fun x a ↦ a * 1 ^ x

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.HilbertPoly

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
d : ℕ
hp : p ≠ 0
hpd : rootMultiplicity 1 p < d
⊢ (p.hilbertPoly d).natDegree = d - rootMultiplicity 1 p - 1

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.HilbertPoly

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
d : ℕ
hh : p.hilbertPoly d ≠ 0
⊢ p ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.HilbertPoly

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
d : ℕ
hh : p.hilbertPoly d ≠ 0
hp : p ≠ 0
⊢ rootMultiplicity 1 p < d

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.HilbertPoly

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
d : ℕ
hh : p.hilbertPoly d ≠ 0
⊢ (p.hilbertPoly d).natDegree = d - rootMultiplicity 1 p - 1

Tactic:
have hp : p ≠ 0 := by
    intro h
    rw [h] at hh
    exact hh (hilbertPoly_zero_left d)
  have hpd : p.rootMultiplicity 1 < d := by
    by_contra h
    exact hh (hilbertPoly_eq_zero_of_le_rootMultiplicity_one <| not_lt.1 h)
  exact natDegree_hilbertPoly_of_ne_zero_of_rootMultiplicity_lt hp hpd

Goal state after:
Module: Mathlib.RingTheory.Polynomial.HilbertPoly

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
d : ℕ
hh : p.hilbertPoly d ≠ 0
⊢ (p.hilbertPoly d).natDegree = d - rootMultiplicity 1 p - 1

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Selmer

Goal state before:
pp: n : ℕ
z : ℂ
h1 : z ^ n = z + 1
h2 : z ^ n + z ^ 2 = 0
⊢ z ^ 3 = 1

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Selmer

Goal state before:
pp: n : ℕ
z : ℂ
h1 : z ^ n = z + 1
h2 : z ^ n + z ^ 2 = 0
h3 : z ^ 3 = 1
⊢ z ^ n = 1 ∨ z ^ n = z ∨ z ^ n = z ^ 2

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Selmer

Goal state before:
pp: n : ℕ
z : ℂ
h1 : z ^ n = z + 1
h2 : z ^ n + z ^ 2 = 0
h3 : z ^ 3 = 1
z_ne_zero : z ≠ 0
key : z ^ n = 1
⊢ z = 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Selmer

Goal state before:
pp: n : ℕ
z : ℂ
h1 : z ^ n = z + 1
h2 : z ^ n + z ^ 2 = 0
h3 : z ^ 3 = 1
z_ne_zero : z ≠ 0
key : z ^ n = z
⊢ 1 = 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Selmer

Goal state before:
pp: n : ℕ
z : ℂ
h1 : z ^ n = z + 1
h2 : z ^ n + z ^ 2 = 0
h3 : z ^ 3 = 1
z_ne_zero : z ≠ 0
key : z ^ n = z ^ 2
⊢ z ^ ?m.376 = 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Selmer

Goal state before:
pp: n : ℕ
z : ℂ
⊢ ¬(z ^ n = z + 1 ∧ z ^ n + z ^ 2 = 0)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Selmer

Goal state before:
pp: n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
hn : 1 < n
⊢ X ^ n - X - 1 = trinomial 0 1 n (-1) (-1) 1

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.ShiftedLegendre

Goal state before:
pp: n : ℕ
⊢ (⇑derivative)^[n] (X ^ n * (1 - X) ^ n) = (⇑derivative)^[n] ((X - X ^ 2) ^ n)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.ShiftedLegendre

Goal state before:
pp: n : ℕ
⊢ (⇑derivative)^[n] ((X - X ^ 2) ^ n) = (⇑derivative)^[n] (∑ m ∈ range (n + 1), n.choose m • (-1) ^ m * X ^ (n + m))

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Selmer

Goal state before:
pp: n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
hn : 1 < n
hp : X ^ n - X - 1 = trinomial 0 1 n (-1) (-1) 1
z : ℂ
h1 : -1 * z ^ 0 + -1 * z ^ 1 + 1 * z ^ n = 0
h2 : 1 * z ^ 0 + -1 * z ^ (n - 1 + 0) + -1 * z ^ n = 0
⊢ z ^ n = z + 1

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.ShiftedLegendre

Goal state before:
pp: n x : ℕ
a✝ : x ∈ range (n + 1)
⊢ n ≤ n + x

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Selmer

Goal state before:
pp: n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
hn : 1 < n
hp : X ^ n - X - 1 = trinomial 0 1 n (-1) (-1) 1
z : ℂ
h1 : z ^ n = z + 1
h2 : 1 * z ^ 0 * z + -1 * (z + 1) + -1 * (z + 1) * z = 0
⊢ z + 1 + z ^ 2 = 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Selmer

Goal state before:
pp: n : ℕ
hn1 : n ≠ 1
⊢ Irreducible (X ^ n - X - 1)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Selmer

Goal state before:
pp: n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
⊢ X ^ n - X - 1 = trinomial 0 1 n (-1) (-1) 1

Tactic:
by

Goal state after: