case h.H
R : Type ?u.1302880
M✝ : Type ?u.1302883
inst✝¹⁷ : Semiring R
inst✝¹⁶ : AddCommMonoid M✝
inst✝¹⁵ : Module R M✝
R₁ : Type ?u.1302919
M₁ : Type ?u.1302922
inst✝¹⁴ : Ring R₁
inst✝¹³ : AddCommGroup M₁
inst✝¹² : Module R₁ M₁
R₂ : Type u_1
M₂ : Type ?u.1303534
inst✝¹¹ : CommSemiring R₂
inst✝¹⁰ : AddCommMonoid M₂
inst✝⁹ : Module R₂ M₂
R₃ : Type ?u.1303721
M₃ : Type ?u.1303724
inst✝⁸ : CommRing R₃
inst✝⁷ : AddCommGroup M₃
inst✝⁶ : Module R₃ M₃
V : Type ?u.1304312
K : Type ?u.1304315
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_2
o : Type ?u.1305532
inst✝² : Fintype n
inst✝¹ : Fintype o
inst✝ : DecidableEq n
b : Basis n R₂ M₂
M : Matrix n n R₂
x✝ y✝ : n → R₂
⊢ bilin (↑(toBilin (Pi.basisFun R₂ n)) M) x✝ y✝ = bilin (↑toBilin' M) x✝ y✝
R : Type ?u.1302880
M : Type ?u.1302883
inst✝¹⁷ : Semiring R
inst✝¹⁶ : AddCommMonoid M
inst✝¹⁵ : Module R M
R₁ : Type ?u.1302919
M₁ : Type ?u.1302922
inst✝¹⁴ : Ring R₁
inst✝¹³ : AddCommGroup M₁
inst✝¹² : Module R₁ M₁
R₂ : Type u_1
M₂ : Type ?u.1303534
inst✝¹¹ : CommSemiring R₂
inst✝¹⁰ : AddCommMonoid M₂
inst✝⁹ : Module R₂ M₂
R₃ : Type ?u.1303721
M₃ : Type ?u.1303724
inst✝⁸ : CommRing R₃
inst✝⁷ : AddCommGroup M₃
inst✝⁶ : Module R₃ M₃
V : Type ?u.1304312
K : Type ?u.1304315
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_2
o : Type ?u.1305532
inst✝² : Fintype n
inst✝¹ : Fintype o
inst✝ : DecidableEq n
b : Basis n R₂ M₂
⊢ toBilin (Pi.basisFun R₂ n) = toBilin'
ext M
no goals
case h.H
R : Type ?u.1302880
M✝ : Type ?u.1302883
inst✝¹⁷ : Semiring R
inst✝¹⁶ : AddCommMonoid M✝
inst✝¹⁵ : Module R M✝
R₁ : Type ?u.1302919
M₁ : Type ?u.1302922
inst✝¹⁴ : Ring R₁
inst✝¹³ : AddCommGroup M₁
inst✝¹² : Module R₁ M₁
R₂ : Type u_1
M₂ : Type ?u.1303534
inst✝¹¹ : CommSemiring R₂
inst✝¹⁰ : AddCommMonoid M₂
inst✝⁹ : Module R₂ M₂
R₃ : Type ?u.1303721
M₃ : Type ?u.1303724
inst✝⁸ : CommRing R₃
inst✝⁷ : AddCommGroup M₃
inst✝⁶ : Module R₃ M₃
V : Type ?u.1304312
K : Type ?u.1304315
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_2
o : Type ?u.1305532
inst✝² : Fintype n
inst✝¹ : Fintype o
inst✝ : DecidableEq n
b : Basis n R₂ M₂
M : Matrix n n R₂
x✝ y✝ : n → R₂
⊢ bilin (↑(toBilin (Pi.basisFun R₂ n)) M) x✝ y✝ = bilin (↑toBilin' M) x✝ y✝
simp only [Matrix.toBilin_apply, Matrix.toBilin'_apply, Pi.basisFun_repr]