awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.MonoidAlgebra.MapDomain
Goal:
ι : Type u_1
F : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
M : Type u_6
N : Type u_7
O : Type u_8
inst : Semiring R
inst_1 : Semiring S
inst_2 : Semiring T
f : M → N
a : M
r : R
inst_3 : Monoid M
inst_4 : Monoid N
inst_5 : Monoid O
e : R ≃+* S
h₁ :
  ∀ (r : R),
    Eq (α := R[M])
      ((RingHom.comp (β := S[M]) (mapRingHom M (↑e.symm : S →+* R)) (mapRingHom M (↑e : R →+* S)) : (a : R[M]) → R[M])
          (single 1 r) :
        R[M])
      ((RingHom.id R[M] : (a : R[M]) → R[M]) (single 1 r) : R[M])
h_of :
  ∀ (m : M),
    Eq (α := R[M])
      ((RingHom.comp (β := S[M]) (mapRingHom M (↑e.symm : S →+* R)) (mapRingHom M (↑e : R →+* S)) : (a : R[M]) → R[M])
          (single m 1) :
        R[M])
      ((RingHom.id R[M] : (a : R[M]) → R[M]) (single m 1) : R[M])
⊢ Eq (α := R[M] →+* R[M]) (RingHom.comp (β := S[M]) (mapRingHom M (↑e.symm : S →+* R)) (mapRingHom M (↑e : R →+* S)))
    (RingHom.id R[M])

Tactic:
apply MonoidAlgebra.ringHom_ext

Premises used: MonoidAlgebra.ringHom_ext
-- Module: Mathlib.Algebra.MonoidAlgebra.MapDomain
Goal:
ι : Type u_1
F : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
M : Type u_6
N : Type u_7
O : Type u_8
inst : Semiring R
inst_1 : Semiring S
inst_2 : Semiring T
f : M → N
a : M
r : R
inst_3 : Monoid M
inst_4 : Monoid N
inst_5 : Monoid O
e : R ≃+* S
⊢ ∀ (r : R),
    Eq (α := R[M])
      ((RingHom.comp (β := S[M]) (mapRingHom M (↑e.symm : S →+* R)) (mapRingHom M (↑e : R →+* S)) : (a : R[M]) → R[M])
          (single 1 r) :
        R[M])
      ((RingHom.id R[M] : (a : R[M]) → R[M]) (single 1 r) : R[M])

Tactic:
simp
-- Module: Mathlib.Algebra.MonoidAlgebra.MapDomain
Goal:
ι : Type u_1
F : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
M : Type u_6
N : Type u_7
O : Type u_8
inst : Semiring R
inst_1 : Semiring S
inst_2 : Semiring T
f : M → N
a : M
r : R
inst_3 : Monoid M
inst_4 : Monoid N
inst_5 : Monoid O
e : R ≃+* S
⊢ ∀ (m : M),
    Eq (α := R[M])
      ((RingHom.comp (β := S[M]) (mapRingHom M (↑e.symm : S →+* R)) (mapRingHom M (↑e : R →+* S)) : (a : R[M]) → R[M])
          (single m 1) :
        R[M])
      ((RingHom.id R[M] : (a : R[M]) → R[M]) (single m 1) : R[M])

Tactic:
simp
-- Module: Mathlib.Algebra.MonoidAlgebra.MapDomain
Goal:
R : Type u_3
S : Type u_4
M : Type u_6
inst : Semiring R
inst_1 : Semiring S
inst_2 : Monoid M
e : R ≃+* S
x : R[M]
m : M
⊢ Eq.{u_4 + 1} (α := S) ((((mapRingEquiv M e : (a : R[M]) → S[M]) x : S[M]) : (a : M) → S) m : S)
    ((e : (a : R) → S) ((x : (a : M) → R) m : R) : S)

Tactic:
simp [mapRingEquiv]

Premises used: MonoidAlgebra.mapRingEquiv
-- Module: Mathlib.Algebra.MonoidAlgebra.MapDomain
Goal:
R : Type u_3
S : Type u_4
M : Type u_6
inst : Semiring R
inst_1 : Semiring S
inst_2 : Monoid M
e : R ≃+* S
r : R
m : M
⊢ Eq (α := S[M]) ((mapRingEquiv M e : (a : R[M]) → S[M]) (single m r) : S[M]) (single m ((e : (a : R) → S) r) : S[M])

Tactic:
simp [mapRingEquiv]

