chore: fix tests

src/Init/Control/Lawful/Instances.lean

@@ -116,6 +116,7 @@ instance [Monad m] [LawfulMonad m] : LawfulMonad (ExceptT ε m) where
     ExceptT.run (liftWith f) = Except.ok <$> (f fun x => x.run) :=
   rfl
 
+set_option backward.isDefEq.respectTransparency false in
 @[simp] theorem run_controlAt [Monad m] [LawfulMonad m] (f : ({β : Type u} → ExceptT ε m β → m (stM m (ExceptT ε m) β)) → m (stM m (ExceptT ε m) α)) :
     ExceptT.run (controlAt m f) = f fun x => x.run := by
   simp [controlAt, run_bind, bind_map_left]
@@ -256,6 +257,7 @@ instance [Monad m] [LawfulMonad m] : LawfulMonad (OptionT m) where
   rw [← bind_pure_comp]
   rfl
 
+set_option backward.isDefEq.respectTransparency false in
 @[simp] theorem run_controlAt [Monad m] [LawfulMonad m] (f : ({β : Type u} → OptionT m β → m (stM m (OptionT m) β)) → m (stM m (OptionT m) α)) :
     OptionT.run (controlAt m f) = f fun x => x.run := by
   simp [controlAt, Option.elimM, Option.elim]
@@ -343,6 +345,7 @@ instance [Monad m] [LawfulMonad m] : LawfulMonad (ReaderT ρ m) where
     ReaderT.run (liftWith f) ctx = (f fun x => x.run ctx) :=
   rfl
 
+set_option backward.isDefEq.respectTransparency false in
 @[simp] theorem run_controlAt [Monad m] [LawfulMonad m] (f : ({β : Type u} → ReaderT ρ m β → m (stM m (ReaderT ρ m) β)) → m (stM m (ReaderT ρ m) α)) (ctx : ρ) :
     ReaderT.run (controlAt m f) ctx = f fun x => x.run ctx := by
   simp [controlAt]
@@ -443,6 +446,7 @@ instance [Monad m] [LawfulMonad m] : LawfulMonad (StateT σ m) where
     StateT.run (liftWith f) s = ((·, s) <$> f fun x => x.run s) := by
   simp [liftWith, MonadControl.liftWith, Function.comp_def]
 
+set_option backward.isDefEq.respectTransparency false in
 @[simp] theorem run_controlAt [Monad m] [LawfulMonad m] (f : ({β : Type u} → StateT σ m β → m (stM m (StateT σ m) β)) → m (stM m (StateT σ m) α)) (s : σ) :
     StateT.run (controlAt m f) s = f fun x => x.run s := by
   simp [controlAt]

src/Init/Control/Lawful/MonadAttach/Instances.lean

@@ -15,7 +15,8 @@ public import Init.Ext
 public instance [Monad m] [LawfulMonad m] [MonadAttach m] [WeaklyLawfulMonadAttach m] :
     WeaklyLawfulMonadAttach (ReaderT ρ m) where
   map_attach := by
-    simp only [Functor.map, MonadAttach.attach, Functor.map_map, WeaklyLawfulMonadAttach.map_attach]
+    simp only [Functor.map, MonadAttach.attach, Functor.map_map, WeaklyLawfulMonadAttach.map_attach,
+      MonadAttach.CanReturn]
     intros; rfl
 
 public instance [Monad m] [LawfulMonad m] [MonadAttach m] [LawfulMonadAttach m] :
@@ -30,7 +31,7 @@ public instance [Monad m] [LawfulMonad m] [MonadAttach m] [WeaklyLawfulMonadAtta
   map_attach := by
     intro α x
     simp only [Functor.map, StateT, funext_iff, StateT.map, bind_pure_comp, MonadAttach.attach,
-      Functor.map_map]
+      Functor.map_map, MonadAttach.CanReturn]
     exact fun s => WeaklyLawfulMonadAttach.map_attach
 
 public instance [Monad m] [LawfulMonad m] [MonadAttach m] [LawfulMonadAttach m] :
@@ -45,7 +46,7 @@ public instance [Monad m] [LawfulMonad m] [MonadAttach m] [LawfulMonadAttach m]
 public instance [Monad m] [LawfulMonad m] [MonadAttach m] [WeaklyLawfulMonadAttach m] :
     WeaklyLawfulMonadAttach (ExceptT ε m) where
   map_attach {α} x := by
-    simp only [Functor.map, MonadAttach.attach, ExceptT.map]
+    simp only [Functor.map, MonadAttach.attach, ExceptT.map, MonadAttach.CanReturn]
     simp
     conv => rhs; rw [← WeaklyLawfulMonadAttach.map_attach (m := m) (x := x)]
     simp only [map_eq_pure_bind]
@@ -83,6 +84,6 @@ attribute [local instance] MonadAttach.trivial
 
 public instance [Monad m] [LawfulMonad m] :
     WeaklyLawfulMonadAttach m where
-  map_attach := by simp [MonadAttach.attach]
+  map_attach := by simp [MonadAttach.attach, MonadAttach.CanReturn]
 
 end

src/Init/Data/Array/Basic.lean

@@ -93,7 +93,7 @@ theorem ext' {xs ys : Array α} (h : xs.toList = ys.toList) : xs = ys := by
 
 @[simp, grind =] theorem getElem?_toList {xs : Array α} {i : Nat} : xs.toList[i]? = xs[i]? := by
   simp only [getElem?_def, getElem_toList]
-  simp only [Array.size]
+  simp only [Array.size]; rfl
 
 /-- `a ∈ as` is a predicate which asserts that `a` is in the array `as`. -/
 -- NB: This is defined as a structure rather than a plain def so that a lemma

src/Init/Data/Array/Bootstrap.lean

@@ -52,7 +52,9 @@ theorem foldrM_eq_reverse_foldlM_toList.aux [Monad m]
   unfold foldrM.fold
   match i with
   | 0 => simp
-  | i+1 => rw [← List.take_concat_get h]; simp [← aux]
+  | i+1 =>
+    set_option backward.isDefEq.respectTransparency false in
+    rw [← List.take_concat_get h]; simp [← aux]
 
 theorem foldrM_eq_reverse_foldlM_toList [Monad m] {f : α → β → m β} {init : β} {xs : Array α} :
     xs.foldrM f init = xs.toList.reverse.foldlM (fun x y => f y x) init := by

src/Init/Data/Array/Count.lean

@@ -117,11 +117,13 @@ grind_pattern Std.Internal.Array.not_of_countP_eq_zero_of_mem => xs.countP p, x
 theorem countP_replicate {a : α} {n : Nat} : countP p (replicate n a) = if p a then n else 0 := by
   simp [← List.toArray_replicate, List.countP_replicate]
 
+set_option backward.isDefEq.respectTransparency false in
 theorem boole_getElem_le_countP {xs : Array α} {i : Nat} (h : i < xs.size) :
     (if p xs[i] then 1 else 0) ≤ xs.countP p := by
   rcases xs with ⟨xs⟩
   simp [List.boole_getElem_le_countP]
 
+set_option backward.isDefEq.respectTransparency false in
 @[grind =]
 theorem countP_set {xs : Array α} {i : Nat} {a : α} (h : i < xs.size) :
     (xs.set i a).countP p = xs.countP p - (if p xs[i] then 1 else 0) + (if p a then 1 else 0) := by

src/Init/Data/Array/DecidableEq.lean

@@ -76,7 +76,7 @@ theorem isEqv_eq_decide (xs ys : Array α) (r) :
     simpa [isEqv_iff_rel] using h'
 
 @[simp, grind =] theorem isEqv_toList [BEq α] (xs ys : Array α) : (xs.toList.isEqv ys.toList r) = (xs.isEqv ys r) := by
-  simp [isEqv_eq_decide, List.isEqv_eq_decide, Array.size]
+  simp [isEqv_eq_decide, List.isEqv_eq_decide, Array.size]; rfl
 
 theorem eq_of_isEqv [DecidableEq α] (xs ys : Array α) (h : Array.isEqv xs ys (fun x y => x = y)) : xs = ys := by
   have ⟨h, h'⟩ := rel_of_isEqv h
