awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : Monoid M
inst_2 : Monoid N
f : R[M × N] →+ R[N][M] := AddEquiv.toAddMonoidHom curryAddEquiv
this :
  ∀ {mn : M × N} {r : R},
    Eq (α := R[N][M]) ((f : (a : R[M × N]) → R[N][M]) (single mn r) : R[N][M]) (single mn.1 (single mn.2 r) : R[N][M])
refine : AddMonoidHom.compr₂ AddMonoidHom.mul f = (AddMonoidHom.comp AddMonoidHom.mul f).compl₂ f
⊢ ∀ (x y : R[M × N]),
    Equiv.toFun (AddEquiv.toEquiv curryAddEquiv) (x * y) =
      HMul.hMul (α := R[N][M]) (β := R[N][M]) (Equiv.toFun (AddEquiv.toEquiv curryAddEquiv) x : R[N][M])
        (Equiv.toFun (AddEquiv.toEquiv curryAddEquiv) y)

Tactic:
refine f.map_mul_iff.2 ?_

Premises used: Iff.mpr, AddMonoidHom.map_mul_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 : Monoid M
inst_2 : Monoid N
f : R[M × N] →+ R[N][M] := AddEquiv.toAddMonoidHom curryAddEquiv
this :
  ∀ {mn : M × N} {r : R},
    Eq (α := R[N][M]) ((f : (a : R[M × N]) → R[N][M]) (single mn r) : R[N][M]) (single mn.1 (single mn.2 r) : R[N][M])
hfg :
  ∀ (m₁ : M) (n₁ : N) (r₁ : R) (m₂ : M) (n₂ : N) (r₂ : R) (m : M) (m_1 : N),
    Eq.{u_1 + 1} (α := R)
      ((((((AddMonoidHom.comp
                          (((AddMonoidHom.compr₂ AddMonoidHom.mul f).comp (singleAddHom (m₁, n₁)) :
                              (a : R) → R[M × N] →+ R[N][M])
                            r₁)
                          (singleAddHom (m₂, n₂)) :
                        (a : R) → R[N][M])
                      r₂ :
                    R[N][M]) :
                  (a : M) → R[N])
                m :
              R[N]) :
            (a : N) → R)
          m_1 :
        R)
      ((((((AddMonoidHom.comp
                          ((((AddMonoidHom.comp AddMonoidHom.mul f).compl₂ f).comp (singleAddHom (m₁, n₁)) :
                              (a : R) → R[M × N] →+ R[N][M])
                            r₁)
                          (singleAddHom (m₂, n₂)) :
                        (a : R) → R[N][M])
                      r₂ :
                    R[N][M]) :
                  (a : M) → R[N])
                m :
              R[N]) :
            (a : N) → R)
          m_1 :
        R)
⊢ AddMonoidHom.compr₂ AddMonoidHom.mul f = (AddMonoidHom.comp AddMonoidHom.mul f).compl₂ f

Tactic:
ext ⟨m₁, n₁⟩ r₁ ⟨m₂, n₂⟩ r₂
-- 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₁_1 r₂_1 : R
m m' m₁_1 m₂_1 : M
inst_1 : Monoid M
inst_2 : Monoid N
f : R[M × N] →+ R[N][M] := AddEquiv.toAddMonoidHom curryAddEquiv
this :
  ∀ {mn : M × N} {r : R},
    Eq (α := R[N][M]) ((f : (a : R[M × N]) → R[N][M]) (single mn r) : R[N][M]) (single mn.1 (single mn.2 r) : R[N][M])
m₁ : M
n₁ : N
r₁ : R
m₂ : M
n₂ : N
r₂ : R
m_1 : M
m_2 : N
⊢ Eq.{u_1 + 1} (α := R)
    ((((((AddMonoidHom.comp
                        (((AddMonoidHom.compr₂ AddMonoidHom.mul f).comp (singleAddHom (m₁, n₁)) :
                            (a : R) → R[M × N] →+ R[N][M])
                          r₁)
                        (singleAddHom (m₂, n₂)) :
                      (a : R) → R[N][M])
                    r₂ :
                  R[N][M]) :
                (a : M) → R[N])
              m_1 :
            R[N]) :
          (a : N) → R)
        m_2 :
      R)
    ((((((AddMonoidHom.comp
                        ((((AddMonoidHom.comp AddMonoidHom.mul f).compl₂ f).comp (singleAddHom (m₁, n₁)) :
                            (a : R) → R[M × N] →+ R[N][M])
                          r₁)
                        (singleAddHom (m₂, n₂)) :
                      (a : R) → R[N][M])
                    r₂ :
                  R[N][M]) :
                (a : M) → R[N])
              m_1 :
            R[N]) :
          (a : N) → R)
        m_2 :
      R)

Tactic:
simp [this]
-- Module: Mathlib.Algebra.MonoidAlgebra.Defs
Goal:
R : Type u_1
M : Type u_4
N : Type u_5
inst : Semiring R
inst_1 : Monoid M
inst_2 : Monoid N
m : M
n : N
r : R
⊢ Eq (α := R[N][M]) ((curryRingEquiv : (a : R[M × N]) → R[N][M]) (single (m, n) r) : R[N][M])
    (single m (single n r) : R[N][M])

Tactic:
Finsupp.curry_single ..

Premises used: Finsupp.curry_single, Finsupp.curry, MonoidAlgebra
-- Module: Mathlib.Algebra.MonoidAlgebra.Defs
Goal:
R : Type u_1
M : Type u_4
N : Type u_5
inst : Semiring R
inst_1 : Monoid M
inst_2 : Monoid N
m : M
n : N
r : R
⊢ Eq (α := R[N][M]) ((curryRingEquiv : (a : R[M × N]) → R[N][M]) (single (m, n) r) : R[N][M])
    (single m (single n r) : R[N][M])

Tactic:
exact Finsupp.curry_single ..

Premises used: Finsupp.curry_single
-- Module: Mathlib.Algebra.MonoidAlgebra.Defs
Goal:
R : Type u_1
M : Type u_4
N : Type u_5
inst : Semiring R
inst_1 : Monoid M
inst_2 : Monoid N
m : M
n : N
r : R
⊢ Eq (α := R[N][M]) ((curryRingEquiv : (a : R[M × N]) → R[N][M]) (single (m, n) r) : R[N][M])
    (single m (single n r) : R[N][M])

Tactic:
classical exact Finsupp.curry_single ..

Premises used: Finsupp.curry_single
-- Module: Mathlib.Algebra.MonoidAlgebra.Defs
Goal:
R : Type u_1
M : Type u_4
N : Type u_5
inst : Semiring R
inst_1 : Monoid M
inst_2 : Monoid N
m : M
n : N
r : R
⊢ Eq (α := R[M × N]) ((RingEquiv.symm curryRingEquiv : (a : R[N][M]) → R[M × N]) (single m (single n r)) : R[M × N])
    (single (m, n) r : R[M × N])

Tactic:
Finsupp.uncurry_single ..

Premises used: Finsupp.uncurry, Finsupp.uncurry_single, MonoidAlgebra
-- Module: Mathlib.Algebra.MonoidAlgebra.Defs
Goal:
R : Type u_1
M : Type u_4
N : Type u_5
inst : Semiring R
inst_1 : Monoid M
inst_2 : Monoid N
m : M
n : N
r : R
⊢ Eq (α := R[M × N]) ((RingEquiv.symm curryRingEquiv : (a : R[N][M]) → R[M × N]) (single m (single n r)) : R[M × N])
    (single (m, n) r : R[M × N])

Tactic:
exact Finsupp.uncurry_single ..

Premises used: Finsupp.uncurry_single
-- Module: Mathlib.Algebra.MonoidAlgebra.Defs
Goal:
R : Type u_1
M : Type u_4
N : Type u_5
inst : Semiring R
inst_1 : Monoid M
inst_2 : Monoid N
m : M
n : N
r : R
⊢ Eq (α := R[M × N]) ((RingEquiv.symm curryRingEquiv : (a : R[N][M]) → R[M × N]) (single m (single n r)) : R[M × N])
    (single (m, n) r : R[M × N])

