R : Type ?u.1104806
M✝ : Type ?u.1104809
inst✝¹⁷ : Semiring R
inst✝¹⁶ : AddCommMonoid M✝
inst✝¹⁵ : Module R M✝
R₁ : Type ?u.1104845
M₁ : Type ?u.1104848
inst✝¹⁴ : Ring R₁
inst✝¹³ : AddCommGroup M₁
inst✝¹² : Module R₁ M₁
R₂ : Type u_2
M₂ : Type u_3
inst✝¹¹ : CommSemiring R₂
inst✝¹⁰ : AddCommMonoid M₂
inst✝⁹ : Module R₂ M₂
R₃ : Type ?u.1105647
M₃ : Type ?u.1105650
inst✝⁸ : CommRing R₃
inst✝⁷ : AddCommGroup M₃
inst✝⁶ : Module R₃ M₃
V : Type ?u.1106238
K : Type ?u.1106241
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_1
o : Type ?u.1107458
inst✝² : Fintype n
inst✝¹ : Fintype o
inst✝ : DecidableEq n
b : Basis n R₂ M₂
M : Matrix n n R₂
x y : M₂
⊢ bilin (↑(LinearEquiv.symm (BilinForm.congr (Basis.equivFun b))) (↑toBilin' M)) x y =
    ∑ i : n, ∑ j : n, ↑(↑b.repr x) i * M i j * ↑(↑b.repr y) j
R : Type ?u.1104806
M✝ : Type ?u.1104809
inst✝¹⁷ : Semiring R
inst✝¹⁶ : AddCommMonoid M✝
inst✝¹⁵ : Module R M✝
R₁ : Type ?u.1104845
M₁ : Type ?u.1104848
inst✝¹⁴ : Ring R₁
inst✝¹³ : AddCommGroup M₁
inst✝¹² : Module R₁ M₁
R₂ : Type u_2
M₂ : Type u_3
inst✝¹¹ : CommSemiring R₂
inst✝¹⁰ : AddCommMonoid M₂
inst✝⁹ : Module R₂ M₂
R₃ : Type ?u.1105647
M₃ : Type ?u.1105650
inst✝⁸ : CommRing R₃
inst✝⁷ : AddCommGroup M₃
inst✝⁶ : Module R₃ M₃
V : Type ?u.1106238
K : Type ?u.1106241
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_1
o : Type ?u.1107458
inst✝² : Fintype n
inst✝¹ : Fintype o
inst✝ : DecidableEq n
b : Basis n R₂ M₂
M : Matrix n n R₂
x y : M₂
⊢ bilin (↑(toBilin b) M) x y = ∑ i : n, ∑ j : n, ↑(↑b.repr x) i * M i j * ↑(↑b.repr y) j
rw [Matrix.toBilin, BilinForm.toMatrix, LinearEquiv.symm_trans_apply, ← Matrix.toBilin']
no goals
R : Type ?u.1104806
M✝ : Type ?u.1104809
inst✝¹⁷ : Semiring R
inst✝¹⁶ : AddCommMonoid M✝
inst✝¹⁵ : Module R M✝
R₁ : Type ?u.1104845
M₁ : Type ?u.1104848
inst✝¹⁴ : Ring R₁
inst✝¹³ : AddCommGroup M₁
inst✝¹² : Module R₁ M₁
R₂ : Type u_2
M₂ : Type u_3
inst✝¹¹ : CommSemiring R₂
inst✝¹⁰ : AddCommMonoid M₂
inst✝⁹ : Module R₂ M₂
R₃ : Type ?u.1105647
M₃ : Type ?u.1105650
inst✝⁸ : CommRing R₃
inst✝⁷ : AddCommGroup M₃
inst✝⁶ : Module R₃ M₃
V : Type ?u.1106238
K : Type ?u.1106241
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_1
o : Type ?u.1107458
inst✝² : Fintype n
inst✝¹ : Fintype o
inst✝ : DecidableEq n
b : Basis n R₂ M₂
M : Matrix n n R₂
x y : M₂
⊢ bilin (↑(LinearEquiv.symm (BilinForm.congr (Basis.equivFun b))) (↑toBilin' M)) x y =
    ∑ i : n, ∑ j : n, ↑(↑b.repr x) i * M i j * ↑(↑b.repr y) j
simp only [congr_symm, congr_apply, LinearEquiv.symm_symm, Matrix.toBilin'_apply,
  Basis.equivFun_apply]