awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)))
refine_1 : #𝒞 ≤ #𝒜
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 ∈ 𝒞
⊢ #(∂^[i] 𝒞) ≤ #(∂^[i] 𝒜)

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

Premises used: Finset.iterated_kk, 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)))
refine_1 : (#range'k).choose r ≤ #𝒜
refine_1₁ : (#(range k)).choose r ≤ #𝒜
refine_1₂ refine_1₃ refine_1₄ refine_1₅ : k.choose r ≤ #𝒜
⊢ #𝒞 ≤ #𝒜

Tactic:
rwa [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)))
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
⊢ ∀ ⦃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:
simp_rw [𝒞, mem_powersetCard]

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)))
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

Tactic:
⟨fun t ht ↦ ?_, ‹_›⟩

Premises used: 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)))
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
refine_2 : ∀ (t : Fin n) (ht : t ∈ B), t ∈ range'k
⊢ B ⊆ range'k ∧ #B = r

Tactic:
refine ⟨fun t ht ↦ ?_, ‹_›⟩
-- 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)))
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
refine_2 : (↑t : ℕ) < k
⊢ t ∈ range'k

Tactic:
rw [mem_attachFin, mem_range]

Premises used: Finset.mem_range, Finset.mem_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)))
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
rwa rwa₁ rwa₂ rwa₃ :
  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)))
⊢ 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:
rwa [toColex_image_lt_toColex_image Fin.val_strictMono]

Premises used: Finset.Colex.toColex_image_lt_toColex_image, Fin.val_strictMono
-- 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)))
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
⊢ 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]
-- 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)))
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 ℕ))
apply : ∀ b ∈ image Fin.val A, b < k
⊢ (↑t : ℕ) < k

Tactic:
apply Colex.forall_lt_mono this.le _ t (mem_image.2 ⟨t, ht, rfl⟩)

Premises used: Iff.mpr, Finset.mem_image, Finset.Colex.forall_lt_mono, LT.lt.le, Fin.val, And.intro, Exists.intro, rfl
-- 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)))
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 ℕ))
simp_rw : ∀ (b : ℕ), (∃ a ∈ A, (↑a : ℕ) = b) → b < k
⊢ ∀ b ∈ image Fin.val A, b < k

Tactic:
simp_rw [mem_image]

Premises used: Finset.mem_image
-- 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)))
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 : ℕ
a : Fin n
ha : a ∈ A
hab : (↑a : ℕ) = b
⊢ b < k

Tactic:
simpa [range'k, hab] using hA.1 ha

Premises used: And.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)))
_ : k.choose (r - i) = #(powersetCard (r - i) range'k)
_₁ : #(powersetCard (r - i) range'k) = #(∂^[i] 𝒞)
_₂ : #(∂^[i] 𝒞) ≤ #(∂^[i] 𝒜)
⊢ k.choose (r - 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

Premises used: Finset.shadow, Nat.choose, HSub.hSub, Nat.iterate, Finset.powersetCard
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
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)
inr : ∀ (h1r : r > 0), #𝒜 ≤ (n - 1).choose (r - 1)
⊢ #𝒜 ≤ (n - 1).choose (r - 1)

Tactic:
rcases Nat.eq_zero_or_pos r with b | h1r

Premises used: Nat.eq_zero_or_pos
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
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 ≤ (n - 1).choose (r - 1)

Tactic:
Nat.zero_le _

Premises used: Nat.zero_le
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
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
h : #𝒜 = 0
⊢ #𝒜 ≤ (n - 1).choose (r - 1)

Tactic:
convert! Nat.zero_le _

Premises used: Nat.zero_le
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
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
h : ∀ (x : Finset (Fin n)), x ∉ 𝒜
⊢ #𝒜 = 0

Tactic:
rw [Finset.card_eq_zero, eq_empty_iff_forall_notMem]

Premises used: Finset.eq_empty_iff_forall_notMem, Finset.card_eq_zero
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
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 ∉ 𝒜

Tactic:
fun A HA ↦ h𝒜 HA HA ?_

Premises used: Not
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
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
h : ∀ (A : Finset (Fin n)) (HA : A ∈ 𝒜), Disjoint A A
⊢ ∀ (x : Finset (Fin n)), x ∉ 𝒜

