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
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
refine' subset_antisymm (support_single_mul_subset f _ _) fun y hy => _
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
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
obtain ⟨y, yf, rfl⟩ : ∃ a : G, a ∈ f.support ∧ x * a = y := by
  simpa only [Finset.mem_image, exists_prop] using hy
no goals
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
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]
no goals
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
simpa only [Finset.mem_image, exists_prop] using hy