From a85d027c90835f2b298191fc286282e0938292f3 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 20 Jun 2016 09:39:22 -0700
Subject: [PATCH] chore(library/init/sigma): remove 'sorry'

---
 library/init/sigma.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/library/init/sigma.lean b/library/init/sigma.lean
index 7216c46bdc..82a5196aaa 100644
--- a/library/init/sigma.lean
+++ b/library/init/sigma.lean
@@ -11,8 +11,8 @@ notation `Σ` binders `, ` r:(scoped P, sigma P) := r
 -- notation for n-ary tuples; input ⟨ ⟩ as \< \>
 notation `⟨`:max t:(foldr `, ` (e r, sigma.mk e r)) `⟩`:0 := t
 
-lemma ex_of_sig {A : Type} {P : A → Prop} : (Σ x, P x) → ∃ x, P x :=
-sorry -- assume h, obtain x hx, from h, exists.intro x hx
+lemma ex_of_sig {A : Type} {P : A → Prop} : (Σ x, P x) → ∃ x, P x
+| ⟨x, hx⟩ := exists.intro x hx
 
 namespace sigma
   notation `pr₁`  := pr1