case zero
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ : Finset (Finset α)
s✝ t : Finset α
a : α
k r : ℕ
𝒜 : Finset (Finset α)
s : Finset α
⊢ s ∈ (∂ ^[zero]) 𝒜 ↔ ∃ t, t ∈ 𝒜 ∧ s ⊆ t ∧ card t = card s + zero

case succ
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ : Finset (Finset α)
s✝ t : Finset α
a : α
k✝ r k : ℕ
ih : ∀ {𝒜 : Finset (Finset α)} {s : Finset α}, s ∈ (∂ ^[k]) 𝒜 ↔ ∃ t, t ∈ 𝒜 ∧ s ⊆ t ∧ card t = card s + k
𝒜 : Finset (Finset α)
s : Finset α
⊢ s ∈ (∂ ^[succ k]) 𝒜 ↔ ∃ t, t ∈ 𝒜 ∧ s ⊆ t ∧ card t = card s + succ k
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s t : Finset α
a : α
k r : ℕ
⊢ s ∈ (∂ ^[k]) 𝒜 ↔ ∃ t, t ∈ 𝒜 ∧ s ⊆ t ∧ card t = card s + k
induction' k with k ih generalizing 𝒜 s
case succ
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ : Finset (Finset α)
s✝ t : Finset α
a : α
k✝ r k : ℕ
ih : ∀ {𝒜 : Finset (Finset α)} {s : Finset α}, s ∈ (∂ ^[k]) 𝒜 ↔ ∃ t, t ∈ 𝒜 ∧ s ⊆ t ∧ card t = card s + k
𝒜 : Finset (Finset α)
s : Finset α
⊢ s ∈ (∂ ^[k]) ((∂ ) 𝒜) ↔ ∃ t, t ∈ 𝒜 ∧ s ⊆ t ∧ card t = card s + succ k
case succ
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ : Finset (Finset α)
s✝ t : Finset α
a : α
k✝ r k : ℕ
ih : ∀ {𝒜 : Finset (Finset α)} {s : Finset α}, s ∈ (∂ ^[k]) 𝒜 ↔ ∃ t, t ∈ 𝒜 ∧ s ⊆ t ∧ card t = card s + k
𝒜 : Finset (Finset α)
s : Finset α
⊢ s ∈ (∂ ^[succ k]) 𝒜 ↔ ∃ t, t ∈ 𝒜 ∧ s ⊆ t ∧ card t = card s + succ k
simp only [exists_prop, Function.comp_apply, Function.iterate_succ]
case succ
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ : Finset (Finset α)
s✝ t : Finset α
a : α
k✝ r k : ℕ
ih : ∀ {𝒜 : Finset (Finset α)} {s : Finset α}, s ∈ (∂ ^[k]) 𝒜 ↔ ∃ t, t ∈ 𝒜 ∧ s ⊆ t ∧ card t = card s + k
𝒜 : Finset (Finset α)
s : Finset α
⊢ (∃ t, t ∈ (∂ ) 𝒜 ∧ s ⊆ t ∧ card t = card s + k) ↔ ∃ t, t ∈ 𝒜 ∧ s ⊆ t ∧ card t = card s + succ k
case succ
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ : Finset (Finset α)
s✝ t : Finset α
a : α
k✝ r k : ℕ
ih : ∀ {𝒜 : Finset (Finset α)} {s : Finset α}, s ∈ (∂ ^[k]) 𝒜 ↔ ∃ t, t ∈ 𝒜 ∧ s ⊆ t ∧ card t = card s + k
𝒜 : Finset (Finset α)
s : Finset α
⊢ s ∈ (∂ ^[k]) ((∂ ) 𝒜) ↔ ∃ t, t ∈ 𝒜 ∧ s ⊆ t ∧ card t = card s + succ k
refine' ih.trans _
case succ
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ : Finset (Finset α)
s✝ t : Finset α
a : α
k✝ r k : ℕ
𝒜 : Finset (Finset α)
s : Finset α
⊢ (∃ t, t ∈ (∂ ) 𝒜 ∧ s ⊆ t ∧ card t = card s + k) ↔ ∃ t, t ∈ 𝒜 ∧ s ⊆ t ∧ card t = card s + succ k
case succ
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ : Finset (Finset α)
s✝ t : Finset α
a : α
k✝ r k : ℕ
ih : ∀ {𝒜 : Finset (Finset α)} {s : Finset α}, s ∈ (∂ ^[k]) 𝒜 ↔ ∃ t, t ∈ 𝒜 ∧ s ⊆ t ∧ card t = card s + k
𝒜 : Finset (Finset α)
s : Finset α
⊢ (∃ t, t ∈ (∂ ) 𝒜 ∧ s ⊆ t ∧ card t = card s + k) ↔ ∃ t, t ∈ 𝒜 ∧ s ⊆ t ∧ card t = card s + succ k
clear ih
case succ.mp
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ : Finset (Finset α)
s✝ t : Finset α
a : α
k✝ r k : ℕ
𝒜 : Finset (Finset α)
s : Finset α
⊢ (∃ t, t ∈ (∂ ) 𝒜 ∧ s ⊆ t ∧ card t = card s + k) → ∃ t, t ∈ 𝒜 ∧ s ⊆ t ∧ card t = card s + succ k