Premises used: MonoidAlgebra.mapRingEquiv
-- Module: Mathlib.Algebra.MonoidAlgebra.MapDomain
Goal:
R : Type u_3
S : Type u_4
M : Type u_6
inst : Semiring R
inst_1 : Semiring S
inst_2 : Monoid M
e : R ≃+* S
⊢ Eq (α := R[M] →+* S[M]) (RingEquiv.toRingHom (mapRingEquiv M e)) (mapRingHom M (↑e : R →+* S))

Tactic:
rfl

Premises used: MonoidAlgebra.ofCoeff, MulEquiv.toMonoidHom, Finsupp.onFinset, MonoidAlgebra.map, RingEquiv.toRingHom, MonoidAlgebra.mapRingHom, Finsupp.mapRange, rfl
-- Module: Mathlib.Algebra.MonoidAlgebra.MapDomain
Goal:
R : Type u_3
S : Type u_4
M : Type u_6
inst : Semiring R
inst_1 : Semiring S
inst_2 : Monoid M
e : R ≃+* S
⊢ Eq (α := S[M] ≃+* R[M]) (RingEquiv.symm (mapRingEquiv M e)) (mapRingEquiv M e.symm)

Tactic:
rfl

Premises used: MonoidAlgebra.mapRingEquiv, RingEquiv.ofRingHom, Equiv.symm, RingEquiv.symm, rfl
-- Module: Mathlib.Algebra.MonoidAlgebra.MapDomain
Goal:
R : Type u_3
S : Type u_4
T : Type u_5
M : Type u_6
inst : Semiring R
inst_1 : Semiring S
inst_2 : Semiring T
inst_3 : Monoid M
e₁ : R ≃+* S
e₂ : S ≃+* T
h :
  ∀ (x : R[M]) (m : M),
    Eq.{u_5 + 1} (α := T) ((((mapRingEquiv M (e₁.trans e₂) : (a : R[M]) → T[M]) x : T[M]) : (a : M) → T) m : T)
      ((((RingEquiv.trans (mapRingEquiv M e₁) (mapRingEquiv M e₂) : (a : R[M]) → T[M]) x : T[M]) : (a : M) → T) m : T)
⊢ Eq (α := R[M] ≃+* T[M]) (mapRingEquiv M (e₁.trans e₂)) (RingEquiv.trans (mapRingEquiv M e₁) (mapRingEquiv M e₂))

Tactic:
ext
-- Module: Mathlib.Algebra.MonoidAlgebra.MapDomain
Goal:
R : Type u_3
S : Type u_4
T : Type u_5
M : Type u_6
inst : Semiring R
inst_1 : Semiring S
inst_2 : Semiring T
inst_3 : Monoid M
e₁ : R ≃+* S
e₂ : S ≃+* T
x : R[M]
m : M
⊢ Eq.{u_5 + 1} (α := T) ((((mapRingEquiv M (e₁.trans e₂) : (a : R[M]) → T[M]) x : T[M]) : (a : M) → T) m : T)
    ((((RingEquiv.trans (mapRingEquiv M e₁) (mapRingEquiv M e₂) : (a : R[M]) → T[M]) x : T[M]) : (a : M) → T) m : T)

Tactic:
simp
-- Module: Mathlib.Algebra.MonoidAlgebra.MapDomain
Goal:
R : Type u_3
M : Type u_6
N : Type u_7
inst : Semiring R
inst_1 : Monoid M
inst_2 : Monoid N
⊢ Eq (α := R[N][M] ≃+* R[M][N]) (RingEquiv.symm commRingEquiv) commRingEquiv

Tactic:
rfl

Premises used: Multiset.sum, Multiset.foldr, Equiv.trans, MonoidAlgebra.commRingEquiv, Finsupp.mapDomain, Finsupp.sum, Finsupp.curry, RingEquiv.trans, Prod.swap, Equiv.symm, Finset.sum, RingEquiv.symm, rfl
-- Module: Mathlib.Algebra.MonoidAlgebra.MapDomain
Goal:
R : Type u_3
M : Type u_6
N : Type u_7
inst : Semiring R
inst_1 : Monoid M
inst_2 : Monoid N
m : M
n : N
r : R
⊢ Eq (α := R[M][N]) ((commRingEquiv : (a : R[N][M]) → R[M][N]) (single m (single n r)) : R[M][N])
    (single n (single m r) : R[M][N])

