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

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

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

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