awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (goal)
Goal:
n r k i : ℕ
𝒜 : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r (↑𝒜 : Set (Finset (Fin n)))
h₂ : k.choose r ≤ #𝒜
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
this : Set.Sized r (↑𝒞 : Set (Finset (Fin n)))
_ : k.choose (r - i) = #(powersetCard (r - i) range'k)
_₁ : #(powersetCard (r - i) range'k) = #(∂^[i] 𝒞)
⊢ k.choose (r - i) ≤ #(∂^[i] 𝒜)
have _₂ : #(∂^[i] 𝒞) ≤ #(∂^[i] 𝒜)
Tactic: calc
    k.choose (r - i)
    _ = #(powersetCard (r - i) range'k) := by rw [card_powersetCard, card_attachFin, card_range]
    _ = #(∂^[i] 𝒞) := by
      congr!
      ext B
      rw [mem_powersetCard, mem_shadow_iterate_iff_exists_sdiff]
      constructor
      · rintro ⟨hBk, hB⟩
        have := exists_subsuperset_card_eq hBk (Nat.le_add_left _ i) <| by
          rwa [hB, card_attachFin, card_range, ← Nat.add_sub_assoc hir, Nat.add_sub_cancel_left]
        obtain ⟨C, BsubC, hCrange, hcard⟩ := this
        rw [hB, ← Nat.add_sub_assoc hir, Nat.add_sub_cancel_left] at hcard
        refine ⟨C, mem_powersetCard.2 ⟨hCrange, hcard⟩, BsubC, ?_⟩
        rw [card_sdiff_of_subset BsubC, hcard, hB, Nat.sub_sub_self hir]
      · rintro ⟨A, Ah, hBA, card_sdiff_i⟩
        rw [mem_powersetCard] at Ah
        refine ⟨hBA.trans Ah.1, eq_tsub_of_add_eq ?_⟩
        rw [← Ah.2, ← card_sdiff_i, add_comm, card_sdiff_add_card_eq_card hBA]
    _ ≤ #(∂^[i] 𝒜) := by
      refine iterated_kk h₁ ?_ ⟨‹_›, ?_⟩
      · rwa [card_powersetCard, card_attachFin, card_range]
      simp_rw [𝒞, mem_powersetCard]
      rintro A B hA ⟨HB₁, HB₂⟩
      refine ⟨fun t ht ↦ ?_, ‹_›⟩
      rw [mem_attachFin, mem_range]
      have : toColex (image Fin.val B) < toColex (image Fin.val A) := by
        rwa [toColex_image_lt_toColex_image Fin.val_strictMono]
      apply Colex.forall_lt_mono this.le _ t (mem_image.2 ⟨t, ht, rfl⟩)
      simp_rw [mem_image]
      rintro _ ⟨a, ha, hab⟩
      simpa [range'k, hab] using hA.1 ha
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (goal)
Goal:
n : ℕ
𝒜 : Finset (Finset (Fin n))
r : ℕ
h𝒜 : (↑𝒜 : Set (Finset (Fin n))).Intersecting
h₂ : Set.Sized r (↑𝒜 : Set (Finset (Fin n)))
h₃ : r ≤ n / 2
⊢ #𝒜 ≤ (n - 1).choose (r - 1)
have inl : ∀ (b : r = 0), #𝒜 ≤ (n - 1).choose (r - 1)
Tactic: rcases Nat.eq_zero_or_pos r with b | h1r
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (goal)
Goal:
n : ℕ
𝒜 : Finset (Finset (Fin n))
r : ℕ
h𝒜 : (↑𝒜 : Set (Finset (Fin n))).Intersecting
h₂ : Set.Sized r (↑𝒜 : Set (Finset (Fin n)))
h₃ : r ≤ n / 2
inl : ∀ (b : r = 0), #𝒜 ≤ (n - 1).choose (r - 1)
⊢ #𝒜 ≤ (n - 1).choose (r - 1)
have inr : ∀ (h1r : r > 0), #𝒜 ≤ (n - 1).choose (r - 1)
Tactic: rcases Nat.eq_zero_or_pos r with b | h1r
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (goal)
Goal:
n : ℕ
𝒜 : Finset (Finset (Fin n))
r : ℕ
h𝒜 : (↑𝒜 : Set (Finset (Fin n))).Intersecting
h₂ : Set.Sized r (↑𝒜 : Set (Finset (Fin n)))
h₃ : r ≤ n / 2
b : r = 0
⊢ #𝒜 ≤ (n - 1).choose (r - 1)
have h : #𝒜 = 0
Tactic: convert! Nat.zero_le _
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (goal)
Goal:
n : ℕ
𝒜 : Finset (Finset (Fin n))
r : ℕ
h𝒜 : (↑𝒜 : Set (Finset (Fin n))).Intersecting
h₂ : Set.Sized r (↑𝒜 : Set (Finset (Fin n)))
h₃ : r ≤ n / 2
b : r = 0
⊢ #𝒜 = 0
have h : ∀ (x : Finset (Fin n)), x ∉ 𝒜
Tactic: rw [Finset.card_eq_zero, eq_empty_iff_forall_notMem]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (goal)
Goal:
n : ℕ
𝒜 : Finset (Finset (Fin n))
r : ℕ
h𝒜 : (↑𝒜 : Set (Finset (Fin n))).Intersecting
h₂ : Set.Sized r (↑𝒜 : Set (Finset (Fin n)))
h₃ : r ≤ n / 2
b : r = 0
⊢ ∀ (x : Finset (Fin n)), x ∉ 𝒜
have h : ∀ (A : Finset (Fin n)) (HA : A ∈ 𝒜), Disjoint A A
Tactic: refine fun A HA ↦ h𝒜 HA HA ?_
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (goal)
Goal:
n : ℕ
𝒜 : Finset (Finset (Fin n))
r : ℕ
h𝒜 : (↑𝒜 : Set (Finset (Fin n))).Intersecting
h₂ : Set.Sized r (↑𝒜 : Set (Finset (Fin n)))
h₃ : r ≤ n / 2
b : r = 0
A : Finset (Fin n)
HA : A ∈ 𝒜
⊢ Disjoint A A
have h : #A = r
Tactic: rw [disjoint_self_iff_empty, ← Finset.card_eq_zero, ← b]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (goal)
Goal:
n : ℕ
𝒜 : Finset (Finset (Fin n))
r : ℕ
h𝒜 : (↑𝒜 : Set (Finset (Fin n))).Intersecting
h₂ : Set.Sized r (↑𝒜 : Set (Finset (Fin n)))
h₃ : r ≤ n / 2
h1r : r > 0
⊢ #𝒜 ≤ (n - 1).choose (r - 1)
have inr : ∀ (size : (n - 1).choose (r - 1) < #𝒜), False
Tactic: refine le_of_not_gt fun size ↦ ?_
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (hypothesis)
Goal:
n : ℕ
𝒜 : Finset (Finset (Fin n))
r : ℕ
h𝒜 : (↑𝒜 : Set (Finset (Fin n))).Intersecting
h₂ : Set.Sized r (↑𝒜 : Set (Finset (Fin n)))
h₃ : r ≤ n / 2
h1r : r > 0
size : (n - 1).choose (r - 1) < #𝒜
A : Finset (Fin n)
hAbar : A ∈ ∂^[n - 2 * r] 𝒜ᶜˢ
hA : A ∈ 𝒜
⊢ False
have hAbar₁ : ∃ (s : Finset (Fin n)), sᶜ ∈ 𝒜 ∧ A ⊆ s ∧ #(s \ A) = n - 2 * r
Tactic: simp only [mem_shadow_iterate_iff_exists_sdiff, mem_compls] at hAbar
Cleared hypotheses: hAbar
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (goal)
Goal:
n : ℕ
𝒜 : Finset (Finset (Fin n))
r : ℕ
h𝒜 : (↑𝒜 : Set (Finset (Fin n))).Intersecting
h₂ : Set.Sized r (↑𝒜 : Set (Finset (Fin n)))
h₃ : r ≤ n / 2
h1r : r > 0
size : (n - 1).choose (r - 1) < #𝒜
A : Finset (Fin n)
hA : A ∈ 𝒜
hAbar : ∃ (s : Finset (Fin n)), sᶜ ∈ 𝒜 ∧ A ⊆ s ∧ #(s \ A) = n - 2 * r
⊢ False
have obtain : ∀ (C : Finset (Fin n)) (hC : Cᶜ ∈ 𝒜) (hAC : A ⊆ C), #(C \ A) = n - 2 * r → False
Tactic: obtain ⟨C, hC, hAC, _⟩ := hAbar
Cleared hypotheses: hAbar
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (hypothesis)
Goal:
n : ℕ
𝒜 : Finset (Finset (Fin n))
r : ℕ
h𝒜 : (↑𝒜 : Set (Finset (Fin n))).Intersecting
h₂ : Set.Sized r (↑𝒜 : Set (Finset (Fin n)))
h₃ : r ≤ n / 2
h1r : r > 0
size : (n - 1).choose (r - 1) < #𝒜
⊢ False
have this : Disjoint 𝒜 (∂^[n - 2 * r] 𝒜ᶜˢ)
Tactic: have : Disjoint 𝒜 (∂^[n - 2 * r] 𝒜ᶜˢ) := disjoint_right.2 fun A hAbar hA ↦ by
    simp only [mem_shadow_iterate_iff_exists_sdiff, mem_compls] at hAbar
    obtain ⟨C, hC, hAC, _⟩ := hAbar
    exact h𝒜 hA hC (disjoint_of_subset_left hAC disjoint_compl_right)
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (hypothesis)
Goal:
n : ℕ
𝒜 : Finset (Finset (Fin n))
r : ℕ
h𝒜 : (↑𝒜 : Set (Finset (Fin n))).Intersecting
h₂ : Set.Sized r (↑𝒜 : Set (Finset (Fin n)))
h₃ : r ≤ n / 2
h1r : r > 0
size : (n - 1).choose (r - 1) < #𝒜
this : Disjoint 𝒜 (∂^[n - 2 * r] 𝒜ᶜˢ)
⊢ False
have this₁ : r ≤ n
Tactic: have : r ≤ n := h₃.trans (Nat.div_le_self n 2)
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (hypothesis)
Goal:
n : ℕ
𝒜 : Finset (Finset (Fin n))
r : ℕ
h𝒜 : (↑𝒜 : Set (Finset (Fin n))).Intersecting
h₂ : Set.Sized r (↑𝒜 : Set (Finset (Fin n)))
h₃ : r ≤ n / 2
h1r : r > 0
size : (n - 1).choose (r - 1) < #𝒜
this_1 : Disjoint 𝒜 (∂^[n - 2 * r] 𝒜ᶜˢ)
this : r ≤ n
⊢ False
have this₁ : 1 ≤ n
Tactic: have : 1 ≤ n := ‹1 ≤ r›.trans ‹r ≤ n›
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (goal)
Goal:
n : ℕ
𝒜 : Finset (Finset (Fin n))
r : ℕ
h𝒜 : (↑𝒜 : Set (Finset (Fin n))).Intersecting
h₂ : Set.Sized r (↑𝒜 : Set (Finset (Fin n)))
h₃ : r ≤ n / 2
h1r : r > 0
size : (n - 1).choose (r - 1) < #𝒜
this_1 : Disjoint 𝒜 (∂^[n - 2 * r] 𝒜ᶜˢ)
this_2 : r ≤ n
this : 1 ≤ n
⊢ (n - 1).choose (n - r) < #𝒜ᶜˢ
have rwa : (n - 1).choose (n - r) < #𝒜
Tactic: rwa [card_compls, choose_symm_of_eq_add (tsub_add_tsub_cancel ‹r ≤ n› ‹1 ≤ r›).symm]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (hypothesis)
Goal:
n : ℕ
𝒜 : Finset (Finset (Fin n))
r : ℕ
h𝒜 : (↑𝒜 : Set (Finset (Fin n))).Intersecting
h₂ : Set.Sized r (↑𝒜 : Set (Finset (Fin n)))
h₃ : r ≤ n / 2
h1r : r > 0
size : (n - 1).choose (r - 1) < #𝒜
this_1 : Disjoint 𝒜 (∂^[n - 2 * r] 𝒜ᶜˢ)
this_2 : r ≤ n
this : 1 ≤ n
⊢ False
have z : (n - 1).choose (n - r) < #𝒜ᶜˢ
Tactic: have z : (n - 1).choose (n - r) < #𝒜ᶜˢ := by
    rwa [card_compls, choose_symm_of_eq_add (tsub_add_tsub_cancel ‹r ≤ n› ‹1 ≤ r›).symm]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (hypothesis)
Goal:
n : ℕ
𝒜 : Finset (Finset (Fin n))
r : ℕ
h𝒜 : (↑𝒜 : Set (Finset (Fin n))).Intersecting
h₂ : Set.Sized r (↑𝒜 : Set (Finset (Fin n)))
h₃ : r ≤ n / 2
h1r : r > 0
size : (n - 1).choose (r - 1) < #𝒜
this_1 : Disjoint 𝒜 (∂^[n - 2 * r] 𝒜ᶜˢ)
this_2 : r ≤ n
this : 1 ≤ n
z : (n - 1).choose (n - r) < #𝒜ᶜˢ
⊢ False
have h𝒜bar : Set.Sized (n - r) (↑𝒜ᶜˢ : Set (Finset (Fin n)))
Tactic: have h𝒜bar : (𝒜ᶜˢ : Set (Finset (Fin n))).Sized (n - r) := by simpa using h₂.compls
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (hypothesis)
Goal:
n : ℕ
𝒜 : Finset (Finset (Fin n))
r : ℕ
h𝒜 : (↑𝒜 : Set (Finset (Fin n))).Intersecting
h₂ : Set.Sized r (↑𝒜 : Set (Finset (Fin n)))
h₃ : r ≤ n / 2
h1r : r > 0
size : (n - 1).choose (r - 1) < #𝒜
this_1 : Disjoint 𝒜 (∂^[n - 2 * r] 𝒜ᶜˢ)
this_2 : r ≤ n
this : 1 ≤ n
z : (n - 1).choose (n - r) < #𝒜ᶜˢ
h𝒜bar : Set.Sized (n - r) (↑𝒜ᶜˢ : Set (Finset (Fin n)))
⊢ False
have kk : (n - 1).choose (n - r - (n - 2 * r)) ≤ #(∂^[n - 2 * r] 𝒜ᶜˢ)
Tactic: have kk := kruskal_katona_lovasz_form (i := n - 2 * r) (by lia)
    ((tsub_le_tsub_iff_left ‹1 ≤ n›).2 h1r) tsub_le_self h𝒜bar z.le
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (hypothesis)
Goal:
n : ℕ
𝒜 : Finset (Finset (Fin n))
r : ℕ
h𝒜 : (↑𝒜 : Set (Finset (Fin n))).Intersecting
h₂ : Set.Sized r (↑𝒜 : Set (Finset (Fin n)))
h₃ : r ≤ n / 2
h1r : r > 0
size : (n - 1).choose (r - 1) < #𝒜
this_1 : Disjoint 𝒜 (∂^[n - 2 * r] 𝒜ᶜˢ)
this_2 : r ≤ n
this : 1 ≤ n
z : (n - 1).choose (n - r) < #𝒜ᶜˢ
h𝒜bar : Set.Sized (n - r) (↑𝒜ᶜˢ : Set (Finset (Fin n)))
kk : (n - 1).choose (n - r - (n - 2 * r)) ≤ #(∂^[n - 2 * r] 𝒜ᶜˢ)
⊢ False
have this₁ : n - r - (n - 2 * r) = r
Tactic: have : n - r - (n - 2 * r) = r := by lia
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (hypothesis)
Goal:
n : ℕ
𝒜 : Finset (Finset (Fin n))
r : ℕ
h𝒜 : (↑𝒜 : Set (Finset (Fin n))).Intersecting
h₂ : Set.Sized r (↑𝒜 : Set (Finset (Fin n)))
h₃ : r ≤ n / 2
h1r : r > 0
size : (n - 1).choose (r - 1) < #𝒜
this_1 : Disjoint 𝒜 (∂^[n - 2 * r] 𝒜ᶜˢ)
this_2 : r ≤ n
this_3 : 1 ≤ n
z : (n - 1).choose (n - r) < #𝒜ᶜˢ
h𝒜bar : Set.Sized (n - r) (↑𝒜ᶜˢ : Set (Finset (Fin n)))
kk : (n - 1).choose (n - r - (n - 2 * r)) ≤ #(∂^[n - 2 * r] 𝒜ᶜˢ)
this : n - r - (n - 2 * r) = r
⊢ False
have kk₁ : (n - 1).choose r ≤ #(∂^[n - 2 * r] 𝒜ᶜˢ)
Tactic: rw [this] at kk
Cleared hypotheses: kk, this
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (goal)
Goal:
n : ℕ
𝒜 : Finset (Finset (Fin n))
r : ℕ
h𝒜 : (↑𝒜 : Set (Finset (Fin n))).Intersecting
h₂ : Set.Sized r (↑𝒜 : Set (Finset (Fin n)))
h₃ : r ≤ n / 2
h1r : r > 0
size : (n - 1).choose (r - 1) < #𝒜
this_1 : Disjoint 𝒜 (∂^[n - 2 * r] 𝒜ᶜˢ)
this_2 : r ≤ n
this_3 : 1 ≤ n
z : (n - 1).choose (n - r) < #𝒜ᶜˢ
h𝒜bar : Set.Sized (n - r) (↑𝒜ᶜˢ : Set (Finset (Fin n)))
kk : (n - 1).choose r ≤ #(∂^[n - 2 * r] 𝒜ᶜˢ)
this : n - r - (n - 2 * r) = r
⊢ n.choose r = (n - 1).choose (r - 1) + (n - 1).choose r
have h : n = (n - 1).succ
Tactic: convert! Nat.choose_succ_succ _ _ using 3
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (goal)
Goal:
n : ℕ
𝒜 : Finset (Finset (Fin n))
r : ℕ
h𝒜 : (↑𝒜 : Set (Finset (Fin n))).Intersecting
h₂ : Set.Sized r (↑𝒜 : Set (Finset (Fin n)))
h₃ : r ≤ n / 2
h1r : r > 0
size : (n - 1).choose (r - 1) < #𝒜
this_1 : Disjoint 𝒜 (∂^[n - 2 * r] 𝒜ᶜˢ)
this_2 : r ≤ n
this_3 : 1 ≤ n
z : (n - 1).choose (n - r) < #𝒜ᶜˢ
h𝒜bar : Set.Sized (n - r) (↑𝒜ᶜˢ : Set (Finset (Fin n)))
kk : (n - 1).choose r ≤ #(∂^[n - 2 * r] 𝒜ᶜˢ)
this : n - r - (n - 2 * r) = r
h : n = (n - 1).succ
⊢ n.choose r = (n - 1).choose (r - 1) + (n - 1).choose r
have h₁ : r = (r - 1).succ
Tactic: convert! Nat.choose_succ_succ _ _ using 3
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (goal)
Goal:
n : ℕ
𝒜 : Finset (Finset (Fin n))
r : ℕ
h𝒜 : (↑𝒜 : Set (Finset (Fin n))).Intersecting
h₂ : Set.Sized r (↑𝒜 : Set (Finset (Fin n)))
h₃ : r ≤ n / 2
h1r : r > 0
size : (n - 1).choose (r - 1) < #𝒜
this_1 : Disjoint 𝒜 (∂^[n - 2 * r] 𝒜ᶜˢ)
this_2 : r ≤ n
this_3 : 1 ≤ n
z : (n - 1).choose (n - r) < #𝒜ᶜˢ
h𝒜bar : Set.Sized (n - r) (↑𝒜ᶜˢ : Set (Finset (Fin n)))
kk : (n - 1).choose r ≤ #(∂^[n - 2 * r] 𝒜ᶜˢ)
this : n - r - (n - 2 * r) = r
⊢ n = (n - 1).succ
have h : n = n.pred.succ
Tactic: rwa [Nat.sub_one, Nat.succ_pred_eq_of_pos]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (goal)
Goal:
n : ℕ
𝒜 : Finset (Finset (Fin n))
r : ℕ
h𝒜 : (↑𝒜 : Set (Finset (Fin n))).Intersecting
h₂ : Set.Sized r (↑𝒜 : Set (Finset (Fin n)))
h₃ : r ≤ n / 2
h1r : r > 0
size : (n - 1).choose (r - 1) < #𝒜
this_1 : Disjoint 𝒜 (∂^[n - 2 * r] 𝒜ᶜˢ)
this_2 : r ≤ n
this_3 : 1 ≤ n
z : (n - 1).choose (n - r) < #𝒜ᶜˢ
h𝒜bar : Set.Sized (n - r) (↑𝒜ᶜˢ : Set (Finset (Fin n)))
kk : (n - 1).choose r ≤ #(∂^[n - 2 * r] 𝒜ᶜˢ)
this : n - r - (n - 2 * r) = r
h : n = n.pred.succ
⊢ n = (n - 1).succ
have h₁ : n = n
Tactic: rwa [Nat.sub_one, Nat.succ_pred_eq_of_pos]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (goal)
Goal:
n : ℕ
𝒜 : Finset (Finset (Fin n))
r : ℕ
h𝒜 : (↑𝒜 : Set (Finset (Fin n))).Intersecting
h₂ : Set.Sized r (↑𝒜 : Set (Finset (Fin n)))
h₃ : r ≤ n / 2
h1r : r > 0
size : (n - 1).choose (r - 1) < #𝒜
this_1 : Disjoint 𝒜 (∂^[n - 2 * r] 𝒜ᶜˢ)
this_2 : r ≤ n
this_3 : 1 ≤ n
z : (n - 1).choose (n - r) < #𝒜ᶜˢ
h𝒜bar : Set.Sized (n - r) (↑𝒜ᶜˢ : Set (Finset (Fin n)))
kk : (n - 1).choose r ≤ #(∂^[n - 2 * r] 𝒜ᶜˢ)
this : n - r - (n - 2 * r) = r
h : n = n.pred.succ
h₁ : n = n
⊢ n = (n - 1).succ
have h₄ : 0 < n
Tactic: rwa [Nat.sub_one, Nat.succ_pred_eq_of_pos]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (goal)
Goal:
n : ℕ
𝒜 : Finset (Finset (Fin n))
r : ℕ
h𝒜 : (↑𝒜 : Set (Finset (Fin n))).Intersecting
h₂ : Set.Sized r (↑𝒜 : Set (Finset (Fin n)))
h₃ : r ≤ n / 2
h1r : r > 0
size : (n - 1).choose (r - 1) < #𝒜
this_1 : Disjoint 𝒜 (∂^[n - 2 * r] 𝒜ᶜˢ)
this_2 : r ≤ n
this_3 : 1 ≤ n
z : (n - 1).choose (n - r) < #𝒜ᶜˢ
h𝒜bar : Set.Sized (n - r) (↑𝒜ᶜˢ : Set (Finset (Fin n)))
kk : (n - 1).choose r ≤ #(∂^[n - 2 * r] 𝒜ᶜˢ)
this : n - r - (n - 2 * r) = r
⊢ r = (r - 1).succ
have h : r = r.pred.succ
Tactic: rwa [Nat.sub_one, Nat.succ_pred_eq_of_pos]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (goal)
Goal:
n : ℕ
𝒜 : Finset (Finset (Fin n))
r : ℕ
h𝒜 : (↑𝒜 : Set (Finset (Fin n))).Intersecting
h₂ : Set.Sized r (↑𝒜 : Set (Finset (Fin n)))
h₃ : r ≤ n / 2
h1r : r > 0
size : (n - 1).choose (r - 1) < #𝒜
this_1 : Disjoint 𝒜 (∂^[n - 2 * r] 𝒜ᶜˢ)
this_2 : r ≤ n
this_3 : 1 ≤ n
z : (n - 1).choose (n - r) < #𝒜ᶜˢ
h𝒜bar : Set.Sized (n - r) (↑𝒜ᶜˢ : Set (Finset (Fin n)))
kk : (n - 1).choose r ≤ #(∂^[n - 2 * r] 𝒜ᶜˢ)
this : n - r - (n - 2 * r) = r
h : r = r.pred.succ
⊢ r = (r - 1).succ
have h₁ : r = r
Tactic: rwa [Nat.sub_one, Nat.succ_pred_eq_of_pos]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (goal)
Goal:
n : ℕ
𝒜 : Finset (Finset (Fin n))
r : ℕ
h𝒜 : (↑𝒜 : Set (Finset (Fin n))).Intersecting
h₂ : Set.Sized r (↑𝒜 : Set (Finset (Fin n)))
h₃ : r ≤ n / 2
h1r : r > 0
size : (n - 1).choose (r - 1) < #𝒜
this_1 : Disjoint 𝒜 (∂^[n - 2 * r] 𝒜ᶜˢ)
this_2 : r ≤ n
this_3 : 1 ≤ n
z : (n - 1).choose (n - r) < #𝒜ᶜˢ
h𝒜bar : Set.Sized (n - r) (↑𝒜ᶜˢ : Set (Finset (Fin n)))
kk : (n - 1).choose r ≤ #(∂^[n - 2 * r] 𝒜ᶜˢ)
this : n - r - (n - 2 * r) = r
h : r = r.pred.succ
h₁ : r = r
⊢ r = (r - 1).succ
have h₄ : 0 < r
Tactic: rwa [Nat.sub_one, Nat.succ_pred_eq_of_pos]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (goal)
Goal:
n : ℕ
𝒜 : Finset (Finset (Fin n))
r : ℕ
h𝒜 : (↑𝒜 : Set (Finset (Fin n))).Intersecting
h₂ : Set.Sized r (↑𝒜 : Set (Finset (Fin n)))
h₃ : r ≤ n / 2
h1r : r > 0
size : (n - 1).choose (r - 1) < #𝒜
this_1 : Disjoint 𝒜 (∂^[n - 2 * r] 𝒜ᶜˢ)
this_2 : r ≤ n
this_3 : 1 ≤ n
z : (n - 1).choose (n - r) < #𝒜ᶜˢ
h𝒜bar : Set.Sized (n - r) (↑𝒜ᶜˢ : Set (Finset (Fin n)))
kk : (n - 1).choose r ≤ #(∂^[n - 2 * r] 𝒜ᶜˢ)
this : n - r - (n - 2 * r) = r
⊢ #𝒜 + #(∂^[n - 2 * r] 𝒜ᶜˢ) = #(𝒜 ∪ ∂^[n - 2 * r] 𝒜ᶜˢ)
have rw : #𝒜 + #(∂^[n - 2 * r] 𝒜ᶜˢ) = #𝒜 + #(∂^[n - 2 * r] 𝒜ᶜˢ)
Tactic: rw [card_union_of_disjoint ‹_›]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (hypothesis)
Goal:
n : ℕ
𝒜 : Finset (Finset (Fin n))
r : ℕ
h𝒜 : (↑𝒜 : Set (Finset (Fin n))).Intersecting
h₂ : Set.Sized r (↑𝒜 : Set (Finset (Fin n)))
h₃ : r ≤ n / 2
h1r : r > 0
size : (n - 1).choose (r - 1) < #𝒜
this_1 : Disjoint 𝒜 (∂^[n - 2 * r] 𝒜ᶜˢ)
this_2 : r ≤ n
this_3 : 1 ≤ n
z : (n - 1).choose (n - r) < #𝒜ᶜˢ
h𝒜bar : Set.Sized (n - r) (↑𝒜ᶜˢ : Set (Finset (Fin n)))
kk : (n - 1).choose r ≤ #(∂^[n - 2 * r] 𝒜ᶜˢ)
this : n - r - (n - 2 * r) = r
⊢ False
have this₁ : n.choose r < #(𝒜 ∪ ∂^[n - 2 * r] 𝒜ᶜˢ)
Tactic: have := calc
    n.choose r = (n - 1).choose (r - 1) + (n - 1).choose r := by
      convert! Nat.choose_succ_succ _ _ using 3 <;> rwa [Nat.sub_one, Nat.succ_pred_eq_of_pos]
    _ < #𝒜 + #(∂^[n - 2 * r] 𝒜ᶜˢ) := add_lt_add_of_lt_of_le size kk
    _ = #(𝒜 ∪ ∂^[n - 2 * r] 𝒜ᶜˢ) := by rw [card_union_of_disjoint ‹_›]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (goal)
Goal:
n : ℕ
𝒜 : Finset (Finset (Fin n))
r : ℕ
h𝒜 : (↑𝒜 : Set (Finset (Fin n))).Intersecting
h₂ : Set.Sized r (↑𝒜 : Set (Finset (Fin n)))
h₃ : r ≤ n / 2
h1r : r > 0
size : (n - 1).choose (r - 1) < #𝒜
this_1 : Disjoint 𝒜 (∂^[n - 2 * r] 𝒜ᶜˢ)
this_2 : r ≤ n
this_3 : 1 ≤ n
z : (n - 1).choose (n - r) < #𝒜ᶜˢ
h𝒜bar : Set.Sized (n - r) (↑𝒜ᶜˢ : Set (Finset (Fin n)))
kk : (n - 1).choose r ≤ #(∂^[n - 2 * r] 𝒜ᶜˢ)
this_4 : n - r - (n - 2 * r) = r
this : n.choose r < #(𝒜 ∪ ∂^[n - 2 * r] 𝒜ᶜˢ)
⊢ False
have inr : #(𝒜 ∪ ∂^[n - 2 * r] 𝒜ᶜˢ) ≤ n.choose r
Tactic: apply this.not_ge
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (goal)
Goal:
n : ℕ
𝒜 : Finset (Finset (Fin n))
r : ℕ
h𝒜 : (↑𝒜 : Set (Finset (Fin n))).Intersecting
h₂ : Set.Sized r (↑𝒜 : Set (Finset (Fin n)))
h₃ : r ≤ n / 2
h1r : r > 0
size : (n - 1).choose (r - 1) < #𝒜
this_1 : Disjoint 𝒜 (∂^[n - 2 * r] 𝒜ᶜˢ)
this_2 : r ≤ n
this_3 : 1 ≤ n
z : (n - 1).choose (n - r) < #𝒜ᶜˢ
h𝒜bar : Set.Sized (n - r) (↑𝒜ᶜˢ : Set (Finset (Fin n)))
kk : (n - 1).choose r ≤ #(∂^[n - 2 * r] 𝒜ᶜˢ)
this_4 : n - r - (n - 2 * r) = r
this : n.choose r < #(𝒜 ∪ ∂^[n - 2 * r] 𝒜ᶜˢ)
⊢ #(𝒜 ∪ ∂^[n - 2 * r] 𝒜ᶜˢ) ≤ n.choose r
have h : n = Fintype.card (Fin n)
Tactic: convert! Set.Sized.card_le _
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (goal)
Goal:
n : ℕ
𝒜 : Finset (Finset (Fin n))
r : ℕ
h𝒜 : (↑𝒜 : Set (Finset (Fin n))).Intersecting
h₂ : Set.Sized r (↑𝒜 : Set (Finset (Fin n)))
h₃ : r ≤ n / 2
h1r : r > 0
size : (n - 1).choose (r - 1) < #𝒜
this_1 : Disjoint 𝒜 (∂^[n - 2 * r] 𝒜ᶜˢ)
this_2 : r ≤ n
this_3 : 1 ≤ n
z : (n - 1).choose (n - r) < #𝒜ᶜˢ
h𝒜bar : Set.Sized (n - r) (↑𝒜ᶜˢ : Set (Finset (Fin n)))
kk : (n - 1).choose r ≤ #(∂^[n - 2 * r] 𝒜ᶜˢ)
this_4 : n - r - (n - 2 * r) = r
this : n.choose r < #(𝒜 ∪ ∂^[n - 2 * r] 𝒜ᶜˢ)
h : n = Fintype.card (Fin n)
⊢ #(𝒜 ∪ ∂^[n - 2 * r] 𝒜ᶜˢ) ≤ n.choose r
have inr : Fintype (Fin n)
Tactic: convert! Set.Sized.card_le _
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (goal)
Goal:
n : ℕ
𝒜 : Finset (Finset (Fin n))
r : ℕ
h𝒜 : (↑𝒜 : Set (Finset (Fin n))).Intersecting
h₂ : Set.Sized r (↑𝒜 : Set (Finset (Fin n)))
h₃ : r ≤ n / 2
h1r : r > 0
size : (n - 1).choose (r - 1) < #𝒜
this_1 : Disjoint 𝒜 (∂^[n - 2 * r] 𝒜ᶜˢ)
this_2 : r ≤ n
this_3 : 1 ≤ n
z : (n - 1).choose (n - r) < #𝒜ᶜˢ
h𝒜bar : Set.Sized (n - r) (↑𝒜ᶜˢ : Set (Finset (Fin n)))
kk : (n - 1).choose r ≤ #(∂^[n - 2 * r] 𝒜ᶜˢ)
this_4 : n - r - (n - 2 * r) = r
this : n.choose r < #(𝒜 ∪ ∂^[n - 2 * r] 𝒜ᶜˢ)
h : n = Fintype.card (Fin n)
inr : Fintype (Fin n)
⊢ #(𝒜 ∪ ∂^[n - 2 * r] 𝒜ᶜˢ) ≤ n.choose r
have inr₁ : Set.Sized r (↑(𝒜 ∪ ∂^[n - 2 * r] 𝒜ᶜˢ) : Set (Finset (Fin n)))
Tactic: convert! Set.Sized.card_le _
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (goal)
Goal:
n : ℕ
𝒜 : Finset (Finset (Fin n))
r : ℕ
h𝒜 : (↑𝒜 : Set (Finset (Fin n))).Intersecting
h₂ : Set.Sized r (↑𝒜 : Set (Finset (Fin n)))
h₃ : r ≤ n / 2
h1r : r > 0
size : (n - 1).choose (r - 1) < #𝒜
this_1 : Disjoint 𝒜 (∂^[n - 2 * r] 𝒜ᶜˢ)
this_2 : r ≤ n
this_3 : 1 ≤ n
z : (n - 1).choose (n - r) < #𝒜ᶜˢ
h𝒜bar : Set.Sized (n - r) (↑𝒜ᶜˢ : Set (Finset (Fin n)))
kk : (n - 1).choose r ≤ #(∂^[n - 2 * r] 𝒜ᶜˢ)
this_4 : n - r - (n - 2 * r) = r
this : n.choose r < #(𝒜 ∪ ∂^[n - 2 * r] 𝒜ᶜˢ)
⊢ n = Fintype.card (Fin n)
have h : n = n
Tactic: rw [Fintype.card_fin]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (goal)
Goal:
n : ℕ
𝒜 : Finset (Finset (Fin n))
r : ℕ
h𝒜 : (↑𝒜 : Set (Finset (Fin n))).Intersecting
h₂ : Set.Sized r (↑𝒜 : Set (Finset (Fin n)))
h₃ : r ≤ n / 2
h1r : r > 0
size : (n - 1).choose (r - 1) < #𝒜
this_1 : Disjoint 𝒜 (∂^[n - 2 * r] 𝒜ᶜˢ)
this_2 : r ≤ n
this_3 : 1 ≤ n
z : (n - 1).choose (n - r) < #𝒜ᶜˢ
h𝒜bar : Set.Sized (n - r) (↑𝒜ᶜˢ : Set (Finset (Fin n)))
kk : (n - 1).choose r ≤ #(∂^[n - 2 * r] 𝒜ᶜˢ)
this_4 : n - r - (n - 2 * r) = r
this : n.choose r < #(𝒜 ∪ ∂^[n - 2 * r] 𝒜ᶜˢ)
⊢ Set.Sized r (↑(𝒜 ∪ ∂^[n - 2 * r] 𝒜ᶜˢ) : Set (Finset (Fin n)))
have inr : Set.Sized r (↑𝒜 : Set (Finset (Fin n))) ∧ Set.Sized r (↑(∂^[n - 2 * r] 𝒜ᶜˢ) : Set (Finset (Fin n)))
Tactic: rw [coe_union, Set.sized_union]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (goal)
Goal:
n : ℕ
𝒜 : Finset (Finset (Fin n))
r : ℕ
h𝒜 : (↑𝒜 : Set (Finset (Fin n))).Intersecting
h₂ : Set.Sized r (↑𝒜 : Set (Finset (Fin n)))
h₃ : r ≤ n / 2
h1r : r > 0
size : (n - 1).choose (r - 1) < #𝒜
this_1 : Disjoint 𝒜 (∂^[n - 2 * r] 𝒜ᶜˢ)
this_2 : r ≤ n
this_3 : 1 ≤ n
z : (n - 1).choose (n - r) < #𝒜ᶜˢ
h𝒜bar : Set.Sized (n - r) (↑𝒜ᶜˢ : Set (Finset (Fin n)))
kk : (n - 1).choose r ≤ #(∂^[n - 2 * r] 𝒜ᶜˢ)
this_4 : n - r - (n - 2 * r) = r
this : n.choose r < #(𝒜 ∪ ∂^[n - 2 * r] 𝒜ᶜˢ)
⊢ Set.Sized r (↑𝒜 : Set (Finset (Fin n))) ∧ Set.Sized r (↑(∂^[n - 2 * r] 𝒜ᶜˢ) : Set (Finset (Fin n)))
have inr : Set.Sized r (↑(∂^[n - 2 * r] 𝒜ᶜˢ) : Set (Finset (Fin n)))
Tactic: refine ⟨‹_›, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (goal)
Goal:
n : ℕ
𝒜 : Finset (Finset (Fin n))
r : ℕ
h𝒜 : (↑𝒜 : Set (Finset (Fin n))).Intersecting
h₂ : Set.Sized r (↑𝒜 : Set (Finset (Fin n)))
h₃ : r ≤ n / 2
h1r : r > 0
size : (n - 1).choose (r - 1) < #𝒜
this_1 : Disjoint 𝒜 (∂^[n - 2 * r] 𝒜ᶜˢ)
this_2 : r ≤ n
this_3 : 1 ≤ n
z : (n - 1).choose (n - r) < #𝒜ᶜˢ
h𝒜bar : Set.Sized (n - r) (↑𝒜ᶜˢ : Set (Finset (Fin n)))
kk : (n - 1).choose r ≤ #(∂^[n - 2 * r] 𝒜ᶜˢ)
this_4 : n - r - (n - 2 * r) = r
this : n.choose r < #(𝒜 ∪ ∂^[n - 2 * r] 𝒜ᶜˢ)
⊢ Set.Sized r (↑(∂^[n - 2 * r] 𝒜ᶜˢ) : Set (Finset (Fin n)))
have h : r = n - r - (n - 2 * r)
Tactic: convert! h𝒜bar.shadow_iterate
-- 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)
⊢ #𝒜 * r ≤ #(∂ 𝒜) * (Fintype.card α - r + 1)
have refine_1 : ∀ (s : Finset α) (hs : s ∈ 𝒜), r ≤ #(bipartiteBelow (fun (x1 x2 : Finset α) ↦ x1 ⊆ x2) (∂ 𝒜) s)
Tactic: refine card_mul_le_card_mul' (· ⊆ ·) (fun s hs => ?_) (fun 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)
refine_1 : ∀ (s : Finset α) (hs : s ∈ 𝒜), r ≤ #(bipartiteBelow (fun (x1 x2 : Finset α) ↦ x1 ⊆ x2) (∂ 𝒜) s)
⊢ #𝒜 * r ≤ #(∂ 𝒜) * (Fintype.card α - r + 1)
have refine_2 : ∀ (s : Finset α) (hs : s ∈ ∂ 𝒜), #(bipartiteAbove (fun (x1 x2 : Finset α) ↦ x1 ⊆ x2) 𝒜 s) ≤ Fintype.card α - r + 1
Tactic: refine card_mul_le_card_mul' (· ⊆ ·) (fun s hs => ?_) (fun s hs => ?_)