no goals
M : Type ?u.43976
inst✝⁶ : Monoid M
R : Type ?u.43982
inst✝⁵ : Semiring R
inst✝⁴ : MulSemiringAction M R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : MulSemiringAction M S
G : Type u_1
inst✝¹ : Group G
inst✝ : MulSemiringAction G S
g : G
f : S[X]
x : S
⊢ eval (g • x) f = g • eval x (g⁻¹ • f)
rw [← smul_eval_smul, smul_inv_smul]