mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hp : p.Monic
hp1 : p ≠ 1
⊢ Irreducible p ↔ ∀ (q : R[X]), q.Monic → q.natDegree ∈ Ioc 0 (p.natDegree / 2) → ¬q ∣ p

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.BigOperators

Goal state before:
pp: R : Type u
ι : Type w
inst✝ : CommRing R
s : Finset ι
f : ι → R
⊢ (∏ i ∈ s, (X - C (f i))).nextCoeff = -∑ i ∈ s, f i

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.BigOperators

Goal state before:
pp: R : Type u
inst✝ : CommRing R
t : Multiset R
ht : 0 < t.card
a✝ : Nontrivial R
⊢ Multiset ?m.52

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.GeomSum

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
f : ℕ → ℕ → R := fun m i ↦ (x + y) ^ i * y ^ (m - 1 - i)
n : ℕ
ih : (∑ i ∈ range n, f n i) * x + y ^ n = (x + y) ^ n
f_last : f (n + 1) n = (x + y) ^ n
i : ℕ
hi : i ∈ range n
⊢ f (n + 1) i = y * f n i

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.GeomSum

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
n : ℕ
⊢ (∑ i ∈ range n, (x + y) ^ i * y ^ (n - 1 - i)) * x + y ^ n = (x + y) ^ n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.GeomSum

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
x : R
n : ℕ
⊢ ∑ i ∈ range n, x ^ i * x ^ (n - 1 - i) = ∑ i ∈ range n, x ^ (i + (n - 1 - i))

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.GeomSum

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
x : R
n : ℕ
⊢ #(range n) • x ^ (n - 1) = ↑n * x ^ (n - 1)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.GeomSum

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
x : R
n : ℕ
⊢ (∑ i ∈ range n, (x + 1) ^ i) * x + 1 = (x + 1) ^ n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.GeomSum

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
x y : R
n : ℕ
h : Commute x y
⊢ ∑ i ∈ range n, x ^ i * y ^ (n - 1 - i) = ∑ i ∈ range n, y ^ i * x ^ (n - 1 - i)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.GeomSum

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : Semiring S
x : R
n : ℕ
f : R →+* S
⊢ f (∑ i ∈ range n, x ^ i) = ∑ i ∈ range n, f x ^ i

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.GeomSum

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : Semiring S
x y : R
n : ℕ
f : R →+* S
⊢ f (∑ i ∈ range n, x ^ i * y ^ (n - 1 - i)) = ∑ i ∈ range n, f x ^ i * f y ^ (n - 1 - i)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.GeomSum

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
inst✝⁵ : PartialOrder R
inst✝⁴ : AddLeftReflectLE R
inst✝³ : AddLeftMono R
inst✝² : ExistsAddOfLE R
inst✝¹ : Sub R
inst✝ : OrderedSub R
x y : R
hxy : y ≤ x
n : ℕ
⊢ (∑ i ∈ range n, x ^ i * y ^ (n - 1 - i)) * (x - y) = x ^ n - y ^ n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.GeomSum

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
inst✝⁵ : PartialOrder R
inst✝⁴ : AddLeftReflectLE R
inst✝³ : AddLeftMono R
inst✝² : ExistsAddOfLE R
inst✝¹ : Sub R
inst✝ : OrderedSub R
x y : R
hxy : x ≤ y
n : ℕ
⊢ (∑ i ∈ range n, x ^ i * y ^ (n - 1 - i)) * (y - x) = y ^ n - x ^ n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.BigOperators

