Theorem: Finset.EKR (LeanCamCombi/KruskalKatona.lean)

State before:
α : 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
⊢ 𝒜.card ≤ (n - 1).choose (r - 1)
Tactic:
cases' Nat.eq_zero_or_pos r with b h1r
State after:
case inl
α : 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
b : r = 0
⊢ 𝒜.card ≤ (n - 1).choose (r - 1)

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
⊢ 𝒜.card ≤ (n - 1).choose (r - 1)

State before:
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
⊢ 𝒜.card ≤ (n - 1).choose (r - 1)
Tactic:
refine' le_of_not_lt fun size ↦ _
State after:
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
⊢ False

State before:
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
⊢ False
Tactic:
have : Disjoint 𝒜 (∂^[n - 2 * r] 𝒜ᶜˢ) := disjoint_right.2 fun A hAbar hA ↦ by
  simp [mem_shadow_iterate_iff_exists_sdiff, mem_compls] at hAbar
  obtain ⟨C, hC, hAC, _⟩ := hAbar
  exact h𝒜 hA hC (disjoint_of_subset_left hAC disjoint_compl_right)
State after:
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] 𝒜ᶜˢ)
⊢ False

State before:
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] 𝒜ᶜˢ)
⊢ False
Tactic:
have : r ≤ n := h₃.trans (Nat.div_le_self n 2)
State after:
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
⊢ False

State before:
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
⊢ False
Tactic:
have : 1 ≤ n := ‹1 ≤ r›.trans ‹r ≤ n›
State after:
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

State before:
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
Tactic:
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]
State after:
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

State before:
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
Tactic:
have h𝒜bar : (𝒜ᶜˢ : Set (Finset (Fin n))).Sized (n - r) := by simpa using h₂.compls
State after:
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

State before:
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
Tactic:
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
State after:
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

State before:
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
Tactic:
have kk :=
  lovasz_form ‹n - 2 * r ≤ n - r› ((tsub_le_tsub_iff_left ‹1 ≤ n›).2 h1r) tsub_le_self h𝒜bar z.le
State after:
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

State before:
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
Tactic:
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₃
State after:
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

State before:
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
Tactic:
rw [q] at kk
State after:
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

State before:
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
Tactic:
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]
State after:
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

State before:
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
Tactic:
apply this.not_le
State after:
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
⊢ (𝒜 ∪ ∂ ^[n - 2 * r] 𝒜ᶜˢ).card ≤ n.choose r

State before:
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
⊢ (𝒜 ∪ ∂ ^[n - 2 * r] 𝒜ᶜˢ).card ≤ n.choose r
Tactic:
convert Set.Sized.card_le _
State after:
case h.e'_4.h.e'_1
α : 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
⊢ n = Fintype.card (Fin n)

case inr.convert_2
α : 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
⊢ Fintype (Fin n)

case inr.convert_5
α : 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
⊢ Set.Sized r ↑(𝒜 ∪ ∂ ^[n - 2 * r] 𝒜ᶜˢ)

State before:
case inr.convert_5
α : 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
⊢ Set.Sized r ↑(𝒜 ∪ ∂ ^[n - 2 * r] 𝒜ᶜˢ)
Tactic:
rw [coe_union, Set.sized_union]
State after:
case inr.convert_5
α : 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
⊢ Set.Sized r ↑𝒜 ∧ Set.Sized r ↑(∂ ^[n - 2 * r] 𝒜ᶜˢ)

State before:
case inr.convert_5
α : 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
⊢ Set.Sized r ↑𝒜 ∧ Set.Sized r ↑(∂ ^[n - 2 * r] 𝒜ᶜˢ)
Tactic:
refine' ⟨‹_›, _⟩
State after:
case inr.convert_5
α : 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
⊢ Set.Sized r ↑(∂ ^[n - 2 * r] 𝒜ᶜˢ)

State before:
case inr.convert_5
α : 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
⊢ Set.Sized r ↑(∂ ^[n - 2 * r] 𝒜ᶜˢ)
Tactic:
convert h𝒜bar.shadow_iterate
State after:
case h.e'_2
α : 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
⊢ r = n - r - (n - 2 * r)

State before:
case h.e'_2
α : 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
⊢ r = n - r - (n - 2 * r)
Tactic:
rw [q]
State after:
no goals

State before:
case inl
α : 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
b : r = 0
⊢ 𝒜.card ≤ (n - 1).choose (r - 1)
Tactic:
convert Nat.zero_le _
State after:
case h.e'_3
α : 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
b : r = 0
⊢ 𝒜.card = 0

State before:
case h.e'_3
α : 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
b : r = 0
⊢ 𝒜.card = 0
Tactic:
rw [Finset.card_eq_zero, eq_empty_iff_forall_not_mem]
State after:
case h.e'_3
α : 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
b : r = 0
⊢ ∀ (x : Finset (Fin n)), x ∉ 𝒜

State before:
case h.e'_3
α : 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
b : r = 0
⊢ ∀ (x : Finset (Fin n)), x ∉ 𝒜
Tactic:
refine' fun A HA ↦ h𝒜 HA HA _
State after:
case h.e'_3
α : 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
b : r = 0
A : Finset (Fin n)
HA : A ∈ 𝒜
⊢ Disjoint A A

State before:
case h.e'_3
α : 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
b : r = 0
A : Finset (Fin n)
HA : A ∈ 𝒜
⊢ Disjoint A A
Tactic:
rw [disjoint_self_iff_empty, ← Finset.card_eq_zero, ← b]
State after:
case h.e'_3
α : 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
b : r = 0
A : Finset (Fin n)
HA : A ∈ 𝒜
⊢ A.card = r

