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

Goal state before:
pp: R : Type u_1
X : Type u_2
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
x✝ : X
a✝ : FreeMonoid X
⊢ (((↑(((lift R) fun x ↦ (MonoidAlgebra.of R (FreeMonoid X)) (FreeMonoid.of x)).comp
                  ((MonoidAlgebra.lift R (FreeAlgebra R X) (FreeMonoid X)) (FreeMonoid.lift (ι R))))).comp
            (MonoidAlgebra.of R (FreeMonoid X)))
          (FreeMonoid.of x✝)).coeff
      a✝ =
    (((↑(AlgHom.id R R[FreeMonoid X])).comp (MonoidAlgebra.of R (FreeMonoid X))) (FreeMonoid.of x✝)).coeff a✝

Tactic:
simp

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

Goal state before:
pp: case zero
R : Type u
inst✝ : Semiring R
p : R[X]
x : R
⊢ eval x (p * X ^ 0) = eval x p * x ^ 0

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.FreeAlgebra

Goal state before:
pp: R : Type u_1
X : Type u_2
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
x✝ : X
⊢ (⇑(((MonoidAlgebra.lift R (FreeAlgebra R X) (FreeMonoid X)) (FreeMonoid.lift (ι R))).comp
            ((lift R) fun x ↦ (MonoidAlgebra.of R (FreeMonoid X)) (FreeMonoid.of x))) ∘
        ι R)
      x✝ =
    (⇑(AlgHom.id R (FreeAlgebra R X)) ∘ ι R) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.FreeAlgebra

Goal state before:
pp: R : Type u_1
X : Type u_2
inst✝ : CommSemiring R
x : R
⊢ algebraMapInv ((algebraMap R (FreeAlgebra R X)) x) = x

Tactic:
simp

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

Goal state before:
pp: case zero
R : Type u
inst✝ : Semiring R
p : R[X]
⊢ (X ^ 0).comp p = p ^ 0

Tactic:
simp

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

Goal state before:
pp: case zero
R : Type u
inst✝ : Semiring R
p r : R[X]
⊢ (p * X ^ 0).comp r = p.comp r * r ^ 0

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
x✝ : R
n✝ : ℕ
⊢ (((mapRingHom f).comp C) x✝).coeff n✝ = ((C.comp f) x✝).coeff n✝

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p q : R[X]
⊢ ∀ (a : R), map f ((C a).comp q) = (map f (C a)).comp (map f q)

Tactic:
simp

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

Goal state before:
pp: case monomial
R : Type u
inst✝ : CommSemiring R
p q : R[X]
x : R
n : ℕ
a : R
⊢ eval x (((monomial n) a).comp q) = eval (eval x q) ((monomial n) a)

Tactic:
simp

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

Goal state before:
pp: case ofNat
R : Type u
inst✝ : Ring R
p : R[X]
a✝ : ℕ
⊢ (↑(Int.ofNat a✝)).comp p = ↑(Int.ofNat a✝)

Tactic:
simp

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

Goal state before:
pp: case negSucc
R : Type u
inst✝ : Ring R
p : R[X]
a✝ : ℕ
⊢ (↑(Int.negSucc a✝)).comp p = ↑(Int.negSucc a✝)

Tactic:
simp

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

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
p : R[X]
S : Type u_1
inst✝ : Ring S
f : R →+* S
n : ℤ
⊢ ↑n = f ↑n

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : Ring S
σ : R →+* S
E : Type u_4
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_5
inst✝¹ : AddCommGroup F
inst✝ : Module S F
c : Set (E →ₛₗ.[σ] F)
hnonempty : c.Nonempty
hc : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) c
x : E
⊢ (∃ y ∈ domain '' c, x ∈ y) ↔ ∃ f ∈ c, x ∈ f.domain

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: R : Type u_1
S✝ : Type u_2
T : Type u_3
inst✝⁸ : Ring R
inst✝⁷ : Ring S✝
inst✝⁶ : Ring T
σ : R →+* S✝
τ : S✝ →+* T
E : Type u_4
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module R E
F : Type u_5
inst✝³ : AddCommGroup F
inst✝² : Module S✝ F
G : Type u_6
inst✝¹ : AddCommGroup G
inst✝ : Module T G
f : E →ₛₗ.[σ] F
S : Submodule R E
⊢ S ⊓ f.domain ≤ f.domain

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: R : Type u_1
S✝ : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : Ring S✝
σ : R →+* S✝
E : Type u_4
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_5
inst✝¹ : AddCommGroup F
inst✝ : Module S✝ F
f : E →ₛₗ.[σ] F
S : Submodule R E
x : ↥(S ⊓ f.domain)
y : ↥f.domain
h : ↑x = ↑y
⊢ S ⊓ f.domain ≤ f.domain

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: R : Type u_1
S✝ : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : Ring S✝
σ : R →+* S✝
E : Type u_4
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_5
inst✝¹ : AddCommGroup F
inst✝ : Module S✝ F
f : E →ₛₗ.[σ] F
S : Submodule R E
⊢ (f.domRestrict S).domain ≤ f.domain

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: R : Type u_1
inst✝⁴ : Ring R
E : Type u_4
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_5
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f : E →ₗ.[R] F
x : ↥f.domain
⊢ (↑x, ↑f x) ∈ f.graph

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: R : Type u_1
inst✝⁴ : Ring R
E : Type u_4
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_5
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f : E →ₗ.[R] F
x✝ : F
⊢ x✝ ∈ Submodule.map (LinearMap.snd R E F) f.graph ↔ x✝ ∈ f.toFun.range

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.CharP.Defs

