mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.MonoidAlgebra.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
M : Type u_7
N : Type u_8
O : Type u_9
inst✝⁹ : CommSemiring R
inst✝⁸ : CommSemiring S
inst✝⁷ : Semiring A
inst✝⁶ : Semiring B
inst✝⁵ : Semiring C
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : Algebra R C
inst✝¹ : Monoid M
inst✝ : Monoid N
f : A →ₐ[R] B
⊢ ∀ (r : R), (↑↑(mapRingHom M ↑f)).toFun ((algebraMap R A[M]) r) = (algebraMap R B[M]) r

Tactic:
by

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

Goal state before:
pp: R : Type u_1
A : Type u_4
B : Type u_5
M : Type u_7
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Semiring B
inst✝² : Algebra R A
inst✝¹ : Algebra R B
inst✝ : Monoid M
f : A →ₐ[R] B
x : A[M]
m : M
⊢ ((mapAlgHom M f) x).coeff m = f (x.coeff m)

Tactic:
by

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

Goal state before:
pp: R✝ : Type u
S : Type v
a b : R✝
n m : ℕ
inst✝⁵ : Semiring R✝
p✝ q r : R✝[X]
R : Type u_1
A : Type u_2
M : Type u_3
inst✝⁴ : Semiring R
inst✝³ : Semiring A
inst✝² : AddCommMonoid M
inst✝¹ : Module R A
inst✝ : Module R M
f : ℕ → A →ₗ[R] M
c : R
p : A[X]
⊢ ((c • p).sum fun x1 x2 ↦ (f x1) x2) = (RingHom.id R) c • p.sum fun x1 x2 ↦ (f x1) x2

Tactic:
by

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

Goal state before:
pp: R : Type u_1
A : Type u_4
B : Type u_5
M : Type u_7
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Semiring B
inst✝² : Algebra R A
inst✝¹ : Algebra R B
inst✝ : Monoid M
f : A →ₐ[R] B
m : M
a : A
⊢ (mapAlgHom M f) (single m a) = single m (f a)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.Extr

Goal state before:
pp: α : Type u
β : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b : α
f : α → β
h₀ : MonotoneOn f (Icc a b)
h₁ : AntitoneOn f (Ici b)
⊢ IsMaxOn f (Ici a) b

Tactic:
by

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

Goal state before:
pp: R : Type u_1
A : Type u_4
M : Type u_7
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : Monoid M
⊢ mapAlgHom M (AlgHom.id R A) = AlgHom.id R A[M]

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
ι : Type u_1
l : List ι
f : ι → R[X]
n : ℕ
⊢ (List.map f l).sum.coeff n = (List.map (fun a ↦ (f a).coeff n) l).sum

Tactic:
by

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
p : R[X]
inst✝ : Semiring S
n : ℕ
f : ℕ → R → S[X]
⊢ (p.sum f).coeff n = p.sum fun a b ↦ (f a b).coeff n

Tactic:
by

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

Goal state before:
pp: R : Type u_1
A : Type u_4
B : Type u_5
C : Type u_6
M : Type u_7
inst✝⁷ : CommSemiring R
inst✝⁶ : Semiring A
inst✝⁵ : Semiring B
inst✝⁴ : Semiring C
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : Algebra R C
inst✝ : Monoid M
f : A →ₐ[R] B
g : B →ₐ[R] C
⊢ mapAlgHom M (g.comp f) = (mapAlgHom M g).comp (mapAlgHom M f)

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
n : ℕ
⊢ (p * q).coeff n = ∑ x ∈ antidiagonal n, p.coeff x.1 * q.coeff x.2

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
M : Type u_7
N : Type u_8
O : Type u_9
inst✝⁹ : CommSemiring R
inst✝⁸ : CommSemiring S
inst✝⁷ : Semiring A
inst✝⁶ : Semiring B
inst✝⁵ : Semiring C
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : Algebra R C
inst✝¹ : Monoid M
inst✝ : Monoid N
e : A ≃ₐ[R] B
x✝ : A[M]
⊢ (mapAlgHom M ↑e.symm) ((↑↑(mapAlgHom M ↑e).toRingHom).toFun x✝) = x✝

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
⊢ (p * q).coeff 1 = p.coeff 0 * q.coeff 1 + p.coeff 1 * q.coeff 0

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
x : R
⊢ constantCoeff (C x) = x

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
M : Type u_7
N : Type u_8
O : Type u_9
inst✝⁹ : CommSemiring R
inst✝⁸ : CommSemiring S
inst✝⁷ : Semiring A
inst✝⁶ : Semiring B
inst✝⁵ : Semiring C
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : Algebra R C
inst✝¹ : Monoid M
inst✝ : Monoid N
e : A ≃ₐ[R] B
x✝ : B[M]
⊢ (↑↑(mapAlgHom M ↑e).toRingHom).toFun ((mapAlgHom M ↑e.symm) x✝) = x✝

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
x : R
k n : ℕ
⊢ (C x * X ^ k).coeff n = if n = k then x else 0

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
x : R
n : ℕ
⊢ (C x * X).coeff n = if n = 1 then x else 0

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.Extr

