no goals
S : Type ?u.7320
R : Type u_1
R₁ : Type ?u.7326
M : Type u_2
inst✝² : Ring R
inst✝¹ : CommRing R₁
inst✝ : AddCommGroup M
f : M → R
x y : M
⊢ polar f x y = polar f y x
rw [polar, polar, add_comm, sub_sub, sub_sub, add_comm (f x) (f y)]