no goals
k : Type u₁
G : Type u₂
inst✝¹ : Semiring k
inst✝ : RightCancelSemigroup G
f : MonoidAlgebra k G
r : k
hr : ∀ (y : k), y * r = 0 ↔ y = 0
x : G
⊢ (f * single x r).support = map (mulRightEmbedding x) f.support
classical
  ext
  simp only [support_mul_single_eq_image f hr (isRightRegular_of_rightCancelSemigroup x),
    mem_image, mem_map, mulRightEmbedding_apply]
case a
k : Type u₁
G : Type u₂
inst✝¹ : Semiring k
inst✝ : RightCancelSemigroup G
f : MonoidAlgebra k G
r : k
hr : ∀ (y : k), y * r = 0 ↔ y = 0
x a✝ : G
⊢ a✝ ∈ (f * single x r).support ↔ a✝ ∈ map (mulRightEmbedding x) f.support
k : Type u₁
G : Type u₂
inst✝¹ : Semiring k
inst✝ : RightCancelSemigroup G
f : MonoidAlgebra k G
r : k
hr : ∀ (y : k), y * r = 0 ↔ y = 0
x : G
⊢ (f * single x r).support = map (mulRightEmbedding x) f.support
ext
no goals
case a
k : Type u₁
G : Type u₂
inst✝¹ : Semiring k
inst✝ : RightCancelSemigroup G
f : MonoidAlgebra k G
r : k
hr : ∀ (y : k), y * r = 0 ↔ y = 0
x a✝ : G
⊢ a✝ ∈ (f * single x r).support ↔ a✝ ∈ map (mulRightEmbedding x) f.support
simp only [support_mul_single_eq_image f hr (isRightRegular_of_rightCancelSemigroup x),
  mem_image, mem_map, mulRightEmbedding_apply]