case a
𝕜 : Type ?u.21156
α : Type u_1
inst✝¹ : LinearOrderedField 𝕜
inst✝ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s✝ s : Finset α
⊢ s ∈ 𝒜 # k ∪ (∂ ) (falling (k + 1) 𝒜) ↔ s ∈ falling k 𝒜
𝕜 : Type ?u.21156
α : Type u_1
inst✝¹ : LinearOrderedField 𝕜
inst✝ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s : Finset α
⊢ 𝒜 # k ∪ (∂ ) (falling (k + 1) 𝒜) = falling k 𝒜
ext s
case a
𝕜 : Type ?u.21156
α : Type u_1
inst✝¹ : LinearOrderedField 𝕜
inst✝ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s✝ s : Finset α
⊢ (s ∈ 𝒜 ∧ card s = k ∨ ∃ t, ((∃ t_1, t_1 ∈ 𝒜 ∧ t ⊆ t_1) ∧ card t = k + 1) ∧ ∃ a, a ∈ t ∧ erase t a = s) ↔
    (∃ t, t ∈ 𝒜 ∧ s ⊆ t) ∧ card s = k
case a
𝕜 : Type ?u.21156
α : Type u_1
inst✝¹ : LinearOrderedField 𝕜
inst✝ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s✝ s : Finset α
⊢ s ∈ 𝒜 # k ∪ (∂ ) (falling (k + 1) 𝒜) ↔ s ∈ falling k 𝒜
simp_rw [mem_union, mem_slice, mem_shadow_iff, mem_falling]
case a.mp
𝕜 : Type ?u.21156
α : Type u_1
inst✝¹ : LinearOrderedField 𝕜
inst✝ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s✝ s : Finset α
⊢ (s ∈ 𝒜 ∧ card s = k ∨ ∃ t, ((∃ t_1, t_1 ∈ 𝒜 ∧ t ⊆ t_1) ∧ card t = k + 1) ∧ ∃ a, a ∈ t ∧ erase t a = s) →
    (∃ t, t ∈ 𝒜 ∧ s ⊆ t) ∧ card s = k

case a.mpr
𝕜 : Type ?u.21156
α : Type u_1
inst✝¹ : LinearOrderedField 𝕜
inst✝ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s✝ s : Finset α
⊢ (∃ t, t ∈ 𝒜 ∧ s ⊆ t) ∧ card s = k →
    s ∈ 𝒜 ∧ card s = k ∨ ∃ t, ((∃ t_1, t_1 ∈ 𝒜 ∧ t ⊆ t_1) ∧ card t = k + 1) ∧ ∃ a, a ∈ t ∧ erase t a = s
case a
𝕜 : Type ?u.21156
α : Type u_1
inst✝¹ : LinearOrderedField 𝕜
inst✝ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s✝ s : Finset α
⊢ (s ∈ 𝒜 ∧ card s = k ∨ ∃ t, ((∃ t_1, t_1 ∈ 𝒜 ∧ t ⊆ t_1) ∧ card t = k + 1) ∧ ∃ a, a ∈ t ∧ erase t a = s) ↔
    (∃ t, t ∈ 𝒜 ∧ s ⊆ t) ∧ card s = k
constructor
case a.mp.inl
𝕜 : Type ?u.21156
α : Type u_1
inst✝¹ : LinearOrderedField 𝕜
inst✝ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s✝ s : Finset α
h : s ∈ 𝒜 ∧ card s = k
⊢ (∃ t, t ∈ 𝒜 ∧ s ⊆ t) ∧ card s = k

case a.mp.inr.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type ?u.21156
α : Type u_1
inst✝¹ : LinearOrderedField 𝕜
inst✝ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s✝ s : Finset α
hs : card s = k + 1
t : Finset α
ht : t ∈ 𝒜
hst : s ⊆ t
a : α
ha : a ∈ s
⊢ (∃ t, t ∈ 𝒜 ∧ erase s a ⊆ t) ∧ card (erase s a) = k
case a.mp
𝕜 : Type ?u.21156
α : Type u_1
inst✝¹ : LinearOrderedField 𝕜
inst✝ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s✝ s : Finset α
⊢ (s ∈ 𝒜 ∧ card s = k ∨ ∃ t, ((∃ t_1, t_1 ∈ 𝒜 ∧ t ⊆ t_1) ∧ card t = k + 1) ∧ ∃ a, a ∈ t ∧ erase t a = s) →
    (∃ t, t ∈ 𝒜 ∧ s ⊆ t) ∧ card s = k
