-- Mathlib/Data/Finset/Powerset.lean
theorem powersetCard_succ_insert [DecidableEq α] {x : α} {s : Finset α} (h : x ∉ s) (n : ℕ) :
    powersetCard n.succ (insert x s) =
    powersetCard n.succ s ∪ (powersetCard n s).image (insert x)

Proof state:
case e_a.e_s.h
α : Type u_1
inst✝ : DecidableEq α
x : α
s : Finset α
h : x ∉ s
n : ℕ
t : Finset α
⊢ t ∈ filter (fun a => #(insert x a) = n.succ) s.powerset ↔ t ∈ filter (fun x => #x = n) s.powerset

Tactic:
simp only [mem_powerset, mem_filter, Function.comp_apply, and_congr_right_iff]

Result:
case e_a.e_s.h
α : Type u_1
inst✝ : DecidableEq α
x : α
s : Finset α
h : x ∉ s
n : ℕ
t : Finset α
⊢ t ⊆ s → (#(insert x t) = n.succ ↔ #t = n)

Proof state:
α : Type u_1
inst✝ : DecidableEq α
x : α
s : Finset α
h : x ∉ s
n : ℕ
⊢ powersetCard n.succ s ∪ filter (fun x => #x = n.succ) (image (insert x) s.powerset) =
    powersetCard n.succ s ∪ image (insert x) (powersetCard n s)

Tactic:
congr

Result:
case e_a
α : Type u_1
inst✝ : DecidableEq α
x : α
s : Finset α
h : x ∉ s
n : ℕ
⊢ filter (fun x => #x = n.succ) (image (insert x) s.powerset) = image (insert x) (powersetCard n s)

Proof state:
case e_a.e_s.h
α : Type u_1
inst✝ : DecidableEq α
x : α
s : Finset α
h : x ∉ s
n : ℕ
t : Finset α
ht : t ⊆ s
this : x ∉ t
⊢ #(insert x t) = n.succ ↔ #t = n

Tactic:
simp [card_insert_of_not_mem this, Nat.succ_inj']

Result:
no goals

Proof state:
case e_a
α : Type u_1
inst✝ : DecidableEq α
x : α
s : Finset α
h : x ∉ s
n : ℕ
⊢ filter (fun x => #x = n.succ) (image (insert x) s.powerset) = image (insert x) (powersetCard n s)

Tactic:
rw [powersetCard_eq_filter, filter_image]

Result:
case e_a
α : Type u_1
inst✝ : DecidableEq α
x : α
s : Finset α
h : x ∉ s
n : ℕ
⊢ image (insert x) (filter (fun a => #(insert x a) = n.succ) s.powerset) =
    image (insert x) (filter (fun x => #x = n) s.powerset)

Proof state:
case e_a
α : Type u_1
inst✝ : DecidableEq α
x : α
s : Finset α
h : x ∉ s
n : ℕ
⊢ image (insert x) (filter (fun a => #(insert x a) = n.succ) s.powerset) =
    image (insert x) (filter (fun x => #x = n) s.powerset)

Tactic:
congr 1

Result:
case e_a.e_s
α : Type u_1
inst✝ : DecidableEq α
x : α
s : Finset α
h : x ∉ s
n : ℕ
⊢ filter (fun a => #(insert x a) = n.succ) s.powerset = filter (fun x => #x = n) s.powerset

Proof state:
case e_a.e_s.h
α : Type u_1
inst✝ : DecidableEq α
x : α
s : Finset α
h : x ∉ s
n : ℕ
t : Finset α
⊢ t ⊆ s → (#(insert x t) = n.succ ↔ #t = n)

Tactic:
intro ht

Result:
case e_a.e_s.h
α : Type u_1
inst✝ : DecidableEq α
x : α
s : Finset α
h : x ∉ s
n : ℕ
t : Finset α
ht : t ⊆ s
⊢ #(insert x t) = n.succ ↔ #t = n

Proof state:
α : Type u_1
inst✝ : DecidableEq α
x : α
s : Finset α
h : x ∉ s
n : ℕ
⊢ powersetCard n.succ (insert x s) = powersetCard n.succ s ∪ image (insert x) (powersetCard n s)

Tactic:
rw [powersetCard_eq_filter, powerset_insert, filter_union, ← powersetCard_eq_filter]

Result:
α : Type u_1
inst✝ : DecidableEq α
x : α
s : Finset α
h : x ∉ s
n : ℕ
⊢ powersetCard n.succ s ∪ filter (fun x => #x = n.succ) (image (insert x) s.powerset) =
    powersetCard n.succ s ∪ image (insert x) (powersetCard n s)

Proof state:
case e_a.e_s
α : Type u_1
inst✝ : DecidableEq α
x : α
s : Finset α
h : x ∉ s
n : ℕ
⊢ filter (fun a => #(insert x a) = n.succ) s.powerset = filter (fun x => #x = n) s.powerset

Tactic:
ext t

Result:
case e_a.e_s.h
α : Type u_1
inst✝ : DecidableEq α
x : α
s : Finset α
h : x ∉ s
n : ℕ
t : Finset α
⊢ t ∈ filter (fun a => #(insert x a) = n.succ) s.powerset ↔ t ∈ filter (fun x => #x = n) s.powerset

Proof state:
case e_a.e_s.h
α : Type u_1
inst✝ : DecidableEq α
x : α
s : Finset α
h : x ∉ s
n : ℕ
t : Finset α
ht : t ⊆ s
⊢ #(insert x t) = n.succ ↔ #t = n

Tactic:
have : x ∉ t := fun H => h (ht H)

Result:
case e_a.e_s.h
α : Type u_1
inst✝ : DecidableEq α
x : α
s : Finset α
h : x ∉ s
n : ℕ
t : Finset α
ht : t ⊆ s
this : x ∉ t
⊢ #(insert x t) = n.succ ↔ #t = n