Theorem: Tutorial.nestedIntervalSucc_eq_or_eq (Solution/Advanced/Analysis/Lecture3.lean)

State before:
ι : Type
U : ι → Set ℝ
a b : ℝ
⊢ nestedIntervalSucc U a b = (a, (a + b) / 2) ∨ nestedIntervalSucc U a b = ((a + b) / 2, b)
Tactic:
apply ite_eq_or_eq
State after:
no goals