chore: capitalise Injective (#501)

We had previously been changing mathport output to write `Function.injective` rather than `Function.Injective`. 

At #498 (comment) @digama0 pointed out that mathport is capitalising correctly here.

This PR re-capitalises `Injective`, `Surjective`, `Bijective`, and `Involutive`, all in the `Function` namespace.

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

Author: kim-em

Mathlib/Algebra/Group/Basic.lean

@@ -143,15 +143,15 @@ section HasInvolutiveInv
 variable [HasInvolutiveInv G] {a b : G}
 
 @[simp, to_additive]
-theorem inv_involutive : Function.involutive (Inv.inv : G → G) :=
+theorem inv_involutive : Function.Involutive (Inv.inv : G → G) :=
   inv_inv
 
 @[simp, to_additive]
-theorem inv_surjective : Function.surjective (Inv.inv : G → G) :=
+theorem inv_surjective : Function.Surjective (Inv.inv : G → G) :=
   inv_involutive.surjective
 
 @[to_additive]
-theorem inv_injective : Function.injective (Inv.inv : G → G) :=
+theorem inv_injective : Function.Injective (Inv.inv : G → G) :=
   inv_involutive.injective
 
 @[simp, to_additive]
@@ -403,11 +403,11 @@ variable [Group G] {a b c d : G}
 theorem div_eq_inv_self : a / b = b⁻¹ ↔ a = 1 := by rw [div_eq_mul_inv, mul_left_eq_self]
 
 @[to_additive]
-theorem mul_left_surjective (a : G) : Function.surjective ((· * ·) a) :=
+theorem mul_left_surjective (a : G) : Function.Surjective ((· * ·) a) :=
   fun x => ⟨a⁻¹ * x, mul_inv_cancel_left a x⟩
 
 @[to_additive]
-theorem mul_right_surjective (a : G) : Function.surjective fun x => x * a := fun x =>
+theorem mul_right_surjective (a : G) : Function.Surjective fun x => x * a := fun x =>
   ⟨x * a⁻¹, inv_mul_cancel_right x a⟩
 
 @[to_additive]
@@ -473,13 +473,13 @@ theorem mul_inv_eq_one : a * b⁻¹ = 1 ↔ a = b := by rw [mul_eq_one_iff_eq_in
 theorem inv_mul_eq_one : a⁻¹ * b = 1 ↔ a = b := by rw [mul_eq_one_iff_eq_inv, inv_inj]
 
 @[to_additive]
-theorem div_left_injective : Function.injective fun a => a / b := by
+theorem div_left_injective : Function.Injective fun a => a / b := by
   -- FIXME this could be by `simpa`, but it fails. This is probably a bug in `simpa`.
   simp only [div_eq_mul_inv]
   exact fun a a' h => mul_left_injective b⁻¹ h
 
 @[to_additive]
-theorem div_right_injective : Function.injective fun a => b / a := by
+theorem div_right_injective : Function.Injective fun a => b / a := by
   -- FIXME see above
   simp only [div_eq_mul_inv]
   exact fun a a' h => inv_injective (mul_right_injective b h)

Mathlib/Algebra/Group/Defs.lean

@@ -177,7 +177,7 @@ theorem mul_left_cancel_iff : a * b = a * c ↔ b = c :=
   ⟨mul_left_cancel, congr_arg _⟩
 
 @[to_additive]
-theorem mul_right_injective (a : G) : Function.injective ((· * ·) a) := fun _ _ => mul_left_cancel
+theorem mul_right_injective (a : G) : Function.Injective ((· * ·) a) := fun _ _ => mul_left_cancel
 
 @[simp, to_additive]
 theorem mul_right_inj (a : G) {b c : G} : a * b = a * c ↔ b = c :=
@@ -215,7 +215,7 @@ theorem mul_right_cancel_iff : b * a = c * a ↔ b = c :=
   ⟨mul_right_cancel, congr_arg (· * a)⟩
 
 @[to_additive]
-theorem mul_left_injective (a : G) : Function.injective (· * a) := fun _ _ => mul_right_cancel
+theorem mul_left_injective (a : G) : Function.Injective (· * a) := fun _ _ => mul_right_cancel
 
 @[simp, to_additive]
 theorem mul_left_inj (a : G) {b c : G} : b * a = c * a ↔ b = c :=
@@ -846,7 +846,7 @@ end Group
 
 @[to_additive]
 theorem Group.toDivInvMonoid_injective {G : Type _} :
-    Function.injective (@Group.toDivInvMonoid G) := by rintro ⟨⟩ ⟨⟩ ⟨⟩; rfl
+    Function.Injective (@Group.toDivInvMonoid G) := by rintro ⟨⟩ ⟨⟩ ⟨⟩; rfl
 
 /-- An additive commutative group is an additive group with commutative `(+)`. -/
 class AddCommGroup (G : Type u) extends AddGroup G, AddCommMonoid G
@@ -860,7 +860,7 @@ attribute [to_additive AddCommGroup.toAddCommMonoid] CommGroup.toCommMonoid
 attribute [instance] AddCommGroup.toAddCommMonoid
 
 @[to_additive]
-theorem CommGroup.toGroup_injective {G : Type u} : Function.injective (@CommGroup.toGroup G) := by
+theorem CommGroup.toGroup_injective {G : Type u} : Function.Injective (@CommGroup.toGroup G) := by
   rintro ⟨⟩ ⟨⟩ ⟨⟩; rfl
 
 section CommGroup

Mathlib/Data/List/Basic.lean

@@ -28,7 +28,7 @@ namespace List
 -- instance : is_associative (List α) has_append.append :=
 -- ⟨ append_assoc ⟩
 
-@[simp] theorem cons_injective {a : α} : injective (cons a) :=
+@[simp] theorem cons_injective {a : α} : Injective (cons a) :=
 λ _ _ Pe => tail_eq_of_cons_eq Pe
 
 /-! ### mem -/
@@ -53,7 +53,7 @@ fun p1 p2 => fun Pain => absurd (eq_or_mem_of_mem_cons Pain) (not_or.mpr ⟨p1,
 theorem ne_and_not_mem_of_not_mem_cons {a y : α} {l : List α} : (a ∉ y::l) → a ≠ y ∧ a ∉ l :=
 fun p => And.intro (ne_of_not_mem_cons p) (not_mem_of_not_mem_cons p)
 
-theorem mem_map_of_injective {f : α → β} (H : injective f) {a : α} {l : List α} :
+theorem mem_map_of_injective {f : α → β} (H : Injective f) {a : α} {l : List α} :
   f a ∈ map f l ↔ a ∈ l :=
 ⟨fun m => let ⟨_, m', e⟩ := exists_of_mem_map m
           H e ▸ m', mem_map_of_mem _⟩
@@ -78,7 +78,7 @@ lemma exists_of_length_succ {n} :
 | h :: t, _ => ⟨h, t, rfl⟩
 
 @[simp]
-lemma length_injective_iff : injective (List.length : List α → ℕ) ↔ Subsingleton α := by
+lemma length_injective_iff : Injective (List.length : List α → ℕ) ↔ Subsingleton α := by
   constructor
   · intro h; refine ⟨λ x y => ?_⟩; (suffices [x] = [y] by simpa using this); apply h; rfl
   · intros hα l1 l2 hl
@@ -91,7 +91,7 @@ lemma length_injective_iff : injective (List.length : List α → ℕ) ↔ Subsi
                              · apply ih; simpa using hl
 
 @[simp default+1]
-lemma length_injective [Subsingleton α] : injective (length : List α → ℕ) :=
+lemma length_injective [Subsingleton α] : Injective (length : List α → ℕ) :=
 length_injective_iff.mpr inferInstance
 
 /-! ### set-theoretic notation of Lists -/
@@ -173,10 +173,10 @@ theorem append_left_cancel {s t₁ t₂ : List α} (h : s ++ t₁ = s ++ t₂) :
 theorem append_right_cancel {s₁ s₂ t : List α} (h : s₁ ++ t = s₂ ++ t) : s₁ = s₂ :=
   (append_left_inj _).1 h
 
-theorem append_right_injective (s : List α) : injective fun t => s ++ t :=
+theorem append_right_injective (s : List α) : Injective fun t => s ++ t :=
 fun _ _ => append_left_cancel
 
-theorem append_left_injective (t : List α) : injective fun s => s ++ t :=
+theorem append_left_injective (t : List α) : Injective fun s => s ++ t :=
 fun _ _ => append_right_cancel
 
 /-! ### nth element -/

Mathlib/Data/List/Nodup.lean

@@ -20,7 +20,7 @@ theorem Nodup.map_on {f : α → β} (H : ∀ x ∈ l, ∀ y ∈ l, f x = f y 
     (map f l).Nodup :=
   Pairwise.map _ (fun a b ⟨ma, mb, n⟩ e => n (H a ma b mb e)) (Pairwise.and_mem.1 d)
 
-protected theorem Nodup.map {f : α → β} (hf : Function.injective f) : Nodup l → Nodup (map f l) :=
+protected theorem Nodup.map {f : α → β} (hf : Function.Injective f) : Nodup l → Nodup (map f l) :=
   Nodup.map_on fun _ _ _ _ h => hf h
 
 theorem Nodup.of_map (f : α → β) {l : List α} : Nodup (map f l) → Nodup l :=

Mathlib/Data/Option/Basic.lean

@@ -9,11 +9,11 @@ import Mathlib.Logic.Basic
 
 namespace Option
 
-theorem some_injective (α : Type _) : Function.injective (@some α) :=
+theorem some_injective (α : Type _) : Function.Injective (@some α) :=
   fun _ _ => some_inj.mp
 
 /-- `option.map f` is injective if `f` is injective. -/
-theorem map_injective {f : α → β} (Hf : Function.injective f) : Function.injective (Option.map f)
+theorem map_injective {f : α → β} (Hf : Function.Injective f) : Function.Injective (Option.map f)
 | none, none, _ => rfl
 | some a₁, some a₂, H => by rw [Hf (Option.some.inj H)]
 

Mathlib/Data/Prod.lean

@@ -68,11 +68,11 @@ theorem mk.inj_iff {a₁ a₂ : α} {b₁ b₂ : β} : (a₁, b₁) = (a₂, b
  by intro hab; rw [hab.left, hab.right]⟩
 
 lemma mk.inj_left {α β : Type _} (a : α) :
-  Function.injective (Prod.mk a : β → α × β) :=
+  Function.Injective (Prod.mk a : β → α × β) :=
 fun _ _ h => (Prod.mk.inj h).right
 
 lemma mk.inj_right {α β : Type _} (b : β) :
-  Function.injective (λ a => Prod.mk a b : α → α × β) :=
+  Function.Injective (λ a => Prod.mk a b : α → α × β) :=
 fun _ _ h => (Prod.mk.inj h).left
 
 -- Port note: this lemma comes from lean3/library/init/data/prod.lean.
@@ -94,16 +94,16 @@ by ext <;> simp
 lemma id_prod : (λ (p : α × α) => (p.1, p.2)) = id :=
 funext $ λ ⟨_, _⟩ => rfl
 
-lemma fst_surjective [h : Nonempty β] : Function.surjective (@fst α β) :=
+lemma fst_surjective [h : Nonempty β] : Function.Surjective (@fst α β) :=
 λ x => h.elim $ λ y => ⟨⟨x, y⟩, rfl⟩
 
-lemma snd_surjective [h : Nonempty α] : Function.surjective (@snd α β) :=
+lemma snd_surjective [h : Nonempty α] : Function.Surjective (@snd α β) :=
 λ y => h.elim $ λ x => ⟨⟨x, y⟩, rfl⟩
 
-lemma fst_injective [Subsingleton β] : Function.injective (@fst α β) :=
+lemma fst_injective [Subsingleton β] : Function.Injective (@fst α β) :=
 λ x y h => ext' h (Subsingleton.elim x.snd y.snd)
 
-lemma snd_injective [Subsingleton α] : Function.injective (@snd α β) :=
+lemma snd_injective [Subsingleton α] : Function.Injective (@snd α β) :=
 λ _ _ h => ext' (Subsingleton.elim _ _) h
 
 /-- Swap the factors of a product. `swap (a, b) = (b, a)` -/
@@ -127,13 +127,13 @@ swap_swap
 lemma swap_RightInverse : Function.RightInverse (@swap α β) swap :=
 swap_swap
 
-lemma swap_injective : Function.injective (@swap α β) :=
+lemma swap_injective : Function.Injective (@swap α β) :=
 swap_LeftInverse.injective
 
-lemma swap_surjective : Function.surjective (@swap α β) :=
+lemma swap_surjective : Function.Surjective (@swap α β) :=
 Function.RightInverse.surjective swap_LeftInverse
 
-lemma swap_bijective : Function.bijective (@swap α β) :=
+lemma swap_bijective : Function.Bijective (@swap α β) :=
 ⟨swap_injective, swap_surjective⟩
 
 @[simp] lemma swap_inj {p q : α × β} : swap p = swap q ↔ p = q :=
@@ -167,17 +167,17 @@ end Prod
 
 open Function
 
-lemma Function.injective.prod_map {f : α → γ} {g : β → δ} (hf : injective f) (hg : injective g) :
-  injective (Prod.map f g) :=
+lemma Function.Injective.prod_map {f : α → γ} {g : β → δ} (hf : Injective f) (hg : Injective g) :
+  Injective (Prod.map f g) :=
 by intros x y h
    have h1 := (Prod.ext_iff.1 h).1
    rw [Prod.map_fst, Prod.map_fst] at h1
    have h2 := (Prod.ext_iff.1 h).2
    rw [Prod.map_snd, Prod.map_snd] at h2
    exact Prod.ext' (hf h1) (hg h2)
 
-lemma Function.surjective.prod_map {f : α → γ} {g : β → δ} (hf : surjective f) (hg : surjective g) :
-  surjective (Prod.map f g) :=
+lemma Function.Surjective.prod_map {f : α → γ} {g : β → δ} (hf : Surjective f) (hg : Surjective g) :
+  Surjective (Prod.map f g) :=
 λ p => let ⟨x, hx⟩ := hf p.1
        let ⟨y, hy⟩ := hg p.2
        ⟨(x, y), Prod.ext' hx hy⟩

Mathlib/Data/Sigma/Basic.lean

@@ -90,31 +90,31 @@ def map (f₁ : α₁ → α₂) (f₂ : ∀ a, β₁ a → β₂ (f₁ a)) (x :
 
 end Sigma
 
-theorem sigma_mk_injective {i : α} : Function.injective (@Sigma.mk α β i)
+theorem sigma_mk_injective {i : α} : Function.Injective (@Sigma.mk α β i)
   | _, _, rfl => rfl
 
-theorem Function.injective.sigma_map {f₁ : α₁ → α₂} {f₂ : ∀ a, β₁ a → β₂ (f₁ a)}
-  (h₁ : Function.injective f₁) (h₂ : ∀ a, Function.injective (f₂ a)) :
-    Function.injective (Sigma.map f₁ f₂)
+theorem Function.Injective.sigma_map {f₁ : α₁ → α₂} {f₂ : ∀ a, β₁ a → β₂ (f₁ a)}
+  (h₁ : Function.Injective f₁) (h₂ : ∀ a, Function.Injective (f₂ a)) :
+    Function.Injective (Sigma.map f₁ f₂)
   | ⟨i, x⟩, ⟨j, y⟩, h => by
     obtain rfl : i = j := h₁ (Sigma.mk.inj_iff.mp h).1
     obtain rfl : x = y := h₂ i (sigma_mk_injective h)
     rfl
 
-theorem Function.injective.of_sigma_map {f₁ : α₁ → α₂} {f₂ : ∀ a, β₁ a → β₂ (f₁ a)}
-    (h : Function.injective (Sigma.map f₁ f₂)) (a : α₁) : Function.injective (f₂ a) :=
+theorem Function.Injective.of_sigma_map {f₁ : α₁ → α₂} {f₂ : ∀ a, β₁ a → β₂ (f₁ a)}
+    (h : Function.Injective (Sigma.map f₁ f₂)) (a : α₁) : Function.Injective (f₂ a) :=
   fun x y hxy =>
   sigma_mk_injective <| @h ⟨a, x⟩ ⟨a, y⟩ (Sigma.ext rfl (heq_of_eq hxy))
 
-theorem Function.injective.sigma_map_iff {f₁ : α₁ → α₂} {f₂ : ∀ a, β₁ a → β₂ (f₁ a)}
-  (h₁ : Function.injective f₁) :
-    Function.injective (Sigma.map f₁ f₂) ↔ ∀ a, Function.injective (f₂ a) :=
+theorem Function.Injective.sigma_map_iff {f₁ : α₁ → α₂} {f₂ : ∀ a, β₁ a → β₂ (f₁ a)}
+  (h₁ : Function.Injective f₁) :
+    Function.Injective (Sigma.map f₁ f₂) ↔ ∀ a, Function.Injective (f₂ a) :=
   ⟨fun h => h.of_sigma_map, h₁.sigma_map⟩
 
-theorem Function.surjective.sigma_map {f₁ : α₁ → α₂} {f₂ : ∀ a, β₁ a → β₂ (f₁ a)}
-  (h₁ : Function.surjective f₁) (h₂ : ∀ a, Function.surjective (f₂ a)) :
-    Function.surjective (Sigma.map f₁ f₂) := by
-  simp only [Function.surjective, Sigma.forall, h₁.forall]
+theorem Function.Surjective.sigma_map {f₁ : α₁ → α₂} {f₂ : ∀ a, β₁ a → β₂ (f₁ a)}
+  (h₁ : Function.Surjective f₁) (h₂ : ∀ a, Function.Surjective (f₂ a)) :
+    Function.Surjective (Sigma.map f₁ f₂) := by
+  simp only [Function.Surjective, Sigma.forall, h₁.forall]
   exact fun i => (h₂ _).forall.2 fun x => ⟨⟨i, x⟩, rfl⟩
 
 /-- Interpret a function on `Σ x : α, β x` as a dependent function with two arguments.

Mathlib/Data/Subtype.lean

@@ -70,11 +70,11 @@ ext_iff
 theorem coe_eq_iff {a : {a // p a}} {b : α} : ↑a = b ↔ ∃ h, a = ⟨b, h⟩ :=
 ⟨λ h => h ▸ ⟨a.2, (coe_eta _ _).symm⟩, λ ⟨_, ha⟩ => ha.symm ▸ rfl⟩
 
-theorem coe_injective : injective ((↑·) : Subtype p → α) :=
+theorem coe_injective : Injective ((↑·) : Subtype p → α) :=
 by intros a b hab
    exact Subtype.ext hab
 
-theorem val_injective : injective (@val _ p) :=
+theorem val_injective : Injective (@val _ p) :=
 coe_injective
 
 /-- Restrict a (dependent) function to a subtype -/
@@ -87,27 +87,27 @@ lemma restrict_apply {α} {β : α → Type _} (f : ∀x, β x) (p : α → Prop
 -- FIXME: replace Subtype.val with (↑)
 lemma restrict_def {α β} (f : α → β) (p : α → Prop) : restrict f p = f ∘ Subtype.val := rfl
 
-lemma restrict_injective {α β} {f : α → β} (p : α → Prop) (h : injective f) :
-  injective (restrict f p) :=
+lemma restrict_injective {α β} {f : α → β} (p : α → Prop) (h : Injective f) :
+  Injective (restrict f p) :=
 h.comp coe_injective
 
 /-- Defining a map into a subtype, this can be seen as an "coinduction principle" of `Subtype`-/
 def coind {α β} (f : α → β) {p : β → Prop} (h : ∀a, p (f a)) : α → Subtype p :=
 λ a => ⟨f a, h a⟩
 
 theorem coind_injective {α β} {f : α → β} {p : β → Prop} (h : ∀a, p (f a))
-  (hf : injective f) : injective (coind f h) :=
+  (hf : Injective f) : Injective (coind f h) :=
 by intros x y hxy
    refine hf ?_
    apply congrArg Subtype.val hxy
 
 theorem coind_surjective {α β} {f : α → β} {p : β → Prop} (h : ∀a, p (f a))
-  (hf : surjective f) : surjective (coind f h) :=
+  (hf : Surjective f) : Surjective (coind f h) :=
 λ x => let ⟨a, ha⟩ := hf x
        ⟨a, coe_injective ha⟩
 
 theorem coind_bijective {α β} {f : α → β} {p : β → Prop} (h : ∀a, p (f a))
-  (hf : bijective f) : bijective (coind f h) :=
+  (hf : Bijective f) : Bijective (coind f h) :=
 ⟨coind_injective h hf.1, coind_surjective h hf.2⟩
 
 /-- Restriction of a function to a function on subtypes. -/
@@ -124,11 +124,11 @@ theorem map_id {p : α → Prop} {h : ∀a, p a → p (id a)} : map (@id α) h =
 funext fun ⟨_, _⟩ => rfl
 
 lemma map_injective {p : α → Prop} {q : β → Prop} {f : α → β} (h : ∀a, p a → q (f a))
-  (hf : injective f) : injective (map f h) :=
+  (hf : Injective f) : Injective (map f h) :=
 coind_injective _ $ hf.comp coe_injective
 
 lemma map_involutive {p : α → Prop} {f : α → α} (h : ∀a, p a → p (f a))
-  (hf : involutive f) : involutive (map f h) :=
+  (hf : Involutive f) : Involutive (map f h) :=
 λ x => Subtype.ext (hf x)
 
 instance [HasEquiv α] (p : α → Prop) : HasEquiv (Subtype p) :=