docs(data/subtype): add module docstring (#8900)

Author: YaelDillies

src/data/subtype.lean

@@ -3,14 +3,29 @@ Copyright (c) 2017 Johannes Hölzl. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl
 -/
-import tactic.lint
 import tactic.ext
+import tactic.lint
 import tactic.simps
 
+/-!
+# Subtypes
+
+This file provides basic API for subtypes, which are defined in core.
+
+A subtype is a type made from restricting another type, say `α`, to its elements that satisfy some
+predicate, say `p : α → Prop`. Specifically, it is the type of pairs `⟨val, property⟩` where
+`val : α` and `property : p val`. It is denoted `subtype p` and notation `{val : α // p val}` is
+available.
+
+A subtype has a natural coercion to the parent type, by coercing `⟨val, property⟩` to `val`. As
+such, subtypes can be thought of as bundled sets, the difference being that elements of a set are
+still of type `α` while elements of a subtype aren't.
+-/
+
 open function
 
 namespace subtype
-variables {α : Sort*} {β : Sort*} {γ : Sort*} {p : α → Prop} {q : α → Prop}
+variables {α β γ : Sort*} {p q : α → Prop}
 
 /-- See Note [custom simps projection] -/
 def simps.coe (x : subtype p) : α := x
@@ -29,7 +44,7 @@ lemma prop (x : subtype p) : p x := x.2
 
 /-- An alternative version of `subtype.forall`. This one is useful if Lean cannot figure out `q`
   when using `subtype.forall` from right to left. -/
-protected theorem forall' {q : ∀x, p x → Prop} :
+protected theorem forall' {q : ∀ x, p x → Prop} :
   (∀ x h, q x h) ↔ (∀ x : {a // p a}, q x x.2) :=
 (@subtype.forall _ _ (λ x, q x.1 x.2)).symm
 
@@ -76,10 +91,10 @@ theorem val_injective : injective (@val _ p) :=
 coe_injective
 
 /-- Restrict a (dependent) function to a subtype -/
-def restrict {α} {β : α → Type*} (f : Πx, β x) (p : α → Prop) (x : subtype p) : β x.1 :=
+def restrict {α} {β : α → Type*} (f : Π x, β x) (p : α → Prop) (x : subtype p) : β x.1 :=
 f x
 
-lemma restrict_apply {α} {β : α → Type*} (f : Πx, β x) (p : α → Prop) (x : subtype p) :
+lemma restrict_apply {α} {β : α → Type*} (f : Π x, β x) (p : α → Prop) (x : subtype p) :
   restrict f p x = f x.1 :=
 by refl
 
@@ -91,39 +106,39 @@ lemma restrict_injective {α β} {f : α → β} (p : α → Prop) (h : injectiv
 h.comp coe_injective
 
 /-- Defining a map into a subtype, this can be seen as an "coinduction principle" of `subtype`-/
-@[simps] def coind {α β} (f : α → β) {p : β → Prop} (h : ∀a, p (f a)) : α → subtype p :=
+@[simps] 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))
+theorem coind_injective {α β} {f : α → β} {p : β → Prop} (h : ∀ a, p (f a))
   (hf : injective f) : injective (coind f h) :=
 λ x y hxy, hf $ by apply congr_arg subtype.val hxy
 
-theorem coind_surjective {α β} {f : α → β} {p : β → Prop} (h : ∀a, p (f a))
+theorem coind_surjective {α β} {f : α → β} {p : β → Prop} (h : ∀ a, p (f a))
   (hf : surjective f) : surjective (coind f h) :=
 λ x, let ⟨a, ha⟩ := hf x in ⟨a, coe_injective ha⟩
 
-theorem coind_bijective {α β} {f : α → β} {p : β → Prop} (h : ∀a, p (f a))
+theorem coind_bijective {α β} {f : α → β} {p : β → Prop} (h : ∀ a, p (f a))
   (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. -/
-@[simps] def map {p : α → Prop} {q : β → Prop} (f : α → β) (h : ∀a, p a → q (f a)) :
+@[simps] def map {p : α → Prop} {q : β → Prop} (f : α → β) (h : ∀ a, p a → q (f a)) :
   subtype p → subtype q :=
 λ x, ⟨f x, h x x.prop⟩
 
 theorem map_comp {p : α → Prop} {q : β → Prop} {r : γ → Prop} {x : subtype p}
-  (f : α → β) (h : ∀a, p a → q (f a)) (g : β → γ) (l : ∀a, q a → r (g a)) :
+  (f : α → β) (h : ∀ a, p a → q (f a)) (g : β → γ) (l : ∀ a, q a → r (g a)) :
   map g l (map f h x) = map (g ∘ f) (assume a ha, l (f a) $ h a ha) x :=
 rfl
 
-theorem map_id {p : α → Prop} {h : ∀a, p a → p (id a)} : map (@id α) h = id :=
+theorem map_id {p : α → Prop} {h : ∀ a, p a → p (id a)} : map (@id α) h = id :=
 funext $ assume ⟨v, h⟩, rfl
 
-lemma map_injective {p : α → Prop} {q : β → Prop} {f : α → β} (h : ∀a, p a → q (f a))
+lemma map_injective {p : α → Prop} {q : β → Prop} {f : α → β} (h : ∀ a, p a → q (f a))
   (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))
+lemma map_involutive {p : α → Prop} {f : α → α} (h : ∀ a, p a → p (f a))
   (hf : involutive f) : involutive (map f h) :=
 λ x, subtype.ext (hf x)
 
@@ -155,7 +170,7 @@ end subtype
 
 namespace subtype
 /-! Some facts about sets, which require that `α` is a type. -/
-variables {α : Type*} {β : Type*} {γ : Type*} {p : α → Prop}
+variables {α β γ : Type*} {p : α → Prop}
 
 @[simp] lemma coe_prop {S : set α} (a : {a // a ∈ S}) : ↑a ∈ S := a.prop