diff --git a/tests/lean/run/add_suggestion.lean b/tests/lean/run/add_suggestion.lean
new file mode 100644
index 0000000000..c86c6a4c95
--- /dev/null
+++ b/tests/lean/run/add_suggestion.lean
@@ -0,0 +1,45 @@
+import Lean.Meta.Tactic.TryThis
+
+set_option linter.unusedVariables false
+set_option linter.missingDocs false
+
+section width
+-- here we test that the width of try this suggestions is not too big
+
+-- simulate a long and complicated term
+def longdef (a b : Nat) (h h h h h h h h h h h h h h h h h
+    h h h h h h h h h h h h h h h h h h h h h h h h h h h h h h h h h
+    h h h h h h h h h h h h h h h h h h h h h h h
+    h h h h h h h h h h h h h h h h h h h h h : a = b) :
+  2 * a = 2 * b := by rw [h]
+
+namespace Lean.Meta.Tactic.TryThis
+open Lean Elab Tactic
+
+set_option hygiene false in
+elab "test" : tactic => do
+  addSuggestion (← getRef) (←
+  `(tactic| exact longdef a b h h h h h h h h h h h h h h
+      h h h h h h h h h h h h h h h h h h h h h h
+      h h h h h h h h h h h h h h h h h h h h h h
+      h h h h h h h h h h h h h h h h h h h h h h h h h h h h h h h h h h h h))
+
+end Lean.Meta.Tactic.TryThis
+
+#guard_msgs (drop info, drop warning) in
+-- ideally we would have a #guard_widgets or #guard_infos too, but instead we can simply check by
+-- hand that the widget suggestion (not the message) fits into 100 columns
+theorem asda (a b : Nat) (h : a = b) : 2 * a = 2 * b := by
+  test
+--exact
+--  longdef a b h h h h h h h h h h h h h h h h h h h h h h h h h h h h h h h h h h h h h h h h h h
+--    h h h h h h h h h h h h h h h h h h h h h h h h h h h h h h h h h h h h h h h h h h h h h h h
+--    h h h h h
+  have : 2 * a = 2 * b := by
+    test
+--  exact
+--    longdef a b h h h h h h h h h h h h h h h h h h h h h h h h h h h h h h h h h h h h h h h h h
+--      h h h h h h h h h h h h h h h h h h h h h h h h h h h h h h h h h h h h h h h h h h h h h h
+--      h h h h h h h
+    sorry
+  sorry
diff --git a/tests/lean/run/bitvec.lean b/tests/lean/run/bitvec.lean
new file mode 100644
index 0000000000..edb5dbf18c
--- /dev/null
+++ b/tests/lean/run/bitvec.lean
@@ -0,0 +1,116 @@
+open BitVec
+
+-- Basic arithmetic
+#guard 1#12 + 2#12 = 3#12
+#guard 3#5 * 7#5 = 0x15#5
+#guard 3#4 * 7#4 = 0x05#4
+
+#guard zeroExtend  4 0x7f#8 = 0xf#4
+#guard zeroExtend 12 0x7f#8 = 0x07f#12
+#guard zeroExtend 12 0x80#8 = 0x080#12
+#guard zeroExtend 16 0xff#8 = 0x00ff#16
+
+#guard signExtend  4 0x7f#8 = 0xf#4
+#guard signExtend 12 0x7f#8 = 0x07f#12
+#guard signExtend 12 0x80#8 = 0xf80#12
+#guard signExtend 16 0xff#8 = 0xffff#16
+
+-- Division and mod/rem
+
+#guard 3#4 / 0 = 0
+#guard 10#4 / 2 = 5
+
+#guard 8#4 % 0 = 8
+#guard 4#4 % 1 = 0
+#guard 4#4 % 3 = 1
+#guard 0xf#4 % (-2) = 1
+#guard 0xf#4 % (-8) = 7
+
+#guard sdiv 6#4 2 = 3#4
+#guard sdiv 7#4 2 = 3#4
+#guard sdiv 6#4 (-2) = -3#4
+#guard sdiv 7#4 (-2) = -3#4
+#guard sdiv (-6#4) 2 = -3#4
+#guard sdiv (-7#4) 2 = -3#4
+#guard sdiv (-6#4) (-2) = 3#4
+#guard sdiv (-7#4) (-2) = 3#4
+
+#guard srem   3#4    2  =  1
+#guard srem (-4#4)   3  = -1
+#guard srem ( 4#4) (-3) =  1
+#guard srem (-4#4) (-3) = -1
+
+#guard smod   3#4    2  = 1
+#guard smod (-4#4)   3  =  2
+#guard smod ( 4#4) (-3) = -2
+#guard smod (-4#4) (-3) = -1
+
+-- ofInt/toInt
+
+#guard .ofInt 3 (-1) = 0b111#3
+#guard .ofInt 3 0 = 0b000#3
+#guard .ofInt 3 4 = 0b100#3
+#guard .ofInt 3 (-2) = 0b110#3
+#guard .ofInt 3 (-4) = 0b100#3
+
+#guard (0x0#4).toInt = 0
+#guard (0x7#4).toInt = 7
+#guard (0x8#4).toInt = -8
+#guard (0xe#4).toInt = -2
+
+-- Bitwise operations
+
+#guard ~~~0b1010#4 = 0b0101#4
+#guard 0b1010#4 &&& 0b0110#4 = 0b0010#4
+#guard 0b1010#4 ||| 0b0110#4 = 0b1110#4
+#guard 0b1010#4 ^^^ 0b0110#4 = 0b1100#4
+
+-- shift operations
+#guard 0b0011#4 <<< 3 = 0b1000
+#guard 0b1011#4 >>> 1 = 0b0101
+#guard sshiftRight 0b1001#4 1 = 0b1100#4
+#guard rotateLeft  0b0011#4 3 = 0b1001
+#guard rotateRight 0b0010#4 2 = 0b1000
+#guard 0xab#8 ++ 0xcd#8 = 0xabcd#16
+
+-- get/extract
+
+#guard !getMsb 0b0101#4 0
+#guard getMsb 0b0101#4 1
+#guard !getMsb 0b0101#4 2
+#guard getMsb 0b0101#4 3
+#guard !getMsb 0b1111#4 4
+
+#guard getLsb 0b0101#4 0
+#guard !getLsb 0b0101#4 1
+#guard getLsb 0b0101#4 2
+#guard !getLsb 0b0101#4 3
+#guard !getLsb 0b1111#4 4
+
+#guard extractLsb 3 0 0x1234#16 = 4
+#guard extractLsb 7 4 0x1234#16 = 3
+#guard extractLsb' 0 4 0x1234#16 = 0x4#4
+
+/--
+This tests the match compiler with bitvector literals to ensure
+it can successfully generate a pattern for a bitvector literals.
+
+This fixes a regression introduced in PR #366.
+-/
+def testMatch8 (i : BitVec 32) :=
+  let op1 := i.extractLsb 28 25
+  match op1 with
+  | 0b1000#4 => some 0
+  | _ => none
+
+-- Pretty-printing
+
+#guard toString 5#12 = "0x005#12"
+#guard toString 5#13 = "0x0005#13"
+#guard toString 5#12 = "0x005#12"
+#guard toString 5#13 = "0x0005#13"
+
+-- Simp
+
+example (n w : Nat) (p : n < 2^w) : { toFin := { val := n, isLt := p } : BitVec w} = .ofNat w n := by
+  simp only [ofFin_eq_ofNat]
diff --git a/tests/lean/run/change.lean b/tests/lean/run/change.lean
new file mode 100644
index 0000000000..04fa47c287
--- /dev/null
+++ b/tests/lean/run/change.lean
@@ -0,0 +1,80 @@
+
+private axiom test_sorry : ∀ {α}, α
+
+set_option linter.missingDocs false
+set_option autoImplicit true
+
+example : n + 2 = m := by
+  change n + 1 + 1 = _
+  guard_target =ₛ n + 1 + 1 = m
+  exact test_sorry
+
+example (h : n + 2 = m) : False := by
+  change _ + 1 = _ at h
+  guard_hyp h :ₛ n + 1 + 1 = m
+  exact test_sorry
+
+example : n + 2 = m := by
+  fail_if_success change true
+  fail_if_success change _ + 3 = _
+  fail_if_success change _ * _ = _
+  change (_ : Nat) + _ = _
+  exact test_sorry
+
+-- `change ... at ...` allows placeholders to mean different things at different hypotheses
+example (h : n + 3 = m) (h' : n + 2 = m) : False := by
+  change _ + 1 = _ at h h'
+  guard_hyp h :ₛ n + 2 + 1 = m
+  guard_hyp h' :ₛ n + 1 + 1 = m
+  exact test_sorry
+
+-- `change ... at ...` preserves dependencies
+example (p : n + 2 = m → Type) (h : n + 2 = m) (x : p h) : false := by
+  change _ + 1 = _ at h
+  guard_hyp x :ₛ p h
+  exact test_sorry
+
+noncomputable example : Nat := by
+  fail_if_success change Type 1
+  exact test_sorry
+
+def foo (a b c : Nat) := if a < b then c else 0
+
+example : foo 1 2 3 = 3 := by
+  change (if _ then _ else _) = _
+  change ite _ _ _ = _
+  change (if _ < _ then _ else _) = _
+  change _ = (if true then 3 else 4)
+  rfl
+
+example (h : foo 1 2 3 = 4) : True := by
+  change ite _ _ _ = _ at h
+  guard_hyp h :ₛ ite (1 < 2) 3 0 = 4
+  trivial
+
+example (h : foo 1 2 3 = 4) : True := by
+  change (if _ then _ else _) = _ at h
+  guard_hyp h : (if 1 < 2 then 3 else 0) = 4
+  trivial
+
+example (α : Type) [LT α] (x : α) (h : x < x) : x < id x := by
+  change _ < _ -- can defer LT typeclass lookup, just like `show`
+  change _ < _ at h -- can defer LT typeclass lookup at h too
+  guard_target =ₛ x < id x
+  change _ < x
+  guard_target =ₛ x < x
+  exact h
+
+-- This example shows using named and anonymous placeholders to create a new goal.
+example (x y : Nat) (h : x = y) : True := by
+  change (if 1 < 2 then x else ?z + ?_) = y at h
+  rotate_left
+  · exact 4
+  · exact 37
+  guard_hyp h : (if 1 < 2 then x else 4 + 37) = y
+  · trivial
+
+example : let x := 22; let y : Nat := x; let z : Fin (y + 1) := 0; z.1 < y + 1 := by
+  intro x y z -- `z` was previously erroneously marked as unused
+  change _ at y
+  exact z.2