Goal state before:
pp: α : Type u
β : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b : α
f : α → β
h₀ : MonotoneOn f (Iic b)
h₁ : AntitoneOn f (Ico b a)
⊢ IsMaxOn f (Iio a) b

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: R : Type u_1
A : Type u_4
B : Type u_5
C : Type u_6
M : Type u_7
inst✝⁷ : CommSemiring R
inst✝⁶ : Semiring A
inst✝⁵ : Semiring B
inst✝⁴ : Semiring C
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : Algebra R C
inst✝ : Monoid M
e₁ : A ≃ₐ[R] B
e₂ : B ≃ₐ[R] C
⊢ mapAlgEquiv R M (e₁.trans e₂) = (mapAlgEquiv R M e₁).trans (mapAlgEquiv R M e₂)

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
a : R
f : R[X]
⊢ C a * f = a • f

Tactic:
by

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

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
M : Type u_7
N : Type u_8
O : Type u_9
inst✝⁹ : CommSemiring R
inst✝⁸ : CommSemiring S
inst✝⁷ : Semiring A
inst✝⁶ : Semiring B
inst✝⁵ : Semiring C
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : Algebra R C
inst✝¹ : Monoid M
inst✝ : Monoid N
⊢ mapAlgEquiv R M 1 = 1

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.Extr

Goal state before:
pp: α : Type u
β : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b : α
f : α → β
h₀ : MonotoneOn f (Iic b)
h₁ : AntitoneOn f (Icc b a)
⊢ IsMaxOn f (Iic a) b

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
M : Type u_7
N : Type u_8
O : Type u_9
inst✝⁹ : CommSemiring R
inst✝⁸ : CommSemiring S
inst✝⁷ : Semiring A
inst✝⁶ : Semiring B
inst✝⁵ : Semiring C
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : Algebra R C
inst✝¹ : Monoid M
inst✝ : Monoid N
x y : A ≃ₐ[R] A
⊢ mapAlgEquiv R M (x * y) = mapAlgEquiv R M x * mapAlgEquiv R M y

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
k n : ℕ
⊢ (X ^ k).coeff n = if n = k then 1 else 0

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.Extr

Goal state before:
pp: α : Type u
β : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Preorder β
b : α
f : α → β
h₀ : MonotoneOn f (Iic b)
h₁ : AntitoneOn f (Ici b)
x : α
x✝ : x ∈ univ
⊢ x ∈ {x | (fun x ↦ f x ≤ f b) x}

Tactic:
rcases le_total x b

Goal state after:
case inl
α : Type u
β : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Preorder β
b : α
f : α → β
h₀ : MonotoneOn f (Iic b)
h₁ : AntitoneOn f (Ici b)
x : α
x✝ : x ∈ univ
h✝ : x ≤ b
⊢ x ∈ {x | (fun x ↦ f x ≤ f b) x}

case inr
α : Type u
β : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Preorder β
b : α
f : α → β
h₀ : MonotoneOn f (Iic b)
h₁ : AntitoneOn f (Ici b)
x : α
x✝ : x ∈ univ
h✝ : b ≤ x
⊢ x ∈ {x | (fun x ↦ f x ≤ f b) x}
Module: Mathlib.Algebra.Polynomial.Coeff

Goal state before:
pp: R : Type u
inst✝ : Semiring R
n : ℕ
⊢ (X ^ n).coeff n = 1

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.Extr

Goal state before:
pp: α : Type u
β : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Preorder β
b : α
f : α → β
h₀ : MonotoneOn f (Iic b)
h₁ : AntitoneOn f (Ici b)
x : α
x✝ : x ∈ univ
⊢ x ∈ {x | (fun x ↦ f x ≤ f b) x}

