case empty
α : Type u_1
s✝ t : Finset α
n✝ : ℕ
s : Finset α
h✝ : n✝ ≤ card s
n : ℕ
h : n ≤ card ∅
⊢ Finset.Nonempty (powersetLen n ∅)

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))
α : Type u_1
s✝ t : Finset α
n : ℕ
s : Finset α
h : n ≤ card s
⊢ Finset.Nonempty (powersetLen n s)
induction' s using Finset.induction_on with x s hx IH generalizing n
case empty
α : Type u_1
s✝ t : Finset α
n✝ : ℕ
s : Finset α
h✝ : n✝ ≤ card s
n : ℕ
h : n = 0
⊢ Finset.Nonempty (powersetLen n ∅)
case empty
α : Type u_1
s✝ t : Finset α
n✝ : ℕ
s : Finset α
h✝ : n✝ ≤ card s
n : ℕ
h : n ≤ card ∅
⊢ Finset.Nonempty (powersetLen n ∅)
rw [card_empty, le_zero_iff] at h
case empty
α : Type u_1
s✝ t : Finset α
n✝ : ℕ
s : Finset α
h✝ : n✝ ≤ card s
n : ℕ
h : n = 0
⊢ Finset.Nonempty {∅}
case empty
α : Type u_1
s✝ t : Finset α
n✝ : ℕ
s : Finset α
h✝ : n✝ ≤ card s
n : ℕ
h : n = 0
⊢ Finset.Nonempty (powersetLen n ∅)
rw [h, powersetLen_zero]
no goals
case empty
α : Type u_1
s✝ t : Finset α
n✝ : ℕ
s : Finset α
h✝ : n✝ ≤ card s
n : ℕ
h : n = 0
⊢ Finset.Nonempty {∅}
exact Finset.singleton_nonempty _
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))

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))
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))
cases n
no goals
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))
simp
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))
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))
rw [card_insert_of_not_mem hx, Nat.succ_le_succ_iff] at h
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))
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))
rw [powersetLen_succ_insert hx]
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)
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))
refine' Nonempty.mono _ ((IH h).image (insert x))
no goals
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)
exact subset_union_right _ _