Tactic:
simp [commRingEquiv, MonoidAlgebra, curryRingEquiv, curryAddEquiv, mapDomainRingEquiv,
    mapDomainRingHom, EquivLike.toEquiv]

Premises used: MonoidAlgebra.commRingEquiv, Finsupp.curryAddEquiv, MonoidAlgebra.curryRingEquiv, MonoidAlgebra, MonoidAlgebra.mapDomainRingHom, MonoidAlgebra.mapDomainRingEquiv, EquivLike.toEquiv
-- Module: Mathlib.Algebra.MonoidAlgebra.MapDomain
Goal:
R : Type u_3
M : Type u_6
N : Type u_7
inst : Semiring R
inst_1 : Monoid M
inst_2 : Monoid N
m : M
⊢ Eq (α := R[M][N]) ((commRingEquiv : (a : R[N][M]) → R[M][N]) (single m 1) : R[M][N]) (single 1 (single m 1) : R[M][N])

Tactic:
commRingEquiv_single_single ..

Premises used: MonoidAlgebra.commRingEquiv_single_single
-- Module: Mathlib.Algebra.MonoidAlgebra.MapDomain
Goal:
R : Type u_3
M : Type u_6
N : Type u_7
inst : Semiring R
inst_1 : Monoid M
inst_2 : Monoid N
m : M
⊢ Eq (α := R[N][M]) ((commRingEquiv : (a : R[M][N]) → R[N][M]) (single 1 (single m 1)) : R[N][M]) (single m 1 : R[N][M])

Tactic:
commRingEquiv_single_single ..

Premises used: MonoidAlgebra.commRingEquiv_single_single
-- Module: Mathlib.Algebra.MonoidAlgebra.MapDomain
Goal:
R : Type u_3
S : Type u_4
M : Type u_6
inst : Ring R
inst_1 : Ring S
f : R →+ S
x : R[M]
⊢ map f (-x) = -map f x

Tactic:
Finsupp.mapRange_neg (hf := f.map_zero) f.map_neg ..

Premises used: MonoidAlgebra.ofCoeff, Finsupp.mapRange_neg, AddMonoidHom.map_neg, Finsupp.onFinset, MonoidAlgebra.map, MonoidAlgebra, Finsupp.mapRange
-- Module: Mathlib.Algebra.MonoidAlgebra.MapDomain
Goal:
R : Type u_3
S : Type u_4
M : Type u_6
inst : Ring R
inst_1 : Ring S
f : R →+ S
x y : R[M]
⊢ map f (x - y) = map f x - map f y

Tactic:
Finsupp.mapRange_sub (hf := f.map_zero) f.map_sub ..

Premises used: MonoidAlgebra.ofCoeff, Finsupp.mapRange_sub, Finsupp.onFinset, MonoidAlgebra.map, MonoidAlgebra, AddMonoidHom.map_sub, Finsupp.mapRange
-- Module: Mathlib.Algebra.MonoidAlgebra.MapDomain
Goal:
ι : Type u_1
F : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
M : Type u_6
N : Type u_7
O : Type u_8
k : Type u_9
G : Type u_10
inst : Semiring k
inst_1 : Add G
x : k[G]
hfg :
  ∀ (m : G),
    Eq.{u_9 + 1} (α := k)
      (((fun (x : MonoidAlgebra.{u_9, u_10} k (Multiplicative G)) ↦
                (MonoidAlgebra.mapDomain (⇑Multiplicative.toAdd : (a : Multiplicative G) → G) x : MonoidAlgebra k G))
              ((fun (x : k[G]) ↦
                  (mapDomain (⇑Multiplicative.ofAdd : (a : G) → Multiplicative G) x :
                    AddMonoidAlgebra.{u_9, u_10} k (Multiplicative G)))
                x) :
            (a : G) → k)
          m :
        k)
      ((x : (a : G) → k) m : k)
⊢ (fun (x : MonoidAlgebra.{u_9, u_10} k (Multiplicative G)) ↦
        (MonoidAlgebra.mapDomain (⇑Multiplicative.toAdd : (a : Multiplicative G) → G) x : MonoidAlgebra k G))
      ((fun (x : k[G]) ↦
          (mapDomain (⇑Multiplicative.ofAdd : (a : G) → Multiplicative G) x :
            AddMonoidAlgebra.{u_9, u_10} k (Multiplicative G)))
        x) =
    x

