awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.MonoidAlgebra.Basic
Goal:
R : Type u_1
A : Type u_4
M : Type u_7
N : Type u_8
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Monoid M
inst_4 : Monoid N
e : M ≃* N
m : M
h :
  ∀ (x : A) (m_1 : N),
    Eq.{u_4 + 1} (α := A)
      ((((AlgEquiv.toLinearMap (domCongr R A e) ∘ₗ lsingle m : (a : A) → A[N]) x : A[N]) : (a : N) → A) m_1 : A)
      (((((lsingle ((e : (a : M) → N) m) : A →ₗ[R] A[N]) : (a : A) → A[N]) x : A[N]) : (a : N) → A) m_1 : A)
⊢ Eq (α := A →ₗ[R] A[N]) (AlgEquiv.toLinearMap (domCongr R A e) ∘ₗ lsingle m) (lsingle ((e : (a : M) → N) m))

Tactic:
ext
-- Module: Mathlib.Algebra.MonoidAlgebra.Basic
Goal:
R : Type u_1
A : Type u_4
M : Type u_7
N : Type u_8
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Monoid M
inst_4 : Monoid N
e : M ≃* N
m : M
x : A
m_1 : N
⊢ Eq.{u_4 + 1} (α := A)
    ((((AlgEquiv.toLinearMap (domCongr R A e) ∘ₗ lsingle m : (a : A) → A[N]) x : A[N]) : (a : N) → A) m_1 : A)
    (((((lsingle ((e : (a : M) → N) m) : A →ₗ[R] A[N]) : (a : A) → A[N]) x : A[N]) : (a : N) → A) m_1 : A)

Tactic:
simp
-- Module: Mathlib.Algebra.MonoidAlgebra.Basic
Goal:
R : Type u_1
A : Type u_4
M : Type u_7
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Monoid M
h :
  ∀ (a : A[M]) (m : M),
    Eq.{u_4 + 1} (α := A) ((((domCongr R A (MulEquiv.refl M) : (a : A[M]) → A[M]) a : A[M]) : (a : M) → A) m : A)
      ((((AlgEquiv.refl : (a : A[M]) → A[M]) a : A[M]) : (a : M) → A) m : A)
⊢ Eq (α := A[M] ≃ₐ[R] A[M]) (domCongr R A (MulEquiv.refl M)) AlgEquiv.refl

Tactic:
ext
-- Module: Mathlib.Algebra.MonoidAlgebra.Basic
Goal:
R : Type u_1
A : Type u_4
M : Type u_7
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Monoid M
a : A[M]
m : M
⊢ Eq.{u_4 + 1} (α := A) ((((domCongr R A (MulEquiv.refl M) : (a : A[M]) → A[M]) a : A[M]) : (a : M) → A) m : A)
    ((((AlgEquiv.refl : (a : A[M]) → A[M]) a : A[M]) : (a : M) → A) m : A)

Tactic:
simp
-- Module: Mathlib.Algebra.MonoidAlgebra.Basic
Goal:
R : Type u_1
A : Type u_4
M : Type u_7
N : Type u_8
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Monoid M
inst_4 : Monoid N
e : M ≃* N
⊢ Eq (α := A[N] ≃ₐ[R] A[M]) (AlgEquiv.symm (domCongr R A e)) (domCongr R A e.symm)

Tactic:
rfl

Premises used: AlgEquiv.symm, MonoidAlgebra.domCongr, Equiv.symm, MulEquiv.symm, rfl
-- Module: Mathlib.Algebra.MonoidAlgebra.Basic
Goal:
R : Type u_1
A : Type u_4
M : Type u_7
N : Type u_8
O : Type u_9
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Monoid M
inst_4 : Monoid N
inst_5 : Monoid O
e : M ≃* N
f : N ≃* O
h :
  ∀ (a : A[M]) (m : O),
    Eq.{u_4 + 1} (α := A)
      ((((AlgEquiv.trans (domCongr R A e) (domCongr R A f) : (a : A[M]) → A[O]) a : A[O]) : (a : O) → A) m : A)
      ((((domCongr R A (e.trans f) : (a : A[M]) → A[O]) a : A[O]) : (a : O) → A) m : A)
⊢ Eq (α := A[M] ≃ₐ[R] A[O]) (AlgEquiv.trans (domCongr R A e) (domCongr R A f)) (domCongr R A (e.trans f))

Tactic:
ext
-- Module: Mathlib.Algebra.MonoidAlgebra.Basic
Goal:
R : Type u_1
A : Type u_4
M : Type u_7
N : Type u_8
O : Type u_9
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Monoid M
inst_4 : Monoid N
inst_5 : Monoid O
e : M ≃* N
f : N ≃* O
a : A[M]
m : O
⊢ Eq.{u_4 + 1} (α := A)
    ((((AlgEquiv.trans (domCongr R A e) (domCongr R A f) : (a : A[M]) → A[O]) a : A[O]) : (a : O) → A) m : A)
    ((((domCongr R A (e.trans f) : (a : A[M]) → A[O]) a : A[O]) : (a : O) → A) m : A)

Tactic:
simp
-- Module: Mathlib.Algebra.MonoidAlgebra.Basic
Goal:
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_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : Monoid M
inst_6 : Monoid N
inst_7 : Monoid O
rw : Eq (α := A[M] ≃ₐ[R] A[M]) (domCongr R A (MulEquiv.refl M)) 1
rw₁ : Eq (α := A[M] ≃ₐ[R] A[M]) (domCongr R A (MulEquiv.refl M)) AlgEquiv.refl
rw₂ rw₃ : Eq (α := A[M] ≃ₐ[R] A[M]) AlgEquiv.refl AlgEquiv.refl
⊢ Eq (α := A[M] ≃ₐ[R] A[M]) (domCongr R A 1) 1

Tactic:
rw [MulAut.one_def, AlgEquiv.aut_one, domCongr_refl]

Premises used: AlgEquiv.aut_one, MulAut.one_def, MonoidAlgebra.domCongr_refl
-- Module: Mathlib.Algebra.MonoidAlgebra.Basic
Goal:
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_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : Monoid M
inst_6 : Monoid N
inst_7 : Monoid O
x x_1 : MulAut M
rw : domCongr R A (MulEquiv.trans x_1 x) = HMul.hMul (α := A[M] ≃ₐ[R] A[M]) (domCongr R A x) (domCongr R A x_1)
rw₁ :
  Eq (α := A[M] ≃ₐ[R] A[M]) (domCongr R A (MulEquiv.trans x_1 x)) (AlgEquiv.trans (domCongr R A x_1) (domCongr R A x))
rw₂ rw₃ : Eq (α := A[M] ≃ₐ[R] A[M]) (domCongr R A (MulEquiv.trans x_1 x)) (domCongr R A (MulEquiv.trans x_1 x))
⊢ domCongr R A (x * x_1) = HMul.hMul (α := A[M] ≃ₐ[R] A[M]) (domCongr R A x) (domCongr R A x_1)

Tactic:
rw [MulAut.mul_def, AlgEquiv.aut_mul, trans_domCongr_domCongr]

Premises used: MulAut.mul_def, MonoidAlgebra.trans_domCongr_domCongr, AlgEquiv.aut_mul
-- Module: Mathlib.Algebra.MonoidAlgebra.Basic
Goal:
R : Type u_1
A : Type u_4
M : Type u_7
N : Type u_8
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Monoid M
inst_4 : Monoid N
⊢ Eq (α := A[N][M] ≃ₐ[R] A[M][N]) (AlgEquiv.symm (commAlgEquiv R)) (commAlgEquiv R)

Tactic:
rfl

