[GOAL]
k : Type u₁
G : Type u₂
inst✝² : Semiring k
inst✝¹ : DecidableEq G
inst✝ : Mul G
f : MonoidAlgebra k G
r : k
a : G
⊢ (single a r * f).support ⊆ image ((fun x x_1 => x * x_1) a) f.support
[PROOFSTEP]
intro x hx
[GOAL]
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 ∈ (single a r * f).support
⊢ x ∈ image ((fun x x_1 => x * x_1) a) f.support
[PROOFSTEP]
contrapose hx
[GOAL]
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_1 => x * x_1) a) f.support
⊢ ¬x ∈ (single a r * f).support
[PROOFSTEP]
have : ∀ y, a * y = x → f y = 0 := by
  simpa only [not_and', mem_image, mem_support_iff, exists_prop, not_exists, Classical.not_not] using hx
[GOAL]
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_1 => x * x_1) a) f.support
⊢ ∀ (y : G), a * y = x → ↑f y = 0
[PROOFSTEP]
simpa only [not_and', mem_image, mem_support_iff, exists_prop, not_exists, Classical.not_not] using hx
[GOAL]
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_1 => x * x_1) a) f.support
this : ∀ (y : G), a * y = x → ↑f y = 0
⊢ ¬x ∈ (single a r * f).support
[PROOFSTEP]
simp only [mem_support_iff, mul_apply, sum_single_index, zero_mul, ite_self, sum_zero, Classical.not_not]
[GOAL]
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_1 => x * x_1) a) f.support
this : ∀ (y : G), a * y = x → ↑f y = 0
⊢ (sum f fun a₂ b₂ => if a * a₂ = x then r * b₂ else 0) = 0
[PROOFSTEP]
exact
  Finset.sum_eq_zero
    (by
      simp (config := { contextual := true }) only [this, mem_support_iff, mul_zero, Ne.def, ite_eq_right_iff,
        eq_self_iff_true, imp_true_iff])
[GOAL]
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_1 => x * x_1) a) f.support
this : ∀ (y : G), a * y = x → ↑f y = 0
⊢ ∀ (x_1 : G), x_1 ∈ f.support → (fun a₂ b₂ => if a * a₂ = x then r * b₂ else 0) x_1 (↑f x_1) = 0
[PROOFSTEP]
simp (config := { contextual := true }) only [this, mem_support_iff, mul_zero, Ne.def, ite_eq_right_iff,
  eq_self_iff_true, imp_true_iff]
[GOAL]
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
[PROOFSTEP]
intro x hx
[GOAL]
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
[PROOFSTEP]
contrapose hx
[GOAL]
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
[PROOFSTEP]
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
[GOAL]
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
[PROOFSTEP]
simpa only [not_and', mem_image, mem_support_iff, exists_prop, not_exists, Classical.not_not] using hx
[GOAL]
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
[PROOFSTEP]
simp only [mem_support_iff, mul_apply, sum_single_index, zero_mul, ite_self, sum_zero, Classical.not_not]
[GOAL]
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
[PROOFSTEP]
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])
[GOAL]
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
[PROOFSTEP]
simp (config := { contextual := true }) only [this, sum_single_index, ite_eq_right_iff, eq_self_iff_true, imp_true_iff,
  zero_mul]
[GOAL]
k : Type u₁
G : Type u₂
inst✝² : Semiring k
inst✝¹ : DecidableEq G
inst✝ : Mul G
f : MonoidAlgebra k G
r : k
hr : ∀ (y : k), r * y = 0 ↔ y = 0
x : G
lx : IsLeftRegular x
⊢ (single x r * f).support = image ((fun x x_1 => x * x_1) x) f.support
[PROOFSTEP]
refine' subset_antisymm (support_single_mul_subset f _ _) fun y hy => _
[GOAL]
k : Type u₁
G : Type u₂
inst✝² : Semiring k
inst✝¹ : DecidableEq G
inst✝ : Mul G
f : MonoidAlgebra k G
r : k
hr : ∀ (y : k), r * y = 0 ↔ y = 0
x : G
lx : IsLeftRegular x
y : G
hy : y ∈ image ((fun x x_1 => x * x_1) x) f.support
⊢ y ∈ (single x r * f).support
[PROOFSTEP]
obtain ⟨y, yf, rfl⟩ : ∃ a : G, a ∈ f.support ∧ x * a = y := by simpa only [Finset.mem_image, exists_prop] using hy
[GOAL]
k : Type u₁
G : Type u₂
inst✝² : Semiring k
inst✝¹ : DecidableEq G
inst✝ : Mul G
f : MonoidAlgebra k G
r : k
hr : ∀ (y : k), r * y = 0 ↔ y = 0
x : G
lx : IsLeftRegular x
y : G
hy : y ∈ image ((fun x x_1 => x * x_1) x) f.support
⊢ ∃ a, a ∈ f.support ∧ x * a = y
[PROOFSTEP]
simpa only [Finset.mem_image, exists_prop] using hy
[GOAL]
case intro.intro
k : Type u₁
G : Type u₂
inst✝² : Semiring k
inst✝¹ : DecidableEq G
inst✝ : Mul G
f : MonoidAlgebra k G
r : k
hr : ∀ (y : k), r * y = 0 ↔ y = 0
x : G
lx : IsLeftRegular x
y : G
yf : y ∈ f.support
hy : x * y ∈ image ((fun x x_1 => x * x_1) x) f.support
⊢ x * y ∈ (single x r * f).support
[PROOFSTEP]
simp only [mul_apply, mem_support_iff.mp yf, hr, mem_support_iff, sum_single_index, Finsupp.sum_ite_eq', Ne.def,
  not_false_iff, if_true, zero_mul, ite_self, sum_zero, lx.eq_iff]
