case h.e'_2.h.a
α : Type ?u.349869
β : Type ?u.349872
γ : Type ?u.349875
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal
f : (a : Ordinal) → a < o → Ordinal
a : Ordinal
a✝ : Ordinal
⊢ (∀ (h : a✝ < o), f a✝ h < a) ↔ ∀ (h : a✝ < o), succ (f a✝ h) ≤ a
α : Type ?u.349869
β : Type ?u.349872
γ : Type ?u.349875
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal
f : (a : Ordinal) → a < o → Ordinal
a : Ordinal
⊢ blsub o f ≤ a ↔ ∀ (i : Ordinal) (h : i < o), f i h < a
convert bsup_le_iff.{_, v} (f := fun a ha => succ (f a ha)) (a := a) using 2
no goals
case h.e'_2.h.a
α : Type ?u.349869
β : Type ?u.349872
γ : Type ?u.349875
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal
f : (a : Ordinal) → a < o → Ordinal
a : Ordinal
a✝ : Ordinal
⊢ (∀ (h : a✝ < o), f a✝ h < a) ↔ ∀ (h : a✝ < o), succ (f a✝ h) ≤ a
simp_rw [succ_le_iff]