-- Mathlib/Combinatorics/SetFamily/LYM.lean
theorem _root_.IsAntichain.sperner [Fintype α] {𝒜 : Finset (Finset α)}
    (h𝒜 : IsAntichain (· ⊆ ·) (𝒜 : Set (Finset α))) :
    #𝒜 ≤ (Fintype.card α).choose (Fintype.card α / 2)

Proof state:
α : Type u_2
inst✝ : Fintype α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun x1 x2 => x1 ⊆ x2) ↑𝒜
this : ↑(∑ x ∈ Iic (Fintype.card α), #(𝒜 # x)) / ↑((Fintype.card α).choose (Fintype.card α / 2)) ≤ 1
⊢ 0 < ↑((Fintype.card α).choose (Fintype.card α / 2))

Tactic:
simp only [cast_pos]

Result:
α : Type u_2
inst✝ : Fintype α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun x1 x2 => x1 ⊆ x2) ↑𝒜
this : ↑(∑ x ∈ Iic (Fintype.card α), #(𝒜 # x)) / ↑((Fintype.card α).choose (Fintype.card α / 2)) ≤ 1
⊢ 0 < (Fintype.card α).choose (Fintype.card α / 2)

Proof state:
α : Type u_2
inst✝ : Fintype α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun x1 x2 => x1 ⊆ x2) ↑𝒜
⊢ ∑ r ∈ Iic (Fintype.card α), ↑(#(𝒜 # r)) / ↑((Fintype.card α).choose (Fintype.card α / 2)) ≤ 1

Tactic:
rw [Iic_eq_Icc, ← Ico_succ_right, bot_eq_zero, Ico_zero_eq_range]

Result:
α : Type u_2
inst✝ : Fintype α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun x1 x2 => x1 ⊆ x2) ↑𝒜
⊢ ∑ r ∈ range (Fintype.card α).succ, ↑(#(𝒜 # r)) / ↑((Fintype.card α).choose (Fintype.card α / 2)) ≤ 1

Proof state:
α : Type u_2
inst✝ : Fintype α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun x1 x2 => x1 ⊆ x2) ↑𝒜
this : ∑ r ∈ Iic (Fintype.card α), ↑(#(𝒜 # r)) / ↑((Fintype.card α).choose (Fintype.card α / 2)) ≤ 1
⊢ #𝒜 ≤ (Fintype.card α).choose (Fintype.card α / 2)

Tactic:
rw [← sum_div, ← Nat.cast_sum, div_le_one] at this

Result:
α : Type u_2
inst✝ : Fintype α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun x1 x2 => x1 ⊆ x2) ↑𝒜
this : ↑(∑ x ∈ Iic (Fintype.card α), #(𝒜 # x)) ≤ ↑((Fintype.card α).choose (Fintype.card α / 2))
⊢ #𝒜 ≤ (Fintype.card α).choose (Fintype.card α / 2)

α : Type u_2
inst✝ : Fintype α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun x1 x2 => x1 ⊆ x2) ↑𝒜
this : ↑(∑ x ∈ Iic (Fintype.card α), #(𝒜 # x)) / ↑((Fintype.card α).choose (Fintype.card α / 2)) ≤ 1
⊢ 0 < ↑((Fintype.card α).choose (Fintype.card α / 2))

Proof state:
case refine_3
α : Type u_2
inst✝ : Fintype α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun x1 x2 => x1 ⊆ x2) ↑𝒜
r : ℕ
hr : r < (Fintype.card α).succ
⊢ (Fintype.card α).choose r ≤ (Fintype.card α).choose (Fintype.card α / 2)

Tactic:
exact choose_le_middle _ _

Result:
no goals

Proof state:
α : Type u_2
inst✝ : Fintype α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun x1 x2 => x1 ⊆ x2) ↑𝒜
r : ℕ
hr : r < (Fintype.card α).succ
⊢ ↑(#(𝒜 # r)) / ↑((Fintype.card α).choose (Fintype.card α / 2)) ≤ ↑(#(𝒜 # r)) / ↑((Fintype.card α).choose r)

Tactic:
refine div_le_div_of_nonneg_left ?_ ?_ ?_ <;> norm_cast

Result:
case refine_1
α : Type u_2
inst✝ : Fintype α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun x1 x2 => x1 ⊆ x2) ↑𝒜
r : ℕ
hr : r < (Fintype.card α).succ
⊢ 0 ≤ #(𝒜 # r)

case refine_2
α : Type u_2
inst✝ : Fintype α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun x1 x2 => x1 ⊆ x2) ↑𝒜
r : ℕ
hr : r < (Fintype.card α).succ
⊢ 0 < (Fintype.card α).choose r

