Feat: add a FunLike and an EmbeddingLike instance (#1488)

Backported in leanprover-community/mathlib#18198.

Mathlib/Data/PEquiv.lean

@@ -68,33 +68,27 @@ variable {α : Type u} {β : Type v} {γ : Type w} {δ : Type x}
 
 open Function Option
 
-instance : CoeFun (α ≃. β) fun _ => α → Option β :=
-  ⟨toFun⟩
+instance : FunLike (α ≃. β) α fun _ => Option β :=
+  { coe := toFun
+    coe_injective' := by
+      rintro ⟨f₁, f₂, hf⟩ ⟨g₁, g₂, hg⟩ (rfl : f₁ = g₁)
+      congr with y x
+      simp only [hf, hg] }
+
+@[simp] theorem coe_mk (f₁ : α → Option β) (f₂ h) : (mk f₁ f₂ h : α → Option β) = f₁ :=
+  rfl
 
 theorem coe_mk_apply (f₁ : α → Option β) (f₂ : β → Option α) (h) (x : α) :
     (PEquiv.mk f₁ f₂ h : α → Option β) x = f₁ x :=
-  by simp
+  rfl
 #align pequiv.coe_mk_apply PEquiv.coe_mk_apply
 
-@[ext]
-theorem ext : ∀ {f g : α ≃. β} (_ : ∀ x, f x = g x), f = g
-  | ⟨f₁, f₂, hf⟩, ⟨g₁, g₂, hg⟩, h => by
-    have h : f₁ = g₁ := funext h
-    have : ∀ b, f₂ b = g₂ b := by
-      subst h
-      intro b
-      have hf := fun a => hf a b
-      have hg := fun a => hg a b
-      cases' h : g₂ b with a
-      · simp only [h, Option.not_mem_none, false_iff_iff] at hg
-        simp only [hg, iff_false_iff] at hf
-        rwa [Option.eq_none_iff_forall_not_mem]
-      · rw [← Option.mem_def, hf, ← hg, h, Option.mem_def]
-    simp [*, funext_iff]
+@[ext] theorem ext {f g : α ≃. β} (h : ∀ x, f x = g x) : f = g :=
+  FunLike.ext f g h
 #align pequiv.ext PEquiv.ext
 
 theorem ext_iff {f g : α ≃. β} : f = g ↔ ∀ x, f x = g x :=
-  ⟨fun h _ => by rw [h], ext⟩
+  FunLike.ext_iff
 #align pequiv.ext_iff PEquiv.ext_iff
 
 /-- The identity map as a partial equivalence. -/

Mathlib/Order/InitialSeg.lean

@@ -66,8 +66,16 @@ namespace InitialSeg
 instance : Coe (r ≼i s) (r ↪r s) :=
   ⟨InitialSeg.toRelEmbedding⟩
 
-instance : CoeFun (r ≼i s) fun _ => α → β :=
-  ⟨fun f x => (f : r ↪r s) x⟩
+instance : EmbeddingLike (r ≼i s) α β :=
+  { coe := fun f => f.toFun
+    coe_injective' := by
+      rintro ⟨f, hf⟩ ⟨g, hg⟩ h
+      congr with x
+      exact congr_fun h x,
+    injective' := fun f => f.inj' }
+
+@[ext] lemma ext {f g : r ≼i s} (h : ∀ x, f x = g x) : f = g :=
+  FunLike.ext f g h
 
 @[simp]
 theorem coe_coe_fn (f : r ≼i s) : ((f : r ↪r s) : α → β) = f :=
@@ -78,11 +86,14 @@ theorem init' (f : r ≼i s) {a : α} {b : β} : s b (f a) → ∃ a', f a' = b
   f.init _ _
 #align initial_seg.init' InitialSeg.init'
 
+theorem map_rel_iff (f : r ≼i s) : s (f a) (f b) ↔ r a b :=
+  f.map_rel_iff'
+
 theorem init_iff (f : r ≼i s) {a : α} {b : β} : s b (f a) ↔ ∃ a', f a' = b ∧ r a' a :=
-  ⟨fun h =>
-    let ⟨a', e⟩ := f.init' h
-    ⟨a', e, (f : r ↪r s).map_rel_iff.1 (by dsimp only at e; rw [e]; exact h)⟩,
-    fun ⟨a', e, h⟩ => e ▸ (f : r ↪r s).map_rel_iff.2 h⟩
+  ⟨fun h => by
+    rcases f.init' h with ⟨a', rfl⟩
+    exact ⟨a', rfl, f.map_rel_iff.1 h⟩,
+    fun ⟨a', e, h⟩ => e ▸ f.map_rel_iff.2 h⟩
 #align initial_seg.init_iff InitialSeg.init_iff
 
 /-- An order isomorphism is an initial segment -/
@@ -104,7 +115,7 @@ instance (r : α → α → Prop) : Inhabited (r ≼i r) :=
 protected def trans (f : r ≼i s) (g : s ≼i t) : r ≼i t :=
   ⟨f.1.trans g.1, fun a c h => by
     simp at h⊢
-    rcases g.2 _ _ h with ⟨b, rfl⟩; have h := g.1.map_rel_iff.1 h
+    rcases g.2 _ _ h with ⟨b, rfl⟩; have h := g.map_rel_iff.1 h
     rcases f.2 _ _ h with ⟨a', rfl⟩; exact ⟨a', rfl⟩⟩
 #align initial_seg.trans InitialSeg.trans
 
@@ -122,23 +133,11 @@ theorem unique_of_trichotomous_of_irrefl [IsTrichotomous β s] [IsIrrefl β s] :
     WellFounded r → Subsingleton (r ≼i s)
   | ⟨h⟩ =>
     ⟨fun f g => by
-      suffices (f : α → β) = g by
-        cases f
-        cases g
-        congr
-        exact RelEmbedding.coe_fn_injective this
-      funext a
-      have := h a
-      induction' this with a _ IH
-      refine' extensional_of_trichotomous_of_irrefl s fun x => ⟨fun h => _, fun h => _⟩
-      · rcases f.init_iff.1 h with ⟨y, rfl, h'⟩
-        dsimp only
-        rw [IH _ h']
-        exact (g : r ↪r s).map_rel_iff.2 h'
-      · rcases g.init_iff.1 h with ⟨y, rfl, h'⟩
-        dsimp only
-        rw [← IH _ h']
-        exact (f : r ↪r s).map_rel_iff.2 h'⟩
+      ext a
+      induction' h a with a _ IH
+      refine extensional_of_trichotomous_of_irrefl s fun x => ?_
+      simp only [f.init_iff, g.init_iff]
+      exact exists_congr fun y => and_congr_left fun h => IH _ h ▸ Iff.rfl⟩
 #align initial_seg.unique_of_trichotomous_of_irrefl InitialSeg.unique_of_trichotomous_of_irrefl
 
 instance [IsWellOrder β s] : Subsingleton (r ≼i s) :=
@@ -293,7 +292,7 @@ instance (r : α → α → Prop) [IsWellOrder α r] : IsEmpty (r ≺i r) :=
 def ltLe (f : r ≺i s) (g : s ≼i t) : r ≺i t :=
   ⟨@RelEmbedding.trans _ _ _ r s t f g, g f.top, fun a => by
     simp only [g.init_iff, PrincipalSeg.down, exists_and_left.symm, exists_swap,
-        RelEmbedding.trans_apply, exists_eq_right']⟩
+        RelEmbedding.trans_apply, exists_eq_right', InitialSeg.coe_coe_fn]⟩
 #align principal_seg.lt_le PrincipalSeg.ltLe
 
 @[simp]
@@ -353,7 +352,7 @@ theorem equivLT_top (f : r ≃r s) (g : s ≺i t) : (equivLT f g).top = g.top :=
 instance [IsWellOrder β s] : Subsingleton (r ≺i s) :=
   ⟨fun f g => by
     have ef : (f : α → β) = g := by
-      show ((f : r ≼i s) : α → β) = g
+      show ((f : r ≼i s) : α → β) = (g : r ≼i s)
       rw [@Subsingleton.elim _ _ (f : r ≼i s) g]
     have et : f.top = g.top := by
       refine' extensional_of_trichotomous_of_irrefl s fun x => _