internlm/Lean-Github huggingface dataset:
Theorem: Finset.UV.kruskal_katona_helper
Proof state before:
case inl
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n r : ℕ
𝒜 A : Finset (Finset (Fin n))
ih :
  ∀ (y : Finset (Finset (Fin n))),
    InvImage (fun x x_1 => x < x_1) Finset.UV.familyMeasure y A →
      Set.Sized r ↑y →
        ∃ ℬ,
          (∂ ℬ).card ≤ (∂ y).card ∧
            y.card = ℬ.card ∧
              Set.Sized r ↑ℬ ∧ ∀ (U V : Finset (Fin n)), Finset.UV.UsefulCompression U V → IsCompressed U V ℬ
h : Set.Sized r ↑A
usable : Finset (Finset (Fin n) × Finset (Fin n)) :=
  filter (fun t => Finset.UV.UsefulCompression t.1 t.2 ∧ ¬IsCompressed t.1 t.2 A) univ
husable : usable = ∅
⊢ ∃ ℬ,
    (∂ ℬ).card ≤ (∂ A).card ∧
      A.card = ℬ.card ∧ Set.Sized r ↑ℬ ∧ ∀ (U V : Finset (Fin n)), Finset.UV.UsefulCompression U V → IsCompressed U V ℬ
Tactic:
refine' ⟨A, le_rfl, rfl, h, fun U V hUV ↦ _⟩
Proof state after:
case inl
α : Type u_1
inst✝ : LinearOrder α
s U✝ V✝ : Finset α
n r : ℕ
𝒜 A : Finset (Finset (Fin n))
ih :
  ∀ (y : Finset (Finset (Fin n))),
    InvImage (fun x x_1 => x < x_1) Finset.UV.familyMeasure y A →
      Set.Sized r ↑y →
        ∃ ℬ,
          (∂ ℬ).card ≤ (∂ y).card ∧
            y.card = ℬ.card ∧
              Set.Sized r ↑ℬ ∧ ∀ (U V : Finset (Fin n)), Finset.UV.UsefulCompression U V → IsCompressed U V ℬ
h : Set.Sized r ↑A
usable : Finset (Finset (Fin n) × Finset (Fin n)) :=
  filter (fun t => Finset.UV.UsefulCompression t.1 t.2 ∧ ¬IsCompressed t.1 t.2 A) univ
husable : usable = ∅
U V : Finset (Fin n)
hUV : Finset.UV.UsefulCompression U V
⊢ IsCompressed U V A
Theorem: Finset.UV.kruskal_katona_helper
Proof state before:
case inl
α : Type u_1
inst✝ : LinearOrder α
s U✝ V✝ : Finset α
n r : ℕ
𝒜 A : Finset (Finset (Fin n))
ih :
  ∀ (y : Finset (Finset (Fin n))),
    InvImage (fun x x_1 => x < x_1) Finset.UV.familyMeasure y A →
      Set.Sized r ↑y →
        ∃ ℬ,
          (∂ ℬ).card ≤ (∂ y).card ∧
            y.card = ℬ.card ∧
              Set.Sized r ↑ℬ ∧ ∀ (U V : Finset (Fin n)), Finset.UV.UsefulCompression U V → IsCompressed U V ℬ
h : Set.Sized r ↑A
usable : Finset (Finset (Fin n) × Finset (Fin n)) :=
  filter (fun t => Finset.UV.UsefulCompression t.1 t.2 ∧ ¬IsCompressed t.1 t.2 A) univ
husable : usable = ∅
U V : Finset (Fin n)
hUV : Finset.UV.UsefulCompression U V
⊢ IsCompressed U V A
Tactic:
rw [eq_empty_iff_forall_not_mem] at husable
Proof state after:
case inl
α : Type u_1
inst✝ : LinearOrder α
s U✝ V✝ : Finset α
n r : ℕ
𝒜 A : Finset (Finset (Fin n))
ih :
  ∀ (y : Finset (Finset (Fin n))),
    InvImage (fun x x_1 => x < x_1) Finset.UV.familyMeasure y A →
      Set.Sized r ↑y →
        ∃ ℬ,
          (∂ ℬ).card ≤ (∂ y).card ∧
            y.card = ℬ.card ∧
              Set.Sized r ↑ℬ ∧ ∀ (U V : Finset (Fin n)), Finset.UV.UsefulCompression U V → IsCompressed U V ℬ
h : Set.Sized r ↑A
usable : Finset (Finset (Fin n) × Finset (Fin n)) :=
  filter (fun t => Finset.UV.UsefulCompression t.1 t.2 ∧ ¬IsCompressed t.1 t.2 A) univ
