α : 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)
α : 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)
rw [powersetLen_eq_filter, powerset_insert, filter_union, ← powersetLen_eq_filter]
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)
α : 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)
congr
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))
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)
rw [powersetLen_eq_filter, image_filter]
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)
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))
congr 1
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)
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)
ext t
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)
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)
simp only [mem_powerset, mem_filter, Function.comp_apply, and_congr_right_iff]
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
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)
intro ht
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
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
have : x ∉ t := fun H => h (ht H)
no goals
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
simp [card_insert_of_not_mem this, Nat.succ_inj']