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)))
B : Finset (Fin n)
h : B ⊆ range'k ∧ #B = r - i → ∃ s ∈ 𝒞, B ⊆ s ∧ #(s \ B) = i
⊢ B ⊆ range'k ∧ #B = r - i ↔ ∃ s ∈ 𝒞, B ⊆ s ∧ #(s \ B) = i
have h₃ : (∃ s ∈ 𝒞, B ⊆ s ∧ #(s \ B) = i) → B ⊆ range'k ∧ #B = r - i
Tactic: constructor
-- 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)))
B : Finset (Fin n)
hBk : B ⊆ range'k
hB : #B = r - i
⊢ i + #B ≤ #range'k
have rwa : i + (r - i) ≤ #range'k
Tactic: rwa [hB, card_attachFin, card_range, ← Nat.add_sub_assoc hir, Nat.add_sub_cancel_left]
-- 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)))
B : Finset (Fin n)
hBk : B ⊆ range'k
hB : #B = r - i
rwa : i + (r - i) ≤ #range'k
⊢ i + #B ≤ #range'k
have rwa₁ : i + (r - i) ≤ #(range k)
Tactic: rwa [hB, card_attachFin, card_range, ← Nat.add_sub_assoc hir, Nat.add_sub_cancel_left]
-- 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)))
B : Finset (Fin n)
hBk : B ⊆ range'k
hB : #B = r - i
rwa : i + (r - i) ≤ #range'k
rwa₁ : i + (r - i) ≤ #(range k)
⊢ i + #B ≤ #range'k
have rwa₂ : i + (r - i) ≤ k
Tactic: rwa [hB, card_attachFin, card_range, ← Nat.add_sub_assoc hir, Nat.add_sub_cancel_left]
-- 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)))
B : Finset (Fin n)
hBk : B ⊆ range'k
hB : #B = r - i
rwa : i + (r - i) ≤ #range'k
rwa₁ : i + (r - i) ≤ #(range k)
rwa₂ : i + (r - i) ≤ k
⊢ i + #B ≤ #range'k
have rwa₃ : i + r - i ≤ k
Tactic: rwa [hB, card_attachFin, card_range, ← Nat.add_sub_assoc hir, Nat.add_sub_cancel_left]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (hypothesis)
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)))
B : Finset (Fin n)
hBk : B ⊆ range'k
hB : #B = r - i
⊢ ∃ s ∈ 𝒞, B ⊆ s ∧ #(s \ B) = i
have this₁ : ∃ (u : Finset (Fin n)), B ⊆ u ∧ u ⊆ range'k ∧ #u = i + #B
Tactic: 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]
-- 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_1 : Set.Sized r (↑𝒞 : Set (Finset (Fin n)))
B : Finset (Fin n)
hBk : B ⊆ range'k
hB : #B = r - i
this : ∃ (u : Finset (Fin n)), B ⊆ u ∧ u ⊆ range'k ∧ #u = i + #B
⊢ ∃ s ∈ 𝒞, B ⊆ s ∧ #(s \ B) = i
have h : ∀ (C : Finset (Fin n)) (BsubC : B ⊆ C) (hCrange : C ⊆ range'k) (hcard : #C = i + #B), ∃ s ∈ 𝒞, B ⊆ s ∧ #(s \ B) = i
Tactic: obtain ⟨C, BsubC, hCrange, hcard⟩ := this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (hypothesis)
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)))
B : Finset (Fin n)
hBk : B ⊆ range'k
hB : #B = r - i
C : Finset (Fin n)
BsubC : B ⊆ C
hCrange : C ⊆ range'k
hcard : #C = i + #B
⊢ ∃ s ∈ 𝒞, B ⊆ s ∧ #(s \ B) = i
have hcard₁ : #C = r
Tactic: rw [hB, ← Nat.add_sub_assoc hir, Nat.add_sub_cancel_left] at hcard
Cleared hypotheses: hcard
-- 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)))
B : Finset (Fin n)
hBk : B ⊆ range'k
hB : #B = r - i
C : Finset (Fin n)
BsubC : B ⊆ C
hCrange : C ⊆ range'k
hcard : #C = r
⊢ ∃ s ∈ 𝒞, B ⊆ s ∧ #(s \ B) = i
have h : #(C \ B) = i
Tactic: refine ⟨C, mem_powersetCard.2 ⟨hCrange, hcard⟩, BsubC, ?_⟩
-- 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)))
B : Finset (Fin n)
hBk : B ⊆ range'k
hB : #B = r - i
C : Finset (Fin n)
BsubC : B ⊆ C
hCrange : C ⊆ range'k
hcard : #C = r
⊢ #(C \ B) = i
have h : #C - #B = i
Tactic: rw [card_sdiff_of_subset BsubC, hcard, hB, Nat.sub_sub_self hir]
-- 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)))
B : Finset (Fin n)
hBk : B ⊆ range'k
hB : #B = r - i
C : Finset (Fin n)
BsubC : B ⊆ C
hCrange : C ⊆ range'k
hcard : #C = r
h : #C - #B = i
⊢ #(C \ B) = i
have h₃ : r - #B = i
Tactic: rw [card_sdiff_of_subset BsubC, hcard, hB, Nat.sub_sub_self hir]
-- 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)))
B : Finset (Fin n)
hBk : B ⊆ range'k
hB : #B = r - i
C : Finset (Fin n)
BsubC : B ⊆ C
hCrange : C ⊆ range'k
hcard : #C = r
h : #C - #B = i
h₃ : r - #B = i
⊢ #(C \ B) = i
have h₄ : r - (r - i) = i
Tactic: rw [card_sdiff_of_subset BsubC, hcard, hB, Nat.sub_sub_self hir]
-- 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)))
B : Finset (Fin n)
hBk : B ⊆ range'k
hB : #B = r - i
C : Finset (Fin n)
BsubC : B ⊆ C
hCrange : C ⊆ range'k
hcard : #C = r
h : #C - #B = i
h₃ : r - #B = i
h₄ : r - (r - i) = i
⊢ #(C \ B) = i
have h₅ : i = i
Tactic: rw [card_sdiff_of_subset BsubC, hcard, hB, Nat.sub_sub_self hir]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (hypothesis)
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)))
B A : Finset (Fin n)
Ah : A ∈ 𝒞
hBA : B ⊆ A
card_sdiff_i : #(A \ B) = i
⊢ B ⊆ range'k ∧ #B = r - i
have Ah₁ : A ⊆ range'k ∧ #A = r
Tactic: rw [mem_powersetCard] at Ah
Cleared hypotheses: Ah, hBA, card_sdiff_i
-- 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)))
B A : Finset (Fin n)
Ah : A ⊆ range'k ∧ #A = r
hBA : B ⊆ A
card_sdiff_i : #(A \ B) = i
⊢ B ⊆ range'k ∧ #B = r - i
have h : #B + i = r
Tactic: refine ⟨hBA.trans Ah.1, eq_tsub_of_add_eq ?_⟩
-- 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)))
B A : Finset (Fin n)
Ah : A ⊆ range'k ∧ #A = r
hBA : B ⊆ A
card_sdiff_i : #(A \ B) = i
⊢ #B + i = r
have h : #B + i = #A
Tactic: rw [← Ah.2, ← card_sdiff_i, add_comm, card_sdiff_add_card_eq_card hBA]
-- 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)))
B A : Finset (Fin n)
Ah : A ⊆ range'k ∧ #A = r
hBA : B ⊆ A
card_sdiff_i : #(A \ B) = i
h : #B + i = #A
⊢ #B + i = r
have h₃ : #B + #(A \ B) = #A
Tactic: rw [← Ah.2, ← card_sdiff_i, add_comm, card_sdiff_add_card_eq_card hBA]
-- 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)))
B A : Finset (Fin n)
Ah : A ⊆ range'k ∧ #A = r
hBA : B ⊆ A
card_sdiff_i : #(A \ B) = i
h : #B + i = #A
h₃ : #B + #(A \ B) = #A
⊢ #B + i = r
have h₄ : #(A \ B) + #B = #A
Tactic: rw [← Ah.2, ← card_sdiff_i, add_comm, card_sdiff_add_card_eq_card hBA]
-- 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)))
B A : Finset (Fin n)
Ah : A ⊆ range'k ∧ #A = r
hBA : B ⊆ A
card_sdiff_i : #(A \ B) = i
h : #B + i = #A
h₃ : #B + #(A \ B) = #A
h₄ : #(A \ B) + #B = #A
⊢ #B + i = r
have h₅ : #A = #A
Tactic: rw [← Ah.2, ← card_sdiff_i, add_comm, card_sdiff_add_card_eq_card hBA]
-- 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)))
⊢ #(∂^[i] 𝒞) ≤ #(∂^[i] 𝒜)
have refine_1 : #𝒞 ≤ #𝒜
Tactic: refine iterated_kk h₁ ?_ ⟨‹_›, ?_⟩
-- 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)))
refine_1 : #𝒞 ≤ #𝒜
⊢ #(∂^[i] 𝒞) ≤ #(∂^[i] 𝒜)
have refine_2 : ∀ ⦃s t : Finset (Fin n)⦄,
  s ∈ 𝒞 →
    LT.lt (α := Colex (Finset (Fin n)))
          ((toColex : (a : Finset (Fin n)) → Colex (Finset (Fin n))) t : Colex (Finset (Fin n)))
          ((toColex : (a : Finset (Fin n)) → Colex (Finset (Fin n))) s : Colex (Finset (Fin n))) ∧
        #t = r →
      t ∈ 𝒞
