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