suffices this : (∂^[i] 𝒞).card = k.choose  (r - i) by
  rw [← this]
  apply iterated_kk h₁ _ _
  rwa [Ccard]
  refine' ⟨‹_›, _⟩
  rintro A B hA ⟨HB₁, HB₂⟩
  rw [mem_powersetCard]
  refine' ⟨fun t ht ↦ _, ‹_›⟩
  rw [mem_attachFin, mem_range]
  have : toColex (image Fin.val B) < toColex (image Fin.val A) := by
    rwa [toColex_image_lt_toColex_image Fin.val_strictMono]
  apply Colex.forall_lt_mono this.le _ t (mem_image.2 ⟨t, ht, rfl⟩)
  simp_rw [mem_image]
  rintro _ ⟨a, ha, q⟩
  rw [mem_powersetCard] at hA
  rw [← q, ← mem_range]
  have := hA.1 ha
  rwa [mem_attachFin] at this
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n r k i : ℕ
𝒜 𝒞✝ : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ 𝒜.card
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
Ccard : 𝒞.card = k.choose r
this : Set.Sized r ↑𝒞
⊢ k.choose (r - i) ≤ (∂ ^[i] 𝒜).card
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n r k i : ℕ
𝒜 𝒞✝ : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ 𝒜.card
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
Ccard : 𝒞.card = k.choose r
this : Set.Sized r ↑𝒞
⊢ (∂ ^[i] 𝒞).card = k.choose (r - i)