Tactic:
classical exact Finsupp.uncurry_single ..

Premises used: Finsupp.uncurry_single
-- Module: Mathlib.Algebra.MonoidAlgebra.Defs
Goal:
R : Type u_1
G : Type u_3
inst : Semiring R
inst_1 : Group G
x : R[G]
r : R
g h : G
⊢ ∀ m' ∈ x.support, m' * g = h ↔ m' = h * g⁻¹

Tactic:
simp [eq_mul_inv_iff_mul_eq]

Premises used: eq_mul_inv_iff_mul_eq
-- Module: Mathlib.Algebra.MonoidAlgebra.Defs
Goal:
R : Type u_1
G : Type u_3
inst : Semiring R
inst_1 : Group G
x : R[G]
r : R
g h : G
⊢ ∀ m' ∈ x.support, g * m' = h ↔ m' = g⁻¹ * h

Tactic:
simp [eq_inv_mul_iff_mul_eq]

Premises used: eq_inv_mul_iff_mul_eq
-- Module: Mathlib.Algebra.MonoidAlgebra.Defs
Goal:
R : Type u_1
G : Type u_3
inst : Semiring R
inst_1 : Group G
x y : R[G]
g : G
rw :
  Eq (α := R) (sum x fun (m₁ : G) (r₁ : R) ↦ sum y fun (m₂ : G) (r₂ : R) ↦ if m₁ * m₂ = g then r₁ * r₂ else 0)
    (sum x fun (h : G) (r : R) ↦ HMul.hMul (β := R) r ((y : (a : G) → R) (h⁻¹ * g) : R))
⊢ Eq (α := R) ((x * y : (a : G) → R) g : R)
    (sum x fun (h : G) (r : R) ↦ HMul.hMul (β := R) r ((y : (a : G) → R) (h⁻¹ * g) : R) : R)

Tactic:
rw [mul_apply]

Premises used: MonoidAlgebra.mul_apply
-- Module: Mathlib.Algebra.MonoidAlgebra.Defs
Goal:
R : Type u_1
G : Type u_3
inst : Semiring R
inst_1 : Group G
x y : R[G]
g : G
a :
  ∀ x_1 ∈ x.support,
    (∑ a ∈ y.support,
        if x_1 * a = g then HMul.hMul (α := R) (β := R) ((x : (a : G) → R) x_1 : R) ((y : (a : G) → R) a : R) else 0) =
      HMul.hMul (α := R) (β := R) ((x : (a : G) → R) x_1 : R) ((y : (a : G) → R) (x_1⁻¹ * g) : R)
⊢ Eq.{u_1 + 1} (α := R)
    (∑ a ∈ x.support,
      ∑ a_1 ∈ y.support,
        if a * a_1 = g then HMul.hMul (α := R) (β := R) ((x : (a : G) → R) a : R) ((y : (a : G) → R) a_1 : R) else 0)
    (∑ a ∈ x.support, HMul.hMul (α := R) (β := R) ((x : (a : G) → R) a : R) ((y : (a : G) → R) (a⁻¹ * g) : R))

Tactic:
congr! 1
-- Module: Mathlib.Algebra.MonoidAlgebra.Defs
Goal:
R : Type u_1
G : Type u_3
inst : Semiring R
inst_1 : Group G
x y : R[G]
g x_1 : G
h : x_1 ∈ x.support
⊢ (∑ a ∈ y.support,
      if x_1 * a = g then HMul.hMul (α := R) (β := R) ((x : (a : G) → R) x_1 : R) ((y : (a : G) → R) a : R) else 0) =
    HMul.hMul (α := R) (β := R) ((x : (a : G) → R) x_1 : R) ((y : (a : G) → R) (x_1⁻¹ * g) : R)

Tactic:
simp +contextual [← eq_inv_mul_iff_mul_eq]

