-- Mathlib/Combinatorics/SetFamily/Compression/Down.lean
theorem memberSubfamily_union_nonMemberSubfamily (a : α) (𝒜 : Finset (Finset α)) :
    𝒜.memberSubfamily a ∪ 𝒜.nonMemberSubfamily a = 𝒜.image fun s => s.erase a

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
𝒜 : Finset (Finset α)
s : Finset α
hs : s ∈ 𝒜
ha : a ∈ s
⊢ insert a (s.erase a) ∈ 𝒜

Tactic:
rwa [insert_erase ha]

Result:
no goals

Proof state:
case h.mpr.intro.intro
α : Type u_1
inst✝ : DecidableEq α
a : α
𝒜 : Finset (Finset α)
s : Finset α
hs : s ∈ 𝒜
⊢ insert a (s.erase a) ∈ 𝒜 ∧ a ∉ s.erase a ∨ s.erase a ∈ 𝒜 ∧ a ∉ s.erase a

Tactic:
by_cases ha : a ∈ s

Result:
case pos
α : Type u_1
inst✝ : DecidableEq α
a : α
𝒜 : Finset (Finset α)
s : Finset α
hs : s ∈ 𝒜
ha : a ∈ s
⊢ insert a (s.erase a) ∈ 𝒜 ∧ a ∉ s.erase a ∨ s.erase a ∈ 𝒜 ∧ a ∉ s.erase a

case neg
α : Type u_1
inst✝ : DecidableEq α
a : α
𝒜 : Finset (Finset α)
s : Finset α
hs : s ∈ 𝒜
ha : a ∉ s
⊢ insert a (s.erase a) ∈ 𝒜 ∧ a ∉ s.erase a ∨ s.erase a ∈ 𝒜 ∧ a ∉ s.erase a

Proof state:
case h.mp.inl
α : Type u_1
inst✝ : DecidableEq α
a : α
𝒜 : Finset (Finset α)
s : Finset α
h : insert a s ∈ 𝒜 ∧ a ∉ s
⊢ ∃ a_1 ∈ 𝒜, a_1.erase a = s

Tactic:
exact ⟨_, h.1, erase_insert h.2⟩

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
𝒜 : Finset (Finset α)
s : Finset α
hs : s ∈ 𝒜
ha : a ∉ s
⊢ s.erase a ∈ 𝒜

Tactic:
rwa [erase_eq_of_not_mem ha]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
𝒜 : Finset (Finset α)
⊢ memberSubfamily a 𝒜 ∪ nonMemberSubfamily a 𝒜 = image (fun s => s.erase a) 𝒜

Tactic:
ext s

Result:
case h
α : Type u_1
inst✝ : DecidableEq α
a : α
𝒜 : Finset (Finset α)
s : Finset α
⊢ s ∈ memberSubfamily a 𝒜 ∪ nonMemberSubfamily a 𝒜 ↔ s ∈ image (fun s => s.erase a) 𝒜

Proof state:
case h.mp.inr
α : Type u_1
inst✝ : DecidableEq α
a : α
𝒜 : Finset (Finset α)
s : Finset α
h : s ∈ 𝒜 ∧ a ∉ s
⊢ ∃ a_1 ∈ 𝒜, a_1.erase a = s

Tactic:
exact ⟨_, h.1, erase_eq_of_not_mem h.2⟩

Result:
no goals

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

Tactic:
rintro ⟨s, hs, rfl⟩

Result:
case h.mpr.intro.intro
α : Type u_1
inst✝ : DecidableEq α
a : α
𝒜 : Finset (Finset α)
s : Finset α
hs : s ∈ 𝒜
⊢ insert a (s.erase a) ∈ 𝒜 ∧ a ∉ s.erase a ∨ s.erase a ∈ 𝒜 ∧ a ∉ s.erase a

Proof state:
case h
α : Type u_1
inst✝ : DecidableEq α
a : α
𝒜 : Finset (Finset α)
s : Finset α
⊢ s ∈ memberSubfamily a 𝒜 ∪ nonMemberSubfamily a 𝒜 ↔ s ∈ image (fun s => s.erase a) 𝒜

Tactic:
simp only [mem_union, mem_memberSubfamily, mem_nonMemberSubfamily, mem_image, exists_prop]

Result:
case h
α : Type u_1
inst✝ : DecidableEq α
a : α
𝒜 : Finset (Finset α)
s : Finset α
⊢ insert a s ∈ 𝒜 ∧ a ∉ s ∨ s ∈ 𝒜 ∧ a ∉ s ↔ ∃ a_1 ∈ 𝒜, a_1.erase a = s

Proof state:
case neg
α : Type u_1
inst✝ : DecidableEq α
a : α
𝒜 : Finset (Finset α)
s : Finset α
hs : s ∈ 𝒜
ha : a ∉ s
⊢ insert a (s.erase a) ∈ 𝒜 ∧ a ∉ s.erase a ∨ s.erase a ∈ 𝒜 ∧ a ∉ s.erase a

Tactic:
exact Or.inr ⟨by rwa [erase_eq_of_not_mem ha], not_mem_erase _ _⟩

Result:
no goals

Proof state:
case h.mp
α : Type u_1
inst✝ : DecidableEq α
a : α
𝒜 : Finset (Finset α)
s : Finset α
⊢ insert a s ∈ 𝒜 ∧ a ∉ s ∨ s ∈ 𝒜 ∧ a ∉ s → ∃ a_2 ∈ 𝒜, a_2.erase a = s

Tactic:
rintro (h | h)

Result:
case h.mp.inl
α : Type u_1
inst✝ : DecidableEq α
a : α
𝒜 : Finset (Finset α)
s : Finset α
h : insert a s ∈ 𝒜 ∧ a ∉ s
⊢ ∃ a_1 ∈ 𝒜, a_1.erase a = s

case h.mp.inr
α : Type u_1
inst✝ : DecidableEq α
a : α
𝒜 : Finset (Finset α)
s : Finset α
h : s ∈ 𝒜 ∧ a ∉ s
⊢ ∃ a_1 ∈ 𝒜, a_1.erase a = s

Proof state:
case h
α : Type u_1
inst✝ : DecidableEq α
a : α
𝒜 : Finset (Finset α)
s : Finset α
⊢ insert a s ∈ 𝒜 ∧ a ∉ s ∨ s ∈ 𝒜 ∧ a ∉ s ↔ ∃ a_1 ∈ 𝒜, a_1.erase a = s

Tactic:
constructor

Result:
case h.mp
α : Type u_1
inst✝ : DecidableEq α
a : α
𝒜 : Finset (Finset α)
s : Finset α
⊢ insert a s ∈ 𝒜 ∧ a ∉ s ∨ s ∈ 𝒜 ∧ a ∉ s → ∃ a_2 ∈ 𝒜, a_2.erase a = s

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

Proof state:
case pos
α : Type u_1
inst✝ : DecidableEq α
a : α
𝒜 : Finset (Finset α)
s : Finset α
hs : s ∈ 𝒜
ha : a ∈ s
⊢ insert a (s.erase a) ∈ 𝒜 ∧ a ∉ s.erase a ∨ s.erase a ∈ 𝒜 ∧ a ∉ s.erase a

Tactic:
exact Or.inl ⟨by rwa [insert_erase ha], not_mem_erase _ _⟩

Result:
no goals