-- Mathlib/Algebra/MonoidAlgebra/Defs.lean
theorem mul_apply [DecidableEq G] [Mul G] (f g : MonoidAlgebra k G) (x : G) :
    (f * g) x = f.sum fun a₁ b₁ => g.sum fun a₂ b₂ => if a₁ * a₂ = x then b₁ * b₂ else 0

Proof state:
k : Type u₁
G : Type u₂
inst✝² : Semiring k
inst✝¹ : DecidableEq G
inst✝ : Mul G
f g : MonoidAlgebra k G
x : G
⊢ (sum f fun a₁ b => (sum g fun a₂ b₂ => single (a₁ * a₂) (b * b₂)) x) =
    sum f fun a₁ b₁ => sum g fun a₂ b₂ => if a₁ * a₂ = x then b₁ * b₂ else 0

Tactic:
congr

Result:
case e_g
k : Type u₁
G : Type u₂
inst✝² : Semiring k
inst✝¹ : DecidableEq G
inst✝ : Mul G
f g : MonoidAlgebra k G
x : G
⊢ (fun a₁ b => (sum g fun a₂ b₂ => single (a₁ * a₂) (b * b₂)) x) = fun a₁ b₁ =>
    sum g fun a₂ b₂ => if a₁ * a₂ = x then b₁ * b₂ else 0

Proof state:
case e_g.h.h.e_g
k : Type u₁
G : Type u₂
inst✝² : Semiring k
inst✝¹ : DecidableEq G
inst✝ : Mul G
f g : MonoidAlgebra k G
x x✝¹ : G
x✝ : k
⊢ (fun a₁ b => (single (x✝¹ * a₁) (x✝ * b)) x) = fun a₂ b₂ => if x✝¹ * a₂ = x then x✝ * b₂ else 0

Tactic:
ext

Result:
case e_g.h.h.e_g.h.h
k : Type u₁
G : Type u₂
inst✝² : Semiring k
inst✝¹ : DecidableEq G
inst✝ : Mul G
f g : MonoidAlgebra k G
x x✝³ : G
x✝² : k
x✝¹ : G
x✝ : k
⊢ (single (x✝³ * x✝¹) (x✝² * x✝)) x = if x✝³ * x✝¹ = x then x✝² * x✝ else 0

Proof state:
k : Type u₁
G : Type u₂
inst✝² : Semiring k
inst✝¹ : DecidableEq G
inst✝ : Mul G
f g : MonoidAlgebra k G
x : G
⊢ (f * g) x = sum f fun a₁ b₁ => sum g fun a₂ b₂ => if a₁ * a₂ = x then b₁ * b₂ else 0

Tactic:
rw [mul_def, Finsupp.sum_apply]

Result:
k : Type u₁
G : Type u₂
inst✝² : Semiring k
inst✝¹ : DecidableEq G
inst✝ : Mul G
f g : MonoidAlgebra k G
x : G
⊢ (sum f fun a₁ b => (sum g fun a₂ b₂ => single (a₁ * a₂) (b * b₂)) x) =
    sum f fun a₁ b₁ => sum g fun a₂ b₂ => if a₁ * a₂ = x then b₁ * b₂ else 0

Proof state:
case e_g.h.h.e_g.h.h
k : Type u₁
G : Type u₂
inst✝² : Semiring k
inst✝¹ : DecidableEq G
inst✝ : Mul G
f g : MonoidAlgebra k G
x x✝³ : G
x✝² : k
x✝¹ : G
x✝ : k
⊢ (single (x✝³ * x✝¹) (x✝² * x✝)) x = if x✝³ * x✝¹ = x then x✝² * x✝ else 0

Tactic:
apply single_apply

Result:
no goals

Proof state:
case e_g.h.h
k : Type u₁
G : Type u₂
inst✝² : Semiring k
inst✝¹ : DecidableEq G
inst✝ : Mul G
f g : MonoidAlgebra k G
x x✝¹ : G
x✝ : k
⊢ (sum g fun a₂ b₂ => single (x✝¹ * a₂) (x✝ * b₂)) x = sum g fun a₂ b₂ => if x✝¹ * a₂ = x then x✝ * b₂ else 0

Tactic:
rw [Finsupp.sum_apply]

Result:
case e_g.h.h
k : Type u₁
G : Type u₂
inst✝² : Semiring k
inst✝¹ : DecidableEq G
inst✝ : Mul G
f g : MonoidAlgebra k G
x x✝¹ : G
x✝ : k
⊢ (sum g fun a₁ b => (single (x✝¹ * a₁) (x✝ * b)) x) = sum g fun a₂ b₂ => if x✝¹ * a₂ = x then x✝ * b₂ else 0

Proof state:
case e_g
k : Type u₁
G : Type u₂
inst✝² : Semiring k
inst✝¹ : DecidableEq G
inst✝ : Mul G
f g : MonoidAlgebra k G
x : G
⊢ (fun a₁ b => (sum g fun a₂ b₂ => single (a₁ * a₂) (b * b₂)) x) = fun a₁ b₁ =>
    sum g fun a₂ b₂ => if a₁ * a₂ = x then b₁ * b₂ else 0

Tactic:
ext

Result:
case e_g.h.h
k : Type u₁
G : Type u₂
inst✝² : Semiring k
inst✝¹ : DecidableEq G
inst✝ : Mul G
f g : MonoidAlgebra k G
x x✝¹ : G
x✝ : k
⊢ (sum g fun a₂ b₂ => single (x✝¹ * a₂) (x✝ * b₂)) x = sum g fun a₂ b₂ => if x✝¹ * a₂ = x then x✝ * b₂ else 0

Proof state:
case e_g.h.h
k : Type u₁
G : Type u₂
inst✝² : Semiring k
inst✝¹ : DecidableEq G
inst✝ : Mul G
f g : MonoidAlgebra k G
x x✝¹ : G
x✝ : k
⊢ (sum g fun a₁ b => (single (x✝¹ * a₁) (x✝ * b)) x) = sum g fun a₂ b₂ => if x✝¹ * a₂ = x then x✝ * b₂ else 0

Tactic:
congr

Result:
case e_g.h.h.e_g
k : Type u₁
G : Type u₂
inst✝² : Semiring k
inst✝¹ : DecidableEq G
inst✝ : Mul G
f g : MonoidAlgebra k G
x x✝¹ : G
x✝ : k
⊢ (fun a₁ b => (single (x✝¹ * a₁) (x✝ * b)) x) = fun a₂ b₂ => if x✝¹ * a₂ = x then x✝ * b₂ else 0