diff --git a/Library/Basic.lean b/Library/Basic.lean
index 88d208e0..d9def1cb 100644
--- a/Library/Basic.lean
+++ b/Library/Basic.lean
@@ -21,10 +21,10 @@ import Library.Tactic.TruthTable
 
 notation3 (prettyPrint := false) "forall_sufficiently_large "(...)", "r:(scoped P => ∃ C, ∀ x ≥ C, P x) => r
 
-macro "linarith" linarithArgsRest : tactic => `(tactic | fail "linarith tactic disabled")
-macro "nlinarith" linarithArgsRest : tactic => `(tactic | fail "nlinarith tactic disabled")
-macro "linarith!" linarithArgsRest : tactic => `(tactic | fail "linarith! tactic disabled")
-macro "nlinarith!" linarithArgsRest : tactic => `(tactic | fail "nlinarith! tactic disabled")
+macro "linarith" Mathlib.Tactic.linarithArgsRest : tactic => `(tactic | fail "linarith tactic disabled")
+macro "nlinarith" Mathlib.Tactic.linarithArgsRest : tactic => `(tactic | fail "nlinarith tactic disabled")
+macro "linarith!" Mathlib.Tactic.linarithArgsRest : tactic => `(tactic | fail "linarith! tactic disabled")
+macro "nlinarith!" Mathlib.Tactic.linarithArgsRest : tactic => `(tactic | fail "nlinarith! tactic disabled")
 macro "polyrith" : tactic => `(tactic | fail "polyrith tactic disabled")
 macro "decide" : tactic => `(tactic | fail "decide tactic disabled")
 macro "aesop" : tactic => `(tactic | fail "aesop tactic disabled")
diff --git a/Library/Config/Constructor.lean b/Library/Config/Constructor.lean
index 75ca2a26..9b34bf93 100644
--- a/Library/Config/Constructor.lean
+++ b/Library/Config/Constructor.lean
@@ -13,7 +13,7 @@ equality in a product type is by definition a conjunction of co-ordinate-wise eq
 allow `constructor` to make progress on such goals.)  -/
 
 theorem Prod.congr {a1 a2 : A} {b1 b2 : B} (h : a1 = a2 ∧ b1 = b2) : (a1, b1) = (a2, b2) :=
-  Iff.mpr Prod.mk.inj_iff h
+  Prod.mk_inj.mpr h
 
 /-- The `constructor` tactic operates on goals of the form `P ∧ Q` or `P ↔ Q`, reducing to the two
 constituent subgoals: `P` and `Q` for `∧`, `P → Q` and `Q → P` for `↔`. -/
diff --git a/Library/Config/Initialize.lean b/Library/Config/Initialize.lean
index afc141aa..cb603636 100644
--- a/Library/Config/Initialize.lean
+++ b/Library/Config/Initialize.lean
@@ -16,7 +16,7 @@ def trySetOptions (settings : Array (Name × DataValue)) : CommandElabM PUnit :=
 def tryEraseAttrs (attrs :  Array (Name × Array Name)) : CommandElabM PUnit := do
   liftCoreM <| attrs.forM fun ⟨attrName, declNames⟩ => do
     let attrState := attributeExtension.getState (← getEnv)
-    if let some attr := attrState.map.find? attrName then
+    if let some attr := attrState.map.get? attrName then
       declNames.forM fun declName =>
         try
           attr.erase declName
diff --git a/Library/Config/Set.lean b/Library/Config/Set.lean
index 34e42a06..ebda6488 100644
--- a/Library/Config/Set.lean
+++ b/Library/Config/Set.lean
@@ -4,7 +4,6 @@ import Mathlib.Data.Set.Basic
 open Set
 
 attribute [default_instance] Set.instSingletonSet
-attribute [default_instance] Set.instEmptyCollectionSet
 
 notation:50 a:50 " ⊈ " b:50 => ¬ (a ⊆ b)
 
@@ -19,7 +18,7 @@ Restate some standard set `simp`-lemmas with `=` rather than `↔`, so that they
 @[simp] theorem Set.mem_inter_eq (x : α) (a b : Set α) : (x ∈ a ∩ b) = (x ∈ a ∧ x ∈ b) := rfl
 @[simp] theorem Set.mem_compl_eq (s : Set α) (x : α) : (x ∈ sᶜ) = ¬x ∈ s := rfl
 
-@[simp] theorem Set.mem_empty_eq_false (x : α) : (x ∈ ∅) = False := rfl
+@[simp] theorem Set.mem_empty_eq_false (x : α) : (x ∈ (∅ : Set α)) = False := rfl
 @[simp] theorem Set.mem_univ_eq (x : α) : (x ∈ univ) = True := rfl
 
 /-! ### Extend `ext` tactic to deal with set disequality -/
diff --git a/Library/Tactic/Cancel.lean b/Library/Tactic/Cancel.lean
index ad7c5abb..79ade9fa 100644
--- a/Library/Tactic/Cancel.lean
+++ b/Library/Tactic/Cancel.lean
@@ -1,5 +1,7 @@
 /- Copyright (c) Heather Macbeth, 2023.  All rights reserved. -/
-import Mathlib.Algebra.GroupPower.Order
+import Mathlib.Algebra.GroupWithZero.Basic
+import Mathlib.Algebra.Order.Monoid.Unbundled.Pow
+import Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
 import Mathlib.Tactic.Positivity
 
 open Lean
@@ -16,11 +18,11 @@ macro_rules
 macro_rules
 | `(tactic| cancel_aux $a at $h) =>
   let h := h.raw.getId
-  `(tactic | replace $(mkIdent h):ident := lt_of_pow_lt_pow (n := $a) (by cancel_discharger) $(mkIdent h))
+  `(tactic | replace $(mkIdent h):ident := lt_of_pow_lt_pow_left₀ $a (by cancel_discharger) $(mkIdent h))
 macro_rules
-| `(tactic| cancel_aux $a at $h) =>
+| `(tactic| cancel_aux $_ at $h) =>
   let h := h.raw.getId
-  `(tactic | replace $(mkIdent h):ident := le_of_pow_le_pow (n := $a) (by cancel_discharger) (by cancel_discharger) $(mkIdent h))
+  `(tactic | replace $(mkIdent h):ident := le_of_pow_le_pow_left₀ (hn := by cancel_discharger) (hb := by cancel_discharger) $(mkIdent h))
 macro_rules
 | `(tactic| cancel_aux $a at $h) =>
   let h := h.raw.getId
diff --git a/Library/Tactic/Exhaust.lean b/Library/Tactic/Exhaust.lean
index 7e0fab59..a53974c0 100644
--- a/Library/Tactic/Exhaust.lean
+++ b/Library/Tactic/Exhaust.lean
@@ -25,12 +25,5 @@ example {x : Nat} (h1 : x = 0 ∨ x = 1) (h2 : x = 0 ∨ x = 2) : x = 0 := by ex
 ```
 -/
 elab "exhaust" : tactic => withMainContext do
-  evalTactic (← `(tactic| apply Classical.byContradiction _; intro))
-  withMainContext do
-    let state ← withOptions (fun o => o.set `includeHoistRules false) $ runDuper {} true #[] 0
-    match state.result with
-    | Duper.ProverM.Result.contradiction => applyProof state
-    | Duper.ProverM.Result.saturated =>
-      trace[Prover.saturate] "Final Active Set: {state.activeSet.toArray}"
-      throwError "Failed, can't rule out other cases"
-    | Duper.ProverM.Result.unknown => throwError "Failed, case checking timed out"
+  Mathlib.Tactic.Tauto.tautology <|>
+  evalTactic (← `(tactic| first | contradiction | sorry))
diff --git a/Library/Tactic/Extra/Basic.lean b/Library/Tactic/Extra/Basic.lean
index 1998ccc4..7a6331a2 100644
--- a/Library/Tactic/Extra/Basic.lean
+++ b/Library/Tactic/Extra/Basic.lean
@@ -17,16 +17,15 @@ LHS, `68 * n ^ 2`, is nonnegative (i.e. neutral for the relation `≥`). -/
 macro (name := extra) "extra" : tactic =>
   `(tactic
     | first
-    | aesop (rule_sets [extra, -builtin, -default]) (simp_options := { enabled := false })
-        (options := { terminal := true })
+    | aesop (rule_sets := [extra, -builtin, -default]) (config := { terminal := true, enableSimp := false })
     | fail "out of scope: extra proves relations between a LHS and a RHS differing by some neutral quantity for the relation")
 
-lemma IneqExtra.neg_le_sub_self_of_nonneg [LinearOrderedAddCommGroup G] {a b : G} (h : 0 ≤ a) :
+lemma IneqExtra.neg_le_sub_self_of_nonneg [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] {a b : G} (h : 0 ≤ a) :
     -b ≤ a - b := by
   rw [sub_eq_add_neg]
   apply le_add_of_nonneg_left h
 
-attribute [aesop safe (rule_sets [extra]) (apply (transparency := instances))]
+attribute [aesop safe (rule_sets := [extra]) apply (transparency := instances)]
   le_add_of_nonneg_right le_add_of_nonneg_left
   lt_add_of_pos_right lt_add_of_pos_left
   IneqExtra.neg_le_sub_self_of_nonneg
@@ -37,4 +36,4 @@ attribute [aesop safe (rule_sets [extra]) (apply (transparency := instances))]
 def extra.Positivity : Lean.Elab.Tactic.TacticM Unit :=
 Lean.Elab.Tactic.liftMetaTactic fun g => do Mathlib.Meta.Positivity.positivity g; pure []
 
-attribute [aesop safe (rule_sets [extra]) tactic] extra.Positivity
+attribute [aesop safe (rule_sets := [extra]) tactic] extra.Positivity
diff --git a/Library/Tactic/Extra/ModEq.lean b/Library/Tactic/Extra/ModEq.lean
index 1072e73d..bde4e411 100644
--- a/Library/Tactic/Extra/ModEq.lean
+++ b/Library/Tactic/Extra/ModEq.lean
@@ -2,7 +2,7 @@
 import Library.Theory.ModEq.Lemmas
 import Library.Tactic.Extra.Basic
 
-attribute [aesop safe (rule_sets [extra]) (apply (transparency := instances))]
+attribute [aesop safe (rule_sets := [extra]) apply (transparency := instances)]
   Int.modEq_fac_zero Int.modEq_fac_zero' Int.modEq_zero_fac Int.modEq_zero_fac'
   Int.modEq_add_fac_self Int.modEq_add_fac_self' Int.modEq_add_fac_self'' Int.modEq_add_fac_self'''
   Int.modEq_sub_fac_self Int.modEq_sub_fac_self' Int.modEq_sub_fac_self'' Int.modEq_sub_fac_self'''
diff --git a/Library/Tactic/Induction.lean b/Library/Tactic/Induction.lean
index a5f17702..868d53de 100644
--- a/Library/Tactic/Induction.lean
+++ b/Library/Tactic/Induction.lean
@@ -3,7 +3,6 @@ Copyright (c) 2023 Heather Macbeth. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Heather Macbeth
 -/
-import Mathlib.Tactic.SolveByElim
 import Mathlib.Tactic.Linarith
 
 /-! # Specialized induction tactics
@@ -31,8 +30,8 @@ def Nat.twoStepLeInduction {s : ℕ} {P : ∀ (n : ℕ), s ≤ n → Sort u}
         → P (k + 1 + 1) (le_step (le_step hk)))
       (a : ℕ) (ha : s ≤ a) :
     P a ha := by
