diff --git a/tests/lean/inaccessible2.lean b/tests/lean/inaccessible2.lean
index 094d22e646..757c50cacd 100644
--- a/tests/lean/inaccessible2.lean
+++ b/tests/lean/inaccessible2.lean
@@ -5,3 +5,9 @@ inductive imf {A B : Type} (f : A → B) : B → Type
 
 definition inv_1 {A B : Type} (f : A → B) : ∀ (b : B), imf f b → A
 | .(f .a) (imf.mk .f a)  := a  -- Error inaccessible annotation inside inaccessible annotation
+
+definition inv_2 {A B : Type} (f : A → B) : ∀ (b : B), imf f b → A
+| .(f a) (let x := (imf.mk .f a) in x)  := a  -- Error invalid occurrence of 'let' expression
+
+definition inv_3 {A B : Type} (f : A → B) : ∀ (b : B), imf f b → A
+| .(f a) ((λ (x : imf f b), x) (imf.mk .f a)) := a  -- Error invalid occurrence of 'lambda' expression
diff --git a/tests/lean/inaccessible2.lean.expected.out b/tests/lean/inaccessible2.lean.expected.out
index 849336f31f..ddd241c93a 100644
--- a/tests/lean/inaccessible2.lean.expected.out
+++ b/tests/lean/inaccessible2.lean.expected.out
@@ -1 +1,3 @@
 inaccessible2.lean:7:7: error: invalid occurrence of 'inaccessible' annotation, it must only occur in patterns
+inaccessible2.lean:10:10: error: invalid pattern, must be an application, constant, variable, type ascription or inaccessible term
+inaccessible2.lean:13:13: error: invalid pattern, must be an application, constant, variable, type ascription or inaccessible term