no goals
l : Type ?u.5121
m : Type u
n : Type u'
α : Type v
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A : Matrix n n α
B : Matrix n m α
inst✝ : Invertible A
⊢ ⅟A ⬝ (A ⬝ B) = B
rw [← Matrix.mul_assoc, Matrix.invOf_mul_self, Matrix.one_mul]