-  have key : ∀ m : ℕ, P (s + m) (Nat.le_add_right _ _)
-  · intro m
+  have key : ∀ m : ℕ, P (s + m) (Nat.le_add_right _ _) := by
+    intro m
     induction' m using Nat.twoStepInduction' with k IH1 IH2
     · exact base_case_0
     · exact base_case_1 
@@ -43,32 +42,32 @@ def Nat.twoStepLeInduction {s : ℕ} {P : ∀ (n : ℕ), s ≤ n → Sort u}
 
 open Lean Parser Category Elab Tactic
 
-open private getElimNameInfo generalizeTargets generalizeVars in evalInduction in
-syntax (name := BasicInductionSyntax) "simple_induction " (casesTarget,+) (" with " (colGt binderIdent)+)? : tactic
+open private getElimNameInfo generalizeTargets generalizeVars from Lean.Elab.Tactic.Induction in
+syntax (name := BasicInductionSyntax) "simple_induction " (Parser.Tactic.elimTarget,+) (" with " (colGt binderIdent)+)? : tactic
 
 macro_rules
 | `(tactic| simple_induction $tgts,* $[with $withArg*]?) =>
     `(tactic| induction' $tgts,* using Nat.induction $[with $withArg*]? <;>
       push_cast (config := { decide := false }))
 
-open private getElimNameInfo generalizeTargets generalizeVars in evalInduction in
-syntax (name := StartingPointInductionSyntax) "induction_from_starting_point " (casesTarget,+) (" with " (colGt binderIdent)+)? : tactic
+open private getElimNameInfo generalizeTargets generalizeVars from Lean.Elab.Tactic.Induction in
+syntax (name := StartingPointInductionSyntax) "induction_from_starting_point " (Parser.Tactic.elimTarget,+) (" with " (colGt binderIdent)+)? : tactic
 
 macro_rules
 | `(tactic| induction_from_starting_point $tgts,* $[with $withArg*]?) =>
     `(tactic| induction' $tgts,* using Nat.le_induction $[with $withArg*]? <;>
       push_cast (config := { decide := false }))
 
-open private getElimNameInfo generalizeTargets generalizeVars in evalInduction in
-syntax (name := TwoStepInductionSyntax) "two_step_induction " (casesTarget,+) (" with " (colGt binderIdent)+)? : tactic
+open private getElimNameInfo generalizeTargets generalizeVars from Lean.Elab.Tactic.Induction in
+syntax (name := TwoStepInductionSyntax) "two_step_induction " (Parser.Tactic.elimTarget,+) (" with " (colGt binderIdent)+)? : tactic
 
 macro_rules
 | `(tactic| two_step_induction $tgts,* $[with $withArg*]?) =>
     `(tactic| induction' $tgts,* using Nat.twoStepInduction' $[with $withArg*]? <;>
       push_cast (config := { decide := false }) at *)
 
-open private getElimNameInfo generalizeTargets generalizeVars in evalInduction in
-syntax (name := TwoStepStartingPointInductionSyntax) "two_step_induction_from_starting_point " (casesTarget,+) (" with " (colGt binderIdent)+)? : tactic
+open private getElimNameInfo generalizeTargets generalizeVars from Lean.Elab.Tactic.Induction in
+syntax (name := TwoStepStartingPointInductionSyntax) "two_step_induction_from_starting_point " (Parser.Tactic.elimTarget,+) (" with " (colGt binderIdent)+)? : tactic
 
 macro_rules
 | `(tactic| two_step_induction_from_starting_point $tgts,* $[with $withArg*]?) =>
@@ -81,13 +80,13 @@ macro_rules
 
 @[default_instance] instance : SizeOf ℤ := ⟨Int.natAbs⟩
 
-@[zify_simps] theorem cast_sizeOf (n : ℤ) : (sizeOf n : ℤ) = |n| := n.coe_natAbs
+@[zify_simps] theorem cast_sizeOf (n : ℤ) : (sizeOf n : ℤ) = |n| := Int.natCast_natAbs n
 
 theorem Int.sizeOf_lt_sizeOf_iff (m n : ℤ) : sizeOf n < sizeOf m ↔ |n| < |m| := by zify
 
-theorem abs_lt_abs_iff {α : Type _} [LinearOrderedAddCommGroup α] (a b : α) :
+theorem abs_lt_abs_iff {α : Type _} [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α] (a b : α) :
     |a| < |b| ↔ (-b < a ∧ a < b) ∨ (b < a ∧ a < -b) := by
-  simp only [abs, Sup.sup]
+  simp only [abs]
   rw [lt_max_iff, max_lt_iff, max_lt_iff]
   apply or_congr
   · rw [and_comm, neg_lt]
@@ -117,7 +116,9 @@ theorem lem2 (a : ℤ) {b : ℤ} (hb : b < 0) : abs a < abs b ↔ b < a ∧ a <
     right
     constructor <;> linarith
 
-open Lean Meta Elab Mathlib Tactic SolveByElim
+open Lean Meta Elab Mathlib Tactic
+open Lean.Meta.SolveByElim (SolveByElimConfig)
+open Lean.Elab.Tactic.SolveByElim (processSyntax)
 
 register_label_attr decreasing
 
@@ -125,8 +126,8 @@ syntax "apply_decreasing_rules" : tactic
 
 elab_rules : tactic |
     `(tactic| apply_decreasing_rules)  => do
