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 𝒜)
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
s t : Finset α
a : α
k r : ℕ
⊢ image compl ((∂ ) 𝒜) = (∂⁺ ) (image compl 𝒜)
ext s
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
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 𝒜)
simp only [mem_image, exists_prop, mem_shadow_iff, mem_upShadow_iff]
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

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
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
constructor
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ᶜ
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
rintro ⟨_, ⟨s, hs, a, ha, rfl⟩, rfl⟩
no goals
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ᶜ
exact ⟨sᶜ, ⟨s, hs, rfl⟩, a, not_mem_compl.2 ha, compl_erase.symm⟩
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ᶜ)
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
rintro ⟨_, ⟨s, hs, rfl⟩, a, ha, rfl⟩
no goals
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ᶜ)
exact ⟨s.erase a, ⟨s, hs, a, not_mem_compl.1 ha, rfl⟩, compl_erase⟩