[GOAL]
α : Type u_1
s✝ t✝ s t : Finset α
⊢ s ∈ powerset t ↔ s ⊆ t
[PROOFSTEP]
cases s
[GOAL]
case mk
α : Type u_1
s t✝ t : Finset α
val✝ : Multiset α
nodup✝ : Nodup val✝
⊢ { val := val✝, nodup := nodup✝ } ∈ powerset t ↔ { val := val✝, nodup := nodup✝ } ⊆ t
[PROOFSTEP]
simp [powerset, mem_mk, mem_pmap, mk.injEq, mem_powerset, exists_prop, exists_eq_right, ← val_le_iff]
[GOAL]
α : Type u_1
s✝ t s : Finset α
⊢ ↑(powerset s) = toSet ⁻¹' 𝒫↑s
[PROOFSTEP]
ext
[GOAL]
case h
α : Type u_1
s✝ t s x✝ : Finset α
⊢ x✝ ∈ ↑(powerset s) ↔ x✝ ∈ toSet ⁻¹' 𝒫↑s
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
s t : Finset α
⊢ powerset s = {∅} ↔ s = ∅
[PROOFSTEP]
rw [← powerset_empty, powerset_inj]
[GOAL]
α : Type u_1
s✝ t✝ s t : Finset α
a : α
ht : t ∈ powerset s
h : ¬a ∈ s
⊢ ¬a ∈ t
[PROOFSTEP]
apply mt _ h
[GOAL]
α : Type u_1
s✝ t✝ s t : Finset α
a : α
ht : t ∈ powerset s
h : ¬a ∈ s
⊢ a ∈ t → a ∈ s
[PROOFSTEP]
apply mem_powerset.1 ht
[GOAL]
α : Type u_1
s✝ t : Finset α
inst✝ : DecidableEq α
s : Finset α
a : α
⊢ powerset (insert a s) = powerset s ∪ image (insert a) (powerset s)
[PROOFSTEP]
ext t
[GOAL]
case a
α : Type u_1
s✝ t✝ : Finset α
inst✝ : DecidableEq α
s : Finset α
a : α
t : Finset α
⊢ t ∈ powerset (insert a s) ↔ t ∈ powerset s ∪ image (insert a) (powerset s)
[PROOFSTEP]
simp only [exists_prop, mem_powerset, mem_image, mem_union, subset_insert_iff]
[GOAL]
case a
α : Type u_1
s✝ t✝ : Finset α
inst✝ : DecidableEq α
s : Finset α
a : α
t : Finset α
⊢ erase t a ⊆ s ↔ t ⊆ s ∨ ∃ a_1, a_1 ⊆ s ∧ insert a a_1 = t
[PROOFSTEP]
by_cases h : a ∈ t
[GOAL]
case pos
α : Type u_1
s✝ t✝ : Finset α
inst✝ : DecidableEq α
s : Finset α
a : α
t : Finset α
h : a ∈ t
⊢ erase t a ⊆ s ↔ t ⊆ s ∨ ∃ a_1, a_1 ⊆ s ∧ insert a a_1 = t
[PROOFSTEP]
constructor
[GOAL]
case pos.mp
α : Type u_1
s✝ t✝ : Finset α
inst✝ : DecidableEq α
s : Finset α
a : α
t : Finset α
h : a ∈ t
⊢ erase t a ⊆ s → t ⊆ s ∨ ∃ a_2, a_2 ⊆ s ∧ insert a a_2 = t
[PROOFSTEP]
exact fun H => Or.inr ⟨_, H, insert_erase h⟩
[GOAL]
case pos.mpr
α : Type u_1
s✝ t✝ : Finset α
inst✝ : DecidableEq α
s : Finset α
a : α
t : Finset α
h : a ∈ t
⊢ (t ⊆ s ∨ ∃ a_1, a_1 ⊆ s ∧ insert a a_1 = t) → erase t a ⊆ s
[PROOFSTEP]
intro H
[GOAL]
case pos.mpr
α : Type u_1
s✝ t✝ : Finset α
inst✝ : DecidableEq α
s : Finset α
a : α
t : Finset α
h : a ∈ t
H : t ⊆ s ∨ ∃ a_1, a_1 ⊆ s ∧ insert a a_1 = t
⊢ erase t a ⊆ s
[PROOFSTEP]
cases' H with H H
[GOAL]
case pos.mpr.inl
α : Type u_1
s✝ t✝ : Finset α
inst✝ : DecidableEq α
s : Finset α
a : α
t : Finset α
h : a ∈ t
H : t ⊆ s
⊢ erase t a ⊆ s
[PROOFSTEP]
exact Subset.trans (erase_subset a t) H
[GOAL]
case pos.mpr.inr
α : Type u_1
s✝ t✝ : Finset α
inst✝ : DecidableEq α
s : Finset α
a : α
t : Finset α
h : a ∈ t
H : ∃ a_1, a_1 ⊆ s ∧ insert a a_1 = t
⊢ erase t a ⊆ s
[PROOFSTEP]
rcases H with ⟨u, hu⟩
[GOAL]
case pos.mpr.inr.intro
α : Type u_1
s✝ t✝ : Finset α
inst✝ : DecidableEq α
s : Finset α
a : α
t : Finset α
h : a ∈ t
u : Finset α
hu : u ⊆ s ∧ insert a u = t
⊢ erase t a ⊆ s
[PROOFSTEP]
rw [← hu.2]
[GOAL]
case pos.mpr.inr.intro
α : Type u_1
s✝ t✝ : Finset α
inst✝ : DecidableEq α
s : Finset α
a : α
t : Finset α
h : a ∈ t
u : Finset α
hu : u ⊆ s ∧ insert a u = t
⊢ erase (insert a u) a ⊆ s
[PROOFSTEP]
exact Subset.trans (erase_insert_subset a u) hu.1
[GOAL]
case neg
α : Type u_1
s✝ t✝ : Finset α
inst✝ : DecidableEq α
s : Finset α
a : α
t : Finset α
h : ¬a ∈ t
⊢ erase t a ⊆ s ↔ t ⊆ s ∨ ∃ a_1, a_1 ⊆ s ∧ insert a a_1 = t
[PROOFSTEP]
have : ¬∃ u : Finset α, u ⊆ s ∧ insert a u = t := by simp [Ne.symm (ne_insert_of_not_mem _ _ h)]
[GOAL]
α : Type u_1
s✝ t✝ : Finset α
inst✝ : DecidableEq α
s : Finset α
a : α
t : Finset α
h : ¬a ∈ t
⊢ ¬∃ u, u ⊆ s ∧ insert a u = t
[PROOFSTEP]
simp [Ne.symm (ne_insert_of_not_mem _ _ h)]
[GOAL]
case neg
α : Type u_1
s✝ t✝ : Finset α
inst✝ : DecidableEq α
s : Finset α
a : α
t : Finset α
h : ¬a ∈ t
this : ¬∃ u, u ⊆ s ∧ insert a u = t
⊢ erase t a ⊆ s ↔ t ⊆ s ∨ ∃ a_1, a_1 ⊆ s ∧ insert a a_1 = t
[PROOFSTEP]
simp [Finset.erase_eq_of_not_mem h, this]
[GOAL]
α : Type u_1
s✝ t✝ : Finset α
inst✝ : DecidableEq α
s t : Finset α
⊢ t ∈ ssubsets s ↔ t ⊂ s
[PROOFSTEP]
rw [ssubsets, mem_erase, mem_powerset, ssubset_iff_subset_ne, and_comm]
[GOAL]
α : Type u_1
s✝ t : Finset α
inst✝ : DecidableEq α
s : Finset α
h : Finset.Nonempty s
⊢ ∅ ∈ ssubsets s
[PROOFSTEP]
rw [mem_ssubsets, ssubset_iff_subset_ne]
[GOAL]
α : Type u_1
s✝ t : Finset α
inst✝ : DecidableEq α
s : Finset α
h : Finset.Nonempty s
⊢ ∅ ⊆ s ∧ ∅ ≠ s
[PROOFSTEP]
exact ⟨empty_subset s, h.ne_empty.symm⟩
[GOAL]
α : Type u_1
s✝ t✝ : Finset α
n : ℕ
s t : Finset α
⊢ s ∈ powersetLen n t ↔ s ⊆ t ∧ card s = n
[PROOFSTEP]
cases s
[GOAL]
case mk
α : Type u_1
s t✝ : Finset α
n : ℕ
t : Finset α
val✝ : Multiset α
nodup✝ : Nodup val✝
⊢ { val := val✝, nodup := nodup✝ } ∈ powersetLen n t ↔
    { val := val✝, nodup := nodup✝ } ⊆ t ∧ card { val := val✝, nodup := nodup✝ } = n
[PROOFSTEP]
simp [powersetLen, val_le_iff.symm]
[GOAL]
α : Type u_1
s✝ t s : Finset α
⊢ powersetLen 0 s = {∅}
[PROOFSTEP]
ext
[GOAL]
case a
α : Type u_1
s✝ t s a✝ : Finset α
⊢ a✝ ∈ powersetLen 0 s ↔ a✝ ∈ {∅}
[PROOFSTEP]
rw [mem_powersetLen, mem_singleton, card_eq_zero]
[GOAL]
case a
α : Type u_1
s✝ t s a✝ : Finset α
⊢ a✝ ⊆ s ∧ a✝ = ∅ ↔ a✝ = ∅
[PROOFSTEP]
refine'
  ⟨fun h => h.2, fun h => by
    rw [h]
    exact ⟨empty_subset s, rfl⟩⟩
[GOAL]
α : Type u_1
s✝ t s a✝ : Finset α
h : a✝ = ∅
⊢ a✝ ⊆ s ∧ a✝ = ∅
[PROOFSTEP]
rw [h]
[GOAL]
α : Type u_1
s✝ t s a✝ : Finset α
h : a✝ = ∅
⊢ ∅ ⊆ s ∧ ∅ = ∅
[PROOFSTEP]
exact ⟨empty_subset s, rfl⟩
[GOAL]
α : Type u_1
s✝ t : Finset α
n : ℕ
s : Finset α
h : card s < n
⊢ card (powersetLen n s) = 0
[PROOFSTEP]
rw [card_powersetLen, Nat.choose_eq_zero_of_lt h]
[GOAL]
α : Type u_1
s✝ t : Finset α
n : ℕ
s : Finset α
⊢ powersetLen n s = filter (fun x => card x = n) (powerset s)
[PROOFSTEP]
ext
[GOAL]
case a
α : Type u_1
s✝ t : Finset α
n : ℕ
s a✝ : Finset α
⊢ a✝ ∈ powersetLen n s ↔ a✝ ∈ filter (fun x => card x = n) (powerset s)
[PROOFSTEP]
simp [mem_powersetLen]
[GOAL]
α : Type u_1
s✝ t : Finset α
inst✝ : DecidableEq α
x : α
s : Finset α
h : ¬x ∈ s
n : ℕ
⊢ powersetLen (Nat.succ n) (insert x s) = powersetLen (Nat.succ n) s ∪ image (insert x) (powersetLen n s)
[PROOFSTEP]
rw [powersetLen_eq_filter, powerset_insert, filter_union, ← powersetLen_eq_filter]
[GOAL]
α : Type u_1
s✝ t : Finset α
inst✝ : DecidableEq α
x : α
s : Finset α
h : ¬x ∈ s
n : ℕ
⊢ powersetLen (Nat.succ n) s ∪ filter (fun x => card x = Nat.succ n) (image (insert x) (powerset s)) =
    powersetLen (Nat.succ n) s ∪ image (insert x) (powersetLen n s)