Premises used: Multiset.sum, Multiset.foldr, MonoidAlgebra.commAlgEquiv, AlgEquiv.symm, Equiv.trans, Finsupp.mapDomain, Finsupp.sum, Finsupp.curry, AlgEquiv.trans, Prod.swap, Equiv.symm, Finset.sum, rfl
-- Module: Mathlib.Algebra.MonoidAlgebra.Basic
Goal:
R : Type u_1
A : Type u_4
M : Type u_7
N : Type u_8
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Monoid M
inst_4 : Monoid N
m : M
n : N
a : A
⊢ Eq (α := A[M][N]) ((commAlgEquiv R : (a : A[N][M]) → A[M][N]) (single m (single n a)) : A[M][N])
    (single n (single m a) : A[M][N])

Tactic:
commRingEquiv_single_single ..

Premises used: MonoidAlgebra.commRingEquiv_single_single
-- Module: Mathlib.Algebra.MonoidAlgebra.Basic
Goal:
R : Type u_1
A : Type u_4
M : Type u_7
N : Type u_8
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Monoid M
inst_4 : Monoid N
m : M
⊢ Eq (α := A[M][N]) ((commAlgEquiv R : (a : A[N][M]) → A[M][N]) (single m 1) : A[M][N])
    (single 1 (single m 1) : A[M][N])

Tactic:
commRingEquiv_single_one ..

Premises used: MonoidAlgebra.commRingEquiv_single_one
-- Module: Mathlib.Algebra.MonoidAlgebra.Basic
Goal:
R : Type u_1
A : Type u_4
M : Type u_7
N : Type u_8
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Monoid M
inst_4 : Monoid N
m : M
⊢ Eq (α := A[N][M]) ((commAlgEquiv R : (a : A[M][N]) → A[N][M]) (single 1 (single m 1)) : A[N][M])
    (single m 1 : A[N][M])

Tactic:
commRingEquiv_single_one_single ..

Premises used: MonoidAlgebra.commRingEquiv_single_one_single
-- Module: Mathlib.Algebra.MonoidAlgebra.Basic
Goal:
R : Type u_1
A : Type u_4
M : Type u_7
N : Type u_8
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Monoid M
inst_4 : Monoid N
f : M →* N
a :
  ∀ (x : R) (m : N),
    Eq.{u_4 + 1} (α := A)
      ((((RingHom.comp (mapDomainRingHom A f) (algebraMap R A[M]) : (a : R) → A[N]) x : A[N]) : (a : N) → A) m : A)
      (((((algebraMap R A[N] : R →+* A[N]) : (a : R) → A[N]) x : A[N]) : (a : N) → A) m : A)
⊢ Eq (α := R →+* A[N]) (RingHom.comp (mapDomainRingHom A f) (algebraMap R A[M])) (algebraMap R A[N])

Tactic:
ext
-- Module: Mathlib.Algebra.MonoidAlgebra.Basic
Goal:
R : Type u_1
A : Type u_4
M : Type u_7
N : Type u_8
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Monoid M
inst_4 : Monoid N
f : M →* N
x : R
m : N
⊢ Eq.{u_4 + 1} (α := A)
    ((((RingHom.comp (mapDomainRingHom A f) (algebraMap R A[M]) : (a : R) → A[N]) x : A[N]) : (a : N) → A) m : A)
    (((((algebraMap R A[N] : R →+* A[N]) : (a : R) → A[N]) x : A[N]) : (a : N) → A) m : A)

Tactic:
simp
-- Module: Mathlib.Algebra.MonoidAlgebra.Basic
Goal:
R : Type u_1
S : Type u_2
M : Type u_7
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Monoid M
f : R →+* S
a :
  ∀ (x : R) (m : M),
    Eq.{u_2 + 1} (α := S)
      ((((RingHom.comp (mapRingHom M f) (algebraMap R R[M]) : (a : R) → S[M]) x : S[M]) : (a : M) → S) m : S)
      (((((RingHom.comp (algebraMap S S[M]) f : R →+* S[M]) : (a : R) → S[M]) x : S[M]) : (a : M) → S) m : S)
⊢ Eq (α := R →+* S[M]) (RingHom.comp (mapRingHom M f) (algebraMap R R[M])) (RingHom.comp (algebraMap S S[M]) f)

