awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : Mul G
R : Type u_3
inst_1 : Semiring R
inst_2 : NonAssocSemiring k
inst_3 : SMul G k
g_hom : Type u_4
inst_4 : FunLike g_hom G R
inst_5 : MulHomClass g_hom G R
f : k →+* R
g : g_hom
a b : SkewMonoidAlgebra k G
h_comm :
  ∀ {x y : G},
    y ∈ a.support →
      HMul.hMul (α := R) (β := R) ((f : (a : k) → R) (y • b.coeff x) : R) ((g : (a : G) → R) y : R) =
        HMul.hMul (α := R) (β := R) ((g : (a : G) → R) y : R) ((f : (a : k) → R) (b.coeff x) : R)
simp_rw :
  Eq.{u_3 + 1} (α := R)
    (a.sum fun (a : G) (b_1 : k) ↦
      b.sum fun (a_1 : G) (b : k) ↦
        HMul.hMul (α := R) (β := R) (((↑f : k →+ R) : (a : k) → R) (b_1 * a • b) : R) ((g : (a : G) → R) (a * a_1) : R))
    (a.sum fun (a : G) (c : k) ↦
      b.sum fun (a_1 : G) (c_1 : k) ↦
        HMul.hMul (α := R) (β := R) (((↑f : k →+ R) : (a : k) → R) c : R) ((g : (a : G) → R) a : R) *
          HMul.hMul (α := R) (β := R) (((↑f : k →+ R) : (a : k) → R) c_1 : R) ((g : (a : G) → R) a_1 : R))
⊢ (liftNC (↑f : k →+ R) (⇑g : (a : G) → R) : (a : SkewMonoidAlgebra k G) → R) (a * b) =
    HMul.hMul (α := R) (β := R)
      ((liftNC (↑f : k →+ R) (⇑g : (a : G) → R) : (a : SkewMonoidAlgebra k G) → R) (a.sum single) : R)
      ((liftNC (↑f : k →+ R) (⇑g : (a : G) → R) : (a : SkewMonoidAlgebra k G) → R) (b.sum single) : R)

Tactic:
simp_rw [mul_def, map_sum, liftNC_single, sum_mul, mul_sum]

Premises used: SkewMonoidAlgebra.sum_mul, SkewMonoidAlgebra.map_sum, SkewMonoidAlgebra.mul_sum, SkewMonoidAlgebra.liftNC_single, SkewMonoidAlgebra.mul_def
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : Mul G
R : Type u_3
inst_1 : Semiring R
inst_2 : NonAssocSemiring k
inst_3 : SMul G k
g_hom : Type u_4
inst_4 : FunLike g_hom G R
inst_5 : MulHomClass g_hom G R
f : k →+* R
g : g_hom
a b : SkewMonoidAlgebra k G
h_comm :
  ∀ {x y : G},
    y ∈ a.support →
      HMul.hMul (α := R) (β := R) ((f : (a : k) → R) (y • b.coeff x) : R) ((g : (a : G) → R) y : R) =
        HMul.hMul (α := R) (β := R) ((g : (a : G) → R) y : R) ((f : (a : k) → R) (b.coeff x) : R)
⊢ Eq.{u_3 + 1} (α := R)
    (a.sum fun (a : G) (b_1 : k) ↦
      b.sum fun (a_1 : G) (b : k) ↦
        HMul.hMul (α := R) (β := R) (((↑f : k →+ R) : (a : k) → R) (b_1 * a • b) : R) ((g : (a : G) → R) (a * a_1) : R))
    (a.sum fun (a : G) (c : k) ↦
      b.sum fun (a_1 : G) (c_1 : k) ↦
        HMul.hMul (α := R) (β := R) (((↑f : k →+ R) : (a : k) → R) c : R) ((g : (a : G) → R) a : R) *
          HMul.hMul (α := R) (β := R) (((↑f : k →+ R) : (a : k) → R) c_1 : R) ((g : (a : G) → R) a_1 : R))

Tactic:
sum_congr fun y hy ↦ sum_congr fun x _hx ↦ ?_