Premises used: eq_inv_mul_iff_mul_eq
-- Module: Mathlib.Algebra.MonoidAlgebra.Defs
Goal:
R : Type u_1
G : Type u_3
inst : Semiring R
inst_1 : Group G
x y : R[G]
g : G
rw rw₁ rw₂ :
  Eq (α := R) (sum x fun (m₁ : G) (r₁ : R) ↦ sum y fun (m₂ : G) (r₂ : R) ↦ if m₁ * m₂ = g then r₁ * r₂ else 0)
    (sum x fun (h : G) (r : R) ↦ HMul.hMul (β := R) r ((y : (a : G) → R) (h⁻¹ * g) : R))
rw₃ :
  Eq.{u_1 + 1} (α := R)
    (∑ a ∈ x.support,
      ∑ a_1 ∈ y.support,
        if a * a_1 = g then HMul.hMul (α := R) (β := R) ((x : (a : G) → R) a : R) ((y : (a : G) → R) a_1 : R) else 0)
    (∑ a ∈ x.support, HMul.hMul (α := R) (β := R) ((x : (a : G) → R) a : R) ((y : (a : G) → R) (a⁻¹ * g) : R))
a :
  ∀ x_1 ∈ x.support,
    (∑ a ∈ y.support,
        if x_1 * a = g then HMul.hMul (α := R) (β := R) ((x : (a : G) → R) x_1 : R) ((y : (a : G) → R) a : R) else 0) =
      HMul.hMul (α := R) (β := R) ((x : (a : G) → R) x_1 : R) ((y : (a : G) → R) (x_1⁻¹ * g) : R)
⊢ Eq (α := R) ((x * y : (a : G) → R) g : R)
    (sum x fun (h : G) (r : R) ↦ HMul.hMul (β := R) r ((y : (a : G) → R) (h⁻¹ * g) : R) : R)

Tactic:
classical
  rw [mul_apply]
  dsimp [Finsupp.sum]
  congr! 1
  simp +contextual [← eq_inv_mul_iff_mul_eq]

Premises used: Finsupp.sum, eq_inv_mul_iff_mul_eq, MonoidAlgebra.mul_apply
-- Module: Mathlib.Algebra.MonoidAlgebra.Defs
Goal:
R : Type u_1
G : Type u_3
inst : Semiring R
inst_1 : Group G
x y : R[G]
g : G
rw :
  Eq (α := R) (sum y fun (x' : G) (v' : R) ↦ sum x fun (x : G) (v : R) ↦ if x * x' = g then v * v' else 0)
    (sum y fun (h : G) (r : R) ↦ HMul.hMul (α := R) ((x : (a : G) → R) (g * h⁻¹) : R) r)
⊢ Eq (α := R) ((x * y : (a : G) → R) g : R)
    (sum y fun (h : G) (r : R) ↦ HMul.hMul (α := R) ((x : (a : G) → R) (g * h⁻¹) : R) r : R)

Tactic:
rw [mul_apply, Finsupp.sum_comm]

Premises used: Finsupp.sum_comm, MonoidAlgebra.mul_apply
-- Module: Mathlib.Algebra.MonoidAlgebra.Defs
Goal:
R : Type u_1
G : Type u_3
inst : Semiring R
inst_1 : Group G
x y : R[G]
g : G
a :
  ∀ x_1 ∈ y.support,
    (∑ a ∈ x.support,
        if a * x_1 = g then HMul.hMul (α := R) (β := R) ((x : (a : G) → R) a : R) ((y : (a : G) → R) x_1 : R) else 0) =
      HMul.hMul (α := R) (β := R) ((x : (a : G) → R) (g * x_1⁻¹) : R) ((y : (a : G) → R) x_1 : R)
⊢ Eq.{u_1 + 1} (α := R)
    (∑ a ∈ y.support,
      ∑ a_1 ∈ x.support,
        if a_1 * a = g then HMul.hMul (α := R) (β := R) ((x : (a : G) → R) a_1 : R) ((y : (a : G) → R) a : R) else 0)
    (∑ a ∈ y.support, HMul.hMul (α := R) (β := R) ((x : (a : G) → R) (g * a⁻¹) : R) ((y : (a : G) → R) a : R))

