From 48375eac3aa5e3be2869d718e1f5c38b83787243 Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Fri, 5 Jan 2024 01:51:49 +0100
Subject: [PATCH 01/10] chore: adjust to lean4#3123 (#92)

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
---
 Aesop/Index.lean   | 8 ++++----
 lake-manifest.json | 4 ++--
 lakefile.lean      | 2 +-
 lean-toolchain     | 2 +-
 4 files changed, 8 insertions(+), 8 deletions(-)

diff --git a/Aesop/Index.lean b/Aesop/Index.lean
index 13a2a95b..fd17623e 100644
--- a/Aesop/Index.lean
+++ b/Aesop/Index.lean
@@ -14,8 +14,8 @@ open Lean.Meta
 namespace Aesop
 
 structure Index (α : Type) [BEq α] [Hashable α] where
-  byTarget : DiscrTree α 
-  byHyp : DiscrTree α 
+  byTarget : DiscrTree α
+  byHyp : DiscrTree α
   unindexed : PHashSet α
   deriving Inhabited
 
@@ -56,9 +56,9 @@ partial def add (r : α) (imode : IndexingMode) (ri : Index α) :
   | IndexingMode.unindexed =>
     { ri with unindexed := ri.unindexed.insert r }
   | IndexingMode.target keys =>
-    { ri with byTarget := ri.byTarget.insertCore keys r discrTreeConfig }
+    { ri with byTarget := ri.byTarget.insertCore keys r }
   | IndexingMode.hyps keys =>
-    { ri with byHyp := ri.byHyp.insertCore keys r discrTreeConfig }
+    { ri with byHyp := ri.byHyp.insertCore keys r }
   | IndexingMode.or imodes =>
     imodes.foldl (init := ri) λ ri imode =>
       ri.add r imode
diff --git a/lake-manifest.json b/lake-manifest.json
index baee9c8b..61936778 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -4,10 +4,10 @@
  [{"url": "https://github.com/leanprover/std4",
    "type": "git",
    "subDir": null,
-   "rev": "ee49cf8fada1bf5a15592c399a925c401848227f",
+   "rev": "3925dba2ddbe524df4ed94143ae8633b50e3f012",
    "name": "std",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "bump/v4.6.0",
    "inherited": false,
    "configFile": "lakefile.lean"}],
  "name": "aesop",
diff --git a/lakefile.lean b/lakefile.lean
index 267a075d..c2ae1065 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -13,4 +13,4 @@ lean_lib AesopTest {
   globs := #[.submodules "AesopTest"]
 }
 
-require std from git "https://github.com/leanprover/std4" @ "main"
+require std from git "https://github.com/leanprover/std4" @ "bump/v4.6.0"
diff --git a/lean-toolchain b/lean-toolchain
index 3f21e50b..091c6b09 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.5.0-rc1
+leanprover/lean4:nightly-2024-01-03

From 3ff7cbfbd7899eb2dd2004e63b9e1d0c8369322f Mon Sep 17 00:00:00 2001
From: Scott Morrison <scott.morrison@gmail.com>
Date: Thu, 11 Jan 2024 16:40:41 +1100
Subject: [PATCH 02/10] chore: adaptations for leanprover/lean4#3124 (#93)

---
 Aesop/Builder/Forward.lean       |  1 -
 Aesop/Search/Expansion/Simp.lean | 64 ++++++--------------------------
 AesopTest/List.lean              |  4 ++
 lake-manifest.json               |  2 +-
 lean-toolchain                   |  2 +-
 5 files changed, 17 insertions(+), 56 deletions(-)

diff --git a/Aesop/Builder/Forward.lean b/Aesop/Builder/Forward.lean
index d0297399..44630abd 100644
--- a/Aesop/Builder/Forward.lean
+++ b/Aesop/Builder/Forward.lean
@@ -57,7 +57,6 @@ def getImmediatePremises (name : Name) (type : Expr) (md : TransparencyMode) :
       let mut unseen := immediate.sortAndDeduplicate (ord := ⟨Name.quickCmp⟩)
       let mut result := #[]
       for h : i in [:args.size] do
-        have h : i < args.size := by simp_all [Membership.mem]
         let argName := (← args[i].fvarId!.getDecl).userName
         if immediate.contains argName then
           result := result.push i
