constructor
case a.mp.intro.intro.intro
α : 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 }
⊢ (s.erase (s.min' hs)).card = t.card ∧ { ofColex := t } ≤ { ofColex := s.erase (s.min' hs) }
case a.mp.intro.intro.intro.left
α : 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 }
⊢ (s.erase (s.min' hs)).card = t.card

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) }