diff --git a/library/algebra/function.lean b/library/algebra/function.lean
index 9180e8770..4bbcdefa7 100644
--- a/library/algebra/function.lean
+++ b/library/algebra/function.lean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2014 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Author: Leonardo de Moura
+Author: Leonardo de Moura, Jeremy Avigad, Haitao Zhang
 
 General operations on functions.
 -/
@@ -65,53 +65,91 @@ infixl  on                 := on_fun
 infixr  $                  := app
 notation f `-[` op `]-` g  := combine f op g
 
-lemma left_inv_eq {finv : B → A} {f : A → B} (linv : finv ∘ f = id) : ∀ x, finv (f x) = x :=
-take x, show (finv ∘ f) x = x, by rewrite linv
+lemma left_id (f : A → B) : id ∘ f = f := rfl
 
-lemma right_inv_eq {finv : B → A} {f : A → B} (rinv : f ∘ finv = id) : ∀ x, f (finv x) = x :=
-take x, show (f ∘ finv) x = x, by rewrite rinv
+lemma right_id (f : A → B) : f ∘ id = f := rfl
 
-definition injective (f : A → B) : Prop := ∀ a₁ a₂, f a₁ = f a₂ → a₁ = a₂
+theorem compose.assoc (f : C → D) (g : B → C) (h : A → B) : (f ∘ g) ∘ h = f ∘ (g ∘ h) := rfl
+
+theorem compose.left_id (f : A → B) : id ∘ f = f := rfl
+
+theorem compose.right_id (f : A → B) : f ∘ id = f := rfl
+
+theorem compose_const_right (f : B → C) (b : B) : f ∘ (const A b) = const A (f b) := rfl
+
+definition injective (f : A → B) : Prop := ∀ ⦃a₁ a₂⦄, f a₁ = f a₂ → a₁ = a₂
+
+theorem injective_compose {g : B → C} {f : A → B} (Hg : injective g) (Hf : injective f) :
+  injective (g ∘ f) :=
+take a₁ a₂, assume Heq, Hf (Hg Heq)
 
 definition surjective (f : A → B) : Prop := ∀ b, ∃ a, f a = b
 
-definition has_left_inverse (f : A → B) : Prop := ∃ finv : B → A, finv ∘ f = id
+theorem surjective_compose {g : B → C} {f : A → B} (Hg : surjective g) (Hf : surjective f) :
+  surjective (g ∘ f) :=
+take c,
+  obtain b (Hb : g b = c), from Hg c,
+  obtain a (Ha : f a = b), from Hf b,
+  exists.intro a (eq.trans (congr_arg g Ha) Hb)
 
-definition has_right_inverse (f : A → B) : Prop := ∃ finv : B → A, f ∘ finv = id
+definition bijective (f : A → B) := injective f ∧ surjective f
 
-lemma injective_of_has_left_inverse {f : A → B} : has_left_inverse f → injective f :=
+theorem bijective_compose {g : B → C} {f : A → B} (Hg : bijective g) (Hf : bijective f) :
+  bijective (g ∘ f) :=
+obtain Hginj Hgsurj, from Hg,
+obtain Hfinj Hfsurj, from Hf,
+and.intro (injective_compose Hginj Hfinj) (surjective_compose Hgsurj Hfsurj)
+
+-- g is a left inverse to f
+definition left_inverse (g : B → A) (f : A → B) : Prop := ∀x, g (f x) = x
+
+definition has_left_inverse (f : A → B) : Prop := ∃ finv : B → A, left_inverse finv f
+
+-- g is a right inverse to f
+definition right_inverse (g : B → A) (f : A → B) : Prop := left_inverse f g
+
+definition has_right_inverse (f : A → B) : Prop := ∃ finv : B → A, right_inverse finv f
+
+theorem injective_of_has_left_inverse {f : A → B} : has_left_inverse f → injective f :=
 assume h, take a b, assume faeqfb,
-obtain (finv : B → A) (inv : finv ∘ f = id), from h,
-calc a = finv (f a) : by rewrite (left_inv_eq inv)
+obtain (finv : B → A) (inv : left_inverse finv f), from h,
+calc a = finv (f a) : by rewrite inv
    ... = finv (f b) : faeqfb
-   ... = b          : by rewrite (left_inv_eq inv)
+   ... = b          : by rewrite inv
 
