diff --git a/Mathlib/Algebra/Polynomial/Div.lean b/Mathlib/Algebra/Polynomial/Div.lean
index 7ee00bdddb3f4f..dd34b114930c06 100644
--- a/Mathlib/Algebra/Polynomial/Div.lean
+++ b/Mathlib/Algebra/Polynomial/Div.lean
@@ -525,7 +525,6 @@ theorem rootMultiplicity_eq_natFind_of_ne_zero {p : R[X]} (p0 : p ≠ 0) {a : R}
 @[deprecated (since := "2026-02-12")]
 alias rootMultiplicity_eq_nat_find_of_nonzero := rootMultiplicity_eq_natFind_of_ne_zero
 
-set_option backward.isDefEq.respectTransparency false in
 theorem rootMultiplicity_eq_multiplicity [DecidableEq R]
     (p : R[X]) (a : R) :
     rootMultiplicity a p =
@@ -535,7 +534,7 @@ theorem rootMultiplicity_eq_multiplicity [DecidableEq R]
   · rfl
   rename_i h
   simp only [finiteMultiplicity_X_sub_C a h, ↓reduceDIte]
-  rw [← ENat.some_eq_coe, WithTop.untopD_coe]
+  rw [untopD_coe_enat]
   congr
 
 @[simp]
diff --git a/Mathlib/Data/ENat/Basic.lean b/Mathlib/Data/ENat/Basic.lean
index ba7945bc7626cd..9e707c4cc57ee8 100644
--- a/Mathlib/Data/ENat/Basic.lean
+++ b/Mathlib/Data/ENat/Basic.lean
@@ -118,6 +118,7 @@ def lift (x : ℕ∞) (h : x < ⊤) : ℕ := WithTop.untop x (WithTop.lt_top_iff
     lift ofNat(n) (WithTop.coe_lt_top n) = OfNat.ofNat n := rfl
 
 @[simp] theorem add_lt_top {a b : ℕ∞} : a + b < ⊤ ↔ a < ⊤ ∧ b < ⊤ := WithTop.add_lt_top
+@[simp] theorem add_eq_top {a b : ℕ∞} : a + b = ⊤ ↔ a = ⊤ ∨ b = ⊤ := WithTop.add_eq_top
 
 @[simp] theorem lift_add (a b : ℕ∞) (h : a + b < ⊤) :
     lift (a + b) h = lift a (add_lt_top.1 h).1 + lift b (add_lt_top.1 h).2 := by
diff --git a/Mathlib/Dynamics/TopologicalEntropy/NetEntropy.lean b/Mathlib/Dynamics/TopologicalEntropy/NetEntropy.lean
index 1f341c7e4489b8..fd3269e6bc03fa 100644
--- a/Mathlib/Dynamics/TopologicalEntropy/NetEntropy.lean
+++ b/Mathlib/Dynamics/TopologicalEntropy/NetEntropy.lean
@@ -188,7 +188,6 @@ lemma netMaxcard_univ (T : X → X) (h : F.Nonempty) (n : ℕ) : netMaxcard T F
   refine Finset.card_le_one.2 fun x x_s y y_s ↦ ?_
   exact PairwiseDisjoint.elim_set s_net x_s y_s x (mem_univ x) (mem_univ x)
 
-set_option backward.isDefEq.respectTransparency false in
 lemma netMaxcard_infinite_iff (T : X → X) (F : Set X) (U : SetRel X X) (n : ℕ) :
     netMaxcard T F U n = ⊤ ↔ ∀ k : ℕ, ∃ s : Finset X, IsDynNetIn T F U n s ∧ k ≤ s.card := by
   apply Iff.intro <;> intro h
@@ -198,11 +197,11 @@ lemma netMaxcard_infinite_iff (T : X → X) (F : Set X) (U : SetRel X X) (n : 
     simp only [Nat.cast_lt, Subtype.exists, exists_prop] at h
     obtain ⟨s, s_net, s_k⟩ := h
     exact ⟨s, s_net, s_k.le⟩
-  · refine WithTop.eq_top_iff_forall_gt.2 fun k ↦ ?_
+  · refine ENat.eq_top_iff_forall_gt.mpr fun k ↦ ?_
     specialize h (k + 1)
     obtain ⟨s, s_net, s_card⟩ := h
     apply s_net.card_le_netMaxcard.trans_lt'
-    rw [ENat.some_eq_coe, Nat.cast_lt]
+    rw [ENat.coe_lt_coe]
     exact (lt_add_one k).trans_le s_card
 
 lemma netMaxcard_le_coverMincard (T : X → X) (F : Set X) (n : ℕ) :
diff --git a/Mathlib/RingTheory/DiscreteValuationRing/Basic.lean b/Mathlib/RingTheory/DiscreteValuationRing/Basic.lean
index f4b52ff1919234..cf440202db633a 100644
--- a/Mathlib/RingTheory/DiscreteValuationRing/Basic.lean
+++ b/Mathlib/RingTheory/DiscreteValuationRing/Basic.lean
@@ -558,14 +558,13 @@ theorem length_quotient_pow_maximalIdeal (n : ℕ) :
 
 end
 
-set_option backward.isDefEq.respectTransparency false in
 instance (R : Type*) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] :
     IsHausdorff (maximalIdeal R) R where
   haus' x hx := by
     obtain ⟨ϖ, hϖ⟩ := exists_irreducible R
     simp only [← Ideal.one_eq_top, smul_eq_mul, mul_one, SModEq.zero, hϖ.maximalIdeal_eq,
       Ideal.span_singleton_pow, Ideal.mem_span_singleton, ← addVal_le_iff_dvd, hϖ.addVal_pow] at hx
-    rwa [← addVal_eq_top_iff, WithTop.eq_top_iff_forall_ge]
+    rwa [← addVal_eq_top_iff, ENat.eq_top_iff_forall_ge]
 
 noncomputable section toEuclideanDomain
 variable {R : Type*} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R]
