diff --git a/Mathlib/Data/FunLike/Basic.lean b/Mathlib/Data/FunLike/Basic.lean
index 02752d9006b1f3..37cb3a798b9160 100644
--- a/Mathlib/Data/FunLike/Basic.lean
+++ b/Mathlib/Data/FunLike/Basic.lean
@@ -21,27 +21,23 @@ A typical type of morphisms should be declared as:
 ```
 structure MyHom (A B : Type*) [MyClass A] [MyClass B] :=
   (toFun : A → B)
-  (map_op' : ∀ {x y : A}, toFun (MyClass.op x y) = MyClass.op (toFun x) (toFun y))
+  (map_op' : ∀ (x y : A), toFun (MyClass.op x y) = MyClass.op (toFun x) (toFun y))
 
 namespace MyHom
 
 variable (A B : Type*) [MyClass A] [MyClass B]
 
--- This instance is optional if you follow the "morphism class" design below:
-instance : FunLike (MyHom A B) A B :=
-  { coe := MyHom.toFun, coe_injective' := fun f g h => by cases f; cases g; congr' }
-
-/-- Helper instance for when there's too many metavariables to apply
-`DFunLike.coe` directly. -/
-instance : CoeFun (MyHom A B) (fun _ => A → B) := ⟨MyHom.toFun⟩
+instance : FunLike (MyHom A B) A B where
+  coe := MyHom.toFun
+  coe_injective' := fun f g h => by cases f; cases g; congr
 
 @[ext] theorem ext {f g : MyHom A B} (h : ∀ x, f x = g x) : f = g := DFunLike.ext f g h
 
 /-- Copy of a `MyHom` with a new `toFun` equal to the old one. Useful to fix definitional
 equalities. -/
-protected def copy (f : MyHom A B) (f' : A → B) (h : f' = ⇑f) : MyHom A B :=
-  { toFun := f',
-    map_op' := h.symm ▸ f.map_op' }
+protected def copy (f : MyHom A B) (f' : A → B) (h : f' = ⇑f) : MyHom A B where
+  toFun := f'
+  map_op' := h.symm ▸ f.map_op'
 
 end MyHom
 ```
@@ -51,8 +47,8 @@ extensionality and simp lemmas.
 
 ## Morphism classes extending `DFunLike` and `FunLike`
 
-The `DFunLike` design provides further benefits if you put in a bit more work.
-The first step is to extend `DFunLike` to create a class of those types satisfying
+The `FunLike` design provides further benefits if you put in a bit more work.
+The first step is to extend `FunLike` to create a class of those types satisfying
 the axioms of your new type of morphisms.
 Continuing the example above:
 
@@ -60,20 +56,20 @@ Continuing the example above:
 /-- `MyHomClass F A B` states that `F` is a type of `MyClass.op`-preserving morphisms.
 You should extend this class when you extend `MyHom`. -/
 class MyHomClass (F : Type*) (A B : outParam Type*) [MyClass A] [MyClass B]
-  [FunLike F A B] : Prop :=
-(map_op : ∀ (f : F) (x y : A), f (MyClass.op x y) = MyClass.op (f x) (f y))
+    [FunLike F A B] : Prop :=
+  (map_op : ∀ (f : F) (x y : A), f (MyClass.op x y) = MyClass.op (f x) (f y))
 
-@[simp] lemma map_op {F A B : Type*} [MyClass A] [MyClass B] [MyHomClass F A B]
-  (f : F) (x y : A) : f (MyClass.op x y) = MyClass.op (f x) (f y) :=
-MyHomClass.map_op
+@[simp]
+lemma map_op {F A B : Type*} [MyClass A] [MyClass B] [FunLike F A B] [MyHomClass F A B]
+    (f : F) (x y : A) :
+    f (MyClass.op x y) = MyClass.op (f x) (f y) :=
+  MyHomClass.map_op _ _ _
 
 -- You can add the below instance next to `MyHomClass.instFunLike`:
-instance : MyHomClass (MyHom A B) A B :=
-  { coe := MyHom.toFun,
-    coe_injective' := λ f g h, by cases f; cases g; congr',
-    map_op := MyHom.map_op' }
+instance : MyHomClass (MyHom A B) A B where
+  map_op := MyHom.map_op'
 
--- [Insert `CoeFun`, `ext` and `copy` here]
+-- [Insert `ext` and `copy` here]
 ```
 
 Note that `A B` are marked as `outParam` even though they are not purely required to be so
@@ -85,28 +81,28 @@ The second step is to add instances of your new `MyHomClass` for all types exten
 Typically, you can just declare a new class analogous to `MyHomClass`:
 
 ```
-structure CoolerHom (A B : Type*) [CoolClass A] [CoolClass B]
-  extends MyHom A B :=
-(map_cool' : toFun CoolClass.cool = CoolClass.cool)
+structure CoolerHom (A B : Type*) [CoolClass A] [CoolClass B] extends MyHom A B :=
+  (map_cool' : toFun CoolClass.cool = CoolClass.cool)
 
 class CoolerHomClass (F : Type*) (A B : outParam Type*) [CoolClass A] [CoolClass B]
-  [FunLike F A B]
-  extends MyHomClass F A B :=
-(map_cool : ∀ (f : F), f CoolClass.cool = CoolClass.cool)
-
-@[simp] lemma map_cool {F A B : Type*} [CoolClass A] [CoolClass B] [FunLike F A (fun _ => B)]
-    [CoolerHomClass F A B] (f : F) :
-    f CoolClass.cool = CoolClass.cool :=
-MyHomClass.map_op
-
--- You can add the below instance next to `MyHom.instFunLike`:
-instance : CoolerHomClass (CoolHom A B) A B :=
-  { coe := CoolHom.toFun,
-    coe_injective' := λ f g h, by cases f; cases g; congr',
-    map_op := CoolHom.map_op',
-    map_cool := CoolHom.map_cool' }
-
--- [Insert `CoeFun`, `ext` and `copy` here]
+  [FunLike F A B] extends MyHomClass F A B :=
+    (map_cool : ∀ (f : F), f CoolClass.cool = CoolClass.cool)
+
+@[simp] lemma map_cool {F A B : Type*} [CoolClass A] [CoolClass B] [FunLike F A B]
+    [CoolerHomClass F A B] (f : F) : f CoolClass.cool = CoolClass.cool :=
+  CoolerHomClass.map_cool _
+
+variable {A B : Type*} [CoolClass A] [CoolClass B]
+
+instance : FunLike (CoolerHom A B) A B where
+  coe f := f.toFun
+  coe_injective' := fun f g h ↦ by cases f; cases g; congr; apply DFunLike.coe_injective; congr
+
+instance : CoolerHomClass (CoolerHom A B) A B where
+  map_op f := f.map_op'
+  map_cool f := f.map_cool'
+
+-- [Insert `ext` and `copy` here]
 ```
 
 Then any declaration taking a specific type of morphisms as parameter can instead take the
diff --git a/Mathlib/Data/FunLike/Embedding.lean b/Mathlib/Data/FunLike/Embedding.lean
index a03121384a9021..2347c05d77a0ae 100644
--- a/Mathlib/Data/FunLike/Embedding.lean
+++ b/Mathlib/Data/FunLike/Embedding.lean
@@ -19,28 +19,27 @@ A typical type of embeddings should be declared as:
 structure MyEmbedding (A B : Type*) [MyClass A] [MyClass B] :=
   (toFun : A → B)
   (injective' : Function.Injective toFun)
-  (map_op' : ∀ {x y : A}, toFun (MyClass.op x y) = MyClass.op (toFun x) (toFun y))
+  (map_op' : ∀ (x y : A), toFun (MyClass.op x y) = MyClass.op (toFun x) (toFun y))
 
 namespace MyEmbedding
 
 variable (A B : Type*) [MyClass A] [MyClass B]
 
--- This instance is optional if you follow the "Embedding class" design below:
-instance : EmbeddingLike (MyEmbedding A B) A B :=
-  { coe := MyEmbedding.toFun,
-    coe_injective' := λ f g h, by cases f; cases g; congr',
-    injective' := MyEmbedding.injective' }
+instance : FunLike (MyEmbedding A B) A B where
+  coe := MyEmbedding.toFun
+  coe_injective' := fun f g h ↦ by cases f; cases g; congr
 
-/-- Helper instance for when there's too many metavariables to `EmbeddingLike.coe` directly. -/
-instance : CoeFun (MyEmbedding A B) (λ _, A → B) := ⟨MyEmbedding.toFun⟩
+-- This instance is optional if you follow the "Embedding class" design below:
+instance : EmbeddingLike (MyEmbedding A B) A B where
+  injective' := MyEmbedding.injective'
 
 @[ext] theorem ext {f g : MyEmbedding A B} (h : ∀ x, f x = g x) : f = g := DFunLike.ext f g h
 
 /-- Copy of a `MyEmbedding` with a new `toFun` equal to the old one. Useful to fix definitional
 equalities. -/
 protected def copy (f : MyEmbedding A B) (f' : A → B) (h : f' = ⇑f) : MyEmbedding A B :=
-  { toFun := f',
-    injective' := h.symm ▸ f.injective',
+  { toFun := f'
+    injective' := h.symm ▸ f.injective'
     map_op' := h.symm ▸ f.map_op' }
 
 end MyEmbedding
@@ -57,28 +56,29 @@ the axioms of your new type of morphisms.
 Continuing the example above:
 
 ```
-section
-
 /-- `MyEmbeddingClass F A B` states that `F` is a type of `MyClass.op`-preserving embeddings.
 You should extend this class when you extend `MyEmbedding`. -/
 class MyEmbeddingClass (F : Type*) (A B : outParam <| Type*) [MyClass A] [MyClass B]
-  extends EmbeddingLike F A B :=
-(map_op : ∀ (f : F) (x y : A), f (MyClass.op x y) = MyClass.op (f x) (f y))
+    [FunLike F A B]
+    extends EmbeddingLike F A B :=
+  (map_op : ∀ (f : F) (x y : A), f (MyClass.op x y) = MyClass.op (f x) (f y))
 
-end
+@[simp]
+lemma map_op {F A B : Type*} [MyClass A] [MyClass B] [FunLike F A B] [MyEmbeddingClass F A B]
+    (f : F) (x y : A) :
+    f (MyClass.op x y) = MyClass.op (f x) (f y) :=
+  MyEmbeddingClass.map_op _ _ _
+
+namespace MyEmbedding
 
-@[simp] lemma map_op {F A B : Type*} [MyClass A] [MyClass B] [MyEmbeddingClass F A B]
-  (f : F) (x y : A) : f (MyClass.op x y) = MyClass.op (f x) (f y) :=
-MyEmbeddingClass.map_op
+variable {A B : Type*} [MyClass A] [MyClass B]
 
 -- You can replace `MyEmbedding.EmbeddingLike` with the below instance:
-instance : MyEmbeddingClass (MyEmbedding A B) A B :=
-  { coe := MyEmbedding.toFun,
-    coe_injective' := λ f g h, by cases f; cases g; congr',
-    injective' := MyEmbedding.injective',
-    map_op := MyEmbedding.map_op' }
+instance : MyEmbeddingClass (MyEmbedding A B) A B where
+  injective' := MyEmbedding.injective'
+  map_op := MyEmbedding.map_op'
 
--- [Insert `CoeFun`, `ext` and `copy` here]
+end MyEmbedding
 ```
 
 The second step is to add instances of your new `MyEmbeddingClass` for all types extending
@@ -86,45 +86,44 @@ The second step is to add instances of your new `MyEmbeddingClass` for all types
 Typically, you can just declare a new class analogous to `MyEmbeddingClass`:
 
 ```
-structure CoolerEmbedding (A B : Type*) [CoolClass A] [CoolClass B]
-  extends MyEmbedding A B :=
-(map_cool' : toFun CoolClass.cool = CoolClass.cool)
-
-section
-set_option old_structure_cmd true
+structure CoolerEmbedding (A B : Type*) [CoolClass A] [CoolClass B] extends MyEmbedding A B :=
+  (map_cool' : toFun CoolClass.cool = CoolClass.cool)
 
 class CoolerEmbeddingClass (F : Type*) (A B : outParam <| Type*) [CoolClass A] [CoolClass B]
-  extends MyEmbeddingClass F A B :=
-(map_cool : ∀ (f : F), f CoolClass.cool = CoolClass.cool)
+    [FunLike F A B]
+    extends MyEmbeddingClass F A B :=
+  (map_cool : ∀ (f : F), f CoolClass.cool = CoolClass.cool)
 
-end
+@[simp]
+lemma map_cool {F A B : Type*} [CoolClass A] [CoolClass B]
+    [FunLike F A B] [CoolerEmbeddingClass F A B] (f : F) :
+    f CoolClass.cool = CoolClass.cool :=
+  CoolerEmbeddingClass.map_cool _
 
-@[simp] lemma map_cool {F A B : Type*} [CoolClass A] [CoolClass B] [CoolerEmbeddingClass F A B]
-  (f : F) : f CoolClass.cool = CoolClass.cool :=
-MyEmbeddingClass.map_op
+variable {A B : Type*} [CoolClass A] [CoolClass B]
 
--- You can also replace `MyEmbedding.EmbeddingLike` with the below instance:
-instance : CoolerEmbeddingClass (CoolerEmbedding A B) A B :=
-  { coe := CoolerEmbedding.toFun,
-    coe_injective' := λ f g h, by cases f; cases g; congr',
-    injective' := MyEmbedding.injective',
-    map_op := CoolerEmbedding.map_op',
-    map_cool := CoolerEmbedding.map_cool' }
+instance : FunLike (CoolerEmbedding A B) A B where
+  coe f := f.toFun
+  coe_injective' f g h := by cases f; cases g; congr; apply DFunLike.coe_injective; congr
 
--- [Insert `CoeFun`, `ext` and `copy` here]
+instance : CoolerEmbeddingClass (CoolerEmbedding A B) A B where
+  injective' f := f.injective'
+  map_op f := f.map_op'
+  map_cool f := f.map_cool'
+
+-- [Insert `ext` and `copy` here]
 ```
 
 Then any declaration taking a specific type of morphisms as parameter can instead take the
 class you just defined:
 ```
 -- Compare with: lemma do_something (f : MyEmbedding A B) : sorry := sorry
-lemma do_something {F : Type*} [MyEmbeddingClass F A B] (f : F) : sorry := sorry
+lemma do_something {F : Type*} [FunLike F A B] [MyEmbeddingClass F A B] (f : F) : sorry := sorry
 ```
 
 This means anything set up for `MyEmbedding`s will automatically work for `CoolerEmbeddingClass`es,
 and defining `CoolerEmbeddingClass` only takes a constant amount of effort,
 instead of linearly increasing the work per `MyEmbedding`-related declaration.
-
 -/
 
 
diff --git a/Mathlib/Data/FunLike/Equiv.lean b/Mathlib/Data/FunLike/Equiv.lean
index d6c425ccd46c71..690a8cfbbd1395 100644
--- a/Mathlib/Data/FunLike/Equiv.lean
+++ b/Mathlib/Data/FunLike/Equiv.lean
@@ -14,37 +14,33 @@ This typeclass is primarily for use by isomorphisms like `MonoidEquiv` and `Line
 
 ## Basic usage of `EquivLike`
 
-A typical type of morphisms should be declared as:
+A typical type of isomorphisms should be declared as:
 ```
-structure MyIso (A B : Type*) [MyClass A] [MyClass B]
-  extends Equiv A B :=
-(map_op' : ∀ {x y : A}, toFun (MyClass.op x y) = MyClass.op (toFun x) (toFun y))
+structure MyIso (A B : Type*) [MyClass A] [MyClass B] extends Equiv A B :=
+  (map_op' : ∀ (x y : A), toFun (MyClass.op x y) = MyClass.op (toFun x) (toFun y))
 
 namespace MyIso
 
 variable (A B : Type*) [MyClass A] [MyClass B]
 
--- This instance is optional if you follow the "Isomorphism class" design below:
-instance : EquivLike (MyIso A B) A (λ _, B) :=
-  { coe := MyIso.toEquiv.toFun,
-    inv := MyIso.toEquiv.invFun,
-    left_inv := MyIso.toEquiv.left_inv,
-    right_inv := MyIso.toEquiv.right_inv,
-    coe_injective' := λ f g h, by cases f; cases g; congr' }
-
-/-- Helper instance for when there's too many metavariables to apply `EquivLike.coe` directly. -/
-instance : CoeFun (MyIso A B) := DFunLike.instCoeFunForAll
+instance instEquivLike : EquivLike (MyIso A B) A B where
+  coe f := f.toFun
+  inv f := f.invFun
+  left_inv f := f.left_inv
+  right_inv f := f.right_inv
+  coe_injective' f g h₁ h₂ := by cases f; cases g; congr; exact EquivLike.coe_injective' _ _ h₁ h₂
 
 @[ext] theorem ext {f g : MyIso A B} (h : ∀ x, f x = g x) : f = g := DFunLike.ext f g h
 
 /-- Copy of a `MyIso` with a new `toFun` equal to the old one. Useful to fix definitional
 equalities. -/
-protected def copy (f : MyIso A B) (f' : A → B) (f_inv : B → A) (h : f' = ⇑f) : MyIso A B :=
-  { toFun := f',
-    invFun := f_inv,
-    left_inv := h.symm ▸ f.left_inv,
-    right_inv := h.symm ▸ f.right_inv,
-    map_op' := h.symm ▸ f.map_op' }
+protected def copy (f : MyIso A B) (f' : A → B) (f_inv : B → A)
+    (h₁ : f' = f) (h₂ : f_inv = f.invFun) : MyIso A B where
+  toFun := f'
+  invFun := f_inv
+  left_inv := h₁.symm ▸ h₂.symm ▸ f.left_inv
+  right_inv := h₁.symm ▸ h₂.symm ▸ f.right_inv
+  map_op' := h₁.symm ▸ f.map_op'
 
 end MyIso
 ```
@@ -60,61 +56,67 @@ the axioms of your new type of isomorphisms.
 Continuing the example above:
 
 ```
-
 /-- `MyIsoClass F A B` states that `F` is a type of `MyClass.op`-preserving morphisms.
 You should extend this class when you extend `MyIso`. -/
 class MyIsoClass (F : Type*) (A B : outParam <| Type*) [MyClass A] [MyClass B]
-  extends EquivLike F A (λ _, B), MyHomClass F A B
+    [EquivLike F A B]
+    extends MyHomClass F A B
+
+namespace MyIso
+
+variable {A B : Type*} [MyClass A] [MyClass B]
 
-end
+-- This goes after `MyIsoClass.instEquivLike`:
+instance : MyIsoClass (MyIso A B) A B where
+  map_op := MyIso.map_op'
 
--- You can replace `MyIso.EquivLike` with the below instance:
-instance : MyIsoClass (MyIso A B) A B :=
-  { coe := MyIso.toFun,
-    inv := MyIso.invFun,
-    left_inv := MyIso.left_inv,
-    right_inv := MyIso.right_inv,
-    coe_injective' := λ f g h, by cases f; cases g; congr',
-    map_op := MyIso.map_op' }
+-- [Insert `ext` and `copy` here]
 
--- [Insert `CoeFun`, `ext` and `copy` here]
+end MyIso
 ```
 
 The second step is to add instances of your new `MyIsoClass` for all types extending `MyIso`.
 Typically, you can just declare a new class analogous to `MyIsoClass`:
 
 ```
-structure CoolerIso (A B : Type*) [CoolClass A] [CoolClass B]
-  extends MyIso A B :=
-(map_cool' : toFun CoolClass.cool = CoolClass.cool)
-
-section
-set_option old_structure_cmd true
+structure CoolerIso (A B : Type*) [CoolClass A] [CoolClass B] extends MyIso A B :=
+  (map_cool' : toFun CoolClass.cool = CoolClass.cool)
 
 class CoolerIsoClass (F : Type*) (A B : outParam <| Type*) [CoolClass A] [CoolClass B]
-  extends MyIsoClass F A B :=
-(map_cool : ∀ (f : F), f CoolClass.cool = CoolClass.cool)
+    [EquivLike F A B]
+    extends MyIsoClass F A B :=
+  (map_cool : ∀ (f : F), f CoolClass.cool = CoolClass.cool)
+
+@[simp] lemma map_cool {F A B : Type*} [CoolClass A] [CoolClass B]
+    [EquivLike F A B] [CoolerIsoClass F A B] (f : F) :
+    f CoolClass.cool = CoolClass.cool :=
+  CoolerIsoClass.map_cool _
+
+namespace CoolerIso
+
+variable {A B : Type*} [CoolClass A] [CoolClass B]
 
-end
+instance : EquivLike (CoolerIso A B) A B where
+  coe f := f.toFun
+  inv f := f.invFun
+  left_inv f := f.left_inv
+  right_inv f := f.right_inv
+  coe_injective' f g h₁ h₂ := by cases f; cases g; congr; exact EquivLike.coe_injective' _ _ h₁ h₂
 
-@[simp] lemma map_cool {F A B : Type*} [CoolClass A] [CoolClass B] [CoolerIsoClass F A B]
-  (f : F) : f CoolClass.cool = CoolClass.cool :=
-CoolerIsoClass.map_cool
+instance : CoolerIsoClass (CoolerIso A B) A B where
+  map_op f := f.map_op'
+  map_cool f := f.map_cool'
 
-instance : CoolerIsoClass (CoolerIso A B) A B :=
-  { coe := CoolerIso.toFun,
-    coe_injective' := λ f g h, by cases f; cases g; congr',
-    map_op := CoolerIso.map_op',
-    map_cool := CoolerIso.map_cool' }
+-- [Insert `ext` and `copy` here]
 
--- [Insert `CoeFun`, `ext` and `copy` here]
+end CoolerIso
 ```
 
 Then any declaration taking a specific type of morphisms as parameter can instead take the
 class you just defined:
 ```
 -- Compare with: lemma do_something (f : MyIso A B) : sorry := sorry
-lemma do_something {F : Type*} [MyIsoClass F A B] (f : F) : sorry := sorry
+lemma do_something {F : Type*} [EquivLike F A B] [MyIsoClass F A B] (f : F) : sorry := sorry
 ```
 
 This means anything set up for `MyIso`s will automatically work for `CoolerIsoClass`es,
diff --git a/Mathlib/Data/SetLike/Basic.lean b/Mathlib/Data/SetLike/Basic.lean
index 72c06be28994ef..1951560630fe54 100644
--- a/Mathlib/Data/SetLike/Basic.lean
+++ b/Mathlib/Data/SetLike/Basic.lean
@@ -48,7 +48,7 @@ instance : SetLike (MySubobject X) X :=
 /-- Copy of a `MySubobject` with a new `carrier` equal to the old one. Useful to fix definitional
 equalities. See Note [range copy pattern]. -/
 protected def copy (p : MySubobject X) (s : Set X) (hs : s = ↑p) : MySubobject X :=
-  { carrier := s,
+  { carrier := s
     op_mem' := hs.symm ▸ p.op_mem' }
 
 @[simp] lemma coe_copy (p : MySubobject X) (s : Set X) (hs : s = ↑p) :