diff --git a/tests/lean/hygienicIntro.lean b/tests/lean/hygienicIntro.lean
index 9a92cdda03..90eade0cd7 100644
--- a/tests/lean/hygienicIntro.lean
+++ b/tests/lean/hygienicIntro.lean
@@ -20,9 +20,9 @@ apply h1;
 assumption
 
 example {p q : Prop} (h₁ : p → q) (h₂ : p ∨ q) : q := by
-cases h₂;
-{ apply h₁; exact h }; -- error "unknown identifier"
-exact h
+  cases h₂;
+  { apply h₁; exact h }; -- error "unknown identifier"
+  exact h
 
 set_option hygienicIntro false in
 example {p q : Prop} (h₁ : p → q) (h₂ : p ∨ q) : q := by
diff --git a/tests/lean/hygienicIntro.lean.expected.out b/tests/lean/hygienicIntro.lean.expected.out
index cccaad22c6..2fea245a39 100644
--- a/tests/lean/hygienicIntro.lean.expected.out
+++ b/tests/lean/hygienicIntro.lean.expected.out
@@ -1,2 +1,2 @@
 hygienicIntro.lean:14:6-14:9: error: unknown identifier 'a_1'
-hygienicIntro.lean:24:18-24:19: error: unknown identifier 'h'
+hygienicIntro.lean:24:20-24:21: error: unknown identifier 'h'