husable : ∀ (x : Finset (Fin n) × Finset (Fin n)), x ∉ usable
U V : Finset (Fin n)
hUV : Finset.UV.UsefulCompression U V
⊢ IsCompressed U V A
Theorem: Finset.UV.kruskal_katona_helper
Proof state before:
case inl
α : Type u_1
inst✝ : LinearOrder α
s U✝ V✝ : Finset α
n r : ℕ
𝒜 A : Finset (Finset (Fin n))
ih :
  ∀ (y : Finset (Finset (Fin n))),
    InvImage (fun x x_1 => x < x_1) Finset.UV.familyMeasure y A →
      Set.Sized r ↑y →
        ∃ ℬ,
          (∂ ℬ).card ≤ (∂ y).card ∧
            y.card = ℬ.card ∧
              Set.Sized r ↑ℬ ∧ ∀ (U V : Finset (Fin n)), Finset.UV.UsefulCompression U V → IsCompressed U V ℬ
h : Set.Sized r ↑A
usable : Finset (Finset (Fin n) × Finset (Fin n)) :=
  filter (fun t => Finset.UV.UsefulCompression t.1 t.2 ∧ ¬IsCompressed t.1 t.2 A) univ
husable : ∀ (x : Finset (Fin n) × Finset (Fin n)), x ∉ usable
U V : Finset (Fin n)
hUV : Finset.UV.UsefulCompression U V
⊢ IsCompressed U V A
Tactic:
by_contra h
Proof state after:
case inl
α : Type u_1
inst✝ : LinearOrder α
s U✝ V✝ : Finset α
n r : ℕ
𝒜 A : Finset (Finset (Fin n))
ih :
  ∀ (y : Finset (Finset (Fin n))),
    InvImage (fun x x_1 => x < x_1) Finset.UV.familyMeasure y A →
      Set.Sized r ↑y →
        ∃ ℬ,
          (∂ ℬ).card ≤ (∂ y).card ∧
            y.card = ℬ.card ∧
              Set.Sized r ↑ℬ ∧ ∀ (U V : Finset (Fin n)), Finset.UV.UsefulCompression U V → IsCompressed U V ℬ
h✝ : Set.Sized r ↑A
usable : Finset (Finset (Fin n) × Finset (Fin n)) :=
  filter (fun t => Finset.UV.UsefulCompression t.1 t.2 ∧ ¬IsCompressed t.1 t.2 A) univ
husable : ∀ (x : Finset (Fin n) × Finset (Fin n)), x ∉ usable
U V : Finset (Fin n)
hUV : Finset.UV.UsefulCompression U V
h : ¬IsCompressed U V A
⊢ False
Theorem: Finset.UV.kruskal_katona_helper
Proof state before:
case inl
α : Type u_1
inst✝ : LinearOrder α
s U✝ V✝ : Finset α
n r : ℕ
𝒜 A : Finset (Finset (Fin n))
ih :
  ∀ (y : Finset (Finset (Fin n))),
    InvImage (fun x x_1 => x < x_1) Finset.UV.familyMeasure y A →
      Set.Sized r ↑y →
        ∃ ℬ,
          (∂ ℬ).card ≤ (∂ y).card ∧
            y.card = ℬ.card ∧
              Set.Sized r ↑ℬ ∧ ∀ (U V : Finset (Fin n)), Finset.UV.UsefulCompression U V → IsCompressed U V ℬ
h✝ : Set.Sized r ↑A
usable : Finset (Finset (Fin n) × Finset (Fin n)) :=
  filter (fun t => Finset.UV.UsefulCompression t.1 t.2 ∧ ¬IsCompressed t.1 t.2 A) univ
husable : ∀ (x : Finset (Fin n) × Finset (Fin n)), x ∉ usable
U V : Finset (Fin n)
hUV : Finset.UV.UsefulCompression U V
h : ¬IsCompressed U V A
⊢ False
Tactic:
exact husable ⟨U, V⟩ $ mem_filter.2 ⟨mem_univ _, hUV, h⟩
Proof state after:
no goals
Theorem: Finset.UV.kruskal_katona_helper
Proof state before:
α : Type u_1
inst✝ : LinearOrder α
s U✝ V✝ : Finset α
n r : ℕ
𝒜 A : Finset (Finset (Fin n))
ih :
  ∀ (y : Finset (Finset (Fin n))),
    InvImage (fun x x_1 => x < x_1) Finset.UV.familyMeasure y A →
      Set.Sized r ↑y →
        ∃ ℬ,
          (∂ ℬ).card ≤ (∂ y).card ∧
            y.card = ℬ.card ∧
              Set.Sized r ↑ℬ ∧ ∀ (U V : Finset (Fin n)), Finset.UV.UsefulCompression U V → IsCompressed U V ℬ
h : Set.Sized r ↑A
usable : Finset (Finset (Fin n) × Finset (Fin n)) :=
  filter (fun t => Finset.UV.UsefulCompression t.1 t.2 ∧ ¬IsCompressed t.1 t.2 A) univ
husable : usable.Nonempty
U V : Finset (Fin n)
hUV : (U, V) ∈ univ ∧ Finset.UV.UsefulCompression (U, V).1 (U, V).2 ∧ ¬IsCompressed (U, V).1 (U, V).2 A
t : ∀ x' ∈ usable, (U, V).1.card ≤ x'.1.card
⊢ ∀ (U₁ V₁ : Finset (Fin n)), Finset.UV.UsefulCompression U₁ V₁ → U₁.card < U.card → IsCompressed U₁ V₁ A
Tactic:
rintro U₁ V₁ huseful hUcard
Proof state after:
α : Type u_1
inst✝ : LinearOrder α
s U✝ V✝ : Finset α
n r : ℕ
𝒜 A : Finset (Finset (Fin n))
ih :
  ∀ (y : Finset (Finset (Fin n))),
    InvImage (fun x x_1 => x < x_1) Finset.UV.familyMeasure y A →
      Set.Sized r ↑y →
        ∃ ℬ,
          (∂ ℬ).card ≤ (∂ y).card ∧
            y.card = ℬ.card ∧
              Set.Sized r ↑ℬ ∧ ∀ (U V : Finset (Fin n)), Finset.UV.UsefulCompression U V → IsCompressed U V ℬ
h : Set.Sized r ↑A
usable : Finset (Finset (Fin n) × Finset (Fin n)) :=
  filter (fun t => Finset.UV.UsefulCompression t.1 t.2 ∧ ¬IsCompressed t.1 t.2 A) univ
husable : usable.Nonempty
U V : Finset (Fin n)
hUV : (U, V) ∈ univ ∧ Finset.UV.UsefulCompression (U, V).1 (U, V).2 ∧ ¬IsCompressed (U, V).1 (U, V).2 A
t : ∀ x' ∈ usable, (U, V).1.card ≤ x'.1.card
U₁ V₁ : Finset (Fin n)
huseful : Finset.UV.UsefulCompression U₁ V₁
hUcard : U₁.card < U.card
⊢ IsCompressed U₁ V₁ A
Theorem: Finset.UV.kruskal_katona_helper
Proof state before:
α : Type u_1
inst✝ : LinearOrder α
s U✝ V✝ : Finset α
n r : ℕ
𝒜 A : Finset (Finset (Fin n))
ih :
  ∀ (y : Finset (Finset (Fin n))),
    InvImage (fun x x_1 => x < x_1) Finset.UV.familyMeasure y A →
      Set.Sized r ↑y →
        ∃ ℬ,
          (∂ ℬ).card ≤ (∂ y).card ∧
            y.card = ℬ.card ∧
              Set.Sized r ↑ℬ ∧ ∀ (U V : Finset (Fin n)), Finset.UV.UsefulCompression U V → IsCompressed U V ℬ
h : Set.Sized r ↑A
usable : Finset (Finset (Fin n) × Finset (Fin n)) :=
  filter (fun t => Finset.UV.UsefulCompression t.1 t.2 ∧ ¬IsCompressed t.1 t.2 A) univ
husable : usable.Nonempty
U V : Finset (Fin n)
hUV : (U, V) ∈ univ ∧ Finset.UV.UsefulCompression (U, V).1 (U, V).2 ∧ ¬IsCompressed (U, V).1 (U, V).2 A
t : ∀ x' ∈ usable, (U, V).1.card ≤ x'.1.card
U₁ V₁ : Finset (Fin n)
huseful : Finset.UV.UsefulCompression U₁ V₁
hUcard : U₁.card < U.card
⊢ IsCompressed U₁ V₁ A
Tactic:
by_contra h
Proof state after:
α : Type u_1
inst✝ : LinearOrder α
s U✝ V✝ : Finset α
n r : ℕ
𝒜 A : Finset (Finset (Fin n))
ih :
  ∀ (y : Finset (Finset (Fin n))),
    InvImage (fun x x_1 => x < x_1) Finset.UV.familyMeasure y A →
      Set.Sized r ↑y →
        ∃ ℬ,
          (∂ ℬ).card ≤ (∂ y).card ∧
            y.card = ℬ.card ∧
              Set.Sized r ↑ℬ ∧ ∀ (U V : Finset (Fin n)), Finset.UV.UsefulCompression U V → IsCompressed U V ℬ
