diff --git a/src/data/equiv/basic.lean b/src/data/equiv/basic.lean
index e45e7b38889a7..bcb1f0fd075fd 100644
--- a/src/data/equiv/basic.lean
+++ b/src/data/equiv/basic.lean
@@ -58,20 +58,15 @@ equiv.ext _ _ H
 ⟨e₂.to_fun ∘ e₁.to_fun, e₁.inv_fun ∘ e₂.inv_fun,
   e₂.left_inv.comp e₁.left_inv, e₂.right_inv.comp e₁.right_inv⟩
 
-protected theorem injective : ∀ f : α ≃ β, injective f
-| ⟨f, g, h₁, h₂⟩ := injective_of_left_inverse h₁
-
-protected theorem surjective : ∀ f : α ≃ β, surjective f
-| ⟨f, g, h₁, h₂⟩ := surjective_of_has_right_inverse ⟨_, h₂⟩
-
-protected theorem bijective (f : α ≃ β) : bijective f :=
-⟨f.injective, f.surjective⟩
+protected theorem bijective : ∀ f : α ≃ β, bijective f
+| ⟨f, g, h₁, h₂⟩ :=
+  ⟨injective_of_left_inverse h₁, surjective_of_has_right_inverse ⟨_, h₂⟩⟩
 
 protected theorem subsingleton (e : α ≃ β) : ∀ [subsingleton β], subsingleton α
-| ⟨H⟩ := ⟨λ a b, e.injective (H _ _)⟩
+| ⟨H⟩ := ⟨λ a b, e.bijective.1 (H _ _)⟩
 
 protected def decidable_eq (e : α ≃ β) [H : decidable_eq β] : decidable_eq α
-| a b := decidable_of_iff _ e.injective.eq_iff
+| a b := decidable_of_iff _ e.bijective.1.eq_iff
 
 protected def cast {α β : Sort*} (h : α = β) : α ≃ β :=
 ⟨cast h, cast h.symm, λ x, by cases h; refl, λ x, by cases h; refl⟩