Tactic:
ext
-- Module: Mathlib.Algebra.MonoidAlgebra.MapDomain
Goal:
ι : Type u_1
F : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
M : Type u_6
N : Type u_7
O : Type u_8
k : Type u_9
G : Type u_10
inst : Semiring k
inst_1 : Add G
x : k[G]
m : G
⊢ Eq.{u_9 + 1} (α := k)
    (((fun (x : MonoidAlgebra.{u_9, u_10} k (Multiplicative G)) ↦
              (MonoidAlgebra.mapDomain (⇑Multiplicative.toAdd : (a : Multiplicative G) → G) x : MonoidAlgebra k G))
            ((fun (x : k[G]) ↦
                (mapDomain (⇑Multiplicative.ofAdd : (a : G) → Multiplicative G) x :
                  AddMonoidAlgebra.{u_9, u_10} k (Multiplicative G)))
              x) :
          (a : G) → k)
        m :
      k)
    ((x : (a : G) → k) m : k)

Tactic:
simp
-- Module: Mathlib.Algebra.MonoidAlgebra.MapDomain
Goal:
ι : Type u_1
F : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
M : Type u_6
N : Type u_7
O : Type u_8
k : Type u_9
G : Type u_10
inst : Semiring k
inst_1 : Add G
x : MonoidAlgebra.{u_9, u_10} k (Multiplicative G)
hfg :
  ∀ (m : Multiplicative G),
    Eq.{u_9 + 1} (α := k)
      (((fun (x : k[G]) ↦
                (mapDomain (⇑Multiplicative.ofAdd : (a : G) → Multiplicative G) x :
                  AddMonoidAlgebra.{u_9, u_10} k (Multiplicative G)))
              ((fun (x : MonoidAlgebra.{u_9, u_10} k (Multiplicative G)) ↦
                  (MonoidAlgebra.mapDomain (⇑Multiplicative.toAdd : (a : Multiplicative G) → G) x : MonoidAlgebra k G))
                x) :
            (a : Multiplicative G) → k)
          m :
        k)
      ((x : (a : Multiplicative G) → k) m : k)
⊢ (fun (x : k[G]) ↦
        (mapDomain (⇑Multiplicative.ofAdd : (a : G) → Multiplicative G) x :
          AddMonoidAlgebra.{u_9, u_10} k (Multiplicative G)))
      ((fun (x : MonoidAlgebra.{u_9, u_10} k (Multiplicative G)) ↦
          (MonoidAlgebra.mapDomain (⇑Multiplicative.toAdd : (a : Multiplicative G) → G) x : MonoidAlgebra k G))
        x) =
    x

Tactic:
ext
-- Module: Mathlib.Algebra.MonoidAlgebra.MapDomain
Goal:
ι : Type u_1
F : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
M : Type u_6
N : Type u_7
O : Type u_8
k : Type u_9
G : Type u_10
inst : Semiring k
inst_1 : Add G
x : MonoidAlgebra.{u_9, u_10} k (Multiplicative G)
m : Multiplicative G
⊢ Eq.{u_9 + 1} (α := k)
    (((fun (x : k[G]) ↦
              (mapDomain (⇑Multiplicative.ofAdd : (a : G) → Multiplicative G) x :
                AddMonoidAlgebra.{u_9, u_10} k (Multiplicative G)))
            ((fun (x : MonoidAlgebra.{u_9, u_10} k (Multiplicative G)) ↦
                (MonoidAlgebra.mapDomain (⇑Multiplicative.toAdd : (a : Multiplicative G) → G) x : MonoidAlgebra k G))
              x) :
          (a : Multiplicative G) → k)
        m :
      k)
    ((x : (a : Multiplicative G) → k) m : k)

Tactic:
simp
-- Module: Mathlib.Algebra.MonoidAlgebra.MapDomain
Goal:
ι : Type u_1
F : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
M : Type u_6
N : Type u_7
O : Type u_8
k : Type u_9
G : Type u_10
inst : Semiring k
inst_1 : Add G
x y : k[G]
dsimp :
  mapDomain (fun (x : G) ↦ x) (x * y) =
    HMul.hMul (α := MonoidAlgebra.{u_9, u_10} k (Multiplicative G)) (mapDomain (fun (x : G) ↦ x) x)
      (mapDomain (fun (x : G) ↦ x) y)
