no goals
R : Type ?u.1830938
M✝ : Type ?u.1830941
inst✝²⁰ : Semiring R
inst✝¹⁹ : AddCommMonoid M✝
inst✝¹⁸ : Module R M✝
R₁ : Type ?u.1830977
M₁ : Type ?u.1830980
inst✝¹⁷ : Ring R₁
inst✝¹⁶ : AddCommGroup M₁
inst✝¹⁵ : Module R₁ M₁
R₂ : Type u_2
M₂ : Type u_5
inst✝¹⁴ : CommSemiring R₂
inst✝¹³ : AddCommMonoid M₂
inst✝¹² : Module R₂ M₂
R₃ : Type ?u.1831779
M₃ : Type ?u.1831782
inst✝¹¹ : CommRing R₃
inst✝¹⁰ : AddCommGroup M₃
inst✝⁹ : Module R₃ M₃
V : Type ?u.1832370
K : Type ?u.1832373
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_3
inst✝⁵ : Fintype n
inst✝⁴ : Fintype o
inst✝³ : DecidableEq n
b : Basis n R₂ M₂
M₂' : Type u_4
inst✝² : AddCommMonoid M₂'
inst✝¹ : Module R₂ M₂'
c : Basis o R₂ M₂'
inst✝ : DecidableEq o
M : Matrix n n R₂
P Q : Matrix n o R₂
⊢ ↑(BilinForm.toMatrix c) (BilinForm.comp (↑(toBilin b) M) (↑(toLin c b) P) (↑(toLin c b) Q)) =
    ↑(BilinForm.toMatrix c) (↑(toBilin c) (Pᵀ ⬝ M ⬝ Q))
simp only [BilinForm.toMatrix_comp b c, BilinForm.toMatrix_toBilin, toMatrix_toLin]