-- Mathlib/Combinatorics/SetFamily/KruskalKatona.lean
theorem erdos_ko_rado {𝒜 : Finset (Finset (Fin n))} {r : ℕ}
    (h𝒜 : (𝒜 : Set (Finset (Fin n))).Intersecting) (h₂ : (𝒜 : Set (Finset (Fin n))).Sized r)
    (h₃ : r ≤ n / 2) :
    #𝒜 ≤ (n - 1).choose (r - 1)

Proof state:
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) < #𝒜
this✝³ : Disjoint 𝒜 (∂ ^[n - 2 * r] 𝒜ᶜˢ)
this✝² : r ≤ n
this✝¹ : 1 ≤ n
z : (n - 1).choose (n - r) < #𝒜ᶜˢ
h𝒜bar : Set.Sized (n - r) ↑𝒜ᶜˢ
this✝ : n - 2 * r ≤ n - r
kk : (n - 1).choose r ≤ #(∂ ^[n - 2 * r] 𝒜ᶜˢ)
this : n - r - (n - 2 * r) = r
⊢ n.choose r < #(𝒜 ∪ ∂ ^[n - 2 * r] 𝒜ᶜˢ)

Tactic:
rw [card_union_of_disjoint ‹_›]

Result:
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) < #𝒜
this✝³ : Disjoint 𝒜 (∂ ^[n - 2 * r] 𝒜ᶜˢ)
this✝² : r ≤ n
this✝¹ : 1 ≤ n
z : (n - 1).choose (n - r) < #𝒜ᶜˢ
h𝒜bar : Set.Sized (n - r) ↑𝒜ᶜˢ
this✝ : n - 2 * r ≤ n - r
kk : (n - 1).choose r ≤ #(∂ ^[n - 2 * r] 𝒜ᶜˢ)
this : n - r - (n - 2 * r) = r
⊢ n.choose r < #𝒜 + #(∂ ^[n - 2 * r] 𝒜ᶜˢ)

Proof state:
case inr
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) < #𝒜
this : Disjoint 𝒜 (∂ ^[n - 2 * r] 𝒜ᶜˢ)
⊢ False

Tactic:
have : r ≤ n := h₃.trans (Nat.div_le_self n 2)

Result:
case inr
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) < #𝒜
this✝ : Disjoint 𝒜 (∂ ^[n - 2 * r] 𝒜ᶜˢ)
this : r ≤ n
⊢ False

Proof state:
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) < #𝒜
this✝¹ : Disjoint 𝒜 (∂ ^[n - 2 * r] 𝒜ᶜˢ)
this✝ : r ≤ n
this : 1 ≤ n
z : (n - 1).choose (n - r) < #𝒜ᶜˢ
⊢ Set.Sized (n - r) ↑𝒜ᶜˢ

Tactic:
simpa using h₂.compls

Result:
no goals

Proof state:
case inr
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) < #𝒜
this✝¹ : Disjoint 𝒜 (∂ ^[n - 2 * r] 𝒜ᶜˢ)
this✝ : r ≤ n
this : 1 ≤ n
z : (n - 1).choose (n - r) < #𝒜ᶜˢ
⊢ False

Tactic:
have h𝒜bar : (𝒜ᶜˢ : Set (Finset (Fin n))).Sized (n - r) := by simpa using h₂.compls

Result:
case inr
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) < #𝒜
this✝¹ : Disjoint 𝒜 (∂ ^[n - 2 * r] 𝒜ᶜˢ)
this✝ : r ≤ n
this : 1 ≤ n
z : (n - 1).choose (n - r) < #𝒜ᶜˢ
h𝒜bar : Set.Sized (n - r) ↑𝒜ᶜˢ
⊢ False

Proof state:
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) < #𝒜
A : Finset (Fin n)
hA : A ∈ 𝒜
hAbar : ∃ s, sᶜ ∈ 𝒜 ∧ A ⊆ s ∧ #(s \ A) = n - 2 * r
⊢ False

Tactic:
obtain ⟨C, hC, hAC, _⟩ := hAbar

Result:
case intro.intro.intro
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) < #𝒜
A : Finset (Fin n)
hA : A ∈ 𝒜
C : Finset (Fin n)
hC : Cᶜ ∈ 𝒜
hAC : A ⊆ C
right✝ : #(C \ A) = n - 2 * r
⊢ False

Proof state:
case h.e'_4.h.e'_1
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) < #𝒜
this✝⁴ : Disjoint 𝒜 (∂ ^[n - 2 * r] 𝒜ᶜˢ)
this✝³ : r ≤ n
this✝² : 1 ≤ n
z : (n - 1).choose (n - r) < #𝒜ᶜˢ
h𝒜bar : Set.Sized (n - r) ↑𝒜ᶜˢ
this✝¹ : n - 2 * r ≤ n - r
kk : (n - 1).choose r ≤ #(∂ ^[n - 2 * r] 𝒜ᶜˢ)
this✝ : n - r - (n - 2 * r) = r
this : n.choose r < #(𝒜 ∪ ∂ ^[n - 2 * r] 𝒜ᶜˢ)
⊢ n = Fintype.card (Fin n)

