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 : AddCommMonoid k
M : Type u_3
inst_1 : AddZeroClass M
f g : SkewMonoidAlgebra k G →+ M
h :
  ∀ (a : G) (b : k),
    Eq.{u_3 + 1} (α := M) ((f : (a : SkewMonoidAlgebra k G) → M) (single a b) : M)
      ((g : (a : SkewMonoidAlgebra k G) → M) (single a b) : M)
p : SkewMonoidAlgebra k G
h₁ : Eq.{u_3 + 1} (α := M) ((f : (a : SkewMonoidAlgebra k G) → M) 0 : M) ((g : (a : SkewMonoidAlgebra k G) → M) 0 : M)
h₂ :
  ∀ (g_1 : G) (a : k),
    Eq.{u_3 + 1} (α := M) ((f : (a : SkewMonoidAlgebra k G) → M) (single g_1 a) : M)
      ((g : (a : SkewMonoidAlgebra k G) → M) (single g_1 a) : M)
⊢ Eq.{u_3 + 1} (α := M) ((f : (a : SkewMonoidAlgebra k G) → M) p : M) ((g : (a : SkewMonoidAlgebra k G) → M) p : M)
have h₃ : ∀ (f_1 g_1 : SkewMonoidAlgebra k G),
  Eq.{u_3 + 1} (α := M) ((f : (a : SkewMonoidAlgebra k G) → M) f_1 : M)
      ((g : (a : SkewMonoidAlgebra k G) → M) f_1 : M) →
    Eq.{u_3 + 1} (α := M) ((f : (a : SkewMonoidAlgebra k G) → M) g_1 : M)
        ((g : (a : SkewMonoidAlgebra k G) → M) g_1 : M) →
      Eq.{u_3 + 1} (α := M) ((f : (a : SkewMonoidAlgebra k G) → M) (f_1 + g_1) : M)
        ((g : (a : SkewMonoidAlgebra k G) → M) (f_1 + g_1) : M)