Tactic:
congr! 1
-- Module: Mathlib.Algebra.MonoidAlgebra.Defs
Goal:
R : Type u_1
G : Type u_3
inst : Semiring R
inst_1 : Group G
x y : R[G]
g x_1 : G
h : x_1 ∈ y.support
⊢ (∑ a ∈ x.support,
      if a * x_1 = g then HMul.hMul (α := R) (β := R) ((x : (a : G) → R) a : R) ((y : (a : G) → R) x_1 : R) else 0) =
    HMul.hMul (α := R) (β := R) ((x : (a : G) → R) (g * x_1⁻¹) : R) ((y : (a : G) → R) x_1 : R)

Tactic:
simp +contextual [← eq_mul_inv_iff_mul_eq]

Premises used: eq_mul_inv_iff_mul_eq
-- Module: Mathlib.Algebra.MonoidAlgebra.Defs
Goal:
R : Type u_1
G : Type u_3
inst : Semiring R
inst_1 : Group G
x y : R[G]
g : G
rw :
  Eq (α := R) (sum x fun (m₁ : G) (r₁ : R) ↦ sum y fun (m₂ : G) (r₂ : R) ↦ if m₁ * m₂ = g then r₁ * r₂ else 0)
    (sum y fun (h : G) (r : R) ↦ HMul.hMul (α := R) ((x : (a : G) → R) (g * h⁻¹) : R) r)
rw₁ rw₂ rw₃ :
  Eq (α := R) (sum y fun (x' : G) (v' : R) ↦ sum x fun (x : G) (v : R) ↦ if x * x' = g then v * v' else 0)
    (sum y fun (h : G) (r : R) ↦ HMul.hMul (α := R) ((x : (a : G) → R) (g * h⁻¹) : R) r)
rw₄ :
  Eq.{u_1 + 1} (α := R)
    (∑ a ∈ y.support,
      ∑ a_1 ∈ x.support,
        if a_1 * a = g then HMul.hMul (α := R) (β := R) ((x : (a : G) → R) a_1 : R) ((y : (a : G) → R) a : R) else 0)
    (∑ a ∈ y.support, HMul.hMul (α := R) (β := R) ((x : (a : G) → R) (g * a⁻¹) : R) ((y : (a : G) → R) a : R))
a :
  ∀ x_1 ∈ y.support,
    (∑ a ∈ x.support,
        if a * x_1 = g then HMul.hMul (α := R) (β := R) ((x : (a : G) → R) a : R) ((y : (a : G) → R) x_1 : R) else 0) =
      HMul.hMul (α := R) (β := R) ((x : (a : G) → R) (g * x_1⁻¹) : R) ((y : (a : G) → R) x_1 : R)
⊢ Eq (α := R) ((x * y : (a : G) → R) g : R)
    (sum y fun (h : G) (r : R) ↦ HMul.hMul (α := R) ((x : (a : G) → R) (g * h⁻¹) : R) r : R)

Tactic:
classical
  rw [mul_apply, Finsupp.sum_comm]
  dsimp [Finsupp.sum]
  congr! 1
  simp +contextual [← eq_mul_inv_iff_mul_eq]

Premises used: Finsupp.sum_comm, Finsupp.sum, eq_mul_inv_iff_mul_eq, MonoidAlgebra.mul_apply
-- 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 : CommSemiring R
inst_1 : CommSemigroup M
f g : R[M]
⊢ f * g = g * f

Tactic:
simp [mul_def, Finsupp.sum, mul_comm, f.support.sum_comm]

Premises used: MonoidAlgebra.mul_def, Finsupp.sum, mul_comm, Finset.sum_comm
-- Module: Mathlib.Algebra.MonoidAlgebra.Defs
Goal:
R : Type u_1
M : Type u_4
inst : CommSemiring R
inst_1 : MulOneClass M
r : R
f : R[M]
⊢ single 1 r * f = f * single 1 r

Tactic:
single_commute .one_left (.all _) f

