awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : Mul G
inst_2 : SMulZeroClass G k
f : SkewMonoidAlgebra k G
r : k
x y z : G
H : ∀ (a : G), x * a = y ↔ a = z
this : Eq (α := k) (f.sum fun (a : G) (b : k) ↦ if x * a = y then 0 * x • b else 0) 0
h : f.coeff z = 0
⊢ 0 = r * x • f.coeff z

Tactic:
simp [h]
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : Mul G
inst_2 : SMulZeroClass G k
f : SkewMonoidAlgebra k G
r : k
x y z : G
H : ∀ (a : G), x * a = y ↔ a = z
this : Eq (α := k) (f.sum fun (a : G) (b : k) ↦ if x * a = y then 0 * x • b else 0) 0
x₁ :
  Eq (α := k) (f.sum fun (a : G) (b : k) ↦ if x * a = y then r * x • b else 0)
    (f.sum fun (a : G) (b : k) ↦ if a = z then r * x • b else 0)
x₂ : (if z ∈ f.support then r * x • f.coeff z else 0) = r * x • f.coeff z
⊢ (single x r * f).coeff y = r * x • f.coeff z

Tactic:
calc
    (single x r * f).coeff y =
        sum f fun a b ↦ ite (x * a = y) (r * x • b) 0 :=
      (coeff_mul _ _ _).trans <| sum_single_index this
    _ = f.sum fun a b ↦ ite (a = z) (r * x • b) 0 := by simp [H]
    _ = if z ∈ f.support then r * x • f.coeff z else 0 := (f.support.sum_ite_eq' _ _)
    _ = _ := by split_ifs with h <;> simp [support] at h <;> simp [h]

Premises used: HMul.hMul, Finset.sum_ite_eq', SkewMonoidAlgebra.coeff_mul, SkewMonoidAlgebra.support, HSMul.hSMul, OfNat.ofNat, SkewMonoidAlgebra.single, Eq, SkewMonoidAlgebra.sum, Eq.trans, SkewMonoidAlgebra.coeff, SkewMonoidAlgebra.sum_single_index, ite
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : Mul G
inst_2 : SMulZeroClass G k
f : SkewMonoidAlgebra k G
r : k
x y z : G
H : ∀ (a : G), x * a = y ↔ a = z
have : Eq (α := k) (f.sum fun (a : G) (b : k) ↦ if x * a = y then 0 * x • b else 0) 0
have₁ :
  ∀ (this : Eq (α := k) (f.sum fun (a : G) (b : k) ↦ if x * a = y then 0 * x • b else 0) 0),
    (single x r * f).coeff y = r * x • f.coeff z
have₂ : Eq (α := k) (f.sum fun (a : G) (b : k) ↦ if x * a = y then 0 * x • b else 0) 0
have₃ have₄ :
  ∀ (this : Eq (α := k) (f.sum fun (a : G) (b : k) ↦ if x * a = y then 0 * x • b else 0) 0),
    (single x r * f).coeff y = r * x • f.coeff z
⊢ (single x r * f).coeff y = r * x • f.coeff z

Tactic:
classical
  have : (f.sum fun a b ↦ ite (x * a = y) (0 * x • b) 0) = 0 := by simp
  calc
    (single x r * f).coeff y =
        sum f fun a b ↦ ite (x * a = y) (r * x • b) 0 :=
      (coeff_mul _ _ _).trans <| sum_single_index this
    _ = f.sum fun a b ↦ ite (a = z) (r * x • b) 0 := by simp [H]
    _ = if z ∈ f.support then r * x • f.coeff z else 0 := (f.support.sum_ite_eq' _ _)
    _ = _ := by split_ifs with h <;> simp [support] at h <;> simp [h]

Premises used: HMul.hMul, SkewMonoidAlgebra.coeff_mul, SkewMonoidAlgebra.support, SkewMonoidAlgebra.single, Eq.trans, SkewMonoidAlgebra.coeff
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : Mul G
inst_2 : SMulZeroClass G k
r : k
g g' : G
x : SkewMonoidAlgebra k G
h : ¬∃ (d : G), g' = g * d
rw : Eq (α := k) (x.sum fun (a₂ : G) (b₂ : k) ↦ if g * a₂ = g' then r * g • b₂ else 0) 0
rw₁ : Eq (α := k) (x.sum fun (a₂ : G) (b₂ : k) ↦ if g * a₂ = g' then 0 * g • b₂ else 0) 0
⊢ (single g r * x).coeff g' = 0

Tactic:
rw [coeff_mul, sum_single_index]

Premises used: SkewMonoidAlgebra.coeff_mul, SkewMonoidAlgebra.sum_single_index
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : Mul G
inst_2 : SMulZeroClass G k
r : k
g g' : G
x : SkewMonoidAlgebra k G
h : ¬∃ (d : G), g' = g * d
h₁ :
  ∀ x_1 ∈ x.toFinsupp.support,
    Eq.{u_1 + 1} (α := k)
      ((fun (a₂ : G) (b₂ : k) ↦ if g * a₂ = g' then r * g • b₂ else 0) x_1 ((x.toFinsupp : (a : G) → k) x_1)) 0
⊢ Eq (α := k) (x.sum fun (a₂ : G) (b₂ : k) ↦ if g * a₂ = g' then r * g • b₂ else 0) 0

Tactic:
apply Finset.sum_eq_zero

Premises used: Finset.sum_eq_zero
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : Mul G
inst_2 : SMulZeroClass G k
r : k
g g' : G
x : SkewMonoidAlgebra k G
h : ¬∃ (d : G), g' = g * d
h₁ : ∀ x_1 ∈ x.toFinsupp.support, g * x_1 = g' → r * HSMul.hSMul (β := k) g ((x.toFinsupp : (a : G) → k) x_1 : k) = 0
⊢ ∀ x_1 ∈ x.toFinsupp.support,
    Eq.{u_1 + 1} (α := k)
      ((fun (a₂ : G) (b₂ : k) ↦ if g * a₂ = g' then r * g • b₂ else 0) x_1 ((x.toFinsupp : (a : G) → k) x_1)) 0

Tactic:
simp_rw [ite_eq_right_iff]

Premises used: ite_eq_right_iff
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : Mul G
inst_2 : SMulZeroClass G k
r : k
g : G
x : SkewMonoidAlgebra k G
g'' : G
_hg'' : g'' ∈ x.toFinsupp.support
h : ¬∃ (d : G), g * g'' = g * d
⊢ r * HSMul.hSMul (β := k) g ((x.toFinsupp : (a : G) → k) g'' : k) = 0

Tactic:
absurd ⟨_, rfl⟩ h

Premises used: absurd
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : Mul G
inst_2 : SMulZeroClass G k
r : k
g : G
x : SkewMonoidAlgebra k G
g'' : G
_hg'' : g'' ∈ x.toFinsupp.support
h : ¬∃ (d : G), g * g'' = g * d
⊢ r * HSMul.hSMul (β := k) g ((x.toFinsupp : (a : G) → k) g'' : k) = 0

Tactic:
exact absurd ⟨_, rfl⟩ h

Premises used: absurd
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : Mul G
inst_2 : SMulZeroClass G k
r : k
g g' : G
x : SkewMonoidAlgebra k G
h : ¬∃ (d : G), g' = g * d
⊢ Eq (α := k) (x.sum fun (a₂ : G) (b₂ : k) ↦ if g * a₂ = g' then 0 * g • b₂ else 0) 0

Tactic:
simp
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : Mul G
inst_2 : SMulZeroClass G k
r : k
g g' : G
x : SkewMonoidAlgebra k G
h : ¬∃ (d : G), g' = g * d
rw :
  Eq (α := k)
    (sum (single g r) fun (a₁ : G) (b₁ : k) ↦ x.sum fun (a₂ : G) (b₂ : k) ↦ if a₁ * a₂ = g' then b₁ * a₁ • b₂ else 0) 0
rw₁ : Eq (α := k) (x.sum fun (a₂ : G) (b₂ : k) ↦ if g * a₂ = g' then r * g • b₂ else 0) 0
rw₂ : Eq (α := k) (x.sum fun (a₂ : G) (b₂ : k) ↦ if g * a₂ = g' then 0 * g • b₂ else 0) 0
rw₃ : Eq (α := k) (x.sum fun (a₂ : G) (b₂ : k) ↦ if g * a₂ = g' then r * g • b₂ else 0) 0
rw₄ : Eq (α := k) (x.sum fun (a₂ : G) (b₂ : k) ↦ if g * a₂ = g' then 0 * g • b₂ else 0) 0
rw₅ : Eq (α := k) (x.sum fun (a₂ : G) (b₂ : k) ↦ if g * a₂ = g' then r * g • b₂ else 0) 0
rw₆ rw₇ : Eq (α := k) (x.sum fun (a₂ : G) (b₂ : k) ↦ if g * a₂ = g' then 0 * g • b₂ else 0) 0
⊢ (single g r * x).coeff g' = 0

Tactic:
classical
  rw [coeff_mul, sum_single_index]
  · apply Finset.sum_eq_zero
    simp_rw [ite_eq_right_iff]
    rintro g'' _hg'' rfl
    exact absurd ⟨_, rfl⟩ h
  · simp

Premises used: Finset.sum_eq_zero, SkewMonoidAlgebra.coeff_mul, absurd, ite_eq_right_iff, rfl, SkewMonoidAlgebra.sum_single_index
-- 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
r : k
x a : G
rw rw₁ : a = x ↔ a = x
⊢ a * 1 = x ↔ a = x

Tactic:
rw [mul_one]

Premises used: mul_one
-- 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
r : k
x : G
⊢ (single 1 r * f).coeff x = r * f.coeff x

Tactic:
simp [coeff_single_mul_aux, one_smul]

Premises used: one_smul, SkewMonoidAlgebra.coeff_single_mul_aux
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : Group G
inst_2 : MulSemiringAction G k
f : SkewMonoidAlgebra k G
r : k
x y : G
⊢ (f * single x r).coeff y = f.coeff (y * x⁻¹) * (y * x⁻¹) • r

Tactic:
f.coeff_mul_single_aux fun _a ↦ eq_mul_inv_iff_mul_eq.symm

Premises used: eq_mul_inv_iff_mul_eq, SkewMonoidAlgebra.coeff_mul_single_aux, Iff.symm
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : Group G
inst_2 : MulSemiringAction G k
r : k
x : G
f : SkewMonoidAlgebra k G
y : G
⊢ (single x r * f).coeff y = r * x • f.coeff (x⁻¹ * y)

Tactic:
f.coeff_single_mul_aux fun _z ↦ eq_inv_mul_iff_mul_eq.symm

Premises used: eq_inv_mul_iff_mul_eq, SkewMonoidAlgebra.coeff_single_mul_aux, Iff.symm
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : Group G
inst_2 : MulSemiringAction G k
f g : SkewMonoidAlgebra k G
x : G
rw : (f * g).coeff x = coeff (f.sum fun (a : G) (b : k) ↦ single a b * g) x
rw₁ : (f * g).coeff x = (f.sum single * g).coeff x
rw₂ rw₃ : (f * g).coeff x = (f * g).coeff x
⊢ (f * g).coeff x = f.sum fun (a : G) (b : k) ↦ (single a b * g).coeff x

Tactic:
rw [← coeff_sum, ← sum_mul g f, f.sum_single]

Premises used: SkewMonoidAlgebra.coeff_sum, SkewMonoidAlgebra.sum_single, SkewMonoidAlgebra.sum_mul
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : Group G
inst_2 : MulSemiringAction G k
f g : SkewMonoidAlgebra k G
x : G
⊢ Eq (α := k) (f.sum fun (a : G) (b : k) ↦ (single a b * g).coeff x)
    (f.sum fun (a : G) (b : k) ↦ b * a • g.coeff (a⁻¹ * x))

Tactic:
simp
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : Group G
inst_2 : MulSemiringAction G k
f g : SkewMonoidAlgebra k G
x : G
rw : (f * g).coeff x = coeff (g.sum fun (a : G) (b : k) ↦ f * single a b) x
rw₁ : (f * g).coeff x = (f * g.sum single).coeff x
rw₂ rw₃ : (f * g).coeff x = (f * g).coeff x
⊢ (f * g).coeff x = g.sum fun (a : G) (b : k) ↦ (f * single a b).coeff x

Tactic:
rw [← coeff_sum, ← mul_sum f g, g.sum_single]

Premises used: SkewMonoidAlgebra.coeff_sum, SkewMonoidAlgebra.sum_single, SkewMonoidAlgebra.mul_sum
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : Group G
inst_2 : MulSemiringAction G k
f g : SkewMonoidAlgebra k G
x : G
⊢ Eq (α := k) (g.sum fun (a : G) (b : k) ↦ (f * single a b).coeff x)
    (g.sum fun (a : G) (b : k) ↦ f.coeff (x * a⁻¹) * (x * a⁻¹) • b)

Tactic:
simp
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : AddCommMonoid k
N : Type u_3
inst_1 : AddZeroClass N
f g : SkewMonoidAlgebra k G →+ N
H : ∀ (x : G), f.comp (singleAddHom x) = g.comp (singleAddHom x)
⊢ f = g

Tactic:
addHom_ext fun x ↦ DFunLike.congr_fun (H x)

Premises used: DFunLike.congr_fun, SkewMonoidAlgebra.addHom_ext
-- 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
a₁ a₂ : G
b₁ b₂ : k
⊢ Eq (α := SkewMonoidAlgebra k G) (sum (single a₂ b₂) fun (a₂ : G) (b₂ : k) ↦ single (a₁ * a₂) (0 * a₁ • b₂)) 0

Tactic:
simp [zero_mul, single_zero, sum_zero]

Premises used: MulZeroClass.zero_mul, SkewMonoidAlgebra.single_zero, SkewMonoidAlgebra.sum_zero
-- 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
a₁ a₂ : G
b₁ b₂ : k
⊢ Eq (α := SkewMonoidAlgebra k G) (single (a₁ * a₂) (b₁ * HSMul.hSMul (β := k) a₁ 0)) 0

Tactic:
simp [smul_zero, mul_zero, single_zero]

Premises used: smul_zero, SkewMonoidAlgebra.single_zero, MulZeroClass.mul_zero
-- 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 y : k
⊢ ZeroHom.toFun (↑(singleAddHom 1) : ZeroHom k (SkewMonoidAlgebra k G)) (x * y) =
    HMul.hMul (α := SkewMonoidAlgebra k G) (ZeroHom.toFun (↑(singleAddHom 1) : ZeroHom k (SkewMonoidAlgebra k G)) x)
      (ZeroHom.toFun (↑(singleAddHom 1) : ZeroHom k (SkewMonoidAlgebra k G)) y)

Tactic:
simp [ZeroHom.toFun_eq_coe, AddMonoidHom.toZeroHom_coe, singleAddHom_apply,
    single_mul_single, mul_one, one_smul]

Premises used: AddMonoidHom.toZeroHom_coe, SkewMonoidAlgebra.single_mul_single, one_smul, mul_one, SkewMonoidAlgebra.singleAddHom_apply, ZeroHom.toFun_eq_coe
-- 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 →+* k
h₁ :
  ∀ (b : k),
    Eq.{u_1 + 1} (α := k) ((f : (a : SkewMonoidAlgebra k G) → k) (single 1 b) : k)
      ((g : (a : SkewMonoidAlgebra k G) → k) (single 1 b) : k)
h_of :
  ∀ (a : G),
    Eq.{u_1 + 1} (α := k) ((f : (a : SkewMonoidAlgebra k G) → k) (single a 1) : k)
      ((g : (a : SkewMonoidAlgebra k G) → k) (single a 1) : k)
a : G
b₁ b₂ : k
⊢ HMul.hMul (α := SkewMonoidAlgebra k G) (single 1 b₁) (single a b₂) = single a (b₁ * b₂)

Tactic:
simp [single_mul_single, one_mul, one_smul]

Premises used: SkewMonoidAlgebra.single_mul_single, one_smul, one_mul
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
α : Type u_3
α₂ : Type u_4
β : Type u_5
F : Type u_6
inst : Semiring β
inst_1 : Monoid α
inst_2 : Monoid α₂
inst_3 : FunLike F α α₂
inst_4 : MonoidHomClass F α α₂
f : F
simp_rw :
  Eq (α := SkewMonoidAlgebra β α₂)
    ((mapDomain (⇑f : (a : α) → α₂) : (a : SkewMonoidAlgebra β α) → SkewMonoidAlgebra β α₂) (single 1 1) :
      SkewMonoidAlgebra β α₂)
    (single 1 1 : SkewMonoidAlgebra β α₂)
simp_rw₁ :
  Eq (α := SkewMonoidAlgebra β α₂) (single ((f : (a : α) → α₂) 1) 1 : SkewMonoidAlgebra β α₂)
    (single 1 1 : SkewMonoidAlgebra β α₂)
⊢ Eq (α := SkewMonoidAlgebra β α₂)
    ((mapDomain (⇑f : (a : α) → α₂) : (a : SkewMonoidAlgebra β α) → SkewMonoidAlgebra β α₂) 1) 1

Tactic:
simp_rw [one_def, mapDomain_single, map_one]

Premises used: SkewMonoidAlgebra.mapDomain_single, SkewMonoidAlgebra.one_def, map_one
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
α : Type u_3
α₂ : Type u_4
β : Type u_5
F : Type u_6
inst : Semiring β
inst_1 : Monoid α
inst_2 : Monoid α₂
inst_3 : FunLike F α α₂
inst_4 : MulSemiringAction α β
inst_5 : MulSemiringAction α₂ β
inst_6 : MulHomClass F α α₂
f : F
x y : SkewMonoidAlgebra β α
hf : ∀ (a : α) (x : β), a • x = HSMul.hSMul.{u_4, u_5, u_5} (α := α₂) ((f : (a : α) → α₂) a : α₂) x
rw :
  (x.sum fun (a : α) (b : β) ↦
      (mapDomain (⇑f : (a : α) → α₂) : (a : SkewMonoidAlgebra β α) → SkewMonoidAlgebra β α₂)
        (y.sum fun (a₂ : α) (b₂ : β) ↦ single (a * a₂) (b * a • b₂))) =
    HMul.hMul (α := SkewMonoidAlgebra β α₂) (β := SkewMonoidAlgebra β α₂)
      ((mapDomain (⇑f : (a : α) → α₂) : (a : SkewMonoidAlgebra β α) → SkewMonoidAlgebra β α₂) x :
        SkewMonoidAlgebra β α₂)
      ((mapDomain (⇑f : (a : α) → α₂) : (a : SkewMonoidAlgebra β α) → SkewMonoidAlgebra β α₂) y :
        SkewMonoidAlgebra β α₂)
⊢ (mapDomain (⇑f : (a : α) → α₂) : (a : SkewMonoidAlgebra β α) → SkewMonoidAlgebra β α₂) (x * y) =
    HMul.hMul (α := SkewMonoidAlgebra β α₂) (β := SkewMonoidAlgebra β α₂)
      ((mapDomain (⇑f : (a : α) → α₂) : (a : SkewMonoidAlgebra β α) → SkewMonoidAlgebra β α₂) x :
        SkewMonoidAlgebra β α₂)
      ((mapDomain (⇑f : (a : α) → α₂) : (a : SkewMonoidAlgebra β α) → SkewMonoidAlgebra β α₂) y :
        SkewMonoidAlgebra β α₂)

Tactic:
rw [mul_def, map_sum]

Premises used: SkewMonoidAlgebra.map_sum, SkewMonoidAlgebra.mul_def
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
α : Type u_3
α₂ : Type u_4
β : Type u_5
F : Type u_6
inst : Semiring β
inst_1 : Monoid α
inst_2 : Monoid α₂
inst_3 : FunLike F α α₂
inst_4 : MulSemiringAction α β
inst_5 : MulSemiringAction α₂ β
inst_6 : MulHomClass F α α₂
f : F
x y : SkewMonoidAlgebra β α
hf : ∀ (a : α) (x : β), a • x = HSMul.hSMul.{u_4, u_5, u_5} (α := α₂) ((f : (a : α) → α₂) a : α₂) x
simp_rw :
  Eq (α := SkewMonoidAlgebra β α₂)
    (x.sum fun (a : α) (b : β) ↦
      y.sum fun (a₂ : α) (b₂ : β) ↦
        single (HMul.hMul (α := α₂) (β := α₂) ((f : (a : α) → α₂) a : α₂) ((f : (a : α) → α₂) a₂ : α₂)) (b * a • b₂))
    (sum ((mapDomain (⇑f : (a : α) → α₂) : (a : SkewMonoidAlgebra β α) → SkewMonoidAlgebra β α₂) x)
      fun (a₁ : α₂) (b₁ : β) ↦
      sum ((mapDomain (⇑f : (a : α) → α₂) : (a : SkewMonoidAlgebra β α) → SkewMonoidAlgebra β α₂) y)
        fun (a₂ : α₂) (b₂ : β) ↦ single (a₁ * a₂) (b₁ * a₁ • b₂))
⊢ Eq (α := SkewMonoidAlgebra β α₂)
    (x.sum fun (a : α) (b : β) ↦
      y.sum fun (a₂ : α) (b₂ : β) ↦
        (mapDomain (⇑f : (a : α) → α₂) : (a : SkewMonoidAlgebra β α) → SkewMonoidAlgebra β α₂)
          (single (a * a₂) (b * a • b₂)))
    (sum ((mapDomain (⇑f : (a : α) → α₂) : (a : SkewMonoidAlgebra β α) → SkewMonoidAlgebra β α₂) x)
      fun (a₁ : α₂) (b₁ : β) ↦
      sum ((mapDomain (⇑f : (a : α) → α₂) : (a : SkewMonoidAlgebra β α) → SkewMonoidAlgebra β α₂) y)
        fun (a₂ : α₂) (b₂ : β) ↦ single (a₁ * a₂) (b₁ * a₁ • b₂))

Tactic:
simp_rw [mapDomain_single, map_mul]

Premises used: SkewMonoidAlgebra.mapDomain_single, map_mul
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
α : Type u_3
α₂ : Type u_4
β : Type u_5
F : Type u_6
inst : Semiring β
inst_1 : Monoid α
inst_2 : Monoid α₂
inst_3 : FunLike F α α₂
inst_4 : MulSemiringAction α β
inst_5 : MulSemiringAction α₂ β
inst_6 : MulHomClass F α α₂
f : F
x y : SkewMonoidAlgebra β α
hf : ∀ (a : α) (x : β), a • x = HSMul.hSMul.{u_4, u_5, u_5} (α := α₂) ((f : (a : α) → α₂) a : α₂) x
⊢ ∀ (b : α₂),
    Eq (α := SkewMonoidAlgebra β α₂)
      (sum ((mapDomain (⇑f : (a : α) → α₂) : (a : SkewMonoidAlgebra β α) → SkewMonoidAlgebra β α₂) y)
        fun (a₂ : α₂) (b₂ : β) ↦ single (b * a₂) (0 * b • b₂))
      0

Tactic:
simp
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
α : Type u_3
α₂ : Type u_4
β : Type u_5
F : Type u_6
inst : Semiring β
inst_1 : Monoid α
inst_2 : Monoid α₂
inst_3 : FunLike F α α₂
inst_4 : MulSemiringAction α β
inst_5 : MulSemiringAction α₂ β
inst_6 : MulHomClass F α α₂
f : F
x y : SkewMonoidAlgebra β α
hf : ∀ (a : α) (x : β), a • x = HSMul.hSMul.{u_4, u_5, u_5} (α := α₂) ((f : (a : α) → α₂) a : α₂) x
⊢ ∀ (b : α₂) (m₁ m₂ : β),
    (sum ((mapDomain (⇑f : (a : α) → α₂) : (a : SkewMonoidAlgebra β α) → SkewMonoidAlgebra β α₂) y)
        fun (a₂ : α₂) (b₂ : β) ↦ single (b * a₂) ((m₁ + m₂) * b • b₂)) =
      HAdd.hAdd (α := SkewMonoidAlgebra β α₂)
        (sum ((mapDomain (⇑f : (a : α) → α₂) : (a : SkewMonoidAlgebra β α) → SkewMonoidAlgebra β α₂) y)
          fun (a₂ : α₂) (b₂ : β) ↦ single (b * a₂) (m₁ * b • b₂))
        (sum ((mapDomain (⇑f : (a : α) → α₂) : (a : SkewMonoidAlgebra β α) → SkewMonoidAlgebra β α₂) y)
          fun (a₂ : α₂) (b₂ : β) ↦ single (b * a₂) (m₂ * b • b₂))

Tactic:
simp [add_mul, single_add, sum_add]

Premises used: add_mul, SkewMonoidAlgebra.single_add, SkewMonoidAlgebra.sum_add
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
α : Type u_3
α₂ : Type u_4
β : Type u_5
F : Type u_6
inst : Semiring β
inst_1 : Monoid α
inst_2 : Monoid α₂
inst_3 : FunLike F α α₂
inst_4 : MulSemiringAction α β
inst_5 : MulSemiringAction α₂ β
inst_6 : MulHomClass F α α₂
f : F
x y : SkewMonoidAlgebra β α
hf : ∀ (a : α) (x : β), a • x = HSMul.hSMul.{u_4, u_5, u_5} (α := α₂) ((f : (a : α) → α₂) a : α₂) x
rw :
  Eq (α := SkewMonoidAlgebra β α₂)
    (x.sum fun (a : α) (b : β) ↦
      y.sum fun (a₂ : α) (b₂ : β) ↦
        single (HMul.hMul (α := α₂) (β := α₂) ((f : (a : α) → α₂) a : α₂) ((f : (a : α) → α₂) a₂ : α₂)) (b * a • b₂))
    (x.sum fun (a : α) (m : β) ↦
      sum ((mapDomain (⇑f : (a : α) → α₂) : (a : SkewMonoidAlgebra β α) → SkewMonoidAlgebra β α₂) y)
        fun (a₂ : α₂) (b₂ : β) ↦
        single (HMul.hMul (α := α₂) ((f : (a : α) → α₂) a : α₂) a₂)
          (m * HSMul.hSMul.{u_4, u_5, u_5} (α := α₂) ((f : (a : α) → α₂) a : α₂) b₂))
⊢ Eq (α := SkewMonoidAlgebra β α₂)
    (x.sum fun (a : α) (b : β) ↦
      y.sum fun (a₂ : α) (b₂ : β) ↦
        single (HMul.hMul (α := α₂) (β := α₂) ((f : (a : α) → α₂) a : α₂) ((f : (a : α) → α₂) a₂ : α₂)) (b * a • b₂))
    (sum ((mapDomain (⇑f : (a : α) → α₂) : (a : SkewMonoidAlgebra β α) → SkewMonoidAlgebra β α₂) x)
      fun (a₁ : α₂) (b₁ : β) ↦
      sum ((mapDomain (⇑f : (a : α) → α₂) : (a : SkewMonoidAlgebra β α) → SkewMonoidAlgebra β α₂) y)
        fun (a₂ : α₂) (b₂ : β) ↦ single (a₁ * a₂) (b₁ * a₁ • b₂))

Tactic:
rw [sum_mapDomain_index (by simp) (by simp [add_mul, single_add, sum_add])]

Premises used: SkewMonoidAlgebra.sum_mapDomain_index
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
α : Type u_3
α₂ : Type u_4
β : Type u_5
F : Type u_6
inst : Semiring β
inst_1 : Monoid α
inst_2 : Monoid α₂
inst_3 : FunLike F α α₂
inst_4 : MulSemiringAction α β
inst_5 : MulSemiringAction α₂ β
inst_6 : MulHomClass F α α₂
f : F
x y : SkewMonoidAlgebra β α
hf : ∀ (a : α) (x : β), a • x = HSMul.hSMul.{u_4, u_5, u_5} (α := α₂) ((f : (a : α) → α₂) a : α₂) x
e_g :
  Eq (α := α → β → SkewMonoidAlgebra β α₂)
    (fun (a : α) (b : β) ↦
      y.sum fun (a₂ : α) (b₂ : β) ↦
        single (HMul.hMul (α := α₂) (β := α₂) ((f : (a : α) → α₂) a : α₂) ((f : (a : α) → α₂) a₂ : α₂)) (b * a • b₂))
    fun (a : α) (m : β) ↦
    sum ((mapDomain (⇑f : (a : α) → α₂) : (a : SkewMonoidAlgebra β α) → SkewMonoidAlgebra β α₂) y)
      fun (a₂ : α₂) (b₂ : β) ↦
      single (HMul.hMul (α := α₂) ((f : (a : α) → α₂) a : α₂) a₂)
        (m * HSMul.hSMul.{u_4, u_5, u_5} (α := α₂) ((f : (a : α) → α₂) a : α₂) b₂)
⊢ Eq (α := SkewMonoidAlgebra β α₂)
    (x.sum fun (a : α) (b : β) ↦
      y.sum fun (a₂ : α) (b₂ : β) ↦
        single (HMul.hMul (α := α₂) (β := α₂) ((f : (a : α) → α₂) a : α₂) ((f : (a : α) → α₂) a₂ : α₂)) (b * a • b₂))
    (x.sum fun (a : α) (m : β) ↦
      sum ((mapDomain (⇑f : (a : α) → α₂) : (a : SkewMonoidAlgebra β α) → SkewMonoidAlgebra β α₂) y)
        fun (a₂ : α₂) (b₂ : β) ↦
        single (HMul.hMul (α := α₂) ((f : (a : α) → α₂) a : α₂) a₂)
          (m * HSMul.hSMul.{u_4, u_5, u_5} (α := α₂) ((f : (a : α) → α₂) a : α₂) b₂))

Tactic:
congr
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
α : Type u_3
α₂ : Type u_4
β : Type u_5
F : Type u_6
inst : Semiring β
inst_1 : Monoid α
inst_2 : Monoid α₂
inst_3 : FunLike F α α₂
inst_4 : MulSemiringAction α β
inst_5 : MulSemiringAction α₂ β
inst_6 : MulHomClass F α α₂
f : F
x y : SkewMonoidAlgebra β α
hf : ∀ (a : α) (x : β), a • x = HSMul.hSMul.{u_4, u_5, u_5} (α := α₂) ((f : (a : α) → α₂) a : α₂) x
e_g :
  ∀ (a : α) (b : β) (c : α₂),
    Eq.{u_5 + 1} (α := β)
      (coeff
        (y.sum fun (a₂ : α) (b₂ : β) ↦
          single (HMul.hMul (α := α₂) (β := α₂) ((f : (a : α) → α₂) a : α₂) ((f : (a : α) → α₂) a₂ : α₂)) (b * a • b₂))
        c)
      (coeff
        (sum ((mapDomain (⇑f : (a : α) → α₂) : (a : SkewMonoidAlgebra β α) → SkewMonoidAlgebra β α₂) y)
          fun (a₂ : α₂) (b₂ : β) ↦
          single (HMul.hMul (α := α₂) ((f : (a : α) → α₂) a : α₂) a₂)
            (b * HSMul.hSMul.{u_4, u_5, u_5} (α := α₂) ((f : (a : α) → α₂) a : α₂) b₂))
        c)
⊢ Eq (α := α → β → SkewMonoidAlgebra β α₂)
    (fun (a : α) (b : β) ↦
      y.sum fun (a₂ : α) (b₂ : β) ↦
        single (HMul.hMul (α := α₂) (β := α₂) ((f : (a : α) → α₂) a : α₂) ((f : (a : α) → α₂) a₂ : α₂)) (b * a • b₂))
    fun (a : α) (m : β) ↦
    sum ((mapDomain (⇑f : (a : α) → α₂) : (a : SkewMonoidAlgebra β α) → SkewMonoidAlgebra β α₂) y)
      fun (a₂ : α₂) (b₂ : β) ↦
      single (HMul.hMul (α := α₂) ((f : (a : α) → α₂) a : α₂) a₂)
        (m * HSMul.hSMul.{u_4, u_5, u_5} (α := α₂) ((f : (a : α) → α₂) a : α₂) b₂)

Tactic:
ext a b c
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
α : Type u_3
α₂ : Type u_4
β : Type u_5
F : Type u_6
inst : Semiring β
inst_1 : Monoid α
inst_2 : Monoid α₂
inst_3 : FunLike F α α₂
inst_4 : MulSemiringAction α β
inst_5 : MulSemiringAction α₂ β
inst_6 : MulHomClass F α α₂
f : F
x y : SkewMonoidAlgebra β α
hf : ∀ (a : α) (x : β), a • x = HSMul.hSMul.{u_4, u_5, u_5} (α := α₂) ((f : (a : α) → α₂) a : α₂) x
a : α
b : β
c : α₂
⊢ ∀ (b_1 : α₂),
    Eq (α := SkewMonoidAlgebra β α₂)
      (single (HMul.hMul (α := α₂) ((f : (a : α) → α₂) a : α₂) b_1)
        (b * HSMul.hSMul.{u_4, u_5, u_5} (α := α₂) (β := β) ((f : (a : α) → α₂) a : α₂) 0))
      0

Tactic:
simp