Tactic:
ext
-- Module: Mathlib.Algebra.MonoidAlgebra.Basic
Goal:
R : Type u_1
S : Type u_2
M : Type u_7
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Monoid M
f : R →+* S
x : R
m : M
⊢ Eq.{u_2 + 1} (α := S)
    ((((RingHom.comp (mapRingHom M f) (algebraMap R R[M]) : (a : R) → S[M]) x : S[M]) : (a : M) → S) m : S)
    (((((RingHom.comp (algebraMap S S[M]) f : R →+* S[M]) : (a : R) → S[M]) x : S[M]) : (a : M) → S) m : S)

Tactic:
simp
-- Module: Mathlib.Algebra.MonoidAlgebra.Basic
Goal:
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_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Semiring B
inst_4 : Semiring C
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : Algebra R C
inst_8 : Monoid M
inst_9 : Monoid N
f : A →ₐ[R] B
⊢ ∀ (r : R),
    Eq (α := B[M])
      (OneHom.toFun (M := A[M]) (↑(↑(mapRingHom M (↑f : A →+* B)) : A[M] →* B[M]) : OneHom A[M] B[M])
        ((algebraMap R A[M] : (a : R) → A[M]) r))
      ((algebraMap R B[M] : (a : R) → B[M]) r)

Tactic:
simp
-- Module: Mathlib.Algebra.MonoidAlgebra.Basic
Goal:
R : Type u_1
A : Type u_4
B : Type u_5
M : Type u_7
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : Monoid M
f : A →ₐ[R] B
⊢ Eq (α := A[M] →+* B[M]) (↑(mapAlgHom M f) : A[M] →+* B[M]) (mapRingHom M f.toRingHom)

Tactic:
rfl

Premises used: MonoidAlgebra.ofCoeff, MonoidHomClass.toMonoidHom, Finsupp.onFinset, MonoidAlgebra.map, RingHomClass.toRingHom, MonoidAlgebra.mapRingHom, Finsupp.mapRange, rfl
-- Module: Mathlib.Algebra.MonoidAlgebra.Basic
Goal:
R : Type u_1
A : Type u_4
B : Type u_5
M : Type u_7
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : Monoid M
f : A →ₐ[R] B
x : A[M]
m : M
⊢ Eq.{u_5 + 1} (α := B) ((((mapAlgHom M f : (a : A[M]) → B[M]) x : B[M]) : (a : M) → B) m : B)
    ((f : (a : A) → B) ((x : (a : M) → A) m : A) : B)

Tactic:
mapRingHom_apply f.toRingHom x m

Premises used: MonoidAlgebra.mapRingHom_apply, AlgHom.toRingHom
-- Module: Mathlib.Algebra.MonoidAlgebra.Basic
Goal:
R : Type u_1
A : Type u_4
B : Type u_5
M : Type u_7
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : Monoid M
f : A →ₐ[R] B
m : M
a : A
hfg :
  ∀ (m_1 : M),
    Eq.{u_5 + 1} (α := B) ((((mapAlgHom M f : (a : A[M]) → B[M]) (single m a) : B[M]) : (a : M) → B) m_1 : B)
      (((single m ((f : (a : A) → B) a) : B[M]) : (a : M) → B) m_1 : B)
⊢ Eq (α := B[M]) ((mapAlgHom M f : (a : A[M]) → B[M]) (single m a) : B[M]) (single m ((f : (a : A) → B) a) : B[M])

Tactic:
ext
-- Module: Mathlib.Algebra.MonoidAlgebra.Basic
Goal:
R : Type u_1
A : Type u_4
B : Type u_5
M : Type u_7
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : Monoid M
f : A →ₐ[R] B
m : M
a : A
m_1 : M
⊢ Eq.{u_5 + 1} (α := B) ((((mapAlgHom M f : (a : A[M]) → B[M]) (single m a) : B[M]) : (a : M) → B) m_1 : B)
    (((single m ((f : (a : A) → B) a) : B[M]) : (a : M) → B) m_1 : B)

Tactic:
simp [single_apply, apply_ite f]

