no goals
R : Type u_3
R₁ : Type ?u.1177421
R₂ : Type ?u.1177424
M✝ : Type ?u.1177427
M₁ : Type ?u.1177430
M₂ : Type ?u.1177433
M₁' : Type ?u.1177436
M₂' : Type ?u.1177439
n : Type u_1
m : Type u_2
n' : Type u_4
m' : Type u_5
ι : Type ?u.1177454
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing R₁
inst✝⁸ : CommRing R₂
inst✝⁷ : Fintype n
inst✝⁶ : Fintype m
inst✝⁵ : DecidableEq n
inst✝⁴ : DecidableEq m
σ₁ : R₁ →+* R
σ₂ : R₂ →+* R
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₂' (compl₁₂ (↑toLinearMap₂' M) (↑toLin' P) (↑toLin' Q)) = ↑toMatrix₂' (↑toLinearMap₂' (Pᵀ ⬝ M ⬝ Q))
simp