⊢ mapDomain (⇑Multiplicative.ofAdd : (a : G) → Multiplicative G) (x * y) =
    HMul.hMul (α := MonoidAlgebra.{u_9, u_10} k (Multiplicative G))
      (mapDomain (⇑Multiplicative.ofAdd : (a : G) → Multiplicative G) x)
      (mapDomain (⇑Multiplicative.ofAdd : (a : G) → Multiplicative G) y)

Tactic:
dsimp [Multiplicative.ofAdd]

Premises used: Multiplicative.ofAdd
-- Module: Mathlib.Algebra.MonoidAlgebra.MapDomain
Goal:
ι : Type u_1
F : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
M : Type u_6
N : Type u_7
O : Type u_8
k : Type u_9
G : Type u_10
inst : Semiring k
inst_1 : Add G
x y : k[G]
⊢ mapDomain (fun (x : G) ↦ x) (x * y) =
    HMul.hMul (α := MonoidAlgebra.{u_9, u_10} k (Multiplicative G)) (mapDomain (fun (x : G) ↦ x) x)
      (mapDomain (fun (x : G) ↦ x) y)

Tactic:
MonoidAlgebra.mapDomain_mul (M := Multiplicative G) (MulHom.id (Multiplicative G)) x y

Premises used: Multiplicative, MulHom.id, MonoidAlgebra.mapDomain_mul
-- Module: Mathlib.Algebra.MonoidAlgebra.MapDomain
Goal:
ι : Type u_1
F : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
M : Type u_6
N : Type u_7
O : Type u_8
k : Type u_9
G : Type u_10
inst : Semiring k
inst_1 : Add G
x y : k[G]
⊢ mapDomain (fun (x : G) ↦ x) (x * y) =
    HMul.hMul (α := MonoidAlgebra.{u_9, u_10} k (Multiplicative G)) (mapDomain (fun (x : G) ↦ x) x)
      (mapDomain (fun (x : G) ↦ x) y)

Tactic:
exact MonoidAlgebra.mapDomain_mul (M := Multiplicative G) (MulHom.id (Multiplicative G)) x y

Premises used: Multiplicative, MulHom.id, MonoidAlgebra.mapDomain_mul
-- Module: Mathlib.Algebra.MonoidAlgebra.MapDomain
Goal:
ι : Type u_1
F : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
M : Type u_6
N : Type u_7
O : Type u_8
k : Type u_9
G : Type u_10
inst : Semiring k
inst_1 : Mul G
x : k[G]
hfg :
  ∀ (m : G),
    Eq.{u_9 + 1} (α := k)
      (((fun (x : AddMonoidAlgebra.{u_9, u_10} k (Additive G)) ↦
                (AddMonoidAlgebra.mapDomain (⇑Additive.toMul : (a : Additive G) → G) x : AddMonoidAlgebra k G))
              ((fun (x : k[G]) ↦
                  (mapDomain (⇑Additive.ofMul : (a : G) → Additive G) x : MonoidAlgebra.{u_9, u_10} k (Additive G)))
                x) :
            (a : G) → k)
          m :
        k)
      ((x : (a : G) → k) m : k)
⊢ (fun (x : AddMonoidAlgebra.{u_9, u_10} k (Additive G)) ↦
        (AddMonoidAlgebra.mapDomain (⇑Additive.toMul : (a : Additive G) → G) x : AddMonoidAlgebra k G))
      ((fun (x : k[G]) ↦
          (mapDomain (⇑Additive.ofMul : (a : G) → Additive G) x : MonoidAlgebra.{u_9, u_10} k (Additive G)))
        x) =
    x

Tactic:
ext
-- Module: Mathlib.Algebra.MonoidAlgebra.MapDomain
Goal:
ι : Type u_1
F : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
M : Type u_6
N : Type u_7
O : Type u_8
k : Type u_9
G : Type u_10
inst : Semiring k
inst_1 : Mul G
x : k[G]
m : G
⊢ Eq.{u_9 + 1} (α := k)
    (((fun (x : AddMonoidAlgebra.{u_9, u_10} k (Additive G)) ↦
              (AddMonoidAlgebra.mapDomain (⇑Additive.toMul : (a : Additive G) → G) x : AddMonoidAlgebra k G))
            ((fun (x : k[G]) ↦
                (mapDomain (⇑Additive.ofMul : (a : G) → Additive G) x : MonoidAlgebra.{u_9, u_10} k (Additive G)))
              x) :
          (a : G) → k)
        m :
      k)
    ((x : (a : G) → k) m : k)

Tactic:
simp
-- Module: Mathlib.Algebra.MonoidAlgebra.MapDomain
Goal:
ι : Type u_1
F : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
M : Type u_6
N : Type u_7
O : Type u_8
k : Type u_9
G : Type u_10
inst : Semiring k
inst_1 : Mul G
x : AddMonoidAlgebra.{u_9, u_10} k (Additive G)
hfg :
  ∀ (m : Additive G),
    Eq.{u_9 + 1} (α := k)
      (((fun (x : k[G]) ↦
                (mapDomain (⇑Additive.ofMul : (a : G) → Additive G) x : MonoidAlgebra.{u_9, u_10} k (Additive G)))
              ((fun (x : AddMonoidAlgebra.{u_9, u_10} k (Additive G)) ↦
                  (AddMonoidAlgebra.mapDomain (⇑Additive.toMul : (a : Additive G) → G) x : AddMonoidAlgebra k G))
                x) :
            (a : Additive G) → k)
          m :
        k)
      ((x : (a : Additive G) → k) m : k)
⊢ (fun (x : k[G]) ↦ (mapDomain (⇑Additive.ofMul : (a : G) → Additive G) x : MonoidAlgebra.{u_9, u_10} k (Additive G)))
      ((fun (x : AddMonoidAlgebra.{u_9, u_10} k (Additive G)) ↦
          (AddMonoidAlgebra.mapDomain (⇑Additive.toMul : (a : Additive G) → G) x : AddMonoidAlgebra k G))
        x) =
    x

Tactic:
ext
-- Module: Mathlib.Algebra.MonoidAlgebra.MapDomain
Goal:
ι : Type u_1
F : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
M : Type u_6
N : Type u_7
O : Type u_8
k : Type u_9
G : Type u_10
inst : Semiring k
inst_1 : Mul G
x : AddMonoidAlgebra.{u_9, u_10} k (Additive G)
m : Additive G
⊢ Eq.{u_9 + 1} (α := k)
    (((fun (x : k[G]) ↦
              (mapDomain (⇑Additive.ofMul : (a : G) → Additive G) x : MonoidAlgebra.{u_9, u_10} k (Additive G)))
            ((fun (x : AddMonoidAlgebra.{u_9, u_10} k (Additive G)) ↦
                (AddMonoidAlgebra.mapDomain (⇑Additive.toMul : (a : Additive G) → G) x : AddMonoidAlgebra k G))
              x) :
          (a : Additive G) → k)
        m :
      k)
    ((x : (a : Additive G) → k) m : k)

Tactic:
simp
-- Module: Mathlib.Algebra.MonoidAlgebra.Module
Goal:
R : Type u_2
M : Type u_4
S : Type u_5
inst : Semiring R
inst_1 : Semiring S
inst_2 : Module R S
s : Set M
x : S[M]
⊢ Membership.mem (γ := Submodule R S[M]) (supported R S s) x ↔ (↑x.coeff.support : Set M) ⊆ s

Tactic:
.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.Subset, Set.preimage
-- Module: Mathlib.Algebra.MonoidAlgebra.Module
Goal:
R : Type u_2
M : Type u_4
S : Type u_5
inst : Semiring R
inst_1 : Semiring S
inst_2 : Module R S
s : Set M
x : S[M]
⊢ Membership.mem (γ := Submodule R S[M]) (supported R S s) x ↔
    ∀ m ∉ s, Eq.{u_5 + 1} (α := S) ((x.coeff : (a : M) → S) m : S) (0 : S)

Tactic:
simp [mem_supported, Set.subset_def, not_imp_comm]

Premises used: Set.subset_def, not_imp_comm, MonoidAlgebra.mem_supported
-- Module: Mathlib.Algebra.MonoidAlgebra.Module
Goal:
R : Type u_2
M : Type u_4
S : Type u_5
inst : Semiring R
inst_1 : Semiring S
inst_2 : Module R S
s : Set M
⊢ Eq (α := Submodule R S[M]) (supported R S s)
    (Submodule.map (↑(LinearEquiv.symm (coeffLinearEquiv R)) : (M →₀ S) →ₗ[R] S[M]) (Finsupp.supported S R s))

Tactic:
Submodule.comap_equiv_eq_map_symm ..

