no goals
R : Type u_3
R₁ : Type ?u.1948955
R₂ : Type ?u.1948958
M✝ : Type ?u.1948961
M₁ : Type u_8
M₂ : Type u_9
M₁' : Type u_6
M₂' : Type u_7
n : Type u_1
m : Type u_2
n' : Type u_4
m' : Type u_5
ι : Type ?u.1948988
inst✝¹⁶ : CommRing R
inst✝¹⁵ : AddCommMonoid M₁
inst✝¹⁴ : Module R M₁
inst✝¹³ : AddCommMonoid M₂
inst✝¹² : Module R M₂
inst✝¹¹ : DecidableEq n
inst✝¹⁰ : Fintype n
inst✝⁹ : DecidableEq m
inst✝⁸ : Fintype m
b₁ : Basis n R M₁
b₂ : Basis m R M₂
inst✝⁷ : AddCommMonoid M₁'
inst✝⁶ : Module R M₁'
inst✝⁵ : AddCommMonoid M₂'
inst✝⁴ : Module R M₂'
b₁' : Basis n' R M₁'
b₂' : Basis m' R M₂'
inst✝³ : Fintype n'
inst✝² : Fintype m'
inst✝¹ : DecidableEq n'
inst✝ : DecidableEq m'
M : Matrix n m R
P : Matrix n n' R
Q : Matrix m m' R
⊢ ↑(toMatrix₂ b₁' b₂') (compl₁₂ (↑(toLinearMap₂ b₁ b₂) M) (↑(toLin b₁' b₁) P) (↑(toLin b₂' b₂) Q)) =
    ↑(toMatrix₂ b₁' b₂') (↑(toLinearMap₂ b₁' b₂') (Pᵀ ⬝ M ⬝ Q))
simp only [LinearMap.toMatrix₂_compl₁₂ b₁ b₂, LinearMap.toMatrix₂_toLinearMap₂,
  toMatrix_toLin]