no goals
α : Type ?u.194863
β : Type ?u.194866
γ : Type ?u.194869
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal
h0 : 0 < o
a : (Quotient.out o).α
⊢ 0 < type fun x x_1 => x < x_1
rwa [type_lt]
α : Type ?u.194863
β : Type ?u.194866
γ : Type ?u.194869
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal
h0 : 0 < o
a : (Quotient.out o).α
⊢ ¬a < enum (fun x x_1 => x < x_1) 0 (_ : 0 < type fun x x_1 => x < x_1)
α : Type ?u.194863
β : Type ?u.194866
γ : Type ?u.194869
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal
h0 : 0 < o
a : (Quotient.out o).α
⊢ enum (fun x x_1 => x < x_1) 0 (_ : 0 < type fun x x_1 => x < x_1) ≤ a
rw [← not_lt]
no goals
α : Type ?u.194863
β : Type ?u.194866
γ : Type ?u.194869
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal
h0 : 0 < o
a : (Quotient.out o).α
⊢ ¬a < enum (fun x x_1 => x < x_1) 0 (_ : 0 < type fun x x_1 => x < x_1)
apply enum_zero_le