awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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_1 : MonoidHom.{u_7, u_4} (Multiplicative M) A
a : M
b : R
f : M →₀ R
h : a ∉ f.support
h_1 : b ≠ 0
ih :
  Eq.{u_4 + 1} (α := A)
    ((((lift S A M : (a : Multiplicative M →* A) → S[M] →ₐ[S] A) f_1 : S[M] →ₐ[S] A) : (a : S[M]) → A)
        ((mapRingHom M (algebraMap R S) : (a : R[M]) → S[M]) f : S[M]) :
      A)
    ((((lift R A M : (a : Multiplicative M →* A) → R[M] →ₐ[R] A) f_1 : R[M] →ₐ[R] A) : (a : R[M]) → A) f : A)
⊢ Eq.{u_4 + 1} (α := A)
    ((((lift S A M : (a : Multiplicative M →* A) → S[M] →ₐ[S] A) f_1 : S[M] →ₐ[S] A) : (a : S[M]) → A)
        ((mapRingHom M (algebraMap R S) : (a : R[M]) → S[M]) (Finsupp.single a b + f) : S[M]) :
      A)
    ((((lift R A M : (a : Multiplicative M →* A) → R[M] →ₐ[R] A) f_1 : R[M] →ₐ[R] A) : (a : R[M]) → A)
        (Finsupp.single a b + f) :
      A)

Tactic:
simp [ih]
-- 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
x : R[M]
zero :
  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)
single_add :
  ∀ (a : M) (b : R) (f_1 : M →₀ R),
    a ∉ f_1.support →
      b ≠ 0 →
        ∀
          (ih :
            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]) f_1 : S[M]) :
                A)
              ((((lift R A M : (a : Multiplicative M →* A) → R[M] →ₐ[R] A) f : R[M] →ₐ[R] A) : (a : R[M]) → A) f_1 :
                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]) (Finsupp.single a b + f_1) : S[M]) :
              A)
            ((((lift R A M : (a : Multiplicative M →* A) → R[M] →ₐ[R] A) f : R[M] →ₐ[R] A) : (a : R[M]) → A)
                (Finsupp.single a b + f_1) :
              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]) x : S[M]) :
      A)
    ((((lift R A M : (a : Multiplicative M →* A) → R[M] →ₐ[R] A) f : R[M] →ₐ[R] A) : (a : R[M]) → A) x : A)

Tactic:
induction x using Finsupp.induction with
  | zero => simp
  | single_add a b f _ _ ih => simp [ih]

Premises used: AddMonoidAlgebra.single_add, AddMonoidAlgebra.zero
-- 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
x : M
⊢ Eq.{u_4 + 1} (α := A) ((φ₁ : (a : R[M]) → A) (single x 1) : A) ((φ₁ : (a : R[M]) → A) (single x 1) : A)