diff --git a/Aesop/Search/Expansion/Simp.lean b/Aesop/Search/Expansion/Simp.lean
index 87d22bc6..f7a33786 100644
--- a/Aesop/Search/Expansion/Simp.lean
+++ b/Aesop/Search/Expansion/Simp.lean
@@ -9,6 +9,7 @@ import Aesop.Script
 import Aesop.RuleSet
 
 open Lean Lean.Meta
+open Lean.Elab.Tactic (mkSimpOnly)
 open Simp (UsedSimps)
 
 namespace Aesop
@@ -29,51 +30,6 @@ end SimpResult
 
 variable [Monad m] [MonadQuotation m] [MonadError m]
 
--- TODO copy-pasta from Lean.Elab.Tactic.traceSimpCall
--- NOTE: Must be executed in the context of the goal on which `simp` was run.
--- `stx` is the syntax of the original `simp`/`simp_all`/`simp?`/`simp_all?`
--- call.
-def mkSimpOnly (stx : Syntax) (usedSimps : UsedSimps) (includeFVars : Bool) :
-    MetaM Syntax := do
-  let mut stx := stx
-  if stx[3].isNone then
-    stx := stx.setArg 3 (mkNullNode #[mkAtom "only"])
-  let mut args : Array Syntax := #[]
-  let mut localsOrStar := some #[]
-  let lctx ← getLCtx
-  let env ← getEnv
-  for (thm, _) in usedSimps.toArray.qsort (·.2 < ·.2) do
-    match thm with
-    | .decl declName inv => -- global definitions in the environment
-      if env.contains declName && !Lean.Elab.Tactic.simpOnlyBuiltins.contains declName then
-        args := args.push (← if inv then
-          `(Parser.Tactic.simpLemma| ← $(mkIdent (← unresolveNameGlobal declName)):ident)
-        else
-          `(Parser.Tactic.simpLemma| $(mkIdent (← unresolveNameGlobal declName)):ident))
-    | .fvar fvarId => -- local hypotheses in the context
-      if ! includeFVars then
-        continue
-      if let some ldecl := lctx.find? fvarId then
-        localsOrStar := localsOrStar.bind fun locals =>
-          if !ldecl.userName.isInaccessibleUserName &&
-              (lctx.findFromUserName? ldecl.userName).get!.fvarId == ldecl.fvarId then
-            some (locals.push ldecl.userName)
-          else
-            none
-      -- Note: the `if let` can fail for `simp (config := {contextual := true})` when
-      -- rewriting with a variable that was introduced in a scope. In that case we just ignore.
-    | .stx _ thmStx => -- simp theorems provided in the local invocation
-      args := args.push thmStx
-    | .other _ => -- Ignore "special" simp lemmas such as constructed by `simp_all`.
-      pure ()     -- We can't display them anyway.
-  if let some locals := localsOrStar then
-    args := args ++ (← locals.mapM fun id => `(Parser.Tactic.simpLemma| $(mkIdent id):ident))
-  else
-    args := args.push (← `(Parser.Tactic.simpStar| *))
-  let argsStx := if args.isEmpty then #[] else #[mkAtom "[", (mkAtom ",").mkSep args, mkAtom "]"]
-  stx := stx.setArg 4 (mkNullNode argsStx)
-  return stx
-
 -- TODO this way to handle (config := ...) is ugly.
 def mkNormSimpSyntax (normSimpUseHyps : Bool)
     (configStx? : Option Term) : MetaM Syntax.Tactic := do
@@ -92,9 +48,8 @@ def mkNormSimpOnlySyntax (inGoal : MVarId) (normSimpUseHyps : Bool)
     (configStx? : Option Term) (usedTheorems : Simp.UsedSimps) :
     MetaM Syntax.Tactic := do
   let originalStx ← mkNormSimpSyntax normSimpUseHyps configStx?
-  let includeFVars := ! normSimpUseHyps
   let stx ← inGoal.withContext do
-    mkSimpOnly originalStx usedTheorems (includeFVars := includeFVars)
+    mkSimpOnly originalStx usedTheorems
   return ⟨stx⟩
 
 def mkNormSimpContext (rs : RuleSet) (simpConfig : Aesop.SimpConfig) :
@@ -106,13 +61,14 @@ def mkNormSimpContext (rs : RuleSet) (simpConfig : Aesop.SimpConfig) :
   }
 
 def simpGoal (mvarId : MVarId) (ctx : Simp.Context)
