From 413d6a860a416d402d698520be11c2e1ea52f329 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Tue, 3 Sep 2024 14:23:43 +1000
Subject: [PATCH 1/2] chore: bump toolchain to v4.12.0-rc1

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

diff --git a/lean-toolchain b/lean-toolchain
index 5a9c76d..98556ba 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.11.0
+leanprover/lean4:v4.12.0-rc1

From fd25302e2221abd7ec7bbebc0960a834ac1edb5b Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Tue, 3 Sep 2024 14:30:20 +1000
Subject: [PATCH 2/2] fix tests

---
 ProofWidgets/Demos/Euclidean.lean | 4 ++--
 ProofWidgets/Demos/Venn.lean      | 8 ++++----
 2 files changed, 6 insertions(+), 6 deletions(-)

diff --git a/ProofWidgets/Demos/Euclidean.lean b/ProofWidgets/Demos/Euclidean.lean
index 00277ff..4f13b42 100644
--- a/ProofWidgets/Demos/Euclidean.lean
+++ b/ProofWidgets/Demos/Euclidean.lean
@@ -149,7 +149,7 @@ def EuclideanDisplay.rpc (props : PanelWidgetProps) : RequestM (RequestTask Html
         Meta.withLCtx lctx md.localInstances do
           -- Which hypotheses have been selected in the UI,
           -- meaning they should *not* be shown in the display.
-          let mut hiddenLocs : HashSet FVarId := mkHashSet props.selectedLocations.size
+          let mut hiddenLocs : Std.HashSet FVarId := .empty props.selectedLocations.size
           for l in props.selectedLocations do
             match l with
             | ⟨mv, .hyp fv⟩ | ⟨mv, .hypType fv _⟩ =>
@@ -311,7 +311,7 @@ show_panel_widgets [local EuclideanConstructions]
 
 -- Try constructing an equilateral triangle abc
 -- with line segment ab as the base.
-example {a b : Point} (hab : a ≠ b) :
+example {a b : Point} (_hab : a ≠ b) :
     ∃ L M c, onLine a L ∧ onLine b M ∧ onLine c M ∧ onLine c L := by
   -- Place your cursor below.
   -- Shift-click hypotheses in 'Tactic state' to select them.
diff --git a/ProofWidgets/Demos/Venn.lean b/ProofWidgets/Demos/Venn.lean
index 6f940e3..425107d 100644
--- a/ProofWidgets/Demos/Venn.lean
+++ b/ProofWidgets/Demos/Venn.lean
@@ -14,7 +14,7 @@ def Set (α : Type u) := α → Prop
 namespace Set
 
 /-- Membership in a set -/
-protected def Mem (a : α) (s : Set α) : Prop :=
+protected def Mem (s : Set α) (a : α) : Prop :=
   s a
 
 instance : Membership α (Set α) :=
@@ -58,14 +58,14 @@ def mkSetDiag (sub : String) (embeds : ExprEmbeds) : MetaM Html := do
 
 def isSetGoal? (hyps : Array LocalDecl) : MetaM (Option Html) := do
   let mut sub := "AutoLabel All\n"
-  let mut sets : HashMap String Expr := .empty
+  let mut sets : Std.HashMap String Expr := .empty
   for assm in hyps do
     let tp ← instantiateMVars assm.type
     if let some (S, T) := isSubsetPred? tp then
       let sS ← toString <$> Lean.Meta.ppExpr S
       let sT ← toString <$> Lean.Meta.ppExpr T
-      let (sets', cS) := sets.insert' sS S
-      let (sets', cT) := sets'.insert' sT T
+      let (cS, sets') := sets.containsThenInsert sS S
+      let (cT, sets') := sets'.containsThenInsert sT T
       sets := sets'
       if !cS then
         sub := sub ++ s!"Set {sS}\n"