Tactic:
refine fun A HA ↦ h𝒜 HA HA ?_
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
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 ∈ 𝒜
h : #A = r
⊢ Disjoint A A

Tactic:
rw [disjoint_self_iff_empty, ← Finset.card_eq_zero, ← b]

Premises used: Finset.disjoint_self_iff_empty, Finset.card_eq_zero
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
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 ∈ 𝒜
⊢ #A = r

Tactic:
h₂ HA
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
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 ∈ 𝒜
⊢ #A = r

Tactic:
exact h₂ HA
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
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)

Tactic:
le_of_not_gt fun size ↦ ?_

Premises used: le_of_not_gt
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
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
inr : ∀ (size : (n - 1).choose (r - 1) < #𝒜), False
⊢ #𝒜 ≤ (n - 1).choose (r - 1)

Tactic:
refine le_of_not_gt fun size ↦ ?_

Premises used: le_of_not_gt
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
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 ∈ 𝒜
⊢ ∃ (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

Premises used: Finset.mem_shadow_iterate_iff_exists_sdiff, Finset.mem_compls
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
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
obtain : ∀ (C : Finset (Fin n)) (hC : Cᶜ ∈ 𝒜) (hAC : A ⊆ C), #(C \ A) = n - 2 * r → False
⊢ False

Tactic:
obtain ⟨C, hC, hAC, _⟩ := hAbar
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
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 ∈ 𝒜
C : Finset (Fin n)
hC : Cᶜ ∈ 𝒜
hAC : A ⊆ C
right : #(C \ A) = n - 2 * r
⊢ False

Tactic:
h𝒜 hA hC (disjoint_of_subset_left hAC disjoint_compl_right)

Premises used: Finset.disjoint_of_subset_left, disjoint_compl_right
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
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 ∈ 𝒜
C : Finset (Fin n)
hC : Cᶜ ∈ 𝒜
hAC : A ⊆ C
right : #(C \ A) = n - 2 * r
⊢ False

Tactic:
exact h𝒜 hA hC (disjoint_of_subset_left hAC disjoint_compl_right)

Premises used: Finset.disjoint_of_subset_left, disjoint_compl_right
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
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) < #𝒜
⊢ 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)
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
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] 𝒜ᶜˢ)
⊢ r ≤ n

Tactic:
have : r ≤ n := h₃.trans (Nat.div_le_self n 2)
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
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
⊢ 1 ≤ n

Tactic:
have : 1 ≤ n := ‹1 ≤ r›.trans ‹r ≤ n›
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
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
rwa : (n - 1).choose (n - r) < #𝒜
rwa₁ rwa₂ rwa₃ rwa₄ : (n - 1).choose (r - 1) < #𝒜
⊢ (n - 1).choose (n - r) < #𝒜ᶜˢ

Tactic:
rwa [card_compls, choose_symm_of_eq_add (tsub_add_tsub_cancel ‹r ≤ n› ‹1 ≤ r›).symm]

Premises used: Finset.card_compls, Eq.symm, tsub_add_tsub_cancel, Nat.choose_symm_of_eq_add
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
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) < #𝒜ᶜˢ

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]
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
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) < #𝒜ᶜˢ
⊢ Set.Sized (n - r) (↑𝒜ᶜˢ : Set (Finset (Fin n)))

Tactic:
simpa using h₂.compls

Premises used: Set.Sized.compls
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
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) < #𝒜ᶜˢ
⊢ Set.Sized (n - r) (↑𝒜ᶜˢ : Set (Finset (Fin n)))

Tactic:
have h𝒜bar : (𝒜ᶜˢ : Set (Finset (Fin n))).Sized (n - r) := by simpa using h₂.compls
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
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)))
⊢ n - 2 * r ≤ n - r

Tactic:
lia
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
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)))
⊢ (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
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
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] 𝒜ᶜˢ)
⊢ n - r - (n - 2 * r) = r

Tactic:
lia
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
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] 𝒜ᶜˢ)
⊢ n - r - (n - 2 * r) = r

Tactic:
have : n - r - (n - 2 * r) = r := by lia
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
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
⊢ (n - 1).choose r ≤ #(∂^[n - 2 * r] 𝒜ᶜˢ)

Tactic:
rw [this] at kk