diff --git a/src/Init/Data/Array/Basic.lean b/src/Init/Data/Array/Basic.lean
index 17bb601808f2..3cb87d701ae1 100644
--- a/src/Init/Data/Array/Basic.lean
+++ b/src/Init/Data/Array/Basic.lean
@@ -170,7 +170,7 @@ Low-level indexing operator which is as fast as a C array read.
 
 This avoids overhead due to unboxing a `Nat` used as an index.
 -/
-@[extern "lean_array_uget", simp, expose]
+@[extern "lean_array_uget", simp, expose, implicit_reducible]
 def uget (xs : @& Array α) (i : USize) (h : i.toNat < xs.size) : α :=
   xs[i.toNat]
 
@@ -189,7 +189,7 @@ in-place when the reference to the array is unique.
 
 This avoids overhead due to unboxing a `Nat` used as an index.
 -/
-@[extern "lean_array_uset", expose]
+@[extern "lean_array_uset", expose, implicit_reducible]
 def uset (xs : Array α) (i : USize) (v : α) (h : i.toNat < xs.size) : Array α :=
   xs.set i.toNat v h
 
diff --git a/src/Init/Data/Array/Lemmas.lean b/src/Init/Data/Array/Lemmas.lean
index 30ac3cbd4f1c..c826f2a4c11c 100644
--- a/src/Init/Data/Array/Lemmas.lean
+++ b/src/Init/Data/Array/Lemmas.lean
@@ -1872,7 +1872,7 @@ theorem getElem_of_append {xs ys zs : Array α} (eq : xs = ys.push a ++ zs) (h :
   rw [← getElem?_eq_getElem, eq, getElem?_append_left (by simp; omega), ← h]
   simp
 
-@[simp] theorem append_singleton {a : α} {as : Array α} : as ++ #[a] = as.push a := rfl
+@[simp] theorem append_singleton {a : α} {as : Array α} : as ++ #[a] = as.push a := (rfl)
 
 @[simp] theorem append_singleton_assoc {a : α} {xs ys : Array α} : xs ++ (#[a] ++ ys) = xs.push a ++ ys := by
   rw [← append_assoc, append_singleton]
@@ -2831,12 +2831,10 @@ theorem getElem_extract_aux {xs : Array α} {start stop : Nat} (h : i < (xs.extr
   rw [size_extract] at h; apply Nat.add_lt_of_lt_sub'; apply Nat.lt_of_lt_of_le h
   apply Nat.sub_le_sub_right; apply Nat.min_le_right
 
-set_option backward.isDefEq.respectTransparency.types false in
 @[simp, grind =] theorem getElem_extract {xs : Array α} {start stop : Nat}
     (h : i < (xs.extract start stop).size) :
-    (xs.extract start stop)[i] = xs[start + i]'(getElem_extract_aux h) :=
-  show (extract.loop xs (min stop xs.size - start) start #[])[i]
-    = xs[start + i]'(getElem_extract_aux h) by rw [getElem_extract_loop_ge]; rfl; exact Nat.zero_le _
+    (xs.extract start stop)[i] = xs[start + i]'(getElem_extract_aux h) := by
+  simp [extract, getElem_extract_loop_ge]
 
 theorem getElem?_extract {xs : Array α} {start stop : Nat} :
     (xs.extract start stop)[i]? = if i < min stop xs.size - start then xs[start + i]? else none := by
diff --git a/src/Init/Data/Array/MapIdx.lean b/src/Init/Data/Array/MapIdx.lean
index f1949d738dee..98defc144722 100644
--- a/src/Init/Data/Array/MapIdx.lean
+++ b/src/Init/Data/Array/MapIdx.lean
@@ -198,7 +198,6 @@ theorem mapFinIdx_append {xs ys : Array α} {f : (i : Nat) → α → (h : i < (
   cases ys
   simp [List.mapFinIdx_append, Array.size]
 
-set_option backward.isDefEq.respectTransparency.types false in
 @[simp, grind =]
 theorem mapFinIdx_push {xs : Array α} {a : α} {f : (i : Nat) → α → (h : i < (xs.push a).size) → β} :
     mapFinIdx (xs.push a) f =
diff --git a/src/Init/Data/BitVec/Basic.lean b/src/Init/Data/BitVec/Basic.lean
index c862c823e2c0..b441b0b90824 100644
--- a/src/Init/Data/BitVec/Basic.lean
+++ b/src/Init/Data/BitVec/Basic.lean
@@ -130,7 +130,7 @@ theorem getElem_eq_testBit_toNat (x : BitVec w) (i : Nat) (h : i < w) :
 
 @[simp, grind =]
 theorem getLsbD_eq_getElem {x : BitVec w} {i : Nat} (h : i < w) :
-    x.getLsbD i = x[i] := rfl
+    x.getLsbD i = x[i] := (rfl)
 
 end getElem
 
@@ -139,7 +139,7 @@ section Int
 /--
 Interprets the bitvector as an integer stored in two's complement form.
 -/
-@[expose]
+@[expose, implicit_reducible]
 protected def toInt (x : BitVec n) : Int :=
   if 2 * x.toNat < 2^n then
     x.toNat
@@ -228,7 +228,7 @@ Usually accessed via the `-` prefix operator.
 
 SMT-LIB name: `bvneg`.
 -/
-@[expose]
+@[expose, implicit_reducible]
 protected def neg (x : BitVec n) : BitVec n := .ofNat n (2^n - x.toNat)
 instance : Neg (BitVec n) := ⟨.neg⟩
 
@@ -753,20 +753,20 @@ instance : Hashable (BitVec n) where
 
 section normalization_eqs
 /-! We add simp-lemmas that rewrite bitvector operations into the equivalent notation -/
-@[simp, grind =] theorem append_eq (x : BitVec w) (y : BitVec v) : BitVec.append x y = x ++ y        := rfl
-@[simp, grind =] theorem shiftLeft_eq (x : BitVec w) (n : Nat)     : BitVec.shiftLeft x n = x <<< n    := rfl
-@[simp, grind =] theorem ushiftRight_eq (x : BitVec w) (n : Nat)   : BitVec.ushiftRight x n = x >>> n  := rfl
-@[simp, grind =] theorem not_eq (x : BitVec w)                     : BitVec.not x = ~~~x               := rfl
-@[simp, grind =] theorem and_eq (x y : BitVec w)                   : BitVec.and x y = x &&& y          := rfl
-@[simp, grind =] theorem or_eq (x y : BitVec w)                    : BitVec.or x y = x ||| y           := rfl
-@[simp, grind =] theorem xor_eq (x y : BitVec w)                   : BitVec.xor x y = x ^^^ y          := rfl
-@[simp, grind =] theorem neg_eq (x : BitVec w)                     : BitVec.neg x = -x                 := rfl
-@[simp, grind =] theorem add_eq (x y : BitVec w)                   : BitVec.add x y = x + y            := rfl
-@[simp, grind =] theorem sub_eq (x y : BitVec w)                   : BitVec.sub x y = x - y            := rfl
-@[simp, grind =] theorem mul_eq (x y : BitVec w)                   : BitVec.mul x y = x * y            := rfl
-@[simp, grind =] theorem udiv_eq (x y : BitVec w)                  : BitVec.udiv x y = x / y           := rfl
-@[simp, grind =] theorem umod_eq (x y : BitVec w)                  : BitVec.umod x y = x % y           := rfl
-@[simp, grind =] theorem zero_eq                                   : BitVec.zero n = 0#n               := rfl
+@[simp, grind =] theorem append_eq (x : BitVec w) (y : BitVec v) : BitVec.append x y = x ++ y        := (rfl)
+@[simp, grind =] theorem shiftLeft_eq (x : BitVec w) (n : Nat)     : BitVec.shiftLeft x n = x <<< n    := (rfl)
+@[simp, grind =] theorem ushiftRight_eq (x : BitVec w) (n : Nat)   : BitVec.ushiftRight x n = x >>> n  := (rfl)
+@[simp, grind =] theorem not_eq (x : BitVec w)                     : BitVec.not x = ~~~x               := (rfl)
+@[simp, grind =] theorem and_eq (x y : BitVec w)                   : BitVec.and x y = x &&& y          := (rfl)
+@[simp, grind =] theorem or_eq (x y : BitVec w)                    : BitVec.or x y = x ||| y           := (rfl)
+@[simp, grind =] theorem xor_eq (x y : BitVec w)                   : BitVec.xor x y = x ^^^ y          := (rfl)
+@[simp, grind =] theorem neg_eq (x : BitVec w)                     : BitVec.neg x = -x                 := (rfl)
+@[simp, grind =] theorem add_eq (x y : BitVec w)                   : BitVec.add x y = x + y            := (rfl)
+@[simp, grind =] theorem sub_eq (x y : BitVec w)                   : BitVec.sub x y = x - y            := (rfl)
+@[simp, grind =] theorem mul_eq (x y : BitVec w)                   : BitVec.mul x y = x * y            := (rfl)
+@[simp, grind =] theorem udiv_eq (x y : BitVec w)                  : BitVec.udiv x y = x / y           := (rfl)
+@[simp, grind =] theorem umod_eq (x y : BitVec w)                  : BitVec.umod x y = x % y           := (rfl)
+@[simp, grind =] theorem zero_eq                                   : BitVec.zero n = 0#n               := (rfl)
 end normalization_eqs
 
 /-- Converts a list of `Bool`s into a big-endian `BitVec`. -/
diff --git a/src/Init/Data/BitVec/Bitblast.lean b/src/Init/Data/BitVec/Bitblast.lean
index 1f9d4bc01771..259840c54f08 100644
--- a/src/Init/Data/BitVec/Bitblast.lean
+++ b/src/Init/Data/BitVec/Bitblast.lean
@@ -2006,7 +2006,6 @@ theorem toInt_smod {x y : BitVec w} :
         simp [BitVec.toInt_eq_neg_toNat_neg_of_msb_true, hxmsb, hymsb,
           Int.fmod_eq_emod_of_nonneg _]
 
-set_option backward.isDefEq.respectTransparency.types false in
 theorem getElem_smod {x y : BitVec w} (h : i < w) :
     (x.smod y)[i] =
       match x.msb, y.msb with
@@ -2015,8 +2014,7 @@ theorem getElem_smod {x y : BitVec w} (h : i < w) :
       | true, false => (if -x % y = 0#w then (-x % y) else (y - -x % y))[i]
       | true, true => (-(-x % -y))[i] := by
   simp only [smod, umod_eq, neg_eq, zero_eq, add_eq, sub_eq]
-  by_cases hx : x.msb <;> by_cases hy : y.msb
-  <;> simp [hx, hy]
+  by_cases hx : x.msb <;> by_cases hy : y.msb <;> simp [hx, hy]
 
 theorem getLsbD_smod {x y : BitVec w} :
     (x.smod y).getLsbD i =
@@ -2032,7 +2030,6 @@ theorem getLsbD_smod {x y : BitVec w} :
   · by_cases hxy : x % -y = 0#w <;> simp [hx, hy, hxy]
   · simp [hx, hy]
 
-set_option backward.isDefEq.respectTransparency.types false in
 theorem getMsbD_smod {x y : BitVec w} :
     (x.smod y).getMsbD i  =
       match x.msb, y.msb with
@@ -2041,8 +2038,7 @@ theorem getMsbD_smod {x y : BitVec w} :
       | true, false => (if -x % y = 0#w then (-x % y) else (y - -x % y)).getMsbD i
       | true, true => (-(-x % -y)).getMsbD i := by
   simp only [smod, umod_eq, neg_eq, zero_eq, add_eq, sub_eq]
-  by_cases hx : x.msb <;> by_cases hy : y.msb
-  <;> simp [hx, hy]
+  by_cases hx : x.msb <;> by_cases hy : y.msb <;> simp [hx, hy]
 
 theorem msb_smod {x y : BitVec w} :
     (x.smod y).msb = (x.msb && y = 0) || (y.msb && (x.smod y) ≠ 0) := by
diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index 21a6334f4470..49188d1b58e7 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -2063,7 +2063,7 @@ theorem shiftLeft_ofNat_eq {x : BitVec w} {k : Nat} : x <<< (BitVec.ofNat w k) =
 /-! ### ushiftRight -/
 
 @[simp, bitvec_to_nat, grind =] theorem toNat_ushiftRight (x : BitVec n) (i : Nat) :
-    (x >>> i).toNat = x.toNat >>> i := rfl
+    (x >>> i).toNat = x.toNat >>> i := (rfl)
 
 @[simp, grind =] theorem getLsbD_ushiftRight (x : BitVec n) (i j : Nat) :
     getLsbD (x >>> i) j = getLsbD x (i+j) := by
@@ -2115,7 +2115,6 @@ theorem ushiftRight_eq_zero {x : BitVec w} {n : Nat} (hn : w ≤ n) :
   have : 2^w ≤ 2^n := Nat.pow_le_pow_of_le Nat.one_lt_two hn
   rw [Nat.shiftRight_eq_div_pow, Nat.div_eq_of_lt (by omega)]
 
-set_option backward.isDefEq.respectTransparency.types false in
 /--
 Unsigned shift right by at least one bit makes the interpretations of the bitvector as an `Int` or `Nat` agree,
 because it makes the value of the bitvector less than or equal to `2^(w-1)`.
@@ -4704,7 +4703,6 @@ theorem toFin_srem {x y : BitVec w} : (x.srem y).toFin =
 
 /-! ### smod -/
 
-set_option backward.isDefEq.respectTransparency.types false in
 /-- Equation theorem for `smod` in terms of `umod`. -/
 theorem smod_eq (x y : BitVec w) : x.smod y =
   match x.msb, y.msb with
@@ -4716,7 +4714,7 @@ theorem smod_eq (x y : BitVec w) : x.smod y =
     let u := umod (- x) y
     (if u = 0#w then u else y - u)
   | true, true => - ((- x).umod (- y)) := by
-  rw [BitVec.smod]
+  rw [BitVec.smod, BitVec.zero_eq]
   rcases x.msb <;> rcases y.msb <;> simp
 
 @[bitvec_to_nat]
@@ -6145,7 +6143,6 @@ theorem clzAuxRec_le {x : BitVec w} (n : Nat) :
       · simp only [hxn, Bool.false_eq_true, reduceIte]
         exact ihn
 
-set_option backward.isDefEq.respectTransparency.types false in
 theorem clzAuxRec_eq_iff_of_getLsbD_false {x : BitVec w} (h : ∀ i, n < i → x.getLsbD i = false) :
     x.clzAuxRec n = BitVec.ofNat w w ↔ ∀ j, j ≤ n → x.getLsbD j = false := by
   rcases w with _|w
diff --git a/src/Init/Data/Dyadic/Basic.lean b/src/Init/Data/Dyadic/Basic.lean
index 5aaff63bc5d4..5debc6dae06c 100644
--- a/src/Init/Data/Dyadic/Basic.lean
+++ b/src/Init/Data/Dyadic/Basic.lean
@@ -673,9 +673,8 @@ theorem blt_eq_false_iff : blt x y = false ↔ ble y x = true := by
     rw [← Int.neg_sub]
     rcases k₁ - k₂ with (_ | _) | _
     · simp
-    · simp [← Int.negSucc_eq]
-    · simp only [Int.neg_negSucc, decide_eq_false_iff_not, Int.not_lt,
-        decide_eq_true_eq]
+    · simp
+    · simp only [decide_eq_false_iff_not, Int.not_lt, decide_eq_true_eq]
 
 theorem ble_iff_toRat : ble x y ↔ x.toRat ≤ y.toRat := by
   rw [← blt_eq_false_iff, Bool.eq_false_iff]
diff --git a/src/Init/Data/Int/Basic.lean b/src/Init/Data/Int/Basic.lean
index fc7879e84960..b7eb8766e7a0 100644
--- a/src/Init/Data/Int/Basic.lean
+++ b/src/Init/Data/Int/Basic.lean
@@ -99,6 +99,7 @@ Examples:
  * `Int.negOfNat 6 = -6`
  * `Int.negOfNat 0 = 0`
 -/
+@[implicit_reducible]
 def negOfNat : Nat → Int
   | 0      => 0
   | succ m => negSucc m
@@ -115,7 +116,7 @@ Examples:
  * `-(-6 : Int) = 6`
  * `(12 : Int).neg = -12`
 -/
-@[extern "lean_int_neg"]
+@[extern "lean_int_neg", implicit_reducible]
 protected def neg (n : @& Int) : Int :=
   match n with
   | ofNat n   => negOfNat n
@@ -141,6 +142,7 @@ Examples:
  * `Int.subNatNat 2 5 = -3`
  * `Int.subNatNat 0 13 = -13`
 -/
+@[implicit_reducible]
 def subNatNat (m n : Nat) : Int :=
   match (n - m : Nat) with
   | 0        => ofNat (m - n)  -- m ≥ n
@@ -203,7 +205,7 @@ Examples:
 * `(7 : Int) - (0 : Int) = 7`
 * `(0 : Int) - (7 : Int) = -7`
 -/
-@[extern "lean_int_sub"]
+@[extern "lean_int_sub", implicit_reducible]
 protected def sub (m n : @& Int) : Int := m + (- n)
 
 instance : Sub Int where
@@ -397,6 +399,7 @@ Examples:
 * `(0 : Int) ^ 10 = 0`
 * `(-7 : Int) ^ 3 = -343`
 -/
+@[implicit_reducible]
 protected def pow : Int → Nat → Int
   | (m : Nat), n => Int.ofNat (m ^ n)
   | m@-[_+1], n => if n % 2 = 0 then Int.ofNat (m.natAbs ^ n) else - Int.ofNat (m.natAbs ^ n)
diff --git a/src/Init/Data/Int/DivMod/Lemmas.lean b/src/Init/Data/Int/DivMod/Lemmas.lean
index 3170e8101ab2..f7bc9569d64a 100644
--- a/src/Init/Data/Int/DivMod/Lemmas.lean
+++ b/src/Init/Data/Int/DivMod/Lemmas.lean
@@ -1288,8 +1288,8 @@ theorem ediv_mul_of_nonneg {x y z : Int} (hy : 0 ≤ y) : x / (y * z) = x / y /
 @[simp] protected theorem tdiv_neg : ∀ a b : Int, a.tdiv (-b) = -(a.tdiv b)
   | ofNat m, 0 => show ofNat (m / 0) = -↑(m / 0) by rw [Nat.div_zero]; rfl
   | ofNat _, -[_+1] | -[_+1], succ _ => (Int.neg_neg _).symm
-  | ofNat _, succ _ | -[_+1], 0 => by simp [Int.tdiv, Int.neg_zero, ← Int.negSucc_eq]
-  | -[_+1], -[_+1] => by simp only [tdiv, neg_negSucc]
+  | ofNat _, succ _ | -[_+1], 0 => by simp [Int.tdiv, Int.neg_zero]
+  | -[_+1], -[_+1] => by simp only [tdiv]
 
 /-!
 There are no lemmas
@@ -1383,9 +1383,9 @@ protected theorem eq_tdiv_of_mul_eq_left {a b c : Int}
 
 @[simp] protected theorem neg_tdiv : ∀ a b : Int, (-a).tdiv b = -(a.tdiv b)
   | 0, n => by simp [Int.neg_zero]
-  | succ _, (n:Nat) => by simp [tdiv, ← Int.negSucc_eq]
+  | succ _, (n:Nat) => by simp [tdiv]
   | -[_+1], 0 | -[_+1], -[_+1] => by
-    simp only [tdiv, neg_negSucc, Int.neg_neg]
+    simp only [tdiv, Int.neg_neg]
   | succ _, -[_+1] | -[_+1], succ _ => (Int.neg_neg _).symm
 
 protected theorem neg_tdiv_neg (a b : Int) : (-a).tdiv (-b) = a.tdiv b := by
@@ -2112,21 +2112,16 @@ theorem neg_fdiv {a b : Int} : (-a).fdiv b = -(a.fdiv b) - if b = 0 ∨ b ∣ a
   | ofNat (a + 1), 0 => simp
   | ofNat (a + 1), ofNat (b + 1) =>
     unfold fdiv
-    simp only [ofNat_eq_natCast, Int.natCast_add, cast_ofNat_Int, Nat.succ_eq_add_one]
-    rw [← negSucc_eq, ← negSucc_eq]
+    simp
   | ofNat (a + 1), -[b+1] =>
     unfold fdiv
-    simp only [ofNat_eq_natCast, Int.natCast_add, cast_ofNat_Int, Nat.succ_eq_add_one]
-    rw [← negSucc_eq, neg_negSucc]
+    simp
   | -[a+1], 0 => simp
   | -[a+1], ofNat (b + 1) =>
     unfold fdiv
-    simp only [ofNat_eq_natCast, Int.natCast_add, cast_ofNat_Int, Nat.succ_eq_add_one]
-    rw [neg_negSucc, ← negSucc_eq]
+    simp
   | -[a+1], -[b+1] =>
     unfold fdiv
-    simp only [ofNat_eq_natCast, natCast_ediv, Nat.succ_eq_add_one, Int.natCast_add, cast_ofNat_Int]
-    rw [neg_negSucc, neg_negSucc]
     simp
 
 theorem fdiv_neg {a b : Int} (h : b ≠ 0) : a.fdiv (-b) = if b ∣ a then -(a.fdiv b) else -(a.fdiv b) - 1 := by
diff --git a/src/Init/Data/Iterators/Basic.lean b/src/Init/Data/Iterators/Basic.lean
index 2ade57faa3a8..57600d13a03d 100644
--- a/src/Init/Data/Iterators/Basic.lean
+++ b/src/Init/Data/Iterators/Basic.lean
@@ -183,14 +183,14 @@ add_decl_doc IterM.mk
 Converts a pure iterator (`Iter β`) into a monadic iterator (`IterM Id β`) in the
 identity monad `Id`.
 -/
-@[expose]
+@[expose, implicit_reducible]
 def Iter.toIterM {α : Type w} {β : Type w} (it : Iter (α := α) β) : IterM (α := α) Id β :=
   ⟨it.internalState⟩
 
 /--
 Converts a monadic iterator (`IterM Id β`) over `Id` into a pure iterator (`Iter β`).
 -/
-@[expose]
+@[expose, implicit_reducible]
 def IterM.toIter {α : Type w} {β : Type w} (it : IterM (α := α) Id β) : Iter (α := α) β :=
   ⟨it.internalState⟩
 
@@ -569,6 +569,12 @@ def IterM.Step.toPure {α : Type w} {β : Type w} [Iterator α Id β] {it : Iter
     (step : it.Step) : it.toIter.Step :=
   ⟨step.val.mapIterator IterM.toIter, (by simp [Iter.IsPlausibleStep, step.property])⟩
 
+@[simp]
+theorem IterM.Step.val_toPure {α β : Type w} [Iterator α Id β] {it : IterM (α := α) Id β}
+    {step : it.Step} :
+    step.toPure.val = step.val.mapIterator IterM.toIter :=
+  (rfl)
+
 @[simp]
 theorem IterM.Step.toPure_yield {α β : Type w} [Iterator α Id β] {it : IterM (α := α) Id β}
     {it' out h} : IterM.Step.toPure (⟨.yield it' out, h⟩ : it.Step) = .yield it'.toIter out h :=
diff --git a/src/Init/Data/Iterators/Lemmas/Combinators/FilterMap.lean b/src/Init/Data/Iterators/Lemmas/Combinators/FilterMap.lean
index 77bfc7088df6..3f9c45a20498 100644
--- a/src/Init/Data/Iterators/Lemmas/Combinators/FilterMap.lean
+++ b/src/Init/Data/Iterators/Lemmas/Combinators/FilterMap.lean
@@ -207,7 +207,6 @@ theorem Iter.step_mapM {f : β → n γ}
   | .skip it' h => rfl
   | .done h => rfl
 
-set_option backward.isDefEq.respectTransparency.types false in
 theorem Iter.step_filterMap {f : β → Option γ} :
     (it.filterMap f).step = match it.step with
       | .yield it' out h =>
@@ -216,13 +215,15 @@ theorem Iter.step_filterMap {f : β → Option γ} :
         | some out' => .yield (it'.filterMap f) out' (.yieldSome (out := out) h h')
       | .skip it' h => .skip (it'.filterMap f) (.skip h)
       | .done h => .done (.done h) := by
+  apply Subtype.ext
   simp only [filterMap_eq_toIter_filterMap_toIterM, toIterM_toIter, IterM.step_filterMap, step]
   simp only [monadLift, Id.run_bind]
   generalize it.toIterM.step.run = step
   cases step.inflate using PlausibleIterStep.casesOn
   · simp only [IterM.Step.toPure_yield, toIter_toIterM, toIterM_toIter]
     split <;> split <;> (try exfalso; simp_all; done)
-    · simp
+    · simp [PlausibleIterStep.skip, Id.run_pure, Shrink.inflate_deflate,
+        IterM.Step.val_toPure, IterStep.mapIterator_skip]
     · rename_i h₁ _ h₂
       rw [h₁] at h₂
       cases h₂
@@ -248,7 +249,6 @@ theorem Iter.val_step_filterMap {f : β → Option γ} :
   · simp
   · simp
 
-set_option backward.isDefEq.respectTransparency.types false in
 theorem Iter.step_map {f : β → γ} :
     (it.map f).step = match it.step with
       | .yield it' out h =>
@@ -257,11 +257,11 @@ theorem Iter.step_map {f : β → γ} :
         .skip (it'.map f) (.skip h)
       | .done h =>
         .done (.done h) := by
+  apply Subtype.ext
   simp only [map_eq_toIter_map_toIterM, step, toIterM_toIter, IterM.step_map, Id.run_bind]
   generalize it.toIterM.step.run = step
   cases step.inflate using PlausibleIterStep.casesOn <;> simp
 
-set_option backward.isDefEq.respectTransparency.types false in
 def Iter.step_filter {f : β → Bool} :
     (it.filter f).step = match it.step with
       | .yield it' out h =>
@@ -273,6 +273,7 @@ def Iter.step_filter {f : β → Bool} :
         .skip (it'.filter f) (.skip h)
       | .done h =>
         .done (.done h) := by
+  apply Subtype.ext
   simp only [filter_eq_toIter_filter_toIterM, step, toIterM_toIter, IterM.step_filter, Id.run_bind]
   generalize it.toIterM.step.run = step
   cases step.inflate using PlausibleIterStep.casesOn
@@ -281,7 +282,6 @@ def Iter.step_filter {f : β → Bool} :
   · simp
   · simp
 
-set_option backward.isDefEq.respectTransparency.types false in
 def Iter.val_step_filter {f : β → Bool} :
     (it.filter f).step.val = match it.step.val with
       | .yield it' out =>
diff --git a/src/Init/Data/Iterators/Lemmas/Combinators/Take.lean b/src/Init/Data/Iterators/Lemmas/Combinators/Take.lean
index 63a4f325f0e3..c1612003a7fe 100644
--- a/src/Init/Data/Iterators/Lemmas/Combinators/Take.lean
+++ b/src/Init/Data/Iterators/Lemmas/Combinators/Take.lean
@@ -102,7 +102,6 @@ theorem Iter.toList_take_zero {α β} [Iterator α Id β]
   rw [toList_eq_match_step]
   simp [step_take]
 
-set_option backward.isDefEq.respectTransparency.types false in
 theorem Iter.step_toTake {α β} [Iterator α Id β] [Finite α Id]
     {it : Iter (α := α) β} :
     it.toTake.step = (
@@ -110,6 +109,7 @@ theorem Iter.step_toTake {α β} [Iterator α Id β] [Finite α Id]
         | .yield it' out h => .yield it'.toTake out (.yield h Nat.zero_ne_one)
         | .skip it' h => .skip it'.toTake (.skip h Nat.zero_ne_one)
         | .done h => .done (.done h)) := by
+  apply Subtype.ext
   simp only [toTake_eq_toIter_toTake_toIterM, Iter.step, toIterM_toIter, IterM.step_toTake,
     Id.run_bind]
   cases it.toIterM.step.run.inflate using PlausibleIterStep.casesOn <;> simp
diff --git a/src/Init/Data/List/Basic.lean b/src/Init/Data/List/Basic.lean
index d0c94b87b42d..b2815b29a837 100644
--- a/src/Init/Data/List/Basic.lean
+++ b/src/Init/Data/List/Basic.lean
@@ -768,6 +768,7 @@ Examples:
 * `["grape"].isEmpty = false`
 * `["apple", "banana"].isEmpty = false`
 -/
+@[implicit_reducible]
 def isEmpty : List α → Bool
   | []     => true
   | _ :: _ => false
@@ -1052,11 +1053,11 @@ def dropLast {α} : List α → List α
   | [_]   => []
   | a::as => a :: dropLast as
 
-@[simp, grind =] theorem dropLast_nil : ([] : List α).dropLast = [] := rfl
-@[simp, grind =] theorem dropLast_singleton : [x].dropLast = [] := rfl
+@[simp, grind =] theorem dropLast_nil : ([] : List α).dropLast = [] := (rfl)
+@[simp, grind =] theorem dropLast_singleton : [x].dropLast = [] := (rfl)
 
 @[simp, grind =] theorem dropLast_cons_cons :
-    (x::y::zs).dropLast = x :: (y::zs).dropLast := rfl
+    (x::y::zs).dropLast = x :: (y::zs).dropLast := (rfl)
 
 @[deprecated dropLast_cons_cons (since := "2026-02-26")]
 theorem dropLast_cons₂ : (x::y::zs).dropLast = x :: (y::zs).dropLast := dropLast_cons_cons
@@ -2095,10 +2096,10 @@ def range' : (start len : Nat) → (step : Nat := 1) → List Nat
   | _, 0, _ => []
   | s, n+1, step => s :: range' (s+step) n step
 
-@[simp, grind =] theorem range'_zero : range' s 0 step = [] := rfl
-@[simp, grind =] theorem range'_one {s step : Nat} : range' s 1 step = [s] := rfl
+@[simp, grind =] theorem range'_zero : range' s 0 step = [] := (rfl)
+@[simp, grind =] theorem range'_one {s step : Nat} : range' s 1 step = [s] := (rfl)
 -- The following theorem is intentionally not a simp lemma.
-theorem range'_succ : range' s (n + 1) step = s :: range' (s + step) n step := rfl
+theorem range'_succ : range' s (n + 1) step = s :: range' (s + step) n step := (rfl)
 
 /-! ### zipIdx -/
 
diff --git a/src/Init/Data/List/TakeDrop.lean b/src/Init/Data/List/TakeDrop.lean
index 00ce45810586..2c5b8981bb3c 100644
--- a/src/Init/Data/List/TakeDrop.lean
+++ b/src/Init/Data/List/TakeDrop.lean
@@ -230,10 +230,10 @@ theorem take_left' {l₁ l₂ : List α} {i} (h : length l₁ = i) : take i (l
 theorem take_add_one {l : List α} {i : Nat} : l.take (i + 1) = l.take i ++ l[i]?.toList := by
   induction l generalizing i with
   | nil =>
-    simp only [take_nil, Option.toList, getElem?_nil, append_nil]
+    simp only [take_nil, Option.toList, append_nil]
   | cons hd tl hl =>
     cases i
-    · simp only [take, Option.toList, getElem?_cons_zero, nil_append]
+    · simp only [take, Option.toList, nil_append]
     · simp only [take, hl, getElem?_cons_succ, cons_append]
 
 @[deprecated take_add_one (since := "2025-10-26")]
diff --git a/src/Init/Data/Nat/Bitwise/Lemmas.lean b/src/Init/Data/Nat/Bitwise/Lemmas.lean
index 7b3ad59ca192..29f5054f0595 100644
--- a/src/Init/Data/Nat/Bitwise/Lemmas.lean
+++ b/src/Init/Data/Nat/Bitwise/Lemmas.lean
@@ -410,8 +410,8 @@ theorem testBit_bitwise (of_false_false : f false false = false) (x y i : Nat) :
     else if y_zero : y = 0 then
       simp [x_zero, y_zero]
       cases p : f true false <;>
-        cases xi : testBit x i <;>
-          simp [p, xi, of_false_false]
+        cases testBit x i <;>
+          simp [p, of_false_false]
     else
       simp only [x_zero, y_zero, ←Nat.two_mul]
       cases i with
diff --git a/src/Init/Data/Ord/Basic.lean b/src/Init/Data/Ord/Basic.lean
index dea4c6a5cbeb..171113afec13 100644
--- a/src/Init/Data/Ord/Basic.lean
+++ b/src/Init/Data/Ord/Basic.lean
@@ -91,7 +91,7 @@ Ordering.gt
 Ordering.lt
 ```
 -/
-@[macro_inline, expose] def «then» (a b : Ordering) : Ordering :=
+@[macro_inline, expose, implicit_reducible] def «then» (a b : Ordering) : Ordering :=
   match a with
   | .eq => b
   | a => a
diff --git a/src/Init/Data/Range/Lemmas.lean b/src/Init/Data/Range/Lemmas.lean
index 4c28b502132d..ebedf0c84d50 100644
--- a/src/Init/Data/Range/Lemmas.lean
+++ b/src/Init/Data/Range/Lemmas.lean
@@ -59,7 +59,6 @@ private theorem size_eq (r : Range) (h : i < r.stop) :
       rw [Nat.div_eq_iff] <;> omega
     omega
 
-set_option backward.isDefEq.respectTransparency.types false in
 private theorem forIn'_loop_eq_forIn'_range' [Monad m] (r : Range)
     (init : β) (f : (a : Nat) → a ∈ r → β → m (ForInStep β)) (i) (w₁) (w₂) :
     forIn'.loop r f init i w₁ w₂ =
diff --git a/src/Init/Data/Range/Polymorphic/Lemmas.lean b/src/Init/Data/Range/Polymorphic/Lemmas.lean
index 2862ec59f6e4..f30fb29b9607 100644
--- a/src/Init/Data/Range/Polymorphic/Lemmas.lean
+++ b/src/Init/Data/Range/Polymorphic/Lemmas.lean
@@ -872,7 +872,6 @@ public theorem toArray_eq_if_roo [UpwardEnumerable α] [LT α] [DecidableLT α]
         #[] := by
   rw [Internal.toArray_eq_toArray_iter, Rxo.Iterator.toArray_eq_match]; rfl
 
-set_option backward.isDefEq.respectTransparency.types false in
 public theorem toList_eq_if_rco [UpwardEnumerable α] [LT α] [DecidableLT α]
     [LawfulUpwardEnumerable α] [Rxo.IsAlwaysFinite α] [LawfulUpwardEnumerableLT α] :
     r.toList = if r.lower < r.upper then
@@ -882,7 +881,7 @@ public theorem toList_eq_if_rco [UpwardEnumerable α] [LT α] [DecidableLT α]
       else
         [] := by
   rw [Internal.toList_eq_toList_iter, Rxo.Iterator.toList_eq_match]
-  simp only [Internal.iter]
+  simp -implicitDefEqProofs only [Internal.iter.eq_1]
   split
   · split
     · simp [Rxo.Iterator.toList_eq_match, *]
@@ -890,7 +889,6 @@ public theorem toList_eq_if_rco [UpwardEnumerable α] [LT α] [DecidableLT α]
       rfl
   · rfl
 
-set_option backward.isDefEq.respectTransparency.types false in
 public theorem toArray_eq_if_rco [UpwardEnumerable α] [LT α] [DecidableLT α]
     [LawfulUpwardEnumerable α] [Rxo.IsAlwaysFinite α] [LawfulUpwardEnumerableLT α] :
     r.toArray = if r.lower < r.upper then
@@ -900,7 +898,7 @@ public theorem toArray_eq_if_rco [UpwardEnumerable α] [LT α] [DecidableLT α]
       else
         #[] := by
   rw [Internal.toArray_eq_toArray_iter, Rxo.Iterator.toArray_eq_match]
-  simp only [Internal.iter]
+  simp -implicitDefEqProofs only [Internal.iter.eq_1]
   split
   · split
     · simp [Rxo.Iterator.toArray_eq_match, *]
@@ -1319,7 +1317,6 @@ namespace Roc
 
 variable {r : Roc α}
 
-set_option backward.isDefEq.respectTransparency.types false in
 public theorem toList_eq_match [LE α] [DecidableLE α] [UpwardEnumerable α]
     [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] :
     r.toList = match UpwardEnumerable.succ? r.lower with
@@ -1330,9 +1327,8 @@ public theorem toList_eq_match [LE α] [DecidableLE α] [UpwardEnumerable α]
         else
           [] := by
   rw [Internal.toList_eq_toList_iter, Rxc.Iterator.toList_eq_match (it := Internal.iter r)]
-  simp [Internal.iter, Internal.toList_eq_toList_iter]
+  simp -implicitDefEqProofs [Internal.iter.eq_1, Internal.toList_eq_toList_iter]
 
-set_option backward.isDefEq.respectTransparency.types false in
 public theorem toArray_eq_match [LE α] [DecidableLE α] [UpwardEnumerable α]
     [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] :
     r.toArray = match UpwardEnumerable.succ? r.lower with
@@ -1343,7 +1339,7 @@ public theorem toArray_eq_match [LE α] [DecidableLE α] [UpwardEnumerable α]
         else
           #[] := by
   rw [Internal.toArray_eq_toArray_iter, Rxc.Iterator.toArray_eq_match (it := Internal.iter r)]
-  simp [Internal.iter, Internal.toArray_eq_toArray_iter]
+  simp -implicitDefEqProofs [Internal.iter.eq_1, Internal.toArray_eq_toArray_iter]
 
 @[cbv_eval]
 public theorem toList_eq_match_rcc [LE α] [DecidableLE α] [UpwardEnumerable α]
@@ -1589,7 +1585,6 @@ public theorem toArray_eq_match [LE α] [LT α] [DecidableLT α] [UpwardEnumerab
           #[] := by
   rw [Internal.toArray_eq_toArray_iter, Rxo.Iterator.toArray_eq_match]; rfl
 
-set_option backward.isDefEq.respectTransparency.types false in
 @[cbv_eval]
 public theorem toList_eq_match_rco [UpwardEnumerable α] [LT α] [DecidableLT α]
     [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] :
@@ -1597,19 +1592,18 @@ public theorem toList_eq_match_rco [UpwardEnumerable α] [LT α] [DecidableLT α
       | none => []
       | some next => (next...r.upper).toList := by
   rw [Internal.toList_eq_toList_iter, Rxo.Iterator.toList_eq_match]
-  simp only [Internal.iter]
+  simp -implicitDefEqProofs only [Internal.iter.eq_1]
   split
   · rfl
   · simp [Rco.toList_eq_if_roo, Roo.toList, Internal.iter]
 
-set_option backward.isDefEq.respectTransparency.types false in
 public theorem toArray_eq_match_rco [UpwardEnumerable α] [LT α] [DecidableLT α]
     [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] :
     r.toArray = match UpwardEnumerable.succ? r.lower with
       | none => #[]
       | some next => (next...r.upper).toArray := by
   rw [Internal.toArray_eq_toArray_iter, Rxo.Iterator.toArray_eq_match]
-  simp only [Internal.iter]
+  simp -implicitDefEqProofs only [Internal.iter.eq_1]
   split
   · rfl
   · simp [Rco.toArray_eq_if_roo, Roo.toArray, Internal.iter]
@@ -2061,7 +2055,6 @@ public theorem toList_toArray [Least? α] [LE α] [DecidableLE α] [UpwardEnumer
     r.toArray.toList = r.toList := by
   simp [Internal.toList_eq_toList_iter, Internal.toArray_eq_toArray_iter]
 
-set_option backward.isDefEq.respectTransparency.types false in
 @[cbv_eval]
 public theorem toList_eq_match_rcc [LE α] [DecidableLE α] [Least? α] [UpwardEnumerable α]
     [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α]
@@ -2072,7 +2065,7 @@ public theorem toList_eq_match_rcc [LE α] [DecidableLE α] [Least? α] [UpwardE
   simp only [Internal.toList_eq_toList_iter, Rcc.Internal.toList_eq_toList_iter,
     Rxc.Iterator.toList_eq_match (it := Internal.iter r),
     Rxc.Iterator.toList_eq_match (it := Rcc.Internal.iter _)]
-  simp [Internal.iter, Rcc.Internal.iter]
+  simp -implicitDefEqProofs [Internal.iter.eq_1, Rcc.Internal.iter.eq_1]
 
 public theorem toList_eq_toList_rcc [LE α] [DecidableLE α] [Least? α] [UpwardEnumerable α]
     [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α] [LawfulUpwardEnumerableLeast? α]
@@ -2365,7 +2358,6 @@ public theorem toList_toArray [Least? α] [LT α] [DecidableLT α] [UpwardEnumer
     r.toArray.toList = r.toList := by
   simp [Internal.toList_eq_toList_iter, Internal.toArray_eq_toArray_iter]
 
-set_option backward.isDefEq.respectTransparency.types false in
 @[cbv_eval]
 public theorem toList_eq_match_rco [LT α] [DecidableLT α] [Least? α] [UpwardEnumerable α]
     [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α]
@@ -2376,9 +2368,8 @@ public theorem toList_eq_match_rco [LT α] [DecidableLT α] [Least? α] [UpwardE
   simp only [Internal.toList_eq_toList_iter, Rco.Internal.toList_eq_toList_iter,
     Rxo.Iterator.toList_eq_match (it := Internal.iter r),
     Rxo.Iterator.toList_eq_match (it := Rco.Internal.iter _)]
-  simp [Internal.iter, Rco.Internal.iter]
+  simp -implicitDefEqProofs [Internal.iter.eq_1, Rco.Internal.iter.eq_1]
 
-set_option backward.isDefEq.respectTransparency.types false in
 public theorem toArray_eq_match_rco [LT α] [DecidableLT α] [Least? α] [UpwardEnumerable α]
     [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α]
     [Rxo.IsAlwaysFinite α] :
@@ -2388,7 +2379,7 @@ public theorem toArray_eq_match_rco [LT α] [DecidableLT α] [Least? α] [Upward
   simp only [Internal.toArray_eq_toArray_iter, Rco.Internal.toArray_eq_toArray_iter,
     Rxo.Iterator.toArray_eq_match (it := Internal.iter r),
     Rxo.Iterator.toArray_eq_match (it := Rco.Internal.iter _)]
-  simp [Internal.iter, Rco.Internal.iter]
+  simp -implicitDefEqProofs [Internal.iter.eq_1, Rco.Internal.iter.eq_1]
 
 public theorem toList_eq_toList_rco [LT α] [DecidableLT α] [Least? α] [UpwardEnumerable α]
     [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α] [LawfulUpwardEnumerableLeast? α]
diff --git a/src/Init/Data/Range/Polymorphic/RangeIterator.lean b/src/Init/Data/Range/Polymorphic/RangeIterator.lean
index 18f595db94ea..765bc11447bb 100644
--- a/src/Init/Data/Range/Polymorphic/RangeIterator.lean
+++ b/src/Init/Data/Range/Polymorphic/RangeIterator.lean
@@ -80,7 +80,6 @@ def Iterator.step [UpwardEnumerable α] [LE α] [DecidableLE α]
     else
       .done
 
-set_option backward.isDefEq.respectTransparency.types false in
 theorem Iterator.step_eq_monadicStep [UpwardEnumerable α] [LE α] [DecidableLE α]
     {it : Iter (α := Rxc.Iterator α) α} :
     Iterator.step it = (Iterator.Monadic.step it.toIterM).mapIterator IterM.toIter := by
@@ -663,7 +662,6 @@ def Iterator.step [UpwardEnumerable α] [LT α] [DecidableLT α]
     else
       .done
 
-set_option backward.isDefEq.respectTransparency.types false in
 theorem Iterator.step_eq_monadicStep [UpwardEnumerable α] [LT α] [DecidableLT α]
     {it : Iter (α := Rxo.Iterator α) α} :
     Iterator.step it = (Iterator.Monadic.step it.toIterM).mapIterator IterM.toIter := by
diff --git a/src/Init/Data/Rat/Lemmas.lean b/src/Init/Data/Rat/Lemmas.lean
index 90eb3e09a3fa..fbe105fc6b0d 100644
--- a/src/Init/Data/Rat/Lemmas.lean
+++ b/src/Init/Data/Rat/Lemmas.lean
@@ -186,11 +186,11 @@ abbrev divInt_self := @num_divInt_den
 theorem neg_divInt_neg (num den) : -num /. -den = num /. den := by
   match den with
   | Nat.succ n =>
-    simp only [divInt, Int.neg_ofNat_succ]
+    simp only [divInt]
     simp [normalize_eq_mkRat, Int.neg_neg]
   | 0 => rfl
   | Int.negSucc n =>
-    simp only [divInt, Int.neg_negSucc]
+    simp only [divInt]
     simp [normalize_eq_mkRat]
 
 theorem divInt_neg' (num den) : num /. -den = -num /. den := by rw [← neg_divInt_neg, Int.neg_neg]
@@ -1242,10 +1242,9 @@ theorem lt_floor {x : Rat} :
 # ceil
 -/
 
-set_option backward.isDefEq.respectTransparency.types false in
 theorem ceil_eq_neg_floor_neg (a : Rat) : a.ceil = -((-a).floor) := by
   rw [Rat.ceil, Rat.floor]
-  simp only [neg_den, neg_num]
+  simp -implicitDefEqProofs only [neg_den, neg_num]
   split
   · simp
   · rw [Int.neg_ediv, if_neg, Int.sign_eq_one_of_pos, Int.neg_sub, Int.sub_neg, Int.add_comm]
diff --git a/src/Init/Data/SInt/Basic.lean b/src/Init/Data/SInt/Basic.lean
index 15011454bdab..f6a521f2e7e0 100644
--- a/src/Init/Data/SInt/Basic.lean
+++ b/src/Init/Data/SInt/Basic.lean
@@ -90,7 +90,7 @@ abbrev Int8.size : Nat := 256
 /--
 Obtain the `BitVec` that contains the 2's complement representation of the `Int8`.
 -/
-@[inline] def Int8.toBitVec (x : Int8) : BitVec 8 := x.toUInt8.toBitVec --
+@[inline, implicit_reducible] def Int8.toBitVec (x : Int8) : BitVec 8 := x.toUInt8.toBitVec --
 
 theorem Int8.toBitVec.inj : {x y : Int8} → x.toBitVec = y.toBitVec → x = y
   | ⟨⟨_⟩⟩, ⟨⟨_⟩⟩, rfl => rfl
@@ -122,7 +122,7 @@ Examples:
  * `Int8.ofNat 128 = -128`
  * `Int8.ofNat 255 = -1`
 -/
-@[extern "lean_int8_of_nat"]
+@[extern "lean_int8_of_nat", implicit_reducible]
 def Int8.ofNat (n : @& Nat) : Int8 := ⟨⟨BitVec.ofNat 8 n⟩⟩
 /--
 Converts an arbitrary-precision integer to an 8-bit integer, wrapping on overflow or underflow.
@@ -151,7 +151,7 @@ Converts an 8-bit signed integer to an arbitrary-precision integer that denotes
 
 This function is overridden at runtime with an efficient implementation.
 -/
-@[extern "lean_int8_to_int", tagged_return]
+@[extern "lean_int8_to_int", tagged_return, implicit_reducible]
 def Int8.toInt (i : Int8) : Int := i.toBitVec.toInt
 /--
 Converts an 8-bit signed integer to a natural number, mapping all negative numbers to `0`.
@@ -167,7 +167,7 @@ Negates 8-bit signed integers. Usually accessed via the `-` prefix operator.
 
 This function is overridden at runtime with an efficient implementation.
 -/
-@[extern "lean_int8_neg"]
+@[extern "lean_int8_neg", implicit_reducible]
 def Int8.neg (i : Int8) : Int8 := ⟨⟨-i.toBitVec⟩⟩
 
 instance : ToString Int8 where
@@ -441,7 +441,7 @@ abbrev Int16.size : Nat := 65536
 /--
 Obtain the `BitVec` that contains the 2's complement representation of the `Int16`.
 -/
-@[inline] def Int16.toBitVec (x : Int16) : BitVec 16 := x.toUInt16.toBitVec
+@[inline, implicit_reducible] def Int16.toBitVec (x : Int16) : BitVec 16 := x.toUInt16.toBitVec
 
 theorem Int16.toBitVec.inj : {x y : Int16} → x.toBitVec = y.toBitVec → x = y
   | ⟨⟨_⟩⟩, ⟨⟨_⟩⟩, rfl => rfl
@@ -474,7 +474,7 @@ Examples:
  * `Int16.ofNat 32768 = -32768`
  * `Int16.ofNat 32770 = -32766`
 -/
-@[extern "lean_int16_of_nat"]
+@[extern "lean_int16_of_nat", implicit_reducible]
 def Int16.ofNat (n : @& Nat) : Int16 := ⟨⟨BitVec.ofNat 16 n⟩⟩
 /--
 Converts an arbitrary-precision integer to a 16-bit integer, wrapping on overflow or underflow.
@@ -504,7 +504,7 @@ Converts a 16-bit signed integer to an arbitrary-precision integer that denotes
 
 This function is overridden at runtime with an efficient implementation.
 -/
-@[extern "lean_int16_to_int", tagged_return]
+@[extern "lean_int16_to_int", tagged_return, implicit_reducible]
 def Int16.toInt (i : Int16) : Int := i.toBitVec.toInt
 /--
 Converts a 16-bit signed integer to a natural number, mapping all negative numbers to `0`.
@@ -535,7 +535,7 @@ Negates 16-bit signed integers. Usually accessed via the `-` prefix operator.
 
 This function is overridden at runtime with an efficient implementation.
 -/
-@[extern "lean_int16_neg"]
+@[extern "lean_int16_neg", implicit_reducible]
 def Int16.neg (i : Int16) : Int16 := ⟨⟨-i.toBitVec⟩⟩
 
 instance : ToString Int16 where
@@ -810,7 +810,7 @@ abbrev Int32.size : Nat := 4294967296
 /--
 Obtain the `BitVec` that contains the 2's complement representation of the `Int32`.
 -/
-@[inline] def Int32.toBitVec (x : Int32) : BitVec 32 := x.toUInt32.toBitVec
+@[inline, implicit_reducible] def Int32.toBitVec (x : Int32) : BitVec 32 := x.toUInt32.toBitVec
 
 theorem Int32.toBitVec.inj : {x y : Int32} → x.toBitVec = y.toBitVec → x = y
   | ⟨⟨_⟩⟩, ⟨⟨_⟩⟩, rfl => rfl
@@ -844,7 +844,7 @@ Examples:
  * `Int32.ofNat 2_147_483_647 = 2_147_483_647`
  * `Int32.ofNat 2_147_483_648 = -2_147_483_648`
 -/
-@[extern "lean_int32_of_nat"]
+@[extern "lean_int32_of_nat", implicit_reducible]
 def Int32.ofNat (n : @& Nat) : Int32 := ⟨⟨BitVec.ofNat 32 n⟩⟩
 /--
 Converts an arbitrary-precision integer to a 32-bit integer, wrapping on overflow or underflow.
@@ -874,7 +874,7 @@ Converts a 32-bit signed integer to an arbitrary-precision integer that denotes
 
 This function is overridden at runtime with an efficient implementation.
 -/
-@[extern "lean_int32_to_int"]
+@[extern "lean_int32_to_int", implicit_reducible]
 def Int32.toInt (i : Int32) : Int := i.toBitVec.toInt
 /--
 Converts a 32-bit signed integer to a natural number, mapping all negative numbers to `0`.
@@ -920,7 +920,7 @@ Negates 32-bit signed integers. Usually accessed via the `-` prefix operator.
 
 This function is overridden at runtime with an efficient implementation.
 -/
-@[extern "lean_int32_neg"]
+@[extern "lean_int32_neg", implicit_reducible]
 def Int32.neg (i : Int32) : Int32 := ⟨⟨-i.toBitVec⟩⟩
 
 instance : ToString Int32 where
@@ -1195,7 +1195,7 @@ abbrev Int64.size : Nat := 18446744073709551616
 /--
 Obtain the `BitVec` that contains the 2's complement representation of the `Int64`.
 -/
-@[inline] def Int64.toBitVec (x : Int64) : BitVec 64 := x.toUInt64.toBitVec
+@[inline, implicit_reducible] def Int64.toBitVec (x : Int64) : BitVec 64 := x.toUInt64.toBitVec
 
 theorem Int64.toBitVec.inj : {x y : Int64} → x.toBitVec = y.toBitVec → x = y
   | ⟨⟨_⟩⟩, ⟨⟨_⟩⟩, rfl => rfl
@@ -1231,7 +1231,7 @@ Examples:
  * `Int64.ofNat 9_223_372_036_854_775_808 = -9_223_372_036_854_775_808`
  * `Int64.ofNat 18_446_744_073_709_551_618 = 0`
 -/
-@[extern "lean_int64_of_nat"]
+@[extern "lean_int64_of_nat", implicit_reducible]
 def Int64.ofNat (n : @& Nat) : Int64 := ⟨⟨BitVec.ofNat 64 n⟩⟩
 /--
 Converts an arbitrary-precision integer to a 64-bit integer, wrapping on overflow or underflow.
@@ -1264,7 +1264,7 @@ Converts a 64-bit signed integer to an arbitrary-precision integer that denotes
 
 This function is overridden at runtime with an efficient implementation.
 -/
-@[extern "lean_int64_to_int_sint"]
+@[extern "lean_int64_to_int_sint", implicit_reducible]
 def Int64.toInt (i : Int64) : Int := i.toBitVec.toInt
 /--
 Converts a 64-bit signed integer to a natural number, mapping all negative numbers to `0`.
@@ -1325,7 +1325,7 @@ Negates 64-bit signed integers. Usually accessed via the `-` prefix operator.
 
 This function is overridden at runtime with an efficient implementation.
 -/
-@[extern "lean_int64_neg"]
+@[extern "lean_int64_neg", implicit_reducible]
 def Int64.neg (i : Int64) : Int64 := ⟨⟨-i.toBitVec⟩⟩
 
 instance : ToString Int64 where
@@ -1599,7 +1599,7 @@ abbrev ISize.size : Nat := 2^System.Platform.numBits
 /--
 Obtain the `BitVec` that contains the 2's complement representation of the `ISize`.
 -/
-@[inline] def ISize.toBitVec (x : ISize) : BitVec System.Platform.numBits := x.toUSize.toBitVec
+@[inline, implicit_reducible] def ISize.toBitVec (x : ISize) : BitVec System.Platform.numBits := x.toUSize.toBitVec
 
 theorem ISize.toBitVec.inj : {x y : ISize} → x.toBitVec = y.toBitVec → x = y
   | ⟨⟨_⟩⟩, ⟨⟨_⟩⟩, rfl => rfl
@@ -1621,7 +1621,7 @@ overflow.
 
 This function is overridden at runtime with an efficient implementation.
 -/
-@[extern "lean_isize_of_nat"]
+@[extern "lean_isize_of_nat", implicit_reducible]
 def ISize.ofNat (n : @& Nat) : ISize := ⟨⟨BitVec.ofNat System.Platform.numBits n⟩⟩
 @[inherit_doc ISize.ofInt]
 abbrev Int.toISize := ISize.ofInt
@@ -1631,7 +1631,7 @@ Converts a word-sized signed integer to an arbitrary-precision integer that deno
 
 This function is overridden at runtime with an efficient implementation.
 -/
-@[extern "lean_isize_to_int"]
+@[extern "lean_isize_to_int", implicit_reducible]
 def ISize.toInt (i : ISize) : Int := i.toBitVec.toInt
 /--
 Converts a word-sized signed integer to a natural number, mapping all negative numbers to `0`.
@@ -1712,7 +1712,7 @@ Negates word-sized signed integers. Usually accessed via the `-` prefix operator
 
 This function is overridden at runtime with an efficient implementation.
 -/
-@[extern "lean_isize_neg"]
+@[extern "lean_isize_neg", implicit_reducible]
 protected def ISize.neg (i : ISize) : ISize := ⟨⟨-i.toBitVec⟩⟩
 
 instance : ToString ISize where
diff --git a/src/Init/Data/SInt/Lemmas.lean b/src/Init/Data/SInt/Lemmas.lean
index 8ed853f79fc4..0dec088fe8ed 100644
--- a/src/Init/Data/SInt/Lemmas.lean
+++ b/src/Init/Data/SInt/Lemmas.lean
@@ -1162,15 +1162,16 @@ theorem ISize.toInt8_ofIntLE {n} (h₁ h₂) : (ISize.ofIntLE n h₁ h₂).toInt
 @[simp] theorem Int64.toInt8_ofNat {n} : toInt8 (no_index (OfNat.ofNat n)) = OfNat.ofNat n := toInt8_ofNat'
 @[simp] theorem ISize.toInt8_ofNat {n} : toInt8 (no_index (OfNat.ofNat n)) = OfNat.ofNat n := toInt8_ofNat'
 
-set_option backward.isDefEq.respectTransparency.types false in
+set_option allowUnsafeReducibility true
+attribute [implicit_reducible] dite ite -- TODO: move as soon as `inferInstanceAs` has been fixed
+
 theorem Int16.toInt8_ofIntTruncate {n : Int} (h₁ : -2 ^ 15 ≤ n) (h₂ : n < 2 ^ 15) :
     (Int16.ofIntTruncate n).toInt8 = Int8.ofInt n := by
-  rw [← ofIntLE_eq_ofIntTruncate (h₁ := h₁) (h₂ := Int.le_of_lt_add_one h₂), toInt8_ofIntLE]
-set_option backward.isDefEq.respectTransparency.types false in
+  rw [← ofIntLE_eq_ofIntTruncate (h₁ := h₁) (h₂ := Int.le_of_lt_add_one h₂)] --, toInt8_ofIntLE]
+  rw [toInt8_ofIntLE]
 theorem Int32.toInt8_ofIntTruncate {n : Int} (h₁ : -2 ^ 31 ≤ n) (h₂ : n < 2 ^ 31) :
     (Int32.ofIntTruncate n).toInt8 = Int8.ofInt n := by
   rw [← ofIntLE_eq_ofIntTruncate (h₁ := h₁) (h₂ := Int.le_of_lt_add_one h₂), toInt8_ofIntLE]
-set_option backward.isDefEq.respectTransparency.types false in
 theorem Int64.toInt8_ofIntTruncate {n : Int} (h₁ : -2 ^ 63 ≤ n) (h₂ : n < 2 ^ 63) :
     (Int64.ofIntTruncate n).toInt8 = Int8.ofInt n := by
   rw [← ofIntLE_eq_ofIntTruncate (h₁ := h₁) (h₂ := Int.le_of_lt_add_one h₂), toInt8_ofIntLE]
@@ -1212,11 +1213,9 @@ theorem ISize.toInt16_ofIntLE {n} (h₁ h₂) : (ISize.ofIntLE n h₁ h₂).toIn
 @[simp] theorem Int64.toInt16_ofNat {n} : toInt16 (no_index (OfNat.ofNat n)) = OfNat.ofNat n := toInt16_ofNat'
 @[simp] theorem ISize.toInt16_ofNat {n} : toInt16 (no_index (OfNat.ofNat n)) = OfNat.ofNat n := toInt16_ofNat'
 
-set_option backward.isDefEq.respectTransparency.types false in
 theorem Int32.toInt16_ofIntTruncate {n : Int} (h₁ : -2 ^ 31 ≤ n) (h₂ : n < 2 ^ 31) :
     (Int32.ofIntTruncate n).toInt16 = Int16.ofInt n := by
   rw [← ofIntLE_eq_ofIntTruncate (h₁ := h₁) (h₂ := Int.le_of_lt_add_one h₂), toInt16_ofIntLE]
-set_option backward.isDefEq.respectTransparency.types false in
 theorem Int64.toInt16_ofIntTruncate {n : Int} (h₁ : -2 ^ 63 ≤ n) (h₂ : n < 2 ^ 63) :
     (Int64.ofIntTruncate n).toInt16 = Int16.ofInt n := by
   rw [← ofIntLE_eq_ofIntTruncate (h₁ := h₁) (h₂ := Int.le_of_lt_add_one h₂), toInt16_ofIntLE]
@@ -1251,7 +1250,6 @@ theorem ISize.toInt32_ofIntLE {n} (h₁ h₂) : (ISize.ofIntLE n h₁ h₂).toIn
 @[simp] theorem Int64.toInt32_ofNat {n} : toInt32 (no_index (OfNat.ofNat n)) = OfNat.ofNat n := toInt32_ofNat'
 @[simp] theorem ISize.toInt32_ofNat {n} : toInt32 (no_index (OfNat.ofNat n)) = OfNat.ofNat n := toInt32_ofNat'
 
-set_option backward.isDefEq.respectTransparency.types false in
 theorem Int64.toInt32_ofIntTruncate {n : Int} (h₁ : -2 ^ 63 ≤ n) (h₂ : n < 2 ^ 63) :
     (Int64.ofIntTruncate n).toInt32 = Int32.ofInt n := by
   rw [← ofIntLE_eq_ofIntTruncate (h₁ := h₁) (h₂ := Int.le_of_lt_add_one h₂), toInt32_ofIntLE]
@@ -1275,7 +1273,6 @@ theorem Int64.toISize_ofIntLE {n} (h₁ h₂) : (Int64.ofIntLE n h₁ h₂).toIS
 
 @[simp] theorem Int64.toISize_ofNat {n} : toISize (no_index (OfNat.ofNat n)) = OfNat.ofNat n := toISize_ofNat'
 
-set_option backward.isDefEq.respectTransparency.types false in
 theorem Int64.toISize_ofIntTruncate {n : Int} (h₁ : -2 ^ 63 ≤ n) (h₂ : n < 2 ^ 63) :
     (Int64.ofIntTruncate n).toISize = ISize.ofInt n := by
   rw [← ofIntLE_eq_ofIntTruncate (h₁ := h₁) (h₂ := Int.le_of_lt_add_one h₂), toISize_ofIntLE]
diff --git a/src/Init/Data/Slice/Array/Lemmas.lean b/src/Init/Data/Slice/Array/Lemmas.lean
index 0aee046bd448..b409c045a017 100644
--- a/src/Init/Data/Slice/Array/Lemmas.lean
+++ b/src/Init/Data/Slice/Array/Lemmas.lean
@@ -44,16 +44,8 @@ theorem step_eq {it : Iter (α := SubarrayIterator α) α} :
   simp only [Iter.step, IterM.Step.toPure, Iter.toIter_toIterM, IterStep.mapIterator, IterM.step,
     Iterator.step, SubarrayIterator.step, Id.run_pure, Shrink.inflate_deflate]
   by_cases h : it.internalState.xs.start < it.internalState.xs.stop
-  · simp only [h, ↓reduceDIte]
-    split
-    · rfl
-    · rename_i h'
-      exact h'.elim h
-  · simp only [h, ↓reduceDIte]
-    split
-    · rename_i h'
-      exact h.elim h'
-    · rfl
+  · simp [h, ↓reduceDIte]
+  · simp [h, ↓reduceDIte]
 
 theorem val_step_eq {it : Iter (α := SubarrayIterator α) α} :
     it.step.val = if h : it.1.xs.start < it.1.xs.stop then
diff --git a/src/Init/Data/String/Basic.lean b/src/Init/Data/String/Basic.lean
index f0089b5f37eb..463edeace6a6 100644
--- a/src/Init/Data/String/Basic.lean
+++ b/src/Init/Data/String/Basic.lean
@@ -513,7 +513,6 @@ theorem Pos.Raw.IsValid.isValidUTF8_extract_utf8ByteSize {s : String} {p : Pos.R
     simpa [utf8ByteSize, Pos.Raw.le_iff] using h.le_rawEndPos
   · simp [utf8ByteSize]
 
-set_option backward.isDefEq.respectTransparency.types false in
 theorem Pos.Raw.isValid_iff_exists_append {s : String} {p : Pos.Raw} :
     p.IsValid s ↔ ∃ s₁ s₂ : String, s = s₁ ++ s₂ ∧ p = s₁.rawEndPos := by
   refine ⟨fun h => ⟨⟨_, h.isValidUTF8_extract_zero⟩, ⟨_, h.isValidUTF8_extract_utf8ByteSize⟩, ?_, ?_⟩, ?_⟩
@@ -648,7 +647,6 @@ where
       rw [List.reverse_cons]
       exact append_singleton _ _ ih
 
-set_option backward.isDefEq.respectTransparency.types false in
 theorem Pos.Raw.isValid_iff_isUTF8FirstByte {s : String} {p : Pos.Raw} :
     p.IsValid s ↔ p = s.rawEndPos ∨ ∃ (h : p < s.rawEndPos), (s.getUTF8Byte p h).IsUTF8FirstByte := by
   induction s using push_induction with
@@ -1735,7 +1733,7 @@ def pos! (s : String) (off : Pos.Raw) : s.Pos :=
   Pos.ofToSlice (s.toSlice.pos! off)
 
 @[simp]
-theorem offset_pos {s : String} {off : Pos.Raw} {h} : (s.pos off h).offset = off := rfl
+theorem offset_pos {s : String} {off : Pos.Raw} {h} : (s.pos off h).offset = off := (rfl)
 
 /-- Constructs a valid position on `t` from a valid position on `s` and a proof that
 `s.copy = t.copy`. -/
@@ -2001,7 +1999,7 @@ theorem Pos.get_toSlice {s : String} {p : s.Pos} {h} :
   rfl
 
 theorem Pos.get_eq_get_toSlice {s : String} {p : s.Pos} {h}  :
-    p.get h = p.toSlice.get (ne_of_apply_ne Pos.ofToSlice (by simp [h])) := rfl
+    p.get h = p.toSlice.get (ne_of_apply_ne Pos.ofToSlice (by simp [h])) := (rfl)
 
 @[simp]
 theorem Pos.offset_next {s : String} (p : s.Pos) (h : p ≠ s.endPos) :
@@ -2522,7 +2520,6 @@ theorem Pos.Raw.isValidForSlice_slice {s : Slice} {p₀ p₁ : s.Pos} {h} (pos :
     omega
   · simpa [offsetBy_assoc] using h₂.isValid_offsetBy
 
-set_option backward.isDefEq.respectTransparency.types false in
 theorem Pos.Raw.isValidForSlice_stringSlice {s : String} {p₀ p₁ : s.Pos} {h} (pos : Pos.Raw) :
     pos.IsValidForSlice (s.slice p₀ p₁ h) ↔
       pos.offsetBy p₀.offset ≤ p₁.offset ∧ (pos.offsetBy p₀.offset).IsValid s := by
diff --git a/src/Init/Data/String/Defs.lean b/src/Init/Data/String/Defs.lean
index 59331178afcf..d571e518c741 100644
--- a/src/Init/Data/String/Defs.lean
+++ b/src/Init/Data/String/Defs.lean
@@ -471,7 +471,7 @@ theorem Pos.Raw.byteIdx_sub_slice {p : Pos.Raw} {s : Slice} :
     (p - s).byteIdx = p.byteIdx - s.utf8ByteSize := rfl
 
 /-- The end position of a slice, as a `Pos.Raw`. -/
-@[expose, inline]
+@[expose, inline, implicit_reducible]
 def Slice.rawEndPos (s : Slice) : Pos.Raw where
   byteIdx := s.utf8ByteSize
 
diff --git a/src/Init/Data/String/Lemmas/Iter.lean b/src/Init/Data/String/Lemmas/Iter.lean
index 62f4253a2ebd..9fc0d69ec89f 100644
--- a/src/Init/Data/String/Lemmas/Iter.lean
+++ b/src/Init/Data/String/Lemmas/Iter.lean
@@ -43,7 +43,7 @@ public theorem intercalateString_eq {α β : Type} [Std.Iterator α Id β] [Std.
     match m with
     | [] => simp
     | x::xs =>
-      simp only [reduceCtorEq, ↓reduceIte, List.cons_append, Option.some.injEq]
+      simp only [List.cons_append, Option.some.injEq]
       rw [← List.cons_append, String.intercalate_append_of_ne_nil (by simp) (by simp),
         String.intercalate_singleton]
 
diff --git a/src/Init/Data/String/Lemmas/Iterate.lean b/src/Init/Data/String/Lemmas/Iterate.lean
index 4f417f8b208d..32bd888af7d5 100644
--- a/src/Init/Data/String/Lemmas/Iterate.lean
+++ b/src/Init/Data/String/Lemmas/Iterate.lean
@@ -76,7 +76,6 @@ theorem Model.map_get_positionsFrom_startPos {s : Slice} :
     (Model.positionsFrom s.startPos).map (fun p => p.1.get p.2) = s.copy.toList :=
   Model.map_get_positionsFrom_of_splits (splits_startPos s)
 
-set_option backward.isDefEq.respectTransparency.types false in
 @[cbv_eval, simp]
 theorem toList_positionsFrom {s : Slice} {p : s.Pos} :
     (s.positionsFrom p).toList = Model.positionsFrom p := by
@@ -163,7 +162,6 @@ theorem Model.map_get_revPositionsFrom_endPos {s : Slice} :
     (Model.revPositionsFrom s.endPos).map (fun p => p.1.get p.2) = s.copy.toList.reverse :=
   Model.map_get_revPositionsFrom_of_splits (splits_endPos s)
 
-set_option backward.isDefEq.respectTransparency.types false in
 @[simp]
 theorem toList_revPositionsFrom {s : Slice} {p : s.Pos} :
     (s.revPositionsFrom p).toList = Model.revPositionsFrom p := by
diff --git a/src/Init/Data/String/Lemmas/Pattern/Basic.lean b/src/Init/Data/String/Lemmas/Pattern/Basic.lean
index dff493ee4cd8..4fd66b3892cb 100644
--- a/src/Init/Data/String/Lemmas/Pattern/Basic.lean
+++ b/src/Init/Data/String/Lemmas/Pattern/Basic.lean
@@ -913,7 +913,6 @@ class LawfulToForwardSearcherModel {ρ : Type} (pat : ρ) [PatternModel pat] {σ
     [∀ s, Std.Iterators.Finite (σ s) Id] : Prop where
   isValidSearchFrom_toList (s) : IsValidSearchFrom pat s.startPos (ToForwardSearcher.toSearcher pat s).toList
 
-set_option backward.isDefEq.respectTransparency.types false in
 theorem LawfulToForwardSearcherModel.defaultImplementation {pat : ρ} [ForwardPattern pat] [StrictForwardPattern pat]
     [PatternModel pat] [LawfulForwardPatternModel pat] :
     letI : ToForwardSearcher pat (ToForwardSearcher.DefaultForwardSearcher pat) := .defaultImplementation
@@ -926,7 +925,7 @@ theorem LawfulToForwardSearcherModel.defaultImplementation {pat : ρ} [ForwardPa
   intro pos
   induction pos using WellFounded.induction Slice.Pos.wellFounded_gt with | h pos ih
   rw [Std.Iter.toList_eq_match_step, Std.Iter.step_eq]
-  simp only [Std.Iter.toIterM, ne_eq]
+  simp only [Std.Iter.toIterM_mk, Std.IterM.internalState_mk, ne_eq]
   by_cases h : pos = s.endPos
   · simpa [h] using IsValidSearchFrom.endPos
   · simp only [h, ↓reduceDIte]
@@ -1025,7 +1024,6 @@ class LawfulToBackwardSearcherModel {ρ : Type} (pat : ρ) [PatternModel pat] {
     [∀ s, Std.Iterators.Finite (σ s) Id] : Prop where
   isValidRevSearchFrom_toList (s) : IsValidRevSearchFrom pat s.endPos (ToBackwardSearcher.toSearcher pat s).toList
 
-set_option backward.isDefEq.respectTransparency.types false in
 theorem LawfulToBackwardSearcherModel.defaultImplementation {pat : ρ} [BackwardPattern pat] [StrictBackwardPattern pat]
     [PatternModel pat] [LawfulBackwardPatternModel pat] :
     letI : ToBackwardSearcher pat (ToBackwardSearcher.DefaultBackwardSearcher pat) := .defaultImplementation
@@ -1038,7 +1036,7 @@ theorem LawfulToBackwardSearcherModel.defaultImplementation {pat : ρ} [Backward
   intro pos
   induction pos using WellFounded.induction Slice.Pos.wellFounded_lt with | h pos ih
   rw [Std.Iter.toList_eq_match_step, Std.Iter.step_eq]
-  simp only [Std.Iter.toIterM, ne_eq]
+  simp only [Std.Iter.toIterM_mk, Std.IterM.internalState_mk, ne_eq]
   by_cases h : pos = s.startPos
   · simpa [h] using IsValidRevSearchFrom.startPos
   · simp only [h, ↓reduceDIte]
diff --git a/src/Init/Data/String/Lemmas/Pattern/String/ForwardSearcher.lean b/src/Init/Data/String/Lemmas/Pattern/String/ForwardSearcher.lean
index 1ebbf8bc39ac..7a985eb43faa 100644
--- a/src/Init/Data/String/Lemmas/Pattern/String/ForwardSearcher.lean
+++ b/src/Init/Data/String/Lemmas/Pattern/String/ForwardSearcher.lean
@@ -319,15 +319,14 @@ theorem computeDistance_eq_prefixFunctionRecurrence {s : Slice} (i : Nat)
     · simp only [ht'.eq_prefixFunction, ih]
     · simp [getUTF8Byte_eq_getUTF8Byte_copy, String.getUTF8Byte, *]
 
-set_option backward.isDefEq.respectTransparency.types false in
 theorem isTable_buildTableGo {pat : Slice} {table : Array Nat} {ht₀ ht h}
     (ht' : IsTable pat.copy.toByteArray table) :
     IsTable pat.copy.toByteArray (buildTable.go pat table ht₀ ht h).1 := by
   fun_induction buildTable.go with
   | case1 t ht₀ ht h hlt patByte dist ih =>
     refine ih (ht'.push (by simp; omega) ?_)
-    simp only [getUTF8Byte_eq_getUTF8Byte_copy, String.getUTF8Byte, ht'.eq_prefixFunction, dist,
-      patByte]
+    simp only [getUTF8Byte_eq_getUTF8Byte_copy, String.getUTF8Byte_eq_getElem,
+      ht'.eq_prefixFunction, dist, patByte]
     rw [computeDistance_eq_prefixFunctionRecurrence _ _ rfl _ ht',
       prefixFunctionRecurrence_eq_prefixFunction]
     · exact prefixFunction_le_prefixFunction_sub_one_add_one ht₀
diff --git a/src/Init/Data/String/PosRaw.lean b/src/Init/Data/String/PosRaw.lean
index 505515150dd2..67067f303fb0 100644
--- a/src/Init/Data/String/PosRaw.lean
+++ b/src/Init/Data/String/PosRaw.lean
@@ -108,6 +108,9 @@ At runtime, this function is implemented by efficient, constant-time code.
 def getUTF8Byte (s : @& String) (p : Pos.Raw) (h : p < s.rawEndPos) : UInt8 :=
   s.toByteArray[p.byteIdx]
 
+theorem getUTF8Byte_eq_getElem {s : String} {p : Pos.Raw} {h} :
+    s.getUTF8Byte p h = s.toByteArray[p.byteIdx] := (rfl)
+
 @[deprecated getUTF8Byte (since := "2025-10-01"), extern "lean_string_get_byte_fast", expose]
 abbrev getUtf8Byte (s : String) (p : Pos.Raw) (h : p < s.rawEndPos) : UInt8 :=
   s.getUTF8Byte p h
diff --git a/src/Init/Data/Vector/Attach.lean b/src/Init/Data/Vector/Attach.lean
index 2ece137f6c4c..45820d9d3749 100644
--- a/src/Init/Data/Vector/Attach.lean
+++ b/src/Init/Data/Vector/Attach.lean
@@ -139,12 +139,30 @@ theorem attachWith_congr {xs ys : Vector α n} (w : xs = ys) {P : α → Prop} {
   subst w
   simp
 
-set_option backward.isDefEq.respectTransparency.types false in
+@[congr]
+theorem mk_congr {xs ys : Array α} (h : xs = ys) {h' : xs.size = n} :
+    mk xs h' = mk ys (h ▸ h') := by
+  subst h
+  simp
+
+/-
+TODO: Correctly place the following lemmas
+-/
+
+theorem _root_.List.attachWith_eq_map_attach {xs : List α} {P : α → Prop} {H : ∀ (a : α), a ∈ xs → P a} :
+    xs.attachWith P H = xs.attach.map fun ⟨x, h⟩ => ⟨x, H _ h⟩ := by
+  induction xs <;> simp_all
+
+theorem _root_.Array.attachWith_eq_map_attach {xs : Array α} {P : α → Prop} {H : ∀ (a : α), a ∈ xs → P a} :
+    xs.attachWith P H = xs.attach.map fun ⟨x, h⟩ => ⟨x, H _ h⟩ := by
+  cases xs <;> simp_all [List.attachWith_eq_map_attach]
+
 @[simp] theorem attach_push {a : α} {xs : Vector α n} :
     (xs.push a).attach =
       (xs.attach.map (fun ⟨x, h⟩ => ⟨x, mem_push_of_mem a h⟩)).push ⟨a, by simp⟩ := by
   rcases xs with ⟨xs, rfl⟩
-  simp [Array.map_attach_eq_pmap]
+  apply Vector.ext
+  simp [Array.attachWith_eq_map_attach, Array.getElem_push]
 
 @[simp] theorem attachWith_push {a : α} {xs : Vector α n} {P : α → Prop} {H : ∀ x ∈ xs.push a, P x} :
     (xs.push a).attachWith P H =
@@ -355,13 +373,15 @@ theorem pmap_append' {p : α → Prop} {f : ∀ a : α, p a → β} {xs : Vector
       xs.pmap f h₁ ++ ys.pmap f h₂ :=
   pmap_append _
 
-set_option backward.isDefEq.respectTransparency.types false in
 @[simp] theorem attach_append {xs : Vector α n} {ys : Vector α m} :
     (xs ++ ys).attach = xs.attach.map (fun ⟨x, h⟩ => (⟨x, mem_append_left ys h⟩ : { x // x ∈ xs ++ ys })) ++
       ys.attach.map (fun ⟨y, h⟩ => (⟨y, mem_append_right xs h⟩ : { y // y ∈ xs ++ ys })) := by
   rcases xs with ⟨xs, rfl⟩
   rcases ys with ⟨ys, rfl⟩
-  simp [Array.map_attach_eq_pmap]; rfl
+  apply Vector.ext
+  intro i hi
+  rw [Vector.getElem_append]
+  simp [Array.attachWith_eq_map_attach, Array.getElem_append]
 
 @[simp] theorem attachWith_append {P : α → Prop} {xs : Vector α n} {ys : Vector α m}
     {H : ∀ (a : α), a ∈ xs ++ ys → P a} :
diff --git a/src/Init/Data/Vector/Basic.lean b/src/Init/Data/Vector/Basic.lean
index 4ebd7925b96f..767996c2be83 100644
--- a/src/Init/Data/Vector/Basic.lean
+++ b/src/Init/Data/Vector/Basic.lean
@@ -64,7 +64,7 @@ recommended_spelling "empty" for "#v[]" in [Vector.mk, «term#v[_,]»]
 recommended_spelling "singleton" for "#v[x]" in [Vector.mk, «term#v[_,]»]
 
 /-- Convert a vector to a list. -/
-@[expose]
+@[expose, implicit_reducible]
 def toList (xs : Vector α n) : List α := xs.toArray.toList
 
 /-- Custom eliminator for `Vector α n` through `Array α` -/
@@ -238,7 +238,7 @@ We immediately simplify this to the `extract` operation, so there is no verifica
   simp [shrink, take]
 
 /-- Maps elements of a vector using the function `f`. -/
-@[inline, expose] def map (f : α → β) (xs : Vector α n) : Vector β n :=
+@[inline, expose, implicit_reducible] def map (f : α → β) (xs : Vector α n) : Vector β n :=
   ⟨xs.toArray.map f, by simp⟩
 
 /-- Maps elements of a vector using the function `f`, which also receives the index of the element. -/
diff --git a/src/Init/Data/Vector/DecidableEq.lean b/src/Init/Data/Vector/DecidableEq.lean
index 7525ad8f84f2..7917103eb09c 100644
--- a/src/Init/Data/Vector/DecidableEq.lean
+++ b/src/Init/Data/Vector/DecidableEq.lean
@@ -22,12 +22,11 @@ theorem isEqv_iff_rel {xs ys : Vector α n} {r} :
   rcases ys with ⟨ys, h⟩
   simp [Array.isEqv_iff_rel, h]
 
-set_option backward.isDefEq.respectTransparency.types false in
 theorem isEqv_eq_decide (xs ys : Vector α n) (r) :
     Vector.isEqv xs ys r = decide (∀ (i : Nat) (h' : i < n), r xs[i] ys[i]) := by
   rcases xs with ⟨xs, rfl⟩
   rcases ys with ⟨ys, h⟩
-  simp [Array.isEqv_eq_decide, h]
+  simp -implicitDefEqProofs [Array.isEqv_eq_decide, h]
 
 @[simp] theorem isEqv_toArray [BEq α] (xs ys : Vector α n) : (xs.toArray.isEqv ys.toArray r) = (xs.isEqv ys r) := by
   simp [isEqv_eq_decide, Array.isEqv_eq_decide]
diff --git a/src/Init/Data/Vector/Lemmas.lean b/src/Init/Data/Vector/Lemmas.lean
index 8c763b6c6223..5b9b1841f622 100644
--- a/src/Init/Data/Vector/Lemmas.lean
+++ b/src/Init/Data/Vector/Lemmas.lean
@@ -696,13 +696,11 @@ theorem toList_zip {as : Vector α n} {bs : Vector β n} :
   cases xs
   simp
 
-set_option backward.isDefEq.respectTransparency.types false in
 @[simp] theorem finIdxOf?_toList [BEq α] {a : α} {xs : Vector α n} :
     xs.toList.finIdxOf? a = (xs.finIdxOf? a).map (Fin.cast (by exact xs.size_toArray.symm)) := by
   rcases xs with ⟨xs, rfl⟩
   simp
 
-set_option backward.isDefEq.respectTransparency.types false in
 @[simp] theorem findFinIdx?_toList {p : α → Bool} {xs : Vector α n} :
     xs.toList.findFinIdx? p = (xs.findFinIdx? p).map (Fin.cast (by exact xs.size_toArray.symm)) := by
   rcases xs with ⟨xs, rfl⟩
diff --git a/src/Init/Data/Vector/Monadic.lean b/src/Init/Data/Vector/Monadic.lean
index dfa23ed96069..3b8233fbd0d0 100644
--- a/src/Init/Data/Vector/Monadic.lean
+++ b/src/Init/Data/Vector/Monadic.lean
@@ -154,12 +154,11 @@ theorem idRun_forIn'_yield_eq_foldl
       xs.attach.foldl (fun b ⟨a, h⟩ => f a h b |>.run) init := by
   simp
 
-set_option backward.isDefEq.respectTransparency.types false in
 @[simp, grind =] theorem forIn'_map [Monad m] [LawfulMonad m]
     {xs : Vector α n} (g : α → β) (f : (b : β) → b ∈ xs.map g → γ → m (ForInStep γ)) :
     forIn' (xs.map g) init f = forIn' xs init fun a h y => f (g a) (mem_map_of_mem h) y := by
   rcases xs with ⟨xs, rfl⟩
-  simp
+  simp [map_mk, forIn'_mk, Array.forIn'_map]
 
 /--
 We can express a for loop over a vector as a fold,
diff --git a/src/Init/GetElem.lean b/src/Init/GetElem.lean
index 8e28f99f50fc..4e974d02e3e1 100644
--- a/src/Init/GetElem.lean
+++ b/src/Init/GetElem.lean
@@ -322,6 +322,7 @@ theorem getElem_cons_drop_succ_eq_drop {as : List α} {i : Nat} (h : i < as.leng
 
 /-- Internal implementation of `as[i]?`. Do not use directly. -/
 -- We still keep it public for reduction purposes
+@[implicit_reducible]
 def get?Internal : (as : List α) → (i : Nat) → Option α
   | a::_,  0   => some a
   | _::as, n+1 => get?Internal as n
diff --git a/src/Init/Internal/Order/Basic.lean b/src/Init/Internal/Order/Basic.lean
index 1f50a87e767f..fda656c20bdd 100644
--- a/src/Init/Internal/Order/Basic.lean
+++ b/src/Init/Internal/Order/Basic.lean
@@ -767,6 +767,23 @@ This is intended to be used in the construction of `partial_fixpoint`, and not m
 -/
 @[expose] def FlatOrder {α : Sort u} (b : α) := α
 
+def FlatOrder.mk {α : Sort u} (b : α) (x : α) : FlatOrder b := x
+
+def FlatOrder.inner {α : Sort u} {b : α} (x : FlatOrder b) : α := x
+
+theorem FlatOrder.mk_inner {α : Sort u} {b : α} {x : FlatOrder b} :
+    FlatOrder.mk b x.inner = x :=
+  (rfl)
+
+theorem FlatOrder.inner_mk {α : Sort u} {b : α} {x : α} :
+    (FlatOrder.mk b x).inner = x :=
+  (rfl)
+
+@[simp]
+theorem FlatOrder.mk_inj {α : Sort u} {b : α} {x y : α} :
+    FlatOrder.mk b x = FlatOrder.mk b y ↔ x = y :=
+  Iff.rfl
+
 variable {b : α}
 
 /--
@@ -793,9 +810,8 @@ private theorem Classical.some_spec₂ {α : Sort _} {p : α → Prop} {h : ∃
 noncomputable def flat_csup (c : FlatOrder b → Prop) : FlatOrder b := by
   by_cases h : ∃ (x : FlatOrder b), c x ∧ x ≠ b
   · exact Classical.choose h
-  · exact b
+  · exact .mk b b
 
-set_option backward.isDefEq.respectTransparency.types false in
 theorem flat_csup_is_sup (c : FlatOrder b → Prop) (hc : chain c) :
     is_sup c (flat_csup c) := by
   intro x
@@ -839,7 +855,7 @@ theorem flat_csup_eq (c : FlatOrder b → Prop) (hchain : chain c) :
   · apply flat_csup_is_sup _ hchain
   · apply CCPO.csup_spec
 
-theorem admissible_flatOrder (P : FlatOrder b → Prop) (hnot : P b) : admissible P := by
+theorem admissible_flatOrder (P : FlatOrder b → Prop) (hnot : P (.mk b b)) : admissible P := by
   intro c hchain h
   by_cases h' : ∃ (x : FlatOrder b), c x ∧ x ≠ b
   · simp [← flat_csup_eq, flat_csup, h']
@@ -890,6 +906,7 @@ instance : MonoBind Option where
 
 theorem Option.admissible_eq_some (P : Prop) (y : α) :
     admissible (fun (x : Option α) => x = some y → P) := by
+  change admissible fun x : FlatOrder none => x = .mk _ (some y) → P
   apply admissible_flatOrder; simp
 
 instance [inst : ∀ α, PartialOrder (m α)] : PartialOrder (ExceptT ε m α) := inst _
diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean
index 2ccd24fd28ec..d4de9cd56509 100644
--- a/src/Init/Prelude.lean
+++ b/src/Init/Prelude.lean
@@ -1046,7 +1046,7 @@ Decides whether two Booleans are equal.
 This function should normally be called via the `DecidableEq Bool` instance that it exists to
 support.
 -/
-@[inline] def Bool.decEq (a b : Bool) : Decidable (Eq a b) :=
+@[inline, implicit_reducible] def Bool.decEq (a b : Bool) : Decidable (Eq a b) :=
    match a, b with
    | false, false => isTrue rfl
    | false, true  => isFalse (fun h => Bool.noConfusion h)
@@ -1116,7 +1116,8 @@ the definition of the function uses `fun _ => t` and `fun _ => e` so this recove
 the expected "lazy" behavior of `if`: the `t` and `e` arguments delay evaluation
 until `c` is known.
 -/
-@[macro_inline] def ite {α : Sort u} (c : Prop) [h : Decidable c] (t e : α) : α :=
+@[macro_inline, implicit_reducible]
+def ite {α : Sort u} (c : Prop) [h : Decidable c] (t e : α) : α :=
   h.casesOn (fun _ => e) (fun _ => t)
 
 @[macro_inline] instance {p q} [dp : Decidable p] [dq : Decidable q] : Decidable (And p q) :=
@@ -2346,7 +2347,7 @@ Returns `a` modulo `n` as a `Fin n`.
 
 This function exists for bootstrapping purposes. Use `Fin.ofNat` instead.
 -/
-@[expose] protected def Fin.Internal.ofNat (n : Nat) (hn : LT.lt 0 n) (a : Nat) : Fin n :=
+@[expose, implicit_reducible] protected def Fin.Internal.ofNat (n : Nat) (hn : LT.lt 0 n) (a : Nat) : Fin n :=
   ⟨HMod.hMod a n, Nat.mod_lt _ hn⟩
 
 /--
@@ -2397,7 +2398,7 @@ Return the underlying `Nat` that represents a bitvector.
 
 This is O(1) because `BitVec` is a (zero-cost) wrapper around a `Nat`.
 -/
-@[expose]
+@[expose, implicit_reducible]
 protected def BitVec.toNat (x : BitVec w) : Nat := x.toFin.val
 
 instance : LT (BitVec w) where lt := (LT.lt ·.toNat ·.toNat)
diff --git a/src/Std/Data/DHashMap/Internal/Defs.lean b/src/Std/Data/DHashMap/Internal/Defs.lean
index ddf61c724821..1968d85c1325 100644
--- a/src/Std/Data/DHashMap/Internal/Defs.lean
+++ b/src/Std/Data/DHashMap/Internal/Defs.lean
@@ -359,6 +359,7 @@ def get? [BEq α] [LawfulBEq α] [Hashable α] (m : Raw₀ α β) (a : α) : Opt
   buckets[i].getCast? a
 
 /-- Internal implementation detail of the hash map -/
+@[implicit_reducible]
 def contains [BEq α] [Hashable α] (m : Raw₀ α β) (a : α) : Bool :=
   let ⟨⟨_, buckets⟩, h⟩ := m
   let ⟨i, h⟩ := mkIdx buckets.size h (hash a)
diff --git a/src/Std/Data/DHashMap/Internal/Model.lean b/src/Std/Data/DHashMap/Internal/Model.lean
index 3457351ffdc1..274f0d236616 100644
--- a/src/Std/Data/DHashMap/Internal/Model.lean
+++ b/src/Std/Data/DHashMap/Internal/Model.lean
@@ -45,6 +45,7 @@ open Std.Internal
 /-! # Setting up the infrastructure -/
 
 /-- Internal implementation detail of the hash map -/
+@[implicit_reducible]
 def bucket [Hashable α] (self : Array (AssocList α β)) (h : 0 < self.size) (k : α) :
     AssocList α β :=
   let ⟨i, h⟩ := mkIdx self.size h (hash k)
@@ -289,6 +290,7 @@ def getKey?ₘ [BEq α] [Hashable α] (m : Raw₀ α β) (a : α) : Option α :=
   (bucket m.1.buckets m.2 a).getKey? a
 
 /-- Internal implementation detail of the hash map -/
+@[implicit_reducible]
 def containsₘ [BEq α] [Hashable α] (m : Raw₀ α β) (a : α) : Bool :=
   (bucket m.1.buckets m.2 a).contains a
 
@@ -526,26 +528,18 @@ theorem getKey!_eq_getKey!ₘ [BEq α] [Hashable α] [Inhabited α] (m : Raw₀
 theorem contains_eq_containsₘ [BEq α] [Hashable α] (m : Raw₀ α β) (a : α) :
     m.contains a = m.containsₘ a := (rfl)
 
-set_option backward.isDefEq.respectTransparency.types false in
 theorem insert_eq_insertₘ [BEq α] [Hashable α] (m : Raw₀ α β) (a : α) (b : β a) :
     m.insert a b = m.insertₘ a b := by
-  rw [insert, insertₘ, containsₘ, bucket]
-  dsimp only [Array.ugetElem_eq_getElem, Array.uset]
-  split
-  · simp only [replaceₘ, Subtype.mk.injEq, Raw.mk.injEq, true_and]
-    rw [Array.set_set, updateBucket]
-    simp only [Array.uset, Array.ugetElem_eq_getElem]
-  · rfl
+  simp [insert, insertₘ, containsₘ, bucket, replaceₘ, updateBucket, consₘ]
 
-set_option backward.isDefEq.respectTransparency.types false in
 theorem alter_eq_alterₘ [BEq α] [Hashable α] [LawfulBEq α] (m : Raw₀ α β) (a : α)
     (f : Option (β a) → Option (β a)) : m.alter a f = m.alterₘ a f := by
-    dsimp only [alter, alterₘ, containsₘ, ← bucket_eq]
-    split
-    · congr 2
-      · simp only [withComputedSize, bucket_updateBucket]
-      · simp only [Array.uset, bucket, Array.ugetElem_eq_getElem, Array.set_set, updateBucket]
-    · congr
+  simp only [alter, alterₘ, containsₘ, ← bucket_eq]
+  simp only [AssocList.contains_eq, Array.uset_eq_set, Array.set_set, buckets_withComputedSize,
+    bucket_updateBucket]
+  split
+  · rfl
+  · rfl
 
 theorem modify_eq_alter [BEq α] [Hashable α] [LawfulBEq α] (m : Raw₀ α β) (a : α)
     (f : β a → β a) : m.modify a f = m.alter a (·.map f) := by
@@ -568,7 +562,6 @@ namespace Const
 
 variable {β : Type v}
 
-set_option backward.isDefEq.respectTransparency.types false in
 theorem alter_eq_alterₘ [BEq α] [Hashable α] [EquivBEq α] (m : Raw₀ α (fun _ => β)) (a : α)
     (f : Option β → Option β) : Const.alter m a f = Const.alterₘ m a f := by
     dsimp only [alter, alterₘ, containsₘ, ← bucket_eq]
@@ -576,7 +569,7 @@ theorem alter_eq_alterₘ [BEq α] [Hashable α] [EquivBEq α] (m : Raw₀ α (f
     · congr 2
       · simp only [withComputedSize, bucket_updateBucket]
       · simp only [Array.uset, bucket, Array.ugetElem_eq_getElem, Array.set_set, updateBucket]
-    · congr
+    · rfl
 
 theorem modify_eq_alter [BEq α] [Hashable α] [EquivBEq α] (m : Raw₀ α (fun _ => β)) (a : α)
     (f : β → β) : Const.modify m a f = Const.alter m a (·.map f) := by
@@ -597,7 +590,6 @@ theorem modify_eq_modifyₘ [BEq α] [Hashable α] [EquivBEq α] (m : Raw₀ α
 
 end Const
 
-set_option backward.isDefEq.respectTransparency.types false in
 theorem containsThenInsert_eq_insertₘ [BEq α] [Hashable α] (m : Raw₀ α β) (a : α) (b : β a) :
     (m.containsThenInsert a b).2 = m.insertₘ a b := by
   rw [containsThenInsert, insertₘ, containsₘ, bucket]
@@ -614,7 +606,6 @@ theorem containsThenInsert_eq_containsₘ [BEq α] [Hashable α] (m : Raw₀ α
   dsimp only [Array.ugetElem_eq_getElem, Array.uset]
   split <;> simp_all
 
-set_option backward.isDefEq.respectTransparency.types false in
 theorem containsThenInsertIfNew_eq_insertIfNewₘ [BEq α] [Hashable α] (m : Raw₀ α β) (a : α)
     (b : β a) : (m.containsThenInsertIfNew a b).2 = m.insertIfNewₘ a b := by
   rw [containsThenInsertIfNew, insertIfNewₘ, containsₘ, bucket]
@@ -644,7 +635,6 @@ theorem getThenInsertIfNew?_eq_get?ₘ [BEq α] [Hashable α] [LawfulBEq α] (m
   dsimp only [Array.ugetElem_eq_getElem, Array.uset]
   split <;> simp_all
 
-set_option backward.isDefEq.respectTransparency.types false in
 theorem erase_eq_eraseₘ [BEq α] [Hashable α] (m : Raw₀ α β) (a : α) :
     m.erase a = m.eraseₘ a := by
   rw [erase, eraseₘ, containsₘ, bucket]
diff --git a/src/Std/Data/DHashMap/Internal/WF.lean b/src/Std/Data/DHashMap/Internal/WF.lean
index 94648cfea7ff..f4a940097c73 100644
--- a/src/Std/Data/DHashMap/Internal/WF.lean
+++ b/src/Std/Data/DHashMap/Internal/WF.lean
@@ -457,13 +457,11 @@ theorem getEntry?ₘ_eq_getEntry? [BEq α] [PartialEquivBEq α] [Hashable α] [L
     m.getEntry?ₘ a = List.getEntry? a (toListModel m.1.buckets) :=
   apply_bucket hm AssocList.getEntry?_eq getEntry?_of_perm getEntry?_append_of_containsKey_eq_false
 
-set_option backward.isDefEq.respectTransparency.types false in
 theorem get_eq_getValueCast [BEq α] [Hashable α] [LawfulBEq α] {m : Raw₀ α β} (hm : Raw.WFImp m.1)
     {a : α} {h : m.contains a} :
     m.get a h = getValueCast a (toListModel m.1.buckets) (contains_eq_containsKey hm ▸ h) := by
   rw [get_eq_getₘ, getₘ_eq_getValue hm]
 
-set_option backward.isDefEq.respectTransparency.types false in
 theorem getEntry_eq_getEntry [BEq α] [Hashable α] [PartialEquivBEq α] [LawfulHashable α] {m : Raw₀ α β} (hm : Raw.WFImp m.1)
     {a : α} {h : m.contains a} :
     m.getEntry a h = List.getEntry a (toListModel m.1.buckets) (contains_eq_containsKey hm ▸ h) := by
@@ -574,7 +572,6 @@ theorem Const.getₘ_eq_getValue [BEq α] [Hashable α] [PartialEquivBEq α] [La
   apply_bucket_with_proof hm a AssocList.get List.getValue AssocList.get_eq List.getValue_of_perm
     List.getValue_append_of_containsKey_eq_false
 
-set_option backward.isDefEq.respectTransparency.types false in
 theorem Const.get_eq_getValue [BEq α] [Hashable α] [PartialEquivBEq α] [LawfulHashable α]
     {m : Raw₀ α (fun _ => β)} (hm : Raw.WFImp m.1) {a : α} {h} :
     Const.get m a h = getValue a (toListModel m.1.buckets) (contains_eq_containsKey hm ▸ h) := by
diff --git a/src/Std/Data/DTreeMap/Internal/Balancing.lean b/src/Std/Data/DTreeMap/Internal/Balancing.lean
index 1a6e66b408be..f665717ed3a8 100644
--- a/src/Std/Data/DTreeMap/Internal/Balancing.lean
+++ b/src/Std/Data/DTreeMap/Internal/Balancing.lean
@@ -534,7 +534,6 @@ def balanceₘ (k : α) (v : β k) (l r : Impl α β) : Impl α β :=
 
 attribute [Std.Internal.tree_tac] and_true true_and and_self heq_eq_eq inner.injEq
 
-set_option backward.isDefEq.respectTransparency.types false in
 theorem balance!_eq_balanceₘ {k v} {l r : Impl α β} (hlb : l.Balanced) (hrb : r.Balanced)
     (hlr : BalanceLErasePrecond l.size r.size ∨ BalanceLErasePrecond r.size l.size) :
     balance! k v l r = balanceₘ k v l r := by
diff --git a/src/Std/Data/DTreeMap/Internal/Def.lean b/src/Std/Data/DTreeMap/Internal/Def.lean
index e907afe2ae30..df7259dd041e 100644
--- a/src/Std/Data/DTreeMap/Internal/Def.lean
+++ b/src/Std/Data/DTreeMap/Internal/Def.lean
@@ -37,7 +37,7 @@ def delta : Nat := 3
 
 /-- The "ratio" parameter of the size-bounded tree. Controls how aggressive the rebalancing
 operations are. -/
-@[inline, Std.Internal.tree_tac]
+@[inline, Std.Internal.tree_tac, implicit_reducible]
 def ratio : Nat := 2
 
 variable {α : Type u} {β : α → Type v}
@@ -52,7 +52,7 @@ In contrast to other functions, `size` is defined here because it is required to
 -/
 
 /-- The size information stored in the tree. -/
-@[inline]
+@[inline, implicit_reducible]
 def size : Impl α β → Nat
   | inner sz _ _ _ _ => sz
   | leaf => 0
diff --git a/src/Std/Data/DTreeMap/Internal/Model.lean b/src/Std/Data/DTreeMap/Internal/Model.lean
index e81fadeff365..804f9f0b245c 100644
--- a/src/Std/Data/DTreeMap/Internal/Model.lean
+++ b/src/Std/Data/DTreeMap/Internal/Model.lean
@@ -1002,7 +1002,6 @@ def getEntryGT?ₘ' [Ord α] (k : α) (t : Impl α β) : Option ((a : α) × β
   | base, .eq _ _ r => r.head?.or base
   | base, .gt _ _ _ _ => base
 
-set_option backward.isDefEq.respectTransparency.types false in
 theorem getEntryGT?_eq_getEntryGT?ₘ' [Ord α] (k : α) (t : Impl α β) :
     getEntryGT? k t = getEntryGT?ₘ' k t := by
   rw [getEntryGT?ₘ', getEntryGT?]
diff --git a/src/Std/Data/DTreeMap/Internal/Operations.lean b/src/Std/Data/DTreeMap/Internal/Operations.lean
index 94c3962aa704..84c06bf49bc4 100644
--- a/src/Std/Data/DTreeMap/Internal/Operations.lean
+++ b/src/Std/Data/DTreeMap/Internal/Operations.lean
@@ -668,6 +668,7 @@ structure BalancedTree where
 attribute [Std.Internal.tree_tac] BalancedTree.balanced_impl
 
 /-- Transforms an element of `SizedBalancedTree` into a `BalancedTree`. -/
+@[implicit_reducible]
 def SizedBalancedTree.toBalancedTree {lb ub} (t : SizedBalancedTree α β lb ub) : BalancedTree α β :=
   ⟨t.impl, t.balanced_impl⟩
 
diff --git a/src/Std/Data/DTreeMap/Internal/WF/Lemmas.lean b/src/Std/Data/DTreeMap/Internal/WF/Lemmas.lean
index c1f8ed9b02bf..97d1868af729 100644
--- a/src/Std/Data/DTreeMap/Internal/WF/Lemmas.lean
+++ b/src/Std/Data/DTreeMap/Internal/WF/Lemmas.lean
@@ -2032,7 +2032,6 @@ theorem WF.constAlter! {_ : Ord α} {β : Type v} {t : Impl α β} {a f} (h : t.
 ### mergeWith!
 -/
 
-set_option backward.isDefEq.respectTransparency.types false in
 theorem mergeWith_eq_mergeWith! {_ : Ord α} [LawfulEqOrd α] {mergeFn} {t₁ t₂ : Impl α β}
     (h : t₁.Balanced) :
     (mergeWith mergeFn t₁ t₂ h).impl = mergeWith! mergeFn t₁ t₂ := by
@@ -2049,13 +2048,11 @@ theorem mergeWith_eq_mergeWith! {_ : Ord α} [LawfulEqOrd α] {mergeFn} {t₁ t
     congr
     exact ihl h
 
-set_option backward.isDefEq.respectTransparency.types false in
 theorem WF.mergeWith! {_ : Ord α} [LawfulEqOrd α] {mergeFn} {t₁ t₂ : Impl α β} (h : t₁.WF) :
     (Impl.mergeWith! mergeFn t₁ t₂).WF := by
   rw [← mergeWith_eq_mergeWith! h.balanced]
   exact h.mergeWith
 
-set_option backward.isDefEq.respectTransparency.types false in
 theorem Const.mergeWith_eq_mergeWith! {β : Type v} {_ : Ord α} {mergeFn} {t₁ t₂ : Impl α β}
     (h : t₁.Balanced) :
     (mergeWith mergeFn t₁ t₂ h).impl = mergeWith! mergeFn t₁ t₂ := by
diff --git a/src/Std/Data/Internal/List/Associative.lean b/src/Std/Data/Internal/List/Associative.lean
index a8863f93768b..b45ffd1e8184 100644
--- a/src/Std/Data/Internal/List/Associative.lean
+++ b/src/Std/Data/Internal/List/Associative.lean
@@ -8491,7 +8491,6 @@ theorem containsKey_minKey? [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l
   obtain ⟨e, ⟨hm, _⟩, rfl⟩ := hkm
   exact containsKey_of_mem hm
 
-set_option backward.isDefEq.respectTransparency.types false in
 theorem min?_keys [Ord α] [TransOrd α]
     [LawfulEqOrd α] [LE α] [LawfulOrderOrd α] [Min α]
     [LawfulOrderLeftLeaningMin α] (l : List ((a : α) × β a)) :
diff --git a/src/Std/Data/Iterators/Combinators/Monadic/Drop.lean b/src/Std/Data/Iterators/Combinators/Monadic/Drop.lean
index 4da99092f0c9..aca9f9285d8c 100644
--- a/src/Std/Data/Iterators/Combinators/Monadic/Drop.lean
+++ b/src/Std/Data/Iterators/Combinators/Monadic/Drop.lean
@@ -52,7 +52,7 @@ it.drop 3   ------⊥
 Currently, this combinator incurs an additional O(1) cost with each output of `it`, even when the iterator
 does not drop any elements anymore.
 -/
-@[always_inline, inline]
+@[always_inline, inline, implicit_reducible]
 def IterM.drop (n : Nat) (it : IterM (α := α) m β) :=
   (⟨Iterators.Types.Drop.mk n it⟩ : IterM m β)
 
diff --git a/src/Std/Data/Iterators/Combinators/Monadic/DropWhile.lean b/src/Std/Data/Iterators/Combinators/Monadic/DropWhile.lean
index c2cc457ba13b..9fbcb72ea036 100644
--- a/src/Std/Data/Iterators/Combinators/Monadic/DropWhile.lean
+++ b/src/Std/Data/Iterators/Combinators/Monadic/DropWhile.lean
@@ -56,7 +56,7 @@ created directly with `IterM.dropWhileWithPostcondition` but only with
 `Intermediate.dropWhileWithPostcondition` is meant to be used only for internally or for
 verification purposes.
 -/
-@[always_inline, inline]
+@[always_inline, inline, implicit_reducible]
 def IterM.Intermediate.dropWhileWithPostcondition (P : β → PostconditionT m (ULift Bool))
     (dropping : Bool) (it : IterM (α := α) m β) :=
   (⟨Iterators.Types.DropWhile.mk (P := P) dropping it⟩ : IterM m β)
@@ -80,7 +80,7 @@ directly with `IterM.dropWhile` but only with `Intermediate.dropWhile`.
 
 `Intermediate.dropWhile` is meant to be used only for internally or for verification purposes.
 -/
-@[always_inline, inline]
+@[always_inline, inline, implicit_reducible]
 def IterM.Intermediate.dropWhile [Monad m] (P : β → Bool) (dropping : Bool)
     (it : IterM (α := α) m β) :=
   (IterM.Intermediate.dropWhileWithPostcondition (pure ∘ ULift.up ∘ P) dropping it : IterM m β)
diff --git a/src/Std/Data/Iterators/Combinators/Monadic/TakeWhile.lean b/src/Std/Data/Iterators/Combinators/Monadic/TakeWhile.lean
index 540dea988814..0818588a0644 100644
--- a/src/Std/Data/Iterators/Combinators/Monadic/TakeWhile.lean
+++ b/src/Std/Data/Iterators/Combinators/Monadic/TakeWhile.lean
@@ -155,7 +155,7 @@ In this case, the `Finite` (or `Productive`) instance needs to be proved manuall
 This combinator calls `P` on each output of `it` until the predicate evaluates to false. Then
 it terminates.
 -/
-@[always_inline, inline]
+@[always_inline, inline, implicit_reducible]
 def IterM.takeWhile [Monad m] (P : β → Bool) (it : IterM (α := α) m β) :=
   (it.takeWhileWithPostcondition (pure ∘ ULift.up ∘ P) : IterM m β)
 
diff --git a/src/Std/Data/Iterators/Lemmas/Combinators/Drop.lean b/src/Std/Data/Iterators/Lemmas/Combinators/Drop.lean
index 50583aa1c80f..e5d84f008a1c 100644
--- a/src/Std/Data/Iterators/Lemmas/Combinators/Drop.lean
+++ b/src/Std/Data/Iterators/Lemmas/Combinators/Drop.lean
@@ -26,7 +26,6 @@ theorem Iter.drop_eq {α β} [Iterator α Id β] {n : Nat}
     it.drop n = (it.toIterM.drop n).toIter :=
   rfl
 
-set_option backward.isDefEq.respectTransparency.types false in
 theorem Iter.step_drop {α β} [Iterator α Id β] {n : Nat}
     {it : Iter (α := α) β} :
     (it.drop n).step = (match it.step with
@@ -38,8 +37,19 @@ theorem Iter.step_drop {α β} [Iterator α Id β] {n : Nat}
     | .done h => .done (.done h)) := by
   simp only [drop_eq, step, toIterM_toIter, IterM.step_drop, Id.run_bind]
   generalize it.toIterM.step.run = step
-  cases step.inflate using PlausibleIterStep.casesOn <;> cases n <;>
-    simp [PlausibleIterStep.yield, PlausibleIterStep.skip, PlausibleIterStep.done]
+  cases step.inflate using PlausibleIterStep.casesOn <;> cases n --<;>
+  · simp only [PlausibleIterStep.yield, Id.run_pure, Shrink.inflate_deflate,
+    IterM.Step.toPure_yield, toIter_toIterM, toIterM_toIter]
+  · simp only [PlausibleIterStep.skip, Id.run_pure, Shrink.inflate_deflate, IterM.Step.toPure_skip,
+    IterM.Step.toPure_yield, PlausibleIterStep.yield, toIter_toIterM, toIterM_toIter]
+  · simp only [PlausibleIterStep.skip, Id.run_pure, Shrink.inflate_deflate, IterM.Step.toPure_skip,
+    toIter_toIterM, toIterM_toIter]
+  · simp only [PlausibleIterStep.skip, Id.run_pure, Shrink.inflate_deflate, IterM.Step.toPure_skip,
+    toIter_toIterM, toIterM_toIter]
+  · simp only [PlausibleIterStep.done, Id.run_pure, Shrink.inflate_deflate, IterM.Step.toPure_done,
+    toIter_toIterM]
+  · simp only [PlausibleIterStep.done, Id.run_pure, Shrink.inflate_deflate, IterM.Step.toPure_done,
+    toIter_toIterM]
 
 theorem Iter.atIdxSlow?_drop {α β}
     [Iterator α Id β] [Productive α Id] {k l : Nat}
diff --git a/src/Std/Data/Iterators/Lemmas/Combinators/DropWhile.lean b/src/Std/Data/Iterators/Lemmas/Combinators/DropWhile.lean
index 2b0f06b0f9f5..4fbc5e4b0fdc 100644
--- a/src/Std/Data/Iterators/Lemmas/Combinators/DropWhile.lean
+++ b/src/Std/Data/Iterators/Lemmas/Combinators/DropWhile.lean
@@ -34,7 +34,6 @@ theorem Iter.dropWhile_eq_dropWhile_toIterM {α β} [Iterator α Id β] {P}
     it.dropWhile P = (it.toIterM.dropWhile P).toIter :=
   rfl
 
-set_option backward.isDefEq.respectTransparency.types false in
 theorem Iter.step_intermediateDropWhile {α β} [Iterator α Id β]
     {it : Iter (α := α) β} {P} {dropping} :
     (Iter.Intermediate.dropWhile P dropping it).step = (match it.step with
diff --git a/src/Std/Data/Iterators/Lemmas/Combinators/Monadic/FilterMap.lean b/src/Std/Data/Iterators/Lemmas/Combinators/Monadic/FilterMap.lean
index 10d1a076e77d..6cb54f7be75c 100644
--- a/src/Std/Data/Iterators/Lemmas/Combinators/Monadic/FilterMap.lean
+++ b/src/Std/Data/Iterators/Lemmas/Combinators/Monadic/FilterMap.lean
@@ -14,7 +14,6 @@ public import Std.Data.Iterators.Lemmas.Equivalence.StepCongr
 namespace Std
 open Std.Internal Std.Iterators
 
-set_option backward.isDefEq.respectTransparency.types false in
 theorem IterM.stepAsHetT_filterMapWithPostcondition [Monad m] [LawfulMonad m] [Monad n]
     [LawfulMonad n] [Iterator α m β] [MonadLiftT m n] [LawfulMonadLiftT m n]
     {f : β → PostconditionT n (Option γ)} {it : IterM (α := α) m β} :
diff --git a/src/Std/Data/Iterators/Lemmas/Combinators/Monadic/Zip.lean b/src/Std/Data/Iterators/Lemmas/Combinators/Monadic/Zip.lean
index 1dcc8fa98d87..3fa415bf3be8 100644
--- a/src/Std/Data/Iterators/Lemmas/Combinators/Monadic/Zip.lean
+++ b/src/Std/Data/Iterators/Lemmas/Combinators/Monadic/Zip.lean
@@ -24,6 +24,7 @@ cannot be created directly with `IterM.zip`.
 
 `Intermediate.zip` is meant to be used only for verification purposes.
 -/
+@[implicit_reducible]
 noncomputable def IterM.Intermediate.zip [Iterator α₁ m β₁] (it₁ : IterM (α := α₁) m β₁)
     (memo : (Option { out : β₁ //
         ∃ it : IterM (α := α₁) m β₁, it.IsPlausibleOutput out }))
diff --git a/src/Std/Data/Iterators/Lemmas/Combinators/TakeWhile.lean b/src/Std/Data/Iterators/Lemmas/Combinators/TakeWhile.lean
index 0f7400a6c76f..0431b9f406d3 100644
--- a/src/Std/Data/Iterators/Lemmas/Combinators/TakeWhile.lean
+++ b/src/Std/Data/Iterators/Lemmas/Combinators/TakeWhile.lean
@@ -24,7 +24,6 @@ theorem Iter.takeWhile_eq {α β} [Iterator α Id β] {P}
     it.takeWhile P = (it.toIterM.takeWhile P).toIter :=
   rfl
 
-set_option backward.isDefEq.respectTransparency.types false in
 theorem Iter.step_takeWhile {α β} [Iterator α Id β] {P}
     {it : Iter (α := α) β} :
     (it.takeWhile P).step = (match it.step with
@@ -41,7 +40,6 @@ theorem Iter.step_takeWhile {α β} [Iterator α Id β] {P}
   · simp
   · simp
 
-set_option backward.isDefEq.respectTransparency.types false in
 theorem Iter.val_step_takeWhile {α β} [Iterator α Id β] {P}
     {it : Iter (α := α) β} :
     (it.takeWhile P).step.val = (match it.step.val with
@@ -50,10 +48,11 @@ theorem Iter.val_step_takeWhile {α β} [Iterator α Id β] {P}
         | false => .done
       | .skip it' => .skip (it'.takeWhile P)
       | .done => .done) := by
-  simp [Iter.takeWhile_eq, Iter.step, toIterM_toIter, IterM.step_takeWhile]
+  simp only [takeWhile_eq, step, toIterM_toIter, IterM.step_takeWhile, PlausibleIterStep.yield,
+    PlausibleIterStep.done, PlausibleIterStep.skip, Id.run_bind, IterM.Step.val_toPure]
   generalize it.toIterM.step.run = step
   cases step.inflate using PlausibleIterStep.casesOn
-  · simp only [IterM.Step.toPure_yield, PlausibleIterStep.yield, toIter_toIterM, toIterM_toIter]
+  · simp only [IterStep.mapIterator_yield, toIterM_toIter]
     split <;> split <;> (try exfalso; simp_all; done) <;> simp_all
   · simp
   · simp
@@ -109,7 +108,6 @@ theorem Iter.atIdxSlow?_takeWhile {α β}
       step_takeWhile]
     split <;> rfl
 
-set_option backward.isDefEq.respectTransparency.types false in
 private theorem List.getElem?_takeWhile {l : List α} {P : α → Bool} {k} :
     (l.takeWhile P)[k]? = if ∀ k' : Nat, k' ≤ k → l[k']?.any P then l[k]? else none := by
   induction l generalizing k
diff --git a/src/Std/Data/Iterators/Lemmas/Combinators/Zip.lean b/src/Std/Data/Iterators/Lemmas/Combinators/Zip.lean
index db3f8bddcad1..1bc94d766344 100644
--- a/src/Std/Data/Iterators/Lemmas/Combinators/Zip.lean
+++ b/src/Std/Data/Iterators/Lemmas/Combinators/Zip.lean
@@ -69,7 +69,6 @@ theorem Iter.zip_eq_intermediateZip [Iterator α₁ Id β₁]
     it₁.zip it₂ = Intermediate.zip it₁ none it₂ := by
   rfl
 
-set_option backward.isDefEq.respectTransparency.types false in
 theorem Iter.step_intermediateZip
     [Iterator α₁ Id β₁] [Iterator α₂ Id β₂]
     {it₁ : Iter (α := α₁) β₁}
diff --git a/src/Std/Data/Iterators/Lemmas/Equivalence/Basic.lean b/src/Std/Data/Iterators/Lemmas/Equivalence/Basic.lean
index 472393a9ccd5..f65f5fbbae48 100644
--- a/src/Std/Data/Iterators/Lemmas/Equivalence/Basic.lean
+++ b/src/Std/Data/Iterators/Lemmas/Equivalence/Basic.lean
@@ -64,6 +64,7 @@ A noncomputable variant of `IterM.step` using the `HetT` monad.
 It is used in the definition of the equivalence relations on iterators,
 namely `IterM.Equiv` and `Iter.Equiv`.
 -/
+@[implicit_reducible]
 noncomputable def IterM.stepAsHetT [Iterator α m β] [Monad m] (it : IterM (α := α) m β) :
     HetT m (IterStep (IterM (α := α) m β) β) :=
     ⟨it.IsPlausibleStep, inferInstance, (fun step => .deflate step.inflate) <$> it.step⟩
@@ -96,7 +97,6 @@ coinductive_fixpoint monotonicity by
 
 end Definition
 
-set_option backward.isDefEq.respectTransparency.types false in
 @[simp]
 theorem Equivalence.prun_liftInner_step [Iterator α m β] [Monad m] [Monad n]
     [MonadLiftT m n] [LawfulMonad m] [LawfulMonad n] [LawfulMonadLiftT m n]
@@ -110,7 +110,6 @@ theorem Equivalence.property_step [Iterator α m β] [Monad m] [LawfulMonad m]
     {it : IterM (α := α) m β} : (IterM.stepAsHetT it).Property = it.IsPlausibleStep :=
   rfl
 
-set_option backward.isDefEq.respectTransparency.types false in
 @[simp]
 theorem Equivalence.prun_step [Iterator α m β] [Monad m] [LawfulMonad m]
     {it : IterM (α := α) m β} {f : (step : _) → _ → m γ} :
@@ -242,7 +241,6 @@ theorem Iter.Equiv.trans {α₁ α₂ α₃ β : Type w}
     (hbc : Iter.Equiv itb itc) : Iter.Equiv ita itc :=
   BundledIterM.Equiv.trans hab hbc
 
-set_option backward.isDefEq.respectTransparency.types false in
 theorem IterM.Equiv.of_morphism {α₁ α₂} {m : Type w → Type w'} [Monad m] [LawfulMonad m]
     {β : Type w} [Iterator α₁ m β] [Iterator α₂ m β]
     (ita : IterM (α := α₁) m β)
diff --git a/src/Std/Data/Iterators/Lemmas/Equivalence/StepCongr.lean b/src/Std/Data/Iterators/Lemmas/Equivalence/StepCongr.lean
index f154b17bde17..f20833768a33 100644
--- a/src/Std/Data/Iterators/Lemmas/Equivalence/StepCongr.lean
+++ b/src/Std/Data/Iterators/Lemmas/Equivalence/StepCongr.lean
@@ -115,7 +115,6 @@ theorem IterStep.restrict_bundle [Iterator α₁ m β] [Iterator α₂ m β] [Mo
     IterM.QuotStep.restrict ⟨step.bundledQuotient, h⟩ = Quot.mk _ h.choose := by
   rfl
 
-set_option backward.isDefEq.respectTransparency.types false in
 /-
 Equivalence and usage of `transportAlongEquiv` tells us:
 
@@ -199,7 +198,6 @@ theorem IterM.Equiv.lift_step_bind_congr {α₁ α₂ : Type w} [Monad m] [Lawfu
   have hex := exists_step_of_step h.symm step.inflate
   simp [hfg (.deflate hex.choose) step (by simpa using hex.choose_spec.symm)]
 
-set_option backward.isDefEq.respectTransparency.types false in
 theorem IterM.Equiv.liftInner_stepAsHetT_pbind_congr [Monad m] [LawfulMonad m]
     [Monad n] [LawfulMonad n]
     [MonadLiftT m n] [LawfulMonadLiftT m n] [Iterator α₁ m β] [Iterator α₂ m β]
diff --git a/src/Std/Data/Iterators/Lemmas/Producers/Monadic/Array.lean b/src/Std/Data/Iterators/Lemmas/Producers/Monadic/Array.lean
index 277f0947022a..ee41fc51db27 100644
--- a/src/Std/Data/Iterators/Lemmas/Producers/Monadic/Array.lean
+++ b/src/Std/Data/Iterators/Lemmas/Producers/Monadic/Array.lean
@@ -53,7 +53,6 @@ theorem Array.step_iterM {array : Array β} :
 
 section Equivalence
 
-set_option backward.isDefEq.respectTransparency.types false in
 theorem Std.Iterators.Types.ArrayIterator.stepAsHetT_iterFromIdxM [LawfulMonad m] {array : Array β}
     {pos : Nat} :
     (array.iterFromIdxM m pos).stepAsHetT = (if _ : pos < array.size then
diff --git a/src/Std/Data/Iterators/Lemmas/Producers/Monadic/List.lean b/src/Std/Data/Iterators/Lemmas/Producers/Monadic/List.lean
index 4b3db1ebcbc0..e2a949d6178d 100644
--- a/src/Std/Data/Iterators/Lemmas/Producers/Monadic/List.lean
+++ b/src/Std/Data/Iterators/Lemmas/Producers/Monadic/List.lean
@@ -15,7 +15,6 @@ open Std.Internal Std.Iterators Std.Iterators.Types
 
 variable {m : Type w → Type w'} {n : Type w → Type w''} [Monad m] {β : Type w}
 
-set_option backward.isDefEq.respectTransparency.types false in
 -- We don't want to pollute `List` with this rarely used lemma.
 public theorem Types.ListIterator.stepAsHetT_iterM [LawfulMonad m] {l : List β} :
     (l.iterM m).stepAsHetT = (match l with
diff --git a/src/Std/Sat/AIG/Basic.lean b/src/Std/Sat/AIG/Basic.lean
index 71803618d516..830e377bb133 100644
--- a/src/Std/Sat/AIG/Basic.lean
+++ b/src/Std/Sat/AIG/Basic.lean
@@ -249,7 +249,7 @@ def Cache.get? (cache : Cache α decls) (decl : Decl α) : Option (CacheHit decl
 An `Array Decl` is a Direct Acyclic Graph (DAG) if a gate at index `i` only points to nodes with index lower than `i`.
 -/
 def IsDAG (α : Type) (decls : Array (Decl α)) : Prop :=
-  ∀ {i lhs rhs} (h : i < decls.size),
+  ∀ ⦃i lhs rhs⦄ (h : i < decls.size),
       decls[i] = .gate lhs rhs → lhs.gate < i ∧ rhs.gate < i
 
 /--
@@ -321,7 +321,7 @@ structure Ref (aig : AIG α) where
 /--
 A `Ref` into `aig1` is also valid for `aig2` if `aig1` is smaller than `aig2`.
 -/
-@[inline]
+@[inline, implicit_reducible]
 def Ref.cast {aig1 aig2 : AIG α} (ref : Ref aig1) (h : aig1.decls.size ≤ aig2.decls.size) :
     Ref aig2 :=
   { ref with hgate := by have := ref.hgate; omega }
@@ -534,7 +534,7 @@ def mkGate (aig : AIG α) (input : BinaryInput aig) : Entrypoint α :=
   let cache := aig.cache.noUpdate
   have hdag := by
     intro i lhs' rhs' h1 h2
-    simp only [Array.getElem_push] at h2
+    simp only [decls, Array.getElem_push] at h2
     split at h2
     · apply aig.hdag <;> assumption
     · injection h2 with hl hr
@@ -556,7 +556,7 @@ def mkAtom (aig : AIG α) (n : α) : Entrypoint α :=
   let cache := aig.cache.noUpdate
   have hdag := by
     intro i lhs rhs h1 h2
-    simp only [Array.getElem_push] at h2
+    simp only [decls, Array.getElem_push] at h2
     split at h2
     · apply aig.hdag <;> assumption
     · contradiction
@@ -574,7 +574,7 @@ def mkConst (aig : AIG α) (val : Bool) : Entrypoint α :=
   let cache := aig.cache.noUpdate
   have hdag := by
     intro i lhs rhs h1 h2
-    simp only [Array.getElem_push] at h2
+    simp only [decls, Array.getElem_push] at h2
     split at h2
     · apply aig.hdag <;> assumption
     · contradiction
diff --git a/src/Std/Sat/AIG/Cached.lean b/src/Std/Sat/AIG/Cached.lean
index bbeab847c7f5..f88e0f42444a 100644
--- a/src/Std/Sat/AIG/Cached.lean
+++ b/src/Std/Sat/AIG/Cached.lean
@@ -40,7 +40,7 @@ def mkAtomCached (aig : AIG α) (n : α) : Entrypoint α :=
     let decls := decls.push decl
     have hdag := by
       intro i lhs rhs h1 h2
-      simp only [Array.getElem_push] at h2
+      simp only [decls, Array.getElem_push] at h2
       split at h2
       · apply hdag <;> assumption
       · contradiction
@@ -116,7 +116,7 @@ where
           let decls := decls.push decl
           have hdag := by
             intro i lhs rhs h1 h2
-            simp only [Array.getElem_push] at h2
+            simp only [decls, Array.getElem_push] at h2
             simp_all
             split at h2
             · apply hdag <;> assumption
diff --git a/src/Std/Sat/AIG/CachedLemmas.lean b/src/Std/Sat/AIG/CachedLemmas.lean
index c8f9dd5509e2..ddef402dad09 100644
--- a/src/Std/Sat/AIG/CachedLemmas.lean
+++ b/src/Std/Sat/AIG/CachedLemmas.lean
@@ -25,7 +25,6 @@ namespace AIG
 
 variable {α : Type} [Hashable α] [DecidableEq α]
 
-set_option backward.isDefEq.respectTransparency.types false in
 /--
 If we find a cached atom declaration in the AIG, denoting it is equivalent to denoting `AIG.mkAtom`.
 -/
@@ -98,7 +97,6 @@ theorem mkAtomCached_eval_eq_mkAtom_eval {aig : AIG α} :
     rw [denote_mkAtom_cached heq1]
   · simp [mkAtom, denote]
 
-set_option backward.isDefEq.respectTransparency.types false in
 /--
 The central equality theorem between `mkConstCached` and `mkConst`.
 -/
@@ -112,7 +110,6 @@ theorem denote_mkConstCached {aig : AIG α} :
   next heq => simp [aig.hconst] at heq
   next heq => simp [aig.hconst] at heq
 
-set_option backward.isDefEq.respectTransparency.types false in
 /--
 If we find a cached gate declaration in the AIG, denoting it is equivalent to denoting `AIG.mkGate`.
 -/
diff --git a/src/Std/Sat/AIG/If.lean b/src/Std/Sat/AIG/If.lean
index 786473caf260..42dd2976533a 100644
--- a/src/Std/Sat/AIG/If.lean
+++ b/src/Std/Sat/AIG/If.lean
@@ -61,20 +61,17 @@ def mkIfCached (aig : AIG α) (input : TernaryInput aig) : Entrypoint α :=
     apply AIG.LawfulOperator.le_size (f := mkNotCached)
   aig.mkOrCached ⟨lhsRef, rhsRef⟩
 
-set_option backward.isDefEq.respectTransparency.types false in
 instance : LawfulOperator α TernaryInput mkIfCached where
   le_size := by
     intros
-    unfold mkIfCached
-    dsimp only
+    simp only [mkIfCached]
     apply LawfulOperator.le_size_of_le_aig_size (f := mkOrCached)
     apply LawfulOperator.le_size_of_le_aig_size (f := mkAndCached)
     apply LawfulOperator.le_size_of_le_aig_size (f := mkNotCached)
     apply LawfulOperator.le_size (f := mkAndCached)
   decl_eq := by
     intros
-    unfold mkIfCached
-    dsimp only
+    simp only [mkIfCached]
     rw [LawfulOperator.decl_eq (f := mkOrCached)]
     rw [LawfulOperator.decl_eq (f := mkAndCached)]
     rw [LawfulOperator.decl_eq (f := mkNotCached)]
@@ -93,25 +90,27 @@ theorem if_as_bool (d l r : Bool) : (if d then l else r) = ((d && l) || (!d && r
   revert d l r
   decide
 
-set_option backward.isDefEq.respectTransparency.types false in
 @[simp]
 theorem denote_mkIfCached {aig : AIG α} {input : TernaryInput aig} :
     ⟦aig.mkIfCached input, assign⟧
       =
     if ⟦aig, input.discr, assign⟧ then ⟦aig, input.lhs, assign⟧ else ⟦aig, input.rhs, assign⟧ := by
   rw [if_as_bool]
-  unfold mkIfCached
-  dsimp only
-  simp only [TernaryInput.cast, Ref.cast_eq, denote_mkOrCached,
-    denote_projected_entry, denote_mkAndCached, denote_mkNotCached]
+  simp only [mkIfCached]
+  simp only [TernaryInput.cast, Ref.cast_eq, Ref.cast, denote_mkOrCached, denote_projected_entry,
+    denote_mkAndCached, denote_mkNotCached]
   congr 2
-  · rw [LawfulOperator.denote_mem_prefix (LawfulOperator.lt_size ..)]
+  · rw [LawfulOperator.denote_mem_prefix]
     rw [LawfulOperator.denote_mem_prefix]
     · simp
     · simp [Ref.hgate]
+    · apply LawfulOperator.lt_size_of_lt_aig_size (f := mkNotCached)
+      simp [Ref.hgate]
+  · rw [LawfulOperator.denote_mem_prefix]
   · rw [LawfulOperator.denote_mem_prefix]
-  · rw [LawfulOperator.denote_mem_prefix (LawfulOperator.lt_size_of_lt_aig_size _ _ input.rhs.hgate)]
     rw [LawfulOperator.denote_mem_prefix]
+    · apply LawfulOperator.lt_size_of_lt_aig_size (f := mkAndCached)
+      simp [Ref.hgate]
 
 namespace RefVec
 
@@ -175,7 +174,6 @@ termination_by w - curr
 
 end ite
 
-set_option backward.isDefEq.respectTransparency.types false in
 instance : LawfulVecOperator α IfInput ite where
   le_size := by
     intros
@@ -183,7 +181,7 @@ instance : LawfulVecOperator α IfInput ite where
     apply ite.go_le_size
   decl_eq := by
     intros
-    unfold ite
+    simp only [ite]
     rw [ite.go_decl_eq]
 
 namespace ite
@@ -238,7 +236,6 @@ theorem go_denote_mem_prefix {w : Nat} (aig : AIG α) (curr : Nat) (hcurr : curr
   · intros
     apply go_le_size
 
-set_option backward.isDefEq.respectTransparency.types false in
 theorem denote_go {w : Nat} (aig : AIG α) (curr : Nat) (hcurr : curr ≤ w) (discr : Ref aig)
     (lhs rhs : RefVec aig w) (s : RefVec aig curr) :
     ∀ (idx : Nat) (hidx1 : idx < w),
@@ -257,7 +254,7 @@ theorem denote_go {w : Nat} (aig : AIG α) (curr : Nat) (hcurr : curr ≤ w) (di
   intro idx hidx1 hidx2
   generalize hgo : go aig curr hcurr discr lhs rhs s = res
   unfold go at hgo
-  dsimp only at hgo
+  simp only at hgo
   split at hgo
   · cases Nat.eq_or_lt_of_le hidx2 with
     | inl heq =>
@@ -266,8 +263,8 @@ theorem denote_go {w : Nat} (aig : AIG α) (curr : Nat) (hcurr : curr ≤ w) (di
       rw [go_get]; case hidx => omega
       rw [AIG.RefVec.get_push_ref_eq']
       · rw [go_denote_mem_prefix]
-        · simp
-        · simp [Ref.hgate]
+        · simp [Ref.cast]
+        · simp [Ref.cast, Ref.hgate]
       · omega
     | inr heq =>
       rw [← hgo]
diff --git a/src/Std/Sat/AIG/Lemmas.lean b/src/Std/Sat/AIG/Lemmas.lean
index 92725b5b6fb5..e473093e8f61 100644
--- a/src/Std/Sat/AIG/Lemmas.lean
+++ b/src/Std/Sat/AIG/Lemmas.lean
@@ -116,7 +116,6 @@ instance : LawfulOperator α BinaryInput mkGate where
     intros
     apply mkGate_decl_eq
 
-set_option backward.isDefEq.respectTransparency.types false in
 @[simp]
 theorem denote_mkGate {aig : AIG α} {input : BinaryInput aig} :
     ⟦aig.mkGate input, assign⟧
@@ -164,7 +163,6 @@ instance : LawfulOperator α (fun _ => α) mkAtom where
     intros
     apply mkAtom_decl_eq
 
-set_option backward.isDefEq.respectTransparency.types false in
 @[simp]
 theorem denote_mkAtom {aig : AIG α} :
     ⟦(aig.mkAtom var), assign⟧ = assign var := by
@@ -205,7 +203,6 @@ instance : LawfulOperator α (fun _ => Bool) mkConst where
     intros
     apply mkConst_decl_eq
 
-set_option backward.isDefEq.respectTransparency.types false in
 @[simp]
 theorem denote_mkConst {aig : AIG α} : ⟦(aig.mkConst val), assign⟧ = val := by
   unfold denote denote.go
@@ -220,7 +217,6 @@ theorem denote_mkConst {aig : AIG α} : ⟦(aig.mkConst val), assign⟧ = val :=
     rw [mkConst, Array.getElem_push_eq] at heq
     contradiction
 
-set_option backward.isDefEq.respectTransparency.types false in
 /--
 If an index contains a `Decl.false` we know how to denote it.
 -/
@@ -229,7 +225,6 @@ theorem denote_idx_false {aig : AIG α} {hstart} (h : aig.decls[start]'hstart =
   unfold denote denote.go
   split <;> simp_all
 
-set_option backward.isDefEq.respectTransparency.types false in
 /--
 If an index contains a `Decl.atom` we know how to denote it.
 -/
@@ -238,7 +233,6 @@ theorem denote_idx_atom {aig : AIG α} {hstart} (h : aig.decls[start] = .atom a)
   unfold denote denote.go
   split <;> simp_all
 
-set_option backward.isDefEq.respectTransparency.types false in
 /--
 If an index contains a `Decl.gate` we know how to denote it.
 -/
diff --git a/src/Std/Sat/AIG/RefVec.lean b/src/Std/Sat/AIG/RefVec.lean
index a5a46eddd13d..577d20ce8811 100644
--- a/src/Std/Sat/AIG/RefVec.lean
+++ b/src/Std/Sat/AIG/RefVec.lean
@@ -34,7 +34,7 @@ def emptyWithCapacity (c : Nat) : RefVec aig 0 where
 theorem emptyWithCapacity_eq : emptyWithCapacity (aig := aig) c = empty := by
   rfl
 
-@[inline]
+@[inline, implicit_reducible]
 def cast' {aig1 aig2 : AIG α} (s : RefVec aig1 len)
     (h :
       (∀ {i : Nat} (h : i < len), s.refs[i].gate < aig1.decls.size)
@@ -48,7 +48,7 @@ def cast' {aig1 aig2 : AIG α} (s : RefVec aig1 len)
       apply s.hrefs
   }
 
-@[inline]
+@[inline, implicit_reducible]
 def cast {aig1 aig2 : AIG α} (s : RefVec aig1 len) (h : aig1.decls.size ≤ aig2.decls.size) :
     RefVec aig2 len :=
   s.cast' <| by
@@ -107,7 +107,7 @@ theorem get_cast {aig1 aig2 : AIG α} (s : RefVec aig1 len) (idx : Nat) (hidx :
     (s.cast hcast).get idx hidx
       =
     (s.get idx hidx).cast hcast := by
-  simp [cast, cast', get]
+  simp [get]
 
 @[inline]
 def append (lhs : RefVec aig lw) (rhs : RefVec aig rw) : RefVec aig (lw + rw) :=
diff --git a/src/Std/Sat/AIG/RefVecOperator/Fold.lean b/src/Std/Sat/AIG/RefVecOperator/Fold.lean
index f6c19ebb93bc..f1734354b02a 100644
--- a/src/Std/Sat/AIG/RefVecOperator/Fold.lean
+++ b/src/Std/Sat/AIG/RefVecOperator/Fold.lean
@@ -82,7 +82,6 @@ theorem fold.go_decl_eq {aig : AIG α} (acc : Ref aig) (i : Nat) (s : RefVec aig
     simp
 termination_by len - i
 
-set_option backward.isDefEq.respectTransparency.types false in
 theorem fold_decl_eq {aig : AIG α} (vec : RefVec aig len)
     (func : (aig : AIG α) → BinaryInput aig → Entrypoint α) [LawfulOperator α BinaryInput func] :
     ∀ idx (h1 : idx < aig.decls.size) (h2),
@@ -90,8 +89,7 @@ theorem fold_decl_eq {aig : AIG α} (vec : RefVec aig len)
         =
       aig.decls[idx]'h1 := by
   intros
-  unfold fold
-  dsimp only
+  simp only [fold]
   rw [fold.go_decl_eq]
 
 theorem fold_lt_size_of_lt_aig_size (aig : AIG α) (vec : RefVec aig len)
diff --git a/src/Std/Sat/AIG/RelabelNat.lean b/src/Std/Sat/AIG/RelabelNat.lean
index 4cdc43aba1e2..f2f586ee19a0 100644
--- a/src/Std/Sat/AIG/RelabelNat.lean
+++ b/src/Std/Sat/AIG/RelabelNat.lean
@@ -331,10 +331,9 @@ theorem relabelNat'_fst_eq_relabelNat {aig : AIG α} : aig.relabelNat'.fst = aig
 theorem relabelNat_size_eq_size {aig : AIG α} : aig.relabelNat.decls.size = aig.decls.size := by
   simp [relabelNat, relabelNat']
 
-set_option backward.isDefEq.respectTransparency.types false in
 theorem relabelNat_unsat_iff_of_NonEmpty [Nonempty α] {aig : AIG α} {hidx1} {hidx2} :
     (aig.relabelNat).UnsatAt idx invert hidx1 ↔ aig.UnsatAt idx invert hidx2 := by
-  dsimp only [relabelNat, relabelNat']
+  simp only [relabelNat, relabelNat']
   rw [relabel_unsat_iff]
   intro x y hx hy heq
   split at heq
diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Carry.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Carry.lean
index ec3bc90f0baa..98c02fdb457a 100644
--- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Carry.lean
+++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Carry.lean
@@ -82,17 +82,14 @@ theorem go_decl_eq {aig : AIG α} {cin} {lhs rhs : AIG.RefVec aig w} :
   · simp [← hgo]
 termination_by w - curr
 
-set_option backward.isDefEq.respectTransparency.types false in
 instance : AIG.LawfulOperator α OverflowInput mkOverflowBit where
   le_size := by
     intros
-    unfold mkOverflowBit
-    dsimp only
+    simp only [mkOverflowBit]
     apply go_le_size
   decl_eq := by
     intros
-    unfold mkOverflowBit
-    dsimp only
+    simp only [mkOverflowBit]
     rw [go_decl_eq]
 
 end mkOverflowBit
diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Add.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Add.lean
index d13b63a78578..cb7b95e6449d 100644
--- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Add.lean
+++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Add.lean
@@ -71,18 +71,15 @@ def mkFullAdderOut (aig : AIG α) (input : FullAdderInput aig) : AIG.Entrypoint
   let cin := cin.cast <| AIG.LawfulOperator.le_size (f := AIG.mkXorCached) ..
   aig.mkXorCached ⟨subExprRef, cin⟩
 
-set_option backward.isDefEq.respectTransparency.types false in
 instance : AIG.LawfulOperator α FullAdderInput mkFullAdderOut where
   le_size := by
     intros
-    unfold mkFullAdderOut
-    dsimp only
+    simp only [mkFullAdderOut]
     apply AIG.LawfulOperator.le_size_of_le_aig_size
     apply AIG.LawfulOperator.le_size
   decl_eq := by
     intros
-    unfold mkFullAdderOut
-    dsimp only
+    simp only [mkFullAdderOut]
     rw [AIG.LawfulOperator.decl_eq]
     rw [AIG.LawfulOperator.decl_eq]
     apply AIG.LawfulOperator.lt_size_of_lt_aig_size
@@ -114,12 +111,10 @@ def mkFullAdderCarry (aig : AIG α) (input : FullAdderInput aig) : AIG.Entrypoin
   let lorRef := lorRef.cast hror
   aig.mkOrCached ⟨lorRef, rorRef⟩
 
-set_option backward.isDefEq.respectTransparency.types false in
 instance : AIG.LawfulOperator α FullAdderInput mkFullAdderCarry where
   le_size := by
     intros
-    unfold mkFullAdderCarry
-    dsimp only
+    simp only [mkFullAdderCarry]
     apply AIG.LawfulOperator.le_size_of_le_aig_size (f := AIG.mkOrCached)
     apply AIG.LawfulOperator.le_size_of_le_aig_size (f := AIG.mkAndCached)
     apply AIG.LawfulOperator.le_size_of_le_aig_size (f := AIG.mkAndCached)
@@ -127,8 +122,7 @@ instance : AIG.LawfulOperator α FullAdderInput mkFullAdderCarry where
 
   decl_eq := by
     intros
-    unfold mkFullAdderCarry
-    dsimp only
+    simp only [mkFullAdderCarry]
     rw [AIG.LawfulOperator.decl_eq]
     rw [AIG.LawfulOperator.decl_eq]
     rw [AIG.LawfulOperator.decl_eq]
@@ -214,7 +208,6 @@ theorem go_le_size (aig : AIG α) (curr : Nat) (hcurr : curr ≤ w) (cin : AIG.R
   · simp
 termination_by w - curr
 
-set_option backward.isDefEq.respectTransparency.types false in
 theorem go_decl_eq (aig : AIG α) (curr : Nat) (hcurr : curr ≤ w) (cin : AIG.Ref aig)
     (s : AIG.RefVec aig curr) (lhs rhs : AIG.RefVec aig w) :
     ∀ (idx : Nat) (h1) (h2),
@@ -233,23 +226,20 @@ theorem go_decl_eq (aig : AIG α) (curr : Nat) (hcurr : curr ≤ w) (cin : AIG.R
       apply AIG.LawfulOperator.lt_size_of_lt_aig_size
       exact h3
     rw [go_decl_eq (w := w) (curr := curr + 1) (h1 := h4)]
-    unfold mkFullAdder
+    simp only [mkFullAdder]
     rw [AIG.LawfulOperator.decl_eq (f := mkFullAdderCarry) (h1 := h3)]
     rw [AIG.LawfulOperator.decl_eq (f := mkFullAdderOut)]
   · simp [← hgo]
 termination_by w - curr
 
-set_option backward.isDefEq.respectTransparency.types false in
 instance : AIG.LawfulVecOperator α AIG.BinaryRefVec blast where
   le_size := by
     intros
-    unfold blast
-    dsimp only
+    simp only [blast]
     apply go_le_size
   decl_eq := by
     intros
-    unfold blast
-    dsimp only
+    simp only [blast]
     rw [go_decl_eq]
 
 end blastAdd
diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Cpop.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Cpop.lean
index 3e386ca4f30e..802aacbbd33a 100644
--- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Cpop.lean
+++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Cpop.lean
@@ -48,19 +48,16 @@ def blastExtractAndExtendBit (aig : AIG α) (target : ExtractAndExtendBitTarget
   let extend := res.vec
   ⟨aig, extend⟩
 
-set_option backward.isDefEq.respectTransparency.types false in
 instance : AIG.LawfulVecOperator α ExtractAndExtendBitTarget blastExtractAndExtendBit where
   le_size := by
     intros
-    unfold blastExtractAndExtendBit
-    dsimp only
+    simp only [blastExtractAndExtendBit]
     apply AIG.LawfulVecOperator.le_size_of_le_aig_size (f := blastZeroExtend)
     apply AIG.LawfulVecOperator.le_size_of_le_aig_size (f := blastExtract)
     omega
   decl_eq := by
     intros
-    unfold blastExtractAndExtendBit
-    dsimp only
+    simp only [blastExtractAndExtendBit]
     rw [AIG.LawfulVecOperator.decl_eq (f := blastZeroExtend),
       AIG.LawfulVecOperator.decl_eq (f := blastExtract)]
     apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size
diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Eq.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Eq.lean
index 744fb4c2ba73..44d0f8777bd0 100644
--- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Eq.lean
+++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Eq.lean
@@ -28,18 +28,15 @@ def mkEq (aig : AIG α) (pair : AIG.BinaryRefVec aig w) : AIG.Entrypoint α :=
   let bits := res.vec
   AIG.RefVec.fold aig bits AIG.mkAndCached
 
-set_option backward.isDefEq.respectTransparency.types false in
 instance {w : Nat} : AIG.LawfulOperator α (AIG.BinaryRefVec · w) mkEq where
   le_size := by
     intros
-    unfold mkEq
-    dsimp only
+    simp only [mkEq]
     apply AIG.RefVec.fold_le_size_of_le_aig_size
     apply AIG.RefVec.zip_le_size
   decl_eq := by
     intros
-    unfold mkEq
-    dsimp only
+    simp only [mkEq]
     rw [AIG.RefVec.fold_decl_eq]
     rw [AIG.RefVec.zip_decl_eq]
     apply AIG.RefVec.zip_lt_size_of_lt_aig_size
diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Neg.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Neg.lean
index 73ab200c397c..4445744b88a9 100644
--- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Neg.lean
+++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Neg.lean
@@ -34,18 +34,15 @@ def blastNeg (aig : AIG α) (input : AIG.RefVec aig w) : AIG.RefVecEntry α w :=
 
   blastAdd aig ⟨notInput, one⟩
 
-set_option backward.isDefEq.respectTransparency.types false in
 instance : AIG.LawfulVecOperator α AIG.RefVec blastNeg where
   le_size := by
     intros
-    unfold blastNeg
-    dsimp only
+    simp only [blastNeg]
     apply AIG.LawfulVecOperator.le_size_of_le_aig_size (f := blastAdd)
     apply AIG.LawfulVecOperator.le_size (f := blastNot)
   decl_eq := by
     intros
-    unfold blastNeg
-    dsimp only
+    simp only [blastNeg]
     rw [AIG.LawfulVecOperator.decl_eq (f := blastAdd)]
     rw [AIG.LawfulVecOperator.decl_eq (f := blastNot)]
     · apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastNot)
diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Sub.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Sub.lean
index 233d69714cdc..8020b8d1a24d 100644
--- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Sub.lean
+++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Sub.lean
@@ -32,16 +32,15 @@ def blastSub (aig : AIG α) (input : AIG.BinaryRefVec aig w) : AIG.RefVecEntry 
 
   blastAdd aig ⟨lhs, negRhs⟩
 
-set_option backward.isDefEq.respectTransparency.types false in
 instance : AIG.LawfulVecOperator α AIG.BinaryRefVec blastSub where
   le_size := by
     intros
-    unfold blastSub
+    simp only [blastSub]
     apply AIG.LawfulVecOperator.le_size_of_le_aig_size (f := blastAdd)
     apply AIG.LawfulVecOperator.le_size (f := blastNeg)
   decl_eq := by
     intros
-    unfold blastSub
+    simp only [blastSub]
     rw [AIG.LawfulVecOperator.decl_eq (f := blastAdd)]
     rw [AIG.LawfulVecOperator.decl_eq (f := blastNeg)]
     apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastNeg)
diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Udiv.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Udiv.lean
index c567f340d89c..39e640013276 100644
--- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Udiv.lean
+++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Udiv.lean
@@ -41,17 +41,14 @@ def blastShiftConcat (aig : AIG α) (input : ShiftConcatInput aig w) : AIG.RefVe
   let new := bit.append lhs
   blastZeroExtend aig ⟨1 + w, new⟩
 
-set_option backward.isDefEq.respectTransparency.types false in
 instance : AIG.LawfulVecOperator α ShiftConcatInput blastShiftConcat where
   le_size := by
     intros
-    unfold blastShiftConcat
-    dsimp only
+    simp only [blastShiftConcat]
     apply AIG.LawfulVecOperator.le_size (f := blastZeroExtend)
   decl_eq := by
     intros
-    unfold blastShiftConcat
-    dsimp only
+    simp only [blastShiftConcat]
     rw [AIG.LawfulVecOperator.decl_eq (f := blastZeroExtend)]
 
 structure BlastDivSubtractShiftOutput (old : AIG α) (w : Nat) where
@@ -277,17 +274,16 @@ def blastUdiv (aig : AIG α) (input : AIG.BinaryRefVec aig w) : AIG.RefVecEntry
 
   AIG.RefVec.ite aig ⟨discr, zero, divRes⟩
 
-set_option backward.isDefEq.respectTransparency.types false in
 instance : AIG.LawfulVecOperator α AIG.BinaryRefVec blastUdiv where
   le_size := by
     intros
-    unfold blastUdiv
+    simp only [blastUdiv]
     apply AIG.LawfulVecOperator.le_size_of_le_aig_size (f := AIG.RefVec.ite)
     refine Nat.le_trans ?_ (by apply blastUdiv.go_le_size)
     apply AIG.LawfulOperator.le_size (f := BVPred.mkEq)
   decl_eq := by
     intros
-    unfold blastUdiv
+    simp only [blastUdiv]
     rw [AIG.LawfulVecOperator.decl_eq (f := AIG.RefVec.ite)]
     rw [blastUdiv.go_decl_eq]
     rw [AIG.LawfulOperator.decl_eq (f := BVPred.mkEq)]
diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Ult.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Ult.lean
index d37b11fdbb86..f73e91e9db5c 100644
--- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Ult.lean
+++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Ult.lean
@@ -38,19 +38,16 @@ def mkUlt (aig : AIG α) (pair : AIG.BinaryRefVec aig w) : AIG.Entrypoint α :=
   let overflowRef := res.ref
   aig.mkNotCached overflowRef
 
-set_option backward.isDefEq.respectTransparency.types false in
 instance {w : Nat} : AIG.LawfulOperator α (AIG.BinaryRefVec · w) mkUlt where
   le_size := by
     intros
-    unfold mkUlt
-    dsimp only
+    simp only [mkUlt]
     apply AIG.LawfulOperator.le_size_of_le_aig_size (f := AIG.mkNotCached)
     apply AIG.LawfulOperator.le_size_of_le_aig_size (f := BVExpr.bitblast.mkOverflowBit)
     apply AIG.LawfulVecOperator.le_size (f := BVExpr.bitblast.blastNot)
   decl_eq := by
     intros
-    unfold mkUlt
-    dsimp only
+    simp only [mkUlt]
     rw [AIG.LawfulOperator.decl_eq (f := AIG.mkNotCached)]
     rw [AIG.LawfulOperator.decl_eq (f := BVExpr.bitblast.mkOverflowBit)]
     rw [AIG.LawfulVecOperator.decl_eq (f := BVExpr.bitblast.blastNot)]
diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Umod.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Umod.lean
index c0aafda3fc15..b37b8daf38d9 100644
--- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Umod.lean
+++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Umod.lean
@@ -45,17 +45,16 @@ def blastUmod (aig : AIG α) (input : AIG.BinaryRefVec aig w) : AIG.RefVecEntry
 
   AIG.RefVec.ite aig ⟨discr, lhs, modRes⟩
 
-set_option backward.isDefEq.respectTransparency.types false in
 instance : AIG.LawfulVecOperator α AIG.BinaryRefVec blastUmod where
   le_size := by
     intros
-    unfold blastUmod
+    simp only [blastUmod]
     apply AIG.LawfulVecOperator.le_size_of_le_aig_size (f := AIG.RefVec.ite)
     refine Nat.le_trans ?_ (by apply blastUdiv.go_le_size)
     apply AIG.LawfulOperator.le_size (f := BVPred.mkEq)
   decl_eq := by
     intros
-    unfold blastUmod
+    simp only [blastUmod]
     rw [AIG.LawfulVecOperator.decl_eq (f := AIG.RefVec.ite)]
     rw [blastUdiv.go_decl_eq]
     rw [AIG.LawfulOperator.decl_eq (f := BVPred.mkEq)]
diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Pred.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Pred.lean
index e690055e87e8..e77c8c840a5a 100644
--- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Pred.lean
+++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Pred.lean
@@ -62,12 +62,11 @@ def bitblast (aig : AIG BVBit) (input : BVExpr.WithCache BVPred aig) : Return ai
     let res := blastGetLsbD aig ⟨refs, idx⟩
     ⟨⟨⟨aig, res⟩, hrefs⟩, cache⟩
 
-set_option backward.isDefEq.respectTransparency.types false in
 theorem bitblast_decl_eq (aig : AIG BVBit) (input : BVExpr.WithCache BVPred aig) :
     ∀ (idx : Nat) (h1) (h2), (bitblast aig input).result.val.aig.decls[idx]'h2 = aig.decls[idx]'h1 := by
   intro idx h1 h2
   rcases input with ⟨pred, cache⟩
-  unfold BVPred.bitblast
+  simp only [BVPred.bitblast]
   cases pred with
   | bin lhs op rhs =>
     cases op with
diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Expr.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Expr.lean
index 8a0e4130eb7d..102b1e7e0e63 100644
--- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Expr.lean
+++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Expr.lean
@@ -60,7 +60,6 @@ theorem Inv_cast (cache : Cache aig1) (hpref : IsPrefix aig1.decls aig2.decls)
   apply denote.eq_of_isPrefix (entry := ⟨aig1, _, _, _⟩)
   exact hpref
 
-set_option backward.isDefEq.respectTransparency.types false in
 theorem Inv_insert (cache : Cache aig) (expr : BVExpr w) (refs : AIG.RefVec aig w)
     (hinv : Inv assign aig cache)
     (hrefs : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, refs.get idx hidx, assign.toAIGAssignment⟧ = (expr.eval assign).getLsbD idx) :
@@ -88,7 +87,7 @@ theorem Inv_insert (cache : Cache aig) (expr : BVExpr w) (refs : AIG.RefVec aig
       · exact hk
       · simp [heq]
     have : ((cache.insert expr refs).map.get k hk) = cache.map.get k hmem := by
-      unfold Cache.insert
+      simp only [Cache.insert]
       rw [Std.DHashMap.get_insert]
       simp [heq]
     specialize hinv k hmem i hi
diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Add.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Add.lean
index 279f87c35259..c4b3e755090b 100644
--- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Add.lean
+++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Add.lean
@@ -39,7 +39,6 @@ theorem denote_mkFullAdderOut (assign : α → Bool) (aig : AIG α) (input : Ful
     ]
   rw [LawfulOperator.denote_mem_prefix (f := mkXorCached)]
 
-set_option backward.isDefEq.respectTransparency.types false in
 @[simp]
 theorem denote_mkFullAdderCarry (assign : α → Bool) (aig : AIG α) (input : FullAdderInput aig) :
     ⟦mkFullAdderCarry aig input, assign⟧
@@ -139,7 +138,6 @@ theorem atLeastTwo_eq_halfAdder (lhsBit rhsBit carry : Bool) :
   revert lhsBit rhsBit carry
   decide
 
-set_option backward.isDefEq.respectTransparency.types false in
 theorem go_denote_eq (aig : AIG α) (curr : Nat) (hcurr : curr ≤ w) (cin : Ref aig)
     (s : AIG.RefVec aig curr) (lhs rhs : AIG.RefVec aig w) (assign : α → Bool)
     (lhsExpr rhsExpr : BitVec w)
diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Cpop.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Cpop.lean
index 5791aaad99c9..d1812ff62631 100644
--- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Cpop.lean
+++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Cpop.lean
@@ -140,7 +140,6 @@ theorem denote_blastExtractAndExtend (assign : α → Bool) (aig : AIG α) (w :
   · simp
   · exact hx
 
-set_option backward.isDefEq.respectTransparency.types false in
 theorem denote_blastCpopLayer.go (aig : AIG α) (iterNum : Nat)
     (oldLayer : AIG.RefVec aig (len * w)) (newLayer : AIG.RefVec aig (iterNum * w))
     (oldLayerBv : BitVec (len * w)) (hold' : 2 * (iterNum - 1) < len)
diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Udiv.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Udiv.lean
index a3c36fc4c358..ca7efc24217d 100644
--- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Udiv.lean
+++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Udiv.lean
@@ -79,7 +79,6 @@ theorem blastDivSubtractShift_denote_mem_prefix (aig : AIG α)
   · intros
     apply blastDivSubtractShift_le_size
 
-set_option backward.isDefEq.respectTransparency.types false in
 theorem denote_blastDivSubtractShift_q (aig : AIG α) (assign : α → Bool) (lhs rhs : BitVec w)
     (n d : AIG.RefVec aig w) (wn wr : Nat)
     (q r : AIG.RefVec aig w) (qbv rbv : BitVec w)
@@ -174,7 +173,6 @@ theorem denote_blastDivSubtractShift_q (aig : AIG α) (assign : α → Bool) (lh
       · rw [denote_mkConstCached]
   . simp [Ref.hgate]
 
-set_option backward.isDefEq.respectTransparency.types false in
 theorem denote_blastDivSubtractShift_r (aig : AIG α) (assign : α → Bool) (lhs rhs : BitVec w)
     (n d : AIG.RefVec aig w) (wn wr : Nat)
     (q r : AIG.RefVec aig w) (qbv rbv : BitVec w)
diff --git a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddSound.lean b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddSound.lean
index 935d1da27ec4..43d58f8f9d55 100644
--- a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddSound.lean
+++ b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddSound.lean
@@ -66,7 +66,7 @@ theorem entails_of_irrelevant_assignment {n : Nat} {p : (PosFin n) → Bool} {c
     · simp [Clause.toList, delete_iff, negl_ne_v, v_in_c_del_l]
     · grind
 
-set_option backward.isDefEq.respectTransparency.types false in
+open Classical in
 theorem assignmentsInvariant_insertRatUnits {n : Nat} (f : DefaultFormula n)
     (hf : f.ratUnits = #[] ∧ AssignmentsInvariant f) (units : CNF.Clause (PosFin n)) :
     AssignmentsInvariant (insertRatUnits f units).1 := by
@@ -76,13 +76,13 @@ theorem assignmentsInvariant_insertRatUnits {n : Nat} (f : DefaultFormula n)
   intro i b hb p hp
   simp only [(· ⊨ ·), Clause.eval] at hp
   simp only [toList, List.append_assoc,
-    List.any_eq_true, Prod.exists, Bool.exists_bool, Bool.decide_coe,
+    List.any_eq_true, Prod.exists, Bool.exists_bool, decide_eq_true_eq,
     List.all_eq_true, List.mem_append, List.mem_filterMap, id_eq, exists_eq_right, List.mem_map] at hp
   have pf : p ⊨ f := by
     simp only [(· ⊨ ·), Clause.eval]
     simp only [toList, List.append_assoc,
       List.any_eq_true, Prod.exists, Bool.exists_bool,
-      Bool.decide_coe, List.all_eq_true, List.mem_append, List.mem_filterMap, id_eq, exists_eq_right, List.mem_map]
+      decide_eq_true_eq, List.all_eq_true, List.mem_append, List.mem_filterMap, id_eq, exists_eq_right, List.mem_map]
     intro c cf
     rcases cf with cf | cf | cf
     · specialize hp c (Or.inl cf)
@@ -110,8 +110,7 @@ theorem assignmentsInvariant_insertRatUnits {n : Nat} (f : DefaultFormula n)
           constructor
           · have h1 : (insertRatUnits f units).fst.ratUnits[j] = (i, true) := by
               rw [hb'] at h1
-              simp only [h1, Prod.mk.injEq, and_true]
-              rfl
+              simp [h1]
             rw [← h1]
             apply Array.getElem_mem_toList
           · rfl
@@ -121,8 +120,7 @@ theorem assignmentsInvariant_insertRatUnits {n : Nat} (f : DefaultFormula n)
           constructor
           · have h1 : (insertRatUnits f units).fst.ratUnits[j] = (i, false) := by
               rw [hb'] at h1
-              simp only [h1, Prod.mk.injEq, and_true]
-              rfl
+              simp [h1]
             rw [← h1]
             apply Array.getElem_mem_toList
           · rfl
@@ -134,7 +132,7 @@ theorem assignmentsInvariant_insertRatUnits {n : Nat} (f : DefaultFormula n)
       rcases hp with ⟨hp1, hp2⟩ | ⟨hp1, hp2⟩
       · simp only [b_eq_b', ← hp1.2, (· ⊨ ·)]
         rw [hp1.1] at hp2
-        exact of_decide_eq_true hp2
+        exact hp2
       · simp only [b_eq_b', ← hp1.2, (· ⊨ ·)]
         rw [hp1.1] at hp2
         exact hp2
@@ -153,8 +151,6 @@ theorem assignmentsInvariant_insertRatUnits {n : Nat} (f : DefaultFormula n)
       constructor
       · have h1 : (insertRatUnits f units).fst.ratUnits[j1] = (i, true) := by
           rw [h1]
-          simp only [Prod.mk.injEq, and_true]
-          rfl
         rw [← h1]
         apply Array.getElem_mem_toList
       · rfl
@@ -169,8 +165,6 @@ theorem assignmentsInvariant_insertRatUnits {n : Nat} (f : DefaultFormula n)
       constructor
       · have h2 : (insertRatUnits f units).fst.ratUnits[j2] = (i, false) := by
           rw [h2]
-          simp only [Prod.mk.injEq, and_true]
-          rfl
         rw [← h2]
         apply Array.getElem_mem_toList
       · rfl
@@ -474,7 +468,7 @@ theorem performRatCheck_success_of_performRatCheck_fold_success {n : Nat} (f : D
   have h := (Array.foldl_induction motive h_base h_inductive).2 performRatCheck_fold_success i
   simpa [getElem!_def, i.2, dite_true] using h
 
-set_option backward.isDefEq.respectTransparency.types false in
+open Classical in
 theorem safe_insert_of_performRatCheck_fold_success {n : Nat} (f : DefaultFormula n)
     (f_readyForRatAdd : ReadyForRatAdd f) (c : DefaultClause n) (pivot : Literal (PosFin n))
     (rupHints : Array Nat) (ratHints : Array (Nat × Array Nat))
@@ -547,7 +541,7 @@ theorem safe_insert_of_performRatCheck_fold_success {n : Nat} (f : DefaultFormul
           apply h c' hc' p
           simp only [(· ⊨ ·), Clause.eval]
           simp only [List.any_eq_true, Prod.exists, Bool.exists_bool,
-            Bool.decide_coe, List.all_eq_true, decide_eq_true_eq]
+            decide_eq_true_eq, List.all_eq_true, decide_eq_true_eq]
           intro c'' hc''
           simp only [toList, clauses_performRupCheck, rupUnits_performRupCheck,
             ratUnits_performRupCheck] at hc''
@@ -571,8 +565,7 @@ theorem safe_insert_of_performRatCheck_fold_success {n : Nat} (f : DefaultFormul
               simp only [Bool.not_eq_true] at h
               assumption
           · simp only [(· ⊨ ·), Clause.eval] at pf
-            simp only [List.any_eq_true, Prod.exists, Bool.exists_bool, Bool.decide_coe, List.all_eq_true] at pf
-            simp only [Bool.decide_eq_false, Bool.not_eq_true'] at pf
+            simp only [List.any_eq_true, Prod.exists, Bool.exists_bool, decide_eq_true_eq, List.all_eq_true] at pf
             apply pf
             assumption
         have p'_entails_c'_del_negPivot : p' ⊨ c'.delete (Literal.negate pivot) := entails_of_irrelevant_assignment h
diff --git a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean
index ec7de2ec9f9e..2502155e370f 100644
--- a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean
+++ b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean
@@ -113,23 +113,22 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen
           ⟨units.size, units_size_lt_updatedUnits_size⟩
         have i_gt_zero : i.1 > 0 := by rw [i_eq_l]; exact l.1.2.1
         refine ⟨mostRecentUnitIdx, l.2, i_gt_zero, ?_⟩
-        simp +zetaDelta only [insertUnit, h3, ite_false, Array.getElem_push_eq, i_eq_l, reduceCtorEq]
+        simp +zetaDelta only [insertUnit, h3, ite_false, Array.getElem_push_eq, i_eq_l,
+          reduceCtorEq, true_and]
         constructor
-        · rfl
+        · grind
         · constructor
           · grind
-          · constructor
-            · grind
-            · intro k hk
-              have k_in_bounds : k.1 < units.size := by
-                apply Nat.lt_of_le_of_ne
-                · have k_property := k.2
-                  grind
-                · intro h
-                  simp only [← h, not_true] at hk
-              rw [Array.getElem_push_lt k_in_bounds]
-              rw [i_eq_l] at h2
-              exact h2 ⟨k.1, k_in_bounds⟩
+          · intro k hk
+            have k_in_bounds : k.1 < units.size := by
+              apply Nat.lt_of_le_of_ne
+              · have k_property := k.2
+                grind
+              · intro h
+                simp only [← h, not_true] at hk
+            rw [Array.getElem_push_lt k_in_bounds]
+            rw [i_eq_l] at h2
+            exact h2 ⟨k.1, k_in_bounds⟩
       next i_ne_l =>
         apply Or.inl
         simp only [insertUnit, h3, ite_false, reduceCtorEq]
@@ -185,7 +184,6 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen
           · rw [Array.getElem_push_lt j.2, h1]
           · constructor
             · simp +zetaDelta [i_eq_l, ← hl]
-              rfl
             · constructor
               · simp only [i_eq_l]
                 rw [Array.getElem_modify_self]
@@ -220,7 +218,6 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen
           simp only [insertUnit, h5, Bool.false_eq_true, ↓reduceIte, mostRecentUnitIdx]
           constructor
           · simp +zetaDelta [i_eq_l, ← hl]
-            rfl
           · constructor
             · rw [Array.getElem_push_lt j.2, h1]
             · constructor
@@ -522,13 +519,11 @@ theorem clear_insert_inductive_case {n : Nat} (f : DefaultFormula n) (f_assignme
               next h2 =>
                 have k_ne_j1 : k ≠ j1 := by grind
                 have h3 := units_nodup k j1 k_ne_j1
-                simp only [Fin.getElem_fin, ih1, ← h1, ← h2, ne_eq] at h3
-                exact h3 rfl
+                simp [ih1, ← h1, ← h2, ne_eq] at h3
               next h2 =>
                 have h3 := units_nodup k j2 k_ne_j2
                 simp only [Bool.not_eq_true] at h2
-                simp only [Fin.getElem_fin, ih2, ← h1, ← h2, ne_eq] at h3
-                exact h3 rfl
+                simp [ih2, ← h1, ← h2, ne_eq] at h3
     next idx_ne_j1 =>
       by_cases idx = j2
       next idx_eq_j2 =>
@@ -554,14 +549,12 @@ theorem clear_insert_inductive_case {n : Nat} (f : DefaultFormula n) (f_assignme
                 by_cases units[k.1].2
                 next h2 =>
                   have h3 := units_nodup k j1 k_ne_j1
-                  simp only [Fin.getElem_fin, ih1, ← h1, ← h2, ne_eq] at h3
-                  exact h3 rfl
+                  simp [Fin.getElem_fin, ih1, ← h1, ← h2, ne_eq] at h3
                 next h2 =>
                   have k_ne_j2 : k ≠ j2 := by grind
                   have h3 := units_nodup k j2 k_ne_j2
                   simp only [Bool.not_eq_true] at h2
-                  simp only [Fin.getElem_fin, ih2, ← h1, ← h2, ne_eq] at h3
-                  exact h3 rfl
+                  simp [ih2, ← h1, ← h2, ne_eq] at h3
       next idx_ne_j2 =>
         refine Or.inr <| Or.inr <| ⟨j1, j2,i_gt_zero, ?_⟩
         constructor
diff --git a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddSound.lean b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddSound.lean
index 78b94afc926c..aa6818c84921 100644
--- a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddSound.lean
+++ b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddSound.lean
@@ -232,7 +232,7 @@ theorem safe_insert_of_insertRup {n : Nat} (f : DefaultFormula n) (f_readyForRup
   · simp only [formulaEntails_def, List.all_eq_true, decide_eq_true_eq] at pf
     exact pf c' c'_in_f
 
-set_option backward.isDefEq.respectTransparency.types false in
+open Classical in
 theorem assignmentsInvariant_insertRupUnits_of_assignmentsInvariant {n : Nat} (f : DefaultFormula n) (f_readyForRupAdd : ReadyForRupAdd f)
     (units : CNF.Clause (PosFin n)) :
     AssignmentsInvariant (insertRupUnits f units).1 := by
@@ -242,12 +242,12 @@ theorem assignmentsInvariant_insertRupUnits_of_assignmentsInvariant {n : Nat} (f
   intro i b hb p hp
   simp only [(· ⊨ ·), Clause.eval] at hp
   simp only [toList, List.append_assoc, List.any_eq_true, Prod.exists,
-    Bool.exists_bool, Bool.decide_coe, List.all_eq_true, List.mem_append, List.mem_filterMap, id_eq,
-    exists_eq_right, List.mem_map] at hp
+    Bool.exists_bool, List.all_eq_true, List.mem_append, List.mem_filterMap, id_eq, exists_eq_right,
+    List.mem_map, decide_eq_true_eq] at hp
   have pf : p ⊨ f := by
     simp only [(· ⊨ ·), Clause.eval]
     simp only [toList, List.append_assoc, List.any_eq_true, Prod.exists, Bool.exists_bool,
-      Bool.decide_coe, List.all_eq_true, List.mem_append, List.mem_filterMap, id_eq, exists_eq_right, List.mem_map]
+      decide_eq_true_eq, List.all_eq_true, List.mem_append, List.mem_filterMap, id_eq, exists_eq_right, List.mem_map]
     intro c cf
     rcases cf with cf | cf | cf
     · specialize hp c (Or.inl cf)
@@ -276,8 +276,6 @@ theorem assignmentsInvariant_insertRupUnits_of_assignmentsInvariant {n : Nat} (f
           · have h1 : (insertRupUnits f units).fst.rupUnits[j] = (i, true) := by
               rw [hb'] at h1
               rw [h1]
-              simp only [Prod.mk.injEq, and_true]
-              rfl
             rw [← h1]
             apply Array.getElem_mem_toList
           · rfl
@@ -288,8 +286,6 @@ theorem assignmentsInvariant_insertRupUnits_of_assignmentsInvariant {n : Nat} (f
           · have h1 : (insertRupUnits f units).fst.rupUnits[j] = (i, false) := by
               rw [hb'] at h1
               rw [h1]
-              simp only [Prod.mk.injEq, and_true]
-              rfl
             rw [← h1]
             apply Array.getElem_mem_toList
           · rfl
@@ -302,7 +298,7 @@ theorem assignmentsInvariant_insertRupUnits_of_assignmentsInvariant {n : Nat} (f
       rcases hp with ⟨hp1, hp2⟩ | ⟨hp1, hp2⟩
       · simp only [b_eq_b', ← hp1.2, Entails.eval]
         rw [hp1.1] at hp2
-        exact of_decide_eq_true hp2
+        exact hp2
       · simp only [b_eq_b', ← hp1.2, Entails.eval]
         rw [hp1.1] at hp2
         exact hp2
@@ -322,8 +318,6 @@ theorem assignmentsInvariant_insertRupUnits_of_assignmentsInvariant {n : Nat} (f
       constructor
       · have h1 : (insertRupUnits f units).fst.rupUnits[j1] = (i, true) := by
           rw [h1]
-          simp only [Prod.mk.injEq, and_true]
-          rfl
         rw [← h1]
         apply Array.getElem_mem_toList
       · rfl
@@ -338,8 +332,6 @@ theorem assignmentsInvariant_insertRupUnits_of_assignmentsInvariant {n : Nat} (f
       constructor
       · have h2 : (insertRupUnits f units).fst.rupUnits[j2] = (i, false) := by
           rw [h2]
-          simp only [Prod.mk.injEq, and_true]
-          rfl
         rw [← h2]
         apply Array.getElem_mem_toList
       · rfl
@@ -351,9 +343,8 @@ theorem assignmentsInvariant_insertRupUnits_of_assignmentsInvariant {n : Nat} (f
     simp only [Fin.getElem_fin] at h1
     simp only [Fin.getElem_fin] at h2
     simp only [Clause.toList, h1, unit_eq, List.mem_cons, Prod.mk.injEq, Bool.false_eq_true,
-      and_false, List.not_mem_nil, or_self, Bool.decide_eq_false, Bool.not_eq_eq_eq_not,
-      Bool.not_true, false_and, and_true, or_false, false_or, h2, Bool.true_eq_false,
-      ] at hp1 hp2
+      and_false, List.not_mem_nil, or_self, false_and, and_true, or_false, false_or, h2,
+      Bool.true_eq_false] at hp1 hp2
     simp only [hp2.1, ← hp1.1, true_and] at hp2
     simp [hp1.2] at hp2
 
diff --git a/src/Std/Tactic/BVDecide/LRAT/Internal/PosFin.lean b/src/Std/Tactic/BVDecide/LRAT/Internal/PosFin.lean
index 1c6889b13eed..135a6bf022ef 100644
--- a/src/Std/Tactic/BVDecide/LRAT/Internal/PosFin.lean
+++ b/src/Std/Tactic/BVDecide/LRAT/Internal/PosFin.lean
@@ -14,19 +14,7 @@ namespace Std.Tactic.BVDecide
 namespace LRAT
 namespace Internal
 
-def PosFin (n : Nat) := {x : Nat // 0 < x ∧ x < n}
-
-instance : DecidableEq (PosFin n) :=
-  inferInstanceAs (DecidableEq {x : Nat // 0 < x ∧ x < n})
-
-instance : CoeOut (PosFin n) Nat where
-  coe p := p.val
-
-instance {n} : Hashable (PosFin n) where
-  hash p := hash p.val
-
-instance : ToString (PosFin n) where
-  toString p := toString p.val
+abbrev PosFin (n : Nat) := {x : Nat // 0 < x ∧ x < n}
 
 end Internal
 end LRAT
diff --git a/tests/elab/slice.lean b/tests/elab/slice.lean
index 321ad0c9a8e5..ca4b8965b425 100644
--- a/tests/elab/slice.lean
+++ b/tests/elab/slice.lean
@@ -48,8 +48,6 @@ example : #[1, 2, 3, 4, 5][1...*][*...=2].toList = [2, 3, 4] := by simp
 example : #[1, 2, 3, 4, 5][1...*][*...*].toList = [2, 3, 4, 5] := by simp
 example : #[1, 2, 3][0...2][*...*].toList = [1, 2] := by simp
 
-set_option backward.isDefEq.respectTransparency.types false -- FIXME
-
 example : #[1, 2, 3][0...2][1...2].toArray = #[2] := by simp
 example : #[1, 2, 3][0...2][1...5].toArray = #[2] := by simp
 example : #[1, 2, 3][1...2][0...2].toArray = #[2] := by simp