diff --git a/tests/lean/run/new_obtain4.lean b/tests/lean/run/new_obtain4.lean
new file mode 100644
index 000000000..326c2e303
--- /dev/null
+++ b/tests/lean/run/new_obtain4.lean
@@ -0,0 +1,14 @@
+import data.set
+open set function eq.ops
+
+variables {X Y Z : Type}
+
+lemma image_compose (f : Y → X) (g : X → Y) (a : set X) : (f ∘ g) '[a] = f '[g '[a]] :=
+setext (take z,
+  iff.intro
+    (assume Hz,
+      obtain x Hx₁ Hx₂, from Hz,
+      by repeat (apply in_image | assumption | reflexivity))
+    (assume Hz,
+      obtain y [x Hz₁ Hz₂] Hy₂, from Hz,
+      by repeat (apply in_image | assumption | esimp [compose] | rewrite Hz₂)))