no goals
α : Type ?u.321274
β : Type ?u.321277
γ : Type ?u.321280
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
ι : Type u
f : ι → Ordinal
a : Ordinal
⊢ a < lsub f ↔ ∃ i, a ≤ f i
simpa only [not_forall, not_lt, not_le] using not_congr (@lsub_le_iff.{_, v} _ f a)