Goal state before:
pp: case inr.inl
R : Type u_1
inst✝¹ : AddGroupWithOne R
p : ℕ
inst✝ : CharP R p
⊢ ↑0 = 0 ↔ ↑p ∣ 0

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.CharP.Defs

Goal state before:
pp: R : Type u_1
inst✝ : NonAssocSemiring R
this : DecidableEq R := Classical.decEq R
H : ∀ (p : ℕ), ↑p = 0 → p = 0
⊢ ↑0 = 0

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Nat.Prime.Defs

Goal state before:
pp: n m✝ : ℕ
n1 : n = 1
m2 : 2 ≤ m✝
x✝ : m✝ ∣ n
⊢ minFac 1 ≤ 2

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: R : Type u_1
inst✝⁴ : Ring R
E : Type u_4
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_5
inst✝¹ : AddCommGroup F
inst✝ : Module R F
g : Submodule R (E × F)
hg : ∀ {x : E × F}, x ∈ g → x.1 = 0 → x.2 = 0
a : E
ha : a ∈ map (LinearMap.fst R E F) g
⊢ (∃ x, (a, x) ∈ g) ↔ a ∈ map (LinearMap.fst R E F) g

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: R : Type u_1
inst✝⁴ : Ring R
E : Type u_4
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_5
inst✝¹ : AddCommGroup F
inst✝ : Module R F
g : Submodule R (E × F)
hg : ∀ {x : E × F}, x ∈ g → x.1 = 0 → x.2 = 0
a : E
ha : a ∈ map (LinearMap.fst R E F) g
y₁ y₂ : F
hy₁ : (a, y₁) ∈ g
hy₂ : (a, y₂) ∈ g
hy : (0, y₁ - y₂) ∈ g
⊢ (0, y₁ - y₂).1 = 0