case succ.mpr
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ : Finset (Finset α)
s✝ t : Finset α
a : α
k✝ r k : ℕ
𝒜 : Finset (Finset α)
s : Finset α
⊢ (∃ t, t ∈ 𝒜 ∧ s ⊆ t ∧ card t = card s + succ k) → ∃ t, t ∈ (∂ ) 𝒜 ∧ s ⊆ t ∧ card t = card s + k
case succ
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ : Finset (Finset α)
s✝ t : Finset α
a : α
k✝ r k : ℕ
𝒜 : Finset (Finset α)
s : Finset α
⊢ (∃ t, t ∈ (∂ ) 𝒜 ∧ s ⊆ t ∧ card t = card s + k) ↔ ∃ t, t ∈ 𝒜 ∧ s ⊆ t ∧ card t = card s + succ k
constructor
case zero
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ : Finset (Finset α)
s✝ t : Finset α
a : α
k r : ℕ
𝒜 : Finset (Finset α)
s : Finset α
⊢ (∃ t, t ∈ 𝒜 ∧ s ⊆ t ∧ card t = card s + zero) → s ∈ (∂ ^[zero]) 𝒜
case zero
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ : Finset (Finset α)
s✝ t : Finset α
a : α
k r : ℕ
𝒜 : Finset (Finset α)
s : Finset α
⊢ s ∈ (∂ ^[zero]) 𝒜 ↔ ∃ t, t ∈ 𝒜 ∧ s ⊆ t ∧ card t = card s + zero
refine' ⟨fun hs => ⟨s, hs, Subset.refl _, rfl⟩, _⟩
case zero.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ : Finset (Finset α)
s✝ t✝ : Finset α
a : α
k r : ℕ
𝒜 : Finset (Finset α)
s t : Finset α
ht : t ∈ 𝒜
hst : s ⊆ t
hcard : card t = card s + zero
⊢ s ∈ (∂ ^[zero]) 𝒜
case zero
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ : Finset (Finset α)
s✝ t : Finset α
a : α
k r : ℕ
𝒜 : Finset (Finset α)
s : Finset α
⊢ (∃ t, t ∈ 𝒜 ∧ s ⊆ t ∧ card t = card s + zero) → s ∈ (∂ ^[zero]) 𝒜
rintro ⟨t, ht, hst, hcard⟩
no goals
case zero.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ : Finset (Finset α)
s✝ t✝ : Finset α
a : α
k r : ℕ
𝒜 : Finset (Finset α)
s t : Finset α
ht : t ∈ 𝒜
hst : s ⊆ t
hcard : card t = card s + zero
⊢ s ∈ (∂ ^[zero]) 𝒜
rwa [eq_of_subset_of_card_le hst hcard.le]
case succ.mp.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ : Finset (Finset α)
s✝ t✝ : Finset α
a : α
k✝ r k : ℕ
𝒜 : Finset (Finset α)
s t : Finset α
ht : t ∈ (∂ ) 𝒜
hst : s ⊆ t
hcardst : card t = card s + k
⊢ ∃ t, t ∈ 𝒜 ∧ s ⊆ t ∧ card t = card s + succ k
case succ.mp
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ : Finset (Finset α)
s✝ t : Finset α
a : α
k✝ r k : ℕ
𝒜 : Finset (Finset α)
s : Finset α
⊢ (∃ t, t ∈ (∂ ) 𝒜 ∧ s ⊆ t ∧ card t = card s + k) → ∃ t, t ∈ 𝒜 ∧ s ⊆ t ∧ card t = card s + succ k
rintro ⟨t, ht, hst, hcardst⟩
case succ.mp.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ : Finset (Finset α)
s✝ t✝ : Finset α
a : α
k✝ r k : ℕ
𝒜 : Finset (Finset α)
s t : Finset α
ht : t ∈ (∂ ) 𝒜
hst : s ⊆ t
hcardst : card t = card s + k
u : Finset α
hu : u ∈ 𝒜
htu : t ⊆ u
hcardtu : card u = card t + 1
⊢ ∃ t, t ∈ 𝒜 ∧ s ⊆ t ∧ card t = card s + succ k
case succ.mp.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ : Finset (Finset α)
s✝ t✝ : Finset α
a : α
k✝ r k : ℕ
𝒜 : Finset (Finset α)
s t : Finset α
ht : t ∈ (∂ ) 𝒜
hst : s ⊆ t
hcardst : card t = card s + k
⊢ ∃ t, t ∈ 𝒜 ∧ s ⊆ t ∧ card t = card s + succ k
obtain ⟨u, hu, htu, hcardtu⟩ := mem_shadow_iff_exists_mem_card_add_one.1 ht
case succ.mp.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ : Finset (Finset α)
s✝ t✝ : Finset α
a : α
k✝ r k : ℕ
𝒜 : Finset (Finset α)
s t : Finset α
ht : t ∈ (∂ ) 𝒜
hst : s ⊆ t
hcardst : card t = card s + k
u : Finset α
hu : u ∈ 𝒜
htu : t ⊆ u
hcardtu : card u = card t + 1
⊢ card u = card s + succ k
case succ.mp.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ : Finset (Finset α)
s✝ t✝ : Finset α
a : α
k✝ r k : ℕ
𝒜 : Finset (Finset α)
s t : Finset α
ht : t ∈ (∂ ) 𝒜
hst : s ⊆ t
hcardst : card t = card s + k
u : Finset α
hu : u ∈ 𝒜
htu : t ⊆ u
hcardtu : card u = card t + 1
⊢ ∃ t, t ∈ 𝒜 ∧ s ⊆ t ∧ card t = card s + succ k
refine' ⟨u, hu, hst.trans htu, _⟩
case succ.mp.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ : Finset (Finset α)
s✝ t✝ : Finset α
a : α
k✝ r k : ℕ
𝒜 : Finset (Finset α)
s t : Finset α
ht : t ∈ (∂ ) 𝒜
hst : s ⊆ t
hcardst : card t = card s + k
u : Finset α
hu : u ∈ 𝒜
htu : t ⊆ u
hcardtu : card u = card t + 1
⊢ card s + k + 1 = card s + succ k
case succ.mp.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ : Finset (Finset α)
s✝ t✝ : Finset α
a : α
k✝ r k : ℕ
𝒜 : Finset (Finset α)
s t : Finset α
ht : t ∈ (∂ ) 𝒜
hst : s ⊆ t
hcardst : card t = card s + k
u : Finset α
hu : u ∈ 𝒜
htu : t ⊆ u
hcardtu : card u = card t + 1
⊢ card u = card s + succ k
rw [hcardtu, hcardst]
no goals
case succ.mp.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ : Finset (Finset α)
s✝ t✝ : Finset α
a : α
k✝ r k : ℕ
𝒜 : Finset (Finset α)
s t : Finset α
ht : t ∈ (∂ ) 𝒜
hst : s ⊆ t
hcardst : card t = card s + k
u : Finset α
hu : u ∈ 𝒜
htu : t ⊆ u
hcardtu : card u = card t + 1
⊢ card s + k + 1 = card s + succ k
rfl
case succ.mpr.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ : Finset (Finset α)
s✝ t✝ : Finset α
a : α
k✝ r k : ℕ
𝒜 : Finset (Finset α)
s t : Finset α
ht : t ∈ 𝒜
hst : s ⊆ t
hcard : card t = card s + succ k
⊢ ∃ t, t ∈ (∂ ) 𝒜 ∧ s ⊆ t ∧ card t = card s + k
case succ.mpr
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ : Finset (Finset α)
s✝ t : Finset α
a : α
k✝ r k : ℕ
𝒜 : Finset (Finset α)
s : Finset α
⊢ (∃ t, t ∈ 𝒜 ∧ s ⊆ t ∧ card t = card s + succ k) → ∃ t, t ∈ (∂ ) 𝒜 ∧ s ⊆ t ∧ card t = card s + k
rintro ⟨t, ht, hst, hcard⟩
case succ.mpr.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ : Finset (Finset α)
s✝ t✝ : Finset α
a : α
k✝ r k : ℕ
𝒜 : Finset (Finset α)
s t : Finset α
ht : t ∈ 𝒜
hst : s ⊆ t
hcard : card t = card s + succ k
u : Finset α
hsu : s ⊆ u
hut : u ⊆ t
hu : card u = k + card s
⊢ ∃ t, t ∈ (∂ ) 𝒜 ∧ s ⊆ t ∧ card t = card s + k
case succ.mpr.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ : Finset (Finset α)
s✝ t✝ : Finset α
a : α
k✝ r k : ℕ
𝒜 : Finset (Finset α)
s t : Finset α
ht : t ∈ 𝒜
hst : s ⊆ t
hcard : card t = card s + succ k
⊢ ∃ t, t ∈ (∂ ) 𝒜 ∧ s ⊆ t ∧ card t = card s + k
obtain ⟨u, hsu, hut, hu⟩ :=
  Finset.exists_intermediate_set k
    (by
      rw [add_comm, hcard]
      exact le_succ _)
    hst
