awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SetFamily.LYM
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r (↑𝒜 : Set (Finset α))
i : DecidableRel fun (x1 x2 : Finset α) ↦ x1 ⊆ x2 :=
  fun (x x_1 : Finset α) ↦ Classical.dec ((fun (x1 x2 : Finset α) ↦ x1 ⊆ x2) x x_1)
s : Finset α
hs : s ∈ ∂ 𝒜
t : Finset α
ht : t ∈ 𝒜 ∧ s ⊆ t
this : ∅ ∉ 𝒜
h : ∃ a ∉ s, insert a s = t
refine_2 :
  ∀ (a : α) (ha : a ∉ s) (ht : insert a s ∈ 𝒜 ∧ s ⊆ insert a s),
    Membership.mem (γ := Finset (Finset α)) (image (fun (a : α) ↦ insert a s) sᶜ) (insert a s)
⊢ Membership.mem (γ := Finset (Finset α)) (image (fun (a : α) ↦ insert a s) sᶜ) t

Tactic:
rcases h with ⟨a, ha, rfl⟩

Premises used: rfl
-- Module: Mathlib.Combinatorics.SetFamily.LYM
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r (↑𝒜 : Set (Finset α))
i : DecidableRel fun (x1 x2 : Finset α) ↦ x1 ⊆ x2 :=
  fun (x x_1 : Finset α) ↦ Classical.dec ((fun (x1 x2 : Finset α) ↦ x1 ⊆ x2) x x_1)
s : Finset α
hs : s ∈ ∂ 𝒜
this : ∅ ∉ 𝒜
a : α
ha : a ∉ s
ht : insert a s ∈ 𝒜 ∧ s ⊆ insert a s
⊢ Membership.mem (γ := Finset (Finset α)) (image (fun (a : α) ↦ insert a s) sᶜ) (insert a s)

Tactic:
mem_image_of_mem _ (mem_compl.2 ha)

Premises used: Iff.mpr, Finset.mem_compl, Finset.mem_image_of_mem
-- Module: Mathlib.Combinatorics.SetFamily.LYM
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r (↑𝒜 : Set (Finset α))
i : DecidableRel fun (x1 x2 : Finset α) ↦ x1 ⊆ x2 :=
  fun (x x_1 : Finset α) ↦ Classical.dec ((fun (x1 x2 : Finset α) ↦ x1 ⊆ x2) x x_1)
s : Finset α
hs : s ∈ ∂ 𝒜
this : ∅ ∉ 𝒜
a : α
ha : a ∉ s
ht : insert a s ∈ 𝒜 ∧ s ⊆ insert a s
⊢ Membership.mem (γ := Finset (Finset α)) (image (fun (a : α) ↦ insert a s) sᶜ) (insert a s)

Tactic:
exact mem_image_of_mem _ (mem_compl.2 ha)

Premises used: Iff.mpr, Finset.mem_compl, Finset.mem_image_of_mem
-- Module: Mathlib.Combinatorics.SetFamily.LYM
Goal:
𝕜 : Type u_1
α : Type u_2
inst : Semifield 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : DecidableEq α
inst_4 : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
hr : r ≠ 0
h𝒜 : Set.Sized r (↑𝒜 : Set (Finset α))
inl :
  ∀ (hr' : Fintype.card α < r),
    HDiv.hDiv (α := 𝕜) (↑(#𝒜) : 𝕜) (↑((Fintype.card α).choose r) : 𝕜) ≤
      HDiv.hDiv (α := 𝕜) (↑(#(∂ 𝒜)) : 𝕜) (↑((Fintype.card α).choose (r - 1)) : 𝕜)
inr :
  ∀ (hr' : r ≤ Fintype.card α),
    HDiv.hDiv (α := 𝕜) (↑(#𝒜) : 𝕜) (↑((Fintype.card α).choose r) : 𝕜) ≤
      HDiv.hDiv (α := 𝕜) (↑(#(∂ 𝒜)) : 𝕜) (↑((Fintype.card α).choose (r - 1)) : 𝕜)
⊢ HDiv.hDiv (α := 𝕜) (↑(#𝒜) : 𝕜) (↑((Fintype.card α).choose r) : 𝕜) ≤
    HDiv.hDiv (α := 𝕜) (↑(#(∂ 𝒜)) : 𝕜) (↑((Fintype.card α).choose (r - 1)) : 𝕜)

Tactic:
obtain hr' | hr' := lt_or_ge (Fintype.card α) r

Premises used: Fintype.card, lt_or_ge
-- Module: Mathlib.Combinatorics.SetFamily.LYM
Goal:
𝕜 : Type u_1
α : Type u_2
inst : Semifield 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : DecidableEq α
inst_4 : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
hr : r ≠ 0
h𝒜 : Set.Sized r (↑𝒜 : Set (Finset α))
hr' : Fintype.card α < r
inl : 0 ≤ HDiv.hDiv (α := 𝕜) (↑(#(∂ 𝒜)) : 𝕜) (↑((Fintype.card α).choose (r - 1)) : 𝕜)
⊢ HDiv.hDiv (α := 𝕜) (↑(#𝒜) : 𝕜) (↑((Fintype.card α).choose r) : 𝕜) ≤
    HDiv.hDiv (α := 𝕜) (↑(#(∂ 𝒜)) : 𝕜) (↑((Fintype.card α).choose (r - 1)) : 𝕜)

Tactic:
rw [choose_eq_zero_of_lt hr', cast_zero, div_zero]

Premises used: Nat.choose_eq_zero_of_lt, Nat.cast_zero, div_zero
-- Module: Mathlib.Combinatorics.SetFamily.LYM
Goal:
𝕜 : Type u_1
α : Type u_2
inst : Semifield 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : DecidableEq α
inst_4 : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
hr : r ≠ 0
h𝒜 : Set.Sized r (↑𝒜 : Set (Finset α))
hr' : Fintype.card α < r
⊢ 0 ≤ HDiv.hDiv (α := 𝕜) (↑(#(∂ 𝒜)) : 𝕜) (↑((Fintype.card α).choose (r - 1)) : 𝕜)

Tactic:
div_nonneg (cast_nonneg _) (cast_nonneg _)

Premises used: Nat.cast_nonneg, div_nonneg
-- Module: Mathlib.Combinatorics.SetFamily.LYM
Goal:
𝕜 : Type u_1
α : Type u_2
inst : Semifield 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : DecidableEq α
inst_4 : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
hr : r ≠ 0
h𝒜 : Set.Sized r (↑𝒜 : Set (Finset α))
hr' : Fintype.card α < r
⊢ 0 ≤ HDiv.hDiv (α := 𝕜) (↑(#(∂ 𝒜)) : 𝕜) (↑((Fintype.card α).choose (r - 1)) : 𝕜)

Tactic:
exact div_nonneg (cast_nonneg _) (cast_nonneg _)

Premises used: div_nonneg
-- Module: Mathlib.Combinatorics.SetFamily.LYM
Goal:
𝕜 : Type u_1
α : Type u_2
inst : Semifield 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : DecidableEq α
inst_4 : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
hr : r ≠ 0
h𝒜 : Set.Sized r (↑𝒜 : Set (Finset α))
hr' : r ≤ Fintype.card α
⊢ #𝒜 * r ≤ #(∂ 𝒜) * (Fintype.card α - r + 1)

Tactic:
replace h𝒜 := local_lubell_yamamoto_meshalkin_inequality_mul h𝒜
-- Module: Mathlib.Combinatorics.SetFamily.LYM
Goal:
𝕜 : Type u_1
α : Type u_2
inst : Semifield 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : DecidableEq α
inst_4 : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
hr : r ≠ 0
hr' : r ≤ Fintype.card α
h𝒜 : #𝒜 * r ≤ #(∂ 𝒜) * (Fintype.card α - r + 1)
inr :
  HMul.hMul (α := 𝕜) (↑(#𝒜) : 𝕜) (↑((Fintype.card α).choose (r - 1)) : 𝕜) ≤
    HMul.hMul (α := 𝕜) (↑(#(∂ 𝒜)) : 𝕜) (↑((Fintype.card α).choose r) : 𝕜)
inr₁ : LT.lt.{u_1} (α := 𝕜) 0 (↑((Fintype.card α).choose r) : 𝕜)
inr₂ : LT.lt.{u_1} (α := 𝕜) 0 (↑((Fintype.card α).choose (r - 1)) : 𝕜)
⊢ HDiv.hDiv (α := 𝕜) (↑(#𝒜) : 𝕜) (↑((Fintype.card α).choose r) : 𝕜) ≤
    HDiv.hDiv (α := 𝕜) (↑(#(∂ 𝒜)) : 𝕜) (↑((Fintype.card α).choose (r - 1)) : 𝕜)

Tactic:
rw [div_le_div_iff₀]

Premises used: div_le_div_iff₀
-- Module: Mathlib.Combinatorics.SetFamily.LYM
Goal:
𝕜 : Type u_1
α : Type u_2
inst : Semifield 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : DecidableEq α
inst_4 : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
hr : r ≠ 0
hr' : r ≤ Fintype.card α
h𝒜 : #𝒜 * r ≤ #(∂ 𝒜) * (Fintype.card α - r + 1)
inr : #𝒜 * (Fintype.card α).choose (r - 1) ≤ #(∂ 𝒜) * (Fintype.card α).choose r
⊢ HMul.hMul (α := 𝕜) (↑(#𝒜) : 𝕜) (↑((Fintype.card α).choose (r - 1)) : 𝕜) ≤
    HMul.hMul (α := 𝕜) (↑(#(∂ 𝒜)) : 𝕜) (↑((Fintype.card α).choose r) : 𝕜)

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 : DecidableEq α
inst_4 : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
hr : r ≠ 0
hr' : r ≤ Fintype.card α
h𝒜 : #𝒜 * r ≤ #(∂ 𝒜) * (Fintype.card α - r + 1)
inr : 0 < (Fintype.card α).choose r
⊢ LT.lt.{u_1} (α := 𝕜) 0 (↑((Fintype.card α).choose r) : 𝕜)

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 : DecidableEq α
inst_4 : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
hr : r ≠ 0
hr' : r ≤ Fintype.card α
h𝒜 : #𝒜 * r ≤ #(∂ 𝒜) * (Fintype.card α - r + 1)
inr : 0 < (Fintype.card α).choose (r - 1)
⊢ LT.lt.{u_1} (α := 𝕜) 0 (↑((Fintype.card α).choose (r - 1)) : 𝕜)

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 : DecidableEq α
inst_4 : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
hr : r ≠ 0
hr' : r ≤ Fintype.card α
h𝒜 : #𝒜 * r ≤ #(∂ 𝒜) * (Fintype.card α - r + 1)
inr :
  ∀ (hr : Ne (α := ℕ) 0 0) (hr' : 0 ≤ Fintype.card α) (h𝒜 : #𝒜 * 0 ≤ #(∂ 𝒜) * (Fintype.card α - 0 + 1)),
    #𝒜 * (Fintype.card α).choose (HSub.hSub (α := ℕ) 0 1) ≤ #(∂ 𝒜) * (Fintype.card α).choose 0
inr₁ :
  ∀ (r : ℕ) (hr : r + 1 ≠ 0) (hr' : r + 1 ≤ Fintype.card α)
    (h𝒜 : #𝒜 * (r + 1) ≤ #(∂ 𝒜) * (Fintype.card α - (r + 1) + 1)),
    #𝒜 * (Fintype.card α).choose (r + 1 - 1) ≤ #(∂ 𝒜) * (Fintype.card α).choose (r + 1)
⊢ #𝒜 * (Fintype.card α).choose (r - 1) ≤ #(∂ 𝒜) * (Fintype.card α).choose r

Tactic:
rcases r with - | r
-- Module: Mathlib.Combinatorics.SetFamily.LYM
Goal:
𝕜 : Type u_1
α : Type u_2
inst : Semifield 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : DecidableEq α
inst_4 : Fintype α
𝒜 : Finset (Finset α)
hr : Ne (α := ℕ) 0 0
hr' : 0 ≤ Fintype.card α
h𝒜 : #𝒜 * 0 ≤ #(∂ 𝒜) * (Fintype.card α - 0 + 1)
⊢ #𝒜 * (Fintype.card α).choose (HSub.hSub (α := ℕ) 0 1) ≤ #(∂ 𝒜) * (Fintype.card α).choose 0

Tactic:
(hr rfl).elim

Premises used: False.elim, rfl
-- Module: Mathlib.Combinatorics.SetFamily.LYM
Goal:
𝕜 : Type u_1
α : Type u_2
inst : Semifield 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : DecidableEq α
inst_4 : Fintype α
𝒜 : Finset (Finset α)
hr : Ne (α := ℕ) 0 0
hr' : 0 ≤ Fintype.card α
h𝒜 : #𝒜 * 0 ≤ #(∂ 𝒜) * (Fintype.card α - 0 + 1)
⊢ #𝒜 * (Fintype.card α).choose (HSub.hSub (α := ℕ) 0 1) ≤ #(∂ 𝒜) * (Fintype.card α).choose 0

Tactic:
exact (hr rfl).elim

Premises used: False.elim, rfl
-- Module: Mathlib.Combinatorics.SetFamily.LYM
Goal:
𝕜 : Type u_1
α : Type u_2
inst : Semifield 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : DecidableEq α
inst_4 : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
hr : r + 1 ≠ 0
hr' : r + 1 ≤ Fintype.card α
h𝒜 : #𝒜 * (r + 1) ≤ #(∂ 𝒜) * (Fintype.card α - (r + 1) + 1)
⊢ #𝒜 * (r + 1) ≤ #(∂ 𝒜) * (Fintype.card α - r)

Tactic:
rw [tsub_add_eq_add_tsub hr', add_tsub_add_eq_tsub_right] at h𝒜

Premises used: tsub_add_eq_add_tsub, add_tsub_add_eq_tsub_right
-- Module: Mathlib.Combinatorics.SetFamily.LYM
Goal:
𝕜 : Type u_1
α : Type u_2
inst : Semifield 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : DecidableEq α
inst_4 : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
hr : r + 1 ≠ 0
hr' : r + 1 ≤ Fintype.card α
h𝒜 : #𝒜 * (r + 1) ≤ #(∂ 𝒜) * (Fintype.card α - r)
apply : #𝒜 * (Fintype.card α).choose (r + 1 - 1) * (r + 1) ≤ #(∂ 𝒜) * (Fintype.card α).choose (r + 1) * (r + 1)
⊢ #𝒜 * (Fintype.card α).choose (r + 1 - 1) ≤ #(∂ 𝒜) * (Fintype.card α).choose (r + 1)

Tactic:
apply le_of_mul_le_mul_right _ (pos_iff_ne_zero.2 hr)

Premises used: Iff.mpr, le_of_mul_le_mul_right, pos_iff_ne_zero
-- Module: Mathlib.Combinatorics.SetFamily.LYM
Goal:
𝕜 : Type u_1
α : Type u_2
inst : Semifield 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : DecidableEq α
inst_4 : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
hr : r + 1 ≠ 0
hr' : r + 1 ≤ Fintype.card α
h𝒜 : #𝒜 * (r + 1) ≤ #(∂ 𝒜) * (Fintype.card α - r)
⊢ #𝒜 * (r + 1) * (Fintype.card α).choose r ≤ #(∂ 𝒜) * (Fintype.card α - r) * (Fintype.card α).choose r

Tactic:
Nat.mul_le_mul_right ((Fintype.card α).choose r) h𝒜

Premises used: Nat.choose, Nat.mul_le_mul_right, Fintype.card
-- Module: Mathlib.Combinatorics.SetFamily.LYM
Goal:
𝕜 : Type u_1
α : Type u_2
inst : Semifield 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : DecidableEq α
inst_4 : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
hr : r + 1 ≠ 0
hr' : r + 1 ≤ Fintype.card α
h𝒜 : #𝒜 * (r + 1) ≤ #(∂ 𝒜) * (Fintype.card α - r)
h : #𝒜 * (Fintype.card α).choose (r + 1 - 1) * (r + 1) = #𝒜 * (r + 1) * (Fintype.card α).choose r
h₁ : #(∂ 𝒜) * (Fintype.card α).choose (r + 1) * (r + 1) = #(∂ 𝒜) * (Fintype.card α - r) * (Fintype.card α).choose r
⊢ #𝒜 * (Fintype.card α).choose (r + 1 - 1) * (r + 1) ≤ #(∂ 𝒜) * (Fintype.card α).choose (r + 1) * (r + 1)

Tactic:
convert! Nat.mul_le_mul_right ((Fintype.card α).choose r) h𝒜 using 1

Premises used: Nat.choose, Nat.mul_le_mul_right, Fintype.card
-- Module: Mathlib.Combinatorics.SetFamily.LYM
Goal:
𝕜 : Type u_1
α : Type u_2
inst : Semifield 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : DecidableEq α
inst_4 : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
hr : r + 1 ≠ 0
hr' : r + 1 ≤ Fintype.card α
h𝒜 : #𝒜 * (r + 1) ≤ #(∂ 𝒜) * (Fintype.card α - r)
⊢ #𝒜 * (Fintype.card α).choose (r + 1 - 1) * (r + 1) = #𝒜 * (r + 1) * (Fintype.card α).choose r

Tactic:
simpa [mul_assoc, Nat.choose_succ_right_eq] using Or.inl (mul_comm _ _)

Premises used: mul_assoc, Nat.choose_succ_right_eq, mul_comm, Or.inl
-- Module: Mathlib.Combinatorics.SetFamily.LYM
Goal:
𝕜 : Type u_1
α : Type u_2
inst : Semifield 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : DecidableEq α
inst_4 : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
hr : r + 1 ≠ 0
hr' : r + 1 ≤ Fintype.card α
h𝒜 : #𝒜 * (r + 1) ≤ #(∂ 𝒜) * (Fintype.card α - r)
h : (Fintype.card α).choose r * (Fintype.card α - r) = (Fintype.card α - r) * (Fintype.card α).choose r ∨ #(∂ 𝒜) = 0
⊢ #(∂ 𝒜) * (Fintype.card α).choose (r + 1) * (r + 1) = #(∂ 𝒜) * (Fintype.card α - r) * (Fintype.card α).choose r

Tactic:
simp only [mul_assoc, choose_succ_right_eq, mul_eq_mul_left_iff]

Premises used: mul_assoc, mul_eq_mul_left_iff, Nat.choose_succ_right_eq
-- Module: Mathlib.Combinatorics.SetFamily.LYM
Goal:
𝕜 : Type u_1
α : Type u_2
inst : Semifield 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : DecidableEq α
inst_4 : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
hr : r + 1 ≠ 0
hr' : r + 1 ≤ Fintype.card α
h𝒜 : #𝒜 * (r + 1) ≤ #(∂ 𝒜) * (Fintype.card α - r)
⊢ (Fintype.card α).choose r * (Fintype.card α - r) = (Fintype.card α - r) * (Fintype.card α).choose r ∨ #(∂ 𝒜) = 0

Tactic:
Or.inl (mul_comm _ _)

Premises used: mul_comm, Or.inl
-- Module: Mathlib.Combinatorics.SetFamily.LYM
Goal:
𝕜 : Type u_1
α : Type u_2
inst : Semifield 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : DecidableEq α
inst_4 : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
hr : r + 1 ≠ 0
hr' : r + 1 ≤ Fintype.card α
h𝒜 : #𝒜 * (r + 1) ≤ #(∂ 𝒜) * (Fintype.card α - r)
⊢ (Fintype.card α).choose r * (Fintype.card α - r) = (Fintype.card α - r) * (Fintype.card α).choose r ∨ #(∂ 𝒜) = 0

Tactic:
exact Or.inl (mul_comm _ _)

Premises used: mul_comm, Or.inl
-- Module: Mathlib.Combinatorics.SetFamily.LYM
Goal:
𝕜 : Type u_1
α : Type u_2
inst : Semifield 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : DecidableEq α
inst_4 : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
hr : r ≠ 0
hr' : r ≤ Fintype.card α
h𝒜 : #𝒜 * r ≤ #(∂ 𝒜) * (Fintype.card α - r + 1)
⊢ 0 < (Fintype.card α).choose r

Tactic:
Nat.choose_pos hr'

Premises used: Nat.choose_pos
-- Module: Mathlib.Combinatorics.SetFamily.LYM
Goal:
𝕜 : Type u_1
α : Type u_2
inst : Semifield 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : DecidableEq α
inst_4 : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
hr : r ≠ 0
hr' : r ≤ Fintype.card α
h𝒜 : #𝒜 * r ≤ #(∂ 𝒜) * (Fintype.card α - r + 1)
⊢ 0 < (Fintype.card α).choose r

Tactic:
exact Nat.choose_pos hr'

Premises used: Nat.choose_pos
-- Module: Mathlib.Combinatorics.SetFamily.LYM
Goal:
𝕜 : Type u_1
α : Type u_2
inst : Semifield 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : DecidableEq α
inst_4 : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
hr : r ≠ 0
hr' : r ≤ Fintype.card α
h𝒜 : #𝒜 * r ≤ #(∂ 𝒜) * (Fintype.card α - r + 1)
⊢ 0 < (Fintype.card α).choose (r - 1)

Tactic:
Nat.choose_pos (r.pred_le.trans hr')

Premises used: Nat.choose_pos, Nat.pred_le, 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 : DecidableEq α
inst_4 : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
hr : r ≠ 0
hr' : r ≤ Fintype.card α
h𝒜 : #𝒜 * r ≤ #(∂ 𝒜) * (Fintype.card α - r + 1)
⊢ 0 < (Fintype.card α).choose (r - 1)

Tactic:
exact Nat.choose_pos (r.pred_le.trans hr')

Premises used: Nat.choose_pos, Nat.pred_le, LE.le.trans
-- Module: Mathlib.Combinatorics.SetFamily.LYM
Goal:
α : Type u_2
inst : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s : Finset α
⊢ s ∈ falling k 𝒜 ↔ (∃ t ∈ 𝒜, s ⊆ t) ∧ #s = k

Tactic:
grind [falling, mem_sup]

Premises used: Finset.mem_sup, Finset.falling
-- Module: Mathlib.Combinatorics.SetFamily.LYM
Goal:
α : Type u_2
inst : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
⊢ Set.Sized k (↑(falling k 𝒜) : Set (Finset α))

Tactic:
fun _ hs => (mem_falling.1 hs).2

Premises used: Set.Sized, And.right, Finset.mem_falling, Iff.mp
-- Module: Mathlib.Combinatorics.SetFamily.LYM
Goal:
α : Type u_2
inst : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
⊢ 𝒜 # k ⊆ falling k 𝒜

Tactic:
fun s hs =>
  mem_falling.2 <| (mem_slice.1 hs).imp_left fun h => ⟨s, h, Subset.refl _⟩

Premises used: Iff.mpr, Finset.Subset.refl, And.imp_left, Finset.mem_falling, And.intro, Exists.intro, Iff.mp, Finset.mem_slice
-- Module: Mathlib.Combinatorics.SetFamily.LYM
Goal:
α : Type u_2
inst : DecidableEq α
𝒜 : Finset (Finset α)
⊢ falling 0 𝒜 ⊆ {∅}

Tactic:
subset_singleton_iff'.2 fun _ ht => card_eq_zero.1 <| sized_falling _ _ ht

Premises used: Iff.mpr, Finset.card_eq_zero, Iff.mp, Finset.subset_singleton_iff', Finset.sized_falling, OfNat.ofNat
-- Module: Mathlib.Combinatorics.SetFamily.LYM
Goal:
α : Type u_2
inst : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
h : ∀ (s : Finset α), s ∈ 𝒜 # k ∪ ∂ (falling (k + 1) 𝒜) ↔ s ∈ falling k 𝒜
⊢ 𝒜 # k ∪ ∂ (falling (k + 1) 𝒜) = falling k 𝒜

Tactic:
ext s
-- Module: Mathlib.Combinatorics.SetFamily.LYM
Goal:
α : Type u_2
inst : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s : Finset α
h :
  (s ∈ 𝒜 ∧ #s = k ∨ ∃ (s_1 : Finset α), ((∃ t ∈ 𝒜, s_1 ⊆ t) ∧ #s_1 = k + 1) ∧ ∃ a ∈ s_1, s_1.erase a = s) ↔
    (∃ t ∈ 𝒜, s ⊆ t) ∧ #s = k
⊢ s ∈ 𝒜 # k ∪ ∂ (falling (k + 1) 𝒜) ↔ s ∈ falling k 𝒜

Tactic:
simp_rw [mem_union, mem_slice, mem_shadow_iff, mem_falling]

Premises used: Finset.mem_falling, Finset.mem_union, Finset.mem_slice, Finset.mem_shadow_iff
-- Module: Mathlib.Combinatorics.SetFamily.LYM
Goal:
α : Type u_2
inst : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s : Finset α
h :
  (s ∈ 𝒜 ∧ #s = k ∨ ∃ (s_1 : Finset α), ((∃ t ∈ 𝒜, s_1 ⊆ t) ∧ #s_1 = k + 1) ∧ ∃ a ∈ s_1, s_1.erase a = s) →
    (∃ t ∈ 𝒜, s ⊆ t) ∧ #s = k
h₁ :
  (∃ t ∈ 𝒜, s ⊆ t) ∧ #s = k →
    s ∈ 𝒜 ∧ #s = k ∨ ∃ (s_1 : Finset α), ((∃ t ∈ 𝒜, s_1 ⊆ t) ∧ #s_1 = k + 1) ∧ ∃ a ∈ s_1, s_1.erase a = s
⊢ (s ∈ 𝒜 ∧ #s = k ∨ ∃ (s_1 : Finset α), ((∃ t ∈ 𝒜, s_1 ⊆ t) ∧ #s_1 = k + 1) ∧ ∃ a ∈ s_1, s_1.erase a = s) ↔
    (∃ t ∈ 𝒜, s ⊆ t) ∧ #s = k

Tactic:
constructor
-- Module: Mathlib.Combinatorics.SetFamily.LYM
Goal:
α : Type u_2
inst : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s : Finset α
h : s ∈ 𝒜 ∧ #s = k
⊢ (∃ t ∈ 𝒜, s ⊆ t) ∧ #s = k

Tactic:
⟨⟨s, h.1, Subset.refl _⟩, h.2⟩

Premises used: Finset.Subset.refl, And.right, And.left, And.intro, Exists.intro
-- Module: Mathlib.Combinatorics.SetFamily.LYM
Goal:
α : Type u_2
inst : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s : Finset α
h : s ∈ 𝒜 ∧ #s = k
⊢ (∃ t ∈ 𝒜, s ⊆ t) ∧ #s = k

Tactic:
exact ⟨⟨s, h.1, Subset.refl _⟩, h.2⟩
-- Module: Mathlib.Combinatorics.SetFamily.LYM
Goal:
α : Type u_2
inst : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s : Finset α
hs : #s = k + 1
t : Finset α
ht : t ∈ 𝒜
hst : s ⊆ t
a : α
ha : a ∈ s
⊢ (∃ t ∈ 𝒜, s.erase a ⊆ t) ∧ #(s.erase a) = k

Tactic:
⟨⟨t, ht, (erase_subset _ _).trans hst⟩, ?_⟩

Premises used: HasSubset.Subset.trans, And.intro, Exists.intro, Finset.erase_subset
-- Module: Mathlib.Combinatorics.SetFamily.LYM
Goal:
α : Type u_2
inst : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s : Finset α
hs : #s = k + 1
t : Finset α
ht : t ∈ 𝒜
hst : s ⊆ t
a : α
ha : a ∈ s
h : #(s.erase a) = k
⊢ (∃ t ∈ 𝒜, s.erase a ⊆ t) ∧ #(s.erase a) = k

Tactic:
refine ⟨⟨t, ht, (erase_subset _ _).trans hst⟩, ?_⟩
-- Module: Mathlib.Combinatorics.SetFamily.LYM
Goal:
α : Type u_2
inst : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s : Finset α
hs : #s = k + 1
t : Finset α
ht : t ∈ 𝒜
hst : s ⊆ t
a : α
ha : a ∈ s
h : k + 1 - 1 = k
⊢ #(s.erase a) = k

Tactic:
rw [card_erase_of_mem ha, hs]

Premises used: Finset.card_erase_of_mem
-- Module: Mathlib.Combinatorics.SetFamily.LYM
Goal:
α : Type u_2
inst : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s : Finset α
hs : #s = k + 1
t : Finset α
ht : t ∈ 𝒜
hst : s ⊆ t
a : α
ha : a ∈ s
⊢ k + 1 - 1 = k

Tactic:
rfl
-- Module: Mathlib.Combinatorics.SetFamily.LYM
Goal:
α : Type u_2
inst : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s : Finset α
hs : #s = k
t : Finset α
ht : t ∈ 𝒜
hst : s ⊆ t
pos :
  ∀ (h : s ∈ 𝒜), s ∈ 𝒜 ∧ #s = k ∨ ∃ (s_1 : Finset α), ((∃ t ∈ 𝒜, s_1 ⊆ t) ∧ #s_1 = k + 1) ∧ ∃ a ∈ s_1, s_1.erase a = s
neg :
  ∀ (h : s ∉ 𝒜), s ∈ 𝒜 ∧ #s = k ∨ ∃ (s_1 : Finset α), ((∃ t ∈ 𝒜, s_1 ⊆ t) ∧ #s_1 = k + 1) ∧ ∃ a ∈ s_1, s_1.erase a = s
⊢ s ∈ 𝒜 ∧ #s = k ∨ ∃ (s_1 : Finset α), ((∃ t ∈ 𝒜, s_1 ⊆ t) ∧ #s_1 = k + 1) ∧ ∃ a ∈ s_1, s_1.erase a = s

Tactic:
by_cases h : s ∈ 𝒜
-- Module: Mathlib.Combinatorics.SetFamily.LYM
Goal:
α : Type u_2
inst : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s : Finset α
hs : #s = k
t : Finset α
ht : t ∈ 𝒜
hst : s ⊆ t
h : s ∈ 𝒜
⊢ s ∈ 𝒜 ∧ #s = k ∨ ∃ (s_1 : Finset α), ((∃ t ∈ 𝒜, s_1 ⊆ t) ∧ #s_1 = k + 1) ∧ ∃ a ∈ s_1, s_1.erase a = s

Tactic:
Or.inl ⟨h, hs⟩

Premises used: And.intro, Or.inl
-- Module: Mathlib.Combinatorics.SetFamily.LYM
Goal:
α : Type u_2
inst : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s : Finset α
hs : #s = k
t : Finset α
ht : t ∈ 𝒜
hst : s ⊆ t
h : s ∈ 𝒜
⊢ s ∈ 𝒜 ∧ #s = k ∨ ∃ (s_1 : Finset α), ((∃ t ∈ 𝒜, s_1 ⊆ t) ∧ #s_1 = k + 1) ∧ ∃ a ∈ s_1, s_1.erase a = s

Tactic:
exact Or.inl ⟨h, hs⟩

Premises used: Or.inl
-- Module: Mathlib.Combinatorics.SetFamily.LYM
Goal:
α : Type u_2
inst : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s : Finset α
hs : #s = k
t : Finset α
ht : t ∈ 𝒜
hst : s ⊆ t
h : s ∉ 𝒜
neg :
  ∀ (a : α) (ha : a ∉ s) (hst : insert a s ⊆ t),
    s ∈ 𝒜 ∧ #s = k ∨ ∃ (s_1 : Finset α), ((∃ t ∈ 𝒜, s_1 ⊆ t) ∧ #s_1 = k + 1) ∧ ∃ a ∈ s_1, s_1.erase a = s
⊢ s ∈ 𝒜 ∧ #s = k ∨ ∃ (s_1 : Finset α), ((∃ t ∈ 𝒜, s_1 ⊆ t) ∧ #s_1 = k + 1) ∧ ∃ a ∈ s_1, s_1.erase a = s

Tactic:
obtain ⟨a, ha, hst⟩ := ssubset_iff.1 (ssubset_of_subset_of_ne hst (ht.ne_of_notMem h).symm)

Premises used: Membership.mem.ne_of_notMem, Ne.symm, Finset.ssubset_iff, Iff.mp, ssubset_of_subset_of_ne
-- Module: Mathlib.Combinatorics.SetFamily.LYM
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
⊢ s ∈ 𝒜 ∧ #s = k ∨ ∃ (s_1 : Finset α), ((∃ t ∈ 𝒜, s_1 ⊆ t) ∧ #s_1 = k + 1) ∧ ∃ a ∈ s_1, s_1.erase a = s

Tactic:
Or.inr ⟨insert a s, ⟨⟨t, ht, hst⟩, ?_⟩, a, mem_insert_self _ _, erase_insert ha⟩

Premises used: Finset.mem_insert_self, Insert.insert, Finset.erase_insert, And.intro, Exists.intro, Or.inr
-- Module: Mathlib.Combinatorics.SetFamily.LYM
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 : #(insert a s) = k + 1
⊢ s ∈ 𝒜 ∧ #s = k ∨ ∃ (s_1 : Finset α), ((∃ t ∈ 𝒜, s_1 ⊆ t) ∧ #s_1 = k + 1) ∧ ∃ a ∈ s_1, s_1.erase a = s

Tactic:
refine Or.inr ⟨insert a s, ⟨⟨t, ht, hst⟩, ?_⟩, a, mem_insert_self _ _, erase_insert ha⟩

Premises used: Or.inr
-- Module: Mathlib.Combinatorics.SetFamily.LYM
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
neg₁ neg₂ : k + 1 = k + 1
⊢ #(insert a s) = k + 1

Tactic:
rw [card_insert_of_notMem ha, hs]

Premises used: Finset.card_insert_of_notMem
-- 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 α
h₁ : s ∈ ∂ (falling n 𝒜)
h₂ : s ∈ 𝒜 # m
⊢ ∃ (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₁

Premises used: Finset.mem_falling, Finset.mem_shadow_iff
-- 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 α
h₂ : s ∈ 𝒜 # m
h₁ : ∃ (s_1 : Finset α), ((∃ t ∈ 𝒜, s_1 ⊆ t) ∧ #s_1 = n) ∧ ∃ a ∈ s_1, s_1.erase a = s
obtain :
  ∀ (s : Finset α),
    #s = n → ∀ (t : Finset α) (ht : t ∈ 𝒜) (hst : s ⊆ t) (a : α) (ha : a ∈ s) (h₂ : s.erase a ∈ 𝒜 # m), False
⊢ False

Tactic:
obtain ⟨s, ⟨⟨t, ht, hst⟩, _⟩, a, ha, rfl⟩ := h₁

Premises used: rfl
-- 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
⊢ False

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

Premises used: Finset.slice_subset, HasSubset.Subset.trans, Finset.erase_subset