no goals
l : Type ?u.360583
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 • mulVec A⁻¹ b = ↑(cramer A) b
rw [cramer_eq_adjugate_mulVec, A.nonsing_inv_apply h, ← smul_mulVec_assoc, smul_smul,
  h.mul_val_inv, one_smul]