Premises used: apply_ite, MonoidAlgebra.single_apply, DFunLike.coe
-- Module: Mathlib.Algebra.MonoidAlgebra.Basic
Goal:
R : Type u_1
A : Type u_4
B : Type u_5
M : Type u_7
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : Monoid M
f : A →ₐ[R] B
m : M
a : A
hfg hfg₁ :
  ∀ (m_1 : M),
    Eq.{u_5 + 1} (α := B) ((((mapAlgHom M f : (a : A[M]) → B[M]) (single m a) : B[M]) : (a : M) → B) m_1 : B)
      (((single m ((f : (a : A) → B) a) : B[M]) : (a : M) → B) m_1 : B)
⊢ Eq (α := B[M]) ((mapAlgHom M f : (a : A[M]) → B[M]) (single m a) : B[M]) (single m ((f : (a : A) → B) a) : B[M])

Tactic:
classical ext; simp [single_apply, apply_ite f]

Premises used: apply_ite, MonoidAlgebra.single_apply, DFunLike.coe
-- Module: Mathlib.Algebra.MonoidAlgebra.Basic
Goal:
k : Type u_10
R : Type u_11
G : Type u_12
inst : CommSemiring k
inst_1 : Semiring R
inst_2 : Algebra k R
inst_3 : Monoid G
H :
  ∀ (x : R[G]) (m : G),
    Eq.{u_11 + 1} (α := R) ((((mapAlgHom G (AlgHom.id k R) : (a : R[G]) → R[G]) x : R[G]) : (a : G) → R) m : R)
      ((((AlgHom.id k R[G] : (a : R[G]) → R[G]) x : R[G]) : (a : G) → R) m : R)
⊢ Eq (α := R[G] →ₐ[k] R[G]) (mapAlgHom G (AlgHom.id k R)) (AlgHom.id k R[G])

Tactic:
ext
-- Module: Mathlib.Algebra.MonoidAlgebra.Basic
Goal:
k : Type u_10
R : Type u_11
G : Type u_12
inst : CommSemiring k
inst_1 : Semiring R
inst_2 : Algebra k R
inst_3 : Monoid G
x : R[G]
m : G
⊢ Eq.{u_11 + 1} (α := R) ((((mapAlgHom G (AlgHom.id k R) : (a : R[G]) → R[G]) x : R[G]) : (a : G) → R) m : R)
    ((((AlgHom.id k R[G] : (a : R[G]) → R[G]) x : R[G]) : (a : G) → R) m : R)

Tactic:
simp
-- Module: Mathlib.Algebra.MonoidAlgebra.Basic
Goal:
k : Type u_10
R : Type u_11
S : Type u_12
T : Type u_13
G : Type u_14
inst : CommSemiring k
inst_1 : Semiring R
inst_2 : Algebra k R
inst_3 : Semiring S
inst_4 : Algebra k S
inst_5 : Semiring T
inst_6 : Algebra k T
inst_7 : Monoid G
f : R →ₐ[k] S
g : S →ₐ[k] T
H :
  ∀ (x : R[G]) (m : G),
    Eq.{u_13 + 1} (α := T) ((((mapAlgHom G (g.comp f) : (a : R[G]) → T[G]) x : T[G]) : (a : G) → T) m : T)
      ((((AlgHom.comp (mapAlgHom G g) (mapAlgHom G f) : (a : R[G]) → T[G]) x : T[G]) : (a : G) → T) m : T)
⊢ Eq (α := R[G] →ₐ[k] T[G]) (mapAlgHom G (g.comp f)) (AlgHom.comp (mapAlgHom G g) (mapAlgHom G f))

Tactic:
ext
-- Module: Mathlib.Algebra.MonoidAlgebra.Basic
Goal:
k : Type u_10
R : Type u_11
S : Type u_12
T : Type u_13
G : Type u_14
inst : CommSemiring k
inst_1 : Semiring R
inst_2 : Algebra k R
inst_3 : Semiring S
inst_4 : Algebra k S
inst_5 : Semiring T
inst_6 : Algebra k T
inst_7 : Monoid G
f : R →ₐ[k] S
g : S →ₐ[k] T
x : R[G]
m : G
⊢ Eq.{u_13 + 1} (α := T) ((((mapAlgHom G (g.comp f) : (a : R[G]) → T[G]) x : T[G]) : (a : G) → T) m : T)
    ((((AlgHom.comp (mapAlgHom G g) (mapAlgHom G f) : (a : R[G]) → T[G]) x : T[G]) : (a : G) → T) m : T)

