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 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
⊢ ∀ 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

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
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
⊢ ∀ 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

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
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
⊢ ∀ 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

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
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
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
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
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
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
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
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
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
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
x₁ : Eq.{u_1 + 1} (α := k) (∑ a₁ ∈ f.support, ∑ a₂ ∈ g.support, F (a₁, a₂)) (∑ p ∈ f.support ×ˢ g.support, F p)
x₂ :
  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)
⊢ (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

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 := by
        apply Finset.sum_congr_of_eq_on_inter <;> aesop
    _ = ∑ 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, 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)
let let₁ let₂ let₃ :
  (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 =
    ∑
      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

Tactic:
classical
  let s := Set.Finite.toFinset (s := ({p : G × G | p.1 * p.2 = x}
    ∩ Function.support fun p ↦ f.coeff p.1 * p.1 • g.coeff p.2)) this
  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 := by
        apply Finset.sum_congr_of_eq_on_inter <;> aesop
    _ = ∑ 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, 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 : SkewMonoidAlgebra k G
r : k
x y z : G
H : ∀ (a : G), a * x = z ↔ a = y
a₁ : G
b₁ : k
⊢ (if a₁ * x = z then b₁ * HSMul.hSMul (β := k) a₁ 0 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
f : SkewMonoidAlgebra k G
r : k
x y z : G
H : ∀ (a : G), a * x = z ↔ a = y
⊢ ∀ (a₁ : G) (b₁ : k),
    (sum (single x r) fun (a₂ : G) (b₂ : k) ↦ if a₁ * a₂ = z then b₁ * a₁ • b₂ else 0) =
      if a₁ * x = z then b₁ * a₁ • r else 0

Tactic:
have A : ∀ a₁ b₁, ((single x r).sum fun a₂ b₂ ↦ ite (a₁ * a₂ = z) (b₁ * a₁ • b₂) 0) =
      ite (a₁ * x = z) (b₁ * a₁ • r) 0 :=
    fun a₁ b₁ ↦ sum_single_index <| by 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
f : SkewMonoidAlgebra k G
r : k
x y z : G
H : ∀ (a : G), a * x = z ↔ a = y
A :
  ∀ (a₁ : G) (b₁ : k),
    (sum (single x r) fun (a₂ : G) (b₂ : k) ↦ if a₁ * a₂ = z then b₁ * a₁ • b₂ else 0) =
      if a₁ * x = z then b₁ * a₁ • r else 0
⊢ (f * single x r).coeff z = f.sum fun (a : G) (b : k) ↦ if a = y then b * y • r else 0

Tactic:
simp [coeff_mul, A, H, sum_ite_eq']

Premises used: SkewMonoidAlgebra.sum_ite_eq', SkewMonoidAlgebra.coeff_mul
-- 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), a * x = z ↔ a = y
A :
  ∀ (a₁ : G) (b₁ : k),
    (sum (single x r) fun (a₂ : G) (b₂ : k) ↦ if a₁ * a₂ = z then b₁ * a₁ • b₂ else 0) =
      if a₁ * x = z then b₁ * a₁ • r else 0
⊢ (f.sum fun (a : G) (b : k) ↦ if a = y then b * y • r else 0) = if y ∈ f.support then f.coeff y * y • r else 0

Tactic:
(f.support.sum_ite_eq' _ _)

Premises used: Finset.sum_ite_eq', Finsupp.sum, 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 : SkewMonoidAlgebra k G
r : k
x y z : G
H : ∀ (a : G), a * x = z ↔ a = y
A :
  ∀ (a₁ : G) (b₁ : k),
    (sum (single x r) fun (a₂ : G) (b₂ : k) ↦ if a₁ * a₂ = z then b₁ * a₁ • b₂ else 0) =
      if a₁ * x = z then b₁ * a₁ • r else 0
pos : ∀ (h : y ∈ f.support), f.coeff y * y • r = f.coeff y * y • r
neg : ∀ (h : y ∉ f.support), 0 = f.coeff y * y • r
⊢ (if y ∈ f.support then f.coeff y * y • r else 0) = f.coeff y * y • r

Tactic:
split_ifs with 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), a * x = z ↔ a = y
A :
  ∀ (a₁ : G) (b₁ : k),
    (sum (single x r) fun (a₂ : G) (b₂ : k) ↦ if a₁ * a₂ = z then b₁ * a₁ • b₂ else 0) =
      if a₁ * x = z then b₁ * a₁ • r else 0
h : y ∈ f.support
⊢ ¬f.coeff y = 0

Tactic:
simp [support] at h

Premises used: SkewMonoidAlgebra.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 : SkewMonoidAlgebra k G
r : k
x y z : G
H : ∀ (a : G), a * x = z ↔ a = y
A :
  ∀ (a₁ : G) (b₁ : k),
    (sum (single x r) fun (a₂ : G) (b₂ : k) ↦ if a₁ * a₂ = z then b₁ * a₁ • b₂ else 0) =
      if a₁ * x = z then b₁ * a₁ • r else 0
h : y ∉ f.support
⊢ f.coeff y = 0

Tactic:
simp [support] at h

Premises used: SkewMonoidAlgebra.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 : SkewMonoidAlgebra k G
r : k
x y z : G
H : ∀ (a : G), a * x = z ↔ a = y
A :
  ∀ (a₁ : G) (b₁ : k),
    (sum (single x r) fun (a₂ : G) (b₂ : k) ↦ if a₁ * a₂ = z then b₁ * a₁ • b₂ else 0) =
      if a₁ * x = z then b₁ * a₁ • r else 0
h : ¬f.coeff y = 0
⊢ f.coeff y * y • r = f.coeff y * y • r

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), a * x = z ↔ a = y
A :
  ∀ (a₁ : G) (b₁ : k),
    (sum (single x r) fun (a₂ : G) (b₂ : k) ↦ if a₁ * a₂ = z then b₁ * a₁ • b₂ else 0) =
      if a₁ * x = z then b₁ * a₁ • r else 0
h : f.coeff y = 0
⊢ 0 = f.coeff y * y • r

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), a * x = z ↔ a = y
A :
  ∀ (a₁ : G) (b₁ : k),
    (sum (single x r) fun (a₂ : G) (b₂ : k) ↦ if a₁ * a₂ = z then b₁ * a₁ • b₂ else 0) =
      if a₁ * x = z then b₁ * a₁ • r else 0
