no goals
M : Type ?u.80364
inst✝⁴ : Monoid M
G : Type u_2
inst✝³ : Group G
inst✝² : Fintype G
R : Type u_1
inst✝¹ : CommRing R
inst✝ : MulSemiringAction G R
x : R
⊢ ↑↑↑(aeval x) (X - ↑C (ofQuotientStabilizer G x ↑1)) = 0
simp