Premises used: SkewMonoidAlgebra.sum_congr
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : Mul G
R : Type u_3
inst_1 : Semiring R
inst_2 : NonAssocSemiring k
inst_3 : SMul G k
g_hom : Type u_4
inst_4 : FunLike g_hom G R
inst_5 : MulHomClass g_hom G R
f : k →+* R
g : g_hom
a b : SkewMonoidAlgebra k G
h_comm :
  ∀ {x y : G},
    y ∈ a.support →
      HMul.hMul (α := R) (β := R) ((f : (a : k) → R) (y • b.coeff x) : R) ((g : (a : G) → R) y : R) =
        HMul.hMul (α := R) (β := R) ((g : (a : G) → R) y : R) ((f : (a : k) → R) (b.coeff x) : R)
refine :
  ∀ (y : G) (hy : y ∈ a.support) (x : G) (_hx : x ∈ b.support),
    HMul.hMul (α := R) (β := R) (((↑f : k →+ R) : (a : k) → R) (a.coeff y * y • b.coeff x) : R)
        ((g : (a : G) → R) (y * x) : R) =
      HMul.hMul (α := R) (β := R) (((↑f : k →+ R) : (a : k) → R) (a.coeff y) : R) ((g : (a : G) → R) y : R) *
        HMul.hMul (α := R) (β := R) (((↑f : k →+ R) : (a : k) → R) (b.coeff x) : R) ((g : (a : G) → R) x : R)
⊢ Eq.{u_3 + 1} (α := R)
    (a.sum fun (a : G) (b_1 : k) ↦
      b.sum fun (a_1 : G) (b : k) ↦
        HMul.hMul (α := R) (β := R) (((↑f : k →+ R) : (a : k) → R) (b_1 * a • b) : R) ((g : (a : G) → R) (a * a_1) : R))
    (a.sum fun (a : G) (c : k) ↦
      b.sum fun (a_1 : G) (c_1 : k) ↦
        HMul.hMul (α := R) (β := R) (((↑f : k →+ R) : (a : k) → R) c : R) ((g : (a : G) → R) a : R) *
          HMul.hMul (α := R) (β := R) (((↑f : k →+ R) : (a : k) → R) c_1 : R) ((g : (a : G) → R) a_1 : R))

Tactic:
refine sum_congr fun y hy ↦ sum_congr fun x _hx ↦ ?_

Premises used: SkewMonoidAlgebra.sum_congr
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : Mul G
R : Type u_3
inst_1 : Semiring R
inst_2 : NonAssocSemiring k
inst_3 : SMul G k
g_hom : Type u_4
inst_4 : FunLike g_hom G R
inst_5 : MulHomClass g_hom G R
f : k →+* R
g : g_hom
a b : SkewMonoidAlgebra k G
h_comm :
  ∀ {x y : G},
    y ∈ a.support →
      HMul.hMul (α := R) (β := R) ((f : (a : k) → R) (y • b.coeff x) : R) ((g : (a : G) → R) y : R) =
        HMul.hMul (α := R) (β := R) ((g : (a : G) → R) y : R) ((f : (a : k) → R) (b.coeff x) : R)
y : G
hy : y ∈ a.support
x : G
_hx : x ∈ b.support
simp :
  HMul.hMul (α := R) (β := R) ((f : (a : k) → R) (a.coeff y) : R) ((f : (a : k) → R) (y • b.coeff x) : R) *
      HMul.hMul (α := R) (β := R) ((g : (a : G) → R) y : R) ((g : (a : G) → R) x : R) =
    HMul.hMul (α := R) (β := R) ((f : (a : k) → R) (a.coeff y) : R) ((g : (a : G) → R) y : R) *
      HMul.hMul (α := R) (β := R) ((f : (a : k) → R) (b.coeff x) : R) ((g : (a : G) → R) x : R)
⊢ HMul.hMul (α := R) (β := R) (((↑f : k →+ R) : (a : k) → R) (a.coeff y * y • b.coeff x) : R)
      ((g : (a : G) → R) (y * x) : R) =
    HMul.hMul (α := R) (β := R) (((↑f : k →+ R) : (a : k) → R) (a.coeff y) : R) ((g : (a : G) → R) y : R) *
      HMul.hMul (α := R) (β := R) (((↑f : k →+ R) : (a : k) → R) (b.coeff x) : R) ((g : (a : G) → R) x : R)

Tactic:
simp only [AddMonoidHom.coe_coe, map_mul]

