From ba78cc42f9df36e462c44a1651deeeec51d27b25 Mon Sep 17 00:00:00 2001
From: Jeremy Avigad <avigad@cmu.edu>
Date: Fri, 8 May 2015 10:43:36 +1000
Subject: [PATCH] fix(library/data/set/basic.lean, function.lean): fix typos

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

diff --git a/library/data/set/basic.lean b/library/data/set/basic.lean
index a5316422e..690a2a252 100644
--- a/library/data/set/basic.lean
+++ b/library/data/set/basic.lean
@@ -54,7 +54,7 @@ theorem mem_univ (x : T) : x ∈ univ := trivial
 definition inter [reducible] (a b : set T) : set T := λx, x ∈ a ∧ x ∈ b
 notation a ∩ b := inter a b
 
-theorem mem_inter (x : T) (a b : set T) : x ∈ a ∩ b ↔ (x ∈ a ∧ x ∈ b) := !iff.refl
+theorem mem_inter (x : T) (a b : set T) : x ∈ a ∩ b ↔ x ∈ a ∧ x ∈ b := !iff.refl
 
 theorem inter_self (a : set T) : a ∩ a = a :=
 setext (take x, !and_self)
@@ -76,7 +76,7 @@ setext (take x, !and.assoc)
 definition union [reducible] (a b : set T) : set T := λx, x ∈ a ∨ x ∈ b
 notation a ∪ b := union a b
 
-theorem mem_union (x : T) (a b : set T) : x ∈ a ∪ b ↔ (x ∈ a ∨ x ∈ b) := !iff.refl
+theorem mem_union (x : T) (a b : set T) : x ∈ a ∪ b ↔ x ∈ a ∨ x ∈ b := !iff.refl
 
 theorem union_self (a : set T) : a ∪ a = a :=
 setext (take x, !or_self)
diff --git a/library/data/set/function.lean b/library/data/set/function.lean
index a59b602ee..8012e0f54 100644
--- a/library/data/set/function.lean
+++ b/library/data/set/function.lean
@@ -41,7 +41,7 @@ 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]] :=
+lemma image_compose (f : Y → Z) (g : X → Y) (a : set X) : (f ∘ g) '[a] = f '[g '[a]] :=
 setext (take z,
   iff.intro
     (assume Hz : z ∈ (f ∘ g) '[a],