no goals
α : Type ?u.308272
β : Type ?u.308275
γ : Type ?u.308278
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
ι : Type u
r : ι → ι → Prop
inst✝ : IsWellOrder ι r
f : ι → Ordinal
⊢ bsup (type r) (bfamilyOfFamily' r f) = sup f
simp only [← sup_eq_bsup' r, enum_typein, familyOfBFamily', bfamilyOfFamily']