case mp
x : EReal
⊢ x = ⊤ → ∀ (y : ℝ), ↑y < x

case mpr
x : EReal
⊢ (∀ (y : ℝ), ↑y < x) → x = ⊤
x : EReal
⊢ x = ⊤ ↔ ∀ (y : ℝ), ↑y < x
constructor
case mp

⊢ ∀ (y : ℝ), ↑y < ⊤
case mp
x : EReal
⊢ x = ⊤ → ∀ (y : ℝ), ↑y < x
rintro rfl
no goals
case mp

⊢ ∀ (y : ℝ), ↑y < ⊤
exact EReal.coe_lt_top
case mpr
x : EReal
⊢ x ≠ ⊤ → ∃ y, x ≤ ↑y
case mpr
x : EReal
⊢ (∀ (y : ℝ), ↑y < x) → x = ⊤
contrapose!
case mpr
x : EReal
h : x ≠ ⊤
⊢ ∃ y, x ≤ ↑y
case mpr
x : EReal
⊢ x ≠ ⊤ → ∃ y, x ≤ ↑y
intro h
no goals
case mpr
x : EReal
h : x ≠ ⊤
⊢ ∃ y, x ≤ ↑y
exact ⟨x.toReal, le_coe_toReal h⟩