Premises used: Submodule.comap_equiv_eq_map_symm, MonoidAlgebra.supported
-- Module: Mathlib.Algebra.MonoidAlgebra.Module
Goal:
R : Type u_2
M : Type u_4
inst : Semiring R
s : Set M
⊢ Eq (α := Submodule R R[M]) (supported R R s) (Submodule.span R ((fun (m : M) ↦ single m 1) '' s))

Tactic:
simp [supported_eq_map, Finsupp.supported_eq_span_single R s, Submodule.map_span,
    ← Set.image_comp, ofCoeff]

Premises used: MonoidAlgebra.ofCoeff, Finsupp.supported_eq_span_single, MonoidAlgebra.supported_eq_map, Set.image_comp, Submodule.map_span
-- Module: Mathlib.Algebra.MonoidAlgebra.Module
Goal:
R : Type u_2
M : Type u_4
S : Type u_5
inst : Semiring R
inst_1 : Semiring S
inst_2 : Module R S
s t : Set M
hst : s ⊆ t
⊢ LE.le (α := Submodule R S[M]) (supported R S s) (supported R S t)

Tactic:
fun _ h ↦ h.trans hst

Premises used: Set.Mem, setOf, HasSubset.Subset.trans, Set.Subset, Set.preimage
-- Module: Mathlib.Algebra.MonoidAlgebra.Module
Goal:
k : Type u₁
G : Type u₂
H : Type u_1
R : Type u_2
S_1 : Type u_3
M : Type u_4
S : Type u_5
inst : Semiring R
inst_1 : Semiring k
inst_2 : Module R k
inst_3 : IsTorsionFree R k
⊢ IsTorsionFree R k[G]

Tactic:
inferInstanceAs <| IsTorsionFree R (G →₀ k)

Premises used: _private.0.MonoidAlgebra.instIsTorsionFree._proof_1
-- Module: Mathlib.Algebra.MonoidAlgebra.Module
Goal:
k : Type u₁
G : Type u₂
H : Type u_1
R : Type u_2
S_1 : Type u_3
M : Type u_4
S : Type u_5
inst : Semiring k
inst_1 : SMulZeroClass R k
inst_2 : FaithfulSMul R k
inst_3 : Nonempty G
⊢ FaithfulSMul R k[G]

Tactic:
inferInstanceAs <| FaithfulSMul R (G →₀ k)

Premises used: _private.0.MonoidAlgebra.faithfulSMul._proof_1
-- Module: Mathlib.Algebra.MonoidAlgebra.Module
Goal:
R : Type u_2
k : Type u_6
inst : Semiring k
r : R
⊢ Eq (α := k[R]) ((basis R k : (a : R) → k[R]) r : k[R]) (single r 1 : k[R])

Tactic:
rfl

Premises used: rfl, Finsupp.single
-- Module: Mathlib.Algebra.MonoidAlgebra.Module
Goal:
k_1 : Type u₁
G : Type u₂
H : Type u_1
R : Type u_2
S : Type u_3
M : Type u_4
inst : Semiring k_1
inst_1 : Monoid R
inst_2 : DistribMulAction R k_1
a : G
k : R
m : k_1
⊢ ZeroHom.toFun (↑(singleAddHom a) : ZeroHom k_1 k_1[G]) (k • m) =
    HSMul.hSMul (α := R) (β := k_1[G]) ((MonoidHom.id R : (a : R) → R) k : R)
      (ZeroHom.toFun (↑(singleAddHom a) : ZeroHom k_1 k_1[G]) m)

Tactic:
simp
-- Module: Mathlib.Algebra.MonoidAlgebra.Module
Goal:
k : Type u₁
G : Type u₂
R : Type u_2
inst : Semiring k
N : Type u_5
inst_1 : Monoid R
inst_2 : AddMonoid N
inst_3 : DistribMulAction R N
inst_4 : DistribMulAction R k
f g : k[G] →+[R] N
h : ∀ (a : G), f.comp (singleDistribMulActionHom a) = g.comp (singleDistribMulActionHom a)
⊢ f = g

Tactic:
Finsupp.distribMulActionHom_ext' h

Premises used: Finsupp.distribMulActionHom_ext', MonoidAlgebra
-- Module: Mathlib.Algebra.MonoidAlgebra.Module
Goal:
k : Type u₁
G : Type u₂
R : Type u_2
inst : Semiring k
inst_1 : Semiring R
inst_2 : Module R k
a : G
b : k
⊢ Eq (α := k[G]) ((lsingle a : (a : k) → k[G]) b : k[G]) (single a b : k[G])

Tactic:
rfl

