no goals
M : Type ?u.48740
inst✝⁶ : Monoid M
R : Type ?u.48746
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 x (g • f) = g • eval (g⁻¹ • x) f
rw [← smul_eval_smul, smul_inv_smul]