k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
a : G
x : AddMonoidAlgebra k G
x✝ : G
⊢ ↑(of' k G a * x /ᵒᶠ a) x✝ = ↑x x✝
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
a : G
x : AddMonoidAlgebra k G
⊢ of' k G a * x /ᵒᶠ a = x
refine Finsupp.ext fun _ => ?_
case H
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
a : G
x : AddMonoidAlgebra k G
x✝ : G
⊢ ∀ (a_1 : G), a + a_1 = a + x✝ ↔ a_1 = x✝
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
a : G
x : AddMonoidAlgebra k G
x✝ : G
⊢ ↑(of' k G a * x /ᵒᶠ a) x✝ = ↑x x✝
rw [AddMonoidAlgebra.divOf_apply, of'_apply, single_mul_apply_aux, one_mul]
case H
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
a : G
x : AddMonoidAlgebra k G
x✝ c : G
⊢ a + c = a + x✝ ↔ c = x✝
case H
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
a : G
x : AddMonoidAlgebra k G
x✝ : G
⊢ ∀ (a_1 : G), a + a_1 = a + x✝ ↔ a_1 = x✝
intro c
no goals
case H
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
a : G
x : AddMonoidAlgebra k G
x✝ c : G
⊢ a + c = a + x✝ ↔ c = x✝
exact add_right_inj _