case refine_3
α : Type u_2
inst✝ : Fintype α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun x1 x2 => x1 ⊆ x2) ↑𝒜
r : ℕ
hr : r < (Fintype.card α).succ
⊢ (Fintype.card α).choose r ≤ (Fintype.card α).choose (Fintype.card α / 2)

Proof state:
case refine_1
α : Type u_2
inst✝ : Fintype α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun x1 x2 => x1 ⊆ x2) ↑𝒜
r : ℕ
hr : r < (Fintype.card α).succ
⊢ 0 ≤ #(𝒜 # r)

Tactic:
exact Nat.zero_le _

Result:
no goals

Proof state:
α : Type u_2
inst✝ : Fintype α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun x1 x2 => x1 ⊆ x2) ↑𝒜
this : ↑(∑ x ∈ Iic (Fintype.card α), #(𝒜 # x)) ≤ ↑((Fintype.card α).choose (Fintype.card α / 2))
⊢ #𝒜 ≤ (Fintype.card α).choose (Fintype.card α / 2)

Tactic:
simp only [cast_le] at this

Result:
α : Type u_2
inst✝ : Fintype α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun x1 x2 => x1 ⊆ x2) ↑𝒜
this : ∑ x ∈ Iic (Fintype.card α), #(𝒜 # x) ≤ (Fintype.card α).choose (Fintype.card α / 2)
⊢ #𝒜 ≤ (Fintype.card α).choose (Fintype.card α / 2)

Proof state:
α : Type u_2
inst✝ : Fintype α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun x1 x2 => x1 ⊆ x2) ↑𝒜
this : ∑ x ∈ Iic (Fintype.card α), #(𝒜 # x) ≤ (Fintype.card α).choose (Fintype.card α / 2)
⊢ #𝒜 ≤ (Fintype.card α).choose (Fintype.card α / 2)

Tactic:
rwa [sum_card_slice] at this

Result:
no goals

Proof state:
case refine_2
α : Type u_2
inst✝ : Fintype α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun x1 x2 => x1 ⊆ x2) ↑𝒜
r : ℕ
hr : r < (Fintype.card α).succ
⊢ 0 < (Fintype.card α).choose r

Tactic:
exact choose_pos (Nat.lt_succ_iff.1 hr)

Result:
no goals

Proof state:
α : Type u_2
inst✝ : Fintype α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun x1 x2 => x1 ⊆ x2) ↑𝒜
r : ℕ
hr : r ∈ range (Fintype.card α).succ
⊢ ↑(#(𝒜 # r)) / ↑((Fintype.card α).choose (Fintype.card α / 2)) ≤ ↑(#(𝒜 # r)) / ↑((Fintype.card α).choose r)

Tactic:
rw [mem_range] at hr

Result:
α : Type u_2
inst✝ : Fintype α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun x1 x2 => x1 ⊆ x2) ↑𝒜
r : ℕ
hr : r < (Fintype.card α).succ
⊢ ↑(#(𝒜 # r)) / ↑((Fintype.card α).choose (Fintype.card α / 2)) ≤ ↑(#(𝒜 # r)) / ↑((Fintype.card α).choose r)

Proof state:
α : Type u_2
inst✝ : Fintype α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun x1 x2 => x1 ⊆ x2) ↑𝒜
⊢ ∑ r ∈ range (Fintype.card α).succ, ↑(#(𝒜 # r)) / ↑((Fintype.card α).choose (Fintype.card α / 2)) ≤ 1

Tactic:
refine (sum_le_sum fun r hr => ?_).trans (sum_card_slice_div_choose_le_one h𝒜)

Result:
α : Type u_2
inst✝ : Fintype α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun x1 x2 => x1 ⊆ x2) ↑𝒜
r : ℕ
hr : r ∈ range (Fintype.card α).succ
⊢ ↑(#(𝒜 # r)) / ↑((Fintype.card α).choose (Fintype.card α / 2)) ≤ ↑(#(𝒜 # r)) / ↑((Fintype.card α).choose r)

Proof state:
α : Type u_2
inst✝ : Fintype α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun x1 x2 => x1 ⊆ x2) ↑𝒜
this : ↑(∑ x ∈ Iic (Fintype.card α), #(𝒜 # x)) / ↑((Fintype.card α).choose (Fintype.card α / 2)) ≤ 1
⊢ 0 < (Fintype.card α).choose (Fintype.card α / 2)

Tactic:
exact choose_pos (Nat.div_le_self _ _)

Result:
no goals