no goals
l : Type ?u.184059
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
⊢ A⁻¹ᵀ = Aᵀ⁻¹
rw [inv_def, inv_def, transpose_smul, det_transpose, adjugate_transpose]