chore(linear_algebra): fix/add coe_fn simp lemmas (#7015)

* move `@[simp]` from `linear_map.comp_apply` to new
  `linear_map.coe_comp`;
* rename `linear_map.comp_coe` to `linear_map.coe_comp`, swap LHS&RHS;
* add `linear_map.coe_proj`, move `@[simp]` from `linear_map.proj_apply`.

Author: urkud

src/algebra/module/linear_map.lean

@@ -212,10 +212,9 @@ variables (f : M₂ →ₗ[R] M₃) (g : M →ₗ[R] M₂)
 /-- Composition of two linear maps is a linear map -/
 def comp : M →ₗ[R] M₃ := ⟨f ∘ g, by simp, by simp⟩
 
-@[simp] lemma comp_apply (x : M) : f.comp g x = f (g x) := rfl
+lemma comp_apply (x : M) : f.comp g x = f (g x) := rfl
 
-@[norm_cast]
-lemma comp_coe : (f : M₂ → M₃) ∘ (g : M → M₂) = f.comp g := rfl
+@[simp, norm_cast] lemma coe_comp : (f.comp g : M → M₃) = f ∘ g := rfl
 
 @[simp] theorem comp_id : f.comp id = f :=
 linear_map.ext $ λ x, rfl

src/linear_algebra/basic.lean

@@ -266,7 +266,7 @@ lemma iterate_bijective (h : bijective f') : ∀ n : ℕ, bijective ⇑(f' ^ n)
 lemma injective_of_iterate_injective {n : ℕ} (hn : n ≠ 0) (h : injective ⇑(f' ^ n)) :
   injective f' :=
 begin
-  rw [← nat.succ_pred_eq_of_pos (pos_iff_ne_zero.mpr hn), iterate_succ, ←comp_coe] at h,
+  rw [← nat.succ_pred_eq_of_pos (pos_iff_ne_zero.mpr hn), iterate_succ, coe_comp] at h,
   exact injective.of_comp h,
 end
 end

src/linear_algebra/pi.lean

@@ -60,7 +60,9 @@ rfl
 def proj (i : ι) : (Πi, φ i) →ₗ[R] φ i :=
 ⟨ λa, a i, assume f g, rfl, assume c f, rfl ⟩
 
-@[simp] lemma proj_apply (i : ι) (b : Πi, φ i) : (proj i : (Πi, φ i) →ₗ[R] φ i) b = b i := rfl
+@[simp] lemma coe_proj (i : ι) : ⇑(proj i : (Πi, φ i) →ₗ[R] φ i) = function.eval i := rfl
+
+lemma proj_apply (i : ι) (b : Πi, φ i) : (proj i : (Πi, φ i) →ₗ[R] φ i) b = b i := rfl
 
 lemma proj_pi (f : Πi, M₂ →ₗ[R] φ i) (i : ι) : (proj i).comp (pi f) = f i :=
 ext $ assume c, rfl