Tactic: refine iterated_kk h₁ ?_ ⟨‹_›, ?_⟩
-- 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)))
⊢ #𝒞 ≤ #𝒜
have refine_1 : (#range'k).choose r ≤ #𝒜
Tactic: rwa [card_powersetCard, card_attachFin, card_range]
-- 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)))
refine_1 : (#range'k).choose r ≤ #𝒜
⊢ #𝒞 ≤ #𝒜
have refine_1₁ : (#(range k)).choose r ≤ #𝒜
Tactic: rwa [card_powersetCard, card_attachFin, card_range]
-- 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)))
⊢ ∀ ⦃s t : Finset (Fin n)⦄,
    s ∈ 𝒞 →
      LT.lt (α := Colex (Finset (Fin n)))
            ((toColex : (a : Finset (Fin n)) → Colex (Finset (Fin n))) t : Colex (Finset (Fin n)))
            ((toColex : (a : Finset (Fin n)) → Colex (Finset (Fin n))) s : Colex (Finset (Fin n))) ∧
          #t = r →
        t ∈ 𝒞
have refine_2 : ∀ ⦃s t : Finset (Fin n)⦄,
  s ⊆ range'k ∧ #s = r →
    LT.lt (α := Colex (Finset (Fin n)))
          ((toColex : (a : Finset (Fin n)) → Colex (Finset (Fin n))) t : Colex (Finset (Fin n)))
          ((toColex : (a : Finset (Fin n)) → Colex (Finset (Fin n))) s : Colex (Finset (Fin n))) ∧
        #t = r →
      t ⊆ range'k ∧ #t = r
Tactic: simp_rw [𝒞, mem_powersetCard]
-- 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)))
A B : Finset (Fin n)
hA : A ⊆ range'k ∧ #A = r
HB₁ :
  LT.lt (α := Colex (Finset (Fin n)))
    ((toColex : (a : Finset (Fin n)) → Colex (Finset (Fin n))) B : Colex (Finset (Fin n)))
    ((toColex : (a : Finset (Fin n)) → Colex (Finset (Fin n))) A : Colex (Finset (Fin n)))
HB₂ : #B = r
⊢ B ⊆ range'k ∧ #B = r
have refine_2 : ∀ (t : Fin n) (ht : t ∈ B), t ∈ range'k
Tactic: refine ⟨fun t ht ↦ ?_, ‹_›⟩
-- 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)))
A B : Finset (Fin n)
hA : A ⊆ range'k ∧ #A = r
HB₁ :
  LT.lt (α := Colex (Finset (Fin n)))
    ((toColex : (a : Finset (Fin n)) → Colex (Finset (Fin n))) B : Colex (Finset (Fin n)))
    ((toColex : (a : Finset (Fin n)) → Colex (Finset (Fin n))) A : Colex (Finset (Fin n)))
HB₂ : #B = r
t : Fin n
ht : t ∈ B
⊢ t ∈ range'k
have refine_2 : (↑t : ℕ) < k
Tactic: rw [mem_attachFin, mem_range]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (hypothesis)
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)))
A B : Finset (Fin n)
hA : A ⊆ range'k ∧ #A = r
HB₁ :
  LT.lt (α := Colex (Finset (Fin n)))
    ((toColex : (a : Finset (Fin n)) → Colex (Finset (Fin n))) B : Colex (Finset (Fin n)))
    ((toColex : (a : Finset (Fin n)) → Colex (Finset (Fin n))) A : Colex (Finset (Fin n)))
HB₂ : #B = r
t : Fin n
ht : t ∈ B
⊢ (↑t : ℕ) < k
have this₁ : LT.lt (α := Colex (Finset ℕ)) ((toColex : (a : Finset ℕ) → Colex (Finset ℕ)) (image Fin.val B) : Colex (Finset ℕ))
  ((toColex : (a : Finset ℕ) → Colex (Finset ℕ)) (image Fin.val A) : Colex (Finset ℕ))
Tactic: have : toColex (image Fin.val B) < toColex (image Fin.val A) := by
        rwa [toColex_image_lt_toColex_image Fin.val_strictMono]
-- 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_1 : Set.Sized r (↑𝒞 : Set (Finset (Fin n)))
A B : Finset (Fin n)
hA : A ⊆ range'k ∧ #A = r
HB₁ :
  LT.lt (α := Colex (Finset (Fin n)))
    ((toColex : (a : Finset (Fin n)) → Colex (Finset (Fin n))) B : Colex (Finset (Fin n)))
    ((toColex : (a : Finset (Fin n)) → Colex (Finset (Fin n))) A : Colex (Finset (Fin n)))
HB₂ : #B = r
t : Fin n
ht : t ∈ B
this :
  LT.lt (α := Colex (Finset ℕ)) ((toColex : (a : Finset ℕ) → Colex (Finset ℕ)) (image Fin.val B) : Colex (Finset ℕ))
    ((toColex : (a : Finset ℕ) → Colex (Finset ℕ)) (image Fin.val A) : Colex (Finset ℕ))
⊢ (↑t : ℕ) < k
have apply : ∀ b ∈ image Fin.val A, b < k
Tactic: apply Colex.forall_lt_mono this.le _ t (mem_image.2 ⟨t, ht, rfl⟩)
-- 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_1 : Set.Sized r (↑𝒞 : Set (Finset (Fin n)))
A B : Finset (Fin n)
hA : A ⊆ range'k ∧ #A = r
HB₁ :
  LT.lt (α := Colex (Finset (Fin n)))
    ((toColex : (a : Finset (Fin n)) → Colex (Finset (Fin n))) B : Colex (Finset (Fin n)))
    ((toColex : (a : Finset (Fin n)) → Colex (Finset (Fin n))) A : Colex (Finset (Fin n)))
HB₂ : #B = r
t : Fin n
ht : t ∈ B
this :
  LT.lt (α := Colex (Finset ℕ)) ((toColex : (a : Finset ℕ) → Colex (Finset ℕ)) (image Fin.val B) : Colex (Finset ℕ))
    ((toColex : (a : Finset ℕ) → Colex (Finset ℕ)) (image Fin.val A) : Colex (Finset ℕ))
⊢ ∀ b ∈ image Fin.val A, b < k
have simp_rw : ∀ (b : ℕ), (∃ a ∈ A, (↑a : ℕ) = b) → b < k
Tactic: simp_rw [mem_image]
-- 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) ≤ #(∂^[i] 𝒜)
have _ : k.choose (r - i) = #(powersetCard (r - i) range'k)
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 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)
⊢ k.choose (r - i) ≤ #(∂^[i] 𝒜)
have _₁ : #(powersetCard (r - i) range'k) = #(∂^[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