no goals
S : Type u_1
R : Type u_2
R₁ : Type ?u.3579
M : Type u_3
inst✝⁴ : Ring R
inst✝³ : CommRing R₁
inst✝² : AddCommGroup M
inst✝¹ : Monoid S
inst✝ : DistribMulAction S R
f : M → R
s : S
x y : M
⊢ polar (s • f) x y = s • polar f x y
simp only [polar, Pi.smul_apply, smul_sub]