awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.LYM (goal)
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 ∈ 𝒜
⊢ r ≤ #(bipartiteBelow (fun (x1 x2 : Finset α) ↦ x1 ⊆ x2) (∂ 𝒜) s)
have refine_1 : #(image s.erase s) ≤ #(bipartiteBelow (fun (x1 x2 : Finset α) ↦ x1 ⊆ x2) (∂ 𝒜) s)
Tactic: rw [← h𝒜 hs, ← card_image_of_injOn s.erase_injOn]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.LYM (goal)
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 ∈ 𝒜
⊢ #(image s.erase s) ≤ #(bipartiteBelow (fun (x1 x2 : Finset α) ↦ x1 ⊆ x2) (∂ 𝒜) s)
have refine_1 : image s.erase s ⊆ bipartiteBelow (fun (x1 x2 : Finset α) ↦ x1 ⊆ x2) (∂ 𝒜) s
Tactic: refine card_le_card ?_
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.LYM (goal)
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 ∈ 𝒜
⊢ image s.erase s ⊆ bipartiteBelow (fun (x1 x2 : Finset α) ↦ x1 ⊆ x2) (∂ 𝒜) s
have refine_1 : ∀ x ∈ s, s.erase x ∈ ∂ 𝒜 ∧ s.erase x ⊆ s
Tactic: simp_rw [image_subset_iff, mem_bipartiteBelow]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.LYM (goal)
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 ∈ ∂ 𝒜
⊢ #(bipartiteAbove (fun (x1 x2 : Finset α) ↦ x1 ⊆ x2) 𝒜 s) ≤ Fintype.card α - r + 1
have refine_2 : #(bipartiteAbove (fun (x1 x2 : Finset α) ↦ x1 ⊆ x2) 𝒜 s) ≤ Fintype.card α - (r - 1)
Tactic: refine le_trans ?_ tsub_tsub_le_tsub_add
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.LYM (goal)
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 ∈ ∂ 𝒜
⊢ #(bipartiteAbove (fun (x1 x2 : Finset α) ↦ x1 ⊆ x2) 𝒜 s) ≤ Fintype.card α - (r - 1)
have refine_2 : #(bipartiteAbove (fun (x1 x2 : Finset α) ↦ x1 ⊆ x2) 𝒜 s) ≤ card (α := Finset α) (image (fun (a : α) ↦ insert a s) sᶜ)
Tactic: rw [← (Set.Sized.shadow h𝒜) hs, ← card_compl, ← card_image_of_injOn (insert_inj_on' _)]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.LYM (goal)
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 ∈ ∂ 𝒜
⊢ #(bipartiteAbove (fun (x1 x2 : Finset α) ↦ x1 ⊆ x2) 𝒜 s) ≤ card (α := Finset α) (image (fun (a : α) ↦ insert a s) sᶜ)
have refine_2 : ∀ (t : Finset α) (ht : t ∈ bipartiteAbove (fun (x1 x2 : Finset α) ↦ x1 ⊆ x2) 𝒜 s),
  Membership.mem (γ := Finset (Finset α)) (image (fun (a : α) ↦ insert a s) sᶜ) t
Tactic: refine card_le_card fun t ht => ?_
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.LYM (hypothesis)
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 ∈ bipartiteAbove (fun (x1 x2 : Finset α) ↦ x1 ⊆ x2) 𝒜 s
⊢ Membership.mem (γ := Finset (Finset α)) (image (fun (a : α) ↦ insert a s) sᶜ) t
have ht₁ : t ∈ 𝒜 ∧ s ⊆ t
Tactic: rw [mem_bipartiteAbove] at ht
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.LYM (goal)
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
⊢ ∅ ∉ 𝒜
have rw : ¬𝒜 = {∅}
Tactic: rw [← mem_coe, h𝒜.empty_mem_iff, coe_eq_singleton]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.LYM (hypothesis)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
r : ℕ
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 t : Finset α
h𝒜 : Set.Sized r (↑{∅} : Set (Finset α))
hs : Membership.mem (γ := Finset (Finset α)) (∂ {∅}) s
ht : Membership.mem (γ := Finset (Finset α)) {∅} t ∧ s ⊆ t
⊢ False
have hs₁ : Membership.mem (γ := Finset (Finset α)) ∅ s
Tactic: rw [shadow_singleton_empty] at hs
Cleared hypotheses: hs, ht
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.LYM (hypothesis)
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
⊢ Membership.mem (γ := Finset (Finset α)) (image (fun (a : α) ↦ insert a s) sᶜ) t
have this : ∅ ∉ 𝒜
Tactic: have : ∅ ∉ 𝒜 := by
    rw [← mem_coe, h𝒜.empty_mem_iff, coe_eq_singleton]
    rintro rfl
    rw [shadow_singleton_empty] at hs
    exact notMem_empty s hs
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.LYM (goal)
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 : ∅ ∉ 𝒜
⊢ #s + 1 = #t
have rw : #s + 1 = r - 1 + 1
Tactic: rw [(sized_shadow_iff this).1 (Set.Sized.shadow h𝒜) ht.1, (Set.Sized.shadow h𝒜) hs]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.LYM (goal)
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 : ∅ ∉ 𝒜
rw : #s + 1 = r - 1 + 1
⊢ #s + 1 = #t
have rw₁ : r - 1 + 1 = r - 1 + 1
Tactic: rw [(sized_shadow_iff this).1 (Set.Sized.shadow h𝒜) ht.1, (Set.Sized.shadow h𝒜) hs]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.LYM (hypothesis)
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 : ∅ ∉ 𝒜
⊢ Membership.mem (γ := Finset (Finset α)) (image (fun (a : α) ↦ insert a s) sᶜ) t
have h : ∃ a ∉ s, insert a s = t
Tactic: 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]⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.LYM (goal)
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
⊢ Membership.mem (γ := Finset (Finset α)) (image (fun (a : α) ↦ insert a s) sᶜ) t
have 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)
Tactic: rcases h with ⟨a, ha, rfl⟩
Cleared hypotheses: t, ht, h
-- 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 α
inst_4 : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
hr : r ≠ 0
h𝒜 : Set.Sized r (↑𝒜 : Set (Finset α))
⊢ HDiv.hDiv (α := 𝕜) (↑(#𝒜) : 𝕜) (↑((Fintype.card α).choose r) : 𝕜) ≤
    HDiv.hDiv (α := 𝕜) (↑(#(∂ 𝒜)) : 𝕜) (↑((Fintype.card α).choose (r - 1)) : 𝕜)
have inl : ∀ (hr' : Fintype.card α < r),
  HDiv.hDiv (α := 𝕜) (↑(#𝒜) : 𝕜) (↑((Fintype.card α).choose r) : 𝕜) ≤
    HDiv.hDiv (α := 𝕜) (↑(#(∂ 𝒜)) : 𝕜) (↑((Fintype.card α).choose (r - 1)) : 𝕜)
Tactic: obtain hr' | hr' := lt_or_ge (Fintype.card α) r
-- 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 α
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)) : 𝕜)
⊢ HDiv.hDiv (α := 𝕜) (↑(#𝒜) : 𝕜) (↑((Fintype.card α).choose r) : 𝕜) ≤
    HDiv.hDiv (α := 𝕜) (↑(#(∂ 𝒜)) : 𝕜) (↑((Fintype.card α).choose (r - 1)) : 𝕜)
have inr : ∀ (hr' : r ≤ Fintype.card α),
  HDiv.hDiv (α := 𝕜) (↑(#𝒜) : 𝕜) (↑((Fintype.card α).choose r) : 𝕜) ≤
    HDiv.hDiv (α := 𝕜) (↑(#(∂ 𝒜)) : 𝕜) (↑((Fintype.card α).choose (r - 1)) : 𝕜)
Tactic: obtain hr' | hr' := lt_or_ge (Fintype.card α) r
-- 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 α
inst_4 : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
hr : r ≠ 0
h𝒜 : Set.Sized r (↑𝒜 : Set (Finset α))
hr' : Fintype.card α < r
⊢ HDiv.hDiv (α := 𝕜) (↑(#𝒜) : 𝕜) (↑((Fintype.card α).choose r) : 𝕜) ≤
    HDiv.hDiv (α := 𝕜) (↑(#(∂ 𝒜)) : 𝕜) (↑((Fintype.card α).choose (r - 1)) : 𝕜)
have inl : 0 ≤ HDiv.hDiv (α := 𝕜) (↑(#(∂ 𝒜)) : 𝕜) (↑((Fintype.card α).choose (r - 1)) : 𝕜)
Tactic: rw [choose_eq_zero_of_lt hr', cast_zero, div_zero]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.LYM (hypothesis)
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 α
⊢ HDiv.hDiv (α := 𝕜) (↑(#𝒜) : 𝕜) (↑((Fintype.card α).choose r) : 𝕜) ≤
    HDiv.hDiv (α := 𝕜) (↑(#(∂ 𝒜)) : 𝕜) (↑((Fintype.card α).choose (r - 1)) : 𝕜)
have h𝒜₁ : #𝒜 * r ≤ #(∂ 𝒜) * (Fintype.card α - r + 1)
Tactic: replace h𝒜 := local_lubell_yamamoto_meshalkin_inequality_mul h𝒜
Cleared hypotheses: h𝒜
-- 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 α
inst_4 : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
hr : r ≠ 0
hr' : r ≤ Fintype.card α
h𝒜 : #𝒜 * r ≤ #(∂ 𝒜) * (Fintype.card α - r + 1)
⊢ HDiv.hDiv (α := 𝕜) (↑(#𝒜) : 𝕜) (↑((Fintype.card α).choose r) : 𝕜) ≤
    HDiv.hDiv (α := 𝕜) (↑(#(∂ 𝒜)) : 𝕜) (↑((Fintype.card α).choose (r - 1)) : 𝕜)
have inr : HMul.hMul (α := 𝕜) (↑(#𝒜) : 𝕜) (↑((Fintype.card α).choose (r - 1)) : 𝕜) ≤
  HMul.hMul (α := 𝕜) (↑(#(∂ 𝒜)) : 𝕜) (↑((Fintype.card α).choose r) : 𝕜)
Tactic: rw [div_le_div_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 : 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) : 𝕜)
⊢ HDiv.hDiv (α := 𝕜) (↑(#𝒜) : 𝕜) (↑((Fintype.card α).choose r) : 𝕜) ≤
    HDiv.hDiv (α := 𝕜) (↑(#(∂ 𝒜)) : 𝕜) (↑((Fintype.card α).choose (r - 1)) : 𝕜)
have inr₁ : LT.lt.{u_1} (α := 𝕜) 0 (↑((Fintype.card α).choose r) : 𝕜)
Tactic: rw [div_le_div_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 : 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) : 𝕜)
⊢ HDiv.hDiv (α := 𝕜) (↑(#𝒜) : 𝕜) (↑((Fintype.card α).choose r) : 𝕜) ≤
    HDiv.hDiv (α := 𝕜) (↑(#(∂ 𝒜)) : 𝕜) (↑((Fintype.card α).choose (r - 1)) : 𝕜)
have inr₂ : LT.lt.{u_1} (α := 𝕜) 0 (↑((Fintype.card α).choose (r - 1)) : 𝕜)
Tactic: rw [div_le_div_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 : DecidableEq α
inst_4 : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
hr : r ≠ 0
hr' : r ≤ Fintype.card α
h𝒜 : #𝒜 * r ≤ #(∂ 𝒜) * (Fintype.card α - r + 1)
⊢ HMul.hMul (α := 𝕜) (↑(#𝒜) : 𝕜) (↑((Fintype.card α).choose (r - 1)) : 𝕜) ≤
    HMul.hMul (α := 𝕜) (↑(#(∂ 𝒜)) : 𝕜) (↑((Fintype.card α).choose r) : 𝕜)
have inr : #𝒜 * (Fintype.card α).choose (r - 1) ≤ #(∂ 𝒜) * (Fintype.card α).choose r
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 : DecidableEq α
inst_4 : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
hr : r ≠ 0
hr' : r ≤ Fintype.card α
h𝒜 : #𝒜 * r ≤ #(∂ 𝒜) * (Fintype.card α - r + 1)
⊢ LT.lt.{u_1} (α := 𝕜) 0 (↑((Fintype.card α).choose r) : 𝕜)
have inr : 0 < (Fintype.card α).choose r
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 : DecidableEq α
inst_4 : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
hr : r ≠ 0
hr' : r ≤ Fintype.card α
h𝒜 : #𝒜 * r ≤ #(∂ 𝒜) * (Fintype.card α - r + 1)
⊢ LT.lt.{u_1} (α := 𝕜) 0 (↑((Fintype.card α).choose (r - 1)) : 𝕜)
have inr : 0 < (Fintype.card α).choose (r - 1)
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 : DecidableEq α
inst_4 : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
hr : r ≠ 0
hr' : r ≤ Fintype.card α
h𝒜 : #𝒜 * r ≤ #(∂ 𝒜) * (Fintype.card α - r + 1)
⊢ #𝒜 * (Fintype.card α).choose (r - 1) ≤ #(∂ 𝒜) * (Fintype.card α).choose r
have 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
Tactic: rcases r with - | r
Cleared hypotheses: r, hr, hr', h𝒜
-- 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 α
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
⊢ #𝒜 * (Fintype.card α).choose (r - 1) ≤ #(∂ 𝒜) * (Fintype.card α).choose r
have 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)
Tactic: rcases r with - | r
Cleared hypotheses: r, hr, hr', h𝒜
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.LYM (hypothesis)
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)
⊢ #𝒜 * (Fintype.card α).choose (r + 1 - 1) ≤ #(∂ 𝒜) * (Fintype.card α).choose (r + 1)
have h𝒜₁ : #𝒜 * (r + 1) ≤ #(∂ 𝒜) * (Fintype.card α - r)
Tactic: rw [tsub_add_eq_add_tsub hr', add_tsub_add_eq_tsub_right] at h𝒜
Cleared hypotheses: h𝒜
-- 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 α
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) ≤ #(∂ 𝒜) * (Fintype.card α).choose (r + 1)
have apply : #𝒜 * (Fintype.card α).choose (r + 1 - 1) * (r + 1) ≤ #(∂ 𝒜) * (Fintype.card α).choose (r + 1) * (r + 1)
Tactic: apply le_of_mul_le_mul_right _ (pos_iff_ne_zero.2 hr)
-- 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 α
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) ≤ #(∂ 𝒜) * (Fintype.card α).choose (r + 1) * (r + 1)
have h : #𝒜 * (Fintype.card α).choose (r + 1 - 1) * (r + 1) = #𝒜 * (r + 1) * (Fintype.card α).choose r
Tactic: convert! Nat.mul_le_mul_right ((Fintype.card α).choose r) h𝒜 using 1
-- 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 α
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
⊢ #𝒜 * (Fintype.card α).choose (r + 1 - 1) * (r + 1) ≤ #(∂ 𝒜) * (Fintype.card α).choose (r + 1) * (r + 1)
have h₁ : #(∂ 𝒜) * (Fintype.card α).choose (r + 1) * (r + 1) = #(∂ 𝒜) * (Fintype.card α - r) * (Fintype.card α).choose r
Tactic: convert! Nat.mul_le_mul_right ((Fintype.card α).choose r) h𝒜 using 1
-- 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 α
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) * (r + 1) = #(∂ 𝒜) * (Fintype.card α - r) * (Fintype.card α).choose r
have h : (Fintype.card α).choose r * (Fintype.card α - r) = (Fintype.card α - r) * (Fintype.card α).choose r ∨ #(∂ 𝒜) = 0
Tactic: simp only [mul_assoc, choose_succ_right_eq, mul_eq_mul_left_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.LYM (goal)
Goal:
α : Type u_2
inst : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
⊢ 𝒜 # k ∪ ∂ (falling (k + 1) 𝒜) = falling k 𝒜
have h : ∀ (s : Finset α), s ∈ 𝒜 # k ∪ ∂ (falling (k + 1) 𝒜) ↔ s ∈ falling k 𝒜
Tactic: ext s
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.LYM (goal)
Goal:
α : Type u_2
inst : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s : Finset α
⊢ s ∈ 𝒜 # k ∪ ∂ (falling (k + 1) 𝒜) ↔ s ∈ falling k 𝒜
have 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
Tactic: simp_rw [mem_union, mem_slice, mem_shadow_iff, mem_falling]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.LYM (goal)
Goal:
α : Type u_2
inst : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s : Finset α
⊢ (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
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.LYM (goal)
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 ∈ 𝒜 ∧ #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
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.LYM (goal)
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
have h : #(s.erase a) = k
Tactic: refine ⟨⟨t, ht, (erase_subset _ _).trans hst⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.LYM (goal)
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
⊢ #(s.erase a) = k
have h : k + 1 - 1 = k
Tactic: rw [card_erase_of_mem 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 : s ⊆ t
⊢ s ∈ 𝒜 ∧ #s = k ∨ ∃ (s_1 : Finset α), ((∃ t ∈ 𝒜, s_1 ⊆ t) ∧ #s_1 = k + 1) ∧ ∃ a ∈ s_1, s_1.erase a = s
have 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
Tactic: by_cases h : s ∈ 𝒜
-- 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 : 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
⊢ s ∈ 𝒜 ∧ #s = k ∨ ∃ (s_1 : Finset α), ((∃ t ∈ 𝒜, s_1 ⊆ t) ∧ #s_1 = k + 1) ∧ ∃ a ∈ s_1, s_1.erase a = s
have 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
Tactic: by_cases h : s ∈ 𝒜
-- 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 : 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
have 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
Tactic: obtain ⟨a, ha, hst⟩ := ssubset_iff.1 (ssubset_of_subset_of_ne hst (ht.ne_of_notMem h).symm)
-- 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
⊢ s ∈ 𝒜 ∧ #s = k ∨ ∃ (s_1 : Finset α), ((∃ t ∈ 𝒜, s_1 ⊆ t) ∧ #s_1 = k + 1) ∧ ∃ a ∈ s_1, s_1.erase a = s
have neg : #(insert a s) = k + 1
Tactic: refine Or.inr ⟨insert a s, ⟨⟨t, ht, hst⟩, ?_⟩, a, mem_insert_self _ _, erase_insert ha⟩