Tactic: induction p using SkewMonoidAlgebra.induction_on
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Basic (goal)
Goal:
k : Type u_1
G : Type u_2
inst : AddCommMonoid k
G' : Type u_3
f : G → G'
v : SkewMonoidAlgebra k G
⊢ toFinsupp ((mapDomain f : (a : SkewMonoidAlgebra k G) → SkewMonoidAlgebra k G') v) = Finsupp.mapDomain f v.toFinsupp
have simp_rw : toFinsupp (v.sum fun (a : G) ↦ single (f a)) = Finsupp.mapDomain f v.toFinsupp
Tactic: simp_rw [mapDomain_apply, Finsupp.mapDomain, toFinsupp_sum', single]
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Basic (goal)
Goal:
k : Type u_1
G : Type u_2
inst : AddCommMonoid k
G' : Type u_3
f : G → G'
v : SkewMonoidAlgebra k G
simp_rw : toFinsupp (v.sum fun (a : G) ↦ single (f a)) = Finsupp.mapDomain f v.toFinsupp
⊢ toFinsupp ((mapDomain f : (a : SkewMonoidAlgebra k G) → SkewMonoidAlgebra k G') v) = Finsupp.mapDomain f v.toFinsupp
have simp_rw₁ : Eq (α := G' →₀ k) (toFinsupp (v.sum fun (a : G) ↦ single (f a))) (v.toFinsupp.sum fun (a : G) ↦ Finsupp.single (f a))
Tactic: simp_rw [mapDomain_apply, Finsupp.mapDomain, toFinsupp_sum', single]
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Basic (goal)
Goal:
k : Type u_1
G : Type u_2
inst : AddCommMonoid k
G' : Type u_3
f : G → G'
v : SkewMonoidAlgebra k G
simp_rw : toFinsupp (v.sum fun (a : G) ↦ single (f a)) = Finsupp.mapDomain f v.toFinsupp
simp_rw₁ :
  Eq (α := G' →₀ k) (toFinsupp (v.sum fun (a : G) ↦ single (f a))) (v.toFinsupp.sum fun (a : G) ↦ Finsupp.single (f a))
⊢ toFinsupp ((mapDomain f : (a : SkewMonoidAlgebra k G) → SkewMonoidAlgebra k G') v) = Finsupp.mapDomain f v.toFinsupp
have simp_rw₂ : Eq (α := G' →₀ k) (v.toFinsupp.sum fun (x1 : G) (x2 : k) ↦ toFinsupp (single (f x1) x2))
  (v.toFinsupp.sum fun (a : G) ↦ Finsupp.single (f a))
Tactic: simp_rw [mapDomain_apply, Finsupp.mapDomain, toFinsupp_sum', single]
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Basic (goal)
Goal:
k : Type u_1
G : Type u_2
inst : AddCommMonoid k
G' : Type u_3
f : G → G'
v : SkewMonoidAlgebra k G
R : Type u_5
inst_1 : Monoid R
inst_2 : DistribMulAction R k
b : R
⊢ (mapDomain f : (a : SkewMonoidAlgebra k G) → SkewMonoidAlgebra k G') (b • v) =
    HSMul.hSMul (β := SkewMonoidAlgebra k G') b
      ((mapDomain f : (a : SkewMonoidAlgebra k G) → SkewMonoidAlgebra k G') v : SkewMonoidAlgebra k G')
have simp_rw : Finsupp.mapDomain f (b • v).toFinsupp = b • Finsupp.mapDomain f v.toFinsupp
Tactic: simp_rw [← toFinsupp_inj, toFinsupp_smul, toFinsupp_mapDomain]
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Basic (goal)
Goal:
k : Type u_1
G : Type u_2
inst : AddCommMonoid k
R : Type u_5
inst_1 : NonUnitalNonAssocSemiring R
f : k →+ R
g : G → R
l : SkewMonoidAlgebra k G →+ R
h :
  ∀ (a : G) (b : k),
    (l : (a : SkewMonoidAlgebra k G) → R) (single a b) = HMul.hMul (α := R) ((f : (a : k) → R) b : R) (g a)
⊢ l = liftNC f g
have h₁ : ∀ (a : G) (b : k),
  Eq.{u_5 + 1} (α := R) ((l : (a : SkewMonoidAlgebra k G) → R) (single a b) : R)
    ((liftNC f g : (a : SkewMonoidAlgebra k G) → R) (single a b) : R)
Tactic: ext a b
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Basic (goal)
Goal:
k : Type u_1
G : Type u_2
inst : AddGroup k
a : SkewMonoidAlgebra k G
⊢ -a + a = 0
have ofFinsupp : ∀ (toFinsupp : G →₀ k),
  -{ toFinsupp := toFinsupp : SkewMonoidAlgebra k G } + { toFinsupp := toFinsupp : SkewMonoidAlgebra k G } = 0
Tactic: cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Basic (goal)
Goal:
k : Type u_1
G : Type u_2
inst : AddGroupWithOne k
inst_1 : One G
z : ℤ
⊢ Eq (α := SkewMonoidAlgebra k G) (↑z : SkewMonoidAlgebra k G) (single 1 (↑z : k))
have ofNat : ∀ (a : ℕ), Eq (α := SkewMonoidAlgebra k G) (↑(Int.ofNat a) : SkewMonoidAlgebra k G) (single 1 (↑(Int.ofNat a) : k))
Tactic: cases z
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Basic (goal)
Goal:
k : Type u_1
G : Type u_2
inst : AddGroupWithOne k
inst_1 : One G
z : ℤ
ofNat :
  ∀ (a : ℕ), Eq (α := SkewMonoidAlgebra k G) (↑(Int.ofNat a) : SkewMonoidAlgebra k G) (single 1 (↑(Int.ofNat a) : k))
⊢ Eq (α := SkewMonoidAlgebra k G) (↑z : SkewMonoidAlgebra k G) (single 1 (↑z : k))
have negSucc : ∀ (a : ℕ), Eq (α := SkewMonoidAlgebra k G) (↑(Int.negSucc a) : SkewMonoidAlgebra k G) (single 1 (↑(Int.negSucc a) : k))
Tactic: cases z
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Basic (goal)
Goal:
k : Type u_1
G : Type u_2
inst : Mul G
inst_1 : NonUnitalNonAssocSemiring k
inst_2 : DistribSMul G k
f g h : SkewMonoidAlgebra k G
⊢ f * (g + h) = f * g + f * h
have simp : (f.sum fun (a₁ : G) (b₁ : k) ↦ (g + h).sum fun (a₂ : G) (b₂ : k) ↦ single (a₁ * a₂) (b₁ * a₁ • b₂)) =
  HAdd.hAdd (α := SkewMonoidAlgebra k G)
    (f.sum fun (a₁ : G) (b₁ : k) ↦ g.sum fun (a₂ : G) (b₂ : k) ↦ single (a₁ * a₂) (b₁ * a₁ • b₂))
    (f.sum fun (a₁ : G) (b₁ : k) ↦ h.sum fun (a₂ : G) (b₂ : k) ↦ single (a₁ * a₂) (b₁ * a₁ • b₂))
Tactic: simp only [mul_def]
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Basic (goal)
Goal:
k : Type u_1
G : Type u_2
inst : Mul G
inst_1 : NonUnitalNonAssocSemiring k
inst_2 : DistribSMul G k
f g h : SkewMonoidAlgebra k G
⊢ (f.sum fun (a₁ : G) (b₁ : k) ↦ (g + h).sum fun (a₂ : G) (b₂ : k) ↦ single (a₁ * a₂) (b₁ * a₁ • b₂)) =
    HAdd.hAdd (α := SkewMonoidAlgebra k G)
      (f.sum fun (a₁ : G) (b₁ : k) ↦ g.sum fun (a₂ : G) (b₂ : k) ↦ single (a₁ * a₂) (b₁ * a₁ • b₂))
      (f.sum fun (a₁ : G) (b₁ : k) ↦ h.sum fun (a₂ : G) (b₂ : k) ↦ single (a₁ * a₂) (b₁ * a₁ • b₂))
have refine_1 : ∀ (x : G) (x_1 : k),
  ∀ a ∈ g.support ∪ h.support, Eq (α := SkewMonoidAlgebra k G) (single (x * a) (x_1 * HSMul.hSMul (β := k) x 0)) 0
Tactic: refine Eq.trans (congr_arg (sum f) (funext₂ fun _ _ ↦ sum_add_index ?_ ?_)) ?_
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Basic (goal)
Goal:
k : Type u_1
G : Type u_2
inst : Mul G
inst_1 : NonUnitalNonAssocSemiring k
inst_2 : DistribSMul G k
f g h : SkewMonoidAlgebra k G
refine_1 :
  ∀ (x : G) (x_1 : k),
    ∀ a ∈ g.support ∪ h.support, Eq (α := SkewMonoidAlgebra k G) (single (x * a) (x_1 * HSMul.hSMul (β := k) x 0)) 0
⊢ (f.sum fun (a₁ : G) (b₁ : k) ↦ (g + h).sum fun (a₂ : G) (b₂ : k) ↦ single (a₁ * a₂) (b₁ * a₁ • b₂)) =
    HAdd.hAdd (α := SkewMonoidAlgebra k G)
      (f.sum fun (a₁ : G) (b₁ : k) ↦ g.sum fun (a₂ : G) (b₂ : k) ↦ single (a₁ * a₂) (b₁ * a₁ • b₂))
      (f.sum fun (a₁ : G) (b₁ : k) ↦ h.sum fun (a₂ : G) (b₂ : k) ↦ single (a₁ * a₂) (b₁ * a₁ • b₂))
have refine_2 : ∀ (x : G) (x_1 : k),
  ∀ a ∈ g.support ∪ h.support,
    ∀ (b₁ b₂ : k),
      single (x * a) (x_1 * x • (b₁ + b₂)) =
        HAdd.hAdd (α := SkewMonoidAlgebra k G) (single (x * a) (x_1 * x • b₁)) (single (x * a) (x_1 * x • b₂))
Tactic: refine Eq.trans (congr_arg (sum f) (funext₂ fun _ _ ↦ sum_add_index ?_ ?_)) ?_
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Basic (goal)
Goal:
k : Type u_1
G : Type u_2
inst : Mul G
inst_1 : NonUnitalNonAssocSemiring k
inst_2 : DistribSMul G k
f g h : SkewMonoidAlgebra k G
refine_1 :
  ∀ (x : G) (x_1 : k),
    ∀ a ∈ g.support ∪ h.support, Eq (α := SkewMonoidAlgebra k G) (single (x * a) (x_1 * HSMul.hSMul (β := k) x 0)) 0
refine_2 :
  ∀ (x : G) (x_1 : k),
    ∀ a ∈ g.support ∪ h.support,
      ∀ (b₁ b₂ : k),
        single (x * a) (x_1 * x • (b₁ + b₂)) =
          HAdd.hAdd (α := SkewMonoidAlgebra k G) (single (x * a) (x_1 * x • b₁)) (single (x * a) (x_1 * x • b₂))
⊢ (f.sum fun (a₁ : G) (b₁ : k) ↦ (g + h).sum fun (a₂ : G) (b₂ : k) ↦ single (a₁ * a₂) (b₁ * a₁ • b₂)) =
    HAdd.hAdd (α := SkewMonoidAlgebra k G)
      (f.sum fun (a₁ : G) (b₁ : k) ↦ g.sum fun (a₂ : G) (b₂ : k) ↦ single (a₁ * a₂) (b₁ * a₁ • b₂))
      (f.sum fun (a₁ : G) (b₁ : k) ↦ h.sum fun (a₂ : G) (b₂ : k) ↦ single (a₁ * a₂) (b₁ * a₁ • b₂))
have refine_3 : (f.sum fun (x : G) (x_1 : k) ↦
    HAdd.hAdd (α := SkewMonoidAlgebra k G) (g.sum fun (a₂ : G) (b₂ : k) ↦ single (x * a₂) (x_1 * x • b₂))
      (h.sum fun (a₂ : G) (b₂ : k) ↦ single (x * a₂) (x_1 * x • b₂))) =
  HAdd.hAdd (α := SkewMonoidAlgebra k G)
    (f.sum fun (a₁ : G) (b₁ : k) ↦ g.sum fun (a₂ : G) (b₂ : k) ↦ single (a₁ * a₂) (b₁ * a₁ • b₂))
    (f.sum fun (a₁ : G) (b₁ : k) ↦ h.sum fun (a₂ : G) (b₂ : k) ↦ single (a₁ * a₂) (b₁ * a₁ • b₂))
Tactic: refine Eq.trans (congr_arg (sum f) (funext₂ fun _ _ ↦ sum_add_index ?_ ?_)) ?_
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Basic (goal)
Goal:
k : Type u_1
G : Type u_2
inst : Mul G
inst_1 : NonUnitalNonAssocSemiring k
inst_2 : DistribSMul G k
f g h : SkewMonoidAlgebra k G
⊢ f * (g + h) = f * g + f * h
have simp : (f.sum fun (a₁ : G) (b₁ : k) ↦ (g + h).sum fun (a₂ : G) (b₂ : k) ↦ single (a₁ * a₂) (b₁ * a₁ • b₂)) =
  HAdd.hAdd (α := SkewMonoidAlgebra k G)
    (f.sum fun (a₁ : G) (b₁ : k) ↦ g.sum fun (a₂ : G) (b₂ : k) ↦ single (a₁ * a₂) (b₁ * a₁ • b₂))
    (f.sum fun (a₁ : G) (b₁ : k) ↦ h.sum fun (a₂ : G) (b₂ : k) ↦ single (a₁ * a₂) (b₁ * a₁ • b₂))
Tactic: classical
    simp only [mul_def]
    refine Eq.trans (congr_arg (sum f) (funext₂ fun _ _ ↦ sum_add_index ?_ ?_)) ?_ <;>
      simp only [smul_zero, smul_add, mul_add, mul_zero, single_zero, single_add,
        forall_true_iff, sum_add]
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Basic (goal)
Goal:
k : Type u_1
G : Type u_2
inst : Mul G
inst_1 : NonUnitalNonAssocSemiring k
inst_2 : DistribSMul G k
f g h : SkewMonoidAlgebra k G
⊢ (f + g) * h = f * h + g * h
have simp : ((f + g).sum fun (a₁ : G) (b₁ : k) ↦ h.sum fun (a₂ : G) (b₂ : k) ↦ single (a₁ * a₂) (b₁ * a₁ • b₂)) =
  HAdd.hAdd (α := SkewMonoidAlgebra k G)
    (f.sum fun (a₁ : G) (b₁ : k) ↦ h.sum fun (a₂ : G) (b₂ : k) ↦ single (a₁ * a₂) (b₁ * a₁ • b₂))
    (g.sum fun (a₁ : G) (b₁ : k) ↦ h.sum fun (a₂ : G) (b₂ : k) ↦ single (a₁ * a₂) (b₁ * a₁ • b₂))
Tactic: simp only [mul_def]
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Basic (goal)
Goal:
k : Type u_1
G : Type u_2
inst : Mul G
inst_1 : NonUnitalNonAssocSemiring k
inst_2 : DistribSMul G k
f g h : SkewMonoidAlgebra k G
⊢ ((f + g).sum fun (a₁ : G) (b₁ : k) ↦ h.sum fun (a₂ : G) (b₂ : k) ↦ single (a₁ * a₂) (b₁ * a₁ • b₂)) =
    HAdd.hAdd (α := SkewMonoidAlgebra k G)
      (f.sum fun (a₁ : G) (b₁ : k) ↦ h.sum fun (a₂ : G) (b₂ : k) ↦ single (a₁ * a₂) (b₁ * a₁ • b₂))
      (g.sum fun (a₁ : G) (b₁ : k) ↦ h.sum fun (a₂ : G) (b₂ : k) ↦ single (a₁ * a₂) (b₁ * a₁ • b₂))
have refine_1 : ∀ a ∈ f.support ∪ g.support,
  Eq (α := SkewMonoidAlgebra k G) (h.sum fun (a₂ : G) (b₂ : k) ↦ single (a * a₂) (0 * a • b₂)) 0
Tactic: refine Eq.trans (sum_add_index ?_ ?_) ?_
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Basic (goal)
Goal:
k : Type u_1
G : Type u_2
inst : Mul G
inst_1 : NonUnitalNonAssocSemiring k
inst_2 : DistribSMul G k
f g h : SkewMonoidAlgebra k G
refine_1 :
  ∀ a ∈ f.support ∪ g.support,
    Eq (α := SkewMonoidAlgebra k G) (h.sum fun (a₂ : G) (b₂ : k) ↦ single (a * a₂) (0 * a • b₂)) 0
⊢ ((f + g).sum fun (a₁ : G) (b₁ : k) ↦ h.sum fun (a₂ : G) (b₂ : k) ↦ single (a₁ * a₂) (b₁ * a₁ • b₂)) =
    HAdd.hAdd (α := SkewMonoidAlgebra k G)
      (f.sum fun (a₁ : G) (b₁ : k) ↦ h.sum fun (a₂ : G) (b₂ : k) ↦ single (a₁ * a₂) (b₁ * a₁ • b₂))
      (g.sum fun (a₁ : G) (b₁ : k) ↦ h.sum fun (a₂ : G) (b₂ : k) ↦ single (a₁ * a₂) (b₁ * a₁ • b₂))
have refine_2 : ∀ a ∈ f.support ∪ g.support,
  ∀ (b₁ b₂ : k),
    (h.sum fun (a₂ : G) (b₂_1 : k) ↦ single (a * a₂) ((b₁ + b₂) * a • b₂_1)) =
      HAdd.hAdd (α := SkewMonoidAlgebra k G) (h.sum fun (a₂ : G) (b₂ : k) ↦ single (a * a₂) (b₁ * a • b₂))
        (h.sum fun (a₂ : G) (b₂_1 : k) ↦ single (a * a₂) (b₂ * a • b₂_1))
Tactic: refine Eq.trans (sum_add_index ?_ ?_) ?_
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Basic (goal)
Goal:
k : Type u_1
G : Type u_2
inst : Mul G
inst_1 : NonUnitalNonAssocSemiring k
inst_2 : DistribSMul G k
f g h : SkewMonoidAlgebra k G
refine_1 :
  ∀ a ∈ f.support ∪ g.support,
    Eq (α := SkewMonoidAlgebra k G) (h.sum fun (a₂ : G) (b₂ : k) ↦ single (a * a₂) (0 * a • b₂)) 0
refine_2 :
  ∀ a ∈ f.support ∪ g.support,
    ∀ (b₁ b₂ : k),
      (h.sum fun (a₂ : G) (b₂_1 : k) ↦ single (a * a₂) ((b₁ + b₂) * a • b₂_1)) =
        HAdd.hAdd (α := SkewMonoidAlgebra k G) (h.sum fun (a₂ : G) (b₂ : k) ↦ single (a * a₂) (b₁ * a • b₂))
          (h.sum fun (a₂ : G) (b₂_1 : k) ↦ single (a * a₂) (b₂ * a • b₂_1))
⊢ ((f + g).sum fun (a₁ : G) (b₁ : k) ↦ h.sum fun (a₂ : G) (b₂ : k) ↦ single (a₁ * a₂) (b₁ * a₁ • b₂)) =
    HAdd.hAdd (α := SkewMonoidAlgebra k G)
      (f.sum fun (a₁ : G) (b₁ : k) ↦ h.sum fun (a₂ : G) (b₂ : k) ↦ single (a₁ * a₂) (b₁ * a₁ • b₂))
      (g.sum fun (a₁ : G) (b₁ : k) ↦ h.sum fun (a₂ : G) (b₂ : k) ↦ single (a₁ * a₂) (b₁ * a₁ • b₂))
have refine_3 : HAdd.hAdd (α := SkewMonoidAlgebra k G)
    (f.sum fun (a₁ : G) (b₁ : k) ↦ h.sum fun (a₂ : G) (b₂ : k) ↦ single (a₁ * a₂) (b₁ * a₁ • b₂))
    (g.sum fun (a₁ : G) (b₁ : k) ↦ h.sum fun (a₂ : G) (b₂ : k) ↦ single (a₁ * a₂) (b₁ * a₁ • b₂)) =
  HAdd.hAdd (α := SkewMonoidAlgebra k G)
    (f.sum fun (a₁ : G) (b₁ : k) ↦ h.sum fun (a₂ : G) (b₂ : k) ↦ single (a₁ * a₂) (b₁ * a₁ • b₂))
    (g.sum fun (a₁ : G) (b₁ : k) ↦ h.sum fun (a₂ : G) (b₂ : k) ↦ single (a₁ * a₂) (b₁ * a₁ • b₂))
Tactic: refine Eq.trans (sum_add_index ?_ ?_) ?_
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Basic (goal)
Goal:
k : Type u_1
G : Type u_2
inst : Mul G
inst_1 : NonUnitalNonAssocSemiring k
inst_2 : DistribSMul G k
f g h : SkewMonoidAlgebra k G
⊢ (f + g) * h = f * h + g * h
have simp : ((f + g).sum fun (a₁ : G) (b₁ : k) ↦ h.sum fun (a₂ : G) (b₂ : k) ↦ single (a₁ * a₂) (b₁ * a₁ • b₂)) =
  HAdd.hAdd (α := SkewMonoidAlgebra k G)
    (f.sum fun (a₁ : G) (b₁ : k) ↦ h.sum fun (a₂ : G) (b₂ : k) ↦ single (a₁ * a₂) (b₁ * a₁ • b₂))
    (g.sum fun (a₁ : G) (b₁ : k) ↦ h.sum fun (a₂ : G) (b₂ : k) ↦ single (a₁ * a₂) (b₁ * a₁ • b₂))
Tactic: classical
    simp only [mul_def]
    refine Eq.trans (sum_add_index ?_ ?_) ?_ <;>
      simp only [add_mul, zero_mul, single_zero, single_add, forall_true_iff, sum_zero, sum_add]
-- 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)
| HMul.hMul (α := R) (β := R) ((liftNC (↑f : k →+ R) (⇑g : (a : G) → R) : (a : SkewMonoidAlgebra k G) → R) a : R)
    ((liftNC (↑f : k →+ R) (⇑g : (a : G) → R) : (a : SkewMonoidAlgebra k G) → R) b : R)
have rw : 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: rw [← sum_single a, ← sum_single b]
-- 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)
⊢ (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 : R)
      ((liftNC (↑f : k →+ R) (⇑g : (a : G) → R) : (a : SkewMonoidAlgebra k G) → R) b : R)
have conv_rhs : (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: conv_rhs => rw [← sum_single a, ← sum_single b]
-- 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)
⊢ (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)
have 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))
Tactic: simp_rw [mul_def, map_sum, liftNC_single, sum_mul, mul_sum]
-- 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)
⊢ 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))
have 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)
Tactic: refine sum_congr fun y hy ↦ sum_congr fun x _hx ↦ ?_
-- 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
⊢ 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)
have 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)
Tactic: simp only [AddMonoidHom.coe_coe, map_mul]
-- 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
⊢ 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) ((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)
Tactic: rw [mul_assoc, ← mul_assoc (f (y • b.coeff x)), h_comm hy, mul_assoc, mul_assoc]