-lemma surjective_of_has_right_inverse {f : A → B} : has_right_inverse f → surjective f :=
+theorem right_inverse_of_injective_of_left_inverse {f : A → B} {g : B → A}
+    (injf : injective f) (lfg : left_inverse f g) :
+  right_inverse f g :=
+take x,
+have H : f (g (f x)) = f x, from lfg (f x),
+injf H
+
+theorem surjective_of_has_right_inverse {f : A → B} : has_right_inverse f → surjective f :=
 assume h, take b,
-obtain (finv : B → A) (inv : f ∘ finv = id), from h,
+obtain (finv : B → A) (inv : right_inverse finv f), from h,
 let  a : A := finv b in
 have h : f a = b, from calc
   f a  = (f ∘ finv) b : rfl
-   ... = id b         : by rewrite (right_inv_eq inv)
+   ... = id b         : by rewrite inv
    ... = b            : rfl,
 exists.intro a h
 
-  theorem compose.assoc (f : C → D) (g : B → C) (h : A → B) : (f ∘ g) ∘ h = f ∘ (g ∘ h) :=
-  funext (take x, rfl)
+theorem left_inverse_of_surjective_of_right_inverse {f : A → B} {g : B → A}
+    (surjf : surjective f) (rfg : right_inverse f g) :
+  left_inverse f g :=
+take y,
+obtain x (Hx : f x = y), from surjf y,
+calc
+  f (g y) = f (g (f x)) : Hx
+      ... = f x         : rfg
+      ... = y           : Hx
 
-  theorem compose.left_id (f : A → B) : id ∘ f = f :=
-  funext (take x, rfl)
+theorem injective_id : injective (@id A) := take a₁ a₂ H, H
 
-  theorem compose.right_id (f : A → B) : f ∘ id = f :=
-  funext (take x, rfl)
+theorem surjective_id : surjective (@id A) := take a, exists.intro a rfl
 
-  theorem compose_const_right (f : B → C) (b : B) : f ∘ (const A b) = const A (f b) :=
-  funext (take x, rfl)
+theorem bijective_id : bijective (@id A) := and.intro injective_id surjective_id
 
-  theorem hfunext {A : Type} {B : A → Type} {B' : A → Type} {f : Π x, B x} {g : Π x, B' x}
-                  (H : ∀ a, f a == g a) : f == g :=
-  let HH : B = B' := (funext (λ x, heq.type_eq (H x))) in
-    cast_to_heq (funext (λ a, heq.to_eq (heq.trans (cast_app HH f a) (H a))))
 end function
 
 -- copy reducible annotations to top-level
diff --git a/library/algebra/group.lean b/library/algebra/group.lean
index 9229ee9f3..901ad1e4f 100644
--- a/library/algebra/group.lean
+++ b/library/algebra/group.lean
@@ -257,11 +257,19 @@ section group
   theorem mul_right_cancel {a b c : A} (H : a * b = c * b) : a = c :=
   by rewrite [-mul_inv_cancel_right a b, H, mul_inv_cancel_right]
 
-  definition group.to_left_cancel_semigroup [instance] [coercion] [reducible] : left_cancel_semigroup A :=
+  theorem mul_eq_one_of_mul_eq_one {a b : A} (H : b * a = 1) : a * b = 1 :=
+  by rewrite [-inv_eq_of_mul_eq_one H, mul.left_inv]
+
+  theorem mul_eq_one_iff_mul_eq_one (a b : A) : a * b = 1 ↔ b * a = 1 :=
+  iff.intro !mul_eq_one_of_mul_eq_one !mul_eq_one_of_mul_eq_one
+
+  definition group.to_left_cancel_semigroup [instance] [coercion] [reducible] :
+    left_cancel_semigroup A :=
   ⦃ left_cancel_semigroup, s,
     mul_left_cancel := @mul_left_cancel A s ⦄
 
-  definition group.to_right_cancel_semigroup [instance] [coercion] [reducible] : right_cancel_semigroup A :=
+  definition group.to_right_cancel_semigroup [instance] [coercion] [reducible] :
+    right_cancel_semigroup A :=
   ⦃ right_cancel_semigroup, s,
     mul_right_cancel := @mul_right_cancel A s ⦄
 
