Theorem: Finset.Colex.IsInitSeg.shadow (LeanCamCombi/KruskalKatona.lean)

State before:
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s t : Finset α
r : ℕ
inst✝ : Finite α
h₁ : IsInitSeg 𝒜 r
⊢ IsInitSeg (∂ 𝒜) (r - 1)
Tactic:
cases nonempty_fintype α
State after:
case intro
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s t : Finset α
r : ℕ
inst✝ : Finite α
h₁ : IsInitSeg 𝒜 r
val✝ : Fintype α
⊢ IsInitSeg (∂ 𝒜) (r - 1)

State before:
case intro
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s t : Finset α
r : ℕ
inst✝ : Finite α
h₁ : IsInitSeg 𝒜 r
val✝ : Fintype α
⊢ IsInitSeg (∂ 𝒜) (r - 1)
Tactic:
obtain rfl | hr := Nat.eq_zero_or_pos r
State after:
case intro.inl
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s t : Finset α
inst✝ : Finite α
val✝ : Fintype α
h₁ : IsInitSeg 𝒜 0
⊢ IsInitSeg (∂ 𝒜) (0 - 1)

case intro.inr
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s t : Finset α
r : ℕ
inst✝ : Finite α
h₁ : IsInitSeg 𝒜 r
val✝ : Fintype α
hr : r > 0
⊢ IsInitSeg (∂ 𝒜) (r - 1)

State before:
case intro.inr
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s t : Finset α
r : ℕ
inst✝ : Finite α
h₁ : IsInitSeg 𝒜 r
val✝ : Fintype α
hr : r > 0
⊢ IsInitSeg (∂ 𝒜) (r - 1)
Tactic:
obtain rfl | h𝒜 := 𝒜.eq_empty_or_nonempty
State after:
case intro.inr.inl
α : Type u_1
inst✝¹ : LinearOrder α
𝒜₁ 𝒜₂ : Finset (Finset α)
s t : Finset α
r : ℕ
inst✝ : Finite α
val✝ : Fintype α
hr : r > 0
h₁ : IsInitSeg ∅ r
⊢ IsInitSeg (∂ ∅) (r - 1)

case intro.inr.inr
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s t : Finset α
r : ℕ
inst✝ : Finite α
h₁ : IsInitSeg 𝒜 r
val✝ : Fintype α
hr : r > 0
h𝒜 : 𝒜.Nonempty
⊢ IsInitSeg (∂ 𝒜) (r - 1)

State before:
case intro.inr.inr
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s t : Finset α
r : ℕ
inst✝ : Finite α
h₁ : IsInitSeg 𝒜 r
val✝ : Fintype α
hr : r > 0
h𝒜 : 𝒜.Nonempty
⊢ IsInitSeg (∂ 𝒜) (r - 1)
Tactic:
obtain ⟨s, rfl, rfl⟩ := h₁.exists_initSeg h𝒜
State after:
case intro.inr.inr.intro.intro
α : Type u_1
inst✝¹ : LinearOrder α
𝒜₁ 𝒜₂ : Finset (Finset α)
s✝ t : Finset α
inst✝ : Finite α
val✝ : Fintype α
s : Finset α
hr : s.card > 0
h𝒜 : (initSeg s).Nonempty
h₁ : IsInitSeg (initSeg s) s.card
⊢ IsInitSeg (∂ (initSeg s)) (s.card - 1)

