case inl
𝕜 : Type u_2
α : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
hr : r ≠ 0
h𝒜 : Set.Sized r ↑𝒜
hr' : Fintype.card α < r
⊢ ↑(card 𝒜) / ↑(Nat.choose (Fintype.card α) r) ≤ ↑(card ((∂ ) 𝒜)) / ↑(Nat.choose (Fintype.card α) (r - 1))

case inr
𝕜 : Type u_2
α : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
hr : r ≠ 0
h𝒜 : Set.Sized r ↑𝒜
hr' : r ≤ Fintype.card α
⊢ ↑(card 𝒜) / ↑(Nat.choose (Fintype.card α) r) ≤ ↑(card ((∂ ) 𝒜)) / ↑(Nat.choose (Fintype.card α) (r - 1))
𝕜 : Type u_2
α : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
hr : r ≠ 0
h𝒜 : Set.Sized r ↑𝒜
⊢ ↑(card 𝒜) / ↑(Nat.choose (Fintype.card α) r) ≤ ↑(card ((∂ ) 𝒜)) / ↑(Nat.choose (Fintype.card α) (r - 1))
obtain hr' | hr' := lt_or_le (Fintype.card α) r
case inr
𝕜 : Type u_2
α : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
hr : r ≠ 0
hr' : r ≤ Fintype.card α
h𝒜 : card 𝒜 * r ≤ card ((∂ ) 𝒜) * (Fintype.card α - r + 1)
⊢ ↑(card 𝒜) / ↑(Nat.choose (Fintype.card α) r) ≤ ↑(card ((∂ ) 𝒜)) / ↑(Nat.choose (Fintype.card α) (r - 1))
case inr
𝕜 : Type u_2
α : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
hr : r ≠ 0
h𝒜 : Set.Sized r ↑𝒜
hr' : r ≤ Fintype.card α
⊢ ↑(card 𝒜) / ↑(Nat.choose (Fintype.card α) r) ≤ ↑(card ((∂ ) 𝒜)) / ↑(Nat.choose (Fintype.card α) (r - 1))
replace h𝒜 := card_mul_le_card_shadow_mul h𝒜
case inr
𝕜 : Type u_2
α : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
hr : r ≠ 0
hr' : r ≤ Fintype.card α
h𝒜 : card 𝒜 * r ≤ card ((∂ ) 𝒜) * (Fintype.card α - r + 1)
⊢ card 𝒜 * Nat.choose (Fintype.card α) (r - 1) ≤ card ((∂ ) 𝒜) * Nat.choose (Fintype.card α) r

case inr.b0
𝕜 : Type u_2
α : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
hr : r ≠ 0
hr' : r ≤ Fintype.card α
h𝒜 : card 𝒜 * r ≤ card ((∂ ) 𝒜) * (Fintype.card α - r + 1)
⊢ 0 < Nat.choose (Fintype.card α) r

