no goals
l : Type ?u.364914
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A✝ B A : Matrix n n α
b : n → α
h : IsUnit (det A)
⊢ det A • vecMul b A⁻¹ = ↑(cramer Aᵀ) b
rw [← A⁻¹.transpose_transpose, vecMul_transpose, transpose_nonsing_inv, ← det_transpose,
  Aᵀ.det_smul_inv_mulVec_eq_cramer _ (isUnit_det_transpose A h)]