mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: R : Type u
S₁ : Type v
inst✝ : CommSemiring R
s : S₁ → R
y : R
f : MvPolynomial (Option S₁) R
⊢ (eval fun x ↦ x.elim y s) f = Polynomial.eval y (Polynomial.map (eval s) ((optionEquivLeft R S₁) f))

Tactic:
by
  -- turn this into a def `Polynomial.mapAlgHom`
  let φ : (MvPolynomial S₁ R)[X] →ₐ[R] R[X] :=
    { Polynomial.mapRingHom (eval s) with
      commutes' := fun r => by
        convert! Polynomial.map_C (eval s)
        exact (eval_C _).symm }
  change
    aeval (fun x ↦ Option.elim x y s) f =
      (Polynomial.aeval y).comp (φ.comp (optionEquivLeft _ _).toAlgHom) f
  congr 2
  apply MvPolynomial.algHom_ext
  rw [Option.forall]
  simp only [aeval_X, Option.elim_none, AlgHom.coe_comp, Polynomial.coe_aeval_eq_eval,
    AlgHom.coe_mk, Polynomial.coe_mapRingHom, AlgEquiv.coe_toAlgHom, comp_apply,
    optionEquivLeft_apply, Polynomial.map_X, Polynomial.eval_X, Option.elim_some,
    Polynomial.map_C, eval_X, Polynomial.eval_C, implies_true, and_self, φ]

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
f : MvPolynomial (Option σ) R
i : ℕ
m : σ →₀ ℕ
⊢ m ∈ (((optionEquivLeft R σ) f).coeff i).support ↔ optionElim i m ∈ f.support

Tactic:
by

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial (Option σ) R
i : ℕ
m : σ →₀ ℕ
hm : ¬coeff m (((optionEquivLeft R σ) p).coeff i) = 0
⊢ ¬coeff (optionElim i m).some (((optionEquivLeft R σ) p).coeff ((optionElim i m) none)) = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
hq : 0 < q.degree
⊢ (p.comp q).degree = p.degree * q.degree

Tactic:
by

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial (Option σ) R
⊢ ((optionEquivLeft R σ) p).support = Finset.image (fun m ↦ m none) p.support

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: R : Type u
inst✝ : Ring R
p : R[X]
a✝ : Nontrivial R
hp : p ≠ 0
⊢ p.comp (-X) ≠ 0

Tactic:
by

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
f : MvPolynomial (Option σ) R
h : f ≠ 0
⊢ ((optionEquivLeft R σ) f).support.Nonempty

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: R : Type u
inst✝ : Ring R
p : R[X]
a✝ : Nontrivial R
hp : p ≠ 0
⊢ p.leadingCoeff * (-X).leadingCoeff ^ p.natDegree ≠ 0

Tactic:
by

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
f : MvPolynomial (Option σ) R
h : f ≠ 0
⊢ (((optionEquivLeft R σ) f).support.sup fun x ↦ x) = degreeOf none f

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: R : Type u
inst✝ : Ring R
p : R[X]
⊢ (p.comp (-X)).degree = p.degree

Tactic:
by

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
f : MvPolynomial (Option σ) R
h : f ≠ 0
⊢ ((optionEquivLeft R σ) f).degree = ↑(degreeOf none f)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: K : Type u_1
inst✝ : DivisionRing K
p : K[X]
⊢ Irreducible (p * C p.leadingCoeff⁻¹) ↔ Irreducible p

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
S : Type u_2
inst✝¹ : CommSemiring S
i : R →+* S
x : S
inst✝ : Invertible x
N : ℕ
f : R[X]
hf : f.natDegree ≤ N
⊢ eval₂ i (⅟x) (reflect N f) * x ^ N = eval₂ i x f

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: K : Type u_1
inst✝ : DivisionRing K
p q : K[X]
hp0 : p ≠ 0
⊢ q ∣ p * C p.leadingCoeff⁻¹ ↔ q ∣ p

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: K : Type u_1
inst✝ : DivisionRing K
p : K[X]
h : p ≠ 0
⊢ (p * C p.leadingCoeff⁻¹).Monic

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: K : Type u_1
inst✝ : DivisionRing K
p : K[X]
hp0 : p ≠ 0
⊢ (C p.leadingCoeff⁻¹).degree = 0

Tactic:
by

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial (Option σ) R
⊢ ((optionEquivLeft R σ) p).natDegree = degreeOf none p

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: K : Type u_1
inst✝ : DivisionRing K
p q : K[X]
h : q ≠ 0
⊢ (p * C q.leadingCoeff⁻¹).degree = p.degree

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: K : Type u_1
inst✝ : DivisionRing K
p : K[X]
⊢ (p * C p.leadingCoeff⁻¹).degree = p.degree

Tactic:
by_cases hp : p = 0
  · simp [hp]
  exact degree_mul_leadingCoeff_inv _ hp

Goal state after:
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: K : Type u_1
inst✝ : DivisionRing K
p : K[X]
⊢ (p * C p.leadingCoeff⁻¹).degree = p.degree

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: K : Type u_1
inst✝ : DivisionRing K
p : K[X]
⊢ p.degree + (C p.leadingCoeff⁻¹).degree = p.degree

Tactic:
by

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

Goal state before:
pp: R : Type u
S₁ : Type v
inst✝ : CommSemiring R
p : MvPolynomial (Option S₁) R
i : ℕ
hi : i ≤ p.totalDegree
hpi : ¬((optionEquivLeft R S₁) p).coeff i = 0
⊢ (((optionEquivLeft R S₁) p).coeff i).support.Nonempty

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
⊢ Subsingleton R → (∀ (f g : R[X]), f = g) ∧ ∀ (a b : R), a = b

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
this : C (p.coeff p.natDegree) = 1
⊢ C (p.coeff p.natDegree) * X ^ p.natDegree + ∑ x ∈ range p.natDegree, C (p.coeff x) * X ^ x =
    X ^ p.natDegree + ∑ i ∈ range p.natDegree, C (p.coeff i) * X ^ i

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
⊢ p = X ^ p.natDegree + ∑ i ∈ range p.natDegree, C (p.coeff i) * X ^ i

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
b : R
hp : b * p.leadingCoeff = 1
⊢ (C b * p).Monic

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
b : R
hp : p.leadingCoeff * b = 1
⊢ (p * C b).Monic

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
H : p.degree < ↑n
⊢ (X ^ n + p).coeff n = 1

Tactic:
by

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

Goal state before:
pp: R : Type u
a : R
inst✝ : Semiring R
n : ℕ
h : n ≠ 0
⊢ 0 < ↑n

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
this : DecidableEq R := Classical.decEq R
h0 : ¬0 = 1
⊢ p.leadingCoeff * q.leadingCoeff ≠ 0

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
this : DecidableEq R := Classical.decEq R
h0 : ¬0 = 1
⊢ (p * q).Monic

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
n : ℕ
⊢ (p ^ (n + 1)).Monic

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
hpq : q.degree < p.degree
⊢ (p + q).Monic

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
hq : q.Monic
hpq : p.degree < q.degree
⊢ (p + q).Monic

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
hpq : (p * q).Monic
⊢ q.Monic

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
motive : R[X] → Prop
N : ℕ
zero : motive 0
C_mul_pow : ∀ (n : ℕ) (r : R), r ≠ 0 → n ≤ N → motive (C r * X ^ n)
add : ∀ (f g : R[X]), f.natDegree < g.natDegree → g.natDegree ≤ N → motive f → motive g → motive (f + g)
f : R[X]
df : f.natDegree ≤ N
⊢ motive f

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
hq : q.Monic
hpq : (p * q).Monic
⊢ p.Monic

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
h : q.natDegree ≠ 0
a✝ : Nontrivial R
⊢ p.leadingCoeff * q.leadingCoeff ^ p.natDegree ≠ 0

Tactic:
by

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

Goal state before:
pp: R : Type u
S₁ : Type v
inst✝ : CommSemiring R
p : MvPolynomial (Option S₁) R
i : ℕ
hi : i ≤ p.totalDegree
⊢ (((optionEquivLeft R S₁) p).coeff i).totalDegree + i ≤ p.totalDegree

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
⊢ (φ 0).natDegree = fu (natDegree 0)

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
h : q.natDegree ≠ 0
⊢ (p.comp q).Monic

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
r : R
⊢ (p.comp (X + C r)).Monic

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
⊢ p.degree ≤ 0 ↔ p = 1

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
S : Type u_2
inst✝¹ : CommSemiring S
i : R →+* S
x : S
inst✝ : Invertible x
N : ℕ
f : R[X]
hf : f.natDegree ≤ N
⊢ eval₂ i (⅟x) (reflect N f) = 0 ↔ eval₂ i x f = 0

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
⊢ (p * q).natDegree = p.natDegree + q.natDegree

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
n : ℕ
⊢ f.reverse.coeff n = f.coeff ((revAt f.natDegree) n)

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]
⊢ (p * q).degree = (q * p).degree

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ f.reverse.coeff 0 = f.leadingCoeff

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ f.reverse = 0 ↔ f = 0

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 ≠ 0
⊢ (p * q).natDegree = p.natDegree + q.natDegree

Tactic:
by

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

Goal state before:
pp: R : Type u
S₁ : Type v
inst✝ : CommSemiring R
p : MvPolynomial (Option S₁) R
i : ℕ
⊢ (((optionEquivLeft R S₁) p).coeff i).totalDegree ≤ p.totalDegree

Tactic:
by

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial (Option σ) R
m : ℕ
d : σ →₀ ℕ
⊢ coeff d (((optionEquivLeft R σ) p).coeff m) = coeff (optionElim m d) p

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ f.reverse.natDegree ≤ f.natDegree

Tactic:
by

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

Goal state before:
pp: R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
⊢ (aeval fun o ↦ o.elim (C Polynomial.X) X).comp (aevalTower (Polynomial.aeval (X none)) fun i ↦ X (Option.some i)) =
    AlgHom.id R (MvPolynomial S₁ R[X])

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]
⊢ (p * q).natDegree = (q * p).natDegree

Tactic:
by

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

Goal state before:
pp: R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
⊢ (aevalTower (Polynomial.aeval (X none)) fun i ↦ X (Option.some i)).comp (aeval fun o ↦ o.elim (C Polynomial.X) X) =
    AlgHom.id R (MvPolynomial (Option S₁) R)

Tactic:
by

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

Goal state before:
pp: R : Type u
S₁ : Type v
inst✝ : CommSemiring R
x : S₁
⊢ (optionEquivRight R S₁) (X (Option.some x)) = X x

Tactic:
by

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

Goal state before:
pp: R : Type u
S₁ : Type v
inst✝ : CommSemiring R
⊢ (optionEquivRight R S₁) (X none) = C Polynomial.X

Tactic:
by

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

Goal state before:
pp: R : Type u
S₁ : Type v
inst✝ : CommSemiring R
r : R
⊢ (optionEquivRight R S₁) (C r) = C (Polynomial.C r)

Tactic:
by

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

Goal state before:
pp: case refine_1
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
n : ℕ
r : R
r0 : r ≠ 0
a✝ : n ≤ p.natDegree
⊢ (φ (C r * X ^ n)).natDegree = fu (C r * X ^ n).natDegree

Tactic:
rw [natDegree_C_mul_X_pow _ _ r0, C_mul_X_pow_eq_monomial, φ_mon_nat _ _ r0]

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

Goal state before:
pp: case a
R : Type u_1
inst✝ : Semiring R
f : R[X]
hf : ¬f = 0
⊢ f.reverse.natDegree + f.natTrailingDegree ≤ f.natDegree

Tactic:
· rw [← le_tsub_iff_left f.reverse_natDegree_le]
    apply natTrailingDegree_le_of_ne_zero
    have key := mt leadingCoeff_eq_zero.mp (mt reverse_eq_zero.mp hf)
    rwa [leadingCoeff, coeff_reverse, revAt_le f.reverse_natDegree_le] at key

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ f.natDegree = f.reverse.natDegree + f.natTrailingDegree

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
n : ℕ
⊢ ↑(finSuccEquiv R n) = eval₂Hom (Polynomial.C.comp C) fun i ↦ Fin.cases Polynomial.X (fun k ↦ Polynomial.C (X k)) i

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ f.reverse.natDegree = f.natDegree - f.natTrailingDegree

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
⊢ (finSuccEquiv R n) p =
    (eval₂Hom (Polynomial.C.comp C) fun i ↦ Fin.cases Polynomial.X (fun k ↦ Polynomial.C (X k)) i) p

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
a : R
⊢ ¬IsUnit (X + C a)

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
n : ℕ
⊢ (↑(finSuccEquiv R n).symm).comp (Polynomial.C.comp C) = C

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ f.reverse.leadingCoeff = f.trailingCoeff

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
n : ℕ
⊢ (finSuccEquiv R n) (X 0) = Polynomial.X

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
n : ℕ
j : Fin n
⊢ (finSuccEquiv R n) (X j.succ) = Polynomial.C (X j)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ f.reverse.natTrailingDegree = 0

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
h0 : q ≠ 0
hl : q.natDegree < p.natDegree
⊢ ¬p ∣ q

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ f.reverse.trailingCoeff = f.leadingCoeff

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f g : R[X]
fg : f.leadingCoeff * g.leadingCoeff ≠ 0
⊢ (f * g).reverse = f.reverse * g.reverse

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
⊢ (p * q).nextCoeff = p.nextCoeff + q.nextCoeff

Tactic:
by

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

Goal state before:
pp: R : Type u_2
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
f g : R[X]
⊢ (f * g).reverse = f.reverse * g.reverse

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
n : ℕ
j : Fin (n + 1) →₀ ℕ
r : R
m : Fin n →₀ ℕ
hjmi : j ≠ cons (j 0) m
⊢ m ≠ j.tail

Tactic:
by

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

Goal state before:
pp: R : Type u_2
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
⊢ (p * q).trailingCoeff = p.trailingCoeff * q.trailingCoeff

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
hf : f.natDegree = 0
⊢ f.natDegree < 1

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ f.reverse.coeff 1 = f.nextCoeff

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
t : R
⊢ (C t).reverse = C t

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
n : ℕ
s : Fin n → R
y : R
f : MvPolynomial (Fin (n + 1)) R
r : R
⊢ (↑↑(Polynomial.mapRingHom (eval s))).toFun ((algebraMap R (MvPolynomial (Fin n) R)[X]) r) = (algebraMap R R[X]) r

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
n : ℕ
⊢ (p ^ n).nextCoeff = n • p.nextCoeff

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : R[X]
⊢ (p * X).reverse = p.reverse

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : R[X]
⊢ (X * p).reverse = p.reverse

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ (p * X ^ n).reverse = p.reverse

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ (X ^ n * p).reverse = p.reverse

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : R[X]
t : R
⊢ (p + C t).reverse = p.reverse + C t * X ^ p.natDegree

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : R[X]
t : R
⊢ (C t + p).reverse = C t * X ^ p.natDegree + p.reverse

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
f : R[X]
N : ℕ
⊢ reflect N (-f) = -reflect N f

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
n : ℕ
s : Fin n → R
y : R
f : MvPolynomial (Fin (n + 1)) R
⊢ (eval (Fin.cons y s)) f = Polynomial.eval y (Polynomial.map (eval s) ((finSuccEquiv R n) f))

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝² : Semiring R
p : R[X]
S : Type u_1
inst✝¹ : Semiring S
inst✝ : Nontrivial S
f : R →+* S
hp : p.Monic
map_eq : Polynomial.map f p = 1
a✝ : Nontrivial R
⊢ p.degree = 0

Tactic:
by

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

Goal state before:
pp: R : Type u
S₁ : Type v
inst✝ : CommSemiring R
s' : S₁ → R
f : (MvPolynomial S₁ R)[X]
i : ℕ
⊢ (Polynomial.map (eval s') f).coeff i = (eval s') (f.coeff i)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
f g : R[X]
N : ℕ
⊢ reflect N (f - g) = reflect N f - reflect N g

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
f : R[X]
⊢ (-f).reverse = -f.reverse

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝² : Semiring R
p : R[X]
S : Type u_1
inst✝¹ : Semiring S
inst✝ : Nontrivial S
f : R →+* S
hp : p.Monic
map_eq : Polynomial.map f p = 1
⊢ p = 1

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.natDegree ≤ List.foldr max 0 (List.map natDegree l)

Tactic:
by

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

Goal state before:
pp: S : Type u_1
inst✝ : Semiring S
l : Multiset S[X]
⊢ ∀ (a : List S[X]), (Multiset.sum ⟦a⟧).natDegree ≤ foldr max 0 (Multiset.map natDegree ⟦a⟧)

Tactic:
by

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

Goal state before:
pp: ι : Type w
s : Finset ι
S : Type u_1
inst✝ : Semiring S
f : ι → S[X]
⊢ (∑ i ∈ s, f i).natDegree ≤ Finset.fold max 0 (natDegree ∘ f) s

Tactic:
by

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

Goal state before:
pp: ι : Type w
s : Finset ι
S : Type u_1
inst✝ : Semiring S
n : ℕ
f : ι → S[X]
h : ∀ i ∈ s, (f i).natDegree ≤ n
⊢ 0 ≤ n ∧ ∀ x ∈ s, (natDegree ∘ f) x ≤ n

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 ι
hf : ∑ k ∈ s, (f k).leadingCoeff ≠ 0
d : ℕ
hd : ∀ k ∈ s, (f k).natDegree = d
this : (∑ k ∈ s, f k).natDegree = d
⊢ (∑ k ∈ s, f k).leadingCoeff = ∑ k ∈ s, (f k).leadingCoeff

Tactic:
by

Goal state after: