no goals
R : Type ?u.2760443
M✝ : Type ?u.2760446
inst✝¹⁹ : Semiring R
inst✝¹⁸ : AddCommMonoid M✝
inst✝¹⁷ : Module R M✝
R₁ : Type ?u.2760482
M₁ : Type ?u.2760485
inst✝¹⁶ : Ring R₁
inst✝¹⁵ : AddCommGroup M₁
inst✝¹⁴ : Module R₁ M₁
R₂ : Type ?u.2761094
M₂ : Type ?u.2761097
inst✝¹³ : CommSemiring R₂
inst✝¹² : AddCommMonoid M₂
inst✝¹¹ : Module R₂ M₂
R₃ : Type u_2
M₃ : Type ?u.2761287
inst✝¹⁰ : CommRing R₃
inst✝⁹ : AddCommGroup M₃
inst✝⁸ : Module R₃ M₃
V : Type ?u.2761875
K : Type ?u.2761878
inst✝⁷ : Field K
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module K V
B : BilinForm R M✝
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
A : Type ?u.2763092
inst✝⁴ : CommRing A
inst✝³ : IsDomain A
inst✝² : Module A M₃
B₃ : BilinForm A M₃
ι : Type u_1
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
M : Matrix ι ι R₃
h : Matrix.Nondegenerate M
x : ι → R₃
hx : ∀ (n : ι → R₃), bilin (↑Matrix.toBilin' M) x n = 0
y : ι → R₃
⊢ x ⬝ᵥ mulVec M y = 0
simpa only [toBilin'_apply'] using hx y