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

Tactic:
have : n - r - (n - 2 * r) = r := by omega

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

Proof state:
case h.e'_2
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] 𝒜ᶜˢ)
⊢ r = n - r - (n - 2 * r)

Tactic:
omega

Result:
no goals

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
⊢ #𝒜 = 0

Tactic:
rw [Finset.card_eq_zero, eq_empty_iff_forall_not_mem]

Result:
case h.e'_3
n : ℕ
𝒜 : Finset (Finset (Fin n))
r : ℕ
h𝒜 : (↑𝒜).Intersecting
h₂ : Set.Sized r ↑𝒜
h₃ : r ≤ n / 2
b : r = 0
⊢ ∀ (x : Finset (Fin n)), x ∉ 𝒜

Proof state:
case inr
n : ℕ
𝒜 : Finset (Finset (Fin n))
r : ℕ
h𝒜 : (↑𝒜).Intersecting
h₂ : Set.Sized r ↑𝒜
h₃ : r ≤ n / 2
h1r : r > 0
⊢ #𝒜 ≤ (n - 1).choose (r - 1)

Tactic:
refine le_of_not_lt fun size ↦ ?_

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) < #𝒜
⊢ 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
⊢ (n - 1).choose (n - r) < #𝒜ᶜˢ

Tactic:
rwa [card_compls, choose_symm_of_eq_add (tsub_add_tsub_cancel ‹r ≤ n› ‹1 ≤ r›).symm]

Result:
no goals

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) ↑𝒜ᶜˢ
⊢ r ≤ 2 * r

Tactic:
exact Nat.le_mul_of_pos_left _ zero_lt_two

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
⊢ False

Tactic:
have z : (n - 1).choose (n - r) < #𝒜ᶜˢ := by
  rwa [card_compls, choose_symm_of_eq_add (tsub_add_tsub_cancel ‹r ≤ n› ‹1 ≤ r›).symm]

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) < #𝒜ᶜˢ
⊢ False

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 ∈ 𝒜
⊢ Disjoint A A

Tactic:
rw [disjoint_self_iff_empty, ← Finset.card_eq_zero, ← b]

Result:
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

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

Tactic:
refine ⟨‹_›, ?_⟩

Result:
case inr.convert_5
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] 𝒜ᶜˢ)
⊢ Set.Sized 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] 𝒜ᶜˢ)
this✝ : r ≤ n
this : 1 ≤ n
z : (n - 1).choose (n - r) < #𝒜ᶜˢ
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

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
⊢ False

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

Tactic:
rw [coe_union, Set.sized_union]

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

Tactic:
have kk := kruskal_katona_lovasz_form ‹n - 2 * r ≤ n - r› ((tsub_le_tsub_iff_left ‹1 ≤ n›).2 h1r)
    tsub_le_self h𝒜bar z.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 (n - r - (n - 2 * r)) ≤ #(∂ ^[n - 2 * r] 𝒜ᶜˢ)
⊢ False