chore(*): regularize naming using injective (#3071)

This begins some of the naming regularization discussed at https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/naming.20of.20injectivity.20lemmas

Some general rules:
1. Lemmas should have `injective` in the name iff they have `injective` in the conclusion
2. `X_injective` is preferable to `injective_X`.
3. Unidirectional `inj` lemmas should be dropped in favour of bidirectional ones.

Mostly, this PR tried to fix the names of lemmas that conclude `injective` (also `surjective` and `bijective`, but they seemed to be much better already).

A lot of the changes are from `injective_X` to `X_injective` style 

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

archive/sensitivity.lean

@@ -361,7 +361,7 @@ begin
     apply dim_V },
   have dim_add : dim (W ⊔ img) + dim (W ⊓ img) = dim W + 2^m,
   { convert ← dim_sup_add_dim_inf_eq W img,
-    rw ← dim_eq_injective (g m) g_injective,
+    rw ← dim_eq_of_injective (g m) g_injective,
     apply dim_V },
   have dimW : dim W = card H,
   { have li : linear_independent ℝ (set.restrict e H) :=

src/algebra/big_operators.lean

@@ -932,7 +932,7 @@ begin
     rw [prod_insert ha, pi_insert ha, ih, sum_mul, sum_bind h₁],
     refine sum_congr rfl (λ b _, _),
     have h₂ : ∀p₁∈pi s t, ∀p₂∈pi s t, pi.cons s a b p₁ = pi.cons s a b p₂ → p₁ = p₂, from
-      assume p₁ h₁ p₂ h₂ eq, injective_pi_cons ha eq,
+      assume p₁ h₁ p₂ h₂ eq, pi_cons_injective ha eq,
     rw [sum_image h₂, mul_sum],
     refine sum_congr rfl (λ g _, _),
     rw [attach_insert, prod_insert, prod_image],

src/algebra/direct_limit.lean

@@ -419,7 +419,7 @@ end of_zero_exact
 
 /-- If the maps in the directed system are injective, then the canonical maps
 from the components to the direct limits are injective. -/
-theorem of_inj (hf : ∀ i j hij, function.injective (f i j hij)) (i) :
+theorem of_injective (hf : ∀ i j hij, function.injective (f i j hij)) (i) :
   function.injective (of G f i) :=
 begin
   suffices : ∀ x, of G f i x = 0 → x = 0,

src/algebra/direct_sum.lean

@@ -62,11 +62,11 @@ is_add_group_hom.map_neg _ x
 @[simp] lemma of_sub (i : ι) (x y) : of β i (x - y) = of β i x - of β i y :=
 is_add_group_hom.map_sub _ x y
 
-theorem mk_inj (s : finset ι) : function.injective (mk β s) :=
-dfinsupp.mk_inj s
+theorem mk_injective (s : finset ι) : function.injective (mk β s) :=
+dfinsupp.mk_injective s
 
-theorem of_inj (i : ι) : function.injective (of β i) :=
-λ x y H, congr_fun (mk_inj _ H) ⟨i, by simp⟩
+theorem of_injective (i : ι) : function.injective (of β i) :=
+λ x y H, congr_fun (mk_injective _ H) ⟨i, by simp⟩
 
 @[elab_as_eliminator]
 protected theorem induction_on {C : direct_sum ι β → Prop}

src/algebra/field_power.lean

@@ -134,7 +134,7 @@ div_pos ha (pow_pos hb k)
 (calc a = a * 1 : (mul_one a).symm
    ...  ≤ a*b^k : (mul_le_mul_left ha).mpr $ one_le_pow_of_one_le hb _)
 
-lemma injective_fpow {x : K} (h₀ : 0 < x) (h₁ : x ≠ 1) :
+lemma fpow_injective {x : K} (h₀ : 0 < x) (h₁ : x ≠ 1) :
   function.injective ((^) x : ℤ → K) :=
 begin
   intros m n h,
@@ -149,7 +149,7 @@ end
 
 @[simp] lemma fpow_inj {x : K} (h₀ : 0 < x) (h₁ : x ≠ 1) {m n : ℤ} :
   x ^ m = x ^ n ↔ m = n :=
-(injective_fpow h₀ h₁).eq_iff
+(fpow_injective h₀ h₁).eq_iff
 
 end ordered
 

src/algebra/group/type_tags.lean

@@ -33,17 +33,17 @@ def additive.of_mul (x : α) : additive α := x
 /-- Reinterpret `x : additive α` as an element of `α`. -/
 def additive.to_mul (x : additive α) : α := x
 
-lemma of_mul_inj : function.injective (@additive.of_mul α) := λ _ _, id
-lemma to_mul_inj : function.injective (@additive.to_mul α) := λ _ _, id
+lemma of_mul_injective : function.injective (@additive.of_mul α) := λ _ _, id
+lemma to_mul_injective : function.injective (@additive.to_mul α) := λ _ _, id
 
 /-- Reinterpret `x : α` as an element of `multiplicative α`. -/
 def multiplicative.of_add (x : α) : multiplicative α := x
 
 /-- Reinterpret `x : multiplicative α` as an element of `α`. -/
 def multiplicative.to_add (x : multiplicative α) : α := x
 
-lemma of_add_inj : function.injective (@multiplicative.of_add α) := λ _ _, id
-lemma to_add_inj : function.injective (@multiplicative.to_add α) := λ _ _, id
+lemma of_add_injective : function.injective (@multiplicative.of_add α) := λ _ _, id
+lemma to_add_injective : function.injective (@multiplicative.to_add α) := λ _ _, id
 
 @[simp] lemma to_add_of_add (x : α) : (multiplicative.of_add x).to_add = x := rfl
 @[simp] lemma of_add_to_add (x : multiplicative α) : multiplicative.of_add x.to_add = x := rfl

src/algebra/module.lean

@@ -436,14 +436,14 @@ protected theorem «exists» {q : p → Prop} : (∃ x, q x) ↔ (∃ x ∈ p, q
 
 protected theorem «forall» {q : p → Prop} : (∀ x, q x) ↔ (∀ x ∈ p, q ⟨x, ‹_›⟩) := set_coe.forall
 
-theorem ext' : injective (coe : submodule R M → set M) :=
+theorem coe_injective : injective (coe : submodule R M → set M) :=
 λ p q h, by cases p; cases q; congr'
 
-@[simp, norm_cast] theorem coe_set_eq : (p : set M) = q ↔ p = q := ext'.eq_iff
+@[simp, norm_cast] theorem coe_set_eq : (p : set M) = q ↔ p = q := coe_injective.eq_iff
 
 theorem ext'_iff : p = q ↔ (p : set M) = q := coe_set_eq.symm
 
-@[ext] theorem ext (h : ∀ x, x ∈ p ↔ x ∈ q) : p = q := ext' $ set.ext h
+@[ext] theorem ext (h : ∀ x, x ∈ p ↔ x ∈ q) : p = q := coe_injective $ set.ext h
 
 theorem to_add_submonoid_injective :
   injective (to_add_submonoid : submodule R M → add_submonoid M) :=

src/algebra/opposites.lean

@@ -17,19 +17,19 @@ instance [has_add α] : has_add (opposite α) :=
 { add := λ x y, op (unop x + unop y) }
 
 instance [add_semigroup α] : add_semigroup (opposite α) :=
-{ add_assoc := λ x y z, unop_inj $ add_assoc (unop x) (unop y) (unop z),
+{ add_assoc := λ x y z, unop_injective $ add_assoc (unop x) (unop y) (unop z),
   .. opposite.has_add α }
 
 instance [add_left_cancel_semigroup α] : add_left_cancel_semigroup (opposite α) :=
-{ add_left_cancel := λ x y z H, unop_inj $ add_left_cancel $ op_inj H,
+{ add_left_cancel := λ x y z H, unop_injective $ add_left_cancel $ op_injective H,
   .. opposite.add_semigroup α }
 
 instance [add_right_cancel_semigroup α] : add_right_cancel_semigroup (opposite α) :=
-{ add_right_cancel := λ x y z H, unop_inj $ add_right_cancel $ op_inj H,
+{ add_right_cancel := λ x y z H, unop_injective $ add_right_cancel $ op_injective H,
   .. opposite.add_semigroup α }
 
 instance [add_comm_semigroup α] : add_comm_semigroup (opposite α) :=
-{ add_comm := λ x y, unop_inj $ add_comm (unop x) (unop y),
+{ add_comm := λ x y, unop_injective $ add_comm (unop x) (unop y),
   .. opposite.add_semigroup α }
 
 instance [has_zero α] : has_zero (opposite α) :=
@@ -45,8 +45,8 @@ iff.refl _
 end
 
 instance [add_monoid α] : add_monoid (opposite α) :=
-{ zero_add := λ x, unop_inj $ zero_add $ unop x,
-  add_zero := λ x, unop_inj $ add_zero $ unop x,
+{ zero_add := λ x, unop_injective $ zero_add $ unop x,
+  add_zero := λ x, unop_injective $ add_zero $ unop x,
   .. opposite.add_semigroup α, .. opposite.has_zero α }
 
 instance [add_comm_monoid α] : add_comm_monoid (opposite α) :=
@@ -56,7 +56,7 @@ instance [has_neg α] : has_neg (opposite α) :=
 { neg := λ x, op $ -(unop x) }
 
 instance [add_group α] : add_group (opposite α) :=
-{ add_left_neg := λ x, unop_inj $ add_left_neg $ unop x,
+{ add_left_neg := λ x, unop_injective $ add_left_neg $ unop x,
   .. opposite.add_monoid α, .. opposite.has_neg α }
 
 instance [add_comm_group α] : add_comm_group (opposite α) :=
@@ -66,19 +66,19 @@ instance [has_mul α] : has_mul (opposite α) :=
 { mul := λ x y, op (unop y * unop x) }
 
 instance [semigroup α] : semigroup (opposite α) :=
-{ mul_assoc := λ x y z, unop_inj $ eq.symm $ mul_assoc (unop z) (unop y) (unop x),
+{ mul_assoc := λ x y z, unop_injective $ eq.symm $ mul_assoc (unop z) (unop y) (unop x),
   .. opposite.has_mul α }
 
 instance [right_cancel_semigroup α] : left_cancel_semigroup (opposite α) :=
-{ mul_left_cancel := λ x y z H, unop_inj $ mul_right_cancel $ op_inj H,
+{ mul_left_cancel := λ x y z H, unop_injective $ mul_right_cancel $ op_injective H,
   .. opposite.semigroup α }
 
 instance [left_cancel_semigroup α] : right_cancel_semigroup (opposite α) :=
-{ mul_right_cancel := λ x y z H, unop_inj $ mul_left_cancel $ op_inj H,
+{ mul_right_cancel := λ x y z H, unop_injective $ mul_left_cancel $ op_injective H,
   .. opposite.semigroup α }
 
 instance [comm_semigroup α] : comm_semigroup (opposite α) :=
-{ mul_comm := λ x y, unop_inj $ mul_comm (unop y) (unop x),
+{ mul_comm := λ x y, unop_injective $ mul_comm (unop y) (unop x),
   .. opposite.semigroup α }
 
 instance [has_one α] : has_one (opposite α) :=
@@ -94,8 +94,8 @@ iff.refl _
 end
 
 instance [monoid α] : monoid (opposite α) :=
-{ one_mul := λ x, unop_inj $ mul_one $ unop x,
-  mul_one := λ x, unop_inj $ one_mul $ unop x,
+{ one_mul := λ x, unop_injective $ mul_one $ unop x,
+  mul_one := λ x, unop_injective $ one_mul $ unop x,
   .. opposite.semigroup α, .. opposite.has_one α }
 
 instance [comm_monoid α] : comm_monoid (opposite α) :=
@@ -105,20 +105,20 @@ instance [has_inv α] : has_inv (opposite α) :=
 { inv := λ x, op $ (unop x)⁻¹ }
 
 instance [group α] : group (opposite α) :=
-{ mul_left_inv := λ x, unop_inj $ mul_inv_self $ unop x,
+{ mul_left_inv := λ x, unop_injective $ mul_inv_self $ unop x,
   .. opposite.monoid α, .. opposite.has_inv α }
 
 instance [comm_group α] : comm_group (opposite α) :=
 { .. opposite.group α, .. opposite.comm_monoid α }
 
 instance [distrib α] : distrib (opposite α) :=
-{ left_distrib := λ x y z, unop_inj $ add_mul (unop y) (unop z) (unop x),
-  right_distrib := λ x y z, unop_inj $ mul_add (unop z) (unop x) (unop y),
+{ left_distrib := λ x y z, unop_injective $ add_mul (unop y) (unop z) (unop x),
+  right_distrib := λ x y z, unop_injective $ mul_add (unop z) (unop x) (unop y),
   .. opposite.has_add α, .. opposite.has_mul α }
 
 instance [semiring α] : semiring (opposite α) :=
-{ zero_mul := λ x, unop_inj $ mul_zero $ unop x,
-  mul_zero := λ x, unop_inj $ zero_mul $ unop x,
+{ zero_mul := λ x, unop_injective $ mul_zero $ unop x,
+  mul_zero := λ x, unop_injective $ zero_mul $ unop x,
   .. opposite.add_comm_monoid α, .. opposite.monoid α, .. opposite.distrib α }
 
 instance [ring α] : ring (opposite α) :=
@@ -128,17 +128,17 @@ instance [comm_ring α] : comm_ring (opposite α) :=
 { .. opposite.ring α, .. opposite.comm_semigroup α }
 
 instance [has_zero α] [has_one α] [nonzero α] : nonzero (opposite α) :=
-{ zero_ne_one := λ h : op (0 : α) = op 1, zero_ne_one (op_inj h) }
+{ zero_ne_one := λ h : op (0 : α) = op 1, zero_ne_one (op_injective h) }
 
 instance [integral_domain α] : integral_domain (opposite α) :=
 { eq_zero_or_eq_zero_of_mul_eq_zero := λ x y (H : op (_ * _) = op (0:α)),
-    or.cases_on (eq_zero_or_eq_zero_of_mul_eq_zero $ op_inj H)
-      (λ hy, or.inr $ unop_inj $ hy) (λ hx, or.inl $ unop_inj $ hx),
+    or.cases_on (eq_zero_or_eq_zero_of_mul_eq_zero $ op_injective H)
+      (λ hy, or.inr $ unop_injective $ hy) (λ hx, or.inl $ unop_injective $ hx),
   .. opposite.comm_ring α, .. opposite.nonzero α }
 
 instance [field α] : field (opposite α) :=
-{ mul_inv_cancel := λ x hx, unop_inj $ inv_mul_cancel $ λ hx', hx $ unop_inj hx',
-  inv_zero := unop_inj inv_zero,
+{ mul_inv_cancel := λ x hx, unop_injective $ inv_mul_cancel $ λ hx', hx $ unop_injective hx',
+  inv_zero := unop_injective inv_zero,
   .. opposite.comm_ring α, .. opposite.nonzero α, .. opposite.has_inv α }
 
 @[simp] lemma op_zero [has_zero α] : op (0 : α) = 0 := rfl

src/algebra/pi_instances.lean

@@ -372,17 +372,17 @@ def inl [has_zero β] (a : α) : α × β := (a, 0)
 /-- Right injection function for the inner product -/
 def inr [has_zero α] (b : β) : α × β := (0, b)
 
-lemma injective_inl [has_zero β] : function.injective (inl : α → α × β) :=
+lemma inl_injective [has_zero β] : function.injective (inl : α → α × β) :=
 assume x y h, (prod.mk.inj_iff.mp h).1
 
-lemma injective_inr [has_zero α] : function.injective (inr : β → α × β) :=
+lemma inr_injective [has_zero α] : function.injective (inr : β → α × β) :=
 assume x y h, (prod.mk.inj_iff.mp h).2
 
 @[simp] lemma inl_eq_inl [has_zero β] {a₁ a₂ : α} : (inl a₁ : α × β) = inl a₂ ↔ a₁ = a₂ :=
-iff.intro (assume h, injective_inl h) (assume h, h ▸ rfl)
+iff.intro (assume h, inl_injective h) (assume h, h ▸ rfl)
 
 @[simp] lemma inr_eq_inr [has_zero α] {b₁ b₂ : β} : (inr b₁ : α × β) = inr b₂ ↔ b₁ = b₂ :=
-iff.intro (assume h, injective_inr h) (assume h, h ▸ rfl)
+iff.intro (assume h, inr_injective h) (assume h, h ▸ rfl)
 
 @[simp] lemma inl_eq_inr [has_zero α] [has_zero β] {a : α} {b : β} :
   inl a = inr b ↔ a = 0 ∧ b = 0 :=

src/algebra/ring.lean

@@ -242,10 +242,10 @@ coe_inj (funext h)
 theorem ext_iff {f g : α →+* β} : f = g ↔ ∀ x, f x = g x :=
 ⟨λ h x, h ▸ rfl, λ h, ext h⟩
 
-theorem coe_add_monoid_hom_inj : function.injective (coe : (α →+* β) → (α →+ β)) :=
+theorem coe_add_monoid_hom_injective : function.injective (coe : (α →+* β) → (α →+ β)) :=
 λ f g h, coe_inj $ show ((f : α →+ β) : α → β) = (g : α →+ β), from congr_arg coe_fn h
 
-theorem coe_monoid_hom_inj : function.injective (coe : (α →+* β) → (α →* β)) :=
+theorem coe_monoid_hom_injective : function.injective (coe : (α →+* β) → (α →* β)) :=
 λ f g h, coe_inj $ show ((f : α →* β) : α → β) = (g : α →* β), from congr_arg coe_fn h
 
 /-- Ring homomorphisms map zero to zero. -/

src/analysis/analytic/basic.lean

@@ -570,7 +570,8 @@ def change_origin_summable_aux_j (k : ℕ) :
     → (Σ (k : ℕ) (n : ℕ), {s : finset (fin n) // finset.card s = k}) :=
 λ ⟨n, s, hs⟩, ⟨k, n, s, hs⟩
 
-lemma change_origin_summable_aux_j_inj (k : ℕ) : function.injective (change_origin_summable_aux_j k) :=
+lemma change_origin_summable_aux_j_injective (k : ℕ) :
+  function.injective (change_origin_summable_aux_j k) :=
 begin
   rintros ⟨_, ⟨_, _⟩⟩ ⟨_, ⟨_, _⟩⟩ a,
   simp only [change_origin_summable_aux_j, true_and, eq_self_iff_true, heq_iff_eq, sigma.mk.inj_iff] at a,
@@ -589,7 +590,7 @@ begin
   have S : @summable ℝ _ _ _ ((λ ⟨n, s, hs⟩, ∥(p n).restr s hs x∥ * (r : ℝ) ^ k) :
     (Σ (n : ℕ), {s : finset (fin n) // finset.card s = k}) → ℝ),
   { convert summable.summable_comp_of_injective (p.change_origin_summable_aux2 hr)
-      (change_origin_summable_aux_j_inj k),
+      (change_origin_summable_aux_j_injective k),
     -- again, cleanup that could be done by `tidy`:
     ext ⟨_, ⟨_, _⟩⟩, refl },
   have : (r : ℝ)^k ≠ 0, by simp [pow_ne_zero, nnreal.coe_eq_zero, ne_of_gt rpos],
@@ -640,7 +641,7 @@ begin
     (Σ (n : ℕ), {s : finset (fin n) // finset.card s = k}) → ℝ) :
       by { rw tsum_mul_right, convert p.change_origin_summable_aux3 k h, tidy }
   ... = tsum (A ∘ change_origin_summable_aux_j k) : by { congr, tidy }
-  ... ≤ tsum A : tsum_comp_le_tsum_of_inj SA A_nonneg (change_origin_summable_aux_j_inj k)
+  ... ≤ tsum A : tsum_comp_le_tsum_of_inj SA A_nonneg (change_origin_summable_aux_j_injective k)
 end
 
 -- From this point on, assume that the space is complete, to make sure that series that converge

src/analysis/analytic/composition.lean

@@ -126,7 +126,7 @@ begin
       by rw B,
     suffices C : (function.update v (r j') z) ∘ r = function.update (v ∘ r) j' z,
       by { convert C, exact (c.embedding_comp_inv j).symm },
-    exact function.update_comp_eq_of_injective _ (c.embedding_inj _) _ _ },
+    exact function.update_comp_eq_of_injective _ (c.embedding_injective _) _ _ },
   { simp only [h, function.update_eq_self, function.update_noteq, ne.def, not_false_iff],
     let r : fin (c.blocks_fun k) → fin n := c.embedding k,
     change p (c.blocks_fun k) ((function.update v j z) ∘ r) = p (c.blocks_fun k) (v ∘ r),

src/analysis/normed_space/point_reflection.lean

@@ -26,7 +26,7 @@ variables (R : Type*) {E : Type*}
 lemma equiv.point_reflection_fixed_iff_of_module [ring R] [invertible (2:R)]
   [add_comm_group E] [module R E] {x y : E} :
   (equiv.point_reflection x : E → E) y = y ↔ y = x :=
-equiv.point_reflection_fixed_iff_of_bit0_inj $ λ x y h,
+equiv.point_reflection_fixed_iff_of_bit0_injective $ λ x y h,
 by rw [← one_smul R x, ← one_smul R y, ← inv_of_mul_self (2:R), mul_smul, mul_smul, two_smul,
   two_smul, ← bit0, ← bit0, h]
 

src/category_theory/adjunction/fully_faithful.lean

@@ -35,7 +35,7 @@ instance unit_is_iso_of_L_fully_faithful [full L] [faithful L] : is_iso (adjunct
   hom_inv_id' :=
   begin
     ext, dsimp,
-    apply L.injectivity,
+    apply L.map_injective,
     simp,
   end }.
 
@@ -54,7 +54,7 @@ instance counit_is_iso_of_R_fully_faithful [full R] [faithful R] : is_iso (adjun
   hom_inv_id' :=
   begin
     ext, dsimp,
-    apply R.injectivity,
+    apply R.map_injective,
     simp,
   end }
 

src/category_theory/concrete_category/basic.lean

@@ -82,7 +82,7 @@ local attribute [instance] concrete_category.has_coe_to_fun
 /-- In any concrete category, we can test equality of morphisms by pointwise evaluations.-/
 lemma concrete_category.hom_ext {X Y : C} (f g : X ⟶ Y) (w : ∀ x : X, f x  = g x) : f = g :=
 begin
-  apply faithful.injectivity (forget C),
+  apply faithful.map_injective (forget C),
   ext,
   exact w x,
 end

src/category_theory/concrete_category/bundled_hom.lean

@@ -68,7 +68,7 @@ This instance generates the type-class problem `bundled_hom ?m` (which is why th
               map := λ X Y f, 𝒞.to_fun X.str Y.str f,
               map_id' := λ X, 𝒞.id_to_fun X.str,
               map_comp' := by intros; erw 𝒞.comp_to_fun; refl },
-  forget_faithful := { injectivity' := by intros; apply 𝒞.hom_ext } }
+  forget_faithful := { map_injective' := by intros; apply 𝒞.hom_ext } }
 
 variables {hom}
 local attribute [instance] concrete_category.has_coe_to_fun

src/category_theory/epi_mono.lean

@@ -42,12 +42,12 @@ end
 
 lemma faithful_reflects_epi (F : C ⥤ D) [faithful F] {X Y : C} {f : X ⟶ Y}
   (hf : epi (F.map f)) : epi f :=
-⟨λ Z g h H, F.injectivity $
+⟨λ Z g h H, F.map_injective $
   by rw [←cancel_epi (F.map f), ←F.map_comp, ←F.map_comp, H]⟩
 
 lemma faithful_reflects_mono (F : C ⥤ D) [faithful F] {X Y : C} {f : X ⟶ Y}
   (hf : mono (F.map f)) : mono f :=
-⟨λ Z g h H, F.injectivity $
+⟨λ Z g h H, F.map_injective $
   by rw [←cancel_mono (F.map f), ←F.map_comp, ←F.map_comp, H]⟩
 end
 

src/category_theory/equivalence.lean

@@ -313,7 +313,7 @@ def ess_surj_of_equivalence (F : C ⥤ D) [is_equivalence F] : ess_surj F :=
 
 @[priority 100] -- see Note [lower instance priority]
 instance faithful_of_equivalence (F : C ⥤ D) [is_equivalence F] : faithful F :=
-{ injectivity' := λ X Y f g w,
+{ map_injective' := λ X Y f g w,
   begin
     have p := congr_arg (@category_theory.functor.map _ _ _ _ F.inv _ _) w,
     simpa only [cancel_epi, cancel_mono, is_equivalence.inv_fun_map] using p
@@ -322,21 +322,21 @@ instance faithful_of_equivalence (F : C ⥤ D) [is_equivalence F] : faithful F :
 @[priority 100] -- see Note [lower instance priority]
 instance full_of_equivalence (F : C ⥤ D) [is_equivalence F] : full F :=
 { preimage := λ X Y f, F.fun_inv_id.inv.app X ≫ F.inv.map f ≫ F.fun_inv_id.hom.app Y,
-  witness' := λ X Y f, F.inv.injectivity
+  witness' := λ X Y f, F.inv.map_injective
   (by simpa only [is_equivalence.inv_fun_map, assoc, hom_inv_id_app_assoc, hom_inv_id_app] using comp_id _) }
 
 @[simp] private def equivalence_inverse (F : C ⥤ D) [full F] [faithful F] [ess_surj F] : D ⥤ C :=
 { obj  := λ X, F.obj_preimage X,
   map := λ X Y f, F.preimage ((F.fun_obj_preimage_iso X).hom ≫ f ≫ (F.fun_obj_preimage_iso Y).inv),
-  map_id' := λ X, begin apply F.injectivity, tidy end,
-  map_comp' := λ X Y Z f g, by apply F.injectivity; simp }
+  map_id' := λ X, begin apply F.map_injective, tidy end,
+  map_comp' := λ X Y Z f g, by apply F.map_injective; simp }
 
 def equivalence_of_fully_faithfully_ess_surj
   (F : C ⥤ D) [full F] [faithful F] [ess_surj F] : is_equivalence F :=
 is_equivalence.mk (equivalence_inverse F)
   (nat_iso.of_components
     (λ X, (preimage_iso $ F.fun_obj_preimage_iso $ F.obj X).symm)
-    (λ X Y f, by { apply F.injectivity, obviously }))
+    (λ X Y f, by { apply F.map_injective, obviously }))
   (nat_iso.of_components
     (λ Y, F.fun_obj_preimage_iso Y)
     (by obviously))