-- Mathlib/Data/Finset/Powerset.lean
theorem powerset_insert [DecidableEq α] (s : Finset α) (a : α) :
    powerset (insert a s) = s.powerset ∪ s.powerset.image (insert a)

Proof state:
case pos.mpr.inl
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a : α
t : Finset α
h : a ∈ t
H : t ⊆ s
⊢ t.erase a ⊆ s

Tactic:
exact Subset.trans (erase_subset a t) H

Result:
no goals

Proof state:
case pos.mp
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a : α
t : Finset α
h : a ∈ t
⊢ t.erase a ⊆ s → t ⊆ s ∨ ∃ a_2 ⊆ s, insert a a_2 = t

Tactic:
exact fun H => Or.inr ⟨_, H, insert_erase h⟩

Result:
no goals

Proof state:
case pos.mpr
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a : α
t : Finset α
h : a ∈ t
⊢ (t ⊆ s ∨ ∃ a_1 ⊆ s, insert a a_1 = t) → t.erase a ⊆ s

Tactic:
intro H

Result:
case pos.mpr
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a : α
t : Finset α
h : a ∈ t
H : t ⊆ s ∨ ∃ a_1 ⊆ s, insert a a_1 = t
⊢ t.erase a ⊆ s

Proof state:
case h
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a : α
t : Finset α
⊢ t.erase a ⊆ s ↔ t ⊆ s ∨ ∃ a_1 ⊆ s, insert a a_1 = t

Tactic:
by_cases h : a ∈ t

Result:
case pos
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a : α
t : Finset α
h : a ∈ t
⊢ t.erase a ⊆ s ↔ t ⊆ s ∨ ∃ a_1 ⊆ s, insert a a_1 = t

case neg
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a : α
t : Finset α
h : a ∉ t
⊢ t.erase a ⊆ s ↔ t ⊆ s ∨ ∃ a_1 ⊆ s, insert a a_1 = t

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a : α
t : Finset α
h : a ∉ t
⊢ ¬∃ u ⊆ s, insert a u = t

Tactic:
simp [Ne.symm (ne_insert_of_not_mem _ _ h)]

Result:
no goals

Proof state:
case pos
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a : α
t : Finset α
h : a ∈ t
⊢ t.erase a ⊆ s ↔ t ⊆ s ∨ ∃ a_1 ⊆ s, insert a a_1 = t

Tactic:
constructor

Result:
case pos.mp
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a : α
t : Finset α
h : a ∈ t
⊢ t.erase a ⊆ s → t ⊆ s ∨ ∃ a_2 ⊆ s, insert a a_2 = t

case pos.mpr
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a : α
t : Finset α
h : a ∈ t
⊢ (t ⊆ s ∨ ∃ a_1 ⊆ s, insert a a_1 = t) → t.erase a ⊆ s

Proof state:
case pos.mpr
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a : α
t : Finset α
h : a ∈ t
H : t ⊆ s ∨ ∃ a_1 ⊆ s, insert a a_1 = t
⊢ t.erase a ⊆ s

Tactic:
rcases H with H | H

Result:
case pos.mpr.inl
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a : α
t : Finset α
h : a ∈ t
H : t ⊆ s
⊢ t.erase a ⊆ s

case pos.mpr.inr
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a : α
t : Finset α
h : a ∈ t
H : ∃ a_1 ⊆ s, insert a a_1 = t
⊢ t.erase a ⊆ s

Proof state:
case pos.mpr.inr.intro
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a : α
t : Finset α
h : a ∈ t
u : Finset α
hu : u ⊆ s ∧ insert a u = t
⊢ t.erase a ⊆ s

Tactic:
rw [← hu.2]

Result:
case pos.mpr.inr.intro
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a : α
t : Finset α
h : a ∈ t
u : Finset α
hu : u ⊆ s ∧ insert a u = t
⊢ (insert a u).erase a ⊆ s

Proof state:
case neg
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a : α
t : Finset α
h : a ∉ t
this : ¬∃ u ⊆ s, insert a u = t
⊢ t.erase a ⊆ s ↔ t ⊆ s ∨ ∃ a_1 ⊆ s, insert a a_1 = t

Tactic:
simp [Finset.erase_eq_of_not_mem h, this]

Result:
no goals

Proof state:
case pos.mpr.inr
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a : α
t : Finset α
h : a ∈ t
H : ∃ a_1 ⊆ s, insert a a_1 = t
⊢ t.erase a ⊆ s

Tactic:
rcases H with ⟨u, hu⟩

Result:
case pos.mpr.inr.intro
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a : α
t : Finset α
h : a ∈ t
u : Finset α
hu : u ⊆ s ∧ insert a u = t
⊢ t.erase a ⊆ s

Proof state:
case h
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a : α
t : Finset α
⊢ t ∈ (insert a s).powerset ↔ t ∈ s.powerset ∪ image (insert a) s.powerset

Tactic:
simp only [exists_prop, mem_powerset, mem_image, mem_union, subset_insert_iff]

Result:
case h
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a : α
t : Finset α
⊢ t.erase a ⊆ s ↔ t ⊆ s ∨ ∃ a_1 ⊆ s, insert a a_1 = t

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a : α
⊢ (insert a s).powerset = s.powerset ∪ image (insert a) s.powerset

Tactic:
ext t

Result:
case h
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a : α
t : Finset α
⊢ t ∈ (insert a s).powerset ↔ t ∈ s.powerset ∪ image (insert a) s.powerset

Proof state:
case pos.mpr.inr.intro
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a : α
t : Finset α
h : a ∈ t
u : Finset α
hu : u ⊆ s ∧ insert a u = t
⊢ (insert a u).erase a ⊆ s

Tactic:
exact Subset.trans (erase_insert_subset a u) hu.1

Result:
no goals

Proof state:
case neg
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a : α
t : Finset α
h : a ∉ t
⊢ t.erase a ⊆ s ↔ t ⊆ s ∨ ∃ a_1 ⊆ s, insert a a_1 = t

Tactic:
have : ¬∃ u : Finset α, u ⊆ s ∧ insert a u = t := by simp [Ne.symm (ne_insert_of_not_mem _ _ h)]

Result:
case neg
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a : α
t : Finset α
h : a ∉ t
this : ¬∃ u ⊆ s, insert a u = t
⊢ t.erase a ⊆ s ↔ t ⊆ s ∨ ∃ a_1 ⊆ s, insert a a_1 = t