chore(Order/RelIso): drop a duplicate lemma (#2390)

Duplicate of `coe_fn_toEquiv` several lines below.
leanprover-community · Dec 7, 2023 · 8289b55 · 8289b55
1 parent 49c5721
commit 8289b55
Showing 1 changed file with 0 additions and 4 deletions.
diff --git a/Mathlib/Order/RelIso/Basic.lean b/Mathlib/Order/RelIso/Basic.lean
@@ -657,10 +657,6 @@ theorem coe_toRelEmbedding (f : r ≃r s) : (f.toRelEmbedding : α → β) = f :
 theorem coe_toEmbedding (f : r ≃r s) : (f.toEmbedding : α → β) = f :=
   rfl
 
-@[simp]
-theorem coe_toEquiv (f : r ≃r s) : (f.toEquiv : α → β) = f :=
-  rfl
-
 theorem map_rel_iff (f : r ≃r s) {a b} : s (f a) (f b) ↔ r a b :=
   f.map_rel_iff'
 #align rel_iso.map_rel_iff RelIso.map_rel_iff