-- Mathlib/Combinatorics/SetFamily/LYM.lean
theorem slice_union_shadow_falling_succ : 𝒜 # k ∪ ∂ (falling (k + 1) 𝒜) = falling k 𝒜

Proof state:
case h.mp.inr.intro.intro.intro.intro.intro.intro.intro
α : Type u_2
inst✝ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s : Finset α
hs : #s = k + 1
t : Finset α
ht : t ∈ 𝒜
hst : s ⊆ t
a : α
ha : a ∈ s
⊢ #(s.erase a) = k

Tactic:
rw [card_erase_of_mem ha, hs]

Result:
case h.mp.inr.intro.intro.intro.intro.intro.intro.intro
α : Type u_2
inst✝ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s : Finset α
hs : #s = k + 1
t : Finset α
ht : t ∈ 𝒜
hst : s ⊆ t
a : α
ha : a ∈ s
⊢ k + 1 - 1 = k

Proof state:
case pos
α : Type u_2
inst✝ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s : Finset α
hs : #s = k
t : Finset α
ht : t ∈ 𝒜
hst : s ⊆ t
h : s ∈ 𝒜
⊢ s ∈ 𝒜 ∧ #s = k ∨ ∃ s_1, ((∃ t ∈ 𝒜, s_1 ⊆ t) ∧ #s_1 = k + 1) ∧ ∃ a ∈ s_1, s_1.erase a = s

Tactic:
exact Or.inl ⟨h, hs⟩

Result:
no goals

Proof state:
case h.mp.inr.intro.intro.intro.intro.intro.intro.intro
α : Type u_2
inst✝ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s : Finset α
hs : #s = k + 1
t : Finset α
ht : t ∈ 𝒜
hst : s ⊆ t
a : α
ha : a ∈ s
⊢ k + 1 - 1 = k

Tactic:
rfl

Result:
no goals

Proof state:
case neg.intro.intro
α : Type u_2
inst✝ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s : Finset α
hs : #s = k
t : Finset α
ht : t ∈ 𝒜
hst✝ : s ⊆ t
h : s ∉ 𝒜
a : α
ha : a ∉ s
hst : insert a s ⊆ t
⊢ s ∈ 𝒜 ∧ #s = k ∨ ∃ s_1, ((∃ t ∈ 𝒜, s_1 ⊆ t) ∧ #s_1 = k + 1) ∧ ∃ a ∈ s_1, s_1.erase a = s

Tactic:
refine Or.inr ⟨insert a s, ⟨⟨t, ht, hst⟩, ?_⟩, a, mem_insert_self _ _, erase_insert ha⟩

Result:
case neg.intro.intro
α : Type u_2
inst✝ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s : Finset α
hs : #s = k
t : Finset α
ht : t ∈ 𝒜
hst✝ : s ⊆ t
h : s ∉ 𝒜
a : α
ha : a ∉ s
hst : insert a s ⊆ t
⊢ #(insert a s) = k + 1

Proof state:
case h.mp.inl
α : Type u_2
inst✝ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s : Finset α
h : s ∈ 𝒜 ∧ #s = k
⊢ (∃ t ∈ 𝒜, s ⊆ t) ∧ #s = k

Tactic:
exact ⟨⟨s, h.1, Subset.refl _⟩, h.2⟩

Result:
no goals

Proof state:
α : Type u_2
inst✝ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
⊢ 𝒜 # k ∪ ∂ (falling (k + 1) 𝒜) = falling k 𝒜

Tactic:
ext s

Result:
case h
α : Type u_2
inst✝ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s : Finset α
⊢ s ∈ 𝒜 # k ∪ ∂ (falling (k + 1) 𝒜) ↔ s ∈ falling k 𝒜

Proof state:
case h.mp.inr.intro.intro.intro.intro.intro.intro.intro
α : Type u_2
inst✝ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s : Finset α
hs : #s = k + 1
t : Finset α
ht : t ∈ 𝒜
hst : s ⊆ t
a : α
ha : a ∈ s
⊢ (∃ t ∈ 𝒜, s.erase a ⊆ t) ∧ #(s.erase a) = k

