awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
Goal:
n r : ℕ
𝒜 : Finset (Finset (Fin n))
h : Set.Sized r (↑𝒜 : Set (Finset (Fin n)))
usable : Finset (Finset (Fin n) × Finset (Fin n)) :=
  {t : Finset (Fin n) × Finset (Fin n) | UsefulCompression t.1 t.2 ∧ ¬IsCompressed t.1 t.2 𝒜}
husable : usable.Nonempty
U V : Finset (Fin n)
hUV :
  Membership.mem (γ := Finset (Finset (Fin n) × Finset (Fin n))) univ (U, V) ∧
    UsefulCompression (U, V).1 (U, V).2 ∧ ¬IsCompressed (U, V).1 (U, V).2 𝒜
t_1 : ∀ x' ∈ usable, #(U, V).1 ≤ #x'.1
h₂ : ∀ (U₁ V₁ : Finset (Fin n)), UsefulCompression U₁ V₁ → #U₁ < #U → IsCompressed U₁ V₁ 𝒜
p1 : #(∂ (𝓒 U V 𝒜)) ≤ #(∂ 𝒜)
hUV' : #(U, V).1 = #(U, V).2
hu : (U, V).1.Nonempty
hv : (U, V).2.Nonempty
hmax : (U, V).1.max' hu < (U, V).2.max' hv
this : familyMeasure (𝓒 (U, V).1 (U, V).2 𝒜) < familyMeasure 𝒜
t : Finset (Finset (Fin n))
q1 : #(∂ t) ≤ #(∂ (𝓒 U V 𝒜))
q2 : #(𝓒 U V 𝒜) = #t
q3 : Set.Sized r (↑t : Set (Finset (Fin n)))
q4 : ∀ (U V : Finset (Fin n)), UsefulCompression U V → IsCompressed U V t
⊢ ∃ (ℬ : Finset (Finset (Fin n))),
    #(∂ ℬ) ≤ #(∂ 𝒜) ∧
      #𝒜 = #ℬ ∧
        Set.Sized r (↑ℬ : Set (Finset (Fin n))) ∧ ∀ (U V : Finset (Fin n)), UsefulCompression U V → IsCompressed U V ℬ

Tactic:
exact ⟨t, q1.trans p1, (card_compression _ _ _).symm.trans q2, q3, q4⟩
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
Goal:
n r : ℕ
𝒜 𝒞 : Finset (Finset (Fin n))
h𝒜r : Set.Sized r (↑𝒜 : Set (Finset (Fin n)))
h𝒞𝒜 : #𝒞 ≤ #𝒜
h𝒞 : IsInitSeg 𝒞 r
obtain : ∀ (𝒜' : Finset (Finset (Fin n))) (h𝒜 : 𝒜' ⊆ 𝒜) (h𝒜𝒞 : #𝒜' = #𝒞), #(∂ 𝒞) ≤ #(∂ 𝒜)
⊢ #(∂ 𝒞) ≤ #(∂ 𝒜)

Tactic:
obtain ⟨𝒜', h𝒜, h𝒜𝒞⟩ := exists_subset_card_eq h𝒞𝒜

Premises used: Finset.exists_subset_card_eq
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
Goal:
n r : ℕ
𝒜 𝒞 : Finset (Finset (Fin n))
h𝒜r : Set.Sized r (↑𝒜 : Set (Finset (Fin n)))
h𝒞𝒜 : #𝒞 ≤ #𝒜
h𝒞 : IsInitSeg 𝒞 r
𝒜' : Finset (Finset (Fin n))
h𝒜 : 𝒜' ⊆ 𝒜
h𝒜𝒞 : #𝒜' = #𝒞
⊢ (↑𝒜' : Set (Finset (Fin n))) ⊆ (↑𝒜 : Set (Finset (Fin n)))

Tactic:
gcongr
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
Goal:
n r : ℕ
𝒜 𝒞 : Finset (Finset (Fin n))
h𝒜r : Set.Sized r (↑𝒜 : Set (Finset (Fin n)))
h𝒞𝒜 : #𝒞 ≤ #𝒜
h𝒞 : IsInitSeg 𝒞 r
𝒜' : Finset (Finset (Fin n))
h𝒜 : 𝒜' ⊆ 𝒜
h𝒜𝒞 : #𝒜' = #𝒞
obtain :
  ∀ (ℬ : Finset (Finset (Fin n))) (hℬ𝒜 : #(∂ ℬ) ≤ #(∂ 𝒜')) (h𝒜ℬ : #𝒜' = #ℬ)
    (hℬr : Set.Sized r (↑ℬ : Set (Finset (Fin n))))
    (hℬ : ∀ (U V : Finset (Fin n)), UV.UsefulCompression U V → IsCompressed U V ℬ), #(∂ 𝒞) ≤ #(∂ 𝒜)
⊢ #(∂ 𝒞) ≤ #(∂ 𝒜)

Tactic:
obtain ⟨ℬ, hℬ𝒜, h𝒜ℬ, hℬr, hℬ⟩ := UV.kruskal_katona_helper 𝒜' (h𝒜r.mono (by gcongr))

Premises used: Set.Sized.mono, _private.0.Finset.UV.kruskal_katona_helper
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
Goal:
n r : ℕ
𝒜 𝒞 : Finset (Finset (Fin n))
h𝒜r : Set.Sized r (↑𝒜 : Set (Finset (Fin n)))
h𝒞𝒜 : #𝒞 ≤ #𝒜
h𝒞 : IsInitSeg 𝒞 r
𝒜' : Finset (Finset (Fin n))
h𝒜 : 𝒜' ⊆ 𝒜
h𝒜𝒞 : #𝒜' = #𝒞
ℬ : Finset (Finset (Fin n))
hℬ𝒜 : #(∂ ℬ) ≤ #(∂ 𝒜')
h𝒜ℬ : #𝒜' = #ℬ
hℬr : Set.Sized r (↑ℬ : Set (Finset (Fin n)))
hℬ : ∀ (U V : Finset (Fin n)), UV.UsefulCompression U V → IsCompressed U V ℬ
this : ℬ = 𝒞
subst : ∀ (h𝒞𝒜 : #ℬ ≤ #𝒜) (h𝒞 : IsInitSeg ℬ r) (h𝒜𝒞 : #𝒜' = #ℬ), #(∂ ℬ) ≤ #(∂ 𝒜)
⊢ #(∂ 𝒞) ≤ #(∂ 𝒜)

Tactic:
subst 𝒞
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
Goal:
n r : ℕ
𝒜 : Finset (Finset (Fin n))
h𝒜r : Set.Sized r (↑𝒜 : Set (Finset (Fin n)))
𝒜' : Finset (Finset (Fin n))
h𝒜 : 𝒜' ⊆ 𝒜
ℬ : Finset (Finset (Fin n))
hℬ𝒜 : #(∂ ℬ) ≤ #(∂ 𝒜')
h𝒜ℬ : #𝒜' = #ℬ
hℬr : Set.Sized r (↑ℬ : Set (Finset (Fin n)))
hℬ : ∀ (U V : Finset (Fin n)), UV.UsefulCompression U V → IsCompressed U V ℬ
h𝒞𝒜 : #ℬ ≤ #𝒜
h𝒞 : IsInitSeg ℬ r
h𝒜𝒞 : #𝒜' = #ℬ
⊢ #(∂ 𝒜') ≤ #(∂ 𝒜)

Tactic:
gcongr
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
Goal:
n r : ℕ
𝒜 : Finset (Finset (Fin n))
h𝒜r : Set.Sized r (↑𝒜 : Set (Finset (Fin n)))
𝒜' : Finset (Finset (Fin n))
h𝒜 : 𝒜' ⊆ 𝒜
ℬ : Finset (Finset (Fin n))
hℬ𝒜 : #(∂ ℬ) ≤ #(∂ 𝒜')
h𝒜ℬ : #𝒜' = #ℬ
hℬr : Set.Sized r (↑ℬ : Set (Finset (Fin n)))
hℬ : ∀ (U V : Finset (Fin n)), UV.UsefulCompression U V → IsCompressed U V ℬ
h𝒞𝒜 : #ℬ ≤ #𝒜
h𝒞 : IsInitSeg ℬ r
h𝒜𝒞 : #𝒜' = #ℬ
⊢ #(∂ ℬ) ≤ #(∂ 𝒜)

Tactic:
exact hℬ𝒜.trans (by gcongr)

Premises used: LE.le.trans
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
Goal:
n r : ℕ
𝒜 𝒞 : Finset (Finset (Fin n))
h𝒜r : Set.Sized r (↑𝒜 : Set (Finset (Fin n)))
h𝒞𝒜 : #𝒞 ≤ #𝒜
h𝒞 : IsInitSeg 𝒞 r
𝒜' : Finset (Finset (Fin n))
h𝒜 : 𝒜' ⊆ 𝒜
h𝒜𝒞 : #𝒜' = #𝒞
ℬ : Finset (Finset (Fin n))
hℬ𝒜 : #(∂ ℬ) ≤ #(∂ 𝒜')
h𝒜ℬ : #𝒜' = #ℬ
hℬr : Set.Sized r (↑ℬ : Set (Finset (Fin n)))
hℬ : ∀ (U V : Finset (Fin n)), UV.UsefulCompression U V → IsCompressed U V ℬ
suffices : ℬ = 𝒞
⊢ #(∂ 𝒞) ≤ #(∂ 𝒜)

Tactic:
suffices ℬ = 𝒞 by subst 𝒞; exact hℬ𝒜.trans (by gcongr)
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
Goal:
n r : ℕ
𝒜 𝒞 : Finset (Finset (Fin n))
h𝒜r : Set.Sized r (↑𝒜 : Set (Finset (Fin n)))
h𝒞𝒜 : #𝒞 ≤ #𝒜
h𝒞 : IsInitSeg 𝒞 r
𝒜' : Finset (Finset (Fin n))
h𝒜 : 𝒜' ⊆ 𝒜
h𝒜𝒞 : #𝒜' = #𝒞
ℬ : Finset (Finset (Fin n))
hℬ𝒜 : #(∂ ℬ) ≤ #(∂ 𝒜')
h𝒜ℬ : #𝒜' = #ℬ
hℬr : Set.Sized r (↑ℬ : Set (Finset (Fin n)))
hℬ : ∀ (U V : Finset (Fin n)), UV.UsefulCompression U V → IsCompressed U V ℬ
⊢ #ℬ = #𝒞

Tactic:
have hcard : #ℬ = #𝒞 := h𝒜ℬ.symm.trans h𝒜𝒞
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
Goal:
n r : ℕ
𝒜 𝒞 : Finset (Finset (Fin n))
h𝒜r : Set.Sized r (↑𝒜 : Set (Finset (Fin n)))
h𝒞𝒜 : #𝒞 ≤ #𝒜
h𝒞 : IsInitSeg 𝒞 r
𝒜' : Finset (Finset (Fin n))
h𝒜 : 𝒜' ⊆ 𝒜
h𝒜𝒞 : #𝒜' = #𝒞
ℬ : Finset (Finset (Fin n))
hℬ𝒜 : #(∂ ℬ) ≤ #(∂ 𝒜')
h𝒜ℬ : #𝒜' = #ℬ
hℬr : Set.Sized r (↑ℬ : Set (Finset (Fin n)))
hℬ : ∀ (U V : Finset (Fin n)), UV.UsefulCompression U V → IsCompressed U V ℬ
hcard : #ℬ = #𝒞
inl : ∀ (h𝒞ℬ : 𝒞 ⊆ ℬ), ℬ = 𝒞
inr : ∀ (hℬ𝒞 : ℬ ⊆ 𝒞), ℬ = 𝒞
⊢ ℬ = 𝒞

Tactic:
obtain h𝒞ℬ | hℬ𝒞 := h𝒞.total (UV.isInitSeg_of_compressed hℬr hℬ)

Premises used: Finset.Colex.IsInitSeg.total, Finset.UV.isInitSeg_of_compressed
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
Goal:
n r : ℕ
𝒜 𝒞 : Finset (Finset (Fin n))
h𝒜r : Set.Sized r (↑𝒜 : Set (Finset (Fin n)))
h𝒞𝒜 : #𝒞 ≤ #𝒜
h𝒞 : IsInitSeg 𝒞 r
𝒜' : Finset (Finset (Fin n))
h𝒜 : 𝒜' ⊆ 𝒜
h𝒜𝒞 : #𝒜' = #𝒞
ℬ : Finset (Finset (Fin n))
hℬ𝒜 : #(∂ ℬ) ≤ #(∂ 𝒜')
h𝒜ℬ : #𝒜' = #ℬ
hℬr : Set.Sized r (↑ℬ : Set (Finset (Fin n)))
hℬ : ∀ (U V : Finset (Fin n)), UV.UsefulCompression U V → IsCompressed U V ℬ
hcard : #ℬ = #𝒞
h𝒞ℬ : 𝒞 ⊆ ℬ
⊢ ℬ = 𝒞

Tactic:
(eq_of_subset_of_card_le h𝒞ℬ hcard.le).symm

Premises used: Eq.le, Finset.eq_of_subset_of_card_le, Eq.symm
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
Goal:
n r : ℕ
𝒜 𝒞 : Finset (Finset (Fin n))
h𝒜r : Set.Sized r (↑𝒜 : Set (Finset (Fin n)))
h𝒞𝒜 : #𝒞 ≤ #𝒜
h𝒞 : IsInitSeg 𝒞 r
𝒜' : Finset (Finset (Fin n))
h𝒜 : 𝒜' ⊆ 𝒜
h𝒜𝒞 : #𝒜' = #𝒞
ℬ : Finset (Finset (Fin n))
hℬ𝒜 : #(∂ ℬ) ≤ #(∂ 𝒜')
h𝒜ℬ : #𝒜' = #ℬ
hℬr : Set.Sized r (↑ℬ : Set (Finset (Fin n)))
hℬ : ∀ (U V : Finset (Fin n)), UV.UsefulCompression U V → IsCompressed U V ℬ
hcard : #ℬ = #𝒞
h𝒞ℬ : 𝒞 ⊆ ℬ
⊢ ℬ = 𝒞

Tactic:
exact (eq_of_subset_of_card_le h𝒞ℬ hcard.le).symm

Premises used: Eq.le, Finset.eq_of_subset_of_card_le, Eq.symm
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
Goal:
n r : ℕ
𝒜 𝒞 : Finset (Finset (Fin n))
h𝒜r : Set.Sized r (↑𝒜 : Set (Finset (Fin n)))
h𝒞𝒜 : #𝒞 ≤ #𝒜
h𝒞 : IsInitSeg 𝒞 r
𝒜' : Finset (Finset (Fin n))
h𝒜 : 𝒜' ⊆ 𝒜
h𝒜𝒞 : #𝒜' = #𝒞
ℬ : Finset (Finset (Fin n))
hℬ𝒜 : #(∂ ℬ) ≤ #(∂ 𝒜')
h𝒜ℬ : #𝒜' = #ℬ
hℬr : Set.Sized r (↑ℬ : Set (Finset (Fin n)))
hℬ : ∀ (U V : Finset (Fin n)), UV.UsefulCompression U V → IsCompressed U V ℬ
hcard : #ℬ = #𝒞
hℬ𝒞 : ℬ ⊆ 𝒞
⊢ ℬ = 𝒞

Tactic:
eq_of_subset_of_card_le hℬ𝒞 hcard.ge

Premises used: Eq.ge, Finset.eq_of_subset_of_card_le
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
Goal:
n r : ℕ
𝒜 𝒞 : Finset (Finset (Fin n))
h𝒜r : Set.Sized r (↑𝒜 : Set (Finset (Fin n)))
h𝒞𝒜 : #𝒞 ≤ #𝒜
h𝒞 : IsInitSeg 𝒞 r
𝒜' : Finset (Finset (Fin n))
h𝒜 : 𝒜' ⊆ 𝒜
h𝒜𝒞 : #𝒜' = #𝒞
ℬ : Finset (Finset (Fin n))
hℬ𝒜 : #(∂ ℬ) ≤ #(∂ 𝒜')
h𝒜ℬ : #𝒜' = #ℬ
hℬr : Set.Sized r (↑ℬ : Set (Finset (Fin n)))
hℬ : ∀ (U V : Finset (Fin n)), UV.UsefulCompression U V → IsCompressed U V ℬ
hcard : #ℬ = #𝒞
hℬ𝒞 : ℬ ⊆ 𝒞
⊢ ℬ = 𝒞

Tactic:
exact eq_of_subset_of_card_le hℬ𝒞 hcard.ge

Premises used: Eq.ge, Finset.eq_of_subset_of_card_le
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
Goal:
n r : ℕ
𝒜 𝒞 : Finset (Finset (Fin n))
h₁ : Set.Sized r (↑𝒜 : Set (Finset (Fin n)))
h₂ : #𝒞 ≤ #𝒜
h₃ : IsInitSeg 𝒞 r
⊢ #(∂^[0] 𝒞) ≤ #(∂^[0] 𝒜)

Tactic:
simpa
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
Goal:
n n_1 : ℕ
ih :
  ∀ {r : ℕ} {𝒜 𝒞 : Finset (Finset (Fin n))} (h₁ : Set.Sized r (↑𝒜 : Set (Finset (Fin n)))) (h₂ : #𝒞 ≤ #𝒜)
    (h₃ : IsInitSeg 𝒞 r), #(∂^[n_1] 𝒞) ≤ #(∂^[n_1] 𝒜)
r : ℕ
𝒜 𝒞 : Finset (Finset (Fin n))
h₁ : Set.Sized r (↑𝒜 : Set (Finset (Fin n)))
h₂ : #𝒞 ≤ #𝒜
h₃ : IsInitSeg 𝒞 r
⊢ #(∂^[n_1 + 1] 𝒞) ≤ #(∂^[n_1 + 1] 𝒜)

Tactic:
ih h₁.shadow (kruskal_katona h₁ h₂ h₃) ?_

Premises used: Nat.iterate, Finset.kruskal_katona, Set.Sized.shadow
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
Goal:
n n_1 : ℕ
ih :
  ∀ {r : ℕ} {𝒜 𝒞 : Finset (Finset (Fin n))} (h₁ : Set.Sized r (↑𝒜 : Set (Finset (Fin n)))) (h₂ : #𝒞 ≤ #𝒜)
    (h₃ : IsInitSeg 𝒞 r), #(∂^[n_1] 𝒞) ≤ #(∂^[n_1] 𝒜)
r : ℕ
𝒜 𝒞 : Finset (Finset (Fin n))
h₁ : Set.Sized r (↑𝒜 : Set (Finset (Fin n)))
h₂ : #𝒞 ≤ #𝒜
h₃ : IsInitSeg 𝒞 r
succ : IsInitSeg (∂ 𝒞) (r - 1)
⊢ #(∂^[n_1 + 1] 𝒞) ≤ #(∂^[n_1 + 1] 𝒜)

Tactic:
refine ih h₁.shadow (kruskal_katona h₁ h₂ h₃) ?_

Premises used: Finset.kruskal_katona, Set.Sized.shadow
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
Goal:
n n_1 : ℕ
ih :
  ∀ {r : ℕ} {𝒜 𝒞 : Finset (Finset (Fin n))} (h₁ : Set.Sized r (↑𝒜 : Set (Finset (Fin n)))) (h₂ : #𝒞 ≤ #𝒜)
    (h₃ : IsInitSeg 𝒞 r), #(∂^[n_1] 𝒞) ≤ #(∂^[n_1] 𝒜)
r : ℕ
𝒜 𝒞 : Finset (Finset (Fin n))
h₁ : Set.Sized r (↑𝒜 : Set (Finset (Fin n)))
h₂ : #𝒞 ≤ #𝒜
h₃ : IsInitSeg 𝒞 r
⊢ IsInitSeg (∂ 𝒞) (r - 1)

Tactic:
h₃.shadow

Premises used: Finset.Colex.IsInitSeg.shadow
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
Goal:
n n_1 : ℕ
ih :
  ∀ {r : ℕ} {𝒜 𝒞 : Finset (Finset (Fin n))} (h₁ : Set.Sized r (↑𝒜 : Set (Finset (Fin n)))) (h₂ : #𝒞 ≤ #𝒜)
    (h₃ : IsInitSeg 𝒞 r), #(∂^[n_1] 𝒞) ≤ #(∂^[n_1] 𝒜)
r : ℕ
𝒜 𝒞 : Finset (Finset (Fin n))
h₁ : Set.Sized r (↑𝒜 : Set (Finset (Fin n)))
h₂ : #𝒞 ≤ #𝒜
h₃ : IsInitSeg 𝒞 r
⊢ IsInitSeg (∂ 𝒞) (r - 1)

Tactic:
convert! h₃.shadow

Premises used: Finset.Colex.IsInitSeg.shadow
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
Goal:
n r k : ℕ
𝒜 𝒞 : Finset (Finset (Fin n))
h₁ : Set.Sized r (↑𝒜 : Set (Finset (Fin n)))
h₂ : #𝒞 ≤ #𝒜
h₃ : IsInitSeg 𝒞 r
zero :
  ∀ {r : ℕ} {𝒜 𝒞 : Finset (Finset (Fin n))} (h₁ : Set.Sized r (↑𝒜 : Set (Finset (Fin n)))) (h₂ : #𝒞 ≤ #𝒜)
    (h₃ : IsInitSeg 𝒞 r), #(∂^[0] 𝒞) ≤ #(∂^[0] 𝒜)
succ :
  ∀ (n_1 : ℕ)
    (ih :
      ∀ {r : ℕ} {𝒜 𝒞 : Finset (Finset (Fin n))} (h₁ : Set.Sized r (↑𝒜 : Set (Finset (Fin n)))) (h₂ : #𝒞 ≤ #𝒜)
        (h₃ : IsInitSeg 𝒞 r), #(∂^[n_1] 𝒞) ≤ #(∂^[n_1] 𝒜))
    {r : ℕ} {𝒜 𝒞 : Finset (Finset (Fin n))} (h₁ : Set.Sized r (↑𝒜 : Set (Finset (Fin n)))) (h₂ : #𝒞 ≤ #𝒜)
    (h₃ : IsInitSeg 𝒞 r), #(∂^[n_1 + 1] 𝒞) ≤ #(∂^[n_1 + 1] 𝒜)
⊢ #(∂^[k] 𝒞) ≤ #(∂^[k] 𝒜)

Tactic:
induction k generalizing r 𝒜 𝒞 with
  | zero => simpa
  | succ _ ih =>
    refine ih h₁.shadow (kruskal_katona h₁ h₂ h₃) ?_
    convert! h₃.shadow

Premises used: Finset.Colex.IsInitSeg.shadow, Nat.zero, Nat.succ
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
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 ≤ #𝒜
m : ℕ
rw : m < k → m < n
⊢ m ∈ range k → m < n

Tactic:
rw [mem_range]

Premises used: Finset.mem_range
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
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 ≤ #𝒜
m : ℕ
⊢ m < k → m < n

Tactic:
apply forall_lt_iff_le.2 hkn

Premises used: Iff.mpr, forall_lt_iff_le
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
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
⊢ Set.Sized r (↑𝒞 : Set (Finset (Fin n)))

Tactic:
have : (𝒞 : Set (Finset (Fin n))).Sized r := Set.sized_powersetCard _ _
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
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)))
rw : k.choose (r - i) = (#range'k).choose (r - i)
rw₁ : k.choose (r - i) = (#(range k)).choose (r - i)
rw₂ rw₃ : k.choose (r - i) = k.choose (r - i)
⊢ k.choose (r - i) = #(powersetCard (r - i) range'k)

Tactic:
rw [card_powersetCard, card_attachFin, card_range]

Premises used: Finset.card_range, Finset.card_attachFin, Finset.card_powersetCard
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
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)))
h : powersetCard (r - i) range'k = ∂^[i] 𝒞
⊢ #(powersetCard (r - i) range'k) = #(∂^[i] 𝒞)

Tactic:
congr!
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
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)))
h : ∀ (B : Finset (Fin n)), B ∈ powersetCard (r - i) range'k ↔ B ∈ ∂^[i] 𝒞
⊢ powersetCard (r - i) range'k = ∂^[i] 𝒞

Tactic:
ext B
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
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 ∈ powersetCard (r - i) range'k ↔ B ∈ ∂^[i] 𝒞

Tactic:
rw [mem_powersetCard, mem_shadow_iterate_iff_exists_sdiff]

Premises used: Finset.mem_shadow_iterate_iff_exists_sdiff, Finset.mem_powersetCard
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
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
h₃ : (∃ s ∈ 𝒞, B ⊆ s ∧ #(s \ B) = i) → B ⊆ range'k ∧ #B = r - i
⊢ B ⊆ range'k ∧ #B = r - i ↔ ∃ s ∈ 𝒞, B ⊆ s ∧ #(s \ B) = i

Tactic:
constructor
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
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
rwa₃ : i + r - i ≤ k
rwa₄ rwa₅ rwa₆ rwa₇ : r ≤ k
⊢ i + #B ≤ #range'k

Tactic:
rwa [hB, card_attachFin, card_range, ← Nat.add_sub_assoc hir, Nat.add_sub_cancel_left]

Premises used: Nat.add_sub_assoc, Finset.card_range, Nat.add_sub_cancel_left, Finset.card_attachFin
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
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
⊢ ∃ (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]
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
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
h : ∀ (C : Finset (Fin n)) (BsubC : B ⊆ C) (hCrange : C ⊆ range'k) (hcard : #C = i + #B), ∃ s ∈ 𝒞, B ⊆ s ∧ #(s \ B) = i
⊢ ∃ s ∈ 𝒞, B ⊆ s ∧ #(s \ B) = i

Tactic:
obtain ⟨C, BsubC, hCrange, hcard⟩ := this
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
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
⊢ #C = r

Tactic:
rw [hB, ← Nat.add_sub_assoc hir, Nat.add_sub_cancel_left] at hcard

Premises used: Nat.add_sub_assoc, Nat.add_sub_cancel_left
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
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

Tactic:
⟨C, mem_powersetCard.2 ⟨hCrange, hcard⟩, BsubC, ?_⟩

Premises used: Iff.mpr, Finset.mem_powersetCard, And.intro, Exists.intro
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
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
⊢ ∃ s ∈ 𝒞, B ⊆ s ∧ #(s \ B) = i

Tactic:
refine ⟨C, mem_powersetCard.2 ⟨hCrange, hcard⟩, BsubC, ?_⟩
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
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
h₅ h₆ : i = i
⊢ #(C \ B) = i

Tactic:
rw [card_sdiff_of_subset BsubC, hcard, hB, Nat.sub_sub_self hir]

Premises used: Nat.sub_sub_self, Finset.card_sdiff_of_subset
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
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
⊢ A ⊆ range'k ∧ #A = r

Tactic:
rw [mem_powersetCard] at Ah

Premises used: Finset.mem_powersetCard
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
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
Ah₁ : A ⊆ range'k ∧ #A = r
⊢ B ⊆ A

Tactic:
rw [mem_powersetCard] at Ah

Premises used: Finset.mem_powersetCard
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
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
Ah₁ : A ⊆ range'k ∧ #A = r
hBA₁ : B ⊆ A
⊢ #(A \ B) = i

Tactic:
rw [mem_powersetCard] at Ah

Premises used: Finset.mem_powersetCard
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
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

Tactic:
⟨hBA.trans Ah.1, eq_tsub_of_add_eq ?_⟩

Premises used: HasSubset.Subset.trans, eq_tsub_of_add_eq, And.left, And.intro
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
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 = r
⊢ B ⊆ range'k ∧ #B = r - i

Tactic:
refine ⟨hBA.trans Ah.1, eq_tsub_of_add_eq ?_⟩
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
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
h₅ h₆ : #A = #A
⊢ #B + i = r

Tactic:
rw [← Ah.2, ← card_sdiff_i, add_comm, card_sdiff_add_card_eq_card hBA]

Premises used: add_comm, And.right, Finset.card_sdiff_add_card_eq_card
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
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] 𝒜)

Tactic:
iterated_kk h₁ ?_ ⟨‹_›, ?_⟩

Premises used: Finset.iterated_kk, And.intro