𝕜 : Type u_2
α : Type u_1
inst✝¹ : LinearOrderedField 𝕜
𝒜 : Finset (Finset α)
s : Finset α
k : ℕ
inst✝ : Fintype α
h𝒜 : IsAntichain (fun x x_1 => x ⊆ x_1) ↑𝒜
⊢ ∑ r in range (Fintype.card α + 1),
      ↑(card (𝒜 # (Fintype.card α - r))) / ↑(Nat.choose (Fintype.card α) (Fintype.card α - r)) ≤
    1
𝕜 : Type u_2
α : Type u_1
inst✝¹ : LinearOrderedField 𝕜
𝒜 : Finset (Finset α)
s : Finset α
k : ℕ
inst✝ : Fintype α
h𝒜 : IsAntichain (fun x x_1 => x ⊆ x_1) ↑𝒜
⊢ ∑ r in range (Fintype.card α + 1), ↑(card (𝒜 # r)) / ↑(Nat.choose (Fintype.card α) r) ≤ 1
rw [← sum_flip]
𝕜 : Type u_2
α : Type u_1
inst✝¹ : LinearOrderedField 𝕜
𝒜 : Finset (Finset α)
s : Finset α
k : ℕ
inst✝ : Fintype α
h𝒜 : IsAntichain (fun x x_1 => x ⊆ x_1) ↑𝒜
⊢ ↑(card (falling (Fintype.card α - Fintype.card α) 𝒜)) /
      ↑(Nat.choose (Fintype.card α) (Fintype.card α - Fintype.card α)) ≤
    1
𝕜 : Type u_2
α : Type u_1
inst✝¹ : LinearOrderedField 𝕜
𝒜 : Finset (Finset α)
s : Finset α
k : ℕ
inst✝ : Fintype α
h𝒜 : IsAntichain (fun x x_1 => x ⊆ x_1) ↑𝒜
⊢ ∑ r in range (Fintype.card α + 1),
      ↑(card (𝒜 # (Fintype.card α - r))) / ↑(Nat.choose (Fintype.card α) (Fintype.card α - r)) ≤
    1
refine' (le_card_falling_div_choose le_rfl h𝒜).trans _
𝕜 : Type u_2
α : Type u_1
inst✝¹ : LinearOrderedField 𝕜
𝒜 : Finset (Finset α)
s : Finset α
k : ℕ
inst✝ : Fintype α
h𝒜 : IsAntichain (fun x x_1 => x ⊆ x_1) ↑𝒜
⊢ card (falling (Fintype.card α - Fintype.card α) 𝒜) ≤ 1 * Nat.choose (Fintype.card α) (Fintype.card α - Fintype.card α)

𝕜 : Type u_2
α : Type u_1
inst✝¹ : LinearOrderedField 𝕜
𝒜 : Finset (Finset α)
s : Finset α
k : ℕ
inst✝ : Fintype α
h𝒜 : IsAntichain (fun x x_1 => x ⊆ x_1) ↑𝒜
⊢ 0 < Nat.choose (Fintype.card α) (Fintype.card α - Fintype.card α)
𝕜 : Type u_2
α : Type u_1
inst✝¹ : LinearOrderedField 𝕜
𝒜 : Finset (Finset α)
s : Finset α
k : ℕ
inst✝ : Fintype α
h𝒜 : IsAntichain (fun x x_1 => x ⊆ x_1) ↑𝒜
⊢ ↑(card (falling (Fintype.card α - Fintype.card α) 𝒜)) /
      ↑(Nat.choose (Fintype.card α) (Fintype.card α - Fintype.card α)) ≤
    1
rw [div_le_iff] <;> norm_cast
no goals
𝕜 : Type u_2
α : Type u_1
inst✝¹ : LinearOrderedField 𝕜
𝒜 : Finset (Finset α)
s : Finset α
k : ℕ
inst✝ : Fintype α
h𝒜 : IsAntichain (fun x x_1 => x ⊆ x_1) ↑𝒜
⊢ card (falling (Fintype.card α - Fintype.card α) 𝒜) ≤ 1 * Nat.choose (Fintype.card α) (Fintype.card α - Fintype.card α)
simpa only [Nat.sub_self, one_mul, Nat.choose_zero_right, falling] using
  Set.Sized.card_le (sized_falling 0 𝒜)
𝕜 : Type u_2
α : Type u_1
inst✝¹ : LinearOrderedField 𝕜
𝒜 : Finset (Finset α)
s : Finset α
k : ℕ
inst✝ : Fintype α
h𝒜 : IsAntichain (fun x x_1 => x ⊆ x_1) ↑𝒜
⊢ 0 < 1
𝕜 : Type u_2
α : Type u_1
inst✝¹ : LinearOrderedField 𝕜
𝒜 : Finset (Finset α)
s : Finset α
k : ℕ
inst✝ : Fintype α
h𝒜 : IsAntichain (fun x x_1 => x ⊆ x_1) ↑𝒜
⊢ 0 < Nat.choose (Fintype.card α) (Fintype.card α - Fintype.card α)
rw [tsub_self, choose_zero_right]
no goals
𝕜 : Type u_2
α : Type u_1
inst✝¹ : LinearOrderedField 𝕜
𝒜 : Finset (Finset α)
s : Finset α
k : ℕ
inst✝ : Fintype α
h𝒜 : IsAntichain (fun x x_1 => x ⊆ x_1) ↑𝒜
⊢ 0 < 1
exact zero_lt_one