𝕜 : Type ?u.33953
α : Type u_1
inst✝¹ : LinearOrderedField 𝕜
inst✝ : Fintype α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun x x_1 => x ⊆ x_1) ↑𝒜
⊢ ∑ r in Iic (Fintype.card α), ↑(card (𝒜 # r)) / ↑(Nat.choose (Fintype.card α) (Fintype.card α / 2)) ≤ 1
𝕜 : Type ?u.33953
α : Type u_1
inst✝¹ : LinearOrderedField 𝕜
inst✝ : Fintype α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun x x_1 => x ⊆ x_1) ↑𝒜
⊢ card 𝒜 ≤ Nat.choose (Fintype.card α) (Fintype.card α / 2)
suffices (∑ r in Iic (Fintype.card α),
    ((𝒜 # r).card : ℚ) / (Fintype.card α).choose (Fintype.card α / 2)) ≤ 1 by
  rw [← sum_div, ← Nat.cast_sum, div_le_one] at this
  simp only [cast_le] at this
  rwa [sum_card_slice] at this
  simp only [cast_pos]
  exact choose_pos (Nat.div_le_self _ _)
𝕜 : Type ?u.33953
α : Type u_1
inst✝¹ : LinearOrderedField 𝕜
inst✝ : Fintype α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun x x_1 => x ⊆ x_1) ↑𝒜
⊢ ∑ r in range (succ (Fintype.card α)), ↑(card (𝒜 # r)) / ↑(Nat.choose (Fintype.card α) (Fintype.card α / 2)) ≤ 1
𝕜 : Type ?u.33953
α : Type u_1
inst✝¹ : LinearOrderedField 𝕜
inst✝ : Fintype α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun x x_1 => x ⊆ x_1) ↑𝒜
⊢ ∑ r in Iic (Fintype.card α), ↑(card (𝒜 # r)) / ↑(Nat.choose (Fintype.card α) (Fintype.card α / 2)) ≤ 1
rw [Iic_eq_Icc, ← Ico_succ_right, bot_eq_zero, Ico_zero_eq_range]
𝕜 : Type ?u.33953
α : Type u_1
inst✝¹ : LinearOrderedField 𝕜
inst✝ : Fintype α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun x x_1 => x ⊆ x_1) ↑𝒜
r : ℕ
hr : r ∈ range (succ (Fintype.card α))
⊢ ↑(card (𝒜 # r)) / ↑(Nat.choose (Fintype.card α) (Fintype.card α / 2)) ≤
    ↑(card (𝒜 # r)) / ↑(Nat.choose (Fintype.card α) r)
𝕜 : Type ?u.33953
α : Type u_1
inst✝¹ : LinearOrderedField 𝕜
inst✝ : Fintype α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun x x_1 => x ⊆ x_1) ↑𝒜
⊢ ∑ r in range (succ (Fintype.card α)), ↑(card (𝒜 # r)) / ↑(Nat.choose (Fintype.card α) (Fintype.card α / 2)) ≤ 1
refine' (sum_le_sum fun r hr => _).trans (sum_card_slice_div_choose_le_one h𝒜)
𝕜 : Type ?u.33953
α : Type u_1
inst✝¹ : LinearOrderedField 𝕜
inst✝ : Fintype α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun x x_1 => x ⊆ x_1) ↑𝒜
r : ℕ
hr : r < succ (Fintype.card α)
⊢ ↑(card (𝒜 # r)) / ↑(Nat.choose (Fintype.card α) (Fintype.card α / 2)) ≤
    ↑(card (𝒜 # r)) / ↑(Nat.choose (Fintype.card α) r)
𝕜 : Type ?u.33953
α : Type u_1
inst✝¹ : LinearOrderedField 𝕜
inst✝ : Fintype α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun x x_1 => x ⊆ x_1) ↑𝒜
r : ℕ
hr : r ∈ range (succ (Fintype.card α))
⊢ ↑(card (𝒜 # r)) / ↑(Nat.choose (Fintype.card α) (Fintype.card α / 2)) ≤
    ↑(card (𝒜 # r)) / ↑(Nat.choose (Fintype.card α) r)
rw [mem_range] at hr
case refine'_1
𝕜 : Type ?u.33953
α : Type u_1
inst✝¹ : LinearOrderedField 𝕜
inst✝ : Fintype α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun x x_1 => x ⊆ x_1) ↑𝒜
r : ℕ
hr : r < succ (Fintype.card α)
⊢ 0 ≤ card (𝒜 # r)

case refine'_2
𝕜 : Type ?u.33953
α : Type u_1
inst✝¹ : LinearOrderedField 𝕜
inst✝ : Fintype α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun x x_1 => x ⊆ x_1) ↑𝒜
r : ℕ
hr : r < succ (Fintype.card α)
⊢ 0 < Nat.choose (Fintype.card α) r

case refine'_3
𝕜 : Type ?u.33953
α : Type u_1
inst✝¹ : LinearOrderedField 𝕜
inst✝ : Fintype α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun x x_1 => x ⊆ x_1) ↑𝒜
r : ℕ
hr : r < succ (Fintype.card α)
⊢ Nat.choose (Fintype.card α) r ≤ Nat.choose (Fintype.card α) (Fintype.card α / 2)
𝕜 : Type ?u.33953
α : Type u_1
inst✝¹ : LinearOrderedField 𝕜
inst✝ : Fintype α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun x x_1 => x ⊆ x_1) ↑𝒜
r : ℕ
hr : r < succ (Fintype.card α)
⊢ ↑(card (𝒜 # r)) / ↑(Nat.choose (Fintype.card α) (Fintype.card α / 2)) ≤
    ↑(card (𝒜 # r)) / ↑(Nat.choose (Fintype.card α) r)
refine' div_le_div_of_le_left _ _ _ <;> norm_cast
𝕜 : Type ?u.33953
α : Type u_1
inst✝¹ : LinearOrderedField 𝕜
inst✝ : Fintype α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun x x_1 => x ⊆ x_1) ↑𝒜
this : ↑(∑ x in Iic (Fintype.card α), card (𝒜 # x)) ≤ ↑(Nat.choose (Fintype.card α) (Fintype.card α / 2))
⊢ card 𝒜 ≤ Nat.choose (Fintype.card α) (Fintype.card α / 2)

𝕜 : Type ?u.33953
α : Type u_1
inst✝¹ : LinearOrderedField 𝕜
inst✝ : Fintype α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun x x_1 => x ⊆ x_1) ↑𝒜
this : ↑(∑ x in Iic (Fintype.card α), card (𝒜 # x)) / ↑(Nat.choose (Fintype.card α) (Fintype.card α / 2)) ≤ 1
⊢ 0 < ↑(Nat.choose (Fintype.card α) (Fintype.card α / 2))
𝕜 : Type ?u.33953
α : Type u_1
inst✝¹ : LinearOrderedField 𝕜
inst✝ : Fintype α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun x x_1 => x ⊆ x_1) ↑𝒜
this : ∑ r in Iic (Fintype.card α), ↑(card (𝒜 # r)) / ↑(Nat.choose (Fintype.card α) (Fintype.card α / 2)) ≤ 1
⊢ card 𝒜 ≤ Nat.choose (Fintype.card α) (Fintype.card α / 2)
rw [← sum_div, ← Nat.cast_sum, div_le_one] at this
𝕜 : Type ?u.33953
α : Type u_1
inst✝¹ : LinearOrderedField 𝕜
inst✝ : Fintype α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun x x_1 => x ⊆ x_1) ↑𝒜
this : ∑ x in Iic (Fintype.card α), card (𝒜 # x) ≤ Nat.choose (Fintype.card α) (Fintype.card α / 2)
⊢ card 𝒜 ≤ Nat.choose (Fintype.card α) (Fintype.card α / 2)

𝕜 : Type ?u.33953
α : Type u_1
inst✝¹ : LinearOrderedField 𝕜
inst✝ : Fintype α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun x x_1 => x ⊆ x_1) ↑𝒜
this : ↑(∑ x in Iic (Fintype.card α), card (𝒜 # x)) / ↑(Nat.choose (Fintype.card α) (Fintype.card α / 2)) ≤ 1
⊢ 0 < ↑(Nat.choose (Fintype.card α) (Fintype.card α / 2))
𝕜 : Type ?u.33953
α : Type u_1
inst✝¹ : LinearOrderedField 𝕜
inst✝ : Fintype α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun x x_1 => x ⊆ x_1) ↑𝒜
this : ↑(∑ x in Iic (Fintype.card α), card (𝒜 # x)) ≤ ↑(Nat.choose (Fintype.card α) (Fintype.card α / 2))
⊢ card 𝒜 ≤ Nat.choose (Fintype.card α) (Fintype.card α / 2)

𝕜 : Type ?u.33953
α : Type u_1
inst✝¹ : LinearOrderedField 𝕜
inst✝ : Fintype α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun x x_1 => x ⊆ x_1) ↑𝒜
this : ↑(∑ x in Iic (Fintype.card α), card (𝒜 # x)) / ↑(Nat.choose (Fintype.card α) (Fintype.card α / 2)) ≤ 1
⊢ 0 < ↑(Nat.choose (Fintype.card α) (Fintype.card α / 2))
simp only [cast_le] at this
𝕜 : Type ?u.33953
α : Type u_1
inst✝¹ : LinearOrderedField 𝕜
inst✝ : Fintype α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun x x_1 => x ⊆ x_1) ↑𝒜
this : ↑(∑ x in Iic (Fintype.card α), card (𝒜 # x)) / ↑(Nat.choose (Fintype.card α) (Fintype.card α / 2)) ≤ 1
⊢ 0 < ↑(Nat.choose (Fintype.card α) (Fintype.card α / 2))
𝕜 : Type ?u.33953
α : Type u_1
inst✝¹ : LinearOrderedField 𝕜
inst✝ : Fintype α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun x x_1 => x ⊆ x_1) ↑𝒜
this : ∑ x in Iic (Fintype.card α), card (𝒜 # x) ≤ Nat.choose (Fintype.card α) (Fintype.card α / 2)
⊢ card 𝒜 ≤ Nat.choose (Fintype.card α) (Fintype.card α / 2)

𝕜 : Type ?u.33953
α : Type u_1
inst✝¹ : LinearOrderedField 𝕜
inst✝ : Fintype α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun x x_1 => x ⊆ x_1) ↑𝒜
this : ↑(∑ x in Iic (Fintype.card α), card (𝒜 # x)) / ↑(Nat.choose (Fintype.card α) (Fintype.card α / 2)) ≤ 1
⊢ 0 < ↑(Nat.choose (Fintype.card α) (Fintype.card α / 2))
rwa [sum_card_slice] at this
𝕜 : Type ?u.33953
α : Type u_1
inst✝¹ : LinearOrderedField 𝕜
inst✝ : Fintype α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun x x_1 => x ⊆ x_1) ↑𝒜
this : ↑(∑ x in Iic (Fintype.card α), card (𝒜 # x)) / ↑(Nat.choose (Fintype.card α) (Fintype.card α / 2)) ≤ 1
⊢ 0 < Nat.choose (Fintype.card α) (Fintype.card α / 2)
𝕜 : Type ?u.33953
α : Type u_1
inst✝¹ : LinearOrderedField 𝕜
inst✝ : Fintype α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun x x_1 => x ⊆ x_1) ↑𝒜
this : ↑(∑ x in Iic (Fintype.card α), card (𝒜 # x)) / ↑(Nat.choose (Fintype.card α) (Fintype.card α / 2)) ≤ 1
⊢ 0 < ↑(Nat.choose (Fintype.card α) (Fintype.card α / 2))
simp only [cast_pos]
no goals
𝕜 : Type ?u.33953
α : Type u_1
inst✝¹ : LinearOrderedField 𝕜
inst✝ : Fintype α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun x x_1 => x ⊆ x_1) ↑𝒜
this : ↑(∑ x in Iic (Fintype.card α), card (𝒜 # x)) / ↑(Nat.choose (Fintype.card α) (Fintype.card α / 2)) ≤ 1
⊢ 0 < Nat.choose (Fintype.card α) (Fintype.card α / 2)
exact choose_pos (Nat.div_le_self _ _)
no goals
case refine'_1
𝕜 : Type ?u.33953
α : Type u_1
inst✝¹ : LinearOrderedField 𝕜
inst✝ : Fintype α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun x x_1 => x ⊆ x_1) ↑𝒜
r : ℕ
hr : r < succ (Fintype.card α)
⊢ 0 ≤ card (𝒜 # r)
exact Nat.zero_le _
no goals
case refine'_2
𝕜 : Type ?u.33953
α : Type u_1
inst✝¹ : LinearOrderedField 𝕜
inst✝ : Fintype α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun x x_1 => x ⊆ x_1) ↑𝒜
r : ℕ
hr : r < succ (Fintype.card α)
⊢ 0 < Nat.choose (Fintype.card α) r
exact choose_pos (lt_succ_iff.1 hr)
no goals
case refine'_3
𝕜 : Type ?u.33953
α : Type u_1
inst✝¹ : LinearOrderedField 𝕜
inst✝ : Fintype α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun x x_1 => x ⊆ x_1) ↑𝒜
r : ℕ
hr : r < succ (Fintype.card α)
⊢ Nat.choose (Fintype.card α) r ≤ Nat.choose (Fintype.card α) (Fintype.card α / 2)
exact choose_le_middle _ _