no goals
R : Type ?u.971905
M✝ : Type ?u.971908
inst✝¹⁸ : Semiring R
inst✝¹⁷ : AddCommMonoid M✝
inst✝¹⁶ : Module R M✝
R₁ : Type ?u.971944
M₁ : Type ?u.971947
inst✝¹⁵ : Ring R₁
inst✝¹⁴ : AddCommGroup M₁
inst✝¹³ : Module R₁ M₁
R₂ : Type u_2
M₂ : Type ?u.972559
inst✝¹² : CommSemiring R₂
inst✝¹¹ : AddCommMonoid M₂
inst✝¹⁰ : Module R₂ M₂
R₃ : Type ?u.972746
M₃ : Type ?u.972749
inst✝⁹ : CommRing R₃
inst✝⁸ : AddCommGroup M₃
inst✝⁷ : Module R₃ M₃
V : Type ?u.973337
K : Type ?u.973340
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
inst✝ : DecidableEq o
M : Matrix n n R₂
P Q : Matrix n o R₂
⊢ ↑BilinForm.toMatrix' (BilinForm.comp (↑toBilin' M) (↑toLin' P) (↑toLin' Q)) =
    ↑BilinForm.toMatrix' (↑toBilin' (Pᵀ ⬝ M ⬝ Q))
simp only [BilinForm.toMatrix'_comp, BilinForm.toMatrix'_toBilin', toMatrix'_toLin']