case e_a
α : Type ?u.307782
β : Type ?u.307785
γ : Type ?u.307788
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal
f : (a : Ordinal) → a < o → Ordinal
⊢ brange o f = range (familyOfBFamily o f)
α : Type ?u.307782
β : Type ?u.307785
γ : Type ?u.307788
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal
f : (a : Ordinal) → a < o → Ordinal
⊢ sSup (brange o f) = bsup o f
congr
no goals
case e_a
α : Type ?u.307782
β : Type ?u.307785
γ : Type ?u.307788
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal
f : (a : Ordinal) → a < o → Ordinal
⊢ brange o f = range (familyOfBFamily o f)
rw [range_familyOfBFamily]