no goals
l : Type ?u.232766
m : Type u
n : Type u'
α : Type v
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A✝ B✝ A B C : Matrix n n α
inst✝ : Invertible A
h : A⁻¹ ⬝ B = C
⊢ B = A ⬝ C
rw [← h, mul_inv_cancel_left_of_invertible]
no goals
l : Type ?u.232766
m : Type u
n : Type u'
α : Type v
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A✝ B✝ A B C : Matrix n n α
inst✝ : Invertible A
h : B = A ⬝ C
⊢ A⁻¹ ⬝ B = C
rw [h, inv_mul_cancel_left_of_invertible]