rintro cards' (rfl | ⟨k, hks, hkt, z⟩)
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 →
    (t = s.erase (s.min' hs) ∨
        ∃ w ∈ s.erase (s.min' hs), w ∉ t ∧ ∀ ⦃a : α⦄, w < a → (a ∈ t ↔ a ∈ s.erase (s.min' hs))) →
      ∃ a ∉ t,
        s.card = (insert a t).card ∧
          (insert a t = s ∨ ∃ w ∈ s, w ∉ insert a t ∧ ∀ ⦃a_1 : α⦄, w < a_1 → (a_1 ∈ insert a t ↔ a_1 ∈ 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
⊢ ∃ a ∉ s.erase (s.min' hs),
    s.card = (insert a (s.erase (s.min' hs))).card ∧
      (insert a (s.erase (s.min' hs)) = s ∨
        ∃ w ∈ s,
          w ∉ insert a (s.erase (s.min' hs)) ∧ ∀ ⦃a_1 : α⦄, w < a_1 → (a_1 ∈ insert a (s.erase (s.min' hs)) ↔ a_1 ∈ s))

case a.mpr.inr.intro.intro.intro
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s t✝ : Finset α
r : ℕ
inst✝ : Fintype α
hs : s.Nonempty
t : Finset α
cards' : (s.erase (s.min' hs)).card = t.card
k : α
hks : k ∈ s.erase (s.min' hs)
hkt : k ∉ t
z : ∀ ⦃a : α⦄, k < a → (a ∈ t ↔ a ∈ s.erase (s.min' hs))
⊢ ∃ a ∉ t,
    s.card = (insert a t).card ∧
      (insert a t = s ∨ ∃ w ∈ s, w ∉ insert a t ∧ ∀ ⦃a_1 : α⦄, w < a_1 → (a_1 ∈ insert a t ↔ a_1 ∈ s))