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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
n : ℕ
⊢ (p ^ n).natDegree = n * p.natDegree

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin n →₀ ℕ
⊢ m ∈ (((finSuccEquiv R n) f).coeff i).support ↔ cons i m ∈ f.support

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
n : ℕ
r : R
⊢ ((X + C r) ^ n).natDegree = n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
hi : ((finSuccEquiv R n) f).coeff i ≠ 0
⊢ (((finSuccEquiv R n) f).coeff i).support.Nonempty

Tactic:
by

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

Goal state before:
pp: ι : Type w
S : Type u_1
inst✝ : Semiring S
f : ι → S[X]
s : Finset ι
d : WithBot ℕ
hd : ∀ k ∈ s, (f k).degree = d
hf : ∑ k ∈ s, (f k).leadingCoeff ≠ 0
⊢ (∑ k ∈ s, f k).leadingCoeff = ∑ k ∈ s, (f k).leadingCoeff

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
hm : p.Monic
hpu : IsUnit p
⊢ p = 1

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
hp : p.Monic
hq : q.Monic
hpq : Associated p q
⊢ p = q

Tactic:
by

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

Goal state before:
pp: R : Type u
n : ℕ
inst✝¹ : Semiring R
inst✝ : Nontrivial R
p : MonicDegreeEq R n
⊢ (↑p).coeff n ≠ 0

Tactic:
by

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

Goal state before:
pp: S : Type u_1
inst✝ : Semiring S
l : List S[X]
n : WithBot ℕ
hl : ∀ p ∈ l, p.degree ≤ n
⊢ l.sum.degree ≤ n

Tactic:
by

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

Goal state before:
pp: R : Type u
n : ℕ
inst✝ : Semiring R
p : MonicDegreeEq R n
⊢ (↑p).Monic

Tactic:
by

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

Goal state before:
pp: R : Type u
n : ℕ
inst✝ : Semiring R
p : MonicDegreeEq R n
i : ℕ
hi : n ≤ i
⊢ (↑p).coeff i = if i = n then 1 else 0

Tactic:
by

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

Goal state before:
pp: R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝¹ : Semiring R
p✝ q r : R[X]
inst✝ : Semiring S
p : R[X]
hp : p.Monic
hp' : p.natDegree = n
⊢ p.coeff n = 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
hi : ((finSuccEquiv R n) f).coeff i ≠ 0
⊢ (((finSuccEquiv R n) f).coeff i).totalDegree + i ≤ f.totalDegree

Tactic:
by

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

Goal state before:
pp: R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝¹ : Semiring R
p✝ q r : R[X]
inst✝ : Semiring S
p : MonicDegreeEq R n
f : R →+* S
⊢ (Polynomial.map f ↑p).coeff n = 1 ∧ ∀ i > n, (Polynomial.map f ↑p).coeff i = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
m : Fin (n + 1) →₀ ℕ
h : ¬coeff m f = 0
⊢ ¬coeff (cons (m 0) m.tail) f = 0

Tactic:
by

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

Goal state before:
pp: S : Type u_1
inst✝ : Semiring S
l : List S[X]
⊢ l.sum.degree ≤ (List.map natDegree l).maximum

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
⊢ ((finSuccEquiv R n) f).support = Finset.image (fun m ↦ m 0) f.support

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
x : ℕ
⊢ x ∈ ((finSuccEquiv R n) f).support ↔ x ∈ (fun m ↦ m 0) '' ↑f.support

Tactic:
by

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

Goal state before:
pp: R : Type u
ι : Type y
inst✝ : CommSemiring R
t : Multiset ι
f : ι → R[X]
ht : ∀ i ∈ t, (f i).Monic
⊢ (Multiset.map f t).prod.Monic

Tactic:
by

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

Goal state before:
pp: case pos
R : Type u
inst✝ : CommSemiring R
α : Type u_1
f : α → R[X]
hf : ∀ i ∈ Function.mulSupport f, (f i).Monic
h✝ : Function.HasFiniteMulSupport f
⊢ (∏ i ∈ Set.Finite.toFinset h✝, f i).Monic

pp: case neg
R : Type u
inst✝ : CommSemiring R
α : Type u_1
f : α → R[X]
hf : ∀ i ∈ Function.mulSupport f, (f i).Monic
h✝ : ¬Function.HasFiniteMulSupport f
⊢ Monic 1

Tactic:
· exact monic_prod_of_monic _ _ fun a ha => hf a ((Set.Finite.mem_toFinset _).mp ha)

