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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
this : DecidableEq R := Classical.decEq R
hp0 : ¬p = 0
hq0 : q = 0
⊢ (p * q).degree = p.degree + q.degree

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Eval.Coeff

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
hf : Function.Surjective ⇑f
p : S[X]
n : ℕ
s : S
r : R
hr : f r = s
⊢ map f ((monomial n) r) = (monomial n) s

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Eval.Coeff

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
h✝ : Function.Surjective (map f)
s : S
p : R[X]
h : map f p = C s
⊢ f (p.coeff 0) = s

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Eval.Coeff

Goal state before:
pp: R : Type u
S : Type v
T : Type w
inst✝² : Semiring R
p : R[X]
inst✝¹ : Semiring S
f : R →+* S
inst✝ : Semiring T
g : S →+* T
x : T
⊢ eval₂ g x (map f p) = eval₂ (g.comp f) x p

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Eval.Coeff

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X]
⊢ eval 0 (map f p) = f (eval 0 p)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Eval.Coeff

Goal state before:
pp: case monomial
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
n : ℕ
r : R
⊢ eval 1 (map f ((monomial n) r)) = f (eval 1 ((monomial n) r))

Tactic:
simp only [one_pow, mul_one, eval_monomial, map_monomial]

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

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

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Eval.Coeff

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X]
⊢ eval 1 (map f p) = f (eval 1 p)

Tactic:
by

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

Goal state before:
pp: R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
⊢ leadingCoeff 1 = 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Eval.Coeff

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X]
n : ℕ
⊢ eval (↑n) (map f p) = f (eval (↑n) p)

Tactic:
by

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

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

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Eval.Coeff

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
p : R[X]
i : ℤ
⊢ eval (↑i) (map f p) = f (eval (↑i) p)

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
n : ℕ
hn : 0 < n
r : R
⊢ (X ^ n - C r).leadingCoeff = 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Eval.Coeff

Goal state before:
pp: R : Type u
S : Type v
T : Type w
inst✝² : Semiring R
p : R[X]
inst✝¹ : Semiring S
inst✝ : Semiring T
f : R →+* S
g : S →+* T
x : S
⊢ g (eval₂ f x p) = eval₂ (g.comp f) (g x) p

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
inst✝ : Nontrivial R
a : R
⊢ (X - C a).degree = 1

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
inst✝ : Nontrivial R
x : R
⊢ (X - C x).natDegree = 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Degree

Goal state before:
pp: R : Type u_1
A : Type u_3
B : Type u_5
inst✝⁷ : Semiring R
inst✝⁶ : LinearOrder B
inst✝⁵ : OrderBot B
p q : R[A]
D : A → B
inst✝⁴ : AddZeroClass A
inst✝³ : Add B
inst✝² : AddLeftStrictMono B
inst✝¹ : AddRightStrictMono B
inst✝ : NoZeroDivisors R
hD : Function.Injective D
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
⊢ leadingCoeff D (p * q) = leadingCoeff D p * leadingCoeff D q

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Eval.Coeff

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X]
⊢ (map f p).support ⊆ p.support

Tactic:
by

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

Goal state before:
pp: S : Type v
inst✝ : Ring S
c : S
⊢ (X - C c).nextCoeff = -c

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
inst✝ : Nontrivial R
n : ℕ
hn : 0 < n
a : R
⊢ (X ^ n - C a).degree = ↑n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Eval.Coeff

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

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
inst✝ : Nontrivial R
n : ℕ
hn : 0 < n
a : R
⊢ X ^ n - C a ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Eval.Coeff

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
x : R
p : R[X]
h : p.IsRoot x
⊢ (Polynomial.map f p).IsRoot (f x)

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: S : Type v
inst✝ : Ring S
r : S
⊢ (X - C r).leadingCoeff = 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Eval.Coeff

Goal state before:
pp: S : Type v
inst✝¹ : CommSemiring S
R : Type u_1
inst✝ : Ring R
f : R →+* S
x : R
p : R[X]
h : (Polynomial.map f p).IsRoot (f x)
hf : Function.Injective ⇑f
⊢ p.IsRoot x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Degree

Goal state before:
pp: R : Type u_1
A : Type u_3
B : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder B
inst✝⁴ : OrderBot B
p q : R[A]
D : A → B
inst✝³ : AddZeroClass A
inst✝² : Add B
inst✝¹ : AddLeftStrictMono B
inst✝ : AddRightStrictMono B
hD : Function.Injective D
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hq : Monic D q
⊢ leadingCoeff D (p * q) = leadingCoeff D p

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
i j : ℕ
⊢ (monomial i) 1 = (monomial j) 1 ↔ i = j