Premises used: SemiconjBy, Commute, MonoidAlgebra.single_commute, Commute.one_left
-- Module: Mathlib.Algebra.MonoidAlgebra.Defs
Goal:
R : Type u_1
M : Type u_4
ι : Type u_7
inst : CommSemiring R
inst_1 : CommMonoid M
s_1 : Finset ι
m : ι → M
r : ι → R
i : ι
s : Finset ι
hi : i ∉ s
ih : Eq (α := R[M]) (∏ i ∈ s, single (m i) (r i)) (single (∏ i ∈ s, m i) (∏ i ∈ s, r i))
rw :
  HMul.hMul (α := R[M]) (single (m i) (r i)) (∏ x ∈ s, single (m x) (r x)) =
    single (∏ i ∈ cons i s hi, m i) (∏ i ∈ cons i s hi, r i)
rw₁ :
  HMul.hMul (α := R[M]) (single (m i) (r i)) (single (∏ i ∈ s, m i) (∏ i ∈ s, r i)) =
    single (∏ i ∈ cons i s hi, m i) (∏ i ∈ cons i s hi, r i)
rw₂ :
  Eq (α := R[M]) (single (m i * ∏ i ∈ s, m i) (r i * ∏ i ∈ s, r i))
    (single (∏ i ∈ cons i s hi, m i) (∏ i ∈ cons i s hi, r i))
rw₃ :
  Eq (α := R[M]) (single (m i * ∏ i ∈ s, m i) (r i * ∏ i ∈ s, r i))
    (single (m i * ∏ x ∈ s, m x) (∏ i ∈ cons i s hi, r i))
rw₄ rw₅ :
  Eq (α := R[M]) (single (m i * ∏ i ∈ s, m i) (r i * ∏ i ∈ s, r i)) (single (m i * ∏ x ∈ s, m x) (r i * ∏ x ∈ s, r x))
⊢ Eq (α := R[M]) (∏ i ∈ cons i s hi, single (m i) (r i)) (single (∏ i ∈ cons i s hi, m i) (∏ i ∈ cons i s hi, r i))

Tactic:
rw [prod_cons, ih, single_mul_single, prod_cons, prod_cons]

Premises used: MonoidAlgebra.single_mul_single, Finset.prod_cons
-- Module: Mathlib.Algebra.MonoidAlgebra.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Ring R
x : R[M]
⊢ (-x).coeff = -x.coeff

Tactic:
rfl

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

Tactic:
rfl

