have : n.choose r < (𝒜 ∪ ∂^[n - 2 * r] 𝒜ᶜˢ).card := by
  rw [card_union_of_disjoint ‹_›]
  convert lt_of_le_of_lt (add_le_add_left kk _) (add_lt_add_right size _) using 1
  convert Nat.choose_succ_succ _ _ using 3
  all_goals rwa [Nat.sub_one, Nat.succ_pred_eq_of_pos]
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
h𝒜bar : Set.Sized (n - r) ↑𝒜ᶜˢ
this : n - 2 * r ≤ n - r
kk : (n - 1).choose r ≤ (∂ ^[n - 2 * r] 𝒜ᶜˢ).card
q : n - r - (n - 2 * r) = r
⊢ 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
h𝒜bar : Set.Sized (n - r) ↑𝒜ᶜˢ
this✝ : n - 2 * r ≤ n - r
kk : (n - 1).choose r ≤ (∂ ^[n - 2 * r] 𝒜ᶜˢ).card
q : n - r - (n - 2 * r) = r
this : n.choose r < (𝒜 ∪ ∂ ^[n - 2 * r] 𝒜ᶜˢ).card
⊢ False