awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SetFamily.LYM
Goal:
α : Type u_2
inst : DecidableEq α
𝒜 : Finset (Finset α)
m n : ℕ
h𝒜 : IsAntichain (fun (x1 x2 : Finset α) ↦ x1 ⊆ x2) (↑𝒜 : Set (Finset α))
s : Finset α
right : #s = n
t : Finset α
ht : t ∈ 𝒜
hst : s ⊆ t
a : α
ha : a ∈ s
h₂ : s.erase a ∈ 𝒜 # m
refine : s.erase a ≠ t
⊢ False

Tactic:
refine h𝒜 (slice_subset h₂) ht ?_ ((erase_subset _ _).trans hst)

Premises used: Finset.slice_subset, HasSubset.Subset.trans, Finset.erase_subset
-- Module: Mathlib.Combinatorics.SetFamily.LYM
Goal:
α : Type u_2
inst : DecidableEq α
𝒜 : Finset (Finset α)
m n : ℕ
h𝒜 : IsAntichain (fun (x1 x2 : Finset α) ↦ x1 ⊆ x2) (↑𝒜 : Set (Finset α))
s : Finset α
right : #s = n
a : α
ha : a ∈ s
h₂ : s.erase a ∈ 𝒜 # m
ht : s.erase a ∈ 𝒜
hst : s ⊆ s.erase a
⊢ False

Tactic:
notMem_erase _ _ (hst ha)

Premises used: Finset.notMem_erase
-- Module: Mathlib.Combinatorics.SetFamily.LYM
Goal:
α : Type u_2
inst : DecidableEq α
𝒜 : Finset (Finset α)
m n : ℕ
h𝒜 : IsAntichain (fun (x1 x2 : Finset α) ↦ x1 ⊆ x2) (↑𝒜 : Set (Finset α))
s : Finset α
right : #s = n
a : α
ha : a ∈ s
h₂ : s.erase a ∈ 𝒜 # m
ht : s.erase a ∈ 𝒜
hst : s ⊆ s.erase a
⊢ False

Tactic:
exact notMem_erase _ _ (hst ha)