case succ.mpr.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ : Finset (Finset α)
s✝ t✝ : Finset α
a : α
k✝ r k : ℕ
𝒜 : Finset (Finset α)
s t : Finset α
ht : t ∈ 𝒜
hst : s ⊆ t
hcard : card t = card s + succ k
u : Finset α
hsu : s ⊆ u
hut : u ⊆ t
hu : card u = card s + k
⊢ ∃ t, t ∈ (∂ ) 𝒜 ∧ s ⊆ t ∧ card t = card s + k
case succ.mpr.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ : Finset (Finset α)
s✝ t✝ : Finset α
a : α
k✝ r k : ℕ
𝒜 : Finset (Finset α)
s t : Finset α
ht : t ∈ 𝒜
hst : s ⊆ t
hcard : card t = card s + succ k
u : Finset α
hsu : s ⊆ u
hut : u ⊆ t
hu : card u = k + card s
⊢ ∃ t, t ∈ (∂ ) 𝒜 ∧ s ⊆ t ∧ card t = card s + k
rw [add_comm] at hu
case succ.mpr.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ : Finset (Finset α)
s✝ t✝ : Finset α
a : α
k✝ r k : ℕ
𝒜 : Finset (Finset α)
s t : Finset α
ht : t ∈ 𝒜
hst : s ⊆ t
hcard : card t = card s + succ k
u : Finset α
hsu : s ⊆ u
hut : u ⊆ t
hu : card u = card s + k
⊢ card t = card u + 1
case succ.mpr.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ : Finset (Finset α)
s✝ t✝ : Finset α
a : α
k✝ r k : ℕ
𝒜 : Finset (Finset α)
s t : Finset α
ht : t ∈ 𝒜
hst : s ⊆ t
hcard : card t = card s + succ k
u : Finset α
hsu : s ⊆ u
hut : u ⊆ t
hu : card u = card s + k
⊢ ∃ t, t ∈ (∂ ) 𝒜 ∧ s ⊆ t ∧ card t = card s + k
refine' ⟨u, mem_shadow_iff_exists_mem_card_add_one.2 ⟨t, ht, hut, _⟩, hsu, hu⟩
case succ.mpr.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ : Finset (Finset α)
s✝ t✝ : Finset α
a : α
k✝ r k : ℕ
𝒜 : Finset (Finset α)
s t : Finset α
ht : t ∈ 𝒜
hst : s ⊆ t
hcard : card t = card s + succ k
u : Finset α
hsu : s ⊆ u
hut : u ⊆ t
hu : card u = card s + k
⊢ card s + succ k = card s + k + 1
case succ.mpr.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ : Finset (Finset α)
s✝ t✝ : Finset α
a : α
k✝ r k : ℕ
𝒜 : Finset (Finset α)
s t : Finset α
ht : t ∈ 𝒜
hst : s ⊆ t
hcard : card t = card s + succ k
u : Finset α
hsu : s ⊆ u
hut : u ⊆ t
hu : card u = card s + k
⊢ card t = card u + 1
rw [hcard, hu]
no goals
case succ.mpr.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ : Finset (Finset α)
s✝ t✝ : Finset α
a : α
k✝ r k : ℕ
𝒜 : Finset (Finset α)
s t : Finset α
ht : t ∈ 𝒜
hst : s ⊆ t
hcard : card t = card s + succ k
u : Finset α
hsu : s ⊆ u
hut : u ⊆ t
hu : card u = card s + k
⊢ card s + succ k = card s + k + 1
rfl
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ : Finset (Finset α)
s✝ t✝ : Finset α
a : α
k✝ r k : ℕ
𝒜 : Finset (Finset α)
s t : Finset α
ht : t ∈ 𝒜
hst : s ⊆ t
hcard : card t = card s + succ k
⊢ card s + k ≤ card s + succ k
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ : Finset (Finset α)
s✝ t✝ : Finset α
a : α
k✝ r k : ℕ
𝒜 : Finset (Finset α)
s t : Finset α
ht : t ∈ 𝒜
hst : s ⊆ t
hcard : card t = card s + succ k
⊢ k + card s ≤ card t
rw [add_comm, hcard]
no goals
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ : Finset (Finset α)
s✝ t✝ : Finset α
a : α
k✝ r k : ℕ
𝒜 : Finset (Finset α)
s t : Finset α
ht : t ∈ 𝒜
hst : s ⊆ t
hcard : card t = card s + succ k
⊢ card s + k ≤ card s + succ k
exact le_succ _