no goals
R : Type u_1
M : Type u_2
inst✝²⁰ : Semiring R
inst✝¹⁹ : AddCommMonoid M
inst✝¹⁸ : Module R M
R₁ : Type ?u.1026415
M₁ : Type ?u.1026418
inst✝¹⁷ : Ring R₁
inst✝¹⁶ : AddCommGroup M₁
inst✝¹⁵ : Module R₁ M₁
R₂ : Type ?u.1027027
M₂ : Type ?u.1027030
inst✝¹⁴ : CommSemiring R₂
inst✝¹³ : AddCommMonoid M₂
inst✝¹² : Module R₂ M₂
R₃ : Type ?u.1027217
M₃ : Type ?u.1027220
inst✝¹¹ : CommRing R₃
inst✝¹⁰ : AddCommGroup M₃
inst✝⁹ : Module R₃ M₃
V : Type ?u.1027808
K : Type ?u.1027811
inst✝⁸ : Field K
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module K V
B : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
M₂' : Type ?u.1029025
M₂'' : Type ?u.1029028
inst✝⁵ : AddCommMonoid M₂'
inst✝⁴ : AddCommMonoid M₂''
inst✝³ : Module R₂ M₂'
inst✝² : Module R₂ M₂''
F : BilinForm R M
M' : Type u_3
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
B' : BilinForm R M'
f f' : M →ₗ[R] M'
g g' : M' →ₗ[R] M
x : M
y : M'
⊢ bilin B' (↑0 x) y = bilin B x (↑0 y)
simp only [BilinForm.zero_left, BilinForm.zero_right, LinearMap.zero_apply]