refine' ⟨fun t ht ↦ _, ‹_›⟩
case intro
α : 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 ↑𝒞
this : (∂ ^[i] 𝒞).card = k.choose (r - i)
A B : Finset (Fin n)
hA : A ∈ 𝒞
HB₁ : { ofColex := B } < { ofColex := A }
HB₂ : B.card = r
⊢ B ⊆ range'k ∧ B.card = r
case intro
α : 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 ↑𝒞
this : (∂ ^[i] 𝒞).card = k.choose (r - i)
A B : Finset (Fin n)
hA : A ∈ 𝒞
HB₁ : { ofColex := B } < { ofColex := A }
HB₂ : B.card = r
t : Fin n
ht : t ∈ B
⊢ t ∈ range'k