awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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) (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)

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
g : M
r : R
c' : M →₀ R
_nm : g ∉ c'.support
_nz : r ≠ 0
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)
refine_2 :
  (f : (a : V) → W) ((Finsupp.single g r + c') • v) =
    HSMul.hSMul (β := W) (Finsupp.single g r + c') ((f : (a : V) → W) v : W)
⊢ (f : (a : V) → W) ((Finsupp.single g r + c') • v) =
    HSMul.hSMul (α := R[M]) (β := W) ((RingHom.id R[M] : (a : R[M]) → R[M]) (Finsupp.single g r + c') : R[M])
      ((f : (a : V) → W) v : W)

Tactic:
dsimp at *
-- 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
g : M
r : R
c' : M →₀ R
_nm : g ∉ c'.support
_nz : ¬r = 0
w : (f : (a : V) → W) (c' • v) = HSMul.hSMul (β := W) c' ((f : (a : V) → W) v : W)
refine_2 :
  HAdd.hAdd (α := W)
      ((f : (a : V) → W)
          (HSMul.hSMul (α := R[M]) ((algebraMap R R[M] : (a : R) → R[M]) r : R[M])
            (HSMul.hSMul (α := R[M]) ((of R M : (a : M) → R[M]) g : R[M]) v)) :
        W)
      (HSMul.hSMul (β := W) c' ((f : (a : V) → W) v : W)) =
    HSMul.hSMul (α := R[M]) ((algebraMap R R[M] : (a : R) → R[M]) r : R[M])
        (HSMul.hSMul (α := R[M]) (β := W) ((of R M : (a : M) → R[M]) g : R[M]) ((f : (a : V) → W) v : W)) +
      HSMul.hSMul (β := W) c' ((f : (a : V) → W) v : W)
⊢ (f : (a : V) → W) ((Finsupp.single g r + c') • v) =
    HSMul.hSMul (β := W) (Finsupp.single g r + c') ((f : (a : V) → W) v : W)

Tactic:
simp only [add_smul, f.map_add, w, single_eq_algebraMap_mul_of, ← smul_smul]

Premises used: LinearMap.map_add, smul_smul, add_smul, MonoidAlgebra.single_eq_algebraMap_mul_of
-- 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
g : M
r : R
c' : M →₀ R
_nm : g ∉ c'.support
_nz : ¬r = 0
w : (f : (a : V) → W) (c' • v) = HSMul.hSMul (β := W) c' ((f : (a : V) → W) v : W)
refine_2 :
  HAdd.hAdd (α := W) ((f : (a : V) → W) (r • HSMul.hSMul (α := R[M]) ((of R M : (a : M) → R[M]) g : R[M]) v) : W)
      (HSMul.hSMul (β := W) c' ((f : (a : V) → W) v : W)) =
    HSMul.hSMul (α := R[M]) ((algebraMap R R[M] : (a : R) → R[M]) r : R[M])
        (HSMul.hSMul (α := R[M]) (β := W) ((of R M : (a : M) → R[M]) g : R[M]) ((f : (a : V) → W) v : W)) +
      HSMul.hSMul (β := W) c' ((f : (a : V) → W) v : W)
refine_2₁ :
  HAdd.hAdd (α := W) ((f : (a : V) → W) (r • HSMul.hSMul (α := R[M]) ((of R M : (a : M) → R[M]) g : R[M]) v) : W)
      (HSMul.hSMul (β := W) c' ((f : (a : V) → W) v : W)) =
    r • HSMul.hSMul (α := R[M]) (β := W) ((of R M : (a : M) → R[M]) g : R[M]) ((f : (a : V) → W) v : W) +
      HSMul.hSMul (β := W) c' ((f : (a : V) → W) v : W)
refine_2₂ :
  HSMul.hSMul (β := W) r ((f : (a : V) → W) (HSMul.hSMul (α := R[M]) ((of R M : (a : M) → R[M]) g : R[M]) v) : W) +
      HSMul.hSMul (β := W) c' ((f : (a : V) → W) v : W) =
    r • HSMul.hSMul (α := R[M]) (β := W) ((of R M : (a : M) → R[M]) g : R[M]) ((f : (a : V) → W) v : W) +
      HSMul.hSMul (β := W) c' ((f : (a : V) → W) v : W)
refine_2₃ :
  HSMul.hSMul (β := W) r ((f : (a : V) → W) (HSMul.hSMul (α := R[M]) (single g 1) v) : W) +
      HSMul.hSMul (β := W) c' ((f : (a : V) → W) v : W) =
    r • HSMul.hSMul (α := R[M]) (β := W) (single g 1) ((f : (a : V) → W) v : W) +
      HSMul.hSMul (β := W) c' ((f : (a : V) → W) v : W)
refine_2₄ refine_2₅ :
  r • HSMul.hSMul (α := R[M]) (β := W) (single g 1) ((f : (a : V) → W) v : W) +
      HSMul.hSMul (β := W) c' ((f : (a : V) → W) v : W) =
    r • HSMul.hSMul (α := R[M]) (β := W) (single g 1) ((f : (a : V) → W) v : W) +
      HSMul.hSMul (β := W) c' ((f : (a : V) → W) v : W)
⊢ HAdd.hAdd (α := W)
      ((f : (a : V) → W)
          (HSMul.hSMul (α := R[M]) ((algebraMap R R[M] : (a : R) → R[M]) r : R[M])
            (HSMul.hSMul (α := R[M]) ((of R M : (a : M) → R[M]) g : R[M]) v)) :
        W)
      (HSMul.hSMul (β := W) c' ((f : (a : V) → W) v : W)) =
    HSMul.hSMul (α := R[M]) ((algebraMap R R[M] : (a : R) → R[M]) r : R[M])
        (HSMul.hSMul (α := R[M]) (β := W) ((of R M : (a : M) → R[M]) g : R[M]) ((f : (a : V) → W) v : W)) +
      HSMul.hSMul (β := W) c' ((f : (a : V) → W) v : W)

Tactic:
rw [algebraMap_smul, algebraMap_smul, f.map_smul, of_apply, h g v]

Premises used: algebraMap_smul, LinearMap.map_smul, MonoidAlgebra.of_apply
-- 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
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
⊢ Eq.{u_11 + 1} (α := W) ((equivariantOfLinearOfComm f h : (a : V) → W) v : W) ((f : (a : V) → W) v : W)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.MonoidAlgebra.Basic
Goal:
R : Type u_1
S : Type u_2
M : Type u_7
inst : CommMonoid M
inst_1 : CommSemiring R
inst_2 : CommSemiring S
inst_3 : Algebra R S
⊢ Eq (α := R[M] →+* S[M]) (algebraMap R[M] S[M]) (mapRingHom M (algebraMap R S))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.MonoidAlgebra.Basic
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
M : Type u_7
inst : CommMonoid M
inst_1 : CommSemiring R
inst_2 : CommSemiring S
inst_3 : Algebra R S
inst_4 : CommSemiring T
inst_5 : Algebra R T
inst_6 : Algebra S T
inst_7 : IsScalarTower R S T
⊢ IsScalarTower R S[M] T[M]

Tactic:
.of_algebraMap_eq' (mapAlgHom _ (IsScalarTower.toAlgHom R S T)).comp_algebraMap.symm

Premises used: AlgHom.comp_algebraMap, IsScalarTower.toAlgHom, MonoidAlgebra.mapAlgHom, IsScalarTower.of_algebraMap_eq', Eq.symm
-- Module: Mathlib.Algebra.MonoidAlgebra.Basic
Goal:
R : Type u_1
A : Type u_4
M : Type u_7
inst : Semiring R
inst_1 : Add M
inst_2 : NonUnitalNonAssocSemiring A
inst_3 : DistribMulAction R A
φ₁ φ₂ : R[M] →ₙₐ[R] A
h : φ₁.toMulHom.comp (ofMagma R M) = φ₂.toMulHom.comp (ofMagma R M)
⊢ φ₁ = φ₂

Tactic:
nonUnitalAlgHom_ext R <| DFunLike.congr_fun h

Premises used: DFunLike.congr_fun, AddMonoidAlgebra.nonUnitalAlgHom_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 : AddMonoid M
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : Semiring B
inst_5 : Algebra R B
f : A →ₐ[R] B
g : MonoidHom.{u_7, u_5} (Multiplicative M) B
h_comm :
  ∀ (x : A) (y : Multiplicative M),
    Commute.{u_5} (S := B) ((f : (a : A) → B) x : B) ((g : (a : Multiplicative M) → B) y : B)
⊢ ∀ (r : R),
    (↑(↑(liftNCRingHom (↑f : A →+* B) g h_comm) : A[M] →* B) : OneHom A[M] B).toFun
        ((algebraMap R A[M] : (a : R) → A[M]) r) =
      (algebraMap R B : (a : R) → B) r

Tactic:
simp [liftNCRingHom]

Premises used: AddMonoidAlgebra.liftNCRingHom
-- 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 : AddMonoid M
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : Semiring B
inst_5 : Algebra R B
f : A →ₐ[R] B
g : MonoidHom.{u_7, u_5} (Multiplicative M) B
h_comm :
  ∀ (x : A) (y : Multiplicative M),
    Commute.{u_5} (S := B) ((f : (a : A) → B) x : B) ((g : (a : Multiplicative M) → B) y : B)
⊢ Eq (α := (a : A[M]) → B) (⇑(liftNCAlgHom f g h_comm) : (a : A[M]) → B)
    (⇑(liftNC (↑f : A →+ B) (⇑g : (a : Multiplicative M) → B)) : (a : A[M]) → B)

Tactic:
rfl

Premises used: Multiset.sum, Multiset.foldr, Finsupp.sum, AddMonoidAlgebra, Finset.sum, rfl
-- Module: Mathlib.Algebra.MonoidAlgebra.Basic
Goal:
R : Type u_1
A : Type u_4
M : Type u_7
inst : CommSemiring R
inst_1 : AddMonoid M
inst_2 : Semiring A
inst_3 : Algebra R A
φ₁ φ₂ : R[M] →ₐ[R] A
h :
  Eq (α := MonoidHom.{u_7, u_4} (Multiplicative M) A) (MonoidHom.comp (↑φ₁ : R[M] →* A) (of R M))
    (MonoidHom.comp (↑φ₂ : R[M] →* A) (of R M))
⊢ φ₁ = φ₂

Tactic:
algHom_ext <| DFunLike.congr_fun h

Premises used: DFunLike.congr_fun, AddMonoidAlgebra.algHom_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 : AddMonoid M
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : Semiring B
inst_5 : Algebra R B
f : MonoidHom.{u_7, u_4} (Multiplicative M) A
h :
  ∀ (x : M),
    Eq.{u_4 + 1} (α := A)
      ((Additive.toMul : (a : Additive A) → A)
          (((MonoidHom.toAdditiveRight : (a : Multiplicative M →* A) → M →+ Additive A)
                  ((fun (f : R[M] →ₐ[R] A) ↦
                      (MonoidHom.comp (↑f : R[M] →* A) (of R M) : MonoidHom.{u_7, u_4} (Multiplicative M) A))
                    ((fun (F : MonoidHom.{u_7, u_4} (Multiplicative M) A) ↦
                        (liftNCAlgHom (Algebra.ofId R A) F ⋯ : R[M] →ₐ[R] A))
                      f)) :
                (a : M) → Additive A)
              x :
            Additive A) :
        A)
      ((Additive.toMul : (a : Additive A) → A)
          ((((MonoidHom.toAdditiveRight : (a : Multiplicative M →* A) → M →+ Additive A) f :
                  AddMonoidHom.{u_7, u_4} M (Additive A)) :
                (a : M) → Additive A)
              x :
            Additive A) :
        A)
⊢ (fun (f : R[M] →ₐ[R] A) ↦ (MonoidHom.comp (↑f : R[M] →* A) (of R M) : MonoidHom.{u_7, u_4} (Multiplicative M) A))
      ((fun (F : MonoidHom.{u_7, u_4} (Multiplicative M) A) ↦ (liftNCAlgHom (Algebra.ofId R A) F ⋯ : R[M] →ₐ[R] A)) f) =
    f

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 : AddMonoid M
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : Semiring B
inst_5 : Algebra R B
f : MonoidHom.{u_7, u_4} (Multiplicative M) A
x : M
⊢ Eq.{u_4 + 1} (α := A)
    ((Additive.toMul : (a : Additive A) → A)
        (((MonoidHom.toAdditiveRight : (a : Multiplicative M →* A) → M →+ Additive A)
                ((fun (f : R[M] →ₐ[R] A) ↦
                    (MonoidHom.comp (↑f : R[M] →* A) (of R M) : MonoidHom.{u_7, u_4} (Multiplicative M) A))
                  ((fun (F : MonoidHom.{u_7, u_4} (Multiplicative M) A) ↦
                      (liftNCAlgHom (Algebra.ofId R A) F ⋯ : R[M] →ₐ[R] A))
                    f)) :
              (a : M) → Additive A)
            x :
          Additive A) :
      A)
    ((Additive.toMul : (a : Additive A) → A)
        ((((MonoidHom.toAdditiveRight : (a : Multiplicative M →* A) → M →+ Additive A) f :
                AddMonoidHom.{u_7, u_4} M (Additive A)) :
              (a : M) → Additive A)
            x :
          Additive A) :
      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 : AddMonoid M
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : Semiring B
inst_5 : Algebra R B
F : R[M] →ₐ[R] A
h :
  ∀ (x : M),
    Eq.{u_4 + 1} (α := A)
      ((Additive.toMul : (a : Additive A) → A)
          ((((MonoidHom.toAdditiveRight : (a : Multiplicative M →* A) → M →+ Additive A)
                    (MonoidHom.comp
                      (↑((fun (F : MonoidHom.{u_7, u_4} (Multiplicative M) A) ↦
                              (liftNCAlgHom (Algebra.ofId R A) F ⋯ : R[M] →ₐ[R] A))
                            ((fun (f : R[M] →ₐ[R] A) ↦
                                (MonoidHom.comp (↑f : R[M] →* A) (of R M) : MonoidHom.{u_7, u_4} (Multiplicative M) A))
                              F)) :
                        R[M] →* A)
                      (of R M)) :
                  AddMonoidHom.{u_7, u_4} M (Additive A)) :
                (a : M) → Additive A)
              x :
            Additive A) :
        A)
      ((Additive.toMul : (a : Additive A) → A)
          ((((MonoidHom.toAdditiveRight : (a : Multiplicative M →* A) → M →+ Additive A)
                    (MonoidHom.comp (↑F : R[M] →* A) (of R M)) :
                  AddMonoidHom.{u_7, u_4} M (Additive A)) :
                (a : M) → Additive A)
              x :
            Additive A) :
        A)
⊢ (fun (F : MonoidHom.{u_7, u_4} (Multiplicative M) A) ↦ (liftNCAlgHom (Algebra.ofId R A) F ⋯ : R[M] →ₐ[R] A))
      ((fun (f : R[M] →ₐ[R] A) ↦ (MonoidHom.comp (↑f : R[M] →* A) (of R M) : MonoidHom.{u_7, u_4} (Multiplicative M) A))
        F) =
    F

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 : AddMonoid M
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : Semiring B
inst_5 : Algebra R B
F : R[M] →ₐ[R] A
x : M
⊢ Eq.{u_4 + 1} (α := A)
    ((Additive.toMul : (a : Additive A) → A)
        ((((MonoidHom.toAdditiveRight : (a : Multiplicative M →* A) → M →+ Additive A)
                  (MonoidHom.comp
                    (↑((fun (F : MonoidHom.{u_7, u_4} (Multiplicative M) A) ↦
                            (liftNCAlgHom (Algebra.ofId R A) F ⋯ : R[M] →ₐ[R] A))
                          ((fun (f : R[M] →ₐ[R] A) ↦
                              (MonoidHom.comp (↑f : R[M] →* A) (of R M) : MonoidHom.{u_7, u_4} (Multiplicative M) A))
                            F)) :
                      R[M] →* A)
                    (of R M)) :
                AddMonoidHom.{u_7, u_4} M (Additive A)) :
              (a : M) → Additive A)
            x :
          Additive A) :
      A)
    ((Additive.toMul : (a : Additive A) → A)
        ((((MonoidHom.toAdditiveRight : (a : Multiplicative M →* A) → M →+ Additive A)
                  (MonoidHom.comp (↑F : R[M] →* A) (of R M)) :
                AddMonoidHom.{u_7, u_4} M (Additive A)) :
              (a : M) → Additive A)
            x :
          Additive A) :
      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 : AddMonoid M
inst_2 : Semiring A
inst_3 : Algebra R A
F : MonoidHom.{u_7, u_4} (Multiplicative M) A
f : R[M]
⊢ Eq.{u_4 + 1} (α := A)
    ((((lift R A M : (a : Multiplicative M →* A) → R[M] →ₐ[R] A) F : R[M] →ₐ[R] A) : (a : R[M]) → A) f : A)
    (sum f fun (a : M) (b : R) ↦
        HMul.hMul (α := A) (β := A) ((algebraMap R A : (a : R) → A) b : A)
          ((F : (a : Multiplicative M) → A) ((Multiplicative.ofAdd : (a : M) → Multiplicative M) a : Multiplicative M) :
            A) :
      A)

Tactic:
rfl

Premises used: Multiset.sum, Multiset.foldr, Finsupp.sum, Finset.sum, rfl
-- Module: Mathlib.Algebra.MonoidAlgebra.Basic
Goal:
R : Type u_1
A : Type u_4
M : Type u_7
inst : CommSemiring R
inst_1 : AddMonoid M
inst_2 : Semiring A
inst_3 : Algebra R A
F : MonoidHom.{u_7, u_4} (Multiplicative M) A
f : R[M]
⊢ Eq.{u_4 + 1} (α := A)
    ((((lift R A M : (a : Multiplicative M →* A) → R[M] →ₐ[R] A) F : R[M] →ₐ[R] A) : (a : R[M]) → A) f : A)
    (sum f fun (a : M) (b : R) ↦
        HSMul.hSMul (β := A) b
          ((F : (a : Multiplicative M) → A) ((Multiplicative.ofAdd : (a : M) → Multiplicative M) a : Multiplicative M) :
            A) :
      A)

Tactic:
simp only [lift_apply', Algebra.smul_def]

Premises used: AddMonoidAlgebra.lift_apply', Algebra.smul_def
-- Module: Mathlib.Algebra.MonoidAlgebra.Basic
Goal:
R : Type u_1
A : Type u_4
M : Type u_7
inst : CommSemiring R
inst_1 : AddMonoid M
inst_2 : Semiring A
inst_3 : Algebra R A
F : MonoidHom.{u_7, u_4} (Multiplicative M) A
⊢ Eq (α := (a : R[M]) → A)
    (⇑((lift R A M : (a : Multiplicative M →* A) → R[M] →ₐ[R] A) F : R[M] →ₐ[R] A) : (a : R[M]) → A)
    (⇑(liftNC (↑(algebraMap R A) : R →+ A) (⇑F : (a : Multiplicative M) → A)) : (a : R[M]) → A)

Tactic:
rfl

Premises used: Multiset.sum, Multiset.foldr, Finsupp.sum, AddMonoidAlgebra, Finset.sum, rfl
-- Module: Mathlib.Algebra.MonoidAlgebra.Basic
Goal:
R : Type u_1
A : Type u_4
M : Type u_7
inst : CommSemiring R
inst_1 : AddMonoid M
inst_2 : Semiring A
inst_3 : Algebra R A
F : R[M] →ₐ[R] A
x : Multiplicative M
⊢ Eq.{u_4 + 1} (α := A)
    ((((Equiv.symm (lift R A M) : (a : R[M] →ₐ[R] A) → Multiplicative M →* A) F :
            MonoidHom.{u_7, u_4} (Multiplicative M) A) :
          (a : Multiplicative M) → A)
        x :
      A)
    ((F : (a : R[M]) → A) (single ((Multiplicative.toAdd : (a : Multiplicative M) → M) x) 1 : R[M]) : A)

Tactic:
rfl

Premises used: rfl, Finsupp.single
-- Module: Mathlib.Algebra.MonoidAlgebra.Basic
Goal:
R : Type u_1
A : Type u_4
M : Type u_7
inst : CommSemiring R
inst_1 : AddMonoid M
inst_2 : Semiring A
inst_3 : Algebra R A
F : MonoidHom.{u_7, u_4} (Multiplicative M) A
x : Multiplicative M
⊢ Eq.{u_4 + 1} (α := A)
    ((((lift R A M : (a : Multiplicative M →* A) → R[M] →ₐ[R] A) F : R[M] →ₐ[R] A) : (a : R[M]) → A)
        ((of R M : (a : Multiplicative M) → R[M]) x : R[M]) :
      A)
    ((F : (a : Multiplicative M) → A) x : A)

Tactic:
MonoidAlgebra.lift_of F x

Premises used: Multiplicative, MonoidAlgebra.lift_of, Finsupp.single
-- Module: Mathlib.Algebra.MonoidAlgebra.Basic
Goal:
R : Type u_1
A : Type u_4
M : Type u_7
inst : CommSemiring R
inst_1 : AddMonoid M
inst_2 : Semiring A
inst_3 : Algebra R A
F : MonoidHom.{u_7, u_4} (Multiplicative M) A
a : M
b : R
⊢ (((lift R A M : (a : Multiplicative M →* A) → R[M] →ₐ[R] A) F : R[M] →ₐ[R] A) : (a : R[M]) → A) (single a b) =
    HSMul.hSMul (β := A) b
      ((F : (a : Multiplicative M) → A) ((Multiplicative.ofAdd : (a : M) → Multiplicative M) a : Multiplicative M) : A)

Tactic:
MonoidAlgebra.lift_single F (.ofAdd a) b

Premises used: Multiplicative, Multiplicative.ofAdd, DFunLike.coe, MonoidAlgebra.lift_single
-- Module: Mathlib.Algebra.MonoidAlgebra.Basic
Goal:
R : Type u_1
A : Type u_4
M : Type u_7
inst : CommSemiring R
inst_1 : AddMonoid M
inst_2 : Semiring A
inst_3 : Algebra R A
F : MonoidHom.{u_7, u_4} (Multiplicative M) A
x : M
⊢ Eq.{u_4 + 1} (α := A)
    ((((lift R A M : (a : Multiplicative M →* A) → R[M] →ₐ[R] A) F : R[M] →ₐ[R] A) : (a : R[M]) → A) (of' R M x) : A)
    ((F : (a : Multiplicative M) → A) ((Multiplicative.ofAdd : (a : M) → Multiplicative M) x : Multiplicative M) : A)

Tactic:
lift_of F x

Premises used: AddMonoidAlgebra.lift_of, AddMonoidAlgebra.of', Finsupp.single
-- Module: Mathlib.Algebra.MonoidAlgebra.Basic
Goal:
R : Type u_1
A : Type u_4
M : Type u_7
inst : CommSemiring R
inst_1 : AddMonoid M
inst_2 : Semiring A
inst_3 : Algebra R A
F : R[M] →ₐ[R] A
⊢ F = (lift R A M : (a : Multiplicative M →* A) → R[M] →ₐ[R] A) (MonoidHom.comp (↑F : R[M] →* A) (of R M))

Tactic:
((lift R A M).apply_symm_apply F).symm

Premises used: Equiv.apply_symm_apply, AddMonoidAlgebra.lift, Eq.symm
-- Module: Mathlib.Algebra.MonoidAlgebra.Basic
Goal:
R : Type u_1
A : Type u_4
M : Type u_7
inst : CommSemiring R
inst_1 : AddMonoid M
inst_2 : Semiring A
inst_3 : Algebra R A
F : R[M] →ₐ[R] A
f : R[M]
rw :
  ((((lift R A M : (a : Multiplicative M →* A) → R[M] →ₐ[R] A) (MonoidHom.comp (↑F : R[M] →* A) (of R M)) :
          R[M] →ₐ[R] A) :
        (a : R[M]) → A)
      f :
    A)
| ((F : (a : R[M]) → A) f : A)

Tactic:
rw [lift_unique' F]

Premises used: AddMonoidAlgebra.lift_unique'
-- Module: Mathlib.Algebra.MonoidAlgebra.Basic
Goal:
R : Type u_1
A : Type u_4
M : Type u_7
inst : CommSemiring R
inst_1 : AddMonoid M
inst_2 : Semiring A
inst_3 : Algebra R A
F : R[M] →ₐ[R] A
f : R[M]
simp : sum f fun (a : M) (b : R) ↦ HSMul.hSMul (β := A) b ((F : (a : R[M]) → A) (single a 1) : A)
| ((((lift R A M : (a : Multiplicative M →* A) → R[M] →ₐ[R] A) (MonoidHom.comp (↑F : R[M] →* A) (of R M)) :
          R[M] →ₐ[R] A) :
        (a : R[M]) → A)
      f :
    A)

Tactic:
simp [lift_apply]

Premises used: AddMonoidAlgebra.lift_apply
-- Module: Mathlib.Algebra.MonoidAlgebra.Basic
Goal:
R : Type u_1
A : Type u_4
M : Type u_7
inst : CommSemiring R
inst_1 : AddMonoid M
inst_2 : Semiring A
inst_3 : Algebra R A
F : R[M] →ₐ[R] A
f : R[M]
rw : sum f fun (a : M) (b : R) ↦ HSMul.hSMul (β := A) b ((F : (a : R[M]) → A) (single a 1) : A)
| ((F : (a : R[M]) → A) f : A)

Tactic:
rw [lift_unique' F]
    simp [lift_apply]

Premises used: AddMonoidAlgebra.lift_apply, AddMonoidAlgebra.lift_unique'
-- Module: Mathlib.Algebra.MonoidAlgebra.Basic
Goal:
R : Type u_1
A : Type u_4
M : Type u_7
inst : CommSemiring R
inst_1 : AddMonoid M
inst_2 : Semiring A
inst_3 : Algebra R A
F : R[M] →ₐ[R] A
f : R[M]
conv_lhs :
  Eq.{u_4 + 1} (α := A) ((F : (a : R[M]) → A) f : A)
    (sum f fun (a : M) (b : R) ↦ HSMul.hSMul (β := A) b ((F : (a : R[M]) → A) (single a 1) : A) : A)
conv_lhs₁ :
  Eq.{u_4 + 1} (α := A) (sum f fun (a : M) (b : R) ↦ HSMul.hSMul (β := A) b ((F : (a : R[M]) → A) (single a 1) : A))
    (sum f fun (a : M) (b : R) ↦ HSMul.hSMul (β := A) b ((F : (a : R[M]) → A) (single a 1) : A))
⊢ Eq.{u_4 + 1} (α := A) ((F : (a : R[M]) → A) f : A)
    (sum f fun (a : M) (b : R) ↦ HSMul.hSMul (β := A) b ((F : (a : R[M]) → A) (single a 1) : A) : A)

Tactic:
conv_lhs =>
    rw [lift_unique' F]
    simp [lift_apply]

Premises used: AddMonoidAlgebra.lift_apply, AddMonoidAlgebra.lift_unique'
-- Module: Mathlib.Algebra.MonoidAlgebra.Basic
Goal:
R : Type u_1
S : Type u_2
A : Type u_4
M : Type u_7
inst : CommSemiring R
inst_1 : AddMonoid M
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : CommSemiring S
inst_5 : Algebra S A
inst_6 : Algebra R S
inst_7 : IsScalarTower R S A
f : MonoidHom.{u_7, u_4} (Multiplicative M) A
⊢ Eq.{u_4 + 1} (α := A)
    ((((lift S A M : (a : Multiplicative M →* A) → S[M] →ₐ[S] A) f : S[M] →ₐ[S] A) : (a : S[M]) → A)
        ((mapRingHom M (algebraMap R S) : (a : R[M]) → S[M]) 0) :
      A)
    ((((lift R A M : (a : Multiplicative M →* A) → R[M] →ₐ[R] A) f : R[M] →ₐ[R] A) : (a : R[M]) → A) 0 : A)

Tactic:
simp