Theorem: Finset.iterated_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
⊢ (∂ ^[k] 𝒞).card ≤ (∂ ^[k] 𝒜).card
Tactic:
induction' k with _k ih generalizing r 𝒜 𝒞
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

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

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

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