[PROOFSTEP]
congr
[GOAL]
case e_a
α : Type u_1
s✝ t : Finset α
inst✝ : DecidableEq α
x : α
s : Finset α
h : ¬x ∈ s
n : ℕ
⊢ filter (fun x => card x = Nat.succ n) (image (insert x) (powerset s)) = image (insert x) (powersetLen n s)
[PROOFSTEP]
rw [powersetLen_eq_filter, image_filter]
[GOAL]
case e_a
α : Type u_1
s✝ t : Finset α
inst✝ : DecidableEq α
x : α
s : Finset α
h : ¬x ∈ s
n : ℕ
⊢ image (insert x) (filter ((fun x => card x = Nat.succ n) ∘ insert x) (powerset s)) =
    image (insert x) (filter (fun x => card x = n) (powerset s))
[PROOFSTEP]
congr 1
[GOAL]
case e_a.e_s
α : Type u_1
s✝ t : Finset α
inst✝ : DecidableEq α
x : α
s : Finset α
h : ¬x ∈ s
n : ℕ
⊢ filter ((fun x => card x = Nat.succ n) ∘ insert x) (powerset s) = filter (fun x => card x = n) (powerset s)
[PROOFSTEP]
ext t
[GOAL]
case e_a.e_s.a
α : Type u_1
s✝ t✝ : Finset α
inst✝ : DecidableEq α
x : α
s : Finset α
h : ¬x ∈ s
n : ℕ
t : Finset α
⊢ t ∈ filter ((fun x => card x = Nat.succ n) ∘ insert x) (powerset s) ↔ t ∈ filter (fun x => card x = n) (powerset s)
[PROOFSTEP]
simp only [mem_powerset, mem_filter, Function.comp_apply, and_congr_right_iff]
[GOAL]
case e_a.e_s.a
α : Type u_1
s✝ t✝ : Finset α
inst✝ : DecidableEq α
x : α
s : Finset α
h : ¬x ∈ s
n : ℕ
t : Finset α
⊢ t ⊆ s → (card (insert x t) = Nat.succ n ↔ card t = n)
[PROOFSTEP]
intro ht
[GOAL]
case e_a.e_s.a
α : Type u_1
s✝ t✝ : Finset α
inst✝ : DecidableEq α
x : α
s : Finset α
h : ¬x ∈ s
n : ℕ
t : Finset α
ht : t ⊆ s
⊢ card (insert x t) = Nat.succ n ↔ card t = n
[PROOFSTEP]
have : x ∉ t := fun H => h (ht H)
[GOAL]
case e_a.e_s.a
α : Type u_1
s✝ t✝ : Finset α
inst✝ : DecidableEq α
x : α
s : Finset α
h : ¬x ∈ s
n : ℕ
t : Finset α
ht : t ⊆ s
this : ¬x ∈ t
⊢ card (insert x t) = Nat.succ n ↔ card t = n
[PROOFSTEP]
simp [card_insert_of_not_mem this, Nat.succ_inj']
[GOAL]
α : Type u_1
s✝ t : Finset α
n : ℕ
s : Finset α
h : n ≤ card s
⊢ Finset.Nonempty (powersetLen n s)
[PROOFSTEP]
classical
induction' s using Finset.induction_on with x s hx IH generalizing n
· rw [card_empty, le_zero_iff] at h 
  rw [h, powersetLen_zero]
  exact Finset.singleton_nonempty _
· cases n
  · simp
  · rw [card_insert_of_not_mem hx, Nat.succ_le_succ_iff] at h 
    rw [powersetLen_succ_insert hx]
    refine' Nonempty.mono _ ((IH h).image (insert x))
    exact subset_union_right _ _
[GOAL]
α : Type u_1
s✝ t : Finset α
n : ℕ
s : Finset α
h : n ≤ card s
⊢ Finset.Nonempty (powersetLen n s)
[PROOFSTEP]
induction' s using Finset.induction_on with x s hx IH generalizing n
[GOAL]
case empty
α : Type u_1
s✝ t : Finset α
n✝ : ℕ
s : Finset α
h✝ : n✝ ≤ card s
n : ℕ
h : n ≤ card ∅
⊢ Finset.Nonempty (powersetLen n ∅)
[PROOFSTEP]
rw [card_empty, le_zero_iff] at h 
[GOAL]
case empty
α : Type u_1
s✝ t : Finset α
n✝ : ℕ
s : Finset α
h✝ : n✝ ≤ card s
n : ℕ
h : n = 0
⊢ Finset.Nonempty (powersetLen n ∅)
[PROOFSTEP]
rw [h, powersetLen_zero]
[GOAL]
case empty
α : Type u_1
s✝ t : Finset α
n✝ : ℕ
s : Finset α
h✝ : n✝ ≤ card s
n : ℕ
h : n = 0
⊢ Finset.Nonempty {∅}
[PROOFSTEP]
exact Finset.singleton_nonempty _
[GOAL]
case insert
α : Type u_1
s✝¹ t : Finset α
n✝ : ℕ
s✝ : Finset α
h✝ : n✝ ≤ card s✝
x : α
s : Finset α
hx : ¬x ∈ s
IH : ∀ {n : ℕ}, n ≤ card s → Finset.Nonempty (powersetLen n s)
n : ℕ
h : n ≤ card (insert x s)
⊢ Finset.Nonempty (powersetLen n (insert x s))
[PROOFSTEP]
cases n
[GOAL]
case insert.zero
α : Type u_1
s✝¹ t : Finset α
n : ℕ
s✝ : Finset α
h✝ : n ≤ card s✝
x : α
s : Finset α
hx : ¬x ∈ s
IH : ∀ {n : ℕ}, n ≤ card s → Finset.Nonempty (powersetLen n s)
h : Nat.zero ≤ card (insert x s)
⊢ Finset.Nonempty (powersetLen Nat.zero (insert x s))
[PROOFSTEP]
simp
[GOAL]
case insert.succ
α : Type u_1
s✝¹ t : Finset α
n : ℕ
s✝ : Finset α
h✝ : n ≤ card s✝
x : α
s : Finset α
hx : ¬x ∈ s
IH : ∀ {n : ℕ}, n ≤ card s → Finset.Nonempty (powersetLen n s)
n✝ : ℕ
h : Nat.succ n✝ ≤ card (insert x s)
⊢ Finset.Nonempty (powersetLen (Nat.succ n✝) (insert x s))
[PROOFSTEP]
rw [card_insert_of_not_mem hx, Nat.succ_le_succ_iff] at h 
[GOAL]
case insert.succ
α : Type u_1
s✝¹ t : Finset α
n : ℕ
s✝ : Finset α
h✝ : n ≤ card s✝
x : α
s : Finset α
hx : ¬x ∈ s
IH : ∀ {n : ℕ}, n ≤ card s → Finset.Nonempty (powersetLen n s)
n✝ : ℕ
h : n✝ ≤ card s
⊢ Finset.Nonempty (powersetLen (Nat.succ n✝) (insert x s))
[PROOFSTEP]
rw [powersetLen_succ_insert hx]
[GOAL]
case insert.succ
α : Type u_1
s✝¹ t : Finset α
n : ℕ
s✝ : Finset α
h✝ : n ≤ card s✝
x : α
s : Finset α
hx : ¬x ∈ s
IH : ∀ {n : ℕ}, n ≤ card s → Finset.Nonempty (powersetLen n s)
n✝ : ℕ
h : n✝ ≤ card s
⊢ Finset.Nonempty (powersetLen (Nat.succ n✝) s ∪ image (insert x) (powersetLen n✝ s))
[PROOFSTEP]
refine' Nonempty.mono _ ((IH h).image (insert x))
[GOAL]
case insert.succ
α : Type u_1
s✝¹ t : Finset α
n : ℕ
s✝ : Finset α
h✝ : n ≤ card s✝
x : α
s : Finset α
hx : ¬x ∈ s
IH : ∀ {n : ℕ}, n ≤ card s → Finset.Nonempty (powersetLen n s)
n✝ : ℕ
h : n✝ ≤ card s
⊢ image (insert x) (powersetLen n✝ s) ⊆ powersetLen (Nat.succ n✝) s ∪ image (insert x) (powersetLen n✝ s)
[PROOFSTEP]
exact subset_union_right _ _
[GOAL]
α : Type u_1
s✝ t s : Finset α
⊢ powersetLen (card s) s = {s}
[PROOFSTEP]
ext
[GOAL]
case a
α : Type u_1
s✝ t s a✝ : Finset α
⊢ a✝ ∈ powersetLen (card s) s ↔ a✝ ∈ {s}
[PROOFSTEP]
rw [mem_powersetLen, mem_singleton]
[GOAL]
case a
α : Type u_1
s✝ t s a✝ : Finset α
⊢ a✝ ⊆ s ∧ card a✝ = card s ↔ a✝ = s
[PROOFSTEP]
constructor
[GOAL]
case a.mp
α : Type u_1
s✝ t s a✝ : Finset α
⊢ a✝ ⊆ s ∧ card a✝ = card s → a✝ = s
[PROOFSTEP]
exact fun ⟨hs, hc⟩ => eq_of_subset_of_card_le hs hc.ge
[GOAL]
case a.mpr
α : Type u_1
s✝ t s a✝ : Finset α
⊢ a✝ = s → a✝ ⊆ s ∧ card a✝ = card s
[PROOFSTEP]
rintro rfl
[GOAL]
case a.mpr
α : Type u_1
s t a✝ : Finset α
⊢ a✝ ⊆ a✝ ∧ card a✝ = card a✝
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
s✝ t s : Finset α
⊢ powerset s =
    disjiUnion (range (card s + 1)) (fun i => powersetLen i s)
      (_ : Set.Pairwise ↑(range (card s + 1)) fun i j => _root_.Disjoint (powersetLen i s) (powersetLen j s))
[PROOFSTEP]
refine' ext fun a => ⟨fun ha => _, fun ha => _⟩
[GOAL]
case refine'_1
α : Type u_1
s✝ t s a : Finset α
ha : a ∈ powerset s
⊢ a ∈
    disjiUnion (range (card s + 1)) (fun i => powersetLen i s)
      (_ : Set.Pairwise ↑(range (card s + 1)) fun i j => _root_.Disjoint (powersetLen i s) (powersetLen j s))
[PROOFSTEP]
rw [mem_disjiUnion]
[GOAL]
case refine'_1
α : Type u_1
s✝ t s a : Finset α
ha : a ∈ powerset s
⊢ ∃ a_1, a_1 ∈ range (card s + 1) ∧ a ∈ powersetLen a_1 s
[PROOFSTEP]
exact
  ⟨a.card, mem_range.mpr (Nat.lt_succ_of_le (card_le_of_subset (mem_powerset.mp ha))),
    mem_powersetLen.mpr ⟨mem_powerset.mp ha, rfl⟩⟩
[GOAL]
case refine'_2
α : Type u_1
s✝ t s a : Finset α
ha :
  a ∈
    disjiUnion (range (card s + 1)) (fun i => powersetLen i s)
      (_ : Set.Pairwise ↑(range (card s + 1)) fun i j => _root_.Disjoint (powersetLen i s) (powersetLen j s))
⊢ a ∈ powerset s
[PROOFSTEP]
rcases mem_disjiUnion.mp ha with ⟨i, _hi, ha⟩
[GOAL]
case refine'_2.intro.intro
α : Type u_1
s✝ t s a : Finset α
ha✝ :
  a ∈
    disjiUnion (range (card s + 1)) (fun i => powersetLen i s)
      (_ : Set.Pairwise ↑(range (card s + 1)) fun i j => _root_.Disjoint (powersetLen i s) (powersetLen j s))
i : ℕ
_hi : i ∈ range (card s + 1)
ha : a ∈ powersetLen i s
⊢ a ∈ powerset s
[PROOFSTEP]
exact mem_powerset.mpr (mem_powersetLen.mp ha).1
[GOAL]
α : Type u_1
s✝ t : Finset α
inst✝ : DecidableEq (Finset α)
s : Finset α
⊢ powerset s = Finset.biUnion (range (card s + 1)) fun i => powersetLen i s
[PROOFSTEP]
simpa only [disjiUnion_eq_biUnion] using powerset_card_disjiUnion s
[GOAL]
α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
u : Finset α
n : ℕ
hn : n < card u
⊢ sup (powersetLen (Nat.succ n) u) id = u
[PROOFSTEP]
apply le_antisymm
[GOAL]
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
[PROOFSTEP]
simp_rw [Finset.sup_le_iff, mem_powersetLen]
[GOAL]
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
[PROOFSTEP]
rintro x ⟨h, -⟩
[GOAL]
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
[PROOFSTEP]
exact h
[GOAL]
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
[PROOFSTEP]
rw [sup_eq_biUnion, le_iff_subset, subset_iff]
[GOAL]
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
[PROOFSTEP]
cases' (Nat.succ_le_of_lt hn).eq_or_lt with h' h'
[GOAL]
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
[PROOFSTEP]
simp [h']
[GOAL]
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
[PROOFSTEP]
intro x hx
[GOAL]
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
[PROOFSTEP]
simp only [mem_biUnion, exists_prop, id.def]
[GOAL]
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
[PROOFSTEP]
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)
[GOAL]
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
[PROOFSTEP]
refine' ⟨insert x t, _, mem_insert_self _ _⟩
[GOAL]
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
[PROOFSTEP]
rw [← insert_erase hx, powersetLen_succ_insert (not_mem_erase _ _)]
[GOAL]
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))
[PROOFSTEP]
exact mem_union_right _ (mem_image_of_mem _ ht)
[GOAL]
α : Type u_1
s✝ t s : Finset α
i : ℕ
⊢ Multiset.map val (powersetLen i s).val = Multiset.powersetLen i s.val
[PROOFSTEP]
simp [Finset.powersetLen, map_pmap, pmap_eq_map, map_id']
[GOAL]
α : Type u_1
s✝ t✝ : Finset α
β : Type u_2
f : α ↪ β
n : ℕ
s : Finset α
t : Finset β
⊢ t ∈ powersetLen n (map f s) ↔ t ∈ map (mapEmbedding f).toEmbedding (powersetLen n s)
[PROOFSTEP]
simp only [card_map, mem_powersetLen, le_eq_subset, gt_iff_lt, mem_map, mapEmbedding_apply]
[GOAL]
α : Type u_1
s✝ t✝ : Finset α
β : Type u_2
f : α ↪ β
n : ℕ
s : Finset α
t : Finset β
⊢ t ⊆ map f s ∧ card t = n ↔ ∃ a, (a ⊆ s ∧ card a = n) ∧ ↑(mapEmbedding f).toEmbedding a = t
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
s✝ t✝ : Finset α
β : Type u_2
f : α ↪ β
n : ℕ
s : Finset α
t : Finset β
⊢ t ⊆ map f s ∧ card t = n → ∃ a, (a ⊆ s ∧ card a = n) ∧ ↑(mapEmbedding f).toEmbedding a = t
[PROOFSTEP]
classical
intro h
have : map f (filter (fun x => (f x ∈ t)) s) = t := by
  ext x
  simp only [mem_map, mem_filter, decide_eq_true_eq]
  exact
    ⟨fun ⟨_y, ⟨_hy₁, hy₂⟩, hy₃⟩ => hy₃ ▸ hy₂, fun hx =>
      let ⟨y, hy⟩ := mem_map.1 (h.1 hx);
      ⟨y, ⟨hy.1, hy.2 ▸ hx⟩, hy.2⟩⟩
refine' ⟨_, _, this⟩
rw [← card_map f, this, h.2]; simp
[GOAL]
case mp
α : Type u_1
s✝ t✝ : Finset α
β : Type u_2
f : α ↪ β
n : ℕ
s : Finset α
t : Finset β
⊢ t ⊆ map f s ∧ card t = n → ∃ a, (a ⊆ s ∧ card a = n) ∧ ↑(mapEmbedding f).toEmbedding a = t
[PROOFSTEP]
intro h
[GOAL]
case mp
α : Type u_1
s✝ t✝ : Finset α
β : Type u_2
f : α ↪ β
n : ℕ
s : Finset α
t : Finset β
h : t ⊆ map f s ∧ card t = n
⊢ ∃ a, (a ⊆ s ∧ card a = n) ∧ ↑(mapEmbedding f).toEmbedding a = t
[PROOFSTEP]
have : map f (filter (fun x => (f x ∈ t)) s) = t := by
  ext x
  simp only [mem_map, mem_filter, decide_eq_true_eq]
  exact
    ⟨fun ⟨_y, ⟨_hy₁, hy₂⟩, hy₃⟩ => hy₃ ▸ hy₂, fun hx =>
      let ⟨y, hy⟩ := mem_map.1 (h.1 hx);
      ⟨y, ⟨hy.1, hy.2 ▸ hx⟩, hy.2⟩⟩
[GOAL]
α : Type u_1
s✝ t✝ : Finset α
β : Type u_2
f : α ↪ β
n : ℕ
s : Finset α
t : Finset β
h : t ⊆ map f s ∧ card t = n
⊢ map f (filter (fun x => ↑f x ∈ t) s) = t
[PROOFSTEP]
ext x
[GOAL]
case a
α : Type u_1
s✝ t✝ : Finset α
β : Type u_2
f : α ↪ β
n : ℕ
s : Finset α
t : Finset β
h : t ⊆ map f s ∧ card t = n
x : β
⊢ x ∈ map f (filter (fun x => ↑f x ∈ t) s) ↔ x ∈ t
[PROOFSTEP]
simp only [mem_map, mem_filter, decide_eq_true_eq]
[GOAL]
case a
α : Type u_1
s✝ t✝ : Finset α
β : Type u_2
f : α ↪ β
n : ℕ
s : Finset α
t : Finset β
h : t ⊆ map f s ∧ card t = n
x : β
⊢ (∃ a, (a ∈ s ∧ ↑f a ∈ t) ∧ ↑f a = x) ↔ x ∈ t
[PROOFSTEP]
exact
  ⟨fun ⟨_y, ⟨_hy₁, hy₂⟩, hy₃⟩ => hy₃ ▸ hy₂, fun hx =>
    let ⟨y, hy⟩ := mem_map.1 (h.1 hx);
    ⟨y, ⟨hy.1, hy.2 ▸ hx⟩, hy.2⟩⟩
[GOAL]
case mp
α : Type u_1
s✝ t✝ : Finset α
β : Type u_2
f : α ↪ β
n : ℕ
s : Finset α
t : Finset β
h : t ⊆ map f s ∧ card t = n
this : map f (filter (fun x => ↑f x ∈ t) s) = t
⊢ ∃ a, (a ⊆ s ∧ card a = n) ∧ ↑(mapEmbedding f).toEmbedding a = t
[PROOFSTEP]
refine' ⟨_, _, this⟩
[GOAL]
case mp
α : Type u_1
s✝ t✝ : Finset α
β : Type u_2
f : α ↪ β
n : ℕ
s : Finset α
t : Finset β
h : t ⊆ map f s ∧ card t = n
this : map f (filter (fun x => ↑f x ∈ t) s) = t
⊢ filter (fun x => ↑f x ∈ t) s ⊆ s ∧ card (filter (fun x => ↑f x ∈ t) s) = n
[PROOFSTEP]
rw [← card_map f, this, h.2]
[GOAL]
case mp
α : Type u_1
s✝ t✝ : Finset α
β : Type u_2
f : α ↪ β
n : ℕ
s : Finset α
t : Finset β
h : t ⊆ map f s ∧ card t = n
this : map f (filter (fun x => ↑f x ∈ t) s) = t
⊢ filter (fun x => ↑f x ∈ t) s ⊆ s ∧ n = n
[PROOFSTEP]
simp
[GOAL]
case mpr
α : Type u_1
s✝ t✝ : Finset α
β : Type u_2
f : α ↪ β
n : ℕ
s : Finset α
t : Finset β
⊢ (∃ a, (a ⊆ s ∧ card a = n) ∧ ↑(mapEmbedding f).toEmbedding a = t) → t ⊆ map f s ∧ card t = n
[PROOFSTEP]
rintro ⟨a, ⟨has, rfl⟩, rfl⟩
[GOAL]
case mpr.intro.intro.intro
α : Type u_1
s✝ t : Finset α
β : Type u_2
f : α ↪ β
s a : Finset α
has : a ⊆ s
⊢ ↑(mapEmbedding f).toEmbedding a ⊆ map f s ∧ card (↑(mapEmbedding f).toEmbedding a) = card a
[PROOFSTEP]
dsimp [RelEmbedding.coe_toEmbedding]
  --Porting note: Why is `rw` required here and not `simp`?
[GOAL]
case mpr.intro.intro.intro
α : Type u_1
s✝ t : Finset α
β : Type u_2
f : α ↪ β
s a : Finset α
has : a ⊆ s
⊢ ↑(mapEmbedding f) a ⊆ map f s ∧ card (↑(mapEmbedding f) a) = card a
[PROOFSTEP]
rw [mapEmbedding_apply]
[GOAL]
case mpr.intro.intro.intro
α : Type u_1
s✝ t : Finset α
β : Type u_2
f : α ↪ β
s a : Finset α
has : a ⊆ s
⊢ map f a ⊆ map f s ∧ card (map f a) = card a
[PROOFSTEP]
simp [has]