Premises used: AddMonoidHom.coe_coe, map_mul
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : Monoid G
inst_2 : MulSemiringAction G k
x : G
a : k
y : G
b : k
z : G
c : k
⊢ HMul.hMul (α := SkewMonoidAlgebra k G) (single x a) (single y b) * single z c =
    single x a * HMul.hMul (α := SkewMonoidAlgebra k G) (single y b) (single z c)

Tactic:
simp [mul_assoc, mul_smul, mul_def]

Premises used: mul_assoc, SemigroupAction.mul_smul, SkewMonoidAlgebra.mul_def
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : Monoid G
inst_2 : MulSemiringAction G k
x : G
a : k
y : G
b : k
f g : SkewMonoidAlgebra k G
h : HMul.hMul (α := SkewMonoidAlgebra k G) (single x a) (single y b) * f = single x a * (single y b * f)
h_1 : HMul.hMul (α := SkewMonoidAlgebra k G) (single x a) (single y b) * g = single x a * (single y b * g)
⊢ HMul.hMul (α := SkewMonoidAlgebra k G) (single x a) (single y b) * (f + g) = single x a * (single y b * (f + g))

Tactic:
simp_all [mul_add]

Premises used: mul_add
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : Monoid G
inst_2 : MulSemiringAction G k
h : SkewMonoidAlgebra k G
x : G
a : k
y : G
b : k
single :
  ∀ (z : G) (c : k),
    HMul.hMul (α := SkewMonoidAlgebra k G) (SkewMonoidAlgebra.single x a) (SkewMonoidAlgebra.single y b) *
        SkewMonoidAlgebra.single z c =
      SkewMonoidAlgebra.single x a *
        HMul.hMul (α := SkewMonoidAlgebra k G) (SkewMonoidAlgebra.single y b) (SkewMonoidAlgebra.single z c)
single₁ :
  ∀ (f g : SkewMonoidAlgebra k G),
    HMul.hMul (α := SkewMonoidAlgebra k G) (SkewMonoidAlgebra.single x a) (SkewMonoidAlgebra.single y b) * f =
        SkewMonoidAlgebra.single x a * (SkewMonoidAlgebra.single y b * f) →
      HMul.hMul (α := SkewMonoidAlgebra k G) (SkewMonoidAlgebra.single x a) (SkewMonoidAlgebra.single y b) * g =
          SkewMonoidAlgebra.single x a * (SkewMonoidAlgebra.single y b * g) →
        HMul.hMul (α := SkewMonoidAlgebra k G) (SkewMonoidAlgebra.single x a) (SkewMonoidAlgebra.single y b) * (f + g) =
          SkewMonoidAlgebra.single x a * (SkewMonoidAlgebra.single y b * (f + g))
⊢ HMul.hMul (α := SkewMonoidAlgebra k G) (SkewMonoidAlgebra.single x a) (SkewMonoidAlgebra.single y b) * h =
    SkewMonoidAlgebra.single x a * (SkewMonoidAlgebra.single y b * h)

Tactic:
induction h with
        | single z c => simp [mul_assoc, mul_smul, mul_def]
        | add => simp_all [mul_add]

Premises used: mul_assoc, _private.0.SkewMonoidAlgebra.add, mul_add, SkewMonoidAlgebra.single, SemigroupAction.mul_smul, SkewMonoidAlgebra.mul_def
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : Monoid G
inst_2 : MulSemiringAction G k
h : SkewMonoidAlgebra k G
x : G
a : k
f g : SkewMonoidAlgebra k G
h_1 : single x a * f * h = single x a * (f * h)
h_2 : single x a * g * h = single x a * (g * h)
⊢ single x a * (f + g) * h = single x a * ((f + g) * h)

Tactic:
simp_all [add_mul, mul_add]

Premises used: add_mul, mul_add
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : Monoid G
inst_2 : MulSemiringAction G k
g h : SkewMonoidAlgebra k G
x : G
a : k
single :
  ∀ (y : G) (b : k),
    HMul.hMul (α := SkewMonoidAlgebra k G) (SkewMonoidAlgebra.single x a) (SkewMonoidAlgebra.single y b) * h =
      SkewMonoidAlgebra.single x a * (SkewMonoidAlgebra.single y b * h)
single₁ :
  ∀ (f g : SkewMonoidAlgebra k G),
    SkewMonoidAlgebra.single x a * f * h = SkewMonoidAlgebra.single x a * (f * h) →
      SkewMonoidAlgebra.single x a * g * h = SkewMonoidAlgebra.single x a * (g * h) →
        SkewMonoidAlgebra.single x a * (f + g) * h = SkewMonoidAlgebra.single x a * ((f + g) * h)
