obtain rfl | hmw : m = w ∨ m < w := (min'_le _ _ hwt).eq_or_lt
case inr.intro.intro.intro.inr
α : 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)
haw : a < w
⊢ { ofColex := s.erase a } ≤ { ofColex := t.erase m }
case inr.intro.intro.intro.inr.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
hwt : m ∈ t
hws : m ∉ s
hw : ∀ ⦃a : α⦄, m < a → (a ∈ s ↔ a ∈ t)
haw : a < m
⊢ { ofColex := s.erase a } ≤ { ofColex := t.erase m }

case inr.intro.intro.intro.inr.inr
α : 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)
haw : a < w
hmw : m < w
⊢ { ofColex := s.erase a } ≤ { ofColex := t.erase m }