Tactic:
simp
-- Module: Mathlib.Algebra.MonoidAlgebra.Basic
Goal:
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_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Semiring B
inst_4 : Semiring C
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : Algebra R C
inst_8 : Monoid M
inst_9 : Monoid N
e : A ≃ₐ[R] B
x : A[M]
⊢ (mapAlgHom M (↑e.symm : B →ₐ[R] A) : (a : B[M]) → A[M])
      (OneHom.toFun (↑(↑(AlgHom.toRingHom (mapAlgHom M (↑e : A →ₐ[R] B))) : A[M] →* B[M]) : OneHom A[M] B[M]) x) =
    x

Tactic:
aesop
-- Module: Mathlib.Algebra.MonoidAlgebra.Basic
Goal:
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_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Semiring B
inst_4 : Semiring C
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : Algebra R C
inst_8 : Monoid M
inst_9 : Monoid N
e : A ≃ₐ[R] B
x : B[M]
⊢ OneHom.toFun (↑(↑(AlgHom.toRingHom (mapAlgHom M (↑e : A →ₐ[R] B))) : A[M] →* B[M]) : OneHom A[M] B[M])
      ((mapAlgHom M (↑e.symm : B →ₐ[R] A) : (a : B[M]) → A[M]) x) =
    x

Tactic:
aesop
-- Module: Mathlib.Algebra.MonoidAlgebra.Basic
Goal:
R : Type u_1
A : Type u_4
B : Type u_5
M : Type u_7
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : Monoid M
e : A ≃ₐ[R] B
⊢ Eq (α := B[M] ≃ₐ[R] A[M]) (AlgEquiv.symm (mapAlgEquiv R M e)) (mapAlgEquiv R M e.symm)

Tactic:
rfl

Premises used: MonoidAlgebra.ofCoeff, AlgEquiv.symm, Finsupp.onFinset, MonoidAlgebra.map, MonoidAlgebra.mapAlgEquiv, Equiv.symm, Finsupp.mapRange, rfl
-- Module: Mathlib.Algebra.MonoidAlgebra.Basic
Goal:
R : Type u_1
A : Type u_4
B : Type u_5
C : Type u_6
M : Type u_7
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Semiring C
inst_4 : Algebra R A
inst_5 : Algebra R B
inst_6 : Algebra R C
inst_7 : Monoid M
e₁ : A ≃ₐ[R] B
e₂ : B ≃ₐ[R] C
h :
  ∀ (a : A[M]) (m : M),
    Eq.{u_6 + 1} (α := C) ((((mapAlgEquiv R M (e₁.trans e₂) : (a : A[M]) → C[M]) a : C[M]) : (a : M) → C) m : C)
      ((((AlgEquiv.trans (mapAlgEquiv R M e₁) (mapAlgEquiv R M e₂) : (a : A[M]) → C[M]) a : C[M]) : (a : M) → C) m : C)
⊢ Eq (α := A[M] ≃ₐ[R] C[M]) (mapAlgEquiv R M (e₁.trans e₂)) (AlgEquiv.trans (mapAlgEquiv R M e₁) (mapAlgEquiv R M e₂))

Tactic:
ext
-- Module: Mathlib.Algebra.MonoidAlgebra.Basic
Goal:
R : Type u_1
A : Type u_4
B : Type u_5
C : Type u_6
M : Type u_7
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Semiring C
inst_4 : Algebra R A
inst_5 : Algebra R B
inst_6 : Algebra R C
inst_7 : Monoid M
e₁ : A ≃ₐ[R] B
e₂ : B ≃ₐ[R] C
a : A[M]
m : M
⊢ Eq.{u_6 + 1} (α := C) ((((mapAlgEquiv R M (e₁.trans e₂) : (a : A[M]) → C[M]) a : C[M]) : (a : M) → C) m : C)
    ((((AlgEquiv.trans (mapAlgEquiv R M e₁) (mapAlgEquiv R M e₂) : (a : A[M]) → C[M]) a : C[M]) : (a : M) → C) m : C)

