have z : (n - 1).choose (n - r) < 𝒜ᶜˢ.card := by
  rwa [card_compls, choose_symm_of_eq_add (tsub_add_tsub_cancel ‹r ≤ n› ‹1 ≤ r›).symm]
case inr
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n : ℕ
𝒜 : Finset (Finset (Fin n))
r : ℕ
h𝒜 : (↑𝒜).Intersecting
h₂ : Set.Sized r ↑𝒜
h₃ : r ≤ n / 2
h1r : r > 0
size : (n - 1).choose (r - 1) < 𝒜.card
this✝¹ : Disjoint 𝒜 (∂ ^[n - 2 * r] 𝒜ᶜˢ)
this✝ : r ≤ n
this : 1 ≤ n
⊢ False
case inr
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n : ℕ
𝒜 : Finset (Finset (Fin n))
r : ℕ
h𝒜 : (↑𝒜).Intersecting
h₂ : Set.Sized r ↑𝒜
h₃ : r ≤ n / 2
h1r : r > 0
size : (n - 1).choose (r - 1) < 𝒜.card
this✝¹ : Disjoint 𝒜 (∂ ^[n - 2 * r] 𝒜ᶜˢ)
this✝ : r ≤ n
this : 1 ≤ n
z : (n - 1).choose (n - r) < 𝒜ᶜˢ.card
⊢ False