From 02662fe489fa8ce278c0a3293a3988346a6b326f Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 6 May 2015 12:51:06 -0700
Subject: [PATCH] test(tests/lean/run/new_obtain4): test new 'obtain'
 expression using minimal amount of annotations

---
 tests/lean/run/new_obtain4.lean | 14 ++++++++++++++
 1 file changed, 14 insertions(+)
 create mode 100644 tests/lean/run/new_obtain4.lean

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₂)))