diff --git a/library/data/finset/bigops.lean b/library/data/finset/bigops.lean
index 4c740d4e0..830de89a2 100644
--- a/library/data/finset/bigops.lean
+++ b/library/data/finset/bigops.lean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2015 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Author: Jeremy Avigad
+Author: Jeremy Avigad, Haitao Zhang
 
 Finite unions and intersections on finsets.
 
@@ -64,7 +64,7 @@ section deceqA
   include deceqA
   theorem Union_insert_of_mem (f : A → finset B) {a : A} {s : finset A} (H : a ∈ s) :
     Union (insert a s) f = Union s f := algebra.Prod_insert_of_mem f H
-  theorem Union_insert_of_not_mem (f : A → finset B) {a : A} {s : finset A} (H : a ∉ s) :
+  private theorem Union_insert_of_not_mem (f : A → finset B) {a : A} {s : finset A} (H : a ∉ s) :
     Union (insert a s) f = f a ∪ Union s f := algebra.Prod_insert_of_not_mem f H
   theorem Union_union (f : A → finset B) {s₁ s₂ : finset A} (disj : s₁ ∩ s₂ = ∅) :
     Union (s₁ ∪ s₂) f = Union s₁ f ∪ Union s₂ f := algebra.Prod_union f disj
@@ -92,6 +92,31 @@ section deceqA
   theorem mem_Union_eq (s : finset A) (f : A → finset B) (b : B) :
     b ∈ (⋃ x ∈ s, f x) = (∃ x, x ∈ s ∧ b ∈ f x ) :=
   propext !mem_Union_iff
+
+  theorem Union_insert (f : A → finset B) {a : A} {s : finset A} :
+    Union (insert a s) f = f a ∪ Union s f :=
+  decidable.by_cases
+    (assume Pin : a ∈ s,
+      begin
+        rewrite [Union_insert_of_mem f Pin],
+        apply ext,
+        intro x,
+        apply iff.intro,
+          exact mem_union_r,
+          rewrite [mem_union_eq],
+          intro Por,
+          exact or.elim Por
+            (assume Pl, begin
+              rewrite mem_Union_eq, exact (exists.intro a (and.intro Pin Pl)) end)
+            (assume Pr, Pr)
+      end)
+    (assume H : a ∉ s, !Union_insert_of_not_mem H)
+
+  lemma image_eq_Union_index_image (s : finset A) (f : A → finset B) :
+    Union s f = Union (image f s) function.id :=
+      finset.induction_on s
+        (by rewrite Union_empty)
+        (take s1 a Pa IH, by rewrite [image_insert, *Union_insert, IH])
 end deceqA
 
 end union
