obtain rfl | h' := eq_or_ne s t
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s t : Finset α
a : α
hst : { ofColex := s } ≤ { ofColex := t }
hcard : s.card ≤ t.card
ha : a ∈ s
ht : t.Nonempty
m : α := t.min' ht
⊢ { ofColex := s.erase a } ≤ { ofColex := t.erase m }
case inl
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s : Finset α
a : α
ha : a ∈ s
hst : { ofColex := s } ≤ { ofColex := s }
hcard : s.card ≤ s.card
ht : s.Nonempty
m : α := s.min' ht
⊢ { ofColex := s.erase a } ≤ { ofColex := s.erase m }

case inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s t : Finset α
a : α
hst : { ofColex := s } ≤ { ofColex := t }
hcard : s.card ≤ t.card
ha : a ∈ s
ht : t.Nonempty
m : α := t.min' ht
h' : s ≠ t
⊢ { ofColex := s.erase a } ≤ { ofColex := t.erase m }