constructor
case a
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s t✝ : Finset α
r : ℕ
inst✝ : Fintype α
hs : s.Nonempty
t : Finset α
⊢ (∃ a ∉ t, s.card = (insert a t).card ∧ { 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
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s t✝ : Finset α
r : ℕ
inst✝ : Fintype α
hs : s.Nonempty
t : Finset α
⊢ (∃ a ∉ t, s.card = (insert a t).card ∧ { ofColex := insert a t } ≤ { ofColex := s }) →
    (s.erase (s.min' hs)).card = t.card ∧ { ofColex := t } ≤ { ofColex := s.erase (s.min' hs) }

case a.mpr
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s t✝ : Finset α
r : ℕ
inst✝ : Fintype α
hs : s.Nonempty
t : Finset α
⊢ (s.erase (s.min' hs)).card = t.card ∧ { ofColex := t } ≤ { ofColex := s.erase (s.min' hs) } →
    ∃ a ∉ t, s.card = (insert a t).card ∧ { ofColex := insert a t } ≤ { ofColex := s }