case h.e'_2.h.a
α : Type ?u.318577
β : Type ?u.318580
γ : Type ?u.318583
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
ι : Type u
f : ι → Ordinal
a : Ordinal
a✝ : ι
⊢ f a✝ < a ↔ (succ ∘ f) a✝ ≤ a
α : Type ?u.318577
β : Type ?u.318580
γ : Type ?u.318583
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
ι : Type u
f : ι → Ordinal
a : Ordinal
⊢ lsub f ≤ a ↔ ∀ (i : ι), f i < a
convert sup_le_iff.{_, v} (f := succ ∘ f) (a := a) using 2
no goals
case h.e'_2.h.a
α : Type ?u.318577
β : Type ?u.318580
γ : Type ?u.318583
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
ι : Type u
f : ι → Ordinal
a : Ordinal
a✝ : ι
⊢ f a✝ < a ↔ (succ ∘ f) a✝ ≤ a
simp only [comp_apply, succ_le_iff]