Tactic:
by

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

Goal state before:
pp: R : Type u
a b : R
m✝ n✝ : ℕ
inst✝¹ : Semiring R
p q r : R[X]
inst✝ : Nontrivial R
m n : ℕ
h : (fun i ↦ (monomial i) 1) m = (fun i ↦ (monomial i) 1) n
⊢ m = n

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
f : R[X]
n : ℕ
hn : f.support ⊆ {n}
i : ℕ
hi : ¬i = n
⊢ f.coeff i = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Degree

Goal state before:
pp: R : Type u_1
A : Type u_3
B : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder B
inst✝⁴ : OrderBot B
p q : R[A]
D : A → B
inst✝³ : AddZeroClass A
inst✝² : Add B
inst✝¹ : AddLeftStrictMono B
inst✝ : AddRightStrictMono B
hD : Function.Injective D
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hp : Monic D p
⊢ leadingCoeff D (p * q) = leadingCoeff D q

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
f : R[X]
⊢ f.support.card ≤ 1 ↔ ∃ n a, f = (monomial n) a

Tactic:
by

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
p : R[X]
inst✝ : Semiring S
f : R →+* S
x : S
⊢ (fun i ↦ eval₂ f x ((monomial i) (p.coeff i))) = fun i ↦ f (p.coeff i) * x ^ i

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
S : Type u_1
inst✝ : Semiring S
f g : R[X] →+* S
h₁ : ∀ (a : R), f (C a) = g (C a)
h₂ : f X = g X
f' : AddMonoidAlgebra R ℕ →+* S := f.comp (toFinsuppIso R).symm.toRingHom
hf' : f' = f.comp (toFinsuppIso R).symm.toRingHom
⊢ f = g

Tactic:
set g' := g.comp (toFinsuppIso R).symm.toRingHom with hg'

Goal state after:
R : Type u
inst✝¹ : Semiring R
S : Type u_1
inst✝ : Semiring S
f g : R[X] →+* S
h₁ : ∀ (a : R), f (C a) = g (C a)
h₂ : f X = g X
f' : AddMonoidAlgebra R ℕ →+* S := f.comp (toFinsuppIso R).symm.toRingHom
hf' : f' = f.comp (toFinsuppIso R).symm.toRingHom
g' : AddMonoidAlgebra R ℕ →+* S := g.comp (toFinsuppIso R).symm.toRingHom
hg' : g' = g.comp (toFinsuppIso R).symm.toRingHom
⊢ f = g
Module: Mathlib.Algebra.MonoidAlgebra.Degree

Goal state before:
pp: R : Type u_1
A : Type u_3
B : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder B
inst✝⁴ : OrderBot B
p q : R[A]
D : A → B
inst✝³ : AddZeroClass A
inst✝² : Add B
inst✝¹ : AddLeftStrictMono B
inst✝ : AddRightStrictMono B
hD : Function.Injective D
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hp : Monic D p
hq : Monic D q
⊢ Monic D (p * q)

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
S : Type u_1
inst✝ : Semiring S
f g : R[X] →+* S
h₁ : ∀ (a : R), f (C a) = g (C a)
h₂ : f X = g X
f' : AddMonoidAlgebra R ℕ →+* S := f.comp (toFinsuppIso R).symm.toRingHom
hf' : f' = f.comp (toFinsuppIso R).symm.toRingHom
g' : AddMonoidAlgebra R ℕ →+* S := g.comp (toFinsuppIso R).symm.toRingHom
hg' : g' = g.comp (toFinsuppIso R).symm.toRingHom
⊢ f' = g'

Tactic:
by

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X]
n : ℕ
hn : p.natDegree < n
x : S
⊢ eval₂ f x p = ∑ i ∈ range n, f (p.coeff i) * x ^ i

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Degree