Tactic:
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 : CommSemiring R
inst_1 : AddMonoid M
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : Semiring B
inst_5 : Algebra R B
h :
  ∀ (a : A[M]) (m : M),
    Eq.{u_4 + 1} (α := A) ((((domCongr R A 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]) (domCongr R A 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 : AddMonoid M
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : Semiring B
inst_5 : Algebra R B
a : A[M]
m : M
⊢ Eq.{u_4 + 1} (α := A) ((((domCongr R A 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 [AddAut.one_def]

Premises used: AddAut.one_def
-- 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
x x_1 : AddAut M
h :
  ∀ (a : A[M]) (m : M),
    Eq.{u_4 + 1} (α := A) ((((domCongr R A (x * x_1) : (a : A[M]) → A[M]) a : A[M]) : (a : M) → A) m : A)
      ((((HMul.hMul (α := A[M] ≃ₐ[R] A[M]) (domCongr R A x) (domCongr R A x_1) : (a : A[M]) → A[M]) a : A[M]) :
            (a : M) → A)
          m :
        A)
⊢ domCongr R A (x * x_1) = HMul.hMul (α := A[M] ≃ₐ[R] A[M]) (domCongr R A x) (domCongr R A x_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 : AddMonoid M
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : Semiring B
inst_5 : Algebra R B
x x_1 : AddAut M
a : A[M]
m : M
⊢ Eq.{u_4 + 1} (α := A) ((((domCongr R A (x * x_1) : (a : A[M]) → A[M]) a : A[M]) : (a : M) → A) m : A)
    ((((HMul.hMul (α := A[M] ≃ₐ[R] A[M]) (domCongr R A x) (domCongr R A x_1) : (a : A[M]) → A[M]) a : A[M]) :
          (a : M) → A)
        m :
      A)

Tactic:
simp [AddAut.mul_def]

Premises used: AddAut.mul_def
-- 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
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 : AddMonoid M
inst_2 : Semiring A
inst_3 : Algebra R A
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 : AddMonoid M
inst_2 : Semiring A
inst_3 : Algebra R A
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 : AddMonoid M
inst_2 : Semiring A
inst_3 : Algebra R A
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
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 : Algebra R A
inst_3 : AddMonoid M
r : R
⊢ Eq (α := MonoidAlgebra.{u_4, u_7} A (Multiplicative M))
    (Equiv.toFun (RingEquiv.toEquiv (AddMonoidAlgebra.toMultiplicative A M)) ((algebraMap R A[M] : (a : R) → A[M]) r))
    ((algebraMap R (MonoidAlgebra.{u_4, u_7} A (Multiplicative M)) : (a : R) → MonoidAlgebra A (Multiplicative M)) r)

Tactic:
simp [AddMonoidAlgebra.toMultiplicative]

Premises used: AddMonoidAlgebra.toMultiplicative
-- 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 : Algebra R A
inst_3 : Monoid M
r : R
⊢ Eq (α := AddMonoidAlgebra.{u_4, u_7} A (Additive M))
    (Equiv.toFun (RingEquiv.toEquiv (MonoidAlgebra.toAdditive A M)) ((algebraMap R A[M] : (a : R) → A[M]) r))
    ((algebraMap R (AddMonoidAlgebra.{u_4, u_7} A (Additive M)) : (a : R) → AddMonoidAlgebra A (Additive M)) r)

Tactic:
simp [MonoidAlgebra.toAdditive]

Premises used: MonoidAlgebra.toAdditive
-- Module: Mathlib.Algebra.MonoidAlgebra.Cardinal
Goal:
R : Type u
M' : Type v
inst : Semiring R
inst_1 : Fintype M'
⊢ #R[M'] = lift.{v, u} #R ^ card M'

Tactic:
simp [MonoidAlgebra]

Premises used: MonoidAlgebra
-- Module: Mathlib.Algebra.MonoidAlgebra.Cardinal
Goal:
R M : Type u
inst : Semiring R
inst_1 : Fintype M
⊢ #R[M] = #R ^ card M

Tactic:
simp
-- Module: Mathlib.Algebra.MonoidAlgebra.Cardinal
Goal:
R : Type u
M' : Type v
inst : Semiring R
inst_1 : Infinite M'
inst_2 : Nontrivial R
⊢ #R[M'] = max (lift.{v, u} #R) (lift.{u, v} #M')

Tactic:
simp [MonoidAlgebra, max_comm]

Premises used: MonoidAlgebra, max_comm
-- Module: Mathlib.Algebra.MonoidAlgebra.Cardinal
Goal:
R M : Type u
inst : Semiring R
inst_1 : Infinite M
inst_2 : Nontrivial R
⊢ #R[M] = max #R #M

Tactic:
simp
-- Module: Mathlib.Algebra.MonoidAlgebra.Cardinal
Goal:
R : Type u
M' : Type v
inst : Semiring R
inst_1 : Nonempty M'
inst_2 : Infinite R
⊢ #R[M'] = max (lift.{v, u} #R) (lift.{u, v} #M')

Tactic:
simp [MonoidAlgebra, max_comm]

Premises used: MonoidAlgebra, max_comm
-- Module: Mathlib.Algebra.MonoidAlgebra.Cardinal
Goal:
R M : Type u
inst : Semiring R
inst_1 : Nonempty M
inst_2 : Infinite R
⊢ #R[M] = max #R #M

Tactic:
simp
-- Module: Mathlib.Algebra.MonoidAlgebra.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
x : M →₀ R
⊢ (ofCoeff x).coeff = x

Tactic:
rfl

Premises used: MonoidAlgebra.coeff, MonoidAlgebra.ofCoeff, rfl
-- Module: Mathlib.Algebra.MonoidAlgebra.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
x : R[M]
⊢ ofCoeff x.coeff = x

Tactic:
rfl

Premises used: MonoidAlgebra.coeff, MonoidAlgebra.ofCoeff, rfl
-- Module: Mathlib.Algebra.MonoidAlgebra.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
P : R[M] → Prop
⊢ (∀ (p : R[M]), P p) ↔ ∀ (q : M →₀ R), P (ofCoeff q)

Tactic:
coeffEquiv.forall_congr_left

Premises used: MonoidAlgebra.ofCoeff, Equiv.forall_congr_left, MonoidAlgebra.coeffEquiv
-- Module: Mathlib.Algebra.MonoidAlgebra.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
P : R[M] → Prop
⊢ (∃ (p : R[M]), P p) ↔ ∃ (q : M →₀ R), P (ofCoeff q)

Tactic:
coeffEquiv.exists_congr_left

Premises used: MonoidAlgebra.ofCoeff, Equiv.exists_congr_left, MonoidAlgebra.coeffEquiv
-- Module: Mathlib.Algebra.MonoidAlgebra.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
⊢ Function.Injective (α := R[M]) coeff

Tactic:
coeffEquiv.injective

Premises used: MonoidAlgebra.coeff, MonoidAlgebra.coeffEquiv, Equiv.injective
-- Module: Mathlib.Algebra.MonoidAlgebra.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
⊢ Function.Injective (α := M →₀ R) ofCoeff

Tactic:
coeffEquiv.symm.injective

Premises used: MonoidAlgebra.ofCoeff, MonoidAlgebra.coeffEquiv, Equiv.injective, Equiv.symm
-- Module: Mathlib.Algebra.MonoidAlgebra.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
x y : R[M]
⊢ x.coeff = y.coeff ↔ x = y

Tactic:
coeff_injective.eq_iff

Premises used: Function.Injective.eq_iff, MonoidAlgebra.coeff_injective
-- Module: Mathlib.Algebra.MonoidAlgebra.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
x y : M →₀ R
⊢ ofCoeff x = ofCoeff y ↔ x = y

Tactic:
ofCoeff_injective.eq_iff

Premises used: MonoidAlgebra.ofCoeff_injective, Function.Injective.eq_iff
-- Module: Mathlib.Algebra.MonoidAlgebra.Defs
Goal:
R : Type u_1
S : Type u_2
G : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
ι : Type u_7
inst : Semiring R
x y : R[M]
r r₁ r₂ : R
m m' m₁ m₂ : M
inst_1 : Nontrivial R
inst_2 : Nonempty M
⊢ Nontrivial R[M]

Tactic:
inferInstanceAs <| Nontrivial <| M →₀ R

Premises used: _private.0.MonoidAlgebra.nontrivial._proof_1
-- Module: Mathlib.Algebra.MonoidAlgebra.Defs
Goal:
R : Type u_1
S : Type u_2
G : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
ι : Type u_7
inst : Semiring R
x y : R[M]
r r₁ r₂ : R
m m' m₁ m₂ : M
inst_1 : IsCancelAdd R
⊢ IsCancelAdd R[M]

Tactic:
inferInstanceAs <| IsCancelAdd <| M →₀ R

Premises used: _private.0.MonoidAlgebra.instIsCancelAdd._proof_1
-- Module: Mathlib.Algebra.MonoidAlgebra.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
f g : R[M]
hfg : ∀ (m : M), Eq.{u_1 + 1} (α := R) ((f : (a : M) → R) m : R) ((g : (a : M) → R) m : R)
⊢ f = g

Tactic:
Finsupp.ext hfg

Premises used: Finsupp.ext, MonoidAlgebra
-- Module: Mathlib.Algebra.MonoidAlgebra.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
⊢ Eq (α := M →₀ R) (coeff 0) 0

Tactic:
rfl

Premises used: MonoidAlgebra.coeff, rfl
-- Module: Mathlib.Algebra.MonoidAlgebra.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
⊢ Eq (α := R[M]) (ofCoeff 0) 0

Tactic:
rfl

Premises used: MonoidAlgebra.ofCoeff, rfl
-- Module: Mathlib.Algebra.MonoidAlgebra.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
x : R[M]
⊢ x.coeff = 0 ↔ x = 0

Tactic:
coeff_inj

Premises used: MonoidAlgebra.coeff, MonoidAlgebra.coeff_inj
-- Module: Mathlib.Algebra.MonoidAlgebra.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
x : M →₀ R
⊢ ofCoeff x = 0 ↔ x = 0

Tactic:
ofCoeff_inj

Premises used: MonoidAlgebra.ofCoeff, MonoidAlgebra.ofCoeff_inj
-- Module: Mathlib.Algebra.MonoidAlgebra.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
x y : R[M]
⊢ (x + y).coeff = x.coeff + y.coeff

Tactic:
rfl

Premises used: MonoidAlgebra.coeff, rfl
-- Module: Mathlib.Algebra.MonoidAlgebra.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
x y : M →₀ R
⊢ ofCoeff (x + y) = ofCoeff x + ofCoeff y

Tactic:
rfl

Premises used: MonoidAlgebra.ofCoeff, rfl
-- Module: Mathlib.Algebra.MonoidAlgebra.Defs
Goal:
R : Type u_1
M : Type u_4
ι : Type u_7
inst : Semiring R
s : Finset ι
f : ι → R[M]
⊢ Eq (α := M →₀ R) (coeff (∑ i ∈ s, f i)) (∑ i ∈ s, (f i).coeff)

Tactic:
map_sum coeffAddEquiv ..

Premises used: Multiset.sum, Multiset.foldr, MonoidAlgebra.coeff, map_sum, MonoidAlgebra.coeffAddEquiv, Finset.sum
-- Module: Mathlib.Algebra.MonoidAlgebra.Defs
Goal:
R : Type u_1
M : Type u_4
ι : Type u_7
inst : Semiring R
s : Finset ι
f : ι → M →₀ R
⊢ Eq (α := R[M]) (ofCoeff (∑ i ∈ s, f i)) (∑ i ∈ s, ofCoeff (f i))

Tactic:
map_sum coeffAddEquiv.symm ..

Premises used: Multiset.sum, Multiset.foldr, MonoidAlgebra.ofCoeff, map_sum, MonoidAlgebra.coeffAddEquiv, Finset.sum, AddEquiv.symm
-- Module: Mathlib.Algebra.MonoidAlgebra.Defs
Goal:
R : Type u_1
M : Type u_4
N : Type u_5
ι : Type u_7
inst : Semiring R
inst_1 : AddCommMonoid N
f : ι →₀ N
g : ι → N → R[M]
⊢ (f.sum g).coeff = f.sum fun (i : ι) (n : N) ↦ (g i n).coeff

Tactic:
map_finsuppSum coeffAddEquiv ..

Premises used: Multiset.sum, Multiset.foldr, MonoidAlgebra.coeff, Finsupp.sum, map_finsuppSum, MonoidAlgebra.coeffAddEquiv, Finset.sum
-- Module: Mathlib.Algebra.MonoidAlgebra.Defs
Goal:
R : Type u_1
M : Type u_4
N : Type u_5
ι : Type u_7
inst : Semiring R
inst_1 : AddCommMonoid N
f : ι →₀ N
g : ι → N → M →₀ R
⊢ ofCoeff (f.sum g) = f.sum fun (i : ι) (n : N) ↦ ofCoeff (g i n)

Tactic:
map_finsuppSum coeffAddEquiv.symm ..

Premises used: Multiset.sum, Multiset.foldr, MonoidAlgebra.ofCoeff, Finsupp.sum, map_finsuppSum, MonoidAlgebra.coeffAddEquiv, Finset.sum, AddEquiv.symm
-- Module: Mathlib.Algebra.MonoidAlgebra.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
m : M
x : R[M]
⊢ (erase m x).coeff = Finsupp.erase m x.coeff

Tactic:
rfl

Premises used: Finsupp.erase, MonoidAlgebra.coeff, MonoidAlgebra.ofCoeff, MonoidAlgebra.erase, rfl
-- Module: Mathlib.Algebra.MonoidAlgebra.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
m : M
x : M →₀ R
⊢ ofCoeff (Finsupp.erase m x) = erase m (ofCoeff x)

Tactic:
rfl

Premises used: MonoidAlgebra.coeff, MonoidAlgebra.ofCoeff, MonoidAlgebra.erase, rfl
-- Module: Mathlib.Algebra.MonoidAlgebra.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
m : M
⊢ Eq (α := R[M]) (erase m 0) 0

Tactic:
simp [erase]

Premises used: MonoidAlgebra.erase
-- Module: Mathlib.Algebra.MonoidAlgebra.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
m : M
r : R
simp : Eq (α := R[M]) 0 0
⊢ Eq (α := R[M]) (erase m (single m r)) 0

Tactic:
simp [erase, ofCoeff, coeff]

Premises used: MonoidAlgebra.coeff, MonoidAlgebra.ofCoeff, MonoidAlgebra.erase
-- Module: Mathlib.Algebra.MonoidAlgebra.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
m : M
r : R
⊢ Eq (α := R[M]) 0 0

Tactic:
rfl
-- Module: Mathlib.Algebra.MonoidAlgebra.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
m : M
r : R
x : R[M]
⊢ (update m r x).coeff = x.coeff.update m r

Tactic:
rfl

Premises used: MonoidAlgebra.coeff, MonoidAlgebra.ofCoeff, Finsupp.update, MonoidAlgebra.update, rfl
-- Module: Mathlib.Algebra.MonoidAlgebra.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
m : M
r : R
x : M →₀ R
⊢ ofCoeff (x.update m r) = update m r (ofCoeff x)

Tactic:
rfl

Premises used: MonoidAlgebra.coeff, MonoidAlgebra.ofCoeff, MonoidAlgebra.update, rfl
-- Module: Mathlib.Algebra.MonoidAlgebra.Defs
Goal:
R : Type u_1
S : Type u_2
G : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
ι : Type u_7
inst : Semiring R
x y : R[M]
r r₁ r₂ : R
m m' m₁ m₂ : M
A : Type u_8
inst_1 : SMulZeroClass A R
⊢ Eq (α := SMul ℕ R[M]) (@SMulZeroClass.toSMul _ _ AddZero.toZero _) AddMonoid.toNSMul

Tactic:
rfl
-- Module: Mathlib.Algebra.MonoidAlgebra.Defs
Goal:
R : Type u_1
S : Type u_2
G : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
ι : Type u_7
inst : Semiring R
x y : R[M]
r r₁ r₂ : R
m m' m₁ m₂ : M
A : Type u_8
inst_1 : SMulZeroClass A R
⊢ Eq (α := SMul ℕ R[M]) (@SMulZeroClass.toSMul _ _ AddZero.toZero _) AddMonoid.toNSMul

Tactic:
with_reducible_and_instances rfl
-- Module: Mathlib.Algebra.MonoidAlgebra.Defs
Goal:
R : Type u_1
S : Type u_2
G : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
ι : Type u_7
inst : Semiring R
x_1 y : R[M]
r r₁ r₂ : R
m m' m₁ m₂ : M
A : Type u_8
inst_1 : SMulZeroClass A R
inst_2 : Monoid A
a : Aˣ
x : R[M]
⊢ a • x = (↑a : A) • x

Tactic:
rfl
-- Module: Mathlib.Algebra.MonoidAlgebra.Defs
Goal:
R : Type u_1
S : Type u_2
G : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
ι : Type u_7
inst : Semiring R
x_1 y : R[M]
r r₁ r₂ : R
m m' m₁ m₂ : M
A : Type u_8
inst_1 : SMulZeroClass A R
inst_2 : Monoid A
a : Aˣ
x : R[M]
⊢ a • x = (↑a : A) • x

Tactic:
with_reducible_and_instances rfl
-- Module: Mathlib.Algebra.MonoidAlgebra.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
A : Type u_8
inst_1 : SMulZeroClass A R
a : A
x : R[M]
⊢ (a • x).coeff = a • x.coeff

Tactic:
rfl

Premises used: MonoidAlgebra.coeff, rfl
-- Module: Mathlib.Algebra.MonoidAlgebra.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
A : Type u_8
inst_1 : SMulZeroClass A R
a : A
x : M →₀ R
⊢ ofCoeff (a • x) = a • ofCoeff x

Tactic:
rfl

Premises used: MonoidAlgebra.ofCoeff, rfl
-- Module: Mathlib.Algebra.MonoidAlgebra.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
A : Type u_8
inst_1 : SMulZeroClass A R
a : A
x : R[M]
m : M
⊢ (a • x : (a : M) → R) m = HSMul.hSMul (β := R) a ((x : (a : M) → R) m : R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.MonoidAlgebra.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
A : Type u_8
inst_1 : SMulZeroClass A R
a : A
m : M
r : R
hfg :
  ∀ (m_1 : M),
    Eq.{u_1 + 1} (α := R) ((HSMul.hSMul (β := R[M]) a (single m r) : (a : M) → R) m_1 : R)
      ((single m (a • r) : (a : M) → R) m_1 : R)
⊢ HSMul.hSMul (β := R[M]) a (single m r) = single m (a • r)

Tactic:
ext
-- Module: Mathlib.Algebra.MonoidAlgebra.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
A : Type u_8
inst_1 : SMulZeroClass A R
a : A
m : M
r : R
m_1 : M
⊢ Eq.{u_1 + 1} (α := R) ((HSMul.hSMul (β := R[M]) a (single m r) : (a : M) → R) m_1 : R)
    ((single m (a • r) : (a : M) → R) m_1 : R)

Tactic:
simp [single, ← Finsupp.smul_single]

Premises used: Finsupp.smul_single, MonoidAlgebra.single
-- Module: Mathlib.Algebra.MonoidAlgebra.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
r' : R
m : M
r : R
⊢ HSMul.hSMul (β := R[M]) r' (single m r) = single m (r' * r)

Tactic:
smul_single ..

Premises used: MonoidAlgebra.smul_single
-- Module: Mathlib.Algebra.MonoidAlgebra.Defs
Goal:
R : Type u_1
S : Type u_2
G : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
ι : Type u_7
inst : Semiring R
x y : R[M]
r r₁ r₂ : R
m m' m₁ m₂ : M
A : Type u_8
inst_1 : SMulZeroClass A R
inst_2 : SMulZeroClass N R
inst_3 : SMulZeroClass O R
inst_4 : SMul N O
inst_5 : IsScalarTower N O R
⊢ IsScalarTower N O R[M]

Tactic:
inferInstanceAs <| IsScalarTower N O (M →₀ R)

Premises used: _private.0.MonoidAlgebra.isScalarTower._proof_1
-- Module: Mathlib.Algebra.MonoidAlgebra.Defs
Goal:
R : Type u_1
S : Type u_2
G : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
ι : Type u_7
inst : Semiring R
x y : R[M]
r r₁ r₂ : R
m m' m₁ m₂ : M
A : Type u_8
inst_1 : SMulZeroClass A R
inst_2 : SMulZeroClass N R
inst_3 : SMulZeroClass O R
inst_4 : SMulCommClass N O R
⊢ SMulCommClass N O R[M]

Tactic:
inferInstanceAs <| SMulCommClass N O (M →₀ R)

Premises used: _private.0.MonoidAlgebra.smulCommClass._proof_1
-- Module: Mathlib.Algebra.MonoidAlgebra.Defs
Goal:
R : Type u_1
S : Type u_2
G : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
ι : Type u_7
inst : Semiring R
x y : R[M]
r r₁ r₂ : R
m m' m₁ m₂ : M
A : Type u_8
inst_1 : SMulZeroClass A R
inst_2 : SMulZeroClass N R
inst_3 : SMulZeroClass.{u_5, u_1} Nᵐᵒᵖ R
inst_4 : IsCentralScalar N R
⊢ IsCentralScalar N R[M]

Tactic:
inferInstanceAs <| IsCentralScalar N (M →₀ R)

Premises used: _private.0.MonoidAlgebra.isCentralScalar._proof_1
-- Module: Mathlib.Algebra.MonoidAlgebra.Defs
Goal:
R : Type u_1
G : Type u_3
inst : Semiring R
f g : R[G]
⊢ (⇑(f + g) : (a : G) → R) = HAdd.hAdd (α := (a : G) → R) (⇑f : (a : G) → R) (⇑g : (a : G) → R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.MonoidAlgebra.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
m : M
⊢ Eq (α := R[M]) (single m 0) 0

Tactic:
Finsupp.single_zero m

Premises used: MonoidAlgebra, Finsupp.single_zero
-- Module: Mathlib.Algebra.MonoidAlgebra.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
m : M
r₁ r₂ : R
⊢ single m (r₁ + r₂) = HAdd.hAdd (α := R[M]) (single m r₁) (single m r₂)

Tactic:
Finsupp.single_add m r₁ r₂

Premises used: Finsupp.single_add, MonoidAlgebra
-- Module: Mathlib.Algebra.MonoidAlgebra.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
N : Type u_8
inst_1 : AddZeroClass N
f g : R[M] →+ N
hfg : ∀ (m : M), f.comp (singleAddHom m) = g.comp (singleAddHom m)
⊢ f = g

Tactic:
Finsupp.addHom_ext' hfg

Premises used: MonoidAlgebra, Finsupp.addHom_ext'
-- Module: Mathlib.Algebra.MonoidAlgebra.Defs
Goal:
R : Type u_1
M : Type u_4
N : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid N
m : M
r : R
h : M → R → N
h_zero : h m 0 = 0
⊢ sum (single m r) h = h m r

Tactic:
simp [h_zero]
-- Module: Mathlib.Algebra.MonoidAlgebra.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
x : R[M]
⊢ sum x single = x

Tactic:
Finsupp.sum_single _

Premises used: MonoidAlgebra, Finsupp.sum_single
-- Module: Mathlib.Algebra.MonoidAlgebra.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
a a' : M
b : R
inst_1 : Decidable (a = a')
⊢ (single a b : (a : M) → R) a' = if a = a' then b else 0

Tactic:
Finsupp.single_apply

Premises used: Finsupp.single_apply