case inr.d0
𝕜 : Type u_2
α : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
hr : r ≠ 0
hr' : r ≤ Fintype.card α
h𝒜 : card 𝒜 * r ≤ card ((∂ ) 𝒜) * (Fintype.card α - r + 1)
⊢ 0 < Nat.choose (Fintype.card α) (r - 1)
case inr
𝕜 : Type u_2
α : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
hr : r ≠ 0
hr' : r ≤ Fintype.card α
h𝒜 : card 𝒜 * r ≤ card ((∂ ) 𝒜) * (Fintype.card α - r + 1)
⊢ ↑(card 𝒜) / ↑(Nat.choose (Fintype.card α) r) ≤ ↑(card ((∂ ) 𝒜)) / ↑(Nat.choose (Fintype.card α) (r - 1))
rw [div_le_div_iff] <;> norm_cast
case inl
𝕜 : Type u_2
α : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
hr : r ≠ 0
h𝒜 : Set.Sized r ↑𝒜
hr' : Fintype.card α < r
⊢ 0 ≤ ↑(card ((∂ ) 𝒜)) / ↑(Nat.choose (Fintype.card α) (r - 1))
case inl
𝕜 : Type u_2
α : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
hr : r ≠ 0
h𝒜 : Set.Sized r ↑𝒜
hr' : Fintype.card α < r
⊢ ↑(card 𝒜) / ↑(Nat.choose (Fintype.card α) r) ≤ ↑(card ((∂ ) 𝒜)) / ↑(Nat.choose (Fintype.card α) (r - 1))
rw [choose_eq_zero_of_lt hr', cast_zero, div_zero]
no goals
case inl
𝕜 : Type u_2
α : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
hr : r ≠ 0
h𝒜 : Set.Sized r ↑𝒜
hr' : Fintype.card α < r
⊢ 0 ≤ ↑(card ((∂ ) 𝒜)) / ↑(Nat.choose (Fintype.card α) (r - 1))
exact div_nonneg (cast_nonneg _) (cast_nonneg _)
case inr.zero
𝕜 : Type u_2
α : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
hr : zero ≠ 0
hr' : zero ≤ Fintype.card α
h𝒜 : card 𝒜 * zero ≤ card ((∂ ) 𝒜) * (Fintype.card α - zero + 1)
⊢ card 𝒜 * Nat.choose (Fintype.card α) (zero - 1) ≤ card ((∂ ) 𝒜) * Nat.choose (Fintype.card α) zero

case inr.succ
𝕜 : Type u_2
α : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
hr : succ r ≠ 0
hr' : succ r ≤ Fintype.card α
h𝒜 : card 𝒜 * succ r ≤ card ((∂ ) 𝒜) * (Fintype.card α - succ r + 1)
⊢ card 𝒜 * Nat.choose (Fintype.card α) (succ r - 1) ≤ card ((∂ ) 𝒜) * Nat.choose (Fintype.card α) (succ r)
case inr
𝕜 : Type u_2
α : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
hr : r ≠ 0
hr' : r ≤ Fintype.card α
h𝒜 : card 𝒜 * r ≤ card ((∂ ) 𝒜) * (Fintype.card α - r + 1)
⊢ card 𝒜 * Nat.choose (Fintype.card α) (r - 1) ≤ card ((∂ ) 𝒜) * Nat.choose (Fintype.card α) r
cases' r with r
case inr.succ
𝕜 : Type u_2
α : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
hr : r + 1 ≠ 0
hr' : r + 1 ≤ Fintype.card α
h𝒜 : card 𝒜 * (r + 1) ≤ card ((∂ ) 𝒜) * (Fintype.card α - (r + 1) + 1)
⊢ card 𝒜 * Nat.choose (Fintype.card α) (r + 1 - 1) ≤ card ((∂ ) 𝒜) * Nat.choose (Fintype.card α) (r + 1)
case inr.succ
𝕜 : Type u_2
α : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
hr : succ r ≠ 0
hr' : succ r ≤ Fintype.card α
h𝒜 : card 𝒜 * succ r ≤ card ((∂ ) 𝒜) * (Fintype.card α - succ r + 1)
⊢ card 𝒜 * Nat.choose (Fintype.card α) (succ r - 1) ≤ card ((∂ ) 𝒜) * Nat.choose (Fintype.card α) (succ r)
rw [Nat.succ_eq_add_one] at *
case inr.succ
𝕜 : Type u_2
α : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
hr : r + 1 ≠ 0
hr' : r + 1 ≤ Fintype.card α
h𝒜 : card 𝒜 * (r + 1) ≤ card ((∂ ) 𝒜) * (Fintype.card α - r)
⊢ card 𝒜 * Nat.choose (Fintype.card α) (r + 1 - 1) ≤ card ((∂ ) 𝒜) * Nat.choose (Fintype.card α) (r + 1)
case inr.succ
𝕜 : Type u_2
α : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
hr : r + 1 ≠ 0
hr' : r + 1 ≤ Fintype.card α
h𝒜 : card 𝒜 * (r + 1) ≤ card ((∂ ) 𝒜) * (Fintype.card α - (r + 1) + 1)
⊢ card 𝒜 * Nat.choose (Fintype.card α) (r + 1 - 1) ≤ card ((∂ ) 𝒜) * Nat.choose (Fintype.card α) (r + 1)
rw [tsub_add_eq_add_tsub hr', add_tsub_add_eq_tsub_right] at h𝒜
𝕜 : Type u_2
α : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
hr : r + 1 ≠ 0
hr' : r + 1 ≤ Fintype.card α
h𝒜 : card 𝒜 * (r + 1) ≤ card ((∂ ) 𝒜) * (Fintype.card α - r)
⊢ card 𝒜 * Nat.choose (Fintype.card α) (r + 1 - 1) * (r + 1) ≤
    card ((∂ ) 𝒜) * Nat.choose (Fintype.card α) (r + 1) * (r + 1)
case inr.succ
𝕜 : Type u_2
α : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
hr : r + 1 ≠ 0
hr' : r + 1 ≤ Fintype.card α
h𝒜 : card 𝒜 * (r + 1) ≤ card ((∂ ) 𝒜) * (Fintype.card α - r)
⊢ card 𝒜 * Nat.choose (Fintype.card α) (r + 1 - 1) ≤ card ((∂ ) 𝒜) * Nat.choose (Fintype.card α) (r + 1)
apply le_of_mul_le_mul_right _ (pos_iff_ne_zero.2 hr)
case h.e'_3
𝕜 : Type u_2
α : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
hr : r + 1 ≠ 0
hr' : r + 1 ≤ Fintype.card α
h𝒜 : card 𝒜 * (r + 1) ≤ card ((∂ ) 𝒜) * (Fintype.card α - r)
⊢ card 𝒜 * Nat.choose (Fintype.card α) (r + 1 - 1) * (r + 1) = card 𝒜 * (r + 1) * Nat.choose (Fintype.card α) r

case h.e'_4
𝕜 : Type u_2
α : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
hr : r + 1 ≠ 0
hr' : r + 1 ≤ Fintype.card α
h𝒜 : card 𝒜 * (r + 1) ≤ card ((∂ ) 𝒜) * (Fintype.card α - r)
⊢ card ((∂ ) 𝒜) * Nat.choose (Fintype.card α) (r + 1) * (r + 1) =
    card ((∂ ) 𝒜) * (Fintype.card α - r) * Nat.choose (Fintype.card α) r
𝕜 : Type u_2
α : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
hr : r + 1 ≠ 0
hr' : r + 1 ≤ Fintype.card α
h𝒜 : card 𝒜 * (r + 1) ≤ card ((∂ ) 𝒜) * (Fintype.card α - r)
⊢ card 𝒜 * Nat.choose (Fintype.card α) (r + 1 - 1) * (r + 1) ≤
    card ((∂ ) 𝒜) * Nat.choose (Fintype.card α) (r + 1) * (r + 1)
convert Nat.mul_le_mul_right ((Fintype.card α).choose r) h𝒜 using 1
no goals
case inr.zero
𝕜 : Type u_2
α : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
hr : zero ≠ 0
hr' : zero ≤ Fintype.card α
h𝒜 : card 𝒜 * zero ≤ card ((∂ ) 𝒜) * (Fintype.card α - zero + 1)
⊢ card 𝒜 * Nat.choose (Fintype.card α) (zero - 1) ≤ card ((∂ ) 𝒜) * Nat.choose (Fintype.card α) zero
exact (hr rfl).elim
case h.e'_3
𝕜 : Type u_2
α : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
hr : r + 1 ≠ 0
hr' : r + 1 ≤ Fintype.card α
h𝒜 : card 𝒜 * (r + 1) ≤ card ((∂ ) 𝒜) * (Fintype.card α - r)
⊢ Nat.choose (Fintype.card α) r * (r + 1) = (r + 1) * Nat.choose (Fintype.card α) r ∨ 𝒜 = ∅
case h.e'_3
𝕜 : Type u_2
α : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
hr : r + 1 ≠ 0
hr' : r + 1 ≤ Fintype.card α
h𝒜 : card 𝒜 * (r + 1) ≤ card ((∂ ) 𝒜) * (Fintype.card α - r)
⊢ card 𝒜 * Nat.choose (Fintype.card α) (r + 1 - 1) * (r + 1) = card 𝒜 * (r + 1) * Nat.choose (Fintype.card α) r
simp [mul_assoc, Nat.choose_succ_right_eq]
no goals
case h.e'_3
𝕜 : Type u_2
α : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
hr : r + 1 ≠ 0
hr' : r + 1 ≤ Fintype.card α
h𝒜 : card 𝒜 * (r + 1) ≤ card ((∂ ) 𝒜) * (Fintype.card α - r)
⊢ Nat.choose (Fintype.card α) r * (r + 1) = (r + 1) * Nat.choose (Fintype.card α) r ∨ 𝒜 = ∅
exact Or.inl (mul_comm _ _)
case h.e'_4
𝕜 : Type u_2
α : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
hr : r + 1 ≠ 0
hr' : r + 1 ≤ Fintype.card α
h𝒜 : card 𝒜 * (r + 1) ≤ card ((∂ ) 𝒜) * (Fintype.card α - r)
⊢ Nat.choose (Fintype.card α) r * (Fintype.card α - r) = (Fintype.card α - r) * Nat.choose (Fintype.card α) r ∨
    card ((∂ ) 𝒜) = 0
case h.e'_4
𝕜 : Type u_2
α : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
hr : r + 1 ≠ 0
hr' : r + 1 ≤ Fintype.card α
h𝒜 : card 𝒜 * (r + 1) ≤ card ((∂ ) 𝒜) * (Fintype.card α - r)
⊢ card ((∂ ) 𝒜) * Nat.choose (Fintype.card α) (r + 1) * (r + 1) =
    card ((∂ ) 𝒜) * (Fintype.card α - r) * Nat.choose (Fintype.card α) r
simp only [mul_assoc, choose_succ_right_eq, mul_eq_mul_left_iff]
no goals
case h.e'_4
𝕜 : Type u_2
α : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
hr : r + 1 ≠ 0
hr' : r + 1 ≤ Fintype.card α
h𝒜 : card 𝒜 * (r + 1) ≤ card ((∂ ) 𝒜) * (Fintype.card α - r)
⊢ Nat.choose (Fintype.card α) r * (Fintype.card α - r) = (Fintype.card α - r) * Nat.choose (Fintype.card α) r ∨
    card ((∂ ) 𝒜) = 0
exact Or.inl (mul_comm _ _)
no goals
case inr.b0
𝕜 : Type u_2
α : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
hr : r ≠ 0
hr' : r ≤ Fintype.card α
h𝒜 : card 𝒜 * r ≤ card ((∂ ) 𝒜) * (Fintype.card α - r + 1)
⊢ 0 < Nat.choose (Fintype.card α) r
exact Nat.choose_pos hr'
no goals
case inr.d0
𝕜 : Type u_2
α : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
hr : r ≠ 0
hr' : r ≤ Fintype.card α
h𝒜 : card 𝒜 * r ≤ card ((∂ ) 𝒜) * (Fintype.card α - r + 1)
⊢ 0 < Nat.choose (Fintype.card α) (r - 1)
exact Nat.choose_pos (r.pred_le.trans hr')