chore(linear_algebra/dual): prove a lemma with rfl (#18444)

I was surprised that `dsimp` didn't clean this up for me.
The proof that used to be here was certainly not interesting.

src/linear_algebra/dual.lean

@@ -118,11 +118,7 @@ instance : has_coe_to_fun (dual R M) (λ _, M → R) := ⟨linear_map.to_fun⟩
 `module.eval_equiv`. -/
 def eval : M →ₗ[R] (dual R (dual R M)) := linear_map.flip linear_map.id
 
-@[simp] lemma eval_apply (v : M) (a : dual R M) : eval R M v a = a v :=
-begin
-  dunfold eval,
-  rw [linear_map.flip_apply, linear_map.id_apply]
-end
+@[simp] lemma eval_apply (v : M) (a : dual R M) : eval R M v a = a v := rfl
 
 variables {R M} {M' : Type*} [add_comm_monoid M'] [module R M']