simpa
case zero
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n i r : ℕ
𝒜 𝒞 : Finset (Finset (Fin n))
h₁ : Set.Sized r ↑𝒜
h₂ : 𝒞.card ≤ 𝒜.card
h₃ : IsInitSeg 𝒞 r
⊢ (∂ ^[0] 𝒞).card ≤ (∂ ^[0] 𝒜).card
no goals