h✝ : Set.Sized r ↑A
usable : Finset (Finset (Fin n) × Finset (Fin n)) :=
  filter (fun t => Finset.UV.UsefulCompression t.1 t.2 ∧ ¬IsCompressed t.1 t.2 A) univ
husable : usable.Nonempty
U V : Finset (Fin n)
hUV : (U, V) ∈ univ ∧ Finset.UV.UsefulCompression (U, V).1 (U, V).2 ∧ ¬IsCompressed (U, V).1 (U, V).2 A
t : ∀ x' ∈ usable, (U, V).1.card ≤ x'.1.card
U₁ V₁ : Finset (Fin n)
huseful : Finset.UV.UsefulCompression U₁ V₁
hUcard : U₁.card < U.card
h : ¬IsCompressed U₁ V₁ A
⊢ False
Theorem: Finset.UV.kruskal_katona_helper
Proof state before:
α : Type u_1
inst✝ : LinearOrder α
s U✝ V✝ : Finset α
n r : ℕ
𝒜 A : Finset (Finset (Fin n))
ih :
  ∀ (y : Finset (Finset (Fin n))),
    InvImage (fun x x_1 => x < x_1) Finset.UV.familyMeasure y A →
      Set.Sized r ↑y →
        ∃ ℬ,
          (∂ ℬ).card ≤ (∂ y).card ∧
            y.card = ℬ.card ∧
              Set.Sized r ↑ℬ ∧ ∀ (U V : Finset (Fin n)), Finset.UV.UsefulCompression U V → IsCompressed U V ℬ
h✝ : Set.Sized r ↑A
usable : Finset (Finset (Fin n) × Finset (Fin n)) :=
  filter (fun t => Finset.UV.UsefulCompression t.1 t.2 ∧ ¬IsCompressed t.1 t.2 A) univ
husable : usable.Nonempty
U V : Finset (Fin n)
hUV : (U, V) ∈ univ ∧ Finset.UV.UsefulCompression (U, V).1 (U, V).2 ∧ ¬IsCompressed (U, V).1 (U, V).2 A
t : ∀ x' ∈ usable, (U, V).1.card ≤ x'.1.card
U₁ V₁ : Finset (Fin n)
huseful : Finset.UV.UsefulCompression U₁ V₁
hUcard : U₁.card < U.card
h : ¬IsCompressed U₁ V₁ A
⊢ False
Tactic:
exact hUcard.not_le $ t ⟨U₁, V₁⟩ $ mem_filter.2 ⟨mem_univ _, huseful, h⟩
Proof state after:
no goals
Theorem: Finset.kruskal_katona
Proof state before:
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n r k i : ℕ
𝒜 𝒞 : Finset (Finset (Fin n))
h₁ : Set.Sized r ↑𝒜
h₂ : 𝒜.card = 𝒞.card
h₃ : IsInitSeg 𝒞 r
⊢ (∂ 𝒞).card ≤ (∂ 𝒜).card
Tactic:
obtain ⟨ℬ, card_le, t, hℬ, fully_comp⟩ := UV.kruskal_katona_helper 𝒜 h₁
Proof state after:
case intro.intro.intro.intro
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n r k i : ℕ
𝒜 𝒞 : Finset (Finset (Fin n))
h₁ : Set.Sized r ↑𝒜
h₂ : 𝒜.card = 𝒞.card
h₃ : IsInitSeg 𝒞 r
ℬ : Finset (Finset (Fin n))
card_le : (∂ ℬ).card ≤ (∂ 𝒜).card
t : 𝒜.card = ℬ.card
hℬ : Set.Sized r ↑ℬ
fully_comp : ∀ (U V : Finset (Fin n)), Finset.UV.UsefulCompression U V → IsCompressed U V ℬ
⊢ (∂ 𝒞).card ≤ (∂ 𝒜).card
Theorem: Finset.kruskal_katona
Proof state before:
case intro.intro.intro.intro
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n r k i : ℕ
𝒜 𝒞 : Finset (Finset (Fin n))
h₁ : Set.Sized r ↑𝒜
h₂ : 𝒜.card = 𝒞.card
h₃ : IsInitSeg 𝒞 r
ℬ : Finset (Finset (Fin n))
card_le : (∂ ℬ).card ≤ (∂ 𝒜).card
t : 𝒜.card = ℬ.card
hℬ : Set.Sized r ↑ℬ
fully_comp : ∀ (U V : Finset (Fin n)), Finset.UV.UsefulCompression U V → IsCompressed U V ℬ
⊢ (∂ 𝒞).card ≤ (∂ 𝒜).card
Tactic:
convert card_le
Proof state after:
case h.e'_3.h.e'_2.h.e'_3
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n r k i : ℕ
𝒜 𝒞 : Finset (Finset (Fin n))
h₁ : Set.Sized r ↑𝒜
h₂ : 𝒜.card = 𝒞.card
h₃ : IsInitSeg 𝒞 r
ℬ : Finset (Finset (Fin n))
card_le : (∂ ℬ).card ≤ (∂ 𝒜).card
t : 𝒜.card = ℬ.card
hℬ : Set.Sized r ↑ℬ
fully_comp : ∀ (U V : Finset (Fin n)), Finset.UV.UsefulCompression U V → IsCompressed U V ℬ
⊢ 𝒞 = ℬ
Theorem: Finset.kruskal_katona
Proof state before:
case h.e'_3.h.e'_2.h.e'_3
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n r k i : ℕ
𝒜 𝒞 : Finset (Finset (Fin n))
h₁ : Set.Sized r ↑𝒜
h₂ : 𝒜.card = 𝒞.card
h₃ : IsInitSeg 𝒞 r
ℬ : Finset (Finset (Fin n))
card_le : (∂ ℬ).card ≤ (∂ 𝒜).card
t : 𝒜.card = ℬ.card
hℬ : Set.Sized r ↑ℬ
fully_comp : ∀ (U V : Finset (Fin n)), Finset.UV.UsefulCompression U V → IsCompressed U V ℬ
⊢ 𝒞 = ℬ
Tactic:
have hcard : card ℬ = card 𝒞 := t.symm.trans h₂
Proof state after:
case h.e'_3.h.e'_2.h.e'_3
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n r k i : ℕ
𝒜 𝒞 : Finset (Finset (Fin n))
h₁ : Set.Sized r ↑𝒜
h₂ : 𝒜.card = 𝒞.card
h₃ : IsInitSeg 𝒞 r
ℬ : Finset (Finset (Fin n))
card_le : (∂ ℬ).card ≤ (∂ 𝒜).card
t : 𝒜.card = ℬ.card
hℬ : Set.Sized r ↑ℬ
fully_comp : ∀ (U V : Finset (Fin n)), Finset.UV.UsefulCompression U V → IsCompressed U V ℬ
hcard : ℬ.card = 𝒞.card
⊢ 𝒞 = ℬ
Theorem: Finset.kruskal_katona
Proof state before:
case h.e'_3.h.e'_2.h.e'_3
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n r k i : ℕ
𝒜 𝒞 : Finset (Finset (Fin n))
h₁ : Set.Sized r ↑𝒜
h₂ : 𝒜.card = 𝒞.card
h₃ : IsInitSeg 𝒞 r
ℬ : Finset (Finset (Fin n))
card_le : (∂ ℬ).card ≤ (∂ 𝒜).card
t : 𝒜.card = ℬ.card
hℬ : Set.Sized r ↑ℬ
fully_comp : ∀ (U V : Finset (Fin n)), Finset.UV.UsefulCompression U V → IsCompressed U V ℬ
hcard : ℬ.card = 𝒞.card
⊢ 𝒞 = ℬ
Tactic:
obtain CB | BC :=
  h₃.total (UV.isInitSeg_of_compressed hℬ fun U V hUV ↦ by convert fully_comp U V hUV)
Proof state after:
case h.e'_3.h.e'_2.h.e'_3.inl
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n r k i : ℕ
𝒜 𝒞 : Finset (Finset (Fin n))
h₁ : Set.Sized r ↑𝒜
h₂ : 𝒜.card = 𝒞.card
h₃ : IsInitSeg 𝒞 r
ℬ : Finset (Finset (Fin n))
card_le : (∂ ℬ).card ≤ (∂ 𝒜).card
t : 𝒜.card = ℬ.card
hℬ : Set.Sized r ↑ℬ
fully_comp : ∀ (U V : Finset (Fin n)), Finset.UV.UsefulCompression U V → IsCompressed U V ℬ
hcard : ℬ.card = 𝒞.card
CB : 𝒞 ⊆ ℬ
⊢ 𝒞 = ℬ

