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✝⁶ : Semiring A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid O
f : M →* A
⊢ (fun f ↦ (↑f).comp (of R M)) ((fun F ↦ liftNCAlgHom (Algebra.ofId R A) F ⋯) f) = f

Tactic:
ext

Goal state after:
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✝⁶ : Semiring A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid O
f : M →* A
x✝ : M
⊢ ((fun f ↦ (↑f).comp (of R M)) ((fun F ↦ liftNCAlgHom (Algebra.ofId R A) F ⋯) f)) x✝ = f x✝
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✝⁶ : Semiring A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid O
F : R[M] →ₐ[R] A
⊢ (fun F ↦ liftNCAlgHom (Algebra.ofId R A) F ⋯) ((fun f ↦ (↑f).comp (of R M)) F) = F

Tactic:
ext

Goal state after:
case single_one_right
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✝⁶ : Semiring A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid O
F : R[M] →ₐ[R] A
m✝ : M
⊢ ((fun F ↦ liftNCAlgHom (Algebra.ofId R A) F ⋯) ((fun f ↦ (↑f).comp (of R M)) F)) (single m✝ 1) = F (single m✝ 1)
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
⊢ mapDomainAlgHom R A (MonoidHom.id M) = AlgHom.id R A[M]

Tactic:
ext

Goal state after:
case single_one_right
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
m✝ a✝ : M
⊢ ((mapDomainAlgHom R A (MonoidHom.id M)) (single m✝ 1)).coeff a✝ = ((AlgHom.id R A[M]) (single m✝ 1)).coeff a✝

case single_one_left
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
x✝ : A
a✝ : M
⊢ (((mapDomainAlgHom R A (MonoidHom.id M)).comp singleOneAlgHom) x✝).coeff a✝ =
    (((AlgHom.id R A[M]).comp singleOneAlgHom) x✝).coeff a✝
Module: Mathlib.Algebra.MonoidAlgebra.Basic

Goal state before:
pp: R : Type u_1
A : Type u_4
M : Type u_7
N : Type u_8
O : Type u_9
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid O
f : M →* N
g : N →* O
⊢ mapDomainAlgHom R A (g.comp f) = (mapDomainAlgHom R A g).comp (mapDomainAlgHom R A f)

Tactic:
ext

Goal state after:
case single_one_right
R : Type u_1
A : Type u_4
M : Type u_7
N : Type u_8
O : Type u_9
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid O
f : M →* N
g : N →* O
m✝ : M
a✝ : O
⊢ ((mapDomainAlgHom R A (g.comp f)) (single m✝ 1)).coeff a✝ =
    (((mapDomainAlgHom R A g).comp (mapDomainAlgHom R A f)) (single m✝ 1)).coeff a✝

case single_one_left
R : Type u_1
A : Type u_4
M : Type u_7
N : Type u_8
O : Type u_9
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid O
f : M →* N
g : N →* O
x✝ : A
a✝ : O
⊢ (((mapDomainAlgHom R A (g.comp f)).comp singleOneAlgHom) x✝).coeff a✝ =
    ((((mapDomainAlgHom R A g).comp (mapDomainAlgHom R A f)).comp singleOneAlgHom) x✝).coeff a✝
Module: Mathlib.Order.Filter.Extr

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

Tactic:
intro x hx
  by_cases! g₀ : x ≤ b
  · exact h₀ ⟨hx.1, g₀⟩ (right_mem_Icc.2 (hx.1.trans g₀)) g₀
  · exact h₁ (left_mem_Icc.2 (g₀.le.trans hx.2)) ⟨g₀.le, hx.2⟩ g₀.le

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✝⁶ : Semiring A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid O
e : M ≃* N
x✝ : R
⊢ (mapDomainRingEquiv A e).toFun ((algebraMap R A[M]) x✝) = (algebraMap R A[N]) x✝

Tactic:
ext

Goal state after:
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✝⁶ : Semiring A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid O
e : M ≃* N
x✝ : R
a✝ : N
⊢ ((mapDomainRingEquiv A e).toFun ((algebraMap R A[M]) x✝)).coeff a✝ = ((algebraMap R A[N]) x✝).coeff a✝
Module: Mathlib.Algebra.MonoidAlgebra.Basic

Goal state before:
pp: R : Type u_1
A : Type u_4
M : Type u_7
N : Type u_8
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Monoid M
inst✝ : Monoid N
e : M ≃* N
m : M
⊢ (domCongr R A e).toLinearMap ∘ₗ lsingle m = lsingle (e m)

Tactic:
ext

Goal state after:
R : Type u_1
A : Type u_4
M : Type u_7
N : Type u_8
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Monoid M
inst✝ : Monoid N
e : M ≃* N
m : M
x✝ : A
a✝ : N
⊢ (((domCongr R A e).toLinearMap ∘ₗ lsingle m) x✝).coeff a✝ = ((lsingle (e m)) x✝).coeff a✝
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
⊢ domCongr R A (MulEquiv.refl M) = AlgEquiv.refl

