chore: bump synthInstance heartbeat limit in structWithAlgTCSynth test

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

src/Init/Control/Lawful/Instances.lean

@@ -347,7 +347,7 @@ instance [Monad m] [LawfulMonad m] : LawfulMonad (ReaderT ρ m) where
 
 @[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]; exact bind_pure _
+  simp [controlAt]
 
 @[simp] theorem run_control [Monad m] [LawfulMonad m] (f : ({β : Type u} → ReaderT ρ m β → m (stM m (ReaderT ρ m) β)) → m (stM m (ReaderT ρ m) α)) (ctx : ρ) :
     ReaderT.run (control f) ctx = f fun x => x.run ctx := run_controlAt f ctx
@@ -439,7 +439,6 @@ instance [Monad m] [LawfulMonad m] : LawfulMonad (StateT σ m) where
 @[simp] theorem run_restoreM [Monad m] [LawfulMonad m] (x : stM m (StateT σ m) α) (s : σ) :
     StateT.run (restoreM x) s = pure x := by
   simp [restoreM, MonadControl.restoreM]
-  rfl
 
 @[simp] theorem run_liftWith [Monad m] [LawfulMonad m] (f : ({β : Type u} → StateT σ m β → m (stM m (StateT σ m) β)) → m α) (s : σ) :
     StateT.run (liftWith f) s = ((·, s) <$> f fun x => x.run s) := by

src/Init/Data/Iterators/Basic.lean

@@ -315,13 +315,13 @@ of another state. Having this proof bundled up with the step is important for te
 See `IterM.Step` and `Iter.Step` for the concrete choice of the plausibility predicate.
 -/
 @[expose]
-def PlausibleIterStep (IsPlausibleStep : IterStep α β → Prop) := Subtype IsPlausibleStep
+abbrev PlausibleIterStep (IsPlausibleStep : IterStep α β → Prop) := Subtype IsPlausibleStep
 
 /--
 Match pattern for the `yield` case. See also `IterStep.yield`.
 -/
 @[match_pattern, simp, spec, expose]
-def PlausibleIterStep.yield {IsPlausibleStep : IterStep α β → Prop}
+abbrev PlausibleIterStep.yield {IsPlausibleStep : IterStep α β → Prop}
     (it' : α) (out : β) (h : IsPlausibleStep (.yield it' out)) :
     PlausibleIterStep IsPlausibleStep :=
   ⟨.yield it' out, h⟩
@@ -330,7 +330,7 @@ def PlausibleIterStep.yield {IsPlausibleStep : IterStep α β → Prop}
 Match pattern for the `skip` case. See also `IterStep.skip`.
 -/
 @[match_pattern, simp, grind =, expose]
-def PlausibleIterStep.skip {IsPlausibleStep : IterStep α β → Prop}
+abbrev PlausibleIterStep.skip {IsPlausibleStep : IterStep α β → Prop}
     (it' : α) (h : IsPlausibleStep (.skip it')) : PlausibleIterStep IsPlausibleStep :=
   ⟨.skip it', h⟩
 
@@ -338,7 +338,7 @@ def PlausibleIterStep.skip {IsPlausibleStep : IterStep α β → Prop}
 Match pattern for the `done` case. See also `IterStep.done`.
 -/
 @[match_pattern, simp, grind =, expose]
-def PlausibleIterStep.done {IsPlausibleStep : IterStep α β → Prop}
+abbrev PlausibleIterStep.done {IsPlausibleStep : IterStep α β → Prop}
     (h : IsPlausibleStep .done) : PlausibleIterStep IsPlausibleStep :=
   ⟨.done, h⟩
 
