case intro
y : EReal
hy : y ≠ ⊤
x : ℝ
h : ↑x ≤ y
hx : ↑x ≠ ⊥
⊢ toReal ↑x ≤ toReal y
x y : EReal
h : x ≤ y
hx : x ≠ ⊥
hy : y ≠ ⊤
⊢ toReal x ≤ toReal y
lift x to ℝ using ⟨ne_top_of_le_ne_top hy h, hx⟩
case intro.intro
x : ℝ
hx : ↑x ≠ ⊥
y : ℝ
hy : ↑y ≠ ⊤
h : ↑x ≤ ↑y
⊢ toReal ↑x ≤ toReal ↑y
case intro
y : EReal
hy : y ≠ ⊤
x : ℝ
h : ↑x ≤ y
hx : ↑x ≠ ⊥
⊢ toReal ↑x ≤ toReal y
lift y to ℝ using ⟨hy, ne_bot_of_le_ne_bot hx h⟩
no goals
case intro.intro
x : ℝ
hx : ↑x ≠ ⊥
y : ℝ
hy : ↑y ≠ ⊤
h : ↑x ≤ ↑y
⊢ toReal ↑x ≤ toReal ↑y
simpa using h