Tactic:
rcases le_total x b <;> aesop

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

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
M : Type u_7
N : Type u_8
O : Type u_9
inst✝⁹ : Monoid M
inst✝⁸ : CommSemiring R
V : Type u_10
W : Type u_11
inst✝⁷ : AddCommMonoid V
inst✝⁶ : Module R V
inst✝⁵ : Module R[M] V
inst✝⁴ : IsScalarTower R R[M] V
inst✝³ : AddCommMonoid W
inst✝² : Module R W
inst✝¹ : Module R[M] W
inst✝ : IsScalarTower R R[M] W
f : V →ₗ[R] W
h : ∀ (g : M) (v : V), f (single g 1 • v) = single g 1 • f v
v v' : V
⊢ f (v + v') = f v + f v'

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.Extr

Goal state before:
pp: α : Type u
β : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Preorder β
b : α
f : α → β
h₀ : MonotoneOn f (Iic b)
h₁ : AntitoneOn f (Ici b)
x : α
x✝ : x ∈ univ
⊢ x ∈ {x | (fun x ↦ f x ≤ f b) x}

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.Extr

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Preorder β
f g : α → β
a : α
l : Filter α
hle : g ≤ᶠ[l] f
hfga : f a = g a
h : IsMaxFilter f l a
⊢ IsMaxFilter g l a

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
k m : ℕ
hkm : k ≠ m
x y : R
hx : x ≠ 0
hy : y ≠ 0
⊢ (C x * X ^ k + C y * X ^ m).support = {k, m}

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.Extr

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Preorder β
f g : α → β
a : α
l : Filter α
h : IsExtrFilter f l a
heq : f =ᶠ[l] g
hfga : f a = g a
⊢ IsExtrFilter g l a

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.Extr

Goal state before:
pp: α : Type u
β : Type v
inst✝² : SemilatticeSup β
inst✝¹ : OrderBot β
D : α → β
s : Finset α
inst✝ : Nonempty α
b : β
hb : b ∈ range D
hmem : Function.invFun D b ∈ s
hmax : ∀ a ∈ s, D a ≤ b
⊢ s.sup D = b

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
k m n : ℕ
hkm : k < m
hmn : m < n
x y z : R
hx : x ≠ 0
hy : y ≠ 0
hz : z ≠ 0
⊢ (C x * X ^ k + C y * X ^ m + C z * X ^ n).support = {k, m, n}

Tactic:
by

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

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
M : Type u_7
N : Type u_8
O : Type u_9
inst✝⁹ : Monoid M
inst✝⁸ : CommSemiring R
V : Type u_10
W : Type u_11
inst✝⁷ : AddCommMonoid V
inst✝⁶ : Module R V
inst✝⁵ : Module R[M] V
inst✝⁴ : IsScalarTower R R[M] V
inst✝³ : AddCommMonoid W
inst✝² : Module R W
inst✝¹ : Module R[M] W
inst✝ : IsScalarTower R R[M] W
f : V →ₗ[R] W
h : ∀ (g : M) (v : V), f (single g 1 • v) = single g 1 • f v
c : R[M]
v : V
⊢ f (c • v) = (RingHom.id R[M]) c • f v

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
k m : ℕ
h : k ≠ m
x y : R
hx : x ≠ 0
hy : y ≠ 0
⊢ #(C x * X ^ k + C y * X ^ m).support = 2

Tactic:
by

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

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
M : Type u_7
N : Type u_8
O : Type u_9
inst✝⁵ : Semiring R
inst✝⁴ : Add M
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
f : Multiplicative M →ₙ* A
t' : R
a : R[M]
⊢ (↑((liftAddHom fun x ↦ (smulAddHom R A).flip (f (Multiplicative.ofAdd x))).comp coeffAddEquiv.toAddMonoidHom)).toFun
      (t' • a) =
    (MonoidHom.id R) t' •
      (↑((liftAddHom fun x ↦ (smulAddHom R A).flip (f (Multiplicative.ofAdd x))).comp
              coeffAddEquiv.toAddMonoidHom)).toFun
        a

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
k m n : ℕ
hkm : k < m
hmn : m < n
x y z : R
hx : x ≠ 0
hy : y ≠ 0
hz : z ≠ 0
⊢ #(C x * X ^ k + C y * X ^ m + C z * X ^ n).support = 3

Tactic:
by

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

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
M : Type u_7
N : Type u_8
O : Type u_9
inst✝⁵ : Semiring R
inst✝⁴ : Add M
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
f : Multiplicative M →ₙ* A
a₁ a₂ : R[M]
⊢ (↑((liftAddHom fun x ↦ (smulAddHom R A).flip (f (Multiplicative.ofAdd x))).comp coeffAddEquiv.toAddMonoidHom)).toFun
      (a₁ * a₂) =
    (↑((liftAddHom fun x ↦ (smulAddHom R A).flip (f (Multiplicative.ofAdd x))).comp coeffAddEquiv.toAddMonoidHom)).toFun
        a₁ *
      (↑((liftAddHom fun x ↦ (smulAddHom R A).flip (f (Multiplicative.ofAdd x))).comp
              coeffAddEquiv.toAddMonoidHom)).toFun
        a₂

Tactic:
by

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

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
M : Type u_7
N : Type u_8
O : Type u_9
inst✝⁵ : Semiring R
inst✝⁴ : Add M
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
f : Multiplicative M →ₙ* A
⊢ (fun F ↦ F.toMulHom.comp (ofMagma R M))
      ((fun f ↦
          let __AddMonoidHom :=
            (liftAddHom fun x ↦ (smulAddHom R A).flip (f (Multiplicative.ofAdd x))).comp coeffAddEquiv.toAddMonoidHom;
          { toFun := (↑__AddMonoidHom).toFun, map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯, map_mul' := ⋯ })
        f) =
    f

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✝² : SemilatticeSup B
inst✝¹ : OrderBot B
inst✝ : Semiring R
degb : A → B
f g : R[A]
⊢ (f + g).coeff.support.sup degb ≤ f.coeff.support.sup degb ⊔ g.coeff.support.sup degb

Tactic:
by

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

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
M : Type u_7
N : Type u_8
O : Type u_9
inst✝⁵ : Semiring R
inst✝⁴ : Add M
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
F : R[M] →ₙₐ[R] A
⊢ (fun f ↦
        let __AddMonoidHom :=
          (liftAddHom fun x ↦ (smulAddHom R A).flip (f (Multiplicative.ofAdd x))).comp coeffAddEquiv.toAddMonoidHom;
        { toFun := (↑__AddMonoidHom).toFun, map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯, map_mul' := ⋯ })
      ((fun F ↦ F.toMulHom.comp (ofMagma R M)) F) =
    F

Tactic:
by

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

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
M : Type u_7
N : Type u_8
O : Type u_9
inst✝⁵ : CommSemiring R
inst✝⁴ : AddMonoid M
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
f : A →ₐ[R] B
g : Multiplicative M →* B
h_comm : ∀ (x : A) (y : Multiplicative M), Commute (f x) (g y)
⊢ ∀ (r : R), (↑↑(liftNCRingHom (↑f) g h_comm)).toFun ((algebraMap R A[M]) r) = (algebraMap R B) r

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
M : Type u_7
N : Type u_8
O : Type u_9
inst✝⁵ : CommSemiring R
inst✝⁴ : AddMonoid M
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
f : Multiplicative M →* A
⊢ (fun f ↦ (↑f).comp (of R M)) ((fun F ↦ liftNCAlgHom (Algebra.ofId R A) F ⋯) f) = f

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✝⁶ : SemilatticeSup B
inst✝⁵ : OrderBot B
inst✝⁴ : Semiring R
inst✝³ : Add A
inst✝² : Add B
inst✝¹ : AddLeftMono B
inst✝ : AddRightMono B
degb : A → B
degbm : ∀ (a b : A), degb (a + b) ≤ degb a + degb b
f g : R[A]
⊢ (f * g).coeff.support.sup degb ≤ f.coeff.support.sup degb + g.coeff.support.sup degb

Tactic:
by

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

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
M : Type u_7
N : Type u_8
O : Type u_9
inst✝⁵ : CommSemiring R
inst✝⁴ : AddMonoid M
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
F : R[M] →ₐ[R] A
⊢ (fun F ↦ liftNCAlgHom (Algebra.ofId R A) F ⋯) ((fun f ↦ (↑f).comp (of R M)) F) = F

Tactic:
by

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

Goal state before:
pp: R : Type u_1
A : Type u_4
M : Type u_7
inst✝³ : CommSemiring R
inst✝² : AddMonoid M
inst✝¹ : Semiring A
inst✝ : Algebra R A
F : Multiplicative M →* A
f : R[M]
⊢ ((lift R A M) F) f = f.coeff.sum fun a b ↦ b • F (Multiplicative.ofAdd a)

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✝⁶ : SemilatticeSup B
inst✝⁵ : OrderBot B
inst✝⁴ : Semiring R
inst✝³ : AddMonoid A
inst✝² : AddMonoid B
inst✝¹ : AddLeftMono B
inst✝ : AddRightMono B
degb : A → B
degb0 : degb 0 ≤ 0
degbm : ∀ (a b : A), degb (a + b) ≤ degb a + degb b
a : A
ha : a ∈ (coeff 1).support
⊢ degb a ≤ 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✝⁶ : SemilatticeSup B
inst✝⁵ : OrderBot B
inst✝⁴ : Semiring R
inst✝³ : AddMonoid A
inst✝² : AddMonoid B
inst✝¹ : AddLeftMono B
inst✝ : AddRightMono B
degb : A → B
degb0 : degb 0 ≤ 0
degbm : ∀ (a b : A), degb (a + b) ≤ degb a + degb b
⊢ [].prod.coeff.support.sup degb ≤ (List.map (fun f ↦ f.coeff.support.sup degb) []).sum

Tactic:
by

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

Goal state before:
pp: R : Type u_1
A : Type u_4
M : Type u_7
inst✝³ : CommSemiring R
inst✝² : AddMonoid M
inst✝¹ : Semiring A
inst✝ : Algebra R A
F : R[M] →ₐ[R] A
f : R[M]
⊢ F f = f.coeff.sum fun m r ↦ r • F (single m 1)

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
n d : ℕ
⊢ (p * X ^ n).coeff d = if n ≤ d then p.coeff (d - n) else 0

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
n d : ℕ
⊢ (X ^ n * p).coeff d = if n ≤ d then p.coeff (d - n) else 0

Tactic:
by

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

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_4
M : Type u_7
inst✝⁷ : CommSemiring R
inst✝⁶ : AddMonoid M
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : CommSemiring S
inst✝² : Algebra S A
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R S A
f : Multiplicative M →* A
x : R[M]
⊢ ((lift S A M) f) ((mapRingHom M (algebraMap R S)) x) = ((lift R A M) f) x

Tactic:
by

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

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

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✝⁶ : SemilatticeSup B
inst✝⁵ : OrderBot B
inst✝⁴ : Semiring R
inst✝³ : AddMonoid A
inst✝² : AddMonoid B
inst✝¹ : AddLeftMono B
inst✝ : AddRightMono B
degb : A → B
degb0 : degb 0 ≤ 0
degbm : ∀ (a b : A), degb (a + b) ≤ degb a + degb b
f : R[A]
fs : List R[A]
⊢ (f :: fs).prod.coeff.support.sup degb ≤ (List.map (fun f ↦ f.coeff.support.sup degb) (f :: fs)).sum

Tactic:
by

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

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

Tactic:
rw [(commute_X p).eq, coeff_mul_X]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
M : Type u_7
N : Type u_8
O : Type u_9
inst✝⁵ : CommSemiring R
inst✝⁴ : AddMonoid M
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
⊢ Additive.ofMul (domCongr R A 0) = 0

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
M : Type u_7
N : Type u_8
O : Type u_9
inst✝⁵ : CommSemiring R
inst✝⁴ : AddMonoid M
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
x✝¹ x✝ : AddAut M
⊢ Additive.ofMul (domCongr R A (x✝¹ + x✝)) = Additive.ofMul (domCongr R A x✝¹) + Additive.ofMul (domCongr R A x✝)

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
M : Type u_7
N : Type u_8
O : Type u_9
inst✝³ : CommSemiring R
inst✝² : AddMonoid M
inst✝¹ : Semiring A
inst✝ : Algebra R A
⊢ mapAlgEquiv R M 1 = 1

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✝⁶ : SemilatticeInf T
inst✝⁵ : OrderTop T
inst✝⁴ : Semiring R
inst✝³ : AddMonoid A
inst✝² : AddMonoid T
inst✝¹ : AddLeftMono T
inst✝ : AddRightMono T
degt : A → T
degt0 : 0 ≤ degt 0
degtm : ∀ (a b : A), degt a + degt b ≤ degt (a + b)
l : List R[A]
⊢ (List.map (fun f ↦ f.coeff.support.inf degt) l).sum ≤ l.prod.coeff.support.inf degt

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
M : Type u_7
N : Type u_8
O : Type u_9
inst✝³ : CommSemiring R
inst✝² : AddMonoid M
inst✝¹ : Semiring A
inst✝ : Algebra R A
x y : A ≃ₐ[R] A
⊢ mapAlgEquiv R M (x * y) = mapAlgEquiv R M x * mapAlgEquiv R M y

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✝⁶ : SemilatticeSup B
inst✝⁵ : OrderBot B
inst✝⁴ : Semiring R
inst✝³ : AddMonoid A
inst✝² : AddMonoid B
inst✝¹ : AddLeftMono B
inst✝ : AddRightMono B
degb : A → B
degb0 : degb 0 ≤ 0
degbm : ∀ (a b : A), degb (a + b) ≤ degb a + degb b
n : ℕ
f : R[A]
⊢ (f ^ n).coeff.support.sup degb ≤ n • f.coeff.support.sup degb

Tactic:
by

Goal state after: