awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.LYM (goal)
Goal:
α : Type u_2
inst : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s : Finset α
hs : #s = k
t : Finset α
ht : t ∈ 𝒜
hst_1 : s ⊆ t
h : s ∉ 𝒜
a : α
ha : a ∉ s
hst : insert a s ⊆ t
⊢ #(insert a s) = k + 1
have neg : #s + 1 = k + 1
Tactic: rw [card_insert_of_notMem ha, hs]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.LYM (goal)
Goal:
α : Type u_2
inst : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s : Finset α
hs : #s = k
t : Finset α
ht : t ∈ 𝒜
hst_1 : s ⊆ t
h : s ∉ 𝒜
a : α
ha : a ∉ s
hst : insert a s ⊆ t
neg : #s + 1 = k + 1
⊢ #(insert a s) = k + 1
have neg₁ : k + 1 = k + 1
Tactic: rw [card_insert_of_notMem ha, hs]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.LYM (hypothesis)
Goal:
α : Type u_2
inst : DecidableEq α
𝒜 : Finset (Finset α)
m n : ℕ
h𝒜 : IsAntichain (fun (x1 x2 : Finset α) ↦ x1 ⊆ x2) (↑𝒜 : Set (Finset α))
s : Finset α
h₁ : s ∈ ∂ (falling n 𝒜)
h₂ : s ∈ 𝒜 # m
⊢ False
have h₃ : ∃ (s_1 : Finset α), ((∃ t ∈ 𝒜, s_1 ⊆ t) ∧ #s_1 = n) ∧ ∃ a ∈ s_1, s_1.erase a = s
Tactic: simp_rw [mem_shadow_iff, mem_falling] at h₁
Cleared hypotheses: h₁
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.LYM (goal)
Goal:
α : Type u_2
inst : DecidableEq α
𝒜 : Finset (Finset α)
m n : ℕ
h𝒜 : IsAntichain (fun (x1 x2 : Finset α) ↦ x1 ⊆ x2) (↑𝒜 : Set (Finset α))
s : Finset α
h₂ : s ∈ 𝒜 # m
h₁ : ∃ (s_1 : Finset α), ((∃ t ∈ 𝒜, s_1 ⊆ t) ∧ #s_1 = n) ∧ ∃ a ∈ s_1, s_1.erase a = s
⊢ False
have obtain : ∀ (s : Finset α),
  #s = n → ∀ (t : Finset α) (ht : t ∈ 𝒜) (hst : s ⊆ t) (a : α) (ha : a ∈ s) (h₂ : s.erase a ∈ 𝒜 # m), False
Tactic: obtain ⟨s, ⟨⟨t, ht, hst⟩, _⟩, a, ha, rfl⟩ := h₁
Cleared hypotheses: s, h₂, h₁
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.LYM (goal)
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
⊢ False
have refine : s.erase a ≠ t
Tactic: refine h𝒜 (slice_subset h₂) ht ?_ ((erase_subset _ _).trans hst)
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.LYM (goal)
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 α
⊢ ∑ 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)) : 𝕜)
have zero : #(𝒜 # Fintype.card α) ≤ #(falling (Fintype.card α) 𝒜)
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]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.LYM (goal)
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 α
⊢ ∑ 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))) : 𝕜)
have 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))) : 𝕜)
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]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.LYM (goal)
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 α
⊢ 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))) : 𝕜)
have 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)) : 𝕜)
Tactic: rw [← tsub_tsub, tsub_add_cancel_of_le (le_tsub_of_add_le_left hk)]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.LYM (goal)
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 α
⊢ 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)) : 𝕜)
have 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)) : 𝕜)
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 _ _]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.LYM (goal)
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)) : 𝕜)
⊢ 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)) : 𝕜)
have 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)) : 𝕜)
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 _ _]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.LYM (goal)
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 α))
⊢ ∑ 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)) : 𝕜)
have 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)) : 𝕜)
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 _ _]
Cleared hypotheses: hk
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.LYM (goal)
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)) : 𝕜)
⊢ ∑ 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)) : 𝕜)
have 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))) : 𝕜)
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 _ _]
Cleared hypotheses: hk
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.LYM (goal)
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
have rw : LE.le.{u_1} (α := 𝕜)
  (∑ r ∈ range (Fintype.card α + 1),
    HDiv.hDiv (α := 𝕜) (↑(#(𝒜 # (Fintype.card α - r))) : 𝕜) (↑((Fintype.card α).choose (Fintype.card α - r)) : 𝕜))
  1
Tactic: rw [← sum_flip]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.LYM (goal)
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
have refine : HDiv.hDiv (α := 𝕜) (↑(#(falling (Fintype.card α - Fintype.card α) 𝒜)) : 𝕜)
    (↑((Fintype.card α).choose (Fintype.card α - Fintype.card α)) : 𝕜) ≤
  1
Tactic: refine (le_card_falling_div_choose le_rfl h𝒜).trans ?_
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.LYM (goal)
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 α))
⊢ HDiv.hDiv (α := 𝕜) (↑(#(falling (Fintype.card α - Fintype.card α) 𝒜)) : 𝕜)
      (↑((Fintype.card α).choose (Fintype.card α - Fintype.card α)) : 𝕜) ≤
    1
have rw : (↑(#(falling (Fintype.card α - Fintype.card α) 𝒜)) : 𝕜) ≤
  HMul.hMul (α := 𝕜) 1 (↑((Fintype.card α).choose (Fintype.card α - Fintype.card α)) : 𝕜)
Tactic: rw [div_le_iff₀]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.LYM (goal)
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 α)) : 𝕜)
⊢ HDiv.hDiv (α := 𝕜) (↑(#(falling (Fintype.card α - Fintype.card α) 𝒜)) : 𝕜)
      (↑((Fintype.card α).choose (Fintype.card α - Fintype.card α)) : 𝕜) ≤
    1
have rw₁ : LT.lt.{u_1} (α := 𝕜) 0 (↑((Fintype.card α).choose (Fintype.card α - Fintype.card α)) : 𝕜)
Tactic: rw [div_le_iff₀]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.LYM (goal)
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 α) 𝒜)) : 𝕜) ≤
    HMul.hMul (α := 𝕜) 1 (↑((Fintype.card α).choose (Fintype.card α - Fintype.card α)) : 𝕜)
have norm_cast : #(falling (Fintype.card α - Fintype.card α) 𝒜) ≤ 1 * (Fintype.card α).choose (Fintype.card α - Fintype.card α)
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.LYM (goal)
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.{u_1} (α := 𝕜) 0 (↑((Fintype.card α).choose (Fintype.card α - Fintype.card α)) : 𝕜)
have norm_cast : 0 < (Fintype.card α).choose (Fintype.card α - Fintype.card α)
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.LYM (goal)
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 α))
⊢ 0 < (Fintype.card α).choose (Fintype.card α - Fintype.card α)
have rw : LT.lt (α := ℕ) 0 1
Tactic: rw [tsub_self, choose_zero_right]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.LYM (goal)
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
have rw : LE.le.{u_1} (α := 𝕜)
  (∑ r ∈ range (Fintype.card α + 1),
    HDiv.hDiv (α := 𝕜) (↑(#(𝒜 # (Fintype.card α - r))) : 𝕜) (↑((Fintype.card α).choose (Fintype.card α - 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
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.LYM (goal)
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
⊢ LE.le.{u_1} (α := 𝕜)
    (∑ r ∈ range (Fintype.card α + 1), HDiv.hDiv (α := 𝕜) (↑(#(𝒜 # r)) : 𝕜) (↑((Fintype.card α).choose r) : 𝕜)) 1
have rw₃ : HDiv.hDiv (α := 𝕜) (↑(#(falling (Fintype.card α - Fintype.card α) 𝒜)) : 𝕜)
    (↑((Fintype.card α).choose (Fintype.card α - Fintype.card α)) : 𝕜) ≤
  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
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.LYM (goal)
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
⊢ LE.le.{u_1} (α := 𝕜)
    (∑ r ∈ range (Fintype.card α + 1), HDiv.hDiv (α := 𝕜) (↑(#(𝒜 # r)) : 𝕜) (↑((Fintype.card α).choose r) : 𝕜)) 1
have rw₄ : #(falling (Fintype.card α - Fintype.card α) 𝒜) ≤ 1 * (Fintype.card α).choose (Fintype.card α - Fintype.card α)
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
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.LYM (goal)
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 α)
⊢ LE.le.{u_1} (α := 𝕜)
    (∑ r ∈ range (Fintype.card α + 1), HDiv.hDiv (α := 𝕜) (↑(#(𝒜 # r)) : 𝕜) (↑((Fintype.card α).choose r) : 𝕜)) 1
have rw₅ : 0 < (Fintype.card α).choose (Fintype.card α - Fintype.card α)
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
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.LYM (goal)
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) : 𝕜)⁻¹)
have h : ∀ i ∈ 𝒜, #i ∈ range (Fintype.card α + 1)
Tactic: rw [sum_fiberwise_of_maps_to']