Tactic:
refine ⟨⟨t, ht, (erase_subset _ _).trans hst⟩, ?_⟩

Result:
case h.mp.inr.intro.intro.intro.intro.intro.intro.intro
α : Type u_2
inst✝ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s : Finset α
hs : #s = k + 1
t : Finset α
ht : t ∈ 𝒜
hst : s ⊆ t
a : α
ha : a ∈ s
⊢ #(s.erase a) = k

Proof state:
case h.mpr.intro.intro.intro
α : Type u_2
inst✝ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s : Finset α
hs : #s = k
t : Finset α
ht : t ∈ 𝒜
hst : s ⊆ t
⊢ s ∈ 𝒜 ∧ #s = k ∨ ∃ s_1, ((∃ t ∈ 𝒜, s_1 ⊆ t) ∧ #s_1 = k + 1) ∧ ∃ a ∈ s_1, s_1.erase a = s

Tactic:
by_cases h : s ∈ 𝒜

Result:
case pos
α : Type u_2
inst✝ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s : Finset α
hs : #s = k
t : Finset α
ht : t ∈ 𝒜
hst : s ⊆ t
h : s ∈ 𝒜
⊢ s ∈ 𝒜 ∧ #s = k ∨ ∃ s_1, ((∃ t ∈ 𝒜, s_1 ⊆ t) ∧ #s_1 = k + 1) ∧ ∃ a ∈ s_1, s_1.erase a = s

case neg
α : Type u_2
inst✝ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s : Finset α
hs : #s = k
t : Finset α
ht : t ∈ 𝒜
hst : s ⊆ t
h : s ∉ 𝒜
⊢ s ∈ 𝒜 ∧ #s = k ∨ ∃ s_1, ((∃ t ∈ 𝒜, s_1 ⊆ t) ∧ #s_1 = k + 1) ∧ ∃ a ∈ s_1, s_1.erase a = s

Proof state:
case h.mpr
α : Type u_2
inst✝ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s : Finset α
⊢ (∃ t ∈ 𝒜, s ⊆ t) ∧ #s = k → s ∈ 𝒜 ∧ #s = k ∨ ∃ s_1, ((∃ t ∈ 𝒜, s_1 ⊆ t) ∧ #s_1 = k + 1) ∧ ∃ a ∈ s_1, s_1.erase a = s

Tactic:
rintro ⟨⟨t, ht, hst⟩, hs⟩

Result:
case h.mpr.intro.intro.intro
α : Type u_2
inst✝ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s : Finset α
hs : #s = k
t : Finset α
ht : t ∈ 𝒜
hst : s ⊆ t
⊢ s ∈ 𝒜 ∧ #s = k ∨ ∃ s_1, ((∃ t ∈ 𝒜, s_1 ⊆ t) ∧ #s_1 = k + 1) ∧ ∃ a ∈ s_1, s_1.erase a = s

Proof state:
case neg.intro.intro
α : Type u_2
inst✝ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s : Finset α
hs : #s = k
t : Finset α
ht : t ∈ 𝒜
hst✝ : s ⊆ t
h : s ∉ 𝒜
a : α
ha : a ∉ s
hst : insert a s ⊆ t
⊢ #(insert a s) = k + 1

Tactic:
rw [card_insert_of_not_mem ha, hs]

Result:
no goals

