no goals
R : Type u_1
M : Type u_2
inst✝¹⁴ : Semiring R
inst✝¹³ : AddCommMonoid M
inst✝¹² : Module R M
R₁ : Type ?u.37057
M₁ : Type ?u.37060
inst✝¹¹ : Ring R₁
inst✝¹⁰ : AddCommGroup M₁
inst✝⁹ : Module R₁ M₁
R₂ : Type ?u.37669
M₂ : Type ?u.37672
inst✝⁸ : CommSemiring R₂
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R₂ M₂
R₃ : Type ?u.37859
M₃ : Type ?u.37862
inst✝⁵ : CommRing R₃
inst✝⁴ : AddCommGroup M₃
inst✝³ : Module R₃ M₃
V : Type ?u.38450
K : Type ?u.38453
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
x : M
⊢ bilin B 0 x = 0
rw [← @zero_smul R _ _ _ _ (0 : M), smul_left, MulZeroClass.zero_mul]