Premises used: Finset.notMem_erase
-- Module: Mathlib.Combinatorics.SetFamily.LYM
Goal:
𝕜 : Type u_1
α : Type u_2
inst : Semifield 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
inst_4 : Fintype α
h𝒜 : IsAntichain (fun (x1 x2 : Finset α) ↦ x1 ⊆ x2) (↑𝒜 : Set (Finset α))
hk : 0 ≤ Fintype.card α
zero : #(𝒜 # Fintype.card α) ≤ #(falling (Fintype.card α) 𝒜)
⊢ ∑ r ∈ range (HAdd.hAdd (α := ℕ) 0 1),
      HDiv.hDiv (α := 𝕜) (↑(#(𝒜 # (Fintype.card α - r))) : 𝕜) (↑((Fintype.card α).choose (Fintype.card α - r)) : 𝕜) ≤
    HDiv.hDiv (α := 𝕜) (↑(#(falling (Fintype.card α - 0) 𝒜)) : 𝕜) (↑((Fintype.card α).choose (Fintype.card α - 0)) : 𝕜)

Tactic:
simp only [cast_one, cast_le, sum_singleton, div_one, choose_self, range_one,
      zero_add, range_one, sum_singleton,
      choose_self, cast_one, div_one, cast_le, tsub_zero]

Premises used: zero_add, Finset.sum_singleton, tsub_zero, Finset.range_one, Nat.cast_le, div_one, Nat.cast_one, Nat.choose_self
-- Module: Mathlib.Combinatorics.SetFamily.LYM
Goal:
𝕜 : Type u_1
α : Type u_2
inst : Semifield 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
inst_4 : Fintype α
h𝒜 : IsAntichain (fun (x1 x2 : Finset α) ↦ x1 ⊆ x2) (↑𝒜 : Set (Finset α))
hk : 0 ≤ Fintype.card α
⊢ #(𝒜 # Fintype.card α) ≤ #(falling (Fintype.card α) 𝒜)

Tactic:
card_le_card (slice_subset_falling _ _)

Premises used: Finset.slice_subset_falling, Finset.card_le_card
-- Module: Mathlib.Combinatorics.SetFamily.LYM
Goal:
𝕜 : Type u_1
α : Type u_2
inst : Semifield 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
inst_4 : Fintype α
h𝒜 : IsAntichain (fun (x1 x2 : Finset α) ↦ x1 ⊆ x2) (↑𝒜 : Set (Finset α))
hk : 0 ≤ Fintype.card α
⊢ #(𝒜 # Fintype.card α) ≤ #(falling (Fintype.card α) 𝒜)

Tactic:
exact card_le_card (slice_subset_falling _ _)

Premises used: Finset.slice_subset_falling, Finset.card_le_card
-- Module: Mathlib.Combinatorics.SetFamily.LYM
Goal:
𝕜 : Type u_1
α : Type u_2
inst : Semifield 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : DecidableEq α
k_1 : ℕ
𝒜 : Finset (Finset α)
inst_4 : Fintype α
h𝒜 : IsAntichain (fun (x1 x2 : Finset α) ↦ x1 ⊆ x2) (↑𝒜 : Set (Finset α))
k : ℕ
ih :
  ∀ (hk : k ≤ Fintype.card α),
    ∑ r ∈ range (k + 1),
        HDiv.hDiv (α := 𝕜) (↑(#(𝒜 # (Fintype.card α - r))) : 𝕜) (↑((Fintype.card α).choose (Fintype.card α - r)) : 𝕜) ≤
      HDiv.hDiv (α := 𝕜) (↑(#(falling (Fintype.card α - k) 𝒜)) : 𝕜)
        (↑((Fintype.card α).choose (Fintype.card α - k)) : 𝕜)
hk : k + 1 ≤ Fintype.card α
succ :
  HDiv.hDiv (α := 𝕜) (↑(#(𝒜 # (Fintype.card α - (k + 1)))) : 𝕜)
        (↑((Fintype.card α).choose (Fintype.card α - (k + 1))) : 𝕜) +
      ∑ x ∈ range (k + 1),
        HDiv.hDiv (α := 𝕜) (↑(#(𝒜 # (Fintype.card α - x))) : 𝕜) (↑((Fintype.card α).choose (Fintype.card α - x)) : 𝕜) ≤
    HDiv.hDiv (α := 𝕜) (↑(#(𝒜 # (Fintype.card α - (k + 1)))) : 𝕜)
        (↑((Fintype.card α).choose (Fintype.card α - (k + 1))) : 𝕜) +
      HDiv.hDiv (α := 𝕜) (↑(#(∂ (falling (Fintype.card α - (k + 1) + 1) 𝒜))) : 𝕜)
        (↑((Fintype.card α).choose (Fintype.card α - (k + 1))) : 𝕜)
⊢ ∑ r ∈ range (k + 1 + 1),
      HDiv.hDiv (α := 𝕜) (↑(#(𝒜 # (Fintype.card α - r))) : 𝕜) (↑((Fintype.card α).choose (Fintype.card α - r)) : 𝕜) ≤
    HDiv.hDiv (α := 𝕜) (↑(#(falling (Fintype.card α - (k + 1)) 𝒜)) : 𝕜)
      (↑((Fintype.card α).choose (Fintype.card α - (k + 1))) : 𝕜)

Tactic:
rw [sum_range_succ, ← slice_union_shadow_falling_succ,
      card_union_of_disjoint (IsAntichain.disjoint_slice_shadow_falling h𝒜),
      cast_add, _root_.add_div, add_comm]

Premises used: add_comm, Nat.cast_add, Finset.slice_union_shadow_falling_succ, Finset.card_union_of_disjoint, Finset.sum_range_succ, Finset.IsAntichain.disjoint_slice_shadow_falling, add_div
-- Module: Mathlib.Combinatorics.SetFamily.LYM
Goal:
𝕜 : Type u_1
α : Type u_2
inst : Semifield 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : DecidableEq α
k_1 : ℕ
𝒜 : Finset (Finset α)
inst_4 : Fintype α
h𝒜 : IsAntichain (fun (x1 x2 : Finset α) ↦ x1 ⊆ x2) (↑𝒜 : Set (Finset α))
k : ℕ
ih :
  ∀ (hk : k ≤ Fintype.card α),
    ∑ r ∈ range (k + 1),
        HDiv.hDiv (α := 𝕜) (↑(#(𝒜 # (Fintype.card α - r))) : 𝕜) (↑((Fintype.card α).choose (Fintype.card α - r)) : 𝕜) ≤
      HDiv.hDiv (α := 𝕜) (↑(#(falling (Fintype.card α - k) 𝒜)) : 𝕜)
        (↑((Fintype.card α).choose (Fintype.card α - k)) : 𝕜)
hk : k + 1 ≤ Fintype.card α
succ :
  HDiv.hDiv (α := 𝕜) (↑(#(𝒜 # (Fintype.card α - k - 1))) : 𝕜)
        (↑((Fintype.card α).choose (Fintype.card α - k - 1)) : 𝕜) +
      ∑ x ∈ range (k + 1),
        HDiv.hDiv (α := 𝕜) (↑(#(𝒜 # (Fintype.card α - x))) : 𝕜) (↑((Fintype.card α).choose (Fintype.card α - x)) : 𝕜) ≤
    HDiv.hDiv (α := 𝕜) (↑(#(𝒜 # (Fintype.card α - k - 1))) : 𝕜)
        (↑((Fintype.card α).choose (Fintype.card α - k - 1)) : 𝕜) +
      HDiv.hDiv (α := 𝕜) (↑(#(∂ (falling (Fintype.card α - k) 𝒜))) : 𝕜)
        (↑((Fintype.card α).choose (Fintype.card α - k - 1)) : 𝕜)
⊢ HDiv.hDiv (α := 𝕜) (↑(#(𝒜 # (Fintype.card α - (k + 1)))) : 𝕜)
        (↑((Fintype.card α).choose (Fintype.card α - (k + 1))) : 𝕜) +
      ∑ x ∈ range (k + 1),
        HDiv.hDiv (α := 𝕜) (↑(#(𝒜 # (Fintype.card α - x))) : 𝕜) (↑((Fintype.card α).choose (Fintype.card α - x)) : 𝕜) ≤
    HDiv.hDiv (α := 𝕜) (↑(#(𝒜 # (Fintype.card α - (k + 1)))) : 𝕜)
        (↑((Fintype.card α).choose (Fintype.card α - (k + 1))) : 𝕜) +
      HDiv.hDiv (α := 𝕜) (↑(#(∂ (falling (Fintype.card α - (k + 1) + 1) 𝒜))) : 𝕜)
        (↑((Fintype.card α).choose (Fintype.card α - (k + 1))) : 𝕜)

Tactic:
rw [← tsub_tsub, tsub_add_cancel_of_le (le_tsub_of_add_le_left hk)]

Premises used: le_tsub_of_add_le_left, tsub_add_cancel_of_le, tsub_tsub
-- Module: Mathlib.Combinatorics.SetFamily.LYM
Goal:
𝕜 : Type u_1
α : Type u_2
inst : Semifield 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : DecidableEq α
k_1 : ℕ
𝒜 : Finset (Finset α)
inst_4 : Fintype α
h𝒜 : IsAntichain (fun (x1 x2 : Finset α) ↦ x1 ⊆ x2) (↑𝒜 : Set (Finset α))
k : ℕ
ih :
  ∀ (hk : k ≤ Fintype.card α),
    ∑ r ∈ range (k + 1),
        HDiv.hDiv (α := 𝕜) (↑(#(𝒜 # (Fintype.card α - r))) : 𝕜) (↑((Fintype.card α).choose (Fintype.card α - r)) : 𝕜) ≤
      HDiv.hDiv (α := 𝕜) (↑(#(falling (Fintype.card α - k) 𝒜)) : 𝕜)
        (↑((Fintype.card α).choose (Fintype.card α - k)) : 𝕜)
hk : k + 1 ≤ Fintype.card α
succ :
  HDiv.hDiv (α := 𝕜) (↑(#(𝒜 # (Fintype.card α - k - 1))) : 𝕜)
        (↑((Fintype.card α).choose (Fintype.card α - k - 1)) : 𝕜) +
      HDiv.hDiv (α := 𝕜) (↑(#(falling (Fintype.card α - k) 𝒜)) : 𝕜)
        (↑((Fintype.card α).choose (Fintype.card α - k)) : 𝕜) ≤
    HDiv.hDiv (α := 𝕜) (↑(#(𝒜 # (Fintype.card α - k - 1))) : 𝕜)
        (↑((Fintype.card α).choose (Fintype.card α - k - 1)) : 𝕜) +
      HDiv.hDiv (α := 𝕜) (↑(#(∂ (falling (Fintype.card α - k) 𝒜))) : 𝕜)
        (↑((Fintype.card α).choose (Fintype.card α - k - 1)) : 𝕜)
succ₁ succ₂ :
  HDiv.hDiv (α := 𝕜) (↑(#(𝒜 # (Fintype.card α - k - 1))) : 𝕜)
        (↑((Fintype.card α).choose (Fintype.card α - k - 1)) : 𝕜) +
      HDiv.hDiv (α := 𝕜) (↑(#(∂ (falling (Fintype.card α - k) 𝒜))) : 𝕜)
        (↑((Fintype.card α).choose (Fintype.card α - k - 1)) : 𝕜) ≤
    HDiv.hDiv (α := 𝕜) (↑(#(𝒜 # (Fintype.card α - k - 1))) : 𝕜)
        (↑((Fintype.card α).choose (Fintype.card α - k - 1)) : 𝕜) +
      HDiv.hDiv (α := 𝕜) (↑(#(∂ (falling (Fintype.card α - k) 𝒜))) : 𝕜)
        (↑((Fintype.card α).choose (Fintype.card α - k - 1)) : 𝕜)
⊢ HDiv.hDiv (α := 𝕜) (↑(#(𝒜 # (Fintype.card α - k - 1))) : 𝕜)
        (↑((Fintype.card α).choose (Fintype.card α - k - 1)) : 𝕜) +
      ∑ x ∈ range (k + 1),
        HDiv.hDiv (α := 𝕜) (↑(#(𝒜 # (Fintype.card α - x))) : 𝕜) (↑((Fintype.card α).choose (Fintype.card α - x)) : 𝕜) ≤
    HDiv.hDiv (α := 𝕜) (↑(#(𝒜 # (Fintype.card α - k - 1))) : 𝕜)
        (↑((Fintype.card α).choose (Fintype.card α - k - 1)) : 𝕜) +
      HDiv.hDiv (α := 𝕜) (↑(#(∂ (falling (Fintype.card α - k) 𝒜))) : 𝕜)
        (↑((Fintype.card α).choose (Fintype.card α - k - 1)) : 𝕜)

Tactic:
grw [ih <| le_of_succ_le hk, local_lubell_yamamoto_meshalkin_inequality_div
      (tsub_pos_iff_lt.2 <| Nat.succ_le_iff.1 hk).ne' <| sized_falling _ _]

Premises used: Iff.mpr, tsub_pos_iff_lt, Finset.local_lubell_yamamoto_meshalkin_inequality_div, Nat.le_of_succ_le, LT.lt.ne', Iff.mp, Finset.sized_falling, Nat.succ_le_iff
-- Module: Mathlib.Combinatorics.SetFamily.LYM
Goal:
𝕜 : Type u_1
α : Type u_2
inst : Semifield 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
inst_4 : Fintype α
hk : k ≤ Fintype.card α
h𝒜 : IsAntichain (fun (x1 x2 : Finset α) ↦ x1 ⊆ x2) (↑𝒜 : Set (Finset α))
zero :
  ∀ (hk : 0 ≤ Fintype.card α),
    ∑ r ∈ range (HAdd.hAdd (α := ℕ) 0 1),
        HDiv.hDiv (α := 𝕜) (↑(#(𝒜 # (Fintype.card α - r))) : 𝕜) (↑((Fintype.card α).choose (Fintype.card α - r)) : 𝕜) ≤
      HDiv.hDiv (α := 𝕜) (↑(#(falling (Fintype.card α - 0) 𝒜)) : 𝕜)
        (↑((Fintype.card α).choose (Fintype.card α - 0)) : 𝕜)
succ :
  ∀ (k : ℕ)
    (ih :
      ∀ (hk : k ≤ Fintype.card α),
        ∑ r ∈ range (k + 1),
            HDiv.hDiv (α := 𝕜) (↑(#(𝒜 # (Fintype.card α - r))) : 𝕜)
              (↑((Fintype.card α).choose (Fintype.card α - r)) : 𝕜) ≤
          HDiv.hDiv (α := 𝕜) (↑(#(falling (Fintype.card α - k) 𝒜)) : 𝕜)
            (↑((Fintype.card α).choose (Fintype.card α - k)) : 𝕜))
    (hk : k + 1 ≤ Fintype.card α),
    ∑ r ∈ range (k + 1 + 1),
        HDiv.hDiv (α := 𝕜) (↑(#(𝒜 # (Fintype.card α - r))) : 𝕜) (↑((Fintype.card α).choose (Fintype.card α - r)) : 𝕜) ≤
      HDiv.hDiv (α := 𝕜) (↑(#(falling (Fintype.card α - (k + 1)) 𝒜)) : 𝕜)
        (↑((Fintype.card α).choose (Fintype.card α - (k + 1))) : 𝕜)
⊢ ∑ r ∈ range (k + 1),
      HDiv.hDiv (α := 𝕜) (↑(#(𝒜 # (Fintype.card α - r))) : 𝕜) (↑((Fintype.card α).choose (Fintype.card α - r)) : 𝕜) ≤
    HDiv.hDiv (α := 𝕜) (↑(#(falling (Fintype.card α - k) 𝒜)) : 𝕜) (↑((Fintype.card α).choose (Fintype.card α - k)) : 𝕜)

Tactic:
induction k with
  | zero =>
    simp only [cast_one, cast_le, sum_singleton, div_one, choose_self, range_one,
      zero_add, range_one, sum_singleton,
      choose_self, cast_one, div_one, cast_le, tsub_zero]
    exact card_le_card (slice_subset_falling _ _)
  | succ k ih =>
    rw [sum_range_succ, ← slice_union_shadow_falling_succ,
      card_union_of_disjoint (IsAntichain.disjoint_slice_shadow_falling h𝒜),
      cast_add, _root_.add_div, add_comm]
    rw [← tsub_tsub, tsub_add_cancel_of_le (le_tsub_of_add_le_left hk)]
    grw [ih <| le_of_succ_le hk, local_lubell_yamamoto_meshalkin_inequality_div
      (tsub_pos_iff_lt.2 <| Nat.succ_le_iff.1 hk).ne' <| sized_falling _ _]

Premises used: Iff.mpr, Finset.slice_subset_falling, tsub_pos_iff_lt, le_tsub_of_add_le_left, Finset.local_lubell_yamamoto_meshalkin_inequality_div, Finset.card_le_card, Nat.le_of_succ_le, tsub_add_cancel_of_le, zero_add, add_comm, Finset.sum_singleton, tsub_zero, LT.lt.ne', Nat.cast_add, Finset.slice_union_shadow_falling_succ, Iff.mp, tsub_tsub, Nat.zero, Finset.range_one, Finset.sized_falling, Nat.cast_le, Nat.succ_le_iff, Finset.card_union_of_disjoint, Nat.succ, div_one, Nat.cast_one, Finset.sum_range_succ, Nat.choose_self, Finset.IsAntichain.disjoint_slice_shadow_falling, add_div
-- Module: Mathlib.Combinatorics.SetFamily.LYM
Goal:
𝕜 : Type u_1
α : Type u_2
inst : Semifield 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : Fintype α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun (x1 x2 : Finset α) ↦ x1 ⊆ x2) (↑𝒜 : Set (Finset α))
rw :
  LE.le.{u_1} (α := 𝕜)
    (∑ r ∈ range (Fintype.card α + 1),
      HDiv.hDiv (α := 𝕜) (↑(#(𝒜 # (Fintype.card α - r))) : 𝕜) (↑((Fintype.card α).choose (Fintype.card α - r)) : 𝕜))
    1
⊢ LE.le.{u_1} (α := 𝕜)
    (∑ r ∈ range (Fintype.card α + 1), HDiv.hDiv (α := 𝕜) (↑(#(𝒜 # r)) : 𝕜) (↑((Fintype.card α).choose r) : 𝕜)) 1

Tactic:
rw [← sum_flip]

Premises used: Finset.sum_flip
-- Module: Mathlib.Combinatorics.SetFamily.LYM
Goal:
𝕜 : Type u_1
α : Type u_2
inst : Semifield 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : Fintype α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun (x1 x2 : Finset α) ↦ x1 ⊆ x2) (↑𝒜 : Set (Finset α))
⊢ LE.le.{u_1} (α := 𝕜)
    (∑ r ∈ range (Fintype.card α + 1),
      HDiv.hDiv (α := 𝕜) (↑(#(𝒜 # (Fintype.card α - r))) : 𝕜) (↑((Fintype.card α).choose (Fintype.card α - r)) : 𝕜))
    1

Tactic:
(le_card_falling_div_choose le_rfl h𝒜).trans ?_

Premises used: le_rfl, Finset.le_card_falling_div_choose, LE.le.trans
-- Module: Mathlib.Combinatorics.SetFamily.LYM
Goal:
𝕜 : Type u_1
α : Type u_2
inst : Semifield 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : Fintype α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun (x1 x2 : Finset α) ↦ x1 ⊆ x2) (↑𝒜 : Set (Finset α))
refine :
  HDiv.hDiv (α := 𝕜) (↑(#(falling (Fintype.card α - Fintype.card α) 𝒜)) : 𝕜)
      (↑((Fintype.card α).choose (Fintype.card α - Fintype.card α)) : 𝕜) ≤
    1
⊢ LE.le.{u_1} (α := 𝕜)
    (∑ r ∈ range (Fintype.card α + 1),
      HDiv.hDiv (α := 𝕜) (↑(#(𝒜 # (Fintype.card α - r))) : 𝕜) (↑((Fintype.card α).choose (Fintype.card α - r)) : 𝕜))
    1

Tactic:
refine (le_card_falling_div_choose le_rfl h𝒜).trans ?_

Premises used: le_rfl, Finset.le_card_falling_div_choose, LE.le.trans
-- Module: Mathlib.Combinatorics.SetFamily.LYM
Goal:
𝕜 : Type u_1
α : Type u_2
inst : Semifield 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : Fintype α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun (x1 x2 : Finset α) ↦ x1 ⊆ x2) (↑𝒜 : Set (Finset α))
rw :
  (↑(#(falling (Fintype.card α - Fintype.card α) 𝒜)) : 𝕜) ≤
    HMul.hMul (α := 𝕜) 1 (↑((Fintype.card α).choose (Fintype.card α - Fintype.card α)) : 𝕜)
rw₁ : LT.lt.{u_1} (α := 𝕜) 0 (↑((Fintype.card α).choose (Fintype.card α - Fintype.card α)) : 𝕜)
⊢ HDiv.hDiv (α := 𝕜) (↑(#(falling (Fintype.card α - Fintype.card α) 𝒜)) : 𝕜)
      (↑((Fintype.card α).choose (Fintype.card α - Fintype.card α)) : 𝕜) ≤
    1

Tactic:
rw [div_le_iff₀]

Premises used: div_le_iff₀
-- Module: Mathlib.Combinatorics.SetFamily.LYM
Goal:
𝕜 : Type u_1
α : Type u_2
inst : Semifield 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : Fintype α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun (x1 x2 : Finset α) ↦ x1 ⊆ x2) (↑𝒜 : Set (Finset α))
norm_cast :
  #(falling (Fintype.card α - Fintype.card α) 𝒜) ≤ 1 * (Fintype.card α).choose (Fintype.card α - Fintype.card α)
⊢ (↑(#(falling (Fintype.card α - Fintype.card α) 𝒜)) : 𝕜) ≤
    HMul.hMul (α := 𝕜) 1 (↑((Fintype.card α).choose (Fintype.card α - Fintype.card α)) : 𝕜)

Tactic:
norm_cast
-- Module: Mathlib.Combinatorics.SetFamily.LYM
Goal:
𝕜 : Type u_1
α : Type u_2
inst : Semifield 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : Fintype α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun (x1 x2 : Finset α) ↦ x1 ⊆ x2) (↑𝒜 : Set (Finset α))
norm_cast : 0 < (Fintype.card α).choose (Fintype.card α - Fintype.card α)
⊢ LT.lt.{u_1} (α := 𝕜) 0 (↑((Fintype.card α).choose (Fintype.card α - Fintype.card α)) : 𝕜)

Tactic:
norm_cast
-- Module: Mathlib.Combinatorics.SetFamily.LYM
Goal:
𝕜 : Type u_1
α : Type u_2
inst : Semifield 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : Fintype α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun (x1 x2 : Finset α) ↦ x1 ⊆ x2) (↑𝒜 : Set (Finset α))
⊢ #(falling (Fintype.card α - Fintype.card α) 𝒜) ≤ 1 * (Fintype.card α).choose (Fintype.card α - Fintype.card α)

Tactic:
simpa only [Nat.sub_self, one_mul, Nat.choose_zero_right, falling] using
        Set.Sized.card_le (sized_falling 0 𝒜)

Premises used: Nat.sub_self, Finset.sized_falling, OfNat.ofNat, Nat.choose_zero_right, one_mul, Set.Sized.card_le, Finset.falling
-- Module: Mathlib.Combinatorics.SetFamily.LYM
Goal:
𝕜 : Type u_1
α : Type u_2
inst : Semifield 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : Fintype α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun (x1 x2 : Finset α) ↦ x1 ⊆ x2) (↑𝒜 : Set (Finset α))
rw : LT.lt (α := ℕ) 0 1
⊢ 0 < (Fintype.card α).choose (Fintype.card α - Fintype.card α)

Tactic:
rw [tsub_self, choose_zero_right]

Premises used: tsub_self, Nat.choose_zero_right
-- Module: Mathlib.Combinatorics.SetFamily.LYM
Goal:
𝕜 : Type u_1
α : Type u_2
inst : Semifield 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : Fintype α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun (x1 x2 : Finset α) ↦ x1 ⊆ x2) (↑𝒜 : Set (Finset α))
⊢ LT.lt (α := ℕ) 0 1

Tactic:
zero_lt_one

Premises used: zero_lt_one
-- Module: Mathlib.Combinatorics.SetFamily.LYM
Goal:
𝕜 : Type u_1
α : Type u_2
inst : Semifield 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : Fintype α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun (x1 x2 : Finset α) ↦ x1 ⊆ x2) (↑𝒜 : Set (Finset α))
⊢ LT.lt (α := ℕ) 0 1

Tactic:
exact zero_lt_one

Premises used: zero_lt_one
-- Module: Mathlib.Combinatorics.SetFamily.LYM
Goal:
𝕜 : Type u_1
α : Type u_2
inst : Semifield 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : Fintype α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun (x1 x2 : Finset α) ↦ x1 ⊆ x2) (↑𝒜 : Set (Finset α))
rw rw₁ rw₂ :
  LE.le.{u_1} (α := 𝕜)
    (∑ r ∈ range (Fintype.card α + 1),
      HDiv.hDiv (α := 𝕜) (↑(#(𝒜 # (Fintype.card α - r))) : 𝕜) (↑((Fintype.card α).choose (Fintype.card α - r)) : 𝕜))
    1
rw₃ :
  HDiv.hDiv (α := 𝕜) (↑(#(falling (Fintype.card α - Fintype.card α) 𝒜)) : 𝕜)
      (↑((Fintype.card α).choose (Fintype.card α - Fintype.card α)) : 𝕜) ≤
    1
rw₄ : #(falling (Fintype.card α - Fintype.card α) 𝒜) ≤ 1 * (Fintype.card α).choose (Fintype.card α - Fintype.card α)
rw₅ rw₆ : 0 < (Fintype.card α).choose (Fintype.card α - Fintype.card α)
⊢ LE.le.{u_1} (α := 𝕜)
    (∑ r ∈ range (Fintype.card α + 1), HDiv.hDiv (α := 𝕜) (↑(#(𝒜 # r)) : 𝕜) (↑((Fintype.card α).choose r) : 𝕜)) 1

Tactic:
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

Premises used: div_le_iff₀, tsub_self, Finset.sum_flip, Nat.sub_self, zero_lt_one, Nat.choose_zero_right, one_mul, Finset.falling
-- Module: Mathlib.Combinatorics.SetFamily.LYM
Goal:
𝕜 : Type u_1
α : Type u_2
inst : Semifield 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : Fintype α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun (x1 x2 : Finset α) ↦ x1 ⊆ x2) (↑𝒜 : Set (Finset α))
h : ∀ i ∈ 𝒜, #i ∈ range (Fintype.card α + 1)
⊢ Eq.{u_1 + 1} (α := 𝕜) (∑ s ∈ 𝒜, (↑((Fintype.card α).choose #s) : 𝕜)⁻¹)
    (∑ r ∈ range (Fintype.card α + 1), ∑ s ∈ 𝒜 with #s = r, (↑((Fintype.card α).choose r) : 𝕜)⁻¹)

Tactic:
rw [sum_fiberwise_of_maps_to']

Premises used: Finset.sum_fiberwise_of_maps_to'
-- Module: Mathlib.Combinatorics.SetFamily.LYM
Goal:
𝕜 : Type u_1
α : Type u_2
inst : Semifield 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : Fintype α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun (x1 x2 : Finset α) ↦ x1 ⊆ x2) (↑𝒜 : Set (Finset α))
⊢ ∀ i ∈ 𝒜, #i ∈ range (Fintype.card α + 1)

Tactic:
simp [card_le_univ]

Premises used: Finset.card_le_univ
-- Module: Mathlib.Combinatorics.SetFamily.LYM
Goal:
𝕜 : Type u_1
α : Type u_2
inst : Semifield 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : Fintype α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun (x1 x2 : Finset α) ↦ x1 ⊆ x2) (↑𝒜 : Set (Finset α))
⊢ Eq.{u_1 + 1} (α := 𝕜) (∑ r ∈ range (Fintype.card α + 1), ∑ s ∈ 𝒜 with #s = r, (↑((Fintype.card α).choose r) : 𝕜)⁻¹)
    (∑ r ∈ range (Fintype.card α + 1), HDiv.hDiv (α := 𝕜) (↑(#(𝒜 # r)) : 𝕜) (↑((Fintype.card α).choose r) : 𝕜))

Tactic:
simp [slice, div_eq_mul_inv]

Premises used: Finset.slice, div_eq_mul_inv
-- Module: Mathlib.Combinatorics.SetFamily.LYM
Goal:
𝕜 : Type u_1
α : Type u_2
inst : Semifield 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : Fintype α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun (x1 x2 : Finset α) ↦ x1 ⊆ x2) (↑𝒜 : Set (Finset α))
⊢ LE.le.{u_1} (α := 𝕜)
    (∑ r ∈ range (Fintype.card α + 1), HDiv.hDiv (α := 𝕜) (↑(#(𝒜 # r)) : 𝕜) (↑((Fintype.card α).choose r) : 𝕜)) 1

Tactic:
lubell_yamamoto_meshalkin_inequality_sum_card_div_choose h𝒜

Premises used: Finset.lubell_yamamoto_meshalkin_inequality_sum_card_div_choose
-- Module: Mathlib.Combinatorics.SetFamily.LYM
Goal:
𝕜 : Type u_1
α : Type u_2
inst : Semifield 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : Fintype α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun (x1 x2 : Finset α) ↦ x1 ⊆ x2) (↑𝒜 : Set (Finset α))
_ :
  Eq.{u_1 + 1} (α := 𝕜) (∑ s ∈ 𝒜, (↑((Fintype.card α).choose #s) : 𝕜)⁻¹)
    (∑ r ∈ range (Fintype.card α + 1), ∑ s ∈ 𝒜 with #s = r, (↑((Fintype.card α).choose r) : 𝕜)⁻¹)
_₁ :
  Eq.{u_1 + 1} (α := 𝕜) (∑ r ∈ range (Fintype.card α + 1), ∑ s ∈ 𝒜 with #s = r, (↑((Fintype.card α).choose r) : 𝕜)⁻¹)
    (∑ r ∈ range (Fintype.card α + 1), HDiv.hDiv (α := 𝕜) (↑(#(𝒜 # r)) : 𝕜) (↑((Fintype.card α).choose r) : 𝕜))
⊢ LE.le.{u_1} (α := 𝕜) (∑ s ∈ 𝒜, (↑((Fintype.card α).choose #s) : 𝕜)⁻¹) 1

Tactic:
calc
    _ = ∑ r ∈ range (Fintype.card α + 1),
        ∑ s ∈ 𝒜 with #s = r, ((Fintype.card α).choose r : 𝕜)⁻¹ := by
      rw [sum_fiberwise_of_maps_to']; simp [card_le_univ]
    _ = ∑ r ∈ range (Fintype.card α + 1), (#(𝒜 # r) / (Fintype.card α).choose r : 𝕜) := by
      simp [slice, div_eq_mul_inv]
    _ ≤ 1 := lubell_yamamoto_meshalkin_inequality_sum_card_div_choose h𝒜

Premises used: Finset.lubell_yamamoto_meshalkin_inequality_sum_card_div_choose, Fintype.card, Finset.range, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Combinatorics.SetFamily.LYM
Goal:
α : Type u_2
inst : Fintype α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun (x1 x2 : Finset α) ↦ x1 ⊆ x2) (↑𝒜 : Set (Finset α))
⊢ LT.lt (α := ℚ≥0) 0 (↑((Fintype.card α).choose (Fintype.card α / 2)) : ℚ≥0)

Tactic:
have : 0 < ((Fintype.card α).choose (Fintype.card α / 2) : ℚ≥0) :=
    Nat.cast_pos.2 <| choose_pos (Nat.div_le_self _ _)
-- Module: Mathlib.Combinatorics.SetFamily.LYM
Goal:
α : Type u_2
inst : Fintype α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun (x1 x2 : Finset α) ↦ x1 ⊆ x2) (↑𝒜 : Set (Finset α))
this : LT.lt (α := ℚ≥0) 0 (↑((Fintype.card α).choose (Fintype.card α / 2)) : ℚ≥0)
h : ∀ (s : Finset α) (hs : s ∈ 𝒜), LT.lt (α := ℚ≥0) 0 (↑((Fintype.card α).choose #s) : ℚ≥0)
h₁ : ∀ (s : Finset α) (hs : s ∈ 𝒜), (Fintype.card α).choose #s ≤ (Fintype.card α).choose (Fintype.card α / 2)
⊢ LE.le (α := ℚ≥0) (∑ s ∈ 𝒜, (↑((Fintype.card α).choose (Fintype.card α / 2)) : ℚ≥0)⁻¹)
    (∑ s ∈ 𝒜, (↑((Fintype.card α).choose #s) : ℚ≥0)⁻¹)

Tactic:
gcongr with s hs
-- Module: Mathlib.Combinatorics.SetFamily.LYM
Goal:
α : Type u_2
inst : Fintype α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun (x1 x2 : Finset α) ↦ x1 ⊆ x2) (↑𝒜 : Set (Finset α))
this : LT.lt (α := ℚ≥0) 0 (↑((Fintype.card α).choose (Fintype.card α / 2)) : ℚ≥0)
s : Finset α
hs : s ∈ 𝒜
⊢ LT.lt (α := ℚ≥0) 0 (↑((Fintype.card α).choose #s) : ℚ≥0)

Tactic:
mod_cast choose_pos s.card_le_univ

Premises used: Nat.choose, congrArg, Nat.cast_lt._simp_1, cast, Fintype.card, Nat.cast, Nat.choose_pos, Finset.card_le_univ, LT.lt, Finset.card, congrFun', Nat.cast_zero, Eq.symm, Eq.trans