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