case zero
𝕜 : Type u_2
α : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s : Finset α
inst✝ : Fintype α
hk✝ : k ≤ Fintype.card α
h𝒜 : IsAntichain (fun x x_1 => x ⊆ x_1) ↑𝒜
hk : zero ≤ Fintype.card α
⊢ ∑ r in range (zero + 1), ↑(card (𝒜 # (Fintype.card α - r))) / ↑(Nat.choose (Fintype.card α) (Fintype.card α - r)) ≤
    ↑(card (falling (Fintype.card α - zero) 𝒜)) / ↑(Nat.choose (Fintype.card α) (Fintype.card α - zero))

case succ
𝕜 : Type u_2
α : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
k✝ : ℕ
𝒜 : Finset (Finset α)
s : Finset α
inst✝ : Fintype α
hk✝ : k✝ ≤ Fintype.card α
h𝒜 : IsAntichain (fun x x_1 => x ⊆ x_1) ↑𝒜
k : ℕ
ih :
  k ≤ Fintype.card α →
    ∑ r in range (k + 1), ↑(card (𝒜 # (Fintype.card α - r))) / ↑(Nat.choose (Fintype.card α) (Fintype.card α - r)) ≤
      ↑(card (falling (Fintype.card α - k) 𝒜)) / ↑(Nat.choose (Fintype.card α) (Fintype.card α - k))
hk : succ k ≤ Fintype.card α
⊢ ∑ r in range (succ k + 1), ↑(card (𝒜 # (Fintype.card α - r))) / ↑(Nat.choose (Fintype.card α) (Fintype.card α - r)) ≤
    ↑(card (falling (Fintype.card α - succ k) 𝒜)) / ↑(Nat.choose (Fintype.card α) (Fintype.card α - succ k))
𝕜 : Type u_2
α : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s : Finset α
inst✝ : Fintype α
hk : k ≤ Fintype.card α
h𝒜 : IsAntichain (fun x x_1 => x ⊆ x_1) ↑𝒜
⊢ ∑ r in range (k + 1), ↑(card (𝒜 # (Fintype.card α - r))) / ↑(Nat.choose (Fintype.card α) (Fintype.card α - r)) ≤
    ↑(card (falling (Fintype.card α - k) 𝒜)) / ↑(Nat.choose (Fintype.card α) (Fintype.card α - k))
induction' k with k ih
case succ
𝕜 : Type u_2
α : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
k✝ : ℕ
𝒜 : Finset (Finset α)
s : Finset α
inst✝ : Fintype α
hk✝ : k✝ ≤ Fintype.card α
h𝒜 : IsAntichain (fun x x_1 => x ⊆ x_1) ↑𝒜
k : ℕ
ih :
  k ≤ Fintype.card α →
    ∑ r in range (k + 1), ↑(card (𝒜 # (Fintype.card α - r))) / ↑(Nat.choose (Fintype.card α) (Fintype.card α - r)) ≤
      ↑(card (falling (Fintype.card α - k) 𝒜)) / ↑(Nat.choose (Fintype.card α) (Fintype.card α - k))
hk : k + 1 ≤ Fintype.card α
⊢ ∑ r in range (k + 1 + 1), ↑(card (𝒜 # (Fintype.card α - r))) / ↑(Nat.choose (Fintype.card α) (Fintype.card α - r)) ≤
    ↑(card (falling (Fintype.card α - (k + 1)) 𝒜)) / ↑(Nat.choose (Fintype.card α) (Fintype.card α - (k + 1)))
case succ
𝕜 : Type u_2
α : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
k✝ : ℕ
𝒜 : Finset (Finset α)
s : Finset α
inst✝ : Fintype α
hk✝ : k✝ ≤ Fintype.card α
h𝒜 : IsAntichain (fun x x_1 => x ⊆ x_1) ↑𝒜
k : ℕ
ih :
  k ≤ Fintype.card α →
    ∑ r in range (k + 1), ↑(card (𝒜 # (Fintype.card α - r))) / ↑(Nat.choose (Fintype.card α) (Fintype.card α - r)) ≤
      ↑(card (falling (Fintype.card α - k) 𝒜)) / ↑(Nat.choose (Fintype.card α) (Fintype.card α - k))
hk : succ k ≤ Fintype.card α
⊢ ∑ r in range (succ k + 1), ↑(card (𝒜 # (Fintype.card α - r))) / ↑(Nat.choose (Fintype.card α) (Fintype.card α - r)) ≤
    ↑(card (falling (Fintype.card α - succ k) 𝒜)) / ↑(Nat.choose (Fintype.card α) (Fintype.card α - succ k))
rw [succ_eq_add_one] at *
case succ
𝕜 : Type u_2
α : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
k✝ : ℕ
𝒜 : Finset (Finset α)
s : Finset α
inst✝ : Fintype α
hk✝ : k✝ ≤ Fintype.card α
h𝒜 : IsAntichain (fun x x_1 => x ⊆ x_1) ↑𝒜
k : ℕ
ih :
  k ≤ Fintype.card α →
    ∑ r in range (k + 1), ↑(card (𝒜 # (Fintype.card α - r))) / ↑(Nat.choose (Fintype.card α) (Fintype.card α - r)) ≤
      ↑(card (falling (Fintype.card α - k) 𝒜)) / ↑(Nat.choose (Fintype.card α) (Fintype.card α - k))
hk : k + 1 ≤ Fintype.card α
⊢ ↑(card (𝒜 # (Fintype.card α - (k + 1)))) / ↑(Nat.choose (Fintype.card α) (Fintype.card α - (k + 1))) +
      ∑ x in range (k + 1), ↑(card (𝒜 # (Fintype.card α - x))) / ↑(Nat.choose (Fintype.card α) (Fintype.card α - x)) ≤
    ↑(card (𝒜 # (Fintype.card α - (k + 1)))) / ↑(Nat.choose (Fintype.card α) (Fintype.card α - (k + 1))) +
      ↑(card ((∂ ) (falling (Fintype.card α - (k + 1) + 1) 𝒜))) /
        ↑(Nat.choose (Fintype.card α) (Fintype.card α - (k + 1)))
case succ
𝕜 : Type u_2
α : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
k✝ : ℕ
𝒜 : Finset (Finset α)
s : Finset α
inst✝ : Fintype α
hk✝ : k✝ ≤ Fintype.card α
h𝒜 : IsAntichain (fun x x_1 => x ⊆ x_1) ↑𝒜
k : ℕ
ih :
  k ≤ Fintype.card α →
    ∑ r in range (k + 1), ↑(card (𝒜 # (Fintype.card α - r))) / ↑(Nat.choose (Fintype.card α) (Fintype.card α - r)) ≤
      ↑(card (falling (Fintype.card α - k) 𝒜)) / ↑(Nat.choose (Fintype.card α) (Fintype.card α - k))
hk : k + 1 ≤ Fintype.card α
⊢ ∑ r in range (k + 1 + 1), ↑(card (𝒜 # (Fintype.card α - r))) / ↑(Nat.choose (Fintype.card α) (Fintype.card α - r)) ≤
    ↑(card (falling (Fintype.card α - (k + 1)) 𝒜)) / ↑(Nat.choose (Fintype.card α) (Fintype.card α - (k + 1)))
rw [sum_range_succ, ← slice_union_shadow_falling_succ,
  card_disjoint_union (IsAntichain.disjoint_slice_shadow_falling h𝒜), cast_add, _root_.add_div,
  add_comm]
case succ
𝕜 : Type u_2
α : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
k✝ : ℕ
𝒜 : Finset (Finset α)
s : Finset α
inst✝ : Fintype α
hk✝ : k✝ ≤ Fintype.card α
h𝒜 : IsAntichain (fun x x_1 => x ⊆ x_1) ↑𝒜
k : ℕ
ih :
  k ≤ Fintype.card α →
    ∑ r in range (k + 1), ↑(card (𝒜 # (Fintype.card α - r))) / ↑(Nat.choose (Fintype.card α) (Fintype.card α - r)) ≤
      ↑(card (falling (Fintype.card α - k) 𝒜)) / ↑(Nat.choose (Fintype.card α) (Fintype.card α - k))
hk : k + 1 ≤ Fintype.card α
⊢ ↑(card (𝒜 # (Fintype.card α - k - 1))) / ↑(Nat.choose (Fintype.card α) (Fintype.card α - k - 1)) +
      ∑ x in range (k + 1), ↑(card (𝒜 # (Fintype.card α - x))) / ↑(Nat.choose (Fintype.card α) (Fintype.card α - x)) ≤
    ↑(card (𝒜 # (Fintype.card α - k - 1))) / ↑(Nat.choose (Fintype.card α) (Fintype.card α - k - 1)) +
      ↑(card ((∂ ) (falling (Fintype.card α - k) 𝒜))) / ↑(Nat.choose (Fintype.card α) (Fintype.card α - k - 1))
case succ
𝕜 : Type u_2
α : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
k✝ : ℕ
𝒜 : Finset (Finset α)
s : Finset α
inst✝ : Fintype α
hk✝ : k✝ ≤ Fintype.card α
h𝒜 : IsAntichain (fun x x_1 => x ⊆ x_1) ↑𝒜
k : ℕ
ih :
  k ≤ Fintype.card α →
    ∑ r in range (k + 1), ↑(card (𝒜 # (Fintype.card α - r))) / ↑(Nat.choose (Fintype.card α) (Fintype.card α - r)) ≤
      ↑(card (falling (Fintype.card α - k) 𝒜)) / ↑(Nat.choose (Fintype.card α) (Fintype.card α - k))
hk : k + 1 ≤ Fintype.card α
⊢ ↑(card (𝒜 # (Fintype.card α - (k + 1)))) / ↑(Nat.choose (Fintype.card α) (Fintype.card α - (k + 1))) +
      ∑ x in range (k + 1), ↑(card (𝒜 # (Fintype.card α - x))) / ↑(Nat.choose (Fintype.card α) (Fintype.card α - x)) ≤
    ↑(card (𝒜 # (Fintype.card α - (k + 1)))) / ↑(Nat.choose (Fintype.card α) (Fintype.card α - (k + 1))) +
      ↑(card ((∂ ) (falling (Fintype.card α - (k + 1) + 1) 𝒜))) /
        ↑(Nat.choose (Fintype.card α) (Fintype.card α - (k + 1)))
rw [← tsub_tsub, tsub_add_cancel_of_le (le_tsub_of_add_le_left hk)]
no goals
case succ
𝕜 : Type u_2
α : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
k✝ : ℕ
𝒜 : Finset (Finset α)
s : Finset α
inst✝ : Fintype α
hk✝ : k✝ ≤ Fintype.card α
h𝒜 : IsAntichain (fun x x_1 => x ⊆ x_1) ↑𝒜
k : ℕ
ih :
  k ≤ Fintype.card α →
    ∑ r in range (k + 1), ↑(card (𝒜 # (Fintype.card α - r))) / ↑(Nat.choose (Fintype.card α) (Fintype.card α - r)) ≤
      ↑(card (falling (Fintype.card α - k) 𝒜)) / ↑(Nat.choose (Fintype.card α) (Fintype.card α - k))
hk : k + 1 ≤ Fintype.card α
⊢ ↑(card (𝒜 # (Fintype.card α - k - 1))) / ↑(Nat.choose (Fintype.card α) (Fintype.card α - k - 1)) +
      ∑ x in range (k + 1), ↑(card (𝒜 # (Fintype.card α - x))) / ↑(Nat.choose (Fintype.card α) (Fintype.card α - x)) ≤
    ↑(card (𝒜 # (Fintype.card α - k - 1))) / ↑(Nat.choose (Fintype.card α) (Fintype.card α - k - 1)) +
      ↑(card ((∂ ) (falling (Fintype.card α - k) 𝒜))) / ↑(Nat.choose (Fintype.card α) (Fintype.card α - k - 1))
exact
  add_le_add_left
    ((ih <| le_of_succ_le hk).trans <|
      card_div_choose_le_card_shadow_div_choose (tsub_pos_iff_lt.2 <| Nat.succ_le_iff.1 hk).ne' <|
        sized_falling _ _) _
case zero
𝕜 : Type u_2
α : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s : Finset α
inst✝ : Fintype α
hk✝ : k ≤ Fintype.card α
h𝒜 : IsAntichain (fun x x_1 => x ⊆ x_1) ↑𝒜
hk : zero ≤ Fintype.card α
⊢ card (𝒜 # Fintype.card α) ≤ card (falling (Fintype.card α) 𝒜)
case zero
𝕜 : Type u_2
α : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s : Finset α
inst✝ : Fintype α
hk✝ : k ≤ Fintype.card α
h𝒜 : IsAntichain (fun x x_1 => x ⊆ x_1) ↑𝒜
hk : zero ≤ Fintype.card α
⊢ ∑ r in range (zero + 1), ↑(card (𝒜 # (Fintype.card α - r))) / ↑(Nat.choose (Fintype.card α) (Fintype.card α - r)) ≤
    ↑(card (falling (Fintype.card α - zero) 𝒜)) / ↑(Nat.choose (Fintype.card α) (Fintype.card α - zero))
simp only [tsub_zero, cast_one, cast_le, sum_singleton, div_one, choose_self, range_one,
  zero_eq, zero_add, range_one, ge_iff_le, sum_singleton, nonpos_iff_eq_zero, tsub_zero,
  choose_self, cast_one, div_one, cast_le]
no goals
case zero
𝕜 : Type u_2
α : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s : Finset α
inst✝ : Fintype α
hk✝ : k ≤ Fintype.card α
h𝒜 : IsAntichain (fun x x_1 => x ⊆ x_1) ↑𝒜
hk : zero ≤ Fintype.card α
⊢ card (𝒜 # Fintype.card α) ≤ card (falling (Fintype.card α) 𝒜)
exact card_le_of_subset (slice_subset_falling _ _)