⊢ SkewMonoidAlgebra.single x a * g * h = SkewMonoidAlgebra.single x a * (g * h)

Tactic:
induction g with
      | single y b => induction h with
        | single z c => simp [mul_assoc, mul_smul, mul_def]
        | add => simp_all [mul_add]
      | add => simp_all [add_mul, mul_add]

Premises used: add_mul, mul_assoc, _private.0.SkewMonoidAlgebra.add, mul_add, SkewMonoidAlgebra.single, SemigroupAction.mul_smul, SkewMonoidAlgebra.mul_def
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : Monoid G
inst_2 : MulSemiringAction G k
g h : SkewMonoidAlgebra k G
f g_1 : SkewMonoidAlgebra k G
h_1 : f * g * h = f * (g * h)
h_2 : g_1 * g * h = g_1 * (g * h)
⊢ (f + g_1) * g * h = (f + g_1) * (g * h)

Tactic:
simp_all [add_mul]

Premises used: add_mul
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : Monoid G
inst_2 : MulSemiringAction G k
f g h : SkewMonoidAlgebra k G
single : ∀ (x : G) (a : k), SkewMonoidAlgebra.single x a * g * h = SkewMonoidAlgebra.single x a * (g * h)
add :
  ∀ (f g_1 : SkewMonoidAlgebra k G),
    f * g * h = f * (g * h) → g_1 * g * h = g_1 * (g * h) → (f + g_1) * g * h = (f + g_1) * (g * h)
⊢ f * g * h = f * (g * h)

Tactic:
induction f with
    | single x a => induction g with
      | single y b => induction h with
        | single z c => simp [mul_assoc, mul_smul, mul_def]
        | add => simp_all [mul_add]
      | add => simp_all [add_mul, mul_add]
    | add => simp_all [add_mul]

Premises used: add_mul, mul_assoc, _private.0.SkewMonoidAlgebra.add, mul_add, SkewMonoidAlgebra.single, SemigroupAction.mul_smul, SkewMonoidAlgebra.mul_def
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : Monoid G
inst_2 : MulSemiringAction G k
g : G
a : k
single :
  Eq (α := SkewMonoidAlgebra k G)
    (sum (SkewMonoidAlgebra.single g a) fun (a₂ : G) (b₂ : k) ↦
      SkewMonoidAlgebra.single (1 * a₂) (1 * HSMul.hSMul.{u_2, u_1, u_1} (α := G) 1 b₂))
    (SkewMonoidAlgebra.single g a)
single₁ :
  Eq (α := SkewMonoidAlgebra k G)
    (sum (SkewMonoidAlgebra.single g a) fun (a₂ : G) (b₂ : k) ↦
      SkewMonoidAlgebra.single (1 * a₂) (0 * HSMul.hSMul.{u_2, u_1, u_1} (α := G) 1 b₂))
    0
⊢ HMul.hMul (α := SkewMonoidAlgebra k G) 1 (SkewMonoidAlgebra.single g a) = SkewMonoidAlgebra.single g a

Tactic:
rw [one_def, mul_def, sum_single_index]

Premises used: SkewMonoidAlgebra.one_def, SkewMonoidAlgebra.sum_single_index, SkewMonoidAlgebra.mul_def
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : Monoid G
inst_2 : MulSemiringAction G k
g : G
a : k
⊢ Eq (α := SkewMonoidAlgebra k G)
    (sum (single g a) fun (a₂ : G) (b₂ : k) ↦ single (1 * a₂) (1 * HSMul.hSMul.{u_2, u_1, u_1} (α := G) 1 b₂))
    (single g a)

Tactic:
simp
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : Monoid G
inst_2 : MulSemiringAction G k
g : G
a : k
⊢ Eq (α := SkewMonoidAlgebra k G)
    (sum (single g a) fun (a₂ : G) (b₂ : k) ↦ single (1 * a₂) (0 * HSMul.hSMul.{u_2, u_1, u_1} (α := G) 1 b₂)) 0

Tactic:
simp
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : Monoid G
inst_2 : MulSemiringAction G k
f g : SkewMonoidAlgebra k G
h : 1 * f = f
h_1 : 1 * g = g
⊢ 1 * (f + g) = f + g

