no goals
S : Type u_2
R : Type u_3
R₁ : Type ?u.15005
M : Type u_4
inst✝⁴ : Ring R
inst✝³ : CommRing R₁
inst✝² : AddCommGroup M
F : Type u_1
inst✝¹ : Ring S
inst✝ : AddMonoidHomClass F R S
f : M → R
g : F
x y : M
⊢ polar (↑g ∘ f) x y = ↑g (polar f x y)
simp only [polar, Pi.smul_apply, Function.comp_apply, map_sub]