α✝ : Type ?u.311394
β : Type ?u.311397
γ : Type ?u.311400
r✝ : α✝ → α✝ → Prop
s : β → β → Prop
t : γ → γ → Prop
f : Ordinal → Ordinal
H : IsNormal f
o : Ordinal
α : Type u
r : α → α → Prop
x✝ : IsWellOrder α r
g : (a : Ordinal) → a < type r → Ordinal
h : type r ≠ 0
this : Nonempty α
⊢ f (Ordinal.bsup (type r) g) = Ordinal.bsup (type r) fun a h => f (g a h)
α✝ : Type ?u.311394
β : Type ?u.311397
γ : Type ?u.311400
r✝ : α✝ → α✝ → Prop
s : β → β → Prop
t : γ → γ → Prop
f : Ordinal → Ordinal
H : IsNormal f
o : Ordinal
α : Type u
r : α → α → Prop
x✝ : IsWellOrder α r
g : (a : Ordinal) → a < type r → Ordinal
h : type r ≠ 0
⊢ f (Ordinal.bsup (type r) g) = Ordinal.bsup (type r) fun a h => f (g a h)
haveI := type_ne_zero_iff_nonempty.1 h
no goals
α✝ : Type ?u.311394
β : Type ?u.311397
γ : Type ?u.311400
r✝ : α✝ → α✝ → Prop
s : β → β → Prop
t : γ → γ → Prop
f : Ordinal → Ordinal
H : IsNormal f
o : Ordinal
α : Type u
r : α → α → Prop
x✝ : IsWellOrder α r
g : (a : Ordinal) → a < type r → Ordinal
h : type r ≠ 0
this : Nonempty α
⊢ f (Ordinal.bsup (type r) g) = Ordinal.bsup (type r) fun a h => f (g a h)
rw [← sup_eq_bsup' r, IsNormal.sup.{_, v, w} H, ← sup_eq_bsup' r] <;> rfl