no goals
S : Type ?u.369777
R : Type u_1
R₁ : Type ?u.369783
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : BilinForm R M
x y : M
⊢ polar (fun x => bilin B x x) x y = bilin B x y + bilin B y x
simp only [add_assoc, add_sub_cancel', add_right, polar, add_left_inj, add_neg_cancel_left,
  add_left, sub_eq_add_neg _ (B y y), add_comm (B y x) _]