no goals
R : Type u_1
R₁ : Type ?u.1026117
R₂ : Type ?u.1026120
M✝ : Type ?u.1026123
M₁ : Type ?u.1026126
M₂ : Type ?u.1026129
M₁' : Type ?u.1026132
M₂' : Type ?u.1026135
n : Type u_2
m : Type u_3
n' : Type u_4
m' : Type ?u.1026147
ι : Type ?u.1026150
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'
B : (n → R) →ₗ[R] (m → R) →ₗ[R] R
M : Matrix n' n R
⊢ M ⬝ ↑toMatrix₂' B = ↑toMatrix₂' (comp B (↑toLin' Mᵀ))
simp only [B.toMatrix₂'_comp, transpose_transpose, toMatrix'_toLin']