Tactic:
ext

Goal state after:
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
a✝¹ : A[M]
a✝ : M
⊢ ((domCongr R A (MulEquiv.refl M)) a✝¹).coeff a✝ = (AlgEquiv.refl a✝¹).coeff a✝
Module: Mathlib.Algebra.MonoidAlgebra.Basic

Goal state before:
pp: R : Type u_1
A : Type u_4
M : Type u_7
N : Type u_8
O : Type u_9
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid O
e : M ≃* N
f : N ≃* O
⊢ (domCongr R A e).trans (domCongr R A f) = domCongr R A (e.trans f)

Tactic:
ext

Goal state after:
R : Type u_1
A : Type u_4
M : Type u_7
N : Type u_8
O : Type u_9
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid O
e : M ≃* N
f : N ≃* O
a✝¹ : A[M]
a✝ : O
⊢ (((domCongr R A e).trans (domCongr R A f)) a✝¹).coeff a✝ = ((domCongr R A (e.trans f)) a✝¹).coeff a✝
Module: Mathlib.Algebra.MonoidAlgebra.Basic

Goal state before:
pp: R : Type u_1
A : Type u_4
M : Type u_7
N : Type u_8
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Monoid M
inst✝ : Monoid N
f : M →* N
⊢ (mapDomainRingHom A f).comp (algebraMap R A[M]) = algebraMap R A[N]

Tactic:
ext

Goal state after:
R : Type u_1
A : Type u_4
M : Type u_7
N : Type u_8
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Monoid M
inst✝ : Monoid N
f : M →* N
x✝ : R
a✝ : N
⊢ (((mapDomainRingHom A f).comp (algebraMap R A[M])) x✝).coeff a✝ = ((algebraMap R A[N]) x✝).coeff a✝
Module: Mathlib.Algebra.MonoidAlgebra.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_7
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Monoid M
f : R →+* S
⊢ (mapRingHom M f).comp (algebraMap R R[M]) = (algebraMap S S[M]).comp f

Tactic:
ext

Goal state after:
R : Type u_1
S : Type u_2
M : Type u_7
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Monoid M
f : R →+* S
x✝ : R
a✝ : M
⊢ (((mapRingHom M f).comp (algebraMap R R[M])) x✝).coeff a✝ = (((algebraMap S S[M]).comp f) x✝).coeff a✝
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:
ext

Goal state after:
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
a✝ : M
⊢ ((mapAlgHom M f) (single m a)).coeff a✝ = (single m (f a)).coeff a✝
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:
ext

Goal state after:
case single_one_right
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
m✝ a✝ : M
⊢ ((mapAlgHom M (AlgHom.id R A)) (single m✝ 1)).coeff a✝ = ((AlgHom.id R A[M]) (single m✝ 1)).coeff a✝

case single_one_left
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
x✝ : A
a✝ : M
⊢ (((mapAlgHom M (AlgHom.id R A)).comp singleOneAlgHom) x✝).coeff a✝ =
    (((AlgHom.id R A[M]).comp singleOneAlgHom) x✝).coeff a✝
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:
ext

Goal state after:
case single_one_right
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
m✝ a✝ : M
⊢ ((mapAlgHom M (g.comp f)) (single m✝ 1)).coeff a✝ = (((mapAlgHom M g).comp (mapAlgHom M f)) (single m✝ 1)).coeff a✝

case single_one_left
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
x✝ : A
a✝ : M
⊢ (((mapAlgHom M (g.comp f)).comp singleOneAlgHom) x✝).coeff a✝ =
    ((((mapAlgHom M g).comp (mapAlgHom M f)).comp singleOneAlgHom) x✝).coeff a✝
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
  rw [← pow_one X, coeff_C_mul_X_pow]

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:
ext

Goal state after:
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
a✝¹ : A[M]
a✝ : M
⊢ ((mapAlgEquiv R M (e₁.trans e₂)) a✝¹).coeff a✝ = (((mapAlgEquiv R M e₁).trans (mapAlgEquiv R M e₂)) a✝¹).coeff a✝
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:
ext

Goal state after:
R : Type u
inst✝ : Semiring R
a : R
f : R[X]
n✝ : ℕ
⊢ (C a * f).coeff n✝ = (a • f).coeff n✝
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:
ext

Goal state after:
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
a✝¹ : A[M]
a✝ : M
⊢ ((mapAlgEquiv R M 1) a✝¹).coeff a✝ = (1 a✝¹).coeff a✝
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:
ext

Goal state after:
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
a✝¹ : A[M]
a✝ : M
⊢ ((mapAlgEquiv R M (x * y)) a✝¹).coeff a✝ = ((mapAlgEquiv R M x * mapAlgEquiv R M y) a✝¹).coeff a✝
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:
ext

