case intro
x : ℝ
hx : ↑x ≠ ⊤
h'x : ↑x ≠ ⊥
⊢ ↑(toReal ↑x) = ↑x
x : EReal
hx : x ≠ ⊤
h'x : x ≠ ⊥
⊢ ↑(toReal x) = x
lift x to ℝ using ⟨hx, h'x⟩
no goals
case intro
x : ℝ
hx : ↑x ≠ ⊤
h'x : ↑x ≠ ⊥
⊢ ↑(toReal ↑x) = ↑x
rfl