case inl
α : Type u_1
inst✝ : LinearOrder α
⊢ toColex ∅ ≤ toColex ∅

case inr
α : Type u_1
inst✝ : LinearOrder α
A : Finset α
hA : Finset.Nonempty A
⊢ toColex ∅ ≤ toColex A
α : Type u_1
inst✝ : LinearOrder α
A : Finset α
⊢ toColex ∅ ≤ toColex A
rcases A.eq_empty_or_nonempty with (rfl | hA)
no goals
case inl
α : Type u_1
inst✝ : LinearOrder α
⊢ toColex ∅ ≤ toColex ∅
simp
no goals
case inr
α : Type u_1
inst✝ : LinearOrder α
A : Finset α
hA : Finset.Nonempty A
⊢ toColex ∅ ≤ toColex A
apply (empty_toColex_lt hA).le