Goal state before:
pp: R : Type u_1
inst✝⁶ : Semiring R
A : Type u_8
B : Type u_9
inst✝⁵ : AddMonoid A
inst✝⁴ : AddMonoid B
inst✝³ : LinearOrder B
inst✝² : OrderBot B
inst✝¹ : AddLeftStrictMono B
inst✝ : AddRightStrictMono B
D : A → B
p : R[A]
n : ℕ
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hD : Function.Injective D
hp : Monic D p
⊢ Monic D (p ^ n)

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
x : R
⊢ eval x p = ∑ i ∈ range (p.natDegree + 1), p.coeff i * x ^ i

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
S : Type u_1
inst✝ : Semiring S
f g : R[X] →+* S
h₁ : ∀ (a : R), f (C a) = g (C a)
h₂ : f X = g X
f' : AddMonoidAlgebra R ℕ →+* S := f.comp (toFinsuppIso R).symm.toRingHom
hf' : f' = f.comp (toFinsuppIso R).symm.toRingHom
g' : AddMonoidAlgebra R ℕ →+* S := g.comp (toFinsuppIso R).symm.toRingHom
hg' : g' = g.comp (toFinsuppIso R).symm.toRingHom
A : f' = g'
⊢ f = f'.comp ↑(toFinsuppIso R)

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
hn : p.natDegree < n
x : R
⊢ eval x p = ∑ i ∈ range n, p.coeff i * x ^ i

Tactic:
by

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

Goal state before:
pp: S : Type v
inst✝ : CommRing S
d : ℕ
y : S
⊢ ↑d + 1 = ↑d.succ

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Degree

Goal state before:
pp: R : Type u_1
inst✝⁷ : Semiring R
A : Type u_8
B : Type u_9
inst✝⁶ : AddMonoid A
inst✝⁵ : AddMonoid B
inst✝⁴ : LinearOrder B
inst✝³ : OrderBot B
inst✝² : AddLeftStrictMono B
inst✝¹ : AddRightStrictMono B
D : A → B
p : R[A]
n : ℕ
hzero : D 0 = 0
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hD : Function.Injective D
inst✝ : Nontrivial R
hp : Monic D p
⊢ supDegree D (p ^ n) = n • supDegree D p

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
S : Type u_1
inst✝ : Semiring S
f g : R[X] →+* S
h₁ : ∀ (a : R), f (C a) = g (C a)
h₂ : f X = g X
f' : AddMonoidAlgebra R ℕ →+* S := f.comp (toFinsuppIso R).symm.toRingHom
hf' : f' = f.comp (toFinsuppIso R).symm.toRingHom
g' : AddMonoidAlgebra R ℕ →+* S := g.comp (toFinsuppIso R).symm.toRingHom
hg' : g' = g.comp (toFinsuppIso R).symm.toRingHom
A : f' = g'
B : f = f'.comp ↑(toFinsuppIso R)
⊢ g = g'.comp ↑(toFinsuppIso R)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Degree

Goal state before:
pp: R : Type u_1
A : Type u_3
T : Type u_4
inst✝² : Semiring R
inst✝¹ : SemilatticeInf T
inst✝ : OrderTop T
D : A → T
s : R[A]
hs : s.coeff.support.Nonempty
⊢ infDegree (WithTop.some ∘ D) s = ↑(infDegree D s)

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
S : Type u_1
inst✝ : Semiring S
f g : R[X] →+* S
h₁ : ∀ (a : R), f (C a) = g (C a)
h₂ : f X = g X
⊢ f = g

Tactic:
by

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

Goal state before:
pp: S : Type v
inst✝ : CommRing S
d : ℕ
y : S
⊢ eval (1 + y) ((monomial d) (↑d + 1)) - eval y ((monomial d) (↑d + 1)) =
    ∑ x_1 ∈ range (d + 1), ↑((d + 1).choose x_1) * (↑x_1 * y ^ (x_1 - 1))

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
⊢ R[ X] = ⊤

Tactic:
by

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

Goal state before:
pp: R : Type u
A : Type z
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A
⊢ R[x] = (aeval x).range

Tactic:
by

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

Goal state before:
pp: R : Type u
A : Type z
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
p : R[X]
x : A
⊢ (aeval x) p ∈ R[x]

Tactic:
by

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

Goal state before:
pp: R : Type u
A : Type z
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x a : A
h : a ∈ R[x]
⊢ ∃ p, (aeval x) p = a

Tactic:
by

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

Goal state before:
pp: R : Type u
A : Type z
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A
a : ↥R[x]
⊢ ↑a ∈ R[x]

Tactic:
by

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

Goal state before:
pp: R : Type u
A : Type z
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A
a : ↥R[x]
⊢ ∃ p, (aeval x) p = ↑a

Tactic:
by

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

Goal state before:
pp: R : Type u
A : Type z
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A
M : ↥R[x] → Prop
a : ↥R[x]
f : ∀ (p : R[X]), M ⟨(aeval x) p, ⋯⟩
⊢ M a

Tactic:
by

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

