α : Type u_1
β : Type ?u.96934
γ : Type ?u.96937
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
inst✝ : IsWellOrder α r
o : Ordinal
h : o < type r
a : α
e : typein r a = o
⊢ typein r (enum r o h) = o
α : Type u_1
β : Type ?u.96934
γ : Type ?u.96937
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
inst✝ : IsWellOrder α r
o : Ordinal
h : o < type r
⊢ typein r (enum r o h) = o
let ⟨a, e⟩ := typein_surj r h
α : Type u_1
β : Type ?u.96934
γ : Type ?u.96937
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
inst✝ : IsWellOrder α r
a : α
h : typein r a < type r
⊢ typein r (enum r (typein r a) h) = typein r a
α : Type u_1
β : Type ?u.96934
γ : Type ?u.96937
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
inst✝ : IsWellOrder α r
o : Ordinal
h : o < type r
a : α
e : typein r a = o
⊢ typein r (enum r o h) = o
subst e
no goals
α : Type u_1
β : Type ?u.96934
γ : Type ?u.96937
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
inst✝ : IsWellOrder α r
a : α
h : typein r a < type r
⊢ typein r (enum r (typein r a) h) = typein r a
rw [enum_typein]