refine (lt_iff_exists_forall_lt.2 ⟨a, mem_erase.2 ⟨hma.ne', (hw hwa).1 ha⟩,
  not_mem_erase _ _, fun b hbs hbt ↦ ?_⟩).le
case inr.intro.intro.intro.inl
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s t : Finset α
a : α
hcard : s.card ≤ t.card
ha : a ∈ s
ht : t.Nonempty
m : α := t.min' ht
h' : s ≠ t
w : α
hwt : w ∈ t
hws : w ∉ s
hw : ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)
hwa : w < a
hma : m < a
⊢ { ofColex := s.erase a } ≤ { ofColex := t.erase m }
case inr.intro.intro.intro.inl
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s t : Finset α
a : α
hcard : s.card ≤ t.card
ha : a ∈ s
ht : t.Nonempty
m : α := t.min' ht
h' : s ≠ t
w : α
hwt : w ∈ t
hws : w ∉ s
hw : ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)
hwa : w < a
hma : m < a
b : α
hbs : b ∈ { ofColex := { val := s.val.erase a, nodup := ⋯ } }.ofColex
hbt : b ∉ { ofColex := { val := t.val.erase m, nodup := ⋯ } }.ofColex
⊢ b < a