Theorem: Finset.kruskal_katona (LeanCamCombi/KruskalKatona.lean)

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

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
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 ℬ
⊢ 𝒞 = ℬ

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₂
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
⊢ 𝒞 = ℬ

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)
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 : ℬ ⊆ 𝒞
⊢ 𝒞 = ℬ

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
State after:
no goals

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
State after:
no goals

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
State after:
no goals