case inl
x : ℝ*
hx : Infinite x
⊢ st x = sSup {y | ↑y < x}

case inr
x : ℝ*
hx : ¬Infinite x
⊢ st x = sSup {y | ↑y < x}
x : ℝ*
⊢ st x = sSup {y | ↑y < x}
rcases _root_.em (Infinite x) with (hx|hx)
case inl
x : ℝ*
hx : Infinite x
⊢ 0 = sSup {y | ↑y < x}
case inl
x : ℝ*
hx : Infinite x
⊢ st x = sSup {y | ↑y < x}
rw [hx.st_eq]
no goals
case inl
x : ℝ*
hx : Infinite x
⊢ 0 = sSup {y | ↑y < x}
cases hx with
| inl hx =>
  convert Real.sSup_univ.symm
  exact Set.eq_univ_of_forall hx
| inr hx =>
  convert Real.sSup_empty.symm
  exact Set.eq_empty_of_forall_not_mem fun y hy ↦ hy.out.not_lt (hx _)
case h.e'_3.h.e'_3
x : ℝ*
hx : InfinitePos x
⊢ {y | ↑y < x} = Set.univ
case inl.inl
x : ℝ*
hx : InfinitePos x
⊢ 0 = sSup {y | ↑y < x}
convert Real.sSup_univ.symm
no goals
case h.e'_3.h.e'_3
x : ℝ*
hx : InfinitePos x
⊢ {y | ↑y < x} = Set.univ
exact Set.eq_univ_of_forall hx
case h.e'_3.h.e'_3
x : ℝ*
hx : InfiniteNeg x
⊢ {y | ↑y < x} = ∅
case inl.inr
x : ℝ*
hx : InfiniteNeg x
⊢ 0 = sSup {y | ↑y < x}
convert Real.sSup_empty.symm
no goals
case h.e'_3.h.e'_3
x : ℝ*
hx : InfiniteNeg x
⊢ {y | ↑y < x} = ∅
exact Set.eq_empty_of_forall_not_mem fun y hy ↦ hy.out.not_lt (hx _)
no goals
case inr
x : ℝ*
hx : ¬Infinite x
⊢ st x = sSup {y | ↑y < x}
exact (isSt_sSup hx).st_eq