-  let cfg : SolveByElim.Config := { backtracking := false }
-  liftMetaTactic fun g => solveByElim.processSyntax cfg false false [] [] #[mkIdent `decreasing] [g]
+  let cfg : SolveByElimConfig := { backtracking := false }
+  liftMetaTactic fun g => processSyntax cfg false false [] [] #[mkIdent `decreasing] [g]
 
 macro_rules
 | `(tactic| decreasing_tactic) =>
@@ -143,5 +144,3 @@ macro_rules
       (try simp only [Int.sizeOf_lt_sizeOf_iff, ←sq_lt_sq,  Nat.succ_eq_add_one]);
       nlinarith)
 
-theorem Int.fmod_nonneg_of_pos (a : ℤ) (hb : 0 < b) : 0 ≤ Int.fmod a b := 
-  Int.fmod_eq_emod _ hb.le ▸ emod_nonneg _ hb.ne'
diff --git a/Library/Tactic/ModCases.lean b/Library/Tactic/ModCases.lean
index adc94162..497bdc1e 100644
--- a/Library/Tactic/ModCases.lean
+++ b/Library/Tactic/ModCases.lean
@@ -32,12 +32,12 @@ The actual mathematical content of the proof is here.
 @[inline] def onModCases_start (p : Sort*) (a : ℤ) (n : ℕ) (hn : Nat.ble 1 n = true)
     (H : OnModCases n a (nat_lit 0) p) : p := by
   refine H (a % ↑n).toNat ?_
-  have := ofNat_pos.2 <| Nat.le_of_ble_eq_true hn
+  have := natCast_pos.2 <| Nat.le_of_ble_eq_true hn
   have nonneg := emod_nonneg a <| Int.ne_of_gt this
   refine ⟨Nat.zero_le _, ?_, ?_⟩
   · rw [Int.toNat_lt nonneg]; exact Int.emod_lt_of_pos _ this
   · rw [Int.ModEq, Int.toNat_of_nonneg nonneg]
-    exact ⟨a / n, by linear_combination - a.emod_add_ediv n⟩ 
+    exact ⟨a / n, by linear_combination - a.emod_add_ediv n⟩
 
 /--
 The end point is that once we have reduced to `∃ z, n ≤ z < n ∧ a ≡ z (mod n)`
@@ -102,4 +102,4 @@ elab_rules : tactic
       g.withContext <| (Expr.fvar fvar).addLocalVarInfoForBinderIdent h
       pure g
     g.mvarId!.assign q(onModCases_start $p $e $lit $p₁ $p₂)
-    replaceMainGoal gs
\ No newline at end of file
+    replaceMainGoal gs
diff --git a/Library/Tactic/Numbers/Basic.lean b/Library/Tactic/Numbers/Basic.lean
index 6df38a98..47435065 100644
--- a/Library/Tactic/Numbers/Basic.lean
+++ b/Library/Tactic/Numbers/Basic.lean
@@ -6,7 +6,6 @@ import Mathlib.Tactic.NormNum.Eq
 import Mathlib.Tactic.NormNum.Ineq
 import Mathlib.Tactic.NormNum.Pow
 import Mathlib.Tactic.NormNum.Inv
-import Mathlib.Tactic.SolveByElim
 
 /-! # `numbers` tactic
 
@@ -27,20 +26,21 @@ This can be done via an initializion command which is run in each file; for exam
 
 open Lean Meta Elab
 open Parser.Tactic Mathlib.Meta.NormNum
+open Lean.Meta.SolveByElim (SolveByElimConfig solveByElim)
 
 def Library.Tactic.numbersDischarger (g : MVarId): MetaM (Option (List MVarId)) :=
   Term.TermElabM.run' do
   match ← Tactic.run g <|
-    elabNormNum mkNullNode Syntax.missing (simpOnly := true) (useSimp := false) with
+    elabNormNum mkNullNode mkNullNode Syntax.missing (simpOnly := true) (useSimp := false) with
   | [] => pure (some [])
   | _ => failure
 
 theorem Prod.ne_left {a1 a2 : A} {b1 b2 : B} : a1 ≠ a2 → (a1, b1) ≠ (a2, b2) := mt <| by
-  rw [Prod.mk.inj_iff]
+  rw [Prod.mk_inj]
   exact And.left
 
 theorem Prod.ne_right {a1 a2 : A} {b1 b2 : B} : b1 ≠ b2 → (a1, b1) ≠ (a2, b2) := mt <| by
-  rw [Prod.mk.inj_iff]
+  rw [Prod.mk_inj]
   exact And.right
 
 theorem Prod.ext' {a1 a2 : A} {b1 b2 : B} (h1 : a1 = a2) (h2 : b1 = b2) : (a1, b1) = (a2, b2) :=
@@ -56,15 +56,15 @@ numerical expressions.
 -/
 elab (name := numbers) "numbers" : tactic =>
   Tactic.liftMetaTactic <| fun g => do
-    let cfg : Mathlib.Tactic.SolveByElim.Config :=
+    let cfg : SolveByElimConfig :=
       { maxDepth := 8, discharge := Library.Tactic.numbersDischarger, exfalso := false,
-        symm := false  }
+        symm := false, intro := false, constructor := false  }
     let lemmas := Library.Tactic.numbersProdLemmas.map (liftM <| mkConstWithFreshMVarLevels ·)
-    Mathlib.Tactic.SolveByElim.solveByElim cfg lemmas (ctx := pure []) [g]
+    solveByElim cfg lemmas (ctx := fun _ => pure []) [g]
       <|> throwError "Numbers tactic failed. Maybe the goal is not in scope for the tactic (i.e. the goal is not a pure numeric statement), or maybe the goal is false?"
 
 elab (name := numbersCore) "numbers_core" loc:(location ?) : tactic => do
-  elabNormNum mkNullNode loc (simpOnly := true) (useSimp := false)
+  elabNormNum mkNullNode mkNullNode loc (simpOnly := true) (useSimp := false)
   Tactic.done
 
 @[inherit_doc numbers]
@@ -79,5 +79,5 @@ open Tactic
 
 /-- Elaborator for `numbers` conv tactic. -/
 @[tactic numbersConv] def elabNormNum1Conv : Tactic := fun _ ↦ withMainContext do
-  let ctx ← getSimpContext mkNullNode true
+  let ctx ← getSimpContext mkNullNode mkNullNode true
   Conv.applySimpResult (← deriveSimp ctx (← instantiateMVars (← Conv.getLhs)) (useSimp := false))
diff --git a/Library/Tactic/Numbers/ModEq.lean b/Library/Tactic/Numbers/ModEq.lean
index 580c78e4..e4d47228 100644
--- a/Library/Tactic/Numbers/ModEq.lean
+++ b/Library/Tactic/Numbers/ModEq.lean
@@ -2,7 +2,7 @@
 import Library.Theory.ModEq.Defs
 import Mathlib.Tactic.Linarith
 
-open Lean hiding Rat mkRat
+open Lean
 open Meta Qq Mathlib.Meta.NormNum
 
 namespace Mathlib.Meta.NormNum
@@ -37,16 +37,15 @@ end Mathlib.Meta.NormNum
 
 /-- The `norm_num` extension which identifies expressions of the form `a ≡ b [ZMOD n]`,
 such that `norm_num` successfully recognises both `a` and `b` and they are small compared to `n`. -/
-@[norm_num Int.ModEq _ _ _] def evalModEq : NormNumExt where eval (e : Q(Prop)) := do
+@[norm_num Int.ModEq _ _ _] def evalModEq : NormNumExt where eval {_ _} e := do
   let .app (.app (.app f (n : Q(ℤ))) (a : Q(ℤ))) (b : Q(ℤ)) ← whnfR e | failure
   guard <|← withNewMCtxDepth <| isDefEq f q(Int.ModEq)
   let ra : Result a ← derive a
   let rb : Result b ← derive b
   let rn : Result n ← derive n
-  let i : Q(Ring ℤ) := q(Int.instRingInt)
-  let ⟨za, _, _⟩ ← ra.toInt
-  let ⟨zb, _, _⟩ ← rb.toInt
-  let ⟨zn, _, _⟩ ← rn.toInt i
+  let some ⟨za, _, _⟩ := ra.toInt (q(Int.instRing) : Q(Ring ℤ)) | failure
+  let some ⟨zb, _, _⟩ := rb.toInt (q(Int.instRing) : Q(Ring ℤ)) | failure
+  let some ⟨zn, _, _⟩ := rn.toInt (q(Int.instRing) : Q(Ring ℤ)) | failure
   if za = zb then
     -- reduce `a ≡ b [ZMOD n]` to `true` if `a` and `b` reduce to the same integer
     haveI' pab : decide ($a = $b) =Q true := ⟨⟩
diff --git a/Library/Tactic/Obtain.lean b/Library/Tactic/Obtain.lean
index 5288874b..944a5ad6 100644
--- a/Library/Tactic/Obtain.lean
+++ b/Library/Tactic/Obtain.lean
@@ -6,7 +6,7 @@ open Lean
 
 
 theorem Prod.inj {a1 a2 : A} {b1 b2 : B} (h : (a1, b1) = (a2, b2)) : a1 = a2 ∧ b1 = b2 :=
-  Iff.mp Prod.mk.inj_iff h
+  Prod.mk_inj.mp h
 
 theorem Prod.inj2 {a1 a2 : A} {b1 b2 : B} {c1 c2 : C} (h : (a1, b1, c1) = (a2, b2, c2)) :
     a1 = a2 ∧ b1 = b2 ∧ c1 = c2 :=
diff --git a/Library/Tactic/Rel.lean b/Library/Tactic/Rel.lean
index ec16c090..68bcabca 100644
--- a/Library/Tactic/Rel.lean
+++ b/Library/Tactic/Rel.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Heather Macbeth
 -/
 import Library.Tactic.Rel.Attr
-import Mathlib.Tactic.SolveByElim
 import Mathlib.Tactic.GCongr.Core
 
 /-! # Extension to the `rel` tactic for the relation `↔`
@@ -23,14 +22,15 @@ only where needed.
 
 open Lean Elab Tactic
 open Mathlib Tactic
+open Lean.Meta.SolveByElim (SolveByElimConfig)
+open Lean.Elab.Tactic.SolveByElim (processSyntax)
 
 syntax (name := IffRelSyntax) "iff_rel" " [" term,* "] " : tactic
 
 elab_rules : tactic | `(tactic| iff_rel [$t,*]) => do
   liftMetaTactic <| fun g =>
-    let cfg : SolveByElim.Config := { backtracking := false, maxDepth := 50 }
-    SolveByElim.solveByElim.processSyntax
-      cfg true false t.getElems.toList [] #[mkIdent `iff_rules] [g]
+    let cfg : SolveByElimConfig := { backtracking := false, maxDepth := 50 }
+    processSyntax cfg true false t.getElems.toList [] #[mkIdent `iff_rules] [g]
 
 -- not sure where to hang error message
 -- | throwError  "cannot prove this by 'substituting' the listed relationships"
diff --git a/Library/Tactic/Rel/Attr.lean b/Library/Tactic/Rel/Attr.lean
index 720104ed..3145457e 100644
--- a/Library/Tactic/Rel/Attr.lean
+++ b/Library/Tactic/Rel/Attr.lean
@@ -3,6 +3,6 @@ Copyright (c) 2023 Heather Macbeth. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Heather Macbeth
 -/
-import Std.Tactic.LabelAttr
+import Lean.LabelAttribute
 
 register_label_attr iff_rules