Goal state before:
pp: R : Type u
inst✝ : CommRing R
t : Multiset R
ht : 0 < t.card
⊢ (Multiset.map (fun x ↦ X - C x) t).prod.coeff (t.card - 1) = -t.sum

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.GeomSum

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
inst✝⁵ : PartialOrder R
inst✝⁴ : AddLeftReflectLE R
inst✝³ : AddLeftMono R
inst✝² : ExistsAddOfLE R
inst✝¹ : Sub R
inst✝ : OrderedSub R
x : R
hx : 1 ≤ x
n : ℕ
⊢ (∑ i ∈ range n, x ^ i) * (x - 1) = x ^ n - 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.GeomSum

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
inst✝⁵ : PartialOrder R
inst✝⁴ : AddLeftReflectLE R
inst✝³ : AddLeftMono R
inst✝² : ExistsAddOfLE R
inst✝¹ : Sub R
inst✝ : OrderedSub R
x : R
hx : x ≤ 1
n : ℕ
⊢ (∑ i ∈ range n, x ^ i) * (1 - x) = 1 - x ^ n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.BigOperators

Goal state before:
pp: R : Type u
ι : Type w
inst✝ : CommRing R
s : Finset ι
f : ι → R
hs : 0 < #s
⊢ 0 < (Multiset.map f s.val).card

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.BigOperators

