have : n - 2 * r ≤ n - r := by
  rw [tsub_le_tsub_iff_left ‹r ≤ n›]
  exact Nat.le_mul_of_pos_left _ zero_lt_two
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) ↑𝒜ᶜˢ
⊢ 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
⊢ False