Goal state before:
pp: R : Type u
S : Type v
T : Type w
A : Type z
A' : Type u_1
B : Type u_2
a b : R
n : ℕ
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : CommSemiring A'
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
p✝ q✝ : R[X]
x : A
x✝¹ x✝ : ↥R[x]
p : A
hp : p ∈ R[x]
q : A
hq : q ∈ R[x]
⊢ ⟨p, hp⟩ * ⟨q, hq⟩ = ⟨q, hq⟩ * ⟨p, hp⟩

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
hqd0 : q.natDegree ≠ 0
⊢ (p.comp q).coeff (p.natDegree * q.natDegree) = p.leadingCoeff * q.leadingCoeff ^ p.natDegree

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
r : R
n : ℕ
⊢ (p.comp (C r * X)).coeff n = p.coeff n * r ^ n

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
r : R
hr : r ∈ nonZeroDivisors R
⊢ p.comp (C r * X) = 0 ↔ p = 0

Tactic:
by

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

Goal state before:
pp: R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p✝ q r : R[X]
inst✝ : Semiring S
f : R →+* S
p : R[X]
e : R ≃+* S
⊢ (mapRingHom ↑e).comp (mapRingHom ↑e.symm) = RingHom.id S[X]

Tactic:
by

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

Goal state before:
pp: R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p✝ q r : R[X]
inst✝ : Semiring S
f : R →+* S
p : R[X]
e : R ≃+* S
⊢ (mapRingHom ↑e.symm).comp (mapRingHom ↑e) = RingHom.id R[X]

Tactic:
by

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X]
hp : p.Monic
hfp : map f p = 0
x : R
⊢ f x = f x * f p.leadingCoeff

Tactic:
by

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X]
hp : p.Monic
hfp : map f p = 0
x : R
⊢ f x * (map f p).coeff p.natDegree = 0

Tactic:
by

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X]
hp : p.Monic
h : ∀ (x : R), f x = 0
n : ℕ
⊢ (map f p).coeff n = coeff 0 n

Tactic:
by

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X]
⊢ (map f p).degree ≤ p.degree

Tactic:
by

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X]
hp : f p.leadingCoeff = 0
hp₀ : p ≠ 0
⊢ (map f p).degree < p.degree

Tactic:
by

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X]
hp : f p.leadingCoeff = 0
hp₀ : map f p ≠ 0
⊢ p ≠ 0

Tactic:
by

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X]
hp : f p.leadingCoeff = 0
hp₀ : 0 < p.natDegree
⊢ (map f p).natDegree < p.natDegree

Tactic:
by

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
f : R →+* S
hf : f p.leadingCoeff ≠ 0
⊢ (map f p).degree = p.degree

Tactic:
by

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
f : R →+* S
hf : f p.leadingCoeff ≠ 0
⊢ (map f p).leadingCoeff = f p.leadingCoeff

Tactic:
by

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
f : R →+* S
hf : f p.leadingCoeff ≠ 0
⊢ (map f p).nextCoeff = f p.nextCoeff

Tactic:
by

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
p q : R[X]
inst✝ : CommSemiring S
f : R →+* S
x : S
⊢ eval₂ f x (p.comp q) = eval₂ f (eval₂ f x q) p

Tactic:
by

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
p q : R[X]
inst✝ : CommSemiring S
f : R →+* S
k : ℕ
t : S
⊢ eval₂ f t (p.comp^[k] q) = (fun x ↦ eval₂ f x p)^[k] (eval₂ f t q)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Notation.Lemmas

Goal state before:
pp: α : Type u_1
inst✝² : One α
p : Prop
inst✝¹ : Decidable p
a : p → α
b : ¬p → α
inst✝ : LE α
ha : ∀ (h : p), 1 ≤ a h
hb : ∀ (h : ¬p), 1 ≤ b h
⊢ 1 ≤ dite p a b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Notation.Lemmas

Goal state before:
pp: α : Type u_1
inst✝² : One α
p : Prop
inst✝¹ : Decidable p
a : p → α
b : ¬p → α
inst✝ : LE α
ha : ∀ (h : p), a h ≤ 1
hb : ∀ (h : ¬p), b h ≤ 1
⊢ dite p a b ≤ 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Notation.Lemmas

Goal state before:
pp: α : Type u_1
inst✝² : One α
p : Prop
inst✝¹ : Decidable p
a : p → α
b : ¬p → α
inst✝ : LT α
ha : ∀ (h : p), 1 < a h
hb : ∀ (h : ¬p), 1 < b h
⊢ 1 < dite p a b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Notation.Lemmas

