simpa [ha] using erase_le_erase_min' hts hst.ge (mem_insert_self _ _)
case a.mp.intro.intro.intro.right
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s t✝ : Finset α
r : ℕ
inst✝ : Fintype α
hs : s.Nonempty
t : Finset α
a : α
ha : a ∉ t
hst : s.card = (insert a t).card
hts : { ofColex := insert a t } ≤ { ofColex := s }
⊢ { ofColex := t } ≤ { ofColex := s.erase (s.min' hs) }
no goals