case a
α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
u : Finset α
n : ℕ
hn : n < card u
⊢ sup (powersetLen (Nat.succ n) u) id ≤ u

case a
α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
u : Finset α
n : ℕ
hn : n < card u
⊢ u ≤ sup (powersetLen (Nat.succ n) u) id
α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
u : Finset α
n : ℕ
hn : n < card u
⊢ sup (powersetLen (Nat.succ n) u) id = u
apply le_antisymm
case a
α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
u : Finset α
n : ℕ
hn : n < card u
⊢ ∀ (b : Finset α), b ⊆ u ∧ card b = Nat.succ n → id b ≤ u
case a
α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
u : Finset α
n : ℕ
hn : n < card u
⊢ sup (powersetLen (Nat.succ n) u) id ≤ u
simp_rw [Finset.sup_le_iff, mem_powersetLen]
case a.intro
α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
u : Finset α
n : ℕ
hn : n < card u
x : Finset α
h : x ⊆ u
⊢ id x ≤ u
case a
α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
u : Finset α
n : ℕ
hn : n < card u
⊢ ∀ (b : Finset α), b ⊆ u ∧ card b = Nat.succ n → id b ≤ u
rintro x ⟨h, -⟩
no goals
case a.intro
α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
u : Finset α
n : ℕ
hn : n < card u
x : Finset α
h : x ⊆ u
⊢ id x ≤ u
exact h
case a
α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
u : Finset α
n : ℕ
hn : n < card u
⊢ ∀ ⦃x : α⦄, x ∈ u → x ∈ Finset.biUnion (powersetLen (Nat.succ n) u) id
case a
α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
u : Finset α
n : ℕ
hn : n < card u
⊢ u ≤ sup (powersetLen (Nat.succ n) u) id
rw [sup_eq_biUnion, le_iff_subset, subset_iff]
case a.inl
α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
u : Finset α
n : ℕ
hn : n < card u
h' : Nat.succ n = card u
⊢ ∀ ⦃x : α⦄, x ∈ u → x ∈ Finset.biUnion (powersetLen (Nat.succ n) u) id

case a.inr
α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
u : Finset α
n : ℕ
hn : n < card u
h' : Nat.succ n < card u
⊢ ∀ ⦃x : α⦄, x ∈ u → x ∈ Finset.biUnion (powersetLen (Nat.succ n) u) id
case a
α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
u : Finset α
n : ℕ
hn : n < card u
⊢ ∀ ⦃x : α⦄, x ∈ u → x ∈ Finset.biUnion (powersetLen (Nat.succ n) u) id
cases' (Nat.succ_le_of_lt hn).eq_or_lt with h' h'
no goals
case a.inl
α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
u : Finset α
n : ℕ
hn : n < card u
h' : Nat.succ n = card u
⊢ ∀ ⦃x : α⦄, x ∈ u → x ∈ Finset.biUnion (powersetLen (Nat.succ n) u) id
simp [h']
case a.inr
α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
u : Finset α
n : ℕ
hn : n < card u
h' : Nat.succ n < card u
x : α
hx : x ∈ u
⊢ x ∈ Finset.biUnion (powersetLen (Nat.succ n) u) id
case a.inr
α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
u : Finset α
n : ℕ
hn : n < card u
h' : Nat.succ n < card u
⊢ ∀ ⦃x : α⦄, x ∈ u → x ∈ Finset.biUnion (powersetLen (Nat.succ n) u) id
intro x hx
case a.inr
α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
u : Finset α
n : ℕ
hn : n < card u
h' : Nat.succ n < card u
x : α
hx : x ∈ u
⊢ ∃ a, a ∈ powersetLen (Nat.succ n) u ∧ x ∈ a
case a.inr
α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
u : Finset α
n : ℕ
hn : n < card u
h' : Nat.succ n < card u
x : α
hx : x ∈ u
⊢ x ∈ Finset.biUnion (powersetLen (Nat.succ n) u) id
simp only [mem_biUnion, exists_prop, id.def]
case a.inr.intro
α : Type u_1
s t✝ : Finset α
inst✝ : DecidableEq α
u : Finset α
n : ℕ
hn : n < card u
h' : Nat.succ n < card u
x : α
hx : x ∈ u
t : Finset α
ht : t ∈ powersetLen n (erase u x)
⊢ ∃ a, a ∈ powersetLen (Nat.succ n) u ∧ x ∈ a
case a.inr
α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
u : Finset α
n : ℕ
hn : n < card u
h' : Nat.succ n < card u
x : α
hx : x ∈ u
⊢ ∃ a, a ∈ powersetLen (Nat.succ n) u ∧ x ∈ a
obtain ⟨t, ht⟩ : ∃ t, t ∈ powersetLen n (u.erase x) := powersetLen_nonempty
  (le_trans (Nat.le_pred_of_lt hn) pred_card_le_card_erase)
case a.inr.intro
α : Type u_1
s t✝ : Finset α
inst✝ : DecidableEq α
u : Finset α
n : ℕ
hn : n < card u
h' : Nat.succ n < card u
x : α
hx : x ∈ u
t : Finset α
ht : t ∈ powersetLen n (erase u x)
⊢ insert x t ∈ powersetLen (Nat.succ n) u
case a.inr.intro
α : Type u_1
s t✝ : Finset α
inst✝ : DecidableEq α
u : Finset α
n : ℕ
hn : n < card u
h' : Nat.succ n < card u
x : α
hx : x ∈ u
t : Finset α
ht : t ∈ powersetLen n (erase u x)
⊢ ∃ a, a ∈ powersetLen (Nat.succ n) u ∧ x ∈ a
refine' ⟨insert x t, _, mem_insert_self _ _⟩
case a.inr.intro
α : Type u_1
s t✝ : Finset α
inst✝ : DecidableEq α
u : Finset α
n : ℕ
hn : n < card u
h' : Nat.succ n < card u
x : α
hx : x ∈ u
t : Finset α
ht : t ∈ powersetLen n (erase u x)
⊢ insert x t ∈ powersetLen (Nat.succ n) (erase u x) ∪ image (insert x) (powersetLen n (erase u x))
case a.inr.intro
α : Type u_1
s t✝ : Finset α
inst✝ : DecidableEq α
u : Finset α
n : ℕ
hn : n < card u
h' : Nat.succ n < card u
x : α
hx : x ∈ u
t : Finset α
ht : t ∈ powersetLen n (erase u x)
⊢ insert x t ∈ powersetLen (Nat.succ n) u
rw [← insert_erase hx, powersetLen_succ_insert (not_mem_erase _ _)]
no goals
case a.inr.intro
α : Type u_1
s t✝ : Finset α
inst✝ : DecidableEq α
u : Finset α
n : ℕ
hn : n < card u
h' : Nat.succ n < card u
x : α
hx : x ∈ u
t : Finset α
ht : t ∈ powersetLen n (erase u x)
⊢ insert x t ∈ powersetLen (Nat.succ n) (erase u x) ∪ image (insert x) (powersetLen n (erase u x))
exact mem_union_right _ (mem_image_of_mem _ ht)