chore(linear_algebra/basic): make linear_map.id_coe elegible for `d…

…simp` (#12334) `dsimp` only considers lemmas which _are_ proved by `rfl`, not ones that just _could_ be.
leanprover-community · Feb 27, 2022 · dfacfd3 · dfacfd3
1 parent f322fa0
commit dfacfd3
Show file tree

Hide file tree

Showing 2 changed files with 1 addition and 3 deletions.
diff --git a/src/algebra/module/linear_map.lean b/src/algebra/module/linear_map.lean
@@ -145,8 +145,7 @@ def id : M →ₗ[R] M :=
 lemma id_apply (x : M) :
   @id R M _ _ _ x = x := rfl
 
-@[simp, norm_cast] lemma id_coe : ((linear_map.id : M →ₗ[R] M) : M → M) = _root_.id :=
-by { ext x, refl }
+@[simp, norm_cast] lemma id_coe : ((linear_map.id : M →ₗ[R] M) : M → M) = _root_.id := rfl
 
 end
 

diff --git a/src/linear_algebra/finsupp.lean b/src/linear_algebra/finsupp.lean
@@ -958,7 +958,6 @@ begin
   ext x y,
   dsimp [splitting_of_fun_on_fintype_surjective],
   rw [linear_equiv_fun_on_fintype_symm_single, finsupp.sum_single_index, one_smul,
-    linear_map.id_coe, id_def,
     (s (finsupp.single x 1)).some_spec, finsupp.single_eq_pi_single],
   rw [zero_smul],
 end