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)
α : Type u_1
s✝ t : Finset α
inst✝ : DecidableEq α
s : Finset α
a : α
⊢ powerset (insert a s) = powerset s ∪ image (insert a) (powerset s)
ext t
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
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)
simp only [exists_prop, mem_powerset, mem_image, mem_union, subset_insert_iff]
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

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
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
by_cases h : a ∈ t
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

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
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
constructor
no goals
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
exact fun H => Or.inr ⟨_, H, insert_erase h⟩
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
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
intro H
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

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
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
cases' H with H H
no goals
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
exact Subset.trans (erase_subset a t) H
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
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
rcases H with ⟨u, hu⟩
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
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
rw [← hu.2]
no goals
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
exact Subset.trans (erase_insert_subset a u) hu.1
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
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
have : ¬∃ u : Finset α, u ⊆ s ∧ insert a u = t := by simp [Ne.symm (ne_insert_of_not_mem _ _ h)]
no goals
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
simp [Finset.erase_eq_of_not_mem h, this]
no goals
α : Type u_1
s✝ t✝ : Finset α
inst✝ : DecidableEq α
s : Finset α
a : α
t : Finset α
h : ¬a ∈ t
⊢ ¬∃ u, u ⊆ s ∧ insert a u = t
simp [Ne.symm (ne_insert_of_not_mem _ _ h)]