obtain ⟨C, BsubC, hCrange, hcard⟩ := this
case a.mpr.intro.refine_2
α : 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 ↑𝒞
B : Finset (Fin n)
hBk : B ⊆ range'k
hB : B.card = r - i
this : ∃ C, B ⊆ C ∧ C ⊆ range'k ∧ C.card = i + B.card
⊢ ∃ s ∈ 𝒞, B ⊆ s ∧ (s \ B).card = i

case a.mpr.intro.refine_1
α : 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 ↑𝒞
B : Finset (Fin n)
hBk : B ⊆ range'k
hB : B.card = r - i
⊢ i + B.card ≤ range'k.card
case a.mpr.intro.refine_2.intro.intro.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 ↑𝒞
B : Finset (Fin n)
hBk : B ⊆ range'k
hB : B.card = r - i
C : Finset (Fin n)
BsubC : B ⊆ C
hCrange : C ⊆ range'k
hcard : C.card = i + B.card
⊢ ∃ s ∈ 𝒞, B ⊆ s ∧ (s \ B).card = i

case a.mpr.intro.refine_1
α : 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 ↑𝒞
B : Finset (Fin n)
hBk : B ⊆ range'k
hB : B.card = r - i
⊢ i + B.card ≤ range'k.card