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
m : M
n : N
a : A
⊢ Eq (α := A[N][M]) ((curryAlgEquiv R : (a : A[M × N]) → A[N][M]) (single (m, n) a) : A[N][M])
    (single m (single n a) : A[N][M])

Tactic:
simp [curryAlgEquiv]

Premises used: MonoidAlgebra.curryAlgEquiv
-- 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]) ((AlgEquiv.symm (curryAlgEquiv R) : (a : A[N][M]) → A[M × N]) (single m (single n a)) : A[M × N])
    (single (m, n) a : A[M × N])

Tactic:
Finsupp.uncurry_single ..

Premises used: Finsupp.uncurry, Finsupp.uncurry_single, MonoidAlgebra
-- 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]) ((AlgEquiv.symm (curryAlgEquiv R) : (a : A[N][M]) → A[M × N]) (single m (single n a)) : A[M × N])
    (single (m, n) a : A[M × N])

Tactic:
exact Finsupp.uncurry_single ..

Premises used: Finsupp.uncurry_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
n : N
a : A
⊢ Eq (α := A[M × N]) ((AlgEquiv.symm (curryAlgEquiv R) : (a : A[N][M]) → A[M × N]) (single m (single n a)) : A[M × N])
    (single (m, n) a : A[M × N])

Tactic:
classical exact Finsupp.uncurry_single ..

Premises used: Finsupp.uncurry_single
-- Module: Mathlib.Algebra.MonoidAlgebra.Basic
Goal:
R : Type u_1
A : Type u_4
M : Type u_7
N : Type u_8
F : Type u_10
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Monoid M
inst_4 : Monoid N
inst_5 : FunLike F M N
inst_6 : MonoidHomClass F M N
f : F
r : R
⊢ Eq (α := A[N]) (mapDomain.{u_4, u_7, u_8} (M := M) (⇑f : (a : M) → N) ((algebraMap R A[M] : (a : R) → A[M]) r))
    ((algebraMap R A[N] : (a : R) → A[N]) r)

Tactic:
simp only [coe_algebraMap, mapDomain_single, map_one, (· ∘ ·)]

