From dc1525fb3ef6eb4348fb1749c302d8abc303d34a Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= <yael.dillies@gmail.com>
Date: Fri, 31 Dec 2021 07:44:08 +0000
Subject: [PATCH] docs(data/sum/basic): Expand module docstring and cleanup
 (#11158)

This moves `data.sum` to `data.sum.basic`, provides a proper docstring for it, cleans it up.

There are no new declarations, just some file rearrangement, variable grouping, unindentation, and a `protected` attribute for `sum.lex.inl`/`sum.lex.inr` to avoid them clashing with `sum.inl`/`sum.inr`.
---
 src/control/bifunctor.lean            |   4 +-
 src/data/equiv/basic.lean             |  13 +-
 src/data/{sum.lean => sum/basic.lean} | 221 ++++++++++++++------------
 src/order/rel_classes.lean            |   2 +-
 src/tactic/fresh_names.lean           |   4 +-
 test/simps.lean                       |   2 +-
 6 files changed, 131 insertions(+), 115 deletions(-)
 rename src/data/{sum.lean => sum/basic.lean} (51%)

diff --git a/src/control/bifunctor.lean b/src/control/bifunctor.lean
index 5fec3f99dacf7..356eab1bda53a 100644
--- a/src/control/bifunctor.lean
+++ b/src/control/bifunctor.lean
@@ -3,10 +3,8 @@ Copyright (c) 2018 Simon Hudon. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Simon Hudon
 -/
-import data.sum
-import logic.function.basic
 import control.functor
-import tactic.core
+import data.sum.basic
 
 /-!
 # Functors with two arguments
diff --git a/src/data/equiv/basic.lean b/src/data/equiv/basic.lean
index 545bb74dc003f..73c5a7b6db0a2 100644
--- a/src/data/equiv/basic.lean
+++ b/src/data/equiv/basic.lean
@@ -4,16 +4,15 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura, Mario Carneiro
 -/
 import data.option.basic
-import data.sum
-import logic.unique
-import logic.function.basic
-import data.quot
-import tactic.simps
-import logic.function.conjugate
 import data.prod
-import tactic.norm_cast
+import data.quot
 import data.sigma.basic
+import data.sum.basic
 import data.subtype
+import logic.function.conjugate
+import logic.unique
+import tactic.norm_cast
+import tactic.simps
 
 /-!
 # Equivalence between types
diff --git a/src/data/sum.lean b/src/data/sum/basic.lean
similarity index 51%
rename from src/data/sum.lean
rename to src/data/sum/basic.lean
index 7953f2e869491..3b93b01fa46fc 100644
--- a/src/data/sum.lean
+++ b/src/data/sum/basic.lean
@@ -4,41 +4,46 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro, Yury G. Kudryashov
 -/
 import logic.function.basic
+import tactic.protected
 
 /-!
-# More theorems about the sum type
--/
+# Disjoint union of types
 
-universes u v w x
-variables {α : Type u} {α' : Type w} {β : Type v} {β' : Type x}
-open sum
+This file proves basic results about the sum type `α ⊕ β`.
 
-/-- Check if a sum is `inl` and if so, retrieve its contents. -/
-@[simp] def sum.get_left {α β} : α ⊕ β → option α
-| (inl a) := some a
-| (inr _) := none
+`α ⊕ β` is the type made of a copy of `α` and a copy of `β`. It is also called *disjoint union*.
 
-/-- Check if a sum is `inr` and if so, retrieve its contents. -/
-@[simp] def sum.get_right {α β} : α ⊕ β → option β
-| (inr b) := some b
-| (inl _) := none
+## Main declarations
 
-/-- Check if a sum is `inl`. -/
-@[simp] def sum.is_left {α β} : α ⊕ β → bool
-| (inl _) := tt
-| (inr _) := ff
+* `sum.get_left`: Retrieves the left content of `x : α ⊕ β` or returns `none` if it's coming from
+  the right.
+* `sum.get_right`: Retrieves the right content of `x : α ⊕ β` or returns `none` if it's coming from
+  the left.
+* `sum.is_left`: Returns whether `x : α ⊕ β` comes from the left component or not.
+* `sum.is_right`: Returns whether `x : α ⊕ β` comes from the right component or not.
+* `sum.map`: Maps `α ⊕ β` to `γ ⊕ δ` component-wise.
+* `sum.elim`: Nondependent eliminator/induction principle for `α ⊕ β`.
+* `sum.swap`: Maps `α ⊕ β` to `β ⊕ α` by swapping components.
+* `sum.lex`: Lexicographic order on `α ⊕ β` induced by a relation on `α` and a relation on `β`.
 
-/-- Check if a sum is `inr`. -/
-@[simp] def sum.is_right {α β} : α ⊕ β → bool
-| (inl _) := ff
-| (inr _) := tt
+## Notes
+
+The definition of `sum` takes values in `Type*`. This effectively forbids `Prop`- valued sum types.
+To this effect, we have `psum`, which takes value in `Sort*` and carries a more complicated
+universe signature in consequence. The `Prop` version is `or`.
+-/
+
+universes u v w x
+variables {α : Type u} {α' : Type w} {β : Type v} {β' : Type x} {γ δ : Type*}
+
+namespace sum
 
 attribute [derive decidable_eq] sum
 
-@[simp] theorem sum.forall {p : α ⊕ β → Prop} : (∀ x, p x) ↔ (∀ a, p (inl a)) ∧ (∀ b, p (inr b)) :=
+@[simp] lemma «forall» {p : α ⊕ β → Prop} : (∀ x, p x) ↔ (∀ a, p (inl a)) ∧ ∀ b, p (inr b) :=
 ⟨λ h, ⟨λ a, h _, λ b, h _⟩, λ ⟨h₁, h₂⟩, sum.rec h₁ h₂⟩
 
-@[simp] theorem sum.exists {p : α ⊕ β → Prop} : (∃ x, p x) ↔ (∃ a, p (inl a)) ∨ ∃ b, p (inr b) :=
+@[simp] lemma «exists» {p : α ⊕ β → Prop} : (∃ x, p x) ↔ (∃ a, p (inl a)) ∨ ∃ b, p (inr b) :=
 ⟨λ h, match h with
 | ⟨inl a, h⟩ := or.inl ⟨a, h⟩
 | ⟨inr b, h⟩ := or.inr ⟨b, h⟩
@@ -47,18 +52,37 @@ end, λ h, match h with
 | or.inr ⟨b, h⟩ := ⟨inr b, h⟩
 end⟩
 
-namespace sum
+lemma inl_injective : function.injective (inl : α → α ⊕ β) := λ x y, inl.inj
+lemma inr_injective : function.injective (inr : β → α ⊕ β) := λ x y, inr.inj
+
+section get
+
+/-- Check if a sum is `inl` and if so, retrieve its contents. -/
+@[simp] def get_left : α ⊕ β → option α
+| (inl a) := some a
+| (inr _) := none
 
-lemma inl_injective : function.injective (sum.inl : α → α ⊕ β) :=
-λ x y, sum.inl.inj
+/-- Check if a sum is `inr` and if so, retrieve its contents. -/
+@[simp] def get_right : α ⊕ β → option β
+| (inr b) := some b
+| (inl _) := none
+
+/-- Check if a sum is `inl`. -/
+@[simp] def is_left : α ⊕ β → bool
+| (inl _) := tt
+| (inr _) := ff
+
+/-- Check if a sum is `inr`. -/
+@[simp] def is_right : α ⊕ β → bool
+| (inl _) := ff
+| (inr _) := tt
 
-lemma inr_injective : function.injective (sum.inr : β → α ⊕ β) :=
-λ x y, sum.inr.inj
+end get
 
 /-- Map `α ⊕ β` to `α' ⊕ β'` sending `α` to `α'` and `β` to `β'`. -/
 protected def map (f : α → α') (g : β → β')  : α ⊕ β → α' ⊕ β'
-| (sum.inl x) := sum.inl (f x)
-| (sum.inr x) := sum.inr (g x)
+| (inl x) := inl (f x)
+| (inr x) := inr (g x)
 
 @[simp] lemma map_inl (f : α → α') (g : β → β') (x : α) : (inl x).map f g = inl (f x) := rfl
 @[simp] lemma map_inr (f : α → α') (g : β → β') (x : β) : (inr x).map f g = inr (g x) := rfl
@@ -114,127 +138,124 @@ funext $ λ x, sum.cases_on x (λ _, rfl) (λ _, rfl)
 
 open function (update update_eq_iff update_comp_eq_of_injective update_comp_eq_of_forall_ne)
 
-@[simp] lemma update_elim_inl {α β γ} [decidable_eq α] [decidable_eq (α ⊕ β)]
-  {f : α → γ} {g : β → γ} {i : α} {x : γ} :
+@[simp] lemma update_elim_inl [decidable_eq α] [decidable_eq (α ⊕ β)] {f : α → γ} {g : β → γ}
+  {i : α} {x : γ} :
   update (sum.elim f g) (inl i) x = sum.elim (update f i x) g :=
 update_eq_iff.2 ⟨by simp, by simp { contextual := tt }⟩
 
-@[simp] lemma update_elim_inr {α β γ} [decidable_eq β] [decidable_eq (α ⊕ β)]
-  {f : α → γ} {g : β → γ} {i : β} {x : γ} :
+@[simp] lemma update_elim_inr [decidable_eq β] [decidable_eq (α ⊕ β)] {f : α → γ} {g : β → γ}
+  {i : β} {x : γ} :
   update (sum.elim f g) (inr i) x = sum.elim f (update g i x) :=
 update_eq_iff.2 ⟨by simp, by simp { contextual := tt }⟩
 
-@[simp] lemma update_inl_comp_inl {α β γ} [decidable_eq α] [decidable_eq (α ⊕ β)]
-  {f : α ⊕ β → γ} {i : α} {x : γ} :
+@[simp] lemma update_inl_comp_inl [decidable_eq α] [decidable_eq (α ⊕ β)] {f : α ⊕ β → γ} {i : α}
+  {x : γ} :
   update f (inl i) x ∘ inl = update (f ∘ inl) i x :=
 update_comp_eq_of_injective _ inl_injective _ _
 
-@[simp] lemma update_inl_apply_inl {α β γ} [decidable_eq α] [decidable_eq (α ⊕ β)]
-  {f : α ⊕ β → γ} {i j : α} {x : γ} :
+@[simp] lemma update_inl_apply_inl [decidable_eq α] [decidable_eq (α ⊕ β)] {f : α ⊕ β → γ}
+  {i j : α} {x : γ} :
   update f (inl i) x (inl j) = update (f ∘ inl) i x j :=
 by rw ← update_inl_comp_inl
 
-@[simp] lemma update_inl_comp_inr {α β γ} [decidable_eq (α ⊕ β)]
-  {f : α ⊕ β → γ} {i : α} {x : γ} :
+@[simp] lemma update_inl_comp_inr [decidable_eq (α ⊕ β)] {f : α ⊕ β → γ} {i : α} {x : γ} :
   update f (inl i) x ∘ inr = f ∘ inr :=
 update_comp_eq_of_forall_ne _ _ $ λ _, inr_ne_inl
 
-@[simp] lemma update_inl_apply_inr {α β γ} [decidable_eq (α ⊕ β)]
-  {f : α ⊕ β → γ} {i : α} {j : β} {x : γ} :
+@[simp] lemma update_inl_apply_inr [decidable_eq (α ⊕ β)] {f : α ⊕ β → γ} {i : α} {j : β} {x : γ} :
   update f (inl i) x (inr j) = f (inr j) :=
 function.update_noteq inr_ne_inl _ _
 
-@[simp] lemma update_inr_comp_inl {α β γ} [decidable_eq (α ⊕ β)]
-  {f : α ⊕ β → γ} {i : β} {x : γ} :
+@[simp] lemma update_inr_comp_inl [decidable_eq (α ⊕ β)] {f : α ⊕ β → γ} {i : β} {x : γ} :
   update f (inr i) x ∘ inl = f ∘ inl :=
 update_comp_eq_of_forall_ne _ _ $ λ _, inl_ne_inr
 
-@[simp] lemma update_inr_apply_inl {α β γ} [decidable_eq (α ⊕ β)]
-  {f : α ⊕ β → γ} {i : α} {j : β} {x : γ} :
+@[simp] lemma update_inr_apply_inl [decidable_eq (α ⊕ β)] {f : α ⊕ β → γ} {i : α} {j : β} {x : γ} :
   update f (inr j) x (inl i) = f (inl i) :=
 function.update_noteq inl_ne_inr _ _
 
-@[simp] lemma update_inr_comp_inr {α β γ} [decidable_eq β] [decidable_eq (α ⊕ β)]
-  {f : α ⊕ β → γ} {i : β} {x : γ} :
+@[simp] lemma update_inr_comp_inr [decidable_eq β] [decidable_eq (α ⊕ β)] {f : α ⊕ β → γ} {i : β}
+  {x : γ} :
   update f (inr i) x ∘ inr = update (f ∘ inr) i x :=
 update_comp_eq_of_injective _ inr_injective _ _
 
-@[simp] lemma update_inr_apply_inr {α β γ} [decidable_eq β] [decidable_eq (α ⊕ β)]
-  {f : α ⊕ β → γ} {i j : β} {x : γ} :
+@[simp] lemma update_inr_apply_inr [decidable_eq β] [decidable_eq (α ⊕ β)] {f : α ⊕ β → γ}
+  {i j : β} {x : γ} :
   update f (inr i) x (inr j) = update (f ∘ inr) i x j :=
 by rw ← update_inr_comp_inr
 
-section
-  variables (ra : α → α → Prop) (rb : β → β → Prop)
-
-  /-- Lexicographic order for sum. Sort all the `inl a` before the `inr b`,
-    otherwise use the respective order on `α` or `β`. -/
-  inductive lex : α ⊕ β → α ⊕ β → Prop
-  | inl {a₁ a₂} (h : ra a₁ a₂) : lex (inl a₁) (inl a₂)
-  | inr {b₁ b₂} (h : rb b₁ b₂) : lex (inr b₁) (inr b₂)
-  | sep (a b) : lex (inl a) (inr b)
+/-- Swap the factors of a sum type -/
+@[simp] def swap : α ⊕ β → β ⊕ α
+| (inl a) := inr a
+| (inr b) := inl b
 
-  variables {ra rb}
+@[simp] lemma swap_swap (x : α ⊕ β) : swap (swap x) = x := by cases x; refl
+@[simp] lemma swap_swap_eq : swap ∘ swap = @id (α ⊕ β) := funext $ swap_swap
+@[simp] lemma swap_left_inverse : function.left_inverse (@swap α β) swap := swap_swap
+@[simp] lemma swap_right_inverse : function.right_inverse (@swap α β) swap := swap_swap
 
-  @[simp] theorem lex_inl_inl {a₁ a₂} : lex ra rb (inl a₁) (inl a₂) ↔ ra a₁ a₂ :=
-  ⟨λ h, by cases h; assumption, lex.inl⟩
+section lex
 
-  @[simp] theorem lex_inr_inr {b₁ b₂} : lex ra rb (inr b₁) (inr b₂) ↔ rb b₁ b₂ :=
-  ⟨λ h, by cases h; assumption, lex.inr⟩
+/-- Lexicographic order for sum. Sort all the `inl a` before the `inr b`, otherwise use the
+respective order on `α` or `β`. -/
+inductive lex (r : α → α → Prop) (s : β → β → Prop) : α ⊕ β → α ⊕ β → Prop
+| inl {a₁ a₂} (h : r a₁ a₂) : lex (inl a₁) (inl a₂)
+| inr {b₁ b₂} (h : s b₁ b₂) : lex (inr b₁) (inr b₂)
+| sep (a b) : lex (inl a) (inr b)
 
-  @[simp] theorem lex_inr_inl {b a} : ¬ lex ra rb (inr b) (inl a) :=
-  λ h, by cases h
+attribute [protected] sum.lex.inl sum.lex.inr
+attribute [simp] lex.sep
 
-  attribute [simp] lex.sep
+variables {r r₁ r₂ : α → α → Prop} {s s₁ s₂ : β → β → Prop} {a a₁ a₂ : α} {b b₁ b₂ : β}
+  {x y : α ⊕ β}
 
-  theorem lex_acc_inl {a} (aca : acc ra a) : acc (lex ra rb) (inl a) :=
-  begin
-    induction aca with a H IH,
-    constructor, intros y h,
-    cases h with a' _ h',
-    exact IH _ h'
-  end
+@[simp] lemma lex_inl_inl : lex r s (inl a₁) (inl a₂) ↔ r a₁ a₂ :=
+⟨λ h, by { cases h, assumption }, lex.inl⟩
 
-  theorem lex_acc_inr (aca : ∀ a, acc (lex ra rb) (inl a)) {b} (acb : acc rb b) :
-    acc (lex ra rb) (inr b) :=
-  begin
-    induction acb with b H IH,
-    constructor, intros y h,
-    cases h with _ _ _ b' _ h' a,
-    { exact IH _ h' },
-    { exact aca _ }
-  end
+@[simp] lemma lex_inr_inr : lex r s (inr b₁) (inr b₂) ↔ s b₁ b₂ :=
+⟨λ h, by { cases h, assumption }, lex.inr⟩
 
-  theorem lex_wf (ha : well_founded ra) (hb : well_founded rb) : well_founded (lex ra rb) :=
-  have aca : ∀ a, acc (lex ra rb) (inl a), from λ a, lex_acc_inl (ha.apply a),
-  ⟨λ x, sum.rec_on x aca (λ b, lex_acc_inr aca (hb.apply b))⟩
+@[simp] lemma lex_inr_inl : ¬ lex r s (inr b) (inl a) .
 
-end
+lemma lex.mono (hr : ∀ a b, r₁ a b → r₂ a b) (hs : ∀ a b, s₁ a b → s₂ a b) (h : lex r₁ s₁ x y) :
+  lex r₂ s₂ x y :=
+by { cases h, exacts [lex.inl (hr _ _ ‹_›), lex.inr (hs _ _ ‹_›), lex.sep _ _] }
 
-/-- Swap the factors of a sum type -/
-@[simp] def swap : α ⊕ β → β ⊕ α
-| (inl a) := inr a
-| (inr b) := inl b
+lemma lex.mono_left (hr : ∀ a b, r₁ a b → r₂ a b) (h : lex r₁ s x y) : lex r₂ s x y :=
+h.mono hr $ λ _ _, id
 
-@[simp] lemma swap_swap (x : α ⊕ β) : swap (swap x) = x :=
-by cases x; refl
+lemma lex.mono_right (hs : ∀ a b, s₁ a b → s₂ a b)  (h : lex r s₁ x y) : lex r s₂ x y :=
+h.mono (λ _ _, id) hs
 
-@[simp] lemma swap_swap_eq : swap ∘ swap = @id (α ⊕ β) :=
-funext $ swap_swap
+lemma lex_acc_inl {a} (aca : acc r a) : acc (lex r s) (inl a) :=
+begin
+  induction aca with a H IH,
+  constructor, intros y h,
+  cases h with a' _ h',
+  exact IH _ h'
+end
 
-@[simp] lemma swap_left_inverse : function.left_inverse (@swap α β) swap :=
-swap_swap
+lemma lex_acc_inr (aca : ∀ a, acc (lex r s) (inl a)) {b} (acb : acc s b) : acc (lex r s) (inr b) :=
+begin
+  induction acb with b H IH,
+  constructor, intros y h,
+  cases h with _ _ _ b' _ h' a,
+  { exact IH _ h' },
+  { exact aca _ }
+end
 
-@[simp] lemma swap_right_inverse : function.right_inverse (@swap α β) swap :=
-swap_swap
+lemma lex_wf (ha : well_founded r) (hb : well_founded s) : well_founded (lex r s) :=
+have aca : ∀ a, acc (lex r s) (inl a), from λ a, lex_acc_inl (ha.apply a),
+⟨λ x, sum.rec_on x aca (λ b, lex_acc_inr aca (hb.apply b))⟩
 
+end lex
 end sum
 
 namespace function
 
 open sum
 
-lemma injective.sum_elim {γ} {f : α → γ} {g : β → γ}
+lemma injective.sum_elim {f : α → γ} {g : β → γ}
   (hf : injective f) (hg : injective g) (hfg : ∀ a b, f a ≠ g b) :
   injective (sum.elim f g)
 | (inl x) (inl y) h := congr_arg inl $ hf h
diff --git a/src/order/rel_classes.lean b/src/order/rel_classes.lean
index 62e7ac8c4c57c..54aaa9bfae95c 100644
--- a/src/order/rel_classes.lean
+++ b/src/order/rel_classes.lean
@@ -3,7 +3,7 @@ Copyright (c) 2020 Jeremy Avigad. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad, Mario Carneiro, Yury G. Kudryashov
 -/
-import data.sum
+import data.sum.basic
 import order.basic
 
 /-!
diff --git a/src/tactic/fresh_names.lean b/src/tactic/fresh_names.lean
index 606fce2996bc9..aa55f0c317340 100644
--- a/src/tactic/fresh_names.lean
+++ b/src/tactic/fresh_names.lean
@@ -3,9 +3,7 @@ Copyright (c) 2020 Jannis Limperg. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jannis Limperg
 -/
-
-import data.sum
-import meta.rb_map
+import data.sum.basic
 import tactic.dependencies
 
 /-!
diff --git a/test/simps.lean b/test/simps.lean
index db3546cfac215..9fc1d75536965 100644
--- a/test/simps.lean
+++ b/test/simps.lean
@@ -1,5 +1,5 @@
 import algebra.group.hom
-import data.sum
+import data.sum.basic
 import tactic.simps
 
 universes v u w