-- Mathlib/Combinatorics/SetFamily/KruskalKatona.lean
/-- This is important for iterating Kruskal-Katona: the shadow of an initial segment is also an
initial segment. -/
lemma shadow_initSeg [Fintype α] (hs : s.Nonempty) :
    ∂ (initSeg s) = initSeg (erase s <| min' s hs)

Proof state:
case h.mpr.inl
α : Type u_1
inst✝¹ : LinearOrder α
s : Finset α
inst✝ : Fintype α
hs : s.Nonempty
cards' : #(s.erase (s.min' hs)) = #(s.erase (s.min' hs))
⊢ ∃ a ∉ s.erase (s.min' hs),
    #s = #(insert a (s.erase (s.min' hs))) ∧
      (insert a (s.erase (s.min' hs)) = s ∨
        ∃ w ∈ s,
          w ∉ insert a (s.erase (s.min' hs)) ∧ ∀ ⦃a_1 : α⦄, w < a_1 → (a_1 ∈ insert a (s.erase (s.min' hs)) ↔ a_1 ∈ s))

Tactic:
refine ⟨min' s hs, not_mem_erase _ _, ?_⟩

Result:
case h.mpr.inl
α : Type u_1
inst✝¹ : LinearOrder α
s : Finset α
inst✝ : Fintype α
hs : s.Nonempty
cards' : #(s.erase (s.min' hs)) = #(s.erase (s.min' hs))
⊢ #s = #(insert (s.min' hs) (s.erase (s.min' hs))) ∧
    (insert (s.min' hs) (s.erase (s.min' hs)) = s ∨
      ∃ w ∈ s,
        w ∉ insert (s.min' hs) (s.erase (s.min' hs)) ∧
          ∀ ⦃a : α⦄, w < a → (a ∈ insert (s.min' hs) (s.erase (s.min' hs)) ↔ a ∈ s))

