no goals
R : Type ?u.1598572
M : Type ?u.1598575
inst✝²⁰ : Semiring R
inst✝¹⁹ : AddCommMonoid M
inst✝¹⁸ : Module R M
R₁ : Type ?u.1598611
M₁ : Type ?u.1598614
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.1599413
M₃ : Type ?u.1599416
inst✝¹¹ : CommRing R₃
inst✝¹⁰ : AddCommGroup M₃
inst✝⁹ : Module R₃ M₃
V : Type ?u.1600004
K : Type ?u.1600007
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_4
o : Type u_1
inst✝⁵ : Fintype n
inst✝⁴ : Fintype o
inst✝³ : DecidableEq n
b : Basis n R₂ M₂
M₂' : Type ?u.1601383
inst✝² : AddCommMonoid M₂'
inst✝¹ : Module R₂ M₂'
c✝ : Basis o R₂ M₂'
inst✝ : DecidableEq o
c : Basis o R₂ M₂
B : BilinForm R₂ M₂
⊢ (Basis.toMatrix b ↑c)ᵀ ⬝ ↑(toMatrix b) B ⬝ Basis.toMatrix b ↑c = ↑(toMatrix c) B
rw [← LinearMap.toMatrix_id_eq_basis_toMatrix, ← BilinForm.toMatrix_comp, BilinForm.comp_id_id]