no goals
α : Type ?u.282487
β : Type ?u.282490
γ : Type ?u.282493
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
ι : Type u
f : ι → Ordinal
a : Ordinal
⊢ a < sup f ↔ ∃ i, a < f i
simpa only [not_forall, not_le] using not_congr (@sup_le_iff.{_, v} _ f a)