diff --git a/Mathlib/RingTheory/Multiplicity.lean b/Mathlib/RingTheory/Multiplicity.lean
index 3ae9ebb2cb3780..a601027c1f34ef 100644
--- a/Mathlib/RingTheory/Multiplicity.lean
+++ b/Mathlib/RingTheory/Multiplicity.lean
@@ -689,7 +689,6 @@ theorem multiplicity_mul {p a b : α} (hp : Prime p) (hfin : FiniteMultiplicity
   rw [hfin.multiplicity_eq_iff]
   exact ⟨hdiv, hsucc⟩
 
-set_option backward.isDefEq.respectTransparency false in
 theorem emultiplicity_mul {p a b : α} (hp : Prime p) :
     emultiplicity p (a * b) = emultiplicity p a + emultiplicity p b := by
   by_cases hfin : FiniteMultiplicity p (a * b)
@@ -697,7 +696,7 @@ theorem emultiplicity_mul {p a b : α} (hp : Prime p) :
       hfin.mul_right.emultiplicity_eq_multiplicity]
     norm_cast
     exact multiplicity_mul hp hfin
-  · rw [emultiplicity_eq_top.2 hfin, eq_comm, WithTop.add_eq_top, emultiplicity_eq_top,
+  · rw [emultiplicity_eq_top.mpr hfin, eq_comm, ENat.add_eq_top, emultiplicity_eq_top,
       emultiplicity_eq_top]
     simpa only [FiniteMultiplicity.mul_iff hp, not_and_or] using hfin
 
diff --git a/Mathlib/RingTheory/OrderOfVanishing/Basic.lean b/Mathlib/RingTheory/OrderOfVanishing/Basic.lean
index bf20bae55d0e2e..fb8aabcebe768f 100644
--- a/Mathlib/RingTheory/OrderOfVanishing/Basic.lean
+++ b/Mathlib/RingTheory/OrderOfVanishing/Basic.lean
@@ -284,7 +284,6 @@ If `x` is not a non zero divisor, `ordMonoidWithZeroHom` is equal to `0`.
 theorem ordMonoidWithZeroHom_eq_zero [Nontrivial R] {x : R} (h : x ∉ nonZeroDivisors R) :
     ordMonoidWithZeroHom R x = 0 := dif_neg h
 
-set_option backward.isDefEq.respectTransparency false in
 /--
 The quotient of a Noetherian ring of krull dimension less than or equal to `1` by a principal ideal
 is of finite length.
@@ -297,8 +296,7 @@ theorem _root_.isFiniteLength_quotient_span_singleton [IsNoetherianRing R]
     ⟨isNoetherian_quotient (Ideal.span {x}),
       isArtinian_of_surjective_algebraMap (Ideal.Quotient.mk_surjective (I := .span {x}))⟩
   rw [isArtinianRing_iff_krullDimLE_zero, Ring.KrullDimLE, Order.krullDimLE_iff,
-    ← WithBot.add_le_add_iff_right' (c := 1) (by simp) (WithBot.coe_eq_coe.not.mpr (by simp)),
-    Nat.cast_zero, zero_add]
+    ← ENat.WithBot.add_le_add_one_right_iff, Nat.cast_zero, zero_add]
   exact (ringKrullDim_quotient_succ_le_of_nonZeroDivisor hx).trans (Order.KrullDimLE.krullDim_le)
 
 variable [IsNoetherianRing R] [Ring.KrullDimLE 1 R]
diff --git a/Mathlib/Topology/Instances/ENat.lean b/Mathlib/Topology/Instances/ENat.lean
index 7a04848b12d4fd..e60bfbe1582e96 100644
--- a/Mathlib/Topology/Instances/ENat.lean
+++ b/Mathlib/Topology/Instances/ENat.lean
@@ -69,11 +69,11 @@ theorem tendsto_natCast_nhds_top : Tendsto Nat.cast atTop (𝓝 (⊤ : ℕ∞))
   filter_upwards [eventually_ge_atTop (n + 1)] with a ha using by simpa
 
 instance : ContinuousAdd ℕ∞ := by
-  refine ⟨continuous_iff_continuousAt.2 fun (a, b) ↦ ?_⟩
+  refine ⟨continuous_iff_continuousAt.mpr fun (a, b) ↦ ?_⟩
   match a, b with
   | ⊤, _ => exact tendsto_nhds_top_mono' continuousAt_fst fun p ↦ le_add_right le_rfl
   | (a : ℕ), ⊤ => exact tendsto_nhds_top_mono' continuousAt_snd fun p ↦ le_add_left le_rfl
-  | (a : ℕ), (b : ℕ) => simp [ContinuousAt, nhds_prod_eq, tendsto_pure_nhds]
+  | (a : ℕ), (b : ℕ) => simp [ContinuousAt, nhds_prod_eq]
 
 instance : ContinuousMul ℕ∞ where
   continuous_mul :=