diff --git a/library/data/finset/card.lean b/library/data/finset/card.lean
index 7481251f7..8e9ec0a09 100644
--- a/library/data/finset/card.lean
+++ b/library/data/finset/card.lean
@@ -118,7 +118,7 @@ finset.induction_on s
         f a ∩ (⋃ (x : A) ∈ s', f x) = (⋃ (x : A) ∈ s', f a ∩ f x)  : inter_Union
                                 ... = (⋃ (x : A) ∈ s', ∅)          : Union_ext H7
                                 ... = ∅                            : Union_empty',
-    by rewrite [Union_insert_of_not_mem _ H, Sum_insert_of_not_mem _ H,
+    by rewrite [Union_insert, Sum_insert_of_not_mem _ H,
                 card_union_of_disjoint H8, H6])
 end deceqB
 
diff --git a/library/data/list/comb.lean b/library/data/list/comb.lean
index e44c10124..2408dded8 100644
--- a/library/data/list/comb.lean
+++ b/library/data/list/comb.lean
@@ -23,6 +23,10 @@ theorem map_id : ∀ l : list A, map id l = l
 | []      := rfl
 | (x::xs) := begin rewrite [map_cons, map_id] end
 
+theorem map_id' {f : A → A} (H : ∀x, f x = x) : ∀ l : list A, map f l = l
+| []      := rfl
+| (x::xs) := begin rewrite [map_cons, H, map_id'] end
+
 theorem map_map (g : B → C) (f : A → B) : ∀ l, map g (map f l) = map (g ∘ f) l
 | []       := rfl
 | (a :: l) :=
diff --git a/library/data/list/set.lean b/library/data/list/set.lean
index 55d265162..86c5883bb 100644
--- a/library/data/list/set.lean
+++ b/library/data/list/set.lean
@@ -283,12 +283,12 @@ theorem nodup_map {f : A → B} (inj : has_left_inverse f) : ∀ {l : list A}, n
   assert ndmfxs : nodup (map f xs), from nodup_map ndxs,
   assert nfxinm : f x ∉ map f xs,   from
     λ ab : f x ∈ map f xs,
-      obtain (finv : B → A) (isinv : finv ∘ f = id), from inj,
+      obtain (finv : B → A) (isinv : left_inverse finv f), from inj,
       assert finvfxin : finv (f x) ∈ map finv (map f xs), from mem_map finv ab,
       assert xinxs : x ∈ xs,
         begin
-          rewrite [map_map at finvfxin, isinv at finvfxin, left_inv_eq isinv at finvfxin],
-          rewrite [map_id at finvfxin],
+          rewrite [map_map at finvfxin, isinv at finvfxin],
+          krewrite [map_id' isinv at finvfxin],
           exact finvfxin
         end,
       absurd xinxs nxinxs,
diff --git a/library/data/set/basic.lean b/library/data/set/basic.lean
index 3b421346c..837a58be8 100644
--- a/library/data/set/basic.lean
+++ b/library/data/set/basic.lean
@@ -24,6 +24,11 @@ funext (take x, propext (H x))
 definition subset (a b : set X) := ∀⦃x⦄, x ∈ a → x ∈ b
 infix `⊆` := subset
 
+theorem subset.refl (a : set X) : a ⊆ a := take x, assume H, H
+
+theorem subset.trans (a b c : set X) (subab : a ⊆ b) (subbc : b ⊆ c) : a ⊆ c :=
+take x, assume ax, subbc (subab ax)
+
 /- bounded quantification -/
 
 abbreviation bounded_forall (a : set X) (P : X → Prop) := ∀⦃x⦄, x ∈ a → P x
diff --git a/library/data/set/function.lean b/library/data/set/function.lean
index 53d7c12f2..e5d59969f 100644
--- a/library/data/set/function.lean
+++ b/library/data/set/function.lean
@@ -51,6 +51,11 @@ setext (take z,
       obtain x (Hz₁ : x ∈ a) (Hz₂ : g x = y),      from Hy₁,
       show z ∈ (f ∘ g) '[a], from in_image Hz₁ (Hz₂⁻¹ ▸ Hy₂)))
 
+lemma image_subset {a b : set X} (f : X → Y) (H : a ⊆ b) : f '[a] ⊆ f '[b] :=
+take y, assume Hy : y ∈ f '[a],
+obtain x (Hx₁ : x ∈ a) (Hx₂ : f x = y), from Hy,
+in_image (H Hx₁) Hx₂
+
 /- maps to -/
 
 definition maps_to [reducible] (f : X → Y) (a : set X) (b : set Y) : Prop := ∀⦃x⦄, x ∈ a → f x ∈ b
@@ -67,6 +72,9 @@ theorem maps_to_compose {g : Y → Z} {f : X → Y} {a : set X} {b : set Y} {c :
    (H1 : maps_to g b c) (H2 : maps_to f a b) : maps_to (g ∘ f) a c :=
 take x, assume H : x ∈ a, H1 (H2 H)
 
+theorem maps_to_univ_univ (f : X → Y) : maps_to f univ univ :=
+take x, assume H, trivial
+
 /- injectivity -/
 
 definition inj_on [reducible] (f : X → Y) (a : set X) : Prop :=
@@ -100,6 +108,13 @@ take x1 x2 : X, assume (x1a : x1 ∈ a) (x2a : x2 ∈ a),
 assume H : f x1 = f x2,
 show x1 = x2, from H1 (H2 x1a) (H2 x2a) H
 
+lemma injective_iff_inj_on_univ {f : X → Y} : injective f ↔ inj_on f univ :=
+iff.intro
+  (assume H, take x₁ x₂, assume ax₁ ax₂, H x₁ x₂)
+  (assume H : inj_on f univ,
+     take x₁ x₂ Heq,
+     show x₁ = x₂, from H trivial trivial Heq)
+
 /- surjectivity -/
 
 definition surj_on [reducible] (f : X → Y) (a : set X) (b : set Y) : Prop := b ⊆ f '[a]
@@ -128,6 +143,15 @@ show ∃x, x ∈ a ∧ g (f x) = z, from
         g (f x) = g y : {and.right H2}
             ... = z   : and.right H1))
 
+lemma surjective_iff_surj_on_univ {f : X → Y} : surjective f ↔ surj_on f univ univ :=
+iff.intro
+  (assume H, take y, assume Hy,
+    obtain x Hx, from H y,
+    in_image trivial Hx)
+  (assume H, take y,
+    obtain x H1x H2x, from H y trivial,
+    exists.intro x H2x)
+
 /- bijectivity -/
 
 definition bij_on [reducible] (f : X → Y) (a : set X) (b : set Y) : Prop :=
@@ -156,6 +180,21 @@ match Hg with and.intro Hgmap (and.intro Hginj Hgsurj) :=
   end
 end
 
+-- TODO: simplify when we have a better way of handling congruences wrt iff
+lemma bijective_iff_bij_on_univ {f : X → Y} : bijective f ↔ bij_on f univ univ :=
+iff.intro
+  (assume H,
+    obtain Hinj Hsurj, from H,
+    and.intro (maps_to_univ_univ f)
+      (and.intro
+        (iff.mp !injective_iff_inj_on_univ Hinj)
+        (iff.mp !surjective_iff_surj_on_univ Hsurj)))
+ (assume H,
+    obtain Hmaps Hinj Hsurj, from H,
+      (and.intro
+        (iff.mp' !injective_iff_inj_on_univ Hinj)
+        (iff.mp' !surjective_iff_surj_on_univ Hsurj)))
+
 /- left inverse -/
 
 -- g is a left inverse to f on a
@@ -227,6 +266,13 @@ theorem right_inv_on_compose {f' : Y → X} {g' : Z → Y} {g : Y → Z} {f : X
     (Hf : right_inv_on f' f b) (Hg : right_inv_on g' g c) : right_inv_on (f' ∘ g') (g ∘ f) c :=
 left_inv_on_compose g'cb Hg Hf
 
+theorem right_inv_on_of_inj_on_of_left_inv_on {f : X → Y} {g : Y → X} {a : set X} {b : set Y}
+    (fab : maps_to f a b) (gba : maps_to g b a) (injf : inj_on f a) (lfg : left_inv_on f g b) :
+  right_inv_on f g a :=
+take x, assume xa : x ∈ a,
+have H : f (g (f x)) = f x, from lfg (fab xa),
+injf (gba (fab xa)) xa H
+
 theorem eq_on_of_left_inv_of_right_inv {g1 g2 : Y → X} {f : X → Y} {a : set X} {b : set Y}
   (g2ba : maps_to g2 b a) (Hg1 : left_inv_on g1 f a) (Hg2 : right_inv_on g2 f b) : eq_on g1 g2 b :=
 take y,
@@ -235,6 +281,16 @@ calc
   g1 y = g1 (f (g2 y)) : {(Hg2 yb)⁻¹}
    ... = g2 y          : Hg1 (g2ba yb)
 
+theorem left_inv_on_of_surj_on_right_inv_on {f : X → Y} {g : Y → X} {a : set X} {b : set Y}
+    (surjf : surj_on f a b) (rfg : right_inv_on f g a) :
+  left_inv_on f g b :=
+take y, assume yb : y ∈ b,
+obtain x (xa : x ∈ a) (Hx : f x = y), from surjf yb,
+calc
+  f (g y) = f (g (f x)) : Hx
+      ... = f x         : rfg xa
+      ... = y           : Hx
+
 /- inverses -/
 
 -- g is an inverse to f viewed as a map from a to b
diff --git a/library/data/set/map.lean b/library/data/set/map.lean
index 52de59ebd..f710a68ac 100644
--- a/library/data/set/map.lean
+++ b/library/data/set/map.lean
@@ -37,7 +37,8 @@ take x, assume Ha : x ∈ a, eq.trans (H₁ Ha) (H₂ Ha)
 
 protected theorem equiv.is_equivalence {X Y : Type} (a : set X) (b : set Y) :
   equivalence (@map.equiv X Y a b) :=
-mk_equivalence (@map.equiv X Y a b) (@equiv.refl X Y a b) (@equiv.symm X Y a b) (@equiv.trans X Y a b)
+mk_equivalence (@map.equiv X Y a b) (@equiv.refl X Y a b) (@equiv.symm X Y a b)
+    (@equiv.trans X Y a b)
 
 /- compose -/
 
@@ -73,7 +74,8 @@ theorem surjective_of_equiv {f1 f2 : map a b} (H1 : f1 ~ f2) (H2 : map.surjectiv
   map.surjective f2 :=
 surj_on_of_eq_on H1 H2
 
-theorem surjective_compose {g : map b c} {f : map a b} (Hg : map.surjective g) (Hf: map.surjective f) :
+theorem surjective_compose {g : map b c} {f : map a b} (Hg : map.surjective g)
+    (Hf: map.surjective f) :
   map.surjective (g ∘ f) :=
 surj_on_compose Hg Hf
 
@@ -109,7 +111,8 @@ theorem injective_of_left_inverse {g : map b a} {f : map a b} (H : map.left_inve
 inj_on_of_left_inv_on H
 
 theorem left_inverse_compose {f' : map b a} {g' : map c b} {g : map b c} {f : map a b}
-    (Hf : map.left_inverse f' f) (Hg : map.left_inverse g' g) : map.left_inverse (f' ∘ g') (g ∘ f) :=
+    (Hf : map.left_inverse f' f) (Hg : map.left_inverse g' g) :
+  map.left_inverse (f' ∘ g') (g ∘ f) :=
 left_inv_on_compose (mapsto f) Hf Hg
 
 /- right inverse -/
@@ -125,12 +128,23 @@ theorem right_inverse_of_equiv_right {g : map b a} {f1 f2 : map a b} (eqf : f1 ~
   (H : map.right_inverse g f1) : map.right_inverse g f2 :=
 map.left_inverse_of_equiv_left eqf H
 
+theorem right_inverse_of_injective_of_left_inverse {f : map a b} {g : map b a}
+    (injf : map.injective f) (lfg : map.left_inverse f g) :
+  map.right_inverse f g :=
+right_inv_on_of_inj_on_of_left_inv_on (mapsto f) (mapsto g) injf lfg
+
 theorem surjective_of_right_inverse {g : map b a} {f : map a b} (H : map.right_inverse g f) :
   map.surjective f :=
 surj_on_of_right_inv_on (mapsto g) H
 
+theorem left_inverse_of_surjective_of_right_inverse {f : map a b} {g : map b a}
+    (surjf : map.surjective f) (rfg : map.right_inverse f g) :
+  map.left_inverse f g :=
+left_inv_on_of_surj_on_right_inv_on surjf rfg
+
 theorem right_inverse_compose {f' : map b a} {g' : map c b} {g : map b c} {f : map a b}
-    (Hf : map.right_inverse f' f) (Hg : map.right_inverse g' g) : map.right_inverse (f' ∘ g') (g ∘ f) :=
+    (Hf : map.right_inverse f' f) (Hg : map.right_inverse g' g) :
+  map.right_inverse (f' ∘ g') (g ∘ f) :=
 map.left_inverse_compose Hg Hf
 
 theorem equiv_of_map.left_inverse_of_right_inverse {g1 g2 : map b a} {f : map a b}
@@ -143,7 +157,8 @@ eq_on_of_left_inv_of_right_inv (mapsto g2) H1 H2
 protected definition is_inverse (g : map b a) (f : map a b) : Prop :=
 map.left_inverse g f ∧ map.right_inverse g f
 
-theorem bijective_of_is_inverse {g : map b a} {f : map a b} (H : map.is_inverse g f) : map.bijective f :=
+theorem bijective_of_is_inverse {g : map b a} {f : map a b} (H : map.is_inverse g f) :
+  map.bijective f :=
 and.intro
   (injective_of_left_inverse (and.left H))
   (surjective_of_right_inverse (and.right H))
diff --git a/library/logic/axioms/examples/leftinv_of_inj.lean b/library/logic/axioms/examples/leftinv_of_inj.lean
index 228c05c7d..db66e633e 100644
--- a/library/logic/axioms/examples/leftinv_of_inj.lean
+++ b/library/logic/axioms/examples/leftinv_of_inj.lean
@@ -19,13 +19,13 @@ theorem has_left_inverse_of_injective {A B : Type} {f : A → B} : nonempty A 
 assume h : nonempty A,
 assume inj  : ∀ a₁ a₂, f a₁ = f a₂ → a₁ = a₂,
 let  finv : B → A := mk_left_inv f in
-have linv : finv ∘ f = id, from
-  funext (λ a,
+have linv : left_inverse finv f, from
+  λ a,
     assert ex : ∃ a₁ : A, f a₁ = f a, from exists.intro a rfl,
     assert h₁ : f (some ex) = f a,    from !some_spec,
     begin
       esimp [mk_left_inv, compose, id],
       rewrite [dif_pos ex],
       exact (!inj h₁)
-    end),
+    end,
 exists.intro finv linv
diff --git a/library/logic/cast.lean b/library/logic/cast.lean
index 6d90638b2..764ce7311 100644
--- a/library/logic/cast.lean
+++ b/library/logic/cast.lean
@@ -121,6 +121,12 @@ section
   H₂ (pi_eq H)
 end
 
+-- function extensionality wrt heterogeneous equality
+theorem hfunext {A : Type} {B : A → Type} {B' : A → Type} {f : Π x, B x} {g : Π x, B' x}
+                (H : ∀ a, f a == g a) : f == g :=
+let HH : B = B' := (funext (λ x, heq.type_eq (H x))) in
+  cast_to_heq (funext (λ a, heq.to_eq (heq.trans (cast_app HH f a) (H a))))
+
 section
   variables {A : Type} {B : A → Type} {C : Πa, B a → Type} {D : Πa b, C a b → Type}
             {E : Πa b c, D a b c → Type} {F : Type}
diff --git a/library/logic/connectives.lean b/library/logic/connectives.lean
index b6e4cbcce..f2e525120 100644
--- a/library/logic/connectives.lean
+++ b/library/logic/connectives.lean
@@ -114,15 +114,15 @@ propext
   (iff.intro (λ Pl a b, Pl (and.intro a b))
   (λ Pr Pand, Pr (and.left Pand) (and.right Pand)))
 
-theorem and_eq_right {a b : Prop} (Ha : a) : (a ∧ b) = b :=
-propext (iff.intro
+theorem and_iff_right {a b : Prop} (Ha : a) : (a ∧ b) ↔ b :=
+iff.intro
   (assume Hab, and.elim_right Hab)
-  (assume Hb, and.intro Ha Hb))
+  (assume Hb, and.intro Ha Hb)
 
-theorem and_eq_left {a b : Prop} (Hb : b) : (a ∧ b) = a :=
-propext (iff.intro
+theorem and_iff_left {a b : Prop} (Hb : b) : (a ∧ b) ↔ a :=
+iff.intro
   (assume Hab, and.elim_left Hab)
-  (assume Ha, and.intro Ha Hb))
+  (assume Ha, and.intro Ha Hb)
 
 /- or -/
 
diff --git a/tests/lean/run/fun.lean b/tests/lean/run/fun.lean
index 626a928f3..ebbc8195c 100644
--- a/tests/lean/run/fun.lean
+++ b/tests/lean/run/fun.lean
@@ -11,10 +11,10 @@ check typeof id : num → num
 
 constant h : num → bool → num
 
-check flip h
-check flip h ff num.zero
+check swap h
+check swap h ff num.zero
 
-check typeof flip h ff num.zero : num
+check typeof swap h ff num.zero : num
 
 constant f1 : num → num → bool
 constant f2 : bool → num
diff --git a/tests/lean/run/tut_104.lean b/tests/lean/run/tut_104.lean
index 754e6e9e5..86e521155 100644
--- a/tests/lean/run/tut_104.lean
+++ b/tests/lean/run/tut_104.lean
@@ -4,7 +4,6 @@ section
 open set
 variables {A B : Type}
 set_option pp.beta false
-definition bijective (f : A → B) := injective f ∧ surjective f
 
 lemma injective_eq_inj_on_univ₁ (f : A → B) : injective f = inj_on f univ :=
   begin
@@ -13,7 +12,7 @@ lemma injective_eq_inj_on_univ₁ (f : A → B) : injective f = inj_on f univ :=
     apply iff.intro,
       intro Pl a1 a2,
         rewrite *true_imp,
-        exact Pl a1 a2,
+        exact @Pl a1 a2,
       intro Pr a1 a2,
       exact Pr trivial trivial
   end
@@ -25,7 +24,7 @@ lemma injective_eq_inj_on_univ₂ (f : A → B) : injective f = inj_on f univ :=
     apply iff.intro,
       intro Pl a1 a2,
         rewrite *(propext !true_imp),
-        exact Pl a1 a2,
+        exact @Pl a1 a2,
       intro Pr a1 a2,
       exact Pr trivial trivial
   end