From f7a610faa3023c8d8c2a0ec8235147a90ac6ab7d Mon Sep 17 00:00:00 2001
From: Jeremy Avigad <avigad@cmu.edu>
Date: Tue, 5 May 2015 20:56:22 +1000
Subject: [PATCH] feat(library/data/set/basic,function): mark set reducible,
 and add theorem from Haitao Zhang

---
 library/data/set/basic.lean    |  2 +-
 library/data/set/function.lean | 18 +++++++++++++++++-
 2 files changed, 18 insertions(+), 2 deletions(-)

diff --git a/library/data/set/basic.lean b/library/data/set/basic.lean
index 96ebc0af7..a5316422e 100644
--- a/library/data/set/basic.lean
+++ b/library/data/set/basic.lean
@@ -8,7 +8,7 @@ Author: Jeremy Avigad, Leonardo de Moura
 import logic
 open eq.ops
 
-definition set (T : Type) := T → Prop
+definition set [reducible] (T : Type) := T → Prop
 
 namespace set
 
diff --git a/library/data/set/function.lean b/library/data/set/function.lean
index 06e117121..300b515f6 100644
--- a/library/data/set/function.lean
+++ b/library/data/set/function.lean
@@ -3,7 +3,7 @@ Copyright (c) 2014 Jeremy Avigad. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 
 Module: data.set.function
-Author: Jeremy Avigad, Andrew Zipperer
+Author: Jeremy Avigad, Andrew Zipperer, Haitao Zhang
 
 Functions between subsets of finite types.
 -/
@@ -37,6 +37,22 @@ setext (take y, iff.intro
     have H5 : f1 x = y, from (H1 H4) ⬝ and.right H3,
     exists.intro x (and.intro H4 H5)))
 
+theorem in_image {f : X → Y} {a : set X} {x : X} {y : Y}
+  (H1 : x ∈ a) (H2 : f x = y) : y ∈ f '[a] :=
+exists.intro x (and.intro H1 H2)
+
+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 : z ∈ (f ∘ g) '[a],
+      obtain x (Hx : x ∈ a ∧ f (g x) = z), from Hz,
+      have Hgx : g x ∈ g '[a], from in_image (and.left Hx) rfl,
+      show z ∈ f '[g '[a]], from in_image Hgx (and.right Hx))
+    (assume Hz : z ∈ f '[g '[a]],
+      obtain y (Hy : y ∈ g '[a] ∧ f y = z), from Hz,
+      obtain x (Hz : x ∈ a ∧ g x = y), from and.left Hy,
+      show z ∈ (f ∘ g) '[a], from in_image (and.left Hz) ((and.right Hz)⁻¹ ▸ (and.right Hy))))
+
 /- maps to -/
 
 definition maps_to [reducible] (f : X → Y) (a : set X) (b : set Y) : Prop := ∀⦃x⦄, x ∈ a → f x ∈ b