State before:
case h.e'_3
α : 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
b : r = 0
A : Finset (Fin n)
HA : A ∈ 𝒜
⊢ A.card = r
Tactic:
exact h₂ HA
State after:
no goals

State before:
α : 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
A : Finset (Fin n)
hAbar : A ∈ ∂ ^[n - 2 * r] 𝒜ᶜˢ
hA : A ∈ 𝒜
⊢ False
Tactic:
simp [mem_shadow_iterate_iff_exists_sdiff, mem_compls] at hAbar
State after:
α : 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
A : Finset (Fin n)
hA : A ∈ 𝒜
hAbar : ∃ s, sᶜ ∈ 𝒜 ∧ A ⊆ s ∧ (s \ A).card = n - 2 * r
⊢ False

State before:
α : 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
A : Finset (Fin n)
hA : A ∈ 𝒜
hAbar : ∃ s, sᶜ ∈ 𝒜 ∧ A ⊆ s ∧ (s \ A).card = n - 2 * r
⊢ False
Tactic:
obtain ⟨C, hC, hAC, _⟩ := hAbar
State after:
case intro.intro.intro
α : 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
A : Finset (Fin n)
hA : A ∈ 𝒜
C : Finset (Fin n)
hC : Cᶜ ∈ 𝒜
hAC : A ⊆ C
right✝ : (C \ A).card = n - 2 * r
⊢ False

State before:
case intro.intro.intro
α : 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
A : Finset (Fin n)
hA : A ∈ 𝒜
C : Finset (Fin n)
hC : Cᶜ ∈ 𝒜
hAC : A ⊆ C
right✝ : (C \ A).card = n - 2 * r
⊢ False
Tactic:
exact h𝒜 hA hC (disjoint_of_subset_left hAC disjoint_compl_right)
State after:
no goals

State before:
α : 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
⊢ (n - 1).choose (n - r) < 𝒜ᶜˢ.card
Tactic:
rwa [card_compls, choose_symm_of_eq_add (tsub_add_tsub_cancel ‹r ≤ n› ‹1 ≤ r›).symm]
State after:
no goals

State before:
α : 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
⊢ Set.Sized (n - r) ↑𝒜ᶜˢ
Tactic:
simpa using h₂.compls
State after:
no goals

State before:
α : 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) ↑𝒜ᶜˢ
⊢ n - 2 * r ≤ n - r
Tactic:
rw [tsub_le_tsub_iff_left ‹r ≤ n›]
State after:
α : 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) ↑𝒜ᶜˢ
⊢ r ≤ 2 * r

State before:
α : 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) ↑𝒜ᶜˢ
⊢ r ≤ 2 * r
Tactic:
exact Nat.le_mul_of_pos_left _ zero_lt_two
State after:
no goals

State before:
α : 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
⊢ n - r - (n - 2 * r) = r
Tactic:
rw [tsub_right_comm, Nat.sub_sub_self, two_mul]
State after:
α : 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
⊢ r + r - r = r

α : 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
⊢ 2 * r ≤ n

State before:
α : 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
⊢ r + r - r = r

α : 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
⊢ 2 * r ≤ n
Tactic:
apply Nat.add_sub_cancel
State after:
α : 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
⊢ 2 * r ≤ n

State before:
α : 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
⊢ 2 * r ≤ n
Tactic:
rw [mul_comm, ← Nat.le_div_iff_mul_le' zero_lt_two]
State after:
α : 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
⊢ r ≤ n / 2

State before:
α : 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
⊢ r ≤ n / 2
Tactic:
exact h₃
State after:
no goals

State before:
α : 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
⊢ n.choose r < (𝒜 ∪ ∂ ^[n - 2 * r] 𝒜ᶜˢ).card
Tactic:
rw [card_union_of_disjoint ‹_›]
State after:
α : 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
⊢ n.choose r < 𝒜.card + (∂ ^[n - 2 * r] 𝒜ᶜˢ).card

State before:
α : 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
⊢ n.choose r < 𝒜.card + (∂ ^[n - 2 * r] 𝒜ᶜˢ).card
Tactic:
convert lt_of_le_of_lt (add_le_add_left kk _) (add_lt_add_right size _) using 1
State after:
case h.e'_3
α : 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
⊢ n.choose r = (n - 1).choose (r - 1) + (n - 1).choose r

State before:
case h.e'_3
α : 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
⊢ n.choose r = (n - 1).choose (r - 1) + (n - 1).choose r
Tactic:
convert Nat.choose_succ_succ _ _ using 3
State after:
case h.e'_2.h.e'_1
α : 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
⊢ n = (n - 1).succ

case h.e'_2.h.e'_2
α : 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
⊢ r = (r - 1).succ

case h.e'_3.h.e'_6.h.e'_2
α : 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
⊢ r = (r - 1).succ

State before:
case h.e'_2.h.e'_1
α : 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
⊢ n = (n - 1).succ

case h.e'_2.h.e'_2
α : 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
⊢ r = (r - 1).succ

case h.e'_3.h.e'_6.h.e'_2
α : 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
⊢ r = (r - 1).succ
Tactic:
all_goals rwa [Nat.sub_one, Nat.succ_pred_eq_of_pos]
State after:
no goals

State before:
case h.e'_3.h.e'_6.h.e'_2
α : 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
⊢ r = (r - 1).succ
Tactic:
rwa [Nat.sub_one, Nat.succ_pred_eq_of_pos]
State after:
no goals

State before:
case h.e'_4.h.e'_1
α : 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
⊢ n = Fintype.card (Fin n)
Tactic:
rw [Fintype.card_fin]
State after:
no goals