State before:
case intro.inr.inr.intro.intro
α : Type u_1
inst✝¹ : LinearOrder α
𝒜₁ 𝒜₂ : Finset (Finset α)
s✝ t : Finset α
inst✝ : Finite α
val✝ : Fintype α
s : Finset α
hr : s.card > 0
h𝒜 : (initSeg s).Nonempty
h₁ : IsInitSeg (initSeg s) s.card
⊢ IsInitSeg (∂ (initSeg s)) (s.card - 1)
Tactic:
rw [shadow_initSeg (card_pos.1 hr), ← card_erase_of_mem (min'_mem _ _)]
State after:
case intro.inr.inr.intro.intro
α : Type u_1
inst✝¹ : LinearOrder α
𝒜₁ 𝒜₂ : Finset (Finset α)
s✝ t : Finset α
inst✝ : Finite α
val✝ : Fintype α
s : Finset α
hr : s.card > 0
h𝒜 : (initSeg s).Nonempty
h₁ : IsInitSeg (initSeg s) s.card
⊢ IsInitSeg (initSeg (s.erase (s.min' ⋯))) (s.erase (s.min' ?m.16021)).card

α : Type u_1
inst✝¹ : LinearOrder α
𝒜₁ 𝒜₂ : Finset (Finset α)
s✝ t : Finset α
inst✝ : Finite α
val✝ : Fintype α
s : Finset α
hr : s.card > 0
h𝒜 : (initSeg s).Nonempty
h₁ : IsInitSeg (initSeg s) s.card
⊢ s.Nonempty

State before:
case intro.inr.inr.intro.intro
α : Type u_1
inst✝¹ : LinearOrder α
𝒜₁ 𝒜₂ : Finset (Finset α)
s✝ t : Finset α
inst✝ : Finite α
val✝ : Fintype α
s : Finset α
hr : s.card > 0
h𝒜 : (initSeg s).Nonempty
h₁ : IsInitSeg (initSeg s) s.card
⊢ IsInitSeg (initSeg (s.erase (s.min' ⋯))) (s.erase (s.min' ?m.16021)).card

α : Type u_1
inst✝¹ : LinearOrder α
𝒜₁ 𝒜₂ : Finset (Finset α)
s✝ t : Finset α
inst✝ : Finite α
val✝ : Fintype α
s : Finset α
hr : s.card > 0
h𝒜 : (initSeg s).Nonempty
h₁ : IsInitSeg (initSeg s) s.card
⊢ s.Nonempty
Tactic:
exact isInitSeg_initSeg
State after:
no goals

State before:
case intro.inl
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s t : Finset α
inst✝ : Finite α
val✝ : Fintype α
h₁ : IsInitSeg 𝒜 0
⊢ IsInitSeg (∂ 𝒜) (0 - 1)
Tactic:
have : 𝒜 ⊆ {∅} := fun s hs ↦ by rw [mem_singleton, ← Finset.card_eq_zero]; exact h₁.1 hs
State after:
case intro.inl
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s t : Finset α
inst✝ : Finite α
val✝ : Fintype α
h₁ : IsInitSeg 𝒜 0
this : 𝒜 ⊆ {∅}
⊢ IsInitSeg (∂ 𝒜) (0 - 1)

State before:
case intro.inl
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s t : Finset α
inst✝ : Finite α
val✝ : Fintype α
h₁ : IsInitSeg 𝒜 0
this : 𝒜 ⊆ {∅}
⊢ IsInitSeg (∂ 𝒜) (0 - 1)
Tactic:
have := shadow_monotone this
State after:
case intro.inl
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s t : Finset α
inst✝ : Finite α
val✝ : Fintype α
h₁ : IsInitSeg 𝒜 0
this✝ : 𝒜 ⊆ {∅}
this : ∂ 𝒜 ≤ ∂ {∅}
⊢ IsInitSeg (∂ 𝒜) (0 - 1)

State before:
case intro.inl
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s t : Finset α
inst✝ : Finite α
val✝ : Fintype α
h₁ : IsInitSeg 𝒜 0
this✝ : 𝒜 ⊆ {∅}
this : ∂ 𝒜 ≤ ∂ {∅}
⊢ IsInitSeg (∂ 𝒜) (0 - 1)
Tactic:
simp only [subset_empty, le_eq_subset, shadow_singleton_empty] at this
State after:
case intro.inl
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s t : Finset α
inst✝ : Finite α
val✝ : Fintype α
h₁ : IsInitSeg 𝒜 0
this✝ : 𝒜 ⊆ {∅}
this : ∂ 𝒜 = ∅
⊢ IsInitSeg (∂ 𝒜) (0 - 1)

State before:
case intro.inl
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s t : Finset α
inst✝ : Finite α
val✝ : Fintype α
h₁ : IsInitSeg 𝒜 0
this✝ : 𝒜 ⊆ {∅}
this : ∂ 𝒜 = ∅
⊢ IsInitSeg (∂ 𝒜) (0 - 1)
Tactic:
simp [this]
State after:
no goals

State before:
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s✝ t : Finset α
inst✝ : Finite α
val✝ : Fintype α
h₁ : IsInitSeg 𝒜 0
s : Finset α
hs : s ∈ 𝒜
⊢ s ∈ {∅}
Tactic:
rw [mem_singleton, ← Finset.card_eq_zero]
State after:
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s✝ t : Finset α
inst✝ : Finite α
val✝ : Fintype α
h₁ : IsInitSeg 𝒜 0
s : Finset α
hs : s ∈ 𝒜
⊢ s.card = 0

State before:
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s✝ t : Finset α
inst✝ : Finite α
val✝ : Fintype α
h₁ : IsInitSeg 𝒜 0
s : Finset α
hs : s ∈ 𝒜
⊢ s.card = 0
Tactic:
exact h₁.1 hs
State after:
no goals

State before:
case intro.inr.inl
α : Type u_1
inst✝¹ : LinearOrder α
𝒜₁ 𝒜₂ : Finset (Finset α)
s t : Finset α
r : ℕ
inst✝ : Finite α
val✝ : Fintype α
hr : r > 0
h₁ : IsInitSeg ∅ r
⊢ IsInitSeg (∂ ∅) (r - 1)
Tactic:
simp
State after:
no goals