From 79cf0c5890fd87e660cff691a0d30a85a427e4ca Mon Sep 17 00:00:00 2001
From: Matthew Robert Ballard <matt@mrb.email>
Date: Thu, 9 May 2024 23:19:41 +0000
Subject: [PATCH] chore(Order.RelIso): remove some porting notes (#12786)

We get the `CoeFun` through `FunLike` which seems the current idiom. The changes are reducibly defeq to the porting remnants.
---
 Mathlib/Order/Birkhoff.lean     |  4 ++--
 Mathlib/Order/RelIso/Basic.lean | 14 --------------
 2 files changed, 2 insertions(+), 16 deletions(-)

diff --git a/Mathlib/Order/Birkhoff.lean b/Mathlib/Order/Birkhoff.lean
index 8b5858c1dbfada..a9d2359da90136 100644
--- a/Mathlib/Order/Birkhoff.lean
+++ b/Mathlib/Order/Birkhoff.lean
@@ -239,13 +239,13 @@ variable [DecidableEq α]
     birkhoffFinset (a ⊔ b) = birkhoffFinset a ∪ birkhoffFinset b := by
   dsimp [OrderEmbedding.birkhoffFinset]
   rw [birkhoffSet_sup, OrderIso.coe_toOrderEmbedding]
-  simpa using OrderIso.map_sup _ _ _
+  simp
 
 @[simp] lemma birkhoffFinset_inf (a b : α) :
     birkhoffFinset (a ⊓ b) = birkhoffFinset a ∩ birkhoffFinset b := by
   dsimp [OrderEmbedding.birkhoffFinset]
   rw [birkhoffSet_inf, OrderIso.coe_toOrderEmbedding]
-  simpa using OrderIso.map_inf _ _ _
+  simp
 
 @[simp] lemma birkhoffSet_apply (a : α) :
     birkhoffSet a = OrderIso.lowerSetSupIrred a := by
diff --git a/Mathlib/Order/RelIso/Basic.lean b/Mathlib/Order/RelIso/Basic.lean
index ba24ad0d2a56a5..272b85e1939c6d 100644
--- a/Mathlib/Order/RelIso/Basic.lean
+++ b/Mathlib/Order/RelIso/Basic.lean
@@ -228,11 +228,6 @@ def toRelHom (f : r ↪r s) : r →r s where
 instance : Coe (r ↪r s) (r →r s) :=
   ⟨toRelHom⟩
 
--- Porting note: removed
--- see Note [function coercion]
--- instance : CoeFun (r ↪r s) fun _ => α → β :=
---   ⟨fun o => o.toEmbedding⟩
-
 -- TODO: define and instantiate a `RelEmbeddingClass` when `EmbeddingLike` is defined
 instance : FunLike (r ↪r s) α β where
   coe := fun x => x.toFun
@@ -636,10 +631,6 @@ theorem toEquiv_injective : Injective (toEquiv : r ≃r s → α ≃ β)
 instance : CoeOut (r ≃r s) (r ↪r s) :=
   ⟨toRelEmbedding⟩
 
--- Porting note: moved to after `RelHomClass` instance and redefined as `DFunLike.coe`
--- instance : CoeFun (r ≃r s) fun _ => α → β :=
---   ⟨fun f => f⟩
-
 -- TODO: define and instantiate a `RelIsoClass` when `EquivLike` is defined
 instance : FunLike (r ≃r s) α β where
   coe := fun x => x
@@ -656,11 +647,6 @@ instance : EquivLike (r ≃r s) α β where
   right_inv f := f.right_inv
   coe_injective' _ _ hf _ := DFunLike.ext' hf
 
--- Porting note: helper instance
--- see Note [function coercion]
-instance : CoeFun (r ≃r s) fun _ => α → β :=
-  ⟨DFunLike.coe⟩
-
 @[simp]
 theorem coe_toRelEmbedding (f : r ≃r s) : (f.toRelEmbedding : α → β) = f :=
   rfl