α : Type ?u.71541
β : Type ?u.71544
γ : Type ?u.71547
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal
i : (Quotient.out o).α
⊢ typein (fun x x_1 => x < x_1) i < type fun x x_1 => x < x_1
α : Type ?u.71541
β : Type ?u.71544
γ : Type ?u.71547
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal
i : (Quotient.out o).α
⊢ typein (fun x x_1 => x < x_1) i < o
simp_rw [← type_lt o]
no goals
α : Type ?u.71541
β : Type ?u.71544
γ : Type ?u.71547
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal
i : (Quotient.out o).α
⊢ typein (fun x x_1 => x < x_1) i < type fun x x_1 => x < x_1
apply typein_lt_type