Theorem: Finset.strengthened_kk (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:
rcases exists_smaller_set 𝒜 𝒞.card h₂ with ⟨𝒜', prop, size⟩
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

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 _)
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
⊢ ∂ 𝒜' ⊆ ∂ 𝒜

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

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