no goals
R : Type ?u.1715810
M✝ : Type ?u.1715813
inst✝²⁰ : Semiring R
inst✝¹⁹ : AddCommMonoid M✝
inst✝¹⁸ : Module R M✝
R₁ : Type ?u.1715849
M₁ : Type ?u.1715852
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.1716651
M₃ : Type ?u.1716654
inst✝¹¹ : CommRing R₃
inst✝¹⁰ : AddCommGroup M₃
inst✝⁹ : Module R₃ M₃
V : Type ?u.1717242
K : Type ?u.1717245
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.1718462
inst✝⁵ : Fintype n
inst✝⁴ : Fintype o
inst✝³ : DecidableEq n
b : Basis n R₂ M₂
M₂' : Type ?u.1718621
inst✝² : AddCommMonoid M₂'
inst✝¹ : Module R₂ M₂'
c : Basis o R₂ M₂'
inst✝ : DecidableEq o
B : BilinForm R₂ M₂
M : Matrix n n R₂
⊢ M ⬝ ↑(toMatrix b) B = ↑(toMatrix b) (compLeft B (↑(Matrix.toLin b b) Mᵀ))
rw [B.toMatrix_compLeft b, toMatrix_toLin, transpose_transpose]