doc(set_theory/game/pgame): divide file into sections (#15250)

src/set_theory/game/pgame.lean

@@ -96,6 +96,8 @@ open function relation
 
 universes u
 
+/-! ### Pre-game moves -/
+
 /-- The type of pre-games, before we have quotiented
   by equivalence (`pgame.setoid`). In ZFC, a combinatorial game is constructed from
   two sets of combinatorial games that have been constructed at an earlier
@@ -228,6 +230,8 @@ meta def pgame_wf_tac :=
    subsequent.mk_left, subsequent.mk_right, subsequent.trans]
   { max_depth := 6 }]
 
+/-! ### Basic pre-games -/
+
 /-- The pre-game `zero` is defined by `0 = { | }`. -/
 instance : has_zero pgame := ⟨⟨pempty, pempty, pempty.elim, pempty.elim⟩⟩
 
@@ -249,6 +253,8 @@ instance : has_one pgame := ⟨⟨punit, pempty, λ _, 0, pempty.elim⟩⟩
 instance unique_one_left_moves : unique (left_moves 1) := punit.unique
 instance is_empty_one_right_moves : is_empty (right_moves 1) := pempty.is_empty
 
+/-! ### Pre-game order relations -/
+
 /-- Define simultaneously by mutual induction the `≤` relation and its swapped converse `⧏` on
   pre-games.
 
@@ -675,6 +681,8 @@ begin
   exact lt_or_equiv_or_gt_or_fuzzy x y
 end
 
+/-! ### Relabellings -/
+
 /-- `restricted x y` says that Left always has no more moves in `x` than in `y`,
      and Right always has no more moves in `y` than in `x` -/
 inductive restricted : pgame.{u} → pgame.{u} → Type (u+1)
@@ -785,6 +793,8 @@ def relabel_relabelling {x : pgame} {xl' xr'} (el : x.left_moves ≃ xl') (er :
   x ≡r relabel el er :=
 relabelling.mk el er (λ i, by simp) (λ j, by simp)
 
+/-! ### Negation -/
+
 /-- The negation of `{L | R}` is `{-R | -L}`. -/
 def neg : pgame → pgame
 | ⟨l, r, L, R⟩ := ⟨r, l, λ i, neg (R i), λ i, neg (L i)⟩
@@ -960,6 +970,8 @@ by rw [←neg_equiv_iff, pgame.neg_zero]
 @[simp] theorem zero_fuzzy_neg_iff {x : pgame} : 0 ∥ -x ↔ 0 ∥ x :=
 by rw [←neg_fuzzy_iff, pgame.neg_zero]
 
+/-! ### Addition and subtraction -/
+
 /-- The sum of `x = {xL | xR}` and `y = {yL | yR}` is `{xL + y, x + yL | xR + y, x + yR}`. -/
 instance : has_add pgame.{u} := ⟨λ x y, begin
   induction x with xl xr xL xR IHxl IHxr generalizing y,
@@ -1318,6 +1330,8 @@ theorem lt_iff_sub_pos {x y : pgame} : x < y ↔ 0 < y - x :=
      ... ≤ y + 0 : add_le_add_left (add_left_neg_le_zero x) _
      ... ≤ y : (add_zero_relabelling y).le⟩
 
+/-! ### Special pre-games -/
+
 /-- The pre-game `star`, which is fuzzy with zero. -/
 def star : pgame.{u} := ⟨punit, punit, λ _, 0, λ _, 0⟩