Goal state after:
case neg
R : Type u
inst✝ : CommSemiring R
α : Type u_1
f : α → R[X]
hf : ∀ i ∈ Function.mulSupport f, (f i).Monic
h✝ : ¬Function.HasFiniteMulSupport f
⊢ Monic 1
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
α : Type u_1
f : α → R[X]
hf : ∀ i ∈ Function.mulSupport f, (f i).Monic
⊢ (finprod f).Monic

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
⊢ Finset.image (cons i) (((finSuccEquiv R n) f).coeff i).support = {m ∈ f.support | m 0 = i}

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
x : Fin (n + 1) →₀ ℕ
⊢ x ∈ cons i '' ↑(((finSuccEquiv R n) f).coeff i).support ↔ x ∈ f.support ∧ x 0 = i

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
h : f ≠ 0
⊢ ((finSuccEquiv R n) f).support.Nonempty

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
h : f ≠ 0
h₀ : ∀ {α : Type ?u.39} {β : Type ?u.41} (f : α → β), (fun x ↦ x) ∘ f = f
h₁ : ∀ {α : Type ?u.55} {β : Type ?u.57} (f : α → β), (f ∘ fun x ↦ x) = f
⊢ (((finSuccEquiv R n) f).support.sup fun x ↦ x) = degreeOf 0 f

Tactic:
by

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

Goal state before:
pp: R : Type u
ι : Type y
inst✝ : CommSemiring R
t : Multiset ι
f : ι → R[X]
h : ∀ i ∈ t, (f i).Monic
⊢ (Multiset.map f t).prod.nextCoeff = (Multiset.map (fun i ↦ (f i).nextCoeff) t).sum

Tactic:
by

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

Goal state before:
pp: S : Type u_1
inst✝ : Semiring S
n : ℕ
hd : S[X]
tl : List S[X]
IH : (∀ p ∈ tl, p.natDegree ≤ n) → tl.prod.coeff (tl.length * n) = (List.map (fun p ↦ p.coeff n) tl).prod
hl : ∀ p ∈ hd :: tl, p.natDegree ≤ n
hl' : ∀ p ∈ tl, p.natDegree ≤ n
⊢ tl.prod.natDegree ≤ n * tl.length

Tactic:
by

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

Goal state before:
pp: S : Type u_1
inst✝ : Semiring S
l : List S[X]
n : ℕ
hl : ∀ p ∈ l, p.natDegree ≤ n
⊢ l.prod.coeff (l.length * n) = (List.map (fun p ↦ p.coeff n) l).prod

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
t : Multiset R[X]
⊢ ∀ (a : List R[X]), (prod ⟦a⟧).natDegree ≤ (Multiset.map natDegree ⟦a⟧).sum

Tactic:
by

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

