no goals
S : Type u_3
R : Type u_1
R₁ : Type ?u.423118
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
h : BilinForm.IsSymm B₁
x y : M
⊢ bilin (↑(associatedHom S) (toQuadraticForm B₁)) x y = bilin B₁ x y
rw [associated_toQuadraticForm, h.eq x y, ← two_mul, ← mul_assoc, invOf_mul_self,
  one_mul]