rintro (h | ⟨s, ⟨⟨t, ht, hst⟩, hs⟩, a, ha, rfl⟩)
case a.mp.inr.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type ?u.21156
α : Type u_1
inst✝¹ : LinearOrderedField 𝕜
inst✝ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s✝ s : Finset α
hs : card s = k + 1
t : Finset α
ht : t ∈ 𝒜
hst : s ⊆ t
a : α
ha : a ∈ s
⊢ card (erase s a) = k
case a.mp.inr.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type ?u.21156
α : Type u_1
inst✝¹ : LinearOrderedField 𝕜
inst✝ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s✝ s : Finset α
hs : card s = k + 1
t : Finset α
ht : t ∈ 𝒜
hst : s ⊆ t
a : α
ha : a ∈ s
⊢ (∃ t, t ∈ 𝒜 ∧ erase s a ⊆ t) ∧ card (erase s a) = k
refine' ⟨⟨t, ht, (erase_subset _ _).trans hst⟩, _⟩
case a.mp.inr.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type ?u.21156
α : Type u_1
inst✝¹ : LinearOrderedField 𝕜
inst✝ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s✝ s : Finset α
hs : card s = k + 1
t : Finset α
ht : t ∈ 𝒜
hst : s ⊆ t
a : α
ha : a ∈ s
⊢ k + 1 - 1 = k
case a.mp.inr.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type ?u.21156
α : Type u_1
inst✝¹ : LinearOrderedField 𝕜
inst✝ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s✝ s : Finset α
hs : card s = k + 1
t : Finset α
ht : t ∈ 𝒜
hst : s ⊆ t
a : α
ha : a ∈ s
⊢ card (erase s a) = k
rw [card_erase_of_mem ha, hs]
no goals
case a.mp.inr.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type ?u.21156
α : Type u_1
inst✝¹ : LinearOrderedField 𝕜
inst✝ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s✝ s : Finset α
hs : card s = k + 1
t : Finset α
ht : t ∈ 𝒜
hst : s ⊆ t
a : α
ha : a ∈ s
⊢ k + 1 - 1 = k
rfl
no goals
case a.mp.inl
𝕜 : Type ?u.21156
α : Type u_1
inst✝¹ : LinearOrderedField 𝕜
inst✝ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s✝ s : Finset α
h : s ∈ 𝒜 ∧ card s = k
⊢ (∃ t, t ∈ 𝒜 ∧ s ⊆ t) ∧ card s = k
exact ⟨⟨s, h.1, Subset.refl _⟩, h.2⟩
case a.mpr.intro.intro.intro
𝕜 : Type ?u.21156
α : Type u_1
inst✝¹ : LinearOrderedField 𝕜
inst✝ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s✝ s : Finset α
hs : card s = k
t : Finset α
ht : t ∈ 𝒜
hst : s ⊆ t
⊢ s ∈ 𝒜 ∧ card s = k ∨ ∃ t, ((∃ t_1, t_1 ∈ 𝒜 ∧ t ⊆ t_1) ∧ card t = k + 1) ∧ ∃ a, a ∈ t ∧ erase t a = s
case a.mpr
𝕜 : Type ?u.21156
α : Type u_1
inst✝¹ : LinearOrderedField 𝕜
inst✝ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s✝ s : Finset α
⊢ (∃ t, t ∈ 𝒜 ∧ s ⊆ t) ∧ card s = k →
    s ∈ 𝒜 ∧ card s = k ∨ ∃ t, ((∃ t_1, t_1 ∈ 𝒜 ∧ t ⊆ t_1) ∧ card t = k + 1) ∧ ∃ a, a ∈ t ∧ erase t a = s
rintro ⟨⟨t, ht, hst⟩, hs⟩
case pos
𝕜 : Type ?u.21156
α : Type u_1
inst✝¹ : LinearOrderedField 𝕜
inst✝ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s✝ s : Finset α
hs : card s = k
t : Finset α
ht : t ∈ 𝒜
hst : s ⊆ t
h : s ∈ 𝒜
⊢ s ∈ 𝒜 ∧ card s = k ∨ ∃ t, ((∃ t_1, t_1 ∈ 𝒜 ∧ t ⊆ t_1) ∧ card t = k + 1) ∧ ∃ a, a ∈ t ∧ erase t a = s

