diff --git a/tests/lean/583.lean.expected.out b/tests/lean/583.lean.expected.out
index 2edc63294a..1dcd41f331 100644
--- a/tests/lean/583.lean.expected.out
+++ b/tests/lean/583.lean.expected.out
@@ -11,5 +11,5 @@ P : f a⁻¹ * f a = 1
 583.lean:27:8: error: failed to add declaration 'group_hom.hom_map_inv' to environment, value has metavariables
 remark: set 'formatter.hide_full_terms' to false to see the complete term
   λ (A : Type) (B : Type) (s1 : …) (s2 : …) (f : …) (Hom : …) (a : A),
-    have P [visible] : …, from …,
+    assert P : …, from …,
     ?M_1
diff --git a/tests/lean/have1.lean.expected.out b/tests/lean/have1.lean.expected.out
index 37dd9aa36d..4e5be8d793 100644
--- a/tests/lean/have1.lean.expected.out
+++ b/tests/lean/have1.lean.expected.out
@@ -1,7 +1,7 @@
-have e1 [visible] : a = b, from H1,
+assert e1 : a = b, from H1,
 have e2 : a = c, from e1 ⬝ H2,
-have e3 : c = a, from e2 ⁻¹,
-have e4 [visible] : b = a, from e1 ⁻¹,
+have e3 : c = a, from e2⁻¹,
+assert e4 : b = a, from e1⁻¹,
 have e5 : b = c, from e4 ⬝ e2,
 have e6 : a = a, from H1 ⬝ H2 ⬝ H2 ⁻¹ ⬝ H1 ⁻¹ ⬝ H1 ⬝ H2 ⬝ H2 ⁻¹ ⬝ H1 ⁻¹,
 e3 ⬝ e2 :
diff --git a/tests/lean/show1.lean.expected.out b/tests/lean/show1.lean.expected.out
index 4653b8060c..cc67b811b0 100644
--- a/tests/lean/show1.lean.expected.out
+++ b/tests/lean/show1.lean.expected.out
@@ -1,8 +1,8 @@
 show a = c, from H1 ⬝ H2 : a = c
 ------------
-have e1 [visible] : a = b, from H1,
+assert e1 : a = b, from H1,
 have e2 : a = c, from e1 ⬝ H2,
-have e3 : c = a, from e2 ⁻¹,
-have e4 [visible] : b = a, from e1 ⁻¹,
-show b = c, from e1 ⁻¹ ⬝ e2 :
+have e3 : c = a, from e2⁻¹,
+assert e4 : b = a, from e1⁻¹,
+show b = c, from e1⁻¹ ⬝ e2 :
   b = c