case intro
α✝ : Type ?u.98794
β : Type ?u.98797
γ : Type ?u.98800
r✝ : α✝ → α✝ → Prop
s : β → β → Prop
t : γ → γ → Prop
a✝ : Ordinal
α : Type u_1
r : α → α → Prop
wo : IsWellOrder α r
a x : α
x✝ : ∀ (y : α), r y x → Acc r y
IH : ∀ (y : α), r y x → Acc (fun x x_1 => x < x_1) (typein r y)
b : α
h : typein r b < typein r x
⊢ Acc (fun x x_1 => x < x_1) (typein r b)
α✝ : Type ?u.98794
β : Type ?u.98797
γ : Type ?u.98800
r✝ : α✝ → α✝ → Prop
s : β → β → Prop
t : γ → γ → Prop
a✝ : Ordinal
α : Type u_1
r : α → α → Prop
wo : IsWellOrder α r
a x : α
x✝ : ∀ (y : α), r y x → Acc r y
IH : ∀ (y : α), r y x → Acc (fun x x_1 => x < x_1) (typein r y)
o : Ordinal
h : o < typein r x
⊢ Acc (fun x x_1 => x < x_1) o
rcases typein_surj r (lt_trans h (typein_lt_type r _)) with ⟨b, rfl⟩
no goals
case intro
α✝ : Type ?u.98794
β : Type ?u.98797
γ : Type ?u.98800
r✝ : α✝ → α✝ → Prop
s : β → β → Prop
t : γ → γ → Prop
a✝ : Ordinal
α : Type u_1
r : α → α → Prop
wo : IsWellOrder α r
a x : α
x✝ : ∀ (y : α), r y x → Acc r y
IH : ∀ (y : α), r y x → Acc (fun x x_1 => x < x_1) (typein r y)
b : α
h : typein r b < typein r x
⊢ Acc (fun x x_1 => x < x_1) (typein r b)
exact IH _ ((typein_lt_typein r).1 h)