no goals
l : Type ?u.206113
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B✝ : Matrix n n α
B : Matrix n m α
h : IsUnit (det A)
⊢ A ⬝ (A⁻¹ ⬝ B) = B
simp [← Matrix.mul_assoc, mul_nonsing_inv A h]