Goal state before:
pp: R : Type u
ι : Type w
s : Finset ι
inst✝ : CommSemiring R
f : ι → R[X]
⊢ (∏ 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
t : Multiset R[X]
⊢ ∀ (a : List R[X]), (prod ⟦a⟧).degree ≤ (Multiset.map degree ⟦a⟧).sum

Tactic:
by

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

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

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
h : f ≠ 0
⊢ ((finSuccEquiv R n) f).degree = ↑(degreeOf 0 f)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝³ : Semiring R
S : Type u_2
F : Type u_3
inst✝² : Semiring S
inst✝¹ : FunLike F R[X] S[X]
inst✝ : AddMonoidHomClass F R[X] S[X]
φ : F
p : R[X]
k : ℕ
fu : ℕ → ℕ
fu0 : ∀ {n : ℕ}, n ≤ k → fu n = 0
fc : ∀ {n m : ℕ}, k ≤ n → n < m → fu n < fu m
φ_k : ∀ {f : R[X]}, f.natDegree < k → φ f = 0
φ_mon_nat : ∀ (n : ℕ) (c : R), c ≠ 0 → (φ ((monomial n) c)).natDegree = fu n
⊢ (φ p).natDegree = fu p.natDegree

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝³ : Semiring R
S : Type u_2
F : Type u_3
inst✝² : Semiring S
inst✝¹ : FunLike F R[X] S[X]
inst✝ : AddMonoidHomClass F R[X] S[X]
φ : F
p : R[X]
k : ℕ
φ_k : ∀ (f : R[X]), f.natDegree < k → φ f = 0
φ_mon : ∀ (n : ℕ) (c : R), c ≠ 0 → (φ ((monomial n) c)).natDegree = n - k
⊢ ∀ {n : ℕ}, n ≤ k → n - k = 0

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝³ : Semiring R
S : Type u_2
F : Type u_3
inst✝² : Semiring S
inst✝¹ : FunLike F R[X] S[X]
inst✝ : AddMonoidHomClass F R[X] S[X]
φ : F
p : R[X]
φ_mon_nat : ∀ (n : ℕ) (c : R), c ≠ 0 → (φ ((monomial n) c)).natDegree = n
⊢ ∀ (n : ℕ) (c : R), c ≠ 0 → (φ ((monomial n) c)).natDegree = n - 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
⊢ ((finSuccEquiv R n) f).natDegree = degreeOf 0 f

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
a : σ
p : MvPolynomial σ R
⊢ degreeOf a p = ((optionEquivLeft R { b // b ≠ a }) ((rename ⇑(Equiv.optionSubtypeNe a).symm) p)).natDegree

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
n : ℕ
k : Fin n → ℕ
x : Fin n → R
hk : Function.Injective k
hx : ∀ (i : Fin n), x i ≠ 0
this : (∑ i, C (x i) * X ^ k i).support = image k univ
⊢ #(∑ i, C (x i) * X ^ k i).support = n

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
t : Multiset R[X]
h : (Multiset.map leadingCoeff t).prod ≠ 0
⊢ t.prod.leadingCoeff = (Multiset.map 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
f : ι → R[X]
h : ∏ i ∈ s, (f i).leadingCoeff ≠ 0
⊢ (Multiset.map leadingCoeff (Multiset.map f s.val)).prod ≠ 0

Tactic:
by

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

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

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
n : ℕ
p : MvPolynomial (Fin (n + 1)) R
j : Fin n
i : ℕ
⊢ degreeOf j (((finSuccEquiv R n) p).coeff i) ≤ degreeOf j.succ p

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]
hp : p.Monic
hp1 : p ≠ 1
⊢ Irreducible p ↔ ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → f = 1 ∨ g = 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
n : ℕ
e : σ ≃ Fin n
φ : MvPolynomial (Option σ) R
this :
  (finSuccEquiv R n).toRingEquiv.toRingHom.comp (rename ⇑(e.optionCongr.trans (_root_.finSuccEquiv n).symm)).toRingHom =
    (Polynomial.mapRingHom (rename ⇑e).toRingHom).comp ↑(optionEquivLeft R σ)
⊢ (finSuccEquiv R n) ((rename ⇑(e.optionCongr.trans (_root_.finSuccEquiv n).symm)) φ) =
    Polynomial.map (rename ⇑e).toRingHom ((optionEquivLeft R σ) φ)

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]
hp : p.Monic
⊢ Irreducible p ↔ p ≠ 1 ∧ ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → f.natDegree = 0 ∨ g.natDegree = 0

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
t : Multiset R[X]
h : (Multiset.map (fun f ↦ f.leadingCoeff) t).prod ≠ 0
⊢ t.prod.natDegree = (Multiset.map (fun f ↦ f.natDegree) t).sum

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
n : ℕ
k : Fin n → ℕ
x : Fin n → R
hk : Function.Injective k
hx : ∀ (i : Fin n), x i ≠ 0
⊢ #(∑ i, C (x i) * X ^ k i).support = n

Tactic:
by

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

Goal state before:
pp: R : Type u
ι : Type w
s : Finset ι
inst✝ : CommSemiring R
f : ι → R[X]
h : ∏ i ∈ s, (f i).leadingCoeff ≠ 0
⊢ (Multiset.map (fun f ↦ f.leadingCoeff) (Multiset.map f s.val)).prod ≠ 0

Tactic:
by

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

Goal state before:
pp: R : Type u
ι : Type w
s : Finset ι
inst✝ : CommSemiring R
f : ι → R[X]
h : ∏ i ∈ s, (f i).leadingCoeff ≠ 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
t : Multiset R[X]
h : ∀ f ∈ t, f.Monic
⊢ t.prod.natDegree = (Multiset.map natDegree t).sum

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
n : ℕ
e : σ ≃ Fin n
φ : MvPolynomial (Option σ) R
⊢ (finSuccEquiv R n) ((rename ⇑(e.optionCongr.trans (_root_.finSuccEquiv n).symm)) φ) =
    Polynomial.map (rename ⇑e).toRingHom ((optionEquivLeft R σ) φ)

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
t : Multiset R[X]
inst✝ : Nontrivial R
h : ∀ f ∈ t, f.Monic
⊢ t.prod.Monic

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
n : ℕ
hn : ∀ {f : R[X]}, #f.support = n → ∃ k x, ∃ (_ : StrictMono k) (_ : ∀ (i : Fin n), x i ≠ 0), f = ∑ i, C (x i) * X ^ k i
f : R[X]
h : #f.support = n + 1
k : Fin n → ℕ
x : Fin n → R
hk : StrictMono k
hx : ∀ (i : Fin n), x i ≠ 0
hf : f.eraseLead = ∑ i, C (x i) * X ^ k i
⊢ ¬∃ k, k.castSucc = Fin.last n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
σ : Type u_2
τ : Type u_3
f : σ → τ
i : σ
p : R[X]
⊢ (rename f) ((Polynomial.aeval (X i)) p) = (Polynomial.aeval (X (f i))) p

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: R : Type u_1
σ : Type u_3
inst✝ : CommSemiring R
i : σ
r : R
⊢ (toMvPolynomial i) (C r) = MvPolynomial.C r

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: R : Type u_1
σ : Type u_3
inst✝ : CommSemiring R
i : σ
⊢ (toMvPolynomial i) X = MvPolynomial.X i

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: R : Type u_1
σ : Type u_3
inst✝ : CommSemiring R
i : σ
⊢ toMvPolynomial i = (MvPolynomial.rename fun x ↦ i).comp ↑(MvPolynomial.uniqueAlgEquiv R Unit).symm

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
t : Multiset R[X]
inst✝ : Nontrivial R
h : ∀ f ∈ t, f.Monic
⊢ t.prod.degree = (Multiset.map degree t).sum

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: R : Type u_1
σ : Type u_3
inst✝ : CommSemiring R
i : σ
⊢ Injective ⇑(toMvPolynomial i)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: R : Type u_1
σ : Type u_3
inst✝ : CommSemiring R
i : σ
p q : R[X]
h : p = q
⊢ (toMvPolynomial i) p = (toMvPolynomial i) q

Tactic:
by

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

Goal state before:
pp: R : Type u
ι : Type w
s : Finset ι
inst✝ : CommSemiring R
f : ι → R[X]
h : ∀ i ∈ s, (f i).Monic
⊢ ∀ f_1 ∈ Multiset.map f s.val, f_1.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
f : ι → R[X]
h : ∀ i ∈ s, (f i).Monic
⊢ (∏ i ∈ s, f i).natDegree = ∑ i ∈ s, (f i).natDegree

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: R : Type u_1
σ : Type u_3
inst✝ : CommSemiring R
f : σ → R
i : σ
⊢ (eval f).comp ↑(toMvPolynomial i) = evalRingHom (f i)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
n : ℕ
hn : ∀ {f : R[X]}, #f.support = n → ∃ k x, ∃ (_ : StrictMono k) (_ : ∀ (i : Fin n), x i ≠ 0), f = ∑ i, C (x i) * X ^ k i
f : R[X]
h : #f.support = n + 1
k : Fin n → ℕ
x : Fin n → R
hk : StrictMono k
hx : ∀ (i : Fin n), x i ≠ 0
hf : f.eraseLead = ∑ i, C (x i) * X ^ k i
H : ¬∃ k, k.castSucc = Fin.last n
i j : Fin (n + 1)
hij : i < j
⊢ i ∈ Set.range Fin.castSucc

Tactic:
by

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

Goal state before:
pp: R : Type u
ι : Type w
s : Finset ι
inst✝¹ : CommSemiring R
f : ι → R[X]
inst✝ : Nontrivial R
h : ∀ i ∈ s, (f i).Monic
⊢ ∀ f_1 ∈ Multiset.map f s.val, f_1.Monic

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: R : Type u_1
S : Type u_2
σ : Type u_3
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
f : σ → S
i : σ
⊢ (aeval f).comp (toMvPolynomial i) = Polynomial.aeval (f i)

Tactic:
by

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

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

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: R : Type u_1
σ : Type u_3
τ : Type u_4
inst✝ : CommSemiring R
f : σ → τ
a : σ
⊢ (rename f).comp (toMvPolynomial a) = toMvPolynomial (f a)

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
t : Multiset R[X]
n : ℕ
hl : ∀ p ∈ t, p.natDegree ≤ n
⊢ t.prod.coeff (t.card * n) = (Multiset.map (fun p ↦ p.coeff n) t).prod

Tactic:
by

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

Goal state before:
pp: R : Type u
ι : Type w
inst✝ : CommSemiring R
f : ι → R[X]
n : ℕ
l : Multiset ι
hl : l.Nodup
h : ∀ p ∈ { val := l, nodup := hl }, (f p).natDegree ≤ n
⊢ (∏ i ∈ { val := l, nodup := hl }, f i).coeff (#{ val := l, nodup := hl } * n) =
    ∏ i ∈ { val := l, nodup := hl }, (f i).coeff n

Tactic:
convert! coeff_multiset_prod_of_natDegree_le (l.map f) n ?_

Goal state after:
case e'_2.e'_4
R : Type u
ι : Type w
inst✝ : CommSemiring R
f : ι → R[X]
n : ℕ
l : Multiset ι
hl : l.Nodup
h : ∀ p ∈ { val := l, nodup := hl }, (f p).natDegree ≤ n
⊢ #{ val := l, nodup := hl } = (Multiset.map f l).card

case e'_3
R : Type u
ι : Type w
inst✝ : CommSemiring R
f : ι → R[X]
n : ℕ
l : Multiset ι
hl : l.Nodup
h : ∀ p ∈ { val := l, nodup := hl }, (f p).natDegree ≤ n
⊢ ∏ i ∈ { val := l, nodup := hl }, (f i).coeff n = (Multiset.map (fun p ↦ p.coeff n) (Multiset.map f l)).prod

R : Type u
ι : Type w
inst✝ : CommSemiring R
f : ι → R[X]
n : ℕ
l : Multiset ι
hl : l.Nodup
h : ∀ p ∈ { val := l, nodup := hl }, (f p).natDegree ≤ n
⊢ ∀ p ∈ Multiset.map f l, p.natDegree ≤ n
Module: Mathlib.Algebra.Ring.GeomSum

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

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
x : R
⊢ ∑ i ∈ range 1, x ^ i = 1

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
x : R
⊢ ∑ i ∈ range 2, x ^ i = x + 1

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
⊢ ∑ i ∈ range 0, 0 ^ i = if 0 = 0 then 0 else 1

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
⊢ ∑ i ∈ range 1, 0 ^ i = if 1 = 0 then 0 else 1

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
n : ℕ
⊢ ∑ i ∈ range n, 1 ^ i = ↑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 : ℕ
⊢ op (∑ i ∈ range n, x ^ i) = ∑ i ∈ range n, op x ^ 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
n : ℕ
⊢ ∑ i ∈ range n, op y ^ (n - 1 - i) * op x ^ i = ∑ i ∈ range n, op y ^ i * op x ^ (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 i : ℕ
x✝ : i ∈ range n
⊢ x ^ i * 1 ^ (n - 1 - i) = x ^ i

Tactic:
by

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

Goal state before:
pp: R : Type u
ι : Type w
s : Finset ι
inst✝ : CommSemiring R
f : ι → R[X]
n : ℕ
h : ∀ p ∈ s, (f p).natDegree ≤ n
⊢ (∏ i ∈ s, f i).coeff (#s * n) = ∏ i ∈ s, (f i).coeff 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
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 (n + 1) n = (x + y) ^ n

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
f g : R[X]
hf : f.Monic
hg : g.Monic
hp : (f * g).Monic
h : f.natDegree ≠ 0 ∧ g.natDegree ≠ 0
hl : f.natDegree ≤ g.natDegree
⊢ f.natDegree + f.natDegree ≤ f.natDegree + g.natDegree

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
f g : R[X]
hf : f.Monic
hg : g.Monic
hp : (f * g).Monic
h : f.natDegree ≠ 0 ∧ g.natDegree ≠ 0
hl : g.natDegree ≤ f.natDegree
⊢ g.natDegree + g.natDegree ≤ f.natDegree + g.natDegree

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]
hp : p.Monic
⊢ Irreducible p ↔ p ≠ 1 ∧ ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → g.natDegree ∉ Ioc 0 (p.natDegree / 2)

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
t : Multiset R[X]
⊢ t.prod.coeff 0 = (Multiset.map (fun f ↦ f.coeff 0) 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
f : ι → R[X]
⊢ (∏ i ∈ s, f i).coeff 0 = ∏ i ∈ s, (f i).coeff 0

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
t : Multiset R
⊢ (Multiset.map (fun x ↦ X - C x) t).prod.nextCoeff = -t.sum

Tactic:
by

Goal state after: