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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
⊢ coeffList 0 = []

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
x : R
h : x ≠ 0
⊢ (C x).coeffList = [x]

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
P : R[X]
h : P ≠ 0
⊢ ∃ ls, P.coeffList = P.leadingCoeff :: ls

Tactic:
simp [coeffList, List.range_succ, withBotSucc_degree_eq_natDegree_add_one h]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
P : R[X]
h : P ≠ 0
⊢ ∃ ls, P.coeffList = P.leadingCoeff :: ls

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Module.HahnEmbedding

Goal state before:
pp: K : Type u_1
inst✝¹³ : DivisionRing K
inst✝¹² : LinearOrder K
inst✝¹¹ : IsOrderedRing K
inst✝¹⁰ : Archimedean K
M : Type u_2
inst✝⁹ : AddCommGroup M
inst✝⁸ : LinearOrder M
inst✝⁷ : IsOrderedAddMonoid M
inst✝⁶ : Module K M
inst✝⁵ : IsOrderedModule K M
R : Type u_3
inst✝⁴ : AddCommGroup R
inst✝³ : LinearOrder R
inst✝² : Module K R
seed : Seed K M R
f : Partial seed
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
x : M
hx : x ∉ (↑f).domain
c d : FiniteArchimedeanClass M
hdc : c ≤ d
y : ↥(↑f).domain
hy : ↑y - x ∈ ball K d
⊢ ↑(ball K d) ⊆ ↑(ball K c)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
P : R[X]
⊢ P.coeffList.length = P.degree.succ

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Module.HahnEmbedding

Goal state before:
pp: K : Type u_1
inst✝¹³ : DivisionRing K
inst✝¹² : LinearOrder K
inst✝¹¹ : IsOrderedRing K
inst✝¹⁰ : Archimedean K
M : Type u_2
inst✝⁹ : AddCommGroup M
inst✝⁸ : LinearOrder M
inst✝⁷ : IsOrderedAddMonoid M
inst✝⁶ : Module K M
inst✝⁵ : IsOrderedModule K M
R : Type u_3
inst✝⁴ : AddCommGroup R
inst✝³ : LinearOrder R
inst✝² : Module K R
seed : Seed K M R
f : Partial seed
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
x : M
hx : x ∉ (↑f).domain
c : FiniteArchimedeanClass M
⊢ toLex ((truncLTLinearMap K c) (ofLex (f.eval x))) ∈ (f.extendFun hx).toFun.range

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : DecidableEq R
P : R[X]
⊢ P.coeffList.length = if P = 0 then 0 else P.natDegree + 1

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
P : R[X]
h : P.nextCoeff ≠ 0
⊢ P.leadingCoeff :: P.eraseLead.coeffList = P.coeffList

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
x : R
hx : x ≠ 0
n : ℕ
h : ¬(monomial n) x = 0
⊢ ((monomial n) x).coeffList.length = (x :: List.replicate n 0).length

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
x : R
hx : x ≠ 0
n : ℕ
h : ¬(monomial n) x = 0
h₁✝ : 0 < ((monomial n) x).coeffList.length
h₁ : 0 < (x :: List.replicate n 0).length
⊢ ∀ (w : List R),
    ((monomial n) x).coeffList = ((monomial n) x).leadingCoeff :: w →
      ((monomial n) x).coeffList.get ⟨0, h₁✝⟩ = (x :: List.replicate n 0).get ⟨0, h₁⟩

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
x : R
hx : x ≠ 0
n : ℕ
h : ¬(monomial n) x = 0
k : ℕ
h₁✝¹ : k + 1 < ((monomial n) x).coeffList.length
h₁✝ : k + 1 < (x :: List.replicate n 0).length
h₁ : k + 1 < n + 1
⊢ ((monomial n) x).natDegree.succ = n + 1

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
x : R
hx : x ≠ 0
n : ℕ
h : ¬(monomial n) x = 0
k : ℕ
h₁✝¹ : k + 1 < ((monomial n) x).coeffList.length
h₁✝ : k + 1 < (x :: List.replicate n 0).length
h₁ : k + 1 < n + 1
this : ((monomial n) x).natDegree.succ = n + 1
⊢ ((monomial n) x).natDegree - (k + 1) ≠ n

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
x : R
hx : x ≠ 0
n : ℕ
⊢ ((monomial n) x).coeffList = x :: List.replicate n 0

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
P : R[X]
h : P ≠ 0
hdp : ¬P.natDegree = 0
hep : P.eraseLead = 0
⊢ (monomial P.natDegree) P.leadingCoeff = P

Tactic:
by

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

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
P : R[X]
h : P ≠ 0
hdp : ¬P.natDegree = 0
hep : ¬P.eraseLead = 0
⊢ P.coeffList = P.leadingCoeff :: (List.replicate (P.natDegree - P.eraseLead.degree.succ) 0 ++ P.eraseLead.coeffList)

Tactic:
have h₁ := withBotSucc_degree_eq_natDegree_add_one h

Goal state after:
case neg
R : Type u_1
inst✝ : Semiring R
P : R[X]
h : P ≠ 0
hdp : ¬P.natDegree = 0
hep : ¬P.eraseLead = 0
h₁ : P.degree.succ = P.natDegree + 1
⊢ P.coeffList = P.leadingCoeff :: (List.replicate (P.natDegree - P.eraseLead.degree.succ) 0 ++ P.eraseLead.coeffList)
Module: Mathlib.Algebra.Polynomial.CoeffList

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
P : R[X]
h : P ≠ 0
hdp : ¬P.natDegree = 0
hep : ¬P.eraseLead = 0
h₁ : P.degree.succ = P.natDegree + 1
h₂ : P.eraseLead.degree.succ = P.eraseLead.natDegree + 1
⊢ ∃ d, P.natDegree = P.eraseLead.natDegree + 1 + d ∧ d = P.natDegree - P.eraseLead.degree.succ

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
P : R[X]
h : P ≠ 0
hdp : ¬P.natDegree = 0
hep : ¬P.eraseLead = 0
h₁ : P.degree.succ = P.natDegree + 1
h₂ : P.eraseLead.degree.succ = P.eraseLead.natDegree + 1
n : ℕ
hn : P.natDegree = P.eraseLead.natDegree + 1 + n
k : ℕ
hkd : k + 1 < P.natDegree + 1
dk : ℕ
hdk : P.natDegree = k + 1 + dk
⊢ k + 1 < (List.map P.coeff (List.range P.degree.succ)).length

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
P : R[X]
h : P ≠ 0
hdp : ¬P.natDegree = 0
hep : ¬P.eraseLead = 0
h₁ : P.degree.succ = P.natDegree + 1
h₂ : P.eraseLead.degree.succ = P.eraseLead.natDegree + 1
n : ℕ
hn : P.natDegree = P.eraseLead.natDegree + 1 + n
k : ℕ
hkd : k + 1 < P.natDegree + 1
dk : ℕ
hdk : P.natDegree = k + 1 + dk
⊢ P.degree.succ - 1 - (k + 1) < P.degree.succ

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
P : R[X]
h : P ≠ 0
hdp : ¬P.natDegree = 0
hep : ¬P.eraseLead = 0
h₁ : P.degree.succ = P.natDegree + 1
h₂ : P.eraseLead.degree.succ = P.eraseLead.natDegree + 1
n : ℕ
hn : P.natDegree = P.eraseLead.natDegree + 1 + n
k : ℕ
hkd : k + 1 < P.natDegree + 1
dk : ℕ
hdk : P.natDegree = k + 1 + dk
⊢ dk ≠ P.natDegree

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
P : R[X]
h : P ≠ 0
hdp : ¬P.natDegree = 0
hep : ¬P.eraseLead = 0
h₁ : P.degree.succ = P.natDegree + 1
h₂ : P.eraseLead.degree.succ = P.eraseLead.natDegree + 1
n : ℕ
hn : P.natDegree = P.eraseLead.natDegree + 1 + n
k : ℕ
hkd : k + 1 < P.natDegree + 1
dk : ℕ
hdk : P.natDegree = k + 1 + dk
hkn : k < n
⊢ P.eraseLead.natDegree < dk

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Derivation.MapCoeffs

Goal state before:
pp: R : Type u_1
A : Type u_2
M : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : Module R M
d : Derivation R A M
⊢ (PolynomialModule.map A ↑d ∘ₗ ↑PolynomialModule.equivPolynomial.symm) 1 = 0

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
P : R[X]
h : P ≠ 0
hdp : ¬P.natDegree = 0
hep : ¬P.eraseLead = 0
h₁ : P.degree.succ = P.natDegree + 1
h₂ : P.eraseLead.degree.succ = P.eraseLead.natDegree + 1
n : ℕ
hn : P.natDegree = P.eraseLead.natDegree + 1 + n
k : ℕ
hkd : k + 1 < P.natDegree + 1
dk : ℕ
hdk : P.natDegree = k + 1 + dk
hkn : n ≤ k
⊢ P.eraseLead.degree.succ - 1 - (k - n) < P.eraseLead.degree.succ

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
P : R[X]
h : P ≠ 0
⊢ P.coeffList = P.leadingCoeff :: (List.replicate (P.natDegree - P.eraseLead.degree.succ) 0 ++ P.eraseLead.coeffList)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Derivation.MapCoeffs

Goal state before:
pp: R : Type u_1
A : Type u_2
M : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : Module R M
d : Derivation R A M
p q : A[X]
⊢ (PolynomialModule.map A ↑d ∘ₗ ↑PolynomialModule.equivPolynomial.symm) (p * q) =
    p • (PolynomialModule.map A ↑d ∘ₗ ↑PolynomialModule.equivPolynomial.symm) q +
      q • (PolynomialModule.map A ↑d ∘ₗ ↑PolynomialModule.equivPolynomial.symm) p

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Derivation.MapCoeffs

Goal state before:
pp: R : Type u_1
A : Type u_2
M : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : Module R M
d : Derivation R A M
n : ℕ
x : A
⊢ d.mapCoeffs ((monomial n) x) = PolynomialModule.single A n (d x)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
P : R[X]
⊢ (-P).coeffList = List.map (fun x ↦ -x) P.coeffList

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Derivation.MapCoeffs

Goal state before:
pp: R : Type u_1
A : Type u_2
M : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : Module R M
d : Derivation R A M
⊢ d.mapCoeffs X = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Module.HahnEmbedding

Goal state before:
pp: K : Type u_1
inst✝¹³ : DivisionRing K
inst✝¹² : LinearOrder K
inst✝¹¹ : IsOrderedRing K
inst✝¹⁰ : Archimedean K
M : Type u_2
inst✝⁹ : AddCommGroup M
inst✝⁸ : LinearOrder M
inst✝⁷ : IsOrderedAddMonoid M
inst✝⁶ : Module K M
inst✝⁵ : IsOrderedModule K M
R : Type u_3
inst✝⁴ : AddCommGroup R
inst✝³ : LinearOrder R
inst✝² : Module K R
seed : Seed K M R
f : Partial seed
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
x : M
hx : x ∉ (↑f).domain
c : FiniteArchimedeanClass M
y' : M
hy'✝ : y' ∈ (f.extendFun hx).domain
hy' : y' ∈ (↑f).domain ⊔ K ∙ x
a : M
ha : a ∈ (↑f).domain
b : M
hb : b ∈ K ∙ x
hab : a + b = y'
k : K
hk : k • x = b
a' : M
ha'mem : a' ∈ (↑f).domain
ha' : (↑f).toFun ⟨a', ha'mem⟩ = toLex ((truncLTLinearMap K c) (ofLex (↑↑f ⟨a, ha⟩)))
⊢ a' ∈ ((↑f).supSpanSingleton x (f.eval x) hx).domain

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Derivation.MapCoeffs

Goal state before:
pp: R : Type u_1
A : Type u_2
M : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : Module R M
d : Derivation R A M
x : A
⊢ d.mapCoeffs (C x) = PolynomialModule.single A 0 (d x)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
P : R[X]
x : R
hx : x ≠ 0
⊢ (C x * P).coeffList = List.map (fun x_1 ↦ x * x_1) P.coeffList

Tactic:
by

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

Goal state before:
pp: R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
p q : S[X]
hq : q.Monic
i✝ i : ℕ
⊢ span R coeffs(p) = 1 ^ deg(p) * span R coeffs(p)

Tactic:
by

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

Goal state before:
pp: R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
p q : S[X]
hq : q.Monic
i✝ i : ℕ
⊢ 1 ^ deg(p) * span R coeffs(p) ≤ spanCoeffs(q) ^ deg(p) * spanCoeffs(p)

Tactic:
by

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

Goal state before:
pp: R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
p q : S[X]
hq : q.Monic
i✝ i : ℕ
⊢ p.coeff i ∈ spanCoeffs(q) ^ deg(p) * spanCoeffs(p)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
x y : R
p : R[X]
⊢ evalEval x y (C p) = eval x p

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
x y : R
p : R[X]
⊢ evalEval x y (map C p) = eval y p

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
x y p : R
⊢ evalEval x y (CC p) = p

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
x y : R
⊢ evalEval x y 0 = 0

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
x y : R
⊢ evalEval x y 1 = 1

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
x y : R
n : ℕ
⊢ evalEval x y ↑n = ↑n

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Derivation.MapCoeffs

Goal state before:
pp: R : Type u_1
A : Type u_2
M : Type u_3
inst✝¹² : CommRing R
inst✝¹¹ : CommRing A
inst✝¹⁰ : Algebra R A
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module A M
inst✝⁷ : Module R M
d : Derivation R A M
B : Type u_4
M' : Type u_5
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R B
inst✝⁴ : Algebra A B
inst✝³ : AddCommGroup M'
inst✝² : Module B M'
inst✝¹ : Module R M'
inst✝ : Module A M'
d' : Derivation R B M'
f : M →ₗ[A] M'
h : ∀ (a : A), f (d a) = d' ((algebraMap A B) a)
x : B
p : A[X]
⊢ d' ((aeval x) p) =
    (PolynomialModule.eval x) ((PolynomialModule.map B f) (d.mapCoeffs p)) + (aeval x) (derivative p) • d' x

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
x y : R
⊢ evalEval x y Y = y

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
x y : R
p q : R[X][Y]
⊢ evalEval x y (p + q) = evalEval x y p + evalEval x y q

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Derivation.MapCoeffs

Goal state before:
pp: R : Type u_1
A : Type u_2
M : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : Module R M
d : Derivation R A M
x : A
p : A[X]
⊢ d (eval x p) = (PolynomialModule.eval x) (d.mapCoeffs p) + eval x (derivative p) • d x

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
x y : R
p : R[X]
f : ℕ → R → R[X][Y]
⊢ evalEval x y (p.sum f) = p.sum fun n a ↦ evalEval x y (f n a)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Derivation.MapCoeffs

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
inst✝ : Differential A
n : ℕ
x : A
⊢ mapCoeffs ((monomial n) x) = (monomial n) x′

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Derivation.MapCoeffs

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
inst✝ : Differential A
⊢ mapCoeffs X = 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Derivation.MapCoeffs

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
inst✝ : Differential A
x : A
⊢ mapCoeffs (C x) = C x′

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
ι : Type u_3
s : Finset ι
x y : R
f : ι → R[X][Y]
⊢ evalEval x y (∑ i ∈ s, f i) = ∑ i ∈ s, evalEval x y (f i)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : Semiring R
inst✝¹ : DistribSMul S R
inst✝ : IsScalarTower S R R
x y : R
s : S
p : R[X][Y]
⊢ evalEval x y (s • p) = s • evalEval x y p

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
x y : R
p : R[X][Y]
⊢ evalEval x y (-p) = -evalEval x y p

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
x y : R
p q : R[X][Y]
⊢ evalEval x y (p - q) = evalEval x y p - evalEval x y q

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
x y : R
n : ℤ
⊢ evalEval x y ↑n = ↑n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Module.HahnEmbedding

Goal state before:
pp: K : Type u_1
inst✝¹³ : DivisionRing K
inst✝¹² : LinearOrder K
inst✝¹¹ : IsOrderedRing K
inst✝¹⁰ : Archimedean K
M : Type u_2
inst✝⁹ : AddCommGroup M
inst✝⁸ : LinearOrder M
inst✝⁷ : IsOrderedAddMonoid M
inst✝⁶ : Module K M
inst✝⁵ : IsOrderedModule K M
R : Type u_3
inst✝⁴ : AddCommGroup R
inst✝³ : LinearOrder R
inst✝² : Module K R
seed : Seed K M R
f : Partial seed
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
x : M
hx : x ∉ (↑f).domain
y : ↥(f.extendFun hx).domain
c : FiniteArchimedeanClass M
⊢ toLex ((truncLTLinearMap K c) (ofLex (↑(f.extendFun hx) y))) ∈ (f.extendFun hx).toFun.range

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
x y : R
p q : R[X][Y]
⊢ evalEval x y (p * q) = evalEval x y p * evalEval x y q

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Derivation.MapCoeffs

Goal state before:
pp: A : Type u_1
inst✝⁵ : CommRing A
inst✝⁴ : Differential A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Differential R
inst✝¹ : Algebra A R
inst✝ : DifferentialAlgebra A R
x : R
p : A[X]
⊢ ((aeval x) p)′ = (aeval x) (mapCoeffs p) + (aeval x) (derivative p) * x′

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Derivation.MapCoeffs

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
inst✝ : Differential A
v : A[X]
b : A
⊢ (implicitDeriv v) (C b) = C b′

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
ι : Type u_3
s : Finset ι
x y : R
p : ι → R[X][Y]
⊢ evalEval x y (∏ j ∈ s, p j) = ∏ j ∈ s, evalEval x y (p j)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Derivation.MapCoeffs

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
inst✝ : Differential A
v : A[X]
⊢ (implicitDeriv v) X = v

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Derivation.MapCoeffs

Goal state before:
pp: A : Type u_1
inst✝⁵ : CommRing A
inst✝⁴ : Differential A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Differential R
inst✝¹ : Algebra A R
inst✝ : DifferentialAlgebra A R
x : R
v : A[X]
h : x′ = (aeval x) v
p : A[X]
⊢ ((aeval x) p)′ = (aeval x) ((implicitDeriv v) p)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
x y : R
l : List R[X][Y]
⊢ evalEval x y l.prod = (List.map (evalEval x y) l).prod

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
x y : R
l : Multiset R[X][Y]
⊢ evalEval x y l.prod = (Multiset.map (evalEval x y) l).prod

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
x y : R
p : R[X][Y]
n : ℕ
⊢ evalEval x y (p ^ n) = evalEval x y p ^ n

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
x : R
⊢ evalEvalRingHom x = eval₂RingHom (evalRingHom x)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
x : R
⊢ eval₂ (evalRingHom x) = evalEval x

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
x y : R
p : R[X][Y]
⊢ eval y (map (evalRingHom x) p) = evalEval x y p

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Module.HahnEmbedding

Goal state before:
pp: K : Type u_1
inst✝¹³ : DivisionRing K
inst✝¹² : LinearOrder K
inst✝¹¹ : IsOrderedRing K
inst✝¹⁰ : Archimedean K
M : Type u_2
inst✝⁹ : AddCommGroup M
inst✝⁸ : LinearOrder M
inst✝⁷ : IsOrderedAddMonoid M
inst✝⁶ : Module K M
inst✝⁵ : IsOrderedModule K M
R : Type u_3
inst✝⁴ : AddCommGroup R
inst✝³ : LinearOrder R
inst✝² : Module K R
seed : Seed K M R
f : Partial seed
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
x : M
hx : x ∉ (↑f).domain
this : f = f.extend hx
⊢ (↑f).domain = (↑(f.extend hx)).domain

Tactic:
by

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X][Y]
q : R[X]
⊢ eval (map f q) (map (mapRingHom f) p) = map f (eval q p)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X][Y]
q : R[X]
r : R
⊢ eval (f r) (eval (map f q) (map (mapRingHom f) p)) = f (eval r (eval q p))

Tactic:
by

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X][Y]
x y : R
⊢ evalEval (f x) (f y) (map (mapRingHom f) p) = f (evalEval x y p)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
x y : S
⊢ eval₂RingHom (eval₂RingHom f x) y = (evalEvalRingHom x y).comp (mapRingHom (mapRingHom f))

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
⊢ (evalRingHom (C X)).comp (eval₂RingHom (mapRingHom (algebraMap R R[X][Y])) (C Y)) = RingHom.id R[X][Y]

Tactic:
by

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
f : A × A
⊢ (fun f ↦ (f (C X), f Y))
      ((fun xy ↦
          (AlgHom.restrictScalars R (aeval xy.1)).comp
            (let this := algebra;
            AlgHom.restrictScalars R (aeval (C xy.2))))
        f) =
    f

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Module.HahnEmbedding

Goal state before:
pp: K : Type u_1
inst✝¹³ : DivisionRing K
inst✝¹² : LinearOrder K
inst✝¹¹ : IsOrderedRing K
inst✝¹⁰ : Archimedean K
M : Type u_2
inst✝⁹ : AddCommGroup M
inst✝⁸ : LinearOrder M
inst✝⁷ : IsOrderedAddMonoid M
inst✝⁶ : Module K M
inst✝⁵ : IsOrderedModule K M
R : Type u_3
inst✝⁴ : AddCommGroup R
inst✝³ : LinearOrder R
inst✝² : Module K R
seed : Seed K M R
f : Partial seed
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
x : M
hx : x ∉ (↑f).domain
this✝ : f = f.extend hx
this : (↑f).domain = (↑(f.extend hx)).domain
h : True
⊢ x ∈ (LinearPMap.mkSpanSingleton x (f.eval x) ⋯).domain

Tactic:
by

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
f : R[X][Y] →ₐ[R] A
⊢ ((fun xy ↦
            (AlgHom.restrictScalars R (aeval xy.1)).comp
              (let this := algebra;
              AlgHom.restrictScalars R (aeval (C xy.2))))
          ((fun f ↦ (f (C X), f Y)) f)).comp
      CAlgHom =
    f.comp CAlgHom

Tactic:
by

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
f : R[X][Y] →ₐ[R] A
⊢ ((fun xy ↦
          (AlgHom.restrictScalars R (aeval xy.1)).comp
            (let this := algebra;
            AlgHom.restrictScalars R (aeval (C xy.2))))
        ((fun f ↦ (f (C X), f Y)) f))
      Y =
    f Y

Tactic:
by

Goal state after: