diff --git a/src/Init/Data/Iterators/Lemmas/Combinators/FilterMap.lean b/src/Init/Data/Iterators/Lemmas/Combinators/FilterMap.lean
index d90a4013d7..94cbac585b 100644
--- a/src/Init/Data/Iterators/Lemmas/Combinators/FilterMap.lean
+++ b/src/Init/Data/Iterators/Lemmas/Combinators/FilterMap.lean
@@ -435,8 +435,9 @@ theorem Iter.forIn_filterMapWithPostcondition
         match ← (f out).run with
         | some c => g c acc
         | none => return .yield acc) := by
-  simp +instances [Iter.forIn_eq_forIn_toIterM, filterMapWithPostcondition, IterM.forIn_filterMapWithPostcondition,
-    instMonadLiftTOfMonadLift_instMonadLiftTOfPure]; rfl
+  simp only [filterMapWithPostcondition, IterM.forIn_filterMapWithPostcondition, forIn_eq_forIn_toIterM]
+  rw [instMonadLiftTOfMonadLift_instMonadLiftTOfPure]
+  rfl -- expressions are equal up to different matchers
 
 theorem Iter.forIn_filterMapM
     [Monad n] [LawfulMonad n] [Monad o] [LawfulMonad o]
@@ -448,8 +449,9 @@ theorem Iter.forIn_filterMapM
         match ← f out with
         | some c => g c acc
         | none => return .yield acc) := by
-  simp +instances [filterMapM, forIn_eq_forIn_toIterM, IterM.forIn_filterMapM,
-    instMonadLiftTOfMonadLift_instMonadLiftTOfPure]; rfl
+  simp [filterMapM, forIn_eq_forIn_toIterM, IterM.forIn_filterMapM]
+  rw [instMonadLiftTOfMonadLift_instMonadLiftTOfPure]
+  rfl
 
 theorem Iter.forIn_filterMap
     [Monad n] [LawfulMonad n] [Finite α Id]
@@ -469,8 +471,8 @@ theorem Iter.forIn_mapWithPostcondition
     {g : β₂ → γ → o (ForInStep γ)} :
     forIn (it.mapWithPostcondition f) init g =
       forIn it init (fun out acc => do g (← (f out).run) acc) := by
-  simp +instances [mapWithPostcondition, forIn_eq_forIn_toIterM, IterM.forIn_mapWithPostcondition,
-    instMonadLiftTOfMonadLift_instMonadLiftTOfPure]
+  simp only [mapWithPostcondition, forIn_eq_forIn_toIterM, IterM.forIn_mapWithPostcondition]
+  rw [instMonadLiftTOfMonadLift_instMonadLiftTOfPure]
 
 theorem Iter.forIn_mapM
     [Monad n] [LawfulMonad n] [Monad o] [LawfulMonad o]
@@ -498,8 +500,8 @@ theorem Iter.forIn_filterWithPostcondition
     haveI : MonadLift n o := ⟨monadLift⟩
     forIn (it.filterWithPostcondition f) init g =
       forIn it init (fun out acc => do if (← (f out).run).down then g out acc else return .yield acc) := by
-  simp +instances [filterWithPostcondition, forIn_eq_forIn_toIterM, IterM.forIn_filterWithPostcondition,
-    instMonadLiftTOfMonadLift_instMonadLiftTOfPure]
+  simp only [filterWithPostcondition, forIn_eq_forIn_toIterM, IterM.forIn_filterWithPostcondition]
+  rw [instMonadLiftTOfMonadLift_instMonadLiftTOfPure]
 
 theorem Iter.forIn_filterM
     [Monad n] [LawfulMonad n] [Monad o] [LawfulMonad o]
@@ -508,8 +510,8 @@ theorem Iter.forIn_filterM
     [IteratorLoop α Id o] [LawfulIteratorLoop α Id o]
     {it : Iter (α := α) β} {f : β → n (ULift Bool)} {init : γ} {g : β → γ → o (ForInStep γ)} :
     forIn (it.filterM f) init g = forIn it init (fun out acc => do if (← f out).down then g out acc else return .yield acc) := by
-  simp +instances [filterM, forIn_eq_forIn_toIterM, IterM.forIn_filterM,
-    instMonadLiftTOfMonadLift_instMonadLiftTOfPure]
+  simp only [filterM, forIn_eq_forIn_toIterM, IterM.forIn_filterM]
+  rw [instMonadLiftTOfMonadLift_instMonadLiftTOfPure]
 
 theorem Iter.forIn_filter
     [Monad n] [LawfulMonad n]
@@ -550,8 +552,9 @@ theorem Iter.foldM_filterMapM {α β γ δ : Type w}
       it.foldM (init := init) (fun d b => do
           let some c ← f b | pure d
           g d c) := by
-  simp +instances [filterMapM, IterM.foldM_filterMapM, foldM_eq_foldM_toIterM,
-    instMonadLiftTOfMonadLift_instMonadLiftTOfPure]; rfl
+  simp only [filterMapM, IterM.foldM_filterMapM, foldM_eq_foldM_toIterM]
+  rw [instMonadLiftTOfMonadLift_instMonadLiftTOfPure]
+  rfl
 
 theorem Iter.foldM_mapWithPostcondition {α β γ δ : Type w}
     {n : Type w → Type w''} {o : Type w → Type w'''}
@@ -563,8 +566,8 @@ theorem Iter.foldM_mapWithPostcondition {α β γ δ : Type w}
     {f : β → PostconditionT n γ} {g : δ → γ → o δ} {init : δ} {it : Iter (α := α) β} :
     (it.mapWithPostcondition f).foldM (init := init) g =
       it.foldM (init := init) (fun d b => do let c ← (f b).run; g d c) := by
-  simp +instances [mapWithPostcondition, IterM.foldM_mapWithPostcondition, foldM_eq_foldM_toIterM,
-    instMonadLiftTOfMonadLift_instMonadLiftTOfPure]
+  simp only [mapWithPostcondition, IterM.foldM_mapWithPostcondition, foldM_eq_foldM_toIterM]
+  rw [instMonadLiftTOfMonadLift_instMonadLiftTOfPure]
 
 theorem Iter.foldM_mapM {α β γ δ : Type w}
     {n : Type w → Type w''} {o : Type w → Type w'''}
@@ -578,8 +581,8 @@ theorem Iter.foldM_mapM {α β γ δ : Type w}
     haveI : MonadLift n o := ⟨MonadLiftT.monadLift⟩
     (it.mapM f).foldM (init := init) g =
       it.foldM (init := init) (fun d b => do let c ← f b; g d c) := by
-  simp +instances [mapM, IterM.foldM_mapM, foldM_eq_foldM_toIterM,
-    instMonadLiftTOfMonadLift_instMonadLiftTOfPure]
+  simp only [mapM, IterM.foldM_mapM, foldM_eq_foldM_toIterM]
+  rw [instMonadLiftTOfMonadLift_instMonadLiftTOfPure]
 
 theorem Iter.foldM_filterWithPostcondition {α β δ : Type w}
     {n : Type w → Type w''} {o : Type w → Type w'''}
@@ -591,8 +594,8 @@ theorem Iter.foldM_filterWithPostcondition {α β δ : Type w}
     {f : β → PostconditionT n (ULift Bool)} {g : δ → β → o δ} {init : δ} {it : Iter (α := α) β} :
     (it.filterWithPostcondition f).foldM (init := init) g =
       it.foldM (init := init) (fun d b => do if (← (f b).run).down then g d b else pure d) := by
-  simp +instances [filterWithPostcondition, IterM.foldM_filterWithPostcondition, foldM_eq_foldM_toIterM,
-    instMonadLiftTOfMonadLift_instMonadLiftTOfPure]
+  simp only [filterWithPostcondition, IterM.foldM_filterWithPostcondition, foldM_eq_foldM_toIterM]
+  rw [instMonadLiftTOfMonadLift_instMonadLiftTOfPure]
 
 theorem Iter.foldM_filterM {α β δ : Type w}
     {n : Type w → Type w''} {o : Type w → Type w'''}
@@ -605,8 +608,8 @@ theorem Iter.foldM_filterM {α β δ : Type w}
     {f : β → n (ULift Bool)} {g : δ → β → o δ} {init : δ} {it : Iter (α := α) β} :
     (it.filterM f).foldM (init := init) g =
       it.foldM (init := init) (fun d b => do if (← f b).down then g d b else pure d) := by
-  simp +instances [filterM, IterM.foldM_filterM, foldM_eq_foldM_toIterM,
-    instMonadLiftTOfMonadLift_instMonadLiftTOfPure]
+  simp only [filterM, IterM.foldM_filterM, foldM_eq_foldM_toIterM]
+  rw [instMonadLiftTOfMonadLift_instMonadLiftTOfPure]
 
 theorem Iter.foldM_filterMap {α β γ δ : Type w} {n : Type w → Type w''}
     [Iterator α Id β] [Finite α Id] [Monad n] [LawfulMonad n]
