diff --git a/src/topology/algebra/module.lean b/src/topology/algebra/module.lean
index 5429b4e857baf..00d78de99d85f 100644
--- a/src/topology/algebra/module.lean
+++ b/src/topology/algebra/module.lean
@@ -725,6 +725,8 @@ instance : has_coe_to_fun (M ≃L[R] M₂) := ⟨λ _, M → M₂, λ f, f⟩
 
 @[simp] theorem coe_apply (e : M ≃L[R] M₂) (b : M) : (e : M →L[R] M₂) b = e b := rfl
 
+@[simp] lemma coe_to_linear_equiv (f : M ≃L[R] M₂) : ⇑f.to_linear_equiv = f := rfl
+
 @[norm_cast] lemma coe_coe (e : M ≃L[R] M₂) : ((e : M →L[R] M₂) : M → M₂) = e := rfl
 
 @[ext] lemma ext {f g : M ≃L[R] M₂} (h : (f : M → M₂) = g) : f = g :=
diff --git a/src/topology/metric_space/isometry.lean b/src/topology/metric_space/isometry.lean
index 9186e0e52ad45..897b67f6effd7 100644
--- a/src/topology/metric_space/isometry.lean
+++ b/src/topology/metric_space/isometry.lean
@@ -125,6 +125,8 @@ instance : has_coe_to_fun (α ≃ᵢ β) := ⟨λ_, α → β, λe, e.to_equiv
 
 lemma coe_eq_to_equiv (h : α ≃ᵢ β) (a : α) : h a = h.to_equiv a := rfl
 
+@[simp] lemma coe_to_equiv (h : α ≃ᵢ β) : ⇑h.to_equiv = h := rfl
+
 protected lemma isometry (h : α ≃ᵢ β) : isometry h := h.isometry_to_fun
 
 protected lemma edist_eq (h : α ≃ᵢ β) (x y : α) : edist (h x) (h y) = edist x y :=