awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : AddCommMonoid k
G' : Type u_3
f : G → G'
v : SkewMonoidAlgebra k G
k' : Type u_5
inst_1 : AddCommMonoid k'
h : G' → k → k'
h_zero : ∀ (b : G'), h b 0 = 0
h_add : ∀ (b : G') (m₁ m₂ : k), h b (m₁ + m₂) = h b m₁ + h b m₂
⊢ sum ((mapDomain f : (a : SkewMonoidAlgebra k G) → SkewMonoidAlgebra k G') v) h = v.sum fun (a : G) (m : k) ↦ h (f a) m

Tactic:
(sum_sum_index h_zero h_add).trans <| sum_congr fun _ _ ↦ sum_single_index (h_zero _)

Premises used: Multiset.sum, Multiset.foldr, Finsupp.sum, SkewMonoidAlgebra.sum_sum_index, SkewMonoidAlgebra.sum_congr, SkewMonoidAlgebra.sum, Finset.sum, Eq.trans, SkewMonoidAlgebra.sum_single_index
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : AddCommMonoid k
G' : Type u_3
f : G → G'
a : G
b : k
⊢ Eq (α := SkewMonoidAlgebra k G')
    ((mapDomain f : (a : SkewMonoidAlgebra k G) → SkewMonoidAlgebra k G') (single a b) : SkewMonoidAlgebra k G')
    (single (f a) b : SkewMonoidAlgebra k G')

Tactic:
sum_single_index <| single_zero _

Premises used: Multiset.sum, Multiset.foldr, Finsupp.sum, SkewMonoidAlgebra.single_zero, SkewMonoidAlgebra.sum, Finset.sum, SkewMonoidAlgebra.sum_single_index
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
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
simp_rw : Finsupp.mapDomain f (b • v).toFinsupp = b • Finsupp.mapDomain f v.toFinsupp
⊢ (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')

Tactic:
simp_rw [← toFinsupp_inj, toFinsupp_smul, toFinsupp_mapDomain]

Premises used: SkewMonoidAlgebra.toFinsupp_smul, SkewMonoidAlgebra.toFinsupp_mapDomain, SkewMonoidAlgebra.toFinsupp_inj
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
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
⊢ Finsupp.mapDomain f (b • v).toFinsupp = b • Finsupp.mapDomain f v.toFinsupp

Tactic:
simp [Finsupp.mapDomain_smul]

Premises used: Finsupp.mapDomain_smul
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
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
a : G
b : k
⊢ (liftNC f g : (a : SkewMonoidAlgebra k G) → R) (single a b) = HMul.hMul (α := R) ((f : (a : k) → R) b : R) (g a)

Tactic:
Finsupp.liftAddHom_apply_single _ _ _

Premises used: Multiset.sum, Multiset.foldr, Finsupp.sum, Finsupp.liftAddHom_apply_single, Finset.sum
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
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)
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)
⊢ l = liftNC f g

Tactic:
ext a b
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
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)
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:
simp_all
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : AddGroup k
a : G →₀ k
⊢ { toFinsupp := -a : SkewMonoidAlgebra k G } = -{ toFinsupp := a }

Tactic:
(rfl)

Premises used: rfl
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : AddGroup k
a : SkewMonoidAlgebra k G
ofFinsupp :
  ∀ (toFinsupp : G →₀ k),
    -{ toFinsupp := toFinsupp : SkewMonoidAlgebra k G } + { toFinsupp := toFinsupp : SkewMonoidAlgebra k G } = 0
⊢ -a + a = 0

Tactic:
cases a
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : AddGroup k
toFinsupp : G →₀ k
⊢ -{ toFinsupp := toFinsupp : SkewMonoidAlgebra k G } + { toFinsupp := toFinsupp : SkewMonoidAlgebra k G } = 0

Tactic:
simp [← ofFinsupp_neg, ← ofFinsupp_add]

Premises used: SkewMonoidAlgebra.ofFinsupp_neg, SkewMonoidAlgebra.ofFinsupp_add
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : AddGroup k
a : SkewMonoidAlgebra k G
⊢ (-a).toFinsupp = -a.toFinsupp

Tactic:
toFinsuppAddEquiv.map_neg a

Premises used: Finsupp.onFinset, Finsupp.mapRange, AddEquiv.map_neg
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : AddGroup k
a b : G →₀ k
⊢ { toFinsupp := a - b : SkewMonoidAlgebra k G } =
    { toFinsupp := a : SkewMonoidAlgebra k G } - { toFinsupp := b : SkewMonoidAlgebra k G }

Tactic:
toFinsuppAddEquiv.symm.map_sub a b

Premises used: AddEquiv.map_sub
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : AddGroup k
a b : SkewMonoidAlgebra k G
⊢ (a - b).toFinsupp = a.toFinsupp - b.toFinsupp

Tactic:
toFinsuppAddEquiv.map_sub a b

Premises used: Finsupp.onFinset, Finsupp.zipWith, AddEquiv.map_sub
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : AddGroup k
a : G
b : k
⊢ Eq (α := SkewMonoidAlgebra k G) (single a (-b)) (-single a b)

Tactic:
simp [← ofFinsupp_single]

Premises used: SkewMonoidAlgebra.ofFinsupp_single
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
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))
negSucc :
  ∀ (a : ℕ),
    Eq (α := SkewMonoidAlgebra k G) (↑(Int.negSucc a) : SkewMonoidAlgebra k G) (single 1 (↑(Int.negSucc a) : k))
⊢ Eq (α := SkewMonoidAlgebra k G) (↑z : SkewMonoidAlgebra k G) (single 1 (↑z : k))

Tactic:
cases z
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : AddGroupWithOne k
inst_1 : One G
a : ℕ
⊢ Eq (α := SkewMonoidAlgebra k G) (↑(Int.ofNat a) : SkewMonoidAlgebra k G) (single 1 (↑(Int.ofNat a) : k))

Tactic:
simp
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : AddGroupWithOne k
inst_1 : One G
a : ℕ
⊢ Eq (α := SkewMonoidAlgebra k G) (↑(Int.negSucc a) : SkewMonoidAlgebra k G) (single 1 (↑(Int.negSucc a) : k))

Tactic:
simp
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
N : Type u_3
inst : AddCommMonoid N
inst_1 : NonUnitalNonAssocSemiring k
g : SkewMonoidAlgebra k G
b : k
h : G → k → N
h0 : ∀ (i : G), h i 0 = 0
⊢ (b • g).sum h = g.sum fun (x1 : G) (x2 : k) ↦ h x1 (b * x2)

Tactic:
simp [sum_def, Finsupp.sum_smul_index' h0]

Premises used: Finsupp.sum_smul_index', SkewMonoidAlgebra.sum_def
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
N : Type u_3
R : Type u_4
inst : AddCommMonoid k
inst_1 : DistribSMul R k
inst_2 : AddCommMonoid N
g : SkewMonoidAlgebra k G
b : R
h : G → k → N
h0 : ∀ (i : G), h i 0 = 0
⊢ (b • g).sum h = g.sum fun (x1 : G) (x2 : k) ↦ h x1 (b • x2)

Tactic:
simp only [sum_def, toFinsupp_smul, Finsupp.sum_smul_index' h0]

Premises used: SkewMonoidAlgebra.toFinsupp_smul, Finsupp.sum_smul_index', SkewMonoidAlgebra.sum_def
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
g_hom : Type u_3
R : Type u_4
inst : NonAssocSemiring k
inst_1 : One G
inst_2 : Semiring R
inst_3 : FunLike g_hom G R
inst_4 : OneHomClass g_hom G R
f : k →+* R
g : g_hom
⊢ Eq.{u_4 + 1} (α := R) ((liftNC (↑f : k →+ R) (⇑g : (a : G) → R) : (a : SkewMonoidAlgebra k G) → R) 1 : R) (1 : R)

Tactic:
simp only [one_def, liftNC_single, AddMonoidHom.coe_coe, map_one, mul_one]

Premises used: SkewMonoidAlgebra.one_def, AddMonoidHom.coe_coe, map_one, SkewMonoidAlgebra.liftNC_single, mul_one
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : Mul G
inst_1 : SMul G k
inst_2 : NonUnitalNonAssocSemiring k
f g : SkewMonoidAlgebra k G
⊢ f * g = f.sum fun (a₁ : G) (b₁ : k) ↦ g.sum fun (a₂ : G) (b₂ : k) ↦ single (a₁ * a₂) (b₁ * a₁ • b₂)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
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
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₂))
⊢ f * (g + h) = f * g + f * h

Tactic:
simp only [mul_def]

Premises used: SkewMonoidAlgebra.mul_def
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
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₂))

Tactic:
Eq.trans (congr_arg (sum f) (funext₂ fun _ _ ↦ sum_add_index ?_ ?_)) ?_

Premises used: SkewMonoidAlgebra.sum_add_index, congr_arg, funext₂, SkewMonoidAlgebra.sum, Eq.trans
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
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₂))
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₂))
⊢ (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:
refine Eq.trans (congr_arg (sum f) (funext₂ fun _ _ ↦ sum_add_index ?_ ?_)) ?_

Premises used: SkewMonoidAlgebra.sum_add_index, congr_arg, funext₂, SkewMonoidAlgebra.sum, Eq.trans
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
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
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:
simp only [smul_zero, smul_add, mul_add, mul_zero, single_zero, single_add,
        forall_true_iff, sum_add]

Premises used: smul_zero, SkewMonoidAlgebra.single_zero, MulZeroClass.mul_zero, SkewMonoidAlgebra.single_add, mul_add, forall_true_iff, SkewMonoidAlgebra.sum_add, smul_add
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
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
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:
simp only [smul_zero, smul_add, mul_add, mul_zero, single_zero, single_add,
        forall_true_iff, sum_add]

Premises used: smul_zero, SkewMonoidAlgebra.single_zero, MulZeroClass.mul_zero, SkewMonoidAlgebra.single_add, mul_add, forall_true_iff, SkewMonoidAlgebra.sum_add, smul_add
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
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 (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:
simp only [smul_zero, smul_add, mul_add, mul_zero, single_zero, single_add,
        forall_true_iff, sum_add]

Premises used: smul_zero, SkewMonoidAlgebra.single_zero, MulZeroClass.mul_zero, SkewMonoidAlgebra.single_add, mul_add, forall_true_iff, SkewMonoidAlgebra.sum_add, smul_add
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
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
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₂))
⊢ f * (g + h) = f * g + f * h

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]

Premises used: SkewMonoidAlgebra.sum_add_index, smul_zero, SkewMonoidAlgebra.single_zero, MulZeroClass.mul_zero, congr_arg, SkewMonoidAlgebra.single_add, funext₂, mul_add, forall_true_iff, SkewMonoidAlgebra.sum_add, SkewMonoidAlgebra.sum, smul_add, Eq.trans, SkewMonoidAlgebra.mul_def
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
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
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₂))
⊢ (f + g) * h = f * h + g * h

Tactic:
simp only [mul_def]

Premises used: SkewMonoidAlgebra.mul_def
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
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₂))

Tactic:
Eq.trans (sum_add_index ?_ ?_) ?_

Premises used: SkewMonoidAlgebra.sum_add_index, Eq.trans
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
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))
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₂))
⊢ ((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:
refine Eq.trans (sum_add_index ?_ ?_) ?_

Premises used: SkewMonoidAlgebra.sum_add_index, Eq.trans
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
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
⊢ ∀ a ∈ f.support ∪ g.support,
    Eq (α := SkewMonoidAlgebra k G) (h.sum fun (a₂ : G) (b₂ : k) ↦ single (a * a₂) (0 * a • b₂)) 0

Tactic:
simp only [add_mul, zero_mul, single_zero, single_add, forall_true_iff, sum_zero, sum_add]

Premises used: add_mul, MulZeroClass.zero_mul, SkewMonoidAlgebra.single_zero, SkewMonoidAlgebra.single_add, forall_true_iff, SkewMonoidAlgebra.sum_add, SkewMonoidAlgebra.sum_zero
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
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
⊢ ∀ 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:
simp only [add_mul, zero_mul, single_zero, single_add, forall_true_iff, sum_zero, sum_add]

Premises used: add_mul, MulZeroClass.zero_mul, SkewMonoidAlgebra.single_zero, SkewMonoidAlgebra.single_add, forall_true_iff, SkewMonoidAlgebra.sum_add, SkewMonoidAlgebra.sum_zero
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
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
⊢ 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:
simp only [add_mul, zero_mul, single_zero, single_add, forall_true_iff, sum_zero, sum_add]

Premises used: add_mul, MulZeroClass.zero_mul, SkewMonoidAlgebra.single_zero, SkewMonoidAlgebra.single_add, forall_true_iff, SkewMonoidAlgebra.sum_add, SkewMonoidAlgebra.sum_zero
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
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
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₂))
⊢ (f + g) * h = f * h + g * h

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]

Premises used: SkewMonoidAlgebra.sum_add_index, add_mul, MulZeroClass.zero_mul, SkewMonoidAlgebra.single_zero, SkewMonoidAlgebra.single_add, forall_true_iff, SkewMonoidAlgebra.sum_add, SkewMonoidAlgebra.sum_zero, Eq.trans, 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)
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)
| 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)

Tactic:
rw [← sum_single a, ← sum_single b]

Premises used: SkewMonoidAlgebra.sum_single
-- 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)
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)
⊢ (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)

Tactic:
conv_rhs => rw [← sum_single a, ← sum_single b]

Premises used: SkewMonoidAlgebra.sum_single