simp only [mem_shadow_iff_insert_mem, mem_initSeg, exists_prop]
case a
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s t✝ : Finset α
r : ℕ
inst✝ : Fintype α
hs : s.Nonempty
t : Finset α
⊢ t ∈ ∂ (initSeg s) ↔ t ∈ initSeg (s.erase (s.min' hs))
case a
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s t✝ : Finset α
r : ℕ
inst✝ : Fintype α
hs : s.Nonempty
t : Finset α
⊢ (∃ a ∉ t, s.card = (insert a t).card ∧ { ofColex := insert a t } ≤ { ofColex := s }) ↔
    (s.erase (s.min' hs)).card = t.card ∧ { ofColex := t } ≤ { ofColex := s.erase (s.min' hs) }