case mp
x : PartENat
⊢ x = ⊤ → ∀ (n : ℕ), ↑n < x

case mpr
x : PartENat
⊢ (∀ (n : ℕ), ↑n < x) → x = ⊤
x : PartENat
⊢ x = ⊤ ↔ ∀ (n : ℕ), ↑n < x
constructor
case mp
n : ℕ
⊢ ↑n < ⊤
case mp
x : PartENat
⊢ x = ⊤ → ∀ (n : ℕ), ↑n < x
rintro rfl n
no goals
case mp
n : ℕ
⊢ ↑n < ⊤
exact natCast_lt_top _
case mpr
x : PartENat
⊢ ¬x = ⊤ → ¬∀ (n : ℕ), ↑n < x
case mpr
x : PartENat
⊢ (∀ (n : ℕ), ↑n < x) → x = ⊤
contrapose
case mpr
x : PartENat
⊢ (∃ n, x = ↑n) → ∃ x_1, ¬↑x_1 < x
case mpr
x : PartENat
⊢ ¬x = ⊤ → ¬∀ (n : ℕ), ↑n < x
rw [←Ne, ne_top_iff, not_forall]
case mpr.intro
n : ℕ
⊢ ∃ x, ¬↑x < ↑n
case mpr
x : PartENat
⊢ (∃ n, x = ↑n) → ∃ x_1, ¬↑x_1 < x
rintro ⟨n, rfl⟩
no goals
case mpr.intro
n : ℕ
⊢ ∃ x, ¬↑x < ↑n
exact ⟨n, irrefl _⟩