α : Type ?u.366887
β : Type ?u.366890
γ : Type ?u.366893
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
f : Ordinal → Ordinal
⊢ (∀ (a : Ordinal), f a < f (succ a)) →
    ((∀ (o : Ordinal), IsLimit o → (bsup o fun x x_1 => f x) = f o) ↔
      ∀ (o : Ordinal), IsLimit o → (blsub o fun x x_1 => f x) = f o)
α : Type ?u.366887
β : Type ?u.366890
γ : Type ?u.366893
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
f : Ordinal → Ordinal
⊢ IsNormal f ↔ (∀ (a : Ordinal), f a < f (succ a)) ∧ ∀ (o : Ordinal), IsLimit o → (blsub o fun x x_1 => f x) = f o
rw [isNormal_iff_lt_succ_and_bsup_eq.{u, v}, and_congr_right_iff]
α : Type ?u.366887
β : Type ?u.366890
γ : Type ?u.366893
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
f : Ordinal → Ordinal
h : ∀ (a : Ordinal), f a < f (succ a)
⊢ (∀ (o : Ordinal), IsLimit o → (bsup o fun x x_1 => f x) = f o) ↔
    ∀ (o : Ordinal), IsLimit o → (blsub o fun x x_1 => f x) = f o
α : Type ?u.366887
β : Type ?u.366890
γ : Type ?u.366893
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
f : Ordinal → Ordinal
⊢ (∀ (a : Ordinal), f a < f (succ a)) →
    ((∀ (o : Ordinal), IsLimit o → (bsup o fun x x_1 => f x) = f o) ↔
      ∀ (o : Ordinal), IsLimit o → (blsub o fun x x_1 => f x) = f o)
intro h
no goals
α : Type ?u.366887
β : Type ?u.366890
γ : Type ?u.366893
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
f : Ordinal → Ordinal
h : ∀ (a : Ordinal), f a < f (succ a)
⊢ (∀ (o : Ordinal), IsLimit o → (bsup o fun x x_1 => f x) = f o) ↔
    ∀ (o : Ordinal), IsLimit o → (blsub o fun x x_1 => f x) = f o
constructor <;> intro H o ho <;> have := H o ho <;>
  rwa [← bsup_eq_blsub_of_lt_succ_limit ho fun a _ => h a] at *