fix: respect transparency

src/Init/Data/Array/Basic.lean

@@ -170,7 +170,7 @@ Low-level indexing operator which is as fast as a C array read.
 
 This avoids overhead due to unboxing a `Nat` used as an index.
 -/
-@[extern "lean_array_uget", simp, expose]
+@[extern "lean_array_uget", simp, expose, implicit_reducible]
 def uget (xs : @& Array α) (i : USize) (h : i.toNat < xs.size) : α :=
   xs[i.toNat]
 
@@ -189,7 +189,7 @@ in-place when the reference to the array is unique.
 
 This avoids overhead due to unboxing a `Nat` used as an index.
 -/
-@[extern "lean_array_uset", expose]
+@[extern "lean_array_uset", expose, implicit_reducible]
 def uset (xs : Array α) (i : USize) (v : α) (h : i.toNat < xs.size) : Array α :=
   xs.set i.toNat v h
 

src/Init/Data/Array/Lemmas.lean

@@ -1872,7 +1872,7 @@ theorem getElem_of_append {xs ys zs : Array α} (eq : xs = ys.push a ++ zs) (h :
   rw [← getElem?_eq_getElem, eq, getElem?_append_left (by simp; omega), ← h]
   simp
 
-@[simp] theorem append_singleton {a : α} {as : Array α} : as ++ #[a] = as.push a := rfl
+@[simp] theorem append_singleton {a : α} {as : Array α} : as ++ #[a] = as.push a := (rfl)
 
 @[simp] theorem append_singleton_assoc {a : α} {xs ys : Array α} : xs ++ (#[a] ++ ys) = xs.push a ++ ys := by
   rw [← append_assoc, append_singleton]
@@ -2831,12 +2831,10 @@ theorem getElem_extract_aux {xs : Array α} {start stop : Nat} (h : i < (xs.extr
   rw [size_extract] at h; apply Nat.add_lt_of_lt_sub'; apply Nat.lt_of_lt_of_le h
   apply Nat.sub_le_sub_right; apply Nat.min_le_right
 
-set_option backward.isDefEq.respectTransparency.types false in
 @[simp, grind =] theorem getElem_extract {xs : Array α} {start stop : Nat}
     (h : i < (xs.extract start stop).size) :
-    (xs.extract start stop)[i] = xs[start + i]'(getElem_extract_aux h) :=
-  show (extract.loop xs (min stop xs.size - start) start #[])[i]
-    = xs[start + i]'(getElem_extract_aux h) by rw [getElem_extract_loop_ge]; rfl; exact Nat.zero_le _
+    (xs.extract start stop)[i] = xs[start + i]'(getElem_extract_aux h) := by
+  simp [extract, getElem_extract_loop_ge]
 
 theorem getElem?_extract {xs : Array α} {start stop : Nat} :
     (xs.extract start stop)[i]? = if i < min stop xs.size - start then xs[start + i]? else none := by

src/Init/Data/Array/MapIdx.lean

@@ -198,7 +198,6 @@ theorem mapFinIdx_append {xs ys : Array α} {f : (i : Nat) → α → (h : i < (
   cases ys
   simp [List.mapFinIdx_append, Array.size]
 
-set_option backward.isDefEq.respectTransparency.types false in
 @[simp, grind =]
 theorem mapFinIdx_push {xs : Array α} {a : α} {f : (i : Nat) → α → (h : i < (xs.push a).size) → β} :
     mapFinIdx (xs.push a) f =

src/Init/Data/BitVec/Basic.lean

@@ -130,7 +130,7 @@ theorem getElem_eq_testBit_toNat (x : BitVec w) (i : Nat) (h : i < w) :
 
 @[simp, grind =]
 theorem getLsbD_eq_getElem {x : BitVec w} {i : Nat} (h : i < w) :
-    x.getLsbD i = x[i] := rfl
+    x.getLsbD i = x[i] := (rfl)
 
 end getElem
 
@@ -139,7 +139,7 @@ section Int
 /--
 Interprets the bitvector as an integer stored in two's complement form.
 -/
-@[expose]
+@[expose, implicit_reducible]
 protected def toInt (x : BitVec n) : Int :=
   if 2 * x.toNat < 2^n then
     x.toNat
@@ -228,7 +228,7 @@ Usually accessed via the `-` prefix operator.
 
 SMT-LIB name: `bvneg`.
 -/
-@[expose]
+@[expose, implicit_reducible]
 protected def neg (x : BitVec n) : BitVec n := .ofNat n (2^n - x.toNat)
 instance : Neg (BitVec n) := ⟨.neg⟩
 
@@ -753,20 +753,20 @@ instance : Hashable (BitVec n) where
 
 section normalization_eqs
 /-! We add simp-lemmas that rewrite bitvector operations into the equivalent notation -/
-@[simp, grind =] theorem append_eq (x : BitVec w) (y : BitVec v) : BitVec.append x y = x ++ y        := rfl
-@[simp, grind =] theorem shiftLeft_eq (x : BitVec w) (n : Nat)     : BitVec.shiftLeft x n = x <<< n    := rfl
-@[simp, grind =] theorem ushiftRight_eq (x : BitVec w) (n : Nat)   : BitVec.ushiftRight x n = x >>> n  := rfl
-@[simp, grind =] theorem not_eq (x : BitVec w)                     : BitVec.not x = ~~~x               := rfl
-@[simp, grind =] theorem and_eq (x y : BitVec w)                   : BitVec.and x y = x &&& y          := rfl
-@[simp, grind =] theorem or_eq (x y : BitVec w)                    : BitVec.or x y = x ||| y           := rfl
-@[simp, grind =] theorem xor_eq (x y : BitVec w)                   : BitVec.xor x y = x ^^^ y          := rfl
-@[simp, grind =] theorem neg_eq (x : BitVec w)                     : BitVec.neg x = -x                 := rfl
-@[simp, grind =] theorem add_eq (x y : BitVec w)                   : BitVec.add x y = x + y            := rfl
-@[simp, grind =] theorem sub_eq (x y : BitVec w)                   : BitVec.sub x y = x - y            := rfl
-@[simp, grind =] theorem mul_eq (x y : BitVec w)                   : BitVec.mul x y = x * y            := rfl
-@[simp, grind =] theorem udiv_eq (x y : BitVec w)                  : BitVec.udiv x y = x / y           := rfl
-@[simp, grind =] theorem umod_eq (x y : BitVec w)                  : BitVec.umod x y = x % y           := rfl
-@[simp, grind =] theorem zero_eq                                   : BitVec.zero n = 0#n               := rfl
+@[simp, grind =] theorem append_eq (x : BitVec w) (y : BitVec v) : BitVec.append x y = x ++ y        := (rfl)
+@[simp, grind =] theorem shiftLeft_eq (x : BitVec w) (n : Nat)     : BitVec.shiftLeft x n = x <<< n    := (rfl)
+@[simp, grind =] theorem ushiftRight_eq (x : BitVec w) (n : Nat)   : BitVec.ushiftRight x n = x >>> n  := (rfl)
+@[simp, grind =] theorem not_eq (x : BitVec w)                     : BitVec.not x = ~~~x               := (rfl)
+@[simp, grind =] theorem and_eq (x y : BitVec w)                   : BitVec.and x y = x &&& y          := (rfl)
+@[simp, grind =] theorem or_eq (x y : BitVec w)                    : BitVec.or x y = x ||| y           := (rfl)
+@[simp, grind =] theorem xor_eq (x y : BitVec w)                   : BitVec.xor x y = x ^^^ y          := (rfl)
+@[simp, grind =] theorem neg_eq (x : BitVec w)                     : BitVec.neg x = -x                 := (rfl)
+@[simp, grind =] theorem add_eq (x y : BitVec w)                   : BitVec.add x y = x + y            := (rfl)
+@[simp, grind =] theorem sub_eq (x y : BitVec w)                   : BitVec.sub x y = x - y            := (rfl)
+@[simp, grind =] theorem mul_eq (x y : BitVec w)                   : BitVec.mul x y = x * y            := (rfl)
+@[simp, grind =] theorem udiv_eq (x y : BitVec w)                  : BitVec.udiv x y = x / y           := (rfl)
+@[simp, grind =] theorem umod_eq (x y : BitVec w)                  : BitVec.umod x y = x % y           := (rfl)
+@[simp, grind =] theorem zero_eq                                   : BitVec.zero n = 0#n               := (rfl)
 end normalization_eqs
 
 /-- Converts a list of `Bool`s into a big-endian `BitVec`. -/

src/Init/Data/BitVec/Bitblast.lean

@@ -2006,7 +2006,6 @@ theorem toInt_smod {x y : BitVec w} :
         simp [BitVec.toInt_eq_neg_toNat_neg_of_msb_true, hxmsb, hymsb,
           Int.fmod_eq_emod_of_nonneg _]
 
-set_option backward.isDefEq.respectTransparency.types false in
 theorem getElem_smod {x y : BitVec w} (h : i < w) :
     (x.smod y)[i] =
       match x.msb, y.msb with
@@ -2015,8 +2014,7 @@ theorem getElem_smod {x y : BitVec w} (h : i < w) :
       | true, false => (if -x % y = 0#w then (-x % y) else (y - -x % y))[i]
       | true, true => (-(-x % -y))[i] := by
   simp only [smod, umod_eq, neg_eq, zero_eq, add_eq, sub_eq]
-  by_cases hx : x.msb <;> by_cases hy : y.msb
-  <;> simp [hx, hy]
+  by_cases hx : x.msb <;> by_cases hy : y.msb <;> simp [hx, hy]
 
 theorem getLsbD_smod {x y : BitVec w} :
     (x.smod y).getLsbD i =
@@ -2032,7 +2030,6 @@ theorem getLsbD_smod {x y : BitVec w} :
   · by_cases hxy : x % -y = 0#w <;> simp [hx, hy, hxy]
   · simp [hx, hy]
 
-set_option backward.isDefEq.respectTransparency.types false in
 theorem getMsbD_smod {x y : BitVec w} :
     (x.smod y).getMsbD i  =
       match x.msb, y.msb with
@@ -2041,8 +2038,7 @@ theorem getMsbD_smod {x y : BitVec w} :
       | true, false => (if -x % y = 0#w then (-x % y) else (y - -x % y)).getMsbD i
       | true, true => (-(-x % -y)).getMsbD i := by
   simp only [smod, umod_eq, neg_eq, zero_eq, add_eq, sub_eq]
-  by_cases hx : x.msb <;> by_cases hy : y.msb
-  <;> simp [hx, hy]
+  by_cases hx : x.msb <;> by_cases hy : y.msb <;> simp [hx, hy]
 
 theorem msb_smod {x y : BitVec w} :
     (x.smod y).msb = (x.msb && y = 0) || (y.msb && (x.smod y) ≠ 0) := by

src/Init/Data/BitVec/Lemmas.lean

@@ -2063,7 +2063,7 @@ theorem shiftLeft_ofNat_eq {x : BitVec w} {k : Nat} : x <<< (BitVec.ofNat w k) =
 /-! ### ushiftRight -/
 
 @[simp, bitvec_to_nat, grind =] theorem toNat_ushiftRight (x : BitVec n) (i : Nat) :
-    (x >>> i).toNat = x.toNat >>> i := rfl
+    (x >>> i).toNat = x.toNat >>> i := (rfl)
 
 @[simp, grind =] theorem getLsbD_ushiftRight (x : BitVec n) (i j : Nat) :
     getLsbD (x >>> i) j = getLsbD x (i+j) := by
@@ -2115,7 +2115,6 @@ theorem ushiftRight_eq_zero {x : BitVec w} {n : Nat} (hn : w ≤ n) :
   have : 2^w ≤ 2^n := Nat.pow_le_pow_of_le Nat.one_lt_two hn
   rw [Nat.shiftRight_eq_div_pow, Nat.div_eq_of_lt (by omega)]
 
-set_option backward.isDefEq.respectTransparency.types false in
 /--
 Unsigned shift right by at least one bit makes the interpretations of the bitvector as an `Int` or `Nat` agree,
 because it makes the value of the bitvector less than or equal to `2^(w-1)`.
@@ -4704,7 +4703,6 @@ theorem toFin_srem {x y : BitVec w} : (x.srem y).toFin =
 
 /-! ### smod -/
 
-set_option backward.isDefEq.respectTransparency.types false in
 /-- Equation theorem for `smod` in terms of `umod`. -/
 theorem smod_eq (x y : BitVec w) : x.smod y =
   match x.msb, y.msb with
@@ -4716,7 +4714,7 @@ theorem smod_eq (x y : BitVec w) : x.smod y =
     let u := umod (- x) y
     (if u = 0#w then u else y - u)
   | true, true => - ((- x).umod (- y)) := by
-  rw [BitVec.smod]
+  rw [BitVec.smod, BitVec.zero_eq]
   rcases x.msb <;> rcases y.msb <;> simp
 
 @[bitvec_to_nat]
@@ -6145,7 +6143,6 @@ theorem clzAuxRec_le {x : BitVec w} (n : Nat) :
       · simp only [hxn, Bool.false_eq_true, reduceIte]
         exact ihn
 
-set_option backward.isDefEq.respectTransparency.types false in
 theorem clzAuxRec_eq_iff_of_getLsbD_false {x : BitVec w} (h : ∀ i, n < i → x.getLsbD i = false) :
     x.clzAuxRec n = BitVec.ofNat w w ↔ ∀ j, j ≤ n → x.getLsbD j = false := by
   rcases w with _|w

src/Init/Data/Dyadic/Basic.lean

@@ -673,9 +673,8 @@ theorem blt_eq_false_iff : blt x y = false ↔ ble y x = true := by
     rw [← Int.neg_sub]
     rcases k₁ - k₂ with (_ | _) | _
     · simp
-    · simp [← Int.negSucc_eq]
-    · simp only [Int.neg_negSucc, decide_eq_false_iff_not, Int.not_lt,
-        decide_eq_true_eq]
+    · simp
+    · simp only [decide_eq_false_iff_not, Int.not_lt, decide_eq_true_eq]
 
 theorem ble_iff_toRat : ble x y ↔ x.toRat ≤ y.toRat := by
   rw [← blt_eq_false_iff, Bool.eq_false_iff]

src/Init/Data/Int/Basic.lean

@@ -99,6 +99,7 @@ Examples:
  * `Int.negOfNat 6 = -6`
  * `Int.negOfNat 0 = 0`
 -/
+@[implicit_reducible]
 def negOfNat : Nat → Int
   | 0      => 0
   | succ m => negSucc m
@@ -115,7 +116,7 @@ Examples:
  * `-(-6 : Int) = 6`
  * `(12 : Int).neg = -12`
 -/
-@[extern "lean_int_neg"]
+@[extern "lean_int_neg", implicit_reducible]
 protected def neg (n : @& Int) : Int :=
   match n with
   | ofNat n   => negOfNat n
@@ -141,6 +142,7 @@ Examples:
  * `Int.subNatNat 2 5 = -3`
  * `Int.subNatNat 0 13 = -13`
 -/
+@[implicit_reducible]
 def subNatNat (m n : Nat) : Int :=
   match (n - m : Nat) with
   | 0        => ofNat (m - n)  -- m ≥ n
@@ -203,7 +205,7 @@ Examples:
 * `(7 : Int) - (0 : Int) = 7`
 * `(0 : Int) - (7 : Int) = -7`
 -/
-@[extern "lean_int_sub"]
+@[extern "lean_int_sub", implicit_reducible]
 protected def sub (m n : @& Int) : Int := m + (- n)
 
 instance : Sub Int where
@@ -397,6 +399,7 @@ Examples:
 * `(0 : Int) ^ 10 = 0`
 * `(-7 : Int) ^ 3 = -343`
 -/
+@[implicit_reducible]
 protected def pow : Int → Nat → Int
   | (m : Nat), n => Int.ofNat (m ^ n)
   | m@-[_+1], n => if n % 2 = 0 then Int.ofNat (m.natAbs ^ n) else - Int.ofNat (m.natAbs ^ n)

src/Init/Data/Int/DivMod/Lemmas.lean

@@ -1288,8 +1288,8 @@ theorem ediv_mul_of_nonneg {x y z : Int} (hy : 0 ≤ y) : x / (y * z) = x / y /
 @[simp] protected theorem tdiv_neg : ∀ a b : Int, a.tdiv (-b) = -(a.tdiv b)
   | ofNat m, 0 => show ofNat (m / 0) = -↑(m / 0) by rw [Nat.div_zero]; rfl
   | ofNat _, -[_+1] | -[_+1], succ _ => (Int.neg_neg _).symm
-  | ofNat _, succ _ | -[_+1], 0 => by simp [Int.tdiv, Int.neg_zero, ← Int.negSucc_eq]
-  | -[_+1], -[_+1] => by simp only [tdiv, neg_negSucc]
+  | ofNat _, succ _ | -[_+1], 0 => by simp [Int.tdiv, Int.neg_zero]
+  | -[_+1], -[_+1] => by simp only [tdiv]
 
 /-!
 There are no lemmas
@@ -1383,9 +1383,9 @@ protected theorem eq_tdiv_of_mul_eq_left {a b c : Int}
 
 @[simp] protected theorem neg_tdiv : ∀ a b : Int, (-a).tdiv b = -(a.tdiv b)
   | 0, n => by simp [Int.neg_zero]
-  | succ _, (n:Nat) => by simp [tdiv, ← Int.negSucc_eq]
+  | succ _, (n:Nat) => by simp [tdiv]
   | -[_+1], 0 | -[_+1], -[_+1] => by
-    simp only [tdiv, neg_negSucc, Int.neg_neg]
+    simp only [tdiv, Int.neg_neg]
   | succ _, -[_+1] | -[_+1], succ _ => (Int.neg_neg _).symm
 
 protected theorem neg_tdiv_neg (a b : Int) : (-a).tdiv (-b) = a.tdiv b := by
@@ -2112,21 +2112,16 @@ theorem neg_fdiv {a b : Int} : (-a).fdiv b = -(a.fdiv b) - if b = 0 ∨ b ∣ a
   | ofNat (a + 1), 0 => simp
   | ofNat (a + 1), ofNat (b + 1) =>
     unfold fdiv
-    simp only [ofNat_eq_natCast, Int.natCast_add, cast_ofNat_Int, Nat.succ_eq_add_one]
-    rw [← negSucc_eq, ← negSucc_eq]
+    simp
   | ofNat (a + 1), -[b+1] =>
     unfold fdiv
-    simp only [ofNat_eq_natCast, Int.natCast_add, cast_ofNat_Int, Nat.succ_eq_add_one]
-    rw [← negSucc_eq, neg_negSucc]
+    simp
   | -[a+1], 0 => simp
   | -[a+1], ofNat (b + 1) =>
     unfold fdiv
-    simp only [ofNat_eq_natCast, Int.natCast_add, cast_ofNat_Int, Nat.succ_eq_add_one]
-    rw [neg_negSucc, ← negSucc_eq]
+    simp
   | -[a+1], -[b+1] =>
     unfold fdiv
-    simp only [ofNat_eq_natCast, natCast_ediv, Nat.succ_eq_add_one, Int.natCast_add, cast_ofNat_Int]
-    rw [neg_negSucc, neg_negSucc]
     simp
 
 theorem fdiv_neg {a b : Int} (h : b ≠ 0) : a.fdiv (-b) = if b ∣ a then -(a.fdiv b) else -(a.fdiv b) - 1 := by

src/Init/Data/Iterators/Basic.lean

@@ -183,14 +183,14 @@ add_decl_doc IterM.mk
 Converts a pure iterator (`Iter β`) into a monadic iterator (`IterM Id β`) in the
 identity monad `Id`.
 -/
-@[expose]
+@[expose, implicit_reducible]
 def Iter.toIterM {α : Type w} {β : Type w} (it : Iter (α := α) β) : IterM (α := α) Id β :=
   ⟨it.internalState⟩
 
 /--
 Converts a monadic iterator (`IterM Id β`) over `Id` into a pure iterator (`Iter β`).
 -/
-@[expose]
+@[expose, implicit_reducible]
 def IterM.toIter {α : Type w} {β : Type w} (it : IterM (α := α) Id β) : Iter (α := α) β :=
   ⟨it.internalState⟩
 
@@ -569,6 +569,12 @@ def IterM.Step.toPure {α : Type w} {β : Type w} [Iterator α Id β] {it : Iter
     (step : it.Step) : it.toIter.Step :=
   ⟨step.val.mapIterator IterM.toIter, (by simp [Iter.IsPlausibleStep, step.property])⟩
 
+@[simp]
+theorem IterM.Step.val_toPure {α β : Type w} [Iterator α Id β] {it : IterM (α := α) Id β}
+    {step : it.Step} :
+    step.toPure.val = step.val.mapIterator IterM.toIter :=
+  (rfl)
+
 @[simp]
 theorem IterM.Step.toPure_yield {α β : Type w} [Iterator α Id β] {it : IterM (α := α) Id β}
     {it' out h} : IterM.Step.toPure (⟨.yield it' out, h⟩ : it.Step) = .yield it'.toIter out h :=

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

@@ -207,7 +207,6 @@ theorem Iter.step_mapM {f : β → n γ}
   | .skip it' h => rfl
   | .done h => rfl
 
-set_option backward.isDefEq.respectTransparency.types false in
 theorem Iter.step_filterMap {f : β → Option γ} :
     (it.filterMap f).step = match it.step with
       | .yield it' out h =>
@@ -216,13 +215,15 @@ theorem Iter.step_filterMap {f : β → Option γ} :
         | some out' => .yield (it'.filterMap f) out' (.yieldSome (out := out) h h')
       | .skip it' h => .skip (it'.filterMap f) (.skip h)
       | .done h => .done (.done h) := by
+  apply Subtype.ext
   simp only [filterMap_eq_toIter_filterMap_toIterM, toIterM_toIter, IterM.step_filterMap, step]
   simp only [monadLift, Id.run_bind]
   generalize it.toIterM.step.run = step
   cases step.inflate using PlausibleIterStep.casesOn
   · simp only [IterM.Step.toPure_yield, toIter_toIterM, toIterM_toIter]
     split <;> split <;> (try exfalso; simp_all; done)
-    · simp
+    · simp [PlausibleIterStep.skip, Id.run_pure, Shrink.inflate_deflate,
+        IterM.Step.val_toPure, IterStep.mapIterator_skip]
     · rename_i h₁ _ h₂
       rw [h₁] at h₂
       cases h₂
@@ -248,7 +249,6 @@ theorem Iter.val_step_filterMap {f : β → Option γ} :
   · simp
   · simp
 
-set_option backward.isDefEq.respectTransparency.types false in
 theorem Iter.step_map {f : β → γ} :
     (it.map f).step = match it.step with
       | .yield it' out h =>
@@ -257,11 +257,11 @@ theorem Iter.step_map {f : β → γ} :
         .skip (it'.map f) (.skip h)
       | .done h =>
         .done (.done h) := by
+  apply Subtype.ext
   simp only [map_eq_toIter_map_toIterM, step, toIterM_toIter, IterM.step_map, Id.run_bind]
   generalize it.toIterM.step.run = step
   cases step.inflate using PlausibleIterStep.casesOn <;> simp
 
-set_option backward.isDefEq.respectTransparency.types false in
 def Iter.step_filter {f : β → Bool} :
     (it.filter f).step = match it.step with
       | .yield it' out h =>
@@ -273,6 +273,7 @@ def Iter.step_filter {f : β → Bool} :
         .skip (it'.filter f) (.skip h)
       | .done h =>
         .done (.done h) := by
+  apply Subtype.ext
   simp only [filter_eq_toIter_filter_toIterM, step, toIterM_toIter, IterM.step_filter, Id.run_bind]
   generalize it.toIterM.step.run = step
   cases step.inflate using PlausibleIterStep.casesOn
@@ -281,7 +282,6 @@ def Iter.step_filter {f : β → Bool} :
   · simp
   · simp
 
-set_option backward.isDefEq.respectTransparency.types false in
 def Iter.val_step_filter {f : β → Bool} :
     (it.filter f).step.val = match it.step.val with
       | .yield it' out =>

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

@@ -102,14 +102,14 @@ theorem Iter.toList_take_zero {α β} [Iterator α Id β]
   rw [toList_eq_match_step]
   simp [step_take]
 
-set_option backward.isDefEq.respectTransparency.types false in
 theorem Iter.step_toTake {α β} [Iterator α Id β] [Finite α Id]
     {it : Iter (α := α) β} :
     it.toTake.step = (
         match it.step with
         | .yield it' out h => .yield it'.toTake out (.yield h Nat.zero_ne_one)
         | .skip it' h => .skip it'.toTake (.skip h Nat.zero_ne_one)
         | .done h => .done (.done h)) := by
+  apply Subtype.ext
   simp only [toTake_eq_toIter_toTake_toIterM, Iter.step, toIterM_toIter, IterM.step_toTake,
     Id.run_bind]
   cases it.toIterM.step.run.inflate using PlausibleIterStep.casesOn <;> simp