diff --git a/src/Init/Data/Iterators/Lemmas/Combinators/FlatMap.lean b/src/Init/Data/Iterators/Lemmas/Combinators/FlatMap.lean
index 12eacb71ab..50a6ab460e 100644
--- a/src/Init/Data/Iterators/Lemmas/Combinators/FlatMap.lean
+++ b/src/Init/Data/Iterators/Lemmas/Combinators/FlatMap.lean
@@ -232,7 +232,6 @@ public theorem Iter.toArray_flatMapM {α α₂ β γ : Type w} {m : Type w → T
     (it₁.flatMapM f).toArray = Array.flatten <$> (it₁.mapM fun b => do (← f b).toArray).toArray := by
   simp [flatMapM, toArray_flatMapAfterM]
 
-set_option backward.isDefEq.respectTransparency false in
 public theorem Iter.toList_flatMapAfter {α α₂ β γ : Type w} [Iterator α Id β] [Iterator α₂ Id γ]
     [Finite α Id] [Finite α₂ Id]
     {f : β → Iter (α := α₂) γ} {it₁ : Iter (α := α) β} {it₂ : Option (Iter (α := α₂) γ)} :
@@ -241,9 +240,9 @@ public theorem Iter.toList_flatMapAfter {α α₂ β γ : Type w} [Iterator α I
       | some it₂ => it₂.toList ++
           (it₁.map fun b => (f b).toList).toList.flatten := by
   simp only [flatMapAfter, Iter.toList, toIterM_toIter, IterM.toList_flatMapAfter]
-  cases it₂ <;> simp [map, IterM.toList_map_eq_toList_mapM, - IterM.toList_map]
+  unfold Iter.toList
+  cases it₂ <;> simp [map]
 
-set_option backward.isDefEq.respectTransparency false in
 public theorem Iter.toArray_flatMapAfter {α α₂ β γ : Type w} [Iterator α Id β] [Iterator α₂ Id γ]
     [Finite α Id] [Finite α₂ Id]
     {f : β → Iter (α := α₂) γ} {it₁ : Iter (α := α) β} {it₂ : Option (Iter (α := α₂) γ)} :
@@ -252,6 +251,7 @@ public theorem Iter.toArray_flatMapAfter {α α₂ β γ : Type w} [Iterator α
       | some it₂ => it₂.toArray ++
           (it₁.map fun b => (f b).toArray).toArray.flatten := by
   simp only [flatMapAfter, Iter.toArray, toIterM_toIter, IterM.toArray_flatMapAfter]
+  unfold Iter.toArray
   cases it₂ <;> simp [map, IterM.toArray_map_eq_toArray_mapM, - IterM.toArray_map]
 
 public theorem Iter.toList_flatMap {α α₂ β γ : Type w} [Iterator α Id β] [Iterator α₂ Id γ]
diff --git a/src/Init/Data/Iterators/Lemmas/Combinators/Monadic/FilterMap.lean b/src/Init/Data/Iterators/Lemmas/Combinators/Monadic/FilterMap.lean
index ddbcc49eaf..1d7e3b8622 100644
--- a/src/Init/Data/Iterators/Lemmas/Combinators/Monadic/FilterMap.lean
+++ b/src/Init/Data/Iterators/Lemmas/Combinators/Monadic/FilterMap.lean
@@ -374,7 +374,6 @@ theorem IterM.toList_map_eq_toList_filterMapM {α β γ : Type w} {m : Type w 
   simp [toList_map_eq_toList_mapM, toList_mapM_eq_toList_filterMapM]
   congr <;> simp
 
-set_option backward.whnf.reducibleClassField false in
 /--
 Variant of `toList_filterMapWithPostcondition_filterMapWithPostcondition` that is intended to be
 used with the `apply` tactic. Because neither the LHS nor the RHS determine all implicit parameters,
@@ -395,7 +394,7 @@ private theorem IterM.toList_filterMapWithPostcondition_filterMapWithPostconditi
       (it.filterMapWithPostcondition (n := o) fg).toList := by
   induction it using IterM.inductSteps with | step it ihy ihs
   letI : MonadLift n o := ⟨monadLift⟩
-  haveI : LawfulMonadLift n o := ⟨by simp +instances [this], by simp +instances [this]⟩
+  haveI : LawfulMonadLift n o := ⟨LawfulMonadLiftT.monadLift_pure, LawfulMonadLiftT.monadLift_bind⟩
   rw [toList_eq_match_step, toList_eq_match_step, step_filterMapWithPostcondition,
     bind_assoc, step_filterMapWithPostcondition, step_filterMapWithPostcondition]
   simp only [bind_assoc, liftM_bind]
@@ -602,7 +601,6 @@ theorem IterM.toList_map_mapM {α β γ δ : Type w}
     toList_filterMapM_mapM]
   congr <;> simp
 
-set_option backward.isDefEq.respectTransparency false in
 @[simp]
 theorem IterM.toList_filterMapWithPostcondition {α β γ : Type w} {m : Type w → Type w'}
     [Monad m] [LawfulMonad m]
@@ -626,7 +624,6 @@ theorem IterM.toList_filterMapWithPostcondition {α β γ : Type w} {m : Type w
   · simp [ihs ‹_›, heq]
   · simp [heq]
 
-set_option backward.isDefEq.respectTransparency false in
 @[simp]
 theorem IterM.toList_mapWithPostcondition {α β γ : Type w} {m : Type w → Type w'}
     [Monad m] [LawfulMonad m] [Iterator α Id β] [Finite α Id]
@@ -647,25 +644,25 @@ theorem IterM.toList_mapWithPostcondition {α β γ : Type w} {m : Type w → Ty
   · simp [ihs ‹_›, heq]
   · simp [heq]
 
-set_option backward.isDefEq.respectTransparency false in
 @[simp]
 theorem IterM.toList_filterMapM {α β γ : Type w} {m : Type w → Type w'}
     [Monad m] [MonadAttach m] [LawfulMonad m] [WeaklyLawfulMonadAttach m]
     [Iterator α Id β] [Finite α Id]
     {f : β → m (Option γ)} (it : IterM (α := α) Id β) :
     (it.filterMapM f).toList = it.toList.run.filterMapM f := by
-  simp [toList_filterMapM_eq_toList_filterMapWithPostcondition, toList_filterMapWithPostcondition,
-    PostconditionT.attachLift, PostconditionT.run_eq_map, WeaklyLawfulMonadAttach.map_attach]
+  simp only [toList_filterMapM_eq_toList_filterMapWithPostcondition,
+    toList_filterMapWithPostcondition, PostconditionT.run_eq_map]
+  simp [PostconditionT.attachLift, WeaklyLawfulMonadAttach.map_attach]
 
-set_option backward.isDefEq.respectTransparency false in
 @[simp]
 theorem IterM.toList_mapM {α β γ : Type w} {m : Type w → Type w'}
     [Monad m] [MonadAttach m] [LawfulMonad m] [WeaklyLawfulMonadAttach m]
     [Iterator α Id β] [Finite α Id]
     {f : β → m γ} (it : IterM (α := α) Id β) :
     (it.mapM f).toList = it.toList.run.mapM f := by
-  simp [toList_mapM_eq_toList_mapWithPostcondition, toList_mapWithPostcondition,
-    PostconditionT.attachLift, PostconditionT.run_eq_map, WeaklyLawfulMonadAttach.map_attach]
+  simp only [toList_mapM_eq_toList_mapWithPostcondition, toList_mapWithPostcondition,
+    PostconditionT.run_eq_map]
+  simp [PostconditionT.attachLift, WeaklyLawfulMonadAttach.map_attach]
 
 @[simp]
 theorem IterM.toList_filterMap {α β γ : Type w} {m : Type w → Type w'}
@@ -1303,7 +1300,6 @@ theorem IterM.forIn_filterMap
   rw [filterMap, forIn_filterMapWithPostcondition]
   simp [PostconditionT.run_eq_map]
 
-set_option backward.isDefEq.respectTransparency false in
 theorem IterM.forIn_mapWithPostcondition
     [Monad m] [LawfulMonad m] [Monad n] [LawfulMonad n] [Monad o] [LawfulMonad o]
     [MonadLiftT m n] [LawfulMonadLiftT m n] [MonadLiftT n o] [LawfulMonadLiftT n o]
@@ -1314,9 +1310,9 @@ theorem IterM.forIn_mapWithPostcondition
     haveI : MonadLift n o := ⟨monadLift⟩
     forIn (it.mapWithPostcondition f) init g =
       forIn it init (fun out acc => do g (← (f out).run) acc) := by
-  rw [mapWithPostcondition, InternalCombinators.map, ← InternalCombinators.filterMap,
-    ← filterMapWithPostcondition, forIn_filterMapWithPostcondition]
-  simp [PostconditionT.run_eq_map]
+  unfold mapWithPostcondition InternalCombinators.map Map.instIterator Map.instIteratorLoop Map
+  rw [← InternalCombinators.filterMap, ← filterMapWithPostcondition, forIn_filterMapWithPostcondition]
+  simp
 
 theorem IterM.forIn_mapM
     [Monad m] [LawfulMonad m] [Monad n] [LawfulMonad n] [Monad o] [LawfulMonad o]
@@ -1480,7 +1476,7 @@ theorem IterM.foldM_filterM {α β δ : Type w}
   simp [filterM, foldM_filterMapWithPostcondition, PostconditionT.run_attachLift]
   congr 1; ext out acc
   apply bind_congr; intro fx
-  cases fx.down <;> simp [PostconditionT.run_eq_map]
+  cases fx.down <;> simp
 
 theorem IterM.foldM_filterMap {α β γ δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''}
     [Iterator α m β] [Finite α m] [Monad m] [Monad n] [LawfulMonad m] [LawfulMonad n]
diff --git a/src/Init/Data/Iterators/Lemmas/Consumers/Loop.lean b/src/Init/Data/Iterators/Lemmas/Consumers/Loop.lean
index f776f4d5e3..fa9e077bff 100644
--- a/src/Init/Data/Iterators/Lemmas/Consumers/Loop.lean
+++ b/src/Init/Data/Iterators/Lemmas/Consumers/Loop.lean
@@ -32,11 +32,12 @@ theorem Iter.forIn'_eq {α β : Type w} [Iterator α Id β] [Finite α Id]
       IterM.DefaultConsumers.forIn' (n := m) (fun _ _ f x => f x.run) γ (fun _ _ _ => True)
         it.toIterM init _ (fun _ => id)
           (fun out h acc => return ⟨← f out (Iter.isPlausibleIndirectOutput_iff_isPlausibleIndirectOutput_toIterM.mpr h) acc, trivial⟩) := by
-  simp +instances only [ForIn'.forIn']
+  simp only [ForIn'.forIn']
   have : ∀ a b c, f a b c = (Subtype.val <$> (⟨·, trivial⟩) <$> f a b c) := by simp
   simp +singlePass only [this]
   rw [hl.lawful (fun _ _ f x => f x.run) (wf := IteratorLoop.wellFounded_of_finite)]
-  simp +instances [IteratorLoop.defaultImplementation]
+  simp only [IteratorLoop.forIn, Functor.map_map, id_map',
+    bind_pure_comp]
 
 theorem Iter.forIn_eq {α β : Type w} [Iterator α Id β] [Finite α Id]
     {m : Type x → Type x'} [Monad m] [LawfulMonad m] [IteratorLoop α Id m]
@@ -81,7 +82,7 @@ theorem Iter.forIn'_eq_forIn'_toIterM {α β : Type w} [Iterator α Id β]
       letI : ForIn' m (IterM (α := α) Id β) β _ := IterM.instForIn'
       ForIn'.forIn' it.toIterM init
         (fun out h acc => f out (isPlausibleIndirectOutput_iff_isPlausibleIndirectOutput_toIterM.mpr h) acc) := by
-  simp +instances [ForIn'.forIn', monadLift]
+  simp [ForIn'.forIn', monadLift]
 
 theorem Iter.forIn_eq_forIn_toIterM {α β : Type w} [Iterator α Id β]
     [Finite α Id] {m : Type w → Type w''} [Monad m] [LawfulMonad m]
diff --git a/src/Init/Data/Iterators/Lemmas/Consumers/Monadic/Loop.lean b/src/Init/Data/Iterators/Lemmas/Consumers/Monadic/Loop.lean
index e23e717779..3347d72420 100644
--- a/src/Init/Data/Iterators/Lemmas/Consumers/Monadic/Loop.lean
+++ b/src/Init/Data/Iterators/Lemmas/Consumers/Monadic/Loop.lean
@@ -109,10 +109,10 @@ theorem IterM.forIn'_eq {α β : Type w} {m : Type w → Type w'} [Iterator α m
     letI : ForIn' n (IterM (α := α) m β) β _ := IterM.instForIn'
     ForIn'.forIn' (α := β) (m := n) it init f = IterM.DefaultConsumers.forIn' (n := n)
         (fun _ _ f x => monadLift x >>= f) γ (fun _ _ _ => True) it init _ (fun _ => id) (return ⟨← f · · ·, trivial⟩) := by
-  simp +instances only [ForIn'.forIn']
+  simp only [ForIn'.forIn']
   have : f = (Subtype.val <$> (⟨·, trivial⟩) <$> f · · ·) := by simp
   rw [this, hl.lawful (fun _ _ f x => monadLift x >>= f) (wf := IteratorLoop.wellFounded_of_finite)]
-  simp +instances [IteratorLoop.defaultImplementation]
+  simp [IteratorLoop.forIn]
   try rfl
 
 theorem IterM.forIn_eq {α β : Type w} {m : Type w → Type w'} [Iterator α m β] [Finite α m]
diff --git a/src/Init/Data/Iterators/PostconditionMonad.lean b/src/Init/Data/Iterators/PostconditionMonad.lean
index 3adc32dd52..93361a83e8 100644
--- a/src/Init/Data/Iterators/PostconditionMonad.lean
+++ b/src/Init/Data/Iterators/PostconditionMonad.lean
@@ -272,6 +272,12 @@ theorem PostconditionT.run_bind' {m : Type w → Type w'} [Monad m] [LawfulMonad
     (x >>= f).run = x.run >>= (f · |>.run) :=
   run_bind
 
+@[simp]
+protected theorem PostconditionT.run_pure {m : Type w → Type w'} [Monad m] [LawfulMonad m]
+    {α : Type w} {x : α} :
+    (pure x : PostconditionT m α).run = pure x := by
+  simp [run_eq_map]
+
 @[simp]
 theorem PostconditionT.property_lift {m : Type w → Type w'} [Functor m] {α : Type w}
     {x : m α} : (lift x : PostconditionT m α).Property = (fun _ => True) := by
diff --git a/src/Init/Data/Order/Factories.lean b/src/Init/Data/Order/Factories.lean
index 8b52b6f22c..071fc7cc57 100644
--- a/src/Init/Data/Order/Factories.lean
+++ b/src/Init/Data/Order/Factories.lean
@@ -208,7 +208,7 @@ public instance LawfulOrderLT.of_lt {α : Type u} [LT α] [i : Asymm (α := α)
     haveI := LE.ofLT α
     LawfulOrderLT α :=
   letI := LE.ofLT α
-  { lt_iff a b := by simp +instances [LE.le]; apply Asymm.asymm }
+  { lt_iff a b := by simp [LE.le]; apply Asymm.asymm }
 
 /--
 If an `LT α` instance is asymmetric and its negation is transitive, then `LE.ofLT α` represents a
@@ -253,8 +253,7 @@ public theorem LawfulOrderInf.of_lt {α : Type u} [Min α] [LT α]
   letI := LE.ofLT α
   { le_min_iff a b c := by
       open Classical in
-      simp +instances only [LE.le]
-      simp [← not_or, Decidable.not_iff_not]
+      simp only [LE.le, ← not_or, Decidable.not_iff_not]
       simpa [Decidable.imp_iff_not_or] using min_lt_iff a b c }
 
 /--
@@ -283,8 +282,7 @@ public theorem LawfulOrderSup.of_lt {α : Type u} [Max α] [LT α]
   letI := LE.ofLT α
   { max_le_iff a b c := by
       open Classical in
-      simp +instances only [LE.le]
-      simp [← not_or, Decidable.not_iff_not]
+      simp only [LE.le, ← not_or, Decidable.not_iff_not]
       simpa [Decidable.imp_iff_not_or] using lt_max_iff a b c }
 
 /--
diff --git a/src/Init/Data/Order/Opposite.lean b/src/Init/Data/Order/Opposite.lean
index 341aca53b4..3cfc17b51b 100644
--- a/src/Init/Data/Order/Opposite.lean
+++ b/src/Init/Data/Order/Opposite.lean
@@ -287,7 +287,7 @@ scoped instance (priority := low) instLawfulOrderLTOpposite {il : LE α} {it : L
   letI := il.opposite
   letI := it.opposite
   { lt_iff a b := by
-      simp +instances only [LE.opposite, LT.opposite]
+      simp only [LE.le, LT.lt]
       letI := il; letI := it
       exact LawfulOrderLT.lt_iff b a }
 
@@ -297,7 +297,7 @@ scoped instance (priority := low) instLawfulOrderBEqOpposite {il : LE α} {ib :
     LawfulOrderBEq α :=
   letI := il.opposite
   { beq_iff_le_and_ge a b := by
-      simp +instances only [LE.opposite]
+      simp only [LE.le]
       letI := il; letI := ib
       rw [LawfulOrderBEq.beq_iff_le_and_ge]
       exact and_comm }
@@ -310,7 +310,7 @@ scoped instance (priority := low) instLawfulOrderInfOpposite {il : LE α} {im :
   letI := il.opposite
   letI := im.oppositeMax
   { max_le_iff a b c := by
-      simp +instances only [LE.opposite, Min.oppositeMax]
+      simp only [LE.le, Max.max]
       letI := il; letI := im
       exact LawfulOrderInf.le_min_iff c a b }
 
@@ -322,11 +322,11 @@ scoped instance (priority := low) instLawfulOrderMinOpposite {il : LE α} {im :
   letI := il.opposite
   letI := im.oppositeMax
   { max_eq_or a b := by
-      simp +instances only [Min.oppositeMax]
+      simp only [Max.max]
       letI := il; letI := im
       exact MinEqOr.min_eq_or a b
     max_le_iff a b c := by
-      simp +instances only [LE.opposite, Min.oppositeMax]
+      simp only [LE.le, Max.max]
       letI := il; letI := im
       exact LawfulOrderInf.le_min_iff c a b }
 
@@ -338,7 +338,7 @@ scoped instance (priority := low) instLawfulOrderSupOpposite {il : LE α} {im :
   letI := il.opposite
   letI := im.oppositeMin
   { le_min_iff a b c := by
-      simp +instances only [LE.opposite, Max.oppositeMin]
+      simp only [LE.le, Min.min]
       letI := il; letI := im
       exact LawfulOrderSup.max_le_iff b c a }
 
@@ -350,11 +350,11 @@ scoped instance (priority := low) instLawfulOrderMaxOpposite {il : LE α} {im :
   letI := il.opposite
   letI := im.oppositeMin
   { min_eq_or a b := by
-      simp +instances only [Max.oppositeMin]
+      simp only [Min.min]
       letI := il; letI := im
       exact MaxEqOr.max_eq_or a b
     le_min_iff a b c := by
-      simp +instances only [LE.opposite, Max.oppositeMin]
+      simp only [LE.le, Min.min]
       letI := il; letI := im
       exact LawfulOrderSup.max_le_iff b c a }
 
@@ -366,11 +366,11 @@ scoped instance (priority := low) instLawfulOrderLeftLeaningMinOpposite {il : LE
   letI := il.opposite
   letI := im.oppositeMax
   { max_eq_left a b hab := by
-      simp +instances only [Min.oppositeMax]
+      simp only [Max.max]
       letI := il; letI := im
       exact LawfulOrderLeftLeaningMin.min_eq_left a b hab
     max_eq_right a b hab := by
-      simp +instances only [Min.oppositeMax]
+      simp only [Max.max]
       letI := il; letI := im
       exact LawfulOrderLeftLeaningMin.min_eq_right a b hab }
 
@@ -382,11 +382,11 @@ scoped instance (priority := low) instLawfulOrderLeftLeaningMaxOpposite {il : LE
   letI := il.opposite
   letI := im.oppositeMin
   { min_eq_left a b hab := by
-      simp +instances only [Max.oppositeMin]
+      simp only [Min.min]
       letI := il; letI := im
       exact LawfulOrderLeftLeaningMax.max_eq_left a b hab
     min_eq_right a b hab := by
-      simp +instances only [Max.oppositeMin]
+      simp only [Min.min]
       letI := il; letI := im
       exact LawfulOrderLeftLeaningMax.max_eq_right a b hab }
 
diff --git a/src/Init/Data/Order/PackageFactories.lean b/src/Init/Data/Order/PackageFactories.lean
index 6551483c25..cd280c5cc3 100644
--- a/src/Init/Data/Order/PackageFactories.lean
+++ b/src/Init/Data/Order/PackageFactories.lean
@@ -796,7 +796,6 @@ automatically. If it fails, it is necessary to provide some of the fields manual
 @[inline, expose, implicit_reducible]
 public def LinearOrderPackage.ofOrd (α : Type u)
     (args : Packages.LinearOrderOfOrdArgs α := by exact {}) : LinearOrderPackage α :=
-  -- set_option backward.isDefEq.respectTransparency false in
   letI := LinearPreorderPackage.ofOrd α args.toLinearPreorderOfOrdArgs
   haveI : LawfulEqOrd α := ⟨args.eq_of_compare _ _⟩
   letI : Min α := args.min
diff --git a/src/Init/Data/Range/Polymorphic/RangeIterator.lean b/src/Init/Data/Range/Polymorphic/RangeIterator.lean
index 0069a56024..765bc11447 100644
--- a/src/Init/Data/Range/Polymorphic/RangeIterator.lean
+++ b/src/Init/Data/Range/Polymorphic/RangeIterator.lean
@@ -597,7 +597,7 @@ instance Iterator.instLawfulIteratorLoop [UpwardEnumerable α] [LE α] [Decidabl
     LawfulIteratorLoop (Rxc.Iterator α) Id n where
   lawful := by
     intro lift instLawfulMonadLiftFunction γ it init Pl wf f
-    simp +instances only [IteratorLoop.forIn, IterM.DefaultConsumers.forIn'_eq_wf Pl wf]
+    simp only [IteratorLoop.forIn, IterM.DefaultConsumers.forIn'_eq_wf Pl wf]
     rw [IterM.DefaultConsumers.forIn'.wf]
     split; rotate_left
     · simp only [IterM.step_eq,
@@ -636,7 +636,7 @@ The pure function mapping a range iterator of type {name}`IterM` to the next ste
 This function is prefixed with {lit}`Monadic` in order to disambiguate it from the version for iterators
 of type {name}`Iter`.
 -/
-@[inline]
+@[inline, implicit_reducible]
 def Iterator.Monadic.step [UpwardEnumerable α] [LT α] [DecidableLT α]
     (it : IterM (α := Rxo.Iterator α) Id α) :
     IterStep (IterM (α := Rxo.Iterator α) Id α) α :=
@@ -1113,7 +1113,6 @@ private theorem Iterator.instIteratorLoop.loop_eq_wf [UpwardEnumerable α] [LT 
     · rw [WellFounded.fix_eq]
       simp_all
 
-set_option backward.isDefEq.respectTransparency false in
 private theorem Iterator.instIteratorLoop.loopWf_eq [UpwardEnumerable α] [LT α] [DecidableLT α]
     [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α]
     {n : Type u → Type w} [Monad n] [LawfulMonad n] (γ : Type u)
@@ -1165,14 +1164,13 @@ termination_by IteratorLoop.WithWF.mk ⟨⟨some next, upperBound⟩⟩ acc (hwf
 decreasing_by
   simp [IteratorLoop.rel, Monadic.isPlausibleStep_iff, Monadic.step, *]
 
-set_option backward.isDefEq.respectTransparency false in
 instance Iterator.instLawfulIteratorLoop [UpwardEnumerable α] [LT α] [DecidableLT α]
     [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α]
     {n : Type u → Type w} [Monad n] [LawfulMonad n] :
     LawfulIteratorLoop (Rxo.Iterator α) Id n where
   lawful := by
     intro lift instLawfulMonadLiftFunction γ it init Pl wf f
-    simp +instances only [IteratorLoop.forIn, IterM.DefaultConsumers.forIn'_eq_wf Pl wf]
+    simp only [IteratorLoop.forIn, IterM.DefaultConsumers.forIn'_eq_wf Pl wf]
     rw [IterM.DefaultConsumers.forIn'.wf]
     split; rotate_left
     · simp [IterM.step_eq, Monadic.step, Internal.LawfulMonadLiftBindFunction.liftBind_pure (liftBind := lift)]
@@ -1637,7 +1635,7 @@ instance Iterator.instLawfulIteratorLoop [UpwardEnumerable α]
     LawfulIteratorLoop (Rxi.Iterator α) Id n where
   lawful := by
     intro lift instLawfulMonadLiftFunction γ it init Pl wf f
-    simp +instances only [IteratorLoop.forIn, IterM.DefaultConsumers.forIn'_eq_wf Pl wf]
+    simp only [IteratorLoop.forIn, IterM.DefaultConsumers.forIn'_eq_wf Pl wf]
     rw [IterM.DefaultConsumers.forIn'.wf]
     split; rotate_left
     · simp [Monadic.step_eq_step, Monadic.step, Internal.LawfulMonadLiftBindFunction.liftBind_pure]
diff --git a/src/Init/Data/Range/Polymorphic/SInt.lean b/src/Init/Data/Range/Polymorphic/SInt.lean
index 37ba74ad27..153e74d991 100644
--- a/src/Init/Data/Range/Polymorphic/SInt.lean
+++ b/src/Init/Data/Range/Polymorphic/SInt.lean
@@ -248,7 +248,16 @@ instance : HasModel Int8 (BitVec 8) where
   le_iff_encode_le := by simp [LE.le, Int8.le]
   lt_iff_encode_lt := by simp [LT.lt, Int8.lt]
 
-set_option backward.whnf.reducibleClassField false in
+private theorem succ?_eq_minValueSealed {x : Int8} :
+    UpwardEnumerable.succ? x = if x + 1 = minValueSealed then none else some (x + 1) :=
+  (rfl)
+
+private theorem succMany?_eq_maxValueSealed {i : Int8} :
+    UpwardEnumerable.succMany? n i =
+      have := i.minValue_le_toInt
+      if h : i.toInt + n ≤ maxValueSealed.toInt then some (.ofIntLE _ (by omega) (maxValueSealed_def ▸ h)) else none :=
+  (rfl)
+
 theorem instUpwardEnumerable_eq :
     instUpwardEnumerable = HasModel.instUpwardEnumerable := by
   apply UpwardEnumerable.ext
@@ -256,16 +265,16 @@ theorem instUpwardEnumerable_eq :
     apply HasModel.succ?_eq_of_technicalCondition
     simp [HasModel.encode, succ?, ← Int8.toBitVec_inj, toBitVec_minValueSealed_eq_intMinSealed]
   · ext
-    simp +instances [HasModel.succMany?_eq, instUpwardEnumerable, HasModel.encode, HasModel.decode,
+    simp [HasModel.succMany?_eq, succMany?_eq_maxValueSealed, HasModel.encode, HasModel.decode,
       ← toInt_toBitVec, toBitVec_maxValueSealed_eq_intMaxSealed, ofIntLE_eq_ofInt]
 
 
 instance : LawfulUpwardEnumerable Int8 := by
-  simp +instances only [instUpwardEnumerable_eq]
+  rw [instUpwardEnumerable_eq]
   infer_instance
 
 instance : LawfulUpwardEnumerableLE Int8 := by
-  simp +instances only [instUpwardEnumerable_eq]
+  rw [instUpwardEnumerable_eq]
   infer_instance
 
 public instance instRxcHasSize : Rxc.HasSize Int8 where
@@ -277,7 +286,7 @@ theorem instRxcHasSize_eq :
     ← toInt_toBitVec, HasModel.toNat_toInt_add_one_sub_toInt (Nat.zero_lt_succ _)]
 
 public instance instRxcLawfulHasSize : Rxc.LawfulHasSize Int8 := by
-  simp +instances only [instUpwardEnumerable_eq, instRxcHasSize_eq]
+  rw [instUpwardEnumerable_eq, instRxcHasSize_eq]
   infer_instance
 public instance : Rxc.IsAlwaysFinite Int8 := by exact inferInstance
 
@@ -294,7 +303,7 @@ theorem instRxiHasSize_eq :
     HasModel.encode, HasModel.toNat_two_pow_sub_one_sub_toInt (show 8 > 0 by omega)]
 
 public instance instRxiLawfulHasSize : Rxi.LawfulHasSize Int8 := by
-  simp +instances only [instUpwardEnumerable_eq, instRxiHasSize_eq]
+  rw [instUpwardEnumerable_eq, instRxiHasSize_eq]
   infer_instance
 public instance instRxiIsAlwaysFinite : Rxi.IsAlwaysFinite Int8 := by exact inferInstance
 
@@ -344,7 +353,6 @@ instance : HasModel Int16 (BitVec 16) where
   le_iff_encode_le := by simp [LE.le, Int16.le]
   lt_iff_encode_lt := by simp [LT.lt, Int16.lt]
 
-set_option backward.whnf.reducibleClassField false in
 theorem instUpwardEnumerable_eq :
     instUpwardEnumerable = HasModel.instUpwardEnumerable := by
   apply UpwardEnumerable.ext
@@ -440,7 +448,6 @@ instance : HasModel Int32 (BitVec 32) where
   le_iff_encode_le := by simp [LE.le, Int32.le]
   lt_iff_encode_lt := by simp [LT.lt, Int32.lt]
 
-set_option backward.whnf.reducibleClassField false in
 theorem instUpwardEnumerable_eq :
     instUpwardEnumerable = HasModel.instUpwardEnumerable := by
   apply UpwardEnumerable.ext
@@ -536,7 +543,6 @@ instance : HasModel Int64 (BitVec 64) where
   le_iff_encode_le := by simp [LE.le, Int64.le]
   lt_iff_encode_lt := by simp [LT.lt, Int64.lt]
 
-set_option backward.whnf.reducibleClassField false in
 theorem instUpwardEnumerable_eq :
     instUpwardEnumerable = HasModel.instUpwardEnumerable := by
   apply UpwardEnumerable.ext
@@ -637,7 +643,6 @@ instance : HasModel ISize (BitVec System.Platform.numBits) where
   le_iff_encode_le := by simp [LE.le, ISize.le]
   lt_iff_encode_lt := by simp [LT.lt, ISize.lt]
 
-set_option backward.whnf.reducibleClassField false in
 theorem instUpwardEnumerable_eq :
     instUpwardEnumerable = HasModel.instUpwardEnumerable := by
   apply UpwardEnumerable.ext
diff --git a/src/Init/Data/Slice/Array/Iterator.lean b/src/Init/Data/Slice/Array/Iterator.lean
index 8b47191a50..b17a563cc4 100644
--- a/src/Init/Data/Slice/Array/Iterator.lean
+++ b/src/Init/Data/Slice/Array/Iterator.lean
@@ -26,7 +26,7 @@ variable {shape : RangeShape} {α : Type u}
 structure SubarrayIterator (α : Type u) where
   xs : Subarray α
 
-@[inline, expose]
+@[inline, expose, implicit_reducible]
 def SubarrayIterator.step :
     IterM (α := SubarrayIterator α) Id α → IterStep (IterM (α := SubarrayIterator α) m α) α
   | ⟨⟨xs⟩⟩ =>
diff --git a/src/Init/Data/Slice/Array/Lemmas.lean b/src/Init/Data/Slice/Array/Lemmas.lean
index 730808098c..7497049302 100644
--- a/src/Init/Data/Slice/Array/Lemmas.lean
+++ b/src/Init/Data/Slice/Array/Lemmas.lean
@@ -28,7 +28,6 @@ open Std Std.Iterators Std.PRange Std.Slice
 
 namespace SubarrayIterator
 
-set_option backward.isDefEq.respectTransparency false in
 theorem step_eq {it : Iter (α := SubarrayIterator α) α} :
     it.step = if h : it.1.xs.start < it.1.xs.stop then
         haveI := it.1.xs.start_le_stop
@@ -215,7 +214,6 @@ public theorem Array.stop_toSubarray {xs : Array α} {lo hi : Nat} :
     (xs.toSubarray lo hi).stop = min hi xs.size := by
   simp [toSubarray_eq_min, Subarray.stop]
 
-set_option backward.whnf.reducibleClassField false in
 public theorem Subarray.toList_eq {xs : Subarray α} :
     xs.toList = (xs.array.extract xs.start xs.stop).toList := by
   let aslice := xs
diff --git a/src/Init/Data/Slice/List/Lemmas.lean b/src/Init/Data/Slice/List/Lemmas.lean
index dc8c147760..fbf75027af 100644
--- a/src/Init/Data/Slice/List/Lemmas.lean
+++ b/src/Init/Data/Slice/List/Lemmas.lean
@@ -70,7 +70,6 @@ end ListSlice
 
 namespace List
 
-set_option backward.whnf.reducibleClassField false in
 @[simp, grind =]
 public theorem toList_mkSlice_rco {xs : List α} {lo hi : Nat} :
     xs[lo...hi].toList = (xs.take hi).drop lo := by
@@ -78,9 +77,9 @@ public theorem toList_mkSlice_rco {xs : List α} {lo hi : Nat} :
   simp only [Std.Rco.Sliceable.mkSlice, toSlice, ListSlice.toList_eq]
   by_cases h : lo < hi
   · have : lo ≤ hi := by omega
-    simp +instances [h, List.take_drop, Nat.add_sub_cancel' ‹_›, ← List.take_eq_take_min]
+    simp [h, List.take_drop, Nat.add_sub_cancel' ‹_›, ← List.take_eq_take_min]
   · have : min hi xs.length ≤ lo := by omega
-    simp +instances [h, Nat.min_eq_right this]
+    simp [h, Nat.min_eq_right this]
 
 @[simp, grind =]
 public theorem toArray_mkSlice_rco {xs : List α} {lo hi : Nat} :
@@ -111,12 +110,11 @@ public theorem size_mkSlice_rcc {xs : List α} {lo hi : Nat} :
     xs[lo...=hi].size = min (hi + 1) xs.length - lo := by
   simp [← length_toList_eq_size]
 
-set_option backward.whnf.reducibleClassField false in
 @[simp, grind =]
 public theorem toList_mkSlice_rci {xs : List α} {lo : Nat} :
     xs[lo...*].toList = xs.drop lo := by
   rw [List.drop_eq_drop_min]
-  simp +instances [ListSlice.toList_eq, Std.Rci.Sliceable.mkSlice, List.toUnboundedSlice]
+  simp [ListSlice.toList_eq, Std.Rci.Sliceable.mkSlice, List.toUnboundedSlice]
 
 @[simp, grind =]
 public theorem toArray_mkSlice_rci {xs : List α} {lo : Nat} :
@@ -290,11 +288,11 @@ section ListSubslices
 
 namespace ListSlice
 
-set_option backward.whnf.reducibleClassField false in
 @[simp, grind =]
 public theorem toList_mkSlice_rco {xs : ListSlice α} {lo hi : Nat} :
     xs[lo...hi].toList = (xs.toList.take hi).drop lo := by
-  simp +instances only [instSliceableListSliceNat_1, List.toList_mkSlice_rco, ListSlice.toList_eq (xs := xs)]
+  rw [instSliceableListSliceNat_1]
+  simp only [List.toList_mkSlice_rco, ListSlice.toList_eq (xs := xs)]
   obtain ⟨⟨xs, stop⟩⟩ := xs
   cases stop
   · simp
@@ -329,13 +327,13 @@ public theorem size_mkSlice_rcc {xs : ListSlice α} {lo hi : Nat} :
     xs[lo...=hi].size = min (hi + 1) xs.size - lo := by
   simp [← length_toList_eq_size]
 
-set_option backward.whnf.reducibleClassField false in
 @[simp, grind =]
 public theorem toList_mkSlice_rci {xs : ListSlice α} {lo : Nat} :
     xs[lo...*].toList = xs.toList.drop lo := by
-  simp +instances only [instSliceableListSliceNat_2, ListSlice.toList_eq (xs := xs)]
+  rw [instSliceableListSliceNat_2]
+  simp only [ListSlice.toList_eq (xs := xs)]
   obtain ⟨⟨xs, stop⟩⟩ := xs
-  simp +instances only
+  simp only
   split <;> simp
 
 @[simp, grind =]
diff --git a/src/Std/Data/DTreeMap/Internal/Model.lean b/src/Std/Data/DTreeMap/Internal/Model.lean
index 0bd744965d..804f9f0b24 100644
--- a/src/Std/Data/DTreeMap/Internal/Model.lean
+++ b/src/Std/Data/DTreeMap/Internal/Model.lean
@@ -1011,7 +1011,6 @@ theorem getEntryGT?_eq_getEntryGT?ₘ [Ord α] (k : α) (t : Impl α β) :
     getEntryGT? k t = getEntryGT?ₘ k t := by
   rw [getEntryGT?_eq_getEntryGT?ₘ', getEntryGT?ₘ', getEntryGT?ₘ, explore_eq_applyPartition] <;> simp
 
-set_option backward.whnf.reducibleClassField false in
 theorem getEntryLT?_eq_getEntryGT?_reverse [o : Ord α] [TransOrd α] {t : Impl α β} {k : α} :
     getEntryLT? k t = @getEntryGT? α β o.opposite k t.reverse := by
   rw [getEntryLT?, @getEntryGT?.eq_def, Ord.opposite]
@@ -1019,7 +1018,6 @@ theorem getEntryLT?_eq_getEntryGT?_reverse [o : Ord α] [TransOrd α] {t : Impl
     simp only [*, getEntryLT?.go, reverse, getEntryGT?.go, OrientedCmp.eq_swap (b := k),
       Ordering.swap]
 
-set_option backward.whnf.reducibleClassField false in
 theorem getEntryLE?_eq_getEntryGE?_reverse [o : Ord α] [TransOrd α] {t : Impl α β} {k : α} :
     getEntryLE? k t = @getEntryGE? α β o.opposite k t.reverse := by
   rw [getEntryLE?, @getEntryGE?.eq_def, Ord.opposite]
diff --git a/src/Std/Data/DTreeMap/Internal/Zipper.lean b/src/Std/Data/DTreeMap/Internal/Zipper.lean
index 46c61398b5..dc54fc1adc 100644
--- a/src/Std/Data/DTreeMap/Internal/Zipper.lean
+++ b/src/Std/Data/DTreeMap/Internal/Zipper.lean
@@ -623,7 +623,6 @@ theorem RxoIterator.step_cons_of_isLT_eq_false [Ord α] {upper : α} {h : (compa
   rw [step, h]
   simp only [Bool.false_eq_true, ↓reduceIte]
 
-set_option backward.isDefEq.respectTransparency false in
 @[simp]
 theorem RxoIterator.val_run_step_toIterM_iter [Ord α] {z : RxoIterator α β} : (⟨z⟩ : Iter (α := RxoIterator α β) ((a : α) × β a)).toIterM.step.run.inflate.val = z.step := by
   rw [IterM.step]
diff --git a/src/Std/Data/DTreeMap/Raw/Lemmas.lean b/src/Std/Data/DTreeMap/Raw/Lemmas.lean
index e2c2ebe369..1edbefb7a1 100644
--- a/src/Std/Data/DTreeMap/Raw/Lemmas.lean
+++ b/src/Std/Data/DTreeMap/Raw/Lemmas.lean
@@ -1895,7 +1895,6 @@ theorem contains_of_contains_insertMany_list' [TransCmp cmp] [BEq α] [LawfulBEq
     (h' : contains (insertMany t l) k = true)
     (w : l.findSomeRev? (fun ⟨a, b⟩ => if cmp a k = .eq then some b else none) = none) :
     contains t k = true :=
-  set_option backward.whnf.reducibleClassField false in
   Impl.Const.contains_of_contains_insertMany_list' h
     (by simpa [Impl.Const.insertMany_eq_insertMany!] using h')
     (by simpa [compare_eq_iff_beq, BEq.comm] using w)