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

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

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