no goals
R : Type ?u.834155
M✝ : Type ?u.834158
inst✝¹⁸ : Semiring R
inst✝¹⁷ : AddCommMonoid M✝
inst✝¹⁶ : Module R M✝
R₁ : Type ?u.834194
M₁ : Type ?u.834197
inst✝¹⁵ : Ring R₁
inst✝¹⁴ : AddCommGroup M₁
inst✝¹³ : Module R₁ M₁
R₂ : Type u_1
M₂ : Type ?u.834809
inst✝¹² : CommSemiring R₂
inst✝¹¹ : AddCommMonoid M₂
inst✝¹⁰ : Module R₂ M₂
R₃ : Type ?u.834996
M₃ : Type ?u.834999
inst✝⁹ : CommRing R₃
inst✝⁸ : AddCommGroup M₃
inst✝⁷ : Module R₃ M₃
V : Type ?u.835587
K : Type ?u.835590
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.836807
inst✝³ : Fintype n
inst✝² : Fintype o
inst✝¹ : DecidableEq n
inst✝ : DecidableEq o
B : BilinForm R₂ (n → R₂)
M : Matrix n n R₂
⊢ M ⬝ ↑toMatrix' B = ↑toMatrix' (compLeft B (↑Matrix.toLin' Mᵀ))
simp only [toMatrix'_compLeft, transpose_transpose, toMatrix'_toLin']