Tactic:
simp_all [mul_add]

Premises used: mul_add
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : Monoid G
inst_2 : MulSemiringAction G k
f : SkewMonoidAlgebra k G
single :
  ∀ (g : G) (a : k),
    HMul.hMul (α := SkewMonoidAlgebra k G) 1 (SkewMonoidAlgebra.single g a) = SkewMonoidAlgebra.single g a
add : ∀ (f g : SkewMonoidAlgebra k G), 1 * f = f → 1 * g = g → 1 * (f + g) = f + g
⊢ 1 * f = f

Tactic:
induction f with
    | single g a => rw [one_def, mul_def, sum_single_index] <;> simp
    | add f g _ _ => simp_all [mul_add]

Premises used: SkewMonoidAlgebra.one_def, _private.0.SkewMonoidAlgebra.add, mul_add, SkewMonoidAlgebra.single, SkewMonoidAlgebra.sum_single_index, SkewMonoidAlgebra.mul_def
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : Monoid G
inst_2 : MulSemiringAction G k
g : G
a : k
single :
  Eq (α := SkewMonoidAlgebra k G) (SkewMonoidAlgebra.single (g * 1) (a * HSMul.hSMul (β := k) g 1))
    (SkewMonoidAlgebra.single g a)
single₁ : Eq (α := SkewMonoidAlgebra k G) (SkewMonoidAlgebra.single (g * 1) (a * HSMul.hSMul (β := k) g 0)) 0
single₂ :
  Eq (α := SkewMonoidAlgebra k G)
    (sum (SkewMonoidAlgebra.single 1 1) fun (a₂ : G) (b₂ : k) ↦ SkewMonoidAlgebra.single (g * a₂) (0 * g • b₂)) 0
⊢ HMul.hMul (α := SkewMonoidAlgebra k G) (SkewMonoidAlgebra.single g a) 1 = SkewMonoidAlgebra.single g a

Tactic:
rw [one_def, mul_def, sum_single_index, sum_single_index]

Premises used: SkewMonoidAlgebra.one_def, SkewMonoidAlgebra.sum_single_index, SkewMonoidAlgebra.mul_def
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : Monoid G
inst_2 : MulSemiringAction G k
g : G
a : k
⊢ Eq (α := SkewMonoidAlgebra k G) (single (g * 1) (a * HSMul.hSMul (β := k) g 1)) (single g a)

Tactic:
simp
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : Monoid G
inst_2 : MulSemiringAction G k
g : G
a : k
⊢ Eq (α := SkewMonoidAlgebra k G) (single (g * 1) (a * HSMul.hSMul (β := k) g 0)) 0

Tactic:
simp
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : Monoid G
inst_2 : MulSemiringAction G k
g : G
a : k
⊢ Eq (α := SkewMonoidAlgebra k G) (sum (single 1 1) fun (a₂ : G) (b₂ : k) ↦ single (g * a₂) (0 * g • b₂)) 0

Tactic:
simp
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : Monoid G
inst_2 : MulSemiringAction G k
f g : SkewMonoidAlgebra k G
h : f * 1 = f
h_1 : g * 1 = g
⊢ (f + g) * 1 = f + g

Tactic:
simp_all [add_mul]

Premises used: add_mul
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : Monoid G
inst_2 : MulSemiringAction G k
f : SkewMonoidAlgebra k G
single :
  ∀ (g : G) (a : k),
    HMul.hMul (α := SkewMonoidAlgebra k G) (SkewMonoidAlgebra.single g a) 1 = SkewMonoidAlgebra.single g a
add : ∀ (f g : SkewMonoidAlgebra k G), f * 1 = f → g * 1 = g → (f + g) * 1 = f + g
⊢ f * 1 = f

Tactic:
induction f with
    | single g a => rw [one_def, mul_def, sum_single_index, sum_single_index] <;> simp
    | add f g _ _ => simp_all [add_mul]

Premises used: add_mul, SkewMonoidAlgebra.one_def, _private.0.SkewMonoidAlgebra.add, SkewMonoidAlgebra.single, SkewMonoidAlgebra.sum_single_index, SkewMonoidAlgebra.mul_def
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : CommSemiring k
inst_1 : CommMonoid G
inst_2 : MulSemiringAction G k
inst_3 : SMulCommClass G k k
a b : SkewMonoidAlgebra k G
g : G
r : k
rw : HSMul.hSMul (β := k) g ((algebraMap k k : (a : k) → k) r : k) = (algebraMap k k : (a : k) → k) r
rw₁ rw₂ : Eq (α := k) ((algebraMap k k : (a : k) → k) r : k) ((algebraMap k k : (a : k) → k) r : k)
⊢ g • r = r