case h.e'_3.h.e'_2.h.e'_3.inr
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n r k i : ℕ
𝒜 𝒞 : Finset (Finset (Fin n))
h₁ : Set.Sized r ↑𝒜
h₂ : 𝒜.card = 𝒞.card
h₃ : IsInitSeg 𝒞 r
ℬ : Finset (Finset (Fin n))
card_le : (∂ ℬ).card ≤ (∂ 𝒜).card
t : 𝒜.card = ℬ.card
hℬ : Set.Sized r ↑ℬ
fully_comp : ∀ (U V : Finset (Fin n)), Finset.UV.UsefulCompression U V → IsCompressed U V ℬ
hcard : ℬ.card = 𝒞.card
BC : ℬ ⊆ 𝒞
⊢ 𝒞 = ℬ
Theorem: Finset.kruskal_katona
Proof state before:
α : Type u_1
inst✝ : LinearOrder α
s U✝ V✝ : Finset α
n r k i : ℕ
𝒜 𝒞 : Finset (Finset (Fin n))
h₁ : Set.Sized r ↑𝒜
h₂ : 𝒜.card = 𝒞.card
h₃ : IsInitSeg 𝒞 r
ℬ : Finset (Finset (Fin n))
card_le : (∂ ℬ).card ≤ (∂ 𝒜).card
t : 𝒜.card = ℬ.card
hℬ : Set.Sized r ↑ℬ
fully_comp : ∀ (U V : Finset (Fin n)), Finset.UV.UsefulCompression U V → IsCompressed U V ℬ
hcard : ℬ.card = 𝒞.card
U V : Finset (Fin n)
hUV : Finset.UV.UsefulCompression U V
⊢ IsCompressed U V ℬ
Tactic:
convert fully_comp U V hUV
Proof state after:
no goals
Theorem: Finset.kruskal_katona
Proof state before:
case h.e'_3.h.e'_2.h.e'_3.inl
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n r k i : ℕ
𝒜 𝒞 : Finset (Finset (Fin n))
h₁ : Set.Sized r ↑𝒜
h₂ : 𝒜.card = 𝒞.card
h₃ : IsInitSeg 𝒞 r
ℬ : Finset (Finset (Fin n))
card_le : (∂ ℬ).card ≤ (∂ 𝒜).card
t : 𝒜.card = ℬ.card
hℬ : Set.Sized r ↑ℬ
fully_comp : ∀ (U V : Finset (Fin n)), Finset.UV.UsefulCompression U V → IsCompressed U V ℬ
hcard : ℬ.card = 𝒞.card
CB : 𝒞 ⊆ ℬ
⊢ 𝒞 = ℬ
Tactic:
exact eq_of_subset_of_card_le CB hcard.le
Proof state after:
no goals
Theorem: Finset.kruskal_katona
Proof state before:
case h.e'_3.h.e'_2.h.e'_3.inr
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n r k i : ℕ
𝒜 𝒞 : Finset (Finset (Fin n))
h₁ : Set.Sized r ↑𝒜
h₂ : 𝒜.card = 𝒞.card
h₃ : IsInitSeg 𝒞 r
ℬ : Finset (Finset (Fin n))
card_le : (∂ ℬ).card ≤ (∂ 𝒜).card
t : 𝒜.card = ℬ.card
hℬ : Set.Sized r ↑ℬ
fully_comp : ∀ (U V : Finset (Fin n)), Finset.UV.UsefulCompression U V → IsCompressed U V ℬ
hcard : ℬ.card = 𝒞.card
BC : ℬ ⊆ 𝒞
⊢ 𝒞 = ℬ
Tactic:
exact (eq_of_subset_of_card_le BC hcard.ge).symm
Proof state after:
no goals
Theorem: Finset.strengthened_kk
Proof state before:
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n r k i : ℕ
𝒜 𝒞 : Finset (Finset (Fin n))
h₁ : Set.Sized r ↑𝒜
h₂ : 𝒞.card ≤ 𝒜.card
h₃ : IsInitSeg 𝒞 r
⊢ (∂ 𝒞).card ≤ (∂ 𝒜).card
Tactic:
rcases exists_smaller_set 𝒜 𝒞.card h₂ with ⟨𝒜', prop, size⟩
Proof state after:
case intro.intro
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n r k i : ℕ
𝒜 𝒞 : Finset (Finset (Fin n))
h₁ : Set.Sized r ↑𝒜
h₂ : 𝒞.card ≤ 𝒜.card
h₃ : IsInitSeg 𝒞 r
𝒜' : Finset (Finset (Fin n))
prop : 𝒜' ⊆ 𝒜
size : 𝒜'.card = 𝒞.card
⊢ (∂ 𝒞).card ≤ (∂ 𝒜).card
Theorem: Finset.strengthened_kk
Proof state before:
case intro.intro
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n r k i : ℕ
𝒜 𝒞 : Finset (Finset (Fin n))
h₁ : Set.Sized r ↑𝒜
h₂ : 𝒞.card ≤ 𝒜.card
h₃ : IsInitSeg 𝒞 r
𝒜' : Finset (Finset (Fin n))
prop : 𝒜' ⊆ 𝒜
size : 𝒜'.card = 𝒞.card
⊢ (∂ 𝒞).card ≤ (∂ 𝒜).card
Tactic:
refine' (kruskal_katona (fun A hA ↦ h₁ (prop hA)) size h₃).trans (card_le_card _)
Proof state after:
case intro.intro
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n r k i : ℕ
𝒜 𝒞 : Finset (Finset (Fin n))
h₁ : Set.Sized r ↑𝒜
h₂ : 𝒞.card ≤ 𝒜.card
h₃ : IsInitSeg 𝒞 r
𝒜' : Finset (Finset (Fin n))
prop : 𝒜' ⊆ 𝒜
size : 𝒜'.card = 𝒞.card
⊢ ∂ 𝒜' ⊆ ∂ 𝒜
Theorem: Finset.strengthened_kk
Proof state before:
case intro.intro
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n r k i : ℕ
𝒜 𝒞 : Finset (Finset (Fin n))
h₁ : Set.Sized r ↑𝒜
h₂ : 𝒞.card ≤ 𝒜.card
h₃ : IsInitSeg 𝒞 r
𝒜' : Finset (Finset (Fin n))
prop : 𝒜' ⊆ 𝒜
size : 𝒜'.card = 𝒞.card
⊢ ∂ 𝒜' ⊆ ∂ 𝒜
Tactic:
rw [shadow, shadow]
Proof state after:
case intro.intro
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n r k i : ℕ
𝒜 𝒞 : Finset (Finset (Fin n))
h₁ : Set.Sized r ↑𝒜
h₂ : 𝒞.card ≤ 𝒜.card
h₃ : IsInitSeg 𝒞 r
𝒜' : Finset (Finset (Fin n))
prop : 𝒜' ⊆ 𝒜
size : 𝒜'.card = 𝒞.card
⊢ (𝒜'.sup fun s => image s.erase s) ⊆ 𝒜.sup fun s => image s.erase s
Theorem: Finset.strengthened_kk
Proof state before:
case intro.intro
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n r k i : ℕ
𝒜 𝒞 : Finset (Finset (Fin n))
h₁ : Set.Sized r ↑𝒜
h₂ : 𝒞.card ≤ 𝒜.card
h₃ : IsInitSeg 𝒞 r
𝒜' : Finset (Finset (Fin n))
prop : 𝒜' ⊆ 𝒜
size : 𝒜'.card = 𝒞.card
⊢ (𝒜'.sup fun s => image s.erase s) ⊆ 𝒜.sup fun s => image s.erase s
Tactic:
apply shadow_monotone prop
Proof state after:
no goals
Theorem: Finset.iterated_kk
Proof state before:
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n r k i : ℕ
𝒜 𝒞 : Finset (Finset (Fin n))
h₁ : Set.Sized r ↑𝒜
h₂ : 𝒞.card ≤ 𝒜.card
h₃ : IsInitSeg 𝒞 r
⊢ (∂ ^[k] 𝒞).card ≤ (∂ ^[k] 𝒜).card
Tactic:
induction' k with _k ih generalizing r 𝒜 𝒞
Proof state after:
case zero
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n i r : ℕ
𝒜 𝒞 : Finset (Finset (Fin n))
h₁ : Set.Sized r ↑𝒜
h₂ : 𝒞.card ≤ 𝒜.card
h₃ : IsInitSeg 𝒞 r
⊢ (∂ ^[0] 𝒞).card ≤ (∂ ^[0] 𝒜).card

case succ
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n i _k : ℕ
ih :
  ∀ {r : ℕ} {𝒜 𝒞 : Finset (Finset (Fin n))},
    Set.Sized r ↑𝒜 → 𝒞.card ≤ 𝒜.card → IsInitSeg 𝒞 r → (∂ ^[_k] 𝒞).card ≤ (∂ ^[_k] 𝒜).card
r : ℕ
𝒜 𝒞 : Finset (Finset (Fin n))
h₁ : Set.Sized r ↑𝒜
h₂ : 𝒞.card ≤ 𝒜.card
h₃ : IsInitSeg 𝒞 r
⊢ (∂ ^[_k + 1] 𝒞).card ≤ (∂ ^[_k + 1] 𝒜).card
Theorem: Finset.iterated_kk
Proof state before:
case zero
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n i r : ℕ
𝒜 𝒞 : Finset (Finset (Fin n))
h₁ : Set.Sized r ↑𝒜
h₂ : 𝒞.card ≤ 𝒜.card
h₃ : IsInitSeg 𝒞 r
⊢ (∂ ^[0] 𝒞).card ≤ (∂ ^[0] 𝒜).card
Tactic:
simpa
Proof state after:
no goals
Theorem: Finset.iterated_kk
Proof state before:
case succ
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n i _k : ℕ
ih :
  ∀ {r : ℕ} {𝒜 𝒞 : Finset (Finset (Fin n))},
    Set.Sized r ↑𝒜 → 𝒞.card ≤ 𝒜.card → IsInitSeg 𝒞 r → (∂ ^[_k] 𝒞).card ≤ (∂ ^[_k] 𝒜).card
r : ℕ
𝒜 𝒞 : Finset (Finset (Fin n))
h₁ : Set.Sized r ↑𝒜
h₂ : 𝒞.card ≤ 𝒜.card
h₃ : IsInitSeg 𝒞 r
⊢ (∂ ^[_k + 1] 𝒞).card ≤ (∂ ^[_k + 1] 𝒜).card
Tactic:
refine' ih h₁.shadow (strengthened_kk h₁ h₂ h₃) _
Proof state after:
case succ
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n i _k : ℕ
ih :
  ∀ {r : ℕ} {𝒜 𝒞 : Finset (Finset (Fin n))},
    Set.Sized r ↑𝒜 → 𝒞.card ≤ 𝒜.card → IsInitSeg 𝒞 r → (∂ ^[_k] 𝒞).card ≤ (∂ ^[_k] 𝒜).card
r : ℕ
𝒜 𝒞 : Finset (Finset (Fin n))
h₁ : Set.Sized r ↑𝒜
h₂ : 𝒞.card ≤ 𝒜.card
h₃ : IsInitSeg 𝒞 r
⊢ IsInitSeg (∂ 𝒞) (r - 1)
Theorem: Finset.iterated_kk
Proof state before:
case succ
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n i _k : ℕ
ih :
  ∀ {r : ℕ} {𝒜 𝒞 : Finset (Finset (Fin n))},
    Set.Sized r ↑𝒜 → 𝒞.card ≤ 𝒜.card → IsInitSeg 𝒞 r → (∂ ^[_k] 𝒞).card ≤ (∂ ^[_k] 𝒜).card
r : ℕ
𝒜 𝒞 : Finset (Finset (Fin n))
h₁ : Set.Sized r ↑𝒜
h₂ : 𝒞.card ≤ 𝒜.card
h₃ : IsInitSeg 𝒞 r
⊢ IsInitSeg (∂ 𝒞) (r - 1)
Tactic:
convert h₃.shadow
Proof state after:
no goals
Theorem: Finset.lovasz_form
Proof state before:
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n r k i : ℕ
𝒜 𝒞 : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ 𝒜.card
⊢ k.choose (r - i) ≤ (∂ ^[i] 𝒜).card
Tactic:
set range'k : Finset (Fin n) :=
  attachFin (range k) fun m ↦ by rw [mem_range]; apply forall_lt_iff_le.2 hkn
Proof state after:
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n r k i : ℕ
𝒜 𝒞 : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ 𝒜.card
range'k : Finset (Fin n) := (range k).attachFin ⋯
⊢ k.choose (r - i) ≤ (∂ ^[i] 𝒜).card
Theorem: Finset.lovasz_form
Proof state before:
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n r k i : ℕ
𝒜 𝒞 : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ 𝒜.card
range'k : Finset (Fin n) := (range k).attachFin ⋯
⊢ k.choose (r - i) ≤ (∂ ^[i] 𝒜).card
Tactic:
set 𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
Proof state after:
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n r k i : ℕ
𝒜 𝒞✝ : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ 𝒜.card
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
⊢ k.choose (r - i) ≤ (∂ ^[i] 𝒜).card
Theorem: Finset.lovasz_form
Proof state before:
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n r k i : ℕ
𝒜 𝒞✝ : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ 𝒜.card
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
⊢ k.choose (r - i) ≤ (∂ ^[i] 𝒜).card
Tactic:
have Ccard : 𝒞.card = k.choose r := by rw [card_powersetCard, card_attachFin, card_range]
Proof state after:
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n r k i : ℕ
𝒜 𝒞✝ : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ 𝒜.card
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
Ccard : 𝒞.card = k.choose r
⊢ k.choose (r - i) ≤ (∂ ^[i] 𝒜).card
Theorem: Finset.lovasz_form
Proof state before:
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n r k i : ℕ
𝒜 𝒞✝ : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ 𝒜.card
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
Ccard : 𝒞.card = k.choose r
⊢ k.choose (r - i) ≤ (∂ ^[i] 𝒜).card
Tactic:
have : (𝒞 : Set (Finset (Fin n))).Sized r := Set.sized_powersetCard _ _
Proof state after:
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n r k i : ℕ
𝒜 𝒞✝ : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ 𝒜.card
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
Ccard : 𝒞.card = k.choose r
this : Set.Sized r ↑𝒞
⊢ k.choose (r - i) ≤ (∂ ^[i] 𝒜).card