-    (discharge? : Option Simp.Discharge := none)
+    (simprocs : Simprocs := {}) (discharge? : Option Simp.Discharge := none)
     (simplifyTarget : Bool := true) (fvarIdsToSimp : Array FVarId := #[])
     (usedSimps : UsedSimps := {}) : MetaM SimpResult := do
   let mvarIdOld := mvarId
   let ctx := { ctx with config.failIfUnchanged := false }
   let (result, usedSimps) ←
-    Meta.simpGoal mvarId ctx discharge? simplifyTarget fvarIdsToSimp usedSimps
+    Meta.simpGoal mvarId ctx simprocs discharge? simplifyTarget fvarIdsToSimp
+      usedSimps
   if let some (_, mvarId) := result then
     if mvarId == mvarIdOld then
       return .unchanged mvarId
@@ -122,7 +78,7 @@ def simpGoal (mvarId : MVarId) (ctx : Simp.Context)
     return .solved usedSimps
 
 def simpGoalWithAllHypotheses (mvarId : MVarId) (ctx : Simp.Context)
-    (discharge? : Option Simp.Discharge := none)
+    (simprocs : Simprocs := {}) (discharge? : Option Simp.Discharge := none)
     (simplifyTarget : Bool := true) (usedSimps : UsedSimps := {}) :
     MetaM SimpResult :=
   mvarId.withContext do
@@ -132,12 +88,14 @@ def simpGoalWithAllHypotheses (mvarId : MVarId) (ctx : Simp.Context)
       if ldecl.isImplementationDetail then
         continue
       fvarIdsToSimp := fvarIdsToSimp.push ldecl.fvarId
-    Aesop.simpGoal mvarId ctx discharge? simplifyTarget fvarIdsToSimp usedSimps
+    Aesop.simpGoal mvarId ctx simprocs discharge? simplifyTarget fvarIdsToSimp
+      usedSimps
 
 def simpAll (mvarId : MVarId) (ctx : Simp.Context)
-    (usedSimps : UsedSimps := {}) : MetaM SimpResult := do
+    (simprocs : Simprocs := {}) (usedSimps : UsedSimps := {}) :
+    MetaM SimpResult := do
   let ctx := { ctx with config.failIfUnchanged := false }
-  match ← Lean.Meta.simpAll mvarId ctx usedSimps with
+  match ← Lean.Meta.simpAll mvarId ctx simprocs usedSimps with
   | (none, usedSimps) => return .solved usedSimps
   | (some mvarIdNew, usedSimps) =>
     if mvarIdNew == mvarId then
diff --git a/AesopTest/List.lean b/AesopTest/List.lean
index d3ca0ccf..7b62960b 100644
--- a/AesopTest/List.lean
+++ b/AesopTest/List.lean
@@ -912,6 +912,8 @@ theorem last_replicate_succ (a m : Nat) :
   induction m <;> aesop
 
 /-! ### last' -/
+section
+set_option linter.deprecated false
 
 @[simp] theorem last'_is_none :
   ∀ {l : List α}, (last' l).isNone ↔ l = []
@@ -989,6 +991,8 @@ theorem last'_append {l₁ l₂ : List α} {x : α} (h : x ∈ l₂.last') :
   x ∈ (l₁ ++ l₂).last' := by
   aesop (add 1% cases List)
 
+end
+
 /-! ### head(') and tail -/
 
 -- Note: Lean 3 head is Lean 4 ihead.
diff --git a/lake-manifest.json b/lake-manifest.json
index 61936778..30030b64 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -4,7 +4,7 @@
  [{"url": "https://github.com/leanprover/std4",
    "type": "git",
    "subDir": null,
-   "rev": "3925dba2ddbe524df4ed94143ae8633b50e3f012",
+   "rev": "5ce12021fcbe7d125aa0881f4e61585def9dec1a",
    "name": "std",
    "manifestFile": "lake-manifest.json",
    "inputRev": "bump/v4.6.0",
diff --git a/lean-toolchain b/lean-toolchain
index 091c6b09..a1cc64c3 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:nightly-2024-01-03
+leanprover/lean4:nightly-2024-01-10

From 60de6c7fc6d6f65a8669dedc34be15feda51e1b8 Mon Sep 17 00:00:00 2001
From: Scott Morrison <scott.morrison@gmail.com>
Date: Sat, 13 Jan 2024 15:12:51 +1100
Subject: [PATCH 03/10] chore: adaptations for leanprover/lean4#3040 (changes
 to termination hints) (#95)

---
 AesopTest/SeqCalcProver.lean | 17 ++++++++---------
 lake-manifest.json           |  4 ++--
 lakefile.lean                |  2 +-
 lean-toolchain               |  2 +-
 4 files changed, 12 insertions(+), 13 deletions(-)

diff --git a/AesopTest/SeqCalcProver.lean b/AesopTest/SeqCalcProver.lean
index 094b9581..b51f2d97 100644
--- a/AesopTest/SeqCalcProver.lean
+++ b/AesopTest/SeqCalcProver.lean
@@ -98,7 +98,6 @@ theorem mem (P : α → Prop) (xs : List α)
   case mpr =>
     intro ⟨a, Pa, Ea⟩
     induction Ea <;> aesop
-termination_by _ => List.length xs
 
 theorem map (P : β → Prop) (f : α → β) (xs : List α)
   : Any P (xs.map f) ↔ Any (fun x => P (f x)) xs := by
@@ -241,8 +240,8 @@ def Cal (l r : List Φ) : (Γ Δ : List (Form Φ)) → Prop
   | Γ, ♩n :: Δ => Cal l (n :: r) Γ Δ
   | φ ⇒ ψ :: Γ, [] => Cal l r Γ [φ] ∧ Cal l r (ψ :: Γ) []
   | Γ, φ ⇒ ψ :: Δ => Cal l r (φ :: Γ) (ψ :: Δ)
-termination_by _ Γ Δ => sum (Γ.map sizeOf) + sum (Δ.map sizeOf)
-decreasing_by simp_wf <;> simp_arith
+termination_by Γ Δ => sum (Γ.map sizeOf) + sum (Δ.map sizeOf)
+decreasing_by all_goals simp_wf <;> simp_arith
 
 instance Cal.instDecidable [DecidableEq Φ] (l r : List Φ) (Γ Δ : List (Form Φ))
   : Decidable (Cal l r Γ Δ) := by
@@ -265,8 +264,8 @@ instance Cal.instDecidable [DecidableEq Φ] (l r : List Φ) (Γ Δ : List (Form
   | Γ, φ ⇒ ψ :: Δ =>
     have ih : Decidable (Cal l r (φ :: Γ) (ψ :: Δ)) := instDecidable l r (φ :: Γ) (ψ :: Δ)
     aesop
-termination_by _ => sum (Γ.map sizeOf) + sum (Δ.map sizeOf)
-decreasing_by simp_wf <;> simp_arith
+termination_by sum (Γ.map sizeOf) + sum (Δ.map sizeOf)
+decreasing_by all_goals simp_wf <;> simp_arith
 
 abbrev Prove (φ : Form Φ) : Prop := Cal [] [] [] [φ]
 
@@ -385,8 +384,8 @@ theorem Cal_sound_complete [DecidableEq Φ]
         have AllΓ : All (Val i) (Γ ++ l.map (♩·)) := by simp_all
         have AnyφψΔ : Any (Val i) (φ ⇒ ψ :: Δ ++ r.map (♩·)) := h i dec AllΓ
         simp_all
-termination_by _ => sum (Γ.map sizeOf) + sum (Δ.map sizeOf)
-decreasing_by simp_wf <;> simp_arith
+termination_by sum (Γ.map sizeOf) + sum (Δ.map sizeOf)
+decreasing_by all_goals simp_wf <;> simp_arith
 
 theorem Prove_sound_complete [DecidableEq Φ] (φ : Form Φ)
   : Prove φ ↔ Valid φ := by
@@ -477,8 +476,8 @@ theorem Cal_Proof [DecidableEq Φ]
     simp at h
     have ih : Proof' l r (φ :: Γ) (ψ :: Δ) := Cal_Proof l r (φ :: Γ) (ψ :: Δ) h
     aesop
-termination_by _ => sum (Γ.map sizeOf) + sum (Δ.map sizeOf)
-decreasing_by simp_wf <;> simp_arith
+termination_by sum (Γ.map sizeOf) + sum (Δ.map sizeOf)
+decreasing_by all_goals simp_wf <;> simp_arith
 
 theorem Proof_sound_complete [DecidableEq Φ] (φ : Form Φ)
   : Proof [] [φ] ↔ Valid φ := by
diff --git a/lake-manifest.json b/lake-manifest.json
index 30030b64..0622f444 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -4,10 +4,10 @@
  [{"url": "https://github.com/leanprover/std4",
    "type": "git",
    "subDir": null,
-   "rev": "5ce12021fcbe7d125aa0881f4e61585def9dec1a",
+   "rev": "27369b95662a33f4d89d1c70a230dd695ddc1b6a",
    "name": "std",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "bump/v4.6.0",
+   "inputRev": "nightly-testing",
    "inherited": false,
    "configFile": "lakefile.lean"}],
  "name": "aesop",
diff --git a/lakefile.lean b/lakefile.lean
index c2ae1065..c2eecf11 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -13,4 +13,4 @@ lean_lib AesopTest {
   globs := #[.submodules "AesopTest"]
 }
 
-require std from git "https://github.com/leanprover/std4" @ "bump/v4.6.0"
+require std from git "https://github.com/leanprover/std4" @ "nightly-testing"
diff --git a/lean-toolchain b/lean-toolchain
index a1cc64c3..4db8563e 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:nightly-2024-01-10
+leanprover/lean4:nightly-2024-01-12

From dd3fcc06697f9a5d382e10635ad972594b8a1451 Mon Sep 17 00:00:00 2001
From: Scott Morrison <scott.morrison@gmail.com>
Date: Wed, 31 Jan 2024 12:03:03 +1100
Subject: [PATCH 04/10] update to nightly-2024-01-30

---
 lake-manifest.json | 2 +-
 lean-toolchain     | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/lake-manifest.json b/lake-manifest.json
index 0a8ab78e..0c92b2c1 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -4,7 +4,7 @@
  [{"url": "https://github.com/leanprover/std4",
    "type": "git",
    "subDir": null,
-   "rev": "3c117bc465a4054afc38c204bb25daa567398ad4",
+   "rev": "74505f7de797c35e703983abb5c6ff3e7570a511",
    "name": "std",
    "manifestFile": "lake-manifest.json",
    "inputRev": "nightly-testing",
diff --git a/lean-toolchain b/lean-toolchain
index b39e2129..ac9a91fd 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:nightly-2024-01-23
+leanprover/lean4:nightly-2024-01-30

From b0de0a268b68cf2ecf9552b6490fbbbb7977c970 Mon Sep 17 00:00:00 2001
From: Scott Morrison <scott.morrison@gmail.com>
Date: Wed, 31 Jan 2024 12:16:11 +1100
Subject: [PATCH 05/10] updates for leanprover/lean4#3210

---
 Aesop/Search/Expansion/Simp.lean | 9 ++++++---
 Aesop/Search/SearchM.lean        | 1 -
 Aesop/Util/Tactic.lean           | 1 -
 lake-manifest.json               | 4 ++--
 lakefile.lean                    | 2 +-
 lean-toolchain                   | 2 +-
 6 files changed, 10 insertions(+), 9 deletions(-)

diff --git a/Aesop/Search/Expansion/Simp.lean b/Aesop/Search/Expansion/Simp.lean
index 340d69d6..da1e39e7 100644
--- a/Aesop/Search/Expansion/Simp.lean
+++ b/Aesop/Search/Expansion/Simp.lean
@@ -48,7 +48,8 @@ def mkNormSimpOnlySyntax (inGoal : MVarId) (normSimpUseHyps : Bool)
     Elab.Tactic.mkSimpOnly originalStx usedTheorems
   return ⟨stx⟩
 
-def simpGoal (mvarId : MVarId) (ctx : Simp.Context) (simprocs : Simprocs)
+def simpGoal (mvarId : MVarId) (ctx : Simp.Context)
+    (simprocs : Simp.SimprocsArray)
     (discharge? : Option Simp.Discharge := none)
     (simplifyTarget : Bool := true) (fvarIdsToSimp : Array FVarId := #[])
     (usedSimps : UsedSimps := {}) : MetaM SimpResult := do
@@ -66,7 +67,8 @@ def simpGoal (mvarId : MVarId) (ctx : Simp.Context) (simprocs : Simprocs)
     return .solved usedSimps
 
 def simpGoalWithAllHypotheses (mvarId : MVarId) (ctx : Simp.Context)
-    (simprocs : Simprocs := {}) (discharge? : Option Simp.Discharge := none)
+    (simprocs : Simp.SimprocsArray := {})
+    (discharge? : Option Simp.Discharge := none)
     (simplifyTarget : Bool := true) (usedSimps : UsedSimps := {}) :
     MetaM SimpResult :=
   mvarId.withContext do
@@ -79,7 +81,8 @@ def simpGoalWithAllHypotheses (mvarId : MVarId) (ctx : Simp.Context)
     Aesop.simpGoal mvarId ctx simprocs discharge? simplifyTarget fvarIdsToSimp
       usedSimps
 
-def simpAll (mvarId : MVarId) (ctx : Simp.Context) (simprocs : Simprocs := {})
+def simpAll (mvarId : MVarId) (ctx : Simp.Context)
+    (simprocs : Simp.SimprocsArray := {})
     (usedSimps : UsedSimps := {}) : MetaM SimpResult := do
   let ctx := { ctx with config.failIfUnchanged := false }
   match ← Lean.Meta.simpAll mvarId ctx simprocs usedSimps with
diff --git a/Aesop/Search/SearchM.lean b/Aesop/Search/SearchM.lean
index 80714633..0d8b97c0 100644
--- a/Aesop/Search/SearchM.lean
+++ b/Aesop/Search/SearchM.lean
@@ -83,7 +83,6 @@ protected def run (ruleSet : RuleSet) (options : Aesop.Options')
   let t ← mkInitialTree goal
   let normSimpContext := {
     config := simpConfig
-    unfoldGround := simpConfig.ground
     maxDischargeDepth := UInt32.ofNatTruncate simpConfig.maxDischargeDepth
     simpTheorems := ruleSet.globalNormSimpTheorems
     congrTheorems := ← getSimpCongrTheorems
diff --git a/Aesop/Util/Tactic.lean b/Aesop/Util/Tactic.lean
index 4b43b8ca..f08e1750 100644
--- a/Aesop/Util/Tactic.lean
+++ b/Aesop/Util/Tactic.lean
@@ -88,7 +88,6 @@ where
           { origin := .decl unfoldThm
             proof := mkConst unfoldThm
             rfl := ← isRflTheorem unfoldThm }
-          (fun _ => return none)
       match result? with
       | none   => return .visit { expr := e }
       | some r =>
diff --git a/lake-manifest.json b/lake-manifest.json
index 0c92b2c1..2e0989c5 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -4,10 +4,10 @@
  [{"url": "https://github.com/leanprover/std4",
    "type": "git",
    "subDir": null,
-   "rev": "74505f7de797c35e703983abb5c6ff3e7570a511",
+   "rev": "efe7a0cbb3735244d2233ff55b06b6a40c287c67",
    "name": "std",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "nightly-testing",
+   "inputRev": "fixes_3210",
    "inherited": false,
    "configFile": "lakefile.lean"}],
  "name": "aesop",
diff --git a/lakefile.lean b/lakefile.lean
index c2eecf11..f5ed6d05 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -13,4 +13,4 @@ lean_lib AesopTest {
   globs := #[.submodules "AesopTest"]
 }
 
-require std from git "https://github.com/leanprover/std4" @ "nightly-testing"
+require std from git "https://github.com/leanprover/std4" @ "fixes_3210"
diff --git a/lean-toolchain b/lean-toolchain
index ac9a91fd..44bf53ed 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:nightly-2024-01-30
+leanprover/lean4-pr-releases:pr-release-3210

From ef2086ecf5d4715f7f188fb18966af55eff4f0ca Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Tue, 30 Jan 2024 18:15:23 -0800
Subject: [PATCH 06/10] fix: some nontermination issues

---
 Aesop/Util/Tactic.lean | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/Aesop/Util/Tactic.lean b/Aesop/Util/Tactic.lean
index f08e1750..705a32a8 100644
--- a/Aesop/Util/Tactic.lean
+++ b/Aesop/Util/Tactic.lean
@@ -72,24 +72,24 @@ where
   -- is slow but correct.
   pre (e : Expr) : StateRefT (HashSet Name) SimpM Simp.Step := do
     let some decl := e.getAppFn'.constName?
-      | return .visit { expr := e }
+      | return .continue
     match unfold? decl with
     | none =>
-      return .visit { expr := e }
+      return .continue
     | some none =>
       if let some e' ← delta? e (λ n => n == decl) then
         modify (·.insert decl)
         return .done { expr := e' }
       else
-        return .visit { expr := e }
+        return .continue
     | some (some unfoldThm) =>
-      let result? ← withReducible <|
+      let result? ← withReducible <| Simp.withDischarger (fun _ => return none) <|
         Simp.tryTheorem? e
           { origin := .decl unfoldThm
             proof := mkConst unfoldThm
             rfl := ← isRflTheorem unfoldThm }
       match result? with
-      | none   => return .visit { expr := e }
+      | none   => return .continue
       | some r =>
         modify (·.insert decl)
         match (← reduceMatcher? r.expr) with

From d6bfe0a3dcc3e3eb7350be071384469fcd353e64 Mon Sep 17 00:00:00 2001
From: Scott Morrison <scott.morrison@gmail.com>
Date: Wed, 31 Jan 2024 13:28:40 +1100
Subject: [PATCH 07/10] correction

---
 Aesop/Util/Tactic.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Aesop/Util/Tactic.lean b/Aesop/Util/Tactic.lean
index 705a32a8..22cd4bc1 100644
--- a/Aesop/Util/Tactic.lean
+++ b/Aesop/Util/Tactic.lean
@@ -83,7 +83,7 @@ where
       else
         return .continue
     | some (some unfoldThm) =>
-      let result? ← withReducible <| Simp.withDischarger (fun _ => return none) <|
+      let result? ← withReducible <|
         Simp.tryTheorem? e
           { origin := .decl unfoldThm
             proof := mkConst unfoldThm

From 825263d983310b72c4a817713c32a15b794b536d Mon Sep 17 00:00:00 2001
From: Scott Morrison <scott.morrison@gmail.com>
Date: Wed, 31 Jan 2024 13:33:00 +1100
Subject: [PATCH 08/10] hack to make test work

---
 AesopTest/List.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/AesopTest/List.lean b/AesopTest/List.lean
index ea10e182..7df86d31 100644
--- a/AesopTest/List.lean
+++ b/AesopTest/List.lean
@@ -186,6 +186,7 @@ theorem subset_trans {l₁ l₂ l₃ : List α} : l₁ ⊆ l₂ → l₂ ⊆ l
 -- END PRELUDE
 
 instance unique_of_is_empty [IsEmpty α] : Unique (List α) := by
+  constructor
   aesop (add 1% cases List)
 
 -- instance : is_left_id (list α) has_append.append [] :=

From ad4ee6b6dab478a090a107d2e9157c21d6046217 Mon Sep 17 00:00:00 2001
From: Jannis Limperg <jannis@limperg.de>
Date: Wed, 31 Jan 2024 18:57:42 +0100
Subject: [PATCH 09/10] Proper fix for List test

---
 AesopTest/List.lean | 2 --
 1 file changed, 2 deletions(-)

diff --git a/AesopTest/List.lean b/AesopTest/List.lean
index 7df86d31..5954d6b8 100644
--- a/AesopTest/List.lean
+++ b/AesopTest/List.lean
@@ -16,7 +16,6 @@ set_option aesop.check.script true
 -- use `sorry` because it generates lots of warnings.
 axiom ADMIT : ∀ {α : Sort _}, α
 
-@[aesop safe cases]
 class IsEmpty (α : Sort _) where
   false : α → False
 
@@ -186,7 +185,6 @@ theorem subset_trans {l₁ l₂ l₃ : List α} : l₁ ⊆ l₂ → l₂ ⊆ l
 -- END PRELUDE
 
 instance unique_of_is_empty [IsEmpty α] : Unique (List α) := by
-  constructor
   aesop (add 1% cases List)
 
 -- instance : is_left_id (list α) has_append.append [] :=

From 38f40262a09c3db75f809579a76a40ed8c0ea27b Mon Sep 17 00:00:00 2001
From: Scott Morrison <scott.morrison@gmail.com>
Date: Thu, 1 Feb 2024 19:39:35 +1100
Subject: [PATCH 10/10] bump toolchain

---
 lean-toolchain | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/lean-toolchain b/lean-toolchain
index 44bf53ed..c854de7c 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4-pr-releases:pr-release-3210
+leanprover/lean4:nightly-2024-02-01