Goal state before:
pp: α : Type u_1
inst✝² : One α
p : Prop
inst✝¹ : Decidable p
a : p → α
b : ¬p → α
inst✝ : LT α
ha : ∀ (h : p), a h < 1
hb : ∀ (h : ¬p), b h < 1
⊢ dite p a b < 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Notation.Lemmas

Goal state before:
pp: α : Type u_1
inst✝² : One α
p : Prop
inst✝¹ : Decidable p
a b : α
inst✝ : LE α
ha : 1 ≤ a
hb : 1 ≤ b
⊢ 1 ≤ if p then a else b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Notation.Lemmas

Goal state before:
pp: α : Type u_1
inst✝² : One α
p : Prop
inst✝¹ : Decidable p
a b : α
inst✝ : LE α
ha : a ≤ 1
hb : b ≤ 1
⊢ (if p then a else b) ≤ 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Notation.Lemmas

Goal state before:
pp: α : Type u_1
inst✝² : One α
p : Prop
inst✝¹ : Decidable p
a b : α
inst✝ : LT α
ha : 1 < a
hb : 1 < b
⊢ 1 < if p then a else b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Notation.Lemmas

Goal state before:
pp: α : Type u_1
inst✝² : One α
p : Prop
inst✝¹ : Decidable p
a b : α
inst✝ : LT α
ha : a < 1
hb : b < 1
⊢ (if p then a else b) < 1

Tactic:
by

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

Goal state before:
pp: R : Type u
S : Type v
inst✝² : Semiring R
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
f : R[X]
hf : IsUnit f.leadingCoeff
H : IsUnit (map φ f)
⊢ IsUnit f

Tactic:
by

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

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : One γ
inst✝ : LE γ
f : α → β
g : α → γ
e : β → γ
hg : 1 ≤ g
he : 1 ≤ e
_b : β
⊢ 1 _b ≤ extend f g e _b

Tactic:
by

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

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : One γ
inst✝ : LE γ
f : α → β
g : α → γ
e : β → γ
hg : g ≤ 1
he : e ≤ 1
_b : β
⊢ extend f g e _b ≤ 1 _b

Tactic:
by

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

Goal state before:
pp: ι : Type u_6
α : ι → Type u_7
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → One (α i)
inst✝ : (i : ι) → Preorder (α i)
i : ι
a b : α i
⊢ mulSingle i a ≤ mulSingle i b ↔ a ≤ b

Tactic:
by

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

Goal state before:
pp: ι : Type u_6
α : ι → Type u_7
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → One (α i)
inst✝ : (i : ι) → Preorder (α i)
i : ι
a : α i
⊢ 1 ≤ mulSingle i a ↔ 1 ≤ a

Tactic:
by

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

Goal state before:
pp: ι : Type u_6
α : ι → Type u_7
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → One (α i)
inst✝ : (i : ι) → Preorder (α i)
i : ι
a : α i
⊢ 1 < mulSingle i a ↔ 1 < a

Tactic:
by

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

Goal state before:
pp: ι : Type u_6
α : ι → Type u_7
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → One (α i)
inst✝ : (i : ι) → Preorder (α i)
i : ι
a : α i
⊢ mulSingle i a ≤ 1 ↔ a ≤ 1

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finsupp.Antidiagonal

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
f : α →₀ ℕ
p : (α →₀ ℕ) × (α →₀ ℕ)
⊢ p ∈ f.antidiagonal'.support ↔ p.1 + p.2 = f

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finsupp.Antidiagonal

Goal state before:
pp: α : Type u
inst✝¹ : DecidableEq α
M : Type u_1
inst✝ : CommMonoid M
n : α →₀ ℕ
f : (α →₀ ℕ) → (α →₀ ℕ) → M
⊢ ∀ (i : (α →₀ ℕ) × (α →₀ ℕ)), i ∈ antidiagonal n ↔ (Equiv.prodComm (α →₀ ℕ) (α →₀ ℕ)) i ∈ antidiagonal n

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finsupp.Antidiagonal

Goal state before:
pp: α : Type u
inst✝¹ : DecidableEq α
M : Type u_1
inst✝ : CommMonoid M
n : α →₀ ℕ
f : (α →₀ ℕ) → (α →₀ ℕ) → M
⊢ ∀ i ∈ antidiagonal n, f i.1 i.2 = f ((Equiv.prodComm (α →₀ ℕ) (α →₀ ℕ)) i).2 ((Equiv.prodComm (α →₀ ℕ) (α →₀ ℕ)) i).1

Tactic:
by

Goal state after: