-- Mathlib/Data/Finset/Powerset.lean
theorem powersetCard_sup [DecidableEq α] (u : Finset α) (n : ℕ) (hn : n < u.card) :
    (powersetCard n.succ u).sup id = u

Proof state:
case a
α : Type u_1
inst✝ : DecidableEq α
u : Finset α
n : ℕ
hn : n < #u
⊢ ∀ (b : Finset α), b ⊆ u ∧ #b = n.succ → id b ≤ u

Tactic:
rintro x ⟨h, -⟩

Result:
case a.intro
α : Type u_1
inst✝ : DecidableEq α
u : Finset α
n : ℕ
hn : n < #u
x : Finset α
h : x ⊆ u
⊢ id x ≤ u

Proof state:
case a.intro
α : Type u_1
inst✝ : DecidableEq α
u : Finset α
n : ℕ
hn : n < #u
x : α
hx : x ∈ u
t : Finset α
ht : t ∈ powersetCard n (u.erase x)
⊢ ∃ a ∈ powersetCard n.succ u, x ∈ a

Tactic:
refine ⟨insert x t, ?_, mem_insert_self _ _⟩

Result:
case a.intro
α : Type u_1
inst✝ : DecidableEq α
u : Finset α
n : ℕ
hn : n < #u
x : α
hx : x ∈ u
t : Finset α
ht : t ∈ powersetCard n (u.erase x)
⊢ insert x t ∈ powersetCard n.succ u

Proof state:
α : Type u_1
inst✝ : DecidableEq α
u : Finset α
n : ℕ
hn : n < #u
⊢ (powersetCard n.succ u).sup id = u

Tactic:
apply le_antisymm

Result:
case a
α : Type u_1
inst✝ : DecidableEq α
u : Finset α
n : ℕ
hn : n < #u
⊢ (powersetCard n.succ u).sup id ≤ u

case a
α : Type u_1
inst✝ : DecidableEq α
u : Finset α
n : ℕ
hn : n < #u
⊢ u ≤ (powersetCard n.succ u).sup id

Proof state:
case a.intro
α : Type u_1
inst✝ : DecidableEq α
u : Finset α
n : ℕ
hn : n < #u
x : α
hx : x ∈ u
t : Finset α
ht : t ∈ powersetCard n (u.erase x)
⊢ insert x t ∈ powersetCard n.succ u

Tactic:
rw [← insert_erase hx, powersetCard_succ_insert (not_mem_erase _ _)]

Result:
case a.intro
α : Type u_1
inst✝ : DecidableEq α
u : Finset α
n : ℕ
hn : n < #u
x : α
hx : x ∈ u
t : Finset α
ht : t ∈ powersetCard n (u.erase x)
⊢ insert x t ∈ powersetCard n.succ (u.erase x) ∪ image (insert x) (powersetCard n (u.erase x))

Proof state:
case a
α : Type u_1
inst✝ : DecidableEq α
u : Finset α
n : ℕ
hn : n < #u
⊢ ∀ ⦃x : α⦄, x ∈ u → x ∈ (powersetCard n.succ u).biUnion id

Tactic:
intro x hx

Result:
case a
α : Type u_1
inst✝ : DecidableEq α
u : Finset α
n : ℕ
hn : n < #u
x : α
hx : x ∈ u
⊢ x ∈ (powersetCard n.succ u).biUnion id

Proof state:
case a.intro
α : Type u_1
inst✝ : DecidableEq α
u : Finset α
n : ℕ
hn : n < #u
x : Finset α
h : x ⊆ u
⊢ id x ≤ u

Tactic:
exact h

Result:
no goals

Proof state:
case a
α : Type u_1
inst✝ : DecidableEq α
u : Finset α
n : ℕ
hn : n < #u
⊢ (powersetCard n.succ u).sup id ≤ u

Tactic:
simp_rw [Finset.sup_le_iff, mem_powersetCard]

Result:
case a
α : Type u_1
inst✝ : DecidableEq α
u : Finset α
n : ℕ
hn : n < #u
⊢ ∀ (b : Finset α), b ⊆ u ∧ #b = n.succ → id b ≤ u

Proof state:
case a
α : Type u_1
inst✝ : DecidableEq α
u : Finset α
n : ℕ
hn : n < #u
x : α
hx : x ∈ u
⊢ x ∈ (powersetCard n.succ u).biUnion id

Tactic:
simp only [mem_biUnion, exists_prop, id]

Result:
case a
α : Type u_1
inst✝ : DecidableEq α
u : Finset α
n : ℕ
hn : n < #u
x : α
hx : x ∈ u
⊢ ∃ a ∈ powersetCard n.succ u, x ∈ a

Proof state:
case a.intro
α : Type u_1
inst✝ : DecidableEq α
u : Finset α
n : ℕ
hn : n < #u
x : α
hx : x ∈ u
t : Finset α
ht : t ∈ powersetCard n (u.erase x)
⊢ insert x t ∈ powersetCard n.succ (u.erase x) ∪ image (insert x) (powersetCard n (u.erase x))

Tactic:
exact mem_union_right _ (mem_image_of_mem _ ht)

Result:
no goals

Proof state:
case a
α : Type u_1
inst✝ : DecidableEq α
u : Finset α
n : ℕ
hn : n < #u
x : α
hx : x ∈ u
⊢ ∃ a ∈ powersetCard n.succ u, x ∈ a

Tactic:
obtain ⟨t, ht⟩ : ∃ t, t ∈ powersetCard n (u.erase x) := powersetCard_nonempty.2
  (le_trans (Nat.le_sub_one_of_lt hn) pred_card_le_card_erase)

Result:
case a.intro
α : Type u_1
inst✝ : DecidableEq α
u : Finset α
n : ℕ
hn : n < #u
x : α
hx : x ∈ u
t : Finset α
ht : t ∈ powersetCard n (u.erase x)
⊢ ∃ a ∈ powersetCard n.succ u, x ∈ a

Proof state:
case a
α : Type u_1
inst✝ : DecidableEq α
u : Finset α
n : ℕ
hn : n < #u
⊢ u ≤ (powersetCard n.succ u).sup id

Tactic:
rw [sup_eq_biUnion, le_iff_subset, subset_iff]

Result:
case a
α : Type u_1
inst✝ : DecidableEq α
u : Finset α
n : ℕ
hn : n < #u
⊢ ∀ ⦃x : α⦄, x ∈ u → x ∈ (powersetCard n.succ u).biUnion id