k : Type u₁
G : Type u₂
inst✝² : Semiring k
inst✝¹ : DecidableEq G
inst✝ : Mul G
f : MonoidAlgebra k G
r : k
a x : G
hx : x ∈ (f * single a r).support
⊢ x ∈ image (fun x => x * a) f.support
k : Type u₁
G : Type u₂
inst✝² : Semiring k
inst✝¹ : DecidableEq G
inst✝ : Mul G
f : MonoidAlgebra k G
r : k
a : G
⊢ (f * single a r).support ⊆ image (fun x => x * a) f.support
intro x hx
k : Type u₁
G : Type u₂
inst✝² : Semiring k
inst✝¹ : DecidableEq G
inst✝ : Mul G
f : MonoidAlgebra k G
r : k
a x : G
hx : ¬x ∈ image (fun x => x * a) f.support
⊢ ¬x ∈ (f * single a r).support
k : Type u₁
G : Type u₂
inst✝² : Semiring k
inst✝¹ : DecidableEq G
inst✝ : Mul G
f : MonoidAlgebra k G
r : k
a x : G
hx : x ∈ (f * single a r).support
⊢ x ∈ image (fun x => x * a) f.support
contrapose hx
k : Type u₁
G : Type u₂
inst✝² : Semiring k
inst✝¹ : DecidableEq G
inst✝ : Mul G
f : MonoidAlgebra k G
r : k
a x : G
hx : ¬x ∈ image (fun x => x * a) f.support
this : ∀ (y : G), y * a = x → ↑f y = 0
⊢ ¬x ∈ (f * single a r).support
k : Type u₁
G : Type u₂
inst✝² : Semiring k
inst✝¹ : DecidableEq G
inst✝ : Mul G
f : MonoidAlgebra k G
r : k
a x : G
hx : ¬x ∈ image (fun x => x * a) f.support
⊢ ¬x ∈ (f * single a r).support
have : ∀ y, y * a = x → f y = 0 := by
  simpa only [not_and', mem_image, mem_support_iff, exists_prop, not_exists,
    Classical.not_not] using hx
k : Type u₁
G : Type u₂
inst✝² : Semiring k
inst✝¹ : DecidableEq G
inst✝ : Mul G
f : MonoidAlgebra k G
r : k
a x : G
hx : ¬x ∈ image (fun x => x * a) f.support
this : ∀ (y : G), y * a = x → ↑f y = 0
⊢ (sum f fun a₁ b₁ => sum (single a r) fun a₂ b₂ => if a₁ * a₂ = x then b₁ * b₂ else 0) = 0
k : Type u₁
G : Type u₂
inst✝² : Semiring k
inst✝¹ : DecidableEq G
inst✝ : Mul G
f : MonoidAlgebra k G
r : k
a x : G
hx : ¬x ∈ image (fun x => x * a) f.support
this : ∀ (y : G), y * a = x → ↑f y = 0
⊢ ¬x ∈ (f * single a r).support
simp only [mem_support_iff, mul_apply, sum_single_index, zero_mul, ite_self, sum_zero,
  Classical.not_not]
no goals
k : Type u₁
G : Type u₂
inst✝² : Semiring k
inst✝¹ : DecidableEq G
inst✝ : Mul G
f : MonoidAlgebra k G
r : k
a x : G
hx : ¬x ∈ image (fun x => x * a) f.support
this : ∀ (y : G), y * a = x → ↑f y = 0
⊢ (sum f fun a₁ b₁ => sum (single a r) fun a₂ b₂ => if a₁ * a₂ = x then b₁ * b₂ else 0) = 0
exact
  Finset.sum_eq_zero
    (by
      simp (config := { contextual := true }) only [this, sum_single_index, ite_eq_right_iff,
        eq_self_iff_true, imp_true_iff, zero_mul])
no goals
k : Type u₁
G : Type u₂
inst✝² : Semiring k
inst✝¹ : DecidableEq G
inst✝ : Mul G
f : MonoidAlgebra k G
r : k
a x : G
hx : ¬x ∈ image (fun x => x * a) f.support
⊢ ∀ (y : G), y * a = x → ↑f y = 0
simpa only [not_and', mem_image, mem_support_iff, exists_prop, not_exists,
  Classical.not_not] using hx
no goals
k : Type u₁
G : Type u₂
inst✝² : Semiring k
inst✝¹ : DecidableEq G
inst✝ : Mul G
f : MonoidAlgebra k G
r : k
a x : G
hx : ¬x ∈ image (fun x => x * a) f.support
this : ∀ (y : G), y * a = x → ↑f y = 0
⊢ ∀ (x_1 : G),
    x_1 ∈ f.support → (fun a₁ b₁ => sum (single a r) fun a₂ b₂ => if a₁ * a₂ = x then b₁ * b₂ else 0) x_1 (↑f x_1) = 0
simp (config := { contextual := true }) only [this, sum_single_index, ite_eq_right_iff,
  eq_self_iff_true, imp_true_iff, zero_mul]