have := shadow_monotone this
case intro.inl
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s t : Finset α
inst✝ : Finite α
val✝ : Fintype α
h₁ : IsInitSeg 𝒜 0
this : 𝒜 ⊆ {∅}
⊢ IsInitSeg (∂ 𝒜) (0 - 1)
case intro.inl
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s t : Finset α
inst✝ : Finite α
val✝ : Fintype α
h₁ : IsInitSeg 𝒜 0
this✝ : 𝒜 ⊆ {∅}
this : ∂ 𝒜 ≤ ∂ {∅}
⊢ IsInitSeg (∂ 𝒜) (0 - 1)