@@ -87,6 +87,7 @@ private theorem isEqvAux_self (r : α → α → Bool) (hr : ∀ a, r a a) (xs :
   induction i with
   | zero => simp [Array.isEqvAux]
   | succ i ih =>
+    set_option backward.isDefEq.respectTransparency false in
     simp_all only [isEqvAux, Bool.and_self]
 
 theorem isEqv_self_beq [BEq α] [ReflBEq α] (xs : Array α) : Array.isEqv xs xs (· == ·) = true := by
@@ -153,7 +154,7 @@ theorem beq_eq_decide [BEq α] (xs ys : Array α) :
   simp [BEq.beq, isEqv_eq_decide]
 
 @[simp, grind =] theorem beq_toList [BEq α] (xs ys : Array α) : (xs.toList == ys.toList) = (xs == ys) := by
-  simp [beq_eq_decide, List.beq_eq_decide, Array.size]
+  simp [beq_eq_decide, List.beq_eq_decide, Array.size]; rfl
 
 end Array
 

src/Init/Data/Array/Find.lean

@@ -425,6 +425,7 @@ theorem lt_findIdx_of_not {p : α → Bool} {xs : Array α} {i : Nat} (h : i < x
   simp only [Nat.not_lt] at f
   exact absurd (@findIdx_getElem _ p xs (Nat.lt_of_le_of_lt f h)) (h2 (xs.findIdx p) f)
 
+set_option backward.isDefEq.respectTransparency false in
 /-- `xs.findIdx p = i` iff `p xs[i]` and `¬ p xs [j]` for all `j < i`. -/
 theorem findIdx_eq {p : α → Bool} {xs : Array α} {i : Nat} (h : i < xs.size) :
     xs.findIdx p = i ↔ p xs[i] ∧ ∀ j (hji : j < i), p (xs[j]'(Nat.lt_trans hji h)) = false := by
@@ -613,12 +614,12 @@ theorem findIdx?_eq_some_le_of_findIdx?_eq_some {xs : Array α} {p q : α → Bo
 /-! ### findFinIdx? -/
 
 @[grind =]
-theorem findFinIdx?_empty {p : α → Bool} : findFinIdx? p #[] = none := by simp
+theorem findFinIdx?_empty {p : α → Bool} : findFinIdx? p #[] = none := by simp; rfl
 
 @[grind =]
 theorem findFinIdx?_singleton {a : α} {p : α → Bool} :
     #[a].findFinIdx? p = if p a then some ⟨0, by simp⟩ else none := by
-  simp
+  simp; rfl
 
 -- We can't mark this as a `@[congr]` lemma since the head of the RHS is not `findFinIdx?`.
 theorem findFinIdx?_congr {p : α → Bool} {xs ys : Array α} (w : xs = ys) :
@@ -714,6 +715,7 @@ theorem findFinIdx?_eq_bind_find?_finIdxOf? [BEq α] [LawfulBEq α] {xs : Array
     xs.findFinIdx? p = (xs.find? p).bind (xs.finIdxOf? ·) := by
   cases xs
   simp [List.findFinIdx?_eq_bind_find?_finIdxOf?]
+  rfl
 
 theorem findIdx_eq_getD_bind_find?_idxOf? [BEq α] [LawfulBEq α] {xs : Array α} {p : α → Bool} :
     xs.findIdx p = ((xs.find? p).bind (xs.idxOf? ·)).getD xs.size := by
@@ -792,7 +794,7 @@ theorem idxOf?_eq_map_finIdxOf?_val [BEq α] {xs : Array α} {a : α} :
     xs.idxOf? a = (xs.finIdxOf? a).map (·.val) := by
   simp [idxOf?, finIdxOf?]
 
-@[grind =] theorem finIdxOf?_empty [BEq α] : (#[] : Array α).finIdxOf? a = none := by simp
+@[grind =] theorem finIdxOf?_empty [BEq α] : (#[] : Array α).finIdxOf? a = none := by simp; rfl
 
 @[simp, grind =] theorem finIdxOf?_eq_none_iff [BEq α] [LawfulBEq α] {xs : Array α} {a : α} :
     xs.finIdxOf? a = none ↔ a ∉ xs := by

src/Init/Data/Array/Lemmas.lean

@@ -170,6 +170,7 @@ theorem getD_getElem? {xs : Array α} {i : Nat} {d : α} :
 
 @[simp] theorem getElem?_empty {i : Nat} : (#[] : Array α)[i]? = none := rfl
 
+set_option backward.isDefEq.respectTransparency false in
 theorem getElem_push_lt {xs : Array α} {x : α} {i : Nat} (h : i < xs.size) :
     have : i < (xs.push x).size := by simp [*, Nat.lt_succ_of_le, Nat.le_of_lt]
     (xs.push x)[i] = xs[i] := by
@@ -895,7 +896,7 @@ theorem all_push {xs : Array α} {a : α} {p : α → Bool} :
 @[simp] theorem getElem_set_ne {xs : Array α} {i : Nat} (h' : i < xs.size) {v : α} {j : Nat}
     (pj : j < xs.size) (h : i ≠ j) :
     (xs.set i v)[j]'(by simp [*]) = xs[j] := by
-  simp only [set, ← getElem_toList, List.getElem_set_ne h]
+  simp only [set, ← getElem_toList, List.getElem_set_ne h]; rfl
 
 @[simp] theorem getElem?_set_ne {xs : Array α} {i : Nat} (h : i < xs.size) {v : α} {j : Nat}
     (ne : i ≠ j) : (xs.set i v)[j]? = xs[j]? := by
@@ -2854,7 +2855,7 @@ theorem getElem?_extract {xs : Array α} {start stop : Nat} :
   · simp only [length_toList, size_extract, List.length_take, List.length_drop]
     omega
   · intro n h₁ h₂
-    simp
+    simp; rfl
 
 @[simp] theorem extract_size {xs : Array α} : xs.extract 0 xs.size = xs := by
   apply ext
@@ -3974,6 +3975,7 @@ theorem all_filterMap {xs : Array α} {f : α → Option β} {p : β → Bool} :
   · simp only [Id.run_pure]
     rw [if_neg (mt (by rintro rfl; exact h) (by simp_all))]
 
+set_option backward.isDefEq.respectTransparency false in
 @[simp, grind =] theorem toList_modify {xs : Array α} {f : α → α} {i : Nat} :
     (xs.modify i f).toList = xs.toList.modify i f := by
   apply List.ext_getElem
@@ -4259,6 +4261,7 @@ private theorem getElem_ofFn_go {f : Fin n → α} {acc i k} (h : i ≤ n) (w₁
     · simp
       omega
 
+set_option backward.isDefEq.respectTransparency false in
 @[simp] theorem getElem_ofFn {f : Fin n → α} {i : Nat} (h : i < (ofFn f).size) :
     (ofFn f)[i] = f ⟨i, size_ofFn (f := f) ▸ h⟩ := by
   unfold ofFn
@@ -4490,11 +4493,13 @@ theorem getElem?_push_eq {xs : Array α} {x : α} : (xs.push x)[xs.size]? = some
   cases xs
   simp
 
+set_option backward.isDefEq.respectTransparency false in
 @[simp, grind =] theorem finIdxOf?_toList [BEq α] {a : α} {xs : Array α} :
     xs.toList.finIdxOf? a = (xs.finIdxOf? a).map (Fin.cast (by simp)) := by
   cases xs
   simp
 
+set_option backward.isDefEq.respectTransparency false in
 @[simp, grind =] theorem findFinIdx?_toList {p : α → Bool} {xs : Array α} :
     xs.toList.findFinIdx? p = (xs.findFinIdx? p).map (Fin.cast (by simp)) := by
   cases xs
@@ -4619,6 +4624,7 @@ namespace List
     as.toArray.unzip = Prod.map List.toArray List.toArray as.unzip := by
   ext1 <;> simp
 
+set_option backward.isDefEq.respectTransparency false in
 @[simp, grind =] theorem firstM_toArray [Alternative m] {as : List α} {f : α → m β} :
     as.toArray.firstM f = as.firstM f := by
   unfold Array.firstM

src/Init/Data/Array/MapIdx.lean

@@ -72,6 +72,7 @@ theorem mapFinIdx_spec {xs : Array α} {f : (i : Nat) → α → (h : i < xs.siz
   simp only [getElem?_def, size_mapFinIdx, getElem_mapFinIdx]
   split <;> simp_all
 
+set_option backward.isDefEq.respectTransparency false in
 @[simp, grind =] theorem toList_mapFinIdx {xs : Array α} {f : (i : Nat) → α → (h : i < xs.size) → β} :
     (xs.mapFinIdx f).toList = xs.toList.mapFinIdx (fun i a h => f i a (by simpa)) := by
   apply List.ext_getElem <;> simp
@@ -105,6 +106,7 @@ theorem mapIdx_spec {f : Nat → α → β} {xs : Array α}
       xs[i]?.map (f i) := by
   simp [getElem?_def, size_mapIdx, getElem_mapIdx]
 
+set_option backward.isDefEq.respectTransparency false in
 @[simp, grind =] theorem toList_mapIdx {f : Nat → α → β} {xs : Array α} :
     (xs.mapIdx f).toList = xs.toList.mapIdx (fun i a => f i a) := by
   apply List.ext_getElem <;> simp

src/Init/Data/Array/OfFn.lean

@@ -41,6 +41,7 @@ theorem ofFn_succ {f : Fin (n+1) → α} :
     intro h₃
     simp only [show i = n by omega]
 
+set_option backward.isDefEq.respectTransparency false in
 theorem ofFn_add {n m} {f : Fin (n + m) → α} :
     ofFn f = (ofFn (fun i => f (i.castLE (Nat.le_add_right n m)))) ++ (ofFn (fun i => f (i.natAdd n))) := by
   induction m with
@@ -107,6 +108,7 @@ theorem ofFnM_succ {n} [Monad m] [LawfulMonad m] {f : Fin (n + 1) → m α} :
       pure (as.push a)) := by
   simp [ofFnM, Fin.foldlM_succ_last]
 
+set_option backward.isDefEq.respectTransparency false in
 theorem ofFnM_add {n m} [Monad m] [LawfulMonad m] {f : Fin (n + k) → m α} :
     ofFnM f = (do
       let as ← ofFnM fun i : Fin n => f (i.castLE (Nat.le_add_right n k))

src/Init/Data/BitVec/Bitblast.lean

@@ -2192,6 +2192,7 @@ def uppcRec {w} (x : BitVec w) (s : Nat) (hs : s < w) : Bool :=
   | 0 => x.msb
   | i + 1 =>  x[w - 1 - i] || uppcRec x i (by omega)
 
+set_option backward.isDefEq.respectTransparency false in
 /-- The unsigned parallel prefix of `x` at `s` is `true` if and only if x interpreted
   as a natural number is greater or equal than `2 ^ (w - 1 - (s - 1))`. -/
 @[simp]

src/Init/Data/BitVec/Lemmas.lean

@@ -1198,7 +1198,7 @@ let x' = x.extractLsb' 7 5  =   _ _ 9 8 7
       (decide (0 < len) &&
       (decide (start + len ≤ w) &&
       x.getMsbD (w - (start + len)))) := by
-  simp [BitVec.msb, getMsbD_extractLsb']
+  simp [BitVec.msb, getMsbD_extractLsb']; rfl
 
 @[simp, grind =] theorem getElem_extract {hi lo : Nat} {x : BitVec n} {i : Nat} (h : i < hi - lo + 1) :
     (extractLsb hi lo x)[i] = getLsbD x (lo+i) := by
@@ -1234,7 +1234,7 @@ let x' = x.extractLsb' 7 5  =   _ _ 9 8 7
 
 @[simp, grind =] theorem msb_extractLsb {hi lo : Nat} {x : BitVec w} :
     (extractLsb hi lo x).msb = (decide (max hi lo < w) && x.getMsbD (w - 1 - max hi lo)) := by
-  simp [BitVec.msb]
+  simp [BitVec.msb]; rfl
 
 theorem extractLsb'_eq_extractLsb {w : Nat} (x : BitVec w) (start len : Nat) (h : len > 0) :
     x.extractLsb' start len = (x.extractLsb (len - 1 + start) start).cast (by omega) := by
@@ -2771,8 +2771,9 @@ theorem msb_append {x : BitVec w} {y : BitVec v} :
 @[simp] theorem append_zero_width (x : BitVec w) (y : BitVec 0) : x ++ y = x := by
   ext i ih
   rw [getElem_append] -- Why does this not work with `simp [getElem_append]`?
-  simp
+  simp; rfl
 
+set_option backward.isDefEq.respectTransparency false in
 @[grind =]
 theorem toInt_append {x : BitVec n} {y : BitVec m} :
     (x ++ y).toInt = if n == 0 then y.toInt else (2 ^ m) * x.toInt + y.toNat := by
@@ -5278,6 +5279,7 @@ theorem and_one_eq_setWidth_ofBool_getLsbD {x : BitVec w} :
 theorem replicate_zero {x : BitVec w} : x.replicate 0 = 0#0 := by
   simp [replicate]
 
+set_option backward.isDefEq.respectTransparency false in
 @[simp, grind =]
 theorem replicate_one {w : Nat} {x : BitVec w} :
     (x.replicate 1) = x.cast (by rw [Nat.mul_one]) := by
@@ -5329,6 +5331,7 @@ theorem append_assoc {x₁ : BitVec w₁} {x₂ : BitVec w₂} {x₃ : BitVec w
 theorem append_assoc' {x₁ : BitVec w₁} {x₂ : BitVec w₂} {x₃ : BitVec w₃} :
     (x₁ ++ (x₂ ++ x₃)) = ((x₁ ++ x₂) ++ x₃).cast (by omega) := by simp [append_assoc]
 
+set_option backward.isDefEq.respectTransparency false in
 theorem replicate_append_self {x : BitVec w} :
     x ++ x.replicate n = (x.replicate n ++ x).cast (by omega) := by
   induction n with

src/Init/Data/ByteArray/Lemmas.lean

@@ -111,13 +111,13 @@ theorem getElem_eq_getElem_data {a : ByteArray} {i : Nat} {h : i < a.size} :
 theorem getElem_append_left {i : Nat} {a b : ByteArray} {h : i < (a ++ b).size}
     (hlt : i < a.size) : (a ++ b)[i] = a[i] := by
   simp only [getElem_eq_getElem_data, data_append]
-  rw [Array.getElem_append_left (by simpa)]
+  rw [Array.getElem_append_left (by simpa)]; rfl
 
 theorem getElem_append_right {i : Nat} {a b : ByteArray} {h : i < (a ++ b).size}
     (hle : a.size ≤ i) : (a ++ b)[i] = b[i - a.size]'(by simp_all; omega) := by
   simp only [getElem_eq_getElem_data, data_append]
   rw [Array.getElem_append_right (by simpa)]
-  simp
+  simp; rfl
 
 @[simp]
 theorem _root_.List.getElem_toByteArray {l : List UInt8} {i : Nat} {h : i < l.toByteArray.size} :
@@ -223,7 +223,7 @@ theorem getElem_extract_aux {xs : ByteArray} {start stop : Nat} (h : i < (xs.ext
 
 theorem getElem_extract {i : Nat} {b : ByteArray} {start stop : Nat}
     (h) : (b.extract start stop)[i]'h = b[start + i]'(getElem_extract_aux h) := by
-  simp [getElem_eq_getElem_data]
+  simp [getElem_eq_getElem_data]; rfl
 
 theorem extract_eq_extract_left {a : ByteArray} {i i' j : Nat} :
     a.extract i j = a.extract i' j ↔ min j a.size - i = min j a.size - i' := by
@@ -236,25 +236,25 @@ theorem extract_add_one {a : ByteArray} {i : Nat} (ha : i + 1 ≤ a.size) :
     omega
   · rename_i j hj hj'
     obtain rfl : j = 0 := by simpa using hj'
-    simp [ByteArray.getElem_eq_getElem_data]
+    simp [ByteArray.getElem_eq_getElem_data]; rfl
 
 theorem extract_add_two {a : ByteArray} {i : Nat} (ha : i + 2 ≤ a.size) :
     a.extract i (i + 2) = [a[i], a[i + 1]].toByteArray := by
   rw [extract_eq_extract_append_extract (i + 1) (by simp) (by omega),
     extract_add_one (by omega), extract_add_one (by omega)]
-  simp [← List.toByteArray_append]
+  simp [← List.toByteArray_append]; rfl
 
 theorem extract_add_three {a : ByteArray} {i : Nat} (ha : i + 3 ≤ a.size) :
     a.extract i (i + 3) = [a[i], a[i + 1], a[i + 2]].toByteArray := by
   rw [extract_eq_extract_append_extract (i + 1) (by simp) (by omega),
     extract_add_one (by omega), extract_add_two (by omega)]
-  simp [← List.toByteArray_append]
+  simp [← List.toByteArray_append]; rfl
 
 theorem extract_add_four {a : ByteArray} {i : Nat} (ha : i + 4 ≤ a.size) :
     a.extract i (i + 4) = [a[i], a[i + 1], a[i + 2], a[i + 3]].toByteArray := by
   rw [extract_eq_extract_append_extract (i + 1) (by simp) (by omega),
     extract_add_one (by omega), extract_add_three (by omega)]
-  simp [← List.toByteArray_append]
+  simp [← List.toByteArray_append]; rfl
 
 theorem append_assoc {a b c : ByteArray} : a ++ b ++ c = a ++ (b ++ c) := by
   ext1

src/Init/Data/Fin/Fold.lean

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: François G. Dorais
 -/
 module
-
 prelude
 public import Init.Control.Lawful.Basic
 public import Init.Ext
@@ -13,7 +12,7 @@ import Init.Data.Nat.Lemmas
 import Init.Omega
 import Init.TacticsExtra
 import Init.WFTactics
-
+import Init.Hints
 public section
 
 namespace Fin
@@ -165,7 +164,7 @@ theorem foldlM_add [Monad m] [LawfulMonad m] (f : α → Fin (n + k) → m α) :
     simp
   | succ k ih =>
     funext x
-    simp [foldlM_succ_last, ← Nat.add_assoc, ih]
+    simp [foldlM_succ_last, ← Nat.add_assoc, ih]; rfl
 
 /-! ### foldrM -/
 
@@ -223,7 +222,7 @@ theorem foldrM_add [Monad m] [LawfulMonad m] (f : Fin (n + k) → α → m α) :
     simp
   | succ k ih =>
     funext x
-    simp [foldrM_succ_last, ← Nat.add_assoc, ih]
+    simp [foldrM_succ_last, ← Nat.add_assoc, ih]; rfl
 
 /-! ### foldl -/
 
@@ -269,7 +268,7 @@ theorem foldl_add (f : α → Fin (n + m) → α) (x) :
         (foldl n (fun x i => f x (i.castLE (Nat.le_add_right n m))) x):= by
   induction m with
   | zero => simp
-  | succ m ih => simp [foldl_succ_last, ih, ← Nat.add_assoc]
+  | succ m ih => simp [foldl_succ_last, ih, ← Nat.add_assoc]; rfl
 
 theorem foldl_eq_foldlM (f : α → Fin n → α) (x) :
     foldl n f x = (foldlM (m := Id) n (pure <| f · ·) x).run := by
@@ -322,7 +321,7 @@ theorem foldr_add (f : Fin (n + m) → α → α) (x) :
         (foldr m (fun i => f (i.natAdd n)) x) := by
   induction m generalizing x with
   | zero => simp
-  | succ m ih => simp [foldr_succ_last, ih, ← Nat.add_assoc]
+  | succ m ih => simp [foldr_succ_last, ih, ← Nat.add_assoc]; rfl
 
 theorem foldr_eq_foldrM (f : Fin n → α → α) (x) :
     foldr n f x = (foldrM (m := Id) n (pure <| f · ·) x).run := by

src/Init/Data/Fin/Iterate.lean

@@ -4,14 +4,12 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joe Hendrix
 -/
 module
-
 prelude
 public import Init.Data.Fin.Basic
 import Init.PropLemmas
 import Init.WFTactics
-
+import Init.Hints
 public section
-
 namespace Fin
 
 /--

src/Init/Data/Fin/Lemmas.lean

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro, Leonardo de Moura
 -/
 module
-
 prelude
 public import Init.Ext
 public import Init.Data.Nat.Div.Basic
@@ -15,7 +14,7 @@ import Init.Data.Nat.Lemmas
 import Init.Data.Nat.Linear
 import Init.Omega
 import Init.TacticsExtra
-
+import Init.Hints
 @[expose] public section
 
 open Std
@@ -998,7 +997,7 @@ For the induction:
 
 @[simp, grind =] theorem reverseInduction_last {n : Nat} {motive : Fin (n + 1) → Sort _} {zero succ} :
     (reverseInduction zero succ (Fin.last n) : motive (Fin.last n)) = zero := by
-  rw [reverseInduction, reverseInduction.go]; simp
+  rw [reverseInduction, reverseInduction.go]; simp; rfl
 
 private theorem reverseInduction_castSucc_aux {n : Nat} {motive : Fin (n + 1) → Sort _} {succ}
     (i : Fin n) (j : Nat) (h) (h2 : i.1 < j) (zero : motive ⟨j, h⟩) :
@@ -1009,9 +1008,9 @@ private theorem reverseInduction_castSucc_aux {n : Nat} {motive : Fin (n + 1)
   | succ j ih =>
     rw [reverseInduction.go, dif_neg (by exact Nat.ne_of_lt h2)]
     by_cases hij : i = j
-    · subst hij; simp [reverseInduction.go]
-    dsimp only
-    rw [ih _ _ (by omega), eq_comm, reverseInduction.go, dif_neg (by change i.1 + 1 ≠ _; omega)]
+    · subst hij; simp [reverseInduction.go]; rfl
+    · dsimp only
+      rw [ih _ _ (by omega), eq_comm, reverseInduction.go, dif_neg (by change i.1 + 1 ≠ _; omega)]
 
 @[simp, grind =] theorem reverseInduction_castSucc {n : Nat} {motive : Fin (n + 1) → Sort _} {zero succ}
     (i : Fin n) : reverseInduction (motive := motive) zero succ (castSucc i) =

src/Init/Data/Iterators/Lemmas/Combinators/FilterMap.lean

@@ -750,6 +750,7 @@ theorem Iter.anyM_filterMapM {α β β' : Type w} {m : Type w → Type w'}
   simp only [filterMapM_eq_toIter_filterMapM_toIterM, IterM.anyM_filterMapM]
   rfl
 
+set_option backward.isDefEq.respectTransparency false in
 -- There is hope to generalize the following theorem as soon there is a `Shrink` type.
 /--
 This lemma expresses `Iter.anyM` in terms of `IterM.anyM`.

src/Init/Data/Iterators/Lemmas/Combinators/FlatMap.lean

@@ -232,6 +232,7 @@ public theorem Iter.toArray_flatMapM {α α₂ β γ : Type w} {m : Type w → T
     (it₁.flatMapM f).toArray = Array.flatten <$> (it₁.mapM fun b => do (← f b).toArray).toArray := by
   simp [flatMapM, toArray_flatMapAfterM]
 
+set_option backward.isDefEq.respectTransparency false in
 public theorem Iter.toList_flatMapAfter {α α₂ β γ : Type w} [Iterator α Id β] [Iterator α₂ Id γ]
     [Finite α Id] [Finite α₂ Id]
     {f : β → Iter (α := α₂) γ} {it₁ : Iter (α := α) β} {it₂ : Option (Iter (α := α₂) γ)} :
@@ -242,6 +243,7 @@ public theorem Iter.toList_flatMapAfter {α α₂ β γ : Type w} [Iterator α I
   simp only [flatMapAfter, Iter.toList, toIterM_toIter, IterM.toList_flatMapAfter]
   cases it₂ <;> simp [map, IterM.toList_map_eq_toList_mapM, - IterM.toList_map]
 
+set_option backward.isDefEq.respectTransparency false in
 public theorem Iter.toArray_flatMapAfter {α α₂ β γ : Type w} [Iterator α Id β] [Iterator α₂ Id γ]
     [Finite α Id] [Finite α₂ Id]
     {f : β → Iter (α := α₂) γ} {it₁ : Iter (α := α) β} {it₂ : Option (Iter (α := α₂) γ)} :

src/Init/Data/Iterators/Lemmas/Combinators/Monadic/FilterMap.lean

@@ -600,6 +600,7 @@ theorem IterM.toList_map_mapM {α β γ δ : Type w}
     toList_filterMapM_mapM]
   congr <;> simp
 
+set_option backward.isDefEq.respectTransparency false in
 @[simp]
 theorem IterM.toList_filterMapWithPostcondition {α β γ : Type w} {m : Type w → Type w'}
     [Monad m] [LawfulMonad m]
@@ -623,6 +624,7 @@ theorem IterM.toList_filterMapWithPostcondition {α β γ : Type w} {m : Type w
   · simp [ihs ‹_›, heq]
   · simp [heq]
 
+set_option backward.isDefEq.respectTransparency false in
 @[simp]
 theorem IterM.toList_mapWithPostcondition {α β γ : Type w} {m : Type w → Type w'}
     [Monad m] [LawfulMonad m] [Iterator α Id β] [Finite α Id]
@@ -643,6 +645,7 @@ theorem IterM.toList_mapWithPostcondition {α β γ : Type w} {m : Type w → Ty
   · simp [ihs ‹_›, heq]
   · simp [heq]
 
+set_option backward.isDefEq.respectTransparency false in
 @[simp]
 theorem IterM.toList_filterMapM {α β γ : Type w} {m : Type w → Type w'}
     [Monad m] [MonadAttach m] [LawfulMonad m] [WeaklyLawfulMonadAttach m]
@@ -652,6 +655,7 @@ theorem IterM.toList_filterMapM {α β γ : Type w} {m : Type w → Type w'}
   simp [toList_filterMapM_eq_toList_filterMapWithPostcondition, toList_filterMapWithPostcondition,
     PostconditionT.attachLift, PostconditionT.run_eq_map, WeaklyLawfulMonadAttach.map_attach]
 
+set_option backward.isDefEq.respectTransparency false in
 @[simp]
 theorem IterM.toList_mapM {α β γ : Type w} {m : Type w → Type w'}
     [Monad m] [MonadAttach m] [LawfulMonad m] [WeaklyLawfulMonadAttach m]
@@ -1297,6 +1301,7 @@ theorem IterM.forIn_filterMap
   rw [filterMap, forIn_filterMapWithPostcondition]
   simp [PostconditionT.run_eq_map]
 
+set_option backward.isDefEq.respectTransparency false in
 theorem IterM.forIn_mapWithPostcondition
     [Monad m] [LawfulMonad m] [Monad n] [LawfulMonad n] [Monad o] [LawfulMonad o]
     [MonadLiftT m n] [LawfulMonadLiftT m n] [MonadLiftT n o] [LawfulMonadLiftT n o]

src/Init/Data/Iterators/Lemmas/Combinators/Monadic/FlatMap.lean

@@ -36,7 +36,7 @@ theorem IterM.step_flattenAfter {α α₂ β : Type w} {m : Type w → Type w'}
   cases it₂
   all_goals
   · apply bind_congr; intro step
-    cases step.inflate using PlausibleIterStep.casesOn <;> simp [IterM.flattenAfter]
+    cases step.inflate using PlausibleIterStep.casesOn <;> simp [IterM.flattenAfter] <;> rfl
 
 namespace Iterators.Types
 

src/Init/Data/Iterators/Lemmas/Combinators/Monadic/ULift.lean

@@ -29,7 +29,7 @@ theorem IterM.step_uLift [Iterator α m β] [Monad n] {it : IterM (α := α) m
       | .done h => return .deflate (.done ⟨_, h, rfl⟩)) := by
   simp only [IterM.step, Iterator.step, IterM.uLift]
   apply bind_congr; intro step
-  split <;> simp [Types.ULiftIterator.Monadic.modifyStep, *]
+  split <;> simp [Types.ULiftIterator.Monadic.modifyStep, *] <;> rfl
 
 @[simp]
 theorem IterM.toList_uLift [Iterator α m β] [Monad m] [Monad n] {it : IterM (α := α) m β}

src/Init/Data/Iterators/Lemmas/Combinators/ULift.lean

@@ -26,6 +26,7 @@ theorem Iter.uLift_eq_toIter_uLift_toIterM {it : Iter (α := α) β} :
     it.uLift = (it.toIterM.uLift Id).toIter :=
   rfl
 
+set_option backward.isDefEq.respectTransparency false in
 theorem Iter.step_uLift [Iterator α Id β] {it : Iter (α := α) β} :
     it.uLift.step = match it.step with
       | .yield it' out h => .yield it'.uLift (.up out) ⟨_, h, rfl⟩
@@ -38,6 +39,7 @@ theorem Iter.step_uLift [Iterator α Id β] {it : Iter (α := α) β} :
     PlausibleIterStep.done, pure_bind]
   cases it.toIterM.step.run.inflate using PlausibleIterStep.casesOn <;> simp
 
+set_option backward.isDefEq.respectTransparency false in
 @[simp]
 theorem Iter.toList_uLift [Iterator α Id β] {it : Iter (α := α) β}
     [Finite α Id] :
@@ -59,6 +61,7 @@ theorem Iter.toArray_uLift [Iterator α Id β] {it : Iter (α := α) β}
   rw [← toArray_toList, ← toArray_toList, toList_uLift]
   simp [-toArray_toList]
 
+set_option backward.isDefEq.respectTransparency false in
 @[simp]
 theorem Iter.length_uLift [Iterator α Id β] {it : Iter (α := α) β}
     [Finite α Id] [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id] :

src/Init/Data/Iterators/Lemmas/Consumers/Loop.lean

@@ -398,7 +398,7 @@ theorem Iter.fold_eq_fold_toIterM {α β : Type w} {γ : Type w} [Iterator α Id
     [Finite α Id] [IteratorLoop α Id Id]
     {f : γ → β → γ} {init : γ} {it : Iter (α := α) β} :
     it.fold (init := init) f = (it.toIterM.fold (init := init) f).run := by
-  rw [fold_eq_foldM, foldM_eq_foldM_toIterM, IterM.fold_eq_foldM]
+  rw [fold_eq_foldM, foldM_eq_foldM_toIterM, IterM.fold_eq_foldM]; rfl
 
 @[simp]
 theorem Iter.forIn_pure_yield_eq_fold {α β : Type w} {γ : Type x} [Iterator α Id β]

src/Init/Data/Iterators/Lemmas/Producers/List.lean

@@ -23,6 +23,7 @@ open Std Std.Iterators
 
 variable {β : Type w}
 
+set_option backward.isDefEq.respectTransparency false in
 @[simp]
 theorem List.step_iter_nil :
     (([] : List β).iter).step = ⟨.done, rfl⟩ := by
@@ -31,7 +32,7 @@ theorem List.step_iter_nil :
 @[simp]
 theorem List.step_iter_cons {x : β} {xs : List β} :
     ((x :: xs).iter).step = ⟨.yield xs.iter x, rfl⟩ := by
-  simp [List.iter, List.iterM, IterM.toIter, Iter.step_eq]
+  simp [List.iter, List.iterM, IterM.toIter, Iter.step_eq]; rfl
 
 @[simp, grind =]
 theorem List.toArray_iter {l : List β} :

src/Init/Data/Iterators/Lemmas/Producers/Monadic/List.lean

@@ -31,7 +31,7 @@ theorem List.step_iterM_nil :
 @[simp]
 theorem List.step_iterM_cons {x : β} {xs : List β} :
     ((x :: xs).iterM m).step = pure (.deflate ⟨.yield (xs.iterM m) x, rfl⟩) := by
-  simp only [List.iterM, IterM.step, Iterator.step]
+  simp only [List.iterM, IterM.step, Iterator.step]; rfl
 
 theorem List.step_iterM {l : List β} :
     (l.iterM m).step = match l with

src/Init/Data/List/Count.lean

@@ -132,7 +132,9 @@ theorem boole_getElem_le_countP {p : α → Bool} {l : List α} {i : Nat} (h : i
   | nil => simp at h
   | cons x l ih =>
     cases i with
-    | zero => simp [countP_cons]
+    | zero =>
+      set_option backward.isDefEq.respectTransparency false in
+      simp [countP_cons]
     | succ i =>
       simp only [length_cons, add_one_lt_add_one_iff] at h
       simp only [getElem_cons_succ, countP_cons]
@@ -263,7 +265,9 @@ theorem count_eq_length_filter {a : α} {l : List α} : count a l = (filter (·
 theorem count_tail : ∀ {l : List α} {a : α},
       l.tail.count a = l.count a - if l.head? == some a then 1 else 0
   | [], a => by simp
-  | _ :: _, a => by simp [count_cons]
+  | _ :: _, a => by
+    set_option backward.isDefEq.respectTransparency false in
+    simp [count_cons]
 
 theorem count_le_length {a : α} {l : List α} : count a l ≤ l.length := countP_le_length
 

src/Init/Data/List/Find.lean

@@ -654,6 +654,7 @@ theorem lt_findIdx_of_not {p : α → Bool} {xs : List α} {i : Nat} (h : i < xs
   simp only [Nat.not_lt] at f
   exact absurd (@findIdx_getElem _ p xs (Nat.lt_of_le_of_lt f h)) (h2 (xs.findIdx p) f)
 
+set_option backward.isDefEq.respectTransparency false in
 /-- `xs.findIdx p = i` iff `p xs[i]` and `¬ p xs [j]` for all `j < i`. -/
 theorem findIdx_eq {p : α → Bool} {xs : List α} {i : Nat} (h : i < xs.length) :
     xs.findIdx p = i ↔ p xs[i] ∧ ∀ j (hji : j < i), p (xs[j]'(Nat.lt_trans hji h)) = false := by
@@ -1038,7 +1039,7 @@ theorem findFinIdx?_append {xs ys : List α} {p : α → Bool} :
 
 @[simp, grind =] theorem findFinIdx?_singleton {a : α} {p : α → Bool} :
     [a].findFinIdx? p = if p a then some ⟨0, by simp⟩ else none := by
-  simp [findFinIdx?_cons, findFinIdx?_nil]
+  simp [findFinIdx?_cons, findFinIdx?_nil]; rfl
 
 @[simp, grind =] theorem findFinIdx?_eq_none_iff {l : List α} {p : α → Bool} :
     l.findFinIdx? p = none ↔ ∀ x ∈ l, ¬ p x := by
@@ -1080,6 +1081,7 @@ theorem isNone_findFinIdx? {l : List α} {p : α → Bool} :
   induction l with
   | nil => simp
   | cons a l ih =>
+    set_option backward.isDefEq.respectTransparency false in
     simp [hf, findFinIdx?_cons]
     split <;> simp [ih, Function.comp_def]
 

src/Init/Data/List/Lemmas.lean

@@ -3525,7 +3525,7 @@ theorem getElem?_insert_succ {l : List α} {a : α} {i : Nat} :
   · split
     · rfl
     · have h' : i - 1 < l.length := Nat.lt_of_le_of_lt (Nat.pred_le _) h
-      simp [h']
+      simp [h']; rfl
 
 theorem head?_insert {l : List α} {a : α} :
     (l.insert a).head? = some (if h : a ∈ l then l.head (ne_nil_of_mem h) else a) := by
@@ -3679,11 +3679,13 @@ theorem get_of_eq {l l' : List α} (h : l = l') (i : Fin l.length) :
 theorem getElem!_nil [Inhabited α] {n : Nat} : ([] : List α)[n]! = default := rfl
 
 theorem getElem!_cons_zero [Inhabited α] {l : List α} : (a::l)[0]! = a := by
-  rw [getElem!_pos] <;> simp
+  rw [getElem!_pos]; rfl; simp
 
 theorem getElem!_cons_succ [Inhabited α] {l : List α} : (a::l)[i+1]! = l[i]! := by
   by_cases h : i < l.length
-  · rw [getElem!_pos, getElem!_pos] <;> simp_all [Nat.succ_lt_succ_iff]
+  · rw [getElem!_pos, getElem!_pos]
+    · rfl
+    · simp; apply Nat.succ_lt_succ; assumption
   · rw [getElem!_neg, getElem!_neg] <;> simp_all [Nat.succ_lt_succ_iff]
 
 theorem getElem!_of_getElem? [Inhabited α] : ∀ {l : List α} {i : Nat}, l[i]? = some a → l[i]! = a

src/Init/Data/List/MapIdx.lean

@@ -350,6 +350,7 @@ theorem getElem?_mapIdx_go : ∀ {l : List α} {acc : Array β} {i : Nat},
   | [], acc, i => by
     simp only [mapIdx.go, getElem?_def, Array.length_toList,
       ← Array.getElem_toList, length_nil, Nat.not_lt_zero, ↓reduceDIte, Option.map_none]
+    rfl
   | a :: l, acc, i => by
     rw [mapIdx.go, getElem?_mapIdx_go]
     simp only [Array.size_push]

src/Init/Data/List/MinMaxIdx.lean

@@ -410,6 +410,7 @@ private theorem minIdxOn_append_aux [LE β] [DecidableLE β]
     match xs with
     | [] => simp [minIdxOn_cons_aux (xs := ys) ‹_›]
     | z :: zs =>
+      set_option backward.isDefEq.respectTransparency false in
       simp +singlePass only [cons_append]
       simp only [minIdxOn_cons_aux (xs := z :: zs ++ ys) (by simp), ih (by simp),
         minIdxOn_cons_aux (xs := z :: zs) (by simp), combineMinIdxOn_assoc]

src/Init/Data/List/Nat/Count.lean

@@ -25,6 +25,7 @@ namespace List
 
 open Nat
 
+set_option backward.isDefEq.respectTransparency false in
 @[grind =]
 theorem countP_set {p : α → Bool} {l : List α} {i : Nat} {a : α} (h : i < l.length) :
     (l.set i a).countP p = l.countP p - (if p l[i] then 1 else 0) + (if p a then 1 else 0) := by

src/Init/Data/List/Nat/Pairwise.lean

@@ -53,10 +53,12 @@ theorem sublist_eq_map_getElem {l l' : List α} (h : l' <+ l) : ∃ is : List (F
   | cons _ _ IH =>
     let ⟨is, IH⟩ := IH
     refine ⟨is.map (·.succ), ?_⟩
+    set_option backward.isDefEq.respectTransparency false in
     simpa [Function.comp_def, pairwise_map]
   | cons₂ _ _ IH =>
     rcases IH with ⟨is,IH⟩
     refine ⟨⟨0, by simp [Nat.zero_lt_succ]⟩ :: is.map (·.succ), ?_⟩
+    set_option backward.isDefEq.respectTransparency false in
     simp [Function.comp_def, pairwise_map, IH, ← get_eq_getElem, get_cons_zero, get_cons_succ']
 
 set_option linter.listVariables false in

src/Init/Data/List/OfFn.lean

@@ -98,7 +98,9 @@ theorem ofFn_add {n m} {f : Fin (n + m) → α} :
     ofFn f = (ofFn fun i => f (i.castLE (Nat.le_add_right n m))) ++ (ofFn fun i => f (i.natAdd n)) := by
   induction m with
   | zero => simp
-  | succ m ih => simp [-ofFn_succ, ofFn_succ_last, ih]
+  | succ m ih =>
+    set_option backward.isDefEq.respectTransparency false in
+    simp [-ofFn_succ, ofFn_succ_last, ih]
 
 @[simp]
 theorem ofFn_eq_nil_iff {f : Fin n → α} : ofFn f = [] ↔ n = 0 := by
@@ -154,8 +156,9 @@ theorem ofFnM_add {n m} [Monad m] [LawfulMonad m] {f : Fin (n + k) → m α} :
       pure (as ++ bs)) := by
   induction k with
   | zero => simp
-  | succ k ih => simp [ofFnM_succ_last, ih]
-
+  | succ k ih =>
+    set_option backward.isDefEq.respectTransparency false in
+    simp [ofFnM_succ_last, ih]
 
 end List
 

src/Init/Data/List/Sort/Basic.lean

@@ -64,6 +64,7 @@ def MergeSort.Internal.splitInTwo (l : { l : List α // l.length = n }) :
 
 open MergeSort.Internal in
 set_option linter.unusedVariables false in
+set_option backward.isDefEq.respectTransparency false in
 /--
 A stable merge sort.
 

src/Init/Data/List/Sort/Impl.lean

@@ -182,14 +182,14 @@ private theorem mergeSortTR_run_eq_mergeSort : {n : Nat} → (l : { l : List α
     simp only [mergeSortTR.run, mergeSortTR.run, mergeSort]
     rw [merge_eq_mergeTR]
     rw [mergeSortTR_run_eq_mergeSort, mergeSortTR_run_eq_mergeSort]
+    rfl
 
 -- We don't make this a `@[csimp]` lemma because `mergeSort_eq_mergeSortTR₂` is faster.
 theorem mergeSort_eq_mergeSortTR : @mergeSort = @mergeSortTR := by
   funext
   rw [mergeSortTR, mergeSortTR_run_eq_mergeSort]
 
--- This mutual block is unfortunately quite slow to elaborate.
-set_option maxHeartbeats 400000 in
+set_option backward.isDefEq.respectTransparency false in
 mutual
 private theorem mergeSortTR₂_run_eq_mergeSort : {n : Nat} → (l : { l : List α // l.length = n }) → mergeSortTR₂.run le l = mergeSort l.1 le
   | 0, ⟨[], _⟩

src/Init/Data/List/ToArray.lean

@@ -280,6 +280,7 @@ theorem findRevM?_toArray [Monad m] [LawfulMonad m] (f : α → m Bool) (l : Lis
     simp only [forIn_cons, find?]
     by_cases f a <;> simp_all
 
+set_option backward.isDefEq.respectTransparency false in
 private theorem findFinIdx?_loop_toArray (w : l' = l.drop j) :
     Array.findFinIdx?.loop p l.toArray j = List.findFinIdx?.go p l l' j h := by
   unfold findFinIdx?.loop
@@ -316,6 +317,7 @@ termination_by l.length - j
   rw [Array.findIdx?_eq_map_findFinIdx?_val, findIdx?_eq_map_findFinIdx?_val]
   simp [Array.size]
 
+set_option backward.isDefEq.respectTransparency false in
 private theorem idxAuxOf_toArray [BEq α] (a : α) (l : List α) (j : Nat) (w : l' = l.drop j) (h) :
     l.toArray.idxOfAux a j = findFinIdx?.go (fun x => x == a) l l' j h := by
   unfold idxOfAux
@@ -361,6 +363,7 @@ termination_by l.length - j
     as.toArray.idxOf a = as.idxOf a := by
   rw [Array.idxOf, findIdx_toArray, idxOf]
 
+set_option backward.isDefEq.respectTransparency false in
 theorem isPrefixOfAux_toArray_succ [BEq α] (l₁ l₂ : List α) (hle : l₁.length ≤ l₂.length) (i : Nat) :
     Array.isPrefixOfAux l₁.toArray l₂.toArray hle (i + 1) =
       Array.isPrefixOfAux l₁.tail.toArray l₂.tail.toArray (by simp; omega) i := by
@@ -586,7 +589,7 @@ theorem flatMap_toArray_cons {β} (f : α → Array β) (a : α) (as : List α)
 @[simp, grind =] theorem swap_toArray (l : List α) (i j : Nat) {hi hj}:
     l.toArray.swap i j hi hj = ((l.set i l[j]).set j l[i]).toArray := by
   apply ext'
-  simp
+  simp; rfl
 
 @[simp, grind =] theorem eraseIdx_toArray (l : List α) (i : Nat) (h : i < l.toArray.size) :
     l.toArray.eraseIdx i h = (l.eraseIdx i).toArray := by
@@ -616,13 +619,13 @@ decreasing_by
 @[simp, grind =] theorem eraseP_toArray {as : List α} {p : α → Bool} :
     as.toArray.eraseP p = (as.eraseP p).toArray := by
   rw [Array.eraseP, List.eraseP_eq_eraseIdx, findFinIdx?_toArray]
-  split <;> simp [*, findIdx?_eq_map_findFinIdx?_val]
+  split <;> simp [*, findIdx?_eq_map_findFinIdx?_val] <;> rfl
 
 @[simp, grind =] theorem erase_toArray [BEq α] {as : List α} {a : α} :
     as.toArray.erase a = (as.erase a).toArray := by
   rw [Array.erase, finIdxOf?_toArray, List.erase_eq_eraseIdx]
   rw [idxOf?_eq_map_finIdxOf?_val]
-  split <;> simp_all
+  split <;> simp_all <;> rfl
 
 private theorem insertIdx_loop_toArray (i : Nat) (l : List α) (j : Nat) (hj : j < l.toArray.size) (h : i ≤ j) :
     insertIdx.loop i l.toArray ⟨j, hj⟩ = (l.take i ++ l[j] :: (l.take j).drop i ++ l.drop (j + 1)).toArray := by
@@ -639,10 +642,10 @@ private theorem insertIdx_loop_toArray (i : Nat) (l : List α) (j : Nat) (hj : j
       getElem_set_self, take_set_of_le (j := j - 1) (by omega),
       take_set_of_le (j := j - 1) (by omega), take_eq_append_getElem_of_pos (by omega) hj,
       drop_append_of_le_length (by simp; omega)]
-    simp only [append_assoc, cons_append, nil_append, append_cancel_right_eq]
+    simp only [append_assoc, cons_append, nil_append]
     cases i with
-    | zero => simp
-    | succ i => rw [take_set_of_le (by omega)]
+    | zero => simp; rfl
+    | succ i => rw [take_set_of_le (by omega)]; rfl
   · simp only [Nat.not_lt] at h'
     have : i = j := by omega
     subst this

src/Init/Data/Nat/Fold.lean

@@ -400,6 +400,7 @@ theorem dfold_add
   induction m with
   | zero => simp; rfl
   | succ m ih =>
+    set_option backward.isDefEq.respectTransparency false in
     simp [dfold_congr (Nat.add_assoc n m 1).symm, ih]
 
 @[simp] theorem dfoldRev_zero
@@ -434,7 +435,9 @@ theorem dfoldRev_add
         (dfoldRev m (α := fun i h => α (n + i)) (fun i h => f (n + i) (by omega)) init) := by
   induction m with
   | zero => simp; rfl
-  | succ m ih => simp [← Nat.add_assoc, ih]
+  | succ m ih =>
+    set_option backward.isDefEq.respectTransparency false in
+    simp [← Nat.add_assoc, ih]
 
 end Nat
 

src/Init/Data/Option/Attach.lean

@@ -444,6 +444,7 @@ instance : MonadAttach Option where
   CanReturn x a := x = some a
   attach x := x.attach
 
+set_option backward.isDefEq.respectTransparency false in
 public instance : LawfulMonadAttach Option where
   map_attach {α} x := by simp [MonadAttach.attach]
   canReturn_map_imp {α P x a} := by
@@ -455,6 +456,7 @@ end Option
 
 namespace OptionT
 
+set_option backward.isDefEq.respectTransparency false in
 public instance [Monad m] [MonadAttach m] [LawfulMonad m] [WeaklyLawfulMonadAttach m] :
     WeaklyLawfulMonadAttach (OptionT m) where
   map_attach {α} x := by

src/Init/Data/Order/PackageFactories.lean

@@ -794,6 +794,7 @@ automatically. If it fails, it is necessary to provide some of the fields manual
 @[expose]
 public def LinearOrderPackage.ofOrd (α : Type u)
     (args : Packages.LinearOrderOfOrdArgs α := by exact {}) : LinearOrderPackage α :=
+  set_option backward.isDefEq.respectTransparency false in
   letI := LinearPreorderPackage.ofOrd α args.toLinearPreorderOfOrdArgs
   haveI : LawfulEqOrd α := ⟨args.eq_of_compare _ _⟩
   letI : Min α := args.min

src/Init/Data/Range/Polymorphic/RangeIterator.lean

@@ -102,7 +102,7 @@ theorem Iterator.Monadic.isPlausibleStep_iff [UpwardEnumerable α] [LE α] [Deci
 theorem Iterator.Monadic.step_eq_step [UpwardEnumerable α] [LE α] [DecidableLE α]
     {it : IterM (α := Rxc.Iterator α) Id α} :
     Std.Iterator.step it = pure (.deflate ⟨Iterator.Monadic.step it, isPlausibleStep_iff.mpr rfl⟩) := by
-  simp [Std.Iterator.step]
+  simp [Std.Iterator.step]; rfl
 
 theorem Iterator.isPlausibleStep_iff [UpwardEnumerable α] [LE α] [DecidableLE α]
     {it : Iter (α := Rxc.Iterator α) α} {step} :
@@ -535,6 +535,7 @@ private theorem Iterator.instIteratorLoop.loop_eq_wf [UpwardEnumerable α] [LE
     · rw [WellFounded.fix_eq]
       simp_all
 
+set_option backward.isDefEq.respectTransparency false in
 private theorem Iterator.instIteratorLoop.loopWf_eq [UpwardEnumerable α] [LE α] [DecidableLE α]
     [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α]
     {n : Type u → Type w} [Monad n] [LawfulMonad n] (γ : Type u)
@@ -586,6 +587,7 @@ termination_by IteratorLoop.WithWF.mk ⟨⟨some next, upperBound⟩⟩ acc (hwf
 decreasing_by
   simp [IteratorLoop.rel, Monadic.isPlausibleStep_iff, Monadic.step, *]
 
+set_option backward.isDefEq.respectTransparency false in
 instance Iterator.instLawfulIteratorLoop [UpwardEnumerable α] [LE α] [DecidableLE α]
     [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α]
     {n : Type u → Type w} [Monad n] [LawfulMonad n] :
@@ -678,7 +680,7 @@ theorem Iterator.Monadic.isPlausibleStep_iff [UpwardEnumerable α] [LT α] [Deci
 theorem Iterator.Monadic.step_eq_step [UpwardEnumerable α] [LT α] [DecidableLT α]
     {it : IterM (α := Rxo.Iterator α) Id α} :
     Std.Iterator.step it = pure (.deflate ⟨Iterator.Monadic.step it, isPlausibleStep_iff.mpr rfl⟩) := by
-  simp [Std.Iterator.step]
+  simp [Std.Iterator.step]; rfl
 
 theorem Iterator.isPlausibleStep_iff [UpwardEnumerable α] [LT α] [DecidableLT α]
     {it : Iter (α := Rxo.Iterator α) α} {step} :
@@ -1107,6 +1109,7 @@ private theorem Iterator.instIteratorLoop.loop_eq_wf [UpwardEnumerable α] [LT
     · rw [WellFounded.fix_eq]
       simp_all
 
+set_option backward.isDefEq.respectTransparency false in
 private theorem Iterator.instIteratorLoop.loopWf_eq [UpwardEnumerable α] [LT α] [DecidableLT α]
     [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α]
     {n : Type u → Type w} [Monad n] [LawfulMonad n] (γ : Type u)
@@ -1158,6 +1161,7 @@ termination_by IteratorLoop.WithWF.mk ⟨⟨some next, upperBound⟩⟩ acc (hwf
 decreasing_by
   simp [IteratorLoop.rel, Monadic.isPlausibleStep_iff, Monadic.step, *]
 
+set_option backward.isDefEq.respectTransparency false in
 instance Iterator.instLawfulIteratorLoop [UpwardEnumerable α] [LT α] [DecidableLT α]
     [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α]
     {n : Type u → Type w} [Monad n] [LawfulMonad n] :
@@ -1240,7 +1244,7 @@ theorem Iterator.Monadic.isPlausibleStep_iff [UpwardEnumerable α]
 theorem Iterator.Monadic.step_eq_step [UpwardEnumerable α]
     {it : IterM (α := Rxi.Iterator α) Id α} :
     it.step = pure (.deflate ⟨Iterator.Monadic.step it, isPlausibleStep_iff.mpr rfl⟩) := by
-  simp [IterM.step, Std.Iterator.step]
+  simp [IterM.step, Std.Iterator.step]; rfl
 
 theorem Iterator.isPlausibleStep_iff [UpwardEnumerable α]
     {it : Iter (α := Rxi.Iterator α) α} {step} :

src/Init/Data/Slice/Array/Lemmas.lean

@@ -28,6 +28,7 @@ open Std Std.Iterators Std.PRange Std.Slice
 
 namespace SubarrayIterator
 
+set_option backward.isDefEq.respectTransparency false in
 theorem step_eq {it : Iter (α := SubarrayIterator α) α} :
     it.step = if h : it.1.xs.start < it.1.xs.stop then
         haveI := it.1.xs.start_le_stop
@@ -66,6 +67,7 @@ theorem val_step_eq {it : Iter (α := SubarrayIterator α) α} :
   simp only [step_eq]
   split <;> simp
 
+set_option backward.isDefEq.respectTransparency false in
 theorem toList_eq {α : Type u} {it : Iter (α := SubarrayIterator α) α} :
     it.toList =
       (it.internalState.xs.array.toList.take it.internalState.xs.stop).drop it.internalState.xs.start := by
@@ -104,11 +106,13 @@ theorem Internal.iter_eq {α : Type u} {s : Subarray α} :
     Internal.iter s = ⟨⟨s⟩⟩ :=
   rfl
 
+set_option backward.isDefEq.respectTransparency false in
 theorem Internal.toList_iter {α : Type u} {s : Subarray α} :
     (Internal.iter s).toList =
       (s.array.toList.take s.stop).drop s.start := by
   simp [SubarrayIterator.toList_eq, Internal.iter_eq_toIteratorIter, ToIterator.iter_eq]
 
+set_option backward.isDefEq.respectTransparency false in
 public instance : LawfulSliceSize (Internal.SubarrayData α) where
   lawful s := by
     simp [SliceSize.size, ToIterator.iter_eq,
@@ -274,7 +278,7 @@ public theorem Subarray.getElem_eq_getElem_array {xs : Subarray α} {h : i < xs.
 
 public theorem Subarray.getElem_toList {xs : Subarray α} {h : i < xs.toList.length} :
     xs.toList[i]'h = xs[i]'(by simpa using h) := by
-  simp [getElem_eq_getElem_array, toList_eq_drop_take]
+  simp [getElem_eq_getElem_array, toList_eq_drop_take]; rfl
 
 public theorem Subarray.getElem_eq_getElem_toList {xs : Subarray α} {h : i < xs.size} :
     xs[i]'h = xs.toList[i]'(by simpa using h) := by

src/Init/Data/Slice/List/Lemmas.lean

@@ -27,7 +27,7 @@ theorem internalIter_eq {α : Type u} {s : ListSlice α} :
     Internal.iter s = match s.internalRepresentation.stop with
         | some stop => s.internalRepresentation.list.iter.take stop
         | none => s.internalRepresentation.list.iter.toTake := by
-  simp only [Internal.iter, ToIterator.iter_eq]; rfl
+  simp only [Internal.iter]; rfl
 
 theorem toList_internalIter {α : Type u} {s : ListSlice α} :
     (Internal.iter s).toList = match s.internalRepresentation.stop with

src/Init/Data/String/Basic.lean

@@ -748,6 +748,7 @@ theorem _root_.ByteArray.IsValidUTF8.isUTF8FirstByte_getElem_zero {b : ByteArray
 theorem isUTF8FirstByte_getUTF8Byte_zero {b : String} {h} : (b.getUTF8Byte 0 h).IsUTF8FirstByte :=
   b.isValidUTF8.isUTF8FirstByte_getElem_zero _
 
+set_option backward.isDefEq.respectTransparency false in
 theorem Pos.Raw.isValidUTF8_extract_iff {s : String} (p₁ p₂ : Pos.Raw) (hle : p₁ ≤ p₂) (hle' : p₂ ≤ s.rawEndPos) :
     (s.toByteArray.extract p₁.byteIdx p₂.byteIdx).IsValidUTF8 ↔ p₁ = p₂ ∨ (p₁.IsValid s ∧ p₂.IsValid s) := by
   have hle'' : p₂.byteIdx ≤ s.toByteArray.size := by simpa [le_iff] using hle'

src/Init/Data/String/Decode.lean

@@ -1121,30 +1121,35 @@ theorem utf8Size_le_of_utf8DecodeChar?_eq_some {b : ByteArray} {c : Char} :
   | case8 => simp
   | case9 => simp
 
+set_option backward.isDefEq.respectTransparency false in
 theorem utf8DecodeChar?_eq_assemble₁ {b : ByteArray} (hb : 1 ≤ b.size) (h : parseFirstByte b[0] = .done) :
     b.utf8DecodeChar? 0 = assemble₁ b[0] h := by
   fun_cases ByteArray.utf8DecodeChar?
   all_goals try (simp_all; done)
   all_goals omega
 
+set_option backward.isDefEq.respectTransparency false in
 theorem utf8DecodeChar?_eq_assemble₂ {b : ByteArray} (hb : 2 ≤ b.size) (h : parseFirstByte b[0] = .oneMore) :
     b.utf8DecodeChar? 0 = assemble₂ b[0] b[1] := by
   fun_cases ByteArray.utf8DecodeChar?
   all_goals try (simp_all; done)
   all_goals omega
 
+set_option backward.isDefEq.respectTransparency false in
 theorem utf8DecodeChar?_eq_assemble₃ {b : ByteArray} (hb : 3 ≤ b.size) (h : parseFirstByte b[0] = .twoMore) :
     b.utf8DecodeChar? 0 = assemble₃ b[0] b[1] b[2] := by
   fun_cases ByteArray.utf8DecodeChar?
   all_goals try (simp_all; done)
   all_goals omega
 
+set_option backward.isDefEq.respectTransparency false in
 theorem utf8DecodeChar?_eq_assemble₄ {b : ByteArray} (hb : 4 ≤ b.size) (h : parseFirstByte b[0] = .threeMore) :
     b.utf8DecodeChar? 0 = assemble₄ b[0] b[1] b[2] b[3] := by
   fun_cases ByteArray.utf8DecodeChar?
   all_goals try (simp_all; done)
   all_goals omega
 
+set_option backward.isDefEq.respectTransparency false in
 theorem utf8DecodeChar?_append_eq_assemble₁ {l : List UInt8} {b : ByteArray} (hl : l.length = 1) (h : parseFirstByte l[0] = .done) :
     (l.toByteArray ++ b).utf8DecodeChar? 0 = assemble₁ l[0] h := by
   have : (l.toByteArray ++ b)[0]'(by simp [hl]; omega) = l[0] := by

src/Init/Data/String/Lemmas/Basic.lean

@@ -106,25 +106,28 @@ These lemmas are slightly evil because they are non-definitional equalities betw
 are useful and they are at least equalities between slices with definitionally equal underlying
 strings, so it should be fine.
 -/
-
+set_option backward.isDefEq.respectTransparency false in
 @[simp]
 theorem Slice.sliceTo_sliceFrom {s : Slice} {pos pos'} :
     (s.sliceFrom pos).sliceTo pos' =
       s.slice pos (Slice.Pos.ofSliceFrom pos') Slice.Pos.le_ofSliceFrom := by
   ext <;> simp [String.Pos.ext_iff, Pos.Raw.offsetBy_assoc]
 
+set_option backward.isDefEq.respectTransparency false in
 @[simp]
 theorem Slice.sliceFrom_sliceTo {s : Slice} {pos pos'} :
     (s.sliceTo pos).sliceFrom pos' =
       s.slice (Slice.Pos.ofSliceTo pos') pos Slice.Pos.ofSliceTo_le := by
   ext <;> simp [String.Pos.ext_iff]
 
+set_option backward.isDefEq.respectTransparency false in
 @[simp]
 theorem Slice.sliceFrom_sliceFrom {s : Slice} {pos pos'} :
     (s.sliceFrom pos).sliceFrom pos' =
       s.sliceFrom (Slice.Pos.ofSliceFrom pos') := by
   ext <;> simp [String.Pos.ext_iff, Pos.Raw.offsetBy_assoc]
 
+set_option backward.isDefEq.respectTransparency false in
 @[simp]
 theorem Slice.sliceTo_sliceTo {s : Slice} {pos pos'} :
     (s.sliceTo pos).sliceTo pos' = s.sliceTo (Slice.Pos.ofSliceTo pos') := by

src/Init/Data/String/Lemmas/Iterate.lean

@@ -60,6 +60,7 @@ 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 false in
 @[simp]
 theorem toList_positionsFrom {s : Slice} {p : s.Pos} :
     (s.positionsFrom p).toList = Model.positionsFrom p := by
@@ -114,6 +115,7 @@ 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 false in
 @[simp]
 theorem toList_revPositionsFrom {s : Slice} {p : s.Pos} :
     (s.revPositionsFrom p).toList = Model.revPositionsFrom p := by
@@ -184,6 +186,7 @@ theorem Model.map_get_positionsFrom_startPos {s : String} :
     (Model.positionsFrom s.startPos).map (fun p => p.1.get p.2) = s.toList :=
   Model.map_get_positionsFrom_of_splits (splits_startPos s)
 
+set_option backward.isDefEq.respectTransparency false in
 @[simp]
 theorem toList_positionsFrom {s : String} {p : s.Pos} :
     (s.positionsFrom p).toList = Model.positionsFrom p := by
@@ -237,6 +240,7 @@ theorem Model.map_get_revPositionsFrom_endPos {s : String} :
     (Model.revPositionsFrom s.endPos).map (fun p => p.1.get p.2) = s.toList.reverse :=
   Model.map_get_revPositionsFrom_of_splits (splits_endPos s)
 
+set_option backward.isDefEq.respectTransparency false in
 @[simp]
 theorem toList_revPositionsFrom {s : String} {p : s.Pos} :
     (s.revPositionsFrom p).toList = Model.revPositionsFrom p := by

src/Init/Data/String/Lemmas/Pattern/Basic.lean

@@ -296,6 +296,7 @@ class LawfulToForwardSearcherModel {ρ : Type} (pat : ρ) [ForwardPatternModel p
     [∀ 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 false in
 theorem LawfulToForwardSearcherModel.defaultImplementation {pat : ρ} [ForwardPattern pat] [StrictForwardPattern pat]
     [ForwardPatternModel pat] [LawfulForwardPatternModel pat] :
     letI : ToForwardSearcher pat (ToForwardSearcher.DefaultForwardSearcher pat) := .defaultImplementation

src/Init/Data/String/Lemmas/Pattern/Split.lean

@@ -197,6 +197,7 @@ theorem IsValidSearchFrom.splitFromSteps_eq_extend_split {ρ : Type} (pat : ρ)
     · exact h' p hp₁ hp
     · exact rej _ (Std.not_lt.1 hp) hp₂
 
+set_option backward.isDefEq.respectTransparency false in
 theorem SplitIterator.toList_eq_splitFromSteps {ρ : Type} {pat : ρ} {σ : Slice → Type}
     [ToForwardSearcher pat σ]
     [∀ s, Std.Iterator (σ s) Id (SearchStep s)] [∀ s, Std.Iterators.Finite (σ s) Id] {s : Slice}

src/Init/Data/String/Lemmas/Pattern/String/ForwardSearcher.lean

@@ -294,6 +294,7 @@ theorem IsTable.push {b : ByteArray} {v : Array Nat} (h : IsTable b v) {d : Nat}
       obtain rfl : i = v.size := by omega
       exact hd
 
+set_option backward.isDefEq.respectTransparency false in
 theorem computeDistance_eq_prefixFunctionRecurrence {s : Slice} (i : Nat)
     (hi : i < s.copy.toByteArray.size) {patByte : UInt8}
     (hpat : patByte = s.copy.toByteArray[i])
@@ -403,6 +404,7 @@ theorem Invariants.isLongestMatchAt {pat s : Slice} {stackPos needlePos : String
   cases h'
   exact h.partialMatch.isLongestMatchAt h.isEmpty_eq_false h.isValidForSlice
 
+set_option backward.isDefEq.respectTransparency false in
 theorem Invariants.not_matchesAt_of_prefixFunction_eq {pat s : Slice}
     {stackPos needlePos : String.Pos.Raw} (h : Invariants pat s needlePos stackPos)
     {k : Nat} {hki} (hk : prefixFunction pat.copy.toByteArray (needlePos.byteIdx - 1) hki = k)
@@ -433,6 +435,7 @@ theorem Invariants.of_prefixFunction_eq {pat s : Slice} {stackPos needlePos : St
   rw [Nat.sub_add_cancel (by simp at h'; omega)] at this
   exact hk ▸ (h.partialMatch.partialMatch_iff.1 this).2
 
+set_option backward.isDefEq.respectTransparency false in
 theorem Invariants.isValidSearchFrom_toList {pat s : Slice} {stackPos needlePos : String.Pos.Raw}
     (it : Std.Iter (α := ForwardSliceSearcher s) (SearchStep s))
     (h : Invariants pat s needlePos stackPos)

src/Init/Data/Vector/Attach.lean

@@ -359,7 +359,7 @@ theorem pmap_append' {p : α → Prop} {f : ∀ a : α, p a → β} {xs : Vector
       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]
+  simp [Array.map_attach_eq_pmap]; rfl
 
 @[simp] theorem attachWith_append {P : α → Prop} {xs : Vector α n} {ys : Vector α m}
     {H : ∀ (a : α), a ∈ xs ++ ys → P a} :

src/Init/Data/Vector/Count.lean

@@ -96,11 +96,13 @@ theorem countP_replicate {a : α} {n : Nat} : countP p (replicate n a) = if p a
   simp only [replicate_eq_mk_replicate, countP_mk]
   simp [Array.countP_replicate]
 
+set_option backward.isDefEq.respectTransparency false in
 theorem boole_getElem_le_countP {p : α → Bool} {xs : Vector α n} (h : i < n) :
     (if p xs[i] then 1 else 0) ≤ xs.countP p := by
   rcases xs with ⟨xs, rfl⟩
   simp [Array.boole_getElem_le_countP]
 
+set_option backward.isDefEq.respectTransparency false in
 @[grind =]
 theorem countP_set {p : α → Bool} {xs : Vector α n} {a : α} (h : i < n) :
     (xs.set i a).countP p = xs.countP p - (if p xs[i] then 1 else 0) + (if p a then 1 else 0) := by
@@ -188,6 +190,7 @@ theorem count_le_count_push {a b : α} {xs : Vector α n} : count a xs ≤ count
   rcases xs with ⟨xs, rfl⟩
   simp
 
+set_option backward.isDefEq.respectTransparency false in
 theorem boole_getElem_le_count {a : α} {xs : Vector α n} (h : i < n) :
     (if xs[i] == a then 1 else 0) ≤ xs.count a := by
   rcases xs with ⟨xs, rfl⟩
@@ -196,7 +199,7 @@ theorem boole_getElem_le_count {a : α} {xs : Vector α n} (h : i < n) :
 theorem count_set {a b : α} {xs : Vector α n} (h : i < n) :
     (xs.set i a).count b = xs.count b - (if xs[i] == b then 1 else 0) + (if a == b then 1 else 0) := by
   rcases xs with ⟨xs, rfl⟩
-  simp [Array.count_set]
+  simp [Array.count_set]; rfl
 
 @[simp] theorem count_cast {xs : Vector α n} : (xs.cast h).count a = xs.count a := by
   rcases xs with ⟨xs, rfl⟩

src/Init/Data/Vector/Extract.lean

@@ -132,6 +132,7 @@ theorem extract_append {xs : Vector α n} {ys : Vector α m} {i j : Nat} :
   rcases ys with ⟨ys, rfl⟩
   simp
 
+set_option backward.isDefEq.respectTransparency false in
 theorem extract_append_left {xs : Vector α n} {ys : Vector α m} :
     (xs ++ ys).extract 0 n = (xs.extract 0 n).cast (by omega) := by
   ext i h
@@ -178,7 +179,7 @@ theorem mem_extract_iff_getElem {xs : Vector α n} {a : α} {i j : Nat} :
 theorem set_eq_push_extract_append_extract {xs : Vector α n} {i : Nat} (h : i < n) {a : α} :
     xs.set i a = ((xs.extract 0 i).push a ++ (xs.extract (i + 1) n)).cast (by omega) := by
   rcases xs with ⟨as, rfl⟩
-  simp [Array.set_eq_push_extract_append_extract]
+  simp [Array.set_eq_push_extract_append_extract]; rfl
 
 theorem extract_reverse {xs : Vector α n} {i j : Nat} :
     xs.reverse.extract i j = (xs.extract (n - j) (n - i)).reverse.cast (by omega) := by

src/Init/Data/Vector/Find.lean

@@ -295,12 +295,12 @@ theorem find?_eq_some_iff_getElem {xs : Vector α n} {p : α → Bool} {b : α}
 /-! ### findFinIdx? -/
 
 @[grind =]
-theorem findFinIdx?_empty {p : α → Bool} : findFinIdx? p (#v[] : Vector α 0) = none := by simp
+theorem findFinIdx?_empty {p : α → Bool} : findFinIdx? p (#v[] : Vector α 0) = none := by simp; rfl
 
 @[grind =]
 theorem findFinIdx?_singleton {a : α} {p : α → Bool} :
     #[a].findFinIdx? p = if p a then some ⟨0, by simp⟩ else none := by
-  simp
+  simp; rfl
 
 @[congr] theorem findFinIdx?_congr {p : α → Bool} {xs : Vector α n} {ys : Vector α n} (w : xs = ys) :
     findFinIdx? p xs = findFinIdx? p ys := by

src/Init/Data/Vector/Lemmas.lean

@@ -528,7 +528,7 @@ theorem toList_zip {as : Vector α n} {bs : Vector β n} :
 @[simp] theorem getElem_toList {xs : Vector α n} {i : Nat} (h : i < xs.toList.length) :
     xs.toList[i] = xs[i]'(by simpa using h) := by
   cases xs
-  simp
+  simp; rfl
 
 @[simp] theorem getElem?_toList {xs : Vector α n} {i : Nat} :
     xs.toList[i]? = xs[i]? := by
@@ -2908,6 +2908,7 @@ theorem replace_extract {xs : Vector α n} {i : Nat} :
   rcases xs with ⟨xs, rfl⟩
   simp [Array.replace_extract]
 
+set_option backward.isDefEq.respectTransparency false in
 @[simp] theorem replace_replicate_self {a : α} (h : 0 < n) :
     (replicate n a).replace a b = (#v[b] ++ replicate (n - 1) a).cast (by omega) := by
   match n, h with
@@ -2926,6 +2927,7 @@ set_option linter.indexVariables false in
 theorem getElem_push_last {xs : Vector α n} {x : α} : (xs.push x)[n] = x := by
   simp
 
+set_option backward.isDefEq.respectTransparency false in
 @[simp] theorem push_pop_back (xs : Vector α (n + 1)) : xs.pop.push xs.back = xs := by
   ext i
   by_cases h : i < n
@@ -3019,6 +3021,7 @@ theorem forall_zero_iff {P : Vector α 0 → Prop} :
     obtain (rfl : xs = #v[]) := (by ext i h; simp at h)
     apply h
 
+set_option backward.isDefEq.respectTransparency false in
 theorem forall_cons_iff {P : Vector α (n + 1) → Prop} :
     (∀ xs : Vector α (n + 1), P xs) ↔ (∀ (x : α) (xs : Vector α n), P (xs.push x)) := by
   constructor

src/Init/Data/Vector/Monadic.lean

@@ -53,7 +53,7 @@ theorem mapM_pure [Monad m] [LawfulMonad m] {xs : Vector α n} (f : α → β) :
     (mk #[] rfl).mapM f = pure #v[] := by
   unfold mapM
   unfold mapM.go
-  simp
+  simp; rfl
 
 @[simp, grind =] theorem mapM_append [Monad m] [LawfulMonad m]
     {f : α → m β} {xs : Vector α n} {ys : Vector α n'} :

src/Init/Data/Vector/OfFn.lean

@@ -119,6 +119,7 @@ theorem ofFnM_succ {n} [Monad m] [LawfulMonad m] {f : Fin (n + 1) → m α} :
       pure (as.push a)) := by
   simp [ofFnM, ofFnM_go_succ]
 
+set_option backward.isDefEq.respectTransparency false in
 theorem ofFnM_add {n m} [Monad m] [LawfulMonad m] {f : Fin (n + k) → m α} :
     ofFnM f = (do
       let as ← ofFnM (fun i => f (i.castLE (Nat.le_add_right n k)))

src/Init/Grind/Ring/Basic.lean

@@ -184,7 +184,7 @@ theorem natCast_succ (n : Nat) : ((n + 1 : Nat) : α) = ((n : α) + 1) := by
 
 theorem ofNat_mul (a b : Nat) : OfNat.ofNat (α := α) (a * b) = OfNat.ofNat a * OfNat.ofNat b := by
   induction b with
-  | zero => simp [Nat.mul_zero, mul_zero]
+  | zero => simp [Nat.mul_zero, mul_zero]; rfl
   | succ a ih => rw [Nat.mul_succ, ofNat_add, ih, ofNat_add, left_distrib, mul_one]
 
 theorem natCast_mul (a b : Nat) : ((a * b : Nat) : α) = ((a : α) * (b : α)) := by

src/Init/GrindInstances/Ring/Fin.lean

@@ -142,6 +142,7 @@ instance (n : Nat) [NeZero n] : IsCharP (Fin n) n := IsCharP.mk' _ _
 example [NeZero n] : ToInt.Neg (Fin n) (.co 0 n) := inferInstance
 example [NeZero n] : ToInt.Sub (Fin n) (.co 0 n) := inferInstance
 
+set_option backward.isDefEq.respectTransparency false in
 instance [i : NeZero n] : ToInt.Pow (Fin n) (.co 0 n) where
   toInt_pow x k := by
     induction k with

src/Init/Hints.lean

@@ -4,17 +4,15 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
-
 prelude
 public import Init.Grind.Tactics
 import Init.NotationExtra
-
 public section
 
 /- Hint for making sure `Not p` is definitionally equal to `p → False` even when
    `TransparencyMode.reducible` -/
 unif_hint (p : Prop) where
-  |- Not p =?= p → False
+  ⊢ Not p =?= p → False
 
 unif_hint (n : Nat) where
   ⊢ n - 0 =?= n

src/Lean/Meta/ExprDefEq.lean

@@ -22,7 +22,7 @@ register_builtin_option backward.isDefEq.lazyWhnfCore : Bool := {
 }
 
 register_builtin_option backward.isDefEq.respectTransparency : Bool := {
-  defValue := false
+  defValue := true
   descr    := "if true (the default), do not bump transparency to `.default` \
   when checking whether implicit arguments are definitionally equal"
 }

src/Std/Data/DHashMap/IteratorLemmas.lean

@@ -22,12 +22,12 @@ open Std.Iterators
 @[simp]
 public theorem step_iter_nil {α : Type u} {β : α → Type v} :
     ((.nil : AssocList α β).iter).step = ⟨.done, rfl⟩ := by
-  simp [Iter.step_eq, iter]
+  simp [Iter.step_eq, iter]; rfl
 
 @[simp]
 public theorem step_iter_cons {α : Type u} {β : α → Type v} {k v} {l : AssocList α β} :
     ((AssocList.cons k v l).iter).step = ⟨.yield l.iter ⟨k, v⟩, rfl⟩ := by
-  simp [Iter.step_eq, iter]
+  simp [Iter.step_eq, iter]; rfl
 
 @[simp]
 public theorem toList_iter {α : Type u} {β : α → Type v} {l : AssocList α β} :

src/Std/Data/DTreeMap/Internal/Zipper.lean

@@ -390,8 +390,8 @@ theorem Zipper.step_done : (done : Zipper α β).step = .done := rfl
 @[simp]
 theorem Zipper.step_cons : (cons k v t it : Zipper α β).step = .yield ⟨it.prependMap t⟩ ⟨k, v⟩ := rfl
 
-@[simp]
-theorem Zipper.val_run_step_toIterM_iter {z : Zipper α β} : z.iter.toIterM.step.run.inflate.val = z.step := by
+set_option backward.isDefEq.respectTransparency false in
+@[simp] theorem Zipper.val_run_step_toIterM_iter {z : Zipper α β} : z.iter.toIterM.step.run.inflate.val = z.step := by
   rw [IterM.step]
   simp only [Iterator.step, Id.run_pure, Shrink.inflate_deflate]
   rfl
@@ -495,6 +495,7 @@ theorem RxcIterator.step_cons_of_not_LE [Ord α] {upper : α} {h : (compare k up
   rw [step, h]
   simp only [Bool.false_eq_true, ↓reduceIte]
 
+set_option backward.isDefEq.respectTransparency false in
 @[simp]
 theorem RxcIterator.val_run_step_toIterM_iter [Ord α] {z : RxcIterator α β} : (⟨z⟩ : Iter (α := RxcIterator α β) ((a : α) × β a)).toIterM.step.run.inflate.val = z.step := by
   rw [IterM.step]
@@ -624,6 +625,7 @@ theorem RxoIterator.step_cons_of_isLT_eq_false [Ord α] {upper : α} {h : (compa
   rw [step, h]
   simp only [Bool.false_eq_true, ↓reduceIte]
 
+set_option backward.isDefEq.respectTransparency false in
 @[simp]
 theorem RxoIterator.val_run_step_toIterM_iter [Ord α] {z : RxoIterator α β} : (⟨z⟩ : Iter (α := RxoIterator α β) ((a : α) × β a)).toIterM.step.run.inflate.val = z.step := by
   rw [IterM.step]
@@ -692,6 +694,7 @@ public def RicSlice.instToIterator {β : α → Type v} [Ord α] :=
     (fun s => ⟨RxcIterator.mk (Zipper.prependMap s.1.treeMap Zipper.done) s.1.range.upper⟩)
 attribute [instance] RicSlice.instToIterator
 
+set_option backward.isDefEq.respectTransparency false in
 public theorem toList_ric {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] (t : Impl α β)
     (ordered : t.Ordered) (bound : α) : t[*...=bound].toList = t.toList.filter (fun e => (compare e.fst bound).isLE) := by
   simp only [Ric.Sliceable.mkSlice, ← Slice.toList_iter, Slice.iter_eq_toIteratorIter,
@@ -721,6 +724,7 @@ public def RicSlice.instToIterator [Ord α] :=
     (⟨RxcIterator.mk (Zipper.prependMap s.1.treeMap Zipper.done) s.1.range.upper⟩ : Iter _ ).map fun e => (e.1)
 attribute [instance] RicSlice.instToIterator
 
+set_option backward.isDefEq.respectTransparency false in
 public theorem toList_ric {α : Type u} [Ord α] [TransOrd α] (t : Impl α (fun _ => Unit))
     (ordered : t.Ordered) (bound : α) : (t : Impl α (fun _ => Unit))[*...=bound].toList = (Internal.Impl.keys t).filter (fun e => (compare e bound).isLE) := by
   simp only [Ric.Sliceable.mkSlice, ← Slice.toList_iter, Slice.iter,
@@ -755,6 +759,7 @@ public def RicSlice.instToIterator {β : Type v} [Ord α] :=
     (⟨RxcIterator.mk (Zipper.prependMap s.1.treeMap Zipper.done) s.1.range.upper⟩ : Iter ((_ : α) × β)).map fun e => (e.1, e.2)
 attribute [instance] RicSlice.instToIterator
 
+set_option backward.isDefEq.respectTransparency false in
 public theorem toList_ric {α : Type u} {β : Type v} [Ord α] [TransOrd α] (t : Impl α (fun _ => β))
     (ordered : t.Ordered) (bound : α) : t[*...=bound].toList = (Internal.Impl.Const.toList t).filter (fun e => (compare e.fst bound).isLE) := by
   simp only [Ric.Sliceable.mkSlice, ← Slice.toList_iter, Slice.iter,
@@ -789,6 +794,7 @@ public def RioSlice.instToIterator {β : α → Type v} [Ord α] :=
     ⟨RxoIterator.mk (Zipper.prependMap s.1.treeMap Zipper.done) s.1.range.upper⟩
 attribute [instance] RioSlice.instToIterator
 
+set_option backward.isDefEq.respectTransparency false in
 public theorem toList_rio {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] (t : Impl α β)
     (ordered : t.Ordered) (bound : α) : t[*...bound].toList = t.toList.filter (fun e => (compare e.fst bound).isLT) := by
   simp only [Rio.Sliceable.mkSlice, ← Slice.toList_iter, Slice.iter,
@@ -819,6 +825,7 @@ public def RioSlice.instToIterator [Ord α] :=
     (⟨RxoIterator.mk (Zipper.prependMap s.1.treeMap Zipper.done) s.1.range.upper⟩ : Iter _ ).map fun e => (e.1)
 attribute [instance] RioSlice.instToIterator
 
+set_option backward.isDefEq.respectTransparency false in
 public theorem toList_rio {α : Type u} [Ord α] [TransOrd α] (t : Impl α (fun _ => Unit))
     (ordered : t.Ordered) (bound : α) : (t : Impl α (fun _ => Unit))[*...<bound].toList = (Internal.Impl.keys t).filter (fun e => (compare e bound).isLT) := by
   simp only [Rio.Sliceable.mkSlice, ← Slice.toList_iter, Slice.iter,
@@ -853,6 +860,7 @@ public def RioSlice.instToIterator {β : Type v} [Ord α] :=
     (⟨RxoIterator.mk (Zipper.prependMap s.1.treeMap Zipper.done) s.1.range.upper⟩ : Iter ((_ : α) × β)).map fun e => (e.1, e.2)
 attribute [instance] RioSlice.instToIterator
 
+set_option backward.isDefEq.respectTransparency false in
 public theorem toList_rio {α : Type u} {β : Type v} [Ord α] [TransOrd α] (t : Impl α (fun _ => β))
     (ordered : t.Ordered) (bound : α) : t[*...<bound].toList = (Internal.Impl.Const.toList t).filter (fun e => (compare e.fst bound).isLT) := by
   simp only [Rio.Sliceable.mkSlice, ← Slice.toList_iter, Slice.iter,
@@ -920,6 +928,7 @@ public def RccSlice.instToIterator {β : α → Type v} [Ord α] :=
     (rccIterator s.1.treeMap s.1.range.lower s.1.range.upper)
 attribute [instance] RccSlice.instToIterator
 
+set_option backward.isDefEq.respectTransparency false in
 public theorem toList_rcc {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] (t : Impl α β)
     (ordered : t.Ordered) (lowerBound upperBound : α) : t[lowerBound...=upperBound].toList = t.toList.filter (fun e => (compare e.fst lowerBound).isGE ∧ (compare e.fst upperBound).isLE) := by
   simp only [Rcc.Sliceable.mkSlice, ← Slice.toList_iter, Slice.iter,
@@ -947,6 +956,7 @@ public def RccSlice.instToIterator [Ord α] :=
     (⟨RxcIterator.mk (Zipper.prependMapGE s.1.treeMap s.1.range.lower .done) s.1.range.upper⟩ : Iter _ ).map fun e => (e.1)
 attribute [instance] RccSlice.instToIterator
 
+set_option backward.isDefEq.respectTransparency false in
 public theorem toList_rcc {α : Type u} [Ord α] [TransOrd α] (t : Impl α (fun _ => Unit))
     (ordered : t.Ordered) (lowerBound upperBound: α) : (t : Impl α (fun _ => Unit))[lowerBound...=upperBound].toList = (Internal.Impl.keys t).filter (fun e => (compare e lowerBound).isGE ∧ (compare e upperBound).isLE) := by
   simp only [Rcc.Sliceable.mkSlice, ← Slice.toList_iter, Slice.iter,
@@ -983,6 +993,7 @@ public def RccSlice.instToIterator {β : Type v} [Ord α] :=
     (⟨RxcIterator.mk (Zipper.prependMapGE s.1.treeMap s.1.range.lower .done) s.1.range.upper⟩ : Iter ((_ : α) × β)).map fun e => (e.1, e.2)
 attribute [instance] RccSlice.instToIterator
 
+set_option backward.isDefEq.respectTransparency false in
 public theorem toList_rcc {α : Type u} {β : Type v} [Ord α] [TransOrd α] (t : Impl α (fun _ => β))
     (ordered : t.Ordered) (lowerBound upperBound : α) : t[lowerBound...=upperBound].toList = (Internal.Impl.Const.toList t).filter (fun e => (compare e.fst lowerBound).isGE ∧ (compare e.fst upperBound).isLE) := by
   simp only [Rcc.Sliceable.mkSlice, ← Slice.toList_iter, Slice.iter,
@@ -1054,6 +1065,7 @@ public def RcoSlice.instToIterator {β : α → Type v} [Ord α] :=
     rcoIterator s.1.treeMap s.1.range.lower s.1.range.upper
 attribute [instance] RcoSlice.instToIterator
 
+set_option backward.isDefEq.respectTransparency false in
 public theorem toList_rco {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] (t : Impl α β)
     (ordered : t.Ordered) (lowerBound upperBound : α) : t[lowerBound...<upperBound].toList = t.toList.filter (fun e => (compare e.fst lowerBound).isGE ∧ (compare e.fst upperBound).isLT) := by
   simp only [Rco.Sliceable.mkSlice, ← Slice.toList_iter, Slice.iter,
@@ -1081,6 +1093,7 @@ public def RcoSlice.instToIterator [Ord α] :=
     (⟨RxoIterator.mk (Zipper.prependMapGE s.1.treeMap s.1.range.lower .done) s.1.range.upper⟩ : Iter _ ).map fun e => (e.1)
 attribute [instance] RcoSlice.instToIterator
 
+set_option backward.isDefEq.respectTransparency false in
 public theorem toList_rco {α : Type u} [Ord α] [TransOrd α] (t : Impl α (fun _ => Unit))
     (ordered : t.Ordered) (lowerBound upperBound: α) : (t : Impl α (fun _ => Unit))[lowerBound...<upperBound].toList = (Internal.Impl.keys t).filter (fun e => (compare e lowerBound).isGE ∧ (compare e upperBound).isLT) := by
   simp only [Rco.Sliceable.mkSlice, ← Slice.toList_iter, Slice.iter,
@@ -1117,6 +1130,7 @@ public def RcoSlice.instToIterator {β : Type v} [Ord α] :=
     (⟨RxoIterator.mk (Zipper.prependMapGE s.1.treeMap s.1.range.lower .done) s.1.range.upper⟩ : Iter ((_ : α) × β)).map fun e => (e.1, e.2)
 attribute [instance] RcoSlice.instToIterator
 
+set_option backward.isDefEq.respectTransparency false in
 public theorem toList_rco {α : Type u} {β : Type v} [Ord α] [TransOrd α] (t : Impl α (fun _ => β))
     (ordered : t.Ordered) (lowerBound upperBound : α) : t[lowerBound...<upperBound].toList = (Internal.Impl.Const.toList t).filter (fun e => (compare e.fst lowerBound).isGE ∧ (compare e.fst upperBound).isLT) := by
   simp only [Rco.Sliceable.mkSlice, ← Slice.toList_iter, Slice.iter,
@@ -1187,6 +1201,7 @@ public def RooSlice.instToIterator {β : α → Type v} [Ord α] :=
     rooIterator s.1.treeMap s.1.range.lower s.1.range.upper
 attribute [instance] RooSlice.instToIterator
 
+set_option backward.isDefEq.respectTransparency false in
 public theorem toList_roo {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] (t : Impl α β)
     (ordered : t.Ordered) (lowerBound upperBound : α) : t[lowerBound<...<upperBound].toList = t.toList.filter (fun e => (compare e.fst lowerBound).isGT ∧ (compare e.fst upperBound).isLT) := by
   simp only [Roo.Sliceable.mkSlice, ← Slice.toList_iter, Slice.iter,
@@ -1214,6 +1229,7 @@ public def RooSlice.instToIterator [Ord α] :=
     (⟨RxoIterator.mk (Zipper.prependMapGT s.1.treeMap s.1.range.lower .done) s.1.range.upper⟩ : Iter _ ).map fun e => (e.1)
 attribute [instance] RooSlice.instToIterator
 
+set_option backward.isDefEq.respectTransparency false in
 public theorem toList_roo {α : Type u} [Ord α] [TransOrd α] (t : Impl α (fun _ => Unit))
     (ordered : t.Ordered) (lowerBound upperBound: α) : (t : Impl α (fun _ => Unit))[lowerBound<...<upperBound].toList = (Internal.Impl.keys t).filter (fun e => (compare e lowerBound).isGT ∧ (compare e upperBound).isLT) := by
   simp only [Roo.Sliceable.mkSlice, ← Slice.toList_iter, Slice.iter,
@@ -1250,6 +1266,7 @@ public def RooSlice.instToIterator {β : Type v} [Ord α] :=
     (⟨RxoIterator.mk (Zipper.prependMapGT s.1.treeMap s.1.range.lower .done) s.1.range.upper⟩ : Iter ((_ : α) × β)).map fun e => (e.1, e.2)
 attribute [instance] RooSlice.instToIterator
 
+set_option backward.isDefEq.respectTransparency false in
 public theorem toList_roo {α : Type u} {β : Type v} [Ord α] [TransOrd α] (t : Impl α (fun _ => β))
     (ordered : t.Ordered) (lowerBound upperBound : α) : t[lowerBound<...<upperBound].toList = (Internal.Impl.Const.toList t).filter (fun e => (compare e.fst lowerBound).isGT ∧ (compare e.fst upperBound).isLT) := by
   simp only [Roo.Sliceable.mkSlice, ← Slice.toList_iter, Slice.iter,
@@ -1321,6 +1338,7 @@ public def RocSlice.instToIterator {β : α → Type v} [Ord α] :=
     rocIterator s.1.treeMap s.1.range.lower s.1.range.upper
 attribute [instance] RocSlice.instToIterator
 
+set_option backward.isDefEq.respectTransparency false in
 public theorem toList_roc {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] (t : Impl α β)
     (ordered : t.Ordered) (lowerBound upperBound : α) : t[lowerBound<...=upperBound].toList = t.toList.filter (fun e => (compare e.fst lowerBound).isGT ∧ (compare e.fst upperBound).isLE) := by
   simp only [Roc.Sliceable.mkSlice, ← Slice.toList_iter, Slice.iter,
@@ -1348,6 +1366,7 @@ public def RocSlice.instToIterator [Ord α] :=
     (⟨RxcIterator.mk (Zipper.prependMapGT s.1.treeMap s.1.range.lower .done) s.1.range.upper⟩ : Iter _ ).map fun e => (e.1)
 attribute [instance] RocSlice.instToIterator
 
+set_option backward.isDefEq.respectTransparency false in
 public theorem toList_roc {α : Type u} [Ord α] [TransOrd α] (t : Impl α (fun _ => Unit))
     (ordered : t.Ordered) (lowerBound upperBound: α) : (t : Impl α (fun _ => Unit))[lowerBound<...=upperBound].toList = (Internal.Impl.keys t).filter (fun e => (compare e lowerBound).isGT ∧ (compare e upperBound).isLE) := by
   simp only [Roc.Sliceable.mkSlice, ← Slice.toList_iter, Slice.iter,
@@ -1384,6 +1403,7 @@ public def RocSlice.instToIterator {β : Type v} [Ord α] :=
     (⟨RxcIterator.mk (Zipper.prependMapGT s.1.treeMap s.1.range.lower .done) s.1.range.upper⟩ : Iter ((_ : α) × β)).map fun e => (e.1, e.2)
 attribute [instance] RocSlice.instToIterator
 
+set_option backward.isDefEq.respectTransparency false in
 public theorem toList_roc {α : Type u} {β : Type v} [Ord α] [TransOrd α] (t : Impl α (fun _ => β))
     (ordered : t.Ordered) (lowerBound upperBound : α) : t[lowerBound<...=upperBound].toList = (Internal.Impl.Const.toList t).filter (fun e => (compare e.fst lowerBound).isGT ∧ (compare e.fst upperBound).isLE) := by
   simp only [Roc.Sliceable.mkSlice, ← Slice.toList_iter, Slice.iter,
@@ -1440,6 +1460,7 @@ public def RciSlice.instToIterator {β : α → Type v} [Ord α] :=
     rciIterator s.1.treeMap s.1.range.lower
 attribute [instance] RciSlice.instToIterator
 
+set_option backward.isDefEq.respectTransparency false in
 public theorem toList_rci {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] (t : Impl α β)
     (ordered : t.Ordered) (lowerBound : α) : t[lowerBound...*].toList = t.toList.filter (fun e => (compare e.fst lowerBound).isGE) := by
   simp only [Rci.Sliceable.mkSlice, ← Slice.toList_iter, Slice.iter,
@@ -1467,6 +1488,7 @@ public def RciSlice.instToIterator [Ord α] :=
     (⟨Zipper.prependMapGE s.1.treeMap s.1.range.lower Zipper.done⟩ : Iter _ ).map fun e => (e.1)
 attribute [instance] RciSlice.instToIterator
 
+set_option backward.isDefEq.respectTransparency false in
 public theorem toList_rci {α : Type u} [Ord α] [TransOrd α] (t : Impl α (fun _ => Unit))
     (ordered : t.Ordered) (lowerBound : α) : (t : Impl α (fun _ => Unit))[lowerBound...*].toList = (Internal.Impl.keys t).filter (fun e => (compare e lowerBound).isGE) := by
   simp only [Rci.Sliceable.mkSlice, ← Slice.toList_iter, Slice.iter,
@@ -1506,6 +1528,7 @@ public def RciSlice.instToIterator {β : Type v} [Ord α] :=
     (⟨(Zipper.prependMapGE s.1.treeMap s.1.range.lower Zipper.done)⟩ : Iter ((_ : α) × β)).map fun e => (e.1, e.2)
 attribute [instance] RciSlice.instToIterator
 
+set_option backward.isDefEq.respectTransparency false in
 public theorem toList_rci {α : Type u} {β : Type v} [Ord α] [TransOrd α] (t : Impl α (fun _ => β))
     (ordered : t.Ordered) (lowerBound : α) : t[lowerBound...*].toList = (Internal.Impl.Const.toList t).filter (fun e => (compare e.fst lowerBound).isGE) := by
   simp only [Rci.Sliceable.mkSlice, ← Slice.toList_iter, Slice.iter,
@@ -1563,6 +1586,7 @@ public def RoiSlice.instToIterator {β : α → Type v} [Ord α] :=
     roiIterator s.1.treeMap s.1.range.lower
 attribute [instance] RoiSlice.instToIterator
 
+set_option backward.isDefEq.respectTransparency false in
 public theorem toList_roi {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] (t : Impl α β)
     (ordered : t.Ordered) (lowerBound : α) : t[lowerBound<...*].toList = t.toList.filter (fun e => (compare e.fst lowerBound).isGT) := by
   simp only [Roi.Sliceable.mkSlice, ← Slice.toList_iter, Slice.iter,
@@ -1590,6 +1614,7 @@ public def RoiSlice.instToIterator [Ord α] :=
     (⟨Zipper.prependMapGT s.1.treeMap s.1.range.lower Zipper.done⟩ : Iter _ ).map fun e => (e.1)
 attribute [instance] RoiSlice.instToIterator
 
+set_option backward.isDefEq.respectTransparency false in
 public theorem toList_roi {α : Type u} [Ord α] [TransOrd α] (t : Impl α (fun _ => Unit))
     (ordered : t.Ordered) (lowerBound : α) : (t : Impl α (fun _ => Unit))[lowerBound<...*].toList = (Internal.Impl.keys t).filter (fun e => (compare e lowerBound).isGT) := by
   simp only [Roi.Sliceable.mkSlice, ← Slice.toList_iter, Slice.iter,
@@ -1629,6 +1654,7 @@ public def RoiSlice.instToIterator {β : Type v} [Ord α] :=
     (⟨(Zipper.prependMapGT s.1.treeMap s.1.range.lower .done)⟩ : Iter ((_ : α) × β)).map fun e => (e.1, e.2)
 attribute [instance] RoiSlice.instToIterator
 
+set_option backward.isDefEq.respectTransparency false in
 public theorem toList_roi {α : Type u} {β : Type v} [Ord α] [TransOrd α] (t : Impl α (fun _ => β))
     (ordered : t.Ordered) (lowerBound : α) : t[lowerBound<...*].toList = (Internal.Impl.Const.toList t).filter (fun e => (compare e.fst lowerBound).isGT) := by
   simp only [Roi.Sliceable.mkSlice, ← Slice.toList_iter, Slice.iter,
@@ -1680,6 +1706,7 @@ public def RiiSlice.instToIterator {β : α → Type v} :=
     riiIterator s.1.treeMap
 attribute [instance] RiiSlice.instToIterator
 
+set_option backward.isDefEq.respectTransparency false in
 public theorem toList_rii {α : Type u} {β : α → Type v} (t : Impl α β) : t[*...*].toList = t.toList := by
   simp only [Rii.Sliceable.mkSlice, ← Slice.toList_iter, Slice.iter,
     Slice.Internal.iter_eq_toIteratorIter, ToIterator.iter, ToIterator.iterM_eq,
@@ -1705,6 +1732,7 @@ public def RiiSlice.instToIterator {α : Type u} :=
     (⟨Zipper.prependMap s.internalRepresentation.treeMap .done⟩ : Iter _ ).map fun e => (e.1)
 attribute [instance] RiiSlice.instToIterator
 
+set_option backward.isDefEq.respectTransparency false in
 public theorem toList_rii {α : Type u} (t : Impl α (fun _ => Unit)) :
     (t : Impl α fun _ => Unit)[*...*].toList = Internal.Impl.keys t := by
   simp only [Rii.Sliceable.mkSlice, ← Slice.toList_iter, Slice.iter,
@@ -1737,6 +1765,7 @@ public def RiiSlice.instToIterator {α : Type u} {β : Type v} :=
     (⟨Zipper.prependMap s.internalRepresentation.treeMap .done⟩ : Iter ((_ : α) × β)).map fun e => (e.1, e.2)
 attribute [instance] RiiSlice.instToIterator
 
+set_option backward.isDefEq.respectTransparency false in
 public theorem toList_rii {α : Type u} {β : Type v} (t : Impl α (fun _ => β)) :
     (t : Impl α fun _ => β)[*...*].toList = Internal.Impl.Const.toList t := by
   simp only [Rii.Sliceable.mkSlice, ← Slice.toList_iter, Slice.iter,

src/Std/Data/Iterators/Lemmas/Combinators/Monadic/DropWhile.lean

@@ -42,6 +42,7 @@ theorem IterM.dropWhile_eq_intermediateDropWhile {α m β} [Monad m]
     it.dropWhile P = Intermediate.dropWhile P true it :=
   rfl
 
+set_option backward.isDefEq.respectTransparency false in
 theorem IterM.step_intermediateDropWhileWithPostcondition {α m β} [Monad m] [Iterator α m β]
     {it : IterM (α := α) m β} {P} {dropping} :
     (IterM.Intermediate.dropWhileWithPostcondition P dropping it).step = (do

src/Std/Data/Iterators/Lemmas/Combinators/Monadic/FilterMap.lean

@@ -76,6 +76,7 @@ theorem IterM.stepAsHetT_filterMapWithPostcondition [Monad m] [LawfulMonad m] [M
     · simp [pure]
     · simp [pure]
 
+set_option backward.isDefEq.respectTransparency false in
 theorem IterM.Equiv.filterMapWithPostcondition {α₁ α₂ β γ : Type w}
     {m : Type w → Type w'} {n : Type w → Type w''}
     [Monad m] [LawfulMonad m] [Monad n] [LawfulMonad n] [Iterator α₁ m β] [Iterator α₂ m β]

src/Std/Data/Iterators/Lemmas/Combinators/Zip.lean

@@ -178,6 +178,7 @@ theorem Iter.toList_intermediateZip_of_finite [Iterator α₁ Id β₁] [Iterato
       · cases hs
         simp
 
+set_option backward.isDefEq.respectTransparency false in
 theorem Iter.atIdxSlow?_intermediateZip [Iterator α₁ Id β₁] [Iterator α₂ Id β₂]
     [Productive α₁ Id] [Productive α₂ Id]
     {it₁ : Iter (α := α₁) β₁} {memo} {it₂ : Iter (α := α₂) β₂} {n : Nat} :

src/Std/Data/Iterators/Lemmas/Equivalence/Basic.lean

@@ -235,6 +235,7 @@ 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 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 β)

src/Std/Data/Iterators/Lemmas/Equivalence/StepCongr.lean

@@ -127,6 +127,7 @@ The difficulty in this lemma is that we want to argue that we can cancel
 `HetT.map QuotStep.bundledQuotient` because `QuotStep.bundledQuotient` is injective. This
 cancellation property does not hold for all monads.
 -/
+set_option backward.isDefEq.respectTransparency false in
 theorem IterM.Equiv.step_eq {α₁ α₂ : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m]
     [Iterator α₁ m β] [Iterator α₂ m β] {ita : IterM (α := α₁) m β} {itb : IterM (α := α₂) m β}
     (h : IterM.Equiv ita itb) :
@@ -161,6 +162,7 @@ theorem IterM.Equiv.step_eq {α₁ α₂ : Type w} {m : Type w → Type w'} [Mon
   let hex := ?hex
   exact hex.choose_spec
 
+set_option backward.isDefEq.respectTransparency false in
 theorem IterM.Equiv.lift_step_bind_congr {α₁ α₂ : Type w} [Monad m] [LawfulMonad m]
     [Monad n] [LawfulMonad n] [MonadLiftT m n] [LawfulMonadLiftT m n]
     [Iterator α₁ m β] [Iterator α₂ m β]

src/Std/Data/Iterators/Lemmas/Producers/Empty.lean

@@ -22,7 +22,7 @@ theorem Iter.toIterM_empty {β} :
 @[simp]
 theorem Iter.step_empty {β} :
     (Iter.empty β).step = ⟨.done, rfl⟩ := by
-  simp [Iter.step]
+  simp [Iter.step]; rfl
 
 @[simp]
 theorem Iter.toList_empty {β} :

src/Std/Data/Iterators/Lemmas/Producers/Monadic/Array.lean

@@ -53,6 +53,7 @@ theorem Array.step_iterM {array : Array β} :
 
 section Equivalence
 
+set_option backward.isDefEq.respectTransparency 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

src/Std/Data/Iterators/Lemmas/Producers/Monadic/List.lean

@@ -16,6 +16,7 @@ open Std.Internal Std.Iterators Std.Iterators.Types
 variable {m : Type w → Type w'} {n : Type w → Type w''} [Monad m] {β : Type w}
 
 -- We don't want to pollute `List` with this rarely used lemma.
+set_option backward.isDefEq.respectTransparency false in
 public theorem Types.ListIterator.stepAsHetT_iterM [LawfulMonad m] {l : List β} :
     (l.iterM m).stepAsHetT = (match l with
       | [] => pure .done

src/Std/Data/Iterators/Lemmas/Producers/Repeat.lean

@@ -19,6 +19,7 @@ open Std.Iterators
 
 variable {α : Type w} {f : α → α} {init : α}
 
+set_option backward.isDefEq.respectTransparency false in
 theorem Iter.step_repeat :
     (Iter.repeat f init).step = .yield (Iter.repeat f (f init)) init ⟨rfl, rfl⟩ := by
   simp [Iter.«repeat», Iter.step, Iter.toIterM, IterM.step, Iterator.step, IterM.toIter]

src/Std/Do/Triple/SpecLemmas.lean

@@ -331,6 +331,7 @@ theorem Spec.liftWith_OptionT [Monad m] [WPMonad m ps]
       (wp⟦f (fun x => x.run)⟧ (Q.1, Q.2.2))
       Q := by simp [Triple.iff]
 
+set_option backward.isDefEq.respectTransparency false in
 @[spec]
 theorem Spec.restoreM_StateT [Monad m] [WPMonad m ps] (x : m (α × σ)) :
     Triple
@@ -345,6 +346,7 @@ theorem Spec.restoreM_ReaderT [Monad m] [WPMonad m ps] (x : m α) :
       (fun s => wp⟦x⟧ (fun a => Q.1 a s, Q.2))
       Q := by simp [Triple.iff]
 
+set_option backward.isDefEq.respectTransparency false in
 @[spec]
 theorem Spec.restoreM_ExceptT [Monad m] [WPMonad m ps] (x : m (Except ε α)) :
     Triple (ps := .except ε ps)
@@ -352,6 +354,7 @@ theorem Spec.restoreM_ExceptT [Monad m] [WPMonad m ps] (x : m (Except ε α)) :
       (wp⟦x⟧ (fun e => e.casesOn Q.2.1 Q.1, Q.2.2))
       Q := by simp [Triple.iff]
 
+set_option backward.isDefEq.respectTransparency false in
 @[spec]
 theorem Spec.restoreM_OptionT [Monad m] [WPMonad m ps] (x : m (Option α)) :
     Triple (ps := .except PUnit ps)

src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Extract.lean

@@ -56,7 +56,7 @@ instance : AIG.LawfulVecOperator α ExtractTarget blastExtract where
   decl_eq := by
     intros
     unfold blastExtract
-    simp
+    simp; rfl
 
 end bitblast
 end BVExpr

src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/RotateLeft.lean

@@ -57,7 +57,7 @@ instance : AIG.LawfulVecOperator α AIG.ShiftTarget blastRotateLeft where
   decl_eq := by
     intros
     unfold blastRotateLeft
-    dsimp only
+    dsimp only; rfl
 
 end bitblast
 end BVExpr

src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/RotateRight.lean

@@ -57,7 +57,7 @@ instance : AIG.LawfulVecOperator α AIG.ShiftTarget blastRotateRight where
   decl_eq := by
     intros
     unfold blastRotateRight
-    dsimp only
+    dsimp only; rfl
 
 end bitblast
 end BVExpr

src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/ShiftRight.lean

@@ -117,7 +117,7 @@ instance : AIG.LawfulVecOperator α AIG.ShiftTarget blastArithShiftRightConst wh
   decl_eq := by
     intros
     unfold blastArithShiftRightConst
-    simp
+    simp; rfl
 
 structure TwoPowShiftTarget (aig : AIG α) (w : Nat) where
   n : Nat

src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Replicate.lean

@@ -52,6 +52,7 @@ theorem aux4 {a b c : Nat} (hidx : a < b * c) (h : c ≤ n) : a < b * n := by
   | inl h => apply aux3 <;> assumption
   | inr h => simp_all
 
+set_option backward.isDefEq.respectTransparency false in
 theorem go_get_aux (aig : AIG α) (n : Nat) (curr : Nat) (hcurr : curr ≤ n)
     (input : AIG.RefVec aig w) (s : AIG.RefVec aig (w * curr)) :
     ∀ (idx : Nat) (hidx : idx < w * curr),
@@ -72,6 +73,7 @@ theorem go_get_aux (aig : AIG α) (n : Nat) (curr : Nat) (hcurr : curr ≤ n)
     simp
 termination_by n - curr
 
+set_option backward.isDefEq.respectTransparency false in
 theorem go_get (aig : AIG α) (n : Nat) (curr : Nat) (hcurr : curr ≤ n)
     (input : AIG.RefVec aig w) (s : AIG.RefVec aig (w * curr)) :
     ∀ (idx : Nat) (hidx1 : idx < w * n),

src/Std/Tactic/BVDecide/LRAT/Internal/Formula/Lemmas.lean

@@ -358,6 +358,7 @@ theorem deleteOne_preserves_assignments_size {n : Nat} (f : DefaultFormula n) (i
   simp only [deleteOne]
   grind
 
+set_option backward.isDefEq.respectTransparency false in
 theorem deleteOne_preserves_strongAssignmentsInvariant {n : Nat} (f : DefaultFormula n) (id : Nat) :
     StrongAssignmentsInvariant f → StrongAssignmentsInvariant (deleteOne f id) := by
   intro hf

src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddSound.lean

@@ -403,6 +403,7 @@ theorem c_without_negPivot_of_performRatCheck_success {n : Nat} (f : DefaultForm
       rw [DefaultFormula.formulaEntails_def, List.all_eq_true] at pfc
       exact of_decide_eq_true (pfc (c.delete negPivot) (by simp [insert_iff]))
 
+set_option backward.isDefEq.respectTransparency false in
 theorem existsRatHint_of_ratHintsExhaustive {n : Nat} (f : DefaultFormula n)
     (f_readyForRatAdd : ReadyForRatAdd f) (pivot : Literal (PosFin n))
     (ratHints : Array (Nat × Array Nat))

src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean

@@ -951,6 +951,7 @@ theorem nodup_derivedLits {n : Nat} (f : DefaultFormula n)
       specialize h3 ⟨j.1, j_in_bounds⟩ j_ne_k
       simp only [derivedLits_arr_def, Fin.getElem_fin] at li_eq_lj
       simp only [Fin.getElem_fin, derivedLits_arr_def, ne_eq, li, li_eq_lj] at h3
+      set_option backward.isDefEq.respectTransparency false in
       simp only [List.get_eq_getElem, ← Array.getElem_toList, not_true_eq_false] at h3
     next k_ne_i =>
       have i_ne_k : ⟨i.1, i_in_bounds⟩ ≠ k := by intro i_eq_k; simp only [← i_eq_k, not_true] at k_ne_i

src/Std/Time/Date/ValidDate.lean

@@ -57,6 +57,7 @@ def dayOfYear (ordinal : ValidDate leap) : Day.Ordinal.OfYear leap :=
   | true, bounded => bounded
   | false, bounded => bounded
 
+set_option backward.isDefEq.respectTransparency false in
 /--
 Transforms a `Day.Ordinal.OfYear` into a tuple of a `Month` and a `Day`.
 -/

stage0/src/stdlib_flags.h

@@ -12,6 +12,7 @@ options get_default_options() {
     // switch to `true` for ABI-breaking changes affecting meta code;
     // see also next option!
     opts = opts.update({"interpreter", "prefer_native"}, false);
+    opts = opts.update({"backward", "isDefEq", "respectTransparency"}, true);
     // switch to `false` when enabling `prefer_native` should also affect use
     // of built-in parsers in quotations; this is usually the case, but setting
     // both to `true` may be necessary for handling non-builtin parsers with

tests/lean/beginEndAsMacro.lean

@@ -8,7 +8,7 @@ macro "begin " ts:tactic,*,? i:"end" : term => do
 theorem ex1 (x : Nat) : x + 0 = 0 + x :=
   begin
     rw [Nat.add_zero],
-    rw [Nat.zero_add],
+    rw [Nat.zero_add]
   end
 /- ANCHOR_END: doc -/
 

tests/lean/run/1302.lean

@@ -10,4 +10,8 @@ example (a : Bool) : (a :: as).get ⟨0, by simp +arith⟩ = a := by
   simp
 
 example (a b c : α) : [a, b, c].get ⟨0, by simp (config := { decide := true })⟩ = a := by
-  rw [Fin.zero_eta, get_cons_zero]
+  erw [Fin.zero_eta]
+  rw [get_cons_zero]
+
+example (a b c : α) : [a, b, c].get ⟨0, by simp (config := { decide := true })⟩ = a := by
+  rw [List.get]

tests/lean/run/1986.lean

@@ -197,7 +197,7 @@ instance Pi.completeDistribLattice' {ι : Type _} {π : ι → Type _}
 CompleteDistribLattice.mk (Pi.coframe.infᵢ_sup_le_sup_infₛ)
 
 -- User: takes around 2 seconds wall clock time on my PC (but very quick in Lean 3)
-set_option maxHeartbeats 400 -- make sure it stays fast
+set_option maxHeartbeats 600 -- make sure it stays fast
 set_option synthInstance.maxHeartbeats 400
 instance Pi.completeDistribLattice'' {ι : Type _} {π : ι → Type _}
     [∀ i, CompleteDistribLattice (π i)] : CompleteDistribLattice (∀ i, π i) :=

tests/lean/run/3807.lean

@@ -1,5 +1,4 @@
 import Lean.Elab.Binders
-
 /-!
 
 This is a test case extracted from Mathlib exhibiting a slow-down in `IsDefEq` after
@@ -12,9 +11,6 @@ but I think it makes a better test case going forward as is.
 The original declaration take around 16,000 heartbeats prior to #3807, but around 210,000 after.
 
 -/
-
-
-
 section Mathlib.Tactic.Spread
 
 open Lean Parser.Term Macro
@@ -1151,6 +1147,7 @@ variable [FunLike F α β]
 
 variable {_ : NonAssocSemiring α} {_ : NonAssocSemiring β} [RingHomClass F α β]
 
+@[instance_reducible]
 def RingHomClass.toRingHom (f : F) : α →+* β :=
   { (f : α →* β), (f : α →+ β) with }
 
@@ -1178,6 +1175,7 @@ end coe
 
 variable {_ : NonAssocSemiring α} {_ : NonAssocSemiring β} {_ : NonAssocSemiring γ}
 
+@[instance_reducible]
 def comp (g : β →+* γ) (f : α →+* β) : α →+* γ :=
   { g.toNonUnitalRingHom.comp f.toNonUnitalRingHom with
     toFun := g ∘ f
@@ -1196,33 +1194,41 @@ namespace Injective
 
 variable {M₁ : Type _} {M₂ : Type _} [Mul M₁]
 
+@[instance_reducible]
 protected def semigroup [Semigroup M₂] (f : M₁ → M₂) (hf : Injective f) : Semigroup M₁ :=
   { ‹Mul M₁› with mul_assoc := sorry }
 
+@[instance_reducible]
 protected def addSemigroup {M₁} [Add M₁] [AddSemigroup M₂] (f : M₁ → M₂) (hf : Injective f) : AddSemigroup M₁ :=
   { ‹Add M₁› with add_assoc := sorry }
 
+@[instance_reducible]
 protected def commMagma [CommMagma M₂] (f : M₁ → M₂) (hf : Injective f) : CommMagma M₁ where
   mul_comm x y := sorry
 
+@[instance_reducible]
 protected def addCommMagma {M₁} [Add M₁] [AddCommMagma M₂] (f : M₁ → M₂) (hf : Injective f) : AddCommMagma M₁ where
   add_comm x y := sorry
 
+@[instance_reducible]
 protected def commSemigroup [CommSemigroup M₂] (f : M₁ → M₂) (hf : Injective f) : CommSemigroup M₁ where
   toSemigroup := hf.semigroup f
   __ := hf.commMagma f
 
+@[instance_reducible]
 protected def addCommSemigroup {M₁} [Add M₁] [AddCommSemigroup M₂] (f : M₁ → M₂) (hf : Injective f) : AddCommSemigroup M₁ where
   toAddSemigroup := hf.addSemigroup f
   __ := hf.addCommMagma f
 
 variable [One M₁]
 
+@[instance_reducible]
 protected def mulOneClass [MulOneClass M₂] (f : M₁ → M₂) (hf : Injective f) : MulOneClass M₁ :=
   { ‹One M₁›, ‹Mul M₁› with
     one_mul := sorry,
     mul_one := sorry }
 
+@[instance_reducible]
 protected def addZeroClass {M₁} [Zero M₁] [Add M₁] [AddZeroClass M₂] (f : M₁ → M₂) (hf : Injective f) : AddZeroClass M₁ :=
   { ‹Zero M₁›, ‹Add M₁› with
     zero_add := sorry,
@@ -1230,18 +1236,21 @@ protected def addZeroClass {M₁} [Zero M₁] [Add M₁] [AddZeroClass M₂] (f
 
 variable [Pow M₁ Nat]
 
+@[instance_reducible]
 protected def monoid [Monoid M₂] (f : M₁ → M₂) (hf : Injective f) : Monoid M₁ :=
   { hf.mulOneClass f, hf.semigroup f with
     npow := fun n x => x ^ n,
     npow_zero := sorry,
     npow_succ := sorry }
 
+@[instance_reducible]
 protected def addMonoid {M₁} [Zero M₁] [Add M₁] [SMul Nat M₁] [AddMonoid M₂] (f : M₁ → M₂) (hf : Injective f) : AddMonoid M₁ :=
   { hf.addZeroClass f, hf.addSemigroup f with
     nsmul := fun n x => n • x,
     nsmul_zero := sorry,
     nsmul_succ := sorry }
 
+@[instance_reducible]
 protected def addMonoidWithOne {M₁} [Zero M₁] [One M₁] [Add M₁] [SMul Nat M₁] [NatCast M₁]
     [AddMonoidWithOne M₂] (f : M₁ → M₂) (hf : Injective f) : AddMonoidWithOne M₁ :=
   { hf.addMonoid f with
@@ -1250,16 +1259,19 @@ protected def addMonoidWithOne {M₁} [Zero M₁] [One M₁] [Add M₁] [SMul Na
     natCast_succ := sorry,
     one := 1 }
 
+@[instance_reducible]
 protected def commMonoid [CommMonoid M₂] (f : M₁ → M₂) (hf : Injective f) :
     CommMonoid M₁ :=
   { hf.monoid f, hf.commSemigroup f with }
 
+@[instance_reducible]
 protected def addCommMonoid {M₁} [Zero M₁] [Add M₁] [SMul Nat M₁] [AddCommMonoid M₂] (f : M₁ → M₂) (hf : Injective f) :
     AddCommMonoid M₁ :=
   { hf.addMonoid f, hf.addCommSemigroup f with }
 
 variable [Inv M₁] [Div M₁] [Pow M₁ Int]
 
+@[instance_reducible]
 protected def divInvMonoid [DivInvMonoid M₂] (f : M₁ → M₂) (hf : Injective f) : DivInvMonoid M₁ :=
   { hf.monoid f, ‹Inv M₁›, ‹Div M₁› with
     zpow := fun n x => x ^ n,
@@ -1268,6 +1280,7 @@ protected def divInvMonoid [DivInvMonoid M₂] (f : M₁ → M₂) (hf : Injecti
     zpow_neg' := sorry,
     div_eq_mul_inv := sorry }
 
+@[instance_reducible]
 protected def subNegMonoid {M₁} [Zero M₁] [One M₁] [Add M₁] [SMul Nat M₁] [Neg M₁] [Sub M₁]
     [SMul Int M₁] [SubNegMonoid M₂] (f : M₁ → M₂) (hf : Injective f) : SubNegMonoid M₁ :=
   { hf.addMonoid f, ‹Neg M₁›, ‹Sub M₁› with
@@ -1277,15 +1290,18 @@ protected def subNegMonoid {M₁} [Zero M₁] [One M₁] [Add M₁] [SMul Nat M
     zsmul_neg' := sorry,
     sub_eq_add_neg := sorry }
 
+@[instance_reducible]
 protected def group [Group M₂] (f : M₁ → M₂) (hf : Injective f) : Group M₁ :=
   { hf.divInvMonoid f with
     mul_left_inv := sorry }
 
+@[instance_reducible]
 protected def addGroup {M₁} [Zero M₁] [One M₁] [Add M₁] [SMul Nat M₁] [Neg M₁] [Sub M₁]
     [SMul Int M₁] [AddGroup M₂] (f : M₁ → M₂) (hf : Injective f) : AddGroup M₁ :=
   { hf.subNegMonoid f with
     add_left_neg := sorry }
 
+@[instance_reducible]
 protected def addGroupWithOne {M₁} [Zero M₁] [One M₁] [Add M₁] [SMul Nat M₁] [Neg M₁] [Sub M₁]
     [SMul Int M₁] [NatCast M₁] [IntCast M₁] [AddGroupWithOne M₂] (f : M₁ → M₂) (hf : Injective f) : AddGroupWithOne M₁ :=
   { hf.addGroup f,
@@ -1294,9 +1310,11 @@ protected def addGroupWithOne {M₁} [Zero M₁] [One M₁] [Add M₁] [SMul Nat
     intCast_ofNat := sorry,
     intCast_negSucc := sorry }
 
+@[instance_reducible]
 protected def commGroup [CommGroup M₂] (f : M₁ → M₂) (hf : Injective f) : CommGroup M₁ :=
   { hf.commMonoid f, hf.group f with }
 
+@[instance_reducible]
 protected def addCommGroup {M₁} [Zero M₁] [One M₁] [Add M₁] [SMul Nat M₁] [Neg M₁] [Sub M₁]
     [SMul Int M₁] [AddCommGroup M₂] (f : M₁ → M₂) (hf : Injective f) : AddCommGroup M₁ :=
   { hf.addCommMonoid f, hf.addGroup f with }
@@ -1316,6 +1334,7 @@ section MulZeroClass
 
 variable [MulZeroClass M₀] {a b : M₀}
 
+@[instance_reducible]
 protected def Function.Injective.mulZeroClass [Mul M₀'] [Zero M₀'] (f : M₀' → M₀) (hf : Injective f) : MulZeroClass M₀' where
   mul := (· * ·)
   zero := 0
@@ -1328,6 +1347,7 @@ section MulZeroOneClass
 
 variable [MulZeroOneClass M₀]
 
+@[instance_reducible]
 protected def Function.Injective.mulZeroOneClass [Mul M₀'] [Zero M₀'] [One M₀'] (f : M₀' → M₀)
     (hf : Injective f) :
     MulZeroOneClass M₀' :=
@@ -1337,6 +1357,7 @@ end MulZeroOneClass
 
 section SemigroupWithZero
 
+@[instance_reducible]
 protected def Function.Injective.semigroupWithZero [Zero M₀'] [Mul M₀'] [SemigroupWithZero M₀]
     (f : M₀' → M₀) (hf : Injective f) :
     SemigroupWithZero M₀' :=
@@ -1346,6 +1367,7 @@ end SemigroupWithZero
 
 section MonoidWithZero
 
+@[instance_reducible]
 protected def Function.Injective.monoidWithZero [Zero M₀'] [Mul M₀'] [One M₀'] [Pow M₀' Nat]
     [MonoidWithZero M₀] (f : M₀' → M₀) (hf : Injective f) :
     MonoidWithZero M₀' :=
@@ -1357,6 +1379,7 @@ section GroupWithZero
 
 variable [GroupWithZero G₀] {a b c g h x : G₀}
 
+@[instance_reducible]
 protected def Function.Injective.groupWithZero [Zero G₀'] [Mul G₀'] [One G₀'] [Inv G₀'] [Div G₀']
     [Pow G₀' Nat] [Pow G₀' Int] (f : G₀' → G₀) (hf : Injective f) : GroupWithZero G₀' :=
   { hf.monoidWithZero f,
@@ -1376,6 +1399,7 @@ universe u v x
 
 variable {α : Type u} {β : Type v} {R : Type x}
 
+@[instance_reducible]
 protected def Function.Injective.distrib {S} [Mul R] [Add R] [Distrib S] (f : R → S)
     (hf : Injective f) :
     Distrib R where
@@ -1385,28 +1409,33 @@ protected def Function.Injective.distrib {S} [Mul R] [Add R] [Distrib S] (f : R
 variable [Zero β] [One β] [Add β] [Mul β] [Neg β] [Sub β] [SMul Nat β] [SMul Int β] [Pow β Nat]
   [NatCast β] [IntCast β]
 
+@[instance_reducible]
 protected def Function.Injective.nonUnitalNonAssocSemiring {α : Type u}
     [NonUnitalNonAssocSemiring α] (f : β → α) (hf : Injective f) : NonUnitalNonAssocSemiring β where
   toAddCommMonoid := hf.addCommMonoid f
   __ := hf.distrib f
   __ := hf.mulZeroClass f
 
+@[instance_reducible]
 protected def Function.Injective.nonUnitalSemiring {α : Type u} [NonUnitalSemiring α] (f : β → α)
     (hf : Injective f) :
     NonUnitalSemiring β where
   toNonUnitalNonAssocSemiring := hf.nonUnitalNonAssocSemiring f
   __ := hf.semigroupWithZero f
 
+@[instance_reducible]
 protected def Function.Injective.nonAssocSemiring {α : Type u} [NonAssocSemiring α] [NatCast β] (f : β → α) (hf : Injective f) : NonAssocSemiring β where
   toNonUnitalNonAssocSemiring := hf.nonUnitalNonAssocSemiring f
   __ := hf.mulZeroOneClass f
   __ := hf.addMonoidWithOne f
 
+@[instance_reducible]
 protected def Function.Injective.semiring {α : Type u} [Semiring α] [NatCast β] (f : β → α) (hf : Injective f) : Semiring β where
   toNonUnitalSemiring := hf.nonUnitalSemiring f
   __ := hf.nonAssocSemiring f
   __ := hf.monoidWithZero f
 
+@[instance_reducible]
 protected def Function.Injective.ring [Ring α] (f : β → α) (hf : Injective f) : Ring β where
   toSemiring := hf.semiring f
   __ := hf.addGroupWithOne f

tests/lean/run/4171.lean

@@ -685,6 +685,7 @@ def toComon_ : Comon_ (Mon_ C) ⥤ Comon_ C := (Mon_.forget C).mapComon
 theorem foo {V} [Quiver V] {X Y x} :
     @Quiver.Hom.unop V _ X Y (Opposite.op (unop := x)) = x := rfl
 
+set_option backward.isDefEq.respectTransparency false in
 example (M : Comon_ (Mon_ C)) : Mon_ (Comon_ C) where
   X := (toComon_ C).obj M
   one := { hom := M.X.one }
@@ -693,6 +694,7 @@ example (M : Comon_ (Mon_ C)) : Mon_ (Comon_ C) where
     ext
     simp [(foo)] -- parentheses around `foo` works
 
+set_option backward.isDefEq.respectTransparency false in
 example (M : Comon_ (Mon_ C)) : Mon_ (Comon_ C) where
   X := (toComon_ C).obj M
   one := { hom := M.X.one }
@@ -704,6 +706,7 @@ example (M : Comon_ (Mon_ C)) : Mon_ (Comon_ C) where
 theorem foo' {V} [Quiver V] {X Y x} :
     @Quiver.Hom.unop V _ X Y no_index (Opposite.op (unop := x)) = x := rfl
 
+set_option backward.isDefEq.respectTransparency false in
 example (M : Comon_ (Mon_ C)) : Mon_ (Comon_ C) where
   X := (toComon_ C).obj M
   one := { hom := M.X.one }
@@ -713,6 +716,7 @@ example (M : Comon_ (Mon_ C)) : Mon_ (Comon_ C) where
     simp [foo'] -- or adding a `no_index` in the statement
 
 
+set_option backward.isDefEq.respectTransparency false in
 /--
 trace: [simp] Diagnostics
   [simp] theorems with bad keys
@@ -734,6 +738,7 @@ example (M : Comon_ (Mon_ C)) : Mon_ (Comon_ C) where
 
 attribute [simp] foo
 
+set_option backward.isDefEq.respectTransparency false in
 /--
 trace: [simp] Diagnostics
   [simp] theorems with bad keys

tests/lean/run/doLogicTests.lean

@@ -570,6 +570,7 @@ instance Result.instWP : WP Result (.except Error .pure) where
   | .fail e => wp (throw e : Except Error _)
   | .div => PredTrans.const ⌜False⌝
 
+set_option backward.isDefEq.respectTransparency false in
 instance Result.instWPMonad : WPMonad Result (.except Error .pure) where
   wp_pure _ := by ext Q; simp [wp]
   wp_bind x f := by
@@ -577,6 +578,7 @@ instance Result.instWPMonad : WPMonad Result (.except Error .pure) where
     ext Q
     grind
 
+set_option backward.isDefEq.respectTransparency false in
 theorem Result.of_wp {α} {x : Result α} (P : Result α → Prop) :
   (⊢ₛ wp⟦x⟧ post⟨fun a => ⌜P (.ok a)⌝, fun e => ⌜P (.fail e)⌝⟩) → P x := by
     intro hspec

tests/lean/run/mvcgenTutorial.lean

@@ -220,6 +220,7 @@ instance Result.instWP : WP Result (.except Error .pure) where
   | .fail e => wp (throw e : Except Error _)
   | .div => PredTrans.const ⌜False⌝
 
+set_option backward.isDefEq.respectTransparency false in
 instance Result.instWPMonad : WPMonad Result (.except Error .pure) where
   wp_pure _ := by
     ext Q

tests/lean/run/ofNatNormNum.lean

@@ -26,12 +26,12 @@ instance [S α] : OfNat α n where
 instance [S α] : OfNatSound α where
   ofNat_add n m := by
     induction m with
-    | zero => simp [S.ofNat]; erw [S.add_zero]; done
+    | zero => simp; erw [S.add_zero]; rfl
     | succ m ih => simp [OfNat.ofNat, S.ofNat] at *; erw [← ih]; rw [S.add_assoc]
 
 theorem S.ofNat_mul [S α] (n m : Nat) : (OfNat.ofNat n : α) * OfNat.ofNat m = OfNat.ofNat (n * m) := by
   induction m with
-  | zero => rw [S.mul_zero, Nat.mul_zero]
+  | zero => rw [Nat.mul_zero]; erw [S.mul_zero]; rfl
   | succ m ih =>
     show OfNat.ofNat (α := α) n * OfNat.ofNat (m + 1) = OfNat.ofNat (n * m.succ)
     rw [Nat.mul_succ, ← ofNat_add, ← ofNat_add, ← ih, left_distrib]

tests/lean/run/structWithAlgTCSynth.lean

@@ -1265,7 +1265,7 @@ variable (R : Type u) [CommSemiring R] (M : Type v)
 
 inductive r : (MvPolynomial M R) → (MvPolynomial M R) → Prop
 
-def Quot_r := RingQuot (r R M)
+abbrev Quot_r := RingQuot (r R M)
 
 instance : Semiring (Quot_r R M) :=
   RingQuot.instSemiring _