no goals
R : Type u_2
A : Type u_1
inst✝¹ : Semiring R
inst✝ : AddLeftCancelSemigroup A
g : AddMonoidAlgebra R A
a x : A
hx : x ∈ (single a 1 * g).support
⊢ ∃ b, b ∈ g.support ∧ a + b = x
rwa [support_single_mul _ _ (fun y => by rw [one_mul] : ∀ y : R, 1 * y = 0 ↔ _),
  Finset.mem_map] at hx
no goals
R : Type u_2
A : Type u_1
inst✝¹ : Semiring R
inst✝ : AddLeftCancelSemigroup A
g : AddMonoidAlgebra R A
a x : A
hx : x ∈ (single a 1 * g).support
y : R
⊢ 1 * y = 0 ↔ y = 0
rw [one_mul]