have q : n - r - (n - 2 * r) = r := by
  rw [tsub_right_comm, Nat.sub_sub_self, two_mul]
  apply Nat.add_sub_cancel
  rw [mul_comm, ← Nat.le_div_iff_mul_le' zero_lt_two]
  exact h₃
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 (n - r - (n - 2 * r)) ≤ (∂ ^[n - 2 * r] 𝒜ᶜˢ).card
⊢ 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 (n - r - (n - 2 * r)) ≤ (∂ ^[n - 2 * r] 𝒜ᶜˢ).card
q : n - r - (n - 2 * r) = r
⊢ False