no goals
S : Type ?u.213182
R : Type u_1
R₁ : Type ?u.213188
M : Type u_2
inst✝⁷ : Ring R
inst✝⁶ : CommRing R₁
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
Q : QuadraticForm R M
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
x y : M
⊢ BilinForm.bilin (Exists.choose (_ : ∃ B, ∀ (x y : M), ↑Q (x + y) = ↑Q x + ↑Q y + BilinForm.bilin B x y)) x y =
    BilinForm.bilin (polarBilin Q) x y
rw [polarBilin_apply, polar, Q.exists_companion.choose_spec, sub_sub, add_sub_cancel']