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