Tactic:
simp

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✝⁴ : Mul M
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
f : M →ₙ* A
x✝ : M
⊢ ((fun F ↦ F.toMulHom.comp (ofMagma R M))
        ((fun f ↦
            let __AddMonoidHom := (liftAddHom fun x ↦ (smulAddHom R A).flip (f x)).comp coeffAddEquiv.toAddMonoidHom;
            { toFun := (↑__AddMonoidHom).toFun, map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯, map_mul' := ⋯ })
          f))
      x✝ =
    f x✝

Tactic:
simp

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✝⁴ : Mul M
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
F : R[M] →ₙₐ[R] A
x✝ : M
⊢ (((fun f ↦
                let __AddMonoidHom :=
                  (liftAddHom fun x ↦ (smulAddHom R A).flip (f 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✝

Tactic:
simp

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✝² : Algebra R A
inst✝¹ : Monoid M
inst✝ : Monoid N
r : R
a✝ : M
⊢ ((↑↑singleOneRingHom).toFun ((algebraMap R A) r)).coeff a✝ = ((algebraMap R A[M]) r).coeff a✝

Tactic:
simp

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✝¹ : Monoid M
inst✝ : Monoid N
r : R
a✝ : M
⊢ (Finsupp.single 1 ((algebraMap R A) r)) a✝ = ((algebraMap R A[M]) r).coeff a✝
Module: Mathlib.Algebra.MonoidAlgebra.Basic

Goal state before:
pp: R : Type u_1
M : Type u_7
inst✝¹ : CommSemiring R
inst✝ : Monoid M
m : M
r : R
⊢ single m r = (algebraMap R R[M]) r * (of R M) m

Tactic:
simp

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
m : M
r : R
⊢ single m ((algebraMap R A) r) = (algebraMap R A[M]) r * (of A M) m

Tactic:
simp

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✝³ : Algebra R A
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Subsingleton M
r : R
⊢ (uniqueRingEquiv M).toFun ((algebraMap R A[M]) r) = (algebraMap R A) r

Tactic:
simp

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

Goal state before:
pp: case zero
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
φ₁ φ₂ : A[M] →ₐ[R] B
single_one_right : ∀ (m : M), φ₁ (single m 1) = φ₂ (single m 1)
single_one_left : φ₁.comp singleOneAlgHom = φ₂.comp singleOneAlgHom
⊢ φ₁ 0 = φ₂ 0

Tactic:
simp

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
f : M →* A
x✝ : M
⊢ ((fun f ↦ (↑f).comp (of R M)) ((fun F ↦ liftNCAlgHom (Algebra.ofId R A) F ⋯) f)) x✝ = f x✝

Tactic:
simp

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

Goal state before:
pp: 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)

Tactic:
simp

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
F : M →* A
m : M
⊢ ((lift R A M) F) ((of R M) m) = F m

Tactic:
simp

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

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

Tactic:
simp

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
f : M →* N
⊢ ∀ (r : R), (↑↑(mapDomainRingHom A f)).toFun ((algebraMap R A[M]) r) = (algebraMap R A[N]) r

Tactic:
simp

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

Goal state before:
pp: 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✝

Tactic:
simp

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

Goal state before:
pp: 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✝

Tactic:
simp

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

Goal state before:
pp: 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✝

Tactic:
simp

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

Goal state before:
pp: 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✝

Tactic:
simp

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
a✝ : N
⊢ ((mapDomainRingEquiv A e).toFun ((algebraMap R A[M]) x✝)).coeff a✝ = ((algebraMap R A[N]) x✝).coeff a✝

Tactic:
simp

Goal state after:
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
x✝ : A
a✝ : N
⊢ (((domCongr R A e).toLinearMap ∘ₗ lsingle m) x✝).coeff a✝ = ((lsingle (e m)) x✝).coeff a✝

Tactic:
simp

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
a✝¹ : A[M]
a✝ : M
⊢ ((domCongr R A (MulEquiv.refl M)) a✝¹).coeff a✝ = (AlgEquiv.refl a✝¹).coeff a✝

Tactic:
simp

Goal state after:
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
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✝

Tactic:
simp

Goal state after:
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
x✝ : R
a✝ : N
⊢ (((mapDomainRingHom A f).comp (algebraMap R A[M])) x✝).coeff a✝ = ((algebraMap R A[N]) x✝).coeff a✝

Tactic:
simp

Goal state after:
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
x✝ : R
a✝ : M
⊢ (((mapRingHom M f).comp (algebraMap R R[M])) x✝).coeff a✝ = (((algebraMap S S[M]).comp f) x✝).coeff a✝

Tactic:
simp

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
f : A →ₐ[R] B
⊢ ∀ (r : R), (↑↑(mapRingHom M ↑f)).toFun ((algebraMap R A[M]) r) = (algebraMap R B[M]) r

Tactic:
simp

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
  intro x hx
  by_cases! g₀ : x ≤ b
  · exact h₀ ⟨hx, g₀⟩ (right_mem_Icc.2 (hx.trans g₀)) g₀
  · exact h₁ self_mem_Ici g₀.le g₀.le

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

Goal state before:
pp: 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✝

Tactic:
simp

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

Goal state before:
pp: 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✝

Tactic:
simp

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

Goal state before:
pp: 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✝

Tactic:
simp

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

Goal state before:
pp: 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✝

Tactic:
simp

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

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

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

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
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✝

Tactic:
simp

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

Tactic:
simp

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Goal state before:
pp: case refine_1
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 (0 • v) = (RingHom.id R[M]) 0 • f v

Tactic:
simp

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 : IsMinFilter f l a ∨ IsMaxFilter f l a
heq : f =ᶠ[l] g
hfga : f a = g a
⊢ IsMinFilter g l a ∨ IsMaxFilter g l a

Tactic:
rwa [← heq.isMaxFilter_iff hfga, ← heq.isMinFilter_iff hfga]

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
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✝

Tactic:
simp

Goal state after: