case inl
α : Type ?u.322539
β : Type ?u.322542
γ : Type ?u.322545
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
ι : Type u
f : ι → Ordinal
h : sup f = lsub f
⊢ sup f = lsub f ∨ succ (sup f) = lsub f

case inr
α : Type ?u.322539
β : Type ?u.322542
γ : Type ?u.322545
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
ι : Type u
f : ι → Ordinal
h : sup f < lsub f
⊢ sup f = lsub f ∨ succ (sup f) = lsub f
α : Type ?u.322539
β : Type ?u.322542
γ : Type ?u.322545
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
ι : Type u
f : ι → Ordinal
⊢ sup f = lsub f ∨ succ (sup f) = lsub f
cases' eq_or_lt_of_le (sup_le_lsub.{_, v} f) with h h
no goals
case inl
α : Type ?u.322539
β : Type ?u.322542
γ : Type ?u.322545
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
ι : Type u
f : ι → Ordinal
h : sup f = lsub f
⊢ sup f = lsub f ∨ succ (sup f) = lsub f
exact Or.inl h
no goals
case inr
α : Type ?u.322539
β : Type ?u.322542
γ : Type ?u.322545
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
ι : Type u
f : ι → Ordinal
h : sup f < lsub f
⊢ sup f = lsub f ∨ succ (sup f) = lsub f
exact Or.inr ((succ_le_of_lt h).antisymm (lsub_le_sup_succ f))