no goals
R : Type ?u.1169905
M : Type ?u.1169908
inst✝¹⁷ : Semiring R
inst✝¹⁶ : AddCommMonoid M
inst✝¹⁵ : Module R M
R₁ : Type ?u.1169944
M₁ : Type ?u.1169947
inst✝¹⁴ : Ring R₁
inst✝¹³ : AddCommGroup M₁
inst✝¹² : Module R₁ M₁
R₂ : Type u_1
M₂ : Type u_2
inst✝¹¹ : CommSemiring R₂
inst✝¹⁰ : AddCommMonoid M₂
inst✝⁹ : Module R₂ M₂
R₃ : Type ?u.1170746
M₃ : Type ?u.1170749
inst✝⁸ : CommRing R₃
inst✝⁷ : AddCommGroup M₃
inst✝⁶ : Module R₃ M₃
V : Type ?u.1171337
K : Type ?u.1171340
inst✝⁵ : Field K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
B✝ : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
n : Type u_3
o : Type ?u.1172557
inst✝² : Fintype n
inst✝¹ : Fintype o
inst✝ : DecidableEq n
b : Basis n R₂ M₂
B : BilinForm R₂ M₂
i j : n
⊢ ↑(toMatrixAux ↑b) B i j = ↑(BilinForm.toMatrix b) B i j
rw [BilinForm.toMatrix_apply, BilinForm.toMatrixAux_apply]