diff --git a/Mathlib/Algebra/BigOperators/Fin.lean b/Mathlib/Algebra/BigOperators/Fin.lean
index 2142f4cfbd240..f88089b7fe83b 100644
--- a/Mathlib/Algebra/BigOperators/Fin.lean
+++ b/Mathlib/Algebra/BigOperators/Fin.lean
@@ -70,7 +70,8 @@ is the product of `f x`, for some `x : Fin (n + 1)` times the remaining product
 `f x`, for some `x : Fin (n + 1)` plus the remaining product"]
 theorem prod_univ_succAbove [CommMonoid β] {n : ℕ} (f : Fin (n + 1) → β) (x : Fin (n + 1)) :
     (∏ i, f i) = f x * ∏ i : Fin n, f (x.succAbove i) := by
-  rw [univ_succAbove, prod_cons, Finset.prod_map]
+  rw [univ_succAbove, prod_cons, Finset.prod_map _ x.succAbove.toEmbedding,
+    RelEmbedding.coe_toEmbedding]
 #align fin.prod_univ_succ_above Fin.prod_univ_succAbove
 #align fin.sum_univ_succ_above Fin.sum_univ_succAbove
 
@@ -172,14 +173,14 @@ theorem sum_const [AddCommMonoid α] (n : ℕ) (x : α) : (∑ _i : Fin n, x) =
 @[to_additive]
 theorem prod_Ioi_zero {M : Type _} [CommMonoid M] {n : ℕ} {v : Fin n.succ → M} :
     (∏ i in Ioi 0, v i) = ∏ j : Fin n, v j.succ := by
-  rw [Ioi_zero_eq_map, Finset.prod_map, val_succEmbedding]
+  rw [Ioi_zero_eq_map, Finset.prod_map, RelEmbedding.coe_toEmbedding, val_succEmbedding]
 #align fin.prod_Ioi_zero Fin.prod_Ioi_zero
 #align fin.sum_Ioi_zero Fin.sum_Ioi_zero
 
 @[to_additive]
 theorem prod_Ioi_succ {M : Type _} [CommMonoid M] {n : ℕ} (i : Fin n) (v : Fin n.succ → M) :
     (∏ j in Ioi i.succ, v j) = ∏ j in Ioi i, v j.succ := by
-  rw [Ioi_succ, Finset.prod_map, val_succEmbedding]
+  rw [Ioi_succ, Finset.prod_map, RelEmbedding.coe_toEmbedding, val_succEmbedding]
 #align fin.prod_Ioi_succ Fin.prod_Ioi_succ
 #align fin.sum_Ioi_succ Fin.sum_Ioi_succ
 
diff --git a/Mathlib/Combinatorics/SimpleGraph/Clique.lean b/Mathlib/Combinatorics/SimpleGraph/Clique.lean
index 1efb158fa64f7..d923ba4b41562 100644
--- a/Mathlib/Combinatorics/SimpleGraph/Clique.lean
+++ b/Mathlib/Combinatorics/SimpleGraph/Clique.lean
@@ -176,9 +176,8 @@ theorem not_cliqueFree_of_top_embedding {n : ℕ} (f : (⊤ : SimpleGraph (Fin n
   simp only [coe_map, Set.mem_image, coe_univ, Set.mem_univ, true_and_iff] at hv hw
   obtain ⟨v', rfl⟩ := hv
   obtain ⟨w', rfl⟩ := hw
-  simp only [f.map_adj_iff, comap_Adj, Function.Embedding.coe_subtype, top_adj, Ne.def,
-    Subtype.mk_eq_mk]
-  exact (Function.Embedding.apply_eq_iff_eq _ _ _).symm.not
+  simp only [coe_sort_coe, RelEmbedding.coe_toEmbedding, comap_Adj, Function.Embedding.coe_subtype,
+    f.map_adj_iff, top_adj, ne_eq, Subtype.mk.injEq, RelEmbedding.inj]
 #align simple_graph.not_clique_free_of_top_embedding SimpleGraph.not_cliqueFree_of_top_embedding
 
 /-- An embedding of a complete graph that witnesses the fact that the graph is not clique-free. -/
diff --git a/Mathlib/Data/Fin/Basic.lean b/Mathlib/Data/Fin/Basic.lean
index e4331675d0170..70767477431a1 100644
--- a/Mathlib/Data/Fin/Basic.lean
+++ b/Mathlib/Data/Fin/Basic.lean
@@ -1256,7 +1256,7 @@ theorem castLT_castSucc {n : ℕ} (a : Fin n) (h : (a : ℕ) < n) : castLT (cast
   cases a; rfl
 #align fin.cast_lt_cast_succ Fin.castLT_castSucc
 
-@[simp]
+--@[simp] Porting note: simp can prove it
 theorem castSucc_lt_castSucc_iff {a b : Fin n}: Fin.castSucc a < Fin.castSucc b ↔ a < b :=
   (@castSucc n).lt_iff_lt
 #align fin.cast_succ_lt_cast_succ_iff Fin.castSucc_lt_castSucc_iff
diff --git a/Mathlib/Data/Fin/Tuple/Basic.lean b/Mathlib/Data/Fin/Tuple/Basic.lean
index b819af5717ead..2e699e6a4353e 100644
--- a/Mathlib/Data/Fin/Tuple/Basic.lean
+++ b/Mathlib/Data/Fin/Tuple/Basic.lean
@@ -671,12 +671,12 @@ theorem insertNth_apply_succAbove (i : Fin (n + 1)) (x : α i) (p : ∀ j, α (i
   simp only [insertNth, succAboveCases, dif_neg (succAbove_ne _ _), succAbove_lt_iff]
   split_ifs with hlt
   · generalize_proofs H₁ H₂; revert H₂
-    generalize hk : castLT ((succAbove i).toEmbedding j) H₁ = k
+    generalize hk : castLT ((succAbove i) j) H₁ = k
     rw [castLT_succAbove hlt] at hk; cases hk
     intro; rfl
   · generalize_proofs H₁ H₂; revert H₂
     generalize hk : pred ((succAbove i).toEmbedding j) H₁ = k
-    rw [pred_succAbove (le_of_not_lt hlt)] at hk; cases hk
+    erw [pred_succAbove (le_of_not_lt hlt)] at hk; cases hk
     intro; rfl
 #align fin.insert_nth_apply_succ_above Fin.insertNth_apply_succAbove
 
diff --git a/Mathlib/Data/Finset/Powerset.lean b/Mathlib/Data/Finset/Powerset.lean
index 59fb7af51cab2..0ea247ae7b7a1 100644
--- a/Mathlib/Data/Finset/Powerset.lean
+++ b/Mathlib/Data/Finset/Powerset.lean
@@ -353,7 +353,10 @@ theorem powersetLen_map {β : Type _} (f : α ↪ β) (n : ℕ) (s : Finset α)
       refine' ⟨_, _, this⟩
       rw [← card_map f, this, h.2]; simp
     . rintro ⟨a, ⟨has, rfl⟩, rfl⟩
-      simp [*]
+      dsimp [RelEmbedding.coe_toEmbedding]
+      --Porting note: Why is `rw` required here and not `simp`?
+      rw [mapEmbedding_apply]
+      simp [has]
 #align finset.powerset_len_map Finset.powersetLen_map
 
 end PowersetLen
diff --git a/Mathlib/Data/Fintype/Fin.lean b/Mathlib/Data/Fintype/Fin.lean
index 6167eac46596a..72bb9b1d0ae57 100644
--- a/Mathlib/Data/Fintype/Fin.lean
+++ b/Mathlib/Data/Fintype/Fin.lean
@@ -39,7 +39,7 @@ theorem Ioi_zero_eq_map : Ioi (0 : Fin n.succ) = univ.map (Fin.succEmbedding _).
     · rintro ⟨⟨⟩⟩
     · intro j _
       use j
-      simp only [val_succEmbedding, and_self]
+      simp only [val_succEmbedding, and_self, RelEmbedding.coe_toEmbedding]
   · rintro ⟨i, _, rfl⟩
     exact succ_pos _
 #align fin.Ioi_zero_eq_map Fin.Ioi_zero_eq_map
diff --git a/Mathlib/Data/Set/Finite.lean b/Mathlib/Data/Set/Finite.lean
index 8578941b3b22d..02a3092243191 100644
--- a/Mathlib/Data/Set/Finite.lean
+++ b/Mathlib/Data/Set/Finite.lean
@@ -982,7 +982,7 @@ theorem exists_finite_iff_finset {p : Set α → Prop} :
 theorem Finite.finite_subsets {α : Type u} {a : Set α} (h : a.Finite) : { b | b ⊆ a }.Finite :=
   ⟨Fintype.ofFinset ((Finset.powerset h.toFinset).map Finset.coeEmb.1) fun s => by
       simpa [← @exists_finite_iff_finset α fun t => t ⊆ a ∧ t = s, Finite.subset_toFinset, ←
-        and_assoc] using h.subset⟩
+        and_assoc, Finset.coeEmb] using h.subset⟩
 #align set.finite.finite_subsets Set.Finite.finite_subsets
 
 /-- Finite product of finite sets is finite -/
diff --git a/Mathlib/GroupTheory/Perm/Fin.lean b/Mathlib/GroupTheory/Perm/Fin.lean
index b221633023580..548cd65374bd7 100644
--- a/Mathlib/GroupTheory/Perm/Fin.lean
+++ b/Mathlib/GroupTheory/Perm/Fin.lean
@@ -173,11 +173,11 @@ theorem cycleRange_of_le {n : ℕ} {i j : Fin n.succ} (h : j ≤ i) :
     cycleRange i j = if j = i then 0 else j + 1 := by
   cases n
   · exact Subsingleton.elim (α := Fin 1) _ _  --Porting note; was `simp`
-  have : j = (Fin.castLE (Nat.succ_le_of_lt i.is_lt)).toEmbedding
+  have : j = (Fin.castLE (Nat.succ_le_of_lt i.is_lt))
     ⟨j, lt_of_le_of_lt h (Nat.lt_succ_self i)⟩ :=
     by simp
   ext
-  rw [this, cycleRange, ofLeftInverse'_eq_ofInjective, ←
+  erw [this, cycleRange, ofLeftInverse'_eq_ofInjective, ←
     Function.Embedding.toEquivRange_eq_ofInjective, ← viaFintypeEmbedding,
     viaFintypeEmbedding_apply_image, coe_castLE, coe_finRotate]
   simp only [Fin.ext_iff, val_last, val_mk, val_zero, Fin.eta, castLE_mk]
diff --git a/Mathlib/Order/Hom/Basic.lean b/Mathlib/Order/Hom/Basic.lean
index fb05e8036816b..00a9834c575ab 100644
--- a/Mathlib/Order/Hom/Basic.lean
+++ b/Mathlib/Order/Hom/Basic.lean
@@ -652,14 +652,12 @@ theorem le_iff_le {a b} : f a ≤ f b ↔ a ≤ b :=
   f.map_rel_iff
 #align order_embedding.le_iff_le OrderEmbedding.le_iff_le
 
--- Porting note: `simp` can prove this.
--- @[simp]
+@[simp]
 theorem lt_iff_lt {a b} : f a < f b ↔ a < b :=
   f.ltEmbedding.map_rel_iff
 #align order_embedding.lt_iff_lt OrderEmbedding.lt_iff_lt
 
--- Porting note: `simp` can prove this.
--- @[simp]
+@[simp]
 theorem eq_iff_eq {a b} : f a = f b ↔ a = b :=
   f.injective.eq_iff
 #align order_embedding.eq_iff_eq OrderEmbedding.eq_iff_eq
@@ -983,7 +981,7 @@ section LE
 
 variable [LE α] [LE β] [LE γ]
 
-@[simp]
+--@[simp] porting note: simp can prove it
 theorem le_iff_le (e : α ≃o β) {x y : α} : e x ≤ e y ↔ x ≤ y :=
   e.map_rel_iff
 #align order_iso.le_iff_le OrderIso.le_iff_le
@@ -1031,7 +1029,7 @@ theorem toRelIsoLT_symm (e : α ≃o β) : e.toRelIsoLT.symm = e.symm.toRelIsoLT
 /-- Converts a `RelIso (<) (<)` into an `OrderIso`. -/
 def ofRelIsoLT {α β} [PartialOrder α] [PartialOrder β]
     (e : ((· < ·) : α → α → Prop) ≃r ((· < ·) : β → β → Prop)) : α ≃o β :=
-  ⟨e.toEquiv, by simp [le_iff_eq_or_lt, e.map_rel_iff]⟩
+  ⟨e.toEquiv, by simp [le_iff_eq_or_lt, e.map_rel_iff, e.injective.eq_iff]⟩
 #align order_iso.of_rel_iso_lt OrderIso.ofRelIsoLT
 
 @[simp]
diff --git a/Mathlib/Order/LiminfLimsup.lean b/Mathlib/Order/LiminfLimsup.lean
index 2a7290903b385..f96121b678918 100644
--- a/Mathlib/Order/LiminfLimsup.lean
+++ b/Mathlib/Order/LiminfLimsup.lean
@@ -952,9 +952,7 @@ theorem OrderIso.apply_blimsup [CompleteLattice γ] (e : α ≃o γ) :
   congr
   ext c
   obtain ⟨a, rfl⟩ := e.surjective c
-  -- Porting note: Also needed to add this next line
-  have : ↑(RelIso.toRelEmbedding e).toEmbedding = FunLike.coe e := rfl
-  simp [this]
+  simp
 #align filter.order_iso.apply_blimsup Filter.OrderIso.apply_blimsup
 
 theorem OrderIso.apply_bliminf [CompleteLattice γ] (e : α ≃o γ) :
diff --git a/Mathlib/Order/RelIso/Basic.lean b/Mathlib/Order/RelIso/Basic.lean
index e12af5f9a283f..15748f8b5baed 100644
--- a/Mathlib/Order/RelIso/Basic.lean
+++ b/Mathlib/Order/RelIso/Basic.lean
@@ -232,13 +232,14 @@ 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⟩
+-- instance : CoeFun (r ↪r s) fun _ => α → β :=
+--   ⟨fun o => o.toEmbedding⟩
 
 -- TODO: define and instantiate a `RelEmbeddingClass` when `EmbeddingLike` is defined
 instance : RelHomClass (r ↪r s) r s where
-  coe := fun x => x
+  coe := fun x => x.toFun
   coe_injective' f g h := by
     rcases f with ⟨⟨⟩⟩
     rcases g with ⟨⟨⟩⟩
@@ -254,6 +255,15 @@ def Simps.apply (h : r ↪r s) : α → β :=
 
 initialize_simps_projections RelEmbedding (toFun → apply)
 
+@[simp]
+theorem coe_toEmbedding : ((f : r ↪r s).toEmbedding : α → β)  = f :=
+  rfl
+#align rel_embedding.coe_fn_to_embedding RelEmbedding.coe_toEmbedding
+
+@[simp]
+theorem coe_toRelHom : ((f : r ↪r s).toRelHom : α → β) = f :=
+  rfl
+
 theorem injective (f : r ↪r s) : Injective f :=
   f.inj'
 #align rel_embedding.injective RelEmbedding.injective
@@ -266,8 +276,10 @@ theorem map_rel_iff (f : r ↪r s) {a b} : s (f a) (f b) ↔ r a b :=
   f.map_rel_iff'
 #align rel_embedding.map_rel_iff RelEmbedding.map_rel_iff
 
-#noalign coe_fn_mk
-#noalign coe_fn_to_embedding
+@[simp]
+theorem coe_mk : ⇑(⟨f, h⟩ : r ↪r s) = f :=
+  rfl
+#align rel_embedding.coe_fn_mk RelEmbedding.coe_mk
 
 /-- The map `coe_fn : (r ↪r s) → (α → β)` is injective. -/
 theorem coe_fn_injective : Injective fun f : r ↪r s => (f : α → β) :=
@@ -595,12 +607,13 @@ def prodLexMkRight (r : α → α → Prop) {b : β} (h : ¬s b b) : r ↪r Prod
 #align rel_embedding.prod_lex_mk_right RelEmbedding.prodLexMkRight
 #align rel_embedding.prod_lex_mk_right_apply RelEmbedding.prodLexMkRight_apply
 
+set_option synthInstance.etaExperiment true
 /-- `Prod.map` as a relation embedding. -/
 @[simps]
 def prodLexMap (f : r ↪r s) (g : t ↪r u) : Prod.Lex r t ↪r Prod.Lex s u where
   toFun := Prod.map f g
   inj' := f.injective.Prod_map g.injective
-  map_rel_iff' := by simp [Prod.lex_def, f.map_rel_iff, g.map_rel_iff]
+  map_rel_iff' := by simp [Prod.lex_def, f.map_rel_iff, g.map_rel_iff, f.inj]
 #align rel_embedding.prod_lex_map RelEmbedding.prodLexMap
 #align rel_embedding.prod_lex_map_apply RelEmbedding.prodLexMap_apply
 
@@ -631,9 +644,9 @@ theorem toEquiv_injective : Injective (toEquiv : r ≃r s → α ≃ β)
 instance : CoeOut (r ≃r s) (r ↪r s) :=
   ⟨toRelEmbedding⟩
 
--- see Note [function coercion]
-instance : CoeFun (r ≃r s) fun _ => α → β :=
-  ⟨fun f => f⟩
+-- Porting note: moved to after `RelHomClass` instance and redefined as `FunLike.coe`
+-- instance : CoeFun (r ≃r s) fun _ => α → β :=
+--   ⟨fun f => f⟩
 
 -- TODO: define and instantiate a `RelIsoClass` when `EquivLike` is defined
 instance : RelHomClass (r ≃r s) r s where
@@ -641,6 +654,23 @@ instance : RelHomClass (r ≃r s) r s where
   coe_injective' := Equiv.coe_fn_injective.comp toEquiv_injective
   map_rel f _ _ := Iff.mpr (map_rel_iff' f)
 
+--Porting note: helper instance
+-- see Note [function coercion]
+instance : CoeFun (r ≃r s) fun _ => α → β :=
+  ⟨FunLike.coe⟩
+
+@[simp]
+theorem coe_toRelEmbedding (f : r ≃r s) : (f.toRelEmbedding : α → β) = f :=
+  rfl
+
+@[simp]
+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
@@ -822,7 +852,8 @@ lexicographic orders on the product.
 -/
 def prodLexCongr {α₁ α₂ β₁ β₂ r₁ r₂ s₁ s₂} (e₁ : @RelIso α₁ β₁ r₁ s₁) (e₂ : @RelIso α₂ β₂ r₂ s₂) :
     Prod.Lex r₁ r₂ ≃r Prod.Lex s₁ s₂ :=
-  ⟨Equiv.prodCongr e₁.toEquiv e₂.toEquiv, by simp [Prod.lex_def, e₁.map_rel_iff, e₂.map_rel_iff]⟩
+  ⟨Equiv.prodCongr e₁.toEquiv e₂.toEquiv, by simp [Prod.lex_def, e₁.map_rel_iff, e₂.map_rel_iff,
+    e₁.injective.eq_iff]⟩
 #align rel_iso.prod_lex_congr RelIso.prodLexCongr
 
 /-- Two relations on empty types are isomorphic. -/
diff --git a/Mathlib/RingTheory/MvPolynomial/Symmetric.lean b/Mathlib/RingTheory/MvPolynomial/Symmetric.lean
index 248ba2ef54981..ebbdc1a5aa750 100644
--- a/Mathlib/RingTheory/MvPolynomial/Symmetric.lean
+++ b/Mathlib/RingTheory/MvPolynomial/Symmetric.lean
@@ -205,6 +205,9 @@ theorem rename_esymm (n : ℕ) (e : σ ≃ τ) : rename e (esymm σ R n) = esymm
       simp_rw [esymm, map_sum, map_prod, rename_X]
     _ = ∑ t in powersetLen n (univ.map e.toEmbedding), ∏ i in t, X i := by
       simp [Finset.powersetLen_map, -Finset.map_univ_equiv]
+      --Porting note: Why did `mapEmbedding_apply` not work?
+      dsimp [mapEmbedding, OrderEmbedding.ofMapLEIff]
+      simp
     _ = ∑ t in powersetLen n univ, ∏ i in t, X i := by rw [Finset.map_univ_equiv]
 
 #align mv_polynomial.rename_esymm MvPolynomial.rename_esymm