Proof state:
case h.mp
α : Type u_2
inst✝ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s : Finset α
⊢ (s ∈ 𝒜 ∧ #s = k ∨ ∃ s_1, ((∃ t ∈ 𝒜, s_1 ⊆ t) ∧ #s_1 = k + 1) ∧ ∃ a ∈ s_1, s_1.erase a = s) → (∃ t ∈ 𝒜, s ⊆ t) ∧ #s = k

Tactic:
rintro (h | ⟨s, ⟨⟨t, ht, hst⟩, hs⟩, a, ha, rfl⟩)

Result:
case h.mp.inl
α : Type u_2
inst✝ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s : Finset α
h : s ∈ 𝒜 ∧ #s = k
⊢ (∃ t ∈ 𝒜, s ⊆ t) ∧ #s = k

case h.mp.inr.intro.intro.intro.intro.intro.intro.intro
α : Type u_2
inst✝ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s : Finset α
hs : #s = k + 1
t : Finset α
ht : t ∈ 𝒜
hst : s ⊆ t
a : α
ha : a ∈ s
⊢ (∃ t ∈ 𝒜, s.erase a ⊆ t) ∧ #(s.erase a) = k

Proof state:
case h
α : Type u_2
inst✝ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s : Finset α
⊢ (s ∈ 𝒜 ∧ #s = k ∨ ∃ s_1, ((∃ t ∈ 𝒜, s_1 ⊆ t) ∧ #s_1 = k + 1) ∧ ∃ a ∈ s_1, s_1.erase a = s) ↔ (∃ t ∈ 𝒜, s ⊆ t) ∧ #s = k

Tactic:
constructor

Result:
case h.mp
α : Type u_2
inst✝ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s : Finset α
⊢ (s ∈ 𝒜 ∧ #s = k ∨ ∃ s_1, ((∃ t ∈ 𝒜, s_1 ⊆ t) ∧ #s_1 = k + 1) ∧ ∃ a ∈ s_1, s_1.erase a = s) → (∃ t ∈ 𝒜, s ⊆ t) ∧ #s = k

case h.mpr
α : Type u_2
inst✝ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s : Finset α
⊢ (∃ t ∈ 𝒜, s ⊆ t) ∧ #s = k → s ∈ 𝒜 ∧ #s = k ∨ ∃ s_1, ((∃ t ∈ 𝒜, s_1 ⊆ t) ∧ #s_1 = k + 1) ∧ ∃ a ∈ s_1, s_1.erase a = s

Proof state:
case h
α : Type u_2
inst✝ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s : Finset α
⊢ s ∈ 𝒜 # k ∪ ∂ (falling (k + 1) 𝒜) ↔ s ∈ falling k 𝒜

Tactic:
simp_rw [mem_union, mem_slice, mem_shadow_iff, mem_falling]

Result:
case h
α : Type u_2
inst✝ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s : Finset α
⊢ (s ∈ 𝒜 ∧ #s = k ∨ ∃ s_1, ((∃ t ∈ 𝒜, s_1 ⊆ t) ∧ #s_1 = k + 1) ∧ ∃ a ∈ s_1, s_1.erase a = s) ↔ (∃ t ∈ 𝒜, s ⊆ t) ∧ #s = k

Proof state:
case neg
α : Type u_2
inst✝ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s : Finset α
hs : #s = k
t : Finset α
ht : t ∈ 𝒜
hst : s ⊆ t
h : s ∉ 𝒜
⊢ s ∈ 𝒜 ∧ #s = k ∨ ∃ s_1, ((∃ t ∈ 𝒜, s_1 ⊆ t) ∧ #s_1 = k + 1) ∧ ∃ a ∈ s_1, s_1.erase a = s

Tactic:
obtain ⟨a, ha, hst⟩ := ssubset_iff.1 (ssubset_of_subset_of_ne hst (ht.ne_of_not_mem h).symm)

Result:
case neg.intro.intro
α : Type u_2
inst✝ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s : Finset α
hs : #s = k
t : Finset α
ht : t ∈ 𝒜
hst✝ : s ⊆ t
h : s ∉ 𝒜
a : α
ha : a ∉ s
hst : insert a s ⊆ t
⊢ s ∈ 𝒜 ∧ #s = k ∨ ∃ s_1, ((∃ t ∈ 𝒜, s_1 ⊆ t) ∧ #s_1 = k + 1) ∧ ∃ a ∈ s_1, s_1.erase a = s