no goals
k : Type u₁
G : Type u₂
R : Type ?u.494305
inst✝¹ : Semiring k
inst✝ : Mul G
f : MonoidAlgebra k G
r : k
x y z : G
H : ∀ (a : G), a * x = z ↔ a = y
⊢ ↑(f * single x r) z = ↑f y * r
classical exact
    have A :
      ∀ a₁ b₁,
        ((single x r).sum fun a₂ b₂ => ite (a₁ * a₂ = z) (b₁ * b₂) 0) =
          ite (a₁ * x = z) (b₁ * r) 0 :=
      fun a₁ b₁ => sum_single_index <| by simp
    calc
      (HMul.hMul (β := MonoidAlgebra k G) f (single x r)) z =
          sum f fun a b => if a = y then b * r else 0 := by simp only [mul_apply, A, H]
      _ = if y ∈ f.support then f y * r else 0 := (f.support.sum_ite_eq' _ _)
      _ = f y * r := by split_ifs with h <;> simp at h <;> simp [h]
no goals
k : Type u₁
G : Type u₂
R : Type ?u.494305
inst✝¹ : Semiring k
inst✝ : Mul G
f : MonoidAlgebra k G
r : k
x y z : G
H : ∀ (a : G), a * x = z ↔ a = y
⊢ ↑(f * single x r) z = ↑f y * r
exact
have A :
∀ a₁ b₁,
((single x r).sum fun a₂ b₂ => ite (a₁ * a₂ = z) (b₁ * b₂) 0) =
ite (a₁ * x = z) (b₁ * r) 0 :=
fun a₁ b₁ => sum_single_index <| by simp
calc
(HMul.hMul (β := MonoidAlgebra k G) f (single x r)) z =
sum f fun a b => if a = y then b * r else 0 := by simp only [mul_apply, A, H]
_ = if y ∈ f.support then f y * r else 0 := (f.support.sum_ite_eq' _ _)
_ = f y * r := by split_ifs with h <;> simp at h <;> simp [h]
no goals
k : Type u₁
G : Type u₂
R : Type ?u.494305
inst✝¹ : Semiring k
inst✝ : Mul G
f : MonoidAlgebra 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₁ * 0 else 0) = 0
simp
no goals
k : Type u₁
G : Type u₂
R : Type ?u.494305
inst✝¹ : Semiring k
inst✝ : Mul G
f : MonoidAlgebra 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₂ b₂ => if a₁ * a₂ = z then b₁ * b₂ else 0) = if a₁ * x = z then b₁ * r else 0
⊢ ↑(f * single x r) z = sum f fun a b => if a = y then b * r else 0
simp only [mul_apply, A, H]
no goals
k : Type u₁
G : Type u₂
R : Type ?u.494305
inst✝¹ : Semiring k
inst✝ : Mul G
f : MonoidAlgebra 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₂ b₂ => if a₁ * a₂ = z then b₁ * b₂ else 0) = if a₁ * x = z then b₁ * r else 0
⊢ (if y ∈ f.support then ↑f y * r else 0) = ↑f y * r
split_ifs with h <;> simp at h <;> simp [h]