no goals
S : Type u_3
R : Type u_1
R₁ : Type ?u.416813
M : Type u_2
inst✝⁷ : Ring R
inst✝⁶ : CommRing R₁
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module R₁ M
inst✝² : CommSemiring S
inst✝¹ : Algebra S R
inst✝ : Invertible 2
B₁ : BilinForm R M
Q : QuadraticForm R M
B : BilinForm R M
x y : M
⊢ bilin (↑(associatedHom S) (toQuadraticForm B)) x y = ⅟2 * (bilin B x y + bilin B y x)
simp only [associated_apply, ← polar_to_quadratic_form, polar, toQuadraticForm_apply]