chore(set_theory/*): Fix lint (#13399)

Add missing docstrings and `inhabited` instances or a `nolint` when an `inhabited` instance isn't reasonable.

src/set_theory/cofinality.lean

@@ -92,6 +92,8 @@ theorem rel_iso.cof {α : Type u} {β : Type v} {r s}
   cardinal.lift.{(max u v)} (order.cof s) :=
 le_antisymm (rel_iso.cof.aux f) (rel_iso.cof.aux f.symm)
 
+/-- Cofinality of a strict order `≺`. This is the smallest cardinality of a set `S : set α` such
+that `∀ a, ∃ b ∈ S, ¬ b ≺ a`. -/
 def strict_order.cof (r : α → α → Prop) [h : is_irrefl α r] : cardinal :=
 @order.cof α (λ x y, ¬ r y x) ⟨h.1⟩
 

src/set_theory/game.lean

@@ -535,6 +535,8 @@ inductive inv_ty (l r : Type u) : bool → Type u
 | right₁ : l → inv_ty ff → inv_ty tt
 | right₂ : r → inv_ty tt → inv_ty tt
 
+instance (l r : Type u) : inhabited (inv_ty l r ff) := ⟨inv_ty.zero⟩
+
 /-- Because the two halves of the definition of `inv` produce more elements
 of each side, we have to define the two families inductively.
 This is the function part, defined by recursion on `inv_ty`. -/

src/set_theory/pgame.lean

@@ -31,11 +31,11 @@ pregame `g`, if the predicate holds for every game resulting from making a move,
 for `g`.
 
 While it is often convenient to work "by induction" on pregames, in some situations this becomes
-awkward, so we also define accessor functions `left_moves`, `right_moves`, `move_left` and
-`move_right`. There is a relation `subsequent p q`, saying that `p` can be reached by playing some
-non-empty sequence of moves starting from `q`, an instance `well_founded subsequent`, and a local
-tactic `pgame_wf_tac` which is helpful for discharging proof obligations in inductive proofs relying
-on this relation.
+awkward, so we also define accessor functions `pgame.left_moves`, `pgame.right_moves`,
+`pgame.move_left` and `pgame.move_right`. There is a relation `pgame.subsequent p q`, saying that
+`p` can be reached by playing some non-empty sequence of moves starting from `q`, an instance
+`well_founded subsequent`, and a local tactic `pgame_wf_tac` which is helpful for discharging proof
+obligations in inductive proofs relying on this relation.
 
 ## Order properties
 
@@ -128,10 +128,10 @@ def of_lists (L R : list pgame.{0}) : pgame.{0} :=
 pgame.mk (fin L.length) (fin R.length) (λ i, L.nth_le i i.is_lt) (λ j, R.nth_le j.val j.is_lt)
 
 /-- The indexing type for allowable moves by Left. -/
-def left_moves : pgame → Type u
+@[nolint has_inhabited_instance] def left_moves : pgame → Type u
 | (mk l _ _ _) := l
 /-- The indexing type for allowable moves by Right. -/
-def right_moves : pgame → Type u
+@[nolint has_inhabited_instance] def right_moves : pgame → Type u
 | (mk _ r _ _) := r
 
 /-- The new game after Left makes an allowed move. -/

src/set_theory/zfc.lean

@@ -83,7 +83,7 @@ inductive pSet : Type (u+1)
 namespace pSet
 
 /-- The underlying type of a pre-set -/
-def type : pSet → Type u
+@[nolint has_inhabited_instance] def type : pSet → Type u
 | ⟨α, A⟩ := α
 
 /-- The underlying pre-set family of a pre-set -/