Goal state before:
pp: R : Type u
ι : Type w
inst✝ : CommRing R
s : Finset ι
f : ι → R
hs : 0 < #s
⊢ (∏ i ∈ s, (X - C (f i))).coeff (#s - 1) = -∑ i ∈ s, f i

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hm : p.Monic
hnd : p.natDegree = 2
⊢ ¬Irreducible p ↔ ∃ c₁ c₂, p.coeff 0 = c₁ * c₂ ∧ p.coeff 1 = c₁ + c₂

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.GeomSum

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
n : ℕ
⊢ ∑ i ∈ range n, (-1) ^ i = if Even n then 0 else 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: R : Type u
S : Type v
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : Nontrivial S
P : R[X]
hmo : P.Monic
f : R →+* S
⊢ (Polynomial.map f P).natDegree = P.natDegree

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: R : Type u
S : Type v
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : Nontrivial S
P : R[X]
hmo : P.Monic
f : R →+* S
⊢ (Polynomial.map f P).degree = P.degree

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
hf : Injective ⇑f
p : R[X]
hp : (map f p).Monic
⊢ p.Monic

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: R : Type u
inst✝ : Ring R
x : R
⊢ (X - C x).Monic

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: R : Type u
inst✝ : Ring R
p : R[X]
n : ℕ
H : p.degree < ↑n
⊢ (X ^ n - p).Monic

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: R : Type u
inst✝ : Ring R
a : R
n : ℕ
h : n ≠ 0
⊢ (X ^ n - C a).Monic

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.GeomSum

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
x y : R
h : Commute x y
n : ℕ
⊢ (∑ i ∈ range n, x ^ i * y ^ (n - 1 - i)) * (x - y) = x ^ n - y ^ n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.GeomSum

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
x y : R
h : Commute x y
n : ℕ
⊢ (y - x) * ∑ i ∈ range n, x ^ i * y ^ (n - 1 - i) = y ^ n - x ^ n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
inst✝ : Nontrivial R
n : ℕ
⊢ ¬IsUnit (X ^ n - 1)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: R : Type u
inst✝ : Ring R
p : R[X]
hp : p.Monic
r : R
⊢ (p.comp (X - C r)).Monic

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.GeomSum

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
x y : R
h : Commute x y
n : ℕ
⊢ (x - y) * ∑ i ∈ range n, x ^ i * y ^ (n - 1 - i) = x ^ n - y ^ n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
hp : p.Monic
hpq : q.degree < p.degree
⊢ (p - q).Monic

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.GeomSum

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
x : R
n : ℕ
⊢ 1 - x ∣ 1 - x ^ n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
hq : q.leadingCoeff = -1
hpq : p.degree < q.degree
⊢ (-q).coeff (-q).natDegree = 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.GeomSum

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
x : R
n : ℕ
⊢ x - 1 ∣ x ^ n - 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.GeomSum

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
x : R
m n : ℕ
⊢ x ^ m - 1 ∣ x ^ (m * n) - 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.GeomSum

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
r : R
a b : ℕ
h : a ∣ b
⊢ r ^ a - 1 ∣ r ^ b - 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
hq : q.leadingCoeff = -1
hpq : p.degree < q.degree
⊢ (p - q).Monic

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.GeomSum

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Ring R
r : R
p a b : ℕ
h : a ∣ b
hp₀ : p = 0
hb₀ : b = 0
⊢ r ^ p ^ a - r ∣ r ^ p ^ b - r

pp: case neg
R : Type u_1
inst✝ : Ring R
r : R
p a b : ℕ
h : a ∣ b
hp₀ : p = 0
hb₀ : ¬b = 0
⊢ r ^ p ^ a - r ∣ r ^ p ^ b - r

Tactic:
· rw [hp₀, hb₀, pow_zero, pow_one, sub_self]
      exact dvd_zero _

Goal state after:
case neg
R : Type u_1
inst✝ : Ring R
r : R
p a b : ℕ
h : a ∣ b
hp₀ : p = 0
hb₀ : ¬b = 0
⊢ r ^ p ^ a - r ∣ r ^ p ^ b - r
Module: Mathlib.Algebra.Ring.GeomSum

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
r : R
p a b : ℕ
h : a ∣ b
hp₀ : p = 0
hb₀ : ¬b = 0
⊢ a ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
q : R[X]
hq : q ≠ 0
⊢ q * p ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
q : R[X]
hq : q ≠ 0
⊢ p * q ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.BigOperators

Goal state before:
pp: R : Type u
ι : Type w
s : Finset ι
inst✝² : CommRing R
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : ι → R[X]
v : ι → A
h : LinearIndepOn R v ↑s
⊢ (∑ i ∈ s, v i • map (algebraMap R A) (f i)).degree = s.sup fun i ↦ (f i).degree

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
h : p.Monic
q : R[X]
hq : q = 0
this : 0 < p.natDegree ↔ p.natDegree ≠ 0
⊢ (p * q).natDegree < p.natDegree ↔ p ≠ 1 ∧ q = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.GeomSum

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
r : R
p a b : ℕ
h : a ∣ b
⊢ r ^ p ^ a - r ∣ r ^ p ^ b - r

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
h : p.Monic
q : R[X]
⊢ (p * q).natDegree < p.natDegree ↔ p ≠ 1 ∧ q = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
h : p.Monic
q : R[X]
⊢ p * q = 0 ↔ q = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
h : p.Monic
q : R[X]
⊢ q * p = 0 ↔ q = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.GeomSum

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
x : R
n : ℕ
⊢ (∑ i ∈ range n, x ^ i) * (x - 1) = x ^ n - 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.GeomSum

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
x : R
n : ℕ
⊢ op ((x - 1) * ∑ i ∈ range n, x ^ i) = op (x ^ n - 1)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
p : R[X]
hp : p.Monic
⊢ IsRegular p

Tactic:
constructor
  · intro q r h
    dsimp only at h
    rw [← sub_eq_zero, ← hp.mul_right_eq_zero_iff, mul_sub, h, sub_self]
  · intro q r h
    simp only at h
    rw [← sub_eq_zero, ← hp.mul_left_eq_zero_iff, sub_mul, h, sub_self]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
p : R[X]
hp : p.Monic
⊢ IsRegular p

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.GeomSum

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
x : R
n : ℕ
⊢ (∑ i ∈ range n, x ^ i) * (1 - x) = 1 - x ^ n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.GeomSum

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
x : R
n : ℕ
⊢ op ((1 - x) * ∑ i ∈ range n, x ^ i) = op (1 - x ^ n)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.BigOperators

Goal state before:
pp: R : Type u
ι : Type w
s : Finset ι
inst✝² : CommRing R
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : ι → R[X]
v : ι → A
h : LinearIndepOn R v ↑s
⊢ (∑ i ∈ s, v i • map (algebraMap R A) (f i)).natDegree = s.sup fun i ↦ (f i).natDegree

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
S : Type u_1
inst✝ : SMulZeroClass S R
k : S
p : R[X]
h : IsSMulRegular R k
⊢ (k • p).degree = p.degree

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.BigOperators

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : Nontrivial R
s : Multiset R
⊢ (Multiset.map (fun x ↦ X - C x) s).prod.natDegree = s.card

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.BigOperators

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : Nontrivial R
α : Type u_1
s : Finset α
f : α → R
⊢ (∏ a ∈ s, (X - C (f a))).natDegree = #s

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
S : Type u_1
inst✝ : SMulZeroClass S R
k : S
p : R[X]
h : IsSMulRegular R k
⊢ (k • p).natDegree = p.natDegree

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
S : Type u_1
inst✝ : SMulZeroClass S R
k : S
p : R[X]
h : IsSMulRegular R k
⊢ (k • p).leadingCoeff = k • p.leadingCoeff

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.GeomSum

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
x y : R
h : Commute x y
m n : ℕ
hmn : m ≤ n
⊢ ∑ k ∈ range m, x ^ k * y ^ (n - 1 - k) = ∑ k ∈ range m, x ^ k * (y ^ (n - m) * y ^ (m - 1 - k))

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
h : IsUnit p.leadingCoeff
⊢ (h.unit⁻¹ • p).Monic

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.BigOperators

Goal state before:
pp: R : Type u
ι : Type w
s : Finset ι
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
f : ι → R[X]
h : ∀ i ∈ s, f i ≠ 0
⊢ (∏ i ∈ s, f i).natDegree = ∑ i ∈ s, (f i).natDegree

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.BigOperators

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
t : Multiset R[X]
h : 0 ∉ t
⊢ t.prod.natDegree = (Multiset.map natDegree t).sum

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
h : IsUnit p.leadingCoeff
q : R[X]
hp : h.unit⁻¹ • (p * q) = 0
⊢ h.unit⁻¹ • (p * q) = h.unit⁻¹ • p * q

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: case mp
R : Type u
inst✝ : Semiring R
p : R[X]
h : IsUnit p.leadingCoeff
q : R[X]
hp : h.unit⁻¹ • (p * q) = 0
⊢ q = 0

Tactic:
have : h.unit⁻¹ • (p * q) = h.unit⁻¹ • p * q := by
      ext
      simp only [Units.smul_def, coeff_smul, coeff_mul, smul_eq_mul, mul_sum]
      refine sum_congr rfl fun x _ => ?_
      rw [← mul_assoc]

Goal state after:
case mp
R : Type u
inst✝ : Semiring R
p : R[X]
h : IsUnit p.leadingCoeff
q : R[X]
hp : h.unit⁻¹ • (p * q) = 0
this : h.unit⁻¹ • (p * q) = h.unit⁻¹ • p * q
⊢ q = 0
Module: Mathlib.Algebra.Polynomial.BigOperators

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
t : Multiset R[X]
⊢ t.prod.leadingCoeff = (Multiset.map (fun f ↦ f.leadingCoeff) t).prod

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.BigOperators

Goal state before:
pp: R : Type u
ι : Type w
s : Finset ι
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
f : ι → R[X]
⊢ (∏ i ∈ s, f i).leadingCoeff = ∏ i ∈ s, (f i).leadingCoeff

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
h : IsUnit p.leadingCoeff
q : R[X]
⊢ p * q = 0 ↔ q = 0

Tactic:
by

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

Goal state before:
pp: R : Type u
S : Type u_1
inst✝ : Semiring R
p : ℕ
h✝ : CharP R p
h : ∀ (x : ℕ), ↑x = 0 ↔ p ∣ x
n : ℕ
⊢ ↑n = 0 ↔ p ∣ n

Tactic:
by

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

Goal state before:
pp: R : Type u
S : Type u_1
inst✝ : Semiring R
p : ℕ
h : ExpChar R p
⊢ ExpChar R[X] p

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
n : WithBot ℕ
f : R[X]
⊢ f ∈ degreeLE R n ↔ f.degree ≤ n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
h : IsUnit p.leadingCoeff
q : R[X]
⊢ q * p = 0 ↔ q = 0

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n : ℕ
⊢ degreeLE R ↑n = Submodule.span R ↑(image (fun n ↦ X ^ n) (range (n + 1)))

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
n : ℕ
f : R[X]
⊢ f ∈ degreeLT R n ↔ f.degree < ↑n

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
n : ℕ
i : Fin n
a : R
⊢ ↑↑i < ↑n

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Adjoin.FG

Goal state before:
pp: R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : (Subalgebra.toSubmodule (adjoin R s)).FG
h2 : (Subalgebra.toSubmodule (adjoin (↥(adjoin R s)) t)).FG
p : Set A
hp : p.Finite
hp' : span R p = Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : q.Finite
hq' : span (↥(adjoin R s)) q = Subalgebra.toSubmodule (adjoin (↥(adjoin R s)) t)
x : A
hx : x ∈ p
y : A
hy : y ∈ q
⊢ x ∈ Subalgebra.toSubmodule (adjoin R s)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
n : ℕ
⊢ #f.support = n ↔ ∃ k x, ∃ (_ : StrictMono k) (_ : ∀ (i : Fin n), x i ≠ 0), f = ∑ i, C (x i) * X ^ k i

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n : ℕ
p : R[X]
hp : p.degree < ↑n
k : ℕ
hk : k ∈ p.support
this : k < n
⊢ X ^ k ∈ ↑(image (fun n ↦ X ^ n) (range n))

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n : ℕ
⊢ degreeLT R n = Submodule.span R ↑(image (fun n ↦ X ^ n) (range n))

Tactic:
by

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

Goal state before:
pp: R : Type u
S : Type u_1
inst✝ : Semiring R
n : ℕ
p q : ↥(degreeLT R n)
⊢ (fun n_1 ↦ (↑(p + q)).coeff ↑n_1) = (fun n_1 ↦ (↑p).coeff ↑n_1) + fun n_1 ↦ (↑q).coeff ↑n_1

Tactic:
by

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

Goal state before:
pp: R : Type u
S : Type u_1
inst✝ : Semiring R
n : ℕ
x : R
p : ↥(degreeLT R n)
⊢ (fun n_1 ↦ (↑(x • p)).coeff ↑n_1) = (RingHom.id R) x • fun n_1 ↦ (↑p).coeff ↑n_1

Tactic:
by

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

Goal state before:
pp: R : Type u
S : Type u_1
inst✝ : Semiring R
n : ℕ
x✝ : ↥(degreeLT R n)
p : R[X]
hp : p ∈ degreeLT R n
⊢ ∀ (i : ℕ), (monomial i) 0 = 0

Tactic:
by

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

Goal state before:
pp: R : Type u
S : Type u_1
inst✝ : Semiring R
n : ℕ
x✝ : ↥(degreeLT R n)
p : R[X]
hp : p ∈ degreeLT R n
⊢ (fun f ↦ ⟨∑ i, (monomial ↑i) (f i), ⋯⟩) ((fun p n_1 ↦ (↑p).coeff ↑n_1) ⟨p, hp⟩) = ⟨p, hp⟩

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Adjoin.FG

Goal state before:
pp: R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : (Subalgebra.toSubmodule (adjoin R s)).FG
h2 : (Subalgebra.toSubmodule (adjoin (↥(adjoin R s)) t)).FG
p : Set A
hp : p.Finite
hp' : span R p = Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : q.Finite
hq' : span (↥(adjoin R s)) q = Subalgebra.toSubmodule (adjoin (↥(adjoin R s)) t)
x : A
hx : x ∈ p
y : A
hy : y ∈ q
⊢ y ∈ Subalgebra.toSubmodule (adjoin (↥(adjoin R s)) t)

Tactic:
by

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

Goal state before:
pp: R : Type u
S : Type u_1
inst✝ : Semiring R
n : ℕ
f : Fin n → R
⊢ (fun p n_1 ↦ (↑p).coeff ↑n_1) ((fun f ↦ ⟨∑ i, (monomial ↑i) (f i), ⋯⟩) f) = f

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ #f.support = 1 ↔ ∃ k x, ∃ (_ : x ≠ 0), f = C x * X ^ k

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
n : ℕ
p : R[X]
hp : p ∈ degreeLT R n
⊢ (degreeLTEquiv R n) ⟨p, hp⟩ = 0 ↔ p = 0

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
n : ℕ
p : R[X]
hp : p ∈ degreeLT R n
x : R
⊢ ∀ (i : ℕ), 0 * x ^ i = 0

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
n : ℕ
p : R[X]
hp : p ∈ degreeLT R n
x : R
⊢ eval x p = ∑ i, (degreeLTEquiv R n) ⟨p, hp⟩ i * x ^ ↑i

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.GeomSum

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
x y : R
h : Commute x y
m n : ℕ
hmn : m ≤ n
⊢ (x - y) * ∑ i ∈ Ico m n, x ^ i * y ^ (n - 1 - i) = x ^ n - x ^ m * y ^ (n - m)

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
n : ℕ
x : R[X]
x_zero : ¬x = 0
⊢ x ≠ 0

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
n : ℕ
⊢ degreeLT R (n + 1) = degreeLE R ↑n

Tactic:
by

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

Goal state before:
pp: R : Type u
S : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
n : ℕ
p : { p // p.Monic ∧ p.natDegree = n }
⊢ (↑p).eraseLead ∈ degreeLT R n

Tactic:
by

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

Goal state before:
pp: R : Type u
S : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
n : ℕ
p : ↥(degreeLT R n)
⊢ (X ^ n + ↑p).natDegree = n

Tactic:
by

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

Goal state before:
pp: R : Type u
S : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
p : R[X]
hp : p.Monic
⊢ ↑((fun p_1 ↦ ⟨X ^ p.natDegree + ↑p_1, ⋯⟩) ((fun p_1 ↦ ⟨(↑p_1).eraseLead, ⋯⟩) ⟨p, ⋯⟩)) = ↑⟨p, ⋯⟩

Tactic:
simp only

Goal state after:
R : Type u
S : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
p : R[X]
hp : p.Monic
⊢ X ^ p.natDegree + p.eraseLead = p
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
S : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
n : ℕ
⊢ Function.LeftInverse (fun p ↦ ⟨X ^ n + ↑p, ⋯⟩) fun p ↦ ⟨(↑p).eraseLead, ⋯⟩

Tactic:
by

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

Goal state before:
pp: R : Type u
S : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
n : ℕ
p : R[X]
hp : p ∈ degreeLT R n
⊢ ↑((fun p ↦ ⟨(↑p).eraseLead, ⋯⟩) ((fun p ↦ ⟨X ^ n + ↑p, ⋯⟩) ⟨p, hp⟩)) = ↑⟨p, hp⟩

Tactic:
simp only

Goal state after:
R : Type u
S : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
n : ℕ
p : R[X]
hp : p ∈ degreeLT R n
⊢ (X ^ n + p).eraseLead = p
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ #f.support = 2 ↔ ∃ k m, ∃ (_ : k < m), ∃ x y, ∃ (_ : x ≠ 0) (_ : y ≠ 0), f = C x * X ^ k + C y * X ^ m

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.GeomSum

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
x y : R
h : Commute x y
n i : ℕ
hi : i ∈ range n
this : n - 1 - i + 1 = n - i
⊢ x ^ i * y ^ (n - i) = x ^ i * y ^ (n - 1 - i + 1)

Tactic:
by

Goal state after: