[GOAL]
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s t : Finset α
a : α
k r : ℕ
⊢ s ∈ ∂ 𝒜 ↔ ∃ t, t ∈ 𝒜 ∧ ∃ a, a ∈ t ∧ erase t a = s
[PROOFSTEP]
simp only [shadow, mem_sup, mem_image]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s t : Finset α
a : α
k r : ℕ
⊢ s ∈ ∂ 𝒜 ↔ ∃ a x, insert a s ∈ 𝒜
[PROOFSTEP]
refine' mem_shadow_iff.trans ⟨_, _⟩
[GOAL]
case refine'_1
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s t : Finset α
a : α
k r : ℕ
⊢ (∃ t, t ∈ 𝒜 ∧ ∃ a, a ∈ t ∧ erase t a = s) → ∃ a x, insert a s ∈ 𝒜
[PROOFSTEP]
rintro ⟨s, hs, a, ha, rfl⟩
[GOAL]
case refine'_1.intro.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
t : Finset α
a✝ : α
k r : ℕ
s : Finset α
hs : s ∈ 𝒜
a : α
ha : a ∈ s
⊢ ∃ a_1 x, insert a_1 (erase s a) ∈ 𝒜
[PROOFSTEP]
refine' ⟨a, not_mem_erase a s, _⟩
[GOAL]
case refine'_1.intro.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
t : Finset α
a✝ : α
k r : ℕ
s : Finset α
hs : s ∈ 𝒜
a : α
ha : a ∈ s
⊢ insert a (erase s a) ∈ 𝒜
[PROOFSTEP]
rwa [insert_erase ha]
[GOAL]
case refine'_2
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s t : Finset α
a : α
k r : ℕ
⊢ (∃ a x, insert a s ∈ 𝒜) → ∃ t, t ∈ 𝒜 ∧ ∃ a, a ∈ t ∧ erase t a = s
[PROOFSTEP]
rintro ⟨a, ha, hs⟩
[GOAL]
case refine'_2.intro.intro
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s t : Finset α
a✝ : α
k r : ℕ
a : α
ha : ¬a ∈ s
hs : insert a s ∈ 𝒜
⊢ ∃ t, t ∈ 𝒜 ∧ ∃ a, a ∈ t ∧ erase t a = s
[PROOFSTEP]
exact ⟨insert a s, hs, a, mem_insert_self _ _, erase_insert ha⟩
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s t : Finset α
a : α
k r : ℕ
h𝒜 : Set.Sized r ↑𝒜
⊢ Set.Sized (r - 1) ↑(∂ 𝒜)
[PROOFSTEP]
intro A h
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s t : Finset α
a : α
k r : ℕ
h𝒜 : Set.Sized r ↑𝒜
A : Finset α
h : A ∈ ↑(∂ 𝒜)
⊢ card A = r - 1
[PROOFSTEP]
obtain ⟨A, hA, i, hi, rfl⟩ := mem_shadow_iff.1 h
[GOAL]
case intro.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s t : Finset α
a : α
k r : ℕ
h𝒜 : Set.Sized r ↑𝒜
A : Finset α
hA : A ∈ 𝒜
i : α
hi : i ∈ A
h : erase A i ∈ ↑(∂ 𝒜)
⊢ card (erase A i) = r - 1
[PROOFSTEP]
rw [card_erase_of_mem hi, h𝒜 hA]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s t : Finset α
a : α
k r : ℕ
h : ¬∅ ∈ 𝒜
⊢ Set.Sized r ↑(∂ 𝒜) ↔ Set.Sized (r + 1) ↑𝒜
[PROOFSTEP]
refine' ⟨fun h𝒜 s hs => _, Set.Sized.shadow⟩
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s✝ t : Finset α
a : α
k r : ℕ
h : ¬∅ ∈ 𝒜
h𝒜 : Set.Sized r ↑(∂ 𝒜)
s : Finset α
hs : s ∈ ↑𝒜
⊢ card s = r + 1
[PROOFSTEP]
obtain ⟨a, ha⟩ := nonempty_iff_ne_empty.2 (ne_of_mem_of_not_mem hs h)
[GOAL]
case intro
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s✝ t : Finset α
a✝ : α
k r : ℕ
h : ¬∅ ∈ 𝒜
h𝒜 : Set.Sized r ↑(∂ 𝒜)
s : Finset α
hs : s ∈ ↑𝒜
a : α
ha : a ∈ s
⊢ card s = r + 1
[PROOFSTEP]
rw [← h𝒜 (erase_mem_shadow hs ha), card_erase_add_one ha]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s t : Finset α
a : α
k r : ℕ
⊢ s ∈ ∂ 𝒜 ↔ ∃ t, t ∈ 𝒜 ∧ s ⊆ t ∧ card t = card s + 1
[PROOFSTEP]
refine' mem_shadow_iff_insert_mem.trans ⟨_, _⟩
[GOAL]
case refine'_1
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s t : Finset α
a : α
k r : ℕ
⊢ (∃ a x, insert a s ∈ 𝒜) → ∃ t, t ∈ 𝒜 ∧ s ⊆ t ∧ card t = card s + 1
[PROOFSTEP]
rintro ⟨a, ha, hs⟩
[GOAL]
case refine'_1.intro.intro
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s t : Finset α
a✝ : α
k r : ℕ
a : α
ha : ¬a ∈ s
hs : insert a s ∈ 𝒜
⊢ ∃ t, t ∈ 𝒜 ∧ s ⊆ t ∧ card t = card s + 1
[PROOFSTEP]
exact ⟨insert a s, hs, subset_insert _ _, card_insert_of_not_mem ha⟩
[GOAL]
case refine'_2
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s t : Finset α
a : α
k r : ℕ
⊢ (∃ t, t ∈ 𝒜 ∧ s ⊆ t ∧ card t = card s + 1) → ∃ a x, insert a s ∈ 𝒜
[PROOFSTEP]
rintro ⟨t, ht, hst, h⟩
[GOAL]
case refine'_2.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s t✝ : Finset α
a : α
k r : ℕ
t : Finset α
ht : t ∈ 𝒜
hst : s ⊆ t
h : card t = card s + 1
⊢ ∃ a x, insert a s ∈ 𝒜
[PROOFSTEP]
obtain ⟨a, ha⟩ : ∃ a, t \ s = { a } := card_eq_one.1 (by rw [card_sdiff hst, h, add_tsub_cancel_left])
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s t✝ : Finset α
a : α
k r : ℕ
t : Finset α
ht : t ∈ 𝒜
hst : s ⊆ t
h : card t = card s + 1
⊢ card (t \ s) = 1
[PROOFSTEP]
rw [card_sdiff hst, h, add_tsub_cancel_left]
[GOAL]
case refine'_2.intro.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s t✝ : Finset α
a✝ : α
k r : ℕ
t : Finset α
ht : t ∈ 𝒜
hst : s ⊆ t
h : card t = card s + 1
a : α
ha : t \ s = {a}
⊢ ∃ a x, insert a s ∈ 𝒜
[PROOFSTEP]
exact
  ⟨a, fun hat => not_mem_sdiff_of_mem_right hat (ha.superset <| mem_singleton_self a), by
    rwa [insert_eq a s, ← ha, sdiff_union_of_subset hst]⟩
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s t✝ : Finset α
a✝ : α
k r : ℕ
t : Finset α
ht : t ∈ 𝒜
hst : s ⊆ t
h : card t = card s + 1
a : α
ha : t \ s = {a}
⊢ insert a s ∈ 𝒜
[PROOFSTEP]
rwa [insert_eq a s, ← ha, sdiff_union_of_subset hst]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s t : Finset α
a : α
k r : ℕ
⊢ s ∈ ∂ ^[k] 𝒜 ↔ ∃ t, t ∈ 𝒜 ∧ s ⊆ t ∧ card t = card s + k
[PROOFSTEP]
induction' k with k ih generalizing 𝒜 s
[GOAL]
case zero
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ : Finset (Finset α)
s✝ t : Finset α
a : α
k r : ℕ
𝒜 : Finset (Finset α)
s : Finset α
⊢ s ∈ ∂ ^[zero] 𝒜 ↔ ∃ t, t ∈ 𝒜 ∧ s ⊆ t ∧ card t = card s + zero
[PROOFSTEP]
refine' ⟨fun hs => ⟨s, hs, Subset.refl _, rfl⟩, _⟩
[GOAL]
case zero
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ : Finset (Finset α)
s✝ t : Finset α
a : α
k r : ℕ
𝒜 : Finset (Finset α)
s : Finset α
⊢ (∃ t, t ∈ 𝒜 ∧ s ⊆ t ∧ card t = card s + zero) → s ∈ ∂ ^[zero] 𝒜
[PROOFSTEP]
rintro ⟨t, ht, hst, hcard⟩
[GOAL]
case zero.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ : Finset (Finset α)
s✝ t✝ : Finset α
a : α
k r : ℕ
𝒜 : Finset (Finset α)
s t : Finset α
ht : t ∈ 𝒜
hst : s ⊆ t
hcard : card t = card s + zero
⊢ s ∈ ∂ ^[zero] 𝒜
[PROOFSTEP]
rwa [eq_of_subset_of_card_le hst hcard.le]
[GOAL]
case succ
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ : Finset (Finset α)
s✝ t : Finset α
a : α
k✝ r k : ℕ
ih : ∀ {𝒜 : Finset (Finset α)} {s : Finset α}, s ∈ ∂ ^[k] 𝒜 ↔ ∃ t, t ∈ 𝒜 ∧ s ⊆ t ∧ card t = card s + k
𝒜 : Finset (Finset α)
s : Finset α
⊢ s ∈ ∂ ^[succ k] 𝒜 ↔ ∃ t, t ∈ 𝒜 ∧ s ⊆ t ∧ card t = card s + succ k
[PROOFSTEP]
simp only [exists_prop, Function.comp_apply, Function.iterate_succ]
[GOAL]
case succ
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ : Finset (Finset α)
s✝ t : Finset α
a : α
k✝ r k : ℕ
ih : ∀ {𝒜 : Finset (Finset α)} {s : Finset α}, s ∈ ∂ ^[k] 𝒜 ↔ ∃ t, t ∈ 𝒜 ∧ s ⊆ t ∧ card t = card s + k
𝒜 : Finset (Finset α)
s : Finset α
⊢ s ∈ ∂ ^[k] (∂ 𝒜) ↔ ∃ t, t ∈ 𝒜 ∧ s ⊆ t ∧ card t = card s + succ k
[PROOFSTEP]
refine' ih.trans _
[GOAL]
case succ
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ : Finset (Finset α)
s✝ t : Finset α
a : α
k✝ r k : ℕ
ih : ∀ {𝒜 : Finset (Finset α)} {s : Finset α}, s ∈ ∂ ^[k] 𝒜 ↔ ∃ t, t ∈ 𝒜 ∧ s ⊆ t ∧ card t = card s + k
𝒜 : Finset (Finset α)
s : Finset α
⊢ (∃ t, t ∈ ∂ 𝒜 ∧ s ⊆ t ∧ card t = card s + k) ↔ ∃ t, t ∈ 𝒜 ∧ s ⊆ t ∧ card t = card s + succ k
[PROOFSTEP]
clear ih
[GOAL]
case succ
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ : Finset (Finset α)
s✝ t : Finset α
a : α
k✝ r k : ℕ
𝒜 : Finset (Finset α)
s : Finset α
⊢ (∃ t, t ∈ ∂ 𝒜 ∧ s ⊆ t ∧ card t = card s + k) ↔ ∃ t, t ∈ 𝒜 ∧ s ⊆ t ∧ card t = card s + succ k
[PROOFSTEP]
constructor
[GOAL]
case succ.mp
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ : Finset (Finset α)
s✝ t : Finset α
a : α
k✝ r k : ℕ
𝒜 : Finset (Finset α)
s : Finset α
⊢ (∃ t, t ∈ ∂ 𝒜 ∧ s ⊆ t ∧ card t = card s + k) → ∃ t, t ∈ 𝒜 ∧ s ⊆ t ∧ card t = card s + succ k
[PROOFSTEP]
rintro ⟨t, ht, hst, hcardst⟩
[GOAL]
case succ.mp.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ : Finset (Finset α)
s✝ t✝ : Finset α
a : α
k✝ r k : ℕ
𝒜 : Finset (Finset α)
s t : Finset α
ht : t ∈ ∂ 𝒜
hst : s ⊆ t
hcardst : card t = card s + k
⊢ ∃ t, t ∈ 𝒜 ∧ s ⊆ t ∧ card t = card s + succ k
[PROOFSTEP]
obtain ⟨u, hu, htu, hcardtu⟩ := mem_shadow_iff_exists_mem_card_add_one.1 ht
[GOAL]
case succ.mp.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ : Finset (Finset α)
s✝ t✝ : Finset α
a : α
k✝ r k : ℕ
𝒜 : Finset (Finset α)
s t : Finset α
ht : t ∈ ∂ 𝒜
hst : s ⊆ t
hcardst : card t = card s + k
u : Finset α
hu : u ∈ 𝒜
htu : t ⊆ u
hcardtu : card u = card t + 1
⊢ ∃ t, t ∈ 𝒜 ∧ s ⊆ t ∧ card t = card s + succ k
[PROOFSTEP]
refine' ⟨u, hu, hst.trans htu, _⟩
[GOAL]
case succ.mp.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ : Finset (Finset α)
s✝ t✝ : Finset α
a : α
k✝ r k : ℕ
𝒜 : Finset (Finset α)
s t : Finset α
ht : t ∈ ∂ 𝒜
hst : s ⊆ t
hcardst : card t = card s + k
u : Finset α
hu : u ∈ 𝒜
htu : t ⊆ u
hcardtu : card u = card t + 1
⊢ card u = card s + succ k
[PROOFSTEP]
rw [hcardtu, hcardst]
[GOAL]
case succ.mp.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ : Finset (Finset α)
s✝ t✝ : Finset α
a : α
k✝ r k : ℕ
𝒜 : Finset (Finset α)
s t : Finset α
ht : t ∈ ∂ 𝒜
hst : s ⊆ t
hcardst : card t = card s + k
u : Finset α
hu : u ∈ 𝒜
htu : t ⊆ u
hcardtu : card u = card t + 1
⊢ card s + k + 1 = card s + succ k
[PROOFSTEP]
rfl
[GOAL]
case succ.mpr
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ : Finset (Finset α)
s✝ t : Finset α
a : α
k✝ r k : ℕ
𝒜 : Finset (Finset α)
s : Finset α
⊢ (∃ t, t ∈ 𝒜 ∧ s ⊆ t ∧ card t = card s + succ k) → ∃ t, t ∈ ∂ 𝒜 ∧ s ⊆ t ∧ card t = card s + k
[PROOFSTEP]
rintro ⟨t, ht, hst, hcard⟩
[GOAL]
case succ.mpr.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ : Finset (Finset α)
s✝ t✝ : Finset α
a : α
k✝ r k : ℕ
𝒜 : Finset (Finset α)
s t : Finset α
ht : t ∈ 𝒜
hst : s ⊆ t
hcard : card t = card s + succ k
⊢ ∃ t, t ∈ ∂ 𝒜 ∧ s ⊆ t ∧ card t = card s + k
[PROOFSTEP]
obtain ⟨u, hsu, hut, hu⟩ :=
  Finset.exists_intermediate_set k
    (by
      rw [add_comm, hcard]
      exact le_succ _)
    hst
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ : Finset (Finset α)
s✝ t✝ : Finset α
a : α
k✝ r k : ℕ
𝒜 : Finset (Finset α)
s t : Finset α
ht : t ∈ 𝒜
hst : s ⊆ t
hcard : card t = card s + succ k
⊢ k + card s ≤ card t
[PROOFSTEP]
rw [add_comm, hcard]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ : Finset (Finset α)
s✝ t✝ : Finset α
a : α
k✝ r k : ℕ
𝒜 : Finset (Finset α)
s t : Finset α
ht : t ∈ 𝒜
hst : s ⊆ t
hcard : card t = card s + succ k
⊢ card s + k ≤ card s + succ k
[PROOFSTEP]
exact le_succ _
[GOAL]
case succ.mpr.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ : Finset (Finset α)
s✝ t✝ : Finset α
a : α
k✝ r k : ℕ
𝒜 : Finset (Finset α)
s t : Finset α
ht : t ∈ 𝒜
hst : s ⊆ t
hcard : card t = card s + succ k
u : Finset α
hsu : s ⊆ u
hut : u ⊆ t
hu : card u = k + card s
⊢ ∃ t, t ∈ ∂ 𝒜 ∧ s ⊆ t ∧ card t = card s + k
[PROOFSTEP]
rw [add_comm] at hu 
[GOAL]
case succ.mpr.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ : Finset (Finset α)
s✝ t✝ : Finset α
a : α
k✝ r k : ℕ
𝒜 : Finset (Finset α)
s t : Finset α
ht : t ∈ 𝒜
hst : s ⊆ t
hcard : card t = card s + succ k
u : Finset α
hsu : s ⊆ u
hut : u ⊆ t
hu : card u = card s + k
⊢ ∃ t, t ∈ ∂ 𝒜 ∧ s ⊆ t ∧ card t = card s + k
[PROOFSTEP]
refine' ⟨u, mem_shadow_iff_exists_mem_card_add_one.2 ⟨t, ht, hut, _⟩, hsu, hu⟩
[GOAL]
case succ.mpr.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ : Finset (Finset α)
s✝ t✝ : Finset α
a : α
k✝ r k : ℕ
𝒜 : Finset (Finset α)
s t : Finset α
ht : t ∈ 𝒜
hst : s ⊆ t
hcard : card t = card s + succ k
u : Finset α
hsu : s ⊆ u
hut : u ⊆ t
hu : card u = card s + k
⊢ card t = card u + 1
[PROOFSTEP]
rw [hcard, hu]
[GOAL]
case succ.mpr.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ : Finset (Finset α)
s✝ t✝ : Finset α
a : α
k✝ r k : ℕ
𝒜 : Finset (Finset α)
s t : Finset α
ht : t ∈ 𝒜
hst : s ⊆ t
hcard : card t = card s + succ k
u : Finset α
hsu : s ⊆ u
hut : u ⊆ t
hu : card u = card s + k
⊢ card s + succ k = card s + k + 1
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
s t : Finset α
a : α
k r : ℕ
⊢ s ∈ ∂⁺ 𝒜 ↔ ∃ t, t ∈ 𝒜 ∧ ∃ a x, insert a t = s
[PROOFSTEP]
simp_rw [upShadow, mem_sup, mem_image, exists_prop, mem_compl]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
s t : Finset α
a : α
k r : ℕ
h𝒜 : Set.Sized r ↑𝒜
⊢ Set.Sized (r + 1) ↑(∂⁺ 𝒜)
[PROOFSTEP]
intro A h
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
s t : Finset α
a : α
k r : ℕ
h𝒜 : Set.Sized r ↑𝒜
A : Finset α
h : A ∈ ↑(∂⁺ 𝒜)
⊢ card A = r + 1
[PROOFSTEP]
obtain ⟨A, hA, i, hi, rfl⟩ := mem_upShadow_iff.1 h
[GOAL]
case intro.intro.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
s t : Finset α
a : α
k r : ℕ
h𝒜 : Set.Sized r ↑𝒜
A : Finset α
hA : A ∈ 𝒜
i : α
hi : ¬i ∈ A
h : insert i A ∈ ↑(∂⁺ 𝒜)
⊢ card (insert i A) = r + 1
[PROOFSTEP]
rw [card_insert_of_not_mem hi, h𝒜 hA]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
s t : Finset α
a : α
k r : ℕ
⊢ s ∈ ∂⁺ 𝒜 ↔ ∃ a, a ∈ s ∧ erase s a ∈ 𝒜
[PROOFSTEP]
refine' mem_upShadow_iff.trans ⟨_, _⟩
[GOAL]
case refine'_1
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
s t : Finset α
a : α
k r : ℕ
⊢ (∃ t, t ∈ 𝒜 ∧ ∃ a x, insert a t = s) → ∃ a, a ∈ s ∧ erase s a ∈ 𝒜
[PROOFSTEP]
rintro ⟨s, hs, a, ha, rfl⟩
[GOAL]
case refine'_1.intro.intro.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
t : Finset α
a✝ : α
k r : ℕ
s : Finset α
hs : s ∈ 𝒜
a : α
ha : ¬a ∈ s
⊢ ∃ a_1, a_1 ∈ insert a s ∧ erase (insert a s) a_1 ∈ 𝒜
[PROOFSTEP]
refine' ⟨a, mem_insert_self a s, _⟩
[GOAL]
case refine'_1.intro.intro.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
t : Finset α
a✝ : α
k r : ℕ
s : Finset α
hs : s ∈ 𝒜
a : α
ha : ¬a ∈ s
⊢ erase (insert a s) a ∈ 𝒜
[PROOFSTEP]
rwa [erase_insert ha]
[GOAL]
case refine'_2
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
s t : Finset α
a : α
k r : ℕ
⊢ (∃ a, a ∈ s ∧ erase s a ∈ 𝒜) → ∃ t, t ∈ 𝒜 ∧ ∃ a x, insert a t = s
[PROOFSTEP]
rintro ⟨a, ha, hs⟩
[GOAL]
case refine'_2.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
s t : Finset α
a✝ : α
k r : ℕ
a : α
ha : a ∈ s
hs : erase s a ∈ 𝒜
⊢ ∃ t, t ∈ 𝒜 ∧ ∃ a x, insert a t = s
[PROOFSTEP]
exact ⟨s.erase a, hs, a, not_mem_erase _ _, insert_erase ha⟩
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
s t : Finset α
a : α
k r : ℕ
⊢ s ∈ ∂⁺ 𝒜 ↔ ∃ t, t ∈ 𝒜 ∧ t ⊆ s ∧ card t + 1 = card s
[PROOFSTEP]
refine' mem_upShadow_iff_erase_mem.trans ⟨_, _⟩
[GOAL]
case refine'_1
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
s t : Finset α
a : α
k r : ℕ
⊢ (∃ a, a ∈ s ∧ erase s a ∈ 𝒜) → ∃ t, t ∈ 𝒜 ∧ t ⊆ s ∧ card t + 1 = card s
[PROOFSTEP]
rintro ⟨a, ha, hs⟩
[GOAL]
case refine'_1.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
s t : Finset α
a✝ : α
k r : ℕ
a : α
ha : a ∈ s
hs : erase s a ∈ 𝒜
⊢ ∃ t, t ∈ 𝒜 ∧ t ⊆ s ∧ card t + 1 = card s
[PROOFSTEP]
exact ⟨s.erase a, hs, erase_subset _ _, card_erase_add_one ha⟩
[GOAL]
case refine'_2
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
s t : Finset α
a : α
k r : ℕ
⊢ (∃ t, t ∈ 𝒜 ∧ t ⊆ s ∧ card t + 1 = card s) → ∃ a, a ∈ s ∧ erase s a ∈ 𝒜
[PROOFSTEP]
rintro ⟨t, ht, hts, h⟩
[GOAL]
case refine'_2.intro.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
s t✝ : Finset α
a : α
k r : ℕ
t : Finset α
ht : t ∈ 𝒜
hts : t ⊆ s
h : card t + 1 = card s
⊢ ∃ a, a ∈ s ∧ erase s a ∈ 𝒜
[PROOFSTEP]
obtain ⟨a, ha⟩ : ∃ a, s \ t = { a } := card_eq_one.1 (by rw [card_sdiff hts, ← h, add_tsub_cancel_left])
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
s t✝ : Finset α
a : α
k r : ℕ
t : Finset α
ht : t ∈ 𝒜
hts : t ⊆ s
h : card t + 1 = card s
⊢ card (s \ t) = 1
[PROOFSTEP]
rw [card_sdiff hts, ← h, add_tsub_cancel_left]
[GOAL]
case refine'_2.intro.intro.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
s t✝ : Finset α
a✝ : α
k r : ℕ
t : Finset α
ht : t ∈ 𝒜
hts : t ⊆ s
h : card t + 1 = card s
a : α
ha : s \ t = {a}
⊢ ∃ a, a ∈ s ∧ erase s a ∈ 𝒜
[PROOFSTEP]
refine' ⟨a, sdiff_subset _ _ ((ha.ge : _ ⊆ _) <| mem_singleton_self a), _⟩
[GOAL]
case refine'_2.intro.intro.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
s t✝ : Finset α
a✝ : α
k r : ℕ
t : Finset α
ht : t ∈ 𝒜
hts : t ⊆ s
h : card t + 1 = card s
a : α
ha : s \ t = {a}
⊢ erase s a ∈ 𝒜
[PROOFSTEP]
rwa [← sdiff_singleton_eq_erase, ← ha, sdiff_sdiff_eq_self hts]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
s t : Finset α
a : α
k r : ℕ
⊢ s ∈ ∂⁺ ^[k] 𝒜 ↔ ∃ t, t ∈ 𝒜 ∧ t ⊆ s ∧ card t + k = card s
[PROOFSTEP]
induction' k with k ih generalizing 𝒜 s
[GOAL]
case zero
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜✝ : Finset (Finset α)
s✝ t : Finset α
a : α
k r : ℕ
𝒜 : Finset (Finset α)
s : Finset α
⊢ s ∈ ∂⁺ ^[zero] 𝒜 ↔ ∃ t, t ∈ 𝒜 ∧ t ⊆ s ∧ card t + zero = card s
[PROOFSTEP]
refine' ⟨fun hs => ⟨s, hs, Subset.refl _, rfl⟩, _⟩
[GOAL]
case zero
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜✝ : Finset (Finset α)
s✝ t : Finset α
a : α
k r : ℕ
𝒜 : Finset (Finset α)
s : Finset α
⊢ (∃ t, t ∈ 𝒜 ∧ t ⊆ s ∧ card t + zero = card s) → s ∈ ∂⁺ ^[zero] 𝒜
[PROOFSTEP]
rintro ⟨t, ht, hst, hcard⟩
[GOAL]
case zero.intro.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜✝ : Finset (Finset α)
s✝ t✝ : Finset α
a : α
k r : ℕ
𝒜 : Finset (Finset α)
s t : Finset α
ht : t ∈ 𝒜
hst : t ⊆ s
hcard : card t + zero = card s
⊢ s ∈ ∂⁺ ^[zero] 𝒜
[PROOFSTEP]
rwa [← eq_of_subset_of_card_le hst hcard.ge]
[GOAL]
case succ
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜✝ : Finset (Finset α)
s✝ t : Finset α
a : α
k✝ r k : ℕ
ih : ∀ {𝒜 : Finset (Finset α)} {s : Finset α}, s ∈ ∂⁺ ^[k] 𝒜 ↔ ∃ t, t ∈ 𝒜 ∧ t ⊆ s ∧ card t + k = card s
𝒜 : Finset (Finset α)
s : Finset α
⊢ s ∈ ∂⁺ ^[succ k] 𝒜 ↔ ∃ t, t ∈ 𝒜 ∧ t ⊆ s ∧ card t + succ k = card s
[PROOFSTEP]
simp only [exists_prop, Function.comp_apply, Function.iterate_succ]
[GOAL]
case succ
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜✝ : Finset (Finset α)
s✝ t : Finset α
a : α
k✝ r k : ℕ
ih : ∀ {𝒜 : Finset (Finset α)} {s : Finset α}, s ∈ ∂⁺ ^[k] 𝒜 ↔ ∃ t, t ∈ 𝒜 ∧ t ⊆ s ∧ card t + k = card s
𝒜 : Finset (Finset α)
s : Finset α
⊢ s ∈ ∂⁺ ^[k] (∂⁺ 𝒜) ↔ ∃ t, t ∈ 𝒜 ∧ t ⊆ s ∧ card t + succ k = card s
[PROOFSTEP]
refine' ih.trans _
[GOAL]
case succ
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜✝ : Finset (Finset α)
s✝ t : Finset α
a : α
k✝ r k : ℕ
ih : ∀ {𝒜 : Finset (Finset α)} {s : Finset α}, s ∈ ∂⁺ ^[k] 𝒜 ↔ ∃ t, t ∈ 𝒜 ∧ t ⊆ s ∧ card t + k = card s
𝒜 : Finset (Finset α)
s : Finset α
⊢ (∃ t, t ∈ ∂⁺ 𝒜 ∧ t ⊆ s ∧ card t + k = card s) ↔ ∃ t, t ∈ 𝒜 ∧ t ⊆ s ∧ card t + succ k = card s
[PROOFSTEP]
clear ih
[GOAL]
case succ
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜✝ : Finset (Finset α)
s✝ t : Finset α
a : α
k✝ r k : ℕ
𝒜 : Finset (Finset α)
s : Finset α
⊢ (∃ t, t ∈ ∂⁺ 𝒜 ∧ t ⊆ s ∧ card t + k = card s) ↔ ∃ t, t ∈ 𝒜 ∧ t ⊆ s ∧ card t + succ k = card s
[PROOFSTEP]
constructor
[GOAL]
case succ.mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜✝ : Finset (Finset α)
s✝ t : Finset α
a : α
k✝ r k : ℕ
𝒜 : Finset (Finset α)
s : Finset α
⊢ (∃ t, t ∈ ∂⁺ 𝒜 ∧ t ⊆ s ∧ card t + k = card s) → ∃ t, t ∈ 𝒜 ∧ t ⊆ s ∧ card t + succ k = card s
[PROOFSTEP]
rintro ⟨t, ht, hts, hcardst⟩
[GOAL]
case succ.mp.intro.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜✝ : Finset (Finset α)
s✝ t✝ : Finset α
a : α
k✝ r k : ℕ
𝒜 : Finset (Finset α)
s t : Finset α
ht : t ∈ ∂⁺ 𝒜
hts : t ⊆ s
hcardst : card t + k = card s
⊢ ∃ t, t ∈ 𝒜 ∧ t ⊆ s ∧ card t + succ k = card s
[PROOFSTEP]
obtain ⟨u, hu, hut, hcardtu⟩ := mem_upShadow_iff_exists_mem_card_add_one.1 ht
[GOAL]
case succ.mp.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜✝ : Finset (Finset α)
s✝ t✝ : Finset α
a : α
k✝ r k : ℕ
𝒜 : Finset (Finset α)
s t : Finset α
ht : t ∈ ∂⁺ 𝒜
hts : t ⊆ s
hcardst : card t + k = card s
u : Finset α
hu : u ∈ 𝒜
hut : u ⊆ t
hcardtu : card u + 1 = card t
⊢ ∃ t, t ∈ 𝒜 ∧ t ⊆ s ∧ card t + succ k = card s
[PROOFSTEP]
refine' ⟨u, hu, hut.trans hts, _⟩
[GOAL]
case succ.mp.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜✝ : Finset (Finset α)
s✝ t✝ : Finset α
a : α
k✝ r k : ℕ
𝒜 : Finset (Finset α)
s t : Finset α
ht : t ∈ ∂⁺ 𝒜
hts : t ⊆ s
hcardst : card t + k = card s
u : Finset α
hu : u ∈ 𝒜
hut : u ⊆ t
hcardtu : card u + 1 = card t
⊢ card u + succ k = card s
[PROOFSTEP]
rw [← hcardst, ← hcardtu, add_right_comm]
[GOAL]
case succ.mp.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜✝ : Finset (Finset α)
s✝ t✝ : Finset α
a : α
k✝ r k : ℕ
𝒜 : Finset (Finset α)
s t : Finset α
ht : t ∈ ∂⁺ 𝒜
hts : t ⊆ s
hcardst : card t + k = card s
u : Finset α
hu : u ∈ 𝒜
hut : u ⊆ t
hcardtu : card u + 1 = card t
⊢ card u + succ k = card u + k + 1
[PROOFSTEP]
rfl
[GOAL]
case succ.mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜✝ : Finset (Finset α)
s✝ t : Finset α
a : α
k✝ r k : ℕ
𝒜 : Finset (Finset α)
s : Finset α
⊢ (∃ t, t ∈ 𝒜 ∧ t ⊆ s ∧ card t + succ k = card s) → ∃ t, t ∈ ∂⁺ 𝒜 ∧ t ⊆ s ∧ card t + k = card s
[PROOFSTEP]
rintro ⟨t, ht, hts, hcard⟩
[GOAL]
case succ.mpr.intro.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜✝ : Finset (Finset α)
s✝ t✝ : Finset α
a : α
k✝ r k : ℕ
𝒜 : Finset (Finset α)
s t : Finset α
ht : t ∈ 𝒜
hts : t ⊆ s
hcard : card t + succ k = card s
⊢ ∃ t, t ∈ ∂⁺ 𝒜 ∧ t ⊆ s ∧ card t + k = card s
[PROOFSTEP]
obtain ⟨u, htu, hus, hu⟩ :=
  Finset.exists_intermediate_set 1
    (by
      rw [add_comm, ← hcard]
      exact add_le_add_left (succ_le_of_lt (zero_lt_succ _)) _)
    hts
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜✝ : Finset (Finset α)
s✝ t✝ : Finset α
a : α
k✝ r k : ℕ
𝒜 : Finset (Finset α)
s t : Finset α
ht : t ∈ 𝒜
hts : t ⊆ s
hcard : card t + succ k = card s
⊢ 1 + card t ≤ card s
[PROOFSTEP]
rw [add_comm, ← hcard]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜✝ : Finset (Finset α)
s✝ t✝ : Finset α
a : α
k✝ r k : ℕ
𝒜 : Finset (Finset α)
s t : Finset α
ht : t ∈ 𝒜
hts : t ⊆ s
hcard : card t + succ k = card s
⊢ card t + 1 ≤ card t + succ k
[PROOFSTEP]
exact add_le_add_left (succ_le_of_lt (zero_lt_succ _)) _
[GOAL]
case succ.mpr.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜✝ : Finset (Finset α)
s✝ t✝ : Finset α
a : α
k✝ r k : ℕ
𝒜 : Finset (Finset α)
s t : Finset α
ht : t ∈ 𝒜
hts : t ⊆ s
hcard : card t + succ k = card s
u : Finset α
htu : t ⊆ u
hus : u ⊆ s
hu : card u = 1 + card t
⊢ ∃ t, t ∈ ∂⁺ 𝒜 ∧ t ⊆ s ∧ card t + k = card s
[PROOFSTEP]
rw [add_comm] at hu 
[GOAL]
case succ.mpr.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜✝ : Finset (Finset α)
s✝ t✝ : Finset α
a : α
k✝ r k : ℕ
𝒜 : Finset (Finset α)
s t : Finset α
ht : t ∈ 𝒜
hts : t ⊆ s
hcard : card t + succ k = card s
u : Finset α
htu : t ⊆ u
hus : u ⊆ s
hu : card u = card t + 1
⊢ ∃ t, t ∈ ∂⁺ 𝒜 ∧ t ⊆ s ∧ card t + k = card s
[PROOFSTEP]
refine' ⟨u, mem_upShadow_iff_exists_mem_card_add_one.2 ⟨t, ht, htu, hu.symm⟩, hus, _⟩
[GOAL]
case succ.mpr.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜✝ : Finset (Finset α)
s✝ t✝ : Finset α
a : α
k✝ r k : ℕ
𝒜 : Finset (Finset α)
s t : Finset α
ht : t ∈ 𝒜
hts : t ⊆ s
hcard : card t + succ k = card s
u : Finset α
htu : t ⊆ u
hus : u ⊆ s
hu : card u = card t + 1
⊢ card u + k = card s
[PROOFSTEP]
rw [hu, ← hcard, add_right_comm]
[GOAL]
case succ.mpr.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜✝ : Finset (Finset α)
s✝ t✝ : Finset α
a : α
k✝ r k : ℕ
𝒜 : Finset (Finset α)
s t : Finset α
ht : t ∈ 𝒜
hts : t ⊆ s
hcard : card t + succ k = card s
u : Finset α
htu : t ⊆ u
hus : u ⊆ s
hu : card u = card t + 1
⊢ card t + k + 1 = card t + succ k
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
s t : Finset α
a : α
k r : ℕ
⊢ image compl (∂ 𝒜) = ∂⁺ (image compl 𝒜)
[PROOFSTEP]
ext s
[GOAL]
case a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
s✝ t : Finset α
a : α
k r : ℕ
s : Finset α
⊢ s ∈ image compl (∂ 𝒜) ↔ s ∈ ∂⁺ (image compl 𝒜)
[PROOFSTEP]
simp only [mem_image, exists_prop, mem_shadow_iff, mem_upShadow_iff]
[GOAL]
case a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
s✝ t : Finset α
a : α
k r : ℕ
s : Finset α
⊢ (∃ a, (∃ t, t ∈ 𝒜 ∧ ∃ a_1, a_1 ∈ t ∧ erase t a_1 = a) ∧ aᶜ = s) ↔
    ∃ t, (∃ a, a ∈ 𝒜 ∧ aᶜ = t) ∧ ∃ a, ¬a ∈ t ∧ insert a t = s
[PROOFSTEP]
constructor
[GOAL]
case a.mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
s✝ t : Finset α
a : α
k r : ℕ
s : Finset α
⊢ (∃ a, (∃ t, t ∈ 𝒜 ∧ ∃ a_1, a_1 ∈ t ∧ erase t a_1 = a) ∧ aᶜ = s) →
    ∃ t, (∃ a, a ∈ 𝒜 ∧ aᶜ = t) ∧ ∃ a, ¬a ∈ t ∧ insert a t = s
[PROOFSTEP]
rintro ⟨_, ⟨s, hs, a, ha, rfl⟩, rfl⟩
[GOAL]
case a.mp.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
s✝ t : Finset α
a✝ : α
k r : ℕ
s : Finset α
hs : s ∈ 𝒜
a : α
ha : a ∈ s
⊢ ∃ t, (∃ a, a ∈ 𝒜 ∧ aᶜ = t) ∧ ∃ a_1, ¬a_1 ∈ t ∧ insert a_1 t = (erase s a)ᶜ
[PROOFSTEP]
exact ⟨sᶜ, ⟨s, hs, rfl⟩, a, not_mem_compl.2 ha, compl_erase.symm⟩
[GOAL]
case a.mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
s✝ t : Finset α
a : α
k r : ℕ
s : Finset α
⊢ (∃ t, (∃ a, a ∈ 𝒜 ∧ aᶜ = t) ∧ ∃ a, ¬a ∈ t ∧ insert a t = s) →
    ∃ a, (∃ t, t ∈ 𝒜 ∧ ∃ a_1, a_1 ∈ t ∧ erase t a_1 = a) ∧ aᶜ = s