Tactic:
rw [Fintype.card_fin]

Result:
no goals

Proof state:
case inr
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) < #𝒜
⊢ 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)

Result:
case inr
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) < #𝒜
this : Disjoint 𝒜 (∂ ^[n - 2 * r] 𝒜ᶜˢ)
⊢ False

Proof state:
case inr
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) < #𝒜
this✝⁴ : Disjoint 𝒜 (∂ ^[n - 2 * r] 𝒜ᶜˢ)
this✝³ : r ≤ n
this✝² : 1 ≤ n
z : (n - 1).choose (n - r) < #𝒜ᶜˢ
h𝒜bar : Set.Sized (n - r) ↑𝒜ᶜˢ
this✝¹ : n - 2 * r ≤ n - r
kk : (n - 1).choose r ≤ #(∂ ^[n - 2 * r] 𝒜ᶜˢ)
this✝ : n - r - (n - 2 * r) = r
this : n.choose r < #(𝒜 ∪ ∂ ^[n - 2 * r] 𝒜ᶜˢ)
⊢ False

Tactic:
apply this.not_le

Result:
case inr
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) < #𝒜
this✝⁴ : Disjoint 𝒜 (∂ ^[n - 2 * r] 𝒜ᶜˢ)
this✝³ : r ≤ n
this✝² : 1 ≤ n
z : (n - 1).choose (n - r) < #𝒜ᶜˢ
h𝒜bar : Set.Sized (n - r) ↑𝒜ᶜˢ
this✝¹ : n - 2 * r ≤ n - r
kk : (n - 1).choose r ≤ #(∂ ^[n - 2 * r] 𝒜ᶜˢ)
this✝ : n - r - (n - 2 * r) = r
this : n.choose r < #(𝒜 ∪ ∂ ^[n - 2 * r] 𝒜ᶜˢ)
⊢ #(𝒜 ∪ ∂ ^[n - 2 * r] 𝒜ᶜˢ) ≤ n.choose r

Proof state:
case inr
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) < #𝒜
this✝³ : Disjoint 𝒜 (∂ ^[n - 2 * r] 𝒜ᶜˢ)
this✝² : r ≤ n
this✝¹ : 1 ≤ n
z : (n - 1).choose (n - r) < #𝒜ᶜˢ
h𝒜bar : Set.Sized (n - r) ↑𝒜ᶜˢ
this✝ : n - 2 * r ≤ n - r
kk : (n - 1).choose r ≤ #(∂ ^[n - 2 * r] 𝒜ᶜˢ)
this : n - r - (n - 2 * r) = r
⊢ False

Tactic:
have : n.choose r < #(𝒜 ∪ ∂^[n - 2 * r] 𝒜ᶜˢ) := 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]

Result:
case inr
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) < #𝒜
this✝⁴ : Disjoint 𝒜 (∂ ^[n - 2 * r] 𝒜ᶜˢ)
this✝³ : r ≤ n
this✝² : 1 ≤ n
z : (n - 1).choose (n - r) < #𝒜ᶜˢ
h𝒜bar : Set.Sized (n - r) ↑𝒜ᶜˢ
this✝¹ : n - 2 * r ≤ n - r
kk : (n - 1).choose r ≤ #(∂ ^[n - 2 * r] 𝒜ᶜˢ)
this✝ : n - r - (n - 2 * r) = r
this : n.choose r < #(𝒜 ∪ ∂ ^[n - 2 * r] 𝒜ᶜˢ)
⊢ False

Proof state:
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) < #𝒜
this✝³ : Disjoint 𝒜 (∂ ^[n - 2 * r] 𝒜ᶜˢ)
this✝² : r ≤ n
this✝¹ : 1 ≤ n
z : (n - 1).choose (n - r) < #𝒜ᶜˢ
h𝒜bar : Set.Sized (n - r) ↑𝒜ᶜˢ
this✝ : n - 2 * r ≤ n - r
kk : (n - 1).choose r ≤ #(∂ ^[n - 2 * r] 𝒜ᶜˢ)
this : n - r - (n - 2 * r) = r
⊢ n.choose r < #𝒜 + #(∂ ^[n - 2 * r] 𝒜ᶜˢ)

Tactic:
convert lt_of_le_of_lt (add_le_add_left kk _) (add_lt_add_right size _) using 1

Result:
case h.e'_3
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) < #𝒜
this✝³ : Disjoint 𝒜 (∂ ^[n - 2 * r] 𝒜ᶜˢ)
this✝² : r ≤ n
this✝¹ : 1 ≤ n
z : (n - 1).choose (n - r) < #𝒜ᶜˢ
h𝒜bar : Set.Sized (n - r) ↑𝒜ᶜˢ
this✝ : n - 2 * r ≤ n - r
kk : (n - 1).choose r ≤ #(∂ ^[n - 2 * r] 𝒜ᶜˢ)
this : n - r - (n - 2 * r) = r
⊢ n.choose r = (n - 1).choose (r - 1) + (n - 1).choose r

Proof state:
case h.e'_3
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 = r

Tactic:
exact h₂ HA

Result:
no goals