chore: workaround for test failure

fix: test

src/Init/Control/Lawful/MonadLift/Lemmas.lean

@@ -17,7 +17,7 @@ universe u v w
 theorem instMonadLiftTOfMonadLift_instMonadLiftTOfPure [Monad m] [Monad n] {_ : MonadLift m n}
     [LawfulMonadLift m n] : instMonadLiftTOfMonadLift Id m n = Id.instMonadLiftTOfPure := by
   have hext {a b : MonadLiftT Id n} (h : @a.monadLift = @b.monadLift) : a = b := by
-    cases a <;> cases b <;> simp_all
+    cases a; cases b; simp [monadLift] at h; simp [h]
   apply hext
   ext α x
   simp [monadLift, LawfulMonadLift.monadLift_pure]

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

@@ -107,6 +107,7 @@ theorem IterM.forIn'_eq {α β : Type w} {m : Type w → Type w'} [Iterator α m
   have : f = (Subtype.val <$> (⟨·, trivial⟩) <$> f · · ·) := by simp
   rw [this, hl.lawful (fun _ _ f x => monadLift x >>= f) (wf := IteratorLoop.wellFounded_of_finite)]
   simp +instances [IteratorLoop.defaultImplementation]
+  try rfl
 
 theorem IterM.forIn_eq {α β : Type w} {m : Type w → Type w'} [Iterator α m β] [Finite α m]
     {n : Type w → Type w''} [Monad m] [Monad n] [LawfulMonad n] [IteratorLoop α m n]
@@ -131,7 +132,7 @@ theorem IterM.forIn_eq {α β : Type w} {m : Type w → Type w'} [Iterator α m
   subst_eqs
   simp only [← funext_iff] at h
   rw [← h]
-  rfl
+  try rfl
 
 @[congr] theorem IterM.forIn_congr {α β : Type w} {m : Type w → Type w'}
     {n : Type w → Type w''} [Monad n] [Monad m]

src/Init/Data/List/MinMaxOn.lean

@@ -274,19 +274,19 @@ protected theorem min_eq_max {min : Min α} {xs : List α} {h} :
     xs.min h = (letI := min.oppositeMax; xs.max h) := by
   simp only [List.min, List.max]
   rw [Min.oppositeMax_def]
-  simp
+  simp; try rfl
 
 protected theorem max_eq_min {max : Max α} {xs : List α} {h} :
     xs.max h = (letI := max.oppositeMin; xs.min h) := by
   simp only [List.min, List.max]
   rw [Max.oppositeMin_def]
-  simp
+  simp; try rfl
 
 protected theorem max?_eq_min? {max : Max α} {xs : List α} :
     xs.max? = (letI := max.oppositeMin; xs.min?) := by
   simp only [List.min?, List.max?]
   rw [Max.oppositeMin_def]
-  simp
+  first | simp | rfl
 
 @[simp]
 protected theorem maxOn_id [Max α] [LE α] [DecidableLE α] [LawfulOrderLeftLeaningMax α]

src/Init/Data/Order/Factories.lean

@@ -208,7 +208,7 @@ public instance LawfulOrderLT.of_lt {α : Type u} [LT α] [i : Asymm (α := α)
     haveI := LE.ofLT α
     LawfulOrderLT α :=
   letI := LE.ofLT α
-  { lt_iff a b := by simpa +instances [LE.ofLT, Classical.not_not] using i.asymm a b }
+  { lt_iff a b := by simp +instances [LE.ofLT, LE.le]; apply Asymm.asymm }
 
 /--
 If an `LT α` instance is asymmetric and its negation is transitive, then `LE.ofLT α` represents a
@@ -253,7 +253,8 @@ public theorem LawfulOrderInf.of_lt {α : Type u} [Min α] [LT α]
   letI := LE.ofLT α
   { le_min_iff a b c := by
       open Classical in
-      simp +instances only [LE.ofLT, ← Decidable.not_iff_not (a := ¬ min b c < a)]
+      simp +instances only [LE.ofLT, LE.le]
+      simp [← not_or, Decidable.not_iff_not]
       simpa [Decidable.imp_iff_not_or] using min_lt_iff a b c }
 
 /--
@@ -282,7 +283,8 @@ public def LawfulOrderSup.of_lt {α : Type u} [Max α] [LT α]
   letI := LE.ofLT α
   { max_le_iff a b c := by
       open Classical in
-      simp +instances only [LE.ofLT, ← Decidable.not_iff_not ( a := ¬ c < max a b)]
+      simp +instances only [LE.ofLT, LE.le]
+      simp [← not_or, Decidable.not_iff_not]
       simpa [Decidable.imp_iff_not_or] using lt_max_iff a b c }
 
 /--

src/Init/Data/Order/Opposite.lean

@@ -50,7 +50,7 @@ def max' [LE α] [DecidableLE α] (a b : α) : α :=
 Without the `open scoped` command, Lean would not find the required {lit}`DecidableLE α`
 instance for the opposite order.
 -/
-def LE.opposite (le : LE α) : LE α where
+@[instance_reducible] def LE.opposite (le : LE α) : LE α where
   le a b := b ≤ a
 
 theorem LE.opposite_def {le : LE α} :
@@ -193,38 +193,30 @@ scoped instance (priority := low) instLEReflOpposite {i : LE α} [Refl (α := α
 scoped instance (priority := low) instLESymmOpposite {i : LE α} [Symm (α := α) (· ≤ ·)] :
     haveI := i.opposite
     Symm (α := α) (· ≤ ·) :=
-  letI := i.opposite
   { symm a b hab := by
-      simp +instances only [LE.opposite] at *
-      letI := i
+      simp [LE.le] at hab ⊢
       exact Symm.symm b a hab }
 
 scoped instance (priority := low) instLEAntisymmOpposite {i : LE α} [Antisymm (α := α) (· ≤ ·)] :
     haveI := i.opposite
     Antisymm (α := α) (· ≤ ·) :=
-  letI := i.opposite
   { antisymm a b hab hba := by
-      simp +instances only [LE.opposite] at *
-      letI := i
+      simp [LE.le] at hab hba
       exact le_antisymm hba hab }
 
 scoped instance (priority := low) instLEAsymmOpposite {i : LE α} [Asymm (α := α) (· ≤ ·)] :
     haveI := i.opposite
     Asymm (α := α) (· ≤ ·) :=
-  letI := i.opposite
   { asymm a b hab := by
-      simp +instances only [LE.opposite] at *
-      letI := i
+      simp [LE.le] at hab ⊢
       exact Asymm.asymm b a hab }
 
 scoped instance (priority := low) instLETransOpposite {i : LE α}
     [Trans (· ≤ ·) (· ≤ ·) (· ≤ · : α → α → Prop)] :
     haveI := i.opposite
     Trans (· ≤ ·) (· ≤ ·) (· ≤ · : α → α → Prop) :=
-  letI := i.opposite
   { trans hab hbc := by
-      simp +instances only [LE.opposite] at *
-      letI := i
+      simp [LE.le] at hab hbc ⊢
       exact Trans.trans hbc hab }
 
 scoped instance (priority := low) instLETotalOpposite {i : LE α} [Total (α := α) (· ≤ ·)] :
@@ -268,16 +260,15 @@ scoped instance (priority := low) instLawfulOrderOrdOpposite {il : LE α} {io :
     haveI := il.opposite
     haveI := io.opposite
     LawfulOrderOrd α :=
-  letI := il.opposite
-  letI := io.opposite
-  { isLE_compare a b := by
-      simp +instances only [LE.opposite, Ord.opposite]
-      letI := il; letI := io
-      apply isLE_compare
-    isGE_compare a b := by
-      simp +instances only [LE.opposite, Ord.opposite]
-      letI := il; letI := io
-      apply isGE_compare }
+      @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)
 
 scoped instance (priority := low) instLawfulOrderLTOpposite {il : LE α} {it : LT α}
     [LawfulOrderLT α] :

src/Init/Data/Range/Polymorphic/Internal/SignedBitVec.lean

@@ -310,8 +310,8 @@ scoped instance instRxiLawfulHasSize : Rxi.LawfulHasSize (BitVec n) where
     rw [← rotate_rotate (x := lo), ← rotate_rotate (x := lo')]
     generalize rotate lo = lo
     generalize rotate lo' = lo'
-    simp +instances only [succ?_rotate, Option.map_eq_map, Option.map_eq_some_iff, rotate_inj, exists_eq_right,
-      instRxiHasSize, rotate_rotate]
+    simp only [succ?_rotate, Option.map_eq_map, Option.map_eq_some_iff, rotate_inj, exists_eq_right,
+      Rxi.HasSize.size, rotate_rotate]
     letI := BitVec.instRxiHasSize (n := n)
     exact Rxi.size_eq_succ_of_succ?_eq_some lo lo'
 

src/Init/Data/Rat/Lemmas.lean

@@ -8,7 +8,13 @@ prelude
 
 public import Init.Data.Rat.Basic
 public import Init.Data.Int.Gcd
-import Init.Data.Int.Bitwise.Lemmas
+import Init.ByCases
+import Init.Data.Bool
+import Init.Data.Int.DivMod.Lemmas
+import Init.Data.Int.Pow
+import Init.Data.Nat.Dvd
+import Init.Omega
+import Init.TacticsExtra
 
 @[expose] public section
 
@@ -636,7 +642,8 @@ theorem ofScientific_ofNat_ofNat :
 /-! ### `≤` and `<` -/
 
 @[simp] theorem num_nonneg {q : Rat} : 0 ≤ q.num ↔ 0 ≤ q := by
-  simp +instances [instLE, Rat.blt, imp.swap]
+  show 0 ≤ q.num ↔ q.blt 0 = false
+  simp [Rat.blt, imp.swap]
 
 @[simp]
 theorem num_eq_zero {q : Rat} : q.num = 0 ↔ q = 0 := by

src/Init/GrindInstances/Ring/UInt.lean

@@ -39,6 +39,7 @@ theorem intCast_ofNat (x : Nat) : (OfNat.ofNat (α := Int) x : UInt8) = OfNat.of
     rw [Int.toNat_pow_of_nonneg (by decide)]
     simp +instances only [ofNat, BitVec.ofNat, Fin.Internal.ofNat_eq_ofNat, Fin.ofNat, Int.reduceToNat, Nat.dvd_refl,
       Nat.mod_mod_of_dvd, instOfNat]
+    try rfl
 
 end UInt8
 
@@ -69,6 +70,7 @@ theorem intCast_ofNat (x : Nat) : (OfNat.ofNat (α := Int) x : UInt16) = OfNat.o
     rw [Int.toNat_pow_of_nonneg (by decide)]
     simp +instances only [ofNat, BitVec.ofNat, Fin.Internal.ofNat_eq_ofNat, Fin.ofNat, Int.reduceToNat, Nat.dvd_refl,
       Nat.mod_mod_of_dvd, instOfNat]
+    try rfl
 
 end UInt16
 
@@ -99,6 +101,7 @@ theorem intCast_ofNat (x : Nat) : (OfNat.ofNat (α := Int) x : UInt32) = OfNat.o
     rw [Int.toNat_pow_of_nonneg (by decide)]
     simp +instances only [ofNat, BitVec.ofNat, Fin.Internal.ofNat_eq_ofNat, Fin.ofNat, Int.reduceToNat, Nat.dvd_refl,
       Nat.mod_mod_of_dvd, instOfNat]
+    try rfl
 
 end UInt32
 
@@ -129,6 +132,7 @@ theorem intCast_ofNat (x : Nat) : (OfNat.ofNat (α := Int) x : UInt64) = OfNat.o
     rw [Int.toNat_pow_of_nonneg (by decide)]
     simp +instances only [ofNat, BitVec.ofNat, Fin.Internal.ofNat_eq_ofNat, Fin.ofNat, Int.reduceToNat, Nat.dvd_refl,
       Nat.mod_mod_of_dvd, instOfNat]
+    try rfl
 
 end UInt64
 
@@ -156,6 +160,7 @@ theorem intCast_ofNat (x : Nat) : (OfNat.ofNat (α := Int) x : USize) = OfNat.of
       rw [Int.toNat_pow_of_nonneg (by decide)]
       simp +instances only [ofNat, BitVec.ofNat, Fin.Internal.ofNat_eq_ofNat, Fin.ofNat, Int.reduceToNat, Nat.dvd_refl,
         Nat.mod_mod_of_dvd, instOfNat]
+      try rfl
     · obtain _ | _ := System.Platform.numBits_eq <;> simp_all
 
 end USize

src/Lean/Meta/WHNF.lean

@@ -768,36 +768,81 @@ where
         failure
     | _ => failure
 
+/--
+Returns `true` if `declName` is the name of class field.
+-/
+private def isProjInst (declName : Name) : MetaM Bool := do
+  let some { fromClass := true, .. } ← getProjectionFnInfo? declName | return false
+  return true
+
+/--
+Auxiliary method for unfolding a class projection. Recall that class fields are not marked with
+`[reducible]`, but we want to reduce them when the transparency setting is `.instances`.
+For example, given `a b : Nat`, the term `a ≤ b` is `LE.le Nat instLENat a b`.
+Unfolding the class field `LE.le` gives `instLENat.1 a b`. This method goes further and
+reduces the instance projection to return `Nat.le a b`.
+-/
+partial def unfoldProjInst? (e : Expr) : MetaM (Option Expr) := do
+  let f := e.getAppFn
+  let .const declName us := f | return none
+  unless (← isProjInst declName) do return none
+  let some fInfo ← withDefault <| getUnfoldableConst? declName | return none
+  deltaBetaDefinition fInfo us e.getAppRevArgs (fun _ => pure none) fun e' => do
+  /-
+  Continuing the example: after delta-beta reducing `LE.le`, we get `e'` which is
+  `instLENat.1 a b`. We consider the unfolding successful if this instance projection
+  reduces to `Nat.le a b` using `.instances` reducibility.
+  -/
+  let some r ← withReducibleAndInstances <| reduceProj? e'.getAppFn | return none
+  recordUnfold declName
+  return some <| mkAppN r e'.getAppArgs |>.headBeta
+
+/--
+Auxiliary method for unfolding a class projection when transparency is set to `TransparencyMode.instances`.
+Recall that class instance projections are not marked with `[reducible]` because we want them to be
+in "reducible canonical form".
+See `unfoldProjInst?`
+-/
+partial def unfoldProjInstWhenInstances? (e : Expr) : MetaM (Option Expr) := do
+  if (← getTransparency) matches .instances then
+    unfoldProjInst? e
+  else
+    return none
+
+register_builtin_option backward.whnf.reducibleClassField : Bool := {
+  defValue := false
+  descr    := "enables better support for unfolding type class fields marked as `[reducible]`"
+}
+
+/--
+Default unfolding function. `e` is of the form `f.{us} a₁ ... aₙ`, and `fInfo` is the `ConstantInfo` for `f`.
+This function has special support for unfolding class fields.
+The support is particularly important when the user marks a class field as `[reducible]` and
+the transparency mode is `.reducible`. For example, suppose `e` is `a ≤ b` where `a b : Nat`,
+and `LE.le` is marked as `[reducible]`. Simply unfolding `LE.le` would give `instLENat.1 a b`,
+which would be stuck because `instLENat` has transparency `[instance_reducible]`. To avoid this, when we unfold
+a `[reducible]` class field, we also unfold the associated projection `instLENat.1` using
+`.instances` reducibility, ultimately returning `Nat.le a b`.
+-/
+private def unfoldDefault (fInfo : ConstantInfo) (us : List Level) (e : Expr) : MetaM (Option Expr) := do
+  if fInfo.hasValue then
+    recordUnfold fInfo.name
+    deltaBetaDefinition fInfo us e.getAppRevArgs (fun _ => pure none) fun e => do
+      if !backward.whnf.reducibleClassField.get (← getOptions) then
+        return some e
+      else if !(← getTransparency) matches .reducible then
+        return some e
+      else if (← isProjInst fInfo.name) then
+        let some r ← withReducibleAndInstances <| reduceProj? e.getAppFn | return some e
+        return mkAppN r e.getAppArgs |>.headBeta
+      else
+        return some e
+  else
+    if fInfo.isAxiom then
+      recordUnfoldAxiom fInfo.name
+    return none
+
 mutual
-
-  /--
-    Auxiliary method for unfolding a class projection.
-  -/
-  partial def unfoldProjInst? (e : Expr) : MetaM (Option Expr) := do
-    match e.getAppFn with
-    | .const declName .. =>
-      match (← getProjectionFnInfo? declName) with
-      | some { fromClass := true, .. } =>
-        match (← withDefault <| unfoldDefinition? e) with
-        | none   => return none
-        | some e =>
-          match (← withReducibleAndInstances <| reduceProj? e.getAppFn) with
-          | none   => return none
-          | some r => recordUnfold declName; return mkAppN r e.getAppArgs |>.headBeta
-      | _ => return none
-    | _ => return none
-
-  /--
-    Auxiliary method for unfolding a class projection when transparency is set to `TransparencyMode.instances`.
-    Recall that class instance projections are not marked with `[reducible]` because we want them to be
-    in "reducible canonical form".
-  -/
-  partial def unfoldProjInstWhenInstances? (e : Expr) : MetaM (Option Expr) := do
-    if (← getTransparency) != TransparencyMode.instances then
-      return none
-    else
-      unfoldProjInst? e
-
   /--
   Unfold definition using "smart unfolding" if possible.
   If `ignoreTransparency = true`, then the definition is unfolded even if the transparency setting does not allow it.
@@ -809,14 +854,8 @@ mutual
         if fInfo.levelParams.length != fLvls.length then
           return none
         else
-          let unfoldDefault (_ : Unit) : MetaM (Option Expr) := do
-            if fInfo.hasValue then
-              recordUnfold fInfo.name
-              deltaBetaDefinition fInfo fLvls e.getAppRevArgs (fun _ => pure none) (fun e => pure (some e))
-            else
-              if fInfo.isAxiom then
-                recordUnfoldAxiom fInfo.name
-              return none
+          let unfoldDefault (_ : Unit) : MetaM (Option Expr) :=
+            unfoldDefault fInfo fLvls e
           if smartUnfolding.get (← getOptions) then
             match ((← getEnv).find? (skipRealize := true) (mkSmartUnfoldingNameFor fInfo.name)) with
             | some fAuxInfo@(.defnInfo _) =>

stage0/src/stdlib_flags.h

@@ -1,3 +1,4 @@
+// update me!!
 #include "util/options.h"
 
 namespace lean {

tests/lean/run/doLogicTests.lean

@@ -142,6 +142,8 @@ example : PostCond (Nat × List.Cursor (List.range' 1 3 1)) (PostShape.except Na
 example : PostCond (Nat × List.Cursor (List.range' 1 3 1)) (PostShape.except Nat (PostShape.arg Nat PostShape.pure)) :=
   post⟨fun (r, xs) s => ⌜r ≤ 4 ∧ s = 4 ∧ r + xs.suffix.sum > 4⌝, fun e s => ⌜e = 42 ∧ s = 4⌝⟩
 
+set_option backward.whnf.reducibleClassField true
+
 theorem throwing_loop_spec :
   ⦃fun s => ⌜s = 4⌝⦄
   throwing_loop
@@ -151,10 +153,8 @@ theorem throwing_loop_spec :
   dsimp +instances only [throwing_loop, get, getThe, instMonadStateOfOfMonadLift, liftM, monadLift]
   mspec
   mspec
-  mspec
   case inv => exact post⟨fun (xs, r) s => ⌜r ≤ 4 ∧ s = 4 ∧ r + xs.suffix.sum > 4⌝, fun e s => ⌜e = 42 ∧ s = 4⌝⟩
   case post.success =>
-    mspec
     mspec
     mspec
     simp_all only [List.sum_nil, Nat.add_zero, gt_iff_lt, SPred.down_pure, SPred.entails_nil,

tests/lean/run/simpDiag.lean

@@ -106,9 +106,8 @@ trace: [simp] Diagnostics
   use `set_option diagnostics.threshold <num>` to control threshold for reporting counters
 ---
 trace: [diag] Diagnostics
-  [reduction] unfolded declarations (max: 246, num: 2):
+  [reduction] unfolded declarations (max: 246, num: 1):
     [reduction] Nat.rec ↦ 246
-    [reduction] OfNat.ofNat ↦ 24
   [reduction] unfolded reducible declarations (max: 246, num: 2):
     [reduction] h ↦ 246
     [reduction] Nat.casesOn ↦ 246

tests/lean/run/unfold_reducible_class_proj.lean

@@ -0,0 +1,48 @@
+import Lean
+
+open Lean Meta
+
+/-!
+Tests whether the class fields marked as `[reducible]` are properly
+reduced by `unfoldDefinition?`.
+-/
+
+set_option backward.whnf.reducibleClassField true
+set_option allowUnsafeReducibility true
+attribute [reducible] MonadControlT.stM
+
+/--
+info: ExceptT ε m
+---
+info: stM m (ExceptT ε m) α
+---
+info: stM m m (MonadControl.stM m (ExceptT ε m) α)
+-/
+#guard_msgs in
+run_meta do
+  withLocalDeclD `ε (.sort 1) fun ε => do
+  withLocalDeclD `α (.sort 1) fun α => do
+  withLocalDeclD `m (.forallE `a (.sort 1) (.sort 1) .default) fun m => do
+  withLocalDeclD `i (mkApp (mkConst ``Monad [0, 0]) m) fun _ => do
+  let e := mkApp2 (mkConst ``ExceptT [0, 0]) ε m
+  check e
+  logInfo e
+  let s ← mkAppM ``stM #[m, e, α]
+  check s
+  logInfo s
+  withReducible do logInfo (← unfoldDefinition? s)
+
+/--
+info: a + a
+---
+info: none
+---
+info: Add.add a a
+-/
+#guard_msgs in
+run_meta do
+  withLocalDeclD `a Nat.mkType fun a => do
+    let e := mkNatAdd a a
+    logInfo e
+    withReducible do logInfo (← unfoldDefinition? e)
+    withReducibleAndInstances do logInfo (← unfoldDefinition? e)

tests/lean/run/unfoldr.lean

@@ -16,7 +16,7 @@ def tst2 (n : Nat) : List Nat :=
   -- Similar example where we provide our custom `SizeOf` instance
   List.unfoldr (sz := ⟨fun b => n - b⟩) (b := 0) fun b =>
     if h : b < n then
-      some (b*2, #(b+1))
+      some (b*2, ⟨b+1, by simp [sizeOf]; omega⟩)
     else
       none