[PROOFSTEP]
rintro ⟨_, ⟨s, hs, rfl⟩, a, ha, rfl⟩
[GOAL]
case a.mpr.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
s✝ t : Finset α
a✝ : α
k r : ℕ
s : Finset α
hs : s ∈ 𝒜
a : α
ha : ¬a ∈ sᶜ
⊢ ∃ a_1, (∃ t, t ∈ 𝒜 ∧ ∃ a, a ∈ t ∧ erase t a = a_1) ∧ a_1ᶜ = insert a sᶜ
[PROOFSTEP]
exact ⟨s.erase a, ⟨s, hs, a, not_mem_compl.1 ha, rfl⟩, compl_erase⟩
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
s t : Finset α
a : α
k r : ℕ
⊢ image compl (∂⁺ 𝒜) = ∂ (image compl 𝒜)
[PROOFSTEP]
ext s
[GOAL]
case a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
s✝ t : Finset α
a : α
k r : ℕ
s : Finset α
⊢ s ∈ image compl (∂⁺ 𝒜) ↔ s ∈ ∂ (image compl 𝒜)
[PROOFSTEP]
simp only [mem_image, exists_prop, mem_shadow_iff, mem_upShadow_iff]
[GOAL]
case a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
s✝ t : Finset α
a : α
k r : ℕ
s : Finset α
⊢ (∃ a, (∃ t, t ∈ 𝒜 ∧ ∃ a_1, ¬a_1 ∈ t ∧ insert a_1 t = a) ∧ aᶜ = s) ↔
    ∃ t, (∃ a, a ∈ 𝒜 ∧ aᶜ = t) ∧ ∃ a, a ∈ t ∧ erase t a = s