Tactic:
simp
-- Module: Mathlib.Algebra.MonoidAlgebra.Basic
Goal:
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_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Semiring B
inst_4 : Semiring C
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : Algebra R C
inst_8 : Monoid M
inst_9 : Monoid N
h :
  ∀ (a : A[M]) (m : M),
    Eq.{u_4 + 1} (α := A) ((((mapAlgEquiv R M 1 : (a : A[M]) → A[M]) a : A[M]) : (a : M) → A) m : A)
      ((((1 : (a : A[M]) → A[M]) a : A[M]) : (a : M) → A) m : A)
⊢ Eq (α := A[M] ≃ₐ[R] A[M]) (mapAlgEquiv R M 1) 1

Tactic:
ext
-- Module: Mathlib.Algebra.MonoidAlgebra.Basic
Goal:
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_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Semiring B
inst_4 : Semiring C
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : Algebra R C
inst_8 : Monoid M
inst_9 : Monoid N
a : A[M]
m : M
⊢ Eq.{u_4 + 1} (α := A) ((((mapAlgEquiv R M 1 : (a : A[M]) → A[M]) a : A[M]) : (a : M) → A) m : A)
    ((((1 : (a : A[M]) → A[M]) a : A[M]) : (a : M) → A) m : A)

Tactic:
simp
-- Module: Mathlib.Algebra.MonoidAlgebra.Basic
Goal:
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_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Semiring B
inst_4 : Semiring C
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : Algebra R C
inst_8 : Monoid M
inst_9 : Monoid N
x y : A ≃ₐ[R] A
h :
  ∀ (a : A[M]) (m : M),
    Eq.{u_4 + 1} (α := A) ((((mapAlgEquiv R M (x * y) : (a : A[M]) → A[M]) a : A[M]) : (a : M) → A) m : A)
      ((((HMul.hMul (α := A[M] ≃ₐ[R] A[M]) (mapAlgEquiv R M x) (mapAlgEquiv R M y) : (a : A[M]) → A[M]) a : A[M]) :
            (a : M) → A)
          m :
        A)
⊢ mapAlgEquiv R M (x * y) = HMul.hMul (α := A[M] ≃ₐ[R] A[M]) (mapAlgEquiv R M x) (mapAlgEquiv R M y)

Tactic:
ext
-- Module: Mathlib.Algebra.MonoidAlgebra.Basic
Goal:
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_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Semiring B
inst_4 : Semiring C
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : Algebra R C
inst_8 : Monoid M
inst_9 : Monoid N
x y : A ≃ₐ[R] A
a : A[M]
m : M
⊢ Eq.{u_4 + 1} (α := A) ((((mapAlgEquiv R M (x * y) : (a : A[M]) → A[M]) a : A[M]) : (a : M) → A) m : A)
    ((((HMul.hMul (α := A[M] ≃ₐ[R] A[M]) (mapAlgEquiv R M x) (mapAlgEquiv R M y) : (a : A[M]) → A[M]) a : A[M]) :
          (a : M) → A)
        m :
      A)

Tactic:
simp
-- Module: Mathlib.Algebra.MonoidAlgebra.Basic
Goal:
R : Type u_1
M : Type u_7
inst : Monoid M
inst_1 : CommSemiring R
V : Type u_10
inst_2 : AddCommMonoid V
inst_3 : Module R V
inst_4 : Module R[M] V
inst_5 : IsScalarTower R R[M] V
g : M
v : V
⊢ (linearMap R V g : (a : V) → V) v = HSMul.hSMul (α := R[M]) (single g 1) v

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.MonoidAlgebra.Basic
Goal:
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_1 : CommSemiring R
V : Type u_10
W : Type u_11
inst_2 : AddCommMonoid V
inst_3 : Module R V
inst_4 : Module R[M] V
inst_5 : IsScalarTower R R[M] V
inst_6 : AddCommMonoid W
inst_7 : Module R W
inst_8 : Module R[M] W
inst_9 : IsScalarTower R R[M] W
f : V →ₗ[R] W
h :
  ∀ (g : M) (v : V),
    (f : (a : V) → W) (HSMul.hSMul (α := R[M]) (single g 1) v) =
      HSMul.hSMul (α := R[M]) (β := W) (single g 1) ((f : (a : V) → W) v : W)
