case pos
x : EReal
h : x ≠ ⊤
h' : x = ⊥
⊢ x ≤ ↑(toReal x)

case neg
x : EReal
h : x ≠ ⊤
h' : ¬x = ⊥
⊢ x ≤ ↑(toReal x)
x : EReal
h : x ≠ ⊤
⊢ x ≤ ↑(toReal x)
by_cases h' : x = ⊥
no goals
case pos
x : EReal
h : x ≠ ⊤
h' : x = ⊥
⊢ x ≤ ↑(toReal x)
simp only [h', bot_le]
no goals
case neg
x : EReal
h : x ≠ ⊤
h' : ¬x = ⊥
⊢ x ≤ ↑(toReal x)
simp only [le_refl, coe_toReal h h']