awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Basic (goal)
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
rw :
  HMul.hMul (α := R) ((f : (a : k) → R) (a.coeff y) : R)
      (HMul.hMul (α := 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 : (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)
have rw₁ : HMul.hMul (α := R) ((f : (a : k) → R) (a.coeff y) : R)
    (HMul.hMul (β := R) (HMul.hMul (α := R) (β := R) ((f : (a : k) → R) (y • b.coeff x) : 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)
Tactic: rw [mul_assoc, ← mul_assoc (f (y • b.coeff x)), h_comm hy, mul_assoc, mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Basic (goal)
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
rw :
  HMul.hMul (α := R) ((f : (a : k) → R) (a.coeff y) : R)
      (HMul.hMul (α := 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)
rw₁ :
  HMul.hMul (α := R) ((f : (a : k) → R) (a.coeff y) : R)
      (HMul.hMul (β := R)
        (HMul.hMul (α := R) (β := R) ((f : (a : k) → R) (y • b.coeff x) : 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 : (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)
have rw₂ : HMul.hMul (α := R) ((f : (a : k) → R) (a.coeff y) : R)
    (HMul.hMul (β := R) (HMul.hMul (α := R) (β := R) ((g : (a : G) → R) y : R) ((f : (a : k) → R) (b.coeff x) : 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)
Tactic: rw [mul_assoc, ← mul_assoc (f (y • b.coeff x)), h_comm hy, mul_assoc, mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Basic (goal)
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
rw :
  HMul.hMul (α := R) ((f : (a : k) → R) (a.coeff y) : R)
      (HMul.hMul (α := 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)
rw₁ :
  HMul.hMul (α := R) ((f : (a : k) → R) (a.coeff y) : R)
      (HMul.hMul (β := R)
        (HMul.hMul (α := R) (β := R) ((f : (a : k) → R) (y • b.coeff x) : 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)
rw₂ :
  HMul.hMul (α := R) ((f : (a : k) → R) (a.coeff y) : R)
      (HMul.hMul (β := R) (HMul.hMul (α := R) (β := R) ((g : (a : G) → R) y : R) ((f : (a : k) → R) (b.coeff x) : 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 : (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)
have rw₃ : HMul.hMul (α := R) ((f : (a : k) → R) (a.coeff y) : R)
    (HMul.hMul (α := 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 : (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)
Tactic: rw [mul_assoc, ← mul_assoc (f (y • b.coeff x)), h_comm hy, mul_assoc, mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Basic (goal)
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
rw :
  HMul.hMul (α := R) ((f : (a : k) → R) (a.coeff y) : R)
      (HMul.hMul (α := 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)
rw₁ :
  HMul.hMul (α := R) ((f : (a : k) → R) (a.coeff y) : R)
      (HMul.hMul (β := R)
        (HMul.hMul (α := R) (β := R) ((f : (a : k) → R) (y • b.coeff x) : 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)
rw₂ :
  HMul.hMul (α := R) ((f : (a : k) → R) (a.coeff y) : R)
      (HMul.hMul (β := R) (HMul.hMul (α := R) (β := R) ((g : (a : G) → R) y : R) ((f : (a : k) → R) (b.coeff x) : 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)
rw₃ :
  HMul.hMul (α := R) ((f : (a : k) → R) (a.coeff y) : R)
      (HMul.hMul (α := 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 : (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 : (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)
have rw₄ : HMul.hMul (α := R) ((f : (a : k) → R) (a.coeff y) : R)
    (HMul.hMul (α := 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) ((f : (a : k) → R) (a.coeff y) : R)
    (HMul.hMul (α := 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)))
Tactic: rw [mul_assoc, ← mul_assoc (f (y • b.coeff x)), h_comm hy, mul_assoc, mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Basic (goal)
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
⊢ HMul.hMul (α := SkewMonoidAlgebra k G) (single x a) (single y b) * h = single x a * (single y b * h)
have single : ∀ (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: induction h with
        | single z c => simp [mul_assoc, mul_smul, mul_def]
        | add => simp_all [mul_add]
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Basic (goal)
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)
⊢ HMul.hMul (α := SkewMonoidAlgebra k G) (SkewMonoidAlgebra.single x a) (SkewMonoidAlgebra.single y b) * h =
    SkewMonoidAlgebra.single x a * (SkewMonoidAlgebra.single y b * h)
have 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))
Tactic: induction h with
        | single z c => simp [mul_assoc, mul_smul, mul_def]
        | add => simp_all [mul_add]
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Basic (goal)
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 x a * g * h = single x a * (g * h)
have single : ∀ (y : G) (b : k), HMul.hMul (α := SkewMonoidAlgebra k G) (single x a) (single y b) * h = single x a * (single y b * 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]
Cleared hypotheses: g
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Basic (goal)
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)
⊢ SkewMonoidAlgebra.single x a * g * h = SkewMonoidAlgebra.single x a * (g * h)
have 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)
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]
Cleared hypotheses: g
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Basic (goal)
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
⊢ f * g * h = f * (g * h)
have single : ∀ (x : G) (a : k), single x a * g * h = single x a * (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]
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Basic (goal)
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)
⊢ f * g * h = f * (g * h)
have 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)
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]
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Basic (goal)
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
⊢ HMul.hMul (α := SkewMonoidAlgebra k G) 1 (single g a) = single g a
have single : 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: rw [one_def, mul_def, sum_single_index]
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Basic (goal)
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)
⊢ HMul.hMul (α := SkewMonoidAlgebra k G) 1 (SkewMonoidAlgebra.single g a) = SkewMonoidAlgebra.single g a
have 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
Tactic: rw [one_def, mul_def, sum_single_index]
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Basic (goal)
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
⊢ 1 * f = f
have single : ∀ (g : G) (a : k), HMul.hMul (α := SkewMonoidAlgebra k G) 1 (single g a) = single g a
Tactic: induction f with
    | single g a => rw [one_def, mul_def, sum_single_index] <;> simp
    | add f g _ _ => simp_all [mul_add]
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Basic (goal)
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
⊢ 1 * f = f
have add : ∀ (f g : SkewMonoidAlgebra k G), 1 * f = f → 1 * g = g → 1 * (f + g) = f + g
Tactic: induction f with
    | single g a => rw [one_def, mul_def, sum_single_index] <;> simp
    | add f g _ _ => simp_all [mul_add]
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Basic (goal)
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
⊢ HMul.hMul (α := SkewMonoidAlgebra k G) (single g a) 1 = single g a
have single : Eq (α := SkewMonoidAlgebra k G) (single (g * 1) (a * HSMul.hSMul (β := k) g 1)) (single g a)
Tactic: rw [one_def, mul_def, sum_single_index, sum_single_index]
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Basic (goal)
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)
⊢ HMul.hMul (α := SkewMonoidAlgebra k G) (SkewMonoidAlgebra.single g a) 1 = SkewMonoidAlgebra.single g a
have single₁ : Eq (α := SkewMonoidAlgebra k G) (SkewMonoidAlgebra.single (g * 1) (a * HSMul.hSMul (β := k) g 0)) 0
Tactic: rw [one_def, mul_def, sum_single_index, sum_single_index]
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Basic (goal)
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
⊢ HMul.hMul (α := SkewMonoidAlgebra k G) (SkewMonoidAlgebra.single g a) 1 = SkewMonoidAlgebra.single g a
have single₂ : Eq (α := SkewMonoidAlgebra k G)
  (sum (SkewMonoidAlgebra.single 1 1) fun (a₂ : G) (b₂ : k) ↦ SkewMonoidAlgebra.single (g * a₂) (0 * g • b₂)) 0
Tactic: rw [one_def, mul_def, sum_single_index, sum_single_index]
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Basic (goal)
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
⊢ f * 1 = f
have single : ∀ (g : G) (a : k), HMul.hMul (α := SkewMonoidAlgebra k G) (single g a) 1 = single g a
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]
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Basic (goal)
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
⊢ f * 1 = f
have add : ∀ (f g : SkewMonoidAlgebra k G), f * 1 = f → g * 1 = g → (f + g) * 1 = f + g
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]
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Basic (goal)
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
have rw : HSMul.hSMul (β := k) g ((algebraMap k k : (a : k) → k) r : k) = (algebraMap k k : (a : k) → k) r
Tactic: rw [← Algebra.algebraMap_self_apply r, smul_algebraMap g r]
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Basic (goal)
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
⊢ g • r = r
have rw₁ : Eq (α := k) ((algebraMap k k : (a : k) → k) r : k) ((algebraMap k k : (a : k) → k) r : k)
Tactic: rw [← Algebra.algebraMap_self_apply r, smul_algebraMap g r]
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Basic (hypothesis)
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
⊢ a * b = b * a
have hgk : ∀ (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]
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Basic (goal)
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
⊢ a * b = b * a
have 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₂))
Tactic: simp only [mul_def, hgk, sum_def]
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Basic (goal)
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)
    (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₂))
have 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₂))
Tactic: rw [Finsupp.sum_comm]
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Basic (goal)
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
⊢ 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)))
have 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)))
Tactic: rw [mul_comm, mul_comm (a.toFinsupp y) _]