Premises used: MonoidAlgebra.coe_algebraMap, Function.comp, map_one, MonoidAlgebra.mapDomain_single
-- 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
f : A →ₐ[R] B
g : M →* B
h_comm : ∀ (x : A) (y : M), Commute.{u_5} (S := B) ((f : (a : A) → B) x : B) ((g : (a : 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: MonoidAlgebra.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 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : Monoid M
f : A →ₐ[R] B
g : M →* B
h_comm : ∀ (x : A) (y : M), Commute.{u_5} (S := B) ((f : (a : A) → B) x : B) ((g : (a : M) → B) y : B)
⊢ Eq (α := (a : A[M]) → B) (⇑(liftNCAlgHom f g h_comm) : (a : A[M]) → B)
    (⇑(liftNC (↑f : A →+ B) (⇑g : (a : M) → B)) : (a : A[M]) → B)

Tactic:
rfl

Premises used: Multiset.sum, Multiset.foldr, Finsupp.sum, MonoidAlgebra, 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 : Semiring A
inst_2 : Algebra R A
inst_3 : Monoid M
φ₁ φ₂ : R[M] →ₐ[R] A
h : ∀ (x : M), Eq.{u_4 + 1} (α := A) ((φ₁ : (a : R[M]) → A) (single x 1) : A) ((φ₂ : (a : R[M]) → A) (single x 1) : A)
⊢ φ₁ = φ₂

Tactic:
AlgHom.toLinearMap_injective <| lhom_ext' fun a ↦ LinearMap.ext_ring (h a)

Premises used: AlgHom.toLinearMap_injective, LinearMap.ext_ring, MonoidAlgebra.lhom_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
φ₁ φ₂ : R[M] →ₐ[R] A
h : Eq (α := 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, MonoidAlgebra.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 : 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
f : M →* A
h :
  ∀ (x : M),
    Eq.{u_4 + 1} (α := A)
      (((fun (f : R[M] →ₐ[R] A) ↦ (MonoidHom.comp (↑f : R[M] →* A) (of R M) : M →* A))
              ((fun (F : M →* A) ↦ (liftNCAlgHom (Algebra.ofId R A) F ⋯ : R[M] →ₐ[R] A)) f) :
            (a : M) → A)
          x :
        A)
      ((f : (a : M) → A) x : A)
⊢ (fun (f : R[M] →ₐ[R] A) ↦ (MonoidHom.comp (↑f : R[M] →* A) (of R M) : M →* A))
      ((fun (F : 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 : 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
f : M →* A
x : M
⊢ Eq.{u_4 + 1} (α := A)
    (((fun (f : R[M] →ₐ[R] A) ↦ (MonoidHom.comp (↑f : R[M] →* A) (of R M) : M →* A))
            ((fun (F : M →* A) ↦ (liftNCAlgHom (Algebra.ofId R A) F ⋯ : R[M] →ₐ[R] A)) f) :
          (a : M) → A)
        x :
      A)
    ((f : (a : M) → A) x : 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
F : R[M] →ₐ[R] A
h :
  ∀ (x : M),
    Eq.{u_4 + 1} (α := A)
      ((MonoidHom.comp
              (↑((fun (F : 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) : M →* A)) F)) :
                R[M] →* A)
              (of R M) :
            (a : M) → A)
          x :
        A)
      ((MonoidHom.comp (↑F : R[M] →* A) (of R M) : (a : M) → A) x : A)
⊢ (fun (F : 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) : 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 : 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
F : R[M] →ₐ[R] A
x : M
⊢ Eq.{u_4 + 1} (α := A)
    ((MonoidHom.comp
            (↑((fun (F : 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) : M →* A)) F)) :
              R[M] →* A)
            (of R M) :
          (a : M) → A)
        x :
      A)
    ((MonoidHom.comp (↑F : R[M] →* A) (of R M) : (a : M) → A) x : 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
F : M →* A
f : R[M]
⊢ Eq.{u_4 + 1} (α := A) ((((lift R A M : (a : 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 : M) → A) a : 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 : Semiring A
inst_2 : Algebra R A
inst_3 : Monoid M
F : M →* A
f : R[M]
⊢ Eq.{u_4 + 1} (α := A) ((((lift R A M : (a : 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 : M) → A) a : A) : A)

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

Premises used: MonoidAlgebra.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 : Semiring A
inst_2 : Algebra R A
inst_3 : Monoid M
F : M →* A
⊢ Eq (α := (a : R[M]) → A) (⇑((lift R A M : (a : M →* A) → R[M] →ₐ[R] A) F : R[M] →ₐ[R] A) : (a : R[M]) → A)
    (⇑(liftNC (↑(algebraMap R A) : R →+ A) (⇑F : (a : M) → A)) : (a : R[M]) → A)

Tactic:
rfl

Premises used: Multiset.sum, Multiset.foldr, Finsupp.sum, MonoidAlgebra, 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 : Semiring A
inst_2 : Algebra R A
inst_3 : Monoid M
F : R[M] →ₐ[R] A
m : M
⊢ Eq.{u_4 + 1} (α := A) ((((Equiv.symm (lift R A M) : (a : R[M] →ₐ[R] A) → M →* A) F : M →* A) : (a : M) → A) m : A)
    ((F : (a : R[M]) → A) (single m 1) : 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 : Semiring A
inst_2 : Algebra R A
inst_3 : Monoid M
F : M →* A
a : M
b : R
rw :
  (liftNC (↑(algebraMap R A) : R →+ A) (⇑F : (a : M) → A) : (a : R[M]) → A) (single a b) =
    HSMul.hSMul (β := A) b ((F : (a : M) → A) a : A)
rw₁ :
  HMul.hMul (α := A) (β := A) (((↑(algebraMap R A) : R →+ A) : (a : R) → A) b : A) ((F : (a : M) → A) a : A) =
    HSMul.hSMul (β := A) b ((F : (a : M) → A) a : A)
rw₂ :
  HMul.hMul (α := A) (β := A) (((↑(algebraMap R A) : R →+ A) : (a : R) → A) b : A) ((F : (a : M) → A) a : A) =
    HMul.hMul (α := A) (β := A) ((algebraMap R A : (a : R) → A) b : A) ((F : (a : M) → A) a : A)
rw₃ rw₄ :
  HMul.hMul (α := A) (β := A) ((algebraMap R A : (a : R) → A) b : A) ((F : (a : M) → A) a : A) =
    HMul.hMul (α := A) (β := A) ((algebraMap R A : (a : R) → A) b : A) ((F : (a : M) → A) a : A)
⊢ (((lift R A M : (a : M →* A) → R[M] →ₐ[R] A) F : R[M] →ₐ[R] A) : (a : R[M]) → A) (single a b) =
    HSMul.hSMul (β := A) b ((F : (a : M) → A) a : A)

Tactic:
rw [lift_def, liftNC_single, Algebra.smul_def, AddMonoidHom.coe_coe]

Premises used: AddMonoidHom.coe_coe, MonoidAlgebra.liftNC_single, Algebra.smul_def, MonoidAlgebra.lift_def
-- 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
F : M →* A
m : M
⊢ Eq.{u_4 + 1} (α := A)
    ((((lift R A M : (a : M →* A) → R[M] →ₐ[R] A) F : R[M] →ₐ[R] A) : (a : R[M]) → A)
        ((of R M : (a : M) → R[M]) m : R[M]) :
      A)
    ((F : (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
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Monoid M
F : R[M] →ₐ[R] A
⊢ F = (lift R A M : (a : 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, MonoidAlgebra.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 : Semiring A
inst_2 : Algebra R A
inst_3 : Monoid M
F : R[M] →ₐ[R] A
f : R[M]
rw :
  ((((lift R A M : (a : 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: MonoidAlgebra.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 : Semiring A
inst_2 : Algebra R A
inst_3 : Monoid M
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 : 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: MonoidAlgebra.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 : Semiring A
inst_2 : Algebra R A
inst_3 : Monoid M
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: MonoidAlgebra.lift_apply, MonoidAlgebra.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 : Semiring A
inst_2 : Algebra R A
inst_3 : Monoid M
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: MonoidAlgebra.lift_apply, MonoidAlgebra.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 : Semiring A
inst_2 : Algebra R A
inst_3 : Monoid M
inst_4 : CommSemiring S
inst_5 : Algebra S A
inst_6 : Algebra R S
inst_7 : IsScalarTower R S A
f : M →* A
⊢ Eq.{u_4 + 1} (α := A)
    ((((lift S A M : (a : 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 : M →* A) → R[M] →ₐ[R] A) f : R[M] →ₐ[R] A) : (a : R[M]) → A) 0 : A)

Tactic:
simp
-- 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 : Semiring A
inst_2 : Algebra R A
inst_3 : Monoid M
inst_4 : CommSemiring S
inst_5 : Algebra S A
inst_6 : Algebra R S
inst_7 : IsScalarTower R S A
f_1 : 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 : 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 : 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 : 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 : 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 : Semiring A
inst_2 : Algebra R A
inst_3 : Monoid M
inst_4 : CommSemiring S
inst_5 : Algebra S A
inst_6 : Algebra R S
inst_7 : IsScalarTower R S A
f : M →* A
x : R[M]
zero :
  Eq.{u_4 + 1} (α := A)
    ((((lift S A M : (a : 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 : 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 : 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 : 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 : 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 : 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 : 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 : 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: MonoidAlgebra.single_add
-- 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
f : M →* N
⊢ ∀ (r : R),
    Eq (α := A[N])
      (OneHom.toFun (↑(↑(mapDomainRingHom A f) : A[M] →* A[N]) : OneHom A[M] A[N])
        ((algebraMap R A[M] : (a : R) → A[M]) r))
      ((algebraMap R A[N] : (a : R) → A[N]) r)

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 :
  ∀ (x : A[M]) (m : M),
    Eq.{u_4 + 1} (α := A) ((((mapDomainAlgHom R A (MonoidHom.id M) : (a : A[M]) → A[M]) x : A[M]) : (a : M) → A) m : A)
      ((((AlgHom.id R A[M] : (a : A[M]) → A[M]) x : A[M]) : (a : M) → A) m : A)
⊢ Eq (α := A[M] →ₐ[R] A[M]) (mapDomainAlgHom R A (MonoidHom.id M)) (AlgHom.id R A[M])

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
x : A[M]
m : M
⊢ Eq.{u_4 + 1} (α := A) ((((mapDomainAlgHom R A (MonoidHom.id M) : (a : A[M]) → A[M]) x : A[M]) : (a : M) → A) m : A)
    ((((AlgHom.id R A[M] : (a : A[M]) → A[M]) x : A[M]) : (a : M) → A) m : A)

Tactic:
simp [MonoidHom.id, ← Function.id_def]

Premises used: Function.id_def, MonoidHom.id
-- 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
f : M →* N
g : N →* O
H :
  ∀ (x : A[M]) (m : O),
    Eq.{u_4 + 1} (α := A) ((((mapDomainAlgHom R A (g.comp f) : (a : A[M]) → A[O]) x : A[O]) : (a : O) → A) m : A)
      ((((AlgHom.comp (mapDomainAlgHom R A g) (mapDomainAlgHom R A f) : (a : A[M]) → A[O]) x : A[O]) : (a : O) → A) m :
        A)
⊢ Eq (α := A[M] →ₐ[R] A[O]) (mapDomainAlgHom R A (g.comp f))
    (AlgHom.comp (mapDomainAlgHom R A g) (mapDomainAlgHom R A 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
f : M →* N
g : N →* O
x : A[M]
m : O
⊢ Eq.{u_4 + 1} (α := A) ((((mapDomainAlgHom R A (g.comp f) : (a : A[M]) → A[O]) x : A[O]) : (a : O) → A) m : A)
    ((((AlgHom.comp (mapDomainAlgHom R A g) (mapDomainAlgHom R A f) : (a : A[M]) → A[O]) x : A[O]) : (a : O) → A) m : A)

Tactic:
simp [mapDomain_comp]

Premises used: Finsupp.mapDomain_comp
-- 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
e : M ≃* N
x : R
hfg :
  ∀ (m : N),
    Eq.{u_4 + 1} (α := A)
      ((Equiv.toFun (RingEquiv.toEquiv (mapDomainRingEquiv A e)) ((algebraMap R A[M] : (a : R) → A[M]) x) : (a : N) → A)
          m :
        A)
      ((((algebraMap R A[N] : (a : R) → A[N]) x : A[N]) : (a : N) → A) m : A)
⊢ Eq (α := A[N]) (Equiv.toFun (RingEquiv.toEquiv (mapDomainRingEquiv A e)) ((algebraMap R A[M] : (a : R) → A[M]) x))
    ((algebraMap R A[N] : (a : R) → A[N]) x)

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 : 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
e : M ≃* N
x : R
m : N
⊢ Eq.{u_4 + 1} (α := A)
    ((Equiv.toFun (RingEquiv.toEquiv (mapDomainRingEquiv A e)) ((algebraMap R A[M] : (a : R) → A[M]) x) : (a : N) → A)
        m :
      A)
    ((((algebraMap 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
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
x : A[M]
n : N
⊢ Eq.{u_4 + 1} (α := A) ((((domCongr R A e : (a : A[M]) → A[N]) x : A[N]) : (a : N) → A) n : A)
    ((x : (a : M) → A) ((e.symm : (a : N) → M) n : M) : A)

Tactic:
simp [domCongr]

Premises used: MonoidAlgebra.domCongr
-- 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[M] →ₐ[R] A[N]) (↑(domCongr R A e) : A[M] →ₐ[R] A[N]) (mapDomainAlgHom R A (↑e : M →* N))

Tactic:
rfl

Premises used: Multiset.sum, Multiset.foldr, AlgEquiv.toAlgHom, Finsupp.mapDomain, Finsupp.sum, MonoidAlgebra.mapDomainRingHom, MonoidAlgebra.mapDomainAlgHom, 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
e : M ≃* N
f : A[M]
h :
  ∀ (a : N),
    Membership.mem (γ := Finset N) (support.{u_8, u_4} (M := A) ((domCongr R A e : (a : A[M]) → A[N]) f)) a ↔
      a ∈ Finset.map (↑e : M ≃ N).toEmbedding f.support
⊢ support.{u_8, u_4} (M := A) ((domCongr R A e : (a : A[M]) → A[N]) f) = Finset.map (↑e : M ≃ N).toEmbedding f.support

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
f : A[M]
a : N
⊢ Membership.mem (γ := Finset N) (support.{u_8, u_4} (M := A) ((domCongr R A e : (a : A[M]) → A[N]) f)) a ↔
    a ∈ Finset.map (↑e : M ≃ N).toEmbedding f.support

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
m : M
a : A
⊢ Eq (α := A[N]) ((domCongr R A e : (a : A[M]) → A[N]) (single m a) : A[N]) (single ((e : (a : M) → N) m) a : A[N])

Tactic:
simp [domCongr]

Premises used: MonoidAlgebra.domCongr