refactor(data/nat/enat): rename enat to part_enat (#15235)

* find+replace `enat` with `part_enat`;
* reflow long lines
* add a sentence to the module docstring of `data.nat.enat`.

I'm going to define `enat := with_top nat` and use it as the default implementation of "nat with top".

Author: urkud

archive/imo/imo2019_q4.lean

@@ -34,13 +34,13 @@ begin
   { exact prime_iff_prime_int.mp prime_two },
   have h2 : n * (n - 1) / 2 < k,
   { suffices : multiplicity 2 (k! : ℤ) = (n * (n - 1) / 2 : ℕ),
-    { rw [← enat.coe_lt_coe, ← this], change multiplicity ((2 : ℕ) : ℤ) _ < _,
+    { rw [← part_enat.coe_lt_coe, ← this], change multiplicity ((2 : ℕ) : ℤ) _ < _,
       simp_rw [int.coe_nat_multiplicity, multiplicity_two_factorial_lt hk.lt.ne.symm] },
     rw [h, multiplicity.finset.prod prime_2, ← sum_range_id, ← sum_nat_coe_enat],
     apply sum_congr rfl, intros i hi,
     rw [multiplicity_sub_of_gt, multiplicity_pow_self_of_prime prime_2],
     rwa [multiplicity_pow_self_of_prime prime_2, multiplicity_pow_self_of_prime prime_2,
-      enat.coe_lt_coe, ←mem_range] },
+      part_enat.coe_lt_coe, ←mem_range] },
   rw [←not_le], intro hn,
   apply ne_of_lt _ h.symm,
   suffices : (∏ i in range n, 2 ^ n : ℤ) < ↑k!,

src/algebra/big_operators/enat.lean

@@ -7,16 +7,16 @@ import algebra.big_operators.basic
 import data.nat.enat
 
 /-!
-# Big operators in `enat`
+# Big operators in `part_enat`
 
-A simple lemma about sums in `enat`.
+A simple lemma about sums in `part_enat`.
 -/
 open_locale big_operators
 variables {α : Type*}
 
 namespace finset
 lemma sum_nat_coe_enat (s : finset α) (f : α → ℕ) :
-  (∑ x in s, (f x : enat)) = (∑ x  in s, f x : ℕ) :=
-(enat.coe_hom.map_sum _ _).symm
+  (∑ x in s, (f x : part_enat)) = (∑ x  in s, f x : ℕ) :=
+(part_enat.coe_hom.map_sum _ _).symm
 
 end finset

src/algebra/order/sub.lean

@@ -11,7 +11,7 @@ This file proves lemmas relating (truncated) subtraction with an order. We provi
 `has_ordered_sub` stating that `a - b ≤ c ↔ a ≤ c + b`.
 
 The subtraction discussed here could both be normal subtraction in an additive group or truncated
-subtraction on a canonically ordered monoid (`ℕ`, `multiset`, `enat`, `ennreal`, ...)
+subtraction on a canonically ordered monoid (`ℕ`, `multiset`, `part_enat`, `ennreal`, ...)
 
 ## Implementation details
 

src/algebra/squarefree.lean

@@ -93,7 +93,7 @@ lemma squarefree_iff_multiplicity_le_one (r : R) :
 begin
   refine forall_congr (λ a, _),
   rw [← sq, pow_dvd_iff_le_multiplicity, or_iff_not_imp_left, not_le, imp_congr _ iff.rfl],
-  simpa using enat.add_one_le_iff_lt (enat.coe_ne_top 1)
+  simpa using part_enat.add_one_le_iff_lt (part_enat.coe_ne_top 1)
 end
 
 end comm_monoid
@@ -110,10 +110,10 @@ begin
   refine wf_dvd_monoid.induction_on_irreducible b (by contradiction) (λ u hu hu', _)
     (λ b p hb hp ih hpb, _),
   { rw [multiplicity.finite_iff_dom, multiplicity.is_unit_right ha.not_unit hu],
-    exact enat.dom_coe 0, },
+    exact part_enat.dom_coe 0, },
   { refine multiplicity.finite_mul ha
-      (multiplicity.finite_iff_dom.mpr (enat.dom_of_le_coe (show multiplicity a p ≤ ↑1, from _)))
-      (ih hb),
+      (multiplicity.finite_iff_dom.mpr
+        (part_enat.dom_of_le_coe (show multiplicity a p ≤ ↑1, from _))) (ih hb),
     norm_cast,
     exact (((multiplicity.squarefree_iff_multiplicity_le_one p).mp hp.squarefree a)
       .resolve_right ha.not_unit) }

src/data/nat/choose/factorization.lean

@@ -39,7 +39,7 @@ begin
   have hp : p.prime := not.imp_symm (choose n k).factorization_eq_zero_of_non_prime h,
   have hkn : k ≤ n, { refine le_of_not_lt (λ hnk, h _), simp [choose_eq_zero_of_lt hnk] },
   rw [←@padic_val_nat_eq_factorization p _ ⟨hp⟩, @padic_val_nat_def _ ⟨hp⟩ _ (choose_pos hkn)],
-  simp only [hp.multiplicity_choose hkn (lt_add_one _), enat.get_coe],
+  simp only [hp.multiplicity_choose hkn (lt_add_one _), part_enat.get_coe],
   refine (finset.card_filter_le _ _).trans (le_of_eq (nat.card_Ico _ _)),
 end
 
@@ -74,7 +74,7 @@ begin
   cases lt_or_le n k with hnk hkn,
   { simp [choose_eq_zero_of_lt hnk] },
   rw [←@padic_val_nat_eq_factorization p _ ⟨hp⟩, @padic_val_nat_def _ ⟨hp⟩ _ (choose_pos hkn)],
-  simp only [hp.multiplicity_choose hkn (lt_add_one _), enat.get_coe,
+  simp only [hp.multiplicity_choose hkn (lt_add_one _), part_enat.get_coe,
     finset.card_eq_zero, finset.filter_eq_empty_iff, not_le],
   intros i hi,
   rcases eq_or_lt_of_le (finset.mem_Ico.mp hi).1 with rfl | hi,