α✝ : Type ?u.100761
β : Type ?u.100764
γ : Type ?u.100767
r✝ : α✝ → α✝ → Prop
s : β → β → Prop
t : γ → γ → Prop
α : Type u_1
r : α → α → Prop
wo : IsWellOrder α r
h : ∀ (a : Ordinal), a < type r → succ a < type r
x : α
⊢ r x (enum r (succ (typein r x)) (_ : succ (typein r x) < type r))
α✝ : Type ?u.100761
β : Type ?u.100764
γ : Type ?u.100767
r✝ : α✝ → α✝ → Prop
s : β → β → Prop
t : γ → γ → Prop
α : Type u_1
r : α → α → Prop
wo : IsWellOrder α r
h : ∀ (a : Ordinal), a < type r → succ a < type r
x : α
⊢ ∃ y, r x y
use enum r (succ (typein r x)) (h _ (typein_lt_type r x))
case h.e'_1
α✝ : Type ?u.100761
β : Type ?u.100764
γ : Type ?u.100767
r✝ : α✝ → α✝ → Prop
s : β → β → Prop
t : γ → γ → Prop
α : Type u_1
r : α → α → Prop
wo : IsWellOrder α r
h : ∀ (a : Ordinal), a < type r → succ a < type r
x : α
⊢ x = enum r (typein r x) (_ : typein r x < type r)
α✝ : Type ?u.100761
β : Type ?u.100764
γ : Type ?u.100767
r✝ : α✝ → α✝ → Prop
s : β → β → Prop
t : γ → γ → Prop
α : Type u_1
r : α → α → Prop
wo : IsWellOrder α r
h : ∀ (a : Ordinal), a < type r → succ a < type r
x : α
⊢ r x (enum r (succ (typein r x)) (_ : succ (typein r x) < type r))
convert (enum_lt_enum (typein_lt_type r x)
  (h _ (typein_lt_type r x))).mpr (lt_succ _)
no goals
case h.e'_1
α✝ : Type ?u.100761
β : Type ?u.100764
γ : Type ?u.100767
r✝ : α✝ → α✝ → Prop
s : β → β → Prop
t : γ → γ → Prop
α : Type u_1
r : α → α → Prop
wo : IsWellOrder α r
h : ∀ (a : Ordinal), a < type r → succ a < type r
x : α
⊢ x = enum r (typein r x) (_ : typein r x < type r)
rw [enum_typein]