diff --git a/tests/lean/anc1.lean.expected.out b/tests/lean/anc1.lean.expected.out
index 9326c24d80..396e79cb0f 100644
--- a/tests/lean/anc1.lean.expected.out
+++ b/tests/lean/anc1.lean.expected.out
@@ -3,7 +3,7 @@ and.intro trivial trivial : true ∧ true
 anc1.lean:5:0: warning: declaration '[anonymous]' uses sorry
 ⟨1, sorry⟩ : Σ' (x : ℕ), x > 0
 show true, from true.intro : true
-Exists.intro 1 (id_locked (1 ≠ 0) (λ (a : 1 = 0), nat.no_confusion a)) : ∃ (x : ℕ), 1 ≠ 0
+Exists.intro 1 (id_locked (λ (a : 1 = 0), nat.no_confusion a)) : ∃ (x : ℕ), 1 ≠ 0
 λ (A B C : Prop) (Ha : A) (Hb : B) (Hc : C), show B ∧ A, from and.intro Hb Ha :
   ∀ (A B C : Prop), A → B → C → B ∧ A
 λ (A B C : Prop) (Ha : A) (Hb : B) (Hc : C),