Tactic:
rw [← Algebra.algebraMap_self_apply r, smul_algebraMap g r]

Premises used: Algebra.algebraMap_self_apply, smul_algebraMap
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : CommSemiring k
inst_1 : CommMonoid G
inst_2 : MulSemiringAction G k
inst_3 : SMulCommClass G k k
a b : SkewMonoidAlgebra k G
⊢ ∀ (g : G) (r : k), g • r = r

Tactic:
have hgk (g : G) (r : k) : g • r = r := by
      rw [← Algebra.algebraMap_self_apply r, smul_algebraMap g r]
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : CommSemiring k
inst_1 : CommMonoid G
inst_2 : MulSemiringAction G k
inst_3 : SMulCommClass G k k
a b : SkewMonoidAlgebra k G
hgk : ∀ (g : G) (r : k), g • r = r
simp :
  Eq (α := SkewMonoidAlgebra k G)
    (a.toFinsupp.sum fun (a₁ : G) (b₁ : k) ↦ b.toFinsupp.sum fun (a₂ : G) (b₂ : k) ↦ single (a₁ * a₂) (b₁ * b₂))
    (b.toFinsupp.sum fun (a₁ : G) (b₁ : k) ↦ a.toFinsupp.sum fun (a₂ : G) (b₂ : k) ↦ single (a₁ * a₂) (b₁ * b₂))
⊢ a * b = b * a

Tactic:
simp only [mul_def, hgk, sum_def]

Premises used: SkewMonoidAlgebra.sum_def, SkewMonoidAlgebra.mul_def
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : CommSemiring k
inst_1 : CommMonoid G
inst_2 : MulSemiringAction G k
inst_3 : SMulCommClass G k k
a b : SkewMonoidAlgebra k G
hgk : ∀ (g : G) (r : k), g • r = r
rw :
  Eq (α := SkewMonoidAlgebra k G)
    (b.toFinsupp.sum fun (x' : G) (v' : k) ↦ a.toFinsupp.sum fun (x : G) (v : k) ↦ single (x * x') (v * v'))
    (b.toFinsupp.sum fun (a₁ : G) (b₁ : k) ↦ a.toFinsupp.sum fun (a₂ : G) (b₂ : k) ↦ single (a₁ * a₂) (b₁ * b₂))
⊢ Eq (α := SkewMonoidAlgebra k G)
    (a.toFinsupp.sum fun (a₁ : G) (b₁ : k) ↦ b.toFinsupp.sum fun (a₂ : G) (b₂ : k) ↦ single (a₁ * a₂) (b₁ * b₂))
    (b.toFinsupp.sum fun (a₁ : G) (b₁ : k) ↦ a.toFinsupp.sum fun (a₂ : G) (b₂ : k) ↦ single (a₁ * a₂) (b₁ * b₂))

Tactic:
rw [Finsupp.sum_comm]

Premises used: Finsupp.sum_comm
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : CommSemiring k
inst_1 : CommMonoid G
inst_2 : MulSemiringAction G k
inst_3 : SMulCommClass G k k
a b : SkewMonoidAlgebra k G
hgk : ∀ (g : G) (r : k), g • r = r
x : G
h : x ∈ b.toFinsupp.support
y : G
h_1 : y ∈ a.toFinsupp.support
rw :
  Eq (α := SkewMonoidAlgebra k G)
    (single (x * y)
      (HMul.hMul (α := k) (β := k) ((a.toFinsupp : (a : G) → k) y : k) ((b.toFinsupp : (a : G) → k) x : k)))
    (single (x * y)
      (HMul.hMul (α := k) (β := k) ((b.toFinsupp : (a : G) → k) x : k) ((a.toFinsupp : (a : G) → k) y : k)))
rw₁ rw₂ :
  Eq (α := SkewMonoidAlgebra k G)
    (single (x * y)
      (HMul.hMul (α := k) (β := k) ((b.toFinsupp : (a : G) → k) x : k) ((a.toFinsupp : (a : G) → k) y : k)))
    (single (x * y)
      (HMul.hMul (α := k) (β := k) ((b.toFinsupp : (a : G) → k) x : k) ((a.toFinsupp : (a : G) → k) y : k)))
