awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
S : Type u_3
S₁ : Type u_4
S₂ : Type u_5
M : Type u_6
α : Type u_7
inst : Monoid G
inst_1 : AddCommMonoid M
inst_2 : MulAction G α
g g' : G
f : SkewMonoidAlgebra M α
rw : (mapDomain fun (x : α) ↦ (g * g') • x : (a : SkewMonoidAlgebra M α) → SkewMonoidAlgebra M α) f = g • g' • f
rw₁ :
  Eq (α := SkewMonoidAlgebra M α)
    ((mapDomain fun (x : α) ↦ (g * g') • x : (a : SkewMonoidAlgebra M α) → SkewMonoidAlgebra M α) f :
      SkewMonoidAlgebra M α)
    ((mapDomain fun (x : α) ↦ g • x : (a : SkewMonoidAlgebra M α) → SkewMonoidAlgebra M α) (g' • f) :
      SkewMonoidAlgebra M α)
rw₂ :
  Eq (α := SkewMonoidAlgebra M α)
    ((mapDomain fun (x : α) ↦ (g * g') • x : (a : SkewMonoidAlgebra M α) → SkewMonoidAlgebra M α) f :
      SkewMonoidAlgebra M α)
    ((mapDomain fun (x : α) ↦ g • x : (a : SkewMonoidAlgebra M α) → SkewMonoidAlgebra M α)
        ((mapDomain fun (x : α) ↦ g' • x : (a : SkewMonoidAlgebra M α) → SkewMonoidAlgebra M α) f) :
      SkewMonoidAlgebra M α)
rw₃ :
  Eq (α := SkewMonoidAlgebra M α)
    ((mapDomain ((fun (x : α) ↦ g • x) ∘ fun (x : α) ↦ g' • x) : (a : SkewMonoidAlgebra M α) → SkewMonoidAlgebra M α)
        f :
      SkewMonoidAlgebra M α)
    ((mapDomain fun (x : α) ↦ g • x : (a : SkewMonoidAlgebra M α) → SkewMonoidAlgebra M α)
        ((mapDomain fun (x : α) ↦ g' • x : (a : SkewMonoidAlgebra M α) → SkewMonoidAlgebra M α) f) :
      SkewMonoidAlgebra M α)
rw₄ rw₅ :
  Eq (α := SkewMonoidAlgebra M α)
    ((mapDomain fun (x : α) ↦ g • x : (a : SkewMonoidAlgebra M α) → SkewMonoidAlgebra M α)
        ((mapDomain fun (x : α) ↦ g' • x : (a : SkewMonoidAlgebra M α) → SkewMonoidAlgebra M α) f) :
      SkewMonoidAlgebra M α)
    ((mapDomain fun (x : α) ↦ g • x : (a : SkewMonoidAlgebra M α) → SkewMonoidAlgebra M α)
        ((mapDomain fun (x : α) ↦ g' • x : (a : SkewMonoidAlgebra M α) → SkewMonoidAlgebra M α) f) :
      SkewMonoidAlgebra M α)
⊢ (g * g') • f = g • g' • f

Tactic:
rw [comapSMul_def, comapSMul_def, comapSMul_def, ← comp_smul_left, mapDomain_comp]

Premises used: SkewMonoidAlgebra.comapSMul_def, comp_smul_left, SkewMonoidAlgebra.mapDomain_comp
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
S : Type u_3
S₁ : Type u_4
S₂ : Type u_5
M : Type u_6
α : Type u_7
inst : Monoid G
inst_1 : AddCommMonoid M
inst_2 : MulAction G α
f : SkewMonoidAlgebra M α
rw :
  (mapDomain fun (x : α) ↦ HSMul.hSMul.{u_2, u_7, u_7} (α := G) 1 x :
        (a : SkewMonoidAlgebra M α) → SkewMonoidAlgebra M α)
      f =
    f
rw₁ : (mapDomain id : (a : SkewMonoidAlgebra M α) → SkewMonoidAlgebra M α) f = f
rw₂ rw₃ : f = f
⊢ HSMul.hSMul (α := G) 1 f = f

Tactic:
rw [comapSMul_def, one_smul_eq_id, mapDomain_id]

Premises used: SkewMonoidAlgebra.comapSMul_def, SkewMonoidAlgebra.mapDomain_id, one_smul_eq_id
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
S : Type u_3
S₁ : Type u_4
S₂ : Type u_5
M : Type u_6
α : Type u_7
inst : Monoid G
inst_1 : AddCommMonoid M
inst_2 : MulAction G α
inst_3 : AddCommMonoid k
g : G
a : ∀ (a : G), (HSMul.hSMul (β := SkewMonoidAlgebra k G) g 0).coeff a = coeff 0 a
⊢ HSMul.hSMul (β := SkewMonoidAlgebra k G) g 0 = 0

Tactic:
ext
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
S : Type u_3
S₁ : Type u_4
S₂ : Type u_5
M : Type u_6
α : Type u_7
inst : Monoid G
inst_1 : AddCommMonoid M
inst_2 : MulAction G α
inst_3 : AddCommMonoid k
g a : G
⊢ (HSMul.hSMul (β := SkewMonoidAlgebra k G) g 0).coeff a = coeff 0 a

Tactic:
simp [comapSMul_def, mapDomain]

Premises used: SkewMonoidAlgebra.mapDomain, SkewMonoidAlgebra.comapSMul_def
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
S : Type u_3
S₁ : Type u_4
S₂ : Type u_5
M : Type u_6
α : Type u_7
inst : Monoid G
inst_1 : AddCommMonoid M
inst_2 : MulAction G α
inst_3 : AddCommMonoid k
g : G
f f' : SkewMonoidAlgebra k G
a : ∀ (a : G), (g • (f + f')).coeff a = (g • f + g • f').coeff a
⊢ g • (f + f') = g • f + g • f'

Tactic:
ext
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
S : Type u_3
S₁ : Type u_4
S₂ : Type u_5
M : Type u_6
α : Type u_7
inst : Monoid G
inst_1 : AddCommMonoid M
inst_2 : MulAction G α
inst_3 : AddCommMonoid k
g : G
f f' : SkewMonoidAlgebra k G
a : G
⊢ (g • (f + f')).coeff a = (g • f + g • f').coeff a

Tactic:
simp [comapSMul_def, map_add]

Premises used: SkewMonoidAlgebra.comapSMul_def, map_add
-- 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
inst_3 : DecidableEq G
f g : SkewMonoidAlgebra k G
x : G
rw :
  Eq (α := k) (f.sum fun (a₁ : G) (b : k) ↦ coeff (g.sum fun (a₂ : G) (b₂ : k) ↦ single (a₁ * a₂) (b * a₁ • b₂)) x)
    (f.sum fun (a₁ : G) (b₁ : k) ↦ g.sum fun (a₂ : G) (b₂ : k) ↦ if a₁ * a₂ = x then b₁ * a₁ • b₂ else 0)
⊢ (f * g).coeff x = f.sum fun (a₁ : G) (b₁ : k) ↦ g.sum fun (a₂ : G) (b₂ : k) ↦ if a₁ * a₂ = x then b₁ * a₁ • b₂ else 0

Tactic:
rw [mul_def, coeff_sum]

Premises used: SkewMonoidAlgebra.coeff_sum, SkewMonoidAlgebra.mul_def
-- 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
inst_3 : DecidableEq G
f g : SkewMonoidAlgebra k G
x : G
e_g :
  Eq (α := G → k → k) (fun (a₁ : G) (b : k) ↦ coeff (g.sum fun (a₂ : G) (b₂ : k) ↦ single (a₁ * a₂) (b * a₁ • b₂)) x)
    fun (a₁ : G) (b₁ : k) ↦ g.sum fun (a₂ : G) (b₂ : k) ↦ if a₁ * a₂ = x then b₁ * a₁ • b₂ else 0
⊢ Eq (α := k) (f.sum fun (a₁ : G) (b : k) ↦ coeff (g.sum fun (a₂ : G) (b₂ : k) ↦ single (a₁ * a₂) (b * a₁ • b₂)) x)
    (f.sum fun (a₁ : G) (b₁ : k) ↦ g.sum fun (a₂ : G) (b₂ : k) ↦ if a₁ * a₂ = x then b₁ * a₁ • b₂ else 0)

Tactic:
congr
-- 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
inst_3 : DecidableEq G
f g : SkewMonoidAlgebra k G
x : G
e_g :
  ∀ (x_1 : G) (x_2 : k),
    Eq (α := k) (coeff (g.sum fun (a₂ : G) (b₂ : k) ↦ single (x_1 * a₂) (x_2 * x_1 • b₂)) x)
      (g.sum fun (a₂ : G) (b₂ : k) ↦ if x_1 * a₂ = x then x_2 * x_1 • b₂ else 0)
⊢ Eq (α := G → k → k) (fun (a₁ : G) (b : k) ↦ coeff (g.sum fun (a₂ : G) (b₂ : k) ↦ single (a₁ * a₂) (b * a₁ • b₂)) x)
    fun (a₁ : G) (b₁ : k) ↦ g.sum fun (a₂ : G) (b₂ : k) ↦ if a₁ * a₂ = x then b₁ * a₁ • b₂ else 0

Tactic:
ext
-- 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
inst_3 : DecidableEq G
f g : SkewMonoidAlgebra k G
x x_1 : G
x_2 : k
e_g :
  Eq (α := k) (g.sum fun (a₁ : G) (b : k) ↦ coeff (single (x_1 * a₁) (x_2 * x_1 • b)) x)
    (g.sum fun (a₂ : G) (b₂ : k) ↦ if x_1 * a₂ = x then x_2 * x_1 • b₂ else 0)
⊢ Eq (α := k) (coeff (g.sum fun (a₂ : G) (b₂ : k) ↦ single (x_1 * a₂) (x_2 * x_1 • b₂)) x)
    (g.sum fun (a₂ : G) (b₂ : k) ↦ if x_1 * a₂ = x then x_2 * x_1 • b₂ else 0)

Tactic:
rw [coeff_sum]

Premises used: SkewMonoidAlgebra.coeff_sum
-- 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
inst_3 : DecidableEq G
f g : SkewMonoidAlgebra k G
x x_1 : G
x_2 : k
e_g :
  Eq (α := G → k → k) (fun (a₁ : G) (b : k) ↦ coeff (single (x_1 * a₁) (x_2 * x_1 • b)) x) fun (a₂ : G) (b₂ : k) ↦
    if x_1 * a₂ = x then x_2 * x_1 • b₂ else 0
⊢ Eq (α := k) (g.sum fun (a₁ : G) (b : k) ↦ coeff (single (x_1 * a₁) (x_2 * x_1 • b)) x)
    (g.sum fun (a₂ : G) (b₂ : k) ↦ if x_1 * a₂ = x then x_2 * x_1 • b₂ else 0)

Tactic:
congr
-- 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
inst_3 : DecidableEq G
f g : SkewMonoidAlgebra k G
x x_1 : G
x_2 : k
e_g :
  ∀ (x_3 : G) (x_4 : k), coeff (single (x_1 * x_3) (x_2 * x_1 • x_4)) x = if x_1 * x_3 = x then x_2 * x_1 • x_4 else 0
⊢ Eq (α := G → k → k) (fun (a₁ : G) (b : k) ↦ coeff (single (x_1 * a₁) (x_2 * x_1 • b)) x) fun (a₂ : G) (b₂ : k) ↦
    if x_1 * a₂ = x then x_2 * x_1 • b₂ else 0

Tactic:
ext
-- 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
inst_3 : DecidableEq G
f g : SkewMonoidAlgebra k G
x x_1 : G
x_2 : k
x_3 : G
x_4 : k
⊢ coeff (single (x_1 * x_3) (x_2 * x_1 • x_4)) x = if x_1 * x_3 = x then x_2 * x_1 • x_4 else 0

Tactic:
coeff_single_apply

Premises used: SkewMonoidAlgebra.coeff_single_apply
-- 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
inst_3 : DecidableEq G
f g : SkewMonoidAlgebra k G
x x_1 : G
x_2 : k
x_3 : G
x_4 : k
⊢ coeff (single (x_1 * x_3) (x_2 * x_1 • x_4)) x = if x_1 * x_3 = x then x_2 * x_1 • x_4 else 0

Tactic:
exact coeff_single_apply

Premises used: SkewMonoidAlgebra.coeff_single_apply
-- 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 g : SkewMonoidAlgebra k G
x : G
s : Finset (G × G)
hs : ∀ {p : G × G}, p ∈ s ↔ p.1 * p.2 = x
F : G × G → k := fun (p : G × G) ↦ if p.1 * p.2 = x then f.coeff p.1 * p.1 • g.coeff p.2 else 0
⊢ (f * g).coeff x = ∑ a₁ ∈ f.support, ∑ a₂ ∈ g.support, F (a₁, a₂)

Tactic:
coeff_mul f g x

Premises used: Finsupp.sum, SkewMonoidAlgebra.coeff_mul, SkewMonoidAlgebra.support, SkewMonoidAlgebra.sum, 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
f g : SkewMonoidAlgebra k G
x : G
s : Finset (G × G)
hs : ∀ {p : G × G}, p ∈ s ↔ p.1 * p.2 = x
F : G × G → k := fun (p : G × G) ↦ if p.1 * p.2 = x then f.coeff p.1 * p.1 • g.coeff p.2 else 0
rw rw₁ : Eq.{u_1 + 1} (α := k) (∑ x ∈ f.support ×ˢ g.support, F x) (∑ p ∈ f.support ×ˢ g.support, F p)
⊢ Eq.{u_1 + 1} (α := k) (∑ a₁ ∈ f.support, ∑ a₂ ∈ g.support, F (a₁, a₂)) (∑ p ∈ f.support ×ˢ g.support, F p)

Tactic:
rw [← Finset.sum_product _ _ _]

Premises used: Finset.sum_product
-- 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 g : SkewMonoidAlgebra k G
x : G
s : Finset (G × G)
hs : ∀ {p : G × G}, p ∈ s ↔ p.1 * p.2 = x
F : G × G → k := fun (p : G × G) ↦ if p.1 * p.2 = x then f.coeff p.1 * p.1 • g.coeff p.2 else 0
⊢ Eq.{u_1 + 1} (α := k) (∑ p ∈ f.support ×ˢ g.support, F p)
    (∑ p ∈ f.support ×ˢ g.support with p.1 * p.2 = x, f.coeff p.1 * p.1 • g.coeff p.2)

Tactic:
(Finset.sum_filter _ _).symm

Premises used: Finset.sum_filter, Eq.symm
-- 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 g : SkewMonoidAlgebra k G
x : G
s : Finset (G × G)
hs : ∀ {p : G × G}, p ∈ s ↔ p.1 * p.2 = x
F : G × G → k := fun (p : G × G) ↦ if p.1 * p.2 = x then f.coeff p.1 * p.1 • g.coeff p.2 else 0
h : ∀ (a : G × G), a ∈ {p ∈ f.support ×ˢ g.support | p.1 * p.2 = x} ↔ a ∈ {p ∈ s | p.1 ∈ f.support ∧ p.2 ∈ g.support}
⊢ {p ∈ f.support ×ˢ g.support | p.1 * p.2 = x} = {p ∈ s | p.1 ∈ f.support ∧ p.2 ∈ g.support}

Tactic:
ext
-- 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 g : SkewMonoidAlgebra k G
x : G
s : Finset (G × G)
hs : ∀ {p : G × G}, p ∈ s ↔ p.1 * p.2 = x
F : G × G → k := fun (p : G × G) ↦ if p.1 * p.2 = x then f.coeff p.1 * p.1 • g.coeff p.2 else 0
a : G × G
⊢ a ∈ {p ∈ f.support ×ˢ g.support | p.1 * p.2 = x} ↔ a ∈ {p ∈ s | p.1 ∈ f.support ∧ p.2 ∈ g.support}

Tactic:
simp [Finset.mem_filter, Finset.mem_product, hs, and_comm]

Premises used: and_comm, Finset.mem_filter, Finset.mem_product
-- 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 g : SkewMonoidAlgebra k G
x : G
s : Finset (G × G)
hs : ∀ {p : G × G}, p ∈ s ↔ p.1 * p.2 = x
F : G × G → k := fun (p : G × G) ↦ if p.1 * p.2 = x then f.coeff p.1 * p.1 • g.coeff p.2 else 0
p : G × G
hps : p ∈ s
hp : p ∉ {p ∈ s | p.1 ∈ f.support ∧ p.2 ∈ g.support}
⊢ p ∈ s → f.coeff p.1 ≠ 0 → g.coeff p.2 = 0

Tactic:
simp only [Finset.mem_filter, mem_support_iff, not_and, Classical.not_not] at hp ⊢

Premises used: Classical.not_not, SkewMonoidAlgebra.mem_support_iff, Finset.mem_filter, not_and
-- 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 g : SkewMonoidAlgebra k G
x : G
s : Finset (G × G)
hs : ∀ {p : G × G}, p ∈ s ↔ p.1 * p.2 = x
F : G × G → k := fun (p : G × G) ↦ if p.1 * p.2 = x then f.coeff p.1 * p.1 • g.coeff p.2 else 0
p : G × G
hps : p ∈ s
hp : p ∈ s → f.coeff p.1 ≠ 0 → g.coeff p.2 = 0
pos : ∀ (h1 : f.coeff p.1 = 0), f.coeff p.1 * p.1 • g.coeff p.2 = 0
neg : ∀ (h1 : ¬f.coeff p.1 = 0), f.coeff p.1 * p.1 • g.coeff p.2 = 0
⊢ f.coeff p.1 * p.1 • g.coeff p.2 = 0

Tactic:
by_cases h1 : f.coeff p.1 = 0

Premises used: Prod.fst, 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
f g : SkewMonoidAlgebra k G
x : G
s : Finset (G × G)
hs : ∀ {p : G × G}, p ∈ s ↔ p.1 * p.2 = x
F : G × G → k := fun (p : G × G) ↦ if p.1 * p.2 = x then f.coeff p.1 * p.1 • g.coeff p.2 else 0
p : G × G
hps : p ∈ s
hp : p ∈ s → f.coeff p.1 ≠ 0 → g.coeff p.2 = 0
h1 : f.coeff p.1 = 0
⊢ f.coeff p.1 * p.1 • g.coeff p.2 = 0

Tactic:
simp_all
-- 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 g : SkewMonoidAlgebra k G
x : G
s : Finset (G × G)
hs : ∀ {p : G × G}, p ∈ s ↔ p.1 * p.2 = x
F : G × G → k := fun (p : G × G) ↦ if p.1 * p.2 = x then f.coeff p.1 * p.1 • g.coeff p.2 else 0
p : G × G
hps : p ∈ s
hp : p ∈ s → f.coeff p.1 ≠ 0 → g.coeff p.2 = 0
h1 : ¬f.coeff p.1 = 0
⊢ f.coeff p.1 * p.1 • g.coeff p.2 = 0

Tactic:
simp_all
-- 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 g : SkewMonoidAlgebra k G
x : G
s : Finset (G × G)
hs : ∀ {p : G × G}, p ∈ s ↔ p.1 * p.2 = x
F : G × G → k := fun (p : G × G) ↦ if p.1 * p.2 = x then f.coeff p.1 * p.1 • g.coeff p.2 else 0
x₁ : Eq.{u_1 + 1} (α := k) (∑ a₁ ∈ f.support, ∑ a₂ ∈ g.support, F (a₁, a₂)) (∑ p ∈ f.support ×ˢ g.support, F p)
⊢ (f * g).coeff x = ∑ p ∈ s, f.coeff p.1 * p.1 • g.coeff p.2

Tactic:
calc
    (f * g).coeff x = ∑ a₁ ∈ f.support, ∑ a₂ ∈ g.support, F (a₁, a₂) := coeff_mul f g x
    _ = ∑ p ∈ f.support ×ˢ g.support, F p := by rw [← Finset.sum_product _ _ _]
    _ = ∑ p ∈ (f.support ×ˢ g.support).filter fun p : G × G ↦ p.1 * p.2 = x,
      f.coeff p.1 * p.1 • g.coeff p.2 := (Finset.sum_filter _ _).symm
    _ = ∑ p ∈ s.filter fun p : G × G ↦ p.1 ∈ f.support ∧ p.2 ∈ g.support,
      f.coeff p.1 * p.1 • g.coeff p.2 :=
      (Finset.sum_congr (by ext; simp [Finset.mem_filter, Finset.mem_product, hs, and_comm])
        fun _ _ ↦ rfl)
    _ = ∑ p ∈ s, f.coeff p.1 * p.1 • g.coeff p.2 :=
      Finset.sum_subset (Finset.filter_subset _ _) fun p hps hp ↦ by
        simp only [Finset.mem_filter, mem_support_iff, not_and, Classical.not_not] at hp ⊢
        by_cases h1 : f.coeff p.1 = 0 <;> simp_all

Premises used: HMul.hMul, SProd.sprod, Membership.mem, Finset.filter_subset, SkewMonoidAlgebra.coeff_mul, Prod.fst, And, SkewMonoidAlgebra.support, Finset.sum_subset, Finset.sum_filter, Eq.symm, Finset.filter, Eq, Prod.snd, Finset.sum_congr, rfl, 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
f g : SkewMonoidAlgebra k G
x : G
s : Finset (G × G)
hs : ∀ {p : G × G}, p ∈ s ↔ p.1 * p.2 = x
let let₁ let₂ : (f * g).coeff x = ∑ p ∈ s, f.coeff p.1 * p.1 • g.coeff p.2
⊢ (f * g).coeff x = ∑ p ∈ s, f.coeff p.1 * p.1 • g.coeff p.2

Tactic:
classical
  let F : G × G → k := fun p ↦ if p.1 * p.2 = x then f.coeff p.1 * p.1 • g.coeff p.2 else 0
  calc
    (f * g).coeff x = ∑ a₁ ∈ f.support, ∑ a₂ ∈ g.support, F (a₁, a₂) := coeff_mul f g x
    _ = ∑ p ∈ f.support ×ˢ g.support, F p := by rw [← Finset.sum_product _ _ _]
    _ = ∑ p ∈ (f.support ×ˢ g.support).filter fun p : G × G ↦ p.1 * p.2 = x,
      f.coeff p.1 * p.1 • g.coeff p.2 := (Finset.sum_filter _ _).symm
    _ = ∑ p ∈ s.filter fun p : G × G ↦ p.1 ∈ f.support ∧ p.2 ∈ g.support,
      f.coeff p.1 * p.1 • g.coeff p.2 :=
      (Finset.sum_congr (by ext; simp [Finset.mem_filter, Finset.mem_product, hs, and_comm])
        fun _ _ ↦ rfl)
    _ = ∑ p ∈ s, f.coeff p.1 * p.1 • g.coeff p.2 :=
      Finset.sum_subset (Finset.filter_subset _ _) fun p hps hp ↦ by
        simp only [Finset.mem_filter, mem_support_iff, not_and, Classical.not_not] at hp ⊢
        by_cases h1 : f.coeff p.1 = 0 <;> simp_all

Premises used: HMul.hMul, Finset.filter_subset, SkewMonoidAlgebra.support, Finset.sum_subset, Finset.sum_filter, Eq.symm, Finset.sum_congr, rfl, 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
f g : SkewMonoidAlgebra k G
x : G
hs :
  Set.Finite.{u_2} (α := G × G) (Function.support.{u_2, u_1} (M := k) fun (p : G × G) ↦ f.coeff p.1 * p.1 • g.coeff p.2)
⊢ Set.Finite.{u_2} (α := G × G)
    ({p : G × G | p.1 * p.2 = x} ∩
      Function.support.{u_2, u_1} (M := k) fun (p : G × G) ↦ f.coeff p.1 * p.1 • g.coeff p.2)

Tactic:
apply Set.Finite.inter_of_right

Premises used: Set.Finite.inter_of_right
-- 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 g : SkewMonoidAlgebra k G
x : G
hs :
  (Function.support.{u_2, u_1} (M := k) fun (p : G × G) ↦ f.coeff p.1 * p.1 • g.coeff p.2) ⊆
    (↑(f.support.product g.support) : Set (G × G))
⊢ Set.Finite.{u_2} (α := G × G) (Function.support.{u_2, u_1} (M := k) fun (p : G × G) ↦ f.coeff p.1 * p.1 • g.coeff p.2)

Tactic:
apply Set.Finite.subset (Finset.finite_toSet ((f.support).product (g.support)))

Premises used: Set.Finite.subset, SkewMonoidAlgebra.support, Finset.finite_toSet, Finset.product
-- 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 g : SkewMonoidAlgebra k G
x : G
⊢ (Function.support.{u_2, u_1} (M := k) fun (p : G × G) ↦ f.coeff p.1 * p.1 • g.coeff p.2) ⊆
    (↑(f.support.product g.support) : Set (G × G))

Tactic:
aesop
-- 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 g : SkewMonoidAlgebra k G
x : G
⊢ Set.Finite.{u_2} (α := G × G)
    ({p : G × G | p.1 * p.2 = x} ∩
      Function.support.{u_2, u_1} (M := k) fun (p : G × G) ↦ f.coeff p.1 * p.1 • g.coeff p.2)

Tactic:
have : ({p : G × G | p.1 * p.2 = x}
      ∩ Function.support fun p ↦ f.coeff p.1 * p.1 • g.coeff p.2).Finite := by
    apply Set.Finite.inter_of_right
    apply Set.Finite.subset (Finset.finite_toSet ((f.support).product (g.support)))
    aesop
-- 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 g : SkewMonoidAlgebra k G
x : G
this :
  Set.Finite.{u_2} (α := G × G)
    ({p : G × G | p.1 * p.2 = x} ∩
      Function.support.{u_2, u_1} (M := k) fun (p : G × G) ↦ f.coeff p.1 * p.1 • g.coeff p.2)
rw :
  (f * g).coeff x =
    ∑
      i ∈
        this.toFinset (s :=
          {p : G × G | p.1 * p.2 = x} ∩
            Function.support.{u_2, u_1} (M := k) fun (p : G × G) ↦ f.coeff p.1 * p.1 • g.coeff p.2),
      f.coeff i.1 * i.1 • g.coeff i.2
⊢ (f * g).coeff x =
    ∑ᶠ (p : G × G) (_ : Membership.mem (γ := Set (G × G)) {p : G × G | p.1 * p.2 = x} p),
      f.coeff p.1 * p.1 • g.coeff p.2

Tactic:
rw [← finsum_mem_inter_support, finsum_mem_eq_finite_toFinset_sum _ this]

Premises used: finsum_mem_eq_finite_toFinset_sum, finsum_mem_inter_support
-- 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 g : SkewMonoidAlgebra k G
x : G
this :
  Set.Finite.{u_2} (α := G × G)
    ({p : G × G | p.1 * p.2 = x} ∩
      Function.support.{u_2, u_1} (M := k) fun (p : G × G) ↦ f.coeff p.1 * p.1 • g.coeff p.2)
s : Finset (G × G) :=
  this.toFinset (s :=
    {p : G × G | p.1 * p.2 = x} ∩
      Function.support.{u_2, u_1} (M := k) fun (p : G × G) ↦ f.coeff p.1 * p.1 • g.coeff p.2)
F : G × G → k := fun (p : G × G) ↦ if p.1 * p.2 = x then f.coeff p.1 * p.1 • g.coeff p.2 else 0
⊢ (f * g).coeff x = ∑ a₁ ∈ f.support, ∑ a₂ ∈ g.support, F (a₁, a₂)

Tactic:
coeff_mul f g x

Premises used: Finsupp.sum, SkewMonoidAlgebra.coeff_mul, SkewMonoidAlgebra.support, SkewMonoidAlgebra.sum, 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
f g : SkewMonoidAlgebra k G
x : G
this :
  Set.Finite.{u_2} (α := G × G)
    ({p : G × G | p.1 * p.2 = x} ∩
      Function.support.{u_2, u_1} (M := k) fun (p : G × G) ↦ f.coeff p.1 * p.1 • g.coeff p.2)
s : Finset (G × G) :=
  this.toFinset (s :=
    {p : G × G | p.1 * p.2 = x} ∩
      Function.support.{u_2, u_1} (M := k) fun (p : G × G) ↦ f.coeff p.1 * p.1 • g.coeff p.2)
F : G × G → k := fun (p : G × G) ↦ if p.1 * p.2 = x then f.coeff p.1 * p.1 • g.coeff p.2 else 0
rw rw₁ : Eq.{u_1 + 1} (α := k) (∑ x ∈ f.support ×ˢ g.support, F x) (∑ p ∈ f.support ×ˢ g.support, F p)
⊢ Eq.{u_1 + 1} (α := k) (∑ a₁ ∈ f.support, ∑ a₂ ∈ g.support, F (a₁, a₂)) (∑ p ∈ f.support ×ˢ g.support, F p)

Tactic:
rw [← Finset.sum_product _ _ _]

Premises used: Finset.sum_product
-- 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 g : SkewMonoidAlgebra k G
x : G
this :
  Set.Finite.{u_2} (α := G × G)
    ({p : G × G | p.1 * p.2 = x} ∩
      Function.support.{u_2, u_1} (M := k) fun (p : G × G) ↦ f.coeff p.1 * p.1 • g.coeff p.2)
s : Finset (G × G) :=
  this.toFinset (s :=
    {p : G × G | p.1 * p.2 = x} ∩
      Function.support.{u_2, u_1} (M := k) fun (p : G × G) ↦ f.coeff p.1 * p.1 • g.coeff p.2)
F : G × G → k := fun (p : G × G) ↦ if p.1 * p.2 = x then f.coeff p.1 * p.1 • g.coeff p.2 else 0
⊢ Eq.{u_1 + 1} (α := k) (∑ p ∈ f.support ×ˢ g.support, F p)
    (∑ p ∈ f.support ×ˢ g.support with p.1 * p.2 = x, f.coeff p.1 * p.1 • g.coeff p.2)

Tactic:
(Finset.sum_filter _ _).symm

Premises used: Finset.sum_filter, Eq.symm
-- 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 g : SkewMonoidAlgebra k G
x : G
this :
  Set.Finite.{u_2} (α := G × G)
    ({p : G × G | p.1 * p.2 = x} ∩
      Function.support.{u_2, u_1} (M := k) fun (p : G × G) ↦ f.coeff p.1 * p.1 • g.coeff p.2)
s : Finset (G × G) :=
  this.toFinset (s :=
    {p : G × G | p.1 * p.2 = x} ∩
      Function.support.{u_2, u_1} (M := k) fun (p : G × G) ↦ f.coeff p.1 * p.1 • g.coeff p.2)
F : G × G → k := fun (p : G × G) ↦ if p.1 * p.2 = x then f.coeff p.1 * p.1 • g.coeff p.2 else 0
h₁ :
  ∀ a ∈ {p ∈ f.support ×ˢ g.support | p.1 * p.2 = x},
    a ∉ {p ∈ s | p.1 ∈ f.support ∧ p.2 ∈ g.support} → f.coeff a.1 * a.1 • g.coeff a.2 = 0
h₂ :
  ∀ a ∈ {p ∈ s | p.1 ∈ f.support ∧ p.2 ∈ g.support},
    a ∉ {p ∈ f.support ×ˢ g.support | p.1 * p.2 = x} → f.coeff a.1 * a.1 • g.coeff a.2 = 0
h :
  ∀ a ∈ {p ∈ f.support ×ˢ g.support | p.1 * p.2 = x},
    a ∈ {p ∈ s | p.1 ∈ f.support ∧ p.2 ∈ g.support} → f.coeff a.1 * a.1 • g.coeff a.2 = f.coeff a.1 * a.1 • g.coeff a.2
⊢ Eq.{u_1 + 1} (α := k) (∑ p ∈ f.support ×ˢ g.support with p.1 * p.2 = x, f.coeff p.1 * p.1 • g.coeff p.2)
    (∑ p ∈ s with p.1 ∈ f.support ∧ p.2 ∈ g.support, f.coeff p.1 * p.1 • g.coeff p.2)

Tactic:
apply Finset.sum_congr_of_eq_on_inter

Premises used: Finset.sum_congr_of_eq_on_inter