[GOAL]
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r ↑𝒜
⊢ card 𝒜 * r ≤ card (∂ 𝒜) * (Fintype.card α - r + 1)
[PROOFSTEP]
let i : DecidableRel ((· ⊆ ·) : Finset α → Finset α → Prop) := fun _ _ => Classical.dec _
[GOAL]
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r ↑𝒜
i : DecidableRel fun x x_1 => x ⊆ x_1 := fun x x_1 => Classical.dec ((fun x x_2 => x ⊆ x_2) x x_1)
⊢ card 𝒜 * r ≤ card (∂ 𝒜) * (Fintype.card α - r + 1)
[PROOFSTEP]
refine' card_mul_le_card_mul' (· ⊆ ·) (fun s hs => _) (fun s hs => _)
[GOAL]
case refine'_1
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r ↑𝒜
i : DecidableRel fun x x_1 => x ⊆ x_1 := fun x x_1 => Classical.dec ((fun x x_2 => x ⊆ x_2) x x_1)
s : Finset α
hs : s ∈ 𝒜
⊢ r ≤ card (bipartiteBelow (fun x x_1 => x ⊆ x_1) (∂ 𝒜) s)
[PROOFSTEP]
rw [← h𝒜 hs, ← card_image_of_injOn s.erase_injOn]
[GOAL]
case refine'_1
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r ↑𝒜
i : DecidableRel fun x x_1 => x ⊆ x_1 := fun x x_1 => Classical.dec ((fun x x_2 => x ⊆ x_2) x x_1)
s : Finset α
hs : s ∈ 𝒜
⊢ card (image (erase s) s) ≤ card (bipartiteBelow (fun x x_1 => x ⊆ x_1) (∂ 𝒜) s)
[PROOFSTEP]
refine' card_le_of_subset _
[GOAL]
case refine'_1
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r ↑𝒜
i : DecidableRel fun x x_1 => x ⊆ x_1 := fun x x_1 => Classical.dec ((fun x x_2 => x ⊆ x_2) x x_1)
s : Finset α
hs : s ∈ 𝒜
⊢ image (erase s) s ⊆ bipartiteBelow (fun x x_1 => x ⊆ x_1) (∂ 𝒜) s
[PROOFSTEP]
simp_rw [image_subset_iff, mem_bipartiteBelow]
[GOAL]
case refine'_1
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r ↑𝒜
i : DecidableRel fun x x_1 => x ⊆ x_1 := fun x x_1 => Classical.dec ((fun x x_2 => x ⊆ x_2) x x_1)
s : Finset α
hs : s ∈ 𝒜
⊢ ∀ (x : α), x ∈ s → erase s x ∈ ∂ 𝒜 ∧ erase s x ⊆ s
[PROOFSTEP]
exact fun a ha => ⟨erase_mem_shadow hs ha, erase_subset _ _⟩
[GOAL]
case refine'_2
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r ↑𝒜
i : DecidableRel fun x x_1 => x ⊆ x_1 := fun x x_1 => Classical.dec ((fun x x_2 => x ⊆ x_2) x x_1)
s : Finset α
hs : s ∈ ∂ 𝒜
⊢ card (bipartiteAbove (fun x x_1 => x ⊆ x_1) 𝒜 s) ≤ Fintype.card α - r + 1
[PROOFSTEP]
refine' le_trans _ tsub_tsub_le_tsub_add
[GOAL]
case refine'_2
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r ↑𝒜
i : DecidableRel fun x x_1 => x ⊆ x_1 := fun x x_1 => Classical.dec ((fun x x_2 => x ⊆ x_2) x x_1)
s : Finset α
hs : s ∈ ∂ 𝒜
⊢ card (bipartiteAbove (fun x x_1 => x ⊆ x_1) 𝒜 s) ≤ Fintype.card α - (r - 1)
[PROOFSTEP]
rw [← (Set.Sized.shadow h𝒜) hs, ← card_compl, ← card_image_of_injOn (insert_inj_on' _)]
[GOAL]
case refine'_2
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r ↑𝒜
i : DecidableRel fun x x_1 => x ⊆ x_1 := fun x x_1 => Classical.dec ((fun x x_2 => x ⊆ x_2) x x_1)
s : Finset α
hs : s ∈ ∂ 𝒜
⊢ card (bipartiteAbove (fun x x_1 => x ⊆ x_1) 𝒜 s) ≤ card (image (fun a => insert a s) sᶜ)
[PROOFSTEP]
refine'
  card_le_of_subset fun t ht =>
    _
      -- porting note: commented out the following line
        -- infer_instance
[GOAL]
case refine'_2
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r ↑𝒜
i : DecidableRel fun x x_1 => x ⊆ x_1 := fun x x_1 => Classical.dec ((fun x x_2 => x ⊆ x_2) x x_1)
s : Finset α
hs : s ∈ ∂ 𝒜
t : Finset α
ht : t ∈ bipartiteAbove (fun x x_1 => x ⊆ x_1) 𝒜 s
⊢ t ∈ image (fun a => insert a s) sᶜ
[PROOFSTEP]
rw [mem_bipartiteAbove] at ht 
[GOAL]
case refine'_2
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r ↑𝒜
i : DecidableRel fun x x_1 => x ⊆ x_1 := fun x x_1 => Classical.dec ((fun x x_2 => x ⊆ x_2) x x_1)
s : Finset α
hs : s ∈ ∂ 𝒜
t : Finset α
ht : t ∈ 𝒜 ∧ s ⊆ t
⊢ t ∈ image (fun a => insert a s) sᶜ
[PROOFSTEP]
have : ∅ ∉ 𝒜 := by
  rw [← mem_coe, h𝒜.empty_mem_iff, coe_eq_singleton]
  rintro rfl
  rw [shadow_singleton_empty] at hs 
  exact not_mem_empty s hs
[GOAL]
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r ↑𝒜
i : DecidableRel fun x x_1 => x ⊆ x_1 := fun x x_1 => Classical.dec ((fun x x_2 => x ⊆ x_2) x x_1)
s : Finset α
hs : s ∈ ∂ 𝒜
t : Finset α
ht : t ∈ 𝒜 ∧ s ⊆ t
⊢ ¬∅ ∈ 𝒜
[PROOFSTEP]
rw [← mem_coe, h𝒜.empty_mem_iff, coe_eq_singleton]
[GOAL]
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r ↑𝒜
i : DecidableRel fun x x_1 => x ⊆ x_1 := fun x x_1 => Classical.dec ((fun x x_2 => x ⊆ x_2) x x_1)
s : Finset α
hs : s ∈ ∂ 𝒜
t : Finset α
ht : t ∈ 𝒜 ∧ s ⊆ t
⊢ ¬𝒜 = {∅}
[PROOFSTEP]
rintro rfl
[GOAL]
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
r : ℕ
i : DecidableRel fun x x_1 => x ⊆ x_1 := fun x x_1 => Classical.dec ((fun x x_2 => x ⊆ x_2) x x_1)
s t : Finset α
h𝒜 : Set.Sized r ↑{∅}
hs : s ∈ ∂ {∅}
ht : t ∈ {∅} ∧ s ⊆ t
⊢ False
[PROOFSTEP]
rw [shadow_singleton_empty] at hs 
[GOAL]
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
r : ℕ
i : DecidableRel fun x x_1 => x ⊆ x_1 := fun x x_1 => Classical.dec ((fun x x_2 => x ⊆ x_2) x x_1)
s t : Finset α
h𝒜 : Set.Sized r ↑{∅}
hs : s ∈ ∅
ht : t ∈ {∅} ∧ s ⊆ t
⊢ False
[PROOFSTEP]
exact not_mem_empty s hs
[GOAL]
case refine'_2
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r ↑𝒜
i : DecidableRel fun x x_1 => x ⊆ x_1 := fun x x_1 => Classical.dec ((fun x x_2 => x ⊆ x_2) x x_1)
s : Finset α
hs : s ∈ ∂ 𝒜
t : Finset α
ht : t ∈ 𝒜 ∧ s ⊆ t
this : ¬∅ ∈ 𝒜
⊢ t ∈ image (fun a => insert a s) sᶜ
[PROOFSTEP]
have h :=
  exists_eq_insert_iff.2 ⟨ht.2, by rw [(sized_shadow_iff this).1 (Set.Sized.shadow h𝒜) ht.1, (Set.Sized.shadow h𝒜) hs]⟩
[GOAL]
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r ↑𝒜
i : DecidableRel fun x x_1 => x ⊆ x_1 := fun x x_1 => Classical.dec ((fun x x_2 => x ⊆ x_2) x x_1)
s : Finset α
hs : s ∈ ∂ 𝒜
t : Finset α
ht : t ∈ 𝒜 ∧ s ⊆ t
this : ¬∅ ∈ 𝒜
⊢ card s + 1 = card t
[PROOFSTEP]
rw [(sized_shadow_iff this).1 (Set.Sized.shadow h𝒜) ht.1, (Set.Sized.shadow h𝒜) hs]
[GOAL]
case refine'_2
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r ↑𝒜
i : DecidableRel fun x x_1 => x ⊆ x_1 := fun x x_1 => Classical.dec ((fun x x_2 => x ⊆ x_2) x x_1)
s : Finset α
hs : s ∈ ∂ 𝒜
t : Finset α
ht : t ∈ 𝒜 ∧ s ⊆ t
this : ¬∅ ∈ 𝒜
h : ∃ a x, insert a s = t
⊢ t ∈ image (fun a => insert a s) sᶜ
[PROOFSTEP]
rcases h with ⟨a, ha, rfl⟩
[GOAL]
case refine'_2.intro.intro
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r ↑𝒜
i : DecidableRel fun x x_1 => x ⊆ x_1 := fun x x_1 => Classical.dec ((fun x x_2 => x ⊆ x_2) x x_1)
s : Finset α
hs : s ∈ ∂ 𝒜
this : ¬∅ ∈ 𝒜
a : α
ha : ¬a ∈ s
ht : insert a s ∈ 𝒜 ∧ s ⊆ insert a s
⊢ insert a s ∈ image (fun a => insert a s) sᶜ
[PROOFSTEP]
exact mem_image_of_mem _ (mem_compl.2 ha)
[GOAL]
𝕜 : Type u_1
α : Type u_2
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))
[PROOFSTEP]
obtain hr' | hr' := lt_or_le (Fintype.card α) r
[GOAL]
case inl
𝕜 : Type u_1
α : Type u_2
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))
[PROOFSTEP]
rw [choose_eq_zero_of_lt hr', cast_zero, div_zero]
[GOAL]
case inl
𝕜 : Type u_1
α : Type u_2
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))
[PROOFSTEP]
exact div_nonneg (cast_nonneg _) (cast_nonneg _)
[GOAL]
case inr
𝕜 : Type u_1
α : Type u_2
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))
[PROOFSTEP]
replace h𝒜 := card_mul_le_card_shadow_mul h𝒜
[GOAL]
case inr
𝕜 : Type u_1
α : Type u_2
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))
[PROOFSTEP]
rw [div_le_div_iff]
[GOAL]
case inr
𝕜 : Type u_1
α : Type u_2
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)
[PROOFSTEP]
norm_cast
[GOAL]
case inr.b0
𝕜 : Type u_1
α : Type u_2
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)
[PROOFSTEP]
norm_cast
[GOAL]
case inr.d0
𝕜 : Type u_1
α : Type u_2
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))
[PROOFSTEP]
norm_cast
[GOAL]
case inr
𝕜 : Type u_1
α : Type u_2
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
[PROOFSTEP]
cases' r with r
[GOAL]
case inr.zero
𝕜 : Type u_1
α : Type u_2
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
[PROOFSTEP]
exact (hr rfl).elim
[GOAL]
case inr.succ
𝕜 : Type u_1
α : Type u_2
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)
[PROOFSTEP]
rw [Nat.succ_eq_add_one] at *
[GOAL]
case inr.succ
𝕜 : Type u_1
α : Type u_2
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)
[PROOFSTEP]
rw [tsub_add_eq_add_tsub hr', add_tsub_add_eq_tsub_right] at h𝒜 
[GOAL]
case inr.succ
𝕜 : Type u_1
α : Type u_2
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)
[PROOFSTEP]
apply le_of_mul_le_mul_right _ (pos_iff_ne_zero.2 hr)
[GOAL]
𝕜 : Type u_1
α : Type u_2
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)
[PROOFSTEP]
convert Nat.mul_le_mul_right ((Fintype.card α).choose r) h𝒜 using 1
[GOAL]
case h.e'_3
𝕜 : Type u_1
α : Type u_2
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
[PROOFSTEP]
simp [mul_assoc, Nat.choose_succ_right_eq]
[GOAL]
case h.e'_3
𝕜 : Type u_1
α : Type u_2
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 ∨ 𝒜 = ∅
[PROOFSTEP]
exact Or.inl (mul_comm _ _)
[GOAL]
case h.e'_4
𝕜 : Type u_1
α : Type u_2
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
[PROOFSTEP]
simp only [mul_assoc, choose_succ_right_eq, mul_eq_mul_left_iff]
[GOAL]
case h.e'_4
𝕜 : Type u_1
α : Type u_2
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
[PROOFSTEP]
exact Or.inl (mul_comm _ _)
[GOAL]
case inr.b0
𝕜 : Type u_1
α : Type u_2
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
[PROOFSTEP]
exact Nat.choose_pos hr'
[GOAL]
case inr.d0
𝕜 : Type u_1
α : Type u_2
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)
[PROOFSTEP]
exact Nat.choose_pos (r.pred_le.trans hr')
[GOAL]
𝕜 : Type u_1
α : Type u_2
inst✝¹ : LinearOrderedField 𝕜
inst✝ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s : Finset α
⊢ s ∈ falling k 𝒜 ↔ (∃ t, t ∈ 𝒜 ∧ s ⊆ t) ∧ card s = k
[PROOFSTEP]
simp_rw [falling, mem_sup, mem_powersetLen]
[GOAL]
𝕜 : Type u_1
α : Type u_2
inst✝¹ : LinearOrderedField 𝕜
inst✝ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s : Finset α
⊢ (∃ v, v ∈ 𝒜 ∧ s ⊆ v ∧ card s = k) ↔ (∃ t, t ∈ 𝒜 ∧ s ⊆ t) ∧ card s = k
[PROOFSTEP]
aesop
[GOAL]
𝕜 : Type u_1
α : Type u_2
inst✝¹ : LinearOrderedField 𝕜
inst✝ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s : Finset α
⊢ 𝒜 # k ∪ ∂ (falling (k + 1) 𝒜) = falling k 𝒜
[PROOFSTEP]
ext s
[GOAL]
case a
𝕜 : Type u_1
α : Type u_2
inst✝¹ : LinearOrderedField 𝕜
inst✝ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s✝ s : Finset α
⊢ s ∈ 𝒜 # k ∪ ∂ (falling (k + 1) 𝒜) ↔ s ∈ falling k 𝒜
[PROOFSTEP]
simp_rw [mem_union, mem_slice, mem_shadow_iff, mem_falling]
[GOAL]
case a
𝕜 : Type u_1
α : Type u_2
inst✝¹ : LinearOrderedField 𝕜
inst✝ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s✝ s : Finset α
⊢ (s ∈ 𝒜 ∧ card s = k ∨ ∃ t, ((∃ t_1, t_1 ∈ 𝒜 ∧ t ⊆ t_1) ∧ card t = k + 1) ∧ ∃ a, a ∈ t ∧ erase t a = s) ↔
    (∃ t, t ∈ 𝒜 ∧ s ⊆ t) ∧ card s = k
[PROOFSTEP]
constructor
[GOAL]
case a.mp
𝕜 : Type u_1
α : Type u_2
inst✝¹ : LinearOrderedField 𝕜
inst✝ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s✝ s : Finset α
⊢ (s ∈ 𝒜 ∧ card s = k ∨ ∃ t, ((∃ t_1, t_1 ∈ 𝒜 ∧ t ⊆ t_1) ∧ card t = k + 1) ∧ ∃ a, a ∈ t ∧ erase t a = s) →
    (∃ t, t ∈ 𝒜 ∧ s ⊆ t) ∧ card s = k
[PROOFSTEP]
rintro (h | ⟨s, ⟨⟨t, ht, hst⟩, hs⟩, a, ha, rfl⟩)
[GOAL]
case a.mp.inl
𝕜 : Type u_1
α : Type u_2
inst✝¹ : LinearOrderedField 𝕜
inst✝ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s✝ s : Finset α
h : s ∈ 𝒜 ∧ card s = k
⊢ (∃ t, t ∈ 𝒜 ∧ s ⊆ t) ∧ card s = k
[PROOFSTEP]
exact ⟨⟨s, h.1, Subset.refl _⟩, h.2⟩
[GOAL]
case a.mp.inr.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
α : Type u_2
inst✝¹ : LinearOrderedField 𝕜
inst✝ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s✝ s : Finset α
hs : card s = k + 1
t : Finset α
ht : t ∈ 𝒜
hst : s ⊆ t
a : α
ha : a ∈ s
⊢ (∃ t, t ∈ 𝒜 ∧ erase s a ⊆ t) ∧ card (erase s a) = k
[PROOFSTEP]
refine' ⟨⟨t, ht, (erase_subset _ _).trans hst⟩, _⟩
[GOAL]
case a.mp.inr.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
α : Type u_2
inst✝¹ : LinearOrderedField 𝕜
inst✝ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s✝ s : Finset α
hs : card s = k + 1
t : Finset α
ht : t ∈ 𝒜
hst : s ⊆ t
a : α
ha : a ∈ s
⊢ card (erase s a) = k
[PROOFSTEP]
rw [card_erase_of_mem ha, hs]
[GOAL]
case a.mp.inr.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
α : Type u_2
inst✝¹ : LinearOrderedField 𝕜
inst✝ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s✝ s : Finset α
hs : card s = k + 1
t : Finset α
ht : t ∈ 𝒜
hst : s ⊆ t
a : α
ha : a ∈ s
⊢ k + 1 - 1 = k
[PROOFSTEP]
rfl
[GOAL]
case a.mpr
𝕜 : Type u_1
α : Type u_2
inst✝¹ : LinearOrderedField 𝕜
inst✝ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s✝ s : Finset α
⊢ (∃ t, t ∈ 𝒜 ∧ s ⊆ t) ∧ card s = k →
    s ∈ 𝒜 ∧ card s = k ∨ ∃ t, ((∃ t_1, t_1 ∈ 𝒜 ∧ t ⊆ t_1) ∧ card t = k + 1) ∧ ∃ a, a ∈ t ∧ erase t a = s
[PROOFSTEP]
rintro ⟨⟨t, ht, hst⟩, hs⟩
[GOAL]
case a.mpr.intro.intro.intro
𝕜 : Type u_1
α : Type u_2
inst✝¹ : LinearOrderedField 𝕜
inst✝ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s✝ s : Finset α
hs : card s = k
t : Finset α
ht : t ∈ 𝒜
hst : s ⊆ t
⊢ s ∈ 𝒜 ∧ card s = k ∨ ∃ t, ((∃ t_1, t_1 ∈ 𝒜 ∧ t ⊆ t_1) ∧ card t = k + 1) ∧ ∃ a, a ∈ t ∧ erase t a = s
[PROOFSTEP]
by_cases h : s ∈ 𝒜
[GOAL]
case pos
𝕜 : Type u_1
α : Type u_2
inst✝¹ : LinearOrderedField 𝕜
inst✝ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s✝ s : Finset α
hs : card s = k
t : Finset α
ht : t ∈ 𝒜
hst : s ⊆ t
h : s ∈ 𝒜
⊢ s ∈ 𝒜 ∧ card s = k ∨ ∃ t, ((∃ t_1, t_1 ∈ 𝒜 ∧ t ⊆ t_1) ∧ card t = k + 1) ∧ ∃ a, a ∈ t ∧ erase t a = s
[PROOFSTEP]
exact Or.inl ⟨h, hs⟩
[GOAL]
case neg
𝕜 : Type u_1
α : Type u_2
inst✝¹ : LinearOrderedField 𝕜
inst✝ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s✝ s : Finset α
hs : card s = k
t : Finset α
ht : t ∈ 𝒜
hst : s ⊆ t
h : ¬s ∈ 𝒜
⊢ s ∈ 𝒜 ∧ card s = k ∨ ∃ t, ((∃ t_1, t_1 ∈ 𝒜 ∧ t ⊆ t_1) ∧ card t = k + 1) ∧ ∃ a, a ∈ t ∧ erase t a = s
[PROOFSTEP]
obtain ⟨a, ha, hst⟩ := ssubset_iff.1 (ssubset_of_subset_of_ne hst (ht.ne_of_not_mem h).symm)
[GOAL]
case neg.intro.intro
𝕜 : Type u_1
α : Type u_2
inst✝¹ : LinearOrderedField 𝕜
inst✝ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s✝ s : Finset α
hs : card s = k
t : Finset α
ht : t ∈ 𝒜
hst✝ : s ⊆ t
h : ¬s ∈ 𝒜
a : α
ha : ¬a ∈ s
hst : insert a s ⊆ t
⊢ s ∈ 𝒜 ∧ card s = k ∨ ∃ t, ((∃ t_1, t_1 ∈ 𝒜 ∧ t ⊆ t_1) ∧ card t = k + 1) ∧ ∃ a, a ∈ t ∧ erase t a = s
[PROOFSTEP]
refine' Or.inr ⟨insert a s, ⟨⟨t, ht, hst⟩, _⟩, a, mem_insert_self _ _, erase_insert ha⟩
[GOAL]
case neg.intro.intro
𝕜 : Type u_1
α : Type u_2
inst✝¹ : LinearOrderedField 𝕜
inst✝ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s✝ s : Finset α
hs : card s = k
t : Finset α
ht : t ∈ 𝒜
hst✝ : s ⊆ t
h : ¬s ∈ 𝒜
a : α
ha : ¬a ∈ s
hst : insert a s ⊆ t
⊢ card (insert a s) = k + 1
[PROOFSTEP]
rw [card_insert_of_not_mem ha, hs]
[GOAL]
𝕜 : Type u_1
α : Type u_2
inst✝¹ : LinearOrderedField 𝕜
inst✝ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s✝ : Finset α
m n : ℕ
h𝒜 : IsAntichain (fun x x_1 => x ⊆ x_1) ↑𝒜
s : Finset α
h₁ : s ∈ ∂ (falling n 𝒜)
h₂ : s ∈ 𝒜 # m
⊢ False
[PROOFSTEP]
simp_rw [mem_shadow_iff, mem_falling] at h₁ 
[GOAL]
𝕜 : Type u_1
α : Type u_2
inst✝¹ : LinearOrderedField 𝕜
inst✝ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s✝ : Finset α
m n : ℕ
h𝒜 : IsAntichain (fun x x_1 => x ⊆ x_1) ↑𝒜
s : Finset α
h₂ : s ∈ 𝒜 # m
h₁ : ∃ t, ((∃ t_1, t_1 ∈ 𝒜 ∧ t ⊆ t_1) ∧ card t = n) ∧ ∃ a, a ∈ t ∧ erase t a = s
⊢ False
[PROOFSTEP]
obtain ⟨s, ⟨⟨t, ht, hst⟩, _⟩, a, ha, rfl⟩ := h₁
[GOAL]
case intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
α : Type u_2
inst✝¹ : LinearOrderedField 𝕜
inst✝ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s✝ : Finset α
m n : ℕ
h𝒜 : IsAntichain (fun x x_1 => x ⊆ x_1) ↑𝒜
s : Finset α
right✝ : card s = n
t : Finset α
ht : t ∈ 𝒜
hst : s ⊆ t
a : α
ha : a ∈ s
h₂ : erase s a ∈ 𝒜 # m
⊢ False
[PROOFSTEP]
refine' h𝒜 (slice_subset h₂) ht _ ((erase_subset _ _).trans hst)
[GOAL]
case intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
α : Type u_2
inst✝¹ : LinearOrderedField 𝕜
inst✝ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s✝ : Finset α
m n : ℕ
h𝒜 : IsAntichain (fun x x_1 => x ⊆ x_1) ↑𝒜
s : Finset α
right✝ : card s = n
t : Finset α
ht : t ∈ 𝒜
hst : s ⊆ t
a : α
ha : a ∈ s
h₂ : erase s a ∈ 𝒜 # m
⊢ erase s a ≠ t
[PROOFSTEP]
rintro rfl
[GOAL]
case intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
α : Type u_2
inst✝¹ : LinearOrderedField 𝕜
inst✝ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s✝ : Finset α
m n : ℕ
h𝒜 : IsAntichain (fun x x_1 => x ⊆ x_1) ↑𝒜
s : Finset α
right✝ : card s = n
a : α
ha : a ∈ s
h₂ : erase s a ∈ 𝒜 # m
ht : erase s a ∈ 𝒜
hst : s ⊆ erase s a
⊢ False
[PROOFSTEP]
exact not_mem_erase _ _ (hst ha)
[GOAL]
𝕜 : Type u_1
α : Type u_2
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))
[PROOFSTEP]
induction' k with k ih
[GOAL]
case zero
𝕜 : Type u_1
α : Type u_2
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))
[PROOFSTEP]
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]
[GOAL]
case zero
𝕜 : Type u_1
α : Type u_2
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 α) 𝒜)
[PROOFSTEP]
exact card_le_of_subset (slice_subset_falling _ _)
[GOAL]
case succ
𝕜 : Type u_1
α : Type u_2
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))
[PROOFSTEP]
rw [succ_eq_add_one] at *
[GOAL]
case succ
𝕜 : Type u_1
α : Type u_2
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)))
[PROOFSTEP]
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]
[GOAL]
case succ
𝕜 : Type u_1
α : Type u_2
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)))
[PROOFSTEP]
rw [← tsub_tsub, tsub_add_cancel_of_le (le_tsub_of_add_le_left hk)]
[GOAL]
case succ
𝕜 : Type u_1
α : Type u_2
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))
[PROOFSTEP]
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 _ _)
    _