Goal state after:
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
x✝ : Multiplicative M
⊢ ((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))
      x✝ =
    f x✝
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:
ext

Goal state after:
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
x✝ : Multiplicative 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' := ⋯ })
              ((fun F ↦ F.toMulHom.comp (ofMagma R M)) F)).toMulHom.comp
        (ofMagma R M))
      x✝ =
    (F.toMulHom.comp (ofMagma R M)) x✝
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:
ext

Goal state after:
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
x✝ : M
⊢ Additive.toMul
      ((MonoidHom.toAdditiveRight ((fun f ↦ (↑f).comp (of R M)) ((fun F ↦ liftNCAlgHom (Algebra.ofId R A) F ⋯) f)))
        x✝) =
    Additive.toMul ((MonoidHom.toAdditiveRight f) x✝)
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:
ext

Goal state after:
case single_zero_right
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
m✝ : M
⊢ ((fun F ↦ liftNCAlgHom (Algebra.ofId R A) F ⋯) ((fun f ↦ (↑f).comp (of R M)) F)) (single m✝ 1) = F (single m✝ 1)
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:
ext

Goal state after:
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
a✝¹ : A[M]
a✝ : M
⊢ ((Additive.toMul (Additive.ofMul (domCongr R A 0))) a✝¹).coeff a✝ = ((Additive.toMul 0) a✝¹).coeff a✝
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:
ext

Goal state after:
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
a✝¹ : A[M]
a✝ : M
⊢ ((Additive.toMul (Additive.ofMul (domCongr R A (x✝¹ + x✝)))) a✝¹).coeff a✝ =
    ((Additive.toMul (Additive.ofMul (domCongr R A x✝¹) + Additive.ofMul (domCongr R A x✝))) a✝¹).coeff a✝
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:
ext

Goal state after:
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
a✝¹ : A[M]
a✝ : M
⊢ ((mapAlgEquiv R M 1) a✝¹).coeff a✝ = (1 a✝¹).coeff a✝
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:
ext

Goal state after:
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
a✝¹ : A[M]
a✝ : M
⊢ ((mapAlgEquiv R M (x * y)) a✝¹).coeff a✝ = ((mapAlgEquiv R M x * mapAlgEquiv R M y) a✝¹).coeff a✝
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✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : AddMonoid M
r : R
⊢ (toMultiplicative A M).toFun ((algebraMap R A[M]) r) = (algebraMap R (MonoidAlgebra A (Multiplicative M))) r

Tactic:
ext

Goal state after:
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✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : AddMonoid M
r : R
a✝ : Multiplicative M
⊢ ((toMultiplicative A M).toFun ((algebraMap R A[M]) r)).coeff a✝ =
    ((algebraMap R (MonoidAlgebra A (Multiplicative M))) r).coeff a✝
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✝ : AddMonoid M
m : M
a : A
⊢ (toMultiplicativeAlgEquiv R A M) (single m a) = MonoidAlgebra.single (Multiplicative.ofAdd m) a

Tactic:
ext

Goal state after:
R : Type u_1
A : Type u_4
M : Type u_7
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : AddMonoid M
m : M
a : A
a✝ : Multiplicative M
⊢ ((toMultiplicativeAlgEquiv R A M) (single m a)).coeff a✝ = (MonoidAlgebra.single (Multiplicative.ofAdd m) a).coeff a✝
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
m : M
a : A
⊢ (toAdditiveAlgEquiv R A M) (single m a) = AddMonoidAlgebra.single (Additive.ofMul m) a

Tactic:
ext

Goal state after:
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
m : M
a : A
a✝ : Additive M
⊢ ((toAdditiveAlgEquiv R A M) (single m a)).coeff a✝ = (AddMonoidAlgebra.single (Additive.ofMul m) a).coeff a✝
Module: Mathlib.Algebra.Polynomial.Degree.Defs

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
hp : p ≠ 0
⊢ p.degree = ↑n ↔ p.natDegree = n

Tactic:
rw [degree_eq_natDegree hp]; exact WithBot.coe_eq_coe

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
n : ℕ
a : R
⊢ ((monomial n) a).degree ≤ ↑n

Tactic:
apply degree_monomial_le

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
r : R
φ : R[X]
⊢ C r ∣ φ ↔ ∀ (i : ℕ), r ∣ φ.coeff i

Tactic:
constructor

Goal state after:
case mp
R : Type u
inst✝ : Semiring R
r : R
φ : R[X]
⊢ C r ∣ φ → ∀ (i : ℕ), r ∣ φ.coeff i

case mpr
R : Type u
inst✝ : Semiring R
r : R
φ : R[X]
⊢ (∀ (i : ℕ), r ∣ φ.coeff i) → C r ∣ φ