[GOAL]
k : Type u₁
G : Type u₂
inst✝² : Semiring k
inst✝¹ : DecidableEq G
inst✝ : Mul G
f : MonoidAlgebra k G
r : k
hr : ∀ (y : k), y * r = 0 ↔ y = 0
x : G
rx : IsRightRegular x
⊢ (f * single x r).support = image (fun x_1 => x_1 * x) f.support
[PROOFSTEP]
refine' subset_antisymm (support_mul_single_subset f _ _) fun y hy => _
[GOAL]
k : Type u₁
G : Type u₂
inst✝² : Semiring k
inst✝¹ : DecidableEq G
inst✝ : Mul G
f : MonoidAlgebra k G
r : k
hr : ∀ (y : k), y * r = 0 ↔ y = 0
x : G
rx : IsRightRegular x
y : G
hy : y ∈ image (fun x_1 => x_1 * x) f.support
⊢ y ∈ (f * single x r).support
[PROOFSTEP]
obtain ⟨y, yf, rfl⟩ : ∃ a : G, a ∈ f.support ∧ a * x = y := by simpa only [Finset.mem_image, exists_prop] using hy
[GOAL]
k : Type u₁
G : Type u₂
inst✝² : Semiring k
inst✝¹ : DecidableEq G
inst✝ : Mul G
f : MonoidAlgebra k G
r : k
hr : ∀ (y : k), y * r = 0 ↔ y = 0
x : G
rx : IsRightRegular x
y : G
hy : y ∈ image (fun x_1 => x_1 * x) f.support
⊢ ∃ a, a ∈ f.support ∧ a * x = y
[PROOFSTEP]
simpa only [Finset.mem_image, exists_prop] using hy
[GOAL]
case intro.intro
k : Type u₁
G : Type u₂
inst✝² : Semiring k
inst✝¹ : DecidableEq G
inst✝ : Mul G
f : MonoidAlgebra k G
r : k
hr : ∀ (y : k), y * r = 0 ↔ y = 0
x : G
rx : IsRightRegular x
y : G
yf : y ∈ f.support
hy : y * x ∈ image (fun x_1 => x_1 * x) f.support
⊢ y * x ∈ (f * single x r).support
[PROOFSTEP]
simp only [mul_apply, mem_support_iff.mp yf, hr, mem_support_iff, sum_single_index, Finsupp.sum_ite_eq', Ne.def,
  not_false_iff, if_true, mul_zero, ite_self, sum_zero, rx.eq_iff]
[GOAL]
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
[PROOFSTEP]
classical
ext
simp only [support_mul_single_eq_image f hr (isRightRegular_of_rightCancelSemigroup x), mem_image, mem_map,
  mulRightEmbedding_apply]
[GOAL]
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
[PROOFSTEP]
ext
[GOAL]
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
[PROOFSTEP]
simp only [support_mul_single_eq_image f hr (isRightRegular_of_rightCancelSemigroup x), mem_image, mem_map,
  mulRightEmbedding_apply]
[GOAL]
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
[PROOFSTEP]
classical
ext
simp only [support_single_mul_eq_image f hr (isLeftRegular_of_leftCancelSemigroup x), mem_image, mem_map,
  mulLeftEmbedding_apply]
[GOAL]
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
[PROOFSTEP]
ext
[GOAL]
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
[PROOFSTEP]
simp only [support_single_mul_eq_image f hr (isLeftRegular_of_leftCancelSemigroup x), mem_image, mem_map,
  mulLeftEmbedding_apply]
[GOAL]
k : Type u₁
G : Type u₂
inst✝¹ : Semiring k
inst✝ : MulOneClass G
f : MonoidAlgebra k G
⊢ f ∈ Submodule.span k (↑(of k G) '' ↑f.support)
[PROOFSTEP]
erw [of, MonoidHom.coe_mk, ← supported_eq_span_single, Finsupp.mem_supported]
[GOAL]
k : Type u₁
G : Type u₂
inst✝¹ : Semiring k
inst✝ : AddZeroClass G
f : AddMonoidAlgebra k G
⊢ f ∈ Submodule.span k (↑(of k G) '' ↑f.support)
[PROOFSTEP]
erw [of, MonoidHom.coe_mk, ← Finsupp.supported_eq_span_single, Finsupp.mem_supported]
[GOAL]
k : Type u₁
G : Type u₂
inst✝ : Semiring k
f : AddMonoidAlgebra k G
⊢ f ∈ Submodule.span k (of' k G '' ↑f.support)
[PROOFSTEP]
delta of'
[GOAL]
k : Type u₁
G : Type u₂
inst✝ : Semiring k
f : AddMonoidAlgebra k G
⊢ f ∈ Submodule.span k ((fun a => single a 1) '' ↑f.support)
[PROOFSTEP]
rw [← Finsupp.supported_eq_span_single, Finsupp.mem_supported]
