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

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