no goals
R : Type ?u.1541084
M : Type ?u.1541087
inst✝²⁰ : Semiring R
inst✝¹⁹ : AddCommMonoid M
inst✝¹⁸ : Module R M
R₁ : Type ?u.1541123
M₁ : Type ?u.1541126
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.1541925
M₃ : Type ?u.1541928
inst✝¹¹ : CommRing R₃
inst✝¹⁰ : AddCommGroup M₃
inst✝⁹ : Module R₃ M₃
V : Type ?u.1542516
K : Type ?u.1542519
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.1543736
inst✝⁵ : Fintype n
inst✝⁴ : Fintype o
inst✝³ : DecidableEq n
b : Basis n R₂ M₂
M₂' : Type ?u.1543895
inst✝² : AddCommMonoid M₂'
inst✝¹ : Module R₂ M₂'
c : Basis o R₂ M₂'
inst✝ : DecidableEq o
B : BilinForm R₂ M₂
f : M₂ →ₗ[R₂] M₂
⊢ ↑(toMatrix b) (compRight B f) = ↑(toMatrix b) B ⬝ ↑(LinearMap.toMatrix b b) f
simp only [BilinForm.compRight, BilinForm.toMatrix_comp b b, toMatrix_id, transpose_one,
  Matrix.one_mul]