@@ -471,13 +466,13 @@ def fin_equiv_subtype (n : ℕ) : fin n ≃ {m // m < n} :=
 ⟨λ x, ⟨x.1, x.2⟩, λ x, ⟨x.1, x.2⟩, λ ⟨a, b⟩, rfl,λ ⟨a, b⟩, rfl⟩
 
 def decidable_eq_of_equiv [decidable_eq β] (e : α ≃ β) : decidable_eq α
-| a₁ a₂ := decidable_of_iff (e a₁ = e a₂) e.injective.eq_iff
+| a₁ a₂ := decidable_of_iff (e a₁ = e a₂) e.bijective.1.eq_iff
 
 def inhabited_of_equiv [inhabited β] (e : α ≃ β) : inhabited α :=
 ⟨e.symm (default _)⟩
 
 def unique_of_equiv (e : α ≃ β) (h : unique β) : unique α :=
-unique.of_surjective e.symm.surjective
+unique.of_surjective e.symm.bijective.2
 
 def unique_congr (e : α ≃ β) : unique α ≃ unique β :=
 { to_fun := e.symm.unique_of_equiv,
diff --git a/src/data/fintype.lean b/src/data/fintype.lean
index 80d41f9e980e8..bc90809acef6e 100644
--- a/src/data/fintype.lean
+++ b/src/data/fintype.lean
@@ -312,7 +312,7 @@ finset.card_le_card_of_inj_on f (λ _ _, finset.mem_univ _) (λ _ _ _ _ h, hf h)
 
 lemma fintype.card_eq_one_iff [fintype α] : fintype.card α = 1 ↔ (∃ x : α, ∀ y, y = x) :=
 by rw [← fintype.card_unit, fintype.card_eq]; exact
-⟨λ ⟨a⟩, ⟨a.symm (), λ y, a.injective (subsingleton.elim _ _)⟩,
+⟨λ ⟨a⟩, ⟨a.symm (), λ y, a.bijective.1 (subsingleton.elim _ _)⟩,
   λ ⟨x, hx⟩, ⟨⟨λ _, (), λ _, x, λ _, (hx _).trans (hx _).symm,
     λ _, subsingleton.elim _ _⟩⟩⟩
 
@@ -370,9 +370,9 @@ lemma fintype.injective_iff_surjective_of_equiv [fintype α] {f : α → β} (e
   injective f ↔ surjective f :=
 have injective (e.symm ∘ f) ↔ surjective (e.symm ∘ f), from fintype.injective_iff_surjective,
 ⟨λ hinj, by simpa [function.comp] using
-  surjective_comp e.surjective (this.1 (injective_comp e.symm.injective hinj)),
+  surjective_comp e.bijective.2 (this.1 (injective_comp e.symm.bijective.1 hinj)),
 λ hsurj, by simpa [function.comp] using
-  injective_comp e.injective (this.2 (surjective_comp e.symm.surjective hsurj))⟩
+  injective_comp e.bijective.1 (this.2 (surjective_comp e.symm.bijective.2 hsurj))⟩
 
 instance list.subtype.fintype [decidable_eq α] (l : list α) : fintype {x // x ∈ l} :=
 fintype.of_list l.attach l.mem_attach
@@ -536,17 +536,17 @@ then
   mem_append_left _ $ mem_perms_of_list_of_mem
     (λ x hx, mem_of_ne_of_mem (λ h, by rw h at hx; exact hx hfa) (h x hx))
 else
-have hfa' : f (f a) ≠ f a, from mt (λ h, f.injective h) hfa,
+have hfa' : f (f a) ≠ f a, from mt (λ h, f.bijective.1 h) hfa,
 have ∀ (x : α), (swap a (f a) * f) x ≠ x → x ∈ l,
   from λ x hx, have hxa : x ≠ a, from λ h, by simpa [h, mul_apply] using hx,
-    have hfxa : f x ≠ f a, from mt (λ h, f.injective h) hxa,
+    have hfxa : f x ≠ f a, from mt (λ h, f.bijective.1 h) hxa,
     list.mem_of_ne_of_mem hxa
       (h x (λ h, by simp [h, mul_apply, swap_apply_def] at hx; split_ifs at hx; cc)),
 suffices f ∈ perms_of_list l ∨ ∃ (b : α), b ∈ l ∧ ∃ g : perm α, g ∈ perms_of_list l ∧ swap a b * g = f,
   by simpa [perms_of_list],
 (@or_iff_not_imp_left _ _ (classical.prop_decidable _)).2
   (λ hfl, ⟨f a,
-    if hffa : f (f a) = a then mem_of_ne_of_mem hfa (h _ (mt (λ h, f.injective h) hfa))
+    if hffa : f (f a) = a then mem_of_ne_of_mem hfa (h _ (mt (λ h, f.bijective.1 h) hfa))
       else this _ $ by simp [mul_apply, swap_apply_def]; split_ifs; cc,
     ⟨swap a (f a) * f, mem_perms_of_list_of_mem this,
       by rw [← mul_assoc, mul_def (swap a (f a)) (swap a (f a)), swap_swap, ← equiv.perm.one_def, one_mul]⟩⟩)
@@ -591,7 +591,7 @@ by rw [perms_of_list, list.nodup_append, list.nodup_bind, pairwise_iff_nth_le];
   λ f hf₁ hf₂,
     let ⟨x, hx, hx'⟩ := list.mem_bind.1 hf₂ in
     let ⟨g, hg⟩ := list.mem_map.1 hx' in
-    have hgxa : g⁻¹ x = a, from f.injective $
+    have hgxa : g⁻¹ x = a, from f.bijective.1 $
       by rw [hmeml hf₁, ← hg.2]; simp,
     have hxa : x ≠ a, from λ h, (list.nodup_cons.1 hl).1 (h ▸ hx),
     (list.nodup_cons.1 hl).1 $
diff --git a/src/group_theory/perm/cycles.lean b/src/group_theory/perm/cycles.lean
index 6456b856f2835..666199cdab389 100644
--- a/src/group_theory/perm/cycles.lean
+++ b/src/group_theory/perm/cycles.lean
@@ -23,7 +23,7 @@ def same_cycle (f : perm β) (x y : β) := ∃ i : ℤ, (f ^ i) x = y
 lemma apply_eq_self_iff_of_same_cycle {f : perm β} {x y : β} :
   same_cycle f x y → (f x = x ↔ f y = y) :=
 λ ⟨i, hi⟩, by rw [← hi, ← mul_apply, ← gpow_one_add, add_comm, gpow_add_one, mul_apply,
-    (f ^ i).injective.eq_iff]
+    (f ^ i).bijective.1.eq_iff]
 
 lemma same_cycle_of_is_cycle {f : perm β} (hf : is_cycle f) {x y : β}
   (hx : f x ≠ x) (hy : f y ≠ y) : same_cycle f x y :=
@@ -47,7 +47,7 @@ lemma same_cycle_apply {f : perm β} {x y : β} : same_cycle f x (f y) ↔ same_
 lemma same_cycle_cycle {f : perm β} {x : β} (hx : f x ≠ x) : is_cycle f ↔
   (∀ {y}, same_cycle f x y ↔ f y ≠ y) :=
 ⟨λ hf y, ⟨λ ⟨i, hi⟩ hy, hx $
-    by rw [← gpow_apply_eq_self_of_apply_eq_self hy i, (f ^ i).injective.eq_iff] at hi;
+    by rw [← gpow_apply_eq_self_of_apply_eq_self hy i, (f ^ i).bijective.1.eq_iff] at hi;
     rw [hi, hy],
   exists_gpow_eq_of_is_cycle hf hx⟩,
   λ h, ⟨x, hx, λ y hy, h.2 hy⟩⟩
diff --git a/src/group_theory/perm/sign.lean b/src/group_theory/perm/sign.lean
index 67d15cb0ed5c6..9416b9afb4076 100644
--- a/src/group_theory/perm/sign.lean
+++ b/src/group_theory/perm/sign.lean
@@ -39,7 +39,7 @@ end⟩
 is_group_hom.one of_subtype
 
 lemma eq_inv_iff_eq {f : perm α} {x y : α} : x = f⁻¹ y ↔ f x = y :=
-by conv {to_lhs, rw [← injective.eq_iff f.injective, apply_inv_self]}
+by conv {to_lhs, rw [← injective.eq_iff f.bijective.1, apply_inv_self]}
 
 lemma inv_eq_iff_eq {f : perm α} {x y : α} : f⁻¹ x = y ↔ x = f y :=
 by rw [eq_comm, eq_inv_iff_eq, eq_comm]
@@ -55,8 +55,8 @@ lemma disjoint_comm {f g : perm α} : disjoint f g ↔ disjoint g f :=
 lemma disjoint_mul_comm {f g : perm α} (h : disjoint f g) : f * g = g * f :=
 equiv.ext _ _ $ λ x, (h x).elim
   (λ hf, (h (g x)).elim (λ hg, by simp [mul_apply, hf, hg])
-    (λ hg, by simp [mul_apply, hf, g.injective hg]))
-  (λ hg, (h (f x)).elim (λ hf, by simp [mul_apply, f.injective hf, hg])
+    (λ hg, by simp [mul_apply, hf, g.bijective.1 hg]))
+  (λ hg, (h (f x)).elim (λ hf, by simp [mul_apply, f.bijective.1 hf, hg])
     (λ hf, by simp [mul_apply, hf, hg]))
 
 @[simp] lemma disjoint_one_left (f : perm α) : disjoint 1 f := λ _, or.inl rfl
@@ -135,7 +135,7 @@ lemma gpow_apply_eq_of_apply_apply_eq_self {f : perm α} {x : α} (hffx : f (f x
   ∀ i : ℤ, (f ^ i) x = x ∨ (f ^ i) x = f x
 | (n : ℕ) := pow_apply_eq_of_apply_apply_eq_self hffx n
 | -[1+ n] :=
-  by rw [gpow_neg_succ, inv_eq_iff_eq, ← injective.eq_iff f.injective, ← mul_apply, ← pow_succ,
+  by rw [gpow_neg_succ, inv_eq_iff_eq, ← injective.eq_iff f.bijective.1, ← mul_apply, ← pow_succ,
     eq_comm, inv_eq_iff_eq, ← mul_apply, ← pow_succ', @eq_comm _ x, or.comm];
   exact pow_apply_eq_of_apply_apply_eq_self hffx _
 
@@ -178,7 +178,7 @@ let ⟨⟨x, hx⟩, ⟨y, hy⟩, hxy⟩ := h in
 lemma ne_and_ne_of_swap_mul_apply_ne_self {f : perm α} {x y : α}
   (hy : (swap x (f x) * f) y ≠ y) : f y ≠ y ∧ y ≠ x :=
 begin
-  simp only [swap_apply_def, mul_apply, injective.eq_iff f.injective] at *,
+  simp only [swap_apply_def, mul_apply, injective.eq_iff f.bijective.1] at *,
   by_cases h : f y = x,
   { split; intro; simp * at * },
   { split_ifs at hy; cc }
@@ -291,7 +291,7 @@ lemma sign_bij_aux_inj {n : ℕ} {f : perm (fin n)} : ∀ a b : Σ a : fin n, fi
   rw mem_fin_pairs_lt at *,
   have : ¬b₁ < b₂ := not_lt_of_ge (le_of_lt hb),
   split_ifs at h;
-  simp [*, injective.eq_iff f.injective, sigma.mk.inj_eq] at *
+  simp [*, injective.eq_iff f.bijective.1, sigma.mk.inj_eq] at *
 end
 
 lemma sign_bij_aux_surj {n : ℕ} {f : perm (fin n)} : ∀ a ∈ fin_pairs_lt n,
@@ -303,7 +303,7 @@ then ⟨⟨f⁻¹ a₁, f⁻¹ a₂⟩, mem_fin_pairs_lt.2 hxa,
     rw [apply_inv_self, apply_inv_self, dif_pos (mem_fin_pairs_lt.1 ha)]⟩
 else ⟨⟨f⁻¹ a₂, f⁻¹ a₁⟩, mem_fin_pairs_lt.2 $ lt_of_le_of_ne
   (le_of_not_gt hxa) $ λ h,
-    by simpa [mem_fin_pairs_lt, (f⁻¹).injective h, lt_irrefl] using ha,
+    by simpa [mem_fin_pairs_lt, (f⁻¹).bijective.1 h, lt_irrefl] using ha,
   by dsimp [sign_bij_aux];
     rw [apply_inv_self, apply_inv_self,
       dif_neg (not_lt_of_ge (le_of_lt (mem_fin_pairs_lt.1 ha)))]⟩
@@ -316,7 +316,7 @@ lemma sign_bij_aux_mem {n : ℕ} {f : perm (fin n)}: ∀ a : Σ a : fin n, fin n
   { exact mem_fin_pairs_lt.2 h },
   { exact mem_fin_pairs_lt.2
     (lt_of_le_of_ne (le_of_not_gt h)
-      (λ h, ne_of_lt (mem_fin_pairs_lt.1 ha) (f.injective h.symm))) }
+      (λ h, ne_of_lt (mem_fin_pairs_lt.1 ha) (f.bijective.1 h.symm))) }
 end
 
 @[simp] lemma sign_aux_inv {n : ℕ} (f : perm (fin n)) : sign_aux f⁻¹ = sign_aux f :=
@@ -347,8 +347,8 @@ begin
   { rw [dif_neg h, inv_apply_self, inv_apply_self, if_pos (le_of_lt hab)],
     by_cases h₁ : f (g b) ≤ f (g a),
     { have : f (g b) ≠ f (g a),
-      { rw [ne.def, injective.eq_iff f.injective,
-          injective.eq_iff g.injective];
+      { rw [ne.def, injective.eq_iff f.bijective.1,
+          injective.eq_iff g.bijective.1];
         exact ne_of_lt hab },
       rw [if_pos h₁, if_neg (not_le_of_gt  (lt_of_le_of_ne h₁ this))],
       refl },
@@ -412,7 +412,7 @@ by rw [this, one_def, equiv.trans_refl, equiv.symm_trans, ← one_def,
     have : (e.symm.trans (swap x (f x) * f)).trans e =
       (swap (e x) (e (f x))) * (e.symm.trans f).trans e,
       from equiv.ext _ _ (λ z, by rw ← equiv.symm_trans_swap_trans; simp [mul_def]),
-    have hefx : e x ≠ e (f x), from mt (injective.eq_iff e.injective).1 hfx,
+    have hefx : e x ≠ e (f x), from mt (injective.eq_iff e.bijective.1).1 hfx,
     rw [if_neg hfx, ← sign_aux_eq_sign_aux2 _ _ e hy, this, sign_aux_mul, sign_aux_swap hefx],
     simp }
 end
@@ -441,7 +441,7 @@ begin
   { rw [← sign_aux_eq_sign_aux2 _ _ e (λ _ _, hs _), ← sign_aux_eq_sign_aux2 _ _ e (λ _ _, hs _),
       ← sign_aux_eq_sign_aux2 _ _ e (λ _ _, hs _), hfg, sign_aux_mul] },
   { assume x y hxy,
-    have hexy : e x ≠ e y, from mt (injective.eq_iff e.injective).1 hxy,
+    have hexy : e x ≠ e y, from mt (injective.eq_iff e.bijective.1).1 hxy,
     rw [← sign_aux_eq_sign_aux2 _ _ e (λ _ _, hs _), equiv.symm_trans_swap_trans, sign_aux_swap hexy] }
 end
 
@@ -566,7 +566,7 @@ calc sign f = sign (@subtype_perm _ f (λ x, f x ≠ x) (by simp)) :
   sign_eq_sign_of_equiv _ _
     (equiv.of_bijective
       (show function.bijective (λ x : {x // f x ≠ x},
-        (⟨i x.1 x.2, have f (f x) ≠ f x, from mt (λ h, f.injective h) x.2,
+        (⟨i x.1 x.2, have f (f x) ≠ f x, from mt (λ h, f.bijective.1 h) x.2,
           by rw [← h _ x.2 this]; exact mt (hi _ _ this x.2) x.2⟩ : {y // g y ≠ y})),
         from ⟨λ ⟨x, hx⟩ ⟨y, hy⟩ h, subtype.eq (hi _ _ _ _ (subtype.mk.inj h)),
           λ ⟨y, hy⟩, let ⟨x, hfx, hx⟩ := hg y hy in ⟨⟨x, hfx⟩, subtype.eq hx⟩⟩))
@@ -604,10 +604,10 @@ lemma is_cycle_swap_mul_aux₁ : ∀ (n : ℕ) {b x : α} {f : perm α}
     have f b ≠ b ∧ b ≠ x, from ne_and_ne_of_swap_mul_apply_ne_self hb,
     have hb' : (swap x (f x) * f) (f⁻¹ b) ≠ f⁻¹ b,
       by rw [mul_apply, apply_inv_self, swap_apply_of_ne_of_ne this.2 (ne.symm hfbx),
-          ne.def, ← injective.eq_iff f.injective, apply_inv_self];
+          ne.def, ← injective.eq_iff f.bijective.1, apply_inv_self];
         exact this.1,
     let ⟨i, hi⟩ := is_cycle_swap_mul_aux₁ n hb'
-      (f.injective $
+      (f.bijective.1 $
         by rw [apply_inv_self];
         rwa [pow_succ, mul_apply] at h) in
     ⟨i + 1, by rw [add_comm, gpow_add, mul_apply, hi, gpow_one, mul_apply, apply_inv_self,
@@ -655,7 +655,7 @@ end
 lemma is_cycle_swap_mul {f : perm α} (hf : is_cycle f) {x : α}
   (hx : f x ≠ x) (hffx : f (f x) ≠ x) : is_cycle (swap x (f x) * f) :=
 ⟨f x, by simp only [swap_apply_def, mul_apply];
-        split_ifs; simp [injective.eq_iff f.injective] at *; cc,
+        split_ifs; simp [injective.eq_iff f.bijective.1] at *; cc,
   λ y hy,
   let ⟨i, hi⟩ := exists_gpow_eq_of_is_cycle hf hx (ne_and_ne_of_swap_mul_apply_ne_self hy).1 in
   have hi : (f ^ (i - 1)) (f x) = y, from
@@ -701,7 +701,7 @@ end equiv.perm
 lemma finset.prod_univ_perm [fintype α] [comm_monoid β] {f : α → β} (σ : perm α) :
   (univ : finset α).prod f = univ.prod (λ z, f (σ z)) :=
 eq.symm $ prod_bij (λ z _, σ z) (λ _ _, mem_univ _) (λ _ _, rfl)
-  (λ _ _ _ _ H, σ.injective H) (λ b _, ⟨σ⁻¹ b, mem_univ _, by simp⟩)
+  (λ _ _ _ _ H, σ.bijective.1 H) (λ b _, ⟨σ⁻¹ b, mem_univ _, by simp⟩)
 
 lemma finset.sum_univ_perm [fintype α] [add_comm_monoid β] {f : α → β} (σ : perm α) :
   (univ : finset α).sum f = univ.sum (λ z, f (σ z)) :=
diff --git a/src/linear_algebra/basic.lean b/src/linear_algebra/basic.lean
index 6546037fd42c5..1bd9ac051860a 100644
--- a/src/linear_algebra/basic.lean
+++ b/src/linear_algebra/basic.lean
@@ -1140,10 +1140,10 @@ def of_linear (f : β →ₗ[α] γ) (g : γ →ₗ[α] β)
   (x : γ) : (of_linear f g h₁ h₂).symm x = g x := rfl
 
 @[simp] protected theorem ker (f : β ≃ₗ[α] γ) : (f : β →ₗ[α] γ).ker = ⊥ :=
-linear_map.ker_eq_bot.2 f.to_equiv.injective
+linear_map.ker_eq_bot.2 f.to_equiv.bijective.1
 
 @[simp] protected theorem range (f : β ≃ₗ[α] γ) : (f : β →ₗ[α] γ).range = ⊤ :=
-linear_map.range_eq_top.2 f.to_equiv.surjective
+linear_map.range_eq_top.2 f.to_equiv.bijective.2
 
 def of_top (p : submodule α β) (h : p = ⊤) : p ≃ₗ[α] β :=
 { inv_fun   := λ x, ⟨x, h.symm ▸ trivial⟩,
diff --git a/src/linear_algebra/determinant.lean b/src/linear_algebra/determinant.lean
index 3fb8ae0db79cb..ff67f80ef2d9e 100644
--- a/src/linear_algebra/determinant.lean
+++ b/src/linear_algebra/determinant.lean
@@ -47,10 +47,10 @@ sum_involution
     have ∀ a, p (swap i j a) = p a := λ a, by simp only [swap_apply_def]; split_ifs; cc,
     have univ.prod (λ x, M (σ x) (p x)) = univ.prod (λ x, M ((σ * swap i j) x) (p x)),
       from prod_bij (λ a _, swap i j a) (λ _ _, mem_univ _) (by simp [this])
-        (λ _ _ _ _ h, (swap i j).injective h)
+        (λ _ _ _ _ h, (swap i j).bijective.1 h)
         (λ b _, ⟨swap i j b, mem_univ _, by simp⟩),
     by simp [sign_mul, this, sign_swap hij.2, prod_mul_distrib])
-  (λ σ _ _ h, hij.2 (σ.injective $ by conv {to_lhs, rw ← h}; simp))
+  (λ σ _ _ h, hij.2 (σ.bijective.1 $ by conv {to_lhs, rw ← h}; simp))
   (λ _ _, mem_univ _)
   (λ _ _, equiv.ext _ _ $ by simp)
 
diff --git a/src/linear_algebra/dimension.lean b/src/linear_algebra/dimension.lean
index 25d52009bb8ca..53525436ab287 100644
--- a/src/linear_algebra/dimension.lean
+++ b/src/linear_algebra/dimension.lean
@@ -66,7 +66,7 @@ variables [add_comm_group γ] [vector_space α γ]
 theorem linear_equiv.dim_eq (f : β ≃ₗ[α] γ) : dim α β = dim α γ :=
 let ⟨b, hb⟩ := exists_is_basis α β in
 hb.mk_eq_dim.symm.trans $
-  (cardinal.mk_eq_of_injective f.to_equiv.injective).symm.trans $
+  (cardinal.mk_eq_of_injective f.to_equiv.bijective.1).symm.trans $
 (f.is_basis hb).mk_eq_dim
 
 lemma dim_bot : dim α (⊥ : submodule α β) = 0 :=
diff --git a/src/logic/embedding.lean b/src/logic/embedding.lean
index d134cd7c41eca..2947b56ec6eb7 100644
--- a/src/logic/embedding.lean
+++ b/src/logic/embedding.lean
@@ -22,7 +22,7 @@ instance {α : Sort u} {β : Sort v} : has_coe_to_fun (α ↪ β) := ⟨_, embed
 end function
 
 protected def equiv.to_embedding {α : Sort u} {β : Sort v} (f : α ≃ β) : α ↪ β :=
-⟨f, f.injective⟩
+⟨f, f.bijective.1⟩
 
 @[simp] theorem equiv.to_embedding_coe_fn {α : Sort u} {β : Sort v} (f : α ≃ β) :
   (f.to_embedding : α → β) = f := rfl
diff --git a/src/order/order_iso.lean b/src/order/order_iso.lean
index a4d3e4442edb2..c18d1ca3b61b2 100644
--- a/src/order/order_iso.lean
+++ b/src/order/order_iso.lean
@@ -261,7 +261,7 @@ theorem prod_lex_congr {α₁ α₂ β₁ β₂ r₁ r₂ s₁ s₂}
   { generalize e : f b₁ = fb₁,
     intro h, cases h with _ _ _ _ h _ _ _ h,
     { subst e, left, exact hf.2 h },
-    { have := f.injective e, subst b₁,
+    { have := f.bijective.1 e, subst b₁,
       right, exact hg.2 h } }
 end⟩
 
diff --git a/src/ring_theory/localization.lean b/src/ring_theory/localization.lean
index 445a7bbfb832a..80e78e9b1ef81 100644
--- a/src/ring_theory/localization.lean
+++ b/src/ring_theory/localization.lean
@@ -557,7 +557,7 @@ begin
   rw [equiv.image_eq_preimage, set.preimage, set.mem_set_of_eq,
     mem_non_zero_divisors_iff_ne_zero, mem_non_zero_divisors_iff_ne_zero, ne.def],
   exact ⟨mt (λ h, h.symm ▸ is_ring_hom.map_zero _),
-    mt ((is_add_group_hom.injective_iff _).1 h.to_equiv.symm.injective _)⟩
+    mt ((is_add_group_hom.injective_iff _).1 h.to_equiv.symm.bijective.1 _)⟩
 end
 
 end map
diff --git a/src/ring_theory/noetherian.lean b/src/ring_theory/noetherian.lean
index ea283f3f86fef..896d0b61a5977 100644
--- a/src/ring_theory/noetherian.lean
+++ b/src/ring_theory/noetherian.lean
@@ -367,7 +367,7 @@ instance is_noetherian_ring_range {R} [comm_ring R] {S} [comm_ring S] (f : R →
 
 theorem is_noetherian_ring_of_ring_equiv (R) [comm_ring R] {S} [comm_ring S]
   (f : R ≃r S) [is_noetherian_ring R] : is_noetherian_ring S :=
-is_noetherian_ring_of_surjective R S f.1 f.1.surjective
+is_noetherian_ring_of_surjective R S f.1 f.1.bijective.2
 
 namespace is_noetherian_ring
 
diff --git a/src/set_theory/cofinality.lean b/src/set_theory/cofinality.lean
index 0a8c0a45faec3..a49386ae13fc3 100644
--- a/src/set_theory/cofinality.lean
+++ b/src/set_theory/cofinality.lean
@@ -34,7 +34,7 @@ begin
       -coe_fn_coe_base, -coe_fn_coe_trans, principal_seg.coe_coe_fn', initial_seg.coe_coe_fn]⟩⟩ },
   { exact lift_mk_le.{u v (max u v)}.2
     ⟨⟨λ ⟨x, h⟩, ⟨f x, h⟩, λ ⟨x, h₁⟩ ⟨y, h₂⟩ h₃,
-      by congr; injection h₃ with h'; exact f.to_equiv.injective h'⟩⟩ }
+      by congr; injection h₃ with h'; exact f.to_equiv.bijective.1 h'⟩⟩ }
 end
 
 theorem order_iso.cof {α : Type u} {β : Type v} {r s}
diff --git a/src/topology/constructions.lean b/src/topology/constructions.lean
index e4fa20a5e44f1..b9c2057ad68bf 100644
--- a/src/topology/constructions.lean
+++ b/src/topology/constructions.lean
@@ -917,11 +917,11 @@ lemma compact_preimage {s : set β} (h : α ≃ₜ β) : compact (h ⁻¹' s) 
 by rw ← image_symm; exact h.symm.compact_image
 
 protected lemma embedding (h : α ≃ₜ β) : embedding h :=
-⟨h.to_equiv.injective, h.induced_eq.symm⟩
+⟨h.to_equiv.bijective.1, h.induced_eq.symm⟩
 
 protected lemma dense_embedding (h : α ≃ₜ β) : dense_embedding h :=
 { dense   := assume a, by rw [h.range_coe, closure_univ]; trivial,
-  inj     := h.to_equiv.injective,
+  inj     := h.to_equiv.bijective.1,
   induced := assume a, by rw [← nhds_induced_eq_comap, h.induced_eq] }
 
 protected lemma is_open_map (h : α ≃ₜ β) : is_open_map h :=
@@ -932,7 +932,7 @@ begin
 end
 
 protected lemma quotient_map (h : α ≃ₜ β) : quotient_map h :=
-⟨h.to_equiv.surjective, h.coinduced_eq.symm⟩
+⟨h.to_equiv.bijective.2, h.coinduced_eq.symm⟩
 
 def prod_congr (h₁ : α ≃ₜ β) (h₂ : γ ≃ₜ δ) : (α × γ) ≃ₜ (β × δ) :=
 { continuous_to_fun  :=