case neg
𝕜 : Type ?u.21156
α : Type u_1
inst✝¹ : LinearOrderedField 𝕜
inst✝ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s✝ s : Finset α
hs : card s = k
t : Finset α
ht : t ∈ 𝒜
hst : s ⊆ t
h : ¬s ∈ 𝒜
⊢ s ∈ 𝒜 ∧ card s = k ∨ ∃ t, ((∃ t_1, t_1 ∈ 𝒜 ∧ t ⊆ t_1) ∧ card t = k + 1) ∧ ∃ a, a ∈ t ∧ erase t a = s
case a.mpr.intro.intro.intro
𝕜 : Type ?u.21156
α : Type u_1
inst✝¹ : LinearOrderedField 𝕜
inst✝ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s✝ s : Finset α
hs : card s = k
t : Finset α
ht : t ∈ 𝒜
hst : s ⊆ t
⊢ s ∈ 𝒜 ∧ card s = k ∨ ∃ t, ((∃ t_1, t_1 ∈ 𝒜 ∧ t ⊆ t_1) ∧ card t = k + 1) ∧ ∃ a, a ∈ t ∧ erase t a = s
by_cases h : s ∈ 𝒜
case neg.intro.intro
𝕜 : Type ?u.21156
α : Type u_1
inst✝¹ : LinearOrderedField 𝕜
inst✝ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s✝ s : Finset α
hs : card s = k
t : Finset α
ht : t ∈ 𝒜
hst✝ : s ⊆ t
h : ¬s ∈ 𝒜
a : α
ha : ¬a ∈ s
hst : insert a s ⊆ t
⊢ s ∈ 𝒜 ∧ card s = k ∨ ∃ t, ((∃ t_1, t_1 ∈ 𝒜 ∧ t ⊆ t_1) ∧ card t = k + 1) ∧ ∃ a, a ∈ t ∧ erase t a = s
case neg
𝕜 : Type ?u.21156
α : Type u_1
inst✝¹ : LinearOrderedField 𝕜
inst✝ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s✝ s : Finset α
hs : card s = k
t : Finset α
ht : t ∈ 𝒜
hst : s ⊆ t
h : ¬s ∈ 𝒜
⊢ s ∈ 𝒜 ∧ card s = k ∨ ∃ t, ((∃ t_1, t_1 ∈ 𝒜 ∧ t ⊆ t_1) ∧ card t = k + 1) ∧ ∃ a, a ∈ t ∧ erase t a = s
obtain ⟨a, ha, hst⟩ := ssubset_iff.1 (ssubset_of_subset_of_ne hst (ht.ne_of_not_mem h).symm)
case neg.intro.intro
𝕜 : Type ?u.21156
α : Type u_1
inst✝¹ : LinearOrderedField 𝕜
inst✝ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s✝ s : Finset α
hs : card s = k
t : Finset α
ht : t ∈ 𝒜
hst✝ : s ⊆ t
h : ¬s ∈ 𝒜
a : α
ha : ¬a ∈ s
hst : insert a s ⊆ t
⊢ card (insert a s) = k + 1
case neg.intro.intro
𝕜 : Type ?u.21156
α : Type u_1
inst✝¹ : LinearOrderedField 𝕜
inst✝ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s✝ s : Finset α
hs : card s = k
t : Finset α
ht : t ∈ 𝒜
hst✝ : s ⊆ t
h : ¬s ∈ 𝒜
a : α
ha : ¬a ∈ s
hst : insert a s ⊆ t
⊢ s ∈ 𝒜 ∧ card s = k ∨ ∃ t, ((∃ t_1, t_1 ∈ 𝒜 ∧ t ⊆ t_1) ∧ card t = k + 1) ∧ ∃ a, a ∈ t ∧ erase t a = s
refine' Or.inr ⟨insert a s, ⟨⟨t, ht, hst⟩, _⟩, a, mem_insert_self _ _, erase_insert ha⟩
no goals
case neg.intro.intro
𝕜 : Type ?u.21156
α : Type u_1
inst✝¹ : LinearOrderedField 𝕜
inst✝ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s✝ s : Finset α
hs : card s = k
t : Finset α
ht : t ∈ 𝒜
hst✝ : s ⊆ t
h : ¬s ∈ 𝒜
a : α
ha : ¬a ∈ s
hst : insert a s ⊆ t
⊢ card (insert a s) = k + 1
rw [card_insert_of_not_mem ha, hs]
no goals
case pos
𝕜 : Type ?u.21156
α : Type u_1
inst✝¹ : LinearOrderedField 𝕜
inst✝ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s✝ s : Finset α
hs : card s = k
t : Finset α
ht : t ∈ 𝒜
hst : s ⊆ t
h : s ∈ 𝒜
⊢ s ∈ 𝒜 ∧ card s = k ∨ ∃ t, ((∃ t_1, t_1 ∈ 𝒜 ∧ t ⊆ t_1) ∧ card t = k + 1) ∧ ∃ a, a ∈ t ∧ erase t a = s
exact Or.inl ⟨h, hs⟩