feat: port Data.Nat.PartENat (#1892)

port of data.net.part_enat



Co-authored-by: Moritz Firsching <firsching@google.com>
Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Co-authored-by: Jon Eugster <eugster.jon@gmail.com>

Mathlib.lean

@@ -489,6 +489,7 @@ import Mathlib.Data.Nat.Order.Lemmas
 import Mathlib.Data.Nat.PSub
 import Mathlib.Data.Nat.Pairing
 import Mathlib.Data.Nat.Parity
+import Mathlib.Data.Nat.PartENat
 import Mathlib.Data.Nat.Pow
 import Mathlib.Data.Nat.Prime
 import Mathlib.Data.Nat.PrimeFin

Mathlib/Data/ENat/Basic.lean

@@ -23,23 +23,22 @@ about this type.
 /-- Extended natural numbers `ℕ∞ = WithTop ℕ`. -/
 def ENat : Type :=
   WithTop ℕ
-deriving Zero, AddCommMonoidWithOne, CanonicallyOrderedCommSemiring, Nontrivial,
+deriving Zero,
+  -- AddCommMonoidWithOne,
+  CanonicallyOrderedCommSemiring, Nontrivial,
   LinearOrder, Bot, Top, CanonicallyLinearOrderedAddMonoid, Sub,
   LinearOrderedAddCommMonoidWithTop, WellFoundedRelation, Inhabited
   -- OrderBot, OrderTop, OrderedSub,  SuccOrder, WellFoundedLt, CharZero
 #align enat ENat
 
+-- Porting Note: In `Data.Nat.ENatPart` proofs timed out when having
+-- the `deriving AddCommMonoidWithOne`, and it seems to work without.
 
 /-- Extended natural numbers `ℕ∞ = WithTop ℕ`. -/
 notation "ℕ∞" => ENat
 
 namespace ENat
 
-/-- The canonical map from `ℕ` to `ℕ∞` -/
-@[coe] def ofNat (n : ℕ) : ℕ∞ := WithTop.some n
-
-instance : Coe ℕ ℕ∞ := ⟨ofNat⟩
-
 --Porting note: instances that derive failed to find
 instance : OrderBot ℕ∞ := WithTop.orderBot
 instance : OrderTop ℕ∞ := WithTop.orderTop