x y : ℝ
hx : 0 < x
⊢ ↑(OrderIso.symm expOrderIso) { val := abs x, property := (_ : 0 < abs x) } =
    ↑(OrderIso.symm expOrderIso) { val := x, property := hx }
x y : ℝ
hx : 0 < x
⊢ log x = ↑(OrderIso.symm expOrderIso) { val := x, property := hx }
rw [log_of_ne_zero hx.ne']
case h.e_6.h.e_val
x y : ℝ
hx : 0 < x
⊢ abs x = x
x y : ℝ
hx : 0 < x
⊢ ↑(OrderIso.symm expOrderIso) { val := abs x, property := (_ : 0 < abs x) } =
    ↑(OrderIso.symm expOrderIso) { val := x, property := hx }
congr
no goals
case h.e_6.h.e_val
x y : ℝ
hx : 0 < x
⊢ abs x = x
exact abs_of_pos hx