x₁ : (f * single x r).coeff z = f.sum fun (a : G) (b : k) ↦ if a = y then b * y • r else 0
x₂ : (if y ∈ f.support then f.coeff y * y • r else 0) = f.coeff y * y • r
⊢ (f * single x r).coeff z = f.coeff y * y • r

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

Premises used: HMul.hMul, Finset.sum_ite_eq', SkewMonoidAlgebra.support, HSMul.hSMul, OfNat.ofNat, SkewMonoidAlgebra.single, Eq, SkewMonoidAlgebra.sum, SkewMonoidAlgebra.coeff, 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), a * x = z ↔ a = y
have have₁ have₂ :
  ∀
    (A :
      ∀ (a₁ : G) (b₁ : k),
        (sum (single x r) fun (a₂ : G) (b₂ : k) ↦ if a₁ * a₂ = z then b₁ * a₁ • b₂ else 0) =
          if a₁ * x = z then b₁ * a₁ • r else 0),
    (f * single x r).coeff z = f.coeff y * y • r
⊢ (f * single x r).coeff z = f.coeff y * y • r

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

Premises used: HMul.hMul, SkewMonoidAlgebra.support, SkewMonoidAlgebra.single, 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 : ∀ (x : G), ¬g' = x * g
simp : Eq (α := k) (x.sum fun (a₁ : G) (b₁ : k) ↦ if a₁ * g = g' then b₁ * a₁ • r else 0) 0
⊢ (x * single g r).coeff g' = 0

Tactic:
simp only [coeff_mul, smul_zero, mul_zero, ite_self, sum_single_index]

Premises used: ite_self, smul_zero, SkewMonoidAlgebra.coeff_mul, MulZeroClass.mul_zero, 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 : ∀ (x : G), ¬g' = x * g
h₁ :
  ∀ x_1 ∈ x.toFinsupp.support,
    Eq.{u_1 + 1} (α := k)
      ((fun (a₁ : G) (b₁ : k) ↦ if a₁ * g = g' then b₁ * a₁ • r else 0) x_1 ((x.toFinsupp : (a : G) → k) x_1)) 0
⊢ Eq (α := k) (x.sum fun (a₁ : G) (b₁ : k) ↦ if a₁ * g = g' then b₁ * a₁ • r 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 : ∀ (x : G), ¬g' = x * g
h₁ : ∀ x_1 ∈ x.toFinsupp.support, x_1 * g = g' → HMul.hMul (α := k) ((x.toFinsupp : (a : G) → k) x_1 : k) (x_1 • r) = 0
⊢ ∀ x_1 ∈ x.toFinsupp.support,
    Eq.{u_1 + 1} (α := k)
      ((fun (a₁ : G) (b₁ : k) ↦ if a₁ * g = g' then b₁ * a₁ • r 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
x_1 : G
h_1 : x_1 ∈ x.toFinsupp.support
h : ∀ (x : G), ¬x_1 * g = x * g
⊢ HMul.hMul (α := k) ((x.toFinsupp : (a : G) → k) x_1 : k) (x_1 • r) = 0

Tactic:
False.elim (h _ rfl)

Premises used: False.elim, rfl
-- 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
x_1 : G
h_1 : x_1 ∈ x.toFinsupp.support
h : ∀ (x : G), ¬x_1 * g = x * g
⊢ HMul.hMul (α := k) ((x.toFinsupp : (a : G) → k) x_1 : k) (x_1 • r) = 0

Tactic:
exact False.elim (h _ rfl)

Premises used: False.elim, rfl
-- 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 : ∀ (x : G), ¬g' = x * g
simp : Eq (α := k) (x.sum fun (a₁ : G) (b₁ : k) ↦ if a₁ * g = g' then b₁ * a₁ • r else 0) 0
h₁ :
  ∀ x_1 ∈ x.toFinsupp.support,
    Eq.{u_1 + 1} (α := k)
      ((fun (a₁ : G) (b₁ : k) ↦ if a₁ * g = g' then b₁ * a₁ • r else 0) x_1 ((x.toFinsupp : (a : G) → k) x_1)) 0
h₂ : ∀ x_1 ∈ x.toFinsupp.support, x_1 * g = g' → HMul.hMul (α := k) ((x.toFinsupp : (a : G) → k) x_1 : k) (x_1 • r) = 0
h₃ :
  ∀ x_1 ∈ x.toFinsupp.support,
    ∀ (h : ∀ (x : G), ¬x_1 * g = x * g), HMul.hMul (α := k) ((x.toFinsupp : (a : G) → k) x_1 : k) (x_1 • r) = 0
⊢ (x * single g r).coeff g' = 0

Tactic:
classical
  simp only [coeff_mul, smul_zero, mul_zero, ite_self, sum_single_index]
  apply Finset.sum_eq_zero
  simp_rw [ite_eq_right_iff]
  rintro _ _ rfl
  exact False.elim (h _ rfl)

Premises used: ite_self, False.elim, Finset.sum_eq_zero, smul_zero, SkewMonoidAlgebra.coeff_mul, MulZeroClass.mul_zero, 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 : 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
⊢ Eq (α := k) (f.sum fun (a : G) (b : k) ↦ if x * a = y then 0 * x • 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
f : SkewMonoidAlgebra k G
r : k
x y z : G
H : ∀ (a : G), x * a = y ↔ a = z
⊢ Eq (α := k) (f.sum fun (a : G) (b : k) ↦ if x * a = y then 0 * x • b else 0) 0

Tactic:
have : (f.sum fun a b ↦ ite (x * a = y) (0 * x • b) 0) = 0 := by 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
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
⊢ (single x r * f).coeff y = f.sum fun (a : G) (b : k) ↦ if x * a = y then r * x • b else 0

Tactic:
(coeff_mul _ _ _).trans <| sum_single_index this

Premises used: SkewMonoidAlgebra.coeff_mul, Eq.trans, 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
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
⊢ 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)

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
⊢ (f.sum fun (a : G) (b : k) ↦ if a = z then r * x • b else 0) = if z ∈ f.support then r * x • f.coeff z else 0

Tactic:
(f.support.sum_ite_eq' _ _)

Premises used: Finset.sum_ite_eq', Finsupp.sum, 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 : 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
pos : ∀ (h : z ∈ f.support), r * x • f.coeff z = r * x • f.coeff z
neg : ∀ (h : z ∉ f.support), 0 = r * x • f.coeff z
⊢ (if z ∈ f.support then r * x • f.coeff z else 0) = r * x • f.coeff z

Tactic:
split_ifs with 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
h : z ∈ f.support
⊢ ¬f.coeff z = 0

Tactic:
simp [support] at h

Premises used: SkewMonoidAlgebra.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 : 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 : z ∉ f.support
⊢ f.coeff z = 0

Tactic:
simp [support] at h

Premises used: SkewMonoidAlgebra.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 : 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
⊢ r * x • f.coeff z = r * x • f.coeff z

Tactic:
simp [h]