have hcard : card s = card (insert j t) := by
  rw [card_insert_of_not_mem ‹j ∉ t›, ← ‹_ = card t›, card_erase_add_one (min'_mem _ _)]
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))
j : α := tᶜ.min' ⋯
hjk : j ≤ k
this : j ∉ t
⊢ ∃ 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.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))
j : α := tᶜ.min' ⋯
hjk : j ≤ k
this : j ∉ t
hcard : s.card = (insert j t).card
⊢ ∃ 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))