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