.

Mathlib.lean

@@ -1672,7 +1672,6 @@ import Mathlib.Data.List.Sym
 import Mathlib.Data.List.TFAE
 import Mathlib.Data.List.ToFinsupp
 import Mathlib.Data.List.Zip
-import Mathlib.Data.MLList.Basic
 import Mathlib.Data.MLList.BestFirst
 import Mathlib.Data.MLList.Dedup
 import Mathlib.Data.MLList.DepthFirst

Mathlib/Data/Nondet/Basic.lean

@@ -5,7 +5,6 @@ Authors: Scott Morrison
 -/
 import Std.Tactic.Lint
 import Std.Data.MLList.Basic
-import Mathlib.Data.MLList.Basic
 
 /-!
 # A nondeterminism monad.

Mathlib/Lean/Meta.lean

@@ -17,16 +17,6 @@ open Lean Meta
 
 namespace Lean.MVarId
 
-/-- Solve a goal by synthesizing an instance. -/
--- FIXME: probably can just be `g.inferInstance` once lean4#2054 is fixed
-def synthInstance (g : MVarId) : MetaM Unit := do
-  g.assign (← Lean.Meta.synthInstance (← g.getType))
-
-/-- Add the hypothesis `h : t`, given `v : t`, and return the new `FVarId`. -/
-def note (g : MVarId) (h : Name) (v : Expr) (t : Option Expr := .none) :
-    MetaM (FVarId × MVarId) := do
-  (← g.assert h (← t.getDM (inferType v)) v).intro1P
-
 /-- Add the hypothesis `h : t`, given `v : t`, and return the new `FVarId`. -/
 def «let» (g : MVarId) (h : Name) (v : Expr) (t : Option Expr := .none) :
     MetaM (FVarId × MVarId) := do

lake-manifest.json

@@ -22,19 +22,19 @@
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
-   "rev": "69404390bdc1de946bf0a2e51b1a69f308e56d7a",
+   "rev": "48375eac3aa5e3be2869d718e1f5c38b83787243",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "master",
+   "inputRev": "bump/v4.6.0",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/ProofWidgets4",
    "type": "git",
    "subDir": null,
-   "rev": "bf61e90de075abfa27f638922e7aafafdce77c44",
+   "rev": "8dd18350791c85c0fc9adbd6254c94a81d260d35",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.24-pre2",
+   "inputRev": "v0.0.25",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover/lean4-cli",

lakefile.lean

@@ -28,8 +28,8 @@ require «doc-gen4» from git "https://github.com/leanprover/doc-gen4" @ "main"
 
 require std from git "https://github.com/leanprover/std4" @ "simproc"
 require Qq from git "https://github.com/leanprover-community/quote4" @ "master"
-require aesop from git "https://github.com/leanprover-community/aesop" @ "master"
-require proofwidgets from git "https://github.com/leanprover-community/ProofWidgets4" @ "v0.0.24-pre2"
+require aesop from git "https://github.com/leanprover-community/aesop" @ "bump/v4.6.0"
+require proofwidgets from git "https://github.com/leanprover-community/ProofWidgets4" @ "v0.0.25"
 require Cli from git "https://github.com/leanprover/lean4-cli" @ "main"
 
 /-!