From 3aac370629268d564a8e70ac313fff90aa6939ff Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 8 May 2015 11:02:06 -0700
Subject: [PATCH] fix(library/data/finset/basic): type error on the
 finset.induction proof

---
 library/data/finset/basic.lean | 11 ++++++++---
 1 file changed, 8 insertions(+), 3 deletions(-)

diff --git a/library/data/finset/basic.lean b/library/data/finset/basic.lean
index 496e6b596..b2b62b903 100644
--- a/library/data/finset/basic.lean
+++ b/library/data/finset/basic.lean
@@ -194,9 +194,9 @@ protected theorem induction {P : finset A → Prop}
   ∀s, P s :=
 take s,
 quot.induction_on s
-  take u,
+ (take u,
   subtype.destruct u
-    take l,
+   (take l,
     list.induction_on l
       (assume nodup_l, H1)
       (take a l',
@@ -206,7 +206,12 @@ quot.induction_on s
         assert nodup_l' : nodup l', from nodup_of_nodup_cons nodup_al',
         assert P_l' : P (quot.mk (subtype.tag l' nodup_l')), from IH nodup_l',
         assert H4 : P (insert a (quot.mk (subtype.tag l' nodup_l'))), from H2 anl' P_l',
-        begin rewrite [eq.symm H3], apply H4 end)
+        begin
+          revert nodup_al',
+          rewrite [-H3],
+          intros,
+          apply H4
+        end)))
 
 protected theorem induction_on {P : finset A → Prop} (s : finset A)
     (H1 : P empty)