[GOAL]
𝕜 : Type u_1
α : Type u_2
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
[PROOFSTEP]
classical
rw [← sum_flip]
refine' (le_card_falling_div_choose le_rfl h𝒜).trans _
rw [div_le_iff] <;> norm_cast
· simpa only [Nat.sub_self, one_mul, Nat.choose_zero_right, falling] using Set.Sized.card_le (sized_falling 0 𝒜)
· rw [tsub_self, choose_zero_right]
  exact zero_lt_one
[GOAL]
𝕜 : Type u_1
α : Type u_2
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
[PROOFSTEP]
rw [← sum_flip]
[GOAL]
𝕜 : Type u_1
α : Type u_2
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
[PROOFSTEP]
refine' (le_card_falling_div_choose le_rfl h𝒜).trans _
[GOAL]
𝕜 : Type u_1
α : Type u_2
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
[PROOFSTEP]
rw [div_le_iff]
[GOAL]
𝕜 : Type u_1
α : Type u_2
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 α))
[PROOFSTEP]
norm_cast
[GOAL]
𝕜 : Type u_1
α : Type u_2
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 α))
[PROOFSTEP]
norm_cast
[GOAL]
𝕜 : Type u_1
α : Type u_2
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 α)
[PROOFSTEP]
simpa only [Nat.sub_self, one_mul, Nat.choose_zero_right, falling] using Set.Sized.card_le (sized_falling 0 𝒜)
[GOAL]
𝕜 : Type u_1
α : Type u_2
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 α)
[PROOFSTEP]
rw [tsub_self, choose_zero_right]
[GOAL]
𝕜 : Type u_1
α : Type u_2
inst✝¹ : LinearOrderedField 𝕜
𝒜 : Finset (Finset α)
s : Finset α
k : ℕ
inst✝ : Fintype α
h𝒜 : IsAntichain (fun x x_1 => x ⊆ x_1) ↑𝒜
⊢ 0 < 1
[PROOFSTEP]
exact zero_lt_one
[GOAL]
𝕜 : Type u_1
α : Type u_2
inst✝¹ : LinearOrderedField 𝕜
inst✝ : Fintype α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun x x_1 => x ⊆ x_1) ↑𝒜
⊢ card 𝒜 ≤ Nat.choose (Fintype.card α) (Fintype.card α / 2)
[PROOFSTEP]
classical
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 _ _)
rw [Iic_eq_Icc, ← Ico_succ_right, bot_eq_zero, Ico_zero_eq_range]
refine' (sum_le_sum fun r hr => _).trans (sum_card_slice_div_choose_le_one h𝒜)
rw [mem_range] at hr 
refine' div_le_div_of_le_left _ _ _ <;> norm_cast
· exact Nat.zero_le _
· exact choose_pos (lt_succ_iff.1 hr)
· exact choose_le_middle _ _
[GOAL]
𝕜 : Type u_1
α : Type u_2
inst✝¹ : LinearOrderedField 𝕜
inst✝ : Fintype α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun x x_1 => x ⊆ x_1) ↑𝒜
⊢ card 𝒜 ≤ Nat.choose (Fintype.card α) (Fintype.card α / 2)
[PROOFSTEP]
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 _ _)
[GOAL]
𝕜 : Type u_1
α : Type u_2
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)
[PROOFSTEP]
rw [← sum_div, ← Nat.cast_sum, div_le_one] at this 
[GOAL]
𝕜 : Type u_1
α : Type u_2
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_1
α : Type u_2
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))
[PROOFSTEP]
simp only [cast_le] at this 
[GOAL]
𝕜 : Type u_1
α : Type u_2
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_1
α : Type u_2
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))
[PROOFSTEP]
rwa [sum_card_slice] at this 
[GOAL]
𝕜 : Type u_1
α : Type u_2
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))
[PROOFSTEP]
simp only [cast_pos]
[GOAL]
𝕜 : Type u_1
α : Type u_2
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)
[PROOFSTEP]
exact choose_pos (Nat.div_le_self _ _)
[GOAL]
𝕜 : Type u_1
α : Type u_2
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
[PROOFSTEP]
rw [Iic_eq_Icc, ← Ico_succ_right, bot_eq_zero, Ico_zero_eq_range]
[GOAL]
𝕜 : Type u_1
α : Type u_2
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
[PROOFSTEP]
refine' (sum_le_sum fun r hr => _).trans (sum_card_slice_div_choose_le_one h𝒜)
[GOAL]
𝕜 : Type u_1
α : Type u_2
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)
[PROOFSTEP]
rw [mem_range] at hr 
[GOAL]
𝕜 : Type u_1
α : Type u_2
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)
[PROOFSTEP]
refine' div_le_div_of_le_left _ _ _
[GOAL]
case refine'_1
𝕜 : Type u_1
α : Type u_2
inst✝¹ : LinearOrderedField 𝕜
inst✝ : Fintype α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun x x_1 => x ⊆ x_1) ↑𝒜
r : ℕ
hr : r < succ (Fintype.card α)
⊢ 0 ≤ ↑(card (𝒜 # r))
[PROOFSTEP]
norm_cast
[GOAL]
case refine'_2
𝕜 : Type u_1
α : Type u_2
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)
[PROOFSTEP]
norm_cast
[GOAL]
case refine'_3
𝕜 : Type u_1
α : Type u_2
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))
[PROOFSTEP]
norm_cast
[GOAL]
case refine'_1
𝕜 : Type u_1
α : Type u_2
inst✝¹ : LinearOrderedField 𝕜
inst✝ : Fintype α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun x x_1 => x ⊆ x_1) ↑𝒜
r : ℕ
hr : r < succ (Fintype.card α)
⊢ 0 ≤ card (𝒜 # r)
[PROOFSTEP]
exact Nat.zero_le _
[GOAL]
case refine'_2
𝕜 : Type u_1
α : Type u_2
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
[PROOFSTEP]
exact choose_pos (lt_succ_iff.1 hr)
[GOAL]
case refine'_3
𝕜 : Type u_1
α : Type u_2
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)
[PROOFSTEP]
exact choose_le_middle _ _
