rw [insert_erase (min'_mem _ _)]
case a.mpr.inl
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s t : Finset α
r : ℕ
inst✝ : Fintype α
hs : s.Nonempty
cards' : (s.erase (s.min' hs)).card = (s.erase (s.min' hs)).card
⊢ s.card = (insert (s.min' hs) (s.erase (s.min' hs))).card ∧
    (insert (s.min' hs) (s.erase (s.min' hs)) = s ∨
      ∃ w ∈ s,
        w ∉ insert (s.min' hs) (s.erase (s.min' hs)) ∧
          ∀ ⦃a : α⦄, w < a → (a ∈ insert (s.min' hs) (s.erase (s.min' hs)) ↔ a ∈ s))
case a.mpr.inl
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s t : Finset α
r : ℕ
inst✝ : Fintype α
hs : s.Nonempty
cards' : (s.erase (s.min' hs)).card = (s.erase (s.min' hs)).card
⊢ s.card = s.card ∧ (s = s ∨ ∃ w ∈ s, w ∉ s ∧ ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ s))