Premises used: rfl, Finsupp.single
-- Module: Mathlib.Algebra.MonoidAlgebra.Module
Goal:
k : Type u₁
G : Type u₂
R : Type u_2
inst : Semiring k
N : Type u_5
inst_1 : Semiring R
inst_2 : AddCommMonoid N
inst_3 : Module R N
inst_4 : Module R k
f g : k[G] →ₗ[R] N
H : ∀ (x : G), f ∘ₗ lsingle x = g ∘ₗ lsingle x
⊢ f = g

Tactic:
Finsupp.lhom_ext' H

Premises used: Finsupp.lhom_ext', MonoidAlgebra
-- Module: Mathlib.Algebra.MonoidAlgebra.Module
Goal:
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : MulOneClass M
m : M
r : R
⊢ HSMul.hSMul (β := R[M]) r ((of R M : (a : M) → R[M]) m : R[M]) = single m r

Tactic:
simp
-- Module: Mathlib.Algebra.MonoidAlgebra.Module
Goal:
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : MulOneClass M
s : Set M
m : M
inst_2 : Nontrivial R
⊢ Membership.mem (α := R[M]) (γ := Submodule R R[M]) (Submodule.span R ((⇑(of R M) : (a : M) → R[M]) '' s))
      ((of R M : (a : M) → R[M]) m : R[M]) ↔
    m ∈ s

Tactic:
single_mem_span_single _

Premises used: Set.Mem, setOf, MonoidAlgebra, Finsupp.single_mem_span_single, Finsupp.single
-- Module: Mathlib.Algebra.MonoidAlgebra.Module
Goal:
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : MulOneClass M
s : Set M
m : M
inst_2 : Nontrivial R
h :
  Membership.mem (α := R[M]) (γ := Submodule R R[M])
    (Submodule.span R (↑(Submonoid.closure ((⇑(of R M) : (a : M) → R[M]) '' s)) : Set R[M]))
    ((of R M : (a : M) → R[M]) m : R[M])
⊢ Membership.mem (α := R[M]) (γ := Submodule R R[M])
    (Submodule.span R (↑(Submonoid.map (F := M →* R[M]) (of R M) (Submonoid.closure s)) : Set R[M]))
    ((of R M : (a : M) → R[M]) m : R[M])

Tactic:
rw [← MonoidHom.map_mclosure] at h

Premises used: MonoidHom.map_mclosure
-- Module: Mathlib.Algebra.MonoidAlgebra.Module
Goal:
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : MulOneClass M
s : Set M
m : M
inst_2 : Nontrivial R
h :
  Membership.mem (α := R[M]) (γ := Submodule R R[M])
    (Submodule.span R (↑(Submonoid.map (F := M →* R[M]) (of R M) (Submonoid.closure s)) : Set R[M]))
    ((of R M : (a : M) → R[M]) m : R[M])
⊢ Membership.mem (γ := Submonoid M) (Submonoid.closure s) m

Tactic:
simpa using of_mem_span_of_iff.1 h

Premises used: MonoidAlgebra.of_mem_span_of_iff, Iff.mp
-- Module: Mathlib.Algebra.MonoidAlgebra.Module
Goal:
R : Type u_2
S : Type u_3
M : Type u_4
inst : Semiring R
inst_1 : Semiring S
inst_2 : MulOneClass M
f : S →+* R
g : M →* R
c : S
φ : S[M]
suffices :
  Eq (α := S[M] →+ R)
    (AddMonoidHom.comp (N := S[M]) (liftNC (↑f : S →+ R) (⇑g : (a : M) → R))
      ((smulAddHom S S[M] : (a : S) → S[M] →+ S[M]) c))
    (AddMonoidHom.comp (AddMonoidHom.mulLeft ((f : (a : S) → R) c)) (liftNC (↑f : S →+ R) (⇑g : (a : M) → R)))
⊢ (liftNC (↑f : S →+ R) (⇑g : (a : M) → R) : (a : S[M]) → R) (c • φ) =
    HMul.hMul (α := R) (β := R) ((f : (a : S) → R) c : R)
      ((liftNC (↑f : S →+ R) (⇑g : (a : M) → R) : (a : S[M]) → R) φ : R)

Tactic:
suffices (liftNC (↑f) g).comp (smulAddHom S S[M] c) =
      (AddMonoidHom.mulLeft (f c)).comp (liftNC (↑f) g) from
    DFunLike.congr_fun this φ