@@ -379,6 +379,8 @@ class Iterator (α : Type w) (m : Type w → Type w') (β : outParam (Type w)) w
   -/
   step : (it : IterM (α := α) m β) → m (Shrink <| PlausibleIterStep <| IsPlausibleStep it)
 
+attribute [reducible] Iterator.IsPlausibleStep
+
 section Monadic
 
 /-- The constructor has been renamed. -/
@@ -424,7 +426,6 @@ theorem IterM.toIter_mk {α β} {it : α} :
 Asserts that certain step is plausibly the successor of a given iterator. What "plausible" means
 is up to the `Iterator` instance but it should be strong enough to allow termination proofs.
 -/
-@[expose]
 abbrev IterM.IsPlausibleStep {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β] :
     IterM (α := α) m β → IterStep (IterM (α := α) m β) β → Prop :=
   Iterator.IsPlausibleStep (α := α) (m := m)
@@ -493,7 +494,7 @@ Asserts that certain step is plausibly the successor of a given iterator. What "
 is up to the `Iterator` instance but it should be strong enough to allow termination proofs.
 -/
 @[expose]
-def Iter.IsPlausibleStep {α : Type w} {β : Type w} [Iterator α Id β]
+abbrev Iter.IsPlausibleStep {α : Type w} {β : Type w} [Iterator α Id β]
     (it : Iter (α := α) β) (step : IterStep (Iter (α := α) β) β) : Prop :=
   it.toIterM.IsPlausibleStep (step.mapIterator Iter.toIterM)
 
@@ -549,7 +550,7 @@ The type of the step object returned by `Iter.step`, containing an `IterStep`
 and a proof that this is a plausible step for the given iterator.
 -/
 @[expose]
-def Iter.Step {α : Type w} {β : Type w} [Iterator α Id β] (it : Iter (α := α) β) :=
+abbrev Iter.Step {α : Type w} {β : Type w} [Iterator α Id β] (it : Iter (α := α) β) :=
   PlausibleIterStep (Iter.IsPlausibleStep it)
 
 /--

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

@@ -280,6 +280,7 @@ For each value emitted by the base iterator `it`, this combinator calls `f`.
 @[inline, expose]
 def IterM.mapWithPostcondition {α β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''}
     [Monad n] [MonadLiftT m n] [Iterator α m β] (f : β → PostconditionT n γ)
+    -- TODO: eta expand `lift`?
     (it : IterM (α := α) m β) : IterM (α := Map α m n (fun ⦃_⦄ => monadLift) f) n γ :=
   InternalCombinators.map (fun {_} => monadLift) f it
 

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

@@ -765,6 +765,7 @@ theorem Iter.anyM_eq_anyM_mapM_pure {α β : Type} {m : Type → Type w'} [Itera
   rw [forIn_eq_match_step, IterM.forIn_eq_match_step, bind_assoc, step_mapM]
   cases it.step using PlausibleIterStep.casesOn
   · rename_i out _
+    simp only
     simp only [bind_assoc, pure_bind, map_eq_pure_bind, Shrink.inflate_deflate,
       liftM, monadLift]
     have {x : m Bool} : x = MonadAttach.attach (pure out) >>= (fun _ => x) := by
@@ -777,7 +778,7 @@ theorem Iter.anyM_eq_anyM_mapM_pure {α β : Type} {m : Type → Type w'} [Itera
     apply bind_congr; intro px
     split
     · simp
-    · simp [ihy ‹_›]
+    · simp [ihy ‹_›, monadLift]
   · simp [ihs ‹_›]
   · simp
 

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

@@ -232,6 +232,35 @@ 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]
 
+-- public theorem Iter.toList_flatMapAfter {α α₂ β γ : Type w} [Iterator α Id β] [Iterator α₂ Id γ]
+--     [Finite α Id] [Finite α₂ Id]
+--     {f : β → Iter (α := α₂) γ} {it₁ : Iter (α := α) β} {it₂ : Option (Iter (α := α₂) γ)} :
+--     (it₁.flatMapAfter f it₂).toList = match it₂ with
+--       | none => (it₁.map fun b => (f b).toList).toList.flatten
+--       | some it₂ => it₂.toList ++
+--           (it₁.map fun b => (f b).toList).toList.flatten := by
+--   unfold Iter.toList
+--   simp only [flatMapAfter, Iter.toList, toIterM_toIter, IterM.toList_flatMapAfter]
+--   cases it₂ <;>
+--     simp only [map, toIterM_toIter]
+--   · -- Here, we rewrite with `Id.pure_run`, making the RHS ill-typed in `reducible` transparency because the `Types.Map.instIterator` instance is *not* rewritten. However, not applying `pure_run` doesn't allow progress, either. `+instances` would help.
+--     -- Could we have `congr` lemmas for these situations?
+--     -- Is it a good idea that `simp` happily rewrites even though this increases the incongruence level?
+--     -- Can we visualize the "incongruence level" by showing explicit casts for `reducible`, `instance` and `semireducible` transparency violations?
+--     simp? [map, IterM.toList_map_eq_toList_mapM, - IterM.toList_map, Id.pure_run]
+--     with_reducible congr -- This solves that problem that we don't rewrite inside instances
+--     -- Observation: Types have already been acknowledged to be equal, and unfolding the very same expressions would make the terms equal, too.
+--     --- Would it be possible to unfold the arguments when they are used in the type and need to be unfolded so that it type-checks?
+--     -- At least, it's unintuitive that types are checked differently.
+--     -- Another perspective on the problem:
+--     --- It's weird that parameters that should be of the same type can syntactically differ, even though they
+--     --- make problems with `simp`.
+--     ---- Again, one could think about collecting all such "type correctness required unfolding equations" and allow simp to unfold them?
+--     simp only [Id.pure_run]
+--   · simp only [map, IterM.toList_map_eq_toList_mapM, - IterM.toList_map]
+--   -- IDEA: Would it be an idea to include instances in the discr tree AFTER REDUCING THEM?
+--   -- Should I just not rely so much on defeq? How would a non-defeq proof look like?
+
 set_option backward.isDefEq.respectTransparency false in
 public theorem Iter.toList_flatMapAfter {α α₂ β γ : Type w} [Iterator α Id β] [Iterator α₂ Id γ]
     [Finite α Id] [Finite α₂ Id]

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

@@ -182,11 +182,12 @@ theorem IterM.step_filterMap [Monad m] [LawfulMonad m] {f : β → Option β'} :
       pure <| .deflate <| .skip (it'.filterMap f) (.skip h)
     | .done h =>
       pure <| .deflate <| .done (.done h)) := by
-  simp only [IterM.filterMap, step_filterMapWithPostcondition, pure]
+  simp only [IterM.filterMap]
+  simp only [step_filterMapWithPostcondition, PostconditionT.operation_pure]
   apply bind_congr
   intro step
   split
-  · simp only [PostconditionT.pure, PlausibleIterStep.skip, PlausibleIterStep.yield, pure_bind]
+  · simp only [PlausibleIterStep.skip, PlausibleIterStep.yield, pure_bind]
     split <;> split <;> simp_all
   · simp
   · simp
@@ -361,8 +362,8 @@ theorem IterM.toList_map_eq_toList_mapM {α β γ : Type w}
       bind_map_left]
     conv => rhs; rhs; ext a; rw [← pure_bind (x := a.val) (f := fun _ => _ <$> _)]
     simp only [← bind_assoc, bind_pure_comp, WeaklyLawfulMonadAttach.map_attach]
-    simp [ihy ‹_›]
-  · simp [ihs ‹_›]
+    simpa using ihy ‹_›
+  · simpa using ihs ‹_›
   · simp
 
 theorem IterM.toList_map_eq_toList_filterMapM {α β γ : Type w} {m : Type w → Type w'}
@@ -373,6 +374,7 @@ theorem IterM.toList_map_eq_toList_filterMapM {α β γ : Type w} {m : Type w
   simp [toList_map_eq_toList_mapM, toList_mapM_eq_toList_filterMapM]
   congr <;> simp
 
+set_option backward.whnf.reducibleClassField false in
 /--
 Variant of `toList_filterMapWithPostcondition_filterMapWithPostcondition` that is intended to be
 used with the `apply` tactic. Because neither the LHS nor the RHS determine all implicit parameters,

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

@@ -26,7 +26,6 @@ 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⟩
@@ -39,12 +38,11 @@ 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] :
     it.uLift.toList = it.toList.map ULift.up := by
-  simp only [monadLift, uLift_eq_toIter_uLift_toIterM, IterM.toList_toIter]
+  simp only [uLift_eq_toIter_uLift_toIterM, IterM.toList_toIter]
   rw [IterM.toList_uLift]
   simp [monadLift, Iter.toList_eq_toList_toIterM]
 
@@ -61,12 +59,11 @@ 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] :
     it.uLift.length = it.length := by
-  simp only [monadLift, uLift_eq_toIter_uLift_toIterM, length_eq_length_toIterM, toIterM_toIter]
+  simp only [uLift_eq_toIter_uLift_toIterM, length_eq_length_toIterM, toIterM_toIter]
   rw [IterM.length_uLift]
   simp [monadLift]
 

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

@@ -58,8 +58,7 @@ theorem Iter.forIn_eq {α β : Type w} [Iterator α Id β] [Finite α Id]
     forIn' ita b f = forIn' itb b' g := by
   subst_eqs
   simp only [← funext_iff] at h
-  rw [← h]
-  rfl
+  rw [← h]; rfl
 
 @[congr] theorem Iter.forIn_congr {α β : Type w} {m : Type w → Type w'} [Monad m]
     [Iterator α Id β] [Finite α Id] [IteratorLoop α Id m]
@@ -276,8 +275,7 @@ theorem Iter.forIn'_eq_forIn'_toList {α β : Type w} [Iterator α Id β]
     {f : (out : β) → _ → γ → m (ForInStep γ)} :
     letI : ForIn' m (Iter (α := α) β) β _ := Iter.instForIn'
     ForIn'.forIn' it init f = ForIn'.forIn' it.toList init (fun out h acc => f out (Iter.mem_toList_iff_isPlausibleIndirectOutput.mp h) acc) := by
-  simp only [forIn'_toList]
-  congr
+  simp only [forIn'_toList]; rfl
 
 theorem Iter.forIn'_eq_forIn'_toArray {α β : Type w} [Iterator α Id β]
     [Finite α Id] {m : Type x → Type x'} [Monad m] [LawfulMonad m]
@@ -287,8 +285,7 @@ theorem Iter.forIn'_eq_forIn'_toArray {α β : Type w} [Iterator α Id β]
     {f : (out : β) → _ → γ → m (ForInStep γ)} :
     letI : ForIn' m (Iter (α := α) β) β _ := Iter.instForIn'
     ForIn'.forIn' it init f = ForIn'.forIn' it.toArray init (fun out h acc => f out (Iter.mem_toArray_iff_isPlausibleIndirectOutput.mp h) acc) := by
-  simp only [forIn'_toArray]
-  congr
+  simp only [forIn'_toArray]; rfl
 
 theorem Iter.forIn_toList {α β : Type w} [Iterator α Id β]
     [Finite α Id] {m : Type x → Type x'} [Monad m] [LawfulMonad m]

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

@@ -70,7 +70,7 @@ private def ListIterator.instFinitenessRelation [Pure m] :
   subrelation {it it'} h := by
     simp_wf
     obtain ⟨step, h, h'⟩ := h
-    cases step <;> simp_all [IterStep.successor, IterM.IsPlausibleStep, Iterator.IsPlausibleStep]
+    cases step <;> simp_all [IterStep.successor, IterM.IsPlausibleStep, Iterator.IsPlausibleStep, instIterator]
 
 instance ListIterator.instFinite [Pure m] : Finite (ListIterator α) m :=
   by exact Finite.of_finitenessRelation ListIterator.instFinitenessRelation

src/Init/Data/Iterators/ToIterator.lean

@@ -32,14 +32,14 @@ def ToIterator.iter [ToIterator γ Id α β] (x : γ) : Iter (α := α) β :=
   ToIterator.iterM x |>.toIter
 
 /-- Creates a monadic `ToIterator` instance. -/
-@[always_inline, inline, expose]
+@[always_inline, inline, expose, instance_reducible]
 def ToIterator.ofM (α : Type w)
     (iterM : γ → IterM (α := α) m β) :
     ToIterator γ m α β where
   iterMInternal x := iterM x
 
 /-- Creates a pure `ToIterator` instance. -/
-@[always_inline, inline, expose]
+@[always_inline, inline, expose, instance_reducible]
 def ToIterator.of (α : Type w)
     (iter : γ → Iter (α := α) β) :
     ToIterator γ Id α β where

src/Init/Data/List/MinMaxIdx.lean

@@ -358,11 +358,19 @@ private theorem combineMinIdxOn_lt [LE β] [DecidableLE β]
   simp only [combineMinIdxOn]
   split <;> (simp; omega)
 
+private theorem combineMinIdxOn_lt' [LE β] [DecidableLE β]
+    (f : α → β) {xs ys : List α} (zs : List α) {i j : Nat} (hi : i < xs.length) (hj : j < ys.length)
+    (h : zs = xs ++ ys) :
+    combineMinIdxOn f i j hi hj < zs.length := by
+  simp only [combineMinIdxOn, h]
+  split <;> (simp; omega)
+
 private theorem combineMinIdxOn_assoc [LE β] [DecidableLE β] [IsLinearPreorder β]
     {xs ys zs : List α} {i j k : Nat} {f : α → β} (hi : i < xs.length) (hj : j < ys.length)
-    (hk : k < zs.length) :
+    (hk : k < zs.length) (h) :
     combineMinIdxOn f (combineMinIdxOn f i j _ _) k
-      (combineMinIdxOn_lt f hi hj) hk = combineMinIdxOn f i (combineMinIdxOn f j k _ _) hi (combineMinIdxOn_lt f hj hk) := by
+      (combineMinIdxOn_lt' f xys hi hj h) hk = combineMinIdxOn f i (combineMinIdxOn f j k _ _) hi (combineMinIdxOn_lt f hj hk) := by
+  cases h
   open scoped Classical.Order in
   simp only [combineMinIdxOn]
   split
@@ -410,10 +418,10 @@ 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]
+        minIdxOn_cons_aux (xs := z :: zs) (by simp)]
+      rw [combineMinIdxOn_assoc (h := by simp)]
 
 protected theorem minIdxOn_append [LE β] [DecidableLE β] [IsLinearPreorder β]
     {xs ys : List α} {f : α → β} (hxs : xs ≠ []) (hys : ys ≠ []) :

src/Init/Data/Order/Opposite.lean

@@ -262,15 +262,18 @@ scoped instance (priority := low) instLawfulOrderOrdOpposite {il : LE α} {io :
     haveI := il.opposite
     haveI := io.opposite
     LawfulOrderOrd α :=
-      @LawfulOrderOrd.mk α io.opposite il.opposite
-        (by intros a b
-            simp +instances only [LE.opposite, Ord.opposite]
-            try simp [compare, LE.le]
-            apply isLE_compare)
-        (by intros a b
-            simp +instances only [LE.opposite, Ord.opposite]
-            try simp [compare, LE.le]
-            apply isGE_compare)
+  letI i := il.opposite
+  letI j := io.opposite
+  { isLE_compare a b := by
+      unfold LE.opposite Ord.opposite
+      simp only [compare, LE.le]
+      letI := il; letI := io
+      apply isLE_compare
+    isGE_compare a b := by
+      unfold LE.opposite Ord.opposite
+      simp only [compare, LE.le]
+      letI := il; letI := io
+      apply isGE_compare }
 
 scoped instance (priority := low) instLawfulOrderLTOpposite {il : LE α} {it : LT α}
     [LawfulOrderLT α] :

src/Init/Data/Order/PackageFactories.lean

@@ -46,7 +46,7 @@ public instance instLawfulOrderBEqOfDecidableLE {α : Type u} [LE α] [Decidable
   beq_iff_le_and_ge := by simp [BEq.beq]
 
 /-- If `LT` can be characterized in terms of a decidable `LE`, then `LT` is decidable either. -/
-@[expose]
+@[expose, instance_reducible]
 public def decidableLTOfLE {α : Type u} [LE α] {_ : LT α} [DecidableLE α] [LawfulOrderLT α] :
     DecidableLT α :=
   fun a b =>
@@ -645,7 +645,7 @@ automatically. If it fails, it is necessary to provide some of the fields manual
 * Other proof obligations, for example `transOrd`, can be omitted if a matching instance can be
   synthesized.
 -/
-@[expose]
+@[expose, instance_reducible]
 public def LinearPreorderPackage.ofOrd (α : Type u)
     (args : Packages.LinearPreorderOfOrdArgs α := by exact {}) : LinearPreorderPackage α :=
   letI := args.ord
@@ -791,10 +791,10 @@ automatically. If it fails, it is necessary to provide some of the fields manual
 * Other proof obligations, such as `transOrd`, can be omitted if matching instances can be
   synthesized.
 -/
-@[expose]
+@[expose, instance_reducible]
 public def LinearOrderPackage.ofOrd (α : Type u)
     (args : Packages.LinearOrderOfOrdArgs α := by exact {}) : LinearOrderPackage α :=
-  set_option backward.isDefEq.respectTransparency false in
+  -- 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/Internal/SignedBitVec.lean

@@ -6,16 +6,16 @@ Authors: Paul Reichert
 module
 
 prelude
-import Init.Data.BitVec.Bootstrap
-import Init.Data.BitVec.Lemmas
-import Init.Data.Int.DivMod.Lemmas
-import Init.Data.Int.Pow
-import Init.Data.Nat.Div.Lemmas
-import Init.Data.Nat.Lemmas
-import Init.Data.Nat.Mod
-import Init.Data.Option.Lemmas
-import Init.Data.Range.Polymorphic.BitVec
-import Init.Omega
+public import Init.Data.BitVec.Bootstrap
+public import Init.Data.BitVec.Lemmas
+public import Init.Data.Int.DivMod.Lemmas
+public import Init.Data.Int.Pow
+public import Init.Data.Nat.Div.Lemmas
+public import Init.Data.Nat.Lemmas
+public import Init.Data.Nat.Mod
+public import Init.Data.Option.Lemmas
+public import Init.Data.Range.Polymorphic.BitVec
+public import Init.Omega
 
 /-!
 # Ranges on signed bit vectors

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

@@ -486,7 +486,7 @@ public theorem Rxc.Iterator.toList_eq_toList_rxoIterator [LE α] [DecidableLE α
   · simp only [UpwardEnumerable.le_iff, UpwardEnumerable.lt_iff, *]
     split <;> rename_i h
     · rw [ihy]; rotate_left
-      · simp [Iter.IsPlausibleStep, IterM.IsPlausibleStep, Iterator.IsPlausibleStep,
+      · simp [Iter.IsPlausibleStep, IterM.IsPlausibleStep, Iterator.IsPlausibleStep, instIteratorIteratorIdOfUpwardEnumerableOfDecidableLE, -- TODO
           Iterator.Monadic.step, Iter.toIterM, *]; rfl
       · simpa [UpwardEnumerable.lt_iff, UpwardEnumerable.le_iff, UpwardEnumerable.lt_succ_iff] using h
     · simpa [UpwardEnumerable.lt_iff, UpwardEnumerable.le_iff, UpwardEnumerable.lt_succ_iff] using h

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

@@ -184,7 +184,7 @@ theorem Iterator.Monadic.isPlausibleSuccessorOf_iff
   · rintro ⟨a, h, hP, h'⟩
     refine ⟨.yield it' a, rfl, ?_⟩
     simp only [IterM.IsPlausibleStep, Iterator.IsPlausibleStep, step, h, hP, ↓reduceIte,
-      IterStep.yield.injEq, and_true]
+      IterStep.yield.injEq, and_true, instIteratorIteratorIdOfUpwardEnumerableOfDecidableLE] -- TODO
     simp [h'.1, ← h'.2]
 
 theorem Iterator.isPlausibleSuccessorOf_iff
@@ -244,10 +244,10 @@ private def Iterator.instFinitenessRelation [UpwardEnumerable α] [LE α] [Decid
       intro bound
       constructor
       intro it' ⟨step, hs₁, hs₂⟩
-      simp only [IterM.IsPlausibleStep, Iterator.IsPlausibleStep, Monadic.step] at hs₂
+      simp only [IterM.IsPlausibleStep, Iterator.IsPlausibleStep, Monadic.step, instIteratorIteratorIdOfUpwardEnumerableOfDecidableLE] at hs₂ -- TODO
       simp [hs₂, IterStep.successor] at hs₁
     simp only [IterM.IsPlausibleSuccessorOf, IterM.IsPlausibleStep, Iterator.IsPlausibleStep,
-      Monadic.step, exists_eq_right] at hnone ⊢
+      Monadic.step, exists_eq_right, instIteratorIteratorIdOfUpwardEnumerableOfDecidableLE] at hnone ⊢ -- TODO
     match it with
     | ⟨⟨none, _⟩⟩ => apply hnone
     | ⟨⟨some init, bound⟩⟩ =>
@@ -293,7 +293,7 @@ private def Iterator.instProductivenessRelation [UpwardEnumerable α] [LE α] [D
   subrelation {it it'} h := by
     exfalso
     simp only [IterM.IsPlausibleSkipSuccessorOf, IterM.IsPlausibleStep,
-      Iterator.IsPlausibleStep, Monadic.step] at h
+      Iterator.IsPlausibleStep, Monadic.step, instIteratorIteratorIdOfUpwardEnumerableOfDecidableLE] at h
     split at h
     · cases h
     · split at h
@@ -535,7 +535,6 @@ 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)
@@ -581,13 +580,17 @@ private theorem Iterator.instIteratorLoop.loopWf_eq [UpwardEnumerable α] [LE α
           · simp
         · simp
     · rw [IterM.DefaultConsumers.forIn'_eq_match_step Pl wf]
-      simp [IterM.step_eq, Monadic.step, instLawfulMonadLiftFunction.liftBind_pure, *]
+      simp only [IterM.step_eq, instLawfulMonadLiftFunction.liftBind_pure, Shrink.inflate_deflate, *]
+      -- Unfolding `Monadic.step` earlier would make some defeq checks fail on reducible transparency:
+      -- `Iterator.IsPlausibleStep` is reducible and it reduces to `Monadic.step`, but `Monadic.step`
+      -- is semireducible, and `simp` isn't able to unfold `Monadic.step` inside `Iterator.IsPlausibleStep`,
+      -- since that one only appears in the type of a constant -- I think?
+      simp [Monadic.step]
   · simp
 termination_by IteratorLoop.WithWF.mk ⟨⟨some next, upperBound⟩⟩ acc (hwf := wf)
 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] :
@@ -598,7 +601,9 @@ instance Iterator.instLawfulIteratorLoop [UpwardEnumerable α] [LE α] [Decidabl
       IterM.DefaultConsumers.forIn'_eq_wf Pl wf]
     rw [IterM.DefaultConsumers.forIn'.wf]
     split; rotate_left
-    · simp [IterM.step_eq, Monadic.step, Internal.LawfulMonadLiftBindFunction.liftBind_pure (liftBind := lift)]
+    · simp only [IterM.step_eq,
+      Internal.LawfulMonadLiftBindFunction.liftBind_pure (liftBind := lift), Shrink.inflate_deflate]
+      simp [Monadic.step]
     rename_i next _
     rw [instIteratorLoop.loop_eq_wf Pl wf, instIteratorLoop.loopWf_eq (lift := lift)]
     simp only [IterM.step_mk, Monadic.step_eq_step, Monadic.step,
@@ -762,7 +767,7 @@ theorem Iterator.Monadic.isPlausibleSuccessorOf_iff
   · rintro ⟨a, h, hP, h'⟩
     refine ⟨.yield it' a, rfl, ?_⟩
     simp only [IterM.IsPlausibleStep, Iterator.IsPlausibleStep, step, h, hP, ↓reduceIte,
-      IterStep.yield.injEq, and_true]
+      IterStep.yield.injEq, and_true, instIteratorIteratorIdOfUpwardEnumerableOfDecidableLT] -- TODO
     simp [h'.1, ← h'.2]
 
 theorem Iterator.isPlausibleSuccessorOf_iff
@@ -822,10 +827,10 @@ private def Iterator.instFinitenessRelation [UpwardEnumerable α] [LT α] [Decid
       intro bound
       constructor
       intro it' ⟨step, hs₁, hs₂⟩
-      simp only [IterM.IsPlausibleStep, Iterator.IsPlausibleStep, Monadic.step] at hs₂
+      simp only [IterM.IsPlausibleStep, Iterator.IsPlausibleStep, Monadic.step, instIteratorIteratorIdOfUpwardEnumerableOfDecidableLT] at hs₂ -- TODO
       simp [hs₂, IterStep.successor] at hs₁
     simp only [IterM.IsPlausibleSuccessorOf, IterM.IsPlausibleStep, Iterator.IsPlausibleStep,
-      Monadic.step, exists_eq_right] at hnone ⊢
+      Monadic.step, exists_eq_right, instIteratorIteratorIdOfUpwardEnumerableOfDecidableLT] at hnone ⊢ -- TODO
     match it with
     | ⟨⟨none, _⟩⟩ => apply hnone
     | ⟨⟨some init, bound⟩⟩ =>
@@ -871,7 +876,7 @@ private def Iterator.instProductivenessRelation [UpwardEnumerable α] [LT α] [D
   subrelation {it it'} h := by
     exfalso
     simp only [IterM.IsPlausibleSkipSuccessorOf, IterM.IsPlausibleStep,
-      Iterator.IsPlausibleStep, Monadic.step] at h
+      Iterator.IsPlausibleStep, Monadic.step, instIteratorIteratorIdOfUpwardEnumerableOfDecidableLT] at h -- TODO
     split at h
     · cases h
     · split at h
@@ -1310,7 +1315,7 @@ theorem Iterator.Monadic.isPlausibleSuccessorOf_iff
   · rintro ⟨a, h, h'⟩
     refine ⟨.yield it' a, rfl, ?_⟩
     simp only [IterM.IsPlausibleStep, Iterator.IsPlausibleStep, step, h,
-      IterStep.yield.injEq, and_true]
+      IterStep.yield.injEq, and_true, instIteratorIteratorIdOfUpwardEnumerable] -- TODO
     simp [h']
 
 theorem Iterator.isPlausibleSuccessorOf_iff
@@ -1345,10 +1350,10 @@ private def Iterator.instFinitenessRelation [UpwardEnumerable α]
         ⟨⟨none⟩⟩ := by
       constructor
       intro it' ⟨step, hs₁, hs₂⟩
-      simp only [IterM.IsPlausibleStep, Iterator.IsPlausibleStep, Monadic.step] at hs₂
+      simp only [IterM.IsPlausibleStep, Iterator.IsPlausibleStep, Monadic.step, instIteratorIteratorIdOfUpwardEnumerable] at hs₂ -- TODO
       simp [hs₂, IterStep.successor] at hs₁
     simp only [IterM.IsPlausibleSuccessorOf, IterM.IsPlausibleStep, Iterator.IsPlausibleStep,
-      Monadic.step, exists_eq_right] at hnone ⊢
+      Monadic.step, exists_eq_right, instIteratorIteratorIdOfUpwardEnumerable] at hnone ⊢ -- TODO
     match it with
     | ⟨⟨none⟩⟩ => apply hnone
     | ⟨⟨some init⟩⟩ =>
@@ -1387,7 +1392,7 @@ private def Iterator.instProductivenessRelation [UpwardEnumerable α]
   subrelation {it it'} h := by
     exfalso
     simp only [IterM.IsPlausibleSkipSuccessorOf, IterM.IsPlausibleStep,
-      Iterator.IsPlausibleStep, Monadic.step] at h
+      Iterator.IsPlausibleStep, Monadic.step, instIteratorIteratorIdOfUpwardEnumerable] at h -- TODO
     split at h <;> cases h
 
 @[no_expose]

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

@@ -4,13 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Paul Reichert
 -/
 module
-
 prelude
-
 public import Init.Data.Range.Polymorphic.Instances
 public import Init.Data.SInt
 import all Init.Data.SInt.Basic
-
 import all Init.Data.Range.Polymorphic.Internal.SignedBitVec
 import Init.ByCases
 import Init.Data.Int.LemmasAux
@@ -246,9 +243,10 @@ instance : HasModel Int8 (BitVec 8) where
   decode x := .ofBitVec x
   encode_decode := by simp
   decode_encode := by simp
-  le_iff_encode_le := by simp +instances [Int8.le_iff_toBitVec_sle, BitVec.Signed.instLE]
-  lt_iff_encode_lt := by simp +instances [Int8.lt_iff_toBitVec_slt, BitVec.Signed.instLT]
+  le_iff_encode_le := by simp [LE.le, Int8.le]
+  lt_iff_encode_lt := by simp [LT.lt, Int8.lt]
 
+set_option backward.whnf.reducibleClassField false in
 theorem instUpwardEnumerable_eq :
     instUpwardEnumerable = HasModel.instUpwardEnumerable := by
   apply UpwardEnumerable.ext
@@ -259,6 +257,7 @@ theorem instUpwardEnumerable_eq :
     simp +instances [HasModel.succMany?_eq, instUpwardEnumerable, HasModel.encode, HasModel.decode,
       ← toInt_toBitVec, toBitVec_maxValueSealed_eq_intMaxSealed, ofIntLE_eq_ofInt]
 
+
 instance : LawfulUpwardEnumerable Int8 := by
   simp +instances only [instUpwardEnumerable_eq]
   infer_instance
@@ -340,9 +339,10 @@ instance : HasModel Int16 (BitVec 16) where
   decode x := .ofBitVec x
   encode_decode := by simp
   decode_encode := by simp
-  le_iff_encode_le := by simp +instances [Int16.le_iff_toBitVec_sle, BitVec.Signed.instLE]
-  lt_iff_encode_lt := by simp +instances [Int16.lt_iff_toBitVec_slt, BitVec.Signed.instLT]
+  le_iff_encode_le := by simp [LE.le, Int16.le]
+  lt_iff_encode_lt := by simp [LT.lt, Int16.lt]
 
+set_option backward.whnf.reducibleClassField false in
 theorem instUpwardEnumerable_eq :
     instUpwardEnumerable = HasModel.instUpwardEnumerable := by
   apply UpwardEnumerable.ext
@@ -350,15 +350,16 @@ theorem instUpwardEnumerable_eq :
     apply HasModel.succ?_eq_of_technicalCondition
     simp [HasModel.encode, succ?, ← Int16.toBitVec_inj, toBitVec_minValueSealed_eq_intMinSealed]
   · ext
-    simp +instances [HasModel.succMany?_eq, instUpwardEnumerable, HasModel.encode, HasModel.decode,
+    simp only [HasModel.succMany?_eq]
+    simp [UpwardEnumerable.succMany?, HasModel.encode, HasModel.decode,
       ← toInt_toBitVec, toBitVec_maxValueSealed_eq_intMaxSealed, ofIntLE_eq_ofInt]
 
 instance : LawfulUpwardEnumerable Int16 := by
-  simp +instances only [instUpwardEnumerable_eq]
+  rw [instUpwardEnumerable_eq]
   infer_instance
 
 instance : LawfulUpwardEnumerableLE Int16 := by
-  simp +instances only [instUpwardEnumerable_eq]
+  rw [instUpwardEnumerable_eq]
   infer_instance
 
 public instance instRxcHasSize : Rxc.HasSize Int16 where
@@ -370,7 +371,7 @@ theorem instRxcHasSize_eq :
     ← toInt_toBitVec, HasModel.toNat_toInt_add_one_sub_toInt (Nat.zero_lt_succ _)]
 
 public instance instRxcLawfulHasSize : Rxc.LawfulHasSize Int16 := by
-  simp +instances only [instUpwardEnumerable_eq, instRxcHasSize_eq]
+  rw [instUpwardEnumerable_eq, instRxcHasSize_eq]
   infer_instance
 public instance : Rxc.IsAlwaysFinite Int16 := by exact inferInstance
 
@@ -387,7 +388,7 @@ theorem instRxiHasSize_eq :
     HasModel.encode, HasModel.toNat_two_pow_sub_one_sub_toInt (show 16 > 0 by omega)]
 
 public instance instRxiLawfulHasSize : Rxi.LawfulHasSize Int16 := by
-  simp +instances only [instUpwardEnumerable_eq, instRxiHasSize_eq]
+  rw [instUpwardEnumerable_eq, instRxiHasSize_eq]
   infer_instance
 public instance instRxiIsAlwaysFinite : Rxi.IsAlwaysFinite Int16 := by exact inferInstance
 
@@ -434,9 +435,10 @@ instance : HasModel Int32 (BitVec 32) where
   decode x := .ofBitVec x
   encode_decode := by simp
   decode_encode := by simp
-  le_iff_encode_le := by simp +instances [Int32.le_iff_toBitVec_sle, BitVec.Signed.instLE]
-  lt_iff_encode_lt := by simp +instances [Int32.lt_iff_toBitVec_slt, BitVec.Signed.instLT]
+  le_iff_encode_le := by simp [LE.le, Int32.le]
+  lt_iff_encode_lt := by simp [LT.lt, Int32.lt]
 
+set_option backward.whnf.reducibleClassField false in
 theorem instUpwardEnumerable_eq :
     instUpwardEnumerable = HasModel.instUpwardEnumerable := by
   apply UpwardEnumerable.ext
@@ -444,15 +446,16 @@ theorem instUpwardEnumerable_eq :
     apply HasModel.succ?_eq_of_technicalCondition
     simp [HasModel.encode, succ?, ← Int32.toBitVec_inj, toBitVec_minValueSealed_eq_intMinSealed]
   · ext
-    simp +instances [HasModel.succMany?_eq, instUpwardEnumerable, HasModel.encode, HasModel.decode,
+    simp only [HasModel.succMany?_eq]
+    simp [UpwardEnumerable.succMany?, HasModel.encode, HasModel.decode,
       ← toInt_toBitVec, toBitVec_maxValueSealed_eq_intMaxSealed, ofIntLE_eq_ofInt]
 
 instance : LawfulUpwardEnumerable Int32 := by
-  simp +instances only [instUpwardEnumerable_eq]
+  rw [instUpwardEnumerable_eq]
   infer_instance
 
 instance : LawfulUpwardEnumerableLE Int32 := by
-  simp +instances only [instUpwardEnumerable_eq]
+  rw [instUpwardEnumerable_eq]
   infer_instance
 
 public instance instRxcHasSize : Rxc.HasSize Int32 where
@@ -464,7 +467,7 @@ theorem instRxcHasSize_eq :
     ← toInt_toBitVec, HasModel.toNat_toInt_add_one_sub_toInt (Nat.zero_lt_succ _)]
 
 public instance instRxcLawfulHasSize : Rxc.LawfulHasSize Int32 := by
-  simp +instances only [instUpwardEnumerable_eq, instRxcHasSize_eq]
+  rw [instUpwardEnumerable_eq, instRxcHasSize_eq]
   infer_instance
 public instance : Rxc.IsAlwaysFinite Int32 := by exact inferInstance
 
@@ -481,7 +484,7 @@ theorem instRxiHasSize_eq :
     HasModel.encode, HasModel.toNat_two_pow_sub_one_sub_toInt (show 32 > 0 by omega)]
 
 public instance instRxiLawfulHasSize : Rxi.LawfulHasSize Int32 := by
-  simp +instances only [instUpwardEnumerable_eq, instRxiHasSize_eq]
+  rw [instUpwardEnumerable_eq, instRxiHasSize_eq]
   infer_instance
 public instance instRxiIsAlwaysFinite : Rxi.IsAlwaysFinite Int32 := by exact inferInstance
 
@@ -528,9 +531,10 @@ instance : HasModel Int64 (BitVec 64) where
   decode x := .ofBitVec x
   encode_decode := by simp
   decode_encode := by simp
-  le_iff_encode_le := by simp +instances [Int64.le_iff_toBitVec_sle, BitVec.Signed.instLE]
-  lt_iff_encode_lt := by simp +instances [Int64.lt_iff_toBitVec_slt, BitVec.Signed.instLT]
+  le_iff_encode_le := by simp [LE.le, Int64.le]
+  lt_iff_encode_lt := by simp [LT.lt, Int64.lt]
 
+set_option backward.whnf.reducibleClassField false in
 theorem instUpwardEnumerable_eq :
     instUpwardEnumerable = HasModel.instUpwardEnumerable := by
   apply UpwardEnumerable.ext
@@ -538,15 +542,16 @@ theorem instUpwardEnumerable_eq :
     apply HasModel.succ?_eq_of_technicalCondition
     simp [HasModel.encode, succ?, ← Int64.toBitVec_inj, toBitVec_minValueSealed_eq_intMinSealed]
   · ext
-    simp +instances [HasModel.succMany?_eq, instUpwardEnumerable, HasModel.encode, HasModel.decode,
+    simp only [HasModel.succMany?_eq]
+    simp [UpwardEnumerable.succMany?, HasModel.encode, HasModel.decode,
       ← toInt_toBitVec, toBitVec_maxValueSealed_eq_intMaxSealed, ofIntLE_eq_ofInt]
 
 instance : LawfulUpwardEnumerable Int64 := by
-  simp +instances only [instUpwardEnumerable_eq]
+  rw [instUpwardEnumerable_eq]
   infer_instance
 
 instance : LawfulUpwardEnumerableLE Int64 := by
-  simp +instances only [instUpwardEnumerable_eq]
+  rw [instUpwardEnumerable_eq]
   infer_instance
 
 public instance instRxcHasSize : Rxc.HasSize Int64 where
@@ -558,7 +563,7 @@ theorem instRxcHasSize_eq :
     ← toInt_toBitVec, HasModel.toNat_toInt_add_one_sub_toInt (Nat.zero_lt_succ _)]
 
 public instance instRxcLawfulHasSize : Rxc.LawfulHasSize Int64 := by
-  simp +instances only [instUpwardEnumerable_eq, instRxcHasSize_eq]
+  rw [instUpwardEnumerable_eq, instRxcHasSize_eq]
   infer_instance
 public instance : Rxc.IsAlwaysFinite Int64 := by exact inferInstance
 
@@ -575,7 +580,7 @@ theorem instRxiHasSize_eq :
     HasModel.encode, HasModel.toNat_two_pow_sub_one_sub_toInt (show 64 > 0 by omega)]
 
 public instance instRxiLawfulHasSize : Rxi.LawfulHasSize Int64 := by
-  simp +instances only [instUpwardEnumerable_eq, instRxiHasSize_eq]
+  rw [instUpwardEnumerable_eq, instRxiHasSize_eq]
   infer_instance
 public instance instRxiIsAlwaysFinite : Rxi.IsAlwaysFinite Int64 := by exact inferInstance
 
@@ -627,9 +632,10 @@ instance : HasModel ISize (BitVec System.Platform.numBits) where
   decode x := .ofBitVec x
   encode_decode := by simp
   decode_encode := by simp
-  le_iff_encode_le := by simp +instances [ISize.le_iff_toBitVec_sle, BitVec.Signed.instLE]
-  lt_iff_encode_lt := by simp +instances [ISize.lt_iff_toBitVec_slt, BitVec.Signed.instLT]
+  le_iff_encode_le := by simp [LE.le, ISize.le]
+  lt_iff_encode_lt := by simp [LT.lt, ISize.lt]
 
+set_option backward.whnf.reducibleClassField false in
 theorem instUpwardEnumerable_eq :
     instUpwardEnumerable = HasModel.instUpwardEnumerable := by
   apply UpwardEnumerable.ext
@@ -637,15 +643,16 @@ theorem instUpwardEnumerable_eq :
     apply HasModel.succ?_eq_of_technicalCondition
     simp [HasModel.encode, succ?, ← ISize.toBitVec_inj, toBitVec_minValueSealed_eq_intMinSealed]
   · ext
-    simp +instances [HasModel.succMany?_eq, instUpwardEnumerable, HasModel.encode, HasModel.decode,
+    simp only [HasModel.succMany?_eq]
+    simp [UpwardEnumerable.succMany?, HasModel.encode, HasModel.decode,
       ← toInt_toBitVec, toBitVec_maxValueSealed_eq_intMaxSealed, ofIntLE_eq_ofInt]
 
 instance : LawfulUpwardEnumerable ISize := by
-  simp +instances only [instUpwardEnumerable_eq]
+  rw [instUpwardEnumerable_eq]
   infer_instance
 
 instance : LawfulUpwardEnumerableLE ISize := by
-  simp +instances only [instUpwardEnumerable_eq]
+  rw [instUpwardEnumerable_eq]
   infer_instance
 
 public instance instRxcHasSize : Rxc.HasSize ISize where
@@ -657,7 +664,7 @@ theorem instRxcHasSize_eq :
     ← toInt_toBitVec, HasModel.toNat_toInt_add_one_sub_toInt System.Platform.numBits_pos]
 
 public instance instRxcLawfulHasSize : Rxc.LawfulHasSize ISize := by
-  simp +instances only [instUpwardEnumerable_eq, instRxcHasSize_eq]
+  rw [instUpwardEnumerable_eq, instRxcHasSize_eq]
   infer_instance
 public instance : Rxc.IsAlwaysFinite ISize := by exact inferInstance
 
@@ -674,7 +681,7 @@ theorem instRxiHasSize_eq :
     HasModel.encode, HasModel.toNat_two_pow_sub_one_sub_toInt System.Platform.numBits_pos]
 
 public instance instRxiLawfulHasSize : Rxi.LawfulHasSize ISize := by
-  simp +instances only [instUpwardEnumerable_eq, instRxiHasSize_eq]
+  rw [instUpwardEnumerable_eq, instRxiHasSize_eq]
   infer_instance
 public instance instRxiIsAlwaysFinite : Rxi.IsAlwaysFinite ISize := by exact inferInstance
 

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

@@ -43,7 +43,7 @@ private def SubarrayIterator.instFinitelessRelation : FinitenessRelation (Subarr
   Rel := InvImage WellFoundedRelation.rel (fun it => it.internalState.xs.stop - it.internalState.xs.start)
   wf := InvImage.wf _ WellFoundedRelation.wf
   subrelation {it it'} h := by
-    simp [IterM.IsPlausibleSuccessorOf, IterM.IsPlausibleStep, Iterator.IsPlausibleStep, step] at h
+    simp [IterM.IsPlausibleSuccessorOf, IterM.IsPlausibleStep, Iterator.IsPlausibleStep, step, instIteratorSubarrayIteratorId] at h -- TODO
     split at h
     · cases h
       simp only [InvImage, Subarray.stop, Subarray.start, WellFoundedRelation.rel, InvImage, sizeOf_nat]

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

@@ -36,11 +36,11 @@ theorem step_eq {it : Iter (α := SubarrayIterator α) α} :
         ⟨.yield ⟨⟨it.1.xs.array, it.1.xs.start + 1, it.1.xs.stop, by omega, by assumption⟩⟩
             (it.1.xs.array[it.1.xs.start]'(by omega)),
           (by
-            simp_all [Iter.IsPlausibleStep, IterM.IsPlausibleStep, Iterator.IsPlausibleStep,
+            simp_all [Iter.IsPlausibleStep, IterM.IsPlausibleStep, Iterator.IsPlausibleStep, instIteratorSubarrayIteratorId, -- TODO
               SubarrayIterator.step, Iter.toIterM])⟩
       else
         ⟨.done, (by
-            simpa [Iter.IsPlausibleStep, IterM.IsPlausibleStep, Iterator.IsPlausibleStep,
+            simpa [Iter.IsPlausibleStep, IterM.IsPlausibleStep, Iterator.IsPlausibleStep, instIteratorSubarrayIteratorId, -- TODO
               SubarrayIterator.step] using h)⟩ := by
   simp only [Iter.step, IterM.Step.toPure, Iter.toIter_toIterM, IterStep.mapIterator, IterM.step,
     Iterator.step, SubarrayIterator.step, Id.run_pure, Shrink.inflate_deflate]
@@ -67,7 +67,6 @@ 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
@@ -84,7 +83,7 @@ theorem toList_eq {α : Type u} {it : Iter (α := SubarrayIterator α) α} :
         simp [it.internalState.xs.stop_le_array_size]
         exact h
       · simp [Subarray.array, Subarray.stop]
-    · simp only [Iter.IsPlausibleStep, IterM.IsPlausibleStep, Iterator.IsPlausibleStep,
+    · simp only [Iter.IsPlausibleStep, IterM.IsPlausibleStep, Iterator.IsPlausibleStep, instIteratorSubarrayIteratorId, -- TODO
       IterStep.mapIterator_yield, SubarrayIterator.step]
       rw [dif_pos]; rotate_left; exact h
       rfl
@@ -106,13 +105,11 @@ 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,
@@ -218,6 +215,7 @@ public theorem Array.stop_toSubarray {xs : Array α} {lo hi : Nat} :
     (xs.toSubarray lo hi).stop = min hi xs.size := by
   simp [toSubarray_eq_min, Subarray.stop]
 
+set_option backward.whnf.reducibleClassField false in
 public theorem Subarray.toList_eq {xs : Subarray α} :
     xs.toList = (xs.array.extract xs.start xs.stop).toList := by
   let aslice := xs
@@ -227,13 +225,13 @@ public theorem Subarray.toList_eq {xs : Subarray α} :
   change aslice.toList = _
   have : aslice.toList = lslice.toList := by
     rw [ListSlice.toList_eq]
-    simp +instances only [aslice, lslice, Std.Slice.toList, Internal.toList_iter]
+    simp only [aslice, lslice, Std.Slice.toList, Internal.toList_iter]
     apply List.ext_getElem
     · have : stop - start ≤ array.size - start := by omega
       simp [Subarray.start, Subarray.stop, *, Subarray.array]
     · intros
       simp [Subarray.array, Subarray.start, Subarray.stop]
-  simp +instances [this, ListSlice.toList_eq, lslice]
+  simp [this, ListSlice.toList_eq, lslice]
 
 -- TODO: The current `List.extract_eq_drop_take` should be called `List.extract_eq_take_drop`
 private theorem Std.Internal.List.extract_eq_drop_take' {l : List α} {start stop : Nat} :

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

@@ -21,7 +21,7 @@ open Std Std.Slice Std.PRange
 /--
 Internal representation of `ListSlice`, which is an abbreviation for `Slice ListSliceData`.
 -/
-public class Std.Slice.Internal.ListSliceData (α : Type u) where
+public structure Std.Slice.Internal.ListSliceData (α : Type u) where
   /-- The relevant suffix of the underlying list. -/
   list : List α
   /-- The maximum length of the slice, starting at the beginning of `list`. -/

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

@@ -70,6 +70,7 @@ end ListSlice
 
 namespace List
 
+set_option backward.whnf.reducibleClassField false in
 @[simp, grind =]
 public theorem toList_mkSlice_rco {xs : List α} {lo hi : Nat} :
     xs[lo...hi].toList = (xs.take hi).drop lo := by
@@ -110,6 +111,7 @@ public theorem size_mkSlice_rcc {xs : List α} {lo hi : Nat} :
     xs[lo...=hi].size = min (hi + 1) xs.length - lo := by
   simp [← length_toList_eq_size]
 
+set_option backward.whnf.reducibleClassField false in
 @[simp, grind =]
 public theorem toList_mkSlice_rci {xs : List α} {lo : Nat} :
     xs[lo...*].toList = xs.drop lo := by
@@ -288,6 +290,7 @@ section ListSubslices
 
 namespace ListSlice
 
+set_option backward.whnf.reducibleClassField false in
 @[simp, grind =]
 public theorem toList_mkSlice_rco {xs : ListSlice α} {lo hi : Nat} :
     xs[lo...hi].toList = (xs.toList.take hi).drop lo := by
@@ -326,6 +329,7 @@ public theorem size_mkSlice_rcc {xs : ListSlice α} {lo hi : Nat} :
     xs[lo...=hi].size = min (hi + 1) xs.size - lo := by
   simp [← length_toList_eq_size]
 
+set_option backward.whnf.reducibleClassField false in
 @[simp, grind =]
 public theorem toList_mkSlice_rci {xs : ListSlice α} {lo : Nat} :
     xs[lo...*].toList = xs.toList.drop lo := by

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

@@ -241,7 +241,7 @@ private def finitenessRelation :
     all_goals try
       cases h
       revert h'
-      simp only [Std.IterM.IsPlausibleStep, Std.Iterator.IsPlausibleStep]
+      simp only [Std.IterM.IsPlausibleStep, Std.Iterator.IsPlausibleStep, instIteratorIdSearchStep] -- TODO
       match it.internalState with
       | .emptyBefore pos =>
         rintro (⟨h, h'⟩|h') <;> simp [h', ForwardSliceSearcher.toOption, Option.lt, Prod.lex_def]

src/Init/Data/String/Slice.lean

@@ -176,7 +176,7 @@ private def finitenessRelation [Std.Iterators.Finite (σ s) Id] :
     match step with
     | .yield it'' out | .skip it'' =>
       obtain rfl : it' = it'' := by simpa using h.symm
-      simp only [Std.IterM.IsPlausibleStep, Std.Iterator.IsPlausibleStep] at h'
+      simp only [Std.IterM.IsPlausibleStep, Std.Iterator.IsPlausibleStep, instIteratorIdSubslice] at h' -- TODO
       revert h'
       match it, it' with
       | ⟨.operating _ searcher⟩, ⟨.operating _ searcher'⟩ => simp [SplitIterator.toOption, Option.lt]
@@ -287,7 +287,7 @@ private def finitenessRelation [Std.Iterators.Finite (σ s) Id] :
     match step with
     | .yield it'' out | .skip it'' =>
       obtain rfl : it' = it'' := by simpa using h.symm
-      simp only [Std.IterM.IsPlausibleStep, Std.Iterator.IsPlausibleStep] at h'
+      simp only [Std.IterM.IsPlausibleStep, Std.Iterator.IsPlausibleStep, instIteratorId] at h' -- TODO
       revert h'
       match it, it' with
       | ⟨.operating _ searcher⟩, ⟨.operating _ searcher'⟩ => simp [SplitInclusiveIterator.toOption, Option.lt]
@@ -627,7 +627,7 @@ private def finitenessRelation [Std.Iterators.Finite (σ s) Id] :
     match step with
     | .yield it'' out | .skip it'' =>
       obtain rfl : it' = it'' := by simpa using h.symm
-      simp only [Std.IterM.IsPlausibleStep, Std.Iterator.IsPlausibleStep] at h'
+      simp only [Std.IterM.IsPlausibleStep, Std.Iterator.IsPlausibleStep, instIteratorOfPure] at h' -- TODO
       revert h'
       match it, it' with
       | ⟨.operating _ searcher⟩, ⟨.operating _ searcher'⟩ => simp [RevSplitIterator.toOption, Option.lt]

src/Lean/Meta/WHNF.lean

@@ -823,7 +823,7 @@ on class fields work as the user expects by temporarily bumping to `.instances`
 See `unfoldDefault` for the implementation.
 -/
 register_builtin_option backward.whnf.reducibleClassField : Bool := {
-  defValue := false
+  defValue := true
   descr    := "enables better support for unfolding type class fields marked as `[reducible]`"
 }
 

src/Std/Data/DHashMap/Internal/AssocList/Iterator.lean

@@ -41,7 +41,7 @@ def AssocListIterator.finitenessRelation :
   subrelation {it it'} h := by
     simp_wf
     obtain ⟨step, h, h'⟩ := h
-    cases step <;> simp_all [IterStep.successor, IterM.IsPlausibleStep, Iterator.IsPlausibleStep]
+    cases step <;> simp_all [IterStep.successor, IterM.IsPlausibleStep, Iterator.IsPlausibleStep, instIteratorAssocListIteratorIdSigma] -- TODO
 
 public instance : Finite (AssocListIterator α β) Id :=
   Finite.of_finitenessRelation AssocListIterator.finitenessRelation

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

@@ -1011,6 +1011,7 @@ theorem getEntryGT?_eq_getEntryGT?ₘ [Ord α] (k : α) (t : Impl α β) :
     getEntryGT? k t = getEntryGT?ₘ k t := by
   rw [getEntryGT?_eq_getEntryGT?ₘ', getEntryGT?ₘ', getEntryGT?ₘ, explore_eq_applyPartition] <;> simp
 
+set_option backward.whnf.reducibleClassField false in
 theorem getEntryLT?_eq_getEntryGT?_reverse [o : Ord α] [TransOrd α] {t : Impl α β} {k : α} :
     getEntryLT? k t = @getEntryGT? α β o.opposite k t.reverse := by
   rw [getEntryLT?, @getEntryGT?.eq_def, Ord.opposite]
@@ -1018,6 +1019,7 @@ theorem getEntryLT?_eq_getEntryGT?_reverse [o : Ord α] [TransOrd α] {t : Impl
     simp only [*, getEntryLT?.go, reverse, getEntryGT?.go, OrientedCmp.eq_swap (b := k),
       Ordering.swap]
 
+set_option backward.whnf.reducibleClassField false in
 theorem getEntryLE?_eq_getEntryGE?_reverse [o : Ord α] [TransOrd α] {t : Impl α β} {k : α} :
     getEntryLE? k t = @getEntryGE? α β o.opposite k t.reverse := by
   rw [getEntryLE?, @getEntryGE?.eq_def, Ord.opposite]

src/Std/Data/DTreeMap/Internal/WF/Lemmas.lean

@@ -2455,7 +2455,7 @@ theorem getEntryLE?_eq_findRev? [Ord α] [TransOrd α] {t : Impl α β} (hto : t
     getEntryLE? k t = t.toListModel.findRev? (fun e => (compare e.1 k).isLE) := by
   rw [getEntryLE?_eq_getEntryGE?_reverse, @getEntryGE?_eq_find?, List.findRev?_eq_find?_reverse,
     toListModel_reverse]
-  · simp +instances only [Ord.opposite, Bool.coe_iff_coe.mp OrientedCmp.isGE_iff_isLE]
+  · simp only [Bool.coe_iff_coe.mp OrientedCmp.isGE_iff_isLE]; rfl
   · exact hto.reverse
 
 theorem getEntryLT?_eq_findRev? [Ord α] [TransOrd α] {t : Impl α β} (hto : t.Ordered) {k : α} :

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

@@ -344,7 +344,7 @@ def Zipper.FinitenessRelation : FinitenessRelation (Zipper α β) Id where
     exact Nat.lt_wfRel.wf
   subrelation {it it'} h := by
     obtain ⟨w, h, h'⟩ := h
-    simp only [IterM.IsPlausibleStep, Iterator.IsPlausibleStep] at h'
+    simp only [IterM.IsPlausibleStep, Iterator.IsPlausibleStep, instIteratorZipperIdSigma] at h' -- TODO
     cases w
     case skip it'' =>
       cases h
@@ -390,7 +390,6 @@ 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
 
-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]
@@ -452,7 +451,7 @@ def RxcIterator.FinitenessRelation [Ord α] : FinitenessRelation (RxcIterator α
     exact Nat.lt_wfRel.wf
   subrelation {it it'} h := by
     obtain ⟨w, h, h'⟩ := h
-    simp only [IterM.IsPlausibleStep, Iterator.IsPlausibleStep] at h'
+    simp only [IterM.IsPlausibleStep, Iterator.IsPlausibleStep, instIteratorRxcIteratorIdSigma] at h' -- TODO
     cases w
     case skip it'' =>
       cases h
@@ -495,7 +494,6 @@ 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]
@@ -582,7 +580,7 @@ def RxoIterator.instFinitenessRelation [Ord α] : FinitenessRelation (RxoIterato
     exact Nat.lt_wfRel.wf
   subrelation {it it'} h := by
     obtain ⟨w, h, h'⟩ := h
-    simp only [IterM.IsPlausibleStep, Iterator.IsPlausibleStep] at h'
+    simp only [IterM.IsPlausibleStep, Iterator.IsPlausibleStep, instIteratorRxoIteratorIdSigma] at h' -- TODO
     cases w
     case skip it'' =>
       cases h
@@ -694,7 +692,6 @@ 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,
@@ -724,7 +721,6 @@ 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,
@@ -759,7 +755,6 @@ 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,
@@ -794,7 +789,6 @@ 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,
@@ -825,7 +819,6 @@ 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,
@@ -860,7 +853,6 @@ 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,
@@ -928,7 +920,6 @@ 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,
@@ -956,7 +947,6 @@ 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,
@@ -993,7 +983,6 @@ 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,
@@ -1065,7 +1054,6 @@ 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,
@@ -1093,7 +1081,6 @@ 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,
@@ -1130,7 +1117,6 @@ 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,
@@ -1201,7 +1187,6 @@ 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,
@@ -1229,7 +1214,6 @@ 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,
@@ -1266,7 +1250,6 @@ 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,
@@ -1338,7 +1321,6 @@ 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,
@@ -1366,7 +1348,6 @@ 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,
@@ -1403,7 +1384,6 @@ 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,
@@ -1460,7 +1440,6 @@ 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,
@@ -1488,7 +1467,6 @@ 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,
@@ -1528,7 +1506,6 @@ 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,
@@ -1586,7 +1563,6 @@ 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,
@@ -1614,7 +1590,6 @@ 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,
@@ -1654,7 +1629,6 @@ 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,
@@ -1706,7 +1680,6 @@ 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,
@@ -1732,7 +1705,6 @@ 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,
@@ -1765,7 +1737,6 @@ 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/DTreeMap/Raw/Lemmas.lean

@@ -1688,6 +1688,7 @@ theorem contains_of_contains_insertMany_list' [TransCmp cmp] [BEq α] [LawfulBEq
     (h' : contains (insertMany t l) k = true)
     (w : l.findSomeRev? (fun ⟨a, b⟩ => if cmp a k = .eq then some b else none) = none) :
     contains t k = true :=
+  set_option backward.whnf.reducibleClassField false in
   Impl.Const.contains_of_contains_insertMany_list' h
     (by simpa [Impl.Const.insertMany_eq_insertMany!] using h')
     (by simpa [compare_eq_iff_beq, BEq.comm] using w)

src/Std/Data/Iterators/Combinators/Monadic/StepSize.lean

@@ -86,7 +86,7 @@ def StepSizeIterator.instFinitenessRelation [Iterator α m β] [IteratorAccess
     apply WellFoundedRelation.wf
   subrelation {it it'} h := by
     obtain ⟨step, hs, h⟩ := h
-    simp only [IterM.IsPlausibleStep, Iterator.IsPlausibleStep] at h
+    simp only [IterM.IsPlausibleStep, Iterator.IsPlausibleStep, instIterator] at h -- TODO
     simp only [InvImage]
     obtain ⟨⟨n, it⟩⟩ := it
     simp only at ⊢ h
@@ -119,7 +119,7 @@ def StepSizeIterator.instProductivenessRelation [Iterator α m β] [IteratorAcce
     apply InvImage.wf
     apply WellFoundedRelation.wf
   subrelation {it it'} h := by
-    simp only [IterM.IsPlausibleSkipSuccessorOf, IterM.IsPlausibleStep, Iterator.IsPlausibleStep] at h
+    simp only [IterM.IsPlausibleSkipSuccessorOf, IterM.IsPlausibleStep, Iterator.IsPlausibleStep, instIterator] at h -- TODO
     simp only [InvImage]
     obtain ⟨⟨n, it⟩⟩ := it
     simp only [IterStep.mapIterator_skip, Function.comp_apply] at ⊢ h

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

@@ -42,7 +42,6 @@ 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
@@ -61,10 +60,11 @@ theorem IterM.step_intermediateDropWhileWithPostcondition {α m β} [Monad m] [I
       return .deflate <| .skip (IterM.Intermediate.dropWhileWithPostcondition P dropping it') (.skip h)
     | .done h =>
       return .deflate <| .done (.done h)) := by
-  simp only [step, Iterator.step]
+  simp only [step, Iterator.step, Intermediate.dropWhileWithPostcondition]
   apply bind_congr
   intro step
-  cases step.inflate using PlausibleIterStep.casesOn <;> rfl
+  simp
+  cases h : step.inflate using PlausibleIterStep.casesOn <;> rfl
 
 theorem IterM.step_dropWhileWithPostcondition {α m β} [Monad m] [Iterator α m β]
     {it : IterM (α := α) m β} {P} :

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

@@ -76,7 +76,6 @@ 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 β]
@@ -97,11 +96,11 @@ theorem IterM.Equiv.filterMapWithPostcondition {α₁ α₂ β γ : Type w}
   case implies =>
     rintro _ _ ⟨ita, itb, rfl, rfl, h'⟩
     replace h := h'
-    simp only [BundledIterM.step, BundledIterM.iterator_ofIterM, HetT.map_eq_pure_bind,
+    simp only [BundledIterM.step, HetT.map_eq_pure_bind,
       HetT.bind_assoc, Function.comp_apply, HetT.pure_bind, IterStep.mapIterator_mapIterator]
     rw [stepAsHetT_filterMapWithPostcondition, stepAsHetT_filterMapWithPostcondition]
     simp only [HetT.bind_assoc]
-    simp only [Equiv, BundledIterM.Equiv, BundledIterM.step, BundledIterM.iterator_ofIterM,
+    simp only [Equiv, BundledIterM.Equiv, BundledIterM.step,
       HetT.map_eq_pure_bind, HetT.bind_assoc, Function.comp_apply, HetT.pure_bind,
       IterStep.mapIterator_mapIterator] at h'
     apply liftInner_stepAsHetT_bind_congr h

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

@@ -178,7 +178,6 @@ 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

@@ -30,7 +30,7 @@ structure BundledIterM (m : Type w → Type w') (β : Type w) where
   inst : Iterator α m β
   iterator : IterM (α := α) m β
 
-def BundledIterM.ofIterM {α} [Iterator α m β] (it : IterM (α := α) m β) :
+abbrev BundledIterM.ofIterM {α} [Iterator α m β] (it : IterM (α := α) m β) :
     BundledIterM m β :=
   ⟨α, inferInstance, it⟩
 
@@ -39,6 +39,11 @@ theorem BundledIterM.iterator_ofIterM {α} [Iterator α m β] (it : IterM (α :=
     (BundledIterM.ofIterM it).iterator = it :=
   rfl
 
+@[simp]
+theorem BundledIterM.α_ofIterM {α} [Iterator α m β] {it : IterM (α := α) m β} :
+    (BundledIterM.ofIterM it).α = α :=
+  rfl
+
 instance (bit : BundledIterM m β) : Iterator bit.α m β :=
   bit.inst
 
@@ -97,7 +102,7 @@ theorem Equivalence.prun_liftInner_step [Iterator α m β] [Monad m] [Monad n]
     {it : IterM (α := α) m β} {f : (step : _) → _ → n γ} :
     ((IterM.stepAsHetT it).liftInner n).prun f =
       (it.step : n _) >>= (fun step => f step.inflate.1 step.inflate.2) := by
-  simp [IterM.stepAsHetT, HetT.liftInner, HetT.prun, PlausibleIterStep]
+  simp [IterM.stepAsHetT, HetT.liftInner, HetT.prun]
 
 @[simp]
 theorem Equivalence.property_step [Iterator α m β] [Monad m] [LawfulMonad m]
@@ -108,7 +113,7 @@ theorem Equivalence.property_step [Iterator α m β] [Monad m] [LawfulMonad m]
 theorem Equivalence.prun_step [Iterator α m β] [Monad m] [LawfulMonad m]
     {it : IterM (α := α) m β} {f : (step : _) → _ → m γ} :
     (IterM.stepAsHetT it).prun f = it.step >>= (fun step => f step.inflate.1 step.inflate.2) := by
-  simp [IterM.stepAsHetT, HetT.prun, PlausibleIterStep]
+  simp [IterM.stepAsHetT, HetT.prun]
 
 /--
 Like `BundledIterM.step`, but takes and returns iterators modulo `BundledIterM.Equiv`.
@@ -235,7 +240,6 @@ theorem Iter.Equiv.trans {α₁ α₂ α₃ β : Type w}
     (hbc : Iter.Equiv itb itc) : Iter.Equiv ita itc :=
   BundledIterM.Equiv.trans hab hbc
 
-set_option backward.isDefEq.respectTransparency 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 β)
@@ -248,13 +252,12 @@ theorem IterM.Equiv.of_morphism {α₁ α₂} {m : Type w → Type w'} [Monad m]
     exact ∃ it, ita = .ofIterM it ∧ itb = .ofIterM (f it)
   case implies =>
     rintro _ _ ⟨it, rfl, rfl⟩
-    simp only [BundledIterM.step, BundledIterM.iterator_ofIterM, HetT.map_eq_pure_bind,
+    simp only [BundledIterM.step, HetT.map_eq_pure_bind,
       HetT.bind_assoc, Function.comp_apply, HetT.pure_bind, IterStep.mapIterator_mapIterator,
       Functor.map, HetT.ext_iff, HetT.prun_bind, Equivalence.property_step, HetT.prun_pure,
       Equivalence.prun_step, HetT.property_bind, HetT.property_pure, h]
     refine ⟨?_, ?_⟩
     · unfold BundledIterM.ofIterM
-      dsimp only
       ext step
       constructor
       all_goals

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

@@ -35,8 +35,8 @@ This type is used in lemmas about iterator equivalence (`Iter.Equiv` and `IterM.
 `it.QuotStep` is the quotient of `it.Step` where two steps are identified if they agree up to
 equivalence of their successor iterator.
 -/
-def IterM.QuotStep [Iterator α m β] [Monad m] [LawfulMonad m]
-    (it : IterM (α := α) m β) :=
+abbrev IterM.QuotStep [Iterator α m β] [Monad m] [LawfulMonad m]
+    (it : IterM (α := α) m β) : Type _ :=
   Quot (fun (s₁ s₂ : it.Step) => s₁.1.bundledQuotient = s₂.1.bundledQuotient)
 
 /--
@@ -127,7 +127,6 @@ 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) :
@@ -162,7 +161,6 @@ 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/Monadic/Array.lean

@@ -60,7 +60,8 @@ theorem Std.Iterators.Types.ArrayIterator.stepAsHetT_iterFromIdxM [LawfulMonad m
     else
       pure .done) := by
   simp only [Array.iterFromIdxM, pure, HetT.ext_iff, Equivalence.property_step,
-    IterM.IsPlausibleStep, Iterator.IsPlausibleStep, Equivalence.prun_step, ge_iff_le]
+    IterM.IsPlausibleStep, instIterator, -- TODO
+    Iterator.IsPlausibleStep, Equivalence.prun_step, ge_iff_le]
   refine ⟨?_, ?_⟩
   · ext step
     cases step

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

@@ -21,7 +21,9 @@ public theorem Types.ListIterator.stepAsHetT_iterM [LawfulMonad m] {l : List β}
       | [] => pure .done
       | x :: xs => pure (.yield (xs.iterM m) x)) := by
   simp only [List.iterM, HetT.ext_iff, Equivalence.property_step, IterM.IsPlausibleStep,
-    Iterator.IsPlausibleStep, Equivalence.prun_step]
+    Equivalence.prun_step,
+    -- TODO: get rid of these
+    Iterator.IsPlausibleStep, ListIterator.instIterator]
   refine ⟨?_, ?_⟩
   · ext step
     cases step

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

@@ -46,7 +46,7 @@ theorem Std.Iterators.Vector.isPlausibleStep_iterFromIdxM_of_lt {xs : Vector β
 theorem Std.Iterators.Vector.isPlausibleStep_iterFromIdxM_of_not_lt {xs : Vector β n} {pos : Nat}
     (h : ¬ pos < n) :
     (xs.iterFromIdxM m pos).IsPlausibleStep .done := by
-  simp only [IterM.IsPlausibleStep, Iterator.IsPlausibleStep]
+  simp only [IterM.IsPlausibleStep, Iterator.IsPlausibleStep, Types.ArrayIterator.instIterator] -- TODO
   simpa [Vector.iterFromIdxM, Array.iterFromIdxM, Nat.not_lt] using h
 
 theorem Std.Iterators.Vector.isPlausibleStep_iterM_of_pos {xs : Vector β n}

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

@@ -52,7 +52,7 @@ theorem Std.Iterators.Vector.isPlausibleStep_iterFromIdx_of_lt {xs : Vector β n
 theorem Std.Iterators.Vector.isPlausibleStep_iterFromIdx_of_not_lt {xs : Vector β n} {pos : Nat}
     (h : ¬ pos < n) :
     (xs.iterFromIdx pos).IsPlausibleStep .done := by
-  simp only [Iter.IsPlausibleStep, IterM.IsPlausibleStep, Iterator.IsPlausibleStep]
+  simp only [Iter.IsPlausibleStep, IterM.IsPlausibleStep, Iterator.IsPlausibleStep, Types.ArrayIterator.instIterator]
   simpa [Vector.iterFromIdx, Array.iterFromIdxM, Array.iterFromIdx, Nat.not_lt] using h
 
 theorem Std.Iterators.Vector.isPlausibleStep_iter_of_pos {xs : Vector β n}

src/lake/Lake/Build/Job/Basic.lean

@@ -118,6 +118,7 @@ public instance : Inhabited (Job α) := ⟨{task := default, caption := default,
 
 namespace Job
 
+set_option backward.whnf.reducibleClassField false in
 public protected def cast (self : Job α) (h : ¬ self.kind.isAnonymous) : Job (DataType self.kind) :=
   let h := by
     match kind_eq:self.kind with

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", "whnf", "reducibleClassField"}, 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/run/structWithAlgTCSynth.lean

@@ -1285,6 +1285,6 @@ Typeclass synthesis should remain fast when multiple `with` patterns are nested
 
 Prior to #2478, this requires over 30000 heartbeats.
 -/
-set_option synthInstance.maxHeartbeats 400 in
+set_option synthInstance.maxHeartbeats 500 in
 instance instAlgebra' (R M : Type _) [CommRing R] (I : Ideal (Quot_r R M)) :
     Algebra R ((Quot_r R M) ⧸ I) := inferInstance