feat: port Order.Height (#2186)

Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
Co-authored-by: int-y1 <jason_yuen2007@hotmail.com>
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

Mathlib.lean

@@ -1373,6 +1373,7 @@ import Mathlib.Order.FixedPoints
 import Mathlib.Order.GaloisConnection
 import Mathlib.Order.GameAdd
 import Mathlib.Order.Grade
+import Mathlib.Order.Height
 import Mathlib.Order.Heyting.Basic
 import Mathlib.Order.Heyting.Boundary
 import Mathlib.Order.Heyting.Hom

Mathlib/Data/ENat/Basic.lean

@@ -18,6 +18,14 @@ import Mathlib.Algebra.Order.Ring.WithTop
 
 In this file we define `ENat` (notation: `ℕ∞`) to be `WithTop ℕ` and prove some basic lemmas
 about this type.
+
+## Implementation details
+
+There are two natural coercions from `ℕ` to `WithTop ℕ = ENat`: `WithTop.some` and `Nat.cast`.  In
+Lean 3, this difference was hidden in typeclass instances. Since these instances were definitionally
+equal, we did not duplicate generic lemmas about `WithTop α` and `WithTop.some` coercion for `ENat`
+and `Nat.cast` coercion. If you need to apply a lemma about `WithTop`, you may either rewrite back
+and forth using `ENat.some_eq_coe`, or restate the lemma for `ENat`.
 -/
 
 /-- Extended natural numbers `ℕ∞ = WithTop ℕ`. -/
@@ -50,6 +58,10 @@ instance : IsWellOrder ℕ∞ (· < ·) where
 
 variable {m n : ℕ∞}
 
+/-- Lemmas about `WithTop` expect (and can output) `WithTop.some` but the normal form for coercion
+`ℕ → ℕ∞` is `Nat.cast`. -/
+@[simp] theorem some_eq_coe : (WithTop.some : ℕ → ℕ∞) = Nat.cast := rfl
+
 --Porting note: `simp` and `norm_cast` can prove it
 --@[simp, norm_cast]
 theorem coe_zero : ((0 : ℕ) : ℕ∞) = 0 :=

Mathlib/Data/ENat/Lattice.lean

@@ -15,9 +15,24 @@ import Mathlib.Data.ENat.Basic
 # Extended natural numbers form a complete linear order
 
 This instance is not in `Data.ENat.Basic` to avoid dependency on `Finset`s.
+
+We also restate some lemmas about `WithTop` for `ENat` to have versions that use `Nat.cast` instead
+of `WithTop.some`.
 -/
 
 -- porting notes: was `deriving instance` but "default handlers have not been implemented yet"
 -- porting notes: `noncomputable` through 'Nat.instConditionallyCompleteLinearOrderBotNat'
 noncomputable instance : CompleteLinearOrder ENat :=
   inferInstanceAs (CompleteLinearOrder (WithTop ℕ))
+
+namespace ENat
+
+variable {ι : Sort _} {f : ι → ℕ}
+
+lemma supᵢ_coe_lt_top : (⨆ x, ↑(f x) : ℕ∞) < ⊤ ↔ BddAbove (Set.range f) :=
+  WithTop.supr_coe_lt_top f
+
+theorem coe_supᵢ (h : BddAbove (Set.range f)) : ↑(⨆ i, f i) = (⨆ i, f i : ℕ∞) :=
+  WithTop.coe_supᵢ _ h
+
+end ENat