Premises used: MonoidAlgebra.ofCoeff, rfl
-- Module: Mathlib.Algebra.MonoidAlgebra.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Ring 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 : Ring 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
inst : Ring R
m : M
x : R[M]
⊢ Eq.{u_1 + 1} (α := R) ((-x : (a : M) → R) m : R) (-(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 : Ring R
m : M
r : R
⊢ Eq (α := R[M]) (single m (-r)) (-single m r)

Tactic:
Finsupp.single_neg m r

Premises used: MonoidAlgebra, Finsupp.single_neg
-- 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 : Ring R
inst_1 : MulOneClass M
n : ℕ
⊢ Eq (α := R[M]) (single 1 (↑(↑n : ℤ) : R)) (↑n : R[M])

Tactic:
simp [natCast_def]

Premises used: MonoidAlgebra.natCast_def
-- 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 : Ring R
inst_1 : MulOneClass M
n : ℕ
⊢ Eq (α := R[M]) (single 1 (↑(Int.negSucc n) : R)) (-(↑(n + 1) : R[M]))

Tactic:
simp [natCast_def, one_def]

Premises used: MonoidAlgebra.one_def, MonoidAlgebra.natCast_def
-- Module: Mathlib.Algebra.MonoidAlgebra.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Ring R
inst_1 : MulOneClass M
z : ℤ
⊢ Eq (α := R[M]) (↑z : R[M]) (single 1 (↑z : R))

Tactic:
rfl

Premises used: rfl, Finsupp.single
-- Module: Mathlib.Algebra.MonoidAlgebra.Defs
Goal:
R_1 : Type u_1
S : Type u_2
G : Type u_3
M_1 : Type u_4
N : Type u_5
O : Type u_6
ι : Type u_7
inst : Semiring R_1
R : Type u_8
M : Type u_9
inst_1 : Semiring R
inst_2 : Add M
⊢ ∀ (x y : Multiplicative M),
    single ((Multiplicative.toAdd : (a : Multiplicative M) → M) (x * y)) 1 =
      HMul.hMul (α := R[M]) (β := R[M]) (single ((Multiplicative.toAdd : (a : Multiplicative M) → M) x) 1 : R[M])
        (single ((Multiplicative.toAdd : (a : Multiplicative M) → M) y) 1 : R[M])

Tactic:
simp
-- Module: Mathlib.Algebra.MonoidAlgebra.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddZeroClass M
a : Multiplicative M
⊢ Eq (α := R[M]) ((of R M : (a : Multiplicative M) → R[M]) a : R[M])
    (single ((Multiplicative.toAdd : (a : Multiplicative M) → M) a) 1 : R[M])

Tactic:
rfl

Premises used: rfl, Finsupp.single
-- Module: Mathlib.Algebra.MonoidAlgebra.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
a : M
⊢ Eq (α := R[M]) (of' R M a) (single a 1)

Tactic:
rfl

Premises used: AddMonoidAlgebra.of', rfl, Finsupp.single
-- Module: Mathlib.Algebra.MonoidAlgebra.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddZeroClass M
a : M
⊢ Eq (α := R[M]) (of' R M a)
    ((of R M : (a : Multiplicative M) → R[M]) ((Multiplicative.ofAdd : (a : M) → Multiplicative M) a))

Tactic:
rfl

Premises used: AddMonoidAlgebra.of', rfl, Finsupp.single
-- Module: Mathlib.Algebra.MonoidAlgebra.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : Nontrivial R
inst_2 : AddZeroClass M
⊢ Function.Injective (α := Multiplicative M) (β := R[M]) (⇑(of R M) : (a : Multiplicative M) → R[M])

Tactic:
MonoidAlgebra.of_injective

Premises used: Multiplicative, MonoidAlgebra.of_injective, AddMonoidAlgebra, Finsupp.single
-- Module: Mathlib.Algebra.MonoidAlgebra.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddZeroClass M
a : M
h : ∀ (a' : M), AddCommute a a'
f : R[M]
⊢ Commute (of' R M a) f

Tactic:
single_commute h .one_left f

Premises used: AddMonoidAlgebra.of', AddMonoidAlgebra.single_commute, Finsupp.single
-- Module: Mathlib.Algebra.MonoidAlgebra.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddMonoid M
p : R[M] → Prop
x : R[M]
hM : ∀ (m : M), p ((of R M : (a : Multiplicative M) → R[M]) ((Multiplicative.ofAdd : (a : M) → Multiplicative M) m))
hadd : ∀ (x y : R[M]), p x → p y → p (x + y)
hsmul : ∀ (r : R) (x : R[M]), p x → p (r • x)
⊢ p 0

Tactic:
simpa using hsmul 0 (of R M 1) (hM 0)

Premises used: AddMonoidAlgebra.of, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.Algebra.MonoidAlgebra.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddMonoid M
p : R[M] → Prop
x : R[M]
hM : ∀ (m : M), p ((of R M : (a : Multiplicative M) → R[M]) ((Multiplicative.ofAdd : (a : M) → Multiplicative M) m))
hadd : ∀ (x y : R[M]), p x → p y → p (x + y)
hsmul : ∀ (r : R) (x : R[M]), p x → p (r • x)
m : M
r : R
⊢ p (Finsupp.single m r)

Tactic:
simpa using hsmul r (of R M m) (hM m)

Premises used: AddMonoidAlgebra.of, DFunLike.coe
-- Module: Mathlib.Algebra.MonoidAlgebra.Defs
Goal:
R : Type u_1
S : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddMonoid M
f g : R[M] →+* S
h₁ : f.comp singleZeroRingHom = g.comp singleZeroRingHom
h_of :
  Eq (α := MonoidHom.{u_4, u_2} (Multiplicative M) S) (MonoidHom.comp (↑f : R[M] →* S) (of R M))
    (MonoidHom.comp (↑g : R[M] →* S) (of R M))
⊢ f = g

Tactic:
ringHom_ext (RingHom.congr_fun h₁) (DFunLike.congr_fun h_of)

Premises used: DFunLike.congr_fun, RingHom.congr_fun, AddMonoidAlgebra.ringHom_ext
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : SemilatticeSup B
inst_1 : OrderBot B
inst_2 : Semiring R
degb : A → B
f g : R[A]
⊢ (f + g).support.sup degb ≤ f.support.sup degb ⊔ g.support.sup degb

Tactic:
(Finset.sup_mono Finsupp.support_add).trans_eq Finset.sup_union

Premises used: LE.le.trans_eq, Finset.sup_union, Finsupp.support_add, Finset.sup_mono
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : SemilatticeSup B
inst_1 : OrderBot B
inst_2 : Semiring R
degb : A → B
f g : R[A]
⊢ (f + g).support.sup degb ≤ f.support.sup degb ⊔ g.support.sup degb

Tactic:
exact (Finset.sup_mono Finsupp.support_add).trans_eq Finset.sup_union

Premises used: LE.le.trans_eq, Finset.sup_union, Finsupp.support_add, Finset.sup_mono
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : SemilatticeSup B
inst_1 : OrderBot B
inst_2 : Semiring R
degb : A → B
f g : R[A]
⊢ (f + g).support.sup degb ≤ f.support.sup degb ⊔ g.support.sup degb

Tactic:
classical
  exact (Finset.sup_mono Finsupp.support_add).trans_eq Finset.sup_union

Premises used: LE.le.trans_eq, Finset.sup_union, Finsupp.support_add, Finset.sup_mono
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R : Type u_1
A : Type u_3
T : Type u_4
inst : SemilatticeInf T
inst_1 : OrderTop T
inst_2 : Semiring R
degt : A → T
f g : R[A]
⊢ f.support.inf degt ⊓ g.support.inf degt ≤ (f + g).support.inf degt

Tactic:
sup_support_add_le (fun a : A => OrderDual.toDual (degt a)) f g

Premises used: OrderDual.toDual, AddMonoidAlgebra.sup_support_add_le, OrderDual, Finset.inf, DFunLike.coe
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : SemilatticeSup B
inst_1 : OrderBot B
inst_2 : Semiring R
inst_3 : Add A
inst_4 : Add B
inst_5 : AddLeftMono B
inst_6 : AddRightMono B
degb : A → B
degbm : ∀ (a b : A), degb (a + b) ≤ degb a + degb b
f g : R[A]
grw : ∀ x ∈ f.support, ∀ y ∈ g.support, degb (x + y) ≤ f.support.sup degb + g.support.sup degb
⊢ (f * g).support.sup degb ≤ f.support.sup degb + g.support.sup degb

Tactic:
grw [support_mul, Finset.sup_add_le]

Premises used: Finset.sup_add_le, AddMonoidAlgebra.support_mul
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : SemilatticeSup B
inst_1 : OrderBot B
inst_2 : Semiring R
inst_3 : Add A
inst_4 : Add B
inst_5 : AddLeftMono B
inst_6 : AddRightMono B
degb : A → B
degbm : ∀ (a b : A), degb (a + b) ≤ degb a + degb b
f g : R[A]
_fd : A
fds : _fd ∈ f.support
_gd : A
gds : _gd ∈ g.support
grw : degb _fd + degb _gd ≤ f.support.sup degb + g.support.sup degb
grw₁ : degb _fd + degb _gd ≤ degb _fd + g.support.sup degb
grw₂ grw₃ : degb _fd + degb _gd ≤ degb _fd + degb _gd
⊢ degb (_fd + _gd) ≤ f.support.sup degb + g.support.sup degb

Tactic:
grw [degbm, ← Finset.le_sup fds, ← Finset.le_sup gds]

Premises used: Finset.le_sup