⊢ Eq (α := SkewMonoidAlgebra k G)
    (single (y * x)
      (HMul.hMul (α := k) (β := k) ((a.toFinsupp : (a : G) → k) y : k) ((b.toFinsupp : (a : G) → k) x : k)))
    (single (x * y)
      (HMul.hMul (α := k) (β := k) ((b.toFinsupp : (a : G) → k) x : k) ((a.toFinsupp : (a : G) → k) y : k)))

Tactic:
rw [mul_comm, mul_comm (a.toFinsupp y) _]

Premises used: SkewMonoidAlgebra.toFinsupp, mul_comm, DFunLike.coe
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : CommSemiring k
inst_1 : CommMonoid G
inst_2 : MulSemiringAction G k
inst_3 : SMulCommClass G k k
a b : SkewMonoidAlgebra k G
hgk : ∀ (g : G) (r : k), g • r = r
⊢ Eq (α := SkewMonoidAlgebra k G)
    (b.toFinsupp.sum fun (x' : G) (v' : k) ↦ a.toFinsupp.sum fun (x : G) (v : k) ↦ single (x * x') (v * v'))
    (b.toFinsupp.sum fun (a₁ : G) (b₁ : k) ↦ a.toFinsupp.sum fun (a₂ : G) (b₂ : k) ↦ single (a₁ * a₂) (b₁ * b₂))

Tactic:
exact Finsupp.sum_congr (fun x _ ↦ Finsupp.sum_congr
      (fun y _ ↦ by rw [mul_comm, mul_comm (a.toFinsupp y) _]))

Premises used: Finsupp.sum_congr
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
S : Type u_3
S₁ : Type u_4
S₂ : Type u_5
inst : AddMonoid k
inst_1 : SMulZeroClass S k
inst_2 : FaithfulSMul S k
inst_3 : Nonempty G
_s₁ _s₂ : S
h : ∀ (a : SkewMonoidAlgebra k G), _s₁ • a = _s₂ • a
apply : ∀ (a : G →₀ k), { toFinsupp := _s₁ • a : SkewMonoidAlgebra k G } = { toFinsupp := _s₂ • a }
⊢ _s₁ = _s₂

Tactic:
apply eq_of_smul_eq_smul fun a : G →₀ k ↦ congr_arg toFinsupp _

Premises used: FaithfulSMul.eq_of_smul_eq_smul, SkewMonoidAlgebra.toFinsupp, congr_arg
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
S : Type u_3
S₁ : Type u_4
S₂ : Type u_5
inst : Semiring S
inst_1 : AddCommMonoid k
inst_2 : Module S k
⊢ ∀ (c : S) (x : SkewMonoidAlgebra k G),
    (toFinsuppAddEquiv : (a : SkewMonoidAlgebra k G) → G →₀ k) (c • x) =
      HSMul.hSMul (β := G →₀ k) c ((toFinsuppAddEquiv : (a : SkewMonoidAlgebra k G) → G →₀ k) x : G →₀ k)

Tactic:
simp
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
S : Type u_3
S₁ : Type u_4
S₂ : Type u_5
inst : Semiring S
inst_1 : Semiring k
⊢ Module.Free k (SkewMonoidAlgebra k G)

Tactic:
Module.Free.of_basis basisSingleOne

Premises used: SkewMonoidAlgebra.basisSingleOne, Module.Free.of_basis
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
G : Type u_2
M : Type u_6
α : Type u_7
inst : Monoid G
inst_1 : AddCommMonoid M
inst_2 : MulAction G α
g : G
f : SkewMonoidAlgebra M α
⊢ g • f = (mapDomain fun (x : α) ↦ g • x : (a : SkewMonoidAlgebra M α) → SkewMonoidAlgebra M α) f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
G : Type u_2
M : Type u_6
α : Type u_7
inst : Monoid G
inst_1 : AddCommMonoid M
inst_2 : MulAction G α
g : G
a : α
b : M
⊢ HSMul.hSMul (β := SkewMonoidAlgebra M α) g (single a b) = single (g • a) b

Tactic:
mapDomain_single

Premises used: SkewMonoidAlgebra.mapDomain_single