no goals
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
s t : Finset α
a : α
k r : ℕ
⊢ s ∈ (∂⁺ ) 𝒜 ↔ ∃ t, t ∈ 𝒜 ∧ ∃ a x, insert a t = s
simp_rw [upShadow, mem_sup, mem_image, exists_prop, mem_compl]