[PROOFSTEP]
constructor
[GOAL]
case a.mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
s✝ t : Finset α
a : α
k r : ℕ
s : Finset α
⊢ (∃ a, (∃ t, t ∈ 𝒜 ∧ ∃ a_1, ¬a_1 ∈ t ∧ insert a_1 t = a) ∧ aᶜ = s) →
    ∃ t, (∃ a, a ∈ 𝒜 ∧ aᶜ = t) ∧ ∃ a, a ∈ t ∧ erase t a = s
[PROOFSTEP]
rintro ⟨_, ⟨s, hs, a, ha, rfl⟩, rfl⟩
[GOAL]
case a.mp.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
s✝ t : Finset α
a✝ : α
k r : ℕ
s : Finset α
hs : s ∈ 𝒜
a : α
ha : ¬a ∈ s
⊢ ∃ t, (∃ a, a ∈ 𝒜 ∧ aᶜ = t) ∧ ∃ a_1, a_1 ∈ t ∧ erase t a_1 = (insert a s)ᶜ
[PROOFSTEP]
exact ⟨sᶜ, ⟨s, hs, rfl⟩, a, mem_compl.2 ha, compl_insert.symm⟩
[GOAL]
case a.mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
s✝ t : Finset α
a : α
k r : ℕ
s : Finset α
⊢ (∃ t, (∃ a, a ∈ 𝒜 ∧ aᶜ = t) ∧ ∃ a, a ∈ t ∧ erase t a = s) →
    ∃ a, (∃ t, t ∈ 𝒜 ∧ ∃ a_1, ¬a_1 ∈ t ∧ insert a_1 t = a) ∧ aᶜ = s
[PROOFSTEP]
rintro ⟨_, ⟨s, hs, rfl⟩, a, ha, rfl⟩
[GOAL]
case a.mpr.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
s✝ t : Finset α
a✝ : α
k r : ℕ
s : Finset α
hs : s ∈ 𝒜
a : α
ha : a ∈ sᶜ
⊢ ∃ a_1, (∃ t, t ∈ 𝒜 ∧ ∃ a, ¬a ∈ t ∧ insert a t = a_1) ∧ a_1ᶜ = erase sᶜ a
[PROOFSTEP]
exact ⟨insert a s, ⟨s, hs, a, mem_compl.1 ha, rfl⟩, compl_insert⟩