Proof state:
case h.mpr.inr.intro.intro.intro
α : Type u_1
inst✝¹ : LinearOrder α
s : Finset α
inst✝ : Fintype α
hs : s.Nonempty
t : Finset α
cards' : #(s.erase (s.min' hs)) = #t
k : α
hks : k ∈ s.erase (s.min' hs)
hkt : k ∉ t
z : ∀ ⦃a : α⦄, k < a → (a ∈ t ↔ a ∈ s.erase (s.min' hs))
j : α := tᶜ.min' ⋯
hjk : j ≤ k
this : j ∉ t
hcard : #s = #(insert j t)
⊢ ∃ a ∉ t,
    #s = #(insert a t) ∧
      (insert a t = s ∨ ∃ w ∈ s, w ∉ insert a t ∧ ∀ ⦃a_1 : α⦄, w < a_1 → (a_1 ∈ insert a t ↔ a_1 ∈ s))

Tactic:
refine ⟨j, ‹_›, hcard, ?_⟩

Result:
case h.mpr.inr.intro.intro.intro
α : Type u_1
inst✝¹ : LinearOrder α
s : Finset α
inst✝ : Fintype α
hs : s.Nonempty
t : Finset α
cards' : #(s.erase (s.min' hs)) = #t
k : α
hks : k ∈ s.erase (s.min' hs)
hkt : k ∉ t
z : ∀ ⦃a : α⦄, k < a → (a ∈ t ↔ a ∈ s.erase (s.min' hs))
j : α := tᶜ.min' ⋯
hjk : j ≤ k
this : j ∉ t
hcard : #s = #(insert j t)
⊢ insert j t = s ∨ ∃ w ∈ s, w ∉ insert j t ∧ ∀ ⦃a : α⦄, w < a → (a ∈ insert j t ↔ a ∈ s)

Proof state:
case h.mp.intro.intro.intro.left
α : Type u_1
inst✝¹ : LinearOrder α
s : Finset α
inst✝ : Fintype α
hs : s.Nonempty
t : Finset α
a : α
ha : a ∉ t
hst : #s = #(insert a t)
hts : { ofColex := insert a t } ≤ { ofColex := s }
⊢ #(s.erase (s.min' hs)) = #t

Tactic:
rw [card_erase_of_mem (min'_mem _ _), hst, card_insert_of_not_mem ha, add_tsub_cancel_right]

Result:
no goals

Proof state:
case h.mp
α : Type u_1
inst✝¹ : LinearOrder α
s : Finset α
inst✝ : Fintype α
hs : s.Nonempty
t : Finset α
⊢ (∃ a ∉ t, #s = #(insert a t) ∧ { ofColex := insert a t } ≤ { ofColex := s }) →
    #(s.erase (s.min' hs)) = #t ∧ { ofColex := t } ≤ { ofColex := s.erase (s.min' hs) }

Tactic:
rintro ⟨a, ha, hst, hts⟩

Result:
case h.mp.intro.intro.intro
α : Type u_1
inst✝¹ : LinearOrder α
s : Finset α
inst✝ : Fintype α
hs : s.Nonempty
t : Finset α
a : α
ha : a ∉ t
hst : #s = #(insert a t)
hts : { ofColex := insert a t } ≤ { ofColex := s }
⊢ #(s.erase (s.min' hs)) = #t ∧ { ofColex := t } ≤ { ofColex := s.erase (s.min' hs) }

Proof state:
α : Type u_1
inst✝¹ : LinearOrder α
s : Finset α
inst✝ : Fintype α
hs : s.Nonempty
t : Finset α
cards' : #(s.erase (s.min' hs)) = #t
k : α
hks : k ∈ s.erase (s.min' hs)
hkt : k ∉ t
z : ∀ ⦃a : α⦄, k < a → (a ∈ t ↔ a ∈ s.erase (s.min' hs))
j : α := tᶜ.min' ⋯
hjk : j ≤ k
this : j ∉ t
hcard : #s = #(insert j t)
r₁ : j = k
a : α
ha : a ∈ s
gt : a < j
x✝ : a ∉ t
⊢ a ∈ tᶜ

Tactic:
rwa [mem_compl]

Result:
no goals

Proof state:
case h.mpr.inr.intro.intro.intro.inr
α : Type u_1
inst✝¹ : LinearOrder α
s : Finset α
inst✝ : Fintype α
hs : s.Nonempty
t : Finset α
cards' : #(s.erase (s.min' hs)) = #t
k : α
hks : k ∈ s.erase (s.min' hs)
hkt : k ∉ t
z : ∀ ⦃a : α⦄, k < a → (a ∈ t ↔ a ∈ s.erase (s.min' hs))
j : α := tᶜ.min' ⋯
hjk : j ≤ k
this : j ∉ t
hcard : #s = #(insert j t)
r₁ : j = k
⊢ insert j t = s ∨ ∃ w ∈ s, w ∉ insert j t ∧ ∀ ⦃a : α⦄, w < a → (a ∈ insert j t ↔ a ∈ s)

Tactic:
refine Or.inl (eq_of_subset_of_card_le (fun a ha ↦ ?_) hcard.ge).symm

Result:
case h.mpr.inr.intro.intro.intro.inr
α : Type u_1
inst✝¹ : LinearOrder α
s : Finset α
inst✝ : Fintype α
hs : s.Nonempty
t : Finset α
cards' : #(s.erase (s.min' hs)) = #t
k : α
hks : k ∈ s.erase (s.min' hs)
hkt : k ∉ t
z : ∀ ⦃a : α⦄, k < a → (a ∈ t ↔ a ∈ s.erase (s.min' hs))
j : α := tᶜ.min' ⋯
hjk : j ≤ k
this : j ∉ t
hcard : #s = #(insert j t)
r₁ : j = k
a : α
ha : a ∈ s
⊢ a ∈ insert j t

Proof state:
case h.mpr.inr.intro.intro.intro
α : Type u_1
inst✝¹ : LinearOrder α
s : Finset α
inst✝ : Fintype α
hs : s.Nonempty
t : Finset α
cards' : #(s.erase (s.min' hs)) = #t
k : α
hks : k ∈ s.erase (s.min' hs)
hkt : k ∉ t
z : ∀ ⦃a : α⦄, k < a → (a ∈ t ↔ a ∈ s.erase (s.min' hs))
j : α := tᶜ.min' ⋯
hjk : j ≤ k
this : j ∉ t
⊢ ∃ a ∉ t,
    #s = #(insert a t) ∧
      (insert a t = s ∨ ∃ w ∈ s, w ∉ insert a t ∧ ∀ ⦃a_1 : α⦄, w < a_1 → (a_1 ∈ insert a t ↔ a_1 ∈ s))

Tactic:
have hcard : #s = #(insert j t) := by
  rw [card_insert_of_not_mem ‹j ∉ t›, ← ‹_ = #t›, card_erase_add_one (min'_mem _ _)]

Result:
case h.mpr.inr.intro.intro.intro
α : Type u_1
inst✝¹ : LinearOrder α
s : Finset α
inst✝ : Fintype α
hs : s.Nonempty
t : Finset α
cards' : #(s.erase (s.min' hs)) = #t
k : α
hks : k ∈ s.erase (s.min' hs)
hkt : k ∉ t
z : ∀ ⦃a : α⦄, k < a → (a ∈ t ↔ a ∈ s.erase (s.min' hs))
j : α := tᶜ.min' ⋯
hjk : j ≤ k
this : j ∉ t
hcard : #s = #(insert j t)
⊢ ∃ a ∉ t,
    #s = #(insert a t) ∧
      (insert a t = s ∨ ∃ w ∈ s, w ∉ insert a t ∧ ∀ ⦃a_1 : α⦄, w < a_1 → (a_1 ∈ insert a t ↔ a_1 ∈ s))

Proof state:
case h.mpr.inr.intro.intro.intro.inr.inr.inl
α : Type u_1
inst✝¹ : LinearOrder α
s : Finset α
inst✝ : Fintype α
hs : s.Nonempty
t : Finset α
cards' : #(s.erase (s.min' hs)) = #t
k : α
hks : k ∈ s.erase (s.min' hs)
hkt : k ∉ t
z : ∀ ⦃a : α⦄, k < a → (a ∈ t ↔ a ∈ s.erase (s.min' hs))
j : α := tᶜ.min' ⋯
hjk : j ≤ k
this : j ∉ t
hcard : #s = #(insert j t)
r₁ : j = k
ha : k ∈ s
⊢ k ∈ insert k t

Tactic:
apply mem_insert_self

Result:
no goals

Proof state:
case h
α : Type u_1
inst✝¹ : LinearOrder α
s : Finset α
inst✝ : Fintype α
hs : s.Nonempty
t : Finset α
⊢ (∃ a ∉ t, #s = #(insert a t) ∧ { ofColex := insert a t } ≤ { ofColex := s }) ↔
    #(s.erase (s.min' hs)) = #t ∧ { ofColex := t } ≤ { ofColex := s.erase (s.min' hs) }

Tactic:
constructor

Result:
case h.mp
α : Type u_1
inst✝¹ : LinearOrder α
s : Finset α
inst✝ : Fintype α
hs : s.Nonempty
t : Finset α
⊢ (∃ a ∉ t, #s = #(insert a t) ∧ { ofColex := insert a t } ≤ { ofColex := s }) →
    #(s.erase (s.min' hs)) = #t ∧ { ofColex := t } ≤ { ofColex := s.erase (s.min' hs) }

case h.mpr
α : Type u_1
inst✝¹ : LinearOrder α
s : Finset α
inst✝ : Fintype α
hs : s.Nonempty
t : Finset α
⊢ #(s.erase (s.min' hs)) = #t ∧ { ofColex := t } ≤ { ofColex := s.erase (s.min' hs) } →
    ∃ a ∉ t, #s = #(insert a t) ∧ { ofColex := insert a t } ≤ { ofColex := s }