no goals
R : Type ?u.1833309
M : Type ?u.1833312
inst✝¹⁷ : Semiring R
inst✝¹⁶ : AddCommMonoid M
inst✝¹⁵ : Module R M
R₁ : Type ?u.1833348
M₁ : Type ?u.1833351
inst✝¹⁴ : Ring R₁
inst✝¹³ : AddCommGroup M₁
inst✝¹² : Module R₁ M₁
R₂ : Type ?u.1833960
M₂ : Type ?u.1833963
inst✝¹¹ : CommSemiring R₂
inst✝¹⁰ : AddCommMonoid M₂
inst✝⁹ : Module R₂ M₂
R₃ : Type ?u.1834150
M₃ : Type ?u.1834153
inst✝⁸ : CommRing R₃
inst✝⁷ : AddCommGroup M₃
inst✝⁶ : Module R₃ M₃
V : Type u_2
K : Type u_1
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.1835958
inst✝² : AddCommMonoid M₂'
inst✝¹ : Module R₂ M₂'
inst✝ : FiniteDimensional K V
B₁ B₂ : BilinForm K V
b₂ : Nondegenerate B₂
v : V
⊢ ↑(↑toLin B₂) (↑(symmCompOfNondegenerate B₁ B₂ b₂) v) = ↑(↑toLin B₁) v
erw [symmCompOfNondegenerate, LinearEquiv.apply_symm_apply (B₂.toDual b₂) _]