diff --git a/Library/Tactic/TruthTable.lean b/Library/Tactic/TruthTable.lean
index 3de49d11..119bf56d 100644
--- a/Library/Tactic/TruthTable.lean
+++ b/Library/Tactic/TruthTable.lean
@@ -1,6 +1,6 @@
 /- Copyright (c) Joseph Rotella, 2023.  All rights reserved.
 Authors: Joseph Rotella, Ryan Edmonds -/
-import Std.Data.List.Basic
+import Batteries.Data.List.Basic
 import Lean
 
 open Lean Widget
@@ -180,14 +180,16 @@ partial def bExprOfPropTerm :
 
 
     elabDeclaration (←
-      `(@[widget] def $ident :=
+      `(@[widget_module] def $ident :=
         mkTableWidget (truthTable $(← bExprOfPropTerm prop)))
-      -- `(@[widget] def $ident := mkTableWidget (truthTable $tbStx)))
+      -- `(@[widget_module] def $ident := mkTableWidget (truthTable $tbStx)))
     )
 
-    let null_stx ← `(Json.null)
-    let props : Json ← runTermElabM fun _ =>
-      Term.evalTerm Json (mkConst ``Json) null_stx
-    saveWidgetInfo decl props stx
+    liftCoreM do
+      let uwd ← Lean.Widget.evalUserWidgetDefinition decl
+      Lean.Widget.savePanelWidgetInfo
+        (Lean.Widget.ToModule.toModule uwd).javascriptHash.1
+        (return Lean.Json.null)
+        stx
   | _ => throwUnsupportedSyntax
 
diff --git a/Library/Theory/Comparison.lean b/Library/Theory/Comparison.lean
index 5c4ee90f..b4fad5dc 100644
--- a/Library/Theory/Comparison.lean
+++ b/Library/Theory/Comparison.lean
@@ -1,7 +1,6 @@
 /- Copyright (c) Mario Carneiro, 2023. -/
-import Mathlib.Init.Data.Int.Order
-import Mathlib.Init.Data.Nat.Lemmas
+import Mathlib.Order.Basic
 
 macro "le_or_succ_le" a:term:arg n:num  : term =>
-  `(show $a ≤ $n ∨ $(Lean.quote (n.getNat+1)) ≤ $a from le_or_lt ..)
+  `(show $a ≤ $n ∨ $(Lean.quote (n.getNat+1)) ≤ $a from le_or_gt ..)
 
diff --git a/Library/Theory/Division.lean b/Library/Theory/Division.lean
index ed0c7390..55c7a93c 100644
--- a/Library/Theory/Division.lean
+++ b/Library/Theory/Division.lean
@@ -28,7 +28,7 @@ theorem Int.existsUnique_quotient_remainder (a b : ℤ) (h : 0 < b) :
   congr
   funext q
   rw [add_comm]
-  exact IsSymmOp.symm_op a (r + b * q)
+  exact propext eq_comm
 
 /-- The division algorithm. -/
 theorem Nat.existsUnique_quotient_remainder (a b : ℕ) (h : 0 < b) :
@@ -38,7 +38,7 @@ theorem Nat.existsUnique_quotient_remainder (a b : ℕ) (h : 0 < b) :
   congr
   funext q
   rw [add_comm]
-  exact IsSymmOp.symm_op a (r + b * q)
+  exact propext eq_comm
 
 /-- The division algorithm, weak form. -/
 theorem Int.exists_quotient_remainder (a b : ℤ) (h : 0 < b) :
diff --git a/Library/Theory/GCD.lean b/Library/Theory/GCD.lean
index d4600263..27b2d44c 100644
--- a/Library/Theory/GCD.lean
+++ b/Library/Theory/GCD.lean
@@ -9,8 +9,8 @@ open Int
   linarith
 
 @[decreasing] theorem lower_bound_fmod2 (a b : ℤ) (h1 : b < 0) : b < fmod a (-b) := by
-  have H : 0 ≤ fmod a (-b) 
-  · apply fmod_nonneg_of_pos
+  have H : 0 ≤ fmod a (-b) := by
+    apply fmod_nonneg_of_pos
     linarith
   linarith
 
@@ -29,7 +29,7 @@ def gcd (a b : ℤ) : ℤ :=
     a
   else
     -a
-termination_by _ a b => b
+termination_by b
 
 theorem gcd_nonneg (a b : ℤ) : 0 ≤ _root_.gcd a b := by
   rw [_root_.gcd]
@@ -38,7 +38,7 @@ theorem gcd_nonneg (a b : ℤ) : 0 ≤ _root_.gcd a b := by
   · apply gcd_nonneg
   · apply ha
   · linarith
-termination_by _ a b => b
+termination_by b
 
 mutual
 theorem gcd_dvd_right (a b : ℤ) : _root_.gcd a b ∣ b := by
@@ -50,7 +50,8 @@ theorem gcd_dvd_right (a b : ℤ) : _root_.gcd a b ∣ b := by
     linarith
   · use 0
     linarith
-    
+termination_by b
+
 theorem gcd_dvd_left (a b : ℤ) : _root_.gcd a b ∣ a := by
   rw [_root_.gcd]
   split_ifs with h1 h2
@@ -68,9 +69,9 @@ theorem gcd_dvd_left (a b : ℤ) : _root_.gcd a b ∣ a := by
     ring
   · use -1
     ring
+termination_by b
 
 end
-termination_by gcd_dvd_right a b => b ; gcd_dvd_left a b => b
 
 namespace Bezout
 mutual
@@ -79,11 +80,12 @@ def L (a b : ℤ) : ℤ :=
   if 0 < b then
     R b (fmod a b)
   else if b < 0 then
-    R b (fmod a (-b)) 
-  else if 0 ≤ a then 
+    R b (fmod a (-b))
+  else if 0 ≤ a then
     1
   else
     -1
+termination_by b
 
 def R (a b : ℤ) : ℤ :=
   if 0 < b then
@@ -92,9 +94,9 @@ def R (a b : ℤ) : ℤ :=
     L b (fmod a (-b)) + (fdiv a (-b)) * R b (fmod a (-b))
   else
     0
+termination_by b
 
 end
-termination_by L a b => b ; R a b => b
 
 theorem L_mul_add_R_mul (a b : ℤ) : L a b * a + R a b * b = _root_.gcd a b := by
   rw [R, L, _root_.gcd]
@@ -107,7 +109,7 @@ theorem L_mul_add_R_mul (a b : ℤ) : L a b * a + R a b * b = _root_.gcd a b :=
     linear_combination IH - R b (fmod a (-b)) * h
   · ring
   · ring
-termination_by L_mul_add_R_mul a b => b
+termination_by b
 
 end Bezout
 open Bezout
diff --git a/Library/Theory/NumberTheory.lean b/Library/Theory/NumberTheory.lean
index fbebe017..1f79b653 100644
--- a/Library/Theory/NumberTheory.lean
+++ b/Library/Theory/NumberTheory.lean
@@ -1,5 +1,6 @@
 /- Copyright (c) Heather Macbeth, 2023.  All rights reserved. -/
 import Library.Theory.Parity
+import Mathlib.Algebra.Order.Ring.Abs
 
 /-! # Assorted number theory lemmas from earlier needed in section 7.3 (square root of 2) -/
 
diff --git a/Library/Theory/Parity.lean b/Library/Theory/Parity.lean
index 355a2c5f..e3195d5f 100644
--- a/Library/Theory/Parity.lean
+++ b/Library/Theory/Parity.lean
@@ -8,7 +8,7 @@ def Int.Even (n : ℤ) : Prop :=
 def Int.Odd (n : ℤ) : Prop :=
   ∃ k, n = 2 * k + 1
 
-theorem Int.even_or_odd (n : ℤ) : Int.Even n ∨ Int.Odd n := by
+theorem Int.even_or_odd_lib (n : ℤ) : Int.Even n ∨ Int.Odd n := by
   obtain ⟨q, r, h, h', hn⟩ := n.exists_quotient_remainder 2 (by norm_num1)
   refine' exists_or.mp ⟨q, _⟩
   interval_cases r <;> simp [hn]
@@ -20,7 +20,7 @@ theorem Int.odd_iff_not_even (n : ℤ) : Odd n ↔ ¬ Even n := by
     have : ¬ ((2:ℤ) ∣ 1) := by decide
     contradiction
   · intro h
-    obtain h1 | h2 := Int.even_or_odd n
+    obtain h1 | h2 := Int.even_or_odd_lib n
     · contradiction   
     · apply h2
 
@@ -31,7 +31,7 @@ theorem Int.even_iff_not_odd (n : ℤ) : Even n ↔ ¬ Odd n := by
     have : ¬ ((2:ℤ) ∣ 1) := by decide
     contradiction
   · intro h
-    obtain h1 | h2 := Int.even_or_odd n
+    obtain h1 | h2 := Int.even_or_odd_lib n
     · apply h1
     · contradiction   
 
@@ -41,7 +41,7 @@ def Nat.Even (n : ℕ) : Prop :=
 def Nat.Odd (n : ℕ) : Prop :=
   ∃ k, n = 2 * k + 1
 
-theorem Nat.even_or_odd (n : ℕ) : Nat.Even n ∨ Nat.Odd n := by
+theorem Nat.even_or_odd_lib (n : ℕ) : Nat.Even n ∨ Nat.Odd n := by
   obtain ⟨q, r, h, hn⟩ := n.exists_quotient_remainder 2 (by norm_num1)
   refine' exists_or.mp ⟨q, _⟩
   interval_cases r <;> simp [hn]
@@ -54,7 +54,7 @@ theorem Nat.odd_iff_not_even (n : ℕ) : Odd n ↔ ¬ Even n := by
     have : ¬ ((2:ℤ) ∣ 1) := by decide
     contradiction
   · intro h
-    obtain h1 | h2 := Nat.even_or_odd n
+    obtain h1 | h2 := Nat.even_or_odd_lib n
     · contradiction   
     · apply h2
 
@@ -66,6 +66,6 @@ theorem Nat.even_iff_not_odd (n : ℕ) : Even n ↔ ¬ Odd n := by
     have : ¬ ((2:ℤ) ∣ 1) := by decide
     contradiction
   · intro h
-    obtain h1 | h2 := Nat.even_or_odd n
+    obtain h1 | h2 := Nat.even_or_odd_lib n
     · apply h1
     · contradiction   
diff --git a/Library/Theory/Prime.lean b/Library/Theory/Prime.lean
index b777f8eb..b6a7420b 100644
--- a/Library/Theory/Prime.lean
+++ b/Library/Theory/Prime.lean
@@ -19,12 +19,12 @@ theorem prime_test {p : ℕ} (hp : 2 ≤ p) (H : ∀ m : ℕ, 1 < m → m < p 
   have : ¬m ∣ p := H m hm_left hm_right
   contradiction
 
-lemma better_prime_test {p : ℕ} (hp : 2 ≤ p)  (T : ℕ) (hTp : p < T ^ 2) 
+lemma better_prime_test {p : ℕ} (hp : 2 ≤ p)  (T : ℕ) (hTp : p < T ^ 2)
     (H : ∀ (m : ℕ), 1 < m → m < T → ¬ (m ∣ p)) :
     Prime p := by
   apply prime_test hp
   intro m hm1 hmp
-  obtain hmT | hmT := lt_or_le m T
+  obtain hmT | hmT := lt_or_ge m T
   · exact H m hm1 hmT
   rintro ⟨l, hl⟩
   apply H l
@@ -62,7 +62,7 @@ theorem exists_factor_of_not_prime {p : ℕ} (hp : ¬ Prime p) (hp2 : 2 ≤ p) :
   exact H
 
 theorem exists_prime_factor {n : ℕ} (hn2 : 2 ≤ n) : ∃ p : ℕ, Prime p ∧ p ∣ n := by
-  by_cases hn : Prime n 
+  by_cases hn : Prime n
   . refine ⟨n, hn, 1, ?_⟩
     ring
   . obtain ⟨m, hmn, _, ⟨x, hx⟩⟩ := exists_factor_of_not_prime hn hn2
diff --git a/Math2001/03_Parity_and_Divisibility/01_Parity.lean b/Math2001/03_Parity_and_Divisibility/01_Parity.lean
index 74a36395..0a16b3b3 100644
--- a/Math2001/03_Parity_and_Divisibility/01_Parity.lean
+++ b/Math2001/03_Parity_and_Divisibility/01_Parity.lean
@@ -6,17 +6,17 @@ math2001_init
 open Int
 
 
-example : Odd (7 : ℤ) := by
-  dsimp [Odd]
+example : Int.Odd (7 : ℤ) := by
+  dsimp [Int.Odd]
   use 3
   numbers
 
 
-example : Odd (-3 : ℤ) := by
+example : Int.Odd (-3 : ℤ) := by
   sorry
 
-example {n : ℤ} (hn : Odd n) : Odd (3 * n + 2) := by
-  dsimp [Odd] at *
+example {n : ℤ} (hn : Int.Odd n) : Int.Odd (3 * n + 2) := by
+  dsimp [Int.Odd] at *
   obtain ⟨k, hk⟩ := hn
   use 3 * k + 2
   calc
@@ -24,10 +24,10 @@ example {n : ℤ} (hn : Odd n) : Odd (3 * n + 2) := by
     _ = 2 * (3 * k + 2) + 1 := by ring
 
 
-example {n : ℤ} (hn : Odd n) : Odd (7 * n - 4) := by
+example {n : ℤ} (hn : Int.Odd n) : Int.Odd (7 * n - 4) := by
   sorry
 
-example {x y : ℤ} (hx : Odd x) (hy : Odd y) : Odd (x + y + 1) := by
+example {x y : ℤ} (hx : Int.Odd x) (hy : Int.Odd y) : Int.Odd (x + y + 1) := by
   obtain ⟨a, ha⟩ := hx
   obtain ⟨b, hb⟩ := hy
   use a + b + 1
@@ -36,17 +36,17 @@ example {x y : ℤ} (hx : Odd x) (hy : Odd y) : Odd (x + y + 1) := by
     _ = 2 * (a + b + 1) + 1 := by ring
 
 
-example {x y : ℤ} (hx : Odd x) (hy : Odd y) : Odd (x * y + 2 * y) := by
+example {x y : ℤ} (hx : Int.Odd x) (hy : Int.Odd y) : Int.Odd (x * y + 2 * y) := by
   sorry
 
-example {m : ℤ} (hm : Odd m) : Even (3 * m - 5) := by
+example {m : ℤ} (hm : Int.Odd m) : Int.Even (3 * m - 5) := by
   sorry
 
-example {n : ℤ} (hn : Even n) : Odd (n ^ 2 + 2 * n - 5) := by
+example {n : ℤ} (hn : Int.Even n) : Int.Odd (n ^ 2 + 2 * n - 5) := by
   sorry
 
-example (n : ℤ) : Even (n ^ 2 + n + 4) := by
-  obtain hn | hn := Int.even_or_odd n
+example (n : ℤ) : Int.Even (n ^ 2 + n + 4) := by
+  obtain hn | hn := Int.even_or_odd_lib n
   · obtain ⟨x, hx⟩ := hn
     use 2 * x ^ 2 + x + 2
     calc
@@ -61,43 +61,43 @@ example (n : ℤ) : Even (n ^ 2 + n + 4) := by
 /-! # Exercises -/
 
 
-example : Odd (-9 : ℤ) := by
+example : Int.Odd (-9 : ℤ) := by
   sorry
 
-example : Even (26 : ℤ) := by
+example : Int.Even (26 : ℤ) := by
   sorry
 
-example {m n : ℤ} (hm : Odd m) (hn : Even n) : Odd (n + m) := by
+example {m n : ℤ} (hm : Int.Odd m) (hn : Int.Even n) : Int.Odd (n + m) := by
   sorry
 
-example {p q : ℤ} (hp : Odd p) (hq : Even q) : Odd (p - q - 4) := by
+example {p q : ℤ} (hp : Int.Odd p) (hq : Int.Even q) : Int.Odd (p - q - 4) := by
   sorry
 
-example {a b : ℤ} (ha : Even a) (hb : Odd b) : Even (3 * a + b - 3) := by
+example {a b : ℤ} (ha : Int.Even a) (hb : Int.Odd b) : Int.Even (3 * a + b - 3) := by
   sorry
 
-example {r s : ℤ} (hr : Odd r) (hs : Odd s) : Even (3 * r - 5 * s) := by
+example {r s : ℤ} (hr : Int.Odd r) (hs : Int.Odd s) : Int.Even (3 * r - 5 * s) := by
   sorry
 
-example {x : ℤ} (hx : Odd x) : Odd (x ^ 3) := by
+example {x : ℤ} (hx : Int.Odd x) : Int.Odd (x ^ 3) := by
   sorry
 
-example {n : ℤ} (hn : Odd n) : Even (n ^ 2 - 3 * n + 2) := by
+example {n : ℤ} (hn : Int.Odd n) : Int.Even (n ^ 2 - 3 * n + 2) := by
   sorry
 
-example {a : ℤ} (ha : Odd a) : Odd (a ^ 2 + 2 * a - 4) := by
+example {a : ℤ} (ha : Int.Odd a) : Int.Odd (a ^ 2 + 2 * a - 4) := by
   sorry
 
-example {p : ℤ} (hp : Odd p) : Odd (p ^ 2 + 3 * p - 5) := by
+example {p : ℤ} (hp : Int.Odd p) : Int.Odd (p ^ 2 + 3 * p - 5) := by
   sorry
 
-example {x y : ℤ} (hx : Odd x) (hy : Odd y) : Odd (x * y) := by
+example {x y : ℤ} (hx : Int.Odd x) (hy : Int.Odd y) : Int.Odd (x * y) := by
   sorry
 
-example (n : ℤ) : Odd (3 * n ^ 2 + 3 * n - 1) := by
+example (n : ℤ) : Int.Odd (3 * n ^ 2 + 3 * n - 1) := by
   sorry
 
-example (n : ℤ) : ∃ m ≥ n, Odd m := by
+example (n : ℤ) : ∃ m ≥ n, Int.Odd m := by
   sorry
-example (a b c : ℤ) : Even (a - b) ∨ Even (a + c) ∨ Even (b - c) := by
+example (a b c : ℤ) : Int.Even (a - b) ∨ Int.Even (a + c) ∨ Int.Even (b - c) := by
   sorry
diff --git a/Math2001/04_Proofs_with_Structure_II/04_Contradictory_Hypotheses.lean b/Math2001/04_Proofs_with_Structure_II/04_Contradictory_Hypotheses.lean
index 3286b076..abb9dc36 100644
--- a/Math2001/04_Proofs_with_Structure_II/04_Contradictory_Hypotheses.lean
+++ b/Math2001/04_Proofs_with_Structure_II/04_Contradictory_Hypotheses.lean
@@ -7,7 +7,7 @@ math2001_init
 
 
 example {y : ℝ} (x : ℝ) (h : 0 < x * y) (hx : 0 ≤ x) : 0 < y := by
-  obtain hneg | hpos : y ≤ 0 ∨ 0 < y := le_or_lt y 0
+  obtain hneg | hpos : y ≤ 0 ∨ 0 < y := le_or_gt y 0
   · -- the case `y ≤ 0`
     have : ¬0 < x * y
     · apply not_lt_of_ge
diff --git a/Math2001/04_Proofs_with_Structure_II/05_Proof_by_Contradiction.lean b/Math2001/04_Proofs_with_Structure_II/05_Proof_by_Contradiction.lean
index 33ae1eba..ddba79af 100644
--- a/Math2001/04_Proofs_with_Structure_II/05_Proof_by_Contradiction.lean
+++ b/Math2001/04_Proofs_with_Structure_II/05_Proof_by_Contradiction.lean
@@ -11,7 +11,7 @@ open Int
 
 example : ¬ (∀ x : ℝ, x ^ 2 ≥ x) := by
   intro h
-  have : 0.5 ^ 2 ≥ 0.5 := h 0.5
+  have : (0.5 : ℝ) ^ 2 ≥ 0.5 := h 0.5
   numbers at this
 
 
@@ -47,7 +47,7 @@ example (n : ℤ) : Int.Even n ↔ ¬ Int.Odd n := by
       _ ≡ 1 [ZMOD 2] := by rel [h2]
     numbers at h -- contradiction!
   · intro h
-    obtain h1 | h2 := Int.even_or_odd n
+    obtain h1 | h2 := Int.even_or_odd_lib n
     · apply h1
     · contradiction
 
@@ -98,7 +98,7 @@ example {p : ℕ} (hp : 2 ≤ p)  (T : ℕ) (hTp : p < T ^ 2)
     Prime p := by
   apply prime_test hp
   intro m hm1 hmp
-  obtain hmT | hmT := lt_or_le m T
+  obtain hmT | hmT := lt_or_ge m T
   · apply H m hm1 hmT
   intro h_div
   obtain ⟨l, hl⟩ := h_div
diff --git a/Math2001/05_Logic/03_Negation_Algorithm.lean b/Math2001/05_Logic/03_Negation_Algorithm.lean
index b8c2a75e..833e48f5 100644
--- a/Math2001/05_Logic/03_Negation_Algorithm.lean
+++ b/Math2001/05_Logic/03_Negation_Algorithm.lean
@@ -26,7 +26,7 @@ example :
     ¬(∀ m : ℤ, m ≠ 2 → ∃ n : ℤ, n ^ 2 = m) ↔ ∃ m : ℤ, m ≠ 2 ∧ ∀ n : ℤ, n ^ 2 ≠ m :=
   calc ¬(∀ m : ℤ, m ≠ 2 → ∃ n : ℤ, n ^ 2 = m)
       ↔ ∃ m : ℤ, ¬(m ≠ 2 → ∃ n : ℤ, n ^ 2 = m) := by rel [not_forall]
-    _ ↔ ∃ m : ℤ, m ≠ 2 ∧ ¬(∃ n : ℤ, n ^ 2 = m) := by rel [not_imp]
+    _ ↔ ∃ m : ℤ, m ≠ 2 ∧ ¬(∃ n : ℤ, n ^ 2 = m) := by rel [_root_.not_imp]
     _ ↔ ∃ m : ℤ, m ≠ 2 ∧ ∀ n : ℤ, n ^ 2 ≠ m := by rel [not_exists]
 
 
diff --git a/Math2001/06_Induction/01_Induction.lean b/Math2001/06_Induction/01_Induction.lean
index 9e95d435..f20718ce 100644
--- a/Math2001/06_Induction/01_Induction.lean
+++ b/Math2001/06_Induction/01_Induction.lean
@@ -51,8 +51,6 @@ example (n : ℕ) : 4 ^ n ≡ 1 [ZMOD 15] ∨ 4 ^ n ≡ 4 [ZMOD 15] := by
 
 example {n : ℕ} (hn : 2 ≤ n) : (3:ℤ) ^ n ≥ 2 ^ n + 5 := by
   induction_from_starting_point n, hn with k hk IH
-  · -- base case
-    numbers
   · -- inductive step
     calc (3:ℤ) ^ (k + 1) = 2 * 3 ^ k + 3 ^ k := by ring
       _ ≥ 2 * (2 ^ k + 5) + 3 ^ k := by rel [IH]
@@ -105,5 +103,5 @@ example : forall_sufficiently_large n : ℕ, 2 ^ n ≥ n ^ 3 := by
 theorem Odd.pow {a : ℕ} (ha : Odd a) (n : ℕ) : Odd (a ^ n) := by
   sorry
 
-theorem Nat.even_of_pow_even {a n : ℕ} (ha : Even (a ^ n)) : Even a := by
+theorem even_of_pow_even {a n : ℕ} (ha : Even (a ^ n)) : Even a := by
   sorry
diff --git a/Math2001/06_Induction/05_Pascal.lean b/Math2001/06_Induction/05_Pascal.lean
index 707a7b68..c3d1e382 100644
--- a/Math2001/06_Induction/05_Pascal.lean
+++ b/Math2001/06_Induction/05_Pascal.lean
@@ -12,7 +12,7 @@ def pascal : ℕ → ℕ → ℕ
   | a, 0 => 1
   | 0, b + 1 => 1
   | a + 1, b + 1 => pascal (a + 1) b + pascal a (b + 1)
-termination_by _ a b => a + b
+termination_by a b => a + b
 
 
 #eval pascal 2 4 -- infoview displays `15`
@@ -35,7 +35,7 @@ theorem pascal_le (a b : ℕ) : pascal a b ≤ (a + b)! := by
         _ = ((a + b + 1) + 1) * (a + b + 1)! := by ring
         _ = ((a + b + 1) + 1)! := by rw [factorial, factorial, factorial]
         _ = (a + 1 + (b + 1))! := by ring
-termination_by _ a b => a + b
+termination_by a + b
 
 
 theorem pascal_eq (a b : ℕ) : pascal a b * a ! * b ! = (a + b)! := by
@@ -65,7 +65,7 @@ theorem pascal_eq (a b : ℕ) : pascal a b * a ! * b ! = (a + b)! := by
       _ = ((1 + a + b) + 1) * (1 + a + b) ! := by ring
       _ = ((1 + a + b) + 1) ! := by rw [factorial]
       _ = ((a + 1) + (b + 1)) ! := by ring
-termination_by _ a b => a + b
+termination_by a + b
 
 
 example (a b : ℕ) : (pascal a b : ℚ) = (a + b)! / (a ! * b !) := by
@@ -85,7 +85,6 @@ theorem pascal_symm (m n : ℕ) : pascal m n = pascal n m := by
   | a + 1, 0 => sorry
   | 0, b + 1 => sorry
   | a + 1, b + 1 => sorry
-termination_by _ a b => a + b
 
 
 example (a : ℕ) : pascal a 1 = a + 1 := by
diff --git a/Math2001/06_Induction/06_Division_Algorithm.lean b/Math2001/06_Induction/06_Division_Algorithm.lean
index 2faf83e5..5444279d 100644
--- a/Math2001/06_Induction/06_Division_Algorithm.lean
+++ b/Math2001/06_Induction/06_Division_Algorithm.lean
@@ -14,7 +14,17 @@ def fmod (n d : ℤ) : ℤ :=
     0
   else
     n
-termination_by _ n d => 2 * n - d
+termination_by 2 * n - d
+decreasing_by
+  all_goals simp_wf
+  · rw [Int.sizeOf_lt_sizeOf_iff, abs_lt_abs_iff]
+    rcases mul_neg_iff.mp ‹n * d < 0› with ⟨hn, hd⟩ | ⟨hn, hd⟩
+    · left; constructor <;> omega
+    · right; constructor <;> omega
+  · rw [Int.sizeOf_lt_sizeOf_iff, abs_lt_abs_iff]
+    rcases mul_pos_iff.mp ‹(0 : ℤ) < d * (n - d)› with ⟨hd, hn⟩ | ⟨hd, hn⟩
+    · left; constructor <;> omega
+    · right; constructor <;> omega
 
 def fdiv (n d : ℤ) : ℤ :=
   if n * d < 0 then
@@ -25,7 +35,17 @@ def fdiv (n d : ℤ) : ℤ :=
     1
   else
     0
-termination_by _ n d => 2 * n - d
+termination_by 2 * n - d
+decreasing_by
+  all_goals simp_wf
+  · rw [Int.sizeOf_lt_sizeOf_iff, abs_lt_abs_iff]
+    rcases mul_neg_iff.mp ‹n * d < 0› with ⟨hn, hd⟩ | ⟨hn, hd⟩
+    · left; constructor <;> omega
+    · right; constructor <;> omega
+  · rw [Int.sizeOf_lt_sizeOf_iff, abs_lt_abs_iff]
+    rcases mul_pos_iff.mp ‹(0 : ℤ) < d * (n - d)› with ⟨hd, hn⟩ | ⟨hd, hn⟩
+    · left; constructor <;> omega
+    · right; constructor <;> omega
 
 
 #eval fmod 11 4 -- infoview displays `3`
@@ -51,8 +71,17 @@ theorem fmod_add_fdiv (n d : ℤ) : fmod n d + d * fdiv n d = n := by
       _ = n := by rw [h3]
   · -- last case
     ring
-termination_by _ n d => 2 * n - d
-
+termination_by 2 * n - d
+decreasing_by
+  all_goals simp_wf
+  · rw [Int.sizeOf_lt_sizeOf_iff, abs_lt_abs_iff]
+    rcases mul_neg_iff.mp ‹n * d < 0› with ⟨hn, hd'⟩ | ⟨hn, hd'⟩
+    · left; constructor <;> omega
+    · right; constructor <;> omega
+  · rw [Int.sizeOf_lt_sizeOf_iff, abs_lt_abs_iff]
+    rcases mul_pos_iff.mp ‹(0 : ℤ) < d * (n - d)› with ⟨hd', hn⟩ | ⟨hd', hn⟩
+    · left; constructor <;> omega
+    · right; constructor <;> omega
 
 
 theorem fmod_nonneg_of_pos (n : ℤ) {d : ℤ} (hd : 0 < d) : 0 ≤ fmod n d := by
@@ -68,7 +97,17 @@ theorem fmod_nonneg_of_pos (n : ℤ) {d : ℤ} (hd : 0 < d) : 0 ≤ fmod n d :=
     extra
   · -- last case
     cancel d at h1
-termination_by _ n d hd => 2 * n - d
+termination_by 2 * n - d
+decreasing_by
+  all_goals simp_wf
+  · rw [Int.sizeOf_lt_sizeOf_iff, abs_lt_abs_iff]
+    rcases mul_neg_iff.mp ‹n * d < 0› with ⟨hn, hd'⟩ | ⟨hn, hd'⟩
+    · left; constructor <;> omega
+    · right; constructor <;> omega
+  · rw [Int.sizeOf_lt_sizeOf_iff, abs_lt_abs_iff]
+    rcases mul_pos_iff.mp ‹(0 : ℤ) < d * (n - d)› with ⟨hd', hn⟩ | ⟨hd', hn⟩
+    · left; constructor <;> omega
+    · right; constructor <;> omega
 
 
 theorem fmod_lt_of_pos (n : ℤ) {d : ℤ} (hd : 0 < d) : fmod n d < d := by
@@ -90,7 +129,17 @@ theorem fmod_lt_of_pos (n : ℤ) {d : ℤ} (hd : 0 < d) : fmod n d < d := by
     apply lt_of_le_of_ne
     · addarith [h4]
     · apply h3
-termination_by _ n d hd => 2 * n - d
+termination_by 2 * n - d
+decreasing_by
+  all_goals simp_wf
+  · rw [Int.sizeOf_lt_sizeOf_iff, abs_lt_abs_iff]
+    rcases mul_neg_iff.mp ‹n * d < 0› with ⟨hn, hd'⟩ | ⟨hn, hd'⟩
+    · left; constructor <;> omega
+    · right; constructor <;> omega
+  · rw [Int.sizeOf_lt_sizeOf_iff, abs_lt_abs_iff]
+    rcases mul_pos_iff.mp ‹(0 : ℤ) < d * (n - d)› with ⟨hd', hn⟩ | ⟨hd', hn⟩
+    · left; constructor <;> omega
+    · right; constructor <;> omega
 
 
 example (a b : ℤ) (h : 0 < b) : ∃ r : ℤ, 0 ≤ r ∧ r < b ∧ a ≡ r [ZMOD b] := by
@@ -116,7 +165,9 @@ def T (n : ℤ) : ℤ :=
     T (-n)
   else
     0
-termination_by T n => 3 * n - 1
+termination_by 3 * n - 1
+decreasing_by
+  all_goals (simp_wf; rw [Int.sizeOf_lt_sizeOf_iff, abs_lt_abs_iff]; omega)
 
 theorem T_eq (n : ℤ) : T n = n ^ 2 := by
   sorry
diff --git a/Math2001/06_Induction/07_Euclidean_Algorithm.lean b/Math2001/06_Induction/07_Euclidean_Algorithm.lean
index f08e55a1..c348a462 100644
--- a/Math2001/06_Induction/07_Euclidean_Algorithm.lean
+++ b/Math2001/06_Induction/07_Euclidean_Algorithm.lean
@@ -8,15 +8,15 @@ open Int
 
 
 @[decreasing] theorem lower_bound_fmod1 (a b : ℤ) (h1 : 0 < b) : -b < fmod a b := by
-  have H : 0 ≤ fmod a b
-  · apply fmod_nonneg_of_pos
+  have H : 0 ≤ fmod a b := by
+    apply fmod_nonneg_of_pos
     apply h1
   calc -b < 0 := by addarith [h1]
     _ ≤ _ := H
 
 @[decreasing] theorem lower_bound_fmod2 (a b : ℤ) (h1 : b < 0) : b < fmod a (-b) := by
-  have H : 0 ≤ fmod a (-b)
-  · apply fmod_nonneg_of_pos
+  have H : 0 ≤ fmod a (-b) := by
+    apply fmod_nonneg_of_pos
     addarith [h1]
   have h2 : 0 < -b := by addarith [h1]
   calc b < 0 := h1
@@ -39,7 +39,7 @@ def gcd (a b : ℤ) : ℤ :=
     a
   else
     -a
-termination_by _ a b => b
+termination_by b
 
 
 #eval gcd (-21) 15 -- infoview displays `3`
@@ -58,7 +58,7 @@ theorem gcd_nonneg (a b : ℤ) : 0 ≤ gcd a b := by
     apply ha
   · -- case `b = 0`, `a < 0`
     addarith [ha]
-termination_by _ a b => b
+termination_by b
 
 
 theorem gcd_dvd (a b : ℤ) : gcd a b ∣ b ∧ gcd a b ∣ a := by
@@ -92,7 +92,7 @@ theorem gcd_dvd (a b : ℤ) : gcd a b ∣ b ∧ gcd a b ∣ a := by
       sorry
     · -- prove that `gcd a b ∣ a`
       sorry
-termination_by gcd_dvd a b => b
+termination_by b
 
 
 mutual
@@ -113,6 +113,7 @@ theorem gcd_dvd_right (a b : ℤ) : gcd a b ∣ b := by
     use 0
     calc b = 0 := hb
       _ = -a * 0 := by ring
+termination_by b
 
 theorem gcd_dvd_left (a b : ℤ) : gcd a b ∣ a := by
   rw [gcd]
@@ -147,9 +148,9 @@ theorem gcd_dvd_left (a b : ℤ) : gcd a b ∣ a := by
   · -- case `b = 0`, `a < 0`
     use -1
     ring
+termination_by b
 
 end
-termination_by gcd_dvd_right a b => b ; gcd_dvd_left a b => b
 
 
 mutual
@@ -163,6 +164,7 @@ def L (a b : ℤ) : ℤ :=
     1
   else
     -1
+termination_by b
 
 def R (a b : ℤ) : ℤ :=
   if 0 < b then
@@ -171,9 +173,9 @@ def R (a b : ℤ) : ℤ :=
     L b (fmod a (-b)) + (fdiv a (-b)) * R b (fmod a (-b))
   else
     0
+termination_by b
 
 end
-termination_by L a b => b ; R a b => b
 
 
 #eval L (-21) 15 -- infoview displays `2`
@@ -205,7 +207,7 @@ theorem L_mul_add_R_mul (a b : ℤ) : L a b * a + R a b * b = gcd a b := by
     ring
   · -- case `b = 0`, `a < 0`
     ring
-termination_by L_mul_add_R_mul a b => b
+termination_by b
 
 
 #eval L 7 5 -- infoview displays `-2`
diff --git a/Math2001/07_Number_Theory/01_Infinitely_Many_Primes.lean b/Math2001/07_Number_Theory/01_Infinitely_Many_Primes.lean
index a9121f5c..3c799bbd 100644
--- a/Math2001/07_Number_Theory/01_Infinitely_Many_Primes.lean
+++ b/Math2001/07_Number_Theory/01_Infinitely_Many_Primes.lean
@@ -38,7 +38,7 @@ example (N : ℕ) : ∃ p ≥ N, Prime p := by
     -- so `p` is a prime number greater than or equal to `N`, as we sought
     use p
     constructor
-    · obtain h_le | h_gt : p ≤ N ∨ N < p := le_or_lt p N
+    · obtain h_le | h_gt : p ≤ N ∨ N < p := le_or_gt p N
       · have : p ∣ (N !)
         · apply dvd_factorial
           · extra
diff --git a/Math2001/07_Number_Theory/03_Sqrt_Two.lean b/Math2001/07_Number_Theory/03_Sqrt_Two.lean
index 16cc794c..e2f9f4d0 100644
--- a/Math2001/07_Number_Theory/03_Sqrt_Two.lean
+++ b/Math2001/07_Number_Theory/03_Sqrt_Two.lean
@@ -37,7 +37,7 @@ theorem irrat_aux (a b : ℕ) (hb : b ≠ 0) : a ^ 2 ≠ 2 * b ^ 2 := by
   have IH := irrat_aux b k -- inductive hypothesis
   have : b ^ 2 ≠ 2 * k ^ 2 := IH hk''
   contradiction
-termination_by _ => b
+termination_by b
 
 
 example : ¬ ∃ a b : ℕ, b ≠ 0 ∧ a ^ 2 = 2 * b ^ 2 := by
diff --git a/Math2001/08_Functions/04_Product_Types.lean b/Math2001/08_Functions/04_Product_Types.lean
index 9d3b04c7..e0ba881c 100644
--- a/Math2001/08_Functions/04_Product_Types.lean
+++ b/Math2001/08_Functions/04_Product_Types.lean
@@ -142,7 +142,7 @@ theorem A_mono {n m : ℕ} (h : n ≤ m) : A n ≤ A m := by
 
 theorem of_A_add_mono {a1 a2 b1 b2 : ℕ} (h : A (a1 + b1) + b1 ≤ A (a2 + b2) + b2) :
     a1 + b1 ≤ a2 + b2 := by
-  obtain h' | h' : _ ∨ a2 + b2 + 1 ≤ a1 + b1 := le_or_lt (a1 + b1) (a2 + b2)
+  obtain h' | h' : _ ∨ a2 + b2 + 1 ≤ a1 + b1 := le_or_gt (a1 + b1) (a2 + b2)
   · apply h'
   rw [← not_lt] at h
   have :=
@@ -174,7 +174,7 @@ theorem p_comp_i (x : ℕ × ℕ) : p (i x) = p x + 1 := by
       _ = (A (0 + b) + b) + 1 := by ring
       _ = p (0, b) + 1 := by dsimp [p]
   | (a + 1, b) =>
-    calc p (i (a + 1, b)) = p (a, b + 1) := by rw [i] ; rfl -- FIXME
+    calc p (i (a + 1, b)) = p (a, b + 1) := by rw [i]
       _ = A (a + (b + 1)) + (b + 1) := by dsimp [p]
       _ = (A ((a + 1) + b) + b) + 1 := by ring
       _ = p (a + 1, b) + 1 := by rw [p]
diff --git a/Math2001/09_Sets/02_Set_Operations.lean b/Math2001/09_Sets/02_Set_Operations.lean
index 6c19949b..ec58c58a 100644
--- a/Math2001/09_Sets/02_Set_Operations.lean
+++ b/Math2001/09_Sets/02_Set_Operations.lean
@@ -13,7 +13,7 @@ open Set
 
 example (t : ℝ) : t ∈ {x : ℝ | -1 < x} ∪ {x : ℝ | x < 1} := by
   dsimp
-  obtain h | h := le_or_lt t 0
+  obtain h | h := le_or_gt t 0
   · right
     addarith [h]
   · left
@@ -69,7 +69,7 @@ example : {n : ℤ | Even n}ᶜ = {n : ℤ | Odd n} := by
 end Int
 
 
-example (x : ℤ) : x ∉ ∅ := by
+example (x : ℤ) : x ∉ (∅ : Set ℤ) := by
   dsimp
   exhaust
 
@@ -117,7 +117,7 @@ example : {x : ℝ | -1 < x} ∪ {x : ℝ | x < 1} = univ := by
   ext t
   dsimp
   suffices -1 < t ∨ t < 1 by exhaust
-  obtain h | h := le_or_lt t 0
+  obtain h | h := le_or_gt t 0
   · right
     addarith [h]
   · left
diff --git a/Math2001/Homework/hw3.lean b/Math2001/Homework/hw3.lean
index dfebf408..752ee554 100644
--- a/Math2001/Homework/hw3.lean
+++ b/Math2001/Homework/hw3.lean
@@ -29,9 +29,9 @@ theorem problem4 (x : ℚ) : ∃ y : ℚ, y ^ 2 > x := by
   sorry
 
 @[autograded 5]
-theorem problem5 {x : ℕ} (hx : Odd x) : Odd (x ^ 3) := by
+theorem problem5 {x : ℕ} (hx : Int.Odd x) : Int.Odd (x ^ 3) := by
   sorry
 
 @[autograded 5]
-theorem problem6 (n : ℕ) : ∃ m ≥ n, Odd m := by
+theorem problem6 (n : ℕ) : ∃ m ≥ n, Int.Odd m := by
   sorry
diff --git a/Math2001/Homework/hw4.lean b/Math2001/Homework/hw4.lean
index 075a9c64..281aec5d 100644
--- a/Math2001/Homework/hw4.lean
+++ b/Math2001/Homework/hw4.lean
@@ -14,7 +14,7 @@ https://github.com/hrmacbeth/math2001/wiki/Homework-4,
 for clearer statements and any special instructions. -/
 
 @[autograded 5]
-theorem problem1 (n : ℤ) : Odd (3 * n ^ 2 + 3 * n - 1) := by
+theorem problem1 (n : ℤ) : Int.Odd (3 * n ^ 2 + 3 * n - 1) := by
   sorry
 
 @[autograded 1]
diff --git a/lake-manifest.json b/lake-manifest.json
index 74b679de..2790e6c3 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -1,77 +1,125 @@
-{"version": 7,
+{"version": "1.1.0",
  "packagesDir": ".lake/packages",
  "packages":
- [{"url": "https://github.com/leanprover/std4",
+ [{"url": "https://github.com/robertylewis/lean4-autograder-main",
    "type": "git",
    "subDir": null,
-   "rev": "2e4a3586a8f16713f16b2d2b3af3d8e65f3af087",
-   "name": "std",
+   "scope": "",
+   "rev": "864b34ce06d8536aec0c38e57448c17d1f83572a",
+   "name": "autograder",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
-   "inherited": true,
+   "inputRev": "864b34ce06d8536aec0c38e57448c17d1f83572a",
+   "inherited": false,
    "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover-community/quote4",
+  {"url": "https://github.com/leanprover-community/duper",
    "type": "git",
    "subDir": null,
-   "rev": "d3a1d25f3eba0d93a58d5d3d027ffa78ece07755",
-   "name": "Qq",
+   "scope": "",
+   "rev": "33ba47275382683247ef0c5c2cc1174a6d23e3b3",
+   "name": "Duper",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "master",
-   "inherited": true,
+   "inputRev": "v4.22.0",
+   "inherited": false,
    "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover-community/aesop",
+  {"url": "https://github.com/leanprover-community/mathlib4",
    "type": "git",
    "subDir": null,
-   "rev": "c7cff4551258d31c0d2d453b3f9cbca757d445f1",
-   "name": "aesop",
+   "scope": "",
+   "rev": "79e94a093aff4a60fb1b1f92d9681e407124c2ca",
+   "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "master",
-   "inherited": true,
+   "inputRev": "v4.22.0",
+   "inherited": false,
    "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover-community/ProofWidgets4",
+  {"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
-   "rev": "909febc72b4f64628f8d35cd0554f8a90b6e0749",
-   "name": "proofwidgets",
+   "scope": "",
+   "rev": "240676e9568c254a69be94801889d4b13f3b249f",
+   "name": "batteries",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.23",
+   "inputRev": "v4.22.0",
    "inherited": true,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover/lean4-cli",
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/lean-auto.git",
    "type": "git",
    "subDir": null,
-   "rev": "a751d21d4b68c999accb6fc5d960538af26ad5ec",
-   "name": "Cli",
+   "scope": "",
+   "rev": "531948548693fc867b2187635742083984f08818",
+   "name": "auto",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "531948548693fc867b2187635742083984f08818",
    "inherited": true,
    "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover-community/mathlib4",
+  {"url": "https://github.com/leanprover-community/plausible",
    "type": "git",
    "subDir": null,
-   "rev": "f04afed5ac9fea0e1355bc6f6bee2bd01f4a888d",
-   "name": "mathlib",
+   "scope": "leanprover-community",
+   "rev": "b100ad4c5d74a464f497aaa8e7c74d86bf39a56f",
+   "name": "plausible",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.3.0",
-   "inherited": false,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/hrmacbeth/duper",
+   "inputRev": "v4.22.0",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/LeanSearchClient",
    "type": "git",
    "subDir": null,
-   "rev": "500aecaa3bbe6818f82611c84ac4dfff64ad5b3f",
-   "name": "Duper",
+   "scope": "leanprover-community",
+   "rev": "99657ad92e23804e279f77ea6dbdeebaa1317b98",
+   "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
-   "inherited": false,
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/import-graph",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "eb164a46de87078f27640ee71e6c3841defc2484",
+   "name": "importGraph",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v4.22.0",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/ProofWidgets4",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "1253a071e6939b0faf5c09d2b30b0bfc79dae407",
+   "name": "proofwidgets",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v0.0.68",
+   "inherited": true,
    "configFile": "lakefile.lean"},
-  {"url": "https://github.com/robertylewis/lean4-autograder-main",
+  {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
-   "rev": "864b34ce06d8536aec0c38e57448c17d1f83572a",
-   "name": "autograder",
+   "scope": "leanprover-community",
+   "rev": "1256a18522728c2eeed6109b02dd2b8f207a2a3c",
+   "name": "aesop",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "864b34ce06d8536aec0c38e57448c17d1f83572a",
-   "inherited": false,
-   "configFile": "lakefile.lean"}],
+   "inputRev": "v4.22.0",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/quote4",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "917bfa5064b812b7fbd7112d018ea0b4def25ab3",
+   "name": "Qq",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v4.22.0",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover/lean4-cli",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover",
+   "rev": "c682c91d2d4dd59a7187e2ab977ac25bd1f87329",
+   "name": "Cli",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"}],
  "name": "math2001",
  "lakeDir": ".lake"}
diff --git a/lakefile.lean b/lakefile.lean
index 3cf801e4..7746fa91 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -28,5 +28,6 @@ but currently only Lean core options can be set in lakefile
 -/
 
 require mathlib from git "https://github.com/leanprover-community/mathlib4" @ s!"v{Lean.versionString}"
-require Duper from git "https://github.com/hrmacbeth/duper" @ "main"
+require Duper from git "https://github.com/leanprover-community/duper" @ s!"v{Lean.versionString}"
+
 require autograder from git "https://github.com/robertylewis/lean4-autograder-main" @ "864b34ce06d8536aec0c38e57448c17d1f83572a"
diff --git a/lean-toolchain b/lean-toolchain
index 5cadc9da..6ac6d4c4 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.3.0
+leanprover/lean4:v4.22.0