no goals
l : Type ?u.261753
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B C : Matrix n n α
h : A ⬝ B = 1
g : C ⬝ A = 1
⊢ B = C
rw [← inv_eq_right_inv h, ← inv_eq_left_inv g]