v v' : V
⊢ (f : (a : V) → W) (v + v') = HAdd.hAdd (α := W) (β := W) ((f : (a : V) → W) v : W) ((f : (a : V) → W) v' : W)

Tactic:
simp
-- Module: Mathlib.Algebra.MonoidAlgebra.Basic
Goal:
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_1 : CommSemiring R
V : Type u_10
W : Type u_11
inst_2 : AddCommMonoid V
inst_3 : Module R V
inst_4 : Module R[M] V
inst_5 : IsScalarTower R R[M] V
inst_6 : AddCommMonoid W
inst_7 : Module R W
inst_8 : Module R[M] W
inst_9 : IsScalarTower R R[M] W
f : V →ₗ[R] W
h :
  ∀ (g : M) (v : V),
    (f : (a : V) → W) (HSMul.hSMul (α := R[M]) (single g 1) v) =
      HSMul.hSMul (α := R[M]) (β := W) (single g 1) ((f : (a : V) → W) v : W)
c : R[M]
v : V
⊢ (f : (a : V) → W) (c • v) =
    HSMul.hSMul (α := R[M]) (β := W) ((RingHom.id R[M] : (a : R[M]) → R[M]) c : R[M]) ((f : (a : V) → W) v : W)

Tactic:
Finsupp.induction c ?_ ?_

Premises used: Finsupp.induction
-- Module: Mathlib.Algebra.MonoidAlgebra.Basic
Goal:
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_1 : CommSemiring R
V : Type u_10
W : Type u_11
inst_2 : AddCommMonoid V
inst_3 : Module R V
inst_4 : Module R[M] V
inst_5 : IsScalarTower R R[M] V
inst_6 : AddCommMonoid W
inst_7 : Module R W
inst_8 : Module R[M] W
inst_9 : IsScalarTower R R[M] W
f : V →ₗ[R] W
h :
  ∀ (g : M) (v : V),
    (f : (a : V) → W) (HSMul.hSMul (α := R[M]) (single g 1) v) =
      HSMul.hSMul (α := R[M]) (β := W) (single g 1) ((f : (a : V) → W) v : W)
c : R[M]
v : V
refine_1 :
  (f : (a : V) → W) (HSMul.hSMul (α := R[M]) 0 v) =
    HSMul.hSMul (α := R[M]) (β := W) ((RingHom.id R[M] : (a : R[M]) → R[M]) 0) ((f : (a : V) → W) v : W)
refine_2 :
  ∀ (a : M) (b : R) (f_1 : M →₀ R),
    a ∉ f_1.support →
      b ≠ 0 →
        (f : (a : V) → W) (f_1 • v) =
            HSMul.hSMul (α := R[M]) (β := W) ((RingHom.id R[M] : (a : R[M]) → R[M]) f_1 : R[M])
              ((f : (a : V) → W) v : W) →
          (f : (a : V) → W) ((Finsupp.single a b + f_1) • v) =
            HSMul.hSMul (α := R[M]) (β := W) ((RingHom.id R[M] : (a : R[M]) → R[M]) (Finsupp.single a b + f_1) : R[M])
              ((f : (a : V) → W) v : W)
⊢ (f : (a : V) → W) (c • v) =
    HSMul.hSMul (α := R[M]) (β := W) ((RingHom.id R[M] : (a : R[M]) → R[M]) c : R[M]) ((f : (a : V) → W) v : W)

Tactic:
refine Finsupp.induction c ?_ ?_