diff --git a/src/algebra/module/submodule.lean b/src/algebra/module/submodule.lean
index 093b0fa09b012..77975f8fbe5f7 100644
--- a/src/algebra/module/submodule.lean
+++ b/src/algebra/module/submodule.lean
@@ -204,7 +204,7 @@ by refine {to_fun := coe, ..}; simp [coe_smul]
 
 @[simp] theorem subtype_apply (x : p) : p.subtype x = x := rfl
 
-lemma subtype_eq_val : ((submodule.subtype p) : p → M) = subtype.val := rfl
+lemma coe_subtype : ((submodule.subtype p) : p → M) = coe := rfl
 
 /-- Note the `add_submonoid` version of this lemma is called `add_submonoid.coe_finset_sum`. -/
 @[simp] lemma coe_sum (x : ι → p) (s : finset ι) : ↑(∑ i in s, x i) = ∑ i in s, (x i : M) :=
diff --git a/src/linear_algebra/basis.lean b/src/linear_algebra/basis.lean
index 89d4e2f3d57ed..76728f562d5df 100644
--- a/src/linear_algebra/basis.lean
+++ b/src/linear_algebra/basis.lean
@@ -926,11 +926,12 @@ basis.mk (linear_independent_span hli) $
 begin
   rw eq_top_iff,
   intros x _,
-  have h₁ : subtype.val '' set.range (λ i, subtype.mk (v i) _) = range v,
-  { rw ← set.range_comp },
+  have h₁ : (coe : span R (range v) → M) '' set.range (λ i, subtype.mk (v i) _) = range v,
+  { rw ← set.range_comp,
+    refl },
   have h₂ : map (submodule.subtype _) (span R (set.range (λ i, subtype.mk (v i) _)))
     = span R (range v),
-  { rw [← span_image, submodule.subtype_eq_val, h₁] },
+  { rw [← span_image, submodule.coe_subtype, h₁] },
   have h₃ : (x : M) ∈ map (submodule.subtype _) (span R (set.range (λ i, subtype.mk (v i) _))),
   { rw h₂, apply subtype.mem x },
   rcases mem_map.1 h₃ with ⟨y, hy₁, hy₂⟩,
diff --git a/src/linear_algebra/finite_dimensional.lean b/src/linear_algebra/finite_dimensional.lean
index 33d4121e96c75..ee2699074a15b 100644
--- a/src/linear_algebra/finite_dimensional.lean
+++ b/src/linear_algebra/finite_dimensional.lean
@@ -348,15 +348,16 @@ begin
   set b := basis.extend this with b_eq,
   letI : fintype (this.extend _) :=
     (finite_of_linear_independent (by simpa using b.linear_independent)).fintype,
-  letI : fintype (subtype.val '' basis.of_vector_space_index K S) :=
+  letI : fintype (coe '' basis.of_vector_space_index K S) :=
     (finite_of_linear_independent this).fintype,
   letI : fintype (basis.of_vector_space_index K S) :=
     (finite_of_linear_independent (by simpa using bS.linear_independent)).fintype,
-  have : subtype.val '' (basis.of_vector_space_index K S) = this.extend (set.subset_univ _),
+  have : coe '' (basis.of_vector_space_index K S) = this.extend (set.subset_univ _),
   from set.eq_of_subset_of_card_le (this.subset_extend _)
-    (by rw [set.card_image_of_injective _ subtype.val_injective, ← finrank_eq_card_basis bS,
+    (by rw [set.card_image_of_injective _ subtype.coe_injective, ← finrank_eq_card_basis bS,
          ← finrank_eq_card_basis b, h]; apply_instance),
-  rw [← b.span_eq, b_eq, basis.coe_extend, subtype.range_coe, ← this, ← subtype_eq_val, span_image],
+  rw [← b.span_eq, b_eq, basis.coe_extend, subtype.range_coe, ← this, ← submodule.coe_subtype,
+    span_image],
   have := bS.span_eq,
   